Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrNUD../05434..
PUbX1../54c71..
vout
PrNUD../b75c3.. 0.01 bars
TMcTC../11ae0.. ownership of 5819e.. as prop with payaddr PrPhD.. rights free controlledby PrPhD.. upto 0
TMKsy../7dc65.. ownership of bc558.. as prop with payaddr PrPhD.. rights free controlledby PrPhD.. upto 0
PUWJA../e2566.. doc published by PrPhD..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0 ⟶ False
Theorem 5819e.. : ∀ 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 ⟶ (x81 = x80 ⟶ False) ⟶ x79 x80 ⟶ False) ⟶ (∀ x80 x81 . x0 x80 x81 ⟶ x79 x81 ⟶ False) ⟶ (∀ x80 . x79 x80 ⟶ (x80 = x78 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 . x0 x80 x81 ⟶ x2 x81 (x1 x82) ⟶ x79 x82 ⟶ False) ⟶ (∀ x80 x81 x82 . x0 x81 x82 ⟶ x2 x82 (x1 x80) ⟶ (x2 x81 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x3 x81 x80 ⟶ (x2 x81 (x1 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x2 x81 (x1 x80) ⟶ (x3 x81 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x2 x80 x81 ⟶ (x79 x81 ⟶ False) ⟶ (x0 x80 x81 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x0 x81 x80 ⟶ (x2 x81 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . (x4 x80 x78 = x80 ⟶ False) ⟶ False) ⟶ (x79 x77 ⟶ False) ⟶ (∀ x80 . (x3 x80 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . (x76 x80 ⟶ False) ⟶ x76 (x75 x80) ⟶ False) ⟶ (∀ x80 . (x76 x80 ⟶ False) ⟶ (x2 (x75 x80) (x1 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 . (x79 x80 ⟶ False) ⟶ (x76 (x74 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 . (x79 x80 ⟶ False) ⟶ x79 (x74 x80) ⟶ False) ⟶ (∀ x80 . (x79 x80 ⟶ False) ⟶ (x2 (x74 x80) (x1 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 . (x79 x80 ⟶ False) ⟶ (x6 (x5 x80) x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . (x79 x80 ⟶ False) ⟶ (x2 (x5 x80) (x1 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 . (x7 x80 ⟶ False) ⟶ x9 x80 ⟶ x79 (x8 x80) ⟶ False) ⟶ (∀ x80 . (x7 x80 ⟶ False) ⟶ x9 x80 ⟶ (x2 (x8 x80) (x1 (x73 x80)) ⟶ False) ⟶ False) ⟶ (∀ x80 . x6 (x10 x80) x80 ⟶ False) ⟶ (∀ x80 . (x2 (x10 x80) (x1 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . (x11 (x12 x80 x81) x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . (x72 (x12 x81 x80) x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . (x13 (x12 x80 x81) ⟶ False) ⟶ False) ⟶ (∀ x80 . x71 x80 ⟶ (x69 (x70 x80) x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x71 x80 ⟶ (x2 (x70 x80) (x1 (x73 x80)) ⟶ False) ⟶ False) ⟶ (x79 x68 ⟶ False) ⟶ (∀ x80 . (x79 (x14 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 . (x2 (x14 x80) (x1 x80) ⟶ False) ⟶ False) ⟶ ((x15 x16 ⟶ False) ⟶ False) ⟶ ((x13 x16 ⟶ False) ⟶ False) ⟶ (∀ x80 . (x17 (x18 x80) x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . (x67 (x18 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 . (x19 (x18 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 . (x66 (x18 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 . (x20 (x18 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 . (x11 (x18 x80) x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . (x72 (x18 x80) x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . (x13 (x18 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 . (x2 (x18 x80) (x1 (x21 x80 x80)) ⟶ False) ⟶ False) ⟶ (∀ x80 . (x65 x80 ⟶ False) ⟶ x9 x80 ⟶ x76 (x64 x80) ⟶ False) ⟶ (∀ x80 . (x65 x80 ⟶ False) ⟶ x9 x80 ⟶ (x2 (x64 x80) (x1 (x73 x80)) ⟶ False) ⟶ False) ⟶ (∀ x80 . (x7 x80 ⟶ False) ⟶ x9 x80 ⟶ (x76 (x63 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 . (x7 x80 ⟶ False) ⟶ x9 x80 ⟶ x79 (x63 x80) ⟶ False) ⟶ (∀ x80 . (x7 x80 ⟶ False) ⟶ x9 x80 ⟶ (x2 (x63 x80) (x1 (x73 x80)) ⟶ False) ⟶ False) ⟶ ((x79 x22 ⟶ False) ⟶ False) ⟶ (∀ x80 . (x79 x80 ⟶ False) ⟶ x79 (x62 x80) ⟶ False) ⟶ (∀ x80 . (x79 x80 ⟶ False) ⟶ (x2 (x62 x80) (x1 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . (x11 (x61 x80 x81) x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . (x72 (x61 x81 x80) x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . (x13 (x61 x80 x81) ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . (x79 (x61 x80 x81) ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . (x2 (x61 x80 x81) (x1 (x21 x81 x80)) ⟶ False) ⟶ False) ⟶ ((x13 x23 ⟶ False) ⟶ False) ⟶ (x79 x23 ⟶ False) ⟶ ((x24 x25 ⟶ False) ⟶ False) ⟶ ((x60 x25 ⟶ False) ⟶ False) ⟶ (∀ x80 . (x4 x80 x80 = x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 x83 x84 x85 . x2 x84 (x1 (x21 x85 x85)) ⟶ x2 x80 (x1 (x21 x85 x85)) ⟶ x59 x85 x84 x80 = x59 x82 x81 x83 ⟶ (x80 = x83 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 x83 x84 x85 . x2 x84 (x1 (x21 x85 x85)) ⟶ x2 x80 (x1 (x21 x85 x85)) ⟶ x59 x85 x84 x80 = x59 x82 x83 x81 ⟶ (x84 = x83 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 x83 x84 x85 . x2 x84 (x1 (x21 x85 x85)) ⟶ x2 x80 (x1 (x21 x85 x85)) ⟶ x59 x85 x84 x80 = x59 x83 x82 x81 ⟶ (x85 = x83 ⟶ False) ⟶ False) ⟶ (∀ x80 . (x26 x80 ⟶ False) ⟶ x71 x80 ⟶ x79 (x27 x80) ⟶ False) ⟶ (∀ x80 . (x58 x80 ⟶ False) ⟶ x9 x80 ⟶ x57 (x73 x80) ⟶ False) ⟶ (∀ x80 . x58 x80 ⟶ x9 x80 ⟶ (x57 (x73 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 . x65 x80 ⟶ x9 x80 ⟶ (x76 (x73 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 . (x65 x80 ⟶ False) ⟶ x9 x80 ⟶ x76 (x73 x80) ⟶ False) ⟶ (∀ x80 x81 . x13 x81 ⟶ x56 x81 ⟶ x13 x80 ⟶ x56 x80 ⟶ (x56 (x4 x81 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . (x13 (x21 x80 x81) ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . (x79 x81 ⟶ False) ⟶ x79 (x4 x80 x81) ⟶ False) ⟶ (∀ x80 x81 . x60 x81 ⟶ (x24 (x28 x81 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x60 x81 ⟶ x7 (x28 x81 x80) ⟶ False) ⟶ (∀ x80 x81 . (x79 x81 ⟶ False) ⟶ x79 (x4 x81 x80) ⟶ False) ⟶ (∀ x80 x81 x82 . x13 x82 ⟶ x11 x82 x80 ⟶ x13 x81 ⟶ x11 x81 x80 ⟶ (x11 (x4 x82 x81) x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x13 x81 ⟶ x20 x81 ⟶ x13 x80 ⟶ x20 x80 ⟶ (x20 (x4 x81 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x13 x81 ⟶ x13 x80 ⟶ (x13 (x4 x81 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 x83 . x66 x83 ⟶ x2 x83 (x1 (x21 x80 x80)) ⟶ x66 x82 ⟶ x2 x82 (x1 (x21 x81 x81)) ⟶ (x66 (x4 x83 x82) ⟶ False) ⟶ False) ⟶ (∀ x80 . x79 (x55 x80) ⟶ False) ⟶ (∀ x80 . (x7 x80 ⟶ False) ⟶ x9 x80 ⟶ x79 (x73 x80) ⟶ False) ⟶ (∀ x80 x81 x82 x83 . x20 x83 ⟶ x2 x83 (x1 (x21 x80 x80)) ⟶ x20 x82 ⟶ x2 x82 (x1 (x21 x81 x81)) ⟶ (x20 (x4 x83 x82) ⟶ False) ⟶ False) ⟶ (∀ x80 . x29 x80 ⟶ x71 x80 ⟶ (x17 (x27 x80) (x73 x80) ⟶ False) ⟶ False) ⟶ ((x79 x78 ⟶ False) ⟶ False) ⟶ (∀ x80 . x79 (x1 x80) ⟶ False) ⟶ (∀ x80 . x7 x80 ⟶ x9 x80 ⟶ (x79 (x73 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 . x13 x82 ⟶ x72 x82 x80 ⟶ x13 x81 ⟶ x72 x81 x80 ⟶ (x72 (x4 x82 x81) x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 x83 . x17 x82 x83 ⟶ x2 x82 (x1 (x21 x83 x83)) ⟶ x17 x80 x81 ⟶ x2 x80 (x1 (x21 x81 x81)) ⟶ (x17 (x4 x82 x80) (x4 x83 x81) ⟶ False) ⟶ False) ⟶ (∀ x80 . x30 x80 ⟶ x32 x80 ⟶ (x66 (x31 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 . x54 x80 ⟶ x32 x80 ⟶ (x56 (x31 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 . x33 x80 ⟶ x32 x80 ⟶ (x20 (x31 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 . x53 x80 ⟶ x32 x80 ⟶ (x17 (x31 x80) (x73 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . (x79 x81 ⟶ False) ⟶ (x79 x80 ⟶ False) ⟶ x79 (x21 x81 x80) ⟶ False) ⟶ (∀ x80 x81 . x13 x81 ⟶ x66 x81 ⟶ x13 x80 ⟶ x66 x80 ⟶ (x66 (x4 x81 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 . (x2 (x34 x80) x80 ⟶ False) ⟶ False) ⟶ ((x60 x52 ⟶ False) ⟶ False) ⟶ ((x9 x35 ⟶ False) ⟶ False) ⟶ ((x32 x51 ⟶ False) ⟶ False) ⟶ ((x71 x36 ⟶ False) ⟶ False) ⟶ (∀ x80 . x32 x80 ⟶ (x2 (x31 x80) (x1 (x21 (x73 x80) (x73 x80))) ⟶ False) ⟶ False) ⟶ (∀ x80 . x71 x80 ⟶ (x2 (x27 x80) (x1 (x21 (x73 x80) (x73 x80))) ⟶ False) ⟶ False) ⟶ ((x79 x50 ⟶ False) ⟶ False) ⟶ (∀ x80 . x60 x80 ⟶ (x32 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x60 x80 ⟶ (x71 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x32 x80 ⟶ (x9 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x71 x80 ⟶ (x9 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x60 x81 ⟶ (x60 (x28 x81 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x60 x81 ⟶ (x24 (x28 x81 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 . x2 x81 (x1 (x21 x82 x82)) ⟶ x2 x80 (x1 (x21 x82 x82)) ⟶ (x60 (x59 x82 x81 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 . x2 x81 (x1 (x21 x82 x82)) ⟶ x2 x80 (x1 (x21 x82 x82)) ⟶ (x24 (x59 x82 x81 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 . (x0 (x37 x80 x81 x82) x82 ⟶ False) ⟶ (x0 (x37 x80 x81 x82) x81 ⟶ False) ⟶ (x0 (x37 x80 x81 x82) x80 ⟶ False) ⟶ (x80 = x4 x82 x81 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 . x0 (x37 x80 x81 x82) x80 ⟶ x0 (x37 x80 x81 x82) x81 ⟶ (x80 = x4 x82 x81 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 . x0 (x37 x80 x81 x82) x80 ⟶ x0 (x37 x80 x81 x82) x82 ⟶ (x80 = x4 x82 x81 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 x83 . x82 = x4 x80 x81 ⟶ x0 x83 x81 ⟶ (x0 x83 x82 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 x83 . x82 = x4 x81 x80 ⟶ x0 x83 x81 ⟶ (x0 x83 x82 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 x83 . x83 = x4 x81 x82 ⟶ x0 x80 x83 ⟶ (x0 x80 x81 ⟶ False) ⟶ (x0 x80 x82 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 . x60 x82 ⟶ x24 x80 ⟶ x60 x80 ⟶ x73 x80 = x4 (x55 x81) (x73 x82) ⟶ x27 x80 = x4 (x21 (x55 x81) (x73 x80)) (x27 x82) ⟶ x31 x80 = x4 (x4 (x21 (x55 x81) (x73 x80)) (x21 (x73 x80) (x55 x81))) (x31 x82) ⟶ (x80 = x28 x82 x81 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 . x60 x82 ⟶ x24 x80 ⟶ x60 x80 ⟶ x80 = x28 x82 x81 ⟶ (x31 x80 = x4 (x4 (x21 (x55 x81) (x73 x80)) (x21 (x73 x80) (x55 x81))) (x31 x82) ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 . x60 x82 ⟶ x24 x80 ⟶ x60 x80 ⟶ x80 = x28 x82 x81 ⟶ (x27 x80 = x4 (x21 (x55 x81) (x73 x80)) (x27 x82) ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 . x60 x82 ⟶ x24 x80 ⟶ x60 x80 ⟶ x80 = x28 x82 x81 ⟶ (x73 x80 = x4 (x55 x81) (x73 x82) ⟶ False) ⟶ False) ⟶ ((x78 = x50 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . (x49 x81 x80 = x80 ⟶ False) ⟶ (x0 (x49 x81 x80) x81 ⟶ False) ⟶ (x81 = x55 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x0 (x49 x81 x80) x81 ⟶ x49 x81 x80 = x80 ⟶ (x81 = x55 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 . x81 = x55 x82 ⟶ x80 = x82 ⟶ (x0 x80 x81 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 . x81 = x55 x82 ⟶ x0 x80 x81 ⟶ (x80 = x82 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . (x4 x81 x80 = x4 x80 x81 ⟶ False) ⟶ False) ⟶ (∀ x80 . x9 x80 ⟶ x38 x80 x78 ⟶ (x7 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x9 x80 ⟶ x7 x80 ⟶ (x38 x80 x78 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x79 x81 ⟶ x13 x80 ⟶ x11 x80 x81 ⟶ (x11 x80 x81 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x79 x81 ⟶ x13 x80 ⟶ x11 x80 x81 ⟶ (x13 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x79 x81 ⟶ x13 x80 ⟶ x11 x80 x81 ⟶ (x79 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x9 x80 ⟶ (x58 x80 ⟶ False) ⟶ x65 x80 ⟶ False) ⟶ (∀ x80 x81 . x79 x81 ⟶ x13 x80 ⟶ x72 x80 x81 ⟶ (x72 x80 x81 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x79 x81 ⟶ x13 x80 ⟶ x72 x80 x81 ⟶ (x13 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x79 x81 ⟶ x13 x80 ⟶ x72 x80 x81 ⟶ (x79 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x9 x80 ⟶ x65 x80 ⟶ (x58 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 . x13 x82 ⟶ x11 x82 x80 ⟶ x2 x81 (x1 x82) ⟶ (x11 x81 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x76 x81 ⟶ x2 x80 (x1 x81) ⟶ (x76 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x9 x80 ⟶ (x58 x80 ⟶ False) ⟶ x58 x80 ⟶ False) ⟶ (∀ x80 . x9 x80 ⟶ (x58 x80 ⟶ False) ⟶ x7 x80 ⟶ False) ⟶ (∀ x80 . x13 x80 ⟶ x39 x80 ⟶ (x40 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x13 x80 ⟶ x39 x80 ⟶ (x20 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x13 x80 ⟶ x39 x80 ⟶ (x13 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 . x13 x82 ⟶ x72 x82 x80 ⟶ x2 x81 (x1 x82) ⟶ (x72 x81 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x13 x80 ⟶ x79 x80 ⟶ (x41 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x13 x80 ⟶ x79 x80 ⟶ (x48 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x13 x80 ⟶ x79 x80 ⟶ (x42 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x13 x80 ⟶ x79 x80 ⟶ (x13 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x79 x81 ⟶ x2 x80 (x1 x81) ⟶ x6 x80 x81 ⟶ False) ⟶ (∀ x80 . x9 x80 ⟶ x7 x80 ⟶ (x58 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x9 x80 ⟶ x7 x80 ⟶ (x7 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 . x79 x82 ⟶ x2 x80 (x1 (x21 x81 x82)) ⟶ (x79 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x13 x80 ⟶ x43 x80 ⟶ (x19 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x13 x80 ⟶ x43 x80 ⟶ (x56 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x13 x80 ⟶ x43 x80 ⟶ (x13 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x79 x80 ⟶ x13 x80 ⟶ (x15 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x79 x80 ⟶ x13 x80 ⟶ (x13 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x32 x80 ⟶ x7 x80 ⟶ (x30 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x32 x80 ⟶ x7 x80 ⟶ (x54 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x32 x80 ⟶ x7 x80 ⟶ (x33 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . (x79 x81 ⟶ False) ⟶ x2 x80 (x1 x81) ⟶ x79 x80 ⟶ (x6 x80 x81 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 . x79 x82 ⟶ x2 x80 (x1 (x21 x82 x81)) ⟶ (x79 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x13 x80 ⟶ x56 x80 ⟶ x67 x80 ⟶ (x43 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x13 x80 ⟶ x56 x80 ⟶ x67 x80 ⟶ (x13 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x79 x80 ⟶ x13 x80 ⟶ (x44 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x79 x80 ⟶ x13 x80 ⟶ (x13 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x32 x80 ⟶ x33 x80 ⟶ (x53 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x13 x80 ⟶ x66 x80 ⟶ x67 x80 ⟶ (x20 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x13 x80 ⟶ x66 x80 ⟶ x67 x80 ⟶ (x13 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x71 x80 ⟶ (x26 x80 ⟶ False) ⟶ x7 x80 ⟶ False) ⟶ (∀ x80 x81 . (x79 x81 ⟶ False) ⟶ x2 x80 (x1 x81) ⟶ (x6 x80 x81 ⟶ False) ⟶ x79 x80 ⟶ False) ⟶ (∀ x80 . x9 x80 ⟶ (x65 x80 ⟶ False) ⟶ x7 x80 ⟶ False) ⟶ (∀ x80 x81 x82 . x2 x82 (x1 (x21 x80 x81)) ⟶ (x11 x82 x81 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 . x2 x82 (x1 (x21 x81 x80)) ⟶ (x72 x82 x81 ⟶ False) ⟶ False) ⟶ (∀ x80 . x13 x80 ⟶ x66 x80 ⟶ x67 x80 ⟶ (x20 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x13 x80 ⟶ x66 x80 ⟶ x67 x80 ⟶ (x13 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x13 x81 ⟶ x2 x80 (x1 x81) ⟶ (x13 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 . (x79 x82 ⟶ False) ⟶ x79 x80 ⟶ x2 x81 (x1 (x21 x82 x80)) ⟶ x17 x81 x82 ⟶ False) ⟶ (∀ x80 x81 . x71 x81 ⟶ x2 x80 (x1 (x73 x81)) ⟶ x79 x80 ⟶ (x69 x80 x81 ⟶ False) ⟶ False) ⟶ (∀ x80 . x71 x80 ⟶ x7 x80 ⟶ (x26 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x13 x80 ⟶ x79 x80 ⟶ (x67 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x13 x80 ⟶ x79 x80 ⟶ (x39 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x13 x80 ⟶ x79 x80 ⟶ (x40 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x13 x80 ⟶ x79 x80 ⟶ (x43 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x13 x80 ⟶ x79 x80 ⟶ (x19 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x13 x80 ⟶ x79 x80 ⟶ (x66 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x13 x80 ⟶ x79 x80 ⟶ (x56 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x13 x80 ⟶ x79 x80 ⟶ (x20 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x13 x80 ⟶ x79 x80 ⟶ (x13 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x79 x81 ⟶ x2 x80 (x1 x81) ⟶ (x79 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x9 x80 ⟶ x7 x80 ⟶ (x65 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 . x2 x82 (x1 (x21 x80 x81)) ⟶ (x13 x82 ⟶ False) ⟶ False) ⟶ (∀ x80 . x79 x80 ⟶ x13 x80 ⟶ (x67 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x79 x80 ⟶ x13 x80 ⟶ (x39 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x79 x80 ⟶ x13 x80 ⟶ (x40 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x79 x80 ⟶ x13 x80 ⟶ (x43 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x79 x80 ⟶ x13 x80 ⟶ (x19 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x79 x80 ⟶ x13 x80 ⟶ (x66 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x79 x80 ⟶ x13 x80 ⟶ (x56 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x79 x80 ⟶ x13 x80 ⟶ (x20 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x79 x80 ⟶ x13 x80 ⟶ (x13 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x79 x80 ⟶ (x13 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x71 x80 ⟶ x7 x80 ⟶ (x29 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 . x79 x82 ⟶ x2 x80 (x1 (x21 x82 x81)) ⟶ (x17 x80 x82 ⟶ False) ⟶ False) ⟶ (∀ x80 . x9 x80 ⟶ (x65 x80 ⟶ False) ⟶ x7 x80 ⟶ False) ⟶ (∀ x80 . x9 x80 ⟶ x38 x80 x77 ⟶ (x65 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x9 x80 ⟶ x38 x80 x77 ⟶ x7 x80 ⟶ False) ⟶ (∀ x80 . x9 x80 ⟶ (x7 x80 ⟶ False) ⟶ x65 x80 ⟶ (x38 x80 x77 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x0 x80 x81 ⟶ x0 x81 x80 ⟶ False) ⟶ (∀ x80 . x60 x80 ⟶ x24 x80 ⟶ (x80 = x59 (x73 x80) (x27 x80) (x31 x80) ⟶ False) ⟶ False) ⟶ (x0 x45 (x73 x46) ⟶ False) ⟶ (x45 = x47 ⟶ False) ⟶ ((x2 x45 (x73 (x28 x46 x47)) ⟶ False) ⟶ False) ⟶ ((x60 x46 ⟶ False) ⟶ False) ⟶ False (proof)