| ∀ 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 x33 . x31 x33 ⟶ (x33 = x32 ⟶ False) ⟶ x31 x32 ⟶ False) ⟶ (∀ x32 x33 . x0 x32 x33 ⟶ x31 x33 ⟶ False) ⟶ (∀ x32 . x31 x32 ⟶ (x32 = x30 ⟶ False) ⟶ False) ⟶ (∀ x32 x33 . x1 x32 x33 ⟶ (x31 x33 ⟶ False) ⟶ (x0 x32 x33 ⟶ False) ⟶ False) ⟶ (∀ x32 . (x29 x32 x30 = x30 ⟶ False) ⟶ False) ⟶ (∀ x32 x33 x34 . x2 x34 ⟶ x0 (x3 x32 x33) (x4 x34) ⟶ (x32 = x33 ⟶ False) ⟶ False) ⟶ (∀ x32 x33 x34 . x2 x34 ⟶ x0 (x3 x32 x33) (x4 x34) ⟶ (x0 x32 (x28 (x4 x34)) ⟶ False) ⟶ False) ⟶ (∀ x32 x33 . x0 x33 x32 ⟶ (x1 x33 x32 ⟶ False) ⟶ False) ⟶ (∀ x32 . (x28 (x27 x32) = x32 ⟶ False) ⟶ False) ⟶ (∀ x32 x33 . (x5 (x6 x32 x33) x32 ⟶ False) ⟶ False) ⟶ (∀ x32 x33 . (x26 (x6 x33 x32) x32 ⟶ False) ⟶ False) ⟶ (∀ x32 x33 . (x2 (x6 x32 x33) ⟶ False) ⟶ False) ⟶ (x31 x25 ⟶ False) ⟶ ((x7 x8 ⟶ False) ⟶ False) ⟶ ((x2 x8 ⟶ False) ⟶ False) ⟶ ((x31 x9 ⟶ False) ⟶ False) ⟶ ((x2 x24 ⟶ False) ⟶ False) ⟶ (x31 x24 ⟶ False) ⟶ (∀ x32 . (x29 x32 x32 = x32 ⟶ False) ⟶ False) ⟶ (∀ x32 . (x31 x32 ⟶ False) ⟶ x2 x32 ⟶ x31 (x28 x32) ⟶ False) ⟶ (∀ x32 x33 x34 x35 . (x2 (x23 (x3 x33 x32) (x3 x35 x34)) ⟶ False) ⟶ False) ⟶ (∀ x32 x33 . (x2 (x10 (x3 x33 x32)) ⟶ False) ⟶ False) ⟶ (∀ x32 x33 . x31 (x23 x32 x33) ⟶ False) ⟶ (∀ x32 . x31 (x10 x32) ⟶ False) ⟶ (∀ x32 . (x5 (x27 x32) x32 ⟶ False) ⟶ False) ⟶ (∀ x32 . (x26 (x27 x32) x32 ⟶ False) ⟶ False) ⟶ (∀ x32 . (x2 (x27 x32) ⟶ False) ⟶ False) ⟶ ((x31 x30 ⟶ False) ⟶ False) ⟶ (∀ x32 x33 . x2 x33 ⟶ (x2 (x29 x33 x32) ⟶ False) ⟶ False) ⟶ (∀ x32 . x31 x32 ⟶ (x31 (x28 x32) ⟶ False) ⟶ False) ⟶ (∀ x32 . (x1 (x22 x32) x32 ⟶ False) ⟶ False) ⟶ ((x31 x11 ⟶ False) ⟶ False) ⟶ (∀ x32 . (x2 (x27 x32) ⟶ False) ⟶ False) ⟶ (∀ x32 . x2 x32 ⟶ (x2 (x4 x32) ⟶ False) ⟶ False) ⟶ (∀ x32 x33 . (x3 x33 x32 = x23 (x23 x33 x32) (x10 x33) ⟶ False) ⟶ False) ⟶ (∀ x32 x33 x34 . (x0 (x12 x32 x33 x34) x33 ⟶ False) ⟶ (x0 (x12 x32 x33 x34) x32 ⟶ False) ⟶ (x32 = x29 x34 x33 ⟶ False) ⟶ False) ⟶ (∀ x32 x33 x34 . (x0 (x12 x32 x33 x34) x34 ⟶ False) ⟶ (x0 (x12 x32 x33 x34) x32 ⟶ False) ⟶ (x32 = x29 x34 x33 ⟶ False) ⟶ False) ⟶ (∀ x32 x33 x34 . x0 (x12 x32 x33 x34) x32 ⟶ x0 (x12 x32 x33 x34) x34 ⟶ x0 (x12 x32 x33 x34) x33 ⟶ (x32 = x29 x34 x33 ⟶ False) ⟶ False) ⟶ (∀ x32 x33 x34 x35 . x35 = x29 x33 x34 ⟶ x0 x32 x33 ⟶ x0 x32 x34 ⟶ (x0 x32 x35 ⟶ False) ⟶ False) ⟶ (∀ x32 x33 x34 x35 . x33 = x29 x32 x34 ⟶ x0 x35 x33 ⟶ (x0 x35 x34 ⟶ False) ⟶ False) ⟶ (∀ x32 x33 x34 x35 . x33 = x29 x34 x32 ⟶ x0 x35 x33 ⟶ (x0 x35 x34 ⟶ False) ⟶ False) ⟶ ((x30 = x11 ⟶ False) ⟶ False) ⟶ (∀ x32 x33 . x2 x33 ⟶ x2 x32 ⟶ (x0 (x3 (x20 x32 x33) (x21 x32 x33)) x32 ⟶ False) ⟶ (x0 (x3 (x20 x32 x33) (x21 x32 x33)) x33 ⟶ False) ⟶ (x33 = x32 ⟶ False) ⟶ False) ⟶ (∀ x32 x33 . x2 x33 ⟶ x2 x32 ⟶ x0 (x3 (x20 x32 x33) (x21 x32 x33)) x33 ⟶ x0 (x3 (x20 x32 x33) (x21 x32 x33)) x32 ⟶ (x33 = x32 ⟶ False) ⟶ False) ⟶ (∀ x32 x33 x34 x35 . x2 x35 ⟶ x2 x32 ⟶ x35 = x32 ⟶ x0 (x3 x34 x33) x32 ⟶ (x0 (x3 x34 x33) x35 ⟶ False) ⟶ False) ⟶ (∀ x32 x33 x34 x35 . x2 x35 ⟶ x2 x32 ⟶ x35 = x32 ⟶ x0 (x3 x34 x33) x35 ⟶ (x0 (x3 x34 x33) x32 ⟶ False) ⟶ False) ⟶ (∀ x32 . x2 x32 ⟶ (x4 x32 = x29 x32 (x27 (x28 x32)) ⟶ False) ⟶ False) ⟶ (∀ x32 x33 . (x0 (x3 (x13 x33 x32) (x14 x33 x32)) x32 ⟶ False) ⟶ (x0 (x13 x33 x32) x33 ⟶ False) ⟶ (x33 = x28 x32 ⟶ False) ⟶ False) ⟶ (∀ x32 x33 x34 . x0 (x13 x34 x33) x34 ⟶ x0 (x3 (x13 x34 x33) x32) x33 ⟶ (x34 = x28 x33 ⟶ False) ⟶ False) ⟶ (∀ x32 x33 x34 x35 . x34 = x28 x35 ⟶ x0 (x3 x32 x33) x35 ⟶ (x0 x32 x34 ⟶ False) ⟶ False) ⟶ (∀ x32 x33 x34 . x33 = x28 x34 ⟶ x0 x32 x33 ⟶ (x0 (x3 x32 (x19 x32 x33 x34)) x34 ⟶ False) ⟶ False) ⟶ (∀ x32 x33 . x2 x33 ⟶ (x15 x33 x32 = x16 x33 x32 ⟶ False) ⟶ (x0 (x3 (x15 x33 x32) (x16 x33 x32)) x33 ⟶ False) ⟶ (x33 = x27 x32 ⟶ False) ⟶ False) ⟶ (∀ x32 x33 . x2 x33 ⟶ (x0 (x15 x33 x32) x32 ⟶ False) ⟶ (x0 (x3 (x15 x33 x32) (x16 x33 x32)) x33 ⟶ False) ⟶ (x33 = x27 x32 ⟶ False) ⟶ False) ⟶ (∀ x32 x33 . x2 x33 ⟶ x0 (x3 (x15 x33 x32) (x16 x33 x32)) x33 ⟶ x0 (x15 x33 x32) x32 ⟶ x15 x33 x32 = x16 x33 x32 ⟶ (x33 = x27 x32 ⟶ False) ⟶ False) ⟶ (∀ x32 x33 x34 x35 . x2 x35 ⟶ x35 = x27 x32 ⟶ x0 x34 x32 ⟶ x34 = x33 ⟶ (x0 (x3 x34 x33) x35 ⟶ False) ⟶ False) ⟶ (∀ x32 x33 x34 x35 . x2 x35 ⟶ x35 = x27 x32 ⟶ x0 (x3 x34 x33) x35 ⟶ (x34 = x33 ⟶ False) ⟶ False) ⟶ (∀ x32 x33 x34 x35 . x2 x35 ⟶ x35 = x27 x32 ⟶ x0 (x3 x34 x33) x35 ⟶ (x0 x34 x32 ⟶ False) ⟶ False) ⟶ (∀ x32 x33 . (x29 x33 x32 = x29 x32 x33 ⟶ False) ⟶ False) ⟶ (∀ x32 x33 . (x23 x33 x32 = x23 x32 x33 ⟶ False) ⟶ False) ⟶ (∀ x32 x33 . x31 x33 ⟶ x2 x32 ⟶ x5 x32 x33 ⟶ (x5 x32 x33 ⟶ False) ⟶ False) ⟶ (∀ x32 x33 . x31 x33 ⟶ x2 x32 ⟶ x5 x32 x33 ⟶ (x2 x32 ⟶ False) ⟶ False) ⟶ (∀ x32 x33 . x31 x33 ⟶ x2 x32 ⟶ x5 x32 x33 ⟶ (x31 x32 ⟶ False) ⟶ False) ⟶ (∀ x32 x33 . x31 x33 ⟶ x2 x32 ⟶ x26 x32 x33 ⟶ (x26 x32 x33 ⟶ False) ⟶ False) ⟶ (∀ x32 x33 . x31 x33 ⟶ x2 x32 ⟶ x26 x32 x33 ⟶ (x2 x32 ⟶ False) ⟶ False) ⟶ (∀ x32 x33 . x31 x33 ⟶ x2 x32 ⟶ x26 x32 x33 ⟶ (x31 x32 ⟶ False) ⟶ False) ⟶ (∀ x32 . x31 x32 ⟶ x2 x32 ⟶ (x7 x32 ⟶ False) ⟶ False) ⟶ (∀ x32 . x31 x32 ⟶ x2 x32 ⟶ (x2 x32 ⟶ False) ⟶ False) ⟶ (∀ x32 . x31 x32 ⟶ x2 x32 ⟶ (x17 x32 ⟶ False) ⟶ False) ⟶ (∀ x32 . x31 x32 ⟶ x2 x32 ⟶ (x2 x32 ⟶ False) ⟶ False) ⟶ (∀ x32 . x31 x32 ⟶ (x2 x32 ⟶ False) ⟶ False) ⟶ (∀ x32 x33 . x0 x32 x33 ⟶ x0 x33 x32 ⟶ False) ⟶ (x4 x18 = x27 (x28 (x4 x18)) ⟶ False) ⟶ ((x2 x18 ⟶ False) ⟶ False) ⟶ False |
|