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