| (∀ x0 : ι → ι → ο . ∀ x1 : ι → ι → ι . ∀ x2 x3 : ι → ο . ∀ x4 : ι → ι . ∀ x5 x6 x7 . and (x6 = x1 (x1 x5 (x1 x7 (x1 (x1 (x1 (x1 x6 (x1 (x1 x5 (x1 x5 (x1 (x1 x5 (x1 (x4 x5) (x1 (x1 x7 (x1 x6 (x1 x6 x6))) x5))) (x1 (x4 (x1 (x1 (x4 x7) x5) (x1 x5 x5))) (x1 x6 (x1 x6 (x1 (x1 (x1 x5 (x1 (x1 x5 (x1 (x4 x6) x7)) (x4 (x1 x7 x5)))) x6) (x4 (x1 (x1 x7 (x1 x5 (x1 (x4 (x1 x5 x7)) x5))) (x1 (x1 (x1 x6 (x1 (x4 x5) x6)) x6) (x4 (x4 (x1 (x1 (x1 (x1 x5 (x1 (x1 x6 (x1 (x1 x7 x5) x7)) x6)) x7) (x1 x7 (x1 x5 x5))) x6))))))))))))) (x1 (x1 (x1 (x1 (x1 x6 (x1 x5 x5)) (x4 (x4 (x1 x7 (x4 (x4 (x1 x7 x5))))))) x5) x6) (x1 x6 x7)))) x5) x5) (x4 x6)))) (x1 (x1 (x4 (x1 (x4 (x1 (x1 (x1 (x1 x7 (x1 (x4 (x4 (x1 (x1 x5 x6) x7))) (x4 (x1 x5 x5)))) x5) (x4 x5)) (x1 (x1 (x1 (x1 (x1 x5 x7) (x4 (x4 (x4 x7)))) x7) x6) x5))) (x1 (x1 (x1 x6 x5) (x4 x6)) x6))) x7) x6)) (∃ x8 . x3 (x4 x5))) ⟶ False |
|