Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrPhD../b08a9..
PUS1v../ee6af..
vout
PrPhD../15ed5.. 102.65 bars
TML6G../bb209.. ownership of c048a.. as prop with payaddr PrPhD.. rights free controlledby PrPhD.. upto 0
TMTTd../a4754.. ownership of a065e.. as prop with payaddr PrPhD.. rights free controlledby PrPhD.. upto 0
PUQi7../25b58.. doc published by PrPhD..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0 ⟶ False
Theorem c048a.. : ∀ 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 . x65 x67 ⟶ (x67 = x66 ⟶ False) ⟶ x65 x66 ⟶ False) ⟶ (∀ x66 x67 . x0 x66 x67 ⟶ x65 x67 ⟶ False) ⟶ (∀ x66 . x65 x66 ⟶ (x66 = x64 ⟶ False) ⟶ False) ⟶ (∀ x66 x67 x68 . x0 x66 x67 ⟶ x2 x67 (x1 x68) ⟶ x65 x68 ⟶ False) ⟶ (∀ x66 x67 x68 . x0 x67 x68 ⟶ x2 x68 (x1 x66) ⟶ (x2 x67 x66 ⟶ False) ⟶ False) ⟶ (∀ x66 x67 . x3 x67 x66 ⟶ (x2 x67 (x1 x66) ⟶ False) ⟶ False) ⟶ (∀ x66 x67 . x2 x67 (x1 x66) ⟶ (x3 x67 x66 ⟶ False) ⟶ False) ⟶ (∀ x66 x67 . x2 x66 x67 ⟶ (x65 x67 ⟶ False) ⟶ (x0 x66 x67 ⟶ False) ⟶ False) ⟶ (∀ x66 x67 . x0 x67 x66 ⟶ (x2 x67 x66 ⟶ False) ⟶ False) ⟶ ((x2 x64 x4 ⟶ False) ⟶ False) ⟶ (∀ x66 x67 x68 x69 . (x65 x69 ⟶ False) ⟶ x54 x66 (x57 x56 x55) ⟶ x63 x66 ⟶ x59 x66 x69 x58 ⟶ x2 x66 (x1 (x62 x69 x58)) ⟶ x54 x67 (x57 x56 x55) ⟶ x63 x67 ⟶ x59 x67 x69 x58 ⟶ x2 x67 (x1 (x62 x69 x58)) ⟶ x54 x68 (x57 x56 x55) ⟶ x63 x68 ⟶ x59 x68 x69 x58 ⟶ x2 x68 (x1 (x62 x69 x58)) ⟶ x61 x66 x67 ⟶ x61 x68 x67 ⟶ (x61 (x60 x69 x66 x68) x67 ⟶ False) ⟶ False) ⟶ (∀ x66 x67 x68 . (x65 x68 ⟶ False) ⟶ x54 x66 (x57 x56 x55) ⟶ x63 x66 ⟶ x59 x66 x68 x58 ⟶ x2 x66 (x1 (x62 x68 x58)) ⟶ x54 x67 (x57 x56 x55) ⟶ x63 x67 ⟶ x59 x67 x68 x58 ⟶ x2 x67 (x1 (x62 x68 x58)) ⟶ (x61 x66 (x60 x68 x66 x67) ⟶ False) ⟶ False) ⟶ (∀ x66 x67 x68 . (x65 x68 ⟶ False) ⟶ x54 x66 (x57 x56 x55) ⟶ x63 x66 ⟶ x59 x66 x68 x58 ⟶ x2 x66 (x1 (x62 x68 x58)) ⟶ x54 x67 (x57 x56 x55) ⟶ x63 x67 ⟶ x59 x67 x68 x58 ⟶ x2 x67 (x1 (x62 x68 x58)) ⟶ (x61 (x53 x68 x66 x67) x66 ⟶ False) ⟶ False) ⟶ ((x2 x55 x58 ⟶ False) ⟶ False) ⟶ ((x2 x55 x52 ⟶ False) ⟶ False) ⟶ ((x5 x55 x58 x52 ⟶ False) ⟶ False) ⟶ ((x51 x55 ⟶ False) ⟶ False) ⟶ (x65 x55 ⟶ False) ⟶ (∀ x66 . (x3 x66 x66 ⟶ False) ⟶ False) ⟶ (∀ x66 x67 . x6 x67 ⟶ x63 x67 ⟶ x7 x67 ⟶ x6 x66 ⟶ x63 x66 ⟶ x7 x66 ⟶ (x61 x67 x67 ⟶ False) ⟶ False) ⟶ (∀ x66 x67 x68 . (x65 x68 ⟶ False) ⟶ (x65 x66 ⟶ False) ⟶ x2 x66 (x1 x68) ⟶ x2 x67 x66 ⟶ (x5 x67 x68 x66 ⟶ False) ⟶ False) ⟶ (∀ x66 x67 x68 . (x65 x68 ⟶ False) ⟶ (x65 x66 ⟶ False) ⟶ x2 x66 (x1 x68) ⟶ x5 x67 x68 x66 ⟶ (x2 x67 x66 ⟶ False) ⟶ False) ⟶ ((x56 = x64 ⟶ False) ⟶ False) ⟶ ((x52 = x4 ⟶ False) ⟶ False) ⟶ (∀ x66 x67 . x50 x67 ⟶ x50 x66 ⟶ (x57 x67 x66 = x49 x67 x66 ⟶ False) ⟶ False) ⟶ (∀ x66 . (x65 x66 ⟶ False) ⟶ (x9 (x8 x66) x66 ⟶ False) ⟶ False) ⟶ (∀ x66 . (x65 x66 ⟶ False) ⟶ (x2 (x8 x66) (x1 x66) ⟶ False) ⟶ False) ⟶ (∀ x66 . x9 (x10 x66) x66 ⟶ False) ⟶ (∀ x66 . (x2 (x10 x66) (x1 x66) ⟶ False) ⟶ False) ⟶ ((x11 x12 ⟶ False) ⟶ False) ⟶ ((x48 x12 ⟶ False) ⟶ False) ⟶ (x65 x12 ⟶ False) ⟶ (x65 x47 ⟶ False) ⟶ (∀ x66 . (x65 (x13 x66) ⟶ False) ⟶ False) ⟶ (∀ x66 . (x2 (x13 x66) (x1 x66) ⟶ False) ⟶ False) ⟶ ((x48 x14 ⟶ False) ⟶ False) ⟶ (x65 x14 ⟶ False) ⟶ ((x65 x15 ⟶ False) ⟶ False) ⟶ ((x46 x45 ⟶ False) ⟶ False) ⟶ ((x63 x45 ⟶ False) ⟶ False) ⟶ ((x6 x45 ⟶ False) ⟶ False) ⟶ (∀ x66 . (x65 x66 ⟶ False) ⟶ x65 (x16 x66) ⟶ False) ⟶ (∀ x66 . (x65 x66 ⟶ False) ⟶ (x2 (x16 x66) (x1 x66) ⟶ False) ⟶ False) ⟶ (∀ x66 x67 . (x54 (x17 x66 x67) x66 ⟶ False) ⟶ False) ⟶ (∀ x66 x67 . (x44 (x17 x67 x66) x66 ⟶ False) ⟶ False) ⟶ (∀ x66 x67 . (x6 (x17 x66 x67) ⟶ False) ⟶ False) ⟶ (∀ x66 x67 . (x65 (x17 x66 x67) ⟶ False) ⟶ False) ⟶ (∀ x66 x67 . (x2 (x17 x66 x67) (x1 (x62 x67 x66)) ⟶ False) ⟶ False) ⟶ ((x48 x43 ⟶ False) ⟶ False) ⟶ (x65 x43 ⟶ False) ⟶ ((x42 x41 ⟶ False) ⟶ False) ⟶ ((x18 x41 ⟶ False) ⟶ False) ⟶ ((x40 x41 ⟶ False) ⟶ False) ⟶ ((x19 x41 ⟶ False) ⟶ False) ⟶ (x65 x41 ⟶ False) ⟶ ((x2 x41 (x1 x58) ⟶ False) ⟶ False) ⟶ (∀ x66 x67 . (x65 x67 ⟶ False) ⟶ x54 x66 (x57 x56 x55) ⟶ x63 x66 ⟶ x59 x66 x67 x58 ⟶ x2 x66 (x1 (x62 x67 x58)) ⟶ (x39 x67 (x39 x67 x66) = x66 ⟶ False) ⟶ False) ⟶ (∀ x66 x67 x68 . (x65 x68 ⟶ False) ⟶ x54 x66 (x57 x56 x55) ⟶ x63 x66 ⟶ x59 x66 x68 x58 ⟶ x2 x66 (x1 (x62 x68 x58)) ⟶ x54 x67 (x57 x56 x55) ⟶ x63 x67 ⟶ x59 x67 x68 x58 ⟶ x2 x67 (x1 (x62 x68 x58)) ⟶ (x60 x68 x66 x66 = x66 ⟶ False) ⟶ False) ⟶ (∀ x66 x67 x68 . (x65 x68 ⟶ False) ⟶ x54 x66 (x57 x56 x55) ⟶ x63 x66 ⟶ x59 x66 x68 x58 ⟶ x2 x66 (x1 (x62 x68 x58)) ⟶ x54 x67 (x57 x56 x55) ⟶ x63 x67 ⟶ x59 x67 x68 x58 ⟶ x2 x67 (x1 (x62 x68 x58)) ⟶ (x53 x68 x66 x66 = x66 ⟶ False) ⟶ False) ⟶ (∀ x66 x67 . x48 x67 ⟶ (x46 (x62 x66 x67) ⟶ False) ⟶ False) ⟶ (x38 x58 ⟶ False) ⟶ (∀ x66 x67 . x20 x67 ⟶ (x54 (x62 x66 x67) x21 ⟶ False) ⟶ False) ⟶ (∀ x66 x67 . x37 x67 ⟶ (x54 (x62 x66 x67) x36 ⟶ False) ⟶ False) ⟶ (∀ x66 x67 . x18 x67 ⟶ (x7 (x62 x66 x67) ⟶ False) ⟶ False) ⟶ (∀ x66 x67 . x40 x67 ⟶ (x35 (x62 x66 x67) ⟶ False) ⟶ False) ⟶ (∀ x66 x67 . x19 x67 ⟶ (x22 (x62 x66 x67) ⟶ False) ⟶ False) ⟶ (x38 x36 ⟶ False) ⟶ (x38 x21 ⟶ False) ⟶ ((x48 x4 ⟶ False) ⟶ False) ⟶ ((x20 x21 ⟶ False) ⟶ False) ⟶ ((x11 x4 ⟶ False) ⟶ False) ⟶ ((x11 x21 ⟶ False) ⟶ False) ⟶ ((x11 x36 ⟶ False) ⟶ False) ⟶ ((x11 x58 ⟶ False) ⟶ False) ⟶ (x65 x21 ⟶ False) ⟶ ((x37 x36 ⟶ False) ⟶ False) ⟶ (x65 x36 ⟶ False) ⟶ ((x18 x58 ⟶ False) ⟶ False) ⟶ ((x65 x64 ⟶ False) ⟶ False) ⟶ (∀ x66 . x65 (x1 x66) ⟶ False) ⟶ (x65 x58 ⟶ False) ⟶ (∀ x66 x67 . (x65 x67 ⟶ False) ⟶ (x65 x66 ⟶ False) ⟶ x65 (x62 x67 x66) ⟶ False) ⟶ (∀ x66 x67 . (x65 x67 ⟶ False) ⟶ (x65 x66 ⟶ False) ⟶ x2 x66 (x1 x67) ⟶ (x5 (x34 x66 x67) x67 x66 ⟶ False) ⟶ False) ⟶ (∀ x66 . (x2 (x23 x66) x66 ⟶ False) ⟶ False) ⟶ (∀ x66 x67 x68 . (x65 x68 ⟶ False) ⟶ (x65 x66 ⟶ False) ⟶ x2 x66 (x1 x68) ⟶ x5 x67 x68 x66 ⟶ (x2 x67 x68 ⟶ False) ⟶ False) ⟶ ((x5 x56 x58 x52 ⟶ False) ⟶ False) ⟶ ((x2 x52 (x1 x58) ⟶ False) ⟶ False) ⟶ (∀ x66 x67 . (x65 x67 ⟶ False) ⟶ x54 x66 (x57 x56 x55) ⟶ x63 x66 ⟶ x59 x66 x67 x58 ⟶ x2 x66 (x1 (x62 x67 x58)) ⟶ (x2 (x39 x67 x66) (x1 (x62 x67 x58)) ⟶ False) ⟶ False) ⟶ (∀ x66 x67 . (x65 x67 ⟶ False) ⟶ x54 x66 (x57 x56 x55) ⟶ x63 x66 ⟶ x59 x66 x67 x58 ⟶ x2 x66 (x1 (x62 x67 x58)) ⟶ (x59 (x39 x67 x66) x67 x58 ⟶ False) ⟶ False) ⟶ (∀ x66 x67 . (x65 x67 ⟶ False) ⟶ x54 x66 (x57 x56 x55) ⟶ x63 x66 ⟶ x59 x66 x67 x58 ⟶ x2 x66 (x1 (x62 x67 x58)) ⟶ (x63 (x39 x67 x66) ⟶ False) ⟶ False) ⟶ (∀ x66 x67 . (x65 x67 ⟶ False) ⟶ x54 x66 (x57 x56 x55) ⟶ x63 x66 ⟶ x59 x66 x67 x58 ⟶ x2 x66 (x1 (x62 x67 x58)) ⟶ (x54 (x39 x67 x66) (x57 x56 x55) ⟶ False) ⟶ False) ⟶ (∀ x66 x67 x68 . (x65 x68 ⟶ False) ⟶ x54 x66 (x57 x56 x55) ⟶ x63 x66 ⟶ x59 x66 x68 x58 ⟶ x2 x66 (x1 (x62 x68 x58)) ⟶ x54 x67 (x57 x56 x55) ⟶ x63 x67 ⟶ x59 x67 x68 x58 ⟶ x2 x67 (x1 (x62 x68 x58)) ⟶ (x2 (x60 x68 x66 x67) (x1 (x62 x68 x58)) ⟶ False) ⟶ False) ⟶ (∀ x66 x67 x68 . (x65 x68 ⟶ False) ⟶ x54 x66 (x57 x56 x55) ⟶ x63 x66 ⟶ x59 x66 x68 x58 ⟶ x2 x66 (x1 (x62 x68 x58)) ⟶ x54 x67 (x57 x56 x55) ⟶ x63 x67 ⟶ x59 x67 x68 x58 ⟶ x2 x67 (x1 (x62 x68 x58)) ⟶ (x59 (x60 x68 x66 x67) x68 x58 ⟶ False) ⟶ False) ⟶ (∀ x66 x67 x68 . (x65 x68 ⟶ False) ⟶ x54 x66 (x57 x56 x55) ⟶ x63 x66 ⟶ x59 x66 x68 x58 ⟶ x2 x66 (x1 (x62 x68 x58)) ⟶ x54 x67 (x57 x56 x55) ⟶ x63 x67 ⟶ x59 x67 x68 x58 ⟶ x2 x67 (x1 (x62 x68 x58)) ⟶ (x63 (x60 x68 x66 x67) ⟶ False) ⟶ False) ⟶ (∀ x66 x67 x68 . (x65 x68 ⟶ False) ⟶ x54 x66 (x57 x56 x55) ⟶ x63 x66 ⟶ x59 x66 x68 x58 ⟶ x2 x66 (x1 (x62 x68 x58)) ⟶ x54 x67 (x57 x56 x55) ⟶ x63 x67 ⟶ x59 x67 x68 x58 ⟶ x2 x67 (x1 (x62 x68 x58)) ⟶ (x54 (x60 x68 x66 x67) (x57 x56 x55) ⟶ False) ⟶ False) ⟶ (∀ x66 x67 . x50 x67 ⟶ x50 x66 ⟶ (x2 (x57 x67 x66) (x1 x58) ⟶ False) ⟶ False) ⟶ (∀ x66 x67 x68 . (x65 x68 ⟶ False) ⟶ x54 x66 (x57 x56 x55) ⟶ x63 x66 ⟶ x59 x66 x68 x58 ⟶ x2 x66 (x1 (x62 x68 x58)) ⟶ x54 x67 (x57 x56 x55) ⟶ x63 x67 ⟶ x59 x67 x68 x58 ⟶ x2 x67 (x1 (x62 x68 x58)) ⟶ (x2 (x33 x68 x66 x67) (x1 (x62 x68 x58)) ⟶ False) ⟶ False) ⟶ (∀ x66 x67 x68 . (x65 x68 ⟶ False) ⟶ x54 x66 (x57 x56 x55) ⟶ x63 x66 ⟶ x59 x66 x68 x58 ⟶ x2 x66 (x1 (x62 x68 x58)) ⟶ x54 x67 (x57 x56 x55) ⟶ x63 x67 ⟶ x59 x67 x68 x58 ⟶ x2 x67 (x1 (x62 x68 x58)) ⟶ (x59 (x33 x68 x66 x67) x68 x58 ⟶ False) ⟶ False) ⟶ (∀ x66 x67 x68 . (x65 x68 ⟶ False) ⟶ x54 x66 (x57 x56 x55) ⟶ x63 x66 ⟶ x59 x66 x68 x58 ⟶ x2 x66 (x1 (x62 x68 x58)) ⟶ x54 x67 (x57 x56 x55) ⟶ x63 x67 ⟶ x59 x67 x68 x58 ⟶ x2 x67 (x1 (x62 x68 x58)) ⟶ (x63 (x33 x68 x66 x67) ⟶ False) ⟶ False) ⟶ (∀ x66 x67 x68 . (x65 x68 ⟶ False) ⟶ x54 x66 (x57 x56 x55) ⟶ x63 x66 ⟶ x59 x66 x68 x58 ⟶ x2 x66 (x1 (x62 x68 x58)) ⟶ x54 x67 (x57 x56 x55) ⟶ x63 x67 ⟶ x59 x67 x68 x58 ⟶ x2 x67 (x1 (x62 x68 x58)) ⟶ (x54 (x33 x68 x66 x67) (x57 x56 x55) ⟶ False) ⟶ False) ⟶ (∀ x66 x67 x68 . (x65 x68 ⟶ False) ⟶ x54 x66 (x57 x56 x55) ⟶ x63 x66 ⟶ x59 x66 x68 x58 ⟶ x2 x66 (x1 (x62 x68 x58)) ⟶ x54 x67 (x57 x56 x55) ⟶ x63 x67 ⟶ x59 x67 x68 x58 ⟶ x2 x67 (x1 (x62 x68 x58)) ⟶ (x2 (x53 x68 x66 x67) (x1 (x62 x68 x58)) ⟶ False) ⟶ False) ⟶ (∀ x66 x67 x68 . (x65 x68 ⟶ False) ⟶ x54 x66 (x57 x56 x55) ⟶ x63 x66 ⟶ x59 x66 x68 x58 ⟶ x2 x66 (x1 (x62 x68 x58)) ⟶ x54 x67 (x57 x56 x55) ⟶ x63 x67 ⟶ x59 x67 x68 x58 ⟶ x2 x67 (x1 (x62 x68 x58)) ⟶ (x59 (x53 x68 x66 x67) x68 x58 ⟶ False) ⟶ False) ⟶ (∀ x66 x67 x68 . (x65 x68 ⟶ False) ⟶ x54 x66 (x57 x56 x55) ⟶ x63 x66 ⟶ x59 x66 x68 x58 ⟶ x2 x66 (x1 (x62 x68 x58)) ⟶ x54 x67 (x57 x56 x55) ⟶ x63 x67 ⟶ x59 x67 x68 x58 ⟶ x2 x67 (x1 (x62 x68 x58)) ⟶ (x63 (x53 x68 x66 x67) ⟶ False) ⟶ False) ⟶ (∀ x66 x67 x68 . (x65 x68 ⟶ False) ⟶ x54 x66 (x57 x56 x55) ⟶ x63 x66 ⟶ x59 x66 x68 x58 ⟶ x2 x66 (x1 (x62 x68 x58)) ⟶ x54 x67 (x57 x56 x55) ⟶ x63 x67 ⟶ x59 x67 x68 x58 ⟶ x2 x67 (x1 (x62 x68 x58)) ⟶ (x54 (x53 x68 x66 x67) (x57 x56 x55) ⟶ False) ⟶ False) ⟶ (∀ x66 x67 x68 . (x65 x68 ⟶ False) ⟶ x54 x66 (x57 x56 x55) ⟶ x63 x66 ⟶ x59 x66 x68 x58 ⟶ x2 x66 (x1 (x62 x68 x58)) ⟶ x54 x67 (x57 x56 x55) ⟶ x63 x67 ⟶ x59 x67 x68 x58 ⟶ x2 x67 (x1 (x62 x68 x58)) ⟶ (x33 x68 x66 x67 = x53 x68 x66 (x39 x68 x67) ⟶ False) ⟶ False) ⟶ (∀ x66 x67 x68 . (x65 x68 ⟶ False) ⟶ x54 x66 (x57 x56 x55) ⟶ x63 x66 ⟶ x59 x66 x68 x58 ⟶ x2 x66 (x1 (x62 x68 x58)) ⟶ x54 x67 (x57 x56 x55) ⟶ x63 x67 ⟶ x59 x67 x68 x58 ⟶ x2 x67 (x1 (x62 x68 x58)) ⟶ (x60 x68 x66 x67 = x60 x68 x67 x66 ⟶ False) ⟶ False) ⟶ (∀ x66 x67 x68 . (x65 x68 ⟶ False) ⟶ x54 x66 (x57 x56 x55) ⟶ x63 x66 ⟶ x59 x66 x68 x58 ⟶ x2 x66 (x1 (x62 x68 x58)) ⟶ x54 x67 (x57 x56 x55) ⟶ x63 x67 ⟶ x59 x67 x68 x58 ⟶ x2 x67 (x1 (x62 x68 x58)) ⟶ (x53 x68 x66 x67 = x53 x68 x67 x66 ⟶ False) ⟶ False) ⟶ (∀ x66 . x65 x66 ⟶ x6 x66 ⟶ (x46 x66 ⟶ False) ⟶ False) ⟶ (∀ x66 . x65 x66 ⟶ x6 x66 ⟶ (x6 x66 ⟶ False) ⟶ False) ⟶ (∀ x66 . x2 x66 (x1 x36) ⟶ (x37 x66 ⟶ False) ⟶ False) ⟶ (∀ x66 . x6 x66 ⟶ x46 x66 ⟶ (x7 x66 ⟶ False) ⟶ False) ⟶ (∀ x66 . x6 x66 ⟶ x46 x66 ⟶ (x6 x66 ⟶ False) ⟶ False) ⟶ (∀ x66 . x2 x66 (x1 x58) ⟶ (x18 x66 ⟶ False) ⟶ False) ⟶ (∀ x66 . x6 x66 ⟶ x46 x66 ⟶ (x54 x66 x36 ⟶ False) ⟶ False) ⟶ (∀ x66 . x6 x66 ⟶ x46 x66 ⟶ (x6 x66 ⟶ False) ⟶ False) ⟶ (∀ x66 . x6 x66 ⟶ x7 x66 ⟶ (x22 x66 ⟶ False) ⟶ False) ⟶ (∀ x66 . x6 x66 ⟶ x7 x66 ⟶ (x6 x66 ⟶ False) ⟶ False) ⟶ (∀ x66 . x6 x66 ⟶ x7 x66 ⟶ (x35 x66 ⟶ False) ⟶ False) ⟶ (∀ x66 . x6 x66 ⟶ x7 x66 ⟶ (x6 x66 ⟶ False) ⟶ False) ⟶ (∀ x66 . x18 x66 ⟶ (x19 x66 ⟶ False) ⟶ False) ⟶ (∀ x66 . x2 x66 (x1 x58) ⟶ x65 x66 ⟶ (x42 x66 ⟶ False) ⟶ False) ⟶ (∀ x66 . x6 x66 ⟶ x54 x66 x36 ⟶ (x7 x66 ⟶ False) ⟶ False) ⟶ (∀ x66 . x6 x66 ⟶ x54 x66 x36 ⟶ (x6 x66 ⟶ False) ⟶ False) ⟶ (∀ x66 x67 . x65 x67 ⟶ x2 x66 (x1 x67) ⟶ x9 x66 x67 ⟶ False) ⟶ (∀ x66 x67 x68 . x65 x68 ⟶ x2 x66 (x1 (x62 x67 x68)) ⟶ (x65 x66 ⟶ False) ⟶ False) ⟶ (∀ x66 . x18 x66 ⟶ (x40 x66 ⟶ False) ⟶ False) ⟶ (∀ x66 . x6 x66 ⟶ x54 x66 x21 ⟶ (x7 x66 ⟶ False) ⟶ False) ⟶ (∀ x66 . x6 x66 ⟶ x54 x66 x21 ⟶ (x6 x66 ⟶ False) ⟶ False) ⟶ (∀ x66 x67 . (x65 x67 ⟶ False) ⟶ x2 x66 (x1 x67) ⟶ x65 x66 ⟶ (x9 x66 x67 ⟶ False) ⟶ False) ⟶ (∀ x66 x67 x68 . x65 x68 ⟶ x2 x66 (x1 (x62 x68 x67)) ⟶ (x65 x66 ⟶ False) ⟶ False) ⟶ (∀ x66 . x37 x66 ⟶ (x18 x66 ⟶ False) ⟶ False) ⟶ (∀ x66 . x6 x66 ⟶ x54 x66 x52 ⟶ (x46 x66 ⟶ False) ⟶ False) ⟶ (∀ x66 . x6 x66 ⟶ x54 x66 x52 ⟶ (x6 x66 ⟶ False) ⟶ False) ⟶ (∀ x66 . x6 x66 ⟶ x54 x66 x58 ⟶ (x7 x66 ⟶ False) ⟶ False) ⟶ (∀ x66 . x6 x66 ⟶ x54 x66 x58 ⟶ (x6 x66 ⟶ False) ⟶ False) ⟶ (∀ x66 . x6 x66 ⟶ x54 x66 x21 ⟶ (x54 x66 x36 ⟶ False) ⟶ False) ⟶ (∀ x66 . x6 x66 ⟶ x54 x66 x21 ⟶ (x6 x66 ⟶ False) ⟶ False) ⟶ (∀ x66 x67 . (x65 x67 ⟶ False) ⟶ x2 x66 (x1 x67) ⟶ (x9 x66 x67 ⟶ False) ⟶ x65 x66 ⟶ False) ⟶ (∀ x66 x67 x68 . x2 x68 (x1 (x62 x66 x67)) ⟶ (x54 x68 x67 ⟶ False) ⟶ False) ⟶ (∀ x66 x67 x68 . x2 x68 (x1 (x62 x67 x66)) ⟶ (x44 x68 x67 ⟶ False) ⟶ False) ⟶ (∀ x66 . x20 x66 ⟶ (x37 x66 ⟶ False) ⟶ False) ⟶ (∀ x66 . x65 x66 ⟶ (x11 x66 ⟶ False) ⟶ False) ⟶ (∀ x66 . x2 x66 x52 ⟶ (x48 x66 ⟶ False) ⟶ False) ⟶ (∀ x66 x67 . x48 x67 ⟶ x2 x66 (x1 x67) ⟶ (x48 x66 ⟶ False) ⟶ False) ⟶ (∀ x66 x67 . x20 x67 ⟶ x2 x66 (x1 x67) ⟶ (x20 x66 ⟶ False) ⟶ False) ⟶ (∀ x66 x67 . x37 x67 ⟶ x2 x66 (x1 x67) ⟶ (x37 x66 ⟶ False) ⟶ False) ⟶ (∀ x66 x67 x68 . x48 x68 ⟶ x2 x66 (x1 (x62 x67 x68)) ⟶ (x46 x66 ⟶ False) ⟶ False) ⟶ (∀ x66 x67 . x18 x67 ⟶ x2 x66 (x1 x67) ⟶ (x18 x66 ⟶ False) ⟶ False) ⟶ (∀ x66 x67 x68 . x20 x68 ⟶ x2 x66 (x1 (x62 x67 x68)) ⟶ (x54 x66 x21 ⟶ False) ⟶ False) ⟶ (∀ x66 x67 . x40 x67 ⟶ x2 x66 (x1 x67) ⟶ (x40 x66 ⟶ False) ⟶ False) ⟶ (∀ x66 . x6 x66 ⟶ x46 x66 ⟶ (x54 x66 x21 ⟶ False) ⟶ False) ⟶ (∀ x66 . x6 x66 ⟶ x46 x66 ⟶ (x6 x66 ⟶ False) ⟶ False) ⟶ (∀ x66 x67 . x65 x67 ⟶ x2 x66 (x1 x67) ⟶ (x65 x66 ⟶ False) ⟶ False) ⟶ (∀ x66 x67 x68 . x2 x68 (x1 (x62 x66 x67)) ⟶ (x6 x68 ⟶ False) ⟶ False) ⟶ (∀ x66 . x48 x66 ⟶ (x20 x66 ⟶ False) ⟶ False) ⟶ (∀ x66 . x2 x66 (x1 x58) ⟶ x42 x66 ⟶ (x24 x66 ⟶ False) ⟶ False) ⟶ (∀ x66 x67 x68 . x37 x68 ⟶ x2 x66 (x1 (x62 x67 x68)) ⟶ (x54 x66 x36 ⟶ False) ⟶ False) ⟶ (∀ x66 x67 . x19 x67 ⟶ x2 x66 (x1 x67) ⟶ (x19 x66 ⟶ False) ⟶ False) ⟶ (∀ x66 x67 x68 . x18 x68 ⟶ x2 x66 (x1 (x62 x67 x68)) ⟶ (x7 x66 ⟶ False) ⟶ False) ⟶ (∀ x66 . x65 x66 ⟶ (x48 x66 ⟶ False) ⟶ False) ⟶ (∀ x66 x67 x68 . x40 x68 ⟶ x2 x66 (x1 (x62 x67 x68)) ⟶ (x35 x66 ⟶ False) ⟶ False) ⟶ (∀ x66 x67 . x48 x67 ⟶ x2 x66 x67 ⟶ (x25 x66 ⟶ False) ⟶ False) ⟶ (∀ x66 x67 x68 . x19 x68 ⟶ x2 x66 (x1 (x62 x67 x68)) ⟶ (x22 x66 ⟶ False) ⟶ False) ⟶ (∀ x66 x67 . x20 x67 ⟶ x2 x66 x67 ⟶ (x26 x66 ⟶ False) ⟶ False) ⟶ (∀ x66 x67 . x6 x67 ⟶ x46 x67 ⟶ x2 x66 (x1 x67) ⟶ (x46 x66 ⟶ False) ⟶ False) ⟶ (∀ x66 x67 . x37 x67 ⟶ x2 x66 x67 ⟶ (x27 x66 ⟶ False) ⟶ False) ⟶ (∀ x66 x67 . x6 x67 ⟶ x54 x67 x21 ⟶ x2 x66 (x1 x67) ⟶ (x54 x66 x21 ⟶ False) ⟶ False) ⟶ (∀ x66 x67 . x18 x67 ⟶ x2 x66 x67 ⟶ (x50 x66 ⟶ False) ⟶ False) ⟶ (∀ x66 x67 . x6 x67 ⟶ x54 x67 x36 ⟶ x2 x66 (x1 x67) ⟶ (x54 x66 x36 ⟶ False) ⟶ False) ⟶ (∀ x66 x67 . x40 x67 ⟶ x2 x66 x67 ⟶ (x28 x66 ⟶ False) ⟶ False) ⟶ (∀ x66 x67 . x6 x67 ⟶ x7 x67 ⟶ x2 x66 (x1 x67) ⟶ (x7 x66 ⟶ False) ⟶ False) ⟶ (∀ x66 x67 . x19 x67 ⟶ x2 x66 x67 ⟶ (x29 x66 ⟶ False) ⟶ False) ⟶ (∀ x66 x67 . x6 x67 ⟶ x35 x67 ⟶ x2 x66 (x1 x67) ⟶ (x35 x66 ⟶ False) ⟶ False) ⟶ (∀ x66 . x2 x66 (x1 x52) ⟶ (x48 x66 ⟶ False) ⟶ False) ⟶ (∀ x66 x67 . x6 x67 ⟶ x22 x67 ⟶ x2 x66 (x1 x67) ⟶ (x22 x66 ⟶ False) ⟶ False) ⟶ (∀ x66 . x2 x66 (x1 x21) ⟶ (x20 x66 ⟶ False) ⟶ False) ⟶ (∀ x66 x67 . x0 x66 x67 ⟶ x0 x67 x66 ⟶ False) ⟶ (x61 (x60 x31 (x53 x31 x30 x32) (x33 x31 x30 x32)) x30 ⟶ False) ⟶ ((x2 x32 (x1 (x62 x31 x58)) ⟶ False) ⟶ False) ⟶ ((x59 x32 x31 x58 ⟶ False) ⟶ False) ⟶ ((x63 x32 ⟶ False) ⟶ False) ⟶ ((x54 x32 (x57 x56 x55) ⟶ False) ⟶ False) ⟶ ((x2 x30 (x1 (x62 x31 x58)) ⟶ False) ⟶ False) ⟶ ((x59 x30 x31 x58 ⟶ False) ⟶ False) ⟶ ((x63 x30 ⟶ False) ⟶ False) ⟶ ((x54 x30 (x57 x56 x55) ⟶ False) ⟶ False) ⟶ (x65 x31 ⟶ False) ⟶ False (proof)