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