Proofgold Address

Theorem 96d2f.. : ∀ x0 x1 x2 : ι → ι → ο . ∀ x3 x4 x5 x6 x7 . ∀ x8 x9 : ι → ι . ∀ x10 x11 x12 : ι → ι → ι . ∀ x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 : ι → ο . x0 x5 x6 ⟶ (∀ x24 . x0 x24 x7 ⟶ or (or (or (x24 = x3) (x24 = x4)) (x24 = x5)) (x24 = x6)) ⟶ (∀ x24 . x1 x24 x24) ⟶ (∀ x24 x25 . x1 (x11 x24 x25) x25) ⟶ (∀ x24 x25 x26 . x2 x24 x25 ⟶ x1 (x10 x24 x25) (x10 x24 x26) ⟶ x1 x25 x26) ⟶ (∀ x24 x25 x26 . x0 x26 x25 ⟶ not (x0 x26 (x12 x24 x25))) ⟶ (∀ x24 x25 x26 . x0 x25 x24 ⟶ x0 x26 x24 ⟶ not (x1 x26 x25) ⟶ x13 x24) ⟶ (∀ x24 x25 . x1 x24 x25 ⟶ x17 x24 ⟶ x17 x25) ⟶ (∀ x24 . x15 x24 ⟶ x14 x24) ⟶ (∀ x24 x25 . x2 x24 x25 ⟶ x13 x24 ⟶ x14 x25 ⟶ x16 (x10 x24 x25)) ⟶ (∀ x24 x25 . x0 x25 x24 ⟶ x14 x24 ⟶ x13 (x12 x24 (x9 x25))) ⟶ not (x5 = x6) ⟶ not (x1 x5 x3) ⟶ (∀ x24 . x1 x24 x5 ⟶ not (x0 x3 x24) ⟶ not (x0 x4 x24) ⟶ x24 = x3) ⟶ x0 x3 (x8 (x9 x4)) ⟶ x0 x3 (x12 (x8 x5) (x9 x4)) ⟶ not (x0 x4 (x9 x5)) ⟶ x1 x4 (x8 (x9 x4)) ⟶ not (x1 x5 (x9 x4)) ⟶ not (x1 x5 (x9 x5)) ⟶ not (x1 (x9 x4) (x9 x5)) ⟶ x1 (x9 x4) (x10 (x9 x4) (x9 (x9 x4))) ⟶ not (x0 (x12 x6 (x9 x4)) (x8 x5)) ⟶ (∀ x24 . x0 x24 (x8 x5) ⟶ or (or (or (x24 = x3) (x24 = x4)) (x24 = x9 x4)) (x24 = x5)) ⟶ not (x9 x5 = x6) ⟶ x1 x6 (x8 x5) ⟶ not (x0 (x9 x5) (x12 (x8 x5) (x9 x4))) ⟶ x0 (x9 (x9 x4)) (x8 (x8 (x9 x4))) ⟶ x0 x3 (x8 (x10 (x9 x4) (x9 (x9 x4)))) ⟶ x0 (x9 x4) (x10 (x10 (x9 x4) (x9 (x9 x4))) (x8 (x9 (x9 x4)))) ⟶ not (x0 (x9 x4) (x10 (x12 (x8 x5) (x8 (x9 x4))) (x8 (x9 (x9 x4))))) ⟶ x0 x5 (x10 (x12 (x8 x5) x5) (x8 (x9 (x9 x4)))) ⟶ not (x0 (x9 x5) (x9 x6)) ⟶ not (x0 (x12 x6 (x9 x4)) x7) ⟶ x0 (x9 x5) (x10 (x8 (x9 x5)) (x9 x6)) ⟶ x0 x4 (x10 (x9 (x9 x5)) x7) ⟶ x0 x5 (x10 (x9 (x9 x5)) x7) ⟶ not (x0 x6 (x9 (x8 x5))) ⟶ x0 (x8 x5) (x10 x6 (x9 (x8 x5))) ⟶ x1 x6 (x10 x6 (x9 (x8 (x9 x4)))) ⟶ x1 (x9 (x9 x5)) (x10 (x12 (x8 x5) (x8 (x9 x5))) (x10 (x8 (x9 x5)) (x9 (x8 x5)))) ⟶ x1 x7 (x10 x7 (x9 (x12 (x8 x5) x5))) ⟶ not (x1 (x10 (x9 (x9 (x9 x4))) (x10 x4 (x9 (x8 x5)))) (x8 (x9 (x9 x4)))) ⟶ not (x1 (x10 (x8 x5) (x9 (x9 x5))) (x8 x5)) ⟶ x12 x5 (x9 x3) = x9 x4 ⟶ x12 x5 (x9 x4) = x4 ⟶ x12 x6 (x9 x3) = x12 (x8 x5) (x8 (x9 x4)) ⟶ x1 (x10 (x9 x4) (x9 (x9 x4))) (x12 (x12 (x8 x5) (x9 x5)) (x9 x3)) ⟶ x1 (x9 x5) (x12 (x12 (x8 x5) (x8 (x9 x4))) (x9 x4)) ⟶ x1 (x12 (x8 x5) (x9 x3)) (x12 (x8 x5) (x8 (x9 x5))) ⟶ x1 (x8 (x9 (x9 x4))) (x12 (x12 (x8 (x10 (x9 x4) (x9 (x9 x4)))) (x9 (x10 (x9 x4) (x9 (x9 x4))))) (x9 (x9 x4))) ⟶ (∀ x24 . x0 x24 (x10 (x12 (x8 x5) (x8 (x9 x5))) (x8 (x9 (x9 x4)))) ⟶ not (x24 = x3) ⟶ x0 x24 (x10 (x12 (x8 x5) (x8 (x9 x5))) (x9 (x9 (x9 x4))))) ⟶ (∀ x24 . x0 x24 (x12 x7 (x9 x5)) ⟶ not (x24 = x6) ⟶ x0 x24 x5) ⟶ x11 (x10 (x9 (x9 x4)) x7) (x10 (x9 x5) (x8 (x9 x5))) = x12 x6 (x9 x4) ⟶ not (x15 (x10 x5 (x9 (x8 x5)))) ⟶ not (x16 (x10 (x10 (x9 x4) (x9 (x9 x4))) (x8 (x9 (x9 x4))))) ⟶ x14 x6 ⟶ x14 (x12 x7 (x9 x4)) ⟶ x15 (x10 x6 (x9 (x8 x5))) ⟶ x16 (x10 (x9 (x9 (x9 x4))) x7) ⟶ x19 x5 ⟶ x19 (x11 (x10 (x9 (x9 x5)) x7) (x12 (x8 x5) (x9 x4))) ⟶ x19 (x12 (x8 x5) x5) ⟶ x20 (x12 (x8 x5) (x9 x5)) ⟶ x20 (x11 (x10 (x10 (x9 x5) (x8 (x9 x5))) (x9 (x12 x6 (x9 x4)))) (x10 (x9 (x9 x4)) (x10 (x9 (x9 x5)) x7))) ⟶ not (x14 (x12 (x11 (x10 x6 (x9 (x12 x6 (x9 x4)))) (x8 (x12 x6 (x9 x4)))) (x9 (x12 x6 (x9 x4))))) ⟶ x20 (x12 (x8 x5) (x9 x3)) ⟶ x21 (x10 x6 (x9 (x9 x5))) ⟶ x20 (x12 (x10 (x9 (x9 (x9 x4))) (x10 x5 (x9 (x8 x5)))) (x9 x3)) ⟶ (∀ x24 . x0 x24 x7 ⟶ not (x0 x24 (x9 x4)) ⟶ x0 x24 (x10 (x10 (x9 x4) (x9 (x9 x4))) (x10 (x8 (x9 x5)) (x9 x6))) ⟶ x0 x24 (x10 (x8 (x9 x5)) (x9 x6))) ⟶ not (x16 (x11 (x10 (x10 (x9 x4) (x9 (x9 x4))) (x10 (x8 (x9 x5)) (x9 x6))) (x10 (x9 (x9 x5)) x7))) ⟶ x22 (x12 (x10 (x9 (x9 x4)) (x10 x7 (x9 (x8 x5)))) (x9 x4)) ⟶ (∀ x24 . x0 x24 (x12 (x8 x5) (x8 (x9 x5))) ⟶ x0 x24 (x10 (x9 (x9 x5)) (x10 x7 (x9 (x8 x5)))) ⟶ not (x0 x24 (x9 x5)) ⟶ x0 x24 (x10 (x9 x4) (x10 (x8 (x9 x5)) (x9 (x8 x5))))) ⟶ (∀ x24 . x0 x24 (x12 (x8 x5) (x8 (x9 x5))) ⟶ x0 x24 (x10 (x9 (x9 x5)) (x10 x7 (x9 (x8 x5)))) ⟶ x0 x24 (x10 x6 (x9 (x9 x5)))) ⟶ (∀ x24 . x0 x24 (x12 (x8 x5) (x8 (x9 x5))) ⟶ x0 x24 (x10 (x9 (x9 x5)) (x10 x7 (x9 (x8 x5)))) ⟶ not (x16 (x12 (x11 (x10 (x12 (x8 x5) (x8 (x9 x5))) (x10 (x8 (x9 x5)) (x9 (x8 x5)))) (x10 (x9 (x9 x5)) (x10 x7 (x9 (x8 x5))))) (x9 x24)))) ⟶ x1 (x12 x6 (x9 x3)) (x12 (x8 x5) (x8 (x9 x4))) (proof)
Known 8106d..^notI : ∀ x0 : ο . (x0 ⟶ False) ⟶ not x0
Known notE^notE : ∀ x0 : ο . not x0 ⟶ x0 ⟶ False
Theorem 06e0d.. : ∀ 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 . iff (x19 x24) (and (x13 x24) (not (x14 x24)))) ⟶ (∀ x24 . iff (x23 x24) (and (x17 x24) (not (x18 x24)))) ⟶ (∀ x24 x25 . x1 x24 x25 ⟶ x1 x25 x24 ⟶ x24 = x25) ⟶ (∀ x24 . iff (x0 x24 x4) (x24 = x3)) ⟶ (∀ x24 x25 x26 . iff (x0 x26 (x12 x24 x25)) (and (x0 x26 x24) (not (x0 x26 x25)))) ⟶ (∀ x24 . x0 x24 x6 ⟶ or (or (x24 = x3) (x24 = x4)) (x24 = x5)) ⟶ x0 x3 x7 ⟶ (∀ x24 . x0 x3 (x8 x24)) ⟶ (∀ x24 x25 x26 . x10 x24 (x10 x25 x26) = x10 (x10 x24 x25) x26) ⟶ (∀ x24 x25 . x0 x24 x25 ⟶ x13 (x8 x25)) ⟶ (∀ x24 x25 . not (x0 x25 x24) ⟶ x13 x24 ⟶ x14 (x10 x24 (x9 x25))) ⟶ (∀ x24 x25 . x0 x25 x24 ⟶ x1 (x9 x25) x24) ⟶ (∀ x24 x25 . x0 x25 x24 ⟶ x21 x24 ⟶ x20 (x12 x24 (x9 x25))) ⟶ (∀ x24 x25 x26 . x1 x26 (x10 x24 x25) ⟶ ∀ x27 . x0 x27 x24 ⟶ not (x0 x27 x26) ⟶ x15 x26 ⟶ or (x14 x24) (x14 x25)) ⟶ not (x0 x5 x3) ⟶ not (x0 x6 x6) ⟶ (∀ x24 . x1 x24 x5 ⟶ not (x0 x3 x24) ⟶ x0 x4 x24 ⟶ x24 = x9 x4) ⟶ x0 x4 (x12 (x8 x5) (x8 (x9 x5))) ⟶ not (x3 = x12 x6 (x9 x4)) ⟶ x0 (x9 x4) (x12 (x8 x5) (x9 x5)) ⟶ not (x4 = x12 x6 (x9 x4)) ⟶ not (x0 x4 (x12 x6 (x9 x4))) ⟶ not (x1 (x9 x5) x5) ⟶ not (x9 x4 = x12 (x8 x5) x5) ⟶ (∀ x24 . x0 x24 (x9 (x9 x4)) ⟶ x24 = x9 x4) ⟶ not (x5 = x8 (x9 x4)) ⟶ not (x9 (x9 x4) = x8 (x9 x4)) ⟶ (∀ x24 . x1 x24 (x8 (x9 x4)) ⟶ not (x0 (x9 x4) x24) ⟶ not (x0 x3 x24) ⟶ x24 = x3) ⟶ (∀ x24 . x1 x24 (x8 (x9 x4)) ⟶ x0 (x9 x4) x24 ⟶ or (or (or (x24 = x3) (x24 = x4)) (x24 = x9 (x9 x4))) (x24 = x8 (x9 x4))) ⟶ not (x0 (x12 (x8 x5) (x8 (x9 x5))) (x12 (x8 x5) (x9 x5))) ⟶ not (x5 = x9 x5) ⟶ not (x1 (x12 x6 (x9 x4)) (x9 x5)) ⟶ x0 x3 (x8 (x9 (x9 x4))) ⟶ not (x0 (x9 x4) (x9 (x10 (x9 x4) (x9 (x9 x4))))) ⟶ x0 (x9 (x9 x4)) (x8 (x10 (x9 x4) (x9 (x9 x4)))) ⟶ x0 (x9 x4) (x10 (x10 (x9 x4) (x9 (x9 x4))) (x8 (x9 (x9 x4)))) ⟶ x0 x4 (x10 (x12 (x8 x5) (x8 (x9 x5))) (x9 (x9 (x9 x4)))) ⟶ not (x0 (x12 x6 (x9 x4)) (x9 (x9 x5))) ⟶ not (x0 x6 (x10 (x8 x5) (x9 (x9 x5)))) ⟶ x0 x3 (x10 x6 (x9 (x9 x5))) ⟶ x0 (x12 x6 (x9 x4)) (x8 (x12 x6 (x9 x4))) ⟶ x2 x5 (x10 (x9 (x9 x4)) (x9 x6)) ⟶ x0 x4 (x12 x7 (x8 (x9 x5))) ⟶ x0 x3 (x10 (x8 (x9 x5)) (x9 x6)) ⟶ x0 x5 (x10 (x12 (x8 x5) (x8 (x9 x4))) (x10 (x9 (x9 x5)) (x9 (x8 x5)))) ⟶ x0 x5 (x10 (x12 (x8 x5) (x8 (x9 x5))) (x10 (x8 (x9 x5)) (x9 (x8 x5)))) ⟶ x0 x4 (x10 (x9 (x9 x5)) (x10 x7 (x9 (x8 x5)))) ⟶ x0 x6 (x10 (x9 (x9 x5)) (x10 x7 (x9 (x8 x5)))) ⟶ (∀ x24 . x0 x24 x7 ⟶ not (x24 = x5) ⟶ or (or (x24 = x3) (x24 = x4)) (x24 = x6)) ⟶ x1 (x8 x5) (x10 (x8 x5) (x9 (x8 x5))) ⟶ x12 x6 (x9 x5) = x5 ⟶ x12 (x12 (x8 x5) (x9 x5)) (x9 x3) = x10 (x9 x4) (x9 (x9 x4)) ⟶ x1 (x8 (x9 x4)) (x12 (x12 (x8 x5) (x9 x5)) (x9 x4)) ⟶ x12 (x12 (x8 x5) (x9 x5)) (x9 x4) = x8 (x9 x4) ⟶ x1 (x9 x4) (x12 (x12 (x8 x5) (x8 (x9 x4))) (x9 x5)) ⟶ (∀ x24 . x0 x24 (x12 (x8 (x10 (x9 x4) (x9 (x9 x4)))) (x9 (x10 (x9 x4) (x9 (x9 x4))))) ⟶ not (x24 = x9 (x9 x4)) ⟶ x0 x24 (x8 (x9 x4))) ⟶ (∀ x24 . x0 x24 (x10 (x12 (x8 x5) (x8 (x9 x5))) (x8 (x9 (x9 x4)))) ⟶ not (x24 = x9 x4) ⟶ x0 x24 (x10 (x12 (x8 x5) (x8 (x9 x4))) (x8 (x9 (x9 x4))))) ⟶ (∀ x24 . x0 x24 (x12 x7 x5) ⟶ not (x24 = x6) ⟶ x0 x24 (x9 x5)) ⟶ (∀ x24 . x0 x24 (x12 x7 (x9 x4)) ⟶ not (x24 = x5) ⟶ x0 x24 (x10 x4 (x9 x6))) ⟶ (∀ x24 . x0 x24 (x12 x7 (x8 (x9 x5))) ⟶ not (x24 = x5) ⟶ x0 x24 (x10 (x9 x4) (x9 x6))) ⟶ x11 (x10 (x9 (x9 x4)) (x10 (x9 (x9 x5)) x7)) (x10 x7 (x9 (x12 (x8 x5) x5))) = x7 ⟶ x1 (x11 (x10 x7 (x9 (x8 x5))) (x10 (x9 x5) (x8 (x9 x5)))) (x12 x6 (x9 x4)) ⟶ not (x15 (x10 (x9 (x9 (x9 x4))) (x10 x4 (x9 (x8 x5))))) ⟶ not (x16 (x10 (x10 (x9 x4) (x9 (x9 x4))) (x8 (x9 (x9 x4))))) ⟶ not (x17 (x10 (x12 (x8 x5) (x8 (x9 x5))) (x8 (x9 (x9 x4))))) ⟶ x13 (x12 (x8 x5) x5) ⟶ x14 (x12 x7 (x9 x5)) ⟶ x16 (x10 (x9 (x9 (x9 x4))) x7) ⟶ x16 (x10 x7 (x9 (x12 (x8 x5) x5))) ⟶ x17 (x10 (x9 (x9 x4)) (x10 (x9 (x9 x5)) x7)) ⟶ x21 (x10 x6 (x9 (x9 x5))) ⟶ x21 x7 ⟶ x21 (x10 (x12 (x8 x5) x5) (x8 (x9 x5))) ⟶ x22 (x10 (x9 (x9 x5)) x7) ⟶ x1 (x12 (x11 (x10 (x10 (x9 x4) (x9 (x9 x4))) (x10 (x8 (x9 x5)) (x9 x6))) (x10 (x9 (x9 x5)) x7)) (x9 x6)) (x10 (x9 x4) (x8 (x9 x5))) ⟶ x1 (x12 (x11 (x10 (x12 (x8 x5) (x8 (x9 x5))) (x10 (x8 (x9 x5)) (x9 (x8 x5)))) (x10 (x9 (x9 x5)) (x10 x7 (x9 (x8 x5))))) (x9 (x8 x5))) (x10 x6 (x9 (x9 x5))) ⟶ (∀ x24 . x0 x24 (x10 (x8 (x9 x5)) (x9 (x8 x5))) ⟶ not (x16 (x12 (x11 (x10 (x12 (x8 x5) (x8 (x9 x5))) (x10 (x8 (x9 x5)) (x9 (x8 x5)))) (x10 (x9 (x9 x5)) (x10 x7 (x9 (x8 x5))))) (x9 x24)))) ⟶ not (x0 x5 x5) (proof)
Known 50594..^iffEL : ∀ x0 x1 : ο . iff x0 x1 ⟶ x0 ⟶ x1
Known b4782..^contra : ∀ x0 : ο . (not x0 ⟶ False) ⟶ x0
Theorem 43593.. : ∀ 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 . iff (x1 x24 x25) (∀ x26 . x0 x26 x24 ⟶ x0 x26 x25)) ⟶ (∀ x24 . iff (x13 x24) (∀ x25 : ο . (∀ x26 . and (x0 x26 x24) (not (x1 x24 (x8 x26))) ⟶ x25) ⟶ x25)) ⟶ (∀ x24 x25 . x0 x25 (x8 x24) ⟶ x1 x25 x24) ⟶ (∀ x24 x25 . (∀ x26 . x0 x26 x24 ⟶ not (x0 x26 x25)) ⟶ x2 x24 x25) ⟶ (∀ x24 x25 . not (x0 x25 (x9 x24)) ⟶ not (x25 = x24)) ⟶ (∀ x24 x25 . x0 x25 x24 ⟶ x11 x24 (x9 x25) = x9 x25) ⟶ (∀ x24 x25 . x15 (x10 x24 x25) ⟶ or (x13 x24) (x14 x25)) ⟶ not (x1 x5 x3) ⟶ not (x0 (x9 x4) x3) ⟶ x0 x4 (x8 x5) ⟶ x1 (x9 x4) x5 ⟶ not (x4 = x9 x4) ⟶ not (x0 x3 (x12 (x8 x5) x5)) ⟶ not (x0 (x9 x4) (x9 x4)) ⟶ not (x0 (x9 x4) (x8 (x9 x5))) ⟶ x1 (x9 x4) (x10 (x9 x4) (x9 (x9 x4))) ⟶ not (x0 (x9 (x9 x4)) x5) ⟶ not (x1 x5 (x12 x6 (x9 x4))) ⟶ (∀ x24 . x0 x24 (x9 (x9 x4)) ⟶ x24 = x9 x4) ⟶ not (x5 = x8 (x9 x4)) ⟶ not (x0 x5 (x10 (x9 x4) (x9 (x9 x4)))) ⟶ not (x1 (x12 (x8 x5) (x9 x5)) (x10 (x9 x4) (x9 (x9 x4)))) ⟶ not (x0 (x12 x6 (x9 x4)) (x8 x5)) ⟶ not (x1 (x12 x6 (x9 x4)) (x9 x5)) ⟶ not (x12 (x8 x5) (x8 (x9 x5)) = x8 x5) ⟶ x0 (x9 x4) (x10 (x9 (x9 x4)) (x9 (x9 (x9 x4)))) ⟶ x0 (x9 (x9 x4)) (x8 (x10 (x9 x4) (x9 (x9 x4)))) ⟶ not (x0 (x9 (x9 x4)) (x9 (x10 (x9 x4) (x9 (x9 x4))))) ⟶ x0 x4 (x10 (x10 (x9 x4) (x9 (x9 x4))) (x8 (x9 (x9 x4)))) ⟶ not (x0 (x8 x5) (x9 (x9 x5))) ⟶ not (x0 (x8 x5) (x10 x6 (x9 (x9 x5)))) ⟶ not (x0 (x12 x6 (x9 x4)) x7) ⟶ x0 (x9 (x9 x4)) (x10 (x9 (x9 (x9 x4))) x7) ⟶ not (x0 (x12 x6 (x9 x4)) (x10 (x8 (x9 x5)) (x9 (x8 x5)))) ⟶ x0 (x8 x5) (x10 (x12 (x8 x5) (x8 (x9 x5))) (x10 (x8 (x9 x5)) (x9 (x8 x5)))) ⟶ not (x0 (x12 (x8 x5) x5) (x10 x7 (x9 (x8 x5)))) ⟶ x0 (x8 x5) (x10 x7 (x9 (x8 x5))) ⟶ x0 x6 (x10 (x9 (x9 x4)) (x10 x7 (x9 (x8 x5)))) ⟶ (∀ x24 . x1 x24 (x10 (x9 x4) (x9 (x9 x4))) ⟶ not (x0 (x9 x4) x24) ⟶ x0 x4 x24 ⟶ or (or (or (x24 = x3) (x24 = x9 x4)) (x24 = x9 (x9 x4))) (x24 = x10 (x9 x4) (x9 (x9 x4)))) ⟶ (∀ x24 . x0 x24 (x12 (x8 x5) (x8 (x9 x5))) ⟶ or (or (x24 = x4) (x24 = x9 x4)) (x24 = x5)) ⟶ x1 x6 (x10 x6 (x9 (x9 x5))) ⟶ not (x1 (x10 x6 (x9 (x9 x5))) x6) ⟶ x1 x7 (x10 (x9 (x9 x4)) (x10 x7 (x9 (x8 x5)))) ⟶ not (x1 (x12 x7 (x9 x4)) (x12 x6 (x9 x4))) ⟶ x1 (x8 (x9 (x9 x4))) (x10 (x12 (x8 x5) (x8 (x9 x5))) (x8 (x9 (x9 x4)))) ⟶ not (x1 (x10 (x9 (x9 x4)) (x10 x7 (x9 (x8 x5)))) (x10 x7 (x9 (x8 x5)))) ⟶ x12 x5 (x9 x4) = x4 ⟶ x12 x6 (x9 x3) = x12 (x8 x5) (x8 (x9 x4)) ⟶ x1 (x12 (x12 (x8 x5) (x9 x5)) (x9 x3)) (x10 (x9 x4) (x9 (x9 x4))) ⟶ (∀ x24 . x0 x24 (x12 (x8 x5) (x8 (x9 x5))) ⟶ not (x24 = x4) ⟶ x0 x24 (x12 (x8 x5) x5)) ⟶ x1 (x12 (x8 x5) (x9 (x9 x4))) x6 ⟶ x1 x6 (x12 (x8 x5) (x9 (x9 x4))) ⟶ (∀ x24 . x0 x24 (x10 (x12 (x8 x5) (x8 (x9 x5))) (x8 (x9 (x9 x4)))) ⟶ not (x24 = x3) ⟶ x0 x24 (x10 (x12 (x8 x5) (x8 (x9 x5))) (x9 (x9 (x9 x4))))) ⟶ x1 (x10 (x9 x4) (x9 x6)) (x12 (x12 x7 (x8 (x9 x5))) (x9 x5)) ⟶ x1 (x10 (x9 x5) (x8 (x9 x5))) (x10 (x8 x5) (x9 (x9 x5))) ⟶ x1 (x8 (x9 x5)) (x10 (x9 (x9 x5)) x7) ⟶ x1 (x8 (x9 x5)) (x10 (x12 (x8 x5) (x8 (x9 x5))) (x10 (x8 (x9 x5)) (x9 (x8 x5)))) ⟶ x1 (x12 x6 (x9 x4)) (x10 (x9 (x9 x4)) x7) ⟶ x11 (x10 (x8 x5) (x9 (x9 x5))) (x12 x7 (x9 x4)) = x12 x6 (x9 x4) ⟶ x11 (x10 x7 (x9 (x8 x5))) (x10 (x9 x5) (x8 (x9 x5))) = x12 x6 (x9 x4) ⟶ not (x13 (x9 (x8 x5))) ⟶ not (x14 (x8 (x9 (x9 x4)))) ⟶ not (x14 (x10 (x9 (x9 x4)) (x9 (x9 (x9 x4))))) ⟶ not (x14 (x10 x4 (x9 x6))) ⟶ (∀ x24 . x0 x24 x6 ⟶ not (x14 (x12 x6 (x9 x24)))) ⟶ not (x16 (x10 (x9 x4) (x10 (x8 (x9 x5)) (x9 (x8 x5))))) ⟶ (∀ x24 . x0 x24 (x10 (x9 x5) (x10 (x8 (x9 x5)) (x9 (x8 x5)))) ⟶ not (x15 (x12 (x10 (x9 x5) (x10 (x8 (x9 x5)) (x9 (x8 x5)))) (x9 x24)))) ⟶ not (x17 (x10 (x9 (x9 x4)) x7)) ⟶ x13 (x12 x7 x5) ⟶ x15 (x10 x6 (x9 (x8 x5))) ⟶ x19 x5 ⟶ x19 (x10 (x9 x4) (x9 (x9 x4))) ⟶ x19 (x12 x7 x5) ⟶ x19 (x10 (x9 x6) (x9 (x8 x5))) ⟶ x21 (x10 x5 (x10 (x9 x6) (x9 (x8 x5)))) ⟶ x21 (x11 (x10 (x9 (x9 x4)) (x10 (x9 (x9 x5)) x7)) (x10 x7 (x9 (x12 (x8 x5) x5)))) ⟶ x20 (x12 (x10 x6 (x9 (x8 x5))) (x9 x3)) ⟶ x22 (x10 (x9 (x9 x4)) x7) ⟶ x20 (x12 (x10 x7 (x9 (x8 x5))) (x12 (x8 x5) (x8 (x9 x5)))) ⟶ x22 (x12 (x10 (x9 (x9 x5)) (x10 x7 (x9 (x8 x5)))) (x9 x4)) ⟶ x1 (x12 (x11 (x10 (x12 (x8 x5) (x8 (x9 x5))) (x10 (x8 (x9 x5)) (x9 (x8 x5)))) (x10 (x9 (x9 x5)) (x10 x7 (x9 (x8 x5))))) (x9 x3)) (x10 (x12 (x8 x5) (x8 (x9 x4))) (x10 (x9 (x9 x5)) (x9 (x8 x5)))) ⟶ x1 (x12 (x11 (x10 (x12 (x8 x5) (x8 (x9 x5))) (x10 (x8 (x9 x5)) (x9 (x8 x5)))) (x10 (x9 (x9 x5)) (x10 x7 (x9 (x8 x5))))) (x9 (x9 x5))) (x10 x6 (x9 (x8 x5))) ⟶ not (x16 (x12 (x11 (x10 (x12 (x8 x5) (x8 (x9 x5))) (x10 (x8 (x9 x5)) (x9 (x8 x5)))) (x10 (x9 (x9 x5)) (x10 x7 (x9 (x8 x5))))) (x9 x4))) ⟶ not (x0 (x9 x4) (x8 (x9 (x9 x4)))) (proof)
Theorem 0d2eb.. : ∀ 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 . iff (x15 x24) (∀ x25 : ο . (∀ x26 . and (x1 x26 x24) (and (not (x1 x24 x26)) (x14 x26)) ⟶ x25) ⟶ x25)) ⟶ (∀ x24 . iff (x20 x24) (and (x14 x24) (not (x15 x24)))) ⟶ (∀ x24 x25 . iff (x0 x25 (x8 x24)) (x1 x25 x24)) ⟶ (∀ x24 x25 x26 . x0 x26 x24 ⟶ x0 x26 (x10 x24 x25)) ⟶ (∀ x24 x25 x26 . x0 x25 x24 ⟶ x0 x26 x24 ⟶ not (x25 = x26) ⟶ x13 x24) ⟶ (∀ x24 x25 . x1 x24 x25 ⟶ x15 x24 ⟶ x15 x25) ⟶ (∀ x24 x25 . x1 x24 x25 ⟶ x16 x24 ⟶ x16 x25) ⟶ (∀ x24 x25 . x15 (x10 x24 x25) ⟶ or (x14 x24) (x13 x25)) ⟶ (∀ x24 x25 . x16 x24 ⟶ not (x14 (x11 x24 x25)) ⟶ x14 (x12 x24 x25)) ⟶ (∀ x24 . x1 x24 x5 ⟶ not (x0 x3 x24) ⟶ not (x0 x4 x24) ⟶ x24 = x3) ⟶ not (x3 = x9 x4) ⟶ not (x1 x5 (x9 x4)) ⟶ not (x0 x3 (x12 (x8 x5) x5)) ⟶ not (x9 x4 = x10 (x9 x4) (x9 (x9 x4))) ⟶ not (x9 x4 = x12 (x8 x5) x5) ⟶ not (x9 x4 = x8 x5) ⟶ (∀ x24 . x1 x24 (x8 (x9 x4)) ⟶ x0 (x9 x4) x24 ⟶ or (or (or (x24 = x3) (x24 = x4)) (x24 = x9 (x9 x4))) (x24 = x8 (x9 x4))) ⟶ (∀ x24 . x1 x24 (x8 (x9 x4)) ⟶ not (x0 (x9 x4) x24) ⟶ or (or (or (x24 = x3) (x24 = x4)) (x24 = x9 (x9 x4))) (x24 = x8 (x9 x4))) ⟶ not (x0 (x12 x6 (x9 x4)) (x9 x5)) ⟶ not (x0 (x12 (x8 x5) x5) x6) ⟶ x1 (x12 (x8 x5) x5) (x12 (x8 x5) (x9 x4)) ⟶ not (x1 (x8 x5) (x12 (x8 x5) (x8 (x9 x5)))) ⟶ not (x12 (x8 x5) (x8 (x9 x5)) = x8 x5) ⟶ x0 (x9 (x9 x4)) (x8 (x9 (x9 x4))) ⟶ x0 (x9 (x9 x4)) (x8 (x8 (x9 x4))) ⟶ x0 x3 (x8 (x10 (x9 x4) (x9 (x9 x4)))) ⟶ x0 (x9 (x9 x4)) (x10 (x10 (x9 x4) (x9 (x9 x4))) (x8 (x9 (x9 x4)))) ⟶ x0 x5 (x10 (x12 (x8 x5) (x8 (x9 x5))) (x9 (x9 (x9 x4)))) ⟶ not (x0 (x12 (x8 x5) x5) (x9 (x9 x5))) ⟶ not (x0 x6 (x10 (x8 x5) (x9 (x9 x5)))) ⟶ not (x0 (x8 x5) (x10 x6 (x9 (x9 x5)))) ⟶ not (x0 x5 (x9 x6)) ⟶ x0 x6 (x10 (x10 (x9 x4) (x9 (x9 x4))) (x10 (x8 (x9 x5)) (x9 x6))) ⟶ x0 (x9 x4) (x10 (x9 (x9 x4)) (x10 (x9 (x9 x5)) x7)) ⟶ x0 (x12 (x8 x5) (x8 (x9 x5))) (x10 (x12 (x8 x5) (x9 x5)) (x9 (x12 (x8 x5) (x8 (x9 x5))))) ⟶ x0 (x8 x5) (x10 x4 (x9 (x8 x5))) ⟶ x0 (x8 x5) (x10 (x9 (x9 (x9 x4))) (x10 x4 (x9 (x8 x5)))) ⟶ x0 x5 (x10 (x12 (x8 x5) (x8 (x9 x4))) (x10 (x9 (x9 x5)) (x9 (x8 x5)))) ⟶ x0 x3 (x10 (x9 (x9 x5)) (x10 x7 (x9 (x8 x5)))) ⟶ (∀ x24 . x0 x24 (x10 (x12 (x8 x5) (x8 (x9 x5))) (x8 (x9 (x9 x4)))) ⟶ or (or (or (or (x24 = x3) (x24 = x4)) (x24 = x9 x4)) (x24 = x5)) (x24 = x9 (x9 x4))) ⟶ (∀ x24 . x0 x24 (x12 x7 (x9 x5)) ⟶ or (or (x24 = x3) (x24 = x4)) (x24 = x6)) ⟶ not (x1 (x10 (x12 (x8 x5) (x8 (x9 x4))) (x8 (x9 (x9 x4)))) x6) ⟶ x1 x7 (x10 x7 (x9 (x12 (x8 x5) x5))) ⟶ x1 (x10 x7 (x9 (x8 x5))) (x10 (x9 (x9 x5)) (x10 x7 (x9 (x8 x5)))) ⟶ x12 x6 (x9 x3) = x12 (x8 x5) (x8 (x9 x4)) ⟶ x1 (x9 x5) (x12 (x12 (x8 x5) (x8 (x9 x4))) (x9 x4)) ⟶ x12 (x12 (x8 x5) (x9 x4)) (x9 (x9 x4)) = x12 x6 (x9 x4) ⟶ x1 (x8 (x9 x4)) (x12 (x12 (x8 x5) (x9 x4)) (x9 x5)) ⟶ x12 (x12 (x8 x5) (x8 (x9 x5))) (x9 x5) = x10 (x9 x4) (x9 (x9 x4)) ⟶ (∀ x24 . x0 x24 (x8 x5) ⟶ not (x24 = x9 x4) ⟶ x0 x24 x6) ⟶ (∀ x24 . x0 x24 (x10 (x12 (x8 x5) (x8 (x9 x5))) (x8 (x9 (x9 x4)))) ⟶ not (x24 = x9 x4) ⟶ x0 x24 (x10 (x12 (x8 x5) (x8 (x9 x4))) (x8 (x9 (x9 x4))))) ⟶ (∀ x24 . x0 x24 (x10 (x12 (x8 x5) (x8 (x9 x5))) (x8 (x9 (x9 x4)))) ⟶ not (x24 = x9 (x9 x4)) ⟶ x0 x24 (x8 x5)) ⟶ x1 (x12 (x12 x7 x5) (x9 x5)) (x9 x6) ⟶ x12 (x12 x7 (x9 x4)) (x9 x6) = x12 x6 (x9 x4) ⟶ x12 (x12 x7 (x8 (x9 x5))) (x9 x4) = x12 x7 x5 ⟶ (∀ x24 . x0 x24 (x12 x7 (x8 (x9 x5))) ⟶ not (x24 = x5) ⟶ x0 x24 (x10 (x9 x4) (x9 x6))) ⟶ (∀ x24 . x0 x24 x7 ⟶ not (x24 = x3) ⟶ x0 x24 (x12 x7 (x8 (x9 x5)))) ⟶ x1 (x12 x6 (x9 x4)) (x10 x7 (x9 (x8 x5))) ⟶ x1 (x10 (x9 x4) (x8 (x9 x5))) (x10 (x9 (x9 x5)) x7) ⟶ x1 (x12 (x8 x5) (x8 (x9 x4))) (x10 x7 (x9 (x8 x5))) ⟶ x11 (x10 (x8 x5) (x9 (x9 x5))) (x10 (x10 (x9 x5) (x8 (x9 x5))) (x9 (x12 x6 (x9 x4)))) = x10 (x9 x5) (x8 (x9 x5)) ⟶ (∀ x24 . x0 x24 (x10 (x8 x5) (x9 (x9 x5))) ⟶ x0 x24 (x10 (x9 x5) (x10 (x8 (x9 x5)) (x9 (x8 x5)))) ⟶ x0 x24 (x10 (x9 x5) (x8 (x9 x5)))) ⟶ (∀ x24 . x0 x24 (x8 x5) ⟶ or (x0 x24 x6) (x24 = x9 x4)) ⟶ x11 (x10 x7 (x9 (x8 x5))) (x12 (x8 x5) (x8 (x9 x5))) = x12 (x8 x5) (x8 (x9 x4)) ⟶ (∀ x24 . x0 x24 (x12 x6 (x9 x4)) ⟶ not (x13 (x12 (x12 x6 (x9 x4)) (x9 x24)))) ⟶ (∀ x24 . x0 x24 (x12 (x8 x5) (x8 (x9 x4))) ⟶ not (x13 (x12 (x12 (x8 x5) (x8 (x9 x4))) (x9 x24)))) ⟶ not (x14 (x12 (x8 x5) (x8 (x9 x4)))) ⟶ not (x14 (x8 (x9 x5))) ⟶ (∀ x24 . x0 x24 (x10 (x12 (x8 x5) (x8 (x9 x4))) (x10 (x9 (x9 x5)) (x9 (x8 x5)))) ⟶ not (x15 (x12 (x10 (x12 (x8 x5) (x8 (x9 x4))) (x10 (x9 (x9 x5)) (x9 (x8 x5)))) (x9 x24)))) ⟶ not (x18 (x10 (x9 (x9 x4)) (x10 (x9 (x9 x5)) x7))) ⟶ x14 (x12 (x8 x5) (x9 x4)) ⟶ x14 (x12 (x8 (x10 (x9 x4) (x9 (x9 x4)))) (x9 (x10 (x9 x4) (x9 (x9 x4))))) ⟶ x15 (x10 (x12 (x8 x5) (x9 x4)) (x9 (x12 (x8 x5) (x8 (x9 x5))))) ⟶ x16 (x10 (x8 x5) (x9 (x8 x5))) ⟶ x16 (x10 x7 (x9 (x8 x5))) ⟶ x17 (x10 (x9 (x9 x5)) (x10 x7 (x9 (x8 x5)))) ⟶ x20 (x11 (x10 (x8 x5) (x9 (x9 x5))) (x10 x7 (x9 (x12 (x8 x5) x5)))) ⟶ x21 (x10 (x12 (x8 x5) (x9 x5)) (x9 (x12 (x8 x5) (x8 (x9 x5))))) ⟶ x21 (x12 (x10 x7 (x9 (x8 x5))) (x9 x3)) ⟶ x21 (x11 (x10 (x10 (x9 x4) (x9 (x9 x4))) (x10 (x8 (x9 x5)) (x9 x6))) (x10 (x9 (x9 x5)) x7)) ⟶ not (x0 (x8 x5) x6) (proof)
Known 93720..^iffER : ∀ x0 x1 : ο . iff x0 x1 ⟶ x1 ⟶ x0
Known eca40..^orIR : ∀ x0 x1 : ο . x1 ⟶ or x0 x1
Known dcbd9..^orIL : ∀ x0 x1 : ο . x0 ⟶ or x0 x1
Theorem 9013d.. : ∀ 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 . iff (x13 x24) (∀ x25 : ο . (∀ x26 . and (x0 x26 x24) (not (x1 x24 (x8 x26))) ⟶ x25) ⟶ x25)) ⟶ (∀ x24 . iff (x0 x24 x6) (or (or (x24 = x3) (x24 = x4)) (x24 = x5))) ⟶ (∀ x24 x25 x26 . iff (x0 x26 (x11 x24 x25)) (and (x0 x26 x24) (x0 x26 x25))) ⟶ (∀ x24 x25 x26 . x0 x26 x25 ⟶ x0 x26 (x10 x24 x25)) ⟶ (∀ x24 x25 x26 . x1 (x10 x24 (x10 x25 x26)) (x10 (x10 x24 x25) x26)) ⟶ (∀ x24 x25 x26 . x1 x26 x25 ⟶ x1 (x12 x24 x25) (x12 x24 x26)) ⟶ (∀ x24 x25 x26 . (∀ x27 . x0 x27 x24 ⟶ not (x0 x27 x25) ⟶ x0 x27 x26) ⟶ x1 (x12 x24 x25) x26) ⟶ (∀ x24 x25 . (∀ x26 . x0 x26 x24 ⟶ not (x0 x26 x25)) ⟶ x2 x24 x25) ⟶ (∀ x24 x25 x26 . not (x0 x26 x24) ⟶ not (x0 x26 (x12 x24 x25))) ⟶ (∀ x24 x25 x26 . x0 x25 x24 ⟶ x0 x26 x24 ⟶ not (x25 = x26) ⟶ x13 x24) ⟶ (∀ x24 x25 . not (x24 = x25) ⟶ x13 (x10 (x9 x24) (x9 x25))) ⟶ (∀ x24 x25 . x1 x24 x25 ⟶ x14 x24 ⟶ x14 x25) ⟶ (∀ x24 x25 . x0 x25 x24 ⟶ x14 x24 ⟶ x13 (x12 x24 (x9 x25))) ⟶ not (x4 = x5) ⟶ (∀ x24 . x0 x24 (x9 x4) ⟶ x24 = x4) ⟶ not (x4 = x9 x4) ⟶ not (x0 (x9 x4) x5) ⟶ x0 x4 (x12 (x8 x5) (x9 x5)) ⟶ not (x0 (x9 x5) x4) ⟶ not (x0 x3 (x9 (x9 x4))) ⟶ x0 (x9 x4) (x10 (x9 x4) (x9 (x9 x4))) ⟶ x1 x4 (x12 x6 (x9 x4)) ⟶ not (x1 x5 (x12 x6 (x9 x4))) ⟶ (∀ x24 . x1 x24 (x8 (x9 x4)) ⟶ or (or (or (x24 = x3) (x24 = x4)) (x24 = x9 (x9 x4))) (x24 = x8 (x9 x4))) ⟶ not (x0 (x12 x6 (x9 x4)) (x12 (x8 x5) (x8 (x9 x5)))) ⟶ not (x0 (x8 x5) (x8 (x8 (x9 x4)))) ⟶ x0 (x9 (x9 x4)) (x10 (x9 (x9 x4)) (x9 (x9 (x9 x4)))) ⟶ not (x0 x3 (x9 (x10 (x9 x4) (x9 (x9 x4))))) ⟶ x0 x4 (x10 (x12 (x8 x5) (x8 (x9 x5))) (x8 (x9 (x9 x4)))) ⟶ x0 x5 (x10 (x12 (x8 x5) (x8 (x9 x5))) (x8 (x9 (x9 x4)))) ⟶ x0 x3 (x10 (x9 x5) (x8 (x9 x5))) ⟶ x0 (x12 x6 (x9 x4)) (x8 (x12 x6 (x9 x4))) ⟶ x0 (x8 x5) (x10 x6 (x9 (x8 x5))) ⟶ (∀ x24 . x0 x24 (x10 (x12 (x8 x5) (x8 (x9 x4))) (x8 (x9 (x9 x4)))) ⟶ or (or (or (x24 = x3) (x24 = x4)) (x24 = x5)) (x24 = x9 (x9 x4))) ⟶ not (x1 (x10 (x9 x4) (x8 (x9 x5))) x5) ⟶ x1 x7 (x10 (x9 (x9 x4)) x7) ⟶ not (x1 (x10 x7 (x9 (x12 (x8 x5) x5))) x7) ⟶ x1 (x12 (x8 x5) (x8 (x9 x4))) (x10 (x12 (x8 x5) (x8 (x9 x5))) (x8 (x9 (x9 x4)))) ⟶ x1 (x12 (x12 (x8 x5) (x9 x5)) (x9 x3)) (x10 (x9 x4) (x9 (x9 x4))) ⟶ x12 (x12 (x8 x5) (x8 (x9 x4))) (x9 x4) = x9 x5 ⟶ x1 (x12 (x12 (x8 x5) (x9 x4)) (x9 x5)) (x8 (x9 x4)) ⟶ x12 (x12 (x8 (x10 (x9 x4) (x9 (x9 x4)))) (x9 (x10 (x9 x4) (x9 (x9 x4))))) (x9 (x9 (x9 x4))) = x8 (x9 x4) ⟶ x1 x6 (x10 (x8 x5) (x9 (x9 x5))) ⟶ (∀ x24 . x0 x24 (x12 (x8 x5) (x8 (x9 x4))) ⟶ not (x13 (x12 (x12 (x8 x5) (x8 (x9 x4))) (x9 x24)))) ⟶ (∀ x24 . x0 x24 (x12 (x8 x5) x5) ⟶ not (x13 (x12 (x12 (x8 x5) x5) (x9 x24)))) ⟶ (∀ x24 . x0 x24 x7 ⟶ not (x0 x24 x5) ⟶ not (x13 (x12 (x12 x7 x5) (x9 x24)))) ⟶ not (x15 (x12 x7 (x9 x4))) ⟶ not (x15 (x10 x5 (x9 (x8 x5)))) ⟶ (∀ x24 . x16 (x12 (x10 (x12 (x8 x5) (x8 (x9 x5))) (x8 (x9 (x9 x4)))) (x9 x24)) ⟶ not (x24 = x4)) ⟶ not (x18 (x10 (x9 (x9 x5)) (x10 x7 (x9 (x8 x5))))) ⟶ x13 (x12 x6 (x9 x4)) ⟶ x15 (x10 (x12 (x8 x5) (x9 x5)) (x9 (x12 (x8 x5) (x8 (x9 x5))))) ⟶ x19 (x12 (x8 x5) (x8 (x9 x4))) ⟶ x19 (x10 x4 (x9 (x8 x5))) ⟶ x19 (x12 (x12 x7 (x9 x5)) (x9 x4)) ⟶ x1 (x12 (x11 (x10 x6 (x9 (x12 x6 (x9 x4)))) (x8 (x12 x6 (x9 x4)))) (x9 x3)) (x10 (x9 x4) (x9 (x12 x6 (x9 x4)))) ⟶ x20 (x12 x7 (x9 x3)) ⟶ x21 (x10 x5 (x10 (x9 x6) (x9 (x8 x5)))) ⟶ x21 (x12 (x10 (x12 (x8 x5) (x8 (x9 x5))) (x8 (x9 (x9 x4)))) (x9 x3)) ⟶ x1 (x12 (x11 (x10 (x10 (x9 x4) (x9 (x9 x4))) (x10 (x8 (x9 x5)) (x9 x6))) (x10 (x9 (x9 x5)) x7)) (x9 x4)) (x10 (x8 (x9 x5)) (x9 x6)) ⟶ x22 (x12 (x10 (x9 (x9 x4)) (x10 x7 (x9 (x8 x5)))) (x9 x6)) ⟶ not (x9 x5 = x6) (proof)
Theorem 67e67.. : ∀ 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 . iff (x2 x24 x25) (x11 x24 x25 = x3)) ⟶ (∀ x24 x25 . iff (x0 x25 (x9 x24)) (x25 = x24)) ⟶ x0 x4 x7 ⟶ (∀ x24 x25 x26 . x0 x26 (x11 x24 x25) ⟶ x0 x26 x25) ⟶ (∀ x24 x25 x26 . x0 x26 x24 ⟶ not (x0 x26 x25) ⟶ x0 x26 (x12 x24 x25)) ⟶ (∀ x24 x25 . x1 (x10 x24 x25) (x10 x25 x24)) ⟶ (∀ x24 x25 x26 . x2 x24 x25 ⟶ x1 (x10 x24 x25) (x10 x24 x26) ⟶ x1 x25 x26) ⟶ (∀ x24 x25 . x0 x24 x25 ⟶ x13 (x8 x25)) ⟶ (∀ x24 x25 . x0 x25 x24 ⟶ not (x17 x24) ⟶ not (x16 (x12 x24 (x9 x25)))) ⟶ (∀ x24 x25 . x1 x24 (x10 (x12 x24 x25) (x11 x24 x25))) ⟶ (∀ x24 x25 . x0 x25 x24 ⟶ x20 x24 ⟶ x19 (x12 x24 (x9 x25))) ⟶ not (x3 = x4) ⟶ not (x0 (x9 x4) x3) ⟶ not (x1 (x12 (x8 x5) (x8 (x9 x5))) x5) ⟶ x1 (x9 (x9 x4)) (x10 (x9 x4) (x9 (x9 x4))) ⟶ (∀ x24 . x0 (x9 x4) x24 ⟶ x0 x3 x24 ⟶ x1 (x8 (x9 x4)) x24) ⟶ not (x1 (x8 x5) (x8 (x9 x4))) ⟶ not (x1 (x12 (x8 x5) (x9 x5)) (x10 (x9 x4) (x9 (x9 x4)))) ⟶ not (x0 x6 (x8 x5)) ⟶ not (x0 x6 (x12 x6 (x9 x4))) ⟶ (∀ x24 . x0 x24 (x8 x5) ⟶ or (or (or (x24 = x3) (x24 = x4)) (x24 = x9 x4)) (x24 = x5)) ⟶ not (x12 x6 (x9 x4) = x6) ⟶ not (x0 x4 (x9 (x8 (x9 x4)))) ⟶ x0 (x9 x4) (x10 (x9 (x9 x4)) (x9 (x9 (x9 x4)))) ⟶ x0 (x9 x5) (x9 (x9 x5)) ⟶ not (x0 x5 (x8 (x12 x6 (x9 x4)))) ⟶ not (x0 (x12 (x8 x5) x5) x7) ⟶ x0 (x9 x4) (x10 (x9 (x9 x4)) x7) ⟶ not (x0 (x9 x4) (x12 x7 x5)) ⟶ x0 (x8 (x9 x4)) (x10 (x9 (x8 (x9 x4))) x7) ⟶ not (x0 (x8 x5) (x10 (x9 (x9 x5)) x7)) ⟶ x0 x3 (x10 (x9 (x9 x5)) x7) ⟶ x0 (x12 (x8 x5) (x8 (x9 x5))) (x10 (x12 (x8 x5) (x9 x4)) (x9 (x12 (x8 x5) (x8 (x9 x5))))) ⟶ not (x0 (x9 x4) (x9 (x8 x5))) ⟶ x0 x3 (x10 (x8 (x9 x5)) (x9 (x8 x5))) ⟶ x0 x4 (x10 (x9 (x9 x4)) (x10 x7 (x9 (x8 x5)))) ⟶ not (x0 (x9 x4) (x10 (x9 (x9 x5)) (x10 x7 (x9 (x8 x5))))) ⟶ not (x1 (x12 x7 (x9 x5)) x5) ⟶ x1 (x10 x6 (x9 (x9 x5))) (x10 (x12 (x8 x5) (x8 (x9 x5))) (x10 (x8 (x9 x5)) (x9 (x8 x5)))) ⟶ x1 x7 (x10 (x9 (x9 (x9 x4))) x7) ⟶ x1 (x12 (x8 x5) (x9 x4)) (x10 (x12 (x8 x5) (x9 x4)) (x9 (x12 (x8 x5) (x8 (x9 x5))))) ⟶ x1 (x12 x5 (x9 x3)) (x9 x4) ⟶ (∀ x24 . x0 x24 x6 ⟶ not (x24 = x3) ⟶ x0 x24 (x12 (x8 x5) (x8 (x9 x4)))) ⟶ x1 (x12 (x12 (x8 x5) x5) (x9 x5)) (x9 (x9 x4)) ⟶ x12 (x12 (x8 x5) x5) (x9 x5) = x9 (x9 x4) ⟶ x12 (x12 (x8 x5) (x9 x4)) (x9 (x9 x4)) = x12 x6 (x9 x4) ⟶ x1 (x8 (x9 x4)) (x12 (x12 (x8 x5) (x9 x4)) (x9 x5)) ⟶ (∀ x24 . x0 x24 (x10 (x12 (x8 x5) (x8 (x9 x5))) (x8 (x9 (x9 x4)))) ⟶ not (x24 = x4) ⟶ x0 x24 (x10 (x12 (x8 x5) x5) (x8 (x9 (x9 x4))))) ⟶ x1 (x10 (x12 (x8 x5) (x8 (x9 x4))) (x8 (x9 (x9 x4)))) (x12 (x10 (x12 (x8 x5) (x8 (x9 x5))) (x8 (x9 (x9 x4)))) (x9 (x9 x4))) ⟶ (∀ x24 . x0 x24 (x10 (x12 (x8 x5) (x8 (x9 x5))) (x8 (x9 (x9 x4)))) ⟶ not (x24 = x9 (x9 x4)) ⟶ x0 x24 (x8 x5)) ⟶ x12 (x10 (x12 (x8 x5) (x8 (x9 x5))) (x8 (x9 (x9 x4)))) (x9 (x9 (x9 x4))) = x8 x5 ⟶ (∀ x24 . x0 x24 (x12 x7 (x8 (x9 x5))) ⟶ not (x24 = x6) ⟶ x0 x24 (x12 (x8 x5) (x8 (x9 x4)))) ⟶ (∀ x24 . x0 x24 x7 ⟶ not (x24 = x3) ⟶ x0 x24 (x12 x7 (x8 (x9 x5)))) ⟶ x1 (x12 x7 (x8 (x9 x5))) (x12 x7 (x9 x3)) ⟶ x1 (x10 x6 (x9 (x9 x5))) (x10 (x8 x5) (x9 (x9 x5))) ⟶ x1 (x10 (x9 x4) (x8 (x9 x5))) (x10 (x10 (x9 x4) (x9 (x9 x4))) (x8 (x9 x5))) ⟶ x1 (x12 x6 (x9 x4)) x7 ⟶ (∀ x24 . x0 x24 x6 ⟶ x0 x24 (x8 (x12 x6 (x9 x4))) ⟶ x0 x24 x5) ⟶ not (x14 x5) ⟶ not (x14 (x8 (x9 x5))) ⟶ (∀ x24 . x0 x24 x7 ⟶ not (x24 = x4) ⟶ not (x14 (x12 (x12 x7 (x9 x4)) (x9 x24)))) ⟶ not (x16 (x8 x5)) ⟶ (∀ x24 . x0 x24 x7 ⟶ not (x15 (x12 x7 (x9 x24)))) ⟶ not (x16 (x10 (x9 (x9 (x9 x4))) (x10 x5 (x9 (x8 x5))))) ⟶ not (x17 (x10 x7 (x9 (x8 x5)))) ⟶ not (x18 (x10 (x9 (x9 x4)) (x10 x7 (x9 (x8 x5))))) ⟶ x15 x7 ⟶ x15 (x10 x6 (x9 (x12 (x8 x5) x5))) ⟶ x15 (x10 (x9 (x9 (x9 x4))) (x10 x5 (x9 (x8 x5)))) ⟶ x16 (x10 (x9 (x8 (x9 x4))) x7) ⟶ x17 (x10 (x9 (x9 x4)) (x10 x7 (x9 (x8 x5)))) ⟶ x20 (x12 (x8 (x10 (x9 x4) (x9 (x9 x4)))) (x9 (x10 (x9 x4) (x9 (x9 x4))))) ⟶ x21 (x12 (x10 x7 (x9 (x8 x5))) (x9 x5)) ⟶ (∀ x24 . x0 x24 x7 ⟶ not (x0 x24 (x9 x6)) ⟶ x0 x24 (x10 (x10 (x9 x4) (x9 (x9 x4))) (x10 (x8 (x9 x5)) (x9 x6))) ⟶ x0 x24 (x10 (x9 x4) (x8 (x9 x5)))) ⟶ not (x15 (x12 (x11 (x10 (x10 (x9 x4) (x9 (x9 x4))) (x10 (x8 (x9 x5)) (x9 x6))) (x10 (x9 (x9 x5)) x7)) (x9 x6))) ⟶ x1 (x10 (x8 (x9 x5)) (x9 (x8 x5))) (x10 (x9 x4) (x10 (x8 (x9 x5)) (x9 (x8 x5)))) ⟶ (∀ x24 . x0 x24 (x10 (x8 (x9 x5)) (x9 (x8 x5))) ⟶ not (x16 (x12 (x11 (x10 (x12 (x8 x5) (x8 (x9 x5))) (x10 (x8 (x9 x5)) (x9 (x8 x5)))) (x10 (x9 (x9 x5)) (x10 x7 (x9 (x8 x5))))) (x9 x24)))) ⟶ not (x0 x3 (x9 (x8 x5))) (proof)
Theorem 8de73.. : ∀ 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 . iff (x13 x24) (∀ x25 : ο . (∀ x26 . and (x0 x26 x24) (not (x1 x24 (x8 x26))) ⟶ x25) ⟶ x25)) ⟶ (∀ x24 . iff (x17 x24) (∀ x25 : ο . (∀ x26 . and (x1 x26 x24) (and (not (x1 x24 x26)) (x16 x26)) ⟶ x25) ⟶ x25)) ⟶ (∀ x24 . not (x0 x24 x24)) ⟶ (∀ x24 x25 x26 . x1 x26 x25 ⟶ x1 (x12 x24 x25) (x12 x24 x26)) ⟶ (∀ x24 x25 . x0 x24 x25 ⟶ x13 (x8 x25)) ⟶ (∀ x24 x25 . x0 x25 x24 ⟶ not (x18 x24) ⟶ not (x17 (x12 x24 (x9 x25)))) ⟶ (∀ x24 x25 . x1 x24 x25 ⟶ x14 x24 ⟶ x14 x25) ⟶ (∀ x24 x25 . not (x17 x24) ⟶ x13 (x11 x24 x25) ⟶ not (x15 (x12 x24 x25))) ⟶ (∀ x24 x25 . x0 x25 x24 ⟶ x16 x24 ⟶ x15 (x12 x24 (x9 x25))) ⟶ (∀ x24 x25 . x0 x25 x24 ⟶ x14 (x12 x24 (x9 x25)) ⟶ x15 x24) ⟶ (∀ x24 x25 . x2 x24 x25 ⟶ x19 x24 ⟶ x19 x25 ⟶ x21 (x10 x24 x25)) ⟶ not (x0 x3 x3) ⟶ not (x3 = x12 (x8 x5) x5) ⟶ x0 (x9 x4) (x10 (x9 x4) (x9 (x9 x4))) ⟶ not (x1 x5 (x9 x5)) ⟶ not (x1 (x9 x4) (x9 x5)) ⟶ not (x1 (x9 x4) (x9 (x9 x4))) ⟶ not (x0 (x9 x4) x6) ⟶ not (x0 (x9 x4) (x12 (x8 x5) (x8 (x9 x4)))) ⟶ (∀ x24 . x1 x24 (x8 (x9 x4)) ⟶ not (x0 (x9 x4) x24) ⟶ not (x0 x3 x24) ⟶ or (or (or (x24 = x3) (x24 = x4)) (x24 = x9 (x9 x4))) (x24 = x8 (x9 x4))) ⟶ not (x0 (x12 (x8 x5) (x8 (x9 x5))) (x12 (x8 x5) (x9 x5))) ⟶ not (x0 (x9 (x9 x4)) x6) ⟶ not (x3 = x8 x5) ⟶ not (x8 (x9 x4) = x6) ⟶ (∀ x24 . x0 x24 (x12 (x8 x5) x5) ⟶ or (x24 = x9 x4) (x24 = x5)) ⟶ not (x1 (x8 x5) (x12 (x8 x5) (x8 (x9 x5)))) ⟶ x0 x3 (x12 (x8 (x8 (x9 x4))) (x9 (x8 (x9 x4)))) ⟶ x0 (x9 x5) (x9 (x9 x5)) ⟶ not (x0 (x8 x5) (x9 (x9 x5))) ⟶ x0 x3 (x10 (x9 x4) (x8 (x9 x5))) ⟶ not (x0 (x12 x6 (x9 x4)) (x10 (x8 x5) (x9 (x9 x5)))) ⟶ not (x0 (x12 (x8 x5) x5) (x10 (x8 x5) (x9 (x9 x5)))) ⟶ x0 x6 (x12 x7 (x9 x4)) ⟶ x0 x6 (x12 x7 (x8 (x9 x5))) ⟶ x0 x6 (x10 (x8 (x9 x5)) (x9 x6)) ⟶ x0 x4 (x10 (x9 (x9 x5)) x7) ⟶ x0 x5 (x10 (x9 (x9 x4)) (x10 (x9 (x9 x5)) x7)) ⟶ x0 x3 (x10 x4 (x9 (x8 x5))) ⟶ x0 x4 (x10 (x12 (x8 x5) (x8 (x9 x4))) (x10 (x9 (x9 x5)) (x9 (x8 x5)))) ⟶ not (x0 (x9 x5) (x10 x7 (x9 (x8 x5)))) ⟶ (∀ x24 . x1 x24 (x10 (x9 x4) (x9 (x9 x4))) ⟶ x0 (x9 x4) x24 ⟶ not (x0 x4 x24) ⟶ x24 = x9 (x9 x4)) ⟶ (∀ x24 . x1 x24 (x10 (x9 x4) (x9 (x9 x4))) ⟶ not (x0 (x9 x4) x24) ⟶ not (x0 x4 x24) ⟶ or (or (or (x24 = x3) (x24 = x9 x4)) (x24 = x9 (x9 x4))) (x24 = x10 (x9 x4) (x9 (x9 x4)))) ⟶ (∀ x24 . x0 x24 (x12 x7 (x8 (x9 x5))) ⟶ or (or (x24 = x4) (x24 = x5)) (x24 = x6)) ⟶ not (x1 (x10 x5 (x9 (x8 x5))) x5) ⟶ x1 x6 (x10 (x12 (x8 x5) (x8 (x9 x4))) (x8 (x9 (x9 x4)))) ⟶ x1 x7 (x10 (x9 (x9 (x9 x4))) x7) ⟶ x1 x7 (x10 (x9 (x9 x4)) (x10 (x9 (x9 x5)) x7)) ⟶ not (x1 (x12 x7 (x9 x4)) (x12 x6 (x9 x4))) ⟶ x1 (x8 x5) (x10 (x8 x5) (x9 (x8 x5))) ⟶ x1 (x10 (x12 (x8 x5) (x8 (x9 x4))) (x8 (x9 (x9 x4)))) (x10 (x12 (x8 x5) (x8 (x9 x5))) (x8 (x9 (x9 x4)))) ⟶ x1 (x12 (x12 (x8 x5) (x9 x5)) (x9 (x9 x4))) x5 ⟶ x1 (x12 (x12 (x8 x5) (x9 x4)) (x9 x3)) (x12 (x8 x5) x5) ⟶ x1 (x12 (x8 x5) (x8 (x9 x4))) (x12 (x12 (x8 x5) (x8 (x9 x5))) (x9 (x9 x4))) ⟶ x1 (x12 (x12 (x8 (x10 (x9 x4) (x9 (x9 x4)))) (x9 (x10 (x9 x4) (x9 (x9 x4))))) (x9 (x9 x4))) (x8 (x9 (x9 x4))) ⟶ x1 (x12 (x12 (x8 (x10 (x9 x4) (x9 (x9 x4)))) (x9 (x10 (x9 x4) (x9 (x9 x4))))) (x9 (x9 (x9 x4)))) (x8 (x9 x4)) ⟶ x1 (x12 (x10 (x12 (x8 x5) (x8 (x9 x5))) (x8 (x9 (x9 x4)))) (x9 x3)) (x10 (x12 (x8 x5) (x8 (x9 x5))) (x9 (x9 (x9 x4)))) ⟶ x1 (x10 (x12 (x8 x5) x5) (x8 (x9 (x9 x4)))) (x12 (x10 (x12 (x8 x5) (x8 (x9 x5))) (x8 (x9 (x9 x4)))) (x9 x4)) ⟶ x12 (x10 (x12 (x8 x5) (x8 (x9 x5))) (x8 (x9 (x9 x4)))) (x9 x5) = x10 (x10 (x9 x4) (x9 (x9 x4))) (x8 (x9 (x9 x4))) ⟶ x12 (x12 x7 (x9 x5)) (x9 x4) = x10 x4 (x9 x6) ⟶ x1 (x12 (x12 x7 x5) (x9 x5)) (x9 x6) ⟶ x1 (x9 x5) (x12 (x12 x7 x5) (x9 x6)) ⟶ x1 (x12 x6 (x9 x4)) x7 ⟶ x11 (x10 (x9 (x9 x4)) (x10 (x9 (x9 x5)) x7)) (x10 x7 (x9 (x12 (x8 x5) x5))) = x7 ⟶ x11 (x10 x7 (x9 (x12 (x8 x5) x5))) (x10 (x9 (x9 x4)) (x10 x7 (x9 (x8 x5)))) = x7 ⟶ x1 (x12 (x8 x5) (x8 (x9 x4))) (x11 (x10 x7 (x9 (x8 x5))) (x12 (x8 x5) (x8 (x9 x5)))) ⟶ x11 (x10 x7 (x9 (x8 x5))) (x10 (x9 x5) (x8 (x9 x5))) = x12 x6 (x9 x4) ⟶ not (x14 (x10 (x9 x4) (x9 (x9 x4)))) ⟶ not (x14 (x10 (x9 x4) (x9 x6))) ⟶ not (x15 (x12 x7 (x9 x5))) ⟶ x13 (x12 (x8 x5) x5) ⟶ x14 (x12 (x8 x5) (x8 (x9 x5))) ⟶ x15 (x10 (x12 (x8 x5) (x9 x5)) (x9 (x12 (x8 x5) (x8 (x9 x5))))) ⟶ x16 (x10 (x9 (x9 x5)) x7) ⟶ x14 (x11 (x10 x6 (x9 (x12 x6 (x9 x4)))) (x8 (x12 x6 (x9 x4)))) ⟶ x19 (x8 (x9 x5)) ⟶ x20 (x12 (x8 x5) (x9 x4)) ⟶ x20 (x11 (x10 (x8 x5) (x9 (x9 x5))) (x10 (x9 x5) (x10 (x8 (x9 x5)) (x9 (x8 x5))))) ⟶ x20 (x11 (x10 (x10 (x9 x5) (x8 (x9 x5))) (x9 (x12 x6 (x9 x4)))) (x10 (x9 x5) (x10 (x8 (x9 x5)) (x9 (x8 x5))))) ⟶ x1 (x12 (x11 (x10 x6 (x9 (x12 x6 (x9 x4)))) (x8 (x12 x6 (x9 x4)))) (x9 x3)) (x10 (x9 x4) (x9 (x12 x6 (x9 x4)))) ⟶ x21 (x10 (x8 (x9 x4)) (x12 x7 x5)) ⟶ x22 (x10 (x8 x5) (x9 (x9 x5))) ⟶ x21 (x12 (x10 x7 (x9 (x8 x5))) (x9 x4)) ⟶ x1 (x12 (x11 (x10 (x10 (x9 x4) (x9 (x9 x4))) (x10 (x8 (x9 x5)) (x9 x6))) (x10 (x9 (x9 x5)) x7)) (x9 x6)) (x10 (x9 x4) (x8 (x9 x5))) ⟶ not (x16 (x11 (x10 (x10 (x9 x4) (x9 (x9 x4))) (x10 (x8 (x9 x5)) (x9 x6))) (x10 (x9 (x9 x5)) x7))) ⟶ (∀ x24 . x0 x24 (x12 (x8 x5) (x8 (x9 x5))) ⟶ x0 x24 (x10 (x9 (x9 x5)) (x10 x7 (x9 (x8 x5)))) ⟶ x0 x24 (x10 x6 (x9 (x8 x5)))) ⟶ x1 (x12 (x11 (x10 (x12 (x8 x5) (x8 (x9 x5))) (x10 (x8 (x9 x5)) (x9 (x8 x5)))) (x10 (x9 (x9 x5)) (x10 x7 (x9 (x8 x5))))) (x9 (x9 x5))) (x10 x6 (x9 (x8 x5))) ⟶ not (x0 x6 x6) (proof)
Theorem 64754.. : ∀ 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 . iff (x0 x24 x5) (or (x24 = x3) (x24 = x4))) ⟶ (∀ x24 . x0 x24 x4 ⟶ x24 = x3) ⟶ (∀ x24 x25 . x0 x25 (x9 x24) ⟶ x25 = x24) ⟶ (∀ x24 x25 x26 . x0 x26 x24 ⟶ not (x0 x26 x25) ⟶ x0 x26 (x12 x24 x25)) ⟶ (∀ x24 x25 . x1 x25 (x10 x24 x25)) ⟶ (∀ x24 x25 x26 . x0 x26 x25 ⟶ not (x0 x26 (x12 x24 x25))) ⟶ (∀ x24 x25 . x2 x24 x25 ⟶ x13 x24 ⟶ x13 x25 ⟶ x15 (x10 x24 x25)) ⟶ (∀ x24 x25 . x2 x24 x25 ⟶ x13 x24 ⟶ x14 x25 ⟶ x16 (x10 x24 x25)) ⟶ (∀ x24 x25 . x2 x24 x25 ⟶ x13 x24 ⟶ x15 x25 ⟶ x17 (x10 x24 x25)) ⟶ (∀ x24 x25 . x0 x25 x24 ⟶ x20 x24 ⟶ x19 (x12 x24 (x9 x25))) ⟶ (∀ x24 x25 x26 . x1 x26 (x10 x24 x25) ⟶ ∀ x27 . x0 x27 x24 ⟶ not (x0 x27 x26) ⟶ x14 x26 ⟶ x14 (x10 (x12 x24 (x9 x27)) x25)) ⟶ (∀ x24 x25 . x0 x25 x24 ⟶ x23 x24 ⟶ x22 (x12 x24 (x9 x25))) ⟶ (∀ x24 x25 . not (x16 x24) ⟶ not (x17 (x10 x24 (x9 x25)))) ⟶ (∀ x24 x25 . not (x17 x24) ⟶ not (x18 (x10 x24 (x9 x25)))) ⟶ x0 x4 (x10 (x9 x4) (x9 (x9 x4))) ⟶ not (x4 = x9 x4) ⟶ not (x0 (x9 x5) x4) ⟶ not (x0 (x9 x4) (x9 x5)) ⟶ not (x1 x5 (x9 x5)) ⟶ not (x0 (x9 x4) (x9 x4)) ⟶ not (x1 (x12 x6 (x9 x4)) x5) ⟶ (∀ x24 . x1 x24 (x8 (x9 x4)) ⟶ not (x0 (x9 x4) x24) ⟶ x0 x3 x24 ⟶ x24 = x4) ⟶ not (x1 (x12 (x8 x5) (x9 x5)) (x10 (x9 x4) (x9 (x9 x4)))) ⟶ not (x0 x6 (x12 x6 (x9 x4))) ⟶ not (x0 (x12 (x8 x5) x5) x6) ⟶ not (x12 x6 (x9 x4) = x8 x5) ⟶ not (x12 (x8 x5) (x8 (x9 x5)) = x8 x5) ⟶ not (x0 (x9 x4) (x8 (x9 (x9 x4)))) ⟶ x0 (x9 x4) (x8 (x10 (x9 x4) (x9 (x9 x4)))) ⟶ x0 x5 (x10 x6 (x9 (x9 x5))) ⟶ x0 x4 (x8 (x12 x6 (x9 x4))) ⟶ not (x0 x5 (x10 x4 (x9 x6))) ⟶ x0 x6 (x10 (x9 (x9 x5)) x7) ⟶ x0 (x8 x5) (x10 x5 (x9 (x8 x5))) ⟶ x0 x4 (x10 x6 (x9 (x8 x5))) ⟶ x0 (x8 x5) (x10 x6 (x9 (x8 x5))) ⟶ x0 x4 (x10 (x9 (x9 (x9 x4))) (x10 x5 (x9 (x8 x5)))) ⟶ (∀ x24 . x1 x24 (x10 (x9 x4) (x9 (x9 x4))) ⟶ not (x0 (x9 x4) x24) ⟶ x0 x4 x24 ⟶ or (or (or (x24 = x3) (x24 = x9 x4)) (x24 = x9 (x9 x4))) (x24 = x10 (x9 x4) (x9 (x9 x4)))) ⟶ (∀ x24 . x0 x24 (x8 (x9 (x9 x4))) ⟶ or (x24 = x3) (x24 = x9 (x9 x4))) ⟶ (∀ x24 . x0 x24 (x10 (x10 (x9 x4) (x9 (x9 x4))) (x8 (x9 (x9 x4)))) ⟶ or (or (or (x24 = x3) (x24 = x4)) (x24 = x9 x4)) (x24 = x9 (x9 x4))) ⟶ x1 x7 (x10 (x9 (x9 x4)) x7) ⟶ x1 x7 (x10 (x9 (x8 (x9 x4))) x7) ⟶ x1 x7 (x10 x7 (x9 (x12 (x8 x5) x5))) ⟶ x1 (x10 x7 (x9 (x8 x5))) (x10 (x9 (x9 x5)) (x10 x7 (x9 (x8 x5)))) ⟶ x1 x4 (x12 x5 (x9 x4)) ⟶ (∀ x24 . x0 x24 x6 ⟶ not (x24 = x3) ⟶ x0 x24 (x12 (x8 x5) (x8 (x9 x4)))) ⟶ x1 (x12 x6 (x9 x3)) (x12 (x8 x5) (x8 (x9 x4))) ⟶ x1 x5 (x12 x6 (x9 x5)) ⟶ x1 x4 (x12 (x12 x6 (x9 x4)) (x9 x5)) ⟶ x1 (x9 x4) (x12 (x12 (x8 x5) (x8 (x9 x4))) (x9 x5)) ⟶ (∀ x24 . x0 x24 (x12 (x8 x5) (x8 (x9 x5))) ⟶ not (x24 = x9 x4) ⟶ x0 x24 (x12 (x8 x5) (x8 (x9 x4)))) ⟶ x1 (x8 (x9 (x9 x4))) (x12 (x12 (x8 (x10 (x9 x4) (x9 (x9 x4)))) (x9 (x10 (x9 x4) (x9 (x9 x4))))) (x9 (x9 x4))) ⟶ (∀ x24 . x0 x24 (x12 x7 (x9 x5)) ⟶ not (x24 = x4) ⟶ x0 x24 (x10 x4 (x9 x6))) ⟶ x12 (x12 x7 (x9 x5)) (x9 x4) = x10 x4 (x9 x6) ⟶ x12 (x12 x7 (x9 x4)) (x9 x3) = x12 x7 x5 ⟶ x12 (x12 x7 (x8 (x9 x5))) (x9 x4) = x12 x7 x5 ⟶ x1 x6 (x12 x7 (x9 x6)) ⟶ x1 (x10 (x9 x4) (x8 (x9 x5))) (x10 (x10 (x9 x4) (x9 (x9 x4))) (x8 (x9 x5))) ⟶ x1 (x8 (x9 x5)) (x10 x6 (x9 (x9 x5))) ⟶ x11 (x10 x7 (x9 (x12 (x8 x5) x5))) (x10 (x9 (x9 x4)) (x10 x7 (x9 (x8 x5)))) = x7 ⟶ x1 (x11 (x10 (x8 x5) (x9 (x9 x5))) (x12 x7 (x9 x4))) (x12 x6 (x9 x4)) ⟶ not (x14 (x12 (x8 x5) x5)) ⟶ not (x14 (x10 (x9 (x9 x5)) (x9 (x8 x5)))) ⟶ not (x15 (x12 (x8 (x10 (x9 x4) (x9 (x9 x4)))) (x9 (x10 (x9 x4) (x9 (x9 x4)))))) ⟶ not (x15 (x10 (x9 x4) (x8 (x9 x5)))) ⟶ (∀ x24 . x0 x24 (x10 (x8 (x9 x5)) (x9 (x8 x5))) ⟶ not (x14 (x12 (x10 (x8 (x9 x5)) (x9 (x8 x5))) (x9 x24)))) ⟶ (∀ x24 . x0 x24 (x10 (x12 (x8 x5) (x8 (x9 x4))) (x10 (x9 (x9 x5)) (x9 (x8 x5)))) ⟶ not (x15 (x12 (x10 (x12 (x8 x5) (x8 (x9 x4))) (x10 (x9 (x9 x5)) (x9 (x8 x5)))) (x9 x24)))) ⟶ x13 (x12 (x8 x5) (x8 (x9 x4))) ⟶ x14 (x12 x7 (x9 x4)) ⟶ x15 (x10 (x9 (x9 (x9 x4))) (x10 x5 (x9 (x8 x5)))) ⟶ x19 (x10 (x9 (x12 (x8 x5) (x8 (x9 x5)))) (x9 (x8 x5))) ⟶ x20 (x12 (x8 x5) (x9 x4)) ⟶ x20 (x10 x5 (x9 (x8 x5))) ⟶ x20 (x12 (x8 x5) (x9 (x9 x4))) ⟶ x22 (x10 x7 (x9 (x8 x5))) ⟶ (∀ x24 . x0 x24 (x12 (x8 x5) (x8 (x9 x5))) ⟶ x0 x24 (x10 (x9 (x9 x5)) (x10 x7 (x9 (x8 x5)))) ⟶ not (x0 x24 (x9 x4)) ⟶ x0 x24 (x10 (x9 x5) (x10 (x8 (x9 x5)) (x9 (x8 x5))))) ⟶ (∀ x24 . x0 x24 (x12 (x8 x5) (x8 (x9 x5))) ⟶ x0 x24 (x10 (x9 (x9 x5)) (x10 x7 (x9 (x8 x5)))) ⟶ x0 x24 (x10 x6 (x9 (x8 x5)))) ⟶ x1 (x12 (x11 (x10 (x12 (x8 x5) (x8 (x9 x5))) (x10 (x8 (x9 x5)) (x9 (x8 x5)))) (x10 (x9 (x9 x5)) (x10 x7 (x9 (x8 x5))))) (x9 (x9 x5))) (x10 x6 (x9 (x8 x5))) ⟶ not (x16 (x12 (x11 (x10 (x12 (x8 x5) (x8 (x9 x5))) (x10 (x8 (x9 x5)) (x9 (x8 x5)))) (x10 (x9 (x9 x5)) (x10 x7 (x9 (x8 x5))))) (x9 x3))) ⟶ not (x0 x3 (x12 (x8 x5) x5)) (proof)
Theorem 67f36.. : ∀ 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 . iff (x0 x26 (x11 x24 x25)) (and (x0 x26 x24) (x0 x26 x25))) ⟶ (∀ x24 x25 x26 . x0 x26 x24 ⟶ not (x0 x26 x25) ⟶ x0 x26 (x12 x24 x25)) ⟶ (∀ x24 x25 . x1 x24 (x10 x24 x25)) ⟶ (∀ x24 x25 x26 . x1 x25 x26 ⟶ x1 (x10 x24 x25) (x10 x24 x26)) ⟶ (∀ x24 x25 x26 . x2 x24 x25 ⟶ x0 x26 x24 ⟶ not (x0 x26 x25)) ⟶ (∀ x24 x25 . x0 x25 x24 ⟶ not (x1 x24 (x12 x24 (x9 x25)))) ⟶ (∀ x24 x25 . x1 x25 x24 ⟶ not (x1 x24 x25) ⟶ ∀ x26 : ο . (∀ x27 . and (x0 x27 x24) (x1 x25 (x12 x24 (x9 x27))) ⟶ x26) ⟶ x26) ⟶ (∀ x24 x25 . x1 x24 x25 ⟶ x16 x24 ⟶ x16 x25) ⟶ (∀ x24 x25 . x0 x25 x24 ⟶ x16 x24 ⟶ x15 (x12 x24 (x9 x25))) ⟶ (∀ x24 x25 . not (x15 x24) ⟶ not (x16 (x10 x24 (x9 x25)))) ⟶ (∀ x24 x25 . x0 x25 x24 ⟶ x23 x24 ⟶ x22 (x12 x24 (x9 x25))) ⟶ not (x0 x5 x3) ⟶ not (x0 x6 x6) ⟶ not (x1 x6 x5) ⟶ not (x4 = x5) ⟶ not (x3 = x6) ⟶ (∀ x24 . x1 x24 (x9 x4) ⟶ or (x24 = x3) (x24 = x9 x4)) ⟶ x0 (x9 x4) (x9 (x9 x4)) ⟶ x0 x3 (x8 (x9 x4)) ⟶ not (x0 x3 (x9 x5)) ⟶ (∀ x24 . x0 x24 (x9 x4) ⟶ x24 = x4) ⟶ not (x3 = x9 x4) ⟶ not (x0 (x9 x4) x5) ⟶ not (x0 (x9 x4) (x9 x4)) ⟶ x1 (x9 x4) (x12 (x8 x5) (x9 x5)) ⟶ not (x4 = x9 (x9 x4)) ⟶ not (x0 (x12 (x8 x5) x5) (x9 (x9 x4))) ⟶ x1 (x9 (x9 x4)) (x10 (x9 x4) (x9 (x9 x4))) ⟶ not (x1 (x8 x5) (x9 (x9 x4))) ⟶ not (x0 (x9 x5) x6) ⟶ (∀ x24 . x0 x24 (x8 x5) ⟶ or (or (or (x24 = x3) (x24 = x4)) (x24 = x9 x4)) (x24 = x5)) ⟶ not (x9 (x9 x4) = x6) ⟶ not (x0 (x8 x5) (x8 (x8 (x9 x4)))) ⟶ x0 x4 (x10 (x12 (x8 x5) (x8 (x9 x4))) (x8 (x9 (x9 x4)))) ⟶ x0 (x9 (x9 x4)) (x10 (x12 (x8 x5) x5) (x8 (x9 (x9 x4)))) ⟶ not (x0 (x9 x4) (x9 (x9 x5))) ⟶ not (x0 x6 (x9 (x9 x5))) ⟶ not (x0 (x12 (x8 x5) x5) (x9 (x9 x5))) ⟶ x0 x3 (x8 (x12 x6 (x9 x4))) ⟶ x0 (x12 x6 (x9 x4)) (x10 x6 (x9 (x12 x6 (x9 x4)))) ⟶ not (x0 (x9 (x9 x4)) x7) ⟶ x0 (x9 x4) (x10 (x9 (x9 x4)) x7) ⟶ x0 x6 (x10 (x8 (x9 x5)) (x9 x6)) ⟶ x0 x4 (x12 (x10 (x9 (x9 x5)) x7) (x12 (x8 x5) (x9 x4))) ⟶ x0 x3 (x10 (x9 (x9 x5)) x7) ⟶ not (x0 (x8 x5) (x10 (x9 (x9 x4)) (x10 (x9 (x9 x5)) x7))) ⟶ x0 (x9 (x9 x4)) (x10 (x9 (x9 (x9 x4))) (x10 x4 (x9 (x8 x5)))) ⟶ x0 (x8 x5) (x10 (x9 (x9 (x9 x4))) (x10 x4 (x9 (x8 x5)))) ⟶ not (x0 (x12 x6 (x9 x4)) (x10 (x9 x5) (x10 (x8 (x9 x5)) (x9 (x8 x5))))) ⟶ x0 (x8 x5) (x10 (x12 (x8 x5) (x8 (x9 x4))) (x10 (x9 (x9 x5)) (x9 (x8 x5)))) ⟶ (∀ x24 . x1 x24 (x10 (x9 x4) (x9 (x9 x4))) ⟶ x0 (x9 x4) x24 ⟶ not (x0 x4 x24) ⟶ x24 = x9 (x9 x4)) ⟶ (∀ x24 . x0 x24 (x9 (x9 (x9 x4))) ⟶ x24 = x9 (x9 x4)) ⟶ (∀ x24 . x0 x24 x7 ⟶ not (x0 x24 x5) ⟶ or (x24 = x5) (x24 = x6)) ⟶ not (x1 (x10 (x9 (x9 (x9 x4))) x7) x7) ⟶ x1 x7 (x10 x7 (x9 (x8 x5))) ⟶ x1 (x8 (x9 (x9 x4))) (x12 (x8 (x10 (x9 x4) (x9 (x9 x4)))) (x9 (x10 (x9 x4) (x9 (x9 x4))))) ⟶ not (x1 (x10 (x9 (x9 (x9 x4))) (x10 x5 (x9 (x8 x5)))) (x12 (x8 (x8 (x9 x4))) (x9 (x8 (x9 x4))))) ⟶ x1 (x9 x4) (x12 (x12 (x8 x5) (x8 (x9 x4))) (x9 x5)) ⟶ x1 (x12 (x12 (x8 x5) (x8 (x9 x5))) (x9 (x9 x4))) (x12 (x8 x5) (x8 (x9 x4))) ⟶ x12 (x12 (x8 x5) (x8 (x9 x5))) (x9 x5) = x10 (x9 x4) (x9 (x9 x4)) ⟶ x12 (x8 x5) (x9 x3) = x12 (x8 x5) (x8 (x9 x5)) ⟶ x12 (x12 x7 x5) (x9 x6) = x9 x5 ⟶ (∀ x24 . x0 x24 (x12 x7 (x8 (x9 x5))) ⟶ not (x24 = x6) ⟶ x0 x24 (x12 (x8 x5) (x8 (x9 x4)))) ⟶ (∀ x24 . x0 x24 x7 ⟶ not (x24 = x3) ⟶ x0 x24 (x12 x7 (x8 (x9 x5)))) ⟶ x12 x7 (x9 x6) = x6 ⟶ x1 x5 (x10 x6 (x9 (x12 x6 (x9 x4)))) ⟶ x1 (x12 x6 (x9 x4)) (x10 (x8 x5) (x9 (x9 x5))) ⟶ x11 (x10 (x8 x5) (x9 (x9 x5))) (x10 x7 (x9 (x12 (x8 x5) x5))) = x6 ⟶ x11 (x10 (x8 x5) (x9 (x9 x5))) (x10 (x9 (x9 x5)) (x10 x7 (x9 (x8 x5)))) = x10 x6 (x9 (x9 x5)) ⟶ x11 (x10 (x9 (x9 x4)) (x10 (x9 (x9 x5)) x7)) (x10 (x9 x5) (x10 (x8 (x9 x5)) (x9 (x8 x5)))) = x10 (x9 x5) (x8 (x9 x5)) ⟶ x1 (x12 x6 (x9 x4)) (x11 (x10 x7 (x9 (x8 x5))) (x10 (x9 x5) (x8 (x9 x5)))) ⟶ not (x14 (x12 (x8 x5) x5)) ⟶ not (x15 (x12 x7 (x8 (x9 x5)))) ⟶ not (x17 (x10 (x8 x5) (x9 (x8 x5)))) ⟶ x13 (x12 (x8 x5) x5) ⟶ x15 x7 ⟶ x19 x5 ⟶ x19 (x12 (x8 x5) (x8 (x9 x4))) ⟶ x19 (x12 (x8 x5) x5) ⟶ (∀ x24 . x0 x24 x6 ⟶ x0 x24 (x8 (x12 x6 (x9 x4))) ⟶ not (x0 x24 (x9 x4)) ⟶ x0 x24 (x10 (x9 x3) (x9 (x12 x6 (x9 x4))))) ⟶ x21 (x10 x5 (x10 (x9 x6) (x9 (x8 x5)))) ⟶ x21 (x12 (x10 x7 (x9 (x8 x5))) (x9 x6)) ⟶ x20 (x12 (x10 (x8 x5) (x9 (x9 x5))) (x12 x7 (x9 x4))) ⟶ x15 (x11 (x10 (x10 (x9 x4) (x9 (x9 x4))) (x10 (x8 (x9 x5)) (x9 x6))) (x10 (x9 (x9 x5)) x7)) ⟶ not (x15 (x12 (x11 (x10 (x10 (x9 x4) (x9 (x9 x4))) (x10 (x8 (x9 x5)) (x9 x6))) (x10 (x9 (x9 x5)) x7)) (x9 x6))) ⟶ x1 (x12 (x8 x5) (x9 x4)) (x10 (x12 (x8 x5) (x9 x4)) (x9 (x12 (x8 x5) (x8 (x9 x5))))) (proof)
Theorem 8cf9e.. : ∀ 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 . iff (x0 x24 x4) (x24 = x3)) ⟶ (∀ x24 . iff (x0 x24 x5) (or (x24 = x3) (x24 = x4))) ⟶ (∀ x24 x25 . iff (x0 x25 (x8 x24)) (x1 x25 x24)) ⟶ (∀ x24 . x1 x24 x3 ⟶ x24 = x3) ⟶ (∀ x24 x25 x26 . x1 x24 x26 ⟶ x1 x25 x26 ⟶ x1 (x10 x24 x25) x26) ⟶ (∀ x24 x25 . x0 x25 x24 ⟶ not (x1 x24 (x12 x24 (x9 x25)))) ⟶ (∀ x24 x25 . not (x0 x25 x24) ⟶ x13 x24 ⟶ x14 (x10 x24 (x9 x25))) ⟶ (∀ x24 x25 . x0 x25 x24 ⟶ x1 (x9 x25) x24) ⟶ (∀ x24 x25 x26 . x1 x26 (x10 x24 x25) ⟶ not (x1 x26 x24) ⟶ not (x1 x26 x25) ⟶ not (x1 (x10 x24 x25) x26) ⟶ or (x13 x24) (x13 x25)) ⟶ (∀ x24 x25 . x17 (x10 x24 x25) ⟶ or (x16 x24) (x13 x25)) ⟶ (∀ x24 x25 . x0 x25 x24 ⟶ x23 x24 ⟶ x22 (x12 x24 (x9 x25))) ⟶ (∀ x24 x25 . x18 (x10 x24 x25) ⟶ or (x17 x24) (x13 x25)) ⟶ (∀ x24 . x0 x3 x24 ⟶ x1 x4 x24) ⟶ (∀ x24 x25 . x1 x25 (x9 x24) ⟶ or (x25 = x3) (x25 = x9 x24)) ⟶ not (x0 x3 (x9 x5)) ⟶ not (x0 x4 (x8 (x9 x4))) ⟶ not (x0 x4 (x8 (x9 x5))) ⟶ not (x0 (x9 (x9 x4)) x5) ⟶ not (x0 (x9 x5) x5) ⟶ x1 (x9 (x9 x4)) (x10 (x9 x4) (x9 (x9 x4))) ⟶ not (x0 (x9 x4) x6) ⟶ not (x0 (x9 x4) (x12 x6 (x9 x4))) ⟶ (∀ x24 . x1 x24 (x8 (x9 x4)) ⟶ not (x0 x3 x24) ⟶ x1 x24 (x9 (x9 x4))) ⟶ (∀ x24 . x1 x24 (x8 (x9 x4)) ⟶ not (x0 (x9 x4) x24) ⟶ x0 x3 x24 ⟶ or (or (or (x24 = x3) (x24 = x4)) (x24 = x9 (x9 x4))) (x24 = x8 (x9 x4))) ⟶ (∀ x24 . x1 x24 (x8 (x9 x4)) ⟶ or (or (or (x24 = x3) (x24 = x4)) (x24 = x9 (x9 x4))) (x24 = x8 (x9 x4))) ⟶ x1 (x12 x6 (x9 x4)) (x12 (x8 x5) (x9 x4)) ⟶ not (x0 x6 (x12 (x8 x5) (x9 x4))) ⟶ not (x0 (x12 (x8 x5) (x8 (x9 x5))) (x12 (x8 x5) (x9 x4))) ⟶ x0 (x9 (x9 x4)) (x10 (x12 (x8 x5) (x8 (x9 x4))) (x8 (x9 (x9 x4)))) ⟶ x0 x3 (x10 (x12 (x8 x5) (x8 (x9 x5))) (x8 (x9 (x9 x4)))) ⟶ x0 (x9 x5) (x10 (x8 x5) (x9 (x9 x5))) ⟶ not (x0 (x12 x6 (x9 x4)) (x10 (x8 x5) (x9 (x9 x5)))) ⟶ not (x0 (x9 x4) (x10 (x9 x5) (x8 (x9 x5)))) ⟶ x0 x5 (x10 (x9 x5) (x8 (x9 x5))) ⟶ x0 (x12 x6 (x9 x4)) (x9 (x12 x6 (x9 x4))) ⟶ x0 (x12 x6 (x9 x4)) (x8 (x12 x6 (x9 x4))) ⟶ x0 x6 (x10 x4 (x9 x6)) ⟶ x0 x3 (x12 x7 (x9 x5)) ⟶ not (x0 (x8 x5) x7) ⟶ not (x0 (x8 x5) (x10 (x9 (x9 x5)) x7)) ⟶ not (x0 x3 (x9 (x8 x5))) ⟶ not (x0 x6 (x9 (x8 x5))) ⟶ x0 x4 (x10 x5 (x9 (x8 x5))) ⟶ x0 x3 (x10 x7 (x9 (x8 x5))) ⟶ x0 (x9 x5) (x10 (x9 (x9 x5)) (x10 x7 (x9 (x8 x5)))) ⟶ (∀ x24 . x0 x24 (x10 (x9 x4) (x9 (x9 x4))) ⟶ or (x24 = x4) (x24 = x9 x4)) ⟶ not (x1 (x12 (x8 (x8 (x9 x4))) (x9 (x8 (x9 x4)))) x5) ⟶ x1 x7 (x10 x7 (x9 (x12 (x8 x5) x5))) ⟶ not (x1 (x10 (x9 (x9 (x9 x4))) (x10 x4 (x9 (x8 x5)))) (x8 (x9 (x9 x4)))) ⟶ x1 (x12 (x8 x5) (x8 (x9 x4))) (x10 (x12 (x8 x5) (x8 (x9 x5))) (x8 (x9 (x9 x4)))) ⟶ x1 (x12 (x12 x6 (x9 x4)) (x9 x5)) x4 ⟶ x12 (x12 x6 (x9 x4)) (x9 x5) = x4 ⟶ x1 (x12 (x12 (x8 x5) (x8 (x9 x4))) (x9 x4)) (x9 x5) ⟶ x1 (x8 (x9 x4)) (x12 (x12 (x8 x5) (x9 x4)) (x9 x5)) ⟶ x1 (x12 (x12 (x8 x5) (x8 (x9 x5))) (x9 (x9 x4))) (x12 (x8 x5) (x8 (x9 x4))) ⟶ x1 x6 (x12 (x8 x5) (x9 (x9 x4))) ⟶ (∀ x24 . x0 x24 (x12 x7 (x9 x5)) ⟶ not (x24 = x6) ⟶ x0 x24 x5) ⟶ x1 (x12 (x12 x7 (x9 x5)) (x9 x6)) x5 ⟶ (∀ x24 . x0 x24 (x12 x7 x5) ⟶ not (x24 = x5) ⟶ x0 x24 (x9 x6)) ⟶ x1 (x12 x7 x5) (x12 (x12 x7 (x9 x4)) (x9 x3)) ⟶ x12 (x12 x7 (x9 x4)) (x9 x6) = x12 x6 (x9 x4) ⟶ x1 x6 (x12 x7 (x9 x6)) ⟶ x1 (x10 (x9 x5) (x8 (x9 x5))) (x10 (x10 (x9 x5) (x8 (x9 x5))) (x9 (x12 x6 (x9 x4)))) ⟶ x1 (x12 (x8 x5) (x8 (x9 x4))) x7 ⟶ (∀ x24 . x0 x24 (x10 (x8 x5) (x9 (x9 x5))) ⟶ x0 x24 (x10 (x9 x5) (x10 (x8 (x9 x5)) (x9 (x8 x5)))) ⟶ x0 x24 (x10 (x9 x5) (x8 (x9 x5)))) ⟶ x11 (x10 (x9 (x9 x4)) (x10 (x9 (x9 x5)) x7)) (x10 x7 (x9 (x12 (x8 x5) x5))) = x7 ⟶ (∀ x24 . x0 x24 (x10 (x9 (x9 x4)) (x10 (x9 (x9 x5)) x7)) ⟶ x0 x24 (x10 (x9 x5) (x10 (x8 (x9 x5)) (x9 (x8 x5)))) ⟶ not (x0 x24 (x9 (x8 x5)))) ⟶ x11 (x10 (x9 (x9 x5)) x7) (x12 (x8 x5) (x9 x4)) = x12 x6 (x9 x4) ⟶ (∀ x24 . x0 x24 (x12 x6 (x9 x4)) ⟶ not (x13 (x12 (x12 x6 (x9 x4)) (x9 x24)))) ⟶ not (x14 (x12 (x8 x5) x5)) ⟶ not (x15 (x10 (x9 x5) (x8 (x9 x5)))) ⟶ (∀ x24 . x0 x24 x7 ⟶ not (x24 = x4) ⟶ not (x14 (x12 (x12 x7 (x9 x4)) (x9 x24)))) ⟶ not (x16 (x10 (x12 (x8 x5) (x9 x5)) (x9 (x12 (x8 x5) (x8 (x9 x5)))))) ⟶ (∀ x24 . x0 x24 (x10 (x12 (x8 x5) (x8 (x9 x5))) (x8 (x9 (x9 x4)))) ⟶ not (x16 (x12 (x10 (x12 (x8 x5) (x8 (x9 x5))) (x8 (x9 (x9 x4)))) (x9 x24)))) ⟶ not (x17 (x10 (x9 (x9 x4)) x7)) ⟶ x13 (x12 x6 (x9 x4)) ⟶ x14 (x10 (x9 (x9 (x9 x4))) (x10 x4 (x9 (x8 x5)))) ⟶ x21 (x11 (x10 (x8 x5) (x9 (x9 x5))) (x10 (x9 (x9 x5)) (x10 x7 (x9 (x8 x5))))) ⟶ x22 (x10 (x9 (x8 (x9 x4))) x7) ⟶ not (x16 (x12 (x11 (x10 (x12 (x8 x5) (x8 (x9 x5))) (x10 (x8 (x9 x5)) (x9 (x8 x5)))) (x10 (x9 (x9 x5)) (x10 x7 (x9 (x8 x5))))) (x9 x3))) ⟶ not (x16 (x12 (x11 (x10 (x12 (x8 x5) (x8 (x9 x5))) (x10 (x8 (x9 x5)) (x9 (x8 x5)))) (x10 (x9 (x9 x5)) (x10 x7 (x9 (x8 x5))))) (x9 (x9 x5)))) ⟶ x1 x4 (x12 (x12 x6 (x9 x4)) (x9 x5)) (proof)
Theorem 260da.. : ∀ 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 . iff (x1 x24 x25) (∀ x26 . x0 x26 x24 ⟶ x0 x26 x25)) ⟶ (∀ x24 . iff (x16 x24) (∀ x25 : ο . (∀ x26 . and (x1 x26 x24) (and (not (x1 x24 x26)) (x15 x26)) ⟶ x25) ⟶ x25)) ⟶ (∀ x24 x25 . x0 x24 x25 ⟶ not (x0 x25 x24)) ⟶ (∀ x24 . iff (x0 x24 x6) (or (or (x24 = x3) (x24 = x4)) (x24 = x5))) ⟶ (∀ x24 x25 x26 . x0 x26 x24 ⟶ x0 x26 x25 ⟶ x0 x26 (x11 x24 x25)) ⟶ (∀ x24 x25 x26 . x1 x25 x26 ⟶ x1 (x10 x24 x25) (x10 x24 x26)) ⟶ (∀ x24 x25 . x2 (x12 x24 x25) (x11 x24 x25)) ⟶ (∀ x24 x25 . x0 x25 x24 ⟶ x1 (x9 x25) x24) ⟶ (∀ x24 x25 . x0 x24 (x8 (x9 x25)) ⟶ or (x24 = x3) (x24 = x9 x25)) ⟶ (∀ x24 x25 x26 . x1 x26 (x10 x24 x25) ⟶ ∀ x27 . x0 x27 x24 ⟶ not (x0 x27 x26) ⟶ x15 x26 ⟶ x15 (x10 (x12 x24 (x9 x27)) x25)) ⟶ (∀ x24 x25 . x16 (x10 x24 x25) ⟶ or (x13 x24) (x15 x25)) ⟶ not (x4 = x5) ⟶ (∀ x24 . x0 x3 x24 ⟶ x1 x4 x24) ⟶ (∀ x24 . x1 x24 (x9 x4) ⟶ or (x24 = x3) (x24 = x9 x4)) ⟶ (∀ x24 . x1 x24 (x9 (x9 x4)) ⟶ or (x24 = x3) (x24 = x9 (x9 x4))) ⟶ not (x0 x4 (x8 (x9 x4))) ⟶ not (x9 x4 = x5) ⟶ not (x0 (x9 x4) (x9 x5)) ⟶ x0 (x9 x4) (x12 (x8 x5) (x9 x4)) ⟶ not (x4 = x9 (x9 x4)) ⟶ not (x1 (x12 (x8 x5) (x8 (x9 x5))) x5) ⟶ not (x5 = x12 x6 (x9 x4)) ⟶ not (x0 (x9 (x9 x4)) x6) ⟶ not (x0 (x9 x5) (x12 x6 (x9 x4))) ⟶ (∀ x24 . x0 x24 (x12 (x8 x5) x5) ⟶ or (x24 = x9 x4) (x24 = x5)) ⟶ x0 x4 (x10 (x12 (x8 x5) (x8 (x9 x4))) (x8 (x9 (x9 x4)))) ⟶ x0 (x9 x4) (x10 (x12 (x8 x5) (x8 (x9 x5))) (x9 (x9 (x9 x4)))) ⟶ x0 x3 (x12 x7 (x9 x5)) ⟶ x2 (x8 (x9 x4)) (x12 x7 x5) ⟶ x0 x3 (x10 (x8 (x9 x5)) (x9 x6)) ⟶ x0 (x9 x5) (x10 (x8 (x9 x5)) (x9 x6)) ⟶ x0 x4 (x12 (x10 (x9 (x9 x5)) x7) (x12 (x8 x5) (x9 x4))) ⟶ not (x0 (x9 x4) (x10 (x9 (x9 x5)) x7)) ⟶ not (x0 (x12 x6 (x9 x4)) (x10 (x9 (x9 x4)) (x10 (x9 (x9 x5)) x7))) ⟶ not (x0 x4 (x9 (x8 x5))) ⟶ not (x0 x6 (x9 (x8 x5))) ⟶ x0 x3 (x10 x4 (x9 (x8 x5))) ⟶ x0 x5 (x10 (x9 x5) (x10 (x8 (x9 x5)) (x9 (x8 x5)))) ⟶ not (x0 (x9 x4) (x10 (x9 (x9 x5)) (x10 x7 (x9 (x8 x5))))) ⟶ (∀ x24 . x0 (x9 x4) x24 ⟶ x0 x4 x24 ⟶ x1 (x10 (x9 x4) (x9 (x9 x4))) x24) ⟶ (∀ x24 . x1 x24 (x10 (x9 x4) (x9 (x9 x4))) ⟶ x0 (x9 x4) x24 ⟶ or (or (or (x24 = x3) (x24 = x9 x4)) (x24 = x9 (x9 x4))) (x24 = x10 (x9 x4) (x9 (x9 x4)))) ⟶ (∀ x24 . x0 x24 (x10 (x12 (x8 x5) x5) (x8 (x9 (x9 x4)))) ⟶ or (or (or (x24 = x3) (x24 = x9 x4)) (x24 = x5)) (x24 = x9 (x9 x4))) ⟶ x1 x5 (x12 x7 (x9 x5)) ⟶ x1 (x10 x6 (x9 (x9 x5))) (x10 (x12 (x8 x5) (x8 (x9 x5))) (x10 (x8 (x9 x5)) (x9 (x8 x5)))) ⟶ x1 x7 (x10 (x9 (x9 x5)) x7) ⟶ not (x1 (x10 (x9 (x9 x5)) x7) x7) ⟶ x1 (x10 x6 (x9 (x9 x5))) (x10 (x9 (x9 x5)) (x10 x7 (x9 (x8 x5)))) ⟶ not (x1 (x10 (x12 (x8 x5) (x8 (x9 x5))) (x8 (x9 (x9 x4)))) (x10 (x12 (x8 x5) (x8 (x9 x4))) (x8 (x9 (x9 x4))))) ⟶ x1 (x10 (x9 (x9 x5)) x7) (x10 (x9 (x9 x4)) (x10 (x9 (x9 x5)) x7)) ⟶ not (x1 (x10 (x9 (x9 x4)) (x10 (x9 (x9 x5)) x7)) (x10 (x9 (x9 x5)) x7)) ⟶ x12 x5 (x9 x4) = x4 ⟶ x1 (x12 x6 (x9 x4)) (x12 (x12 (x8 x5) (x9 x4)) (x9 (x9 x4))) ⟶ x12 (x12 (x8 x5) (x9 x4)) (x9 (x9 x4)) = x12 x6 (x9 x4) ⟶ (∀ x24 . x0 x24 (x12 (x8 x5) (x8 (x9 x5))) ⟶ not (x24 = x5) ⟶ x0 x24 (x10 (x9 x4) (x9 (x9 x4)))) ⟶ x1 (x12 (x12 (x8 (x10 (x9 x4) (x9 (x9 x4)))) (x9 (x10 (x9 x4) (x9 (x9 x4))))) (x9 (x9 (x9 x4)))) (x8 (x9 x4)) ⟶ x1 (x12 (x10 (x12 (x8 x5) (x8 (x9 x5))) (x8 (x9 (x9 x4)))) (x9 (x9 x4))) (x10 (x12 (x8 x5) (x8 (x9 x4))) (x8 (x9 (x9 x4)))) ⟶ (∀ x24 . x0 x24 (x10 (x12 (x8 x5) (x8 (x9 x5))) (x8 (x9 (x9 x4)))) ⟶ not (x24 = x9 (x9 x4)) ⟶ x0 x24 (x8 x5)) ⟶ x12 (x10 (x12 (x8 x5) (x8 (x9 x5))) (x8 (x9 (x9 x4)))) (x9 (x9 (x9 x4))) = x8 x5 ⟶ x1 (x12 (x12 x7 (x8 (x9 x5))) (x9 x5)) (x10 (x9 x4) (x9 x6)) ⟶ x12 (x12 x7 (x8 (x9 x5))) (x9 x6) = x12 (x8 x5) (x8 (x9 x4)) ⟶ x1 x5 (x10 x6 (x9 (x12 x6 (x9 x4)))) ⟶ x1 (x10 (x10 (x9 x4) (x9 (x9 x4))) (x8 (x9 x5))) (x10 (x10 (x9 x4) (x9 (x9 x4))) (x10 (x8 (x9 x5)) (x9 x6))) ⟶ x1 (x11 (x10 (x9 (x9 x5)) x7) (x12 (x8 x5) (x9 x4))) (x12 x6 (x9 x4)) ⟶ not (x13 (x9 (x8 x5))) ⟶ not (x15 (x12 (x8 x5) (x9 x4))) ⟶ (∀ x24 . x0 x24 (x10 (x12 (x8 x5) (x8 (x9 x4))) (x10 (x9 (x9 x5)) (x9 (x8 x5)))) ⟶ not (x15 (x12 (x10 (x12 (x8 x5) (x8 (x9 x4))) (x10 (x9 (x9 x5)) (x9 (x8 x5)))) (x9 x24)))) ⟶ x13 (x10 (x9 x4) (x9 (x9 x4))) ⟶ x13 (x8 (x9 (x9 x4))) ⟶ x19 (x12 x7 x5) ⟶ x19 (x11 (x10 x7 (x9 (x8 x5))) (x12 (x8 x5) (x8 (x9 x5)))) ⟶ x21 (x10 (x10 (x9 x5) (x9 (x9 x5))) (x10 x4 (x9 x6))) ⟶ x21 (x10 (x9 (x9 (x9 x4))) (x10 x5 (x9 (x8 x5)))) ⟶ x22 (x10 x7 (x9 (x12 (x8 x5) x5))) ⟶ x21 (x11 (x10 (x10 (x9 x4) (x9 (x9 x4))) (x10 (x8 (x9 x5)) (x9 x6))) (x10 (x9 (x9 x5)) x7)) ⟶ (∀ x24 . x0 x24 (x12 (x8 x5) (x8 (x9 x5))) ⟶ x0 x24 (x10 (x9 (x9 x5)) (x10 x7 (x9 (x8 x5)))) ⟶ not (x0 x24 (x9 x4)) ⟶ x0 x24 (x10 (x9 x5) (x10 (x8 (x9 x5)) (x9 (x8 x5))))) ⟶ not (x17 (x11 (x10 (x12 (x8 x5) (x8 (x9 x5))) (x10 (x8 (x9 x5)) (x9 (x8 x5)))) (x10 (x9 (x9 x5)) (x10 x7 (x9 (x8 x5)))))) ⟶ x22 (x11 (x10 (x12 (x8 x5) (x8 (x9 x5))) (x10 (x8 (x9 x5)) (x9 (x8 x5)))) (x10 (x9 (x9 x5)) (x10 x7 (x9 (x8 x5))))) ⟶ not (x0 x4 x4) (proof)
Theorem 46a3e.. : ∀ x0 x1 x2 : ι → ι → ο . ∀ x3 x4 x5 x6 x7 . ∀ x8 x9 : ι → ι . ∀ x10 x11 x12 : ι → ι → ι . ∀ x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 : ι → ο . x0 x6 x7 ⟶ (∀ x24 x25 x26 . x0 x26 x24 ⟶ not (x0 x26 x25) ⟶ x0 x26 (x12 x24 x25)) ⟶ (∀ x24 x25 . not (x0 x25 (x9 x24)) ⟶ not (x25 = x24)) ⟶ (∀ x24 . not (x13 (x9 x24))) ⟶ (∀ x24 x25 x26 . x1 x26 (x10 x24 x25) ⟶ ∀ x27 . not (x0 x27 x26) ⟶ x1 x26 (x10 (x12 x24 (x9 x27)) x25)) ⟶ (∀ x24 x25 x26 . x1 x26 (x10 x24 x25) ⟶ ∀ x27 . x0 x27 x24 ⟶ not (x0 x27 x26) ⟶ x15 x26 ⟶ x15 (x10 (x12 x24 (x9 x27)) x25)) ⟶ not (x0 x3 (x9 x5)) ⟶ x1 x4 (x12 x6 (x9 x4)) ⟶ not (x0 x5 (x8 (x9 x4))) ⟶ not (x1 x5 (x9 x5)) ⟶ not (x3 = x10 (x9 x4) (x9 (x9 x4))) ⟶ not (x1 (x12 (x8 x5) x5) x5) ⟶ (∀ x24 . x1 x24 (x8 (x9 x4)) ⟶ or (or (or (x24 = x3) (x24 = x4)) (x24 = x9 (x9 x4))) (x24 = x8 (x9 x4))) ⟶ not (x0 (x8 x5) x6) ⟶ not (x9 x5 = x6) ⟶ x0 (x9 (x9 x4)) (x12 (x8 (x8 (x9 x4))) (x9 (x8 (x9 x4)))) ⟶ not (x0 (x9 x4) (x9 (x10 (x9 x4) (x9 (x9 x4))))) ⟶ x0 (x8 (x9 x4)) (x10 x6 (x9 (x8 (x9 x4)))) ⟶ not (x0 (x12 x6 (x9 x4)) (x9 (x9 x5))) ⟶ not (x0 x6 (x8 (x9 x5))) ⟶ x0 x3 (x10 (x9 x4) (x8 (x9 x5))) ⟶ not (x0 (x9 x4) x7) ⟶ x0 (x9 x5) (x10 (x8 x5) (x9 (x9 x5))) ⟶ not (x0 x5 (x10 x4 (x9 x6))) ⟶ not (x0 (x9 x4) (x10 (x9 (x9 x5)) x7)) ⟶ x0 x5 (x10 (x9 (x9 x5)) x7) ⟶ not (x0 (x9 x4) (x9 (x8 x5))) ⟶ x0 (x8 x5) (x9 (x8 x5)) ⟶ x0 x4 (x10 (x9 x4) (x10 (x8 (x9 x5)) (x9 (x8 x5)))) ⟶ x2 x5 (x10 (x9 x6) (x9 (x8 x5))) ⟶ x0 x5 (x10 x7 (x9 (x8 x5))) ⟶ x0 x6 (x10 (x9 (x9 x4)) (x10 x7 (x9 (x8 x5)))) ⟶ (∀ x24 . x0 x24 (x12 x7 x5) ⟶ or (x24 = x5) (x24 = x6)) ⟶ (∀ x24 . x0 x24 x7 ⟶ not (x24 = x4) ⟶ or (or (x24 = x3) (x24 = x5)) (x24 = x6)) ⟶ x1 x5 (x10 (x9 x4) (x8 (x9 x5))) ⟶ not (x1 (x10 x7 (x9 (x8 x5))) x7) ⟶ not (x1 (x10 (x12 (x8 x5) (x8 (x9 x5))) (x8 (x9 (x9 x4)))) (x10 (x12 (x8 x5) (x8 (x9 x4))) (x8 (x9 (x9 x4))))) ⟶ x1 x4 (x12 x5 (x9 x4)) ⟶ x1 (x12 (x12 (x8 x5) x5) (x9 x5)) (x9 (x9 x4)) ⟶ (∀ x24 . x0 x24 (x12 (x8 x5) (x9 x4)) ⟶ not (x24 = x3) ⟶ x0 x24 (x12 (x8 x5) x5)) ⟶ x12 (x12 (x8 x5) (x9 x4)) (x9 x5) = x8 (x9 x4) ⟶ x1 (x12 (x12 (x8 (x10 (x9 x4) (x9 (x9 x4)))) (x9 (x10 (x9 x4) (x9 (x9 x4))))) (x9 x3)) (x10 (x9 (x9 x4)) (x9 (x9 (x9 x4)))) ⟶ x12 (x12 (x8 (x10 (x9 x4) (x9 (x9 x4)))) (x9 (x10 (x9 x4) (x9 (x9 x4))))) (x9 (x9 x4)) = x8 (x9 (x9 x4)) ⟶ x12 (x12 (x8 (x10 (x9 x4) (x9 (x9 x4)))) (x9 (x10 (x9 x4) (x9 (x9 x4))))) (x9 (x9 (x9 x4))) = x8 (x9 x4) ⟶ (∀ x24 . x0 x24 (x12 x7 (x8 (x9 x5))) ⟶ not (x24 = x4) ⟶ x0 x24 (x12 x7 x5)) ⟶ x1 (x10 (x9 x4) (x9 x6)) (x12 (x12 x7 (x8 (x9 x5))) (x9 x5)) ⟶ x1 (x10 (x9 x5) (x8 (x9 x5))) (x10 (x9 x5) (x10 (x8 (x9 x5)) (x9 (x8 x5)))) ⟶ x1 (x10 (x9 x4) (x8 (x9 x5))) (x10 (x10 (x9 x4) (x9 (x9 x4))) (x10 (x8 (x9 x5)) (x9 x6))) ⟶ x1 (x8 (x9 x5)) (x10 (x12 (x8 x5) (x8 (x9 x5))) (x10 (x8 (x9 x5)) (x9 (x8 x5)))) ⟶ (∀ x24 . x0 x24 x6 ⟶ not (x14 (x12 x6 (x9 x24)))) ⟶ (∀ x24 . x0 x24 x7 ⟶ not (x24 = x5) ⟶ not (x14 (x12 (x12 x7 (x9 x5)) (x9 x24)))) ⟶ not (x16 (x10 (x12 (x8 x5) (x9 x5)) (x9 (x12 (x8 x5) (x8 (x9 x5)))))) ⟶ (∀ x24 . x16 (x12 (x10 (x12 (x8 x5) (x8 (x9 x5))) (x8 (x9 (x9 x4)))) (x9 x24)) ⟶ not (x24 = x9 (x9 x4))) ⟶ not (x17 (x10 (x9 (x9 (x9 x4))) x7)) ⟶ x14 (x10 x5 (x9 (x8 x5))) ⟶ x15 (x10 x6 (x9 (x8 (x9 x4)))) ⟶ x16 (x10 x7 (x9 (x8 x5))) ⟶ x19 (x8 (x9 x4)) ⟶ x20 (x10 (x9 x5) (x8 (x9 x5))) ⟶ x20 (x12 (x10 x6 (x9 (x9 x5))) (x9 x5)) ⟶ x21 (x10 x5 (x10 (x9 x6) (x9 (x8 x5)))) ⟶ x21 (x12 (x10 (x9 (x9 x5)) x7) (x9 x6)) ⟶ x22 (x10 x7 (x9 (x12 (x8 x5) x5))) ⟶ x23 (x10 (x9 (x9 x4)) (x10 x7 (x9 (x8 x5)))) ⟶ x20 (x12 (x10 (x9 (x9 x5)) x7) (x12 (x8 x5) (x9 x4))) ⟶ x1 (x12 (x11 (x10 (x10 (x9 x4) (x9 (x9 x4))) (x10 (x8 (x9 x5)) (x9 x6))) (x10 (x9 (x9 x5)) x7)) (x9 (x9 x5))) (x12 x7 (x9 x5)) ⟶ not (x15 (x12 (x11 (x10 (x10 (x9 x4) (x9 (x9 x4))) (x10 (x8 (x9 x5)) (x9 x6))) (x10 (x9 (x9 x5)) x7)) (x9 x3))) ⟶ not (x17 (x11 (x10 (x12 (x8 x5) (x8 (x9 x5))) (x10 (x8 (x9 x5)) (x9 (x8 x5)))) (x10 (x9 (x9 x5)) (x10 x7 (x9 (x8 x5)))))) ⟶ x0 (x12 (x8 x5) (x8 (x9 x5))) (x9 (x12 (x8 x5) (x8 (x9 x5)))) (proof)