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