Search for blocks/addresses/...

Proofgold Asset

asset id
480ee4887d686a22172064b5dee96becd8457ff50ba22037eb120086d140faf6
asset hash
3bed210d664cc2db55c34245bfc35fde7a801fdacc828a023d83e4bf76ca0995
bday / block
35136
tx
23518..
preasset
doc published by PrPhD..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0 ⟶ False
Theorem df410.. : ∀ 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 . x58 x60 ⟶ (x60 = x59 ⟶ False) ⟶ x58 x59 ⟶ False) ⟶ (∀ x59 x60 . x0 x59 x60 ⟶ x58 x60 ⟶ False) ⟶ (∀ x59 . x58 x59 ⟶ (x59 = x57 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 x61 . x0 x59 x60 ⟶ x2 x60 (x1 x61) ⟶ x58 x61 ⟶ False) ⟶ (∀ x59 x60 x61 . x0 x60 x61 ⟶ x2 x61 (x1 x59) ⟶ (x2 x60 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 . x3 x60 x59 ⟶ (x2 x60 (x1 x59) ⟶ False) ⟶ False) ⟶ (∀ x59 x60 . x2 x60 (x1 x59) ⟶ (x3 x60 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 . (x4 x60 ⟶ False) ⟶ x16 x60 ⟶ x5 x60 ⟶ x15 x59 ⟶ x7 x59 (x6 x60) (x6 x60) ⟶ x14 x59 (x6 x60) (x6 x60) ⟶ x2 x59 (x1 (x8 (x6 x60) (x6 x60))) ⟶ x9 x60 (x10 x59 x60) (x12 x59 x60) (x11 (x6 x60) (x6 x60) x59 (x10 x59 x60)) (x11 (x6 x60) (x6 x60) x59 (x12 x59 x60)) ⟶ (x13 x59 x60 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 . (x4 x60 ⟶ False) ⟶ x16 x60 ⟶ x5 x60 ⟶ x15 x59 ⟶ x7 x59 (x6 x60) (x6 x60) ⟶ x14 x59 (x6 x60) (x6 x60) ⟶ x2 x59 (x1 (x8 (x6 x60) (x6 x60))) ⟶ (x2 (x12 x59 x60) (x6 x60) ⟶ False) ⟶ (x13 x59 x60 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 . (x4 x60 ⟶ False) ⟶ x16 x60 ⟶ x5 x60 ⟶ x15 x59 ⟶ x7 x59 (x6 x60) (x6 x60) ⟶ x14 x59 (x6 x60) (x6 x60) ⟶ x2 x59 (x1 (x8 (x6 x60) (x6 x60))) ⟶ (x2 (x10 x59 x60) (x6 x60) ⟶ False) ⟶ (x13 x59 x60 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 x61 x62 . (x4 x62 ⟶ False) ⟶ x16 x62 ⟶ x5 x62 ⟶ x15 x59 ⟶ x7 x59 (x6 x62) (x6 x62) ⟶ x14 x59 (x6 x62) (x6 x62) ⟶ x2 x59 (x1 (x8 (x6 x62) (x6 x62))) ⟶ x13 x59 x62 ⟶ x2 x61 (x6 x62) ⟶ x2 x60 (x6 x62) ⟶ (x9 x62 x61 x60 (x11 (x6 x62) (x6 x62) x59 x61) (x11 (x6 x62) (x6 x62) x59 x60) ⟶ False) ⟶ False) ⟶ (∀ x59 x60 x61 x62 x63 x64 . (x4 x64 ⟶ False) ⟶ x16 x64 ⟶ x5 x64 ⟶ x2 x59 (x6 x64) ⟶ x2 x63 (x6 x64) ⟶ x2 x60 (x6 x64) ⟶ x2 x62 (x6 x64) ⟶ x2 x61 (x6 x64) ⟶ x17 x64 x59 x63 x60 ⟶ x17 x64 x59 x63 x62 ⟶ x17 x64 x59 x63 x61 ⟶ (x59 = x63 ⟶ False) ⟶ (x17 x64 x60 x62 x61 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 x61 . (x4 x61 ⟶ False) ⟶ x16 x61 ⟶ x5 x61 ⟶ x2 x59 (x6 x61) ⟶ x2 x60 (x6 x61) ⟶ (x17 x61 x59 x60 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 x61 . (x4 x61 ⟶ False) ⟶ x16 x61 ⟶ x5 x61 ⟶ x2 x59 (x6 x61) ⟶ x2 x60 (x6 x61) ⟶ (x17 x61 x59 x60 x60 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 x61 . (x4 x61 ⟶ False) ⟶ x16 x61 ⟶ x5 x61 ⟶ x2 x59 (x6 x61) ⟶ x2 x60 (x6 x61) ⟶ (x17 x61 x59 x59 x60 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 x61 x62 . (x4 x62 ⟶ False) ⟶ x16 x62 ⟶ x5 x62 ⟶ x2 x59 (x6 x62) ⟶ x2 x61 (x6 x62) ⟶ x2 x60 (x6 x62) ⟶ x17 x62 x59 x61 x60 ⟶ (x17 x62 x60 x61 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 x61 x62 . (x4 x62 ⟶ False) ⟶ x16 x62 ⟶ x5 x62 ⟶ x2 x59 (x6 x62) ⟶ x2 x61 (x6 x62) ⟶ x2 x60 (x6 x62) ⟶ x17 x62 x59 x61 x60 ⟶ (x17 x62 x60 x59 x61 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 x61 x62 . (x4 x62 ⟶ False) ⟶ x16 x62 ⟶ x5 x62 ⟶ x2 x59 (x6 x62) ⟶ x2 x61 (x6 x62) ⟶ x2 x60 (x6 x62) ⟶ x17 x62 x59 x61 x60 ⟶ (x17 x62 x61 x60 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 x61 x62 . (x4 x62 ⟶ False) ⟶ x16 x62 ⟶ x5 x62 ⟶ x2 x59 (x6 x62) ⟶ x2 x61 (x6 x62) ⟶ x2 x60 (x6 x62) ⟶ x17 x62 x59 x61 x60 ⟶ (x17 x62 x61 x59 x60 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 x61 x62 . (x4 x62 ⟶ False) ⟶ x16 x62 ⟶ x5 x62 ⟶ x2 x59 (x6 x62) ⟶ x2 x61 (x6 x62) ⟶ x2 x60 (x6 x62) ⟶ x17 x62 x59 x61 x60 ⟶ (x17 x62 x59 x60 x61 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 . x2 x59 x60 ⟶ (x58 x60 ⟶ False) ⟶ (x0 x59 x60 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 . x0 x60 x59 ⟶ (x2 x60 x59 ⟶ False) ⟶ False) ⟶ (x58 x56 ⟶ False) ⟶ (∀ x59 . (x3 x59 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 x61 x62 . (x58 x62 ⟶ False) ⟶ x15 x59 ⟶ x7 x59 x62 x61 ⟶ x2 x59 (x1 (x8 x62 x61)) ⟶ x2 x60 x62 ⟶ (x11 x62 x61 x59 x60 = x55 x59 x60 ⟶ False) ⟶ False) ⟶ ((x18 x19 ⟶ False) ⟶ False) ⟶ (x58 x19 ⟶ False) ⟶ (∀ x59 x60 . (x15 (x20 x59 x60) ⟶ False) ⟶ False) ⟶ (∀ x59 x60 . (x54 (x20 x59 x60) x59 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 . (x21 (x20 x60 x59) x59 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 . (x53 (x20 x59 x60) ⟶ False) ⟶ False) ⟶ (x22 x23 ⟶ False) ⟶ ((x15 x23 ⟶ False) ⟶ False) ⟶ ((x53 x23 ⟶ False) ⟶ False) ⟶ (∀ x59 . (x52 x59 ⟶ False) ⟶ x50 x59 ⟶ x58 (x51 x59) ⟶ False) ⟶ (∀ x59 . (x52 x59 ⟶ False) ⟶ x50 x59 ⟶ (x2 (x51 x59) (x1 (x6 x59)) ⟶ False) ⟶ False) ⟶ (∀ x59 x60 . (x58 x60 ⟶ False) ⟶ (x58 x59 ⟶ False) ⟶ x58 (x49 x59 x60) ⟶ False) ⟶ (∀ x59 x60 . (x58 x60 ⟶ False) ⟶ (x58 x59 ⟶ False) ⟶ (x15 (x49 x59 x60) ⟶ False) ⟶ False) ⟶ (∀ x59 x60 . (x58 x60 ⟶ False) ⟶ (x58 x59 ⟶ False) ⟶ (x54 (x49 x59 x60) x59 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 . (x58 x60 ⟶ False) ⟶ (x58 x59 ⟶ False) ⟶ (x21 (x49 x59 x60) x60 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 . (x58 x60 ⟶ False) ⟶ (x58 x59 ⟶ False) ⟶ (x53 (x49 x59 x60) ⟶ False) ⟶ False) ⟶ (∀ x59 x60 . (x58 x60 ⟶ False) ⟶ (x58 x59 ⟶ False) ⟶ (x2 (x49 x59 x60) (x1 (x8 x60 x59)) ⟶ False) ⟶ False) ⟶ (x58 x48 ⟶ False) ⟶ (∀ x59 . (x14 (x24 x59) x59 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 . (x7 (x24 x59) x59 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 . (x25 (x24 x59) x59 ⟶ False) ⟶ False) ⟶ (∀ x59 . (x15 (x24 x59) ⟶ False) ⟶ False) ⟶ (∀ x59 . (x54 (x24 x59) x59 ⟶ False) ⟶ False) ⟶ (∀ x59 . (x21 (x24 x59) x59 ⟶ False) ⟶ False) ⟶ (∀ x59 . (x53 (x24 x59) ⟶ False) ⟶ False) ⟶ (∀ x59 . (x2 (x24 x59) (x1 (x8 x59 x59)) ⟶ False) ⟶ False) ⟶ ((x26 x27 ⟶ False) ⟶ False) ⟶ ((x15 x27 ⟶ False) ⟶ False) ⟶ ((x53 x27 ⟶ False) ⟶ False) ⟶ (∀ x59 . (x4 x59 ⟶ False) ⟶ x50 x59 ⟶ x47 (x46 x59) ⟶ False) ⟶ (∀ x59 . (x4 x59 ⟶ False) ⟶ x50 x59 ⟶ (x2 (x46 x59) (x1 (x6 x59)) ⟶ False) ⟶ False) ⟶ (∀ x59 . (x52 x59 ⟶ False) ⟶ x50 x59 ⟶ (x47 (x45 x59) ⟶ False) ⟶ False) ⟶ (∀ x59 . (x52 x59 ⟶ False) ⟶ x50 x59 ⟶ x58 (x45 x59) ⟶ False) ⟶ (∀ x59 . (x52 x59 ⟶ False) ⟶ x50 x59 ⟶ (x2 (x45 x59) (x1 (x6 x59)) ⟶ False) ⟶ False) ⟶ ((x58 x28 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 . (x54 (x44 x59 x60) x59 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 . (x21 (x44 x60 x59) x59 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 . (x53 (x44 x59 x60) ⟶ False) ⟶ False) ⟶ (∀ x59 x60 . (x58 (x44 x59 x60) ⟶ False) ⟶ False) ⟶ (∀ x59 x60 . (x2 (x44 x59 x60) (x1 (x8 x60 x59)) ⟶ False) ⟶ False) ⟶ (∀ x59 x60 . (x15 (x29 x59 x60) ⟶ False) ⟶ False) ⟶ (∀ x59 x60 . (x54 (x29 x59 x60) x59 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 . (x21 (x29 x60 x59) x59 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 . (x53 (x29 x59 x60) ⟶ False) ⟶ False) ⟶ (∀ x59 x60 . (x2 (x29 x59 x60) (x1 (x8 x60 x59)) ⟶ False) ⟶ False) ⟶ (∀ x59 x60 . (x7 (x43 x59 x60) x60 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 . (x15 (x43 x59 x60) ⟶ False) ⟶ False) ⟶ (∀ x59 x60 . (x54 (x43 x59 x60) x59 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 . (x21 (x43 x60 x59) x59 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 . (x53 (x43 x59 x60) ⟶ False) ⟶ False) ⟶ (∀ x59 x60 . (x2 (x43 x59 x60) (x1 (x8 x60 x59)) ⟶ False) ⟶ False) ⟶ ((x15 x42 ⟶ False) ⟶ False) ⟶ ((x53 x42 ⟶ False) ⟶ False) ⟶ (∀ x59 . (x41 x59 ⟶ False) ⟶ x50 x59 ⟶ x40 (x6 x59) ⟶ False) ⟶ (∀ x59 . x41 x59 ⟶ x50 x59 ⟶ (x40 (x6 x59) ⟶ False) ⟶ False) ⟶ (∀ x59 . x4 x59 ⟶ x50 x59 ⟶ (x47 (x6 x59) ⟶ False) ⟶ False) ⟶ (∀ x59 . (x4 x59 ⟶ False) ⟶ x50 x59 ⟶ x47 (x6 x59) ⟶ False) ⟶ (∀ x59 . (x52 x59 ⟶ False) ⟶ x50 x59 ⟶ x58 (x6 x59) ⟶ False) ⟶ ((x58 x57 ⟶ False) ⟶ False) ⟶ (∀ x59 . x52 x59 ⟶ x50 x59 ⟶ (x58 (x6 x59) ⟶ False) ⟶ False) ⟶ (∀ x59 x60 x61 . x18 x61 ⟶ x53 x59 ⟶ x54 x59 x61 ⟶ x15 x59 ⟶ (x15 (x55 x59 x60) ⟶ False) ⟶ False) ⟶ (∀ x59 x60 x61 . x18 x61 ⟶ x53 x59 ⟶ x54 x59 x61 ⟶ x15 x59 ⟶ (x53 (x55 x59 x60) ⟶ False) ⟶ False) ⟶ (∀ x59 . (x2 (x30 x59) x59 ⟶ False) ⟶ False) ⟶ ((x50 x39 ⟶ False) ⟶ False) ⟶ ((x5 x31 ⟶ False) ⟶ False) ⟶ (∀ x59 . x5 x59 ⟶ (x50 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 x61 x62 . (x58 x62 ⟶ False) ⟶ x15 x59 ⟶ x7 x59 x62 x61 ⟶ x2 x59 (x1 (x8 x62 x61)) ⟶ x2 x60 x62 ⟶ (x2 (x11 x62 x61 x59 x60) x61 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 x61 x62 . (x52 x62 ⟶ False) ⟶ x5 x62 ⟶ x2 x61 (x6 x62) ⟶ x2 x59 (x6 x62) ⟶ x2 x60 (x6 x62) ⟶ x9 x62 x61 x59 x61 x60 ⟶ (x17 x62 x61 x59 x60 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 x61 x62 . (x52 x62 ⟶ False) ⟶ x5 x62 ⟶ x2 x61 (x6 x62) ⟶ x2 x59 (x6 x62) ⟶ x2 x60 (x6 x62) ⟶ x17 x62 x61 x59 x60 ⟶ (x9 x62 x61 x59 x61 x60 ⟶ False) ⟶ False) ⟶ (∀ x59 . x50 x59 ⟶ x38 x59 x57 ⟶ (x52 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 . x18 x60 ⟶ x2 x59 (x1 x60) ⟶ (x18 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 . x50 x59 ⟶ x52 x59 ⟶ (x38 x59 x57 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 x61 . (x58 x61 ⟶ False) ⟶ (x58 x59 ⟶ False) ⟶ x2 x60 (x1 (x8 x61 x59)) ⟶ x15 x60 ⟶ x7 x60 x61 x59 ⟶ (x7 x60 x61 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 x61 . (x58 x61 ⟶ False) ⟶ (x58 x59 ⟶ False) ⟶ x2 x60 (x1 (x8 x61 x59)) ⟶ x15 x60 ⟶ x7 x60 x61 x59 ⟶ x58 x60 ⟶ False) ⟶ (∀ x59 x60 x61 . (x58 x61 ⟶ False) ⟶ (x58 x59 ⟶ False) ⟶ x2 x60 (x1 (x8 x61 x59)) ⟶ x15 x60 ⟶ x7 x60 x61 x59 ⟶ (x15 x60 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 . x18 x60 ⟶ x2 x59 x60 ⟶ (x15 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 . x18 x60 ⟶ x2 x59 x60 ⟶ (x53 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 . x50 x59 ⟶ (x41 x59 ⟶ False) ⟶ x4 x59 ⟶ False) ⟶ (∀ x59 . x58 x59 ⟶ (x18 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 . x50 x59 ⟶ x4 x59 ⟶ (x41 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 x61 . x2 x61 (x1 (x8 x59 x60)) ⟶ x15 x61 ⟶ x26 x61 ⟶ x32 x61 x60 ⟶ (x14 x61 x59 x60 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 x61 . x2 x61 (x1 (x8 x59 x60)) ⟶ x15 x61 ⟶ x26 x61 ⟶ x32 x61 x60 ⟶ (x15 x61 ⟶ False) ⟶ False) ⟶ (∀ x59 . x47 x59 ⟶ x53 x59 ⟶ x15 x59 ⟶ (x22 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 . x47 x59 ⟶ x53 x59 ⟶ x15 x59 ⟶ (x15 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 . x47 x59 ⟶ x53 x59 ⟶ x15 x59 ⟶ (x53 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 . x50 x59 ⟶ (x41 x59 ⟶ False) ⟶ x41 x59 ⟶ False) ⟶ (∀ x59 . x50 x59 ⟶ (x41 x59 ⟶ False) ⟶ x52 x59 ⟶ False) ⟶ (∀ x59 x60 x61 . x2 x61 (x1 (x8 x60 x59)) ⟶ x15 x61 ⟶ x14 x61 x60 x59 ⟶ (x32 x61 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 x61 . x2 x61 (x1 (x8 x60 x59)) ⟶ x15 x61 ⟶ x14 x61 x60 x59 ⟶ (x26 x61 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 x61 . x2 x61 (x1 (x8 x60 x59)) ⟶ x15 x61 ⟶ x14 x61 x60 x59 ⟶ (x15 x61 ⟶ False) ⟶ False) ⟶ (∀ x59 . x53 x59 ⟶ x15 x59 ⟶ (x22 x59 ⟶ False) ⟶ (x15 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 . x53 x59 ⟶ x15 x59 ⟶ (x22 x59 ⟶ False) ⟶ (x53 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 . x53 x59 ⟶ x15 x59 ⟶ (x22 x59 ⟶ False) ⟶ x47 x59 ⟶ False) ⟶ (∀ x59 . x50 x59 ⟶ x52 x59 ⟶ (x41 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 . x50 x59 ⟶ x52 x59 ⟶ (x52 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 x61 . x58 x61 ⟶ x2 x59 (x1 (x8 x60 x61)) ⟶ (x58 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 . x2 x60 (x1 (x8 x59 x59)) ⟶ x7 x60 x59 x59 ⟶ (x25 x60 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 . x58 x59 ⟶ x53 x59 ⟶ x15 x59 ⟶ (x22 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 . x58 x59 ⟶ x53 x59 ⟶ x15 x59 ⟶ (x15 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 . x58 x59 ⟶ x53 x59 ⟶ x15 x59 ⟶ (x53 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 x61 . x58 x61 ⟶ x2 x59 (x1 (x8 x61 x60)) ⟶ (x58 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 x61 . (x58 x61 ⟶ False) ⟶ x2 x59 (x1 (x8 x60 x61)) ⟶ x7 x59 x60 x61 ⟶ (x25 x59 x60 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 . x53 x60 ⟶ x15 x60 ⟶ x2 x59 (x1 x60) ⟶ (x15 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 . x50 x59 ⟶ (x4 x59 ⟶ False) ⟶ x52 x59 ⟶ False) ⟶ (∀ x59 x60 x61 . x2 x61 (x1 (x8 x59 x60)) ⟶ (x54 x61 x60 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 x61 . x2 x61 (x1 (x8 x60 x59)) ⟶ (x21 x61 x60 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 x61 . (x58 x61 ⟶ False) ⟶ x58 x59 ⟶ x2 x60 (x1 (x8 x61 x59)) ⟶ x25 x60 x61 ⟶ False) ⟶ (∀ x59 x60 x61 . x58 x61 ⟶ x2 x59 (x1 (x8 x61 x60)) ⟶ x7 x59 x61 x60 ⟶ (x25 x59 x61 ⟶ False) ⟶ False) ⟶ (∀ x59 . x58 x59 ⟶ x53 x59 ⟶ x15 x59 ⟶ (x26 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 . x58 x59 ⟶ x53 x59 ⟶ x15 x59 ⟶ (x15 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 . x58 x59 ⟶ x53 x59 ⟶ x15 x59 ⟶ (x53 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 . x50 x59 ⟶ x52 x59 ⟶ (x4 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 x61 . x2 x61 (x1 (x8 x59 x60)) ⟶ (x53 x61 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 x61 . x58 x61 ⟶ x2 x59 (x1 (x8 x61 x60)) ⟶ (x25 x59 x61 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 x61 . x2 x60 (x1 (x8 x61 x59)) ⟶ x25 x60 x61 ⟶ (x7 x60 x61 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 . x58 x59 ⟶ (x15 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 . x50 x59 ⟶ (x4 x59 ⟶ False) ⟶ x52 x59 ⟶ False) ⟶ (∀ x59 . x50 x59 ⟶ x38 x59 x56 ⟶ (x4 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 . x50 x59 ⟶ x38 x59 x56 ⟶ x52 x59 ⟶ False) ⟶ (∀ x59 . x50 x59 ⟶ (x52 x59 ⟶ False) ⟶ x4 x59 ⟶ (x38 x59 x56 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 . x0 x59 x60 ⟶ x0 x60 x59 ⟶ False) ⟶ (x11 (x6 x36) (x6 x36) x37 x35 = x35 ⟶ False) ⟶ (x17 x36 x34 x33 x35 ⟶ False) ⟶ ((x11 (x6 x36) (x6 x36) x37 x33 = x33 ⟶ False) ⟶ False) ⟶ ((x11 (x6 x36) (x6 x36) x37 x34 = x34 ⟶ False) ⟶ False) ⟶ ((x13 x37 x36 ⟶ False) ⟶ False) ⟶ ((x2 x37 (x1 (x8 (x6 x36) (x6 x36))) ⟶ False) ⟶ False) ⟶ ((x14 x37 (x6 x36) (x6 x36) ⟶ False) ⟶ False) ⟶ ((x7 x37 (x6 x36) (x6 x36) ⟶ False) ⟶ False) ⟶ ((x15 x37 ⟶ False) ⟶ False) ⟶ ((x2 x35 (x6 x36) ⟶ False) ⟶ False) ⟶ ((x2 x33 (x6 x36) ⟶ False) ⟶ False) ⟶ ((x2 x34 (x6 x36) ⟶ False) ⟶ False) ⟶ ((x5 x36 ⟶ False) ⟶ False) ⟶ ((x16 x36 ⟶ False) ⟶ False) ⟶ (x4 x36 ⟶ False) ⟶ False (proof)