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