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