| ∀ 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) |
|