Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrNUD../5329e..
PUNgr../30f61..
vout
PrNUD../bd01f.. 0.00 bars
TMGxU../7479a.. ownership of bec91.. as prop with payaddr PrPhD.. rights free controlledby PrPhD.. upto 0
TMTGQ../3f301.. ownership of 82672.. as prop with payaddr PrPhD.. rights free controlledby PrPhD.. upto 0
PUZRD../85c63.. doc published by PrPhD..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0 ⟶ False
Theorem bec91.. : ∀ 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 . x70 x72 ⟶ x70 x71 ⟶ (x66 (x65 x72 x71) = x67 (x68 (x69 x72) (x66 x71)) (x68 (x69 x71) (x66 x72)) ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x70 x72 ⟶ x70 x71 ⟶ (x69 (x65 x72 x71) = x0 (x68 (x69 x72) (x69 x71)) (x68 (x66 x72) (x66 x71)) ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x64 x72 ⟶ (x72 = x71 ⟶ False) ⟶ x64 x71 ⟶ False) ⟶ ((x66 x1 = x2 ⟶ False) ⟶ False) ⟶ ((x69 x1 = x63 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x3 x71 x72 ⟶ x64 x72 ⟶ False) ⟶ (∀ x71 . x64 x71 ⟶ (x71 = x62 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 x73 . x3 x71 x72 ⟶ x5 x72 (x4 x73) ⟶ x64 x73 ⟶ False) ⟶ (∀ x71 x72 x73 . x3 x72 x73 ⟶ x5 x73 (x4 x71) ⟶ (x5 x72 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x70 x71 ⟶ (x6 x71 x63 = x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x61 x72 x71 ⟶ (x5 x72 (x4 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x5 x72 (x4 x71) ⟶ (x61 x72 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x70 x71 ⟶ (x65 x2 x71 = x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x5 x71 x72 ⟶ (x64 x72 ⟶ False) ⟶ (x3 x71 x72 ⟶ False) ⟶ False) ⟶ (∀ x71 . x70 x71 ⟶ (x65 x71 x63 = x63 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x3 x72 x71 ⟶ (x5 x72 x71 ⟶ False) ⟶ False) ⟶ ((x5 x62 x60 ⟶ False) ⟶ False) ⟶ (∀ x71 . x70 x71 ⟶ (x7 x71 x63 = x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x70 x72 ⟶ x70 x71 ⟶ (x6 (x59 x72) (x59 x71) = x6 x71 x72 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x70 x72 ⟶ x70 x71 ⟶ (x7 (x59 x72) (x59 x71) = x59 (x7 x72 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 x72 x73 . x70 x73 ⟶ x70 x71 ⟶ x70 x72 ⟶ (x65 (x65 x73 x71) x72 = x65 x73 (x65 x71 x72) ⟶ False) ⟶ False) ⟶ (∀ x71 x72 x73 . x70 x73 ⟶ x70 x71 ⟶ x70 x72 ⟶ (x7 (x7 x73 x71) x72 = x7 x73 (x7 x71 x72) ⟶ False) ⟶ False) ⟶ (∀ x71 x72 x73 . x70 x73 ⟶ x70 x71 ⟶ x70 x72 ⟶ (x65 (x7 x73 x71) x72 = x7 (x65 x73 x72) (x65 x71 x72) ⟶ False) ⟶ False) ⟶ ((x5 x9 x8 ⟶ False) ⟶ False) ⟶ ((x5 x9 x58 ⟶ False) ⟶ False) ⟶ ((x10 x9 x8 x58 ⟶ False) ⟶ False) ⟶ ((x57 x9 ⟶ False) ⟶ False) ⟶ (x64 x9 ⟶ False) ⟶ (∀ x71 . x70 x71 ⟶ (x65 x71 (x59 x2) = x59 x71 ⟶ False) ⟶ False) ⟶ ((x5 x2 x8 ⟶ False) ⟶ False) ⟶ ((x5 x2 x58 ⟶ False) ⟶ False) ⟶ ((x10 x2 x8 x58 ⟶ False) ⟶ False) ⟶ ((x57 x2 ⟶ False) ⟶ False) ⟶ (x64 x2 ⟶ False) ⟶ (∀ x71 x72 . x70 x72 ⟶ x70 x71 ⟶ (x7 x72 (x59 x71) = x6 x72 x71 ⟶ False) ⟶ False) ⟶ ((x5 x11 x8 ⟶ False) ⟶ False) ⟶ ((x5 x11 x58 ⟶ False) ⟶ False) ⟶ ((x10 x11 x8 x58 ⟶ False) ⟶ False) ⟶ ((x64 x11 ⟶ False) ⟶ False) ⟶ ((x59 (x59 x9) = x9 ⟶ False) ⟶ False) ⟶ ((x59 (x59 x2) = x2 ⟶ False) ⟶ False) ⟶ ((x59 x9 = x59 x9 ⟶ False) ⟶ False) ⟶ ((x59 x2 = x59 x2 ⟶ False) ⟶ False) ⟶ ((x59 x11 = x11 ⟶ False) ⟶ False) ⟶ ((x59 (x7 (x65 (x59 x9) x56) (x59 x9)) = x7 (x65 x9 x56) x9 ⟶ False) ⟶ False) ⟶ ((x59 (x7 (x65 (x59 x9) x56) (x59 x2)) = x7 (x65 x9 x56) x2 ⟶ False) ⟶ False) ⟶ ((x59 (x7 (x65 (x59 x9) x56) x9) = x7 (x65 x9 x56) (x59 x9) ⟶ False) ⟶ False) ⟶ ((x59 (x7 (x65 (x59 x9) x56) x2) = x7 (x65 x9 x56) (x59 x2) ⟶ False) ⟶ False) ⟶ ((x59 (x65 (x59 x9) x56) = x65 x9 x56 ⟶ False) ⟶ False) ⟶ ((x59 (x7 (x65 (x59 x2) x56) (x59 x2)) = x7 x56 x2 ⟶ False) ⟶ False) ⟶ ((x59 (x7 (x65 (x59 x2) x56) x2) = x7 x56 (x59 x2) ⟶ False) ⟶ False) ⟶ ((x59 (x65 (x59 x2) x56) = x56 ⟶ False) ⟶ False) ⟶ ((x59 (x7 (x65 x9 x56) (x59 x9)) = x7 (x65 (x59 x9) x56) x9 ⟶ False) ⟶ False) ⟶ ((x59 (x7 (x65 x9 x56) x9) = x7 (x65 (x59 x9) x56) (x59 x9) ⟶ False) ⟶ False) ⟶ ((x59 (x7 (x65 x9 x56) x2) = x7 (x65 (x59 x9) x56) (x59 x2) ⟶ False) ⟶ False) ⟶ ((x59 (x65 x9 x56) = x65 (x59 x9) x56 ⟶ False) ⟶ False) ⟶ ((x59 (x7 x56 (x59 x2)) = x7 (x65 (x59 x2) x56) x2 ⟶ False) ⟶ False) ⟶ ((x59 (x7 x56 x2) = x7 (x65 (x59 x2) x56) (x59 x2) ⟶ False) ⟶ False) ⟶ ((x59 x56 = x65 (x59 x2) x56 ⟶ False) ⟶ False) ⟶ ((x65 (x59 x9) x2 = x59 x9 ⟶ False) ⟶ False) ⟶ ((x65 (x59 x9) x11 = x11 ⟶ False) ⟶ False) ⟶ ((x65 (x59 x9) (x65 (x59 x2) x56) = x65 x9 x56 ⟶ False) ⟶ False) ⟶ ((x65 (x59 x9) x56 = x65 (x59 x9) x56 ⟶ False) ⟶ False) ⟶ ((x65 x9 x2 = x9 ⟶ False) ⟶ False) ⟶ ((x65 x9 x11 = x11 ⟶ False) ⟶ False) ⟶ ((x65 x9 (x65 (x59 x2) x56) = x65 (x59 x9) x56 ⟶ False) ⟶ False) ⟶ ((x65 x9 x56 = x65 x9 x56 ⟶ False) ⟶ False) ⟶ ((x65 x2 (x59 x9) = x59 x9 ⟶ False) ⟶ False) ⟶ ((x65 x2 x9 = x9 ⟶ False) ⟶ False) ⟶ ((x65 x2 x2 = x2 ⟶ False) ⟶ False) ⟶ ((x65 x2 x11 = x11 ⟶ False) ⟶ False) ⟶ ((x65 x2 (x7 (x65 (x59 x2) x56) x2) = x7 (x65 (x59 x2) x56) x2 ⟶ False) ⟶ False) ⟶ ((x65 x2 (x65 (x59 x2) x56) = x65 (x59 x2) x56 ⟶ False) ⟶ False) ⟶ ((x65 x2 (x65 x9 x56) = x65 x9 x56 ⟶ False) ⟶ False) ⟶ ((x65 x2 x56 = x56 ⟶ False) ⟶ False) ⟶ ((x65 x11 (x59 x9) = x11 ⟶ False) ⟶ False) ⟶ ((x65 x11 x9 = x11 ⟶ False) ⟶ False) ⟶ ((x65 x11 x2 = x11 ⟶ False) ⟶ False) ⟶ ((x65 x11 x11 = x11 ⟶ False) ⟶ False) ⟶ ((x65 x11 x56 = x11 ⟶ False) ⟶ False) ⟶ ((x65 (x65 (x59 x9) x56) x2 = x65 (x59 x9) x56 ⟶ False) ⟶ False) ⟶ ((x65 (x65 (x59 x9) x56) (x65 (x59 x2) x56) = x59 x9 ⟶ False) ⟶ False) ⟶ ((x65 (x65 (x59 x9) x56) x56 = x9 ⟶ False) ⟶ False) ⟶ ((x65 (x7 (x65 (x59 x2) x56) (x59 x2)) x2 = x7 (x65 (x59 x2) x56) (x59 x2) ⟶ False) ⟶ False) ⟶ ((x65 (x7 (x65 (x59 x2) x56) (x59 x2)) (x65 (x59 x2) x56) = x7 x56 (x59 x2) ⟶ False) ⟶ False) ⟶ ((x65 (x7 (x65 (x59 x2) x56) (x59 x2)) x56 = x7 (x65 (x59 x2) x56) x2 ⟶ False) ⟶ False) ⟶ ((x65 (x7 (x65 (x59 x2) x56) x9) x2 = x7 (x65 (x59 x2) x56) x9 ⟶ False) ⟶ False) ⟶ ((x65 (x7 (x65 (x59 x2) x56) x9) (x65 (x59 x2) x56) = x7 (x65 (x59 x9) x56) (x59 x2) ⟶ False) ⟶ False) ⟶ ((x65 (x7 (x65 (x59 x2) x56) x9) x56 = x7 (x65 x9 x56) x2 ⟶ False) ⟶ False) ⟶ ((x65 (x7 (x65 (x59 x2) x56) x2) (x59 x9) = x7 (x65 x9 x56) (x59 x9) ⟶ False) ⟶ False) ⟶ ((x65 (x7 (x65 (x59 x2) x56) x2) x9 = x7 (x65 (x59 x9) x56) x9 ⟶ False) ⟶ False) ⟶ ((x65 (x7 (x65 (x59 x2) x56) x2) x2 = x7 (x65 (x59 x2) x56) x2 ⟶ False) ⟶ False) ⟶ ((x65 (x7 (x65 (x59 x2) x56) x2) (x65 (x59 x2) x56) = x7 (x65 (x59 x2) x56) (x59 x2) ⟶ False) ⟶ False) ⟶ ((x65 (x7 (x65 (x59 x2) x56) x2) x56 = x7 x56 x2 ⟶ False) ⟶ False) ⟶ ((x65 (x65 (x59 x2) x56) (x59 x9) = x65 x9 x56 ⟶ False) ⟶ False) ⟶ ((x65 (x65 (x59 x2) x56) x9 = x65 (x59 x9) x56 ⟶ False) ⟶ False) ⟶ ((x65 (x65 (x59 x2) x56) x2 = x65 (x59 x2) x56 ⟶ False) ⟶ False) ⟶ ((x65 (x65 (x59 x2) x56) (x65 (x59 x9) x56) = x59 x9 ⟶ False) ⟶ False) ⟶ ((x65 (x65 (x59 x2) x56) (x65 (x59 x2) x56) = x59 x2 ⟶ False) ⟶ False) ⟶ ((x65 (x65 (x59 x2) x56) (x65 x9 x56) = x9 ⟶ False) ⟶ False) ⟶ ((x65 (x65 (x59 x2) x56) x56 = x2 ⟶ False) ⟶ False) ⟶ ((x65 (x7 (x65 x9 x56) (x59 x9)) x2 = x7 (x65 x9 x56) (x59 x9) ⟶ False) ⟶ False) ⟶ ((x65 (x65 x9 x56) x2 = x65 x9 x56 ⟶ False) ⟶ False) ⟶ ((x65 (x65 x9 x56) x56 = x59 x9 ⟶ False) ⟶ False) ⟶ ((x65 (x7 x56 (x59 x2)) (x59 x9) = x7 (x65 (x59 x9) x56) x9 ⟶ False) ⟶ False) ⟶ ((x65 (x7 x56 (x59 x2)) x9 = x7 (x65 x9 x56) (x59 x9) ⟶ False) ⟶ False) ⟶ ((x65 (x7 x56 (x59 x2)) x2 = x7 x56 (x59 x2) ⟶ False) ⟶ False) ⟶ ((x65 (x7 x56 (x59 x2)) (x65 (x59 x9) x56) = x7 (x65 x9 x56) x9 ⟶ False) ⟶ False) ⟶ ((x65 (x7 x56 (x59 x2)) (x65 (x59 x2) x56) = x7 x56 x2 ⟶ False) ⟶ False) ⟶ ((x65 (x7 x56 (x59 x2)) (x65 x9 x56) = x7 (x65 (x59 x9) x56) (x59 x9) ⟶ False) ⟶ False) ⟶ ((x65 (x7 x56 (x59 x2)) x56 = x7 (x65 (x59 x2) x56) (x59 x2) ⟶ False) ⟶ False) ⟶ ((x65 (x7 x56 x9) x2 = x7 x56 x9 ⟶ False) ⟶ False) ⟶ ((x65 (x7 x56 x9) (x65 (x59 x2) x56) = x7 (x65 (x59 x9) x56) x2 ⟶ False) ⟶ False) ⟶ ((x65 (x7 x56 x9) x56 = x7 (x65 x9 x56) (x59 x2) ⟶ False) ⟶ False) ⟶ ((x65 (x7 x56 x2) x2 = x7 x56 x2 ⟶ False) ⟶ False) ⟶ ((x65 (x7 x56 x2) (x65 (x59 x2) x56) = x7 (x65 (x59 x2) x56) x2 ⟶ False) ⟶ False) ⟶ ((x65 (x7 x56 x2) x56 = x7 x56 (x59 x2) ⟶ False) ⟶ False) ⟶ ((x65 x56 (x59 x9) = x65 (x59 x9) x56 ⟶ False) ⟶ False) ⟶ ((x65 x56 x9 = x65 x9 x56 ⟶ False) ⟶ False) ⟶ ((x65 x56 x2 = x56 ⟶ False) ⟶ False) ⟶ ((x65 x56 x11 = x11 ⟶ False) ⟶ False) ⟶ ((x65 x56 (x65 (x59 x9) x56) = x9 ⟶ False) ⟶ False) ⟶ ((x65 x56 (x7 (x65 (x59 x2) x56) x2) = x7 x56 x2 ⟶ False) ⟶ False) ⟶ ((x65 x56 (x65 (x59 x2) x56) = x2 ⟶ False) ⟶ False) ⟶ ((x65 x56 (x65 x9 x56) = x59 x9 ⟶ False) ⟶ False) ⟶ ((x65 x56 x56 = x59 x2 ⟶ False) ⟶ False) ⟶ ((x6 (x59 x9) (x59 x9) = x11 ⟶ False) ⟶ False) ⟶ ((x6 (x59 x9) (x59 x2) = x59 x2 ⟶ False) ⟶ False) ⟶ ((x6 (x59 x9) x11 = x59 x9 ⟶ False) ⟶ False) ⟶ ((x6 (x59 x9) (x65 (x59 x9) x56) = x7 (x65 x9 x56) (x59 x9) ⟶ False) ⟶ False) ⟶ ((x6 (x59 x9) (x65 (x59 x2) x56) = x7 x56 (x59 x9) ⟶ False) ⟶ False) ⟶ ((x6 (x59 x9) (x65 x9 x56) = x7 (x65 (x59 x9) x56) (x59 x9) ⟶ False) ⟶ False) ⟶ ((x6 (x59 x9) x56 = x7 (x65 (x59 x2) x56) (x59 x9) ⟶ False) ⟶ False) ⟶ ((x6 (x59 x2) (x59 x9) = x2 ⟶ False) ⟶ False) ⟶ ((x6 (x59 x2) (x59 x2) = x11 ⟶ False) ⟶ False) ⟶ ((x6 (x59 x2) x2 = x59 x9 ⟶ False) ⟶ False) ⟶ ((x6 (x59 x2) x11 = x59 x2 ⟶ False) ⟶ False) ⟶ ((x6 (x59 x2) (x65 (x59 x9) x56) = x7 (x65 x9 x56) (x59 x2) ⟶ False) ⟶ False) ⟶ ((x6 (x59 x2) (x7 (x65 (x59 x2) x56) (x59 x2)) = x56 ⟶ False) ⟶ False) ⟶ ((x6 (x59 x2) (x65 (x59 x2) x56) = x7 x56 (x59 x2) ⟶ False) ⟶ False) ⟶ ((x6 (x59 x2) (x7 (x65 x9 x56) (x59 x2)) = x65 (x59 x9) x56 ⟶ False) ⟶ False) ⟶ ((x6 (x59 x2) (x65 x9 x56) = x7 (x65 (x59 x9) x56) (x59 x2) ⟶ False) ⟶ False) ⟶ ((x6 (x59 x2) (x7 x56 (x59 x2)) = x65 (x59 x2) x56 ⟶ False) ⟶ False) ⟶ ((x6 (x59 x2) x56 = x7 (x65 (x59 x2) x56) (x59 x2) ⟶ False) ⟶ False) ⟶ ((x6 x9 x9 = x11 ⟶ False) ⟶ False) ⟶ ((x6 x9 x2 = x2 ⟶ False) ⟶ False) ⟶ ((x6 x9 x11 = x9 ⟶ False) ⟶ False) ⟶ ((x6 x9 (x65 (x59 x9) x56) = x7 (x65 x9 x56) x9 ⟶ False) ⟶ False) ⟶ ((x6 x9 (x7 (x65 (x59 x2) x56) x2) = x7 x56 x2 ⟶ False) ⟶ False) ⟶ ((x6 x9 (x65 (x59 x2) x56) = x7 x56 x9 ⟶ False) ⟶ False) ⟶ ((x6 x9 (x65 x9 x56) = x7 (x65 (x59 x9) x56) x9 ⟶ False) ⟶ False) ⟶ ((x6 x9 (x7 x56 x2) = x7 (x65 (x59 x2) x56) x2 ⟶ False) ⟶ False) ⟶ ((x6 x9 x56 = x7 (x65 (x59 x2) x56) x9 ⟶ False) ⟶ False) ⟶ ((x6 x2 (x59 x2) = x9 ⟶ False) ⟶ False) ⟶ ((x6 x2 x9 = x59 x2 ⟶ False) ⟶ False) ⟶ ((x6 x2 x2 = x11 ⟶ False) ⟶ False) ⟶ ((x6 x2 x11 = x2 ⟶ False) ⟶ False) ⟶ ((x6 x2 (x65 (x59 x9) x56) = x7 (x65 x9 x56) x2 ⟶ False) ⟶ False) ⟶ ((x6 x2 (x7 (x65 (x59 x2) x56) x2) = x56 ⟶ False) ⟶ False) ⟶ ((x6 x2 (x65 (x59 x2) x56) = x7 x56 x2 ⟶ False) ⟶ False) ⟶ ((x6 x2 (x7 (x65 x9 x56) x2) = x65 (x59 x9) x56 ⟶ False) ⟶ False) ⟶ ((x6 x2 (x65 x9 x56) = x7 (x65 (x59 x9) x56) x2 ⟶ False) ⟶ False) ⟶ ((x6 x2 (x7 x56 x2) = x65 (x59 x2) x56 ⟶ False) ⟶ False) ⟶ ((x6 x2 x56 = x7 (x65 (x59 x2) x56) x2 ⟶ False) ⟶ False) ⟶ ((x6 x11 (x59 x9) = x9 ⟶ False) ⟶ False) ⟶ ((x6 x11 (x59 x2) = x2 ⟶ False) ⟶ False) ⟶ ((x6 x11 x9 = x59 x9 ⟶ False) ⟶ False) ⟶ ((x6 x11 x2 = x59 x2 ⟶ False) ⟶ False) ⟶ ((x6 x11 x11 = x11 ⟶ False) ⟶ False) ⟶ ((x6 x11 (x65 (x59 x2) x56) = x56 ⟶ False) ⟶ False) ⟶ ((x6 x11 x56 = x65 (x59 x2) x56 ⟶ False) ⟶ False) ⟶ ((x6 (x7 (x65 (x59 x9) x56) (x59 x2)) (x59 x2) = x65 (x59 x9) x56 ⟶ False) ⟶ False) ⟶ ((x6 (x7 (x65 (x59 x9) x56) x9) (x7 (x65 (x59 x9) x56) x9) = x11 ⟶ False) ⟶ False) ⟶ ((x6 (x7 (x65 (x59 x9) x56) x2) (x59 x2) = x7 (x65 (x59 x9) x56) x9 ⟶ False) ⟶ False) ⟶ ((x6 (x65 (x59 x9) x56) (x59 x9) = x7 (x65 (x59 x9) x56) x9 ⟶ False) ⟶ False) ⟶ ((x6 (x65 (x59 x9) x56) (x59 x2) = x7 (x65 (x59 x9) x56) x2 ⟶ False) ⟶ False) ⟶ ((x6 (x65 (x59 x9) x56) x9 = x7 (x65 (x59 x9) x56) (x59 x9) ⟶ False) ⟶ False) ⟶ ((x6 (x65 (x59 x9) x56) (x65 (x59 x9) x56) = x11 ⟶ False) ⟶ False) ⟶ ((x6 (x65 (x59 x9) x56) (x65 (x59 x2) x56) = x65 (x59 x2) x56 ⟶ False) ⟶ False) ⟶ ((x6 (x7 (x65 (x59 x2) x56) (x59 x2)) (x59 x2) = x65 (x59 x2) x56 ⟶ False) ⟶ False) ⟶ ((x6 (x7 (x65 (x59 x2) x56) (x59 x2)) (x7 (x65 (x59 x2) x56) (x59 x2)) = x11 ⟶ False) ⟶ False) ⟶ ((x6 (x7 (x65 (x59 x2) x56) (x59 x2)) (x65 (x59 x2) x56) = x59 x2 ⟶ False) ⟶ False) ⟶ ((x6 (x7 (x65 (x59 x2) x56) (x59 x2)) x56 = x7 (x65 (x59 x9) x56) (x59 x2) ⟶ False) ⟶ False) ⟶ ((x6 (x7 (x65 (x59 x2) x56) x9) (x7 (x65 (x59 x2) x56) x9) = x11 ⟶ False) ⟶ False) ⟶ ((x6 (x7 (x65 (x59 x2) x56) x2) (x59 x2) = x7 (x65 (x59 x2) x56) x9 ⟶ False) ⟶ False) ⟶ ((x6 (x7 (x65 (x59 x2) x56) x2) x2 = x65 (x59 x2) x56 ⟶ False) ⟶ False) ⟶ ((x6 (x7 (x65 (x59 x2) x56) x2) x11 = x7 (x65 (x59 x2) x56) x2 ⟶ False) ⟶ False) ⟶ ((x6 (x7 (x65 (x59 x2) x56) x2) (x7 (x65 (x59 x2) x56) x2) = x11 ⟶ False) ⟶ False) ⟶ ((x6 (x7 (x65 (x59 x2) x56) x2) (x65 (x59 x2) x56) = x2 ⟶ False) ⟶ False) ⟶ ((x6 (x7 (x65 (x59 x2) x56) x2) (x7 x56 x2) = x65 (x59 x9) x56 ⟶ False) ⟶ False) ⟶ ((x6 (x7 (x65 (x59 x2) x56) x2) x56 = x7 (x65 (x59 x9) x56) x2 ⟶ False) ⟶ False) ⟶ ((x6 (x65 (x59 x2) x56) (x59 x2) = x7 (x65 (x59 x2) x56) x2 ⟶ False) ⟶ False) ⟶ ((x6 (x65 (x59 x2) x56) x9 = x7 (x65 (x59 x2) x56) (x59 x9) ⟶ False) ⟶ False) ⟶ ((x6 (x65 (x59 x2) x56) x2 = x7 (x65 (x59 x2) x56) (x59 x2) ⟶ False) ⟶ False) ⟶ ((x6 (x65 (x59 x2) x56) (x65 (x59 x9) x56) = x56 ⟶ False) ⟶ False) ⟶ ((x6 (x65 (x59 x2) x56) (x7 (x65 (x59 x2) x56) x2) = x59 x2 ⟶ False) ⟶ False) ⟶ ((x6 (x65 (x59 x2) x56) (x65 (x59 x2) x56) = x11 ⟶ False) ⟶ False) ⟶ ((x6 (x65 (x59 x2) x56) x56 = x65 (x59 x9) x56 ⟶ False) ⟶ False) ⟶ ((x6 (x7 (x65 x9 x56) (x59 x9)) (x7 (x65 x9 x56) (x59 x9)) = x11 ⟶ False) ⟶ False) ⟶ ((x6 (x7 (x65 x9 x56) (x59 x9)) (x65 x9 x56) = x59 x9 ⟶ False) ⟶ False) ⟶ ((x6 (x65 x9 x56) x9 = x7 (x65 x9 x56) (x59 x9) ⟶ False) ⟶ False) ⟶ ((x6 (x65 x9 x56) x2 = x7 (x65 x9 x56) (x59 x2) ⟶ False) ⟶ False) ⟶ ((x6 (x65 x9 x56) (x7 (x65 x9 x56) (x59 x9)) = x9 ⟶ False) ⟶ False) ⟶ ((x6 (x65 x9 x56) (x65 x9 x56) = x11 ⟶ False) ⟶ False) ⟶ ((x6 (x65 x9 x56) x56 = x56 ⟶ False) ⟶ False) ⟶ ((x6 (x7 x56 (x59 x2)) (x59 x2) = x56 ⟶ False) ⟶ False) ⟶ ((x6 (x7 x56 (x59 x2)) (x65 (x59 x2) x56) = x7 (x65 x9 x56) (x59 x2) ⟶ False) ⟶ False) ⟶ ((x6 (x7 x56 (x59 x2)) (x7 x56 (x59 x2)) = x11 ⟶ False) ⟶ False) ⟶ ((x6 (x7 x56 (x59 x2)) x56 = x59 x2 ⟶ False) ⟶ False) ⟶ ((x6 (x7 x56 x9) (x7 x56 x9) = x11 ⟶ False) ⟶ False) ⟶ ((x6 (x7 x56 x2) (x59 x2) = x7 x56 x9 ⟶ False) ⟶ False) ⟶ ((x6 (x7 x56 x2) x2 = x56 ⟶ False) ⟶ False) ⟶ ((x6 (x7 x56 x2) x11 = x7 x56 x2 ⟶ False) ⟶ False) ⟶ ((x6 (x7 x56 x2) (x65 (x59 x2) x56) = x7 (x65 x9 x56) x2 ⟶ False) ⟶ False) ⟶ ((x6 (x7 x56 x2) (x7 x56 x2) = x11 ⟶ False) ⟶ False) ⟶ ((x6 (x7 x56 x2) x56 = x2 ⟶ False) ⟶ False) ⟶ ((x6 x56 (x59 x2) = x7 x56 x2 ⟶ False) ⟶ False) ⟶ ((x6 x56 x9 = x7 x56 (x59 x9) ⟶ False) ⟶ False) ⟶ ((x6 x56 x2 = x7 x56 (x59 x2) ⟶ False) ⟶ False) ⟶ ((x6 x56 x11 = x56 ⟶ False) ⟶ False) ⟶ ((x6 x56 (x65 (x59 x2) x56) = x65 x9 x56 ⟶ False) ⟶ False) ⟶ ((x6 x56 (x65 x9 x56) = x65 (x59 x2) x56 ⟶ False) ⟶ False) ⟶ ((x6 x56 (x7 x56 (x59 x2)) = x2 ⟶ False) ⟶ False) ⟶ ((x6 x56 (x7 x56 x2) = x59 x2 ⟶ False) ⟶ False) ⟶ ((x6 x56 x56 = x11 ⟶ False) ⟶ False) ⟶ ((x7 (x59 x9) x9 = x11 ⟶ False) ⟶ False) ⟶ ((x7 (x59 x9) x2 = x59 x2 ⟶ False) ⟶ False) ⟶ ((x7 (x59 x2) (x59 x2) = x59 x9 ⟶ False) ⟶ False) ⟶ ((x7 (x59 x2) x9 = x2 ⟶ False) ⟶ False) ⟶ ((x7 (x59 x2) x2 = x11 ⟶ False) ⟶ False) ⟶ ((x7 (x59 x2) x11 = x59 x2 ⟶ False) ⟶ False) ⟶ ((x7 x9 (x59 x9) = x11 ⟶ False) ⟶ False) ⟶ ((x7 x9 (x59 x2) = x2 ⟶ False) ⟶ False) ⟶ ((x7 x9 x11 = x9 ⟶ False) ⟶ False) ⟶ ((x7 x2 (x59 x9) = x59 x2 ⟶ False) ⟶ False) ⟶ ((x7 x2 (x59 x2) = x11 ⟶ False) ⟶ False) ⟶ ((x7 x2 x2 = x9 ⟶ False) ⟶ False) ⟶ ((x7 x2 x11 = x2 ⟶ False) ⟶ False) ⟶ ((x7 x2 (x65 (x59 x2) x56) = x7 (x65 (x59 x2) x56) x2 ⟶ False) ⟶ False) ⟶ ((x7 x2 x56 = x7 x56 x2 ⟶ False) ⟶ False) ⟶ ((x7 x11 (x59 x9) = x59 x9 ⟶ False) ⟶ False) ⟶ ((x7 x11 (x59 x2) = x59 x2 ⟶ False) ⟶ False) ⟶ ((x7 x11 x9 = x9 ⟶ False) ⟶ False) ⟶ ((x7 x11 x2 = x2 ⟶ False) ⟶ False) ⟶ ((x7 x11 x11 = x11 ⟶ False) ⟶ False) ⟶ ((x7 x11 (x65 (x59 x2) x56) = x65 (x59 x2) x56 ⟶ False) ⟶ False) ⟶ ((x7 x11 x56 = x56 ⟶ False) ⟶ False) ⟶ ((x7 (x65 (x59 x9) x56) (x65 x9 x56) = x11 ⟶ False) ⟶ False) ⟶ ((x7 (x65 (x59 x9) x56) x56 = x65 (x59 x2) x56 ⟶ False) ⟶ False) ⟶ ((x7 (x65 (x59 x2) x56) x2 = x7 (x65 (x59 x2) x56) x2 ⟶ False) ⟶ False) ⟶ ((x7 (x65 (x59 x2) x56) (x65 (x59 x2) x56) = x65 (x59 x9) x56 ⟶ False) ⟶ False) ⟶ ((x7 (x65 (x59 x2) x56) (x65 x9 x56) = x56 ⟶ False) ⟶ False) ⟶ ((x7 (x65 (x59 x2) x56) x56 = x11 ⟶ False) ⟶ False) ⟶ ((x7 (x65 x9 x56) (x65 (x59 x9) x56) = x11 ⟶ False) ⟶ False) ⟶ ((x7 (x65 x9 x56) (x65 (x59 x2) x56) = x56 ⟶ False) ⟶ False) ⟶ ((x7 x56 x2 = x7 x56 x2 ⟶ False) ⟶ False) ⟶ ((x7 x56 x11 = x56 ⟶ False) ⟶ False) ⟶ ((x7 x56 (x65 (x59 x9) x56) = x65 (x59 x2) x56 ⟶ False) ⟶ False) ⟶ ((x7 x56 (x65 (x59 x2) x56) = x11 ⟶ False) ⟶ False) ⟶ ((x7 x56 x56 = x65 x9 x56 ⟶ False) ⟶ False) ⟶ (∀ x71 . (x61 x71 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 x73 . (x64 x73 ⟶ False) ⟶ (x64 x71 ⟶ False) ⟶ x5 x71 (x4 x73) ⟶ x5 x72 x71 ⟶ (x10 x72 x73 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 x73 . (x64 x73 ⟶ False) ⟶ (x64 x71 ⟶ False) ⟶ x5 x71 (x4 x73) ⟶ x10 x72 x73 x71 ⟶ (x5 x72 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x5 x72 x8 ⟶ x12 x71 ⟶ (x0 x72 x71 = x6 x72 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x5 x72 x8 ⟶ x12 x71 ⟶ (x68 x72 x71 = x65 x72 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x5 x72 x8 ⟶ x12 x71 ⟶ (x67 x72 x71 = x7 x72 x71 ⟶ False) ⟶ False) ⟶ ((x1 = x56 ⟶ False) ⟶ False) ⟶ ((x63 = x62 ⟶ False) ⟶ False) ⟶ ((x58 = x60 ⟶ False) ⟶ False) ⟶ (∀ x71 . x70 x71 ⟶ (x66 x71 = x13 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x70 x71 ⟶ (x69 x71 = x55 x71 ⟶ False) ⟶ False) ⟶ ((x14 x15 ⟶ False) ⟶ False) ⟶ ((x64 x15 ⟶ False) ⟶ False) ⟶ ((x12 x16 ⟶ False) ⟶ False) ⟶ ((x14 x16 ⟶ False) ⟶ False) ⟶ ((x70 x16 ⟶ False) ⟶ False) ⟶ ((x64 x16 ⟶ False) ⟶ False) ⟶ ((x17 x18 ⟶ False) ⟶ False) ⟶ ((x14 x18 ⟶ False) ⟶ False) ⟶ ((x12 x19 ⟶ False) ⟶ False) ⟶ ((x17 x19 ⟶ False) ⟶ False) ⟶ ((x14 x19 ⟶ False) ⟶ False) ⟶ ((x70 x19 ⟶ False) ⟶ False) ⟶ ((x20 x21 ⟶ False) ⟶ False) ⟶ ((x54 x21 ⟶ False) ⟶ False) ⟶ (x64 x21 ⟶ False) ⟶ ((x57 x53 ⟶ False) ⟶ False) ⟶ ((x14 x53 ⟶ False) ⟶ False) ⟶ ((x12 x52 ⟶ False) ⟶ False) ⟶ ((x57 x52 ⟶ False) ⟶ False) ⟶ ((x14 x52 ⟶ False) ⟶ False) ⟶ ((x70 x52 ⟶ False) ⟶ False) ⟶ ((x70 x51 ⟶ False) ⟶ False) ⟶ (x64 x51 ⟶ False) ⟶ (x64 x50 ⟶ False) ⟶ ((x54 x22 ⟶ False) ⟶ False) ⟶ (x64 x22 ⟶ False) ⟶ ((x14 x23 ⟶ False) ⟶ False) ⟶ ((x12 x49 ⟶ False) ⟶ False) ⟶ ((x70 x24 ⟶ False) ⟶ False) ⟶ ((x64 x48 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . (x25 (x26 x71 x72) x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . (x47 (x26 x72 x71) x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . (x27 (x26 x71 x72) ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . (x64 (x26 x71 x72) ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . (x5 (x26 x71 x72) (x4 (x28 x72 x71)) ⟶ False) ⟶ False) ⟶ ((x54 x46 ⟶ False) ⟶ False) ⟶ (x64 x46 ⟶ False) ⟶ (∀ x71 . x70 x71 ⟶ (x59 (x59 x71) = x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . (x17 x72 ⟶ False) ⟶ x12 x72 ⟶ (x17 x71 ⟶ False) ⟶ x12 x71 ⟶ x17 (x7 x72 x71) ⟶ False) ⟶ (x45 x44 ⟶ False) ⟶ (∀ x71 x72 . (x64 x72 ⟶ False) ⟶ x70 x72 ⟶ (x64 x71 ⟶ False) ⟶ x70 x71 ⟶ x64 (x65 x72 x71) ⟶ False) ⟶ (x45 x8 ⟶ False) ⟶ (∀ x71 x72 . x12 x72 ⟶ x12 x71 ⟶ (x12 (x6 x72 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x12 x72 ⟶ x12 x71 ⟶ (x12 (x65 x72 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 . (x64 x71 ⟶ False) ⟶ x70 x71 ⟶ (x70 (x59 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 . (x64 x71 ⟶ False) ⟶ x70 x71 ⟶ x64 (x59 x71) ⟶ False) ⟶ ((x54 x60 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x12 x72 ⟶ x12 x71 ⟶ (x12 (x7 x72 x71) ⟶ False) ⟶ False) ⟶ ((x20 x60 ⟶ False) ⟶ False) ⟶ ((x20 x8 ⟶ False) ⟶ False) ⟶ ((x20 x44 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x70 x72 ⟶ x70 x71 ⟶ (x70 (x6 x72 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 . x12 x71 ⟶ (x12 (x59 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 . x12 x71 ⟶ (x70 (x59 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x70 x72 ⟶ x70 x71 ⟶ (x70 (x65 x72 x71) ⟶ False) ⟶ False) ⟶ ((x43 x8 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x70 x72 ⟶ x70 x71 ⟶ (x70 (x7 x72 x71) ⟶ False) ⟶ False) ⟶ (x64 x44 ⟶ False) ⟶ (∀ x71 . x70 x71 ⟶ (x12 (x13 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . (x17 x72 ⟶ False) ⟶ x12 x72 ⟶ (x17 x71 ⟶ False) ⟶ x12 x71 ⟶ x17 (x65 x72 x71) ⟶ False) ⟶ (∀ x71 x72 . (x57 x72 ⟶ False) ⟶ x12 x72 ⟶ (x57 x71 ⟶ False) ⟶ x12 x71 ⟶ x17 (x65 x72 x71) ⟶ False) ⟶ (∀ x71 x72 . (x57 x72 ⟶ False) ⟶ x12 x72 ⟶ (x17 x71 ⟶ False) ⟶ x12 x71 ⟶ x57 (x65 x71 x72) ⟶ False) ⟶ (∀ x71 x72 . (x57 x72 ⟶ False) ⟶ x12 x72 ⟶ (x17 x71 ⟶ False) ⟶ x12 x71 ⟶ x57 (x65 x72 x71) ⟶ False) ⟶ (∀ x71 x72 . x17 x72 ⟶ x12 x72 ⟶ (x17 x71 ⟶ False) ⟶ x12 x71 ⟶ (x57 (x6 x71 x72) ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x17 x72 ⟶ x12 x72 ⟶ (x17 x71 ⟶ False) ⟶ x12 x71 ⟶ (x17 (x6 x72 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x57 x72 ⟶ x12 x72 ⟶ (x57 x71 ⟶ False) ⟶ x12 x71 ⟶ (x17 (x6 x71 x72) ⟶ False) ⟶ False) ⟶ ((x70 x56 ⟶ False) ⟶ False) ⟶ ((x64 x62 ⟶ False) ⟶ False) ⟶ (x64 x8 ⟶ False) ⟶ ((x42 x44 ⟶ False) ⟶ False) ⟶ (∀ x71 . x70 x71 ⟶ (x12 (x55 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x57 x72 ⟶ x12 x72 ⟶ (x57 x71 ⟶ False) ⟶ x12 x71 ⟶ (x57 (x6 x72 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . (x17 x72 ⟶ False) ⟶ x12 x72 ⟶ (x57 x71 ⟶ False) ⟶ x12 x71 ⟶ x57 (x6 x71 x72) ⟶ False) ⟶ (∀ x71 x72 . (x17 x72 ⟶ False) ⟶ x12 x72 ⟶ (x57 x71 ⟶ False) ⟶ x12 x71 ⟶ x17 (x6 x72 x71) ⟶ False) ⟶ (∀ x71 . (x17 x71 ⟶ False) ⟶ x12 x71 ⟶ x57 (x59 x71) ⟶ False) ⟶ (∀ x71 . (x17 x71 ⟶ False) ⟶ x12 x71 ⟶ (x70 (x59 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 . (x57 x71 ⟶ False) ⟶ x12 x71 ⟶ x17 (x59 x71) ⟶ False) ⟶ (∀ x71 . (x57 x71 ⟶ False) ⟶ x12 x71 ⟶ (x70 (x59 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x17 x72 ⟶ x12 x72 ⟶ (x57 x71 ⟶ False) ⟶ x12 x71 ⟶ (x17 (x7 x71 x72) ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x17 x72 ⟶ x12 x72 ⟶ (x57 x71 ⟶ False) ⟶ x12 x71 ⟶ (x17 (x7 x72 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x57 x72 ⟶ x12 x72 ⟶ (x17 x71 ⟶ False) ⟶ x12 x71 ⟶ (x57 (x7 x71 x72) ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x57 x72 ⟶ x12 x72 ⟶ (x17 x71 ⟶ False) ⟶ x12 x71 ⟶ (x57 (x7 x72 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . (x57 x72 ⟶ False) ⟶ x12 x72 ⟶ (x57 x71 ⟶ False) ⟶ x12 x71 ⟶ x57 (x7 x72 x71) ⟶ False) ⟶ (∀ x71 x72 . (x64 x72 ⟶ False) ⟶ (x64 x71 ⟶ False) ⟶ x5 x71 (x4 x72) ⟶ (x10 (x41 x71 x72) x72 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . (x5 (x29 x71) x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 x73 . (x64 x73 ⟶ False) ⟶ (x64 x71 ⟶ False) ⟶ x5 x71 (x4 x73) ⟶ x10 x72 x73 x71 ⟶ (x5 x72 x73 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x5 x72 x8 ⟶ x12 x71 ⟶ (x5 (x0 x72 x71) x8 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x5 x72 x8 ⟶ x12 x71 ⟶ (x5 (x68 x72 x71) x8 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x5 x72 x8 ⟶ x12 x71 ⟶ (x5 (x67 x72 x71) x8 ⟶ False) ⟶ False) ⟶ ((x5 x1 x44 ⟶ False) ⟶ False) ⟶ ((x10 x63 x8 x58 ⟶ False) ⟶ False) ⟶ ((x5 x58 (x4 x8) ⟶ False) ⟶ False) ⟶ (∀ x71 . x70 x71 ⟶ (x70 (x59 x71) ⟶ False) ⟶ False) ⟶ (∀ x71 . x70 x71 ⟶ (x5 (x66 x71) x8 ⟶ False) ⟶ False) ⟶ (∀ x71 . x70 x71 ⟶ (x5 (x69 x71) x8 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 x73 . x70 x73 ⟶ (x3 x73 x8 ⟶ False) ⟶ x40 x72 ⟶ x38 x72 x9 x8 ⟶ x5 x72 (x4 (x28 x9 x8)) ⟶ x73 = x72 ⟶ x71 = x39 x72 x2 ⟶ (x71 = x13 x73 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x70 x72 ⟶ (x3 x72 x8 ⟶ False) ⟶ x71 = x13 x72 ⟶ (x71 = x39 (x30 x71 x72) x2 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x70 x72 ⟶ (x3 x72 x8 ⟶ False) ⟶ x71 = x13 x72 ⟶ (x72 = x30 x71 x72 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x70 x72 ⟶ (x3 x72 x8 ⟶ False) ⟶ x71 = x13 x72 ⟶ (x5 (x30 x71 x72) (x4 (x28 x9 x8)) ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x70 x72 ⟶ (x3 x72 x8 ⟶ False) ⟶ x71 = x13 x72 ⟶ (x38 (x30 x71 x72) x9 x8 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x70 x72 ⟶ (x3 x72 x8 ⟶ False) ⟶ x71 = x13 x72 ⟶ (x40 (x30 x71 x72) ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x70 x72 ⟶ x3 x72 x8 ⟶ x71 = x63 ⟶ (x71 = x13 x72 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x70 x72 ⟶ x3 x72 x8 ⟶ x71 = x13 x72 ⟶ (x71 = x63 ⟶ False) ⟶ False) ⟶ (∀ x71 . x3 x71 x8 ⟶ (x12 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x12 x71 ⟶ (x3 x71 x8 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x5 x72 x8 ⟶ x12 x71 ⟶ (x68 x72 x71 = x68 x71 x72 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x5 x72 x8 ⟶ x12 x71 ⟶ (x67 x72 x71 = x67 x71 x72 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x70 x72 ⟶ x70 x71 ⟶ (x65 x72 x71 = x65 x71 x72 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x70 x72 ⟶ x70 x71 ⟶ (x7 x72 x71 = x7 x71 x72 ⟶ False) ⟶ False) ⟶ (∀ x71 . x14 x71 ⟶ (x57 x71 ⟶ False) ⟶ (x17 x71 ⟶ False) ⟶ (x14 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x14 x71 ⟶ (x57 x71 ⟶ False) ⟶ (x17 x71 ⟶ False) ⟶ (x64 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x5 x71 (x4 x8) ⟶ (x43 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x64 x71 ⟶ x14 x71 ⟶ x17 x71 ⟶ False) ⟶ (∀ x71 . x64 x71 ⟶ x14 x71 ⟶ x57 x71 ⟶ False) ⟶ (∀ x71 . x64 x71 ⟶ x14 x71 ⟶ (x14 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . (x64 x71 ⟶ False) ⟶ x14 x71 ⟶ (x57 x71 ⟶ False) ⟶ (x17 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . (x64 x71 ⟶ False) ⟶ x14 x71 ⟶ (x57 x71 ⟶ False) ⟶ (x14 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x5 x71 (x4 x44) ⟶ (x42 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x14 x71 ⟶ x17 x71 ⟶ x57 x71 ⟶ False) ⟶ (∀ x71 . x14 x71 ⟶ x17 x71 ⟶ (x14 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x14 x71 ⟶ x17 x71 ⟶ x64 x71 ⟶ False) ⟶ (∀ x71 . x43 x71 ⟶ (x42 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . (x64 x71 ⟶ False) ⟶ x14 x71 ⟶ (x17 x71 ⟶ False) ⟶ (x57 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . (x64 x71 ⟶ False) ⟶ x14 x71 ⟶ (x17 x71 ⟶ False) ⟶ (x14 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x12 x71 ⟶ (x14 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 x73 . x64 x73 ⟶ x5 x71 (x4 (x28 x72 x73)) ⟶ (x64 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x43 x71 ⟶ (x31 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x14 x71 ⟶ x57 x71 ⟶ x17 x71 ⟶ False) ⟶ (∀ x71 . x14 x71 ⟶ x57 x71 ⟶ (x14 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x14 x71 ⟶ x57 x71 ⟶ x64 x71 ⟶ False) ⟶ (∀ x71 . x12 x71 ⟶ (x70 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x5 x71 x44 ⟶ (x70 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 x73 . x64 x73 ⟶ x5 x71 (x4 (x28 x73 x72)) ⟶ (x64 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x37 x71 ⟶ (x43 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x32 x71 ⟶ (x14 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x32 x71 ⟶ (x12 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x32 x71 ⟶ (x70 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 x73 . x5 x73 (x4 (x28 x71 x72)) ⟶ (x25 x73 x72 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 x73 . x5 x73 (x4 (x28 x72 x71)) ⟶ (x47 x73 x72 ⟶ False) ⟶ False) ⟶ (∀ x71 . x36 x71 ⟶ (x37 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x64 x71 ⟶ (x20 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x5 x71 x58 ⟶ (x54 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x54 x72 ⟶ x5 x71 (x4 x72) ⟶ (x54 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x36 x72 ⟶ x5 x71 (x4 x72) ⟶ (x36 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x37 x72 ⟶ x5 x71 (x4 x72) ⟶ (x37 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x43 x72 ⟶ x5 x71 (x4 x72) ⟶ (x43 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x31 x72 ⟶ x5 x71 (x4 x72) ⟶ (x31 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x5 x71 x8 ⟶ (x12 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x5 x71 x8 ⟶ (x70 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 x73 . x5 x73 (x4 (x28 x71 x72)) ⟶ (x27 x73 ⟶ False) ⟶ False) ⟶ (∀ x71 . x54 x71 ⟶ (x36 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x42 x72 ⟶ x5 x71 (x4 x72) ⟶ (x42 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x64 x71 ⟶ (x54 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x54 x72 ⟶ x5 x71 x72 ⟶ (x32 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x36 x72 ⟶ x5 x71 x72 ⟶ (x33 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x37 x72 ⟶ x5 x71 x72 ⟶ (x35 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x43 x72 ⟶ x5 x71 x72 ⟶ (x12 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x31 x72 ⟶ x5 x71 x72 ⟶ (x14 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x42 x72 ⟶ x5 x71 x72 ⟶ (x70 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 . x5 x71 (x4 x58) ⟶ (x54 x71 ⟶ False) ⟶ False) ⟶ (∀ x71 x72 . x3 x71 x72 ⟶ x3 x72 x71 ⟶ False) ⟶ (x69 (x65 x34 x1) = x63 ⟶ False) ⟶ ((x12 x34 ⟶ False) ⟶ False) ⟶ False (proof)