Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrNUD../5a5a7..
PUfzD../067b3..
vout
PrNUD../f73bb.. 0.04 bars
TMKpu../0e837.. ownership of 1e19a.. as prop with payaddr PrPhD.. rights free controlledby PrPhD.. upto 0
TMFJK../cdb76.. ownership of f6e8f.. as prop with payaddr PrPhD.. rights free controlledby PrPhD.. upto 0
PUdUJ../abc54.. doc published by PrPhD..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0 ⟶ False
Theorem 1e19a.. : ∀ 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 . x75 x77 ⟶ (x77 = x76 ⟶ False) ⟶ x75 x76 ⟶ False) ⟶ (∀ x76 x77 . x0 x76 x77 ⟶ x75 x77 ⟶ False) ⟶ (∀ x76 . x75 x76 ⟶ (x76 = x74 ⟶ False) ⟶ False) ⟶ (∀ x76 x77 x78 . x0 x76 x77 ⟶ x2 x77 (x1 x78) ⟶ x75 x78 ⟶ False) ⟶ (∀ x76 x77 x78 . x0 x77 x78 ⟶ x2 x78 (x1 x76) ⟶ (x2 x77 x76 ⟶ False) ⟶ False) ⟶ (∀ x76 x77 . x3 x77 x76 ⟶ (x2 x77 (x1 x76) ⟶ False) ⟶ False) ⟶ (∀ x76 x77 . x2 x77 (x1 x76) ⟶ (x3 x77 x76 ⟶ False) ⟶ False) ⟶ (∀ x76 x77 . x2 x76 x77 ⟶ (x75 x77 ⟶ False) ⟶ (x0 x76 x77 ⟶ False) ⟶ False) ⟶ (∀ x76 . (x73 x76 x74 = x74 ⟶ False) ⟶ False) ⟶ (∀ x76 x77 . x0 x77 x76 ⟶ (x2 x77 x76 ⟶ False) ⟶ False) ⟶ (x75 x72 ⟶ False) ⟶ (∀ x76 . (x3 x76 x76 ⟶ False) ⟶ False) ⟶ (∀ x76 x77 x78 . x2 x77 (x1 x78) ⟶ (x71 x78 x76 x77 = x73 x76 x77 ⟶ False) ⟶ False) ⟶ (∀ x76 . x4 x76 ⟶ x7 x76 ⟶ (x5 (x6 x76) x76 ⟶ False) ⟶ False) ⟶ (∀ x76 . x4 x76 ⟶ x7 x76 ⟶ (x2 (x6 x76) (x1 (x70 x76)) ⟶ False) ⟶ False) ⟶ (∀ x76 . (x8 x76 ⟶ False) ⟶ x4 x76 ⟶ x7 x76 ⟶ (x10 (x9 x76) x76 ⟶ False) ⟶ False) ⟶ (∀ x76 . (x8 x76 ⟶ False) ⟶ x4 x76 ⟶ x7 x76 ⟶ x75 (x9 x76) ⟶ False) ⟶ (∀ x76 . (x8 x76 ⟶ False) ⟶ x4 x76 ⟶ x7 x76 ⟶ (x2 (x9 x76) (x1 (x70 x76)) ⟶ False) ⟶ False) ⟶ (∀ x76 . (x8 x76 ⟶ False) ⟶ x4 x76 ⟶ x7 x76 ⟶ x68 (x69 x76) x76 ⟶ False) ⟶ (∀ x76 . (x8 x76 ⟶ False) ⟶ x4 x76 ⟶ x7 x76 ⟶ x75 (x69 x76) ⟶ False) ⟶ (∀ x76 . (x8 x76 ⟶ False) ⟶ x4 x76 ⟶ x7 x76 ⟶ (x2 (x69 x76) (x1 (x70 x76)) ⟶ False) ⟶ False) ⟶ (∀ x76 . (x11 x76 ⟶ False) ⟶ x11 (x12 x76) ⟶ False) ⟶ (∀ x76 . (x11 x76 ⟶ False) ⟶ (x2 (x12 x76) (x1 x76) ⟶ False) ⟶ False) ⟶ (∀ x76 . x4 x76 ⟶ x7 x76 ⟶ (x10 (x13 x76) x76 ⟶ False) ⟶ False) ⟶ (∀ x76 . x4 x76 ⟶ x7 x76 ⟶ (x2 (x13 x76) (x1 (x70 x76)) ⟶ False) ⟶ False) ⟶ (∀ x76 . x7 x76 ⟶ (x68 (x14 x76) x76 ⟶ False) ⟶ False) ⟶ (∀ x76 . x7 x76 ⟶ (x2 (x14 x76) (x1 (x70 x76)) ⟶ False) ⟶ False) ⟶ (∀ x76 . (x75 x76 ⟶ False) ⟶ (x11 (x15 x76) ⟶ False) ⟶ False) ⟶ (∀ x76 . (x75 x76 ⟶ False) ⟶ x75 (x15 x76) ⟶ False) ⟶ (∀ x76 . (x75 x76 ⟶ False) ⟶ (x2 (x15 x76) (x1 x76) ⟶ False) ⟶ False) ⟶ (∀ x76 . x4 x76 ⟶ x7 x76 ⟶ (x4 (x67 x76) ⟶ False) ⟶ False) ⟶ (∀ x76 . x4 x76 ⟶ x7 x76 ⟶ (x16 (x67 x76) ⟶ False) ⟶ False) ⟶ (∀ x76 . x4 x76 ⟶ x7 x76 ⟶ (x66 (x67 x76) x76 ⟶ False) ⟶ False) ⟶ (∀ x76 . x7 x76 ⟶ (x18 (x17 x76) x76 ⟶ False) ⟶ False) ⟶ (∀ x76 . x7 x76 ⟶ (x2 (x17 x76) (x1 (x70 x76)) ⟶ False) ⟶ False) ⟶ (∀ x76 . (x75 x76 ⟶ False) ⟶ (x20 (x19 x76) x76 ⟶ False) ⟶ False) ⟶ (∀ x76 . (x75 x76 ⟶ False) ⟶ (x2 (x19 x76) (x1 x76) ⟶ False) ⟶ False) ⟶ (∀ x76 . (x8 x76 ⟶ False) ⟶ x22 x76 ⟶ x75 (x21 x76) ⟶ False) ⟶ (∀ x76 . (x8 x76 ⟶ False) ⟶ x22 x76 ⟶ (x2 (x21 x76) (x1 (x70 x76)) ⟶ False) ⟶ False) ⟶ (∀ x76 . (x8 x76 ⟶ False) ⟶ x7 x76 ⟶ (x16 (x23 x76) ⟶ False) ⟶ False) ⟶ (∀ x76 . (x8 x76 ⟶ False) ⟶ x7 x76 ⟶ x8 (x23 x76) ⟶ False) ⟶ (∀ x76 . (x8 x76 ⟶ False) ⟶ x7 x76 ⟶ (x66 (x23 x76) x76 ⟶ False) ⟶ False) ⟶ (∀ x76 . (x8 x76 ⟶ False) ⟶ x4 x76 ⟶ x7 x76 ⟶ (x10 (x65 x76) x76 ⟶ False) ⟶ False) ⟶ (∀ x76 . (x8 x76 ⟶ False) ⟶ x4 x76 ⟶ x7 x76 ⟶ (x24 (x65 x76) x76 ⟶ False) ⟶ False) ⟶ (∀ x76 . (x8 x76 ⟶ False) ⟶ x4 x76 ⟶ x7 x76 ⟶ x75 (x65 x76) ⟶ False) ⟶ (∀ x76 . (x8 x76 ⟶ False) ⟶ x4 x76 ⟶ x7 x76 ⟶ (x2 (x65 x76) (x1 (x70 x76)) ⟶ False) ⟶ False) ⟶ (∀ x76 . x20 (x64 x76) x76 ⟶ False) ⟶ (∀ x76 . (x2 (x64 x76) (x1 x76) ⟶ False) ⟶ False) ⟶ (∀ x76 . x7 x76 ⟶ (x16 (x63 x76) ⟶ False) ⟶ False) ⟶ (∀ x76 . x7 x76 ⟶ (x66 (x63 x76) x76 ⟶ False) ⟶ False) ⟶ (x75 x62 ⟶ False) ⟶ (∀ x76 . x4 x76 ⟶ x7 x76 ⟶ (x10 (x25 x76) x76 ⟶ False) ⟶ False) ⟶ (∀ x76 . x4 x76 ⟶ x7 x76 ⟶ (x24 (x25 x76) x76 ⟶ False) ⟶ False) ⟶ (∀ x76 . x4 x76 ⟶ x7 x76 ⟶ (x2 (x25 x76) (x1 (x70 x76)) ⟶ False) ⟶ False) ⟶ (∀ x76 . (x75 (x61 x76) ⟶ False) ⟶ False) ⟶ (∀ x76 . (x2 (x61 x76) (x1 x76) ⟶ False) ⟶ False) ⟶ ((x4 x60 ⟶ False) ⟶ False) ⟶ ((x16 x60 ⟶ False) ⟶ False) ⟶ (x8 x60 ⟶ False) ⟶ ((x7 x60 ⟶ False) ⟶ False) ⟶ (∀ x76 . (x59 x76 ⟶ False) ⟶ x22 x76 ⟶ x11 (x58 x76) ⟶ False) ⟶ (∀ x76 . (x59 x76 ⟶ False) ⟶ x22 x76 ⟶ (x2 (x58 x76) (x1 (x70 x76)) ⟶ False) ⟶ False) ⟶ (∀ x76 . (x8 x76 ⟶ False) ⟶ x22 x76 ⟶ (x11 (x57 x76) ⟶ False) ⟶ False) ⟶ (∀ x76 . (x8 x76 ⟶ False) ⟶ x22 x76 ⟶ x75 (x57 x76) ⟶ False) ⟶ (∀ x76 . (x8 x76 ⟶ False) ⟶ x22 x76 ⟶ (x2 (x57 x76) (x1 (x70 x76)) ⟶ False) ⟶ False) ⟶ ((x75 x26 ⟶ False) ⟶ False) ⟶ (∀ x76 . x4 x76 ⟶ x7 x76 ⟶ (x24 (x56 x76) x76 ⟶ False) ⟶ False) ⟶ (∀ x76 . x4 x76 ⟶ x7 x76 ⟶ (x2 (x56 x76) (x1 (x70 x76)) ⟶ False) ⟶ False) ⟶ (∀ x76 . (x75 x76 ⟶ False) ⟶ x75 (x55 x76) ⟶ False) ⟶ (∀ x76 . (x75 x76 ⟶ False) ⟶ (x2 (x55 x76) (x1 x76) ⟶ False) ⟶ False) ⟶ ((x16 x54 ⟶ False) ⟶ False) ⟶ ((x7 x54 ⟶ False) ⟶ False) ⟶ (∀ x76 . x7 x76 ⟶ (x75 (x53 x76) ⟶ False) ⟶ False) ⟶ (∀ x76 . x7 x76 ⟶ (x2 (x53 x76) (x1 (x70 x76)) ⟶ False) ⟶ False) ⟶ ((x4 x52 ⟶ False) ⟶ False) ⟶ ((x16 x52 ⟶ False) ⟶ False) ⟶ ((x8 x52 ⟶ False) ⟶ False) ⟶ ((x7 x52 ⟶ False) ⟶ False) ⟶ ((x16 x51 ⟶ False) ⟶ False) ⟶ ((x8 x51 ⟶ False) ⟶ False) ⟶ ((x7 x51 ⟶ False) ⟶ False) ⟶ (∀ x76 . x4 x76 ⟶ x7 x76 ⟶ (x24 (x27 x76) x76 ⟶ False) ⟶ False) ⟶ (∀ x76 . x4 x76 ⟶ x7 x76 ⟶ (x2 (x27 x76) (x1 (x70 x76)) ⟶ False) ⟶ False) ⟶ (∀ x76 x77 . x7 x77 ⟶ x2 x76 (x1 (x70 x77)) ⟶ (x28 x77 (x28 x77 x76) = x28 x77 x76 ⟶ False) ⟶ False) ⟶ (∀ x76 x77 x78 x79 . (x8 x79 ⟶ False) ⟶ x4 x79 ⟶ x7 x79 ⟶ x66 x76 x79 ⟶ x2 x78 (x1 (x70 x79)) ⟶ x2 x77 (x1 (x70 x76)) ⟶ x78 = x77 ⟶ (x3 (x71 (x70 x76) (x28 x79 x78) (x50 x76)) (x28 x76 x77) ⟶ False) ⟶ False) ⟶ (∀ x76 x77 x78 . x2 x76 (x1 x78) ⟶ (x71 x78 x77 x77 = x77 ⟶ False) ⟶ False) ⟶ (∀ x76 . (x73 x76 x76 = x76 ⟶ False) ⟶ False) ⟶ (∀ x76 x77 x78 x79 . x2 x78 (x1 (x1 x79)) ⟶ x29 x79 x78 = x29 x77 x76 ⟶ (x78 = x76 ⟶ False) ⟶ False) ⟶ (∀ x76 x77 x78 x79 . x2 x78 (x1 (x1 x79)) ⟶ x29 x79 x78 = x29 x76 x77 ⟶ (x79 = x76 ⟶ False) ⟶ False) ⟶ (∀ x76 x77 . x4 x77 ⟶ x7 x77 ⟶ x2 x76 (x1 (x70 x77)) ⟶ (x24 (x28 x77 x76) x77 ⟶ False) ⟶ False) ⟶ (∀ x76 . (x49 x76 ⟶ False) ⟶ x22 x76 ⟶ x48 (x70 x76) ⟶ False) ⟶ (∀ x76 x77 . (x75 x77 ⟶ False) ⟶ x2 x76 (x1 (x1 x77)) ⟶ (x16 (x29 x77 x76) ⟶ False) ⟶ False) ⟶ (∀ x76 x77 . (x75 x77 ⟶ False) ⟶ x2 x76 (x1 (x1 x77)) ⟶ x8 (x29 x77 x76) ⟶ False) ⟶ (∀ x76 . x49 x76 ⟶ x22 x76 ⟶ (x48 (x70 x76) ⟶ False) ⟶ False) ⟶ (∀ x76 x77 . x7 x77 ⟶ x75 x76 ⟶ x2 x76 (x1 (x70 x77)) ⟶ (x16 (x47 x77 x76) ⟶ False) ⟶ False) ⟶ (∀ x76 x77 . x7 x77 ⟶ x75 x76 ⟶ x2 x76 (x1 (x70 x77)) ⟶ (x8 (x47 x77 x76) ⟶ False) ⟶ False) ⟶ (∀ x76 . x59 x76 ⟶ x22 x76 ⟶ (x11 (x70 x76) ⟶ False) ⟶ False) ⟶ (∀ x76 . (x8 x76 ⟶ False) ⟶ x7 x76 ⟶ (x16 (x29 (x70 x76) (x30 x76)) ⟶ False) ⟶ False) ⟶ (∀ x76 . (x8 x76 ⟶ False) ⟶ x7 x76 ⟶ x8 (x29 (x70 x76) (x30 x76)) ⟶ False) ⟶ (∀ x76 x77 x78 . x4 x78 ⟶ x7 x78 ⟶ x24 x77 x78 ⟶ x2 x77 (x1 (x70 x78)) ⟶ x24 x76 x78 ⟶ x2 x76 (x1 (x70 x78)) ⟶ (x24 (x73 x77 x76) x78 ⟶ False) ⟶ False) ⟶ (∀ x76 . (x59 x76 ⟶ False) ⟶ x22 x76 ⟶ x11 (x70 x76) ⟶ False) ⟶ (∀ x76 . x4 x76 ⟶ x7 x76 ⟶ (x4 (x29 (x70 x76) (x30 x76)) ⟶ False) ⟶ False) ⟶ (∀ x76 . x4 x76 ⟶ x7 x76 ⟶ (x16 (x29 (x70 x76) (x30 x76)) ⟶ False) ⟶ False) ⟶ (∀ x76 . (x8 x76 ⟶ False) ⟶ x22 x76 ⟶ x75 (x50 x76) ⟶ False) ⟶ (∀ x76 x77 x78 . x4 x78 ⟶ x7 x78 ⟶ x10 x77 x78 ⟶ x2 x77 (x1 (x70 x78)) ⟶ x10 x76 x78 ⟶ x2 x76 (x1 (x70 x78)) ⟶ (x10 (x73 x77 x76) x78 ⟶ False) ⟶ False) ⟶ (∀ x76 . x8 x76 ⟶ x22 x76 ⟶ (x75 (x50 x76) ⟶ False) ⟶ False) ⟶ (∀ x76 . x4 x76 ⟶ x7 x76 ⟶ (x10 (x50 x76) x76 ⟶ False) ⟶ False) ⟶ (∀ x76 x77 . x4 x77 ⟶ x7 x77 ⟶ x2 x76 (x1 (x70 x77)) ⟶ (x4 (x47 x77 x76) ⟶ False) ⟶ False) ⟶ (∀ x76 x77 . x4 x77 ⟶ x7 x77 ⟶ x2 x76 (x1 (x70 x77)) ⟶ (x16 (x47 x77 x76) ⟶ False) ⟶ False) ⟶ (∀ x76 . (x8 x76 ⟶ False) ⟶ x22 x76 ⟶ x75 (x70 x76) ⟶ False) ⟶ (∀ x76 x77 . (x8 x77 ⟶ False) ⟶ x7 x77 ⟶ (x75 x76 ⟶ False) ⟶ x2 x76 (x1 (x70 x77)) ⟶ (x16 (x47 x77 x76) ⟶ False) ⟶ False) ⟶ (∀ x76 x77 . (x8 x77 ⟶ False) ⟶ x7 x77 ⟶ (x75 x76 ⟶ False) ⟶ x2 x76 (x1 (x70 x77)) ⟶ x8 (x47 x77 x76) ⟶ False) ⟶ ((x75 x74 ⟶ False) ⟶ False) ⟶ (∀ x76 . x75 (x1 x76) ⟶ False) ⟶ (∀ x76 . x8 x76 ⟶ x22 x76 ⟶ (x75 (x70 x76) ⟶ False) ⟶ False) ⟶ (∀ x76 . x4 x76 ⟶ x7 x76 ⟶ x75 (x30 x76) ⟶ False) ⟶ (∀ x76 . (x8 x76 ⟶ False) ⟶ x4 x76 ⟶ x7 x76 ⟶ x68 (x50 x76) x76 ⟶ False) ⟶ (∀ x76 x77 . x7 x77 ⟶ x68 x76 x77 ⟶ x2 x76 (x1 (x70 x77)) ⟶ (x75 (x28 x77 x76) ⟶ False) ⟶ False) ⟶ (∀ x76 . x7 x76 ⟶ (x18 (x50 x76) x76 ⟶ False) ⟶ False) ⟶ (∀ x76 . x22 x76 ⟶ x20 (x50 x76) (x70 x76) ⟶ False) ⟶ (∀ x76 . x4 x76 ⟶ x7 x76 ⟶ (x24 (x50 x76) x76 ⟶ False) ⟶ False) ⟶ (∀ x76 . (x2 (x31 x76) x76 ⟶ False) ⟶ False) ⟶ (∀ x76 . x7 x76 ⟶ (x66 (x46 x76) x76 ⟶ False) ⟶ False) ⟶ (∀ x76 x77 . (x8 x77 ⟶ False) ⟶ x4 x77 ⟶ x7 x77 ⟶ x2 x76 (x70 x77) ⟶ (x33 (x32 x76 x77) x77 x76 ⟶ False) ⟶ False) ⟶ ((x22 x45 ⟶ False) ⟶ False) ⟶ ((x7 x34 ⟶ False) ⟶ False) ⟶ (∀ x76 . x7 x76 ⟶ (x2 (x30 x76) (x1 (x1 (x70 x76))) ⟶ False) ⟶ False) ⟶ (∀ x76 x77 . x7 x77 ⟶ x66 x76 x77 ⟶ (x7 x76 ⟶ False) ⟶ False) ⟶ (∀ x76 x77 x78 . (x8 x78 ⟶ False) ⟶ x4 x78 ⟶ x7 x78 ⟶ x2 x76 (x70 x78) ⟶ x33 x77 x78 x76 ⟶ (x2 x77 (x1 (x70 x78)) ⟶ False) ⟶ False) ⟶ (∀ x76 . x7 x76 ⟶ (x22 x76 ⟶ False) ⟶ False) ⟶ (∀ x76 x77 x78 . x2 x77 (x1 x78) ⟶ (x2 (x71 x78 x76 x77) (x1 x78) ⟶ False) ⟶ False) ⟶ (∀ x76 . x22 x76 ⟶ (x2 (x50 x76) (x1 (x70 x76)) ⟶ False) ⟶ False) ⟶ (∀ x76 x77 . x7 x77 ⟶ x2 x76 (x1 (x70 x77)) ⟶ (x2 (x28 x77 x76) (x1 (x70 x77)) ⟶ False) ⟶ False) ⟶ (∀ x76 x77 . x7 x77 ⟶ x2 x76 (x1 (x70 x77)) ⟶ (x66 (x47 x77 x76) x77 ⟶ False) ⟶ False) ⟶ (∀ x76 x77 . x7 x77 ⟶ x2 x76 (x1 (x70 x77)) ⟶ (x16 (x47 x77 x76) ⟶ False) ⟶ False) ⟶ (∀ x76 x77 . x2 x77 (x1 (x1 x76)) ⟶ (x7 (x29 x76 x77) ⟶ False) ⟶ False) ⟶ (∀ x76 x77 . x2 x77 (x1 (x1 x76)) ⟶ (x16 (x29 x76 x77) ⟶ False) ⟶ False) ⟶ (∀ x76 x77 x78 . (x0 (x35 x76 x77 x78) x77 ⟶ False) ⟶ (x0 (x35 x76 x77 x78) x76 ⟶ False) ⟶ (x76 = x73 x78 x77 ⟶ False) ⟶ False) ⟶ (∀ x76 x77 x78 . (x0 (x35 x76 x77 x78) x78 ⟶ False) ⟶ (x0 (x35 x76 x77 x78) x76 ⟶ False) ⟶ (x76 = x73 x78 x77 ⟶ False) ⟶ False) ⟶ (∀ x76 x77 x78 . x0 (x35 x76 x77 x78) x76 ⟶ x0 (x35 x76 x77 x78) x78 ⟶ x0 (x35 x76 x77 x78) x77 ⟶ (x76 = x73 x78 x77 ⟶ False) ⟶ False) ⟶ (∀ x76 x77 x78 x79 . x79 = x73 x77 x78 ⟶ x0 x76 x77 ⟶ x0 x76 x78 ⟶ (x0 x76 x79 ⟶ False) ⟶ False) ⟶ (∀ x76 x77 x78 x79 . x77 = x73 x76 x78 ⟶ x0 x79 x77 ⟶ (x0 x79 x78 ⟶ False) ⟶ False) ⟶ (∀ x76 x77 x78 x79 . x77 = x73 x78 x76 ⟶ x0 x79 x77 ⟶ (x0 x79 x78 ⟶ False) ⟶ False) ⟶ (∀ x76 . x22 x76 ⟶ (x50 x76 = x70 x76 ⟶ False) ⟶ False) ⟶ (∀ x76 x77 x78 . (x8 x78 ⟶ False) ⟶ x4 x78 ⟶ x7 x78 ⟶ x2 x76 (x70 x78) ⟶ x2 x77 (x1 (x70 x78)) ⟶ x0 x76 (x28 x78 x77) ⟶ (x33 x77 x78 x76 ⟶ False) ⟶ False) ⟶ (∀ x76 x77 x78 . (x8 x78 ⟶ False) ⟶ x4 x78 ⟶ x7 x78 ⟶ x2 x76 (x70 x78) ⟶ x2 x77 (x1 (x70 x78)) ⟶ x33 x77 x78 x76 ⟶ (x0 x76 (x28 x78 x77) ⟶ False) ⟶ False) ⟶ (∀ x76 x77 x78 . x2 x77 (x1 x78) ⟶ (x71 x78 x76 x77 = x71 x78 x77 x76 ⟶ False) ⟶ False) ⟶ (∀ x76 x77 . (x73 x77 x76 = x73 x76 x77 ⟶ False) ⟶ False) ⟶ (∀ x76 . x22 x76 ⟶ x44 x76 x74 ⟶ (x8 x76 ⟶ False) ⟶ False) ⟶ (∀ x76 . x7 x76 ⟶ x8 x76 ⟶ (x36 x76 ⟶ False) ⟶ False) ⟶ (∀ x76 . x22 x76 ⟶ x8 x76 ⟶ (x44 x76 x74 ⟶ False) ⟶ False) ⟶ (∀ x76 . x22 x76 ⟶ (x49 x76 ⟶ False) ⟶ x59 x76 ⟶ False) ⟶ (∀ x76 x77 . x4 x77 ⟶ x7 x77 ⟶ x2 x76 (x1 (x70 x77)) ⟶ x24 x76 x77 ⟶ x5 x76 x77 ⟶ (x75 x76 ⟶ False) ⟶ False) ⟶ (∀ x76 . x22 x76 ⟶ x59 x76 ⟶ (x49 x76 ⟶ False) ⟶ False) ⟶ (∀ x76 x77 . x4 x77 ⟶ x7 x77 ⟶ x2 x76 (x1 (x70 x77)) ⟶ x10 x76 x77 ⟶ x68 x76 x77 ⟶ (x5 x76 x77 ⟶ False) ⟶ False) ⟶ (∀ x76 x77 . x11 x77 ⟶ x2 x76 (x1 x77) ⟶ (x11 x76 ⟶ False) ⟶ False) ⟶ (∀ x76 . x22 x76 ⟶ (x49 x76 ⟶ False) ⟶ x49 x76 ⟶ False) ⟶ (∀ x76 . x22 x76 ⟶ (x49 x76 ⟶ False) ⟶ x8 x76 ⟶ False) ⟶ (∀ x76 x77 . x4 x77 ⟶ x7 x77 ⟶ x2 x76 (x1 (x70 x77)) ⟶ x5 x76 x77 ⟶ (x68 x76 x77 ⟶ False) ⟶ False) ⟶ (∀ x76 x77 . x75 x77 ⟶ x2 x76 (x1 x77) ⟶ x20 x76 x77 ⟶ False) ⟶ (∀ x76 . x22 x76 ⟶ x8 x76 ⟶ (x49 x76 ⟶ False) ⟶ False) ⟶ (∀ x76 . x22 x76 ⟶ x8 x76 ⟶ (x8 x76 ⟶ False) ⟶ False) ⟶ (∀ x76 x77 . x7 x77 ⟶ x2 x76 (x1 (x70 x77)) ⟶ x75 x76 ⟶ (x43 x76 x77 ⟶ False) ⟶ False) ⟶ (∀ x76 x77 . x4 x77 ⟶ x7 x77 ⟶ x2 x76 (x1 (x70 x77)) ⟶ x75 x76 ⟶ (x5 x76 x77 ⟶ False) ⟶ False) ⟶ (∀ x76 x77 . (x75 x77 ⟶ False) ⟶ x2 x76 (x1 x77) ⟶ x75 x76 ⟶ (x20 x76 x77 ⟶ False) ⟶ False) ⟶ (∀ x76 x77 . x7 x77 ⟶ x2 x76 (x1 (x70 x77)) ⟶ x75 x76 ⟶ (x68 x76 x77 ⟶ False) ⟶ False) ⟶ (∀ x76 x77 . (x75 x77 ⟶ False) ⟶ x2 x76 (x1 x77) ⟶ (x20 x76 x77 ⟶ False) ⟶ x75 x76 ⟶ False) ⟶ (∀ x76 . x22 x76 ⟶ (x59 x76 ⟶ False) ⟶ x8 x76 ⟶ False) ⟶ (∀ x76 x77 . x4 x77 ⟶ x7 x77 ⟶ x2 x76 (x1 (x70 x77)) ⟶ x75 x76 ⟶ (x10 x76 x77 ⟶ False) ⟶ False) ⟶ (∀ x76 x77 . x4 x77 ⟶ x7 x77 ⟶ x2 x76 (x1 (x70 x77)) ⟶ x75 x76 ⟶ (x24 x76 x77 ⟶ False) ⟶ False) ⟶ (∀ x76 x77 . x75 x77 ⟶ x2 x76 (x1 x77) ⟶ (x75 x76 ⟶ False) ⟶ False) ⟶ (∀ x76 . x22 x76 ⟶ x8 x76 ⟶ (x59 x76 ⟶ False) ⟶ False) ⟶ (∀ x76 x77 . x4 x77 ⟶ x7 x77 ⟶ x66 x76 x77 ⟶ (x4 x76 ⟶ False) ⟶ False) ⟶ (∀ x76 . x22 x76 ⟶ (x59 x76 ⟶ False) ⟶ x8 x76 ⟶ False) ⟶ (∀ x76 . x22 x76 ⟶ x44 x76 x72 ⟶ (x59 x76 ⟶ False) ⟶ False) ⟶ (∀ x76 . x22 x76 ⟶ x44 x76 x72 ⟶ x8 x76 ⟶ False) ⟶ (∀ x76 . x22 x76 ⟶ (x8 x76 ⟶ False) ⟶ x59 x76 ⟶ (x44 x76 x72 ⟶ False) ⟶ False) ⟶ (∀ x76 x77 . x0 x76 x77 ⟶ x0 x77 x76 ⟶ False) ⟶ (∀ x76 . x7 x76 ⟶ x16 x76 ⟶ (x76 = x29 (x70 x76) (x30 x76) ⟶ False) ⟶ False) ⟶ (x33 x37 (x47 x38 x39) x40 ⟶ False) ⟶ ((x40 = x42 ⟶ False) ⟶ False) ⟶ ((x37 = x41 ⟶ False) ⟶ False) ⟶ ((x33 x41 x38 x42 ⟶ False) ⟶ False) ⟶ ((x2 x42 (x70 x38) ⟶ False) ⟶ False) ⟶ ((x2 x41 (x1 (x70 x38)) ⟶ False) ⟶ False) ⟶ ((x2 x37 (x1 (x70 (x47 x38 x39))) ⟶ False) ⟶ False) ⟶ ((x2 x40 (x70 (x47 x38 x39)) ⟶ False) ⟶ False) ⟶ ((x2 x39 (x1 (x70 x38)) ⟶ False) ⟶ False) ⟶ (x75 x39 ⟶ False) ⟶ ((x7 x38 ⟶ False) ⟶ False) ⟶ ((x4 x38 ⟶ False) ⟶ False) ⟶ (x8 x38 ⟶ False) ⟶ False (proof)