Search for blocks/addresses/...

Proofgold Asset

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