Proofgold Asset

Definition False^False := ∀ x0 : ο . x0
Theorem 08f54..^t3_xregular : ∀ x0 : ι → ι . ∀ x1 : ι → ι → ι . ∀ x2 : ι → ο . ∀ x3 : ι → ι . ∀ x4 : ι → ι → ι . ∀ x5 : ι → ι → ο . ∀ x6 : ι → ι . ∀ x7 : ι → ι → ι . ∀ x8 . ∀ x9 x10 : ι → ι . ∀ x11 x12 x13 . ∀ x14 : ι → ι . ∀ x15 : ι → ι → ι . ∀ x16 : ι → ι → ι → ι . ∀ x17 : ι → ι → ο . ∀ x18 : ι → ι → ι → ι . ∀ x19 : ι → ι → ι . (∀ x20 x21 x22 . (x21 = x19 x20 x22 ⟶ False) ⟶ x17 (x18 x20 x22 x21) x21 ⟶ x17 (x18 x20 x22 x21) x20 ⟶ False) ⟶ (∀ x20 x21 x22 . (x21 = x19 x22 x20 ⟶ False) ⟶ x17 (x18 x22 x20 x21) x21 ⟶ x17 (x18 x22 x20 x21) x20 ⟶ False) ⟶ (∀ x20 x21 x22 . (x21 = x19 x20 x22 ⟶ False) ⟶ (x17 (x18 x20 x22 x21) x21 ⟶ False) ⟶ (x17 (x18 x20 x22 x21) x22 ⟶ False) ⟶ (x17 (x18 x20 x22 x21) x20 ⟶ False) ⟶ False) ⟶ (∀ x20 x21 x22 . (x21 = x0 x22 ⟶ False) ⟶ x17 x20 x22 ⟶ x17 (x1 x22 x21) x20 ⟶ x17 (x1 x22 x21) x21 ⟶ False) ⟶ (∀ x20 x21 x22 . (x17 (x16 x20 x21 x22) x20 ⟶ False) ⟶ x21 = x0 x20 ⟶ x17 x22 x21 ⟶ False) ⟶ (∀ x20 x21 x22 . (x17 x22 (x16 x20 x21 x22) ⟶ False) ⟶ x21 = x0 x20 ⟶ x17 x22 x21 ⟶ False) ⟶ (∀ x20 x21 . (x21 = x0 x20 ⟶ False) ⟶ (x17 (x1 x20 x21) x21 ⟶ False) ⟶ (x17 (x1 x20 x21) (x15 x20 x21) ⟶ False) ⟶ False) ⟶ (∀ x20 x21 . (x2 x21 ⟶ False) ⟶ x17 x20 (x3 x21) ⟶ x5 (x4 x21 x20) x21 ⟶ False) ⟶ (∀ x20 x21 x22 . (x2 x22 ⟶ False) ⟶ (x5 x20 x22 ⟶ False) ⟶ (x17 x21 (x3 x22) ⟶ False) ⟶ x17 x20 x21 ⟶ x17 x21 (x0 x22) ⟶ False) ⟶ (∀ x20 x21 . (x2 x21 ⟶ False) ⟶ (x5 x20 x21 ⟶ False) ⟶ (x17 x20 (x6 x21) ⟶ False) ⟶ x17 x20 (x0 (x0 x21)) ⟶ False) ⟶ (∀ x20 x21 . (x21 = x0 x20 ⟶ False) ⟶ (x17 (x1 x20 x21) x21 ⟶ False) ⟶ (x17 (x15 x20 x21) x20 ⟶ False) ⟶ False) ⟶ (∀ x20 x21 x22 . (x5 x22 (x19 x21 x20) ⟶ False) ⟶ x5 x22 x20 ⟶ x5 x22 x21 ⟶ False) ⟶ (∀ x20 x21 x22 . (x5 x21 x22 ⟶ False) ⟶ x5 x21 (x19 x22 x20) ⟶ False) ⟶ (∀ x20 x21 x22 . (x5 x21 x22 ⟶ False) ⟶ x5 x21 (x19 x20 x22) ⟶ False) ⟶ (∀ x20 x21 . (x2 x21 ⟶ False) ⟶ (x17 (x4 x21 x20) x20 ⟶ False) ⟶ x17 x20 (x3 x21) ⟶ False) ⟶ (∀ x20 x21 x22 x23 . (x17 x22 x23 ⟶ False) ⟶ (x17 x22 x20 ⟶ False) ⟶ x21 = x19 x20 x23 ⟶ x17 x22 x21 ⟶ False) ⟶ (∀ x20 x21 . (x2 x21 ⟶ False) ⟶ (x17 x20 (x0 (x0 x21)) ⟶ False) ⟶ x17 x20 (x6 x21) ⟶ False) ⟶ (∀ x20 x21 x22 x23 . (x17 x22 x23 ⟶ False) ⟶ x23 = x0 x20 ⟶ x17 x21 x20 ⟶ x17 x22 x21 ⟶ False) ⟶ (∀ x20 x21 x22 . x17 x21 x22 ⟶ x17 x21 x20 ⟶ x5 x20 x22 ⟶ False) ⟶ (∀ x20 x21 x22 x23 . (x17 x22 x23 ⟶ False) ⟶ x23 = x19 x20 x21 ⟶ x17 x22 x20 ⟶ False) ⟶ (∀ x20 x21 x22 x23 . (x17 x22 x23 ⟶ False) ⟶ x23 = x19 x21 x20 ⟶ x17 x22 x20 ⟶ False) ⟶ (∀ x20 x21 . (x2 x21 ⟶ False) ⟶ x5 x20 x21 ⟶ x17 x20 (x6 x21) ⟶ False) ⟶ (∀ x20 x21 . (x2 x21 ⟶ False) ⟶ (x17 x20 (x0 x21) ⟶ False) ⟶ x17 x20 (x3 x21) ⟶ False) ⟶ (∀ x20 x21 . (x5 x20 x21 ⟶ False) ⟶ (x17 (x7 x20 x21) x20 ⟶ False) ⟶ False) ⟶ (∀ x20 x21 . (x5 x21 x20 ⟶ False) ⟶ (x17 (x7 x21 x20) x20 ⟶ False) ⟶ False) ⟶ (∀ x20 x21 . (x2 x21 ⟶ False) ⟶ x2 (x19 x21 x20) ⟶ False) ⟶ (∀ x20 x21 . (x2 x21 ⟶ False) ⟶ x2 (x19 x20 x21) ⟶ False) ⟶ (∀ x20 . x17 x20 x8 ⟶ x5 (x9 x20) x8 ⟶ False) ⟶ (∀ x20 . (x17 (x9 x20) (x14 x20) ⟶ False) ⟶ x17 x20 x8 ⟶ False) ⟶ (∀ x20 x21 . x17 x20 x21 ⟶ x17 x21 x20 ⟶ False) ⟶ (∀ x20 . (x17 (x14 x20) x20 ⟶ False) ⟶ x17 x20 x8 ⟶ False) ⟶ (∀ x20 x21 . (x5 x20 x21 ⟶ False) ⟶ x5 x21 x20 ⟶ False) ⟶ (∀ x20 x21 . x2 x21 ⟶ x17 x20 x21 ⟶ False) ⟶ (∀ x20 . (x2 x20 ⟶ False) ⟶ (x5 (x10 x20) x20 ⟶ False) ⟶ False) ⟶ (∀ x20 . (x2 x20 ⟶ False) ⟶ (x17 (x10 x20) x20 ⟶ False) ⟶ False) ⟶ (∀ x20 x21 . (x21 = x20 ⟶ False) ⟶ x2 x20 ⟶ x2 x21 ⟶ False) ⟶ (∀ x20 . (x20 = x13 ⟶ False) ⟶ x2 x20 ⟶ False) ⟶ (x2 x11 ⟶ False) ⟶ (x2 x8 ⟶ False) ⟶ (∀ x20 x21 x22 . (x19 (x19 x22 x20) x21 = x19 x22 (x19 x20 x21) ⟶ False) ⟶ False) ⟶ (∀ x20 x21 . (x19 x21 x20 = x19 x20 x21 ⟶ False) ⟶ False) ⟶ (∀ x20 . (x19 x20 x20 = x20 ⟶ False) ⟶ False) ⟶ (∀ x20 . (x19 x20 x13 = x20 ⟶ False) ⟶ False) ⟶ ((x2 x12 ⟶ False) ⟶ False) ⟶ ((x2 x13 ⟶ False) ⟶ False) ⟶ False (proof)
Theorem ac28c..^t4_xregular : ∀ x0 : ι → ι . ∀ x1 : ι → ι → ι . ∀ x2 : ι → ι . ∀ x3 x4 : ι → ι → ι . ∀ x5 x6 x7 : ι → ι . ∀ x8 x9 x10 . ∀ x11 : ι → ι . ∀ x12 . ∀ x13 x14 x15 : ι → ι → ι . ∀ x16 : ι → ι . ∀ x17 : ι → ι → ο . ∀ x18 : ι → ι . ∀ x19 : ι → ο . ∀ x20 : ι → ι → ι → ι . ∀ x21 : ι → ι → ο . ∀ x22 : ι → ι → ι → ι . ∀ x23 : ι → ι → ι . (∀ x24 x25 x26 . (x25 = x23 x24 x26 ⟶ False) ⟶ x21 (x22 x24 x26 x25) x25 ⟶ x21 (x22 x24 x26 x25) x24 ⟶ False) ⟶ (∀ x24 x25 x26 . (x25 = x23 x26 x24 ⟶ False) ⟶ x21 (x22 x26 x24 x25) x25 ⟶ x21 (x22 x26 x24 x25) x24 ⟶ False) ⟶ (∀ x24 x25 x26 . (x25 = x23 x24 x26 ⟶ False) ⟶ (x21 (x22 x24 x26 x25) x25 ⟶ False) ⟶ (x21 (x22 x24 x26 x25) x26 ⟶ False) ⟶ (x21 (x22 x24 x26 x25) x24 ⟶ False) ⟶ False) ⟶ (∀ x24 x25 x26 . (x25 = x0 x26 ⟶ False) ⟶ x21 x24 x26 ⟶ x21 (x1 x26 x25) x24 ⟶ x21 (x1 x26 x25) x25 ⟶ False) ⟶ (∀ x24 x25 x26 . (x21 (x20 x24 x25 x26) x24 ⟶ False) ⟶ x25 = x0 x24 ⟶ x21 x26 x25 ⟶ False) ⟶ (∀ x24 x25 x26 . (x21 x26 (x20 x24 x25 x26) ⟶ False) ⟶ x25 = x0 x24 ⟶ x21 x26 x25 ⟶ False) ⟶ (∀ x24 x25 . (x19 x25 ⟶ False) ⟶ (x17 x24 x25 ⟶ False) ⟶ (x21 x24 (x18 x25) ⟶ False) ⟶ x21 x24 (x0 (x0 (x0 x25))) ⟶ False) ⟶ (∀ x24 x25 x26 x27 . (x19 x27 ⟶ False) ⟶ (x17 x24 x27 ⟶ False) ⟶ (x21 x26 (x2 x27) ⟶ False) ⟶ x21 x25 x26 ⟶ x21 x24 x25 ⟶ x21 x26 (x0 x27) ⟶ False) ⟶ (∀ x24 x25 x26 . (x19 x26 ⟶ False) ⟶ (x17 x24 x26 ⟶ False) ⟶ (x21 x25 (x16 x26) ⟶ False) ⟶ x21 x24 x25 ⟶ x21 x25 (x0 (x0 x26)) ⟶ False) ⟶ (∀ x24 x25 . (x25 = x0 x24 ⟶ False) ⟶ (x21 (x1 x24 x25) x25 ⟶ False) ⟶ (x21 (x1 x24 x25) (x3 x24 x25) ⟶ False) ⟶ False) ⟶ (∀ x24 x25 . (x19 x25 ⟶ False) ⟶ (x21 (x15 x25 x24) (x14 x25 x24) ⟶ False) ⟶ x21 x24 (x2 x25) ⟶ False) ⟶ (∀ x24 x25 . (x19 x25 ⟶ False) ⟶ x21 x24 (x16 x25) ⟶ x17 (x4 x25 x24) x25 ⟶ False) ⟶ (∀ x24 x25 . (x19 x25 ⟶ False) ⟶ x21 x24 (x2 x25) ⟶ x17 (x15 x25 x24) x25 ⟶ False) ⟶ (∀ x24 x25 . (x19 x25 ⟶ False) ⟶ (x21 x24 (x0 (x0 (x0 x25))) ⟶ False) ⟶ x21 x24 (x18 x25) ⟶ False) ⟶ (∀ x24 x25 . (x25 = x0 x24 ⟶ False) ⟶ (x21 (x1 x24 x25) x25 ⟶ False) ⟶ (x21 (x3 x24 x25) x24 ⟶ False) ⟶ False) ⟶ (∀ x24 x25 x26 . (x17 x26 (x23 x25 x24) ⟶ False) ⟶ x17 x26 x24 ⟶ x17 x26 x25 ⟶ False) ⟶ (∀ x24 x25 x26 . (x17 x25 x26 ⟶ False) ⟶ x17 x25 (x23 x26 x24) ⟶ False) ⟶ (∀ x24 x25 x26 . (x17 x25 x26 ⟶ False) ⟶ x17 x25 (x23 x24 x26) ⟶ False) ⟶ (∀ x24 x25 . (x19 x25 ⟶ False) ⟶ (x21 (x4 x25 x24) x24 ⟶ False) ⟶ x21 x24 (x16 x25) ⟶ False) ⟶ (∀ x24 x25 . (x19 x25 ⟶ False) ⟶ (x21 (x14 x25 x24) x24 ⟶ False) ⟶ x21 x24 (x2 x25) ⟶ False) ⟶ (∀ x24 x25 x26 x27 . (x21 x26 x27 ⟶ False) ⟶ (x21 x26 x24 ⟶ False) ⟶ x25 = x23 x24 x27 ⟶ x21 x26 x25 ⟶ False) ⟶ (∀ x24 x25 . (x19 x25 ⟶ False) ⟶ (x21 x24 (x0 (x0 x25)) ⟶ False) ⟶ x21 x24 (x16 x25) ⟶ False) ⟶ (∀ x24 x25 x26 x27 . (x21 x26 x27 ⟶ False) ⟶ x27 = x0 x24 ⟶ x21 x25 x24 ⟶ x21 x26 x25 ⟶ False) ⟶ (∀ x24 x25 x26 . x21 x25 x26 ⟶ x21 x25 x24 ⟶ x17 x24 x26 ⟶ False) ⟶ (∀ x24 x25 x26 x27 . (x21 x26 x27 ⟶ False) ⟶ x27 = x23 x24 x25 ⟶ x21 x26 x24 ⟶ False) ⟶ (∀ x24 x25 x26 x27 . (x21 x26 x27 ⟶ False) ⟶ x27 = x23 x25 x24 ⟶ x21 x26 x24 ⟶ False) ⟶ (∀ x24 x25 . (x19 x25 ⟶ False) ⟶ x17 x24 x25 ⟶ x21 x24 (x18 x25) ⟶ False) ⟶ (∀ x24 x25 . (x19 x25 ⟶ False) ⟶ (x21 x24 (x0 x25) ⟶ False) ⟶ x21 x24 (x2 x25) ⟶ False) ⟶ (∀ x24 x25 . (x17 x24 x25 ⟶ False) ⟶ (x21 (x13 x24 x25) x24 ⟶ False) ⟶ False) ⟶ (∀ x24 x25 . (x17 x25 x24 ⟶ False) ⟶ (x21 (x13 x25 x24) x24 ⟶ False) ⟶ False) ⟶ (∀ x24 x25 . (x19 x25 ⟶ False) ⟶ x19 (x23 x25 x24) ⟶ False) ⟶ (∀ x24 x25 . (x19 x25 ⟶ False) ⟶ x19 (x23 x24 x25) ⟶ False) ⟶ (∀ x24 . x21 x24 x12 ⟶ x17 (x11 x24) x12 ⟶ False) ⟶ (∀ x24 . (x21 (x6 x24) (x5 x24) ⟶ False) ⟶ x21 x24 x12 ⟶ False) ⟶ (∀ x24 . (x21 (x11 x24) (x6 x24) ⟶ False) ⟶ x21 x24 x12 ⟶ False) ⟶ (∀ x24 x25 . x21 x24 x25 ⟶ x21 x25 x24 ⟶ False) ⟶ (∀ x24 . (x21 (x5 x24) x24 ⟶ False) ⟶ x21 x24 x12 ⟶ False) ⟶ (∀ x24 x25 . (x17 x24 x25 ⟶ False) ⟶ x17 x25 x24 ⟶ False) ⟶ (∀ x24 x25 . x19 x25 ⟶ x21 x24 x25 ⟶ False) ⟶ (∀ x24 . (x19 x24 ⟶ False) ⟶ (x17 (x7 x24) x24 ⟶ False) ⟶ False) ⟶ (∀ x24 . (x19 x24 ⟶ False) ⟶ (x21 (x7 x24) x24 ⟶ False) ⟶ False) ⟶ (∀ x24 x25 . (x25 = x24 ⟶ False) ⟶ x19 x24 ⟶ x19 x25 ⟶ False) ⟶ (∀ x24 . (x24 = x10 ⟶ False) ⟶ x19 x24 ⟶ False) ⟶ (x19 x8 ⟶ False) ⟶ (x19 x12 ⟶ False) ⟶ (∀ x24 x25 x26 . (x23 (x23 x26 x24) x25 = x23 x26 (x23 x24 x25) ⟶ False) ⟶ False) ⟶ (∀ x24 x25 . (x23 x25 x24 = x23 x24 x25 ⟶ False) ⟶ False) ⟶ (∀ x24 . (x23 x24 x24 = x24 ⟶ False) ⟶ False) ⟶ (∀ x24 . (x23 x24 x10 = x24 ⟶ False) ⟶ False) ⟶ ((x19 x9 ⟶ False) ⟶ False) ⟶ ((x19 x10 ⟶ False) ⟶ False) ⟶ False (proof)
Theorem 2faed..^t5_xregular : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι . ∀ x3 : ι → ι → ο . ∀ x4 : ι → ι → ι → ι . ∀ x5 x6 : ι → ι . ∀ x7 x8 x9 x10 : ι → ι → ι . ∀ x11 x12 : ι → ι . ∀ x13 x14 x15 . ∀ x16 x17 x18 : ι → ι . ∀ x19 . ∀ x20 x21 x22 x23 : ι → ι → ι . ∀ x24 : ι → ι . ∀ x25 : ι → ι → ι . ∀ x26 : ι → ι → ο . ∀ x27 : ι → ι → ι → ι . ∀ x28 : ι → ι → ι . (∀ x29 x30 x31 . (x30 = x28 x29 x31 ⟶ False) ⟶ x26 (x27 x29 x31 x30) x30 ⟶ x26 (x27 x29 x31 x30) x29 ⟶ False) ⟶ (∀ x29 x30 x31 . (x30 = x28 x31 x29 ⟶ False) ⟶ x26 (x27 x31 x29 x30) x30 ⟶ x26 (x27 x31 x29 x30) x29 ⟶ False) ⟶ (∀ x29 x30 x31 . (x30 = x28 x29 x31 ⟶ False) ⟶ (x26 (x27 x29 x31 x30) x30 ⟶ False) ⟶ (x26 (x27 x29 x31 x30) x31 ⟶ False) ⟶ (x26 (x27 x29 x31 x30) x29 ⟶ False) ⟶ False) ⟶ (∀ x29 x30 . (x0 x30 ⟶ False) ⟶ (x3 x29 x30 ⟶ False) ⟶ (x26 x29 (x2 x30) ⟶ False) ⟶ x26 x29 (x1 (x1 (x1 (x1 x30)))) ⟶ False) ⟶ (∀ x29 x30 x31 . (x30 = x1 x31 ⟶ False) ⟶ x26 x29 x31 ⟶ x26 (x25 x31 x30) x29 ⟶ x26 (x25 x31 x30) x30 ⟶ False) ⟶ (∀ x29 x30 x31 . (x26 (x4 x29 x30 x31) x29 ⟶ False) ⟶ x30 = x1 x29 ⟶ x26 x31 x30 ⟶ False) ⟶ (∀ x29 x30 x31 . (x26 x31 (x4 x29 x30 x31) ⟶ False) ⟶ x30 = x1 x29 ⟶ x26 x31 x30 ⟶ False) ⟶ (∀ x29 x30 x31 . (x0 x31 ⟶ False) ⟶ (x3 x29 x31 ⟶ False) ⟶ (x26 x30 (x5 x31) ⟶ False) ⟶ x26 x29 x30 ⟶ x26 x30 (x1 (x1 (x1 x31))) ⟶ False) ⟶ (∀ x29 x30 . (x0 x30 ⟶ False) ⟶ (x26 x29 (x1 (x1 (x1 (x1 x30)))) ⟶ False) ⟶ x26 x29 (x2 x30) ⟶ False) ⟶ (∀ x29 x30 x31 x32 x33 . (x0 x33 ⟶ False) ⟶ (x3 x29 x33 ⟶ False) ⟶ (x26 x32 (x6 x33) ⟶ False) ⟶ x26 x30 x32 ⟶ x26 x31 x30 ⟶ x26 x29 x31 ⟶ x26 x32 (x1 x33) ⟶ False) ⟶ (∀ x29 x30 x31 x32 . (x0 x32 ⟶ False) ⟶ (x3 x29 x32 ⟶ False) ⟶ (x26 x31 (x24 x32) ⟶ False) ⟶ x26 x30 x31 ⟶ x26 x29 x30 ⟶ x26 x31 (x1 (x1 x32)) ⟶ False) ⟶ (∀ x29 x30 . (x30 = x1 x29 ⟶ False) ⟶ (x26 (x25 x29 x30) x30 ⟶ False) ⟶ (x26 (x25 x29 x30) (x7 x29 x30) ⟶ False) ⟶ False) ⟶ (∀ x29 x30 . (x0 x30 ⟶ False) ⟶ (x26 (x23 x30 x29) (x22 x30 x29) ⟶ False) ⟶ x26 x29 (x24 x30) ⟶ False) ⟶ (∀ x29 x30 . (x0 x30 ⟶ False) ⟶ (x26 (x8 x30 x29) (x9 x30 x29) ⟶ False) ⟶ x26 x29 (x6 x30) ⟶ False) ⟶ (∀ x29 x30 . (x0 x30 ⟶ False) ⟶ (x26 (x21 x30 x29) (x8 x30 x29) ⟶ False) ⟶ x26 x29 (x6 x30) ⟶ False) ⟶ (∀ x29 x30 . (x0 x30 ⟶ False) ⟶ x26 x29 (x5 x30) ⟶ x3 (x10 x30 x29) x30 ⟶ False) ⟶ (∀ x29 x30 . (x0 x30 ⟶ False) ⟶ x26 x29 (x24 x30) ⟶ x3 (x23 x30 x29) x30 ⟶ False) ⟶ (∀ x29 x30 . (x0 x30 ⟶ False) ⟶ x26 x29 (x6 x30) ⟶ x3 (x21 x30 x29) x30 ⟶ False) ⟶ (∀ x29 x30 . (x0 x30 ⟶ False) ⟶ (x26 x29 (x1 (x1 (x1 x30))) ⟶ False) ⟶ x26 x29 (x5 x30) ⟶ False) ⟶ (∀ x29 x30 . (x30 = x1 x29 ⟶ False) ⟶ (x26 (x25 x29 x30) x30 ⟶ False) ⟶ (x26 (x7 x29 x30) x29 ⟶ False) ⟶ False) ⟶ (∀ x29 x30 x31 . (x3 x31 (x28 x30 x29) ⟶ False) ⟶ x3 x31 x29 ⟶ x3 x31 x30 ⟶ False) ⟶ (∀ x29 x30 x31 . (x3 x30 x31 ⟶ False) ⟶ x3 x30 (x28 x31 x29) ⟶ False) ⟶ (∀ x29 x30 x31 . (x3 x30 x31 ⟶ False) ⟶ x3 x30 (x28 x29 x31) ⟶ False) ⟶ (∀ x29 x30 . (x0 x30 ⟶ False) ⟶ (x26 (x10 x30 x29) x29 ⟶ False) ⟶ x26 x29 (x5 x30) ⟶ False) ⟶ (∀ x29 x30 . (x0 x30 ⟶ False) ⟶ (x26 (x22 x30 x29) x29 ⟶ False) ⟶ x26 x29 (x24 x30) ⟶ False) ⟶ (∀ x29 x30 . (x0 x30 ⟶ False) ⟶ (x26 (x9 x30 x29) x29 ⟶ False) ⟶ x26 x29 (x6 x30) ⟶ False) ⟶ (∀ x29 x30 x31 x32 . (x26 x31 x32 ⟶ False) ⟶ (x26 x31 x29 ⟶ False) ⟶ x30 = x28 x29 x32 ⟶ x26 x31 x30 ⟶ False) ⟶ (∀ x29 x30 . (x0 x30 ⟶ False) ⟶ (x26 x29 (x1 (x1 x30)) ⟶ False) ⟶ x26 x29 (x24 x30) ⟶ False) ⟶ (∀ x29 x30 x31 x32 . (x26 x31 x32 ⟶ False) ⟶ x32 = x1 x29 ⟶ x26 x30 x29 ⟶ x26 x31 x30 ⟶ False) ⟶ (∀ x29 x30 x31 . x26 x30 x31 ⟶ x26 x30 x29 ⟶ x3 x29 x31 ⟶ False) ⟶ (∀ x29 x30 x31 x32 . (x26 x31 x32 ⟶ False) ⟶ x32 = x28 x29 x30 ⟶ x26 x31 x29 ⟶ False) ⟶ (∀ x29 x30 x31 x32 . (x26 x31 x32 ⟶ False) ⟶ x32 = x28 x30 x29 ⟶ x26 x31 x29 ⟶ False) ⟶ (∀ x29 x30 . (x0 x30 ⟶ False) ⟶ x3 x29 x30 ⟶ x26 x29 (x2 x30) ⟶ False) ⟶ (∀ x29 x30 . (x0 x30 ⟶ False) ⟶ (x26 x29 (x1 x30) ⟶ False) ⟶ x26 x29 (x6 x30) ⟶ False) ⟶ (∀ x29 x30 . (x3 x29 x30 ⟶ False) ⟶ (x26 (x20 x29 x30) x29 ⟶ False) ⟶ False) ⟶ (∀ x29 x30 . (x3 x30 x29 ⟶ False) ⟶ (x26 (x20 x30 x29) x29 ⟶ False) ⟶ False) ⟶ (∀ x29 x30 . (x0 x30 ⟶ False) ⟶ x0 (x28 x30 x29) ⟶ False) ⟶ (∀ x29 x30 . (x0 x30 ⟶ False) ⟶ x0 (x28 x29 x30) ⟶ False) ⟶ (∀ x29 . x26 x29 x19 ⟶ x3 (x18 x29) x19 ⟶ False) ⟶ (∀ x29 . (x26 (x12 x29) (x11 x29) ⟶ False) ⟶ x26 x29 x19 ⟶ False) ⟶ (∀ x29 . (x26 (x17 x29) (x12 x29) ⟶ False) ⟶ x26 x29 x19 ⟶ False) ⟶ (∀ x29 . (x26 (x18 x29) (x17 x29) ⟶ False) ⟶ x26 x29 x19 ⟶ False) ⟶ (∀ x29 x30 . x26 x29 x30 ⟶ x26 x30 x29 ⟶ False) ⟶ (∀ x29 . (x26 (x11 x29) x29 ⟶ False) ⟶ x26 x29 x19 ⟶ False) ⟶ (∀ x29 x30 . (x3 x29 x30 ⟶ False) ⟶ x3 x30 x29 ⟶ False) ⟶ (∀ x29 x30 . x0 x30 ⟶ x26 x29 x30 ⟶ False) ⟶ (∀ x29 . (x0 x29 ⟶ False) ⟶ (x3 (x16 x29) x29 ⟶ False) ⟶ False) ⟶ (∀ x29 . (x0 x29 ⟶ False) ⟶ (x26 (x16 x29) x29 ⟶ False) ⟶ False) ⟶ (∀ x29 x30 . (x30 = x29 ⟶ False) ⟶ x0 x29 ⟶ x0 x30 ⟶ False) ⟶ (∀ x29 . (x29 = x13 ⟶ False) ⟶ x0 x29 ⟶ False) ⟶ (x0 x15 ⟶ False) ⟶ (x0 x19 ⟶ False) ⟶ (∀ x29 x30 x31 . (x28 (x28 x31 x29) x30 = x28 x31 (x28 x29 x30) ⟶ False) ⟶ False) ⟶ (∀ x29 x30 . (x28 x30 x29 = x28 x29 x30 ⟶ False) ⟶ False) ⟶ (∀ x29 . (x28 x29 x29 = x29 ⟶ False) ⟶ False) ⟶ (∀ x29 . (x28 x29 x13 = x29 ⟶ False) ⟶ False) ⟶ ((x0 x14 ⟶ False) ⟶ False) ⟶ ((x0 x13 ⟶ False) ⟶ False) ⟶ False (proof)
Theorem 307f0..^t6_xregular : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι . ∀ x3 : ι → ι → ο . ∀ x4 x5 : ι → ι . ∀ x6 x7 x8 x9 x10 x11 x12 x13 : ι → ι → ι . ∀ x14 . ∀ x15 x16 : ι → ι . ∀ x17 x18 x19 . ∀ x20 x21 x22 x23 : ι → ι . ∀ x24 x25 x26 x27 x28 : ι → ι → ι . ∀ x29 : ι → ι → ι → ι . ∀ x30 x31 : ι → ι . ∀ x32 : ι → ι → ο . ∀ x33 : ι → ι → ι → ι . ∀ x34 : ι → ι → ι . (∀ x35 x36 x37 . (x36 = x34 x35 x37 ⟶ False) ⟶ x32 (x33 x35 x37 x36) x36 ⟶ x32 (x33 x35 x37 x36) x35 ⟶ False) ⟶ (∀ x35 x36 x37 . (x36 = x34 x37 x35 ⟶ False) ⟶ x32 (x33 x37 x35 x36) x36 ⟶ x32 (x33 x37 x35 x36) x35 ⟶ False) ⟶ (∀ x35 x36 x37 . (x36 = x34 x35 x37 ⟶ False) ⟶ (x32 (x33 x35 x37 x36) x36 ⟶ False) ⟶ (x32 (x33 x35 x37 x36) x37 ⟶ False) ⟶ (x32 (x33 x35 x37 x36) x35 ⟶ False) ⟶ False) ⟶ (∀ x35 x36 . (x0 x36 ⟶ False) ⟶ (x3 x35 x36 ⟶ False) ⟶ (x32 x35 (x2 x36) ⟶ False) ⟶ x32 x35 (x1 (x1 (x1 (x1 (x1 x36))))) ⟶ False) ⟶ (∀ x35 x36 . (x0 x36 ⟶ False) ⟶ (x32 x35 (x1 (x1 (x1 (x1 (x1 x36))))) ⟶ False) ⟶ x32 x35 (x2 x36) ⟶ False) ⟶ (∀ x35 x36 x37 . (x0 x37 ⟶ False) ⟶ (x3 x35 x37 ⟶ False) ⟶ (x32 x36 (x4 x37) ⟶ False) ⟶ x32 x35 x36 ⟶ x32 x36 (x1 (x1 (x1 (x1 x37)))) ⟶ False) ⟶ (∀ x35 x36 x37 x38 . (x0 x38 ⟶ False) ⟶ (x3 x35 x38 ⟶ False) ⟶ (x32 x37 (x31 x38) ⟶ False) ⟶ x32 x36 x37 ⟶ x32 x35 x36 ⟶ x32 x37 (x1 (x1 (x1 x38))) ⟶ False) ⟶ (∀ x35 x36 x37 x38 x39 x40 . (x0 x40 ⟶ False) ⟶ (x3 x35 x40 ⟶ False) ⟶ (x32 x39 (x5 x40) ⟶ False) ⟶ x32 x36 x39 ⟶ x32 x38 x36 ⟶ x32 x37 x38 ⟶ x32 x35 x37 ⟶ x32 x39 (x1 x40) ⟶ False) ⟶ (∀ x35 x36 x37 x38 x39 . (x0 x39 ⟶ False) ⟶ (x3 x35 x39 ⟶ False) ⟶ (x32 x38 (x30 x39) ⟶ False) ⟶ x32 x36 x38 ⟶ x32 x37 x36 ⟶ x32 x35 x37 ⟶ x32 x38 (x1 (x1 x39)) ⟶ False) ⟶ (∀ x35 x36 x37 . (x36 = x1 x37 ⟶ False) ⟶ x32 x35 x37 ⟶ x32 (x6 x37 x36) x35 ⟶ x32 (x6 x37 x36) x36 ⟶ False) ⟶ (∀ x35 x36 x37 . (x32 (x29 x35 x36 x37) x35 ⟶ False) ⟶ x36 = x1 x35 ⟶ x32 x37 x36 ⟶ False) ⟶ (∀ x35 x36 x37 . (x32 x37 (x29 x35 x36 x37) ⟶ False) ⟶ x36 = x1 x35 ⟶ x32 x37 x36 ⟶ False) ⟶ (∀ x35 x36 . (x0 x36 ⟶ False) ⟶ (x32 x35 (x1 (x1 (x1 (x1 x36)))) ⟶ False) ⟶ x32 x35 (x4 x36) ⟶ False) ⟶ (∀ x35 x36 . (x36 = x1 x35 ⟶ False) ⟶ (x32 (x6 x35 x36) x36 ⟶ False) ⟶ (x32 (x6 x35 x36) (x7 x35 x36) ⟶ False) ⟶ False) ⟶ (∀ x35 x36 . (x0 x36 ⟶ False) ⟶ (x32 (x28 x36 x35) (x27 x36 x35) ⟶ False) ⟶ x32 x35 (x31 x36) ⟶ False) ⟶ (∀ x35 x36 . (x0 x36 ⟶ False) ⟶ (x32 (x8 x36 x35) (x9 x36 x35) ⟶ False) ⟶ x32 x35 (x30 x36) ⟶ False) ⟶ (∀ x35 x36 . (x0 x36 ⟶ False) ⟶ (x32 (x26 x36 x35) (x8 x36 x35) ⟶ False) ⟶ x32 x35 (x30 x36) ⟶ False) ⟶ (∀ x35 x36 . (x0 x36 ⟶ False) ⟶ (x32 (x10 x36 x35) (x11 x36 x35) ⟶ False) ⟶ x32 x35 (x5 x36) ⟶ False) ⟶ (∀ x35 x36 . (x0 x36 ⟶ False) ⟶ (x32 (x25 x36 x35) (x10 x36 x35) ⟶ False) ⟶ x32 x35 (x5 x36) ⟶ False) ⟶ (∀ x35 x36 . (x0 x36 ⟶ False) ⟶ (x32 (x12 x36 x35) (x25 x36 x35) ⟶ False) ⟶ x32 x35 (x5 x36) ⟶ False) ⟶ (∀ x35 x36 . (x0 x36 ⟶ False) ⟶ x32 x35 (x4 x36) ⟶ x3 (x24 x36 x35) x36 ⟶ False) ⟶ (∀ x35 x36 . (x0 x36 ⟶ False) ⟶ x32 x35 (x31 x36) ⟶ x3 (x28 x36 x35) x36 ⟶ False) ⟶ (∀ x35 x36 . (x0 x36 ⟶ False) ⟶ x32 x35 (x30 x36) ⟶ x3 (x26 x36 x35) x36 ⟶ False) ⟶ (∀ x35 x36 . (x0 x36 ⟶ False) ⟶ x32 x35 (x5 x36) ⟶ x3 (x12 x36 x35) x36 ⟶ False) ⟶ (∀ x35 x36 . (x0 x36 ⟶ False) ⟶ (x32 x35 (x1 (x1 (x1 x36))) ⟶ False) ⟶ x32 x35 (x31 x36) ⟶ False) ⟶ (∀ x35 x36 . (x36 = x1 x35 ⟶ False) ⟶ (x32 (x6 x35 x36) x36 ⟶ False) ⟶ (x32 (x7 x35 x36) x35 ⟶ False) ⟶ False) ⟶ (∀ x35 x36 x37 . (x3 x37 (x34 x36 x35) ⟶ False) ⟶ x3 x37 x35 ⟶ x3 x37 x36 ⟶ False) ⟶ (∀ x35 x36 x37 . (x3 x36 x37 ⟶ False) ⟶ x3 x36 (x34 x37 x35) ⟶ False) ⟶ (∀ x35 x36 x37 . (x3 x36 x37 ⟶ False) ⟶ x3 x36 (x34 x35 x37) ⟶ False) ⟶ (∀ x35 x36 . (x0 x36 ⟶ False) ⟶ (x32 (x24 x36 x35) x35 ⟶ False) ⟶ x32 x35 (x4 x36) ⟶ False) ⟶ (∀ x35 x36 . (x0 x36 ⟶ False) ⟶ (x32 (x27 x36 x35) x35 ⟶ False) ⟶ x32 x35 (x31 x36) ⟶ False) ⟶ (∀ x35 x36 . (x0 x36 ⟶ False) ⟶ (x32 (x9 x36 x35) x35 ⟶ False) ⟶ x32 x35 (x30 x36) ⟶ False) ⟶ (∀ x35 x36 . (x0 x36 ⟶ False) ⟶ (x32 (x11 x36 x35) x35 ⟶ False) ⟶ x32 x35 (x5 x36) ⟶ False) ⟶ (∀ x35 x36 x37 x38 . (x32 x37 x38 ⟶ False) ⟶ (x32 x37 x35 ⟶ False) ⟶ x36 = x34 x35 x38 ⟶ x32 x37 x36 ⟶ False) ⟶ (∀ x35 x36 . (x0 x36 ⟶ False) ⟶ (x32 x35 (x1 (x1 x36)) ⟶ False) ⟶ x32 x35 (x30 x36) ⟶ False) ⟶ (∀ x35 x36 x37 x38 . (x32 x37 x38 ⟶ False) ⟶ x38 = x1 x35 ⟶ x32 x36 x35 ⟶ x32 x37 x36 ⟶ False) ⟶ (∀ x35 x36 x37 . x32 x36 x37 ⟶ x32 x36 x35 ⟶ x3 x35 x37 ⟶ False) ⟶ (∀ x35 x36 x37 x38 . (x32 x37 x38 ⟶ False) ⟶ x38 = x34 x35 x36 ⟶ x32 x37 x35 ⟶ False) ⟶ (∀ x35 x36 x37 x38 . (x32 x37 x38 ⟶ False) ⟶ x38 = x34 x36 x35 ⟶ x32 x37 x35 ⟶ False) ⟶ (∀ x35 x36 . (x0 x36 ⟶ False) ⟶ x3 x35 x36 ⟶ x32 x35 (x2 x36) ⟶ False) ⟶ (∀ x35 x36 . (x0 x36 ⟶ False) ⟶ (x32 x35 (x1 x36) ⟶ False) ⟶ x32 x35 (x5 x36) ⟶ False) ⟶ (∀ x35 x36 . (x3 x35 x36 ⟶ False) ⟶ (x32 (x13 x35 x36) x35 ⟶ False) ⟶ False) ⟶ (∀ x35 x36 . (x3 x36 x35 ⟶ False) ⟶ (x32 (x13 x36 x35) x35 ⟶ False) ⟶ False) ⟶ (∀ x35 x36 . (x0 x36 ⟶ False) ⟶ x0 (x34 x36 x35) ⟶ False) ⟶ (∀ x35 x36 . (x0 x36 ⟶ False) ⟶ x0 (x34 x35 x36) ⟶ False) ⟶ (∀ x35 . x32 x35 x14 ⟶ x3 (x15 x35) x14 ⟶ False) ⟶ (∀ x35 . (x32 (x22 x35) (x23 x35) ⟶ False) ⟶ x32 x35 x14 ⟶ False) ⟶ (∀ x35 . (x32 (x16 x35) (x22 x35) ⟶ False) ⟶ x32 x35 x14 ⟶ False) ⟶ (∀ x35 . (x32 (x21 x35) (x16 x35) ⟶ False) ⟶ x32 x35 x14 ⟶ False) ⟶ (∀ x35 . (x32 (x15 x35) (x21 x35) ⟶ False) ⟶ x32 x35 x14 ⟶ False) ⟶ (∀ x35 x36 . x32 x35 x36 ⟶ x32 x36 x35 ⟶ False) ⟶ (∀ x35 . (x32 (x23 x35) x35 ⟶ False) ⟶ x32 x35 x14 ⟶ False) ⟶ (∀ x35 x36 . (x3 x35 x36 ⟶ False) ⟶ x3 x36 x35 ⟶ False) ⟶ (∀ x35 x36 . x0 x36 ⟶ x32 x35 x36 ⟶ False) ⟶ (∀ x35 . (x0 x35 ⟶ False) ⟶ (x3 (x20 x35) x35 ⟶ False) ⟶ False) ⟶ (∀ x35 . (x0 x35 ⟶ False) ⟶ (x32 (x20 x35) x35 ⟶ False) ⟶ False) ⟶ (∀ x35 x36 . (x36 = x35 ⟶ False) ⟶ x0 x35 ⟶ x0 x36 ⟶ False) ⟶ (∀ x35 . (x35 = x17 ⟶ False) ⟶ x0 x35 ⟶ False) ⟶ (x0 x19 ⟶ False) ⟶ (x0 x14 ⟶ False) ⟶ (∀ x35 x36 x37 . (x34 (x34 x37 x35) x36 = x34 x37 (x34 x35 x36) ⟶ False) ⟶ False) ⟶ (∀ x35 x36 . (x34 x36 x35 = x34 x35 x36 ⟶ False) ⟶ False) ⟶ (∀ x35 . (x34 x35 x35 = x35 ⟶ False) ⟶ False) ⟶ (∀ x35 . (x34 x35 x17 = x35 ⟶ False) ⟶ False) ⟶ ((x0 x18 ⟶ False) ⟶ False) ⟶ ((x0 x17 ⟶ False) ⟶ False) ⟶ False (proof)