Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrPhD../07507..
PUbyr../96279..
vout
PrPhD../5ac9a.. 3.37 bars
TMJp4../f2763.. ownership of 2dc28.. as prop with payaddr PrPhD.. rights free controlledby PrPhD.. upto 0
TMKqd../7821c.. ownership of bfd4b.. as prop with payaddr PrPhD.. rights free controlledby PrPhD.. upto 0
PUc7d../2c2a7.. doc published by PrPhD..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0 ⟶ False
Theorem 2dc28.. : ∀ 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 . x64 x66 ⟶ (x66 = x65 ⟶ False) ⟶ x64 x65 ⟶ False) ⟶ (∀ x65 x66 . x0 x65 x66 ⟶ x64 x66 ⟶ False) ⟶ (∀ x65 x66 x67 . (x63 x67 ⟶ False) ⟶ x55 x67 ⟶ x62 x67 ⟶ x56 x67 ⟶ x61 x66 x67 ⟶ x57 x66 x67 ⟶ x61 x65 x67 ⟶ x57 x65 x67 ⟶ (x59 (x60 x65 x66 x67) = x58 x67 x66 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 x67 . (x63 x67 ⟶ False) ⟶ x55 x67 ⟶ x62 x67 ⟶ x56 x67 ⟶ x61 x66 x67 ⟶ x57 x66 x67 ⟶ x61 x65 x67 ⟶ x57 x65 x67 ⟶ (x57 (x60 x65 x66 x67) x67 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 x67 . (x63 x67 ⟶ False) ⟶ x55 x67 ⟶ x62 x67 ⟶ x56 x67 ⟶ x61 x66 x67 ⟶ x57 x66 x67 ⟶ x61 x65 x67 ⟶ x57 x65 x67 ⟶ (x61 (x60 x65 x66 x67) x67 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 x67 . (x63 x67 ⟶ False) ⟶ x55 x67 ⟶ x62 x67 ⟶ x56 x67 ⟶ x61 x66 x67 ⟶ x57 x66 x67 ⟶ x61 x65 x67 ⟶ x57 x65 x67 ⟶ (x1 (x60 x65 x66 x67) ⟶ False) ⟶ False) ⟶ (∀ x65 . x64 x65 ⟶ (x65 = x54 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 x67 . x0 x65 x66 ⟶ x3 x66 (x2 x67) ⟶ x64 x67 ⟶ False) ⟶ (∀ x65 x66 x67 . (x63 x67 ⟶ False) ⟶ x55 x67 ⟶ x62 x67 ⟶ x56 x67 ⟶ x57 x66 x67 ⟶ x57 x65 x67 ⟶ x53 (x59 x66) (x59 x65) ⟶ (x57 x66 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 x67 x68 . (x63 x68 ⟶ False) ⟶ x55 x68 ⟶ x62 x68 ⟶ x56 x68 ⟶ x57 x67 x68 ⟶ x57 x65 x68 ⟶ x57 x66 x68 ⟶ x57 x65 x66 ⟶ (x53 (x58 x68 x67 x65) (x58 x68 x67 x66) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 x67 x68 . (x63 x68 ⟶ False) ⟶ x55 x68 ⟶ x62 x68 ⟶ x56 x68 ⟶ x57 x67 x68 ⟶ x57 x65 x68 ⟶ x57 x66 x68 ⟶ x57 x67 x65 ⟶ (x53 (x58 x68 x67 x66) (x58 x68 x65 x66) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 x67 . x0 x66 x67 ⟶ x3 x67 (x2 x65) ⟶ (x3 x66 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x53 x66 x65 ⟶ (x3 x66 (x2 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x3 x66 (x2 x65) ⟶ (x53 x66 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 x67 . x0 x66 x67 ⟶ x0 x65 x67 ⟶ x0 x65 (x52 x67 x66) ⟶ False) ⟶ (∀ x65 x66 . x0 x66 x65 ⟶ (x0 (x52 x65 x66) x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x3 x65 x66 ⟶ (x64 x66 ⟶ False) ⟶ (x0 x65 x66 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x0 x66 x65 ⟶ (x3 x66 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x51 x65 x66 ⟶ (x51 x66 x65 ⟶ False) ⟶ False) ⟶ (x64 x4 ⟶ False) ⟶ (∀ x65 . (x53 x65 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . (x64 x66 ⟶ False) ⟶ x3 x65 x66 ⟶ (x5 x66 x65 = x6 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . (x63 x65 ⟶ False) ⟶ x49 x65 ⟶ x64 (x50 x65) ⟶ False) ⟶ (∀ x65 . (x63 x65 ⟶ False) ⟶ x49 x65 ⟶ (x3 (x50 x65) (x2 (x59 x65)) ⟶ False) ⟶ False) ⟶ ((x62 x48 ⟶ False) ⟶ False) ⟶ ((x55 x48 ⟶ False) ⟶ False) ⟶ ((x47 x48 ⟶ False) ⟶ False) ⟶ ((x1 x48 ⟶ False) ⟶ False) ⟶ ((x46 x48 ⟶ False) ⟶ False) ⟶ (x63 x48 ⟶ False) ⟶ ((x56 x48 ⟶ False) ⟶ False) ⟶ (x64 x7 ⟶ False) ⟶ (∀ x65 . (x63 x65 ⟶ False) ⟶ x55 x65 ⟶ x62 x65 ⟶ x56 x65 ⟶ (x62 (x45 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 . (x63 x65 ⟶ False) ⟶ x55 x65 ⟶ x62 x65 ⟶ x56 x65 ⟶ (x55 (x45 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 . (x63 x65 ⟶ False) ⟶ x55 x65 ⟶ x62 x65 ⟶ x56 x65 ⟶ (x47 (x45 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 . (x63 x65 ⟶ False) ⟶ x55 x65 ⟶ x62 x65 ⟶ x56 x65 ⟶ (x1 (x45 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 . (x63 x65 ⟶ False) ⟶ x55 x65 ⟶ x62 x65 ⟶ x56 x65 ⟶ (x46 (x45 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 . (x63 x65 ⟶ False) ⟶ x55 x65 ⟶ x62 x65 ⟶ x56 x65 ⟶ x63 (x45 x65) ⟶ False) ⟶ (∀ x65 . (x63 x65 ⟶ False) ⟶ x55 x65 ⟶ x62 x65 ⟶ x56 x65 ⟶ (x57 (x45 x65) x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . (x8 x65 ⟶ False) ⟶ x49 x65 ⟶ x9 (x10 x65) ⟶ False) ⟶ (∀ x65 . (x8 x65 ⟶ False) ⟶ x49 x65 ⟶ (x3 (x10 x65) (x2 (x59 x65)) ⟶ False) ⟶ False) ⟶ (∀ x65 . (x63 x65 ⟶ False) ⟶ x49 x65 ⟶ (x9 (x11 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 . (x63 x65 ⟶ False) ⟶ x49 x65 ⟶ x64 (x11 x65) ⟶ False) ⟶ (∀ x65 . (x63 x65 ⟶ False) ⟶ x49 x65 ⟶ (x3 (x11 x65) (x2 (x59 x65)) ⟶ False) ⟶ False) ⟶ ((x64 x44 ⟶ False) ⟶ False) ⟶ (∀ x65 . (x63 x65 ⟶ False) ⟶ x55 x65 ⟶ x62 x65 ⟶ x56 x65 ⟶ (x61 (x12 x65) x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . (x63 x65 ⟶ False) ⟶ x55 x65 ⟶ x62 x65 ⟶ x56 x65 ⟶ (x62 (x12 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 . (x63 x65 ⟶ False) ⟶ x55 x65 ⟶ x62 x65 ⟶ x56 x65 ⟶ (x55 (x12 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 . (x63 x65 ⟶ False) ⟶ x55 x65 ⟶ x62 x65 ⟶ x56 x65 ⟶ (x47 (x12 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 . (x63 x65 ⟶ False) ⟶ x55 x65 ⟶ x62 x65 ⟶ x56 x65 ⟶ (x1 (x12 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 . (x63 x65 ⟶ False) ⟶ x55 x65 ⟶ x62 x65 ⟶ x56 x65 ⟶ x63 (x12 x65) ⟶ False) ⟶ (∀ x65 . (x63 x65 ⟶ False) ⟶ x55 x65 ⟶ x62 x65 ⟶ x56 x65 ⟶ (x57 (x12 x65) x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . (x63 x65 ⟶ False) ⟶ x55 x65 ⟶ x62 x65 ⟶ x56 x65 ⟶ (x62 (x43 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 . (x63 x65 ⟶ False) ⟶ x55 x65 ⟶ x62 x65 ⟶ x56 x65 ⟶ (x55 (x43 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 . (x63 x65 ⟶ False) ⟶ x55 x65 ⟶ x62 x65 ⟶ x56 x65 ⟶ (x47 (x43 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 . (x63 x65 ⟶ False) ⟶ x55 x65 ⟶ x62 x65 ⟶ x56 x65 ⟶ (x1 (x43 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 . (x63 x65 ⟶ False) ⟶ x55 x65 ⟶ x62 x65 ⟶ x56 x65 ⟶ x63 (x43 x65) ⟶ False) ⟶ (∀ x65 . (x63 x65 ⟶ False) ⟶ x55 x65 ⟶ x62 x65 ⟶ x56 x65 ⟶ (x57 (x43 x65) x65 ⟶ False) ⟶ False) ⟶ ((x62 x42 ⟶ False) ⟶ False) ⟶ ((x55 x42 ⟶ False) ⟶ False) ⟶ ((x1 x42 ⟶ False) ⟶ False) ⟶ (x63 x42 ⟶ False) ⟶ ((x56 x42 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 x67 x68 . x13 x68 ⟶ x15 x68 (x16 x65 x65) x65 ⟶ x3 x68 (x2 (x16 (x16 x65 x65) x65)) ⟶ x14 x65 x68 = x14 x67 x66 ⟶ (x68 = x66 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 x67 x68 . x13 x68 ⟶ x15 x68 (x16 x65 x65) x65 ⟶ x3 x68 (x2 (x16 (x16 x65 x65) x65)) ⟶ x14 x65 x68 = x14 x66 x67 ⟶ (x65 = x66 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 x67 x68 x69 . (x63 x69 ⟶ False) ⟶ x55 x69 ⟶ x62 x69 ⟶ x56 x69 ⟶ x57 x68 x69 ⟶ x57 x65 x69 ⟶ x3 x67 (x59 x69) ⟶ x66 = x67 ⟶ (x51 (x19 x69 x65 x67) (x18 x69 x68) ⟶ False) ⟶ (x0 x66 (x17 x69 x68 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 x67 x68 . (x63 x68 ⟶ False) ⟶ x55 x68 ⟶ x62 x68 ⟶ x56 x68 ⟶ x57 x67 x68 ⟶ x57 x65 x68 ⟶ x0 x66 (x17 x68 x67 x65) ⟶ x51 (x19 x68 x65 (x41 x65 x67 x68 x66)) (x18 x68 x67) ⟶ False) ⟶ (∀ x65 x66 x67 x68 . (x63 x68 ⟶ False) ⟶ x55 x68 ⟶ x62 x68 ⟶ x56 x68 ⟶ x57 x67 x68 ⟶ x57 x65 x68 ⟶ x0 x66 (x17 x68 x67 x65) ⟶ (x66 = x41 x65 x67 x68 x66 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 x67 x68 . (x63 x68 ⟶ False) ⟶ x55 x68 ⟶ x62 x68 ⟶ x56 x68 ⟶ x57 x67 x68 ⟶ x57 x65 x68 ⟶ x0 x66 (x17 x68 x67 x65) ⟶ (x3 (x41 x65 x67 x68 x66) (x59 x68) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 x67 x68 x69 x70 . (x63 x70 ⟶ False) ⟶ x56 x70 ⟶ x3 x69 (x2 (x59 x70)) ⟶ x3 x65 (x2 (x59 x70)) ⟶ x3 x68 (x59 x70) ⟶ x3 x66 (x59 x70) ⟶ x67 = x20 x70 x68 x66 ⟶ x0 x68 x69 ⟶ x0 x66 x65 ⟶ (x0 x67 (x21 x70 x69 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 x67 x68 . (x63 x68 ⟶ False) ⟶ x56 x68 ⟶ x3 x67 (x2 (x59 x68)) ⟶ x3 x65 (x2 (x59 x68)) ⟶ x0 x66 (x21 x68 x67 x65) ⟶ (x0 (x40 x65 x67 x68 x66) x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 x67 x68 . (x63 x68 ⟶ False) ⟶ x56 x68 ⟶ x3 x67 (x2 (x59 x68)) ⟶ x3 x65 (x2 (x59 x68)) ⟶ x0 x66 (x21 x68 x67 x65) ⟶ (x0 (x22 x65 x67 x68 x66) x67 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 x67 x68 . (x63 x68 ⟶ False) ⟶ x56 x68 ⟶ x3 x67 (x2 (x59 x68)) ⟶ x3 x65 (x2 (x59 x68)) ⟶ x0 x66 (x21 x68 x67 x65) ⟶ (x66 = x20 x68 (x22 x65 x67 x68 x66) (x40 x65 x67 x68 x66) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 x67 x68 . (x63 x68 ⟶ False) ⟶ x56 x68 ⟶ x3 x67 (x2 (x59 x68)) ⟶ x3 x65 (x2 (x59 x68)) ⟶ x0 x66 (x21 x68 x67 x65) ⟶ (x3 (x40 x65 x67 x68 x66) (x59 x68) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 x67 x68 . (x63 x68 ⟶ False) ⟶ x56 x68 ⟶ x3 x67 (x2 (x59 x68)) ⟶ x3 x65 (x2 (x59 x68)) ⟶ x0 x66 (x21 x68 x67 x65) ⟶ (x3 (x22 x65 x67 x68 x66) (x59 x68) ⟶ False) ⟶ False) ⟶ (∀ x65 . (x46 x65 ⟶ False) ⟶ x49 x65 ⟶ x23 (x59 x65) ⟶ False) ⟶ (∀ x65 . x46 x65 ⟶ x49 x65 ⟶ (x23 (x59 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 . x8 x65 ⟶ x49 x65 ⟶ (x9 (x59 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 . (x8 x65 ⟶ False) ⟶ x49 x65 ⟶ x9 (x59 x65) ⟶ False) ⟶ (∀ x65 . (x63 x65 ⟶ False) ⟶ x55 x65 ⟶ x62 x65 ⟶ x56 x65 ⟶ (x25 (x24 x65) (x59 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 . (x63 x65 ⟶ False) ⟶ x55 x65 ⟶ x62 x65 ⟶ x56 x65 ⟶ (x15 (x24 x65) (x16 (x59 x65) (x59 x65)) (x59 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 . (x63 x65 ⟶ False) ⟶ x55 x65 ⟶ x62 x65 ⟶ x56 x65 ⟶ (x13 (x24 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 . x64 (x6 x65) ⟶ False) ⟶ (∀ x65 . (x63 x65 ⟶ False) ⟶ x49 x65 ⟶ x64 (x59 x65) ⟶ False) ⟶ (∀ x65 . (x63 x65 ⟶ False) ⟶ x47 x65 ⟶ x56 x65 ⟶ (x39 (x24 x65) (x59 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 . (x63 x65 ⟶ False) ⟶ x47 x65 ⟶ x56 x65 ⟶ (x15 (x24 x65) (x16 (x59 x65) (x59 x65)) (x59 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 . (x63 x65 ⟶ False) ⟶ x47 x65 ⟶ x56 x65 ⟶ (x13 (x24 x65) ⟶ False) ⟶ False) ⟶ ((x64 x54 ⟶ False) ⟶ False) ⟶ (∀ x65 . x63 x65 ⟶ x49 x65 ⟶ (x64 (x59 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 . (x63 x65 ⟶ False) ⟶ x62 x65 ⟶ x56 x65 ⟶ (x26 (x24 x65) (x59 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 . (x63 x65 ⟶ False) ⟶ x62 x65 ⟶ x56 x65 ⟶ (x15 (x24 x65) (x16 (x59 x65) (x59 x65)) (x59 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 . (x63 x65 ⟶ False) ⟶ x62 x65 ⟶ x56 x65 ⟶ (x13 (x24 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 . (x3 (x38 x65) x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . (x63 x65 ⟶ False) ⟶ x55 x65 ⟶ x56 x65 ⟶ (x57 (x27 x65) x65 ⟶ False) ⟶ False) ⟶ ((x56 x37 ⟶ False) ⟶ False) ⟶ ((x49 x28 ⟶ False) ⟶ False) ⟶ (∀ x65 . x56 x65 ⟶ (x3 (x24 x65) (x2 (x16 (x16 (x59 x65) (x59 x65)) (x59 x65))) ⟶ False) ⟶ False) ⟶ (∀ x65 . x56 x65 ⟶ (x15 (x24 x65) (x16 (x59 x65) (x59 x65)) (x59 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 . x56 x65 ⟶ (x13 (x24 x65) ⟶ False) ⟶ False) ⟶ ((x64 x29 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . (x63 x66 ⟶ False) ⟶ x55 x66 ⟶ x56 x66 ⟶ x57 x65 x66 ⟶ (x56 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . (x63 x66 ⟶ False) ⟶ x55 x66 ⟶ x56 x66 ⟶ x57 x65 x66 ⟶ (x55 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . (x63 x66 ⟶ False) ⟶ x55 x66 ⟶ x56 x66 ⟶ x57 x65 x66 ⟶ x63 x65 ⟶ False) ⟶ (∀ x65 . x56 x65 ⟶ (x49 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . (x63 x66 ⟶ False) ⟶ x55 x66 ⟶ x62 x66 ⟶ x56 x66 ⟶ x57 x65 x66 ⟶ (x3 (x18 x66 x65) (x2 (x59 x66)) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . (x64 x66 ⟶ False) ⟶ x3 x65 x66 ⟶ (x3 (x5 x66 x65) (x2 x66) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 x67 . x56 x67 ⟶ x3 x65 (x59 x67) ⟶ x3 x66 (x59 x67) ⟶ (x3 (x20 x67 x65 x66) (x59 x67) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 x67 . (x63 x67 ⟶ False) ⟶ x56 x67 ⟶ x3 x66 (x59 x67) ⟶ x3 x65 (x2 (x59 x67)) ⟶ (x3 (x30 x67 x66 x65) (x2 (x59 x67)) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 x67 . (x63 x67 ⟶ False) ⟶ x55 x67 ⟶ x62 x67 ⟶ x56 x67 ⟶ x57 x66 x67 ⟶ x57 x65 x67 ⟶ (x3 (x58 x67 x66 x65) (x2 (x59 x67)) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 x67 . (x63 x67 ⟶ False) ⟶ x56 x67 ⟶ x3 x66 (x2 (x59 x67)) ⟶ x3 x65 (x2 (x59 x67)) ⟶ (x3 (x31 x67 x66 x65) (x2 (x59 x67)) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 x67 . (x63 x67 ⟶ False) ⟶ x55 x67 ⟶ x62 x67 ⟶ x56 x67 ⟶ x57 x66 x67 ⟶ x3 x65 (x59 x67) ⟶ (x3 (x19 x67 x66 x65) (x2 (x59 x67)) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x13 x66 ⟶ x15 x66 (x16 x65 x65) x65 ⟶ x3 x66 (x2 (x16 (x16 x65 x65) x65)) ⟶ (x56 (x14 x65 x66) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x13 x66 ⟶ x15 x66 (x16 x65 x65) x65 ⟶ x3 x66 (x2 (x16 (x16 x65 x65) x65)) ⟶ (x1 (x14 x65 x66) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . (x63 x66 ⟶ False) ⟶ x55 x66 ⟶ x62 x66 ⟶ x56 x66 ⟶ x57 x65 x66 ⟶ (x18 x66 x65 = x59 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 x67 . (x63 x67 ⟶ False) ⟶ x55 x67 ⟶ x62 x67 ⟶ x56 x67 ⟶ x57 x66 x67 ⟶ x57 x65 x67 ⟶ (x58 x67 x66 x65 = x17 x67 x66 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 x67 . (x63 x67 ⟶ False) ⟶ x56 x67 ⟶ x3 x66 (x59 x67) ⟶ x3 x65 (x2 (x59 x67)) ⟶ (x30 x67 x66 x65 = x31 x67 (x5 (x59 x67) x66) x65 ⟶ False) ⟶ False) ⟶ ((x54 = x29 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 x67 . (x63 x67 ⟶ False) ⟶ x56 x67 ⟶ x3 x66 (x2 (x59 x67)) ⟶ x3 x65 (x2 (x59 x67)) ⟶ (x31 x67 x66 x65 = x21 x67 x66 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 x67 . (x63 x67 ⟶ False) ⟶ x55 x67 ⟶ x62 x67 ⟶ x56 x67 ⟶ x57 x66 x67 ⟶ x3 x65 (x59 x67) ⟶ (x19 x67 x66 x65 = x30 x67 x65 (x18 x67 x66) ⟶ False) ⟶ False) ⟶ (∀ x65 . x49 x65 ⟶ x32 x65 x54 ⟶ (x63 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x49 x65 ⟶ x63 x65 ⟶ (x32 x65 x54 ⟶ False) ⟶ False) ⟶ (∀ x65 . x49 x65 ⟶ (x46 x65 ⟶ False) ⟶ x8 x65 ⟶ False) ⟶ (∀ x65 . x49 x65 ⟶ x8 x65 ⟶ (x46 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x49 x65 ⟶ (x46 x65 ⟶ False) ⟶ x46 x65 ⟶ False) ⟶ (∀ x65 . x49 x65 ⟶ (x46 x65 ⟶ False) ⟶ x63 x65 ⟶ False) ⟶ (∀ x65 . x49 x65 ⟶ x63 x65 ⟶ (x46 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x49 x65 ⟶ x63 x65 ⟶ (x63 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . (x63 x66 ⟶ False) ⟶ x46 x66 ⟶ x55 x66 ⟶ x62 x66 ⟶ x56 x66 ⟶ x57 x65 x66 ⟶ (x46 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x49 x65 ⟶ (x8 x65 ⟶ False) ⟶ x63 x65 ⟶ False) ⟶ (∀ x65 . x49 x65 ⟶ x63 x65 ⟶ (x8 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . (x63 x66 ⟶ False) ⟶ x55 x66 ⟶ x62 x66 ⟶ x56 x66 ⟶ x57 x65 x66 ⟶ (x62 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x56 x65 ⟶ x55 x65 ⟶ (x47 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x49 x65 ⟶ (x8 x65 ⟶ False) ⟶ x63 x65 ⟶ False) ⟶ (∀ x65 . x49 x65 ⟶ x32 x65 x4 ⟶ (x8 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x49 x65 ⟶ x32 x65 x4 ⟶ x63 x65 ⟶ False) ⟶ (∀ x65 . x49 x65 ⟶ (x63 x65 ⟶ False) ⟶ x8 x65 ⟶ (x32 x65 x4 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x0 x65 x66 ⟶ x0 x66 x65 ⟶ False) ⟶ (∀ x65 . x56 x65 ⟶ x1 x65 ⟶ (x65 = x14 (x59 x65) (x24 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x1 x66 ⟶ x61 x66 x33 ⟶ x57 x66 x33 ⟶ x1 x65 ⟶ x61 x65 x33 ⟶ x57 x65 x33 ⟶ x59 x66 = x58 x33 x35 x34 ⟶ x59 x65 = x58 x33 x36 x34 ⟶ x53 (x58 x33 x35 x66) (x58 x33 x35 x65) ⟶ False) ⟶ ((x57 x35 x36 ⟶ False) ⟶ False) ⟶ ((x57 x36 x33 ⟶ False) ⟶ False) ⟶ ((x61 x36 x33 ⟶ False) ⟶ False) ⟶ ((x57 x35 x33 ⟶ False) ⟶ False) ⟶ ((x61 x35 x33 ⟶ False) ⟶ False) ⟶ ((x57 x34 x33 ⟶ False) ⟶ False) ⟶ ((x61 x34 x33 ⟶ False) ⟶ False) ⟶ ((x56 x33 ⟶ False) ⟶ False) ⟶ ((x62 x33 ⟶ False) ⟶ False) ⟶ ((x55 x33 ⟶ False) ⟶ False) ⟶ (x63 x33 ⟶ False) ⟶ False (proof)