| ∀ x0 . ∀ x1 : ι → ι → ι . (∀ x2 . In x2 x0 ⟶ ∀ x3 . In x3 x0 ⟶ In (x1 x2 x3) x0) ⟶ ∀ x2 : ι → ι → ι → ι . (∀ x3 . In x3 x0 ⟶ ∀ x4 . In x4 x0 ⟶ ∀ x5 . In x5 x0 ⟶ In (x2 x3 x4 x5) x0) ⟶ ∀ x3 . In x3 x0 ⟶ ∀ x4 . In x4 x0 ⟶ ∀ x5 . In x5 x0 ⟶ ∀ x6 : ι → ι → ι . (∀ x7 . In x7 x0 ⟶ ∀ x8 . In x8 x0 ⟶ In (x6 x7 x8) x0) ⟶ ∀ x7 : ι → ι → ι . (∀ x8 . In x8 x0 ⟶ ∀ x9 . In x9 x0 ⟶ In (x7 x8 x9) x0) ⟶ ∀ x8 : ι → ι → ι . (∀ x9 . In x9 x0 ⟶ ∀ x10 . In x10 x0 ⟶ In (x8 x9 x10) x0) ⟶ (∀ x9 . In x9 x0 ⟶ ∀ x10 . In x10 x0 ⟶ (x8 x9 (x7 x9 x10) = x10 ⟶ False) ⟶ False) ⟶ (∀ x9 . In x9 x0 ⟶ ∀ x10 . In x10 x0 ⟶ (x1 x9 x10 = x7 x9 (x8 x10 x9) ⟶ False) ⟶ False) ⟶ (∀ x9 . In x9 x0 ⟶ (x6 x5 x9 = x9 ⟶ False) ⟶ False) ⟶ (∀ x9 . In x9 x0 ⟶ ∀ x10 . In x10 x0 ⟶ (x2 x5 x9 x10 = x10 ⟶ False) ⟶ False) ⟶ (∀ x9 . In x9 x0 ⟶ ∀ x10 . In x10 x0 ⟶ (x2 x9 x5 x10 = x10 ⟶ False) ⟶ False) ⟶ (∀ x9 . In x9 x0 ⟶ ∀ x10 . In x10 x0 ⟶ ∀ x11 . In x11 x0 ⟶ ∀ x12 . In x12 x0 ⟶ (x2 x9 x11 (x6 x10 (x1 x9 (x2 x11 x10 (x2 x9 x11 (x6 x10 (x1 x9 (x2 x11 x10 (x2 x9 x11 (x6 x10 (x1 x9 (x2 x11 x10 (x2 x9 x11 (x6 x10 (x1 x9 (x2 x11 x10 (x2 x9 x11 (x6 x10 (x1 x9 (x2 x11 x10 x12))))))))))))))))))) = x12 ⟶ False) ⟶ False) ⟶ (∀ x9 . In x9 x0 ⟶ ∀ x10 . In x10 x0 ⟶ ∀ x11 . In x11 x0 ⟶ ∀ x12 . In x12 x0 ⟶ (x2 x9 x11 (x1 x10 (x6 x9 (x2 x11 x10 (x2 x9 x11 (x1 x10 (x6 x9 (x2 x11 x10 x12))))))) = x12 ⟶ False) ⟶ False) ⟶ (x8 x3 x4 = x8 x4 x3 ⟶ False) ⟶ False |
|