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