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