Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrNUD../2856e..
PUfMA../e4f1a..
vout
PrNUD../5bc11.. 0.03 bars
TMdTw../b8a35.. ownership of e7855.. as prop with payaddr PrPhD.. rightscost 0.00 controlledby PrPhD.. upto 0
TMbPM../9cf18.. ownership of 43ab4.. as prop with payaddr PrPhD.. rightscost 0.00 controlledby PrPhD.. upto 0
PUc5T../08f11.. doc published by PrPhD..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0 ⟶ False
Theorem e7855.. : ∀ 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 . x59 x61 ⟶ x59 x60 ⟶ (x55 (x54 x61 x60) = x56 (x57 (x58 x61) (x55 x60)) (x57 (x58 x60) (x55 x61)) ⟶ False) ⟶ False) ⟶ (∀ x60 x61 . x59 x61 ⟶ x59 x60 ⟶ (x58 (x54 x61 x60) = x0 (x57 (x58 x61) (x58 x60)) (x57 (x55 x61) (x55 x60)) ⟶ False) ⟶ False) ⟶ (∀ x60 x61 . x53 x61 ⟶ (x61 = x60 ⟶ False) ⟶ x53 x60 ⟶ False) ⟶ (∀ x60 x61 . x1 x60 x61 ⟶ x53 x61 ⟶ False) ⟶ (∀ x60 . x53 x60 ⟶ (x60 = x52 ⟶ False) ⟶ False) ⟶ (∀ x60 x61 x62 . x1 x60 x61 ⟶ x3 x61 (x2 x62) ⟶ x53 x62 ⟶ False) ⟶ (∀ x60 x61 x62 . x1 x61 x62 ⟶ x3 x62 (x2 x60) ⟶ (x3 x61 x60 ⟶ False) ⟶ False) ⟶ (∀ x60 x61 . x4 x61 x60 ⟶ (x3 x61 (x2 x60) ⟶ False) ⟶ False) ⟶ (∀ x60 x61 . x3 x61 (x2 x60) ⟶ (x4 x61 x60 ⟶ False) ⟶ False) ⟶ (∀ x60 . x59 x60 ⟶ (x54 x5 x60 = x60 ⟶ False) ⟶ False) ⟶ (∀ x60 x61 . x3 x60 x61 ⟶ (x53 x61 ⟶ False) ⟶ (x1 x60 x61 ⟶ False) ⟶ False) ⟶ (∀ x60 x61 . x1 x61 x60 ⟶ (x3 x61 x60 ⟶ False) ⟶ False) ⟶ ((x3 x52 x51 ⟶ False) ⟶ False) ⟶ (∀ x60 x61 . x59 x61 ⟶ x59 x60 ⟶ (x7 (x6 x61) (x6 x60) = x7 x60 x61 ⟶ False) ⟶ False) ⟶ (∀ x60 x61 . x59 x61 ⟶ x59 x60 ⟶ (x50 (x6 x61) (x6 x60) = x6 (x50 x61 x60) ⟶ False) ⟶ False) ⟶ (∀ x60 x61 x62 . x59 x62 ⟶ x59 x60 ⟶ x59 x61 ⟶ (x54 (x54 x62 x60) x61 = x54 x62 (x54 x60 x61) ⟶ False) ⟶ False) ⟶ (∀ x60 x61 x62 . x59 x62 ⟶ x59 x60 ⟶ x59 x61 ⟶ (x50 (x50 x62 x60) x61 = x50 x62 (x50 x60 x61) ⟶ False) ⟶ False) ⟶ (∀ x60 x61 x62 . x59 x62 ⟶ x59 x60 ⟶ x59 x61 ⟶ (x54 (x50 x62 x60) x61 = x50 (x54 x62 x61) (x54 x60 x61) ⟶ False) ⟶ False) ⟶ ((x3 x48 x49 ⟶ False) ⟶ False) ⟶ ((x3 x48 x8 ⟶ False) ⟶ False) ⟶ ((x47 x48 x49 x8 ⟶ False) ⟶ False) ⟶ ((x9 x48 ⟶ False) ⟶ False) ⟶ (x53 x48 ⟶ False) ⟶ (∀ x60 . x59 x60 ⟶ (x54 x60 (x6 x5) = x6 x60 ⟶ False) ⟶ False) ⟶ ((x3 x5 x49 ⟶ False) ⟶ False) ⟶ ((x3 x5 x8 ⟶ False) ⟶ False) ⟶ ((x47 x5 x49 x8 ⟶ False) ⟶ False) ⟶ ((x9 x5 ⟶ False) ⟶ False) ⟶ (x53 x5 ⟶ False) ⟶ (∀ x60 x61 . x59 x61 ⟶ x59 x60 ⟶ (x50 x61 (x6 x60) = x7 x61 x60 ⟶ False) ⟶ False) ⟶ ((x3 x46 x49 ⟶ False) ⟶ False) ⟶ ((x3 x46 x8 ⟶ False) ⟶ False) ⟶ ((x47 x46 x49 x8 ⟶ False) ⟶ False) ⟶ ((x53 x46 ⟶ False) ⟶ False) ⟶ ((x6 (x6 x48) = x48 ⟶ False) ⟶ False) ⟶ ((x6 (x6 x5) = x5 ⟶ False) ⟶ False) ⟶ ((x6 x48 = x6 x48 ⟶ False) ⟶ False) ⟶ ((x6 x5 = x6 x5 ⟶ False) ⟶ False) ⟶ ((x6 x46 = x46 ⟶ False) ⟶ False) ⟶ ((x54 (x6 x48) x5 = x6 x48 ⟶ False) ⟶ False) ⟶ ((x54 (x6 x48) x46 = x46 ⟶ False) ⟶ False) ⟶ ((x54 x48 x5 = x48 ⟶ False) ⟶ False) ⟶ ((x54 x48 x46 = x46 ⟶ False) ⟶ False) ⟶ ((x54 x5 (x6 x48) = x6 x48 ⟶ False) ⟶ False) ⟶ ((x54 x5 x48 = x48 ⟶ False) ⟶ False) ⟶ ((x54 x5 x5 = x5 ⟶ False) ⟶ False) ⟶ ((x54 x5 x46 = x46 ⟶ False) ⟶ False) ⟶ ((x54 x46 (x6 x48) = x46 ⟶ False) ⟶ False) ⟶ ((x54 x46 x48 = x46 ⟶ False) ⟶ False) ⟶ ((x54 x46 x5 = x46 ⟶ False) ⟶ False) ⟶ ((x54 x46 x46 = x46 ⟶ False) ⟶ False) ⟶ ((x7 (x6 x48) (x6 x48) = x46 ⟶ False) ⟶ False) ⟶ ((x7 (x6 x48) (x6 x5) = x6 x5 ⟶ False) ⟶ False) ⟶ ((x7 (x6 x48) x46 = x6 x48 ⟶ False) ⟶ False) ⟶ ((x7 (x6 x5) (x6 x48) = x5 ⟶ False) ⟶ False) ⟶ ((x7 (x6 x5) (x6 x5) = x46 ⟶ False) ⟶ False) ⟶ ((x7 (x6 x5) x5 = x6 x48 ⟶ False) ⟶ False) ⟶ ((x7 (x6 x5) x46 = x6 x5 ⟶ False) ⟶ False) ⟶ ((x7 x48 x48 = x46 ⟶ False) ⟶ False) ⟶ ((x7 x48 x5 = x5 ⟶ False) ⟶ False) ⟶ ((x7 x48 x46 = x48 ⟶ False) ⟶ False) ⟶ ((x7 x5 (x6 x5) = x48 ⟶ False) ⟶ False) ⟶ ((x7 x5 x48 = x6 x5 ⟶ False) ⟶ False) ⟶ ((x7 x5 x5 = x46 ⟶ False) ⟶ False) ⟶ ((x7 x5 x46 = x5 ⟶ False) ⟶ False) ⟶ ((x7 x46 (x6 x48) = x48 ⟶ False) ⟶ False) ⟶ ((x7 x46 (x6 x5) = x5 ⟶ False) ⟶ False) ⟶ ((x7 x46 x48 = x6 x48 ⟶ False) ⟶ False) ⟶ ((x7 x46 x5 = x6 x5 ⟶ False) ⟶ False) ⟶ ((x7 x46 x46 = x46 ⟶ False) ⟶ False) ⟶ ((x50 (x6 x48) x48 = x46 ⟶ False) ⟶ False) ⟶ ((x50 (x6 x48) x5 = x6 x5 ⟶ False) ⟶ False) ⟶ ((x50 (x6 x5) (x6 x5) = x6 x48 ⟶ False) ⟶ False) ⟶ ((x50 (x6 x5) x48 = x5 ⟶ False) ⟶ False) ⟶ ((x50 (x6 x5) x5 = x46 ⟶ False) ⟶ False) ⟶ ((x50 (x6 x5) x46 = x6 x5 ⟶ False) ⟶ False) ⟶ ((x50 x48 (x6 x48) = x46 ⟶ False) ⟶ False) ⟶ ((x50 x48 (x6 x5) = x5 ⟶ False) ⟶ False) ⟶ ((x50 x48 x46 = x48 ⟶ False) ⟶ False) ⟶ ((x50 x5 (x6 x48) = x6 x5 ⟶ False) ⟶ False) ⟶ ((x50 x5 (x6 x5) = x46 ⟶ False) ⟶ False) ⟶ ((x50 x5 x5 = x48 ⟶ False) ⟶ False) ⟶ ((x50 x5 x46 = x5 ⟶ False) ⟶ False) ⟶ ((x50 x46 (x6 x48) = x6 x48 ⟶ False) ⟶ False) ⟶ ((x50 x46 (x6 x5) = x6 x5 ⟶ False) ⟶ False) ⟶ ((x50 x46 x48 = x48 ⟶ False) ⟶ False) ⟶ ((x50 x46 x5 = x5 ⟶ False) ⟶ False) ⟶ ((x50 x46 x46 = x46 ⟶ False) ⟶ False) ⟶ (∀ x60 . (x4 x60 x60 ⟶ False) ⟶ False) ⟶ (∀ x60 x61 x62 . (x53 x62 ⟶ False) ⟶ (x53 x60 ⟶ False) ⟶ x3 x60 (x2 x62) ⟶ x3 x61 x60 ⟶ (x47 x61 x62 x60 ⟶ False) ⟶ False) ⟶ (∀ x60 x61 x62 . (x53 x62 ⟶ False) ⟶ (x53 x60 ⟶ False) ⟶ x3 x60 (x2 x62) ⟶ x47 x61 x62 x60 ⟶ (x3 x61 x60 ⟶ False) ⟶ False) ⟶ (∀ x60 x61 . x3 x61 x49 ⟶ x10 x60 ⟶ (x0 x61 x60 = x7 x61 x60 ⟶ False) ⟶ False) ⟶ (∀ x60 x61 . x3 x61 x49 ⟶ x10 x60 ⟶ (x57 x61 x60 = x54 x61 x60 ⟶ False) ⟶ False) ⟶ (∀ x60 x61 . x3 x61 x49 ⟶ x10 x60 ⟶ (x56 x61 x60 = x50 x61 x60 ⟶ False) ⟶ False) ⟶ (∀ x60 . x3 x60 x49 ⟶ (x45 x60 = x44 x60 ⟶ False) ⟶ False) ⟶ ((x8 = x51 ⟶ False) ⟶ False) ⟶ (∀ x60 . x59 x60 ⟶ (x55 x60 = x43 x60 ⟶ False) ⟶ False) ⟶ (∀ x60 . x59 x60 ⟶ (x58 x60 = x11 x60 ⟶ False) ⟶ False) ⟶ ((x42 x41 ⟶ False) ⟶ False) ⟶ ((x53 x41 ⟶ False) ⟶ False) ⟶ ((x10 x40 ⟶ False) ⟶ False) ⟶ ((x42 x40 ⟶ False) ⟶ False) ⟶ ((x59 x40 ⟶ False) ⟶ False) ⟶ ((x53 x40 ⟶ False) ⟶ False) ⟶ ((x39 x38 ⟶ False) ⟶ False) ⟶ ((x42 x38 ⟶ False) ⟶ False) ⟶ ((x10 x37 ⟶ False) ⟶ False) ⟶ ((x39 x37 ⟶ False) ⟶ False) ⟶ ((x42 x37 ⟶ False) ⟶ False) ⟶ ((x59 x37 ⟶ False) ⟶ False) ⟶ ((x36 x35 ⟶ False) ⟶ False) ⟶ ((x12 x35 ⟶ False) ⟶ False) ⟶ (x53 x35 ⟶ False) ⟶ ((x9 x13 ⟶ False) ⟶ False) ⟶ ((x42 x13 ⟶ False) ⟶ False) ⟶ ((x10 x14 ⟶ False) ⟶ False) ⟶ ((x9 x14 ⟶ False) ⟶ False) ⟶ ((x42 x14 ⟶ False) ⟶ False) ⟶ ((x59 x14 ⟶ False) ⟶ False) ⟶ ((x59 x15 ⟶ False) ⟶ False) ⟶ (x53 x15 ⟶ False) ⟶ (x53 x16 ⟶ False) ⟶ ((x12 x34 ⟶ False) ⟶ False) ⟶ (x53 x34 ⟶ False) ⟶ ((x42 x33 ⟶ False) ⟶ False) ⟶ ((x10 x17 ⟶ False) ⟶ False) ⟶ ((x59 x32 ⟶ False) ⟶ False) ⟶ ((x53 x18 ⟶ False) ⟶ False) ⟶ ((x12 x31 ⟶ False) ⟶ False) ⟶ (x53 x31 ⟶ False) ⟶ (∀ x60 . x59 x60 ⟶ (x6 (x6 x60) = x60 ⟶ False) ⟶ False) ⟶ (∀ x60 x61 . (x39 x61 ⟶ False) ⟶ x10 x61 ⟶ (x39 x60 ⟶ False) ⟶ x10 x60 ⟶ x39 (x50 x61 x60) ⟶ False) ⟶ (∀ x60 x61 . (x53 x61 ⟶ False) ⟶ x59 x61 ⟶ (x53 x60 ⟶ False) ⟶ x59 x60 ⟶ x53 (x54 x61 x60) ⟶ False) ⟶ (x19 x49 ⟶ False) ⟶ (∀ x60 x61 . x10 x61 ⟶ x10 x60 ⟶ (x10 (x7 x61 x60) ⟶ False) ⟶ False) ⟶ (∀ x60 x61 . x10 x61 ⟶ x10 x60 ⟶ (x10 (x54 x61 x60) ⟶ False) ⟶ False) ⟶ (∀ x60 . (x53 x60 ⟶ False) ⟶ x59 x60 ⟶ (x59 (x6 x60) ⟶ False) ⟶ False) ⟶ (∀ x60 . (x53 x60 ⟶ False) ⟶ x59 x60 ⟶ x53 (x6 x60) ⟶ False) ⟶ ((x12 x51 ⟶ False) ⟶ False) ⟶ (∀ x60 x61 . x10 x61 ⟶ x10 x60 ⟶ (x10 (x50 x61 x60) ⟶ False) ⟶ False) ⟶ ((x36 x51 ⟶ False) ⟶ False) ⟶ ((x36 x49 ⟶ False) ⟶ False) ⟶ (∀ x60 x61 . x59 x61 ⟶ x59 x60 ⟶ (x59 (x7 x61 x60) ⟶ False) ⟶ False) ⟶ (∀ x60 . x10 x60 ⟶ (x10 (x6 x60) ⟶ False) ⟶ False) ⟶ (∀ x60 . x10 x60 ⟶ (x59 (x6 x60) ⟶ False) ⟶ False) ⟶ (∀ x60 x61 . x59 x61 ⟶ x59 x60 ⟶ (x59 (x54 x61 x60) ⟶ False) ⟶ False) ⟶ ((x30 x49 ⟶ False) ⟶ False) ⟶ (∀ x60 x61 . x59 x61 ⟶ x59 x60 ⟶ (x59 (x50 x61 x60) ⟶ False) ⟶ False) ⟶ (∀ x60 . x10 x60 ⟶ (x10 (x44 x60) ⟶ False) ⟶ False) ⟶ (∀ x60 . x59 x60 ⟶ (x10 (x43 x60) ⟶ False) ⟶ False) ⟶ (∀ x60 x61 . (x39 x61 ⟶ False) ⟶ x10 x61 ⟶ (x39 x60 ⟶ False) ⟶ x10 x60 ⟶ x39 (x54 x61 x60) ⟶ False) ⟶ (∀ x60 x61 . (x9 x61 ⟶ False) ⟶ x10 x61 ⟶ (x9 x60 ⟶ False) ⟶ x10 x60 ⟶ x39 (x54 x61 x60) ⟶ False) ⟶ (∀ x60 x61 . (x9 x61 ⟶ False) ⟶ x10 x61 ⟶ (x39 x60 ⟶ False) ⟶ x10 x60 ⟶ x9 (x54 x60 x61) ⟶ False) ⟶ (∀ x60 x61 . (x9 x61 ⟶ False) ⟶ x10 x61 ⟶ (x39 x60 ⟶ False) ⟶ x10 x60 ⟶ x9 (x54 x61 x60) ⟶ False) ⟶ (∀ x60 x61 . x39 x61 ⟶ x10 x61 ⟶ (x39 x60 ⟶ False) ⟶ x10 x60 ⟶ (x9 (x7 x60 x61) ⟶ False) ⟶ False) ⟶ (∀ x60 x61 . x39 x61 ⟶ x10 x61 ⟶ (x39 x60 ⟶ False) ⟶ x10 x60 ⟶ (x39 (x7 x61 x60) ⟶ False) ⟶ False) ⟶ (∀ x60 x61 . x9 x61 ⟶ x10 x61 ⟶ (x9 x60 ⟶ False) ⟶ x10 x60 ⟶ (x39 (x7 x60 x61) ⟶ False) ⟶ False) ⟶ ((x53 x52 ⟶ False) ⟶ False) ⟶ (∀ x60 . x59 x60 ⟶ (x59 (x44 x60) ⟶ False) ⟶ False) ⟶ (x53 x49 ⟶ False) ⟶ (∀ x60 . x59 x60 ⟶ (x10 (x11 x60) ⟶ False) ⟶ False) ⟶ (∀ x60 x61 . x9 x61 ⟶ x10 x61 ⟶ (x9 x60 ⟶ False) ⟶ x10 x60 ⟶ (x9 (x7 x61 x60) ⟶ False) ⟶ False) ⟶ (∀ x60 x61 . (x39 x61 ⟶ False) ⟶ x10 x61 ⟶ (x9 x60 ⟶ False) ⟶ x10 x60 ⟶ x9 (x7 x60 x61) ⟶ False) ⟶ (∀ x60 x61 . (x39 x61 ⟶ False) ⟶ x10 x61 ⟶ (x9 x60 ⟶ False) ⟶ x10 x60 ⟶ x39 (x7 x61 x60) ⟶ False) ⟶ (∀ x60 . (x39 x60 ⟶ False) ⟶ x10 x60 ⟶ x9 (x6 x60) ⟶ False) ⟶ (∀ x60 . (x39 x60 ⟶ False) ⟶ x10 x60 ⟶ (x59 (x6 x60) ⟶ False) ⟶ False) ⟶ (∀ x60 . (x9 x60 ⟶ False) ⟶ x10 x60 ⟶ x39 (x6 x60) ⟶ False) ⟶ (∀ x60 . (x9 x60 ⟶ False) ⟶ x10 x60 ⟶ (x59 (x6 x60) ⟶ False) ⟶ False) ⟶ (∀ x60 x61 . x39 x61 ⟶ x10 x61 ⟶ (x9 x60 ⟶ False) ⟶ x10 x60 ⟶ (x39 (x50 x60 x61) ⟶ False) ⟶ False) ⟶ (∀ x60 x61 . x39 x61 ⟶ x10 x61 ⟶ (x9 x60 ⟶ False) ⟶ x10 x60 ⟶ (x39 (x50 x61 x60) ⟶ False) ⟶ False) ⟶ (∀ x60 x61 . x9 x61 ⟶ x10 x61 ⟶ (x39 x60 ⟶ False) ⟶ x10 x60 ⟶ (x9 (x50 x60 x61) ⟶ False) ⟶ False) ⟶ (∀ x60 x61 . x9 x61 ⟶ x10 x61 ⟶ (x39 x60 ⟶ False) ⟶ x10 x60 ⟶ (x9 (x50 x61 x60) ⟶ False) ⟶ False) ⟶ (∀ x60 x61 . (x9 x61 ⟶ False) ⟶ x10 x61 ⟶ (x9 x60 ⟶ False) ⟶ x10 x60 ⟶ x9 (x50 x61 x60) ⟶ False) ⟶ (∀ x60 x61 . (x53 x61 ⟶ False) ⟶ (x53 x60 ⟶ False) ⟶ x3 x60 (x2 x61) ⟶ (x47 (x20 x60 x61) x61 x60 ⟶ False) ⟶ False) ⟶ (∀ x60 . (x3 (x29 x60) x60 ⟶ False) ⟶ False) ⟶ (∀ x60 x61 x62 . (x53 x62 ⟶ False) ⟶ (x53 x60 ⟶ False) ⟶ x3 x60 (x2 x62) ⟶ x47 x61 x62 x60 ⟶ (x3 x61 x62 ⟶ False) ⟶ False) ⟶ (∀ x60 x61 . x3 x61 x49 ⟶ x10 x60 ⟶ (x3 (x0 x61 x60) x49 ⟶ False) ⟶ False) ⟶ (∀ x60 x61 . x3 x61 x49 ⟶ x10 x60 ⟶ (x3 (x57 x61 x60) x49 ⟶ False) ⟶ False) ⟶ (∀ x60 x61 . x3 x61 x49 ⟶ x10 x60 ⟶ (x3 (x56 x61 x60) x49 ⟶ False) ⟶ False) ⟶ (∀ x60 . x3 x60 x49 ⟶ (x3 (x45 x60) x49 ⟶ False) ⟶ False) ⟶ ((x3 x8 (x2 x49) ⟶ False) ⟶ False) ⟶ (∀ x60 . x59 x60 ⟶ (x59 (x6 x60) ⟶ False) ⟶ False) ⟶ (∀ x60 . x59 x60 ⟶ (x3 (x55 x60) x49 ⟶ False) ⟶ False) ⟶ (∀ x60 . x59 x60 ⟶ (x3 (x58 x60) x49 ⟶ False) ⟶ False) ⟶ (∀ x60 . x59 x60 ⟶ (x44 x60 = x54 x60 x60 ⟶ False) ⟶ False) ⟶ (∀ x60 x61 . x3 x61 x49 ⟶ x10 x60 ⟶ (x57 x61 x60 = x57 x60 x61 ⟶ False) ⟶ False) ⟶ (∀ x60 x61 . x3 x61 x49 ⟶ x10 x60 ⟶ (x56 x61 x60 = x56 x60 x61 ⟶ False) ⟶ False) ⟶ (∀ x60 x61 . x59 x61 ⟶ x59 x60 ⟶ (x54 x61 x60 = x54 x60 x61 ⟶ False) ⟶ False) ⟶ (∀ x60 x61 . x59 x61 ⟶ x59 x60 ⟶ (x50 x61 x60 = x50 x60 x61 ⟶ False) ⟶ False) ⟶ (∀ x60 . x42 x60 ⟶ (x9 x60 ⟶ False) ⟶ (x39 x60 ⟶ False) ⟶ (x42 x60 ⟶ False) ⟶ False) ⟶ (∀ x60 . x42 x60 ⟶ (x9 x60 ⟶ False) ⟶ (x39 x60 ⟶ False) ⟶ (x53 x60 ⟶ False) ⟶ False) ⟶ (∀ x60 . x3 x60 (x2 x49) ⟶ (x30 x60 ⟶ False) ⟶ False) ⟶ (∀ x60 . x53 x60 ⟶ x42 x60 ⟶ x39 x60 ⟶ False) ⟶ (∀ x60 . x53 x60 ⟶ x42 x60 ⟶ x9 x60 ⟶ False) ⟶ (∀ x60 . x53 x60 ⟶ x42 x60 ⟶ (x42 x60 ⟶ False) ⟶ False) ⟶ (∀ x60 . (x53 x60 ⟶ False) ⟶ x42 x60 ⟶ (x9 x60 ⟶ False) ⟶ (x39 x60 ⟶ False) ⟶ False) ⟶ (∀ x60 . (x53 x60 ⟶ False) ⟶ x42 x60 ⟶ (x9 x60 ⟶ False) ⟶ (x42 x60 ⟶ False) ⟶ False) ⟶ (∀ x60 . x42 x60 ⟶ x39 x60 ⟶ x9 x60 ⟶ False) ⟶ (∀ x60 . x42 x60 ⟶ x39 x60 ⟶ (x42 x60 ⟶ False) ⟶ False) ⟶ (∀ x60 . x42 x60 ⟶ x39 x60 ⟶ x53 x60 ⟶ False) ⟶ (∀ x60 . x30 x60 ⟶ (x28 x60 ⟶ False) ⟶ False) ⟶ (∀ x60 . (x53 x60 ⟶ False) ⟶ x42 x60 ⟶ (x39 x60 ⟶ False) ⟶ (x9 x60 ⟶ False) ⟶ False) ⟶ (∀ x60 . (x53 x60 ⟶ False) ⟶ x42 x60 ⟶ (x39 x60 ⟶ False) ⟶ (x42 x60 ⟶ False) ⟶ False) ⟶ (∀ x60 . x10 x60 ⟶ (x42 x60 ⟶ False) ⟶ False) ⟶ (∀ x60 . x30 x60 ⟶ (x27 x60 ⟶ False) ⟶ False) ⟶ (∀ x60 . x42 x60 ⟶ x9 x60 ⟶ x39 x60 ⟶ False) ⟶ (∀ x60 . x42 x60 ⟶ x9 x60 ⟶ (x42 x60 ⟶ False) ⟶ False) ⟶ (∀ x60 . x42 x60 ⟶ x9 x60 ⟶ x53 x60 ⟶ False) ⟶ (∀ x60 . x10 x60 ⟶ (x59 x60 ⟶ False) ⟶ False) ⟶ (∀ x60 . x21 x60 ⟶ (x30 x60 ⟶ False) ⟶ False) ⟶ (∀ x60 . x26 x60 ⟶ (x42 x60 ⟶ False) ⟶ False) ⟶ (∀ x60 . x26 x60 ⟶ (x10 x60 ⟶ False) ⟶ False) ⟶ (∀ x60 . x26 x60 ⟶ (x59 x60 ⟶ False) ⟶ False) ⟶ (∀ x60 . x22 x60 ⟶ (x21 x60 ⟶ False) ⟶ False) ⟶ (∀ x60 . x53 x60 ⟶ (x36 x60 ⟶ False) ⟶ False) ⟶ (∀ x60 . x3 x60 x8 ⟶ (x12 x60 ⟶ False) ⟶ False) ⟶ (∀ x60 x61 . x12 x61 ⟶ x3 x60 (x2 x61) ⟶ (x12 x60 ⟶ False) ⟶ False) ⟶ (∀ x60 x61 . x22 x61 ⟶ x3 x60 (x2 x61) ⟶ (x22 x60 ⟶ False) ⟶ False) ⟶ (∀ x60 x61 . x21 x61 ⟶ x3 x60 (x2 x61) ⟶ (x21 x60 ⟶ False) ⟶ False) ⟶ (∀ x60 x61 . x30 x61 ⟶ x3 x60 (x2 x61) ⟶ (x30 x60 ⟶ False) ⟶ False) ⟶ (∀ x60 x61 . x27 x61 ⟶ x3 x60 (x2 x61) ⟶ (x27 x60 ⟶ False) ⟶ False) ⟶ (∀ x60 . x3 x60 x49 ⟶ (x10 x60 ⟶ False) ⟶ False) ⟶ (∀ x60 . x3 x60 x49 ⟶ (x59 x60 ⟶ False) ⟶ False) ⟶ (∀ x60 . x12 x60 ⟶ (x22 x60 ⟶ False) ⟶ False) ⟶ (∀ x60 x61 . x28 x61 ⟶ x3 x60 (x2 x61) ⟶ (x28 x60 ⟶ False) ⟶ False) ⟶ (∀ x60 . x53 x60 ⟶ (x12 x60 ⟶ False) ⟶ False) ⟶ (∀ x60 x61 . x12 x61 ⟶ x3 x60 x61 ⟶ (x26 x60 ⟶ False) ⟶ False) ⟶ (∀ x60 x61 . x22 x61 ⟶ x3 x60 x61 ⟶ (x23 x60 ⟶ False) ⟶ False) ⟶ (∀ x60 x61 . x21 x61 ⟶ x3 x60 x61 ⟶ (x25 x60 ⟶ False) ⟶ False) ⟶ (∀ x60 x61 . x30 x61 ⟶ x3 x60 x61 ⟶ (x10 x60 ⟶ False) ⟶ False) ⟶ (∀ x60 x61 . x27 x61 ⟶ x3 x60 x61 ⟶ (x42 x60 ⟶ False) ⟶ False) ⟶ (∀ x60 x61 . x28 x61 ⟶ x3 x60 x61 ⟶ (x59 x60 ⟶ False) ⟶ False) ⟶ (∀ x60 . x3 x60 (x2 x8) ⟶ (x12 x60 ⟶ False) ⟶ False) ⟶ (∀ x60 x61 . x1 x60 x61 ⟶ x1 x61 x60 ⟶ False) ⟶ (x58 (x54 x24 x24) = x0 (x45 (x58 x24)) (x45 (x55 x24)) ⟶ x55 (x54 x24 x24) = x57 x48 (x57 (x58 x24) (x55 x24)) ⟶ False) ⟶ ((x59 x24 ⟶ False) ⟶ False) ⟶ False (proof)