| ∀ 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 . and (x1 x25 x24) (and (not (x1 x24 x25)) (x14 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) |
|