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