Definition False^False := ∀ x0 : ο . x0
Definition not^not := λ x0 : ο . x0 ⟶ False
Theorem 6ae76.. : ∀ 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 . x60 x62 ⟶ (x62 = x61 ⟶ False) ⟶ x60 x61 ⟶ False) ⟶ (∀ x61 x62 . (x0 x62 ⟶ False) ⟶ x16 x62 ⟶ x1 x62 ⟶ x15 x61 ⟶ x3 x61 (x2 x62) (x2 x62) ⟶ x14 x61 (x2 x62) (x2 x62) ⟶ x4 x61 (x6 (x5 (x2 x62) (x2 x62))) ⟶ (x8 x62 (x7 (x2 x62) (x2 x62) x61 (x9 x61 x62)) (x7 (x2 x62) (x2 x62) x61 (x12 x61 x62)) (x7 (x2 x62) (x2 x62) x61 (x11 x61 x62)) (x7 (x2 x62) (x2 x62) x61 (x10 x61 x62)) ⟶ False) ⟶ (x8 x62 (x9 x61 x62) (x12 x61 x62) (x11 x61 x62) (x10 x61 x62) ⟶ False) ⟶ (x13 x61 x62 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . (x0 x62 ⟶ False) ⟶ x16 x62 ⟶ x1 x62 ⟶ x15 x61 ⟶ x3 x61 (x2 x62) (x2 x62) ⟶ x14 x61 (x2 x62) (x2 x62) ⟶ x4 x61 (x6 (x5 (x2 x62) (x2 x62))) ⟶ x8 x62 (x9 x61 x62) (x12 x61 x62) (x11 x61 x62) (x10 x61 x62) ⟶ x8 x62 (x7 (x2 x62) (x2 x62) x61 (x9 x61 x62)) (x7 (x2 x62) (x2 x62) x61 (x12 x61 x62)) (x7 (x2 x62) (x2 x62) x61 (x11 x61 x62)) (x7 (x2 x62) (x2 x62) x61 (x10 x61 x62)) ⟶ (x13 x61 x62 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . (x0 x62 ⟶ False) ⟶ x16 x62 ⟶ x1 x62 ⟶ x15 x61 ⟶ x3 x61 (x2 x62) (x2 x62) ⟶ x14 x61 (x2 x62) (x2 x62) ⟶ x4 x61 (x6 (x5 (x2 x62) (x2 x62))) ⟶ (x4 (x10 x61 x62) (x2 x62) ⟶ False) ⟶ (x13 x61 x62 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . (x0 x62 ⟶ False) ⟶ x16 x62 ⟶ x1 x62 ⟶ x15 x61 ⟶ x3 x61 (x2 x62) (x2 x62) ⟶ x14 x61 (x2 x62) (x2 x62) ⟶ x4 x61 (x6 (x5 (x2 x62) (x2 x62))) ⟶ (x4 (x11 x61 x62) (x2 x62) ⟶ False) ⟶ (x13 x61 x62 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . (x0 x62 ⟶ False) ⟶ x16 x62 ⟶ x1 x62 ⟶ x15 x61 ⟶ x3 x61 (x2 x62) (x2 x62) ⟶ x14 x61 (x2 x62) (x2 x62) ⟶ x4 x61 (x6 (x5 (x2 x62) (x2 x62))) ⟶ (x4 (x12 x61 x62) (x2 x62) ⟶ False) ⟶ (x13 x61 x62 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . (x0 x62 ⟶ False) ⟶ x16 x62 ⟶ x1 x62 ⟶ x15 x61 ⟶ x3 x61 (x2 x62) (x2 x62) ⟶ x14 x61 (x2 x62) (x2 x62) ⟶ x4 x61 (x6 (x5 (x2 x62) (x2 x62))) ⟶ (x4 (x9 x61 x62) (x2 x62) ⟶ False) ⟶ (x13 x61 x62 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 x63 x64 x65 x66 . (x0 x66 ⟶ False) ⟶ x16 x66 ⟶ x1 x66 ⟶ x15 x61 ⟶ x3 x61 (x2 x66) (x2 x66) ⟶ x14 x61 (x2 x66) (x2 x66) ⟶ x4 x61 (x6 (x5 (x2 x66) (x2 x66))) ⟶ x13 x61 x66 ⟶ x4 x65 (x2 x66) ⟶ x4 x62 (x2 x66) ⟶ x4 x64 (x2 x66) ⟶ x4 x63 (x2 x66) ⟶ x8 x66 (x7 (x2 x66) (x2 x66) x61 x65) (x7 (x2 x66) (x2 x66) x61 x62) (x7 (x2 x66) (x2 x66) x61 x64) (x7 (x2 x66) (x2 x66) x61 x63) ⟶ (x8 x66 x65 x62 x64 x63 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 x63 x64 x65 x66 . (x0 x66 ⟶ False) ⟶ x16 x66 ⟶ x1 x66 ⟶ x15 x61 ⟶ x3 x61 (x2 x66) (x2 x66) ⟶ x14 x61 (x2 x66) (x2 x66) ⟶ x4 x61 (x6 (x5 (x2 x66) (x2 x66))) ⟶ x13 x61 x66 ⟶ x4 x65 (x2 x66) ⟶ x4 x62 (x2 x66) ⟶ x4 x64 (x2 x66) ⟶ x4 x63 (x2 x66) ⟶ x8 x66 x65 x62 x64 x63 ⟶ (x8 x66 (x7 (x2 x66) (x2 x66) x61 x65) (x7 (x2 x66) (x2 x66) x61 x62) (x7 (x2 x66) (x2 x66) x61 x64) (x7 (x2 x66) (x2 x66) x61 x63) ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . x17 x61 x62 ⟶ x60 x62 ⟶ False) ⟶ (∀ x61 . x60 x61 ⟶ (x61 = x59 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 x63 . x17 x61 x62 ⟶ x4 x62 (x6 x63) ⟶ x60 x63 ⟶ False) ⟶ (∀ x61 x62 x63 . x17 x62 x63 ⟶ x4 x63 (x6 x61) ⟶ (x4 x62 x61 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . x18 x62 x61 ⟶ (x4 x62 (x6 x61) ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . x4 x62 (x6 x61) ⟶ (x18 x62 x61 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . x4 x61 x62 ⟶ (x60 x62 ⟶ False) ⟶ (x17 x61 x62 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . x17 x62 x61 ⟶ (x4 x62 x61 ⟶ False) ⟶ False) ⟶ (x60 x19 ⟶ False) ⟶ (∀ x61 . (x18 x61 x61 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 x63 x64 . (x60 x64 ⟶ False) ⟶ x15 x61 ⟶ x3 x61 x64 x63 ⟶ x4 x61 (x6 (x5 x64 x63)) ⟶ x4 x62 x64 ⟶ (x7 x64 x63 x61 x62 = x20 x61 x62 ⟶ False) ⟶ False) ⟶ ((x58 x57 ⟶ False) ⟶ False) ⟶ (x60 x57 ⟶ False) ⟶ (∀ x61 x62 . (x15 (x56 x61 x62) ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . (x21 (x56 x61 x62) x61 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . (x55 (x56 x62 x61) x61 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . (x22 (x56 x61 x62) ⟶ False) ⟶ False) ⟶ (x54 x53 ⟶ False) ⟶ ((x15 x53 ⟶ False) ⟶ False) ⟶ ((x22 x53 ⟶ False) ⟶ False) ⟶ (∀ x61 . (x23 x61 ⟶ False) ⟶ x25 x61 ⟶ x60 (x24 x61) ⟶ False) ⟶ (∀ x61 . (x23 x61 ⟶ False) ⟶ x25 x61 ⟶ (x4 (x24 x61) (x6 (x2 x61)) ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . (x60 x62 ⟶ False) ⟶ (x60 x61 ⟶ False) ⟶ x60 (x26 x61 x62) ⟶ False) ⟶ (∀ x61 x62 . (x60 x62 ⟶ False) ⟶ (x60 x61 ⟶ False) ⟶ (x15 (x26 x61 x62) ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . (x60 x62 ⟶ False) ⟶ (x60 x61 ⟶ False) ⟶ (x21 (x26 x61 x62) x61 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . (x60 x62 ⟶ False) ⟶ (x60 x61 ⟶ False) ⟶ (x55 (x26 x61 x62) x62 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . (x60 x62 ⟶ False) ⟶ (x60 x61 ⟶ False) ⟶ (x22 (x26 x61 x62) ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . (x60 x62 ⟶ False) ⟶ (x60 x61 ⟶ False) ⟶ (x4 (x26 x61 x62) (x6 (x5 x62 x61)) ⟶ False) ⟶ False) ⟶ (x60 x27 ⟶ False) ⟶ (∀ x61 . (x14 (x52 x61) x61 x61 ⟶ False) ⟶ False) ⟶ (∀ x61 . (x3 (x52 x61) x61 x61 ⟶ False) ⟶ False) ⟶ (∀ x61 . (x51 (x52 x61) x61 ⟶ False) ⟶ False) ⟶ (∀ x61 . (x15 (x52 x61) ⟶ False) ⟶ False) ⟶ (∀ x61 . (x21 (x52 x61) x61 ⟶ False) ⟶ False) ⟶ (∀ x61 . (x55 (x52 x61) x61 ⟶ False) ⟶ False) ⟶ (∀ x61 . (x22 (x52 x61) ⟶ False) ⟶ False) ⟶ (∀ x61 . (x4 (x52 x61) (x6 (x5 x61 x61)) ⟶ False) ⟶ False) ⟶ ((x50 x49 ⟶ False) ⟶ False) ⟶ ((x15 x49 ⟶ False) ⟶ False) ⟶ ((x22 x49 ⟶ False) ⟶ False) ⟶ (∀ x61 . (x0 x61 ⟶ False) ⟶ x25 x61 ⟶ x28 (x29 x61) ⟶ False) ⟶ (∀ x61 . (x0 x61 ⟶ False) ⟶ x25 x61 ⟶ (x4 (x29 x61) (x6 (x2 x61)) ⟶ False) ⟶ False) ⟶ (∀ x61 . (x23 x61 ⟶ False) ⟶ x25 x61 ⟶ (x28 (x30 x61) ⟶ False) ⟶ False) ⟶ (∀ x61 . (x23 x61 ⟶ False) ⟶ x25 x61 ⟶ x60 (x30 x61) ⟶ False) ⟶ (∀ x61 . (x23 x61 ⟶ False) ⟶ x25 x61 ⟶ (x4 (x30 x61) (x6 (x2 x61)) ⟶ False) ⟶ False) ⟶ ((x60 x48 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . (x21 (x31 x61 x62) x61 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . (x55 (x31 x62 x61) x61 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . (x22 (x31 x61 x62) ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . (x60 (x31 x61 x62) ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . (x4 (x31 x61 x62) (x6 (x5 x62 x61)) ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . (x15 (x47 x61 x62) ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . (x21 (x47 x61 x62) x61 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . (x55 (x47 x62 x61) x61 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . (x22 (x47 x61 x62) ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . (x4 (x47 x61 x62) (x6 (x5 x62 x61)) ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . (x3 (x32 x61 x62) x62 x61 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . (x15 (x32 x61 x62) ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . (x21 (x32 x61 x62) x61 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . (x55 (x32 x62 x61) x61 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . (x22 (x32 x61 x62) ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . (x4 (x32 x61 x62) (x6 (x5 x62 x61)) ⟶ False) ⟶ False) ⟶ ((x15 x33 ⟶ False) ⟶ False) ⟶ ((x22 x33 ⟶ False) ⟶ False) ⟶ (∀ x61 . (x34 x61 ⟶ False) ⟶ x25 x61 ⟶ x35 (x2 x61) ⟶ False) ⟶ (∀ x61 . x34 x61 ⟶ x25 x61 ⟶ (x35 (x2 x61) ⟶ False) ⟶ False) ⟶ (∀ x61 . x0 x61 ⟶ x25 x61 ⟶ (x28 (x2 x61) ⟶ False) ⟶ False) ⟶ (∀ x61 . (x0 x61 ⟶ False) ⟶ x25 x61 ⟶ x28 (x2 x61) ⟶ False) ⟶ (∀ x61 . (x23 x61 ⟶ False) ⟶ x25 x61 ⟶ x60 (x2 x61) ⟶ False) ⟶ ((x60 x59 ⟶ False) ⟶ False) ⟶ (∀ x61 . x23 x61 ⟶ x25 x61 ⟶ (x60 (x2 x61) ⟶ False) ⟶ False) ⟶ (∀ x61 x62 x63 . x58 x63 ⟶ x22 x61 ⟶ x21 x61 x63 ⟶ x15 x61 ⟶ (x15 (x20 x61 x62) ⟶ False) ⟶ False) ⟶ (∀ x61 x62 x63 . x58 x63 ⟶ x22 x61 ⟶ x21 x61 x63 ⟶ x15 x61 ⟶ (x22 (x20 x61 x62) ⟶ False) ⟶ False) ⟶ (∀ x61 . (x4 (x46 x61) x61 ⟶ False) ⟶ False) ⟶ ((x25 x36 ⟶ False) ⟶ False) ⟶ ((x1 x45 ⟶ False) ⟶ False) ⟶ (∀ x61 . x1 x61 ⟶ (x25 x61 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 x63 x64 . (x60 x64 ⟶ False) ⟶ x15 x61 ⟶ x3 x61 x64 x63 ⟶ x4 x61 (x6 (x5 x64 x63)) ⟶ x4 x62 x64 ⟶ (x4 (x7 x64 x63 x61 x62) x63 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 x63 x64 . (x0 x64 ⟶ False) ⟶ x16 x64 ⟶ x1 x64 ⟶ x4 x61 (x2 x64) ⟶ x4 x63 (x2 x64) ⟶ x4 x62 (x2 x64) ⟶ x8 x64 x61 x63 x61 x62 ⟶ (x37 x64 x61 x63 x62 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 x63 x64 . (x0 x64 ⟶ False) ⟶ x16 x64 ⟶ x1 x64 ⟶ x4 x61 (x2 x64) ⟶ x4 x63 (x2 x64) ⟶ x4 x62 (x2 x64) ⟶ x37 x64 x61 x63 x62 ⟶ (x8 x64 x61 x63 x61 x62 ⟶ False) ⟶ False) ⟶ (∀ x61 . x25 x61 ⟶ x38 x61 x59 ⟶ (x23 x61 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . x58 x62 ⟶ x4 x61 (x6 x62) ⟶ (x58 x61 ⟶ False) ⟶ False) ⟶ (∀ x61 . x25 x61 ⟶ x23 x61 ⟶ (x38 x61 x59 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 x63 . (x60 x63 ⟶ False) ⟶ (x60 x61 ⟶ False) ⟶ x4 x62 (x6 (x5 x63 x61)) ⟶ x15 x62 ⟶ x3 x62 x63 x61 ⟶ (x3 x62 x63 x61 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 x63 . (x60 x63 ⟶ False) ⟶ (x60 x61 ⟶ False) ⟶ x4 x62 (x6 (x5 x63 x61)) ⟶ x15 x62 ⟶ x3 x62 x63 x61 ⟶ x60 x62 ⟶ False) ⟶ (∀ x61 x62 x63 . (x60 x63 ⟶ False) ⟶ (x60 x61 ⟶ False) ⟶ x4 x62 (x6 (x5 x63 x61)) ⟶ x15 x62 ⟶ x3 x62 x63 x61 ⟶ (x15 x62 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . x58 x62 ⟶ x4 x61 x62 ⟶ (x15 x61 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . x58 x62 ⟶ x4 x61 x62 ⟶ (x22 x61 ⟶ False) ⟶ False) ⟶ (∀ x61 . x25 x61 ⟶ (x34 x61 ⟶ False) ⟶ x0 x61 ⟶ False) ⟶ (∀ x61 . x60 x61 ⟶ (x58 x61 ⟶ False) ⟶ False) ⟶ (∀ x61 . x25 x61 ⟶ x0 x61 ⟶ (x34 x61 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 x63 . x4 x63 (x6 (x5 x61 x62)) ⟶ x15 x63 ⟶ x50 x63 ⟶ x44 x63 x62 ⟶ (x14 x63 x61 x62 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 x63 . x4 x63 (x6 (x5 x61 x62)) ⟶ x15 x63 ⟶ x50 x63 ⟶ x44 x63 x62 ⟶ (x15 x63 ⟶ False) ⟶ False) ⟶ (∀ x61 . x28 x61 ⟶ x22 x61 ⟶ x15 x61 ⟶ (x54 x61 ⟶ False) ⟶ False) ⟶ (∀ x61 . x28 x61 ⟶ x22 x61 ⟶ x15 x61 ⟶ (x15 x61 ⟶ False) ⟶ False) ⟶ (∀ x61 . x28 x61 ⟶ x22 x61 ⟶ x15 x61 ⟶ (x22 x61 ⟶ False) ⟶ False) ⟶ (∀ x61 . x25 x61 ⟶ (x34 x61 ⟶ False) ⟶ x34 x61 ⟶ False) ⟶ (∀ x61 . x25 x61 ⟶ (x34 x61 ⟶ False) ⟶ x23 x61 ⟶ False) ⟶ (∀ x61 x62 x63 . x4 x63 (x6 (x5 x62 x61)) ⟶ x15 x63 ⟶ x14 x63 x62 x61 ⟶ (x44 x63 x61 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 x63 . x4 x63 (x6 (x5 x62 x61)) ⟶ x15 x63 ⟶ x14 x63 x62 x61 ⟶ (x50 x63 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 x63 . x4 x63 (x6 (x5 x62 x61)) ⟶ x15 x63 ⟶ x14 x63 x62 x61 ⟶ (x15 x63 ⟶ False) ⟶ False) ⟶ (∀ x61 . x22 x61 ⟶ x15 x61 ⟶ (x54 x61 ⟶ False) ⟶ (x15 x61 ⟶ False) ⟶ False) ⟶ (∀ x61 . x22 x61 ⟶ x15 x61 ⟶ (x54 x61 ⟶ False) ⟶ (x22 x61 ⟶ False) ⟶ False) ⟶ (∀ x61 . x22 x61 ⟶ x15 x61 ⟶ (x54 x61 ⟶ False) ⟶ x28 x61 ⟶ False) ⟶ (∀ x61 . x25 x61 ⟶ x23 x61 ⟶ (x34 x61 ⟶ False) ⟶ False) ⟶ (∀ x61 . x25 x61 ⟶ x23 x61 ⟶ (x23 x61 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 x63 . x60 x63 ⟶ x4 x61 (x6 (x5 x62 x63)) ⟶ (x60 x61 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . x4 x62 (x6 (x5 x61 x61)) ⟶ x3 x62 x61 x61 ⟶ (x51 x62 x61 ⟶ False) ⟶ False) ⟶ (∀ x61 . x60 x61 ⟶ x22 x61 ⟶ x15 x61 ⟶ (x54 x61 ⟶ False) ⟶ False) ⟶ (∀ x61 . x60 x61 ⟶ x22 x61 ⟶ x15 x61 ⟶ (x15 x61 ⟶ False) ⟶ False) ⟶ (∀ x61 . x60 x61 ⟶ x22 x61 ⟶ x15 x61 ⟶ (x22 x61 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 x63 . x60 x63 ⟶ x4 x61 (x6 (x5 x63 x62)) ⟶ (x60 x61 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 x63 . (x60 x63 ⟶ False) ⟶ x4 x61 (x6 (x5 x62 x63)) ⟶ x3 x61 x62 x63 ⟶ (x51 x61 x62 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . x22 x62 ⟶ x15 x62 ⟶ x4 x61 (x6 x62) ⟶ (x15 x61 ⟶ False) ⟶ False) ⟶ (∀ x61 . x25 x61 ⟶ (x0 x61 ⟶ False) ⟶ x23 x61 ⟶ False) ⟶ (∀ x61 x62 x63 . x4 x63 (x6 (x5 x61 x62)) ⟶ (x21 x63 x62 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 x63 . x4 x63 (x6 (x5 x62 x61)) ⟶ (x55 x63 x62 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 x63 . (x60 x63 ⟶ False) ⟶ x60 x61 ⟶ x4 x62 (x6 (x5 x63 x61)) ⟶ x51 x62 x63 ⟶ False) ⟶ (∀ x61 x62 x63 . x60 x63 ⟶ x4 x61 (x6 (x5 x63 x62)) ⟶ x3 x61 x63 x62 ⟶ (x51 x61 x63 ⟶ False) ⟶ False) ⟶ (∀ x61 . x60 x61 ⟶ x22 x61 ⟶ x15 x61 ⟶ (x50 x61 ⟶ False) ⟶ False) ⟶ (∀ x61 . x60 x61 ⟶ x22 x61 ⟶ x15 x61 ⟶ (x15 x61 ⟶ False) ⟶ False) ⟶ (∀ x61 . x60 x61 ⟶ x22 x61 ⟶ x15 x61 ⟶ (x22 x61 ⟶ False) ⟶ False) ⟶ (∀ x61 . x25 x61 ⟶ x23 x61 ⟶ (x0 x61 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 x63 . x4 x63 (x6 (x5 x61 x62)) ⟶ (x22 x63 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 x63 . x60 x63 ⟶ x4 x61 (x6 (x5 x63 x62)) ⟶ (x51 x61 x63 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 x63 . x4 x62 (x6 (x5 x63 x61)) ⟶ x51 x62 x63 ⟶ (x3 x62 x63 x61 ⟶ False) ⟶ False) ⟶ (∀ x61 . x60 x61 ⟶ (x15 x61 ⟶ False) ⟶ False) ⟶ (∀ x61 . x25 x61 ⟶ (x0 x61 ⟶ False) ⟶ x23 x61 ⟶ False) ⟶ (∀ x61 . x25 x61 ⟶ x38 x61 x19 ⟶ (x0 x61 ⟶ False) ⟶ False) ⟶ (∀ x61 . x25 x61 ⟶ x38 x61 x19 ⟶ x23 x61 ⟶ False) ⟶ (∀ x61 . x25 x61 ⟶ (x23 x61 ⟶ False) ⟶ x0 x61 ⟶ (x38 x61 x19 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . x17 x61 x62 ⟶ x17 x62 x61 ⟶ False) ⟶ ((x37 x39 (x7 (x2 x39) (x2 x39) x43 x42) (x7 (x2 x39) (x2 x39) x43 x41) (x7 (x2 x39) (x2 x39) x43 x40) ⟶ False) ⟶ (x37 x39 x42 x41 x40 ⟶ False) ⟶ False) ⟶ (x37 x39 x42 x41 x40 ⟶ x37 x39 (x7 (x2 x39) (x2 x39) x43 x42) (x7 (x2 x39) (x2 x39) x43 x41) (x7 (x2 x39) (x2 x39) x43 x40) ⟶ False) ⟶ ((x13 x43 x39 ⟶ False) ⟶ False) ⟶ ((x4 x43 (x6 (x5 (x2 x39) (x2 x39))) ⟶ False) ⟶ False) ⟶ ((x14 x43 (x2 x39) (x2 x39) ⟶ False) ⟶ False) ⟶ ((x3 x43 (x2 x39) (x2 x39) ⟶ False) ⟶ False) ⟶ ((x15 x43 ⟶ False) ⟶ False) ⟶ ((x4 x40 (x2 x39) ⟶ False) ⟶ False) ⟶ ((x4 x41 (x2 x39) ⟶ False) ⟶ False) ⟶ ((x4 x42 (x2 x39) ⟶ False) ⟶ False) ⟶ ((x1 x39 ⟶ False) ⟶ False) ⟶ ((x16 x39 ⟶ False) ⟶ False) ⟶ (x0 x39 ⟶ False) ⟶ False (proof)

Proofgold Asset