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