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