| ∀ x0 : ι → ι → ο . ∀ x1 : ι → ι . ∀ x2 x3 : ι → ι → ο . ∀ x4 : ι → ο . ∀ x5 : ι → ι . ∀ x6 : ι → ι → ι . ∀ x7 : ι → ι → ο . ∀ x8 : ι → ι → ι → ι . ∀ x9 x10 : ι → ι . ∀ x11 : ι → ι → ο . ∀ x12 : ι → ι . ∀ x13 . ∀ x14 : ι → ι . ∀ x15 : ι → ο . ∀ x16 x17 x18 . ∀ x19 : ι → ι → ι . ∀ x20 . ∀ x21 : ι → ι . ∀ x22 . ∀ x23 x24 : ι → ι . ∀ x25 x26 x27 : ι → ι → ι . ∀ x28 : ι → ο . ∀ x29 . ∀ x30 : ι → ο . (∀ x31 x32 . x30 x32 ⟶ (x32 = x31 ⟶ False) ⟶ x30 x31 ⟶ False) ⟶ (∀ x31 x32 . x0 x31 x32 ⟶ x30 x32 ⟶ False) ⟶ (∀ x31 . x30 x31 ⟶ (x31 = x29 ⟶ False) ⟶ False) ⟶ (∀ x31 x32 x33 . x0 x31 x32 ⟶ x2 x32 (x1 x33) ⟶ x30 x33 ⟶ False) ⟶ (∀ x31 x32 x33 . x0 x32 x33 ⟶ x2 x33 (x1 x31) ⟶ (x2 x32 x31 ⟶ False) ⟶ False) ⟶ (∀ x31 x32 . x3 x32 x31 ⟶ (x2 x32 (x1 x31) ⟶ False) ⟶ False) ⟶ (∀ x31 x32 . x2 x32 (x1 x31) ⟶ (x3 x32 x31 ⟶ False) ⟶ False) ⟶ (∀ x31 x32 . x2 x31 x32 ⟶ (x30 x32 ⟶ False) ⟶ (x0 x31 x32 ⟶ False) ⟶ False) ⟶ (∀ x31 x32 . x0 x32 x31 ⟶ (x2 x32 x31 ⟶ False) ⟶ False) ⟶ (∀ x31 x32 . x4 x32 ⟶ x2 x31 (x1 (x5 x32)) ⟶ (x3 x31 (x6 x32 x31) ⟶ False) ⟶ False) ⟶ (∀ x31 x32 . x28 x32 ⟶ x4 x32 ⟶ x2 x31 (x1 (x5 x32)) ⟶ (x6 x32 x31 = x27 (x5 x32) (x26 x31 x32) ⟶ False) ⟶ False) ⟶ (∀ x31 x32 x33 . x28 x33 ⟶ x4 x33 ⟶ x2 x32 (x1 (x5 x33)) ⟶ x2 x31 (x1 (x5 x33)) ⟶ x7 x31 x33 ⟶ x3 x32 x31 ⟶ (x0 x31 (x26 x32 x33) ⟶ False) ⟶ False) ⟶ (∀ x31 x32 x33 . x28 x33 ⟶ x4 x33 ⟶ x2 x32 (x1 (x5 x33)) ⟶ x2 x31 (x1 (x5 x33)) ⟶ x0 x31 (x26 x32 x33) ⟶ (x3 x32 x31 ⟶ False) ⟶ False) ⟶ (∀ x31 x32 x33 . x28 x33 ⟶ x4 x33 ⟶ x2 x32 (x1 (x5 x33)) ⟶ x2 x31 (x1 (x5 x33)) ⟶ x0 x31 (x26 x32 x33) ⟶ (x7 x31 x33 ⟶ False) ⟶ False) ⟶ (∀ x31 x32 . x28 x32 ⟶ x4 x32 ⟶ x2 x31 (x1 (x5 x32)) ⟶ (x2 (x26 x31 x32) (x1 (x1 (x5 x32))) ⟶ False) ⟶ False) ⟶ (∀ x31 x32 x33 . x4 x33 ⟶ x2 x31 (x1 (x5 x33)) ⟶ x0 x32 (x5 x33) ⟶ x0 x32 (x8 x32 x31 x33) ⟶ (x0 x32 (x6 x33 x31) ⟶ False) ⟶ False) ⟶ (∀ x31 x32 x33 . x4 x33 ⟶ x2 x31 (x1 (x5 x33)) ⟶ x0 x32 (x5 x33) ⟶ (x3 x31 (x8 x32 x31 x33) ⟶ False) ⟶ (x0 x32 (x6 x33 x31) ⟶ False) ⟶ False) ⟶ (∀ x31 x32 x33 . x4 x33 ⟶ x2 x31 (x1 (x5 x33)) ⟶ x0 x32 (x5 x33) ⟶ (x7 (x8 x32 x31 x33) x33 ⟶ False) ⟶ (x0 x32 (x6 x33 x31) ⟶ False) ⟶ False) ⟶ (∀ x31 x32 x33 . x4 x33 ⟶ x2 x31 (x1 (x5 x33)) ⟶ x0 x32 (x5 x33) ⟶ (x2 (x8 x32 x31 x33) (x1 (x5 x33)) ⟶ False) ⟶ (x0 x32 (x6 x33 x31) ⟶ False) ⟶ False) ⟶ (∀ x31 x32 x33 x34 . x4 x34 ⟶ x2 x31 (x1 (x5 x34)) ⟶ x0 x33 (x5 x34) ⟶ x0 x33 (x6 x34 x31) ⟶ x2 x32 (x1 (x5 x34)) ⟶ x7 x32 x34 ⟶ x3 x31 x32 ⟶ (x0 x33 x32 ⟶ False) ⟶ False) ⟶ (∀ x31 x32 . x28 x32 ⟶ x4 x32 ⟶ x2 x31 (x1 (x1 (x5 x32))) ⟶ x7 (x25 x31 x32) x32 ⟶ (x7 (x27 (x5 x32) x31) x32 ⟶ False) ⟶ False) ⟶ (∀ x31 x32 . x28 x32 ⟶ x4 x32 ⟶ x2 x31 (x1 (x1 (x5 x32))) ⟶ (x0 (x25 x31 x32) x31 ⟶ False) ⟶ (x7 (x27 (x5 x32) x31) x32 ⟶ False) ⟶ False) ⟶ (∀ x31 x32 . x28 x32 ⟶ x4 x32 ⟶ x2 x31 (x1 (x1 (x5 x32))) ⟶ (x2 (x25 x31 x32) (x1 (x5 x32)) ⟶ False) ⟶ (x7 (x27 (x5 x32) x31) x32 ⟶ False) ⟶ False) ⟶ (∀ x31 . (x3 x31 x31 ⟶ False) ⟶ False) ⟶ (∀ x31 x32 . x2 x31 (x1 (x1 x32)) ⟶ (x27 x32 x31 = x24 x31 ⟶ False) ⟶ False) ⟶ (∀ x31 . x28 x31 ⟶ x4 x31 ⟶ (x7 (x9 x31) x31 ⟶ False) ⟶ False) ⟶ (∀ x31 . x28 x31 ⟶ x4 x31 ⟶ (x2 (x9 x31) (x1 (x5 x31)) ⟶ False) ⟶ False) ⟶ (∀ x31 . (x30 x31 ⟶ False) ⟶ (x11 (x10 x31) x31 ⟶ False) ⟶ False) ⟶ (∀ x31 . (x30 x31 ⟶ False) ⟶ (x2 (x10 x31) (x1 x31) ⟶ False) ⟶ False) ⟶ (∀ x31 . x11 (x12 x31) x31 ⟶ False) ⟶ (∀ x31 . (x2 (x12 x31) (x1 x31) ⟶ False) ⟶ False) ⟶ (x30 x13 ⟶ False) ⟶ (∀ x31 . (x30 (x23 x31) ⟶ False) ⟶ False) ⟶ (∀ x31 . (x2 (x23 x31) (x1 x31) ⟶ False) ⟶ False) ⟶ ((x30 x22 ⟶ False) ⟶ False) ⟶ (∀ x31 . (x30 x31 ⟶ False) ⟶ x30 (x14 x31) ⟶ False) ⟶ (∀ x31 . (x30 x31 ⟶ False) ⟶ (x2 (x14 x31) (x1 x31) ⟶ False) ⟶ False) ⟶ (∀ x31 x32 . x4 x32 ⟶ x2 x31 (x1 (x5 x32)) ⟶ (x6 x32 (x6 x32 x31) = x6 x32 x31 ⟶ False) ⟶ False) ⟶ ((x30 x29 ⟶ False) ⟶ False) ⟶ (∀ x31 . x30 (x1 x31) ⟶ False) ⟶ (∀ x31 . (x2 (x21 x31) x31 ⟶ False) ⟶ False) ⟶ ((x15 x16 ⟶ False) ⟶ False) ⟶ ((x4 x20 ⟶ False) ⟶ False) ⟶ (∀ x31 . x4 x31 ⟶ (x15 x31 ⟶ False) ⟶ False) ⟶ (∀ x31 x32 . x2 x32 (x1 (x1 x31)) ⟶ (x2 (x27 x31 x32) (x1 x31) ⟶ False) ⟶ False) ⟶ (∀ x31 x32 . x4 x32 ⟶ x2 x31 (x1 (x5 x32)) ⟶ (x2 (x6 x32 x31) (x1 (x5 x32)) ⟶ False) ⟶ False) ⟶ (∀ x31 x32 . x0 (x19 x31 x32) x31 ⟶ (x3 x32 x31 ⟶ False) ⟶ False) ⟶ (∀ x31 x32 . (x0 (x19 x31 x32) x32 ⟶ False) ⟶ (x3 x32 x31 ⟶ False) ⟶ False) ⟶ (∀ x31 x32 x33 . x3 x32 x33 ⟶ x0 x31 x32 ⟶ (x0 x31 x33 ⟶ False) ⟶ False) ⟶ (∀ x31 x32 . x3 x32 x31 ⟶ x3 x31 x32 ⟶ (x32 = x31 ⟶ False) ⟶ False) ⟶ (∀ x31 x32 . x31 = x32 ⟶ (x3 x32 x31 ⟶ False) ⟶ False) ⟶ (∀ x31 x32 . x32 = x31 ⟶ (x3 x32 x31 ⟶ False) ⟶ False) ⟶ (∀ x31 x32 . x30 x32 ⟶ x2 x31 (x1 x32) ⟶ x11 x31 x32 ⟶ False) ⟶ (∀ x31 x32 . (x30 x32 ⟶ False) ⟶ x2 x31 (x1 x32) ⟶ x30 x31 ⟶ (x11 x31 x32 ⟶ False) ⟶ False) ⟶ (∀ x31 x32 . (x30 x32 ⟶ False) ⟶ x2 x31 (x1 x32) ⟶ (x11 x31 x32 ⟶ False) ⟶ x30 x31 ⟶ False) ⟶ (∀ x31 x32 . x30 x32 ⟶ x2 x31 (x1 x32) ⟶ (x30 x31 ⟶ False) ⟶ False) ⟶ (∀ x31 x32 . x0 x31 x32 ⟶ x0 x32 x31 ⟶ False) ⟶ (x6 x17 x18 = x18 ⟶ x7 x18 x17 ⟶ False) ⟶ (x6 x17 x18 = x18 ⟶ (x6 x17 x18 = x18 ⟶ False) ⟶ False) ⟶ (x6 x17 x18 = x18 ⟶ (x28 x17 ⟶ False) ⟶ False) ⟶ ((x7 x18 x17 ⟶ False) ⟶ x7 x18 x17 ⟶ False) ⟶ ((x7 x18 x17 ⟶ False) ⟶ (x6 x17 x18 = x18 ⟶ False) ⟶ False) ⟶ ((x7 x18 x17 ⟶ False) ⟶ (x28 x17 ⟶ False) ⟶ False) ⟶ ((x2 x18 (x1 (x5 x17)) ⟶ False) ⟶ False) ⟶ ((x4 x17 ⟶ False) ⟶ False) ⟶ False |
|