Search for blocks/addresses/...

Proofgold Asset

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