Search for blocks/addresses/...

Proofgold Asset

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