Let x0 of type ι → ι → ο be given.
Let x1 of type ι → ι → ο be given.
Let x2 of type ι → ο be given.
Let x3 of type ι → ι be given.
Let x4 of type ι be given.
Let x5 of type ι → ι be given.
Let x6 of type ι → ι be given.
Let x7 of type ι → ι → ο be given.
Let x8 of type ι → ι → ο be given.
Let x9 of type ι → ο be given.
Let x10 of type ι → ι be given.
Let x11 of type ι → ι be given.
Let x12 of type ι → ι be given.
Let x13 of type ι → ι be given.
Let x14 of type ι be given.
Let x15 of type ι be given.
Let x16 of type ι be given.
Let x17 of type ι be given.
Let x18 of type ι be given.
Let x19 of type ι → ο be given.
Let x20 of type ι → ο be given.
Let x21 of type ι be given.
Let x22 of type ι be given.
Let x23 of type ι → ι → ο be given.
Let x24 of type ι → ι be given.
Let x25 of type ι → ι be given.
Let x26 of type ι → ι be given.
Let x27 of type ι → ι be given.
Let x28 of type ι → ι → ο be given.
Let x29 of type ι be given.
Let x30 of type ι → ι → ι be given.
Let x31 of type ι → ο be given.
Let x32 of type ι → ι → ο be given.
Let x33 of type ι → ο be given.
Let x34 of type ι → ι → ι be given.
Let x35 of type ι → ι → ι be given.
Let x36 of type ι → ι → ι → ι be given.
Let x37 of type ι → ι be given.
Let x38 of type ι → ι be given.
Let x39 of type ι → ι → ο be given.
Let x40 of type ι → ο be given.
Assume H5:
∀ x41 x42 x43 . x40 x43 ⟶ x33 x43 ⟶ x39 x42 (x38 (x37 x43)) ⟶ x39 x41 (x38 (x37 x43)) ⟶ (x36 (x37 x43) (x34 x43 (x35 x43 (x36 (x37 x43) x42 (x36 (x37 x43) (x34 x43 (x35 x43 x41)) x41)))) (x36 (x37 x43) x42 (x36 (x37 x43) (x34 x43 (x35 x43 x41)) x41)) = x36 (x37 x43) (x34 x43 (x35 x43 (x36 (x37 x43) x42 x41))) (x36 (x37 x43) x42 x41) ⟶ False) ⟶ False.
Assume H6:
∀ x41 x42 . x0 x42 x41 ⟶ (x39 x42 (x38 x41) ⟶ False) ⟶ False.
Assume H7:
∀ x41 x42 . x39 x42 (x38 x41) ⟶ (x0 x42 x41 ⟶ False) ⟶ False.
Assume H8:
∀ x41 x42 . x40 x42 ⟶ x33 x42 ⟶ x39 x41 (x38 (x37 x42)) ⟶ (x1 (x34 x42 x41) x42 ⟶ False) ⟶ False.
Assume H9:
∀ x41 x42 . x40 x42 ⟶ x33 x42 ⟶ x39 x41 (x38 (x37 x42)) ⟶ (x32 (x35 x42 x41) x42 ⟶ False) ⟶ False.
Assume H10:
∀ x41 . x2 (x38 x41) ⟶ False.
Assume H11:
∀ x41 . x33 x41 ⟶ (x31 x41 ⟶ False) ⟶ False.
Assume H12:
∀ x41 x42 x43 . x39 x42 (x38 x43) ⟶ x39 x41 (x38 x43) ⟶ (x39 (x36 x43 x42 x41) (x38 x43) ⟶ False) ⟶ False.
Assume H13:
∀ x41 x42 . x33 x42 ⟶ x39 x41 (x38 (x37 x42)) ⟶ (x39 (x35 x42 x41) (x38 (x37 x42)) ⟶ False) ⟶ False.
Assume H14:
∀ x41 x42 . x33 x42 ⟶ x39 x41 (x38 (x37 x42)) ⟶ (x39 (x34 x42 x41) (x38 (x37 x42)) ⟶ False) ⟶ False.
Assume H15:
∀ x41 x42 x43 . x39 x42 (x38 x43) ⟶ x39 x41 (x38 x43) ⟶ (x36 x43 x42 x41 = x30 x42 x41 ⟶ False) ⟶ False.
Assume H16:
∀ x41 . (x39 (x3 x41) x41 ⟶ False) ⟶ False.
Assume H18:
∀ x41 x42 x43 . ... ⟶ ... ⟶ (x36 x43 x42 x42 = x42 ⟶ False) ⟶ False.