Search for blocks/addresses/...

Proofgold Asset

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