| ∀ 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 : ι → ι → ι . (∀ x4 . In x4 x0 ⟶ ∀ x5 . In x5 x0 ⟶ In (x3 x4 x5) x0) ⟶ ∀ x4 . In x4 x0 ⟶ ∀ x5 . In x5 x0 ⟶ ∀ x6 : ι → ι → ι → ι . (∀ x7 . In x7 x0 ⟶ ∀ x8 . In x8 x0 ⟶ ∀ x9 . In x9 x0 ⟶ In (x6 x7 x8 x9) x0) ⟶ ∀ x7 : ι → ι → ι . (∀ x8 . In x8 x0 ⟶ ∀ x9 . In x9 x0 ⟶ In (x7 x8 x9) x0) ⟶ ∀ x8 . In x8 x0 ⟶ ∀ x9 : ι → ι → ι . (∀ x10 . In x10 x0 ⟶ ∀ x11 . In x11 x0 ⟶ In (x9 x10 x11) x0) ⟶ (∀ x10 . In x10 x0 ⟶ (x9 x8 x10 = x10 ⟶ False) ⟶ False) ⟶ (∀ x10 . In x10 x0 ⟶ (x9 x10 x8 = x10 ⟶ False) ⟶ False) ⟶ (∀ x10 . In x10 x0 ⟶ ∀ x11 . In x11 x0 ⟶ (x7 (x9 x11 x10) x10 = x11 ⟶ False) ⟶ False) ⟶ (∀ x10 . In x10 x0 ⟶ ∀ x11 . In x11 x0 ⟶ (x1 x10 x11 = x9 (x7 x8 (x7 x8 x10)) (x7 x11 x10) ⟶ False) ⟶ False) ⟶ (∀ x10 . In x10 x0 ⟶ (x7 x10 x8 = x10 ⟶ False) ⟶ False) ⟶ (∀ x10 . In x10 x0 ⟶ (x7 x10 x10 = x8 ⟶ False) ⟶ False) ⟶ (∀ x10 . In x10 x0 ⟶ ∀ x11 . In x11 x0 ⟶ (x6 x10 x8 x11 = x11 ⟶ False) ⟶ False) ⟶ (∀ x10 . In x10 x0 ⟶ ∀ x11 . In x11 x0 ⟶ (x2 x8 x10 x11 = x11 ⟶ False) ⟶ False) ⟶ (∀ x10 . In x10 x0 ⟶ ∀ x11 . In x11 x0 ⟶ (x2 x10 x8 x11 = x11 ⟶ False) ⟶ False) ⟶ (∀ x10 . In x10 x0 ⟶ ∀ x11 . In x11 x0 ⟶ ∀ x12 . In x12 x0 ⟶ ∀ x13 . In x13 x0 ⟶ (x6 x10 x12 (x1 x11 (x3 x10 (x2 x12 x11 (x6 x10 x12 (x1 x11 (x3 x10 (x2 x12 x11 (x6 x10 x12 (x1 x11 (x3 x10 (x2 x12 x11 (x6 x10 x12 (x1 x11 (x3 x10 (x2 x12 x11 (x6 x10 x12 (x1 x11 (x3 x10 (x2 x12 x11 x13))))))))))))))))))) = x13 ⟶ False) ⟶ False) ⟶ (∀ x10 . In x10 x0 ⟶ ∀ x11 . In x11 x0 ⟶ ∀ x12 . In x12 x0 ⟶ ∀ x13 . In x13 x0 ⟶ (x6 x10 x12 (x1 x11 (x3 x10 (x2 x12 x11 (x6 x10 x12 (x1 x11 (x3 x10 (x2 x12 x11 (x6 x10 x12 (x1 x11 (x3 x10 (x2 x12 x11 (x6 x10 x12 (x1 x11 (x3 x10 (x2 x12 x11 x13))))))))))))))) = x13 ⟶ False) ⟶ False) ⟶ (x9 x4 x5 = x9 x5 x4 ⟶ False) ⟶ False |
|