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