Search for blocks/addresses/...

Proofgold Asset

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