Search for blocks/addresses/...

Proofgold Asset

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