Search for blocks/addresses/...

Proofgold Asset

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