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