Search for blocks/addresses/...

Proofgold Asset

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