Search for blocks/addresses/...

Proofgold Asset

asset id
a392b9f85af82d83a21e04f2c53065ad3c25e8cec0c91126039e3d68efa1d8f7
asset hash
4de74c97bcad4d936c4117cd66b09f46d8d6cd20af338774e0b179265b5b2b3c
bday / block
35127
tx
e848c..
preasset
doc published by PrPhD..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0 ⟶ False
Theorem d6bc4.. : ∀ 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 : ι → ο . ∀ x49 x50 x51 . ∀ x52 : ι → ι → ο . ∀ x53 : ι → ι . ∀ x54 : ι → ο . ∀ x55 x56 . ∀ x57 : ι → ο . ∀ x58 : ι → ι . ∀ x59 : ι → ο . ∀ x60 : ι → ι → ι → ι → ι → ι . ∀ x61 : ι → ι → ι → ι . ∀ x62 : ι → ι → ι . ∀ x63 : ι → ο . ∀ x64 : ι → ι → ι . ∀ x65 : ι → ο . ∀ x66 : ι → ι → ι → ο . ∀ x67 x68 . ∀ x69 : ι → ι . ∀ x70 . ∀ x71 x72 : ι → ι → ι . ∀ x73 . ∀ x74 : ι → ι → ι . ∀ x75 x76 x77 : ι → ο . ∀ x78 : ι → ι → ο . ∀ x79 : ι → ο . (∀ x80 x81 . x79 x81 ⟶ x79 x80 ⟶ (x78 x81 x80 ⟶ False) ⟶ (x77 x80 ⟶ False) ⟶ (x76 x81 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x0 x81 ⟶ (x81 = x80 ⟶ False) ⟶ x0 x80 ⟶ False) ⟶ (∀ x80 x81 . x79 x81 ⟶ x79 x80 ⟶ (x78 x81 x80 ⟶ False) ⟶ (x76 x81 ⟶ False) ⟶ (x77 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x1 x80 x81 ⟶ x0 x81 ⟶ False) ⟶ (∀ x80 x81 . x79 x81 ⟶ x79 x80 ⟶ x78 x81 x80 ⟶ (x0 x81 ⟶ False) ⟶ (x76 x80 ⟶ False) ⟶ (x77 x81 ⟶ False) ⟶ False) ⟶ (∀ x80 . x0 x80 ⟶ (x80 = x2 ⟶ False) ⟶ False) ⟶ (∀ x80 . x75 x80 ⟶ (x74 x80 x73 = x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 . x1 x80 x81 ⟶ x4 x81 (x3 x82) ⟶ x0 x82 ⟶ False) ⟶ (∀ x80 x81 . x79 x81 ⟶ x79 x80 ⟶ x78 x81 x80 ⟶ (x0 x80 ⟶ False) ⟶ (x77 x81 ⟶ False) ⟶ (x76 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x75 x80 ⟶ (x74 x5 x80 = x5 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 . x1 x81 x82 ⟶ x4 x82 (x3 x80) ⟶ (x4 x81 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x79 x81 ⟶ x79 x80 ⟶ x78 x81 x80 ⟶ (x76 x80 ⟶ False) ⟶ x76 x81 ⟶ False) ⟶ (∀ x80 . x75 x80 ⟶ (x72 x80 x5 = x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x6 x81 x80 ⟶ (x4 x81 (x3 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x4 x81 (x3 x80) ⟶ (x6 x81 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x79 x81 ⟶ x79 x80 ⟶ x78 x81 x80 ⟶ (x77 x81 ⟶ False) ⟶ x77 x80 ⟶ False) ⟶ (∀ x80 . x75 x80 ⟶ (x71 x73 x80 = x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x4 x80 x81 ⟶ (x0 x81 ⟶ False) ⟶ (x1 x80 x81 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x79 x81 ⟶ x79 x80 ⟶ x78 x81 x80 ⟶ x77 x80 ⟶ (x77 x81 ⟶ False) ⟶ False) ⟶ (∀ x80 . x75 x80 ⟶ (x71 x80 x5 = x5 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x1 x81 x80 ⟶ (x4 x81 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x79 x81 ⟶ x79 x80 ⟶ x78 x81 x80 ⟶ x76 x81 ⟶ (x76 x80 ⟶ False) ⟶ False) ⟶ ((x4 x2 x70 ⟶ False) ⟶ False) ⟶ (∀ x80 . x75 x80 ⟶ (x7 x80 x5 = x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x75 x81 ⟶ x75 x80 ⟶ (x72 (x69 x81) (x69 x80) = x72 x80 x81 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x75 x81 ⟶ x75 x80 ⟶ (x7 (x69 x81) (x69 x80) = x69 (x7 x81 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 . x75 x82 ⟶ x75 x80 ⟶ x75 x81 ⟶ (x71 (x71 x82 x80) x81 = x71 x82 (x71 x80 x81) ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 . x75 x82 ⟶ x75 x80 ⟶ x75 x81 ⟶ (x7 (x7 x82 x80) x81 = x7 x82 (x7 x80 x81) ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 . x75 x82 ⟶ x75 x80 ⟶ x75 x81 ⟶ (x71 (x7 x82 x80) x81 = x7 (x71 x82 x81) (x71 x80 x81) ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 . x75 x82 ⟶ x75 x80 ⟶ x75 x81 ⟶ (x71 x82 (x74 x80 x81) = x74 (x71 x82 x80) x81 ⟶ False) ⟶ False) ⟶ ((x4 x67 x68 ⟶ False) ⟶ False) ⟶ ((x4 x67 x8 ⟶ False) ⟶ False) ⟶ ((x66 x67 x68 x8 ⟶ False) ⟶ False) ⟶ ((x76 x67 ⟶ False) ⟶ False) ⟶ (x0 x67 ⟶ False) ⟶ ((x4 x9 x68 ⟶ False) ⟶ False) ⟶ ((x4 x9 x8 ⟶ False) ⟶ False) ⟶ ((x66 x9 x68 x8 ⟶ False) ⟶ False) ⟶ ((x76 x9 ⟶ False) ⟶ False) ⟶ (x0 x9 ⟶ False) ⟶ (∀ x80 . x75 x80 ⟶ (x71 x80 (x69 x73) = x69 x80 ⟶ False) ⟶ False) ⟶ ((x4 x73 x68 ⟶ False) ⟶ False) ⟶ ((x4 x73 x8 ⟶ False) ⟶ False) ⟶ ((x66 x73 x68 x8 ⟶ False) ⟶ False) ⟶ ((x76 x73 ⟶ False) ⟶ False) ⟶ (x0 x73 ⟶ False) ⟶ (∀ x80 x81 . x75 x81 ⟶ x75 x80 ⟶ (x7 x81 (x69 x80) = x72 x81 x80 ⟶ False) ⟶ False) ⟶ ((x4 x10 x68 ⟶ False) ⟶ False) ⟶ ((x4 x10 x8 ⟶ False) ⟶ False) ⟶ ((x66 x10 x68 x8 ⟶ False) ⟶ False) ⟶ ((x0 x10 ⟶ False) ⟶ False) ⟶ ((x69 (x74 (x69 x67) x9) = x74 x67 x9 ⟶ False) ⟶ False) ⟶ ((x69 (x74 (x69 x9) x67) = x74 x9 x67 ⟶ False) ⟶ False) ⟶ ((x69 (x74 (x69 x73) x67) = x74 x73 x67 ⟶ False) ⟶ False) ⟶ ((x69 (x74 (x69 x73) x9) = x74 x73 x9 ⟶ False) ⟶ False) ⟶ ((x69 (x74 x67 x9) = x74 (x69 x67) x9 ⟶ False) ⟶ False) ⟶ ((x69 (x74 x9 x67) = x74 (x69 x9) x67 ⟶ False) ⟶ False) ⟶ ((x69 (x74 x73 x67) = x74 (x69 x73) x67 ⟶ False) ⟶ False) ⟶ ((x69 (x74 x73 x9) = x74 (x69 x73) x9 ⟶ False) ⟶ False) ⟶ ((x69 (x69 x67) = x67 ⟶ False) ⟶ False) ⟶ ((x69 (x69 x9) = x9 ⟶ False) ⟶ False) ⟶ ((x69 (x69 x73) = x73 ⟶ False) ⟶ False) ⟶ ((x69 x67 = x69 x67 ⟶ False) ⟶ False) ⟶ ((x69 x9 = x69 x9 ⟶ False) ⟶ False) ⟶ ((x69 x73 = x69 x73 ⟶ False) ⟶ False) ⟶ ((x69 x10 = x10 ⟶ False) ⟶ False) ⟶ ((x71 (x74 (x69 x67) x9) (x74 (x69 x9) x67) = x73 ⟶ False) ⟶ False) ⟶ ((x71 (x74 (x69 x67) x9) (x74 (x69 x73) x67) = x74 x73 x9 ⟶ False) ⟶ False) ⟶ ((x71 (x74 (x69 x67) x9) (x74 x9 x67) = x69 x73 ⟶ False) ⟶ False) ⟶ ((x71 (x74 (x69 x67) x9) (x74 x73 x67) = x74 (x69 x73) x9 ⟶ False) ⟶ False) ⟶ ((x71 (x74 (x69 x67) x9) (x69 x9) = x67 ⟶ False) ⟶ False) ⟶ ((x71 (x74 (x69 x67) x9) x9 = x69 x67 ⟶ False) ⟶ False) ⟶ ((x71 (x74 (x69 x67) x9) x73 = x74 (x69 x67) x9 ⟶ False) ⟶ False) ⟶ ((x71 (x74 (x69 x9) x67) (x74 (x69 x67) x9) = x73 ⟶ False) ⟶ False) ⟶ ((x71 (x74 (x69 x9) x67) (x74 (x69 x73) x9) = x74 x73 x67 ⟶ False) ⟶ False) ⟶ ((x71 (x74 (x69 x9) x67) (x74 x67 x9) = x69 x73 ⟶ False) ⟶ False) ⟶ ((x71 (x74 (x69 x9) x67) (x74 x73 x9) = x74 (x69 x73) x67 ⟶ False) ⟶ False) ⟶ ((x71 (x74 (x69 x9) x67) (x69 x67) = x9 ⟶ False) ⟶ False) ⟶ ((x71 (x74 (x69 x9) x67) x67 = x69 x9 ⟶ False) ⟶ False) ⟶ ((x71 (x74 (x69 x9) x67) x73 = x74 (x69 x9) x67 ⟶ False) ⟶ False) ⟶ ((x71 (x74 (x69 x73) x67) (x74 (x69 x67) x9) = x74 x73 x9 ⟶ False) ⟶ False) ⟶ ((x71 (x74 (x69 x73) x67) (x74 x67 x9) = x74 (x69 x73) x9 ⟶ False) ⟶ False) ⟶ ((x71 (x74 (x69 x73) x67) (x69 x67) = x73 ⟶ False) ⟶ False) ⟶ ((x71 (x74 (x69 x73) x67) (x69 x9) = x74 x9 x67 ⟶ False) ⟶ False) ⟶ ((x71 (x74 (x69 x73) x67) x67 = x69 x73 ⟶ False) ⟶ False) ⟶ ((x71 (x74 (x69 x73) x67) x9 = x74 (x69 x9) x67 ⟶ False) ⟶ False) ⟶ ((x71 (x74 (x69 x73) x67) x73 = x74 (x69 x73) x67 ⟶ False) ⟶ False) ⟶ ((x71 (x74 (x69 x73) x9) (x74 x9 x67) = x74 (x69 x73) x67 ⟶ False) ⟶ False) ⟶ ((x71 (x74 (x69 x73) x9) (x69 x67) = x74 x67 x9 ⟶ False) ⟶ False) ⟶ ((x71 (x74 (x69 x73) x9) (x69 x9) = x73 ⟶ False) ⟶ False) ⟶ ((x71 (x74 (x69 x73) x9) x67 = x74 (x69 x67) x9 ⟶ False) ⟶ False) ⟶ ((x71 (x74 (x69 x73) x9) x9 = x69 x73 ⟶ False) ⟶ False) ⟶ ((x71 (x74 (x69 x73) x9) x73 = x74 (x69 x73) x9 ⟶ False) ⟶ False) ⟶ ((x71 (x74 x67 x9) (x74 (x69 x9) x67) = x69 x73 ⟶ False) ⟶ False) ⟶ ((x71 (x74 x67 x9) (x74 (x69 x73) x67) = x74 (x69 x73) x9 ⟶ False) ⟶ False) ⟶ ((x71 (x74 x67 x9) (x74 x9 x67) = x73 ⟶ False) ⟶ False) ⟶ ((x71 (x74 x67 x9) (x74 x73 x67) = x74 x73 x9 ⟶ False) ⟶ False) ⟶ ((x71 (x74 x67 x9) (x69 x9) = x69 x67 ⟶ False) ⟶ False) ⟶ ((x71 (x74 x67 x9) x9 = x67 ⟶ False) ⟶ False) ⟶ ((x71 (x74 x67 x9) x73 = x74 x67 x9 ⟶ False) ⟶ False) ⟶ ((x71 (x74 x9 x67) (x74 (x69 x67) x9) = x69 x73 ⟶ False) ⟶ False) ⟶ ((x71 (x74 x9 x67) (x74 (x69 x73) x9) = x74 (x69 x73) x67 ⟶ False) ⟶ False) ⟶ ((x71 (x74 x9 x67) (x74 x67 x9) = x73 ⟶ False) ⟶ False) ⟶ ((x71 (x74 x9 x67) (x74 x73 x9) = x74 x73 x67 ⟶ False) ⟶ False) ⟶ ((x71 (x74 x9 x67) (x69 x67) = x69 x9 ⟶ False) ⟶ False) ⟶ ((x71 (x74 x9 x67) x67 = x9 ⟶ False) ⟶ False) ⟶ ((x71 (x74 x9 x67) x73 = x74 x9 x67 ⟶ False) ⟶ False) ⟶ ((x71 (x74 x9 x67) x10 = x10 ⟶ False) ⟶ False) ⟶ ((x71 (x74 x73 x67) (x74 (x69 x67) x9) = x74 (x69 x73) x9 ⟶ False) ⟶ False) ⟶ ((x71 (x74 x73 x67) (x74 x67 x9) = x74 x73 x9 ⟶ False) ⟶ False) ⟶ ((x71 (x74 x73 x67) (x69 x67) = x69 x73 ⟶ False) ⟶ False) ⟶ ((x71 (x74 x73 x67) (x69 x9) = x74 (x69 x9) x67 ⟶ False) ⟶ False) ⟶ ((x71 (x74 x73 x67) x67 = x73 ⟶ False) ⟶ False) ⟶ ((x71 (x74 x73 x67) x9 = x74 x9 x67 ⟶ False) ⟶ False) ⟶ ((x71 (x74 x73 x67) x73 = x74 x73 x67 ⟶ False) ⟶ False) ⟶ ((x71 (x74 x73 x9) (x74 (x69 x9) x67) = x74 (x69 x73) x67 ⟶ False) ⟶ False) ⟶ ((x71 (x74 x73 x9) (x74 x9 x67) = x74 x73 x67 ⟶ False) ⟶ False) ⟶ ((x71 (x74 x73 x9) (x69 x67) = x74 (x69 x67) x9 ⟶ False) ⟶ False) ⟶ ((x71 (x74 x73 x9) (x69 x9) = x69 x73 ⟶ False) ⟶ False) ⟶ ((x71 (x74 x73 x9) x67 = x74 x67 x9 ⟶ False) ⟶ False) ⟶ ((x71 (x74 x73 x9) x9 = x73 ⟶ False) ⟶ False) ⟶ ((x71 (x74 x73 x9) x73 = x74 x73 x9 ⟶ False) ⟶ False) ⟶ ((x71 (x74 x73 x9) x10 = x10 ⟶ False) ⟶ False) ⟶ ((x71 (x69 x67) (x74 (x69 x9) x67) = x9 ⟶ False) ⟶ False) ⟶ ((x71 (x69 x67) (x74 (x69 x73) x67) = x73 ⟶ False) ⟶ False) ⟶ ((x71 (x69 x67) (x74 (x69 x73) x9) = x74 x67 x9 ⟶ False) ⟶ False) ⟶ ((x71 (x69 x67) (x74 x9 x67) = x69 x9 ⟶ False) ⟶ False) ⟶ ((x71 (x69 x67) (x74 x73 x67) = x69 x73 ⟶ False) ⟶ False) ⟶ ((x71 (x69 x67) (x74 x73 x9) = x74 (x69 x67) x9 ⟶ False) ⟶ False) ⟶ ((x71 (x69 x67) x73 = x69 x67 ⟶ False) ⟶ False) ⟶ ((x71 (x69 x67) x10 = x10 ⟶ False) ⟶ False) ⟶ ((x71 (x69 x9) (x74 (x69 x67) x9) = x67 ⟶ False) ⟶ False) ⟶ ((x71 (x69 x9) (x74 (x69 x73) x67) = x74 x9 x67 ⟶ False) ⟶ False) ⟶ ((x71 (x69 x9) (x74 (x69 x73) x9) = x73 ⟶ False) ⟶ False) ⟶ ((x71 (x69 x9) (x74 x67 x9) = x69 x67 ⟶ False) ⟶ False) ⟶ ((x71 (x69 x9) (x74 x73 x67) = x74 (x69 x9) x67 ⟶ False) ⟶ False) ⟶ ((x71 (x69 x9) (x74 x73 x9) = x69 x73 ⟶ False) ⟶ False) ⟶ ((x71 (x69 x9) x73 = x69 x9 ⟶ False) ⟶ False) ⟶ ((x71 (x69 x9) x10 = x10 ⟶ False) ⟶ False) ⟶ ((x71 x67 (x74 (x69 x9) x67) = x69 x9 ⟶ False) ⟶ False) ⟶ ((x71 x67 (x74 (x69 x73) x67) = x69 x73 ⟶ False) ⟶ False) ⟶ ((x71 x67 (x74 (x69 x73) x9) = x74 (x69 x67) x9 ⟶ False) ⟶ False) ⟶ ((x71 x67 (x74 x9 x67) = x9 ⟶ False) ⟶ False) ⟶ ((x71 x67 (x74 x73 x67) = x73 ⟶ False) ⟶ False) ⟶ ((x71 x67 (x74 x73 x9) = x74 x67 x9 ⟶ False) ⟶ False) ⟶ ((x71 x67 x73 = x67 ⟶ False) ⟶ False) ⟶ ((x71 x67 x10 = x10 ⟶ False) ⟶ False) ⟶ ((x71 x9 (x74 (x69 x67) x9) = x69 x67 ⟶ False) ⟶ False) ⟶ ((x71 x9 (x74 (x69 x73) x67) = x74 (x69 x9) x67 ⟶ False) ⟶ False) ⟶ ((x71 x9 (x74 (x69 x73) x9) = x69 x73 ⟶ False) ⟶ False) ⟶ ((x71 x9 (x74 x67 x9) = x67 ⟶ False) ⟶ False) ⟶ ((x71 x9 (x74 x73 x67) = x74 x9 x67 ⟶ False) ⟶ False) ⟶ ((x71 x9 (x74 x73 x9) = x73 ⟶ False) ⟶ False) ⟶ ((x71 x9 x73 = x9 ⟶ False) ⟶ False) ⟶ ((x71 x9 x10 = x10 ⟶ False) ⟶ False) ⟶ ((x71 x73 (x74 (x69 x67) x9) = x74 (x69 x67) x9 ⟶ False) ⟶ False) ⟶ ((x71 x73 (x74 (x69 x9) x67) = x74 (x69 x9) x67 ⟶ False) ⟶ False) ⟶ ((x71 x73 (x74 (x69 x73) x67) = x74 (x69 x73) x67 ⟶ False) ⟶ False) ⟶ ((x71 x73 (x74 (x69 x73) x9) = x74 (x69 x73) x9 ⟶ False) ⟶ False) ⟶ ((x71 x73 (x74 x67 x9) = x74 x67 x9 ⟶ False) ⟶ False) ⟶ ((x71 x73 (x74 x9 x67) = x74 x9 x67 ⟶ False) ⟶ False) ⟶ ((x71 x73 (x74 x73 x67) = x74 x73 x67 ⟶ False) ⟶ False) ⟶ ((x71 x73 (x74 x73 x9) = x74 x73 x9 ⟶ False) ⟶ False) ⟶ ((x71 x73 (x69 x67) = x69 x67 ⟶ False) ⟶ False) ⟶ ((x71 x73 (x69 x9) = x69 x9 ⟶ False) ⟶ False) ⟶ ((x71 x73 x67 = x67 ⟶ False) ⟶ False) ⟶ ((x71 x73 x9 = x9 ⟶ False) ⟶ False) ⟶ ((x71 x73 x73 = x73 ⟶ False) ⟶ False) ⟶ ((x71 x73 x10 = x10 ⟶ False) ⟶ False) ⟶ ((x71 x10 (x74 x9 x67) = x10 ⟶ False) ⟶ False) ⟶ ((x71 x10 (x74 x73 x67) = x10 ⟶ False) ⟶ False) ⟶ ((x71 x10 (x74 x73 x9) = x10 ⟶ False) ⟶ False) ⟶ ((x71 x10 (x69 x67) = x10 ⟶ False) ⟶ False) ⟶ ((x71 x10 (x69 x9) = x10 ⟶ False) ⟶ False) ⟶ ((x71 x10 x67 = x10 ⟶ False) ⟶ False) ⟶ ((x71 x10 x9 = x10 ⟶ False) ⟶ False) ⟶ ((x71 x10 x73 = x10 ⟶ False) ⟶ False) ⟶ ((x71 x10 x10 = x10 ⟶ False) ⟶ False) ⟶ ((x74 (x69 x9) x9 = x69 x73 ⟶ False) ⟶ False) ⟶ ((x74 (x69 x73) x9 = x74 (x69 x73) x9 ⟶ False) ⟶ False) ⟶ ((x74 (x69 x73) x73 = x69 x73 ⟶ False) ⟶ False) ⟶ ((x74 x67 x67 = x73 ⟶ False) ⟶ False) ⟶ ((x74 x67 x9 = x74 x67 x9 ⟶ False) ⟶ False) ⟶ ((x74 x9 x67 = x74 x9 x67 ⟶ False) ⟶ False) ⟶ ((x74 x9 x9 = x73 ⟶ False) ⟶ False) ⟶ ((x74 x9 x73 = x9 ⟶ False) ⟶ False) ⟶ ((x74 x73 (x74 (x69 x67) x9) = x74 (x69 x9) x67 ⟶ False) ⟶ False) ⟶ ((x74 x73 (x74 (x69 x73) x67) = x69 x67 ⟶ False) ⟶ False) ⟶ ((x74 x73 (x74 (x69 x73) x9) = x69 x9 ⟶ False) ⟶ False) ⟶ ((x74 x73 (x74 x67 x9) = x74 x9 x67 ⟶ False) ⟶ False) ⟶ ((x74 x73 (x74 x9 x67) = x74 x67 x9 ⟶ False) ⟶ False) ⟶ ((x74 x73 (x74 x73 x67) = x67 ⟶ False) ⟶ False) ⟶ ((x74 x73 (x74 x73 x9) = x9 ⟶ False) ⟶ False) ⟶ ((x74 x73 (x69 x67) = x74 (x69 x73) x67 ⟶ False) ⟶ False) ⟶ ((x74 x73 (x69 x9) = x74 (x69 x73) x9 ⟶ False) ⟶ False) ⟶ ((x74 x73 (x69 x73) = x69 x73 ⟶ False) ⟶ False) ⟶ ((x74 x73 x67 = x74 x73 x67 ⟶ False) ⟶ False) ⟶ ((x74 x73 x9 = x74 x73 x9 ⟶ False) ⟶ False) ⟶ ((x74 x73 x73 = x73 ⟶ False) ⟶ False) ⟶ ((x72 (x74 (x69 x67) x9) (x74 (x69 x67) x9) = x10 ⟶ False) ⟶ False) ⟶ ((x72 (x74 (x69 x67) x9) (x74 (x69 x73) x9) = x69 x73 ⟶ False) ⟶ False) ⟶ ((x72 (x74 (x69 x67) x9) (x74 x67 x9) = x69 x67 ⟶ False) ⟶ False) ⟶ ((x72 (x74 (x69 x67) x9) (x74 x73 x9) = x69 x9 ⟶ False) ⟶ False) ⟶ ((x72 (x74 (x69 x67) x9) (x69 x67) = x74 x67 x9 ⟶ False) ⟶ False) ⟶ ((x72 (x74 (x69 x67) x9) (x69 x9) = x74 x73 x9 ⟶ False) ⟶ False) ⟶ ((x72 (x74 (x69 x67) x9) (x69 x73) = x74 (x69 x73) x9 ⟶ False) ⟶ False) ⟶ ((x72 (x74 (x69 x67) x9) x10 = x74 (x69 x67) x9 ⟶ False) ⟶ False) ⟶ ((x72 (x74 (x69 x9) x67) (x74 (x69 x9) x67) = x10 ⟶ False) ⟶ False) ⟶ ((x72 (x74 (x69 x9) x67) (x74 (x69 x73) x67) = x74 (x69 x73) x67 ⟶ False) ⟶ False) ⟶ ((x72 (x74 (x69 x9) x67) (x74 x73 x67) = x69 x73 ⟶ False) ⟶ False) ⟶ ((x72 (x74 (x69 x9) x67) (x69 x73) = x74 x73 x67 ⟶ False) ⟶ False) ⟶ ((x72 (x74 (x69 x73) x67) (x74 (x69 x9) x67) = x74 x73 x67 ⟶ False) ⟶ False) ⟶ ((x72 (x74 (x69 x73) x67) (x74 (x69 x73) x67) = x10 ⟶ False) ⟶ False) ⟶ ((x72 (x74 (x69 x73) x67) (x74 x9 x67) = x69 x73 ⟶ False) ⟶ False) ⟶ ((x72 (x74 (x69 x73) x67) (x74 x73 x67) = x74 (x69 x9) x67 ⟶ False) ⟶ False) ⟶ ((x72 (x74 (x69 x73) x67) (x69 x73) = x74 x9 x67 ⟶ False) ⟶ False) ⟶ ((x72 (x74 (x69 x73) x67) x10 = x74 (x69 x73) x67 ⟶ False) ⟶ False) ⟶ ((x72 (x74 (x69 x73) x9) (x74 (x69 x67) x9) = x73 ⟶ False) ⟶ False) ⟶ ((x72 (x74 (x69 x73) x9) (x74 (x69 x73) x9) = x10 ⟶ False) ⟶ False) ⟶ ((x72 (x74 (x69 x73) x9) (x74 x67 x9) = x69 x9 ⟶ False) ⟶ False) ⟶ ((x72 (x74 (x69 x73) x9) (x74 x73 x9) = x69 x73 ⟶ False) ⟶ False) ⟶ ((x72 (x74 (x69 x73) x9) (x69 x9) = x74 x67 x9 ⟶ False) ⟶ False) ⟶ ((x72 (x74 (x69 x73) x9) (x69 x73) = x74 x73 x9 ⟶ False) ⟶ False) ⟶ ((x72 (x74 (x69 x73) x9) x73 = x74 (x69 x67) x9 ⟶ False) ⟶ False) ⟶ ((x72 (x74 (x69 x73) x9) x10 = x74 (x69 x73) x9 ⟶ False) ⟶ False) ⟶ ((x72 (x74 x67 x9) (x74 (x69 x67) x9) = x67 ⟶ False) ⟶ False) ⟶ ((x72 (x74 x67 x9) (x74 (x69 x73) x9) = x9 ⟶ False) ⟶ False) ⟶ ((x72 (x74 x67 x9) (x74 x67 x9) = x10 ⟶ False) ⟶ False) ⟶ ((x72 (x74 x67 x9) (x74 x73 x9) = x73 ⟶ False) ⟶ False) ⟶ ((x72 (x74 x67 x9) x67 = x74 (x69 x67) x9 ⟶ False) ⟶ False) ⟶ ((x72 (x74 x67 x9) x9 = x74 (x69 x73) x9 ⟶ False) ⟶ False) ⟶ ((x72 (x74 x67 x9) x73 = x74 x73 x9 ⟶ False) ⟶ False) ⟶ ((x72 (x74 x67 x9) x10 = x74 x67 x9 ⟶ False) ⟶ False) ⟶ ((x72 (x74 x9 x67) (x74 (x69 x73) x67) = x73 ⟶ False) ⟶ False) ⟶ ((x72 (x74 x9 x67) (x74 x9 x67) = x10 ⟶ False) ⟶ False) ⟶ ((x72 (x74 x9 x67) (x74 x73 x67) = x74 x73 x67 ⟶ False) ⟶ False) ⟶ ((x72 (x74 x9 x67) x73 = x74 (x69 x73) x67 ⟶ False) ⟶ False) ⟶ ((x72 (x74 x9 x67) x10 = x74 x9 x67 ⟶ False) ⟶ False) ⟶ ((x72 (x74 x73 x67) (x74 (x69 x9) x67) = x73 ⟶ False) ⟶ False) ⟶ ((x72 (x74 x73 x67) (x74 (x69 x73) x67) = x74 x9 x67 ⟶ False) ⟶ False) ⟶ ((x72 (x74 x73 x67) (x74 x9 x67) = x74 (x69 x73) x67 ⟶ False) ⟶ False) ⟶ ((x72 (x74 x73 x67) (x74 x73 x67) = x10 ⟶ False) ⟶ False) ⟶ ((x72 (x74 x73 x67) x73 = x74 (x69 x9) x67 ⟶ False) ⟶ False) ⟶ ((x72 (x74 x73 x67) x10 = x74 x73 x67 ⟶ False) ⟶ False) ⟶ ((x72 (x74 x73 x9) (x74 (x69 x67) x9) = x9 ⟶ False) ⟶ False) ⟶ ((x72 (x74 x73 x9) (x74 (x69 x73) x9) = x73 ⟶ False) ⟶ False) ⟶ ((x72 (x74 x73 x9) (x74 x67 x9) = x69 x73 ⟶ False) ⟶ False) ⟶ ((x72 (x74 x73 x9) (x74 x73 x9) = x10 ⟶ False) ⟶ False) ⟶ ((x72 (x74 x73 x9) (x69 x73) = x74 x67 x9 ⟶ False) ⟶ False) ⟶ ((x72 (x74 x73 x9) x9 = x74 (x69 x67) x9 ⟶ False) ⟶ False) ⟶ ((x72 (x74 x73 x9) x73 = x74 (x69 x73) x9 ⟶ False) ⟶ False) ⟶ ((x72 (x74 x73 x9) x10 = x74 x73 x9 ⟶ False) ⟶ False) ⟶ ((x72 (x69 x67) (x74 (x69 x67) x9) = x74 (x69 x67) x9 ⟶ False) ⟶ False) ⟶ ((x72 (x69 x67) (x69 x67) = x10 ⟶ False) ⟶ False) ⟶ ((x72 (x69 x67) (x69 x9) = x69 x73 ⟶ False) ⟶ False) ⟶ ((x72 (x69 x67) (x69 x73) = x69 x9 ⟶ False) ⟶ False) ⟶ ((x72 (x69 x67) x10 = x69 x67 ⟶ False) ⟶ False) ⟶ ((x72 (x69 x9) (x74 (x69 x67) x9) = x74 (x69 x73) x9 ⟶ False) ⟶ False) ⟶ ((x72 (x69 x9) (x74 (x69 x73) x9) = x74 (x69 x67) x9 ⟶ False) ⟶ False) ⟶ ((x72 (x69 x9) (x69 x67) = x73 ⟶ False) ⟶ False) ⟶ ((x72 (x69 x9) (x69 x9) = x10 ⟶ False) ⟶ False) ⟶ ((x72 (x69 x9) (x69 x73) = x69 x73 ⟶ False) ⟶ False) ⟶ ((x72 (x69 x9) x73 = x69 x67 ⟶ False) ⟶ False) ⟶ ((x72 (x69 x9) x10 = x69 x9 ⟶ False) ⟶ False) ⟶ ((x72 (x69 x73) (x74 (x69 x67) x9) = x74 x73 x9 ⟶ False) ⟶ False) ⟶ ((x72 (x69 x73) (x74 (x69 x9) x67) = x74 (x69 x73) x67 ⟶ False) ⟶ False) ⟶ ((x72 (x69 x73) (x74 (x69 x73) x67) = x74 (x69 x9) x67 ⟶ False) ⟶ False) ⟶ ((x72 (x69 x73) (x74 (x69 x73) x9) = x74 (x69 x73) x9 ⟶ False) ⟶ False) ⟶ ((x72 (x69 x73) (x74 x73 x9) = x74 (x69 x67) x9 ⟶ False) ⟶ False) ⟶ ((x72 (x69 x73) (x69 x67) = x9 ⟶ False) ⟶ False) ⟶ ((x72 (x69 x73) (x69 x9) = x73 ⟶ False) ⟶ False) ⟶ ((x72 (x69 x73) (x69 x73) = x10 ⟶ False) ⟶ False) ⟶ ((x72 (x69 x73) x9 = x69 x67 ⟶ False) ⟶ False) ⟶ ((x72 (x69 x73) x73 = x69 x9 ⟶ False) ⟶ False) ⟶ ((x72 (x69 x73) x10 = x69 x73 ⟶ False) ⟶ False) ⟶ ((x72 x67 (x74 x67 x9) = x74 x67 x9 ⟶ False) ⟶ False) ⟶ ((x72 x67 x67 = x10 ⟶ False) ⟶ False) ⟶ ((x72 x67 x9 = x73 ⟶ False) ⟶ False) ⟶ ((x72 x67 x73 = x9 ⟶ False) ⟶ False) ⟶ ((x72 x67 x10 = x67 ⟶ False) ⟶ False) ⟶ ((x72 x9 (x74 x67 x9) = x74 x73 x9 ⟶ False) ⟶ False) ⟶ ((x72 x9 (x74 x73 x9) = x74 x67 x9 ⟶ False) ⟶ False) ⟶ ((x72 x9 (x69 x73) = x67 ⟶ False) ⟶ False) ⟶ ((x72 x9 x67 = x69 x73 ⟶ False) ⟶ False) ⟶ ((x72 x9 x9 = x10 ⟶ False) ⟶ False) ⟶ ((x72 x9 x73 = x73 ⟶ False) ⟶ False) ⟶ ((x72 x9 x10 = x9 ⟶ False) ⟶ False) ⟶ ((x72 x73 (x74 (x69 x73) x9) = x74 x67 x9 ⟶ False) ⟶ False) ⟶ ((x72 x73 (x74 x67 x9) = x74 (x69 x73) x9 ⟶ False) ⟶ False) ⟶ ((x72 x73 (x74 x9 x67) = x74 x73 x67 ⟶ False) ⟶ False) ⟶ ((x72 x73 (x74 x73 x67) = x74 x9 x67 ⟶ False) ⟶ False) ⟶ ((x72 x73 (x74 x73 x9) = x74 x73 x9 ⟶ False) ⟶ False) ⟶ ((x72 x73 (x69 x9) = x67 ⟶ False) ⟶ False) ⟶ ((x72 x73 (x69 x73) = x9 ⟶ False) ⟶ False) ⟶ ((x72 x73 x67 = x69 x9 ⟶ False) ⟶ False) ⟶ ((x72 x73 x9 = x69 x73 ⟶ False) ⟶ False) ⟶ ((x72 x73 x73 = x10 ⟶ False) ⟶ False) ⟶ ((x72 x73 x10 = x73 ⟶ False) ⟶ False) ⟶ ((x72 x10 (x74 (x69 x67) x9) = x74 x67 x9 ⟶ False) ⟶ False) ⟶ ((x72 x10 (x74 (x69 x73) x9) = x74 x73 x9 ⟶ False) ⟶ False) ⟶ ((x72 x10 (x74 x67 x9) = x74 (x69 x67) x9 ⟶ False) ⟶ False) ⟶ ((x72 x10 (x74 x9 x67) = x74 (x69 x9) x67 ⟶ False) ⟶ False) ⟶ ((x72 x10 (x74 x73 x67) = x74 (x69 x73) x67 ⟶ False) ⟶ False) ⟶ ((x72 x10 (x74 x73 x9) = x74 (x69 x73) x9 ⟶ False) ⟶ False) ⟶ ((x72 x10 (x69 x67) = x67 ⟶ False) ⟶ False) ⟶ ((x72 x10 (x69 x9) = x9 ⟶ False) ⟶ False) ⟶ ((x72 x10 (x69 x73) = x73 ⟶ False) ⟶ False) ⟶ ((x72 x10 x67 = x69 x67 ⟶ False) ⟶ False) ⟶ ((x72 x10 x9 = x69 x9 ⟶ False) ⟶ False) ⟶ ((x72 x10 x73 = x69 x73 ⟶ False) ⟶ False) ⟶ ((x72 x10 x10 = x10 ⟶ False) ⟶ False) ⟶ ((x7 (x74 (x69 x67) x9) (x74 (x69 x67) x9) = x69 x67 ⟶ False) ⟶ False) ⟶ ((x7 (x74 (x69 x67) x9) (x74 x67 x9) = x10 ⟶ False) ⟶ False) ⟶ ((x7 (x74 (x69 x67) x9) (x74 x73 x9) = x69 x73 ⟶ False) ⟶ False) ⟶ ((x7 (x74 (x69 x67) x9) x9 = x74 x73 x9 ⟶ False) ⟶ False) ⟶ ((x7 (x74 (x69 x67) x9) x73 = x74 (x69 x73) x9 ⟶ False) ⟶ False) ⟶ ((x7 (x74 (x69 x9) x67) (x74 (x69 x73) x67) = x69 x73 ⟶ False) ⟶ False) ⟶ ((x7 (x74 (x69 x9) x67) (x74 x9 x67) = x10 ⟶ False) ⟶ False) ⟶ ((x7 (x74 (x69 x9) x67) x73 = x74 x73 x67 ⟶ False) ⟶ False) ⟶ ((x7 (x74 (x69 x73) x67) (x74 (x69 x9) x67) = x69 x73 ⟶ False) ⟶ False) ⟶ ((x7 (x74 (x69 x73) x67) (x74 (x69 x73) x67) = x74 (x69 x9) x67 ⟶ False) ⟶ False) ⟶ ((x7 (x74 (x69 x73) x67) (x74 x9 x67) = x74 x73 x67 ⟶ False) ⟶ False) ⟶ ((x7 (x74 (x69 x73) x67) (x74 x73 x67) = x10 ⟶ False) ⟶ False) ⟶ ((x7 (x74 (x69 x73) x67) x73 = x74 x9 x67 ⟶ False) ⟶ False) ⟶ ((x7 (x74 (x69 x73) x9) (x74 (x69 x67) x9) = x69 x9 ⟶ False) ⟶ False) ⟶ ((x7 (x74 (x69 x73) x9) (x74 (x69 x73) x9) = x69 x73 ⟶ False) ⟶ False) ⟶ ((x7 (x74 (x69 x73) x9) (x74 x67 x9) = x73 ⟶ False) ⟶ False) ⟶ ((x7 (x74 (x69 x73) x9) (x74 x73 x9) = x10 ⟶ False) ⟶ False) ⟶ ((x7 (x74 (x69 x73) x9) (x69 x73) = x74 (x69 x67) x9 ⟶ False) ⟶ False) ⟶ ((x7 (x74 (x69 x73) x9) x9 = x74 x67 x9 ⟶ False) ⟶ False) ⟶ ((x7 (x74 (x69 x73) x9) x73 = x74 x73 x9 ⟶ False) ⟶ False) ⟶ ((x7 (x74 x67 x9) (x74 (x69 x67) x9) = x10 ⟶ False) ⟶ False) ⟶ ((x7 (x74 x67 x9) (x74 (x69 x73) x9) = x73 ⟶ False) ⟶ False) ⟶ ((x7 (x74 x67 x9) (x74 x67 x9) = x67 ⟶ False) ⟶ False) ⟶ ((x7 (x74 x67 x9) (x74 x73 x9) = x9 ⟶ False) ⟶ False) ⟶ ((x7 (x74 x67 x9) (x69 x9) = x74 (x69 x73) x9 ⟶ False) ⟶ False) ⟶ ((x7 (x74 x67 x9) (x69 x73) = x74 x73 x9 ⟶ False) ⟶ False) ⟶ ((x7 (x74 x67 x9) x10 = x74 x67 x9 ⟶ False) ⟶ False) ⟶ ((x7 (x74 x9 x67) (x74 (x69 x9) x67) = x10 ⟶ False) ⟶ False) ⟶ ((x7 (x74 x9 x67) (x74 (x69 x73) x67) = x74 x73 x67 ⟶ False) ⟶ False) ⟶ ((x7 (x74 x9 x67) (x74 x73 x67) = x73 ⟶ False) ⟶ False) ⟶ ((x7 (x74 x9 x67) x10 = x74 x9 x67 ⟶ False) ⟶ False) ⟶ ((x7 (x74 x73 x67) (x74 (x69 x9) x67) = x74 (x69 x73) x67 ⟶ False) ⟶ False) ⟶ ((x7 (x74 x73 x67) (x74 (x69 x73) x67) = x10 ⟶ False) ⟶ False) ⟶ ((x7 (x74 x73 x67) (x74 x9 x67) = x73 ⟶ False) ⟶ False) ⟶ ((x7 (x74 x73 x67) (x74 x73 x67) = x74 x9 x67 ⟶ False) ⟶ False) ⟶ ((x7 (x74 x73 x9) (x74 (x69 x67) x9) = x69 x73 ⟶ False) ⟶ False) ⟶ ((x7 (x74 x73 x9) (x74 (x69 x73) x9) = x10 ⟶ False) ⟶ False) ⟶ ((x7 (x74 x73 x9) (x74 x67 x9) = x9 ⟶ False) ⟶ False) ⟶ ((x7 (x74 x73 x9) (x74 x73 x9) = x73 ⟶ False) ⟶ False) ⟶ ((x7 (x74 x73 x9) (x69 x9) = x74 (x69 x67) x9 ⟶ False) ⟶ False) ⟶ ((x7 (x74 x73 x9) (x69 x73) = x74 (x69 x73) x9 ⟶ False) ⟶ False) ⟶ ((x7 (x74 x73 x9) x73 = x74 x67 x9 ⟶ False) ⟶ False) ⟶ ((x7 (x74 x73 x9) x10 = x74 x73 x9 ⟶ False) ⟶ False) ⟶ ((x7 (x69 x67) (x74 x67 x9) = x74 (x69 x67) x9 ⟶ False) ⟶ False) ⟶ ((x7 (x69 x67) x67 = x10 ⟶ False) ⟶ False) ⟶ ((x7 (x69 x67) x9 = x69 x73 ⟶ False) ⟶ False) ⟶ ((x7 (x69 x67) x73 = x69 x9 ⟶ False) ⟶ False) ⟶ ((x7 (x69 x9) (x74 x67 x9) = x74 (x69 x73) x9 ⟶ False) ⟶ False) ⟶ ((x7 (x69 x9) (x69 x73) = x69 x67 ⟶ False) ⟶ False) ⟶ ((x7 (x69 x9) x67 = x73 ⟶ False) ⟶ False) ⟶ ((x7 (x69 x9) x9 = x10 ⟶ False) ⟶ False) ⟶ ((x7 (x69 x9) x73 = x69 x73 ⟶ False) ⟶ False) ⟶ ((x7 (x69 x73) (x74 (x69 x73) x9) = x74 (x69 x67) x9 ⟶ False) ⟶ False) ⟶ ((x7 (x69 x73) (x74 x67 x9) = x74 x73 x9 ⟶ False) ⟶ False) ⟶ ((x7 (x69 x73) (x74 x9 x67) = x74 (x69 x73) x67 ⟶ False) ⟶ False) ⟶ ((x7 (x69 x73) (x74 x73 x9) = x74 (x69 x73) x9 ⟶ False) ⟶ False) ⟶ ((x7 (x69 x73) (x69 x9) = x69 x67 ⟶ False) ⟶ False) ⟶ ((x7 (x69 x73) (x69 x73) = x69 x9 ⟶ False) ⟶ False) ⟶ ((x7 (x69 x73) x67 = x9 ⟶ False) ⟶ False) ⟶ ((x7 (x69 x73) x9 = x73 ⟶ False) ⟶ False) ⟶ ((x7 (x69 x73) x73 = x10 ⟶ False) ⟶ False) ⟶ ((x7 (x69 x73) x10 = x69 x73 ⟶ False) ⟶ False) ⟶ ((x7 x67 (x69 x67) = x10 ⟶ False) ⟶ False) ⟶ ((x7 x67 (x69 x9) = x73 ⟶ False) ⟶ False) ⟶ ((x7 x67 (x69 x73) = x9 ⟶ False) ⟶ False) ⟶ ((x7 x67 x10 = x67 ⟶ False) ⟶ False) ⟶ ((x7 x9 (x74 (x69 x67) x9) = x74 x73 x9 ⟶ False) ⟶ False) ⟶ ((x7 x9 (x74 (x69 x73) x9) = x74 x67 x9 ⟶ False) ⟶ False) ⟶ ((x7 x9 (x69 x67) = x69 x73 ⟶ False) ⟶ False) ⟶ ((x7 x9 (x69 x9) = x10 ⟶ False) ⟶ False) ⟶ ((x7 x9 (x69 x73) = x73 ⟶ False) ⟶ False) ⟶ ((x7 x9 x73 = x67 ⟶ False) ⟶ False) ⟶ ((x7 x9 x10 = x9 ⟶ False) ⟶ False) ⟶ ((x7 x73 (x74 (x69 x9) x67) = x74 x73 x67 ⟶ False) ⟶ False) ⟶ ((x7 x73 (x74 (x69 x73) x67) = x74 x9 x67 ⟶ False) ⟶ False) ⟶ ((x7 x73 (x74 (x69 x73) x9) = x74 x73 x9 ⟶ False) ⟶ False) ⟶ ((x7 x73 (x74 x73 x9) = x74 x67 x9 ⟶ False) ⟶ False) ⟶ ((x7 x73 (x69 x67) = x69 x9 ⟶ False) ⟶ False) ⟶ ((x7 x73 (x69 x9) = x69 x73 ⟶ False) ⟶ False) ⟶ ((x7 x73 (x69 x73) = x10 ⟶ False) ⟶ False) ⟶ ((x7 x73 x9 = x67 ⟶ False) ⟶ False) ⟶ ((x7 x73 x73 = x9 ⟶ False) ⟶ False) ⟶ ((x7 x73 x10 = x73 ⟶ False) ⟶ False) ⟶ ((x7 x10 (x74 (x69 x73) x9) = x74 (x69 x73) x9 ⟶ False) ⟶ False) ⟶ ((x7 x10 (x74 x67 x9) = x74 x67 x9 ⟶ False) ⟶ False) ⟶ ((x7 x10 (x74 x9 x67) = x74 x9 x67 ⟶ False) ⟶ False) ⟶ ((x7 x10 (x74 x73 x9) = x74 x73 x9 ⟶ False) ⟶ False) ⟶ ((x7 x10 (x69 x67) = x69 x67 ⟶ False) ⟶ False) ⟶ ((x7 x10 (x69 x9) = x69 x9 ⟶ False) ⟶ False) ⟶ ((x7 x10 (x69 x73) = x69 x73 ⟶ False) ⟶ False) ⟶ ((x7 x10 x67 = x67 ⟶ False) ⟶ False) ⟶ ((x7 x10 x9 = x9 ⟶ False) ⟶ False) ⟶ ((x7 x10 x73 = x73 ⟶ False) ⟶ False) ⟶ ((x7 x10 x10 = x10 ⟶ False) ⟶ False) ⟶ ((x78 (x74 (x69 x73) x67) (x74 (x69 x73) x67) ⟶ False) ⟶ False) ⟶ ((x78 (x74 (x69 x73) x67) (x74 x9 x67) ⟶ False) ⟶ False) ⟶ ((x78 (x74 (x69 x73) x67) (x74 x73 x67) ⟶ False) ⟶ False) ⟶ (x78 (x74 (x69 x73) x67) (x69 x73) ⟶ False) ⟶ ((x78 (x74 (x69 x73) x67) x67 ⟶ False) ⟶ False) ⟶ ((x78 (x74 (x69 x73) x67) x9 ⟶ False) ⟶ False) ⟶ ((x78 (x74 (x69 x73) x67) x73 ⟶ False) ⟶ False) ⟶ ((x78 (x74 (x69 x73) x67) x10 ⟶ False) ⟶ False) ⟶ ((x78 (x74 (x69 x73) x9) (x74 (x69 x73) x9) ⟶ False) ⟶ False) ⟶ ((x78 (x74 (x69 x73) x9) (x74 x67 x9) ⟶ False) ⟶ False) ⟶ ((x78 (x74 (x69 x73) x9) (x74 x73 x9) ⟶ False) ⟶ False) ⟶ (x78 (x74 (x69 x73) x9) (x69 x73) ⟶ False) ⟶ ((x78 (x74 (x69 x73) x9) x67 ⟶ False) ⟶ False) ⟶ ((x78 (x74 (x69 x73) x9) x9 ⟶ False) ⟶ False) ⟶ ((x78 (x74 (x69 x73) x9) x73 ⟶ False) ⟶ False) ⟶ ((x78 (x74 (x69 x73) x9) x10 ⟶ False) ⟶ False) ⟶ (x78 (x74 x67 x9) (x74 (x69 x73) x9) ⟶ False) ⟶ ((x78 (x74 x67 x9) (x74 x67 x9) ⟶ False) ⟶ False) ⟶ (x78 (x74 x67 x9) (x74 x73 x9) ⟶ False) ⟶ (x78 (x74 x67 x9) (x69 x73) ⟶ False) ⟶ ((x78 (x74 x67 x9) x67 ⟶ False) ⟶ False) ⟶ ((x78 (x74 x67 x9) x9 ⟶ False) ⟶ False) ⟶ (x78 (x74 x67 x9) x73 ⟶ False) ⟶ (x78 (x74 x67 x9) x10 ⟶ False) ⟶ (x78 (x74 x9 x67) (x74 (x69 x73) x67) ⟶ False) ⟶ ((x78 (x74 x9 x67) (x74 x9 x67) ⟶ False) ⟶ False) ⟶ (x78 (x74 x9 x67) (x74 x73 x67) ⟶ False) ⟶ (x78 (x74 x9 x67) (x74 x73 x9) ⟶ False) ⟶ (x78 (x74 x9 x67) (x69 x73) ⟶ False) ⟶ ((x78 (x74 x9 x67) x67 ⟶ False) ⟶ False) ⟶ ((x78 (x74 x9 x67) x9 ⟶ False) ⟶ False) ⟶ ((x78 (x74 x9 x67) x73 ⟶ False) ⟶ False) ⟶ (x78 (x74 x9 x67) x10 ⟶ False) ⟶ (x78 (x74 x73 x67) (x74 (x69 x73) x67) ⟶ False) ⟶ ((x78 (x74 x73 x67) (x74 x9 x67) ⟶ False) ⟶ False) ⟶ ((x78 (x74 x73 x67) (x74 x73 x67) ⟶ False) ⟶ False) ⟶ (x78 (x74 x73 x67) (x69 x73) ⟶ False) ⟶ ((x78 (x74 x73 x67) x67 ⟶ False) ⟶ False) ⟶ ((x78 (x74 x73 x67) x9 ⟶ False) ⟶ False) ⟶ ((x78 (x74 x73 x67) x73 ⟶ False) ⟶ False) ⟶ (x78 (x74 x73 x67) x10 ⟶ False) ⟶ (x78 (x74 x73 x9) (x74 (x69 x73) x9) ⟶ False) ⟶ ((x78 (x74 x73 x9) (x74 x67 x9) ⟶ False) ⟶ False) ⟶ ((x78 (x74 x73 x9) (x74 x9 x67) ⟶ False) ⟶ False) ⟶ ((x78 (x74 x73 x9) (x74 x73 x9) ⟶ False) ⟶ False) ⟶ (x78 (x74 x73 x9) (x69 x67) ⟶ False) ⟶ (x78 (x74 x73 x9) (x69 x9) ⟶ False) ⟶ (x78 (x74 x73 x9) (x69 x73) ⟶ False) ⟶ ((x78 (x74 x73 x9) x67 ⟶ False) ⟶ False) ⟶ ((x78 (x74 x73 x9) x9 ⟶ False) ⟶ False) ⟶ ((x78 (x74 x73 x9) x73 ⟶ False) ⟶ False) ⟶ (x78 (x74 x73 x9) x10 ⟶ False) ⟶ ((x78 (x69 x67) (x74 x73 x9) ⟶ False) ⟶ False) ⟶ ((x78 (x69 x67) (x69 x67) ⟶ False) ⟶ False) ⟶ ((x78 (x69 x67) (x69 x9) ⟶ False) ⟶ False) ⟶ ((x78 (x69 x67) (x69 x73) ⟶ False) ⟶ False) ⟶ ((x78 (x69 x67) x67 ⟶ False) ⟶ False) ⟶ ((x78 (x69 x67) x9 ⟶ False) ⟶ False) ⟶ ((x78 (x69 x67) x73 ⟶ False) ⟶ False) ⟶ ((x78 (x69 x67) x10 ⟶ False) ⟶ False) ⟶ ((x78 (x69 x9) (x74 x73 x9) ⟶ False) ⟶ False) ⟶ (x78 (x69 x9) (x69 x67) ⟶ False) ⟶ ((x78 (x69 x9) (x69 x9) ⟶ False) ⟶ False) ⟶ ((x78 (x69 x9) (x69 x73) ⟶ False) ⟶ False) ⟶ ((x78 (x69 x9) x67 ⟶ False) ⟶ False) ⟶ ((x78 (x69 x9) x9 ⟶ False) ⟶ False) ⟶ ((x78 (x69 x9) x73 ⟶ False) ⟶ False) ⟶ ((x78 (x69 x9) x10 ⟶ False) ⟶ False) ⟶ ((x78 (x69 x73) (x74 (x69 x73) x67) ⟶ False) ⟶ False) ⟶ ((x78 (x69 x73) (x74 (x69 x73) x9) ⟶ False) ⟶ False) ⟶ ((x78 (x69 x73) (x74 x67 x9) ⟶ False) ⟶ False) ⟶ ((x78 (x69 x73) (x74 x9 x67) ⟶ False) ⟶ False) ⟶ ((x78 (x69 x73) (x74 x73 x67) ⟶ False) ⟶ False) ⟶ ((x78 (x69 x73) (x74 x73 x9) ⟶ False) ⟶ False) ⟶ (x78 (x69 x73) (x69 x67) ⟶ False) ⟶ (x78 (x69 x73) (x69 x9) ⟶ False) ⟶ ((x78 (x69 x73) (x69 x73) ⟶ False) ⟶ False) ⟶ ((x78 (x69 x73) x67 ⟶ False) ⟶ False) ⟶ ((x78 (x69 x73) x9 ⟶ False) ⟶ False) ⟶ ((x78 (x69 x73) x73 ⟶ False) ⟶ False) ⟶ ((x78 (x69 x73) x10 ⟶ False) ⟶ False) ⟶ (x78 x67 (x74 (x69 x73) x67) ⟶ False) ⟶ (x78 x67 (x74 (x69 x73) x9) ⟶ False) ⟶ (x78 x67 (x74 x67 x9) ⟶ False) ⟶ (x78 x67 (x74 x9 x67) ⟶ False) ⟶ (x78 x67 (x74 x73 x67) ⟶ False) ⟶ (x78 x67 (x74 x73 x9) ⟶ False) ⟶ (x78 x67 (x69 x67) ⟶ False) ⟶ (x78 x67 (x69 x9) ⟶ False) ⟶ (x78 x67 (x69 x73) ⟶ False) ⟶ ((x78 x67 x67 ⟶ False) ⟶ False) ⟶ (x78 x67 x9 ⟶ False) ⟶ (x78 x67 x73 ⟶ False) ⟶ (x78 x67 x10 ⟶ False) ⟶ (x78 x9 (x74 (x69 x73) x67) ⟶ False) ⟶ (x78 x9 (x74 (x69 x73) x9) ⟶ False) ⟶ (x78 x9 (x74 x67 x9) ⟶ False) ⟶ (x78 x9 (x74 x9 x67) ⟶ False) ⟶ (x78 x9 (x74 x73 x67) ⟶ False) ⟶ (x78 x9 (x74 x73 x9) ⟶ False) ⟶ (x78 x9 (x69 x67) ⟶ False) ⟶ (x78 x9 (x69 x9) ⟶ False) ⟶ (x78 x9 (x69 x73) ⟶ False) ⟶ ((x78 x9 x67 ⟶ False) ⟶ False) ⟶ ((x78 x9 x9 ⟶ False) ⟶ False) ⟶ (x78 x9 x73 ⟶ False) ⟶ (x78 x9 x10 ⟶ False) ⟶ (x78 x73 (x74 (x69 x73) x67) ⟶ False) ⟶ (x78 x73 (x74 (x69 x73) x9) ⟶ False) ⟶ ((x78 x73 (x74 x67 x9) ⟶ False) ⟶ False) ⟶ (x78 x73 (x74 x9 x67) ⟶ False) ⟶ (x78 x73 (x74 x73 x67) ⟶ False) ⟶ (x78 x73 (x74 x73 x9) ⟶ False) ⟶ (x78 x73 (x69 x67) ⟶ False) ⟶ (x78 x73 (x69 x9) ⟶ False) ⟶ (x78 x73 (x69 x73) ⟶ False) ⟶ ((x78 x73 x67 ⟶ False) ⟶ False) ⟶ ((x78 x73 x9 ⟶ False) ⟶ False) ⟶ ((x78 x73 x73 ⟶ False) ⟶ False) ⟶ (x78 x73 x10 ⟶ False) ⟶ (x78 x10 (x74 (x69 x73) x67) ⟶ False) ⟶ (x78 x10 (x74 (x69 x73) x9) ⟶ False) ⟶ ((x78 x10 (x74 x67 x9) ⟶ False) ⟶ False) ⟶ ((x78 x10 (x74 x9 x67) ⟶ False) ⟶ False) ⟶ ((x78 x10 (x74 x73 x67) ⟶ False) ⟶ False) ⟶ ((x78 x10 (x74 x73 x9) ⟶ False) ⟶ False) ⟶ (x78 x10 (x69 x67) ⟶ False) ⟶ (x78 x10 (x69 x9) ⟶ False) ⟶ (x78 x10 (x69 x73) ⟶ False) ⟶ ((x78 x10 x67 ⟶ False) ⟶ False) ⟶ ((x78 x10 x9 ⟶ False) ⟶ False) ⟶ ((x78 x10 x73 ⟶ False) ⟶ False) ⟶ ((x78 x10 x10 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x65 x81 ⟶ x65 x80 ⟶ (x78 x81 x81 ⟶ False) ⟶ False) ⟶ (∀ x80 . (x6 x80 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 . (x0 x82 ⟶ False) ⟶ (x0 x80 ⟶ False) ⟶ x4 x80 (x3 x82) ⟶ x4 x81 x80 ⟶ (x66 x81 x82 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 . (x0 x82 ⟶ False) ⟶ (x0 x80 ⟶ False) ⟶ x4 x80 (x3 x82) ⟶ x66 x81 x82 x80 ⟶ (x4 x81 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x4 x81 x68 ⟶ x79 x80 ⟶ (x64 x81 x80 = x71 x81 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x4 x81 x68 ⟶ x79 x80 ⟶ (x11 x81 x80 = x7 x81 x80 ⟶ False) ⟶ False) ⟶ ((x5 = x2 ⟶ False) ⟶ False) ⟶ ((x8 = x70 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 x83 x84 . x63 x84 ⟶ x4 x84 (x3 (x62 (x62 x81 x80) x68)) ⟶ x4 x83 x81 ⟶ x4 x82 x80 ⟶ (x60 x81 x80 x84 x83 x82 = x61 x84 x83 x82 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x4 x81 x68 ⟶ x79 x80 ⟶ (x12 x81 x80 = x74 x81 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . (x59 (x58 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 . (x13 (x58 x80) x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . (x63 (x58 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 . (x14 (x58 x80) x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . (x57 (x58 x80) ⟶ False) ⟶ False) ⟶ ((x15 x16 ⟶ False) ⟶ False) ⟶ (x0 x16 ⟶ False) ⟶ ((x65 x17 ⟶ False) ⟶ False) ⟶ ((x0 x17 ⟶ False) ⟶ False) ⟶ ((x79 x18 ⟶ False) ⟶ False) ⟶ ((x65 x18 ⟶ False) ⟶ False) ⟶ ((x75 x18 ⟶ False) ⟶ False) ⟶ ((x0 x18 ⟶ False) ⟶ False) ⟶ ((x15 x19 ⟶ False) ⟶ False) ⟶ ((x77 x56 ⟶ False) ⟶ False) ⟶ ((x65 x56 ⟶ False) ⟶ False) ⟶ ((x79 x55 ⟶ False) ⟶ False) ⟶ ((x77 x55 ⟶ False) ⟶ False) ⟶ ((x65 x55 ⟶ False) ⟶ False) ⟶ ((x75 x55 ⟶ False) ⟶ False) ⟶ (∀ x80 . (x54 (x53 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 . (x63 (x53 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 . (x52 (x53 x80) x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . (x57 (x53 x80) ⟶ False) ⟶ False) ⟶ ((x76 x51 ⟶ False) ⟶ False) ⟶ ((x65 x51 ⟶ False) ⟶ False) ⟶ ((x79 x50 ⟶ False) ⟶ False) ⟶ ((x76 x50 ⟶ False) ⟶ False) ⟶ ((x65 x50 ⟶ False) ⟶ False) ⟶ ((x75 x50 ⟶ False) ⟶ False) ⟶ (x0 x49 ⟶ False) ⟶ ((x20 x21 ⟶ False) ⟶ False) ⟶ ((x48 x21 ⟶ False) ⟶ False) ⟶ ((x22 x21 ⟶ False) ⟶ False) ⟶ (x0 x21 ⟶ False) ⟶ ((x65 x23 ⟶ False) ⟶ False) ⟶ ((x79 x47 ⟶ False) ⟶ False) ⟶ ((x0 x24 ⟶ False) ⟶ False) ⟶ ((x59 x46 ⟶ False) ⟶ False) ⟶ ((x63 x46 ⟶ False) ⟶ False) ⟶ ((x57 x46 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . (x52 (x25 x80 x81) x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . (x14 (x25 x81 x80) x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . (x57 (x25 x80 x81) ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . (x0 (x25 x80 x81) ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . (x4 (x25 x80 x81) (x3 (x62 x81 x80)) ⟶ False) ⟶ False) ⟶ ((x20 x45 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . (x26 (x27 x80 x81) x81 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . (x63 (x27 x80 x81) ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . (x52 (x27 x80 x81) x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . (x14 (x27 x81 x80) x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . (x57 (x27 x80 x81) ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . (x4 (x27 x80 x81) (x3 (x62 x81 x80)) ⟶ False) ⟶ False) ⟶ (∀ x80 . x75 x80 ⟶ (x69 (x69 x80) = x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . (x77 x81 ⟶ False) ⟶ x79 x81 ⟶ (x77 x80 ⟶ False) ⟶ x79 x80 ⟶ x77 (x7 x81 x80) ⟶ False) ⟶ (∀ x80 x81 . x79 x81 ⟶ x79 x80 ⟶ (x79 (x74 x81 x80) ⟶ False) ⟶ False) ⟶ (x44 x68 ⟶ False) ⟶ (∀ x80 x81 . x79 x81 ⟶ x79 x80 ⟶ (x79 (x72 x81 x80) ⟶ False) ⟶ False) ⟶ (x44 x43 ⟶ False) ⟶ (∀ x80 x81 . x79 x81 ⟶ x79 x80 ⟶ (x79 (x71 x81 x80) ⟶ False) ⟶ False) ⟶ ((x20 x70 ⟶ False) ⟶ False) ⟶ (x0 x70 ⟶ False) ⟶ (x44 x42 ⟶ False) ⟶ (∀ x80 x81 . x79 x81 ⟶ x79 x80 ⟶ (x79 (x7 x81 x80) ⟶ False) ⟶ False) ⟶ (x0 x42 ⟶ False) ⟶ (∀ x80 . x79 x80 ⟶ (x79 (x69 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 . x79 x80 ⟶ (x75 (x69 x80) ⟶ False) ⟶ False) ⟶ (x0 x43 ⟶ False) ⟶ (∀ x80 x81 . (x76 x81 ⟶ False) ⟶ x79 x81 ⟶ (x76 x80 ⟶ False) ⟶ x79 x80 ⟶ x77 (x74 x81 x80) ⟶ False) ⟶ (∀ x80 x81 . (x77 x81 ⟶ False) ⟶ x79 x81 ⟶ (x77 x80 ⟶ False) ⟶ x79 x80 ⟶ x77 (x74 x81 x80) ⟶ False) ⟶ (∀ x80 x81 . (x77 x81 ⟶ False) ⟶ x79 x81 ⟶ (x76 x80 ⟶ False) ⟶ x79 x80 ⟶ x76 (x74 x80 x81) ⟶ False) ⟶ (∀ x80 x81 . (x77 x81 ⟶ False) ⟶ x79 x81 ⟶ (x76 x80 ⟶ False) ⟶ x79 x80 ⟶ x76 (x74 x81 x80) ⟶ False) ⟶ (∀ x80 x81 x82 . x57 x82 ⟶ x63 x82 ⟶ x59 x82 ⟶ (x15 (x61 x82 x80 x81) ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . (x77 x81 ⟶ False) ⟶ x79 x81 ⟶ (x77 x80 ⟶ False) ⟶ x79 x80 ⟶ x77 (x71 x81 x80) ⟶ False) ⟶ (∀ x80 x81 . (x76 x81 ⟶ False) ⟶ x79 x81 ⟶ (x76 x80 ⟶ False) ⟶ x79 x80 ⟶ x77 (x71 x81 x80) ⟶ False) ⟶ (∀ x80 x81 . (x76 x81 ⟶ False) ⟶ x79 x81 ⟶ (x77 x80 ⟶ False) ⟶ x79 x80 ⟶ x76 (x71 x80 x81) ⟶ False) ⟶ (∀ x80 x81 . (x76 x81 ⟶ False) ⟶ x79 x81 ⟶ (x77 x80 ⟶ False) ⟶ x79 x80 ⟶ x76 (x71 x81 x80) ⟶ False) ⟶ (∀ x80 x81 . x77 x81 ⟶ x79 x81 ⟶ (x77 x80 ⟶ False) ⟶ x79 x80 ⟶ (x76 (x72 x80 x81) ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x77 x81 ⟶ x79 x81 ⟶ (x77 x80 ⟶ False) ⟶ x79 x80 ⟶ (x77 (x72 x81 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x76 x81 ⟶ x79 x81 ⟶ (x76 x80 ⟶ False) ⟶ x79 x80 ⟶ (x77 (x72 x80 x81) ⟶ False) ⟶ False) ⟶ ((x0 x2 ⟶ False) ⟶ False) ⟶ (x0 x68 ⟶ False) ⟶ (∀ x80 x81 . x76 x81 ⟶ x79 x81 ⟶ (x76 x80 ⟶ False) ⟶ x79 x80 ⟶ (x76 (x72 x81 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . (x77 x81 ⟶ False) ⟶ x79 x81 ⟶ (x76 x80 ⟶ False) ⟶ x79 x80 ⟶ x76 (x72 x80 x81) ⟶ False) ⟶ (∀ x80 x81 . (x77 x81 ⟶ False) ⟶ x79 x81 ⟶ (x76 x80 ⟶ False) ⟶ x79 x80 ⟶ x77 (x72 x81 x80) ⟶ False) ⟶ (∀ x80 . (x77 x80 ⟶ False) ⟶ x79 x80 ⟶ x76 (x69 x80) ⟶ False) ⟶ (∀ x80 . (x77 x80 ⟶ False) ⟶ x79 x80 ⟶ (x75 (x69 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 . (x76 x80 ⟶ False) ⟶ x79 x80 ⟶ x77 (x69 x80) ⟶ False) ⟶ (∀ x80 . (x76 x80 ⟶ False) ⟶ x79 x80 ⟶ (x75 (x69 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x77 x81 ⟶ x79 x81 ⟶ (x76 x80 ⟶ False) ⟶ x79 x80 ⟶ (x77 (x7 x80 x81) ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x77 x81 ⟶ x79 x81 ⟶ (x76 x80 ⟶ False) ⟶ x79 x80 ⟶ (x77 (x7 x81 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x76 x81 ⟶ x79 x81 ⟶ (x77 x80 ⟶ False) ⟶ x79 x80 ⟶ (x76 (x7 x80 x81) ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x76 x81 ⟶ x79 x81 ⟶ (x77 x80 ⟶ False) ⟶ x79 x80 ⟶ (x76 (x7 x81 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . (x76 x81 ⟶ False) ⟶ x79 x81 ⟶ (x76 x80 ⟶ False) ⟶ x79 x80 ⟶ x76 (x7 x81 x80) ⟶ False) ⟶ (∀ x80 x81 . (x0 x81 ⟶ False) ⟶ (x0 x80 ⟶ False) ⟶ x4 x80 (x3 x81) ⟶ (x66 (x41 x80 x81) x81 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . (x4 (x28 x80) x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 . (x0 x82 ⟶ False) ⟶ (x0 x80 ⟶ False) ⟶ x4 x80 (x3 x82) ⟶ x66 x81 x82 x80 ⟶ (x4 x81 x82 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x4 x81 x68 ⟶ x79 x80 ⟶ (x4 (x64 x81 x80) x68 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x4 x81 x68 ⟶ x79 x80 ⟶ (x4 (x11 x81 x80) x68 ⟶ False) ⟶ False) ⟶ ((x66 x5 x68 x8 ⟶ False) ⟶ False) ⟶ ((x4 x8 (x3 x68) ⟶ False) ⟶ False) ⟶ (∀ x80 . x75 x80 ⟶ (x75 (x69 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 x83 x84 . x63 x84 ⟶ x4 x84 (x3 (x62 (x62 x81 x80) x68)) ⟶ x4 x83 x81 ⟶ x4 x82 x80 ⟶ (x4 (x60 x81 x80 x84 x83 x82) x68 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x4 x81 x68 ⟶ x79 x80 ⟶ (x4 (x12 x81 x80) x68 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x63 x81 ⟶ x26 x81 (x62 x80 x80) x68 ⟶ x4 x81 (x3 (x62 (x62 x80 x80) x68)) ⟶ x38 x81 x80 = x37 x81 x80 ⟶ x60 x80 x80 x81 (x38 x81 x80) (x37 x81 x80) = x5 ⟶ x60 x80 x80 x81 (x38 x81 x80) (x37 x81 x80) = x60 x80 x80 x81 (x37 x81 x80) (x38 x81 x80) ⟶ x78 (x60 x80 x80 x81 (x38 x81 x80) (x39 x81 x80)) (x11 (x60 x80 x80 x81 (x38 x81 x80) (x37 x81 x80)) (x60 x80 x80 x81 (x37 x81 x80) (x39 x81 x80))) ⟶ (x40 x80 x81 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x63 x81 ⟶ x26 x81 (x62 x80 x80) x68 ⟶ x4 x81 (x3 (x62 (x62 x80 x80) x68)) ⟶ x38 x81 x80 = x37 x81 x80 ⟶ (x38 x81 x80 = x37 x81 x80 ⟶ False) ⟶ x60 x80 x80 x81 (x38 x81 x80) (x37 x81 x80) = x60 x80 x80 x81 (x37 x81 x80) (x38 x81 x80) ⟶ x78 (x60 x80 x80 x81 (x38 x81 x80) (x39 x81 x80)) (x11 (x60 x80 x80 x81 (x38 x81 x80) (x37 x81 x80)) (x60 x80 x80 x81 (x37 x81 x80) (x39 x81 x80))) ⟶ (x40 x80 x81 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x63 x81 ⟶ x26 x81 (x62 x80 x80) x68 ⟶ x4 x81 (x3 (x62 (x62 x80 x80) x68)) ⟶ (x60 x80 x80 x81 (x38 x81 x80) (x37 x81 x80) = x5 ⟶ False) ⟶ x60 x80 x80 x81 (x38 x81 x80) (x37 x81 x80) = x5 ⟶ x60 x80 x80 x81 (x38 x81 x80) (x37 x81 x80) = x60 x80 x80 x81 (x37 x81 x80) (x38 x81 x80) ⟶ x78 (x60 x80 x80 x81 (x38 x81 x80) (x39 x81 x80)) (x11 (x60 x80 x80 x81 (x38 x81 x80) (x37 x81 x80)) (x60 x80 x80 x81 (x37 x81 x80) (x39 x81 x80))) ⟶ (x40 x80 x81 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x63 x81 ⟶ x26 x81 (x62 x80 x80) x68 ⟶ x4 x81 (x3 (x62 (x62 x80 x80) x68)) ⟶ (x60 x80 x80 x81 (x38 x81 x80) (x37 x81 x80) = x5 ⟶ False) ⟶ (x38 x81 x80 = x37 x81 x80 ⟶ False) ⟶ x60 x80 x80 x81 (x38 x81 x80) (x37 x81 x80) = x60 x80 x80 x81 (x37 x81 x80) (x38 x81 x80) ⟶ x78 (x60 x80 x80 x81 (x38 x81 x80) (x39 x81 x80)) (x11 (x60 x80 x80 x81 (x38 x81 x80) (x37 x81 x80)) (x60 x80 x80 x81 (x37 x81 x80) (x39 x81 x80))) ⟶ (x40 x80 x81 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x63 x81 ⟶ x26 x81 (x62 x80 x80) x68 ⟶ x4 x81 (x3 (x62 (x62 x80 x80) x68)) ⟶ (x4 (x39 x81 x80) x80 ⟶ False) ⟶ (x40 x80 x81 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x63 x81 ⟶ x26 x81 (x62 x80 x80) x68 ⟶ x4 x81 (x3 (x62 (x62 x80 x80) x68)) ⟶ (x4 (x37 x81 x80) x80 ⟶ False) ⟶ (x40 x80 x81 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x63 x81 ⟶ x26 x81 (x62 x80 x80) x68 ⟶ x4 x81 (x3 (x62 (x62 x80 x80) x68)) ⟶ (x4 (x38 x81 x80) x80 ⟶ False) ⟶ (x40 x80 x81 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 x83 x84 . x63 x84 ⟶ x26 x84 (x62 x80 x80) x68 ⟶ x4 x84 (x3 (x62 (x62 x80 x80) x68)) ⟶ x40 x80 x84 ⟶ x4 x83 x80 ⟶ x4 x81 x80 ⟶ x4 x82 x80 ⟶ (x78 (x60 x80 x80 x84 x83 x82) (x11 (x60 x80 x80 x84 x83 x81) (x60 x80 x80 x84 x81 x82)) ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 x83 x84 . x63 x84 ⟶ x26 x84 (x62 x80 x80) x68 ⟶ x4 x84 (x3 (x62 (x62 x80 x80) x68)) ⟶ x40 x80 x84 ⟶ x4 x83 x80 ⟶ x4 x81 x80 ⟶ x4 x82 x80 ⟶ (x60 x80 x80 x84 x83 x81 = x60 x80 x80 x84 x81 x83 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 x83 x84 . x63 x84 ⟶ x26 x84 (x62 x80 x80) x68 ⟶ x4 x84 (x3 (x62 (x62 x80 x80) x68)) ⟶ x40 x80 x84 ⟶ x4 x83 x80 ⟶ x4 x81 x80 ⟶ x4 x82 x80 ⟶ x83 = x81 ⟶ (x60 x80 x80 x84 x83 x81 = x5 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 x83 x84 . x63 x84 ⟶ x26 x84 (x62 x80 x80) x68 ⟶ x4 x84 (x3 (x62 (x62 x80 x80) x68)) ⟶ x40 x80 x84 ⟶ x4 x83 x80 ⟶ x4 x81 x80 ⟶ x4 x82 x80 ⟶ x60 x80 x80 x84 x83 x81 = x5 ⟶ (x83 = x81 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x65 x81 ⟶ x65 x80 ⟶ (x78 x81 x80 ⟶ False) ⟶ (x78 x80 x81 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x4 x81 x68 ⟶ x79 x80 ⟶ (x64 x81 x80 = x64 x80 x81 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x4 x81 x68 ⟶ x79 x80 ⟶ (x11 x81 x80 = x11 x80 x81 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x75 x81 ⟶ x75 x80 ⟶ (x71 x81 x80 = x71 x80 x81 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x75 x81 ⟶ x75 x80 ⟶ (x7 x81 x80 = x7 x80 x81 ⟶ False) ⟶ False) ⟶ (∀ x80 . x0 x80 ⟶ x57 x80 ⟶ (x59 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x0 x80 ⟶ x57 x80 ⟶ (x57 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x0 x80 ⟶ (x36 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x65 x80 ⟶ (x76 x80 ⟶ False) ⟶ (x77 x80 ⟶ False) ⟶ (x65 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x65 x80 ⟶ (x76 x80 ⟶ False) ⟶ (x77 x80 ⟶ False) ⟶ (x0 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x57 x80 ⟶ x59 x80 ⟶ (x29 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x57 x80 ⟶ x59 x80 ⟶ (x57 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x4 x80 x70 ⟶ (x15 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 . (x0 x82 ⟶ False) ⟶ (x0 x80 ⟶ False) ⟶ x4 x81 (x3 (x62 x82 x80)) ⟶ x63 x81 ⟶ x26 x81 x82 x80 ⟶ (x26 x81 x82 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 . (x0 x82 ⟶ False) ⟶ (x0 x80 ⟶ False) ⟶ x4 x81 (x3 (x62 x82 x80)) ⟶ x63 x81 ⟶ x26 x81 x82 x80 ⟶ x0 x81 ⟶ False) ⟶ (∀ x80 x81 x82 . (x0 x82 ⟶ False) ⟶ (x0 x80 ⟶ False) ⟶ x4 x81 (x3 (x62 x82 x80)) ⟶ x63 x81 ⟶ x26 x81 x82 x80 ⟶ (x63 x81 ⟶ False) ⟶ False) ⟶ (∀ x80 . x0 x80 ⟶ x65 x80 ⟶ x77 x80 ⟶ False) ⟶ (∀ x80 . x0 x80 ⟶ x65 x80 ⟶ x76 x80 ⟶ False) ⟶ (∀ x80 . x0 x80 ⟶ x65 x80 ⟶ (x65 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x57 x80 ⟶ x59 x80 ⟶ (x52 x80 x43 ⟶ False) ⟶ False) ⟶ (∀ x80 . x57 x80 ⟶ x59 x80 ⟶ (x57 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x0 x80 ⟶ (x15 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . (x0 x80 ⟶ False) ⟶ x65 x80 ⟶ (x76 x80 ⟶ False) ⟶ (x77 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . (x0 x80 ⟶ False) ⟶ x65 x80 ⟶ (x76 x80 ⟶ False) ⟶ (x65 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x57 x80 ⟶ x29 x80 ⟶ (x30 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x57 x80 ⟶ x29 x80 ⟶ (x57 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x15 x80 ⟶ (x20 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x65 x80 ⟶ x77 x80 ⟶ x76 x80 ⟶ False) ⟶ (∀ x80 . x65 x80 ⟶ x77 x80 ⟶ (x65 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x65 x80 ⟶ x77 x80 ⟶ x0 x80 ⟶ False) ⟶ (∀ x80 . x57 x80 ⟶ x29 x80 ⟶ (x31 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x57 x80 ⟶ x29 x80 ⟶ (x57 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x20 x81 ⟶ x4 x80 x81 ⟶ (x20 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . (x0 x80 ⟶ False) ⟶ x65 x80 ⟶ (x77 x80 ⟶ False) ⟶ (x76 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . (x0 x80 ⟶ False) ⟶ x65 x80 ⟶ (x77 x80 ⟶ False) ⟶ (x65 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x79 x80 ⟶ (x65 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x57 x80 ⟶ x52 x80 x43 ⟶ (x29 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x57 x80 ⟶ x52 x80 x43 ⟶ (x57 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 . x0 x82 ⟶ x4 x80 (x3 (x62 x81 x82)) ⟶ (x0 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x0 x80 ⟶ (x54 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x4 x81 (x3 (x62 x80 x80)) ⟶ x26 x81 x80 x80 ⟶ (x13 x81 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x65 x80 ⟶ x76 x80 ⟶ x77 x80 ⟶ False) ⟶ (∀ x80 . x65 x80 ⟶ x76 x80 ⟶ (x65 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x65 x80 ⟶ x76 x80 ⟶ x0 x80 ⟶ False) ⟶ (∀ x80 . x79 x80 ⟶ (x75 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x57 x80 ⟶ x52 x80 x42 ⟶ (x29 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x57 x80 ⟶ x52 x80 x42 ⟶ (x57 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 . x0 x82 ⟶ x4 x80 (x3 (x62 x82 x81)) ⟶ (x0 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x0 x80 ⟶ (x20 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 . (x0 x82 ⟶ False) ⟶ x4 x80 (x3 (x62 x81 x82)) ⟶ x26 x80 x81 x82 ⟶ (x13 x80 x81 ⟶ False) ⟶ False) ⟶ (∀ x80 . x57 x80 ⟶ x52 x80 x8 ⟶ (x59 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x57 x80 ⟶ x52 x80 x8 ⟶ (x57 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x57 x80 ⟶ x52 x80 x68 ⟶ (x29 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x57 x80 ⟶ x52 x80 x68 ⟶ (x57 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x15 x80 ⟶ (x65 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x15 x80 ⟶ (x79 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x57 x80 ⟶ x52 x80 x42 ⟶ (x52 x80 x43 ⟶ False) ⟶ False) ⟶ (∀ x80 . x57 x80 ⟶ x52 x80 x42 ⟶ (x57 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 . x4 x82 (x3 (x62 x80 x81)) ⟶ (x52 x82 x81 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 . x4 x82 (x3 (x62 x81 x80)) ⟶ (x14 x82 x81 ⟶ False) ⟶ False) ⟶ (∀ x80 . x22 x80 ⟶ x48 x80 ⟶ (x20 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 . x0 x82 ⟶ x4 x80 (x3 (x62 x82 x81)) ⟶ x26 x80 x82 x81 ⟶ (x13 x80 x82 ⟶ False) ⟶ False) ⟶ (∀ x80 . x4 x80 x68 ⟶ (x79 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x57 x80 ⟶ x59 x80 ⟶ (x52 x80 x42 ⟶ False) ⟶ False) ⟶ (∀ x80 . x57 x80 ⟶ x59 x80 ⟶ (x57 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 . x4 x82 (x3 (x62 x80 x81)) ⟶ (x57 x82 ⟶ False) ⟶ False) ⟶ (∀ x80 . x20 x80 ⟶ (x48 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x20 x80 ⟶ (x22 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 . x4 x81 (x3 (x62 x82 x80)) ⟶ x13 x81 x82 ⟶ (x26 x81 x82 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x57 x81 ⟶ x59 x81 ⟶ x4 x80 (x3 x81) ⟶ (x59 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x57 x81 ⟶ x52 x81 x42 ⟶ x4 x80 (x3 x81) ⟶ (x52 x80 x42 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x57 x81 ⟶ x52 x81 x43 ⟶ x4 x80 (x3 x81) ⟶ (x52 x80 x43 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x57 x81 ⟶ x29 x81 ⟶ x4 x80 (x3 x81) ⟶ (x29 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x57 x81 ⟶ x31 x81 ⟶ x4 x80 (x3 x81) ⟶ (x31 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x57 x81 ⟶ x30 x81 ⟶ x4 x80 (x3 x81) ⟶ (x30 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x36 x81 ⟶ x4 x80 (x3 x81) ⟶ (x36 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x1 x80 x81 ⟶ x1 x81 x80 ⟶ False) ⟶ (x78 x5 (x60 x32 x32 x33 x34 x35) ⟶ False) ⟶ ((x4 x35 x32 ⟶ False) ⟶ False) ⟶ ((x4 x34 x32 ⟶ False) ⟶ False) ⟶ ((x40 x32 x33 ⟶ False) ⟶ False) ⟶ ((x4 x33 (x3 (x62 (x62 x32 x32) x68)) ⟶ False) ⟶ False) ⟶ ((x26 x33 (x62 x32 x32) x68 ⟶ False) ⟶ False) ⟶ ((x63 x33 ⟶ False) ⟶ False) ⟶ (x0 x32 ⟶ False) ⟶ False (proof)