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