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