Search for blocks/addresses/...

Proofgold Asset

asset id
62e9358e0216c62a358806f0b3b7447acae41c68d0b2fdba921eab161119ff77
asset hash
17f0a85b417d810405ca724f30841bcd94d75b300df1bf76f8cd5a014dfb970d
bday / block
35118
tx
c942b..
preasset
doc published by PrPhD..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0 ⟶ False
Theorem cc4cd.. : ∀ 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 x78 . x76 x78 ⟶ (x78 = x77 ⟶ False) ⟶ x76 x77 ⟶ False) ⟶ (∀ x77 x78 . x0 x77 x78 ⟶ x76 x78 ⟶ False) ⟶ (∀ x77 . x76 x77 ⟶ (x77 = x75 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 x79 x80 . (x1 x80 ⟶ False) ⟶ (x15 x80 ⟶ False) ⟶ x2 x80 ⟶ x14 x80 ⟶ x3 x80 ⟶ x13 x80 ⟶ x4 x80 ⟶ x12 x80 ⟶ (x1 x79 ⟶ False) ⟶ (x15 x79 ⟶ False) ⟶ x2 x79 ⟶ x14 x79 ⟶ x3 x79 ⟶ x13 x79 ⟶ x4 x79 ⟶ x12 x79 ⟶ x5 x78 x80 x79 ⟶ x10 x77 (x11 x80) ⟶ (x9 (x7 x80) (x7 x79) x78 (x8 x80 x77) = x8 x79 (x9 (x11 x80) (x11 x79) (x6 x80 x79 x78) x77) ⟶ False) ⟶ False) ⟶ (∀ x77 x78 x79 . x0 x77 x78 ⟶ x10 x78 (x74 x79) ⟶ x76 x79 ⟶ False) ⟶ (∀ x77 x78 x79 . x0 x78 x79 ⟶ x10 x79 (x74 x77) ⟶ (x10 x78 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 . x73 x78 x77 ⟶ (x10 x78 (x74 x77) ⟶ False) ⟶ False) ⟶ (∀ x77 x78 . x10 x78 (x74 x77) ⟶ (x73 x78 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 . x10 x77 x78 ⟶ (x76 x78 ⟶ False) ⟶ (x0 x77 x78 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 . (x1 x78 ⟶ False) ⟶ (x15 x78 ⟶ False) ⟶ x2 x78 ⟶ x14 x78 ⟶ x3 x78 ⟶ x13 x78 ⟶ x4 x78 ⟶ x12 x78 ⟶ x10 x77 (x11 (x16 x78)) ⟶ (x18 x78 (x8 (x16 x78) x77) = x8 x78 (x17 x78 x77) ⟶ False) ⟶ False) ⟶ (∀ x77 x78 . x0 x78 x77 ⟶ (x10 x78 x77 ⟶ False) ⟶ False) ⟶ (x76 x19 ⟶ False) ⟶ (∀ x77 . (x73 x77 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 x79 x80 . (x76 x80 ⟶ False) ⟶ x23 x77 ⟶ x20 x77 x80 x79 ⟶ x10 x77 (x74 (x21 x80 x79)) ⟶ x10 x78 x80 ⟶ (x9 x80 x79 x77 x78 = x22 x77 x78 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 x79 x80 . (x76 x80 ⟶ False) ⟶ (x76 x77 ⟶ False) ⟶ (x76 x79 ⟶ False) ⟶ x23 x78 ⟶ x10 x78 (x74 (x21 (x21 x80 x77) x79)) ⟶ (x72 x80 x77 x79 x78 = x71 x78 ⟶ False) ⟶ False) ⟶ (∀ x77 . (x1 x77 ⟶ False) ⟶ x25 x77 ⟶ x76 (x24 x77) ⟶ False) ⟶ (∀ x77 . (x1 x77 ⟶ False) ⟶ x25 x77 ⟶ (x10 (x24 x77) (x74 (x11 x77)) ⟶ False) ⟶ False) ⟶ ((x4 x26 ⟶ False) ⟶ False) ⟶ ((x13 x26 ⟶ False) ⟶ False) ⟶ ((x3 x26 ⟶ False) ⟶ False) ⟶ ((x14 x26 ⟶ False) ⟶ False) ⟶ ((x2 x26 ⟶ False) ⟶ False) ⟶ ((x70 x26 ⟶ False) ⟶ False) ⟶ ((x27 x26 ⟶ False) ⟶ False) ⟶ (x15 x26 ⟶ False) ⟶ (x1 x26 ⟶ False) ⟶ ((x12 x26 ⟶ False) ⟶ False) ⟶ (x76 x28 ⟶ False) ⟶ (x15 x69 ⟶ False) ⟶ (x1 x69 ⟶ False) ⟶ ((x12 x69 ⟶ False) ⟶ False) ⟶ (x29 x30 ⟶ False) ⟶ ((x68 x30 ⟶ False) ⟶ False) ⟶ (∀ x77 . (x31 x77 ⟶ False) ⟶ x25 x77 ⟶ x32 (x33 x77) ⟶ False) ⟶ (∀ x77 . (x31 x77 ⟶ False) ⟶ x25 x77 ⟶ (x10 (x33 x77) (x74 (x11 x77)) ⟶ False) ⟶ False) ⟶ (∀ x77 . (x1 x77 ⟶ False) ⟶ x25 x77 ⟶ (x32 (x34 x77) ⟶ False) ⟶ False) ⟶ (∀ x77 . (x1 x77 ⟶ False) ⟶ x25 x77 ⟶ x76 (x34 x77) ⟶ False) ⟶ (∀ x77 . (x1 x77 ⟶ False) ⟶ x25 x77 ⟶ (x10 (x34 x77) (x74 (x11 x77)) ⟶ False) ⟶ False) ⟶ ((x76 x67 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 . (x35 (x36 x77 x78) x77 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 . (x66 (x36 x78 x77) x77 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 . (x37 (x36 x77 x78) ⟶ False) ⟶ False) ⟶ (∀ x77 x78 . (x76 (x36 x77 x78) ⟶ False) ⟶ False) ⟶ (∀ x77 x78 . (x10 (x36 x77 x78) (x74 (x21 x78 x77)) ⟶ False) ⟶ False) ⟶ (∀ x77 x78 . (x20 (x65 x77 x78) x78 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 . (x23 (x65 x77 x78) ⟶ False) ⟶ False) ⟶ (∀ x77 x78 . (x35 (x65 x77 x78) x77 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 . (x66 (x65 x78 x77) x77 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 . (x37 (x65 x77 x78) ⟶ False) ⟶ False) ⟶ (∀ x77 x78 . (x10 (x65 x77 x78) (x74 (x21 x78 x77)) ⟶ False) ⟶ False) ⟶ ((x70 x64 ⟶ False) ⟶ False) ⟶ ((x12 x64 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 x79 x80 x81 x82 x83 x84 x85 x86 . x23 x86 ⟶ x20 x86 x77 x78 ⟶ x10 x86 (x74 (x21 x77 x78)) ⟶ x23 x79 ⟶ x20 x79 x77 x78 ⟶ x10 x79 (x74 (x21 x77 x78)) ⟶ x23 x85 ⟶ x10 x85 (x74 (x21 (x21 x77 x77) x77)) ⟶ x63 x78 x77 x86 x79 x85 = x63 x83 x80 x82 x81 x84 ⟶ (x85 = x84 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 x79 x80 x81 x82 x83 x84 x85 x86 . x23 x86 ⟶ x20 x86 x77 x78 ⟶ x10 x86 (x74 (x21 x77 x78)) ⟶ x23 x79 ⟶ x20 x79 x77 x78 ⟶ x10 x79 (x74 (x21 x77 x78)) ⟶ x23 x85 ⟶ x10 x85 (x74 (x21 (x21 x77 x77) x77)) ⟶ x63 x78 x77 x86 x79 x85 = x63 x83 x80 x82 x84 x81 ⟶ (x79 = x84 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 x79 x80 x81 x82 x83 x84 x85 x86 . x23 x86 ⟶ x20 x86 x77 x78 ⟶ x10 x86 (x74 (x21 x77 x78)) ⟶ x23 x79 ⟶ x20 x79 x77 x78 ⟶ x10 x79 (x74 (x21 x77 x78)) ⟶ x23 x85 ⟶ x10 x85 (x74 (x21 (x21 x77 x77) x77)) ⟶ x63 x78 x77 x86 x79 x85 = x63 x83 x80 x84 x82 x81 ⟶ (x86 = x84 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 x79 x80 x81 x82 x83 x84 x85 x86 . x23 x86 ⟶ x20 x86 x77 x78 ⟶ x10 x86 (x74 (x21 x77 x78)) ⟶ x23 x79 ⟶ x20 x79 x77 x78 ⟶ x10 x79 (x74 (x21 x77 x78)) ⟶ x23 x85 ⟶ x10 x85 (x74 (x21 (x21 x77 x77) x77)) ⟶ x63 x78 x77 x86 x79 x85 = x63 x83 x84 x82 x81 x80 ⟶ (x77 = x84 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 x79 x80 x81 x82 x83 x84 x85 x86 . x23 x86 ⟶ x20 x86 x77 x78 ⟶ x10 x86 (x74 (x21 x77 x78)) ⟶ x23 x79 ⟶ x20 x79 x77 x78 ⟶ x10 x79 (x74 (x21 x77 x78)) ⟶ x23 x85 ⟶ x10 x85 (x74 (x21 (x21 x77 x77) x77)) ⟶ x63 x78 x77 x86 x79 x85 = x63 x84 x80 x83 x82 x81 ⟶ (x78 = x84 ⟶ False) ⟶ False) ⟶ (∀ x77 . (x38 x77 ⟶ False) ⟶ x25 x77 ⟶ x39 (x11 x77) ⟶ False) ⟶ (∀ x77 . x38 x77 ⟶ x25 x77 ⟶ (x39 (x11 x77) ⟶ False) ⟶ False) ⟶ (∀ x77 . x31 x77 ⟶ x25 x77 ⟶ (x32 (x11 x77) ⟶ False) ⟶ False) ⟶ (∀ x77 . (x31 x77 ⟶ False) ⟶ x25 x77 ⟶ x32 (x11 x77) ⟶ False) ⟶ (∀ x77 . (x1 x77 ⟶ False) ⟶ x25 x77 ⟶ x76 (x11 x77) ⟶ False) ⟶ (∀ x77 . (x29 x77 ⟶ False) ⟶ x68 x77 ⟶ x32 (x7 x77) ⟶ False) ⟶ (∀ x77 . x29 x77 ⟶ x68 x77 ⟶ (x32 (x7 x77) ⟶ False) ⟶ False) ⟶ ((x76 x75 ⟶ False) ⟶ False) ⟶ (∀ x77 . x1 x77 ⟶ x25 x77 ⟶ (x76 (x11 x77) ⟶ False) ⟶ False) ⟶ (∀ x77 . (x1 x77 ⟶ False) ⟶ (x15 x77 ⟶ False) ⟶ x2 x77 ⟶ x14 x77 ⟶ x3 x77 ⟶ x13 x77 ⟶ x4 x77 ⟶ x12 x77 ⟶ (x4 (x16 x77) ⟶ False) ⟶ False) ⟶ (∀ x77 . (x1 x77 ⟶ False) ⟶ (x15 x77 ⟶ False) ⟶ x2 x77 ⟶ x14 x77 ⟶ x3 x77 ⟶ x13 x77 ⟶ x4 x77 ⟶ x12 x77 ⟶ (x13 (x16 x77) ⟶ False) ⟶ False) ⟶ (∀ x77 . (x1 x77 ⟶ False) ⟶ (x15 x77 ⟶ False) ⟶ x2 x77 ⟶ x14 x77 ⟶ x3 x77 ⟶ x13 x77 ⟶ x4 x77 ⟶ x12 x77 ⟶ (x3 (x16 x77) ⟶ False) ⟶ False) ⟶ (∀ x77 . (x1 x77 ⟶ False) ⟶ (x15 x77 ⟶ False) ⟶ x2 x77 ⟶ x14 x77 ⟶ x3 x77 ⟶ x13 x77 ⟶ x4 x77 ⟶ x12 x77 ⟶ (x14 (x16 x77) ⟶ False) ⟶ False) ⟶ (∀ x77 . (x1 x77 ⟶ False) ⟶ (x15 x77 ⟶ False) ⟶ x2 x77 ⟶ x14 x77 ⟶ x3 x77 ⟶ x13 x77 ⟶ x4 x77 ⟶ x12 x77 ⟶ (x2 (x16 x77) ⟶ False) ⟶ False) ⟶ (∀ x77 . (x1 x77 ⟶ False) ⟶ (x15 x77 ⟶ False) ⟶ x2 x77 ⟶ x14 x77 ⟶ x3 x77 ⟶ x13 x77 ⟶ x4 x77 ⟶ x12 x77 ⟶ (x70 (x16 x77) ⟶ False) ⟶ False) ⟶ (∀ x77 . (x1 x77 ⟶ False) ⟶ (x15 x77 ⟶ False) ⟶ x2 x77 ⟶ x14 x77 ⟶ x3 x77 ⟶ x13 x77 ⟶ x4 x77 ⟶ x12 x77 ⟶ x15 (x16 x77) ⟶ False) ⟶ (∀ x77 . (x1 x77 ⟶ False) ⟶ (x15 x77 ⟶ False) ⟶ x2 x77 ⟶ x14 x77 ⟶ x3 x77 ⟶ x13 x77 ⟶ x4 x77 ⟶ x12 x77 ⟶ x1 (x16 x77) ⟶ False) ⟶ (∀ x77 . (x15 x77 ⟶ False) ⟶ x68 x77 ⟶ x76 (x7 x77) ⟶ False) ⟶ (∀ x77 . x15 x77 ⟶ x68 x77 ⟶ (x76 (x7 x77) ⟶ False) ⟶ False) ⟶ (∀ x77 x78 . (x1 x78 ⟶ False) ⟶ (x15 x78 ⟶ False) ⟶ x2 x78 ⟶ x14 x78 ⟶ x3 x78 ⟶ x13 x78 ⟶ x4 x78 ⟶ x12 x78 ⟶ (x1 x77 ⟶ False) ⟶ (x15 x77 ⟶ False) ⟶ x2 x77 ⟶ x14 x77 ⟶ x3 x77 ⟶ x13 x77 ⟶ x4 x77 ⟶ x12 x77 ⟶ (x5 (x62 x77 x78) x78 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 . (x10 (x40 x77) x77 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 x79 . (x1 x79 ⟶ False) ⟶ (x15 x79 ⟶ False) ⟶ x12 x79 ⟶ x10 x77 (x11 x79) ⟶ x10 x78 (x11 x79) ⟶ (x61 (x60 x78 x77 x79) x79 x77 x78 ⟶ False) ⟶ False) ⟶ ((x68 x41 ⟶ False) ⟶ False) ⟶ ((x25 x59 ⟶ False) ⟶ False) ⟶ ((x42 x43 ⟶ False) ⟶ False) ⟶ ((x12 x58 ⟶ False) ⟶ False) ⟶ (∀ x77 . x42 x77 ⟶ (x10 (x44 x77) (x74 (x21 (x7 x77) (x11 x77))) ⟶ False) ⟶ False) ⟶ (∀ x77 . x42 x77 ⟶ (x20 (x44 x77) (x7 x77) (x11 x77) ⟶ False) ⟶ False) ⟶ (∀ x77 . x42 x77 ⟶ (x23 (x44 x77) ⟶ False) ⟶ False) ⟶ (∀ x77 . x42 x77 ⟶ (x10 (x57 x77) (x74 (x21 (x7 x77) (x11 x77))) ⟶ False) ⟶ False) ⟶ (∀ x77 . x42 x77 ⟶ (x20 (x57 x77) (x7 x77) (x11 x77) ⟶ False) ⟶ False) ⟶ (∀ x77 . x42 x77 ⟶ (x23 (x57 x77) ⟶ False) ⟶ False) ⟶ (∀ x77 . x12 x77 ⟶ (x10 (x45 x77) (x74 (x21 (x21 (x7 x77) (x7 x77)) (x7 x77))) ⟶ False) ⟶ False) ⟶ (∀ x77 . x12 x77 ⟶ (x23 (x45 x77) ⟶ False) ⟶ False) ⟶ ((x76 x46 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 x79 . (x1 x79 ⟶ False) ⟶ (x15 x79 ⟶ False) ⟶ x2 x79 ⟶ x14 x79 ⟶ x3 x79 ⟶ x13 x79 ⟶ x4 x79 ⟶ x12 x79 ⟶ (x1 x78 ⟶ False) ⟶ (x15 x78 ⟶ False) ⟶ x2 x78 ⟶ x14 x78 ⟶ x3 x78 ⟶ x13 x78 ⟶ x4 x78 ⟶ x12 x78 ⟶ x5 x77 x79 x78 ⟶ (x10 x77 (x74 (x21 (x7 x79) (x7 x78))) ⟶ False) ⟶ False) ⟶ (∀ x77 x78 x79 . (x1 x79 ⟶ False) ⟶ (x15 x79 ⟶ False) ⟶ x2 x79 ⟶ x14 x79 ⟶ x3 x79 ⟶ x13 x79 ⟶ x4 x79 ⟶ x12 x79 ⟶ (x1 x78 ⟶ False) ⟶ (x15 x78 ⟶ False) ⟶ x2 x78 ⟶ x14 x78 ⟶ x3 x78 ⟶ x13 x78 ⟶ x4 x78 ⟶ x12 x78 ⟶ x5 x77 x79 x78 ⟶ (x20 x77 (x7 x79) (x7 x78) ⟶ False) ⟶ False) ⟶ (∀ x77 x78 x79 . (x1 x79 ⟶ False) ⟶ (x15 x79 ⟶ False) ⟶ x2 x79 ⟶ x14 x79 ⟶ x3 x79 ⟶ x13 x79 ⟶ x4 x79 ⟶ x12 x79 ⟶ (x1 x78 ⟶ False) ⟶ (x15 x78 ⟶ False) ⟶ x2 x78 ⟶ x14 x78 ⟶ x3 x78 ⟶ x13 x78 ⟶ x4 x78 ⟶ x12 x78 ⟶ x5 x77 x79 x78 ⟶ (x23 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 x79 x80 . (x1 x80 ⟶ False) ⟶ (x15 x80 ⟶ False) ⟶ x12 x80 ⟶ x10 x77 (x11 x80) ⟶ x10 x79 (x11 x80) ⟶ x61 x78 x80 x77 x79 ⟶ (x10 x78 (x7 x80) ⟶ False) ⟶ False) ⟶ (∀ x77 . x68 x77 ⟶ (x25 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 . x42 x77 ⟶ (x68 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 . x12 x77 ⟶ (x42 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 x79 . (x1 x79 ⟶ False) ⟶ (x15 x79 ⟶ False) ⟶ x2 x79 ⟶ x14 x79 ⟶ x3 x79 ⟶ x13 x79 ⟶ x4 x79 ⟶ x12 x79 ⟶ (x1 x78 ⟶ False) ⟶ (x15 x78 ⟶ False) ⟶ x2 x78 ⟶ x14 x78 ⟶ x3 x78 ⟶ x13 x78 ⟶ x4 x78 ⟶ x12 x78 ⟶ x23 x77 ⟶ x20 x77 (x7 x79) (x7 x78) ⟶ x10 x77 (x74 (x21 (x7 x79) (x7 x78))) ⟶ (x10 (x6 x79 x78 x77) (x74 (x21 (x11 x79) (x11 x78))) ⟶ False) ⟶ False) ⟶ (∀ x77 x78 x79 . (x1 x79 ⟶ False) ⟶ (x15 x79 ⟶ False) ⟶ x2 x79 ⟶ x14 x79 ⟶ x3 x79 ⟶ x13 x79 ⟶ x4 x79 ⟶ x12 x79 ⟶ (x1 x78 ⟶ False) ⟶ (x15 x78 ⟶ False) ⟶ x2 x78 ⟶ x14 x78 ⟶ x3 x78 ⟶ x13 x78 ⟶ x4 x78 ⟶ x12 x78 ⟶ x23 x77 ⟶ x20 x77 (x7 x79) (x7 x78) ⟶ x10 x77 (x74 (x21 (x7 x79) (x7 x78))) ⟶ (x20 (x6 x79 x78 x77) (x11 x79) (x11 x78) ⟶ False) ⟶ False) ⟶ (∀ x77 x78 x79 . (x1 x79 ⟶ False) ⟶ (x15 x79 ⟶ False) ⟶ x2 x79 ⟶ x14 x79 ⟶ x3 x79 ⟶ x13 x79 ⟶ x4 x79 ⟶ x12 x79 ⟶ (x1 x78 ⟶ False) ⟶ (x15 x78 ⟶ False) ⟶ x2 x78 ⟶ x14 x78 ⟶ x3 x78 ⟶ x13 x78 ⟶ x4 x78 ⟶ x12 x78 ⟶ x23 x77 ⟶ x20 x77 (x7 x79) (x7 x78) ⟶ x10 x77 (x74 (x21 (x7 x79) (x7 x78))) ⟶ (x23 (x6 x79 x78 x77) ⟶ False) ⟶ False) ⟶ (∀ x77 x78 . (x1 x78 ⟶ False) ⟶ (x15 x78 ⟶ False) ⟶ x2 x78 ⟶ x14 x78 ⟶ x3 x78 ⟶ x13 x78 ⟶ x4 x78 ⟶ x12 x78 ⟶ x10 x77 (x7 (x16 x78)) ⟶ (x10 (x18 x78 x77) (x7 x78) ⟶ False) ⟶ False) ⟶ (∀ x77 x78 . (x1 x78 ⟶ False) ⟶ (x15 x78 ⟶ False) ⟶ x2 x78 ⟶ x14 x78 ⟶ x3 x78 ⟶ x13 x78 ⟶ x4 x78 ⟶ x12 x78 ⟶ x10 x77 (x7 x78) ⟶ (x10 (x47 x78 x77) (x7 (x16 x78)) ⟶ False) ⟶ False) ⟶ (∀ x77 x78 . (x1 x78 ⟶ False) ⟶ (x15 x78 ⟶ False) ⟶ x2 x78 ⟶ x14 x78 ⟶ x3 x78 ⟶ x13 x78 ⟶ x4 x78 ⟶ x12 x78 ⟶ x10 x77 (x11 (x16 x78)) ⟶ (x10 (x17 x78 x77) (x11 x78) ⟶ False) ⟶ False) ⟶ (∀ x77 x78 . (x1 x78 ⟶ False) ⟶ (x15 x78 ⟶ False) ⟶ x13 x78 ⟶ x4 x78 ⟶ x12 x78 ⟶ x10 x77 (x11 x78) ⟶ (x61 (x8 x78 x77) x78 x77 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 . (x1 x78 ⟶ False) ⟶ (x15 x78 ⟶ False) ⟶ x2 x78 ⟶ x14 x78 ⟶ x3 x78 ⟶ x13 x78 ⟶ x4 x78 ⟶ x12 x78 ⟶ x10 x77 (x11 x78) ⟶ (x10 (x56 x78 x77) (x11 (x16 x78)) ⟶ False) ⟶ False) ⟶ (∀ x77 x78 x79 x80 . (x76 x80 ⟶ False) ⟶ x23 x77 ⟶ x20 x77 x80 x79 ⟶ x10 x77 (x74 (x21 x80 x79)) ⟶ x10 x78 x80 ⟶ (x10 (x9 x80 x79 x77 x78) x79 ⟶ False) ⟶ False) ⟶ (∀ x77 . (x1 x77 ⟶ False) ⟶ (x15 x77 ⟶ False) ⟶ x2 x77 ⟶ x14 x77 ⟶ x3 x77 ⟶ x13 x77 ⟶ x4 x77 ⟶ x12 x77 ⟶ (x12 (x16 x77) ⟶ False) ⟶ False) ⟶ (∀ x77 . (x1 x77 ⟶ False) ⟶ (x15 x77 ⟶ False) ⟶ x2 x77 ⟶ x14 x77 ⟶ x3 x77 ⟶ x13 x77 ⟶ x4 x77 ⟶ x12 x77 ⟶ (x70 (x16 x77) ⟶ False) ⟶ False) ⟶ (∀ x77 . (x1 x77 ⟶ False) ⟶ (x15 x77 ⟶ False) ⟶ x2 x77 ⟶ x14 x77 ⟶ x3 x77 ⟶ x13 x77 ⟶ x4 x77 ⟶ x12 x77 ⟶ x15 (x16 x77) ⟶ False) ⟶ (∀ x77 . (x1 x77 ⟶ False) ⟶ (x15 x77 ⟶ False) ⟶ x2 x77 ⟶ x14 x77 ⟶ x3 x77 ⟶ x13 x77 ⟶ x4 x77 ⟶ x12 x77 ⟶ x1 (x16 x77) ⟶ False) ⟶ (∀ x77 . x37 x77 ⟶ x23 x77 ⟶ (x23 (x71 x77) ⟶ False) ⟶ False) ⟶ (∀ x77 . x37 x77 ⟶ x23 x77 ⟶ (x37 (x71 x77) ⟶ False) ⟶ False) ⟶ (∀ x77 x78 x79 x80 . (x76 x80 ⟶ False) ⟶ (x76 x77 ⟶ False) ⟶ (x76 x79 ⟶ False) ⟶ x23 x78 ⟶ x10 x78 (x74 (x21 (x21 x80 x77) x79)) ⟶ (x10 (x72 x80 x77 x79 x78) (x74 (x21 (x21 x77 x80) x79)) ⟶ False) ⟶ False) ⟶ (∀ x77 x78 x79 x80 . (x76 x80 ⟶ False) ⟶ (x76 x77 ⟶ False) ⟶ (x76 x79 ⟶ False) ⟶ x23 x78 ⟶ x10 x78 (x74 (x21 (x21 x80 x77) x79)) ⟶ (x23 (x72 x80 x77 x79 x78) ⟶ False) ⟶ False) ⟶ (∀ x77 x78 x79 . (x1 x79 ⟶ False) ⟶ (x15 x79 ⟶ False) ⟶ x2 x79 ⟶ x14 x79 ⟶ x3 x79 ⟶ x13 x79 ⟶ x4 x79 ⟶ x12 x79 ⟶ (x1 x78 ⟶ False) ⟶ (x15 x78 ⟶ False) ⟶ x2 x78 ⟶ x14 x78 ⟶ x3 x78 ⟶ x13 x78 ⟶ x4 x78 ⟶ x12 x78 ⟶ x23 x77 ⟶ x20 x77 (x7 x79) (x7 x78) ⟶ x10 x77 (x74 (x21 (x7 x79) (x7 x78))) ⟶ (x10 (x55 x79 x78 x77) (x74 (x21 (x7 (x16 x79)) (x7 x78))) ⟶ False) ⟶ False) ⟶ (∀ x77 x78 x79 . (x1 x79 ⟶ False) ⟶ (x15 x79 ⟶ False) ⟶ x2 x79 ⟶ x14 x79 ⟶ x3 x79 ⟶ x13 x79 ⟶ x4 x79 ⟶ x12 x79 ⟶ (x1 x78 ⟶ False) ⟶ (x15 x78 ⟶ False) ⟶ x2 x78 ⟶ x14 x78 ⟶ x3 x78 ⟶ x13 x78 ⟶ x4 x78 ⟶ x12 x78 ⟶ x23 x77 ⟶ x20 x77 (x7 x79) (x7 x78) ⟶ x10 x77 (x74 (x21 (x7 x79) (x7 x78))) ⟶ (x20 (x55 x79 x78 x77) (x7 (x16 x79)) (x7 x78) ⟶ False) ⟶ False) ⟶ (∀ x77 x78 x79 . (x1 x79 ⟶ False) ⟶ (x15 x79 ⟶ False) ⟶ x2 x79 ⟶ x14 x79 ⟶ x3 x79 ⟶ x13 x79 ⟶ x4 x79 ⟶ x12 x79 ⟶ (x1 x78 ⟶ False) ⟶ (x15 x78 ⟶ False) ⟶ x2 x78 ⟶ x14 x78 ⟶ x3 x78 ⟶ x13 x78 ⟶ x4 x78 ⟶ x12 x78 ⟶ x23 x77 ⟶ x20 x77 (x7 x79) (x7 x78) ⟶ x10 x77 (x74 (x21 (x7 x79) (x7 x78))) ⟶ (x23 (x55 x79 x78 x77) ⟶ False) ⟶ False) ⟶ (∀ x77 x78 x79 x80 x81 . x23 x81 ⟶ x20 x81 x77 x78 ⟶ x10 x81 (x74 (x21 x77 x78)) ⟶ x23 x79 ⟶ x20 x79 x77 x78 ⟶ x10 x79 (x74 (x21 x77 x78)) ⟶ x23 x80 ⟶ x10 x80 (x74 (x21 (x21 x77 x77) x77)) ⟶ (x12 (x63 x78 x77 x81 x79 x80) ⟶ False) ⟶ False) ⟶ (∀ x77 x78 x79 x80 x81 . x23 x81 ⟶ x20 x81 x77 x78 ⟶ x10 x81 (x74 (x21 x77 x78)) ⟶ x23 x79 ⟶ x20 x79 x77 x78 ⟶ x10 x79 (x74 (x21 x77 x78)) ⟶ x23 x80 ⟶ x10 x80 (x74 (x21 (x21 x77 x77) x77)) ⟶ (x70 (x63 x78 x77 x81 x79 x80) ⟶ False) ⟶ False) ⟶ (∀ x77 x78 . (x1 x78 ⟶ False) ⟶ (x15 x78 ⟶ False) ⟶ x2 x78 ⟶ x14 x78 ⟶ x3 x78 ⟶ x13 x78 ⟶ x4 x78 ⟶ x12 x78 ⟶ x10 x77 (x7 (x16 x78)) ⟶ (x18 x78 x77 = x47 (x16 x78) x77 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 . (x1 x78 ⟶ False) ⟶ (x15 x78 ⟶ False) ⟶ x2 x78 ⟶ x14 x78 ⟶ x3 x78 ⟶ x13 x78 ⟶ x4 x78 ⟶ x12 x78 ⟶ x10 x77 (x7 x78) ⟶ (x47 x78 x77 = x77 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 . (x1 x78 ⟶ False) ⟶ (x15 x78 ⟶ False) ⟶ x2 x78 ⟶ x14 x78 ⟶ x3 x78 ⟶ x13 x78 ⟶ x4 x78 ⟶ x12 x78 ⟶ x10 x77 (x11 (x16 x78)) ⟶ (x17 x78 x77 = x56 (x16 x78) x77 ⟶ False) ⟶ False) ⟶ ((x75 = x46 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 . (x1 x78 ⟶ False) ⟶ (x15 x78 ⟶ False) ⟶ x2 x78 ⟶ x14 x78 ⟶ x3 x78 ⟶ x13 x78 ⟶ x4 x78 ⟶ x12 x78 ⟶ x10 x77 (x11 x78) ⟶ (x56 x78 x77 = x77 ⟶ False) ⟶ False) ⟶ (∀ x77 . (x1 x77 ⟶ False) ⟶ (x15 x77 ⟶ False) ⟶ x2 x77 ⟶ x14 x77 ⟶ x3 x77 ⟶ x13 x77 ⟶ x4 x77 ⟶ x12 x77 ⟶ (x16 x77 = x63 (x11 x77) (x7 x77) (x44 x77) (x57 x77) (x72 (x7 x77) (x7 x77) (x7 x77) (x45 x77)) ⟶ False) ⟶ False) ⟶ (∀ x77 x78 x79 x80 . (x1 x80 ⟶ False) ⟶ (x15 x80 ⟶ False) ⟶ x2 x80 ⟶ x14 x80 ⟶ x3 x80 ⟶ x13 x80 ⟶ x4 x80 ⟶ x12 x80 ⟶ (x1 x79 ⟶ False) ⟶ (x15 x79 ⟶ False) ⟶ x2 x79 ⟶ x14 x79 ⟶ x3 x79 ⟶ x13 x79 ⟶ x4 x79 ⟶ x12 x79 ⟶ x23 x78 ⟶ x20 x78 (x7 x80) (x7 x79) ⟶ x10 x78 (x74 (x21 (x7 x80) (x7 x79))) ⟶ x23 x77 ⟶ x20 x77 (x7 (x16 x80)) (x7 x79) ⟶ x10 x77 (x74 (x21 (x7 (x16 x80)) (x7 x79))) ⟶ x9 (x7 (x16 x80)) (x7 x79) x77 (x48 x77 x78 x79 x80) = x9 (x7 x80) (x7 x79) x78 (x18 x80 (x48 x77 x78 x79 x80)) ⟶ (x77 = x55 x80 x79 x78 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 x79 x80 . (x1 x80 ⟶ False) ⟶ (x15 x80 ⟶ False) ⟶ x2 x80 ⟶ x14 x80 ⟶ x3 x80 ⟶ x13 x80 ⟶ x4 x80 ⟶ x12 x80 ⟶ (x1 x79 ⟶ False) ⟶ (x15 x79 ⟶ False) ⟶ x2 x79 ⟶ x14 x79 ⟶ x3 x79 ⟶ x13 x79 ⟶ x4 x79 ⟶ x12 x79 ⟶ x23 x78 ⟶ x20 x78 (x7 x80) (x7 x79) ⟶ x10 x78 (x74 (x21 (x7 x80) (x7 x79))) ⟶ x23 x77 ⟶ x20 x77 (x7 (x16 x80)) (x7 x79) ⟶ x10 x77 (x74 (x21 (x7 (x16 x80)) (x7 x79))) ⟶ (x10 (x48 x77 x78 x79 x80) (x7 (x16 x80)) ⟶ False) ⟶ (x77 = x55 x80 x79 x78 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 x79 x80 x81 . (x1 x81 ⟶ False) ⟶ (x15 x81 ⟶ False) ⟶ x2 x81 ⟶ x14 x81 ⟶ x3 x81 ⟶ x13 x81 ⟶ x4 x81 ⟶ x12 x81 ⟶ (x1 x80 ⟶ False) ⟶ (x15 x80 ⟶ False) ⟶ x2 x80 ⟶ x14 x80 ⟶ x3 x80 ⟶ x13 x80 ⟶ x4 x80 ⟶ x12 x80 ⟶ x23 x79 ⟶ x20 x79 (x7 x81) (x7 x80) ⟶ x10 x79 (x74 (x21 (x7 x81) (x7 x80))) ⟶ x23 x77 ⟶ x20 x77 (x7 (x16 x81)) (x7 x80) ⟶ x10 x77 (x74 (x21 (x7 (x16 x81)) (x7 x80))) ⟶ x77 = x55 x81 x80 x79 ⟶ x10 x78 (x7 (x16 x81)) ⟶ (x9 (x7 (x16 x81)) (x7 x80) x77 x78 = x9 (x7 x81) (x7 x80) x79 (x18 x81 x78) ⟶ False) ⟶ False) ⟶ (∀ x77 . x25 x77 ⟶ x54 x77 x75 ⟶ (x1 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 . x25 x77 ⟶ x1 x77 ⟶ (x54 x77 x75 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 x79 . (x76 x79 ⟶ False) ⟶ (x76 x77 ⟶ False) ⟶ x10 x78 (x74 (x21 x79 x77)) ⟶ x23 x78 ⟶ x20 x78 x79 x77 ⟶ (x20 x78 x79 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 x79 . (x76 x79 ⟶ False) ⟶ (x76 x77 ⟶ False) ⟶ x10 x78 (x74 (x21 x79 x77)) ⟶ x23 x78 ⟶ x20 x78 x79 x77 ⟶ x76 x78 ⟶ False) ⟶ (∀ x77 x78 x79 . (x76 x79 ⟶ False) ⟶ (x76 x77 ⟶ False) ⟶ x10 x78 (x74 (x21 x79 x77)) ⟶ x23 x78 ⟶ x20 x78 x79 x77 ⟶ (x23 x78 ⟶ False) ⟶ False) ⟶ (∀ x77 . x25 x77 ⟶ (x38 x77 ⟶ False) ⟶ x31 x77 ⟶ False) ⟶ (∀ x77 . x25 x77 ⟶ x31 x77 ⟶ (x38 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 . x25 x77 ⟶ (x38 x77 ⟶ False) ⟶ x38 x77 ⟶ False) ⟶ (∀ x77 . x25 x77 ⟶ (x38 x77 ⟶ False) ⟶ x1 x77 ⟶ False) ⟶ (∀ x77 . x25 x77 ⟶ x1 x77 ⟶ (x38 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 . x25 x77 ⟶ x1 x77 ⟶ (x1 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 x79 . x76 x79 ⟶ x10 x77 (x74 (x21 x78 x79)) ⟶ (x76 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 . x10 x78 (x74 (x21 x77 x77)) ⟶ x20 x78 x77 x77 ⟶ (x53 x78 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 x79 . x76 x79 ⟶ x10 x77 (x74 (x21 x79 x78)) ⟶ (x76 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 x79 . (x76 x79 ⟶ False) ⟶ x10 x77 (x74 (x21 x78 x79)) ⟶ x20 x77 x78 x79 ⟶ (x53 x77 x78 ⟶ False) ⟶ False) ⟶ (∀ x77 . x25 x77 ⟶ (x31 x77 ⟶ False) ⟶ x1 x77 ⟶ False) ⟶ (∀ x77 x78 x79 . x10 x79 (x74 (x21 x77 x78)) ⟶ (x35 x79 x78 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 x79 . x10 x79 (x74 (x21 x78 x77)) ⟶ (x66 x79 x78 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 x79 . x76 x79 ⟶ x10 x77 (x74 (x21 x79 x78)) ⟶ x20 x77 x79 x78 ⟶ (x53 x77 x79 ⟶ False) ⟶ False) ⟶ (∀ x77 . x12 x77 ⟶ (x1 x77 ⟶ False) ⟶ (x15 x77 ⟶ False) ⟶ x29 x77 ⟶ (x4 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 . x12 x77 ⟶ (x1 x77 ⟶ False) ⟶ (x15 x77 ⟶ False) ⟶ x29 x77 ⟶ (x3 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 . x12 x77 ⟶ (x1 x77 ⟶ False) ⟶ (x15 x77 ⟶ False) ⟶ x29 x77 ⟶ x15 x77 ⟶ False) ⟶ (∀ x77 . x12 x77 ⟶ (x1 x77 ⟶ False) ⟶ (x15 x77 ⟶ False) ⟶ x29 x77 ⟶ x1 x77 ⟶ False) ⟶ (∀ x77 . x25 x77 ⟶ x1 x77 ⟶ (x31 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 x79 . x10 x79 (x74 (x21 x77 x78)) ⟶ (x37 x79 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 x79 . x10 x78 (x74 (x21 x79 x77)) ⟶ x53 x78 x79 ⟶ (x20 x78 x79 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 . x12 x77 ⟶ (x1 x77 ⟶ False) ⟶ x31 x77 ⟶ (x15 x77 ⟶ False) ⟶ (x13 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 . x12 x77 ⟶ (x1 x77 ⟶ False) ⟶ x31 x77 ⟶ (x15 x77 ⟶ False) ⟶ (x14 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 . x12 x77 ⟶ (x1 x77 ⟶ False) ⟶ x31 x77 ⟶ (x15 x77 ⟶ False) ⟶ x15 x77 ⟶ False) ⟶ (∀ x77 . x12 x77 ⟶ (x1 x77 ⟶ False) ⟶ x31 x77 ⟶ (x15 x77 ⟶ False) ⟶ x1 x77 ⟶ False) ⟶ (∀ x77 . x25 x77 ⟶ (x31 x77 ⟶ False) ⟶ x1 x77 ⟶ False) ⟶ (∀ x77 . x68 x77 ⟶ x15 x77 ⟶ (x29 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 . x68 x77 ⟶ (x15 x77 ⟶ False) ⟶ x27 x77 ⟶ x1 x77 ⟶ False) ⟶ (∀ x77 . x68 x77 ⟶ x1 x77 ⟶ x27 x77 ⟶ (x15 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 . x68 x77 ⟶ x15 x77 ⟶ (x27 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 . x68 x77 ⟶ (x1 x77 ⟶ False) ⟶ (x27 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 . x25 x77 ⟶ x54 x77 x19 ⟶ (x31 x77 ⟶ False) ⟶ False) ⟶ (∀ x77 . x25 x77 ⟶ x54 x77 x19 ⟶ x1 x77 ⟶ False) ⟶ (∀ x77 . x25 x77 ⟶ (x1 x77 ⟶ False) ⟶ x31 x77 ⟶ (x54 x77 x19 ⟶ False) ⟶ False) ⟶ (∀ x77 x78 . x0 x77 x78 ⟶ x0 x78 x77 ⟶ False) ⟶ (∀ x77 . x12 x77 ⟶ x70 x77 ⟶ (x77 = x63 (x11 x77) (x7 x77) (x57 x77) (x44 x77) (x45 x77) ⟶ False) ⟶ False) ⟶ (x9 (x7 (x16 x49)) (x7 x52) (x55 x49 x52 x51) (x8 (x16 x49) x50) = x8 x52 (x9 (x11 x49) (x11 x52) (x6 x49 x52 x51) (x17 x49 x50)) ⟶ False) ⟶ ((x10 x50 (x11 (x16 x49)) ⟶ False) ⟶ False) ⟶ ((x5 x51 x49 x52 ⟶ False) ⟶ False) ⟶ ((x12 x52 ⟶ False) ⟶ False) ⟶ ((x4 x52 ⟶ False) ⟶ False) ⟶ ((x13 x52 ⟶ False) ⟶ False) ⟶ ((x3 x52 ⟶ False) ⟶ False) ⟶ ((x14 x52 ⟶ False) ⟶ False) ⟶ ((x2 x52 ⟶ False) ⟶ False) ⟶ (x15 x52 ⟶ False) ⟶ (x1 x52 ⟶ False) ⟶ ((x12 x49 ⟶ False) ⟶ False) ⟶ ((x4 x49 ⟶ False) ⟶ False) ⟶ ((x13 x49 ⟶ False) ⟶ False) ⟶ ((x3 x49 ⟶ False) ⟶ False) ⟶ ((x14 x49 ⟶ False) ⟶ False) ⟶ ((x2 x49 ⟶ False) ⟶ False) ⟶ (x15 x49 ⟶ False) ⟶ (x1 x49 ⟶ False) ⟶ False (proof)