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