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