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