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