Proofgold Proposition

∀ 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 . x74 x76 ⟶ (x76 = x75 ⟶ False) ⟶ x74 x75 ⟶ False) ⟶ (∀ x75 x76 . x0 x75 x76 ⟶ x74 x76 ⟶ False) ⟶ (∀ x75 . x74 x75 ⟶ (x75 = x73 ⟶ False) ⟶ False) ⟶ (∀ x75 x76 x77 x78 x79 x80 . (x1 x80 ⟶ False) ⟶ (x19 x80 ⟶ False) ⟶ x2 x80 ⟶ x18 x80 ⟶ x3 x80 ⟶ x17 x80 ⟶ x4 x80 ⟶ x16 x80 ⟶ (x1 x79 ⟶ False) ⟶ (x19 x79 ⟶ False) ⟶ x2 x79 ⟶ x18 x79 ⟶ x3 x79 ⟶ x17 x79 ⟶ x4 x79 ⟶ x16 x79 ⟶ x5 x78 ⟶ x14 x78 (x15 x80) (x15 x79) ⟶ x6 x78 (x8 (x7 (x15 x80) (x15 x79))) ⟶ x6 x75 (x13 x79) ⟶ x11 (x15 x80) (x15 x79) x78 (x9 x80 (x10 x78 x79 x80)) = x9 x79 x75 ⟶ x6 x76 (x13 x80) ⟶ x6 x77 (x13 x79) ⟶ x11 (x15 x80) (x15 x79) x78 (x9 x80 x76) = x9 x79 x77 ⟶ (x11 (x13 x80) (x13 x79) (x12 x80 x79 x78) x76 = x77 ⟶ False) ⟶ False) ⟶ (∀ x75 x76 x77 x78 x79 . (x1 x79 ⟶ False) ⟶ (x19 x79 ⟶ False) ⟶ x2 x79 ⟶ x18 x79 ⟶ x3 x79 ⟶ x17 x79 ⟶ x4 x79 ⟶ x16 x79 ⟶ (x1 x78 ⟶ False) ⟶ (x19 x78 ⟶ False) ⟶ x2 x78 ⟶ x18 x78 ⟶ x3 x78 ⟶ x17 x78 ⟶ x4 x78 ⟶ x16 x78 ⟶ x5 x77 ⟶ x14 x77 (x15 x79) (x15 x78) ⟶ x6 x77 (x8 (x7 (x15 x79) (x15 x78))) ⟶ (x6 (x10 x77 x78 x79) (x13 x79) ⟶ False) ⟶ x6 x76 (x13 x79) ⟶ x6 x75 (x13 x78) ⟶ x11 (x15 x79) (x15 x78) x77 (x9 x79 x76) = x9 x78 x75 ⟶ (x11 (x13 x79) (x13 x78) (x12 x79 x78 x77) x76 = x75 ⟶ False) ⟶ False) ⟶ (∀ x75 x76 x77 . x0 x75 x76 ⟶ x6 x76 (x8 x77) ⟶ x74 x77 ⟶ False) ⟶ (∀ x75 x76 x77 . x0 x76 x77 ⟶ x6 x77 (x8 x75) ⟶ (x6 x76 x75 ⟶ False) ⟶ False) ⟶ (∀ x75 x76 . x20 x76 x75 ⟶ (x6 x76 (x8 x75) ⟶ False) ⟶ False) ⟶ (∀ x75 x76 . x6 x76 (x8 x75) ⟶ (x20 x76 x75 ⟶ False) ⟶ False) ⟶ (∀ x75 x76 . x6 x75 x76 ⟶ (x74 x76 ⟶ False) ⟶ (x0 x75 x76 ⟶ False) ⟶ False) ⟶ (∀ x75 x76 . x0 x76 x75 ⟶ (x6 x76 x75 ⟶ False) ⟶ False) ⟶ (x74 x21 ⟶ False) ⟶ (∀ x75 . (x20 x75 x75 ⟶ False) ⟶ False) ⟶ (∀ x75 x76 x77 x78 . (x74 x78 ⟶ False) ⟶ x5 x75 ⟶ x14 x75 x78 x77 ⟶ x6 x75 (x8 (x7 x78 x77)) ⟶ x6 x76 x78 ⟶ (x11 x78 x77 x75 x76 = x22 x75 x76 ⟶ False) ⟶ False) ⟶ (∀ x75 x76 x77 x78 . (x74 x78 ⟶ False) ⟶ (x74 x75 ⟶ False) ⟶ (x74 x77 ⟶ False) ⟶ x5 x76 ⟶ x6 x76 (x8 (x7 (x7 x78 x75) x77)) ⟶ (x72 x78 x75 x77 x76 = x71 x76 ⟶ False) ⟶ False) ⟶ (∀ x75 . (x1 x75 ⟶ False) ⟶ x24 x75 ⟶ x74 (x23 x75) ⟶ False) ⟶ (∀ x75 . (x1 x75 ⟶ False) ⟶ x24 x75 ⟶ (x6 (x23 x75) (x8 (x13 x75)) ⟶ False) ⟶ False) ⟶ ((x4 x25 ⟶ False) ⟶ False) ⟶ ((x17 x25 ⟶ False) ⟶ False) ⟶ ((x3 x25 ⟶ False) ⟶ False) ⟶ ((x18 x25 ⟶ False) ⟶ False) ⟶ ((x2 x25 ⟶ False) ⟶ False) ⟶ ((x70 x25 ⟶ False) ⟶ False) ⟶ ((x26 x25 ⟶ False) ⟶ False) ⟶ (x19 x25 ⟶ False) ⟶ (x1 x25 ⟶ False) ⟶ ((x16 x25 ⟶ False) ⟶ False) ⟶ (x74 x27 ⟶ False) ⟶ (x19 x69 ⟶ False) ⟶ (x1 x69 ⟶ False) ⟶ ((x16 x69 ⟶ False) ⟶ False) ⟶ (x28 x29 ⟶ False) ⟶ ((x68 x29 ⟶ False) ⟶ False) ⟶ (∀ x75 . (x30 x75 ⟶ False) ⟶ x24 x75 ⟶ x31 (x32 x75) ⟶ False) ⟶ (∀ x75 . (x30 x75 ⟶ False) ⟶ x24 x75 ⟶ (x6 (x32 x75) (x8 (x13 x75)) ⟶ False) ⟶ False) ⟶ (∀ x75 . (x1 x75 ⟶ False) ⟶ x24 x75 ⟶ (x31 (x33 x75) ⟶ False) ⟶ False) ⟶ (∀ x75 . (x1 x75 ⟶ False) ⟶ x24 x75 ⟶ x74 (x33 x75) ⟶ False) ⟶ (∀ x75 . (x1 x75 ⟶ False) ⟶ x24 x75 ⟶ (x6 (x33 x75) (x8 (x13 x75)) ⟶ False) ⟶ False) ⟶ ((x74 x67 ⟶ False) ⟶ False) ⟶ (∀ x75 x76 . (x34 (x35 x75 x76) x75 ⟶ False) ⟶ False) ⟶ (∀ x75 x76 . (x66 (x35 x76 x75) x75 ⟶ False) ⟶ False) ⟶ (∀ x75 x76 . (x36 (x35 x75 x76) ⟶ False) ⟶ False) ⟶ (∀ x75 x76 . (x74 (x35 x75 x76) ⟶ False) ⟶ False) ⟶ (∀ x75 x76 . (x6 (x35 x75 x76) (x8 (x7 x76 x75)) ⟶ False) ⟶ False) ⟶ (∀ x75 x76 . (x14 (x65 x75 x76) x76 x75 ⟶ False) ⟶ False) ⟶ (∀ x75 x76 . (x5 (x65 x75 x76) ⟶ False) ⟶ False) ⟶ (∀ x75 x76 . (x34 (x65 x75 x76) x75 ⟶ False) ⟶ False) ⟶ (∀ x75 x76 . (x66 (x65 x76 x75) x75 ⟶ False) ⟶ False) ⟶ (∀ x75 x76 . (x36 (x65 x75 x76) ⟶ False) ⟶ False) ⟶ (∀ x75 x76 . (x6 (x65 x75 x76) (x8 (x7 x76 x75)) ⟶ False) ⟶ False) ⟶ ((x70 x64 ⟶ False) ⟶ False) ⟶ ((x16 x64 ⟶ False) ⟶ False) ⟶ (∀ x75 x76 x77 x78 . (x1 x78 ⟶ False) ⟶ (x19 x78 ⟶ False) ⟶ x2 x78 ⟶ x18 x78 ⟶ x3 x78 ⟶ x17 x78 ⟶ x4 x78 ⟶ x16 x78 ⟶ (x1 x77 ⟶ False) ⟶ (x19 x77 ⟶ False) ⟶ x2 x77 ⟶ x18 x77 ⟶ x3 x77 ⟶ x17 x77 ⟶ x4 x77 ⟶ x16 x77 ⟶ x63 x76 x78 x77 ⟶ x6 x75 (x13 (x60 x78)) ⟶ (x11 (x15 (x60 x78)) (x15 x77) (x62 x78 x77 x76) (x9 (x60 x78) x75) = x9 x77 (x11 (x13 x78) (x13 x77) (x12 x78 x77 x76) (x61 x78 x75)) ⟶ False) ⟶ False) ⟶ (∀ x75 x76 x77 x78 x79 x80 x81 x82 x83 x84 . x5 x84 ⟶ x14 x84 x75 x76 ⟶ x6 x84 (x8 (x7 x75 x76)) ⟶ x5 x77 ⟶ x14 x77 x75 x76 ⟶ x6 x77 (x8 (x7 x75 x76)) ⟶ x5 x83 ⟶ x6 x83 (x8 (x7 (x7 x75 x75) x75)) ⟶ x37 x76 x75 x84 x77 x83 = x37 x81 x78 x80 x79 x82 ⟶ (x83 = x82 ⟶ False) ⟶ False) ⟶ (∀ x75 x76 x77 x78 x79 x80 x81 x82 x83 x84 . x5 x84 ⟶ x14 x84 x75 x76 ⟶ x6 x84 (x8 (x7 x75 x76)) ⟶ x5 x77 ⟶ x14 x77 x75 x76 ⟶ x6 x77 (x8 (x7 x75 x76)) ⟶ x5 x83 ⟶ x6 x83 (x8 (x7 (x7 x75 x75) x75)) ⟶ x37 x76 x75 x84 x77 x83 = x37 x81 x78 x80 x82 x79 ⟶ (x77 = x82 ⟶ False) ⟶ False) ⟶ (∀ x75 x76 x77 x78 x79 x80 x81 x82 x83 x84 . x5 x84 ⟶ x14 x84 x75 x76 ⟶ x6 x84 (x8 (x7 x75 x76)) ⟶ x5 x77 ⟶ x14 x77 x75 x76 ⟶ x6 x77 (x8 (x7 x75 x76)) ⟶ x5 x83 ⟶ x6 x83 (x8 (x7 (x7 x75 x75) x75)) ⟶ x37 x76 x75 x84 x77 x83 = x37 x81 x78 x82 x80 x79 ⟶ (x84 = x82 ⟶ False) ⟶ False) ⟶ (∀ x75 x76 x77 x78 x79 x80 x81 x82 x83 x84 . x5 x84 ⟶ x14 x84 x75 x76 ⟶ x6 x84 (x8 (x7 x75 x76)) ⟶ x5 x77 ⟶ x14 x77 x75 x76 ⟶ x6 x77 (x8 (x7 x75 x76)) ⟶ x5 x83 ⟶ x6 x83 (x8 (x7 (x7 x75 x75) x75)) ⟶ x37 x76 x75 x84 x77 x83 = x37 x81 x82 x80 x79 x78 ⟶ (x75 = x82 ⟶ False) ⟶ False) ⟶ (∀ x75 x76 x77 x78 x79 x80 x81 x82 x83 x84 . x5 x84 ⟶ x14 x84 x75 x76 ⟶ x6 x84 (x8 (x7 x75 x76)) ⟶ x5 x77 ⟶ x14 x77 x75 x76 ⟶ x6 x77 (x8 (x7 x75 x76)) ⟶ x5 x83 ⟶ x6 x83 (x8 (x7 (x7 x75 x75) x75)) ⟶ x37 x76 x75 x84 x77 x83 = x37 x82 x78 x81 x80 x79 ⟶ (x76 = x82 ⟶ False) ⟶ False) ⟶ (∀ x75 . (x59 x75 ⟶ False) ⟶ x24 x75 ⟶ x58 (x13 x75) ⟶ False) ⟶ (∀ x75 . x59 x75 ⟶ x24 x75 ⟶ (x58 (x13 x75) ⟶ False) ⟶ False) ⟶ (∀ x75 . x30 x75 ⟶ x24 x75 ⟶ (x31 (x13 x75) ⟶ False) ⟶ False) ⟶ (∀ x75 . (x30 x75 ⟶ False) ⟶ x24 x75 ⟶ x31 (x13 x75) ⟶ False) ⟶ (∀ x75 . (x1 x75 ⟶ False) ⟶ x24 x75 ⟶ x74 (x13 x75) ⟶ False) ⟶ (∀ x75 . (x28 x75 ⟶ False) ⟶ x68 x75 ⟶ x31 (x15 x75) ⟶ False) ⟶ (∀ x75 . x28 x75 ⟶ x68 x75 ⟶ (x31 (x15 x75) ⟶ False) ⟶ False) ⟶ ((x74 x73 ⟶ False) ⟶ False) ⟶ (∀ x75 . x1 x75 ⟶ x24 x75 ⟶ (x74 (x13 x75) ⟶ False) ⟶ False) ⟶ (∀ x75 . (x1 x75 ⟶ False) ⟶ (x19 x75 ⟶ False) ⟶ x2 x75 ⟶ x18 x75 ⟶ x3 x75 ⟶ x17 x75 ⟶ x4 x75 ⟶ x16 x75 ⟶ (x4 (x60 x75) ⟶ False) ⟶ False) ⟶ (∀ x75 . (x1 x75 ⟶ False) ⟶ (x19 x75 ⟶ False) ⟶ x2 x75 ⟶ x18 x75 ⟶ x3 x75 ⟶ x17 x75 ⟶ x4 x75 ⟶ x16 x75 ⟶ (x17 (x60 x75) ⟶ False) ⟶ False) ⟶ (∀ x75 . (x1 x75 ⟶ False) ⟶ (x19 x75 ⟶ False) ⟶ x2 x75 ⟶ x18 x75 ⟶ x3 x75 ⟶ x17 x75 ⟶ x4 x75 ⟶ x16 x75 ⟶ (x3 (x60 x75) ⟶ False) ⟶ False) ⟶ (∀ x75 . (x1 x75 ⟶ False) ⟶ (x19 x75 ⟶ False) ⟶ x2 x75 ⟶ x18 x75 ⟶ x3 x75 ⟶ x17 x75 ⟶ x4 x75 ⟶ x16 x75 ⟶ (x18 (x60 x75) ⟶ False) ⟶ False) ⟶ (∀ x75 . (x1 x75 ⟶ False) ⟶ (x19 x75 ⟶ False) ⟶ x2 x75 ⟶ x18 x75 ⟶ x3 x75 ⟶ x17 x75 ⟶ x4 x75 ⟶ x16 x75 ⟶ (x2 (x60 x75) ⟶ False) ⟶ False) ⟶ (∀ x75 . (x1 x75 ⟶ False) ⟶ (x19 x75 ⟶ False) ⟶ x2 x75 ⟶ x18 x75 ⟶ x3 x75 ⟶ x17 x75 ⟶ x4 x75 ⟶ x16 x75 ⟶ (x70 (x60 x75) ⟶ False) ⟶ False) ⟶ (∀ x75 . (x1 x75 ⟶ False) ⟶ (x19 x75 ⟶ False) ⟶ x2 x75 ⟶ x18 x75 ⟶ x3 x75 ⟶ x17 x75 ⟶ x4 x75 ⟶ x16 x75 ⟶ x19 (x60 x75) ⟶ False) ⟶ (∀ x75 . (x1 x75 ⟶ False) ⟶ (x19 x75 ⟶ False) ⟶ x2 x75 ⟶ x18 x75 ⟶ x3 x75 ⟶ x17 x75 ⟶ x4 x75 ⟶ x16 x75 ⟶ x1 (x60 x75) ⟶ False) ⟶ (∀ x75 . (x19 x75 ⟶ False) ⟶ x68 x75 ⟶ x74 (x15 x75) ⟶ False) ⟶ (∀ x75 . x19 x75 ⟶ x68 x75 ⟶ (x74 (x15 x75) ⟶ False) ⟶ False) ⟶ (∀ x75 . (x6 (x38 x75) x75 ⟶ False) ⟶ False) ⟶ (∀ x75 x76 . (x1 x76 ⟶ False) ⟶ (x19 x76 ⟶ False) ⟶ x2 x76 ⟶ x18 x76 ⟶ x3 x76 ⟶ x17 x76 ⟶ x4 x76 ⟶ x16 x76 ⟶ (x1 x75 ⟶ False) ⟶ (x19 x75 ⟶ False) ⟶ x2 x75 ⟶ x18 x75 ⟶ x3 x75 ⟶ x17 x75 ⟶ x4 x75 ⟶ x16 x75 ⟶ (x63 (x57 x75 x76) x76 x75 ⟶ False) ⟶ False) ⟶ (∀ x75 x76 x77 . (x1 x77 ⟶ False) ⟶ (x19 x77 ⟶ False) ⟶ x16 x77 ⟶ x6 x75 (x13 x77) ⟶ x6 x76 (x13 x77) ⟶ (x39 (x40 x76 x75 x77) x77 x75 x76 ⟶ False) ⟶ False) ⟶ ((x68 x56 ⟶ False) ⟶ False) ⟶ ((x24 x41 ⟶ False) ⟶ False) ⟶ ((x55 x54 ⟶ False) ⟶ False) ⟶ ((x16 x42 ⟶ False) ⟶ False) ⟶ (∀ x75 . x55 x75 ⟶ (x6 (x53 x75) (x8 (x7 (x15 x75) (x13 x75))) ⟶ False) ⟶ False) ⟶ (∀ x75 . x55 x75 ⟶ (x14 (x53 x75) (x15 x75) (x13 x75) ⟶ False) ⟶ False) ⟶ (∀ x75 . x55 x75 ⟶ (x5 (x53 x75) ⟶ False) ⟶ False) ⟶ (∀ x75 . x55 x75 ⟶ (x6 (x43 x75) (x8 (x7 (x15 x75) (x13 x75))) ⟶ False) ⟶ False) ⟶ (∀ x75 . x55 x75 ⟶ (x14 (x43 x75) (x15 x75) (x13 x75) ⟶ False) ⟶ False) ⟶ (∀ x75 . x55 x75 ⟶ (x5 (x43 x75) ⟶ False) ⟶ False) ⟶ (∀ x75 . x16 x75 ⟶ (x6 (x52 x75) (x8 (x7 (x7 (x15 x75) (x15 x75)) (x15 x75))) ⟶ False) ⟶ False) ⟶ (∀ x75 . x16 x75 ⟶ (x5 (x52 x75) ⟶ False) ⟶ False) ⟶ ((x74 x51 ⟶ False) ⟶ False) ⟶ (∀ x75 x76 x77 . (x1 x77 ⟶ False) ⟶ (x19 x77 ⟶ False) ⟶ x2 x77 ⟶ x18 x77 ⟶ x3 x77 ⟶ x17 x77 ⟶ x4 x77 ⟶ x16 x77 ⟶ (x1 x76 ⟶ False) ⟶ (x19 x76 ⟶ False) ⟶ x2 x76 ⟶ x18 x76 ⟶ x3 x76 ⟶ x17 x76 ⟶ x4 x76 ⟶ x16 x76 ⟶ x63 x75 x77 x76 ⟶ (x6 x75 (x8 (x7 (x15 x77) (x15 x76))) ⟶ False) ⟶ False) ⟶ (∀ x75 x76 x77 . (x1 x77 ⟶ False) ⟶ (x19 x77 ⟶ False) ⟶ x2 x77 ⟶ x18 x77 ⟶ x3 x77 ⟶ x17 x77 ⟶ x4 x77 ⟶ x16 x77 ⟶ (x1 x76 ⟶ False) ⟶ (x19 x76 ⟶ False) ⟶ x2 x76 ⟶ x18 x76 ⟶ x3 x76 ⟶ x17 x76 ⟶ x4 x76 ⟶ x16 x76 ⟶ x63 x75 x77 x76 ⟶ (x14 x75 (x15 x77) (x15 x76) ⟶ False) ⟶ False) ⟶ (∀ x75 x76 x77 . (x1 x77 ⟶ False) ⟶ (x19 x77 ⟶ False) ⟶ x2 x77 ⟶ x18 x77 ⟶ x3 x77 ⟶ x17 x77 ⟶ x4 x77 ⟶ x16 x77 ⟶ (x1 x76 ⟶ False) ⟶ (x19 x76 ⟶ False) ⟶ x2 x76 ⟶ x18 x76 ⟶ x3 x76 ⟶ x17 x76 ⟶ x4 x76 ⟶ x16 x76 ⟶ x63 x75 x77 x76 ⟶ (x5 x75 ⟶ False) ⟶ False) ⟶ (∀ x75 x76 x77 x78 . (x1 x78 ⟶ False) ⟶ (x19 x78 ⟶ False) ⟶ x16 x78 ⟶ x6 x75 (x13 x78) ⟶ x6 x77 (x13 x78) ⟶ x39 x76 x78 x75 x77 ⟶ (x6 x76 (x15 x78) ⟶ False) ⟶ False) ⟶ (∀ x75 . x68 x75 ⟶ (x24 x75 ⟶ False) ⟶ False) ⟶ (∀ x75 . x55 x75 ⟶ (x68 x75 ⟶ False) ⟶ False) ⟶ (∀ x75 . x16 x75 ⟶ (x55 x75 ⟶ False) ⟶ False) ⟶ (∀ x75 x76 x77 . (x1 x77 ⟶ False) ⟶ (x19 x77 ⟶ False) ⟶ x2 x77 ⟶ x18 x77 ⟶ x3 x77 ⟶ x17 x77 ⟶ x4 x77 ⟶ x16 x77 ⟶ (x1 x76 ⟶ False) ⟶ (x19 x76 ⟶ False) ⟶ x2 x76 ⟶ x18 x76 ⟶ x3 x76 ⟶ x17 x76 ⟶ x4 x76 ⟶ x16 x76 ⟶ x5 x75 ⟶ x14 x75 (x15 x77) (x15 x76) ⟶ x6 x75 (x8 (x7 (x15 x77) (x15 x76))) ⟶ (x6 (x12 x77 x76 x75) (x8 (x7 (x13 x77) (x13 x76))) ⟶ False) ⟶ False) ⟶ (∀ x75 x76 x77 . (x1 x77 ⟶ False) ⟶ (x19 x77 ⟶ False) ⟶ x2 x77 ⟶ x18 x77 ⟶ x3 x77 ⟶ x17 x77 ⟶ x4 x77 ⟶ x16 x77 ⟶ (x1 x76 ⟶ False) ⟶ (x19 x76 ⟶ False) ⟶ x2 x76 ⟶ x18 x76 ⟶ x3 x76 ⟶ x17 x76 ⟶ x4 x76 ⟶ x16 x76 ⟶ x5 x75 ⟶ x14 x75 (x15 x77) (x15 x76) ⟶ x6 x75 (x8 (x7 (x15 x77) (x15 x76))) ⟶ (x14 (x12 x77 x76 x75) (x13 x77) (x13 x76) ⟶ False) ⟶ False) ⟶ (∀ x75 x76 x77 . (x1 x77 ⟶ False) ⟶ (x19 x77 ⟶ False) ⟶ x2 x77 ⟶ x18 x77 ⟶ x3 x77 ⟶ x17 x77 ⟶ x4 x77 ⟶ x16 x77 ⟶ (x1 x76 ⟶ False) ⟶ (x19 x76 ⟶ False) ⟶ x2 x76 ⟶ x18 x76 ⟶ x3 x76 ⟶ x17 x76 ⟶ x4 x76 ⟶ x16 x76 ⟶ x5 x75 ⟶ x14 x75 (x15 x77) (x15 x76) ⟶ x6 x75 (x8 (x7 (x15 x77) (x15 x76))) ⟶ (x5 (x12 x77 x76 x75) ⟶ False) ⟶ False) ⟶ (∀ x75 x76 . (x1 x76 ⟶ False) ⟶ (x19 x76 ⟶ False) ⟶ x2 x76 ⟶ x18 x76 ⟶ x3 x76 ⟶ x17 x76 ⟶ x4 x76 ⟶ x16 x76 ⟶ x6 x75 (x13 (x60 x76)) ⟶ (x6 (x61 x76 x75) (x13 x76) ⟶ False) ⟶ False) ⟶ (∀ x75 x76 . (x1 x76 ⟶ False) ⟶ (x19 x76 ⟶ False) ⟶ x17 x76 ⟶ x4 x76 ⟶ x16 x76 ⟶ x6 x75 (x13 x76) ⟶ (x39 (x9 x76 x75) x76 x75 x75 ⟶ False) ⟶ False) ⟶ (∀ x75 x76 . (x1 x76 ⟶ False) ⟶ (x19 x76 ⟶ False) ⟶ x2 x76 ⟶ x18 x76 ⟶ x3 x76 ⟶ x17 x76 ⟶ x4 x76 ⟶ x16 x76 ⟶ x6 x75 (x13 x76) ⟶ (x6 (x44 x76 x75) (x13 (x60 x76)) ⟶ False) ⟶ False) ⟶ (∀ x75 x76 x77 x78 . (x74 x78 ⟶ False) ⟶ x5 x75 ⟶ x14 x75 x78 x77 ⟶ x6 x75 (x8 (x7 x78 x77)) ⟶ x6 x76 x78 ⟶ (x6 (x11 x78 x77 x75 x76) x77 ⟶ False) ⟶ False) ⟶ (∀ x75 . (x1 x75 ⟶ False) ⟶ (x19 x75 ⟶ False) ⟶ x2 x75 ⟶ x18 x75 ⟶ x3 x75 ⟶ x17 x75 ⟶ x4 x75 ⟶ x16 x75 ⟶ (x16 (x60 x75) ⟶ False) ⟶ False) ⟶ (∀ x75 . (x1 x75 ⟶ False) ⟶ (x19 x75 ⟶ False) ⟶ x2 x75 ⟶ x18 x75 ⟶ x3 x75 ⟶ x17 x75 ⟶ x4 x75 ⟶ x16 x75 ⟶ (x70 (x60 x75) ⟶ False) ⟶ False) ⟶ (∀ x75 . (x1 x75 ⟶ False) ⟶ (x19 x75 ⟶ False) ⟶ x2 x75 ⟶ x18 x75 ⟶ x3 x75 ⟶ x17 x75 ⟶ x4 x75 ⟶ x16 x75 ⟶ x19 (x60 x75) ⟶ False) ⟶ (∀ x75 . (x1 x75 ⟶ False) ⟶ (x19 x75 ⟶ False) ⟶ x2 x75 ⟶ x18 x75 ⟶ x3 x75 ⟶ x17 x75 ⟶ x4 x75 ⟶ x16 x75 ⟶ x1 (x60 x75) ⟶ False) ⟶ (∀ x75 . x36 x75 ⟶ x5 x75 ⟶ (x5 (x71 x75) ⟶ False) ⟶ False) ⟶ (∀ x75 . x36 x75 ⟶ x5 x75 ⟶ (x36 (x71 x75) ⟶ False) ⟶ False) ⟶ (∀ x75 x76 x77 x78 . (x74 x78 ⟶ False) ⟶ (x74 x75 ⟶ False) ⟶ (x74 x77 ⟶ False) ⟶ x5 x76 ⟶ x6 x76 (x8 (x7 (x7 x78 x75) x77)) ⟶ (x6 (x72 x78 x75 x77 x76) (x8 (x7 (x7 x75 x78) x77)) ⟶ False) ⟶ False) ⟶ (∀ x75 x76 x77 x78 . (x74 x78 ⟶ False) ⟶ (x74 x75 ⟶ False) ⟶ (x74 x77 ⟶ False) ⟶ x5 x76 ⟶ x6 x76 (x8 (x7 (x7 x78 x75) x77)) ⟶ (x5 (x72 x78 x75 x77 x76) ⟶ False) ⟶ False) ⟶ (∀ x75 x76 x77 . (x1 x77 ⟶ False) ⟶ (x19 x77 ⟶ False) ⟶ x2 x77 ⟶ x18 x77 ⟶ x3 x77 ⟶ x17 x77 ⟶ x4 x77 ⟶ x16 x77 ⟶ (x1 x76 ⟶ False) ⟶ (x19 x76 ⟶ False) ⟶ x2 x76 ⟶ x18 x76 ⟶ x3 x76 ⟶ x17 x76 ⟶ x4 x76 ⟶ x16 x76 ⟶ x5 x75 ⟶ x14 x75 (x15 x77) (x15 x76) ⟶ x6 x75 (x8 (x7 (x15 x77) (x15 x76))) ⟶ (x6 (x62 x77 x76 x75) (x8 (x7 (x15 (x60 x77)) (x15 x76))) ⟶ False) ⟶ False) ⟶ (∀ x75 x76 x77 . (x1 x77 ⟶ False) ⟶ (x19 x77 ⟶ False) ⟶ x2 x77 ⟶ x18 x77 ⟶ x3 x77 ⟶ x17 x77 ⟶ x4 x77 ⟶ x16 x77 ⟶ (x1 x76 ⟶ False) ⟶ (x19 x76 ⟶ False) ⟶ x2 x76 ⟶ x18 x76 ⟶ x3 x76 ⟶ x17 x76 ⟶ x4 x76 ⟶ x16 x76 ⟶ x5 x75 ⟶ x14 x75 (x15 x77) (x15 x76) ⟶ x6 x75 (x8 (x7 (x15 x77) (x15 x76))) ⟶ (x14 (x62 x77 x76 x75) (x15 (x60 x77)) (x15 x76) ⟶ False) ⟶ False) ⟶ (∀ x75 x76 x77 . (x1 x77 ⟶ False) ⟶ (x19 x77 ⟶ False) ⟶ x2 x77 ⟶ x18 x77 ⟶ x3 x77 ⟶ x17 x77 ⟶ x4 x77 ⟶ x16 x77 ⟶ (x1 x76 ⟶ False) ⟶ (x19 x76 ⟶ False) ⟶ x2 x76 ⟶ x18 x76 ⟶ x3 x76 ⟶ x17 x76 ⟶ x4 x76 ⟶ x16 x76 ⟶ x5 x75 ⟶ x14 x75 (x15 x77) (x15 x76) ⟶ x6 x75 (x8 (x7 (x15 x77) (x15 x76))) ⟶ (x5 (x62 x77 x76 x75) ⟶ False) ⟶ False) ⟶ (∀ x75 x76 x77 x78 x79 . x5 x79 ⟶ x14 x79 x75 x76 ⟶ x6 x79 (x8 (x7 x75 x76)) ⟶ x5 x77 ⟶ x14 x77 x75 x76 ⟶ x6 x77 (x8 (x7 x75 x76)) ⟶ x5 x78 ⟶ x6 x78 (x8 (x7 (x7 x75 x75) x75)) ⟶ (x16 (x37 x76 x75 x79 x77 x78) ⟶ False) ⟶ False) ⟶ (∀ x75 x76 x77 x78 x79 . x5 x79 ⟶ x14 x79 x75 x76 ⟶ x6 x79 (x8 (x7 x75 x76)) ⟶ x5 x77 ⟶ x14 x77 x75 x76 ⟶ x6 x77 (x8 (x7 x75 x76)) ⟶ x5 x78 ⟶ x6 x78 (x8 (x7 (x7 x75 x75) x75)) ⟶ (x70 (x37 x76 x75 x79 x77 x78) ⟶ False) ⟶ False) ⟶ (∀ x75 x76 . (x1 x76 ⟶ False) ⟶ (x19 x76 ⟶ False) ⟶ x2 x76 ⟶ x18 x76 ⟶ x3 x76 ⟶ x17 x76 ⟶ x4 x76 ⟶ x16 x76 ⟶ x6 x75 (x13 (x60 x76)) ⟶ (x61 x76 x75 = x44 (x60 x76) x75 ⟶ False) ⟶ False) ⟶ ((x73 = x51 ⟶ False) ⟶ False) ⟶ (∀ x75 x76 . (x1 x76 ⟶ False) ⟶ (x19 x76 ⟶ False) ⟶ x2 x76 ⟶ x18 x76 ⟶ x3 x76 ⟶ x17 x76 ⟶ x4 x76 ⟶ x16 x76 ⟶ x6 x75 (x13 x76) ⟶ (x44 x76 x75 = x75 ⟶ False) ⟶ False) ⟶ (∀ x75 . (x1 x75 ⟶ False) ⟶ (x19 x75 ⟶ False) ⟶ x2 x75 ⟶ x18 x75 ⟶ x3 x75 ⟶ x17 x75 ⟶ x4 x75 ⟶ x16 x75 ⟶ (x60 x75 = x37 (x13 x75) (x15 x75) (x53 x75) (x43 x75) (x72 (x15 x75) (x15 x75) (x15 x75) (x52 x75)) ⟶ False) ⟶ False) ⟶ (∀ x75 . x24 x75 ⟶ x50 x75 x73 ⟶ (x1 x75 ⟶ False) ⟶ False) ⟶ (∀ x75 . x24 x75 ⟶ x1 x75 ⟶ (x50 x75 x73 ⟶ False) ⟶ False) ⟶ (∀ x75 x76 x77 . (x74 x77 ⟶ False) ⟶ (x74 x75 ⟶ False) ⟶ x6 x76 (x8 (x7 x77 x75)) ⟶ x5 x76 ⟶ x14 x76 x77 x75 ⟶ (x14 x76 x77 x75 ⟶ False) ⟶ False) ⟶ (∀ x75 x76 x77 . (x74 x77 ⟶ False) ⟶ (x74 x75 ⟶ False) ⟶ x6 x76 (x8 (x7 x77 x75)) ⟶ x5 x76 ⟶ x14 x76 x77 x75 ⟶ x74 x76 ⟶ False) ⟶ (∀ x75 x76 x77 . (x74 x77 ⟶ False) ⟶ (x74 x75 ⟶ False) ⟶ x6 x76 (x8 (x7 x77 x75)) ⟶ x5 x76 ⟶ x14 x76 x77 x75 ⟶ (x5 x76 ⟶ False) ⟶ False) ⟶ (∀ x75 . x24 x75 ⟶ (x59 x75 ⟶ False) ⟶ x30 x75 ⟶ False) ⟶ (∀ x75 . x24 x75 ⟶ x30 x75 ⟶ (x59 x75 ⟶ False) ⟶ False) ⟶ (∀ x75 . x24 x75 ⟶ (x59 x75 ⟶ False) ⟶ x59 x75 ⟶ False) ⟶ (∀ x75 . x24 x75 ⟶ (x59 x75 ⟶ False) ⟶ x1 x75 ⟶ False) ⟶ (∀ x75 . x24 x75 ⟶ x1 x75 ⟶ (x59 x75 ⟶ False) ⟶ False) ⟶ (∀ x75 . x24 x75 ⟶ x1 x75 ⟶ (x1 x75 ⟶ False) ⟶ False) ⟶ (∀ x75 x76 x77 . x74 x77 ⟶ x6 x75 (x8 (x7 x76 x77)) ⟶ (x74 x75 ⟶ False) ⟶ False) ⟶ (∀ x75 x76 . x6 x76 (x8 (x7 x75 x75)) ⟶ x14 x76 x75 x75 ⟶ (x49 x76 x75 ⟶ False) ⟶ False) ⟶ (∀ x75 x76 x77 . x74 x77 ⟶ x6 x75 (x8 (x7 x77 x76)) ⟶ (x74 x75 ⟶ False) ⟶ False) ⟶ (∀ x75 x76 x77 . (x74 x77 ⟶ False) ⟶ x6 x75 (x8 (x7 x76 x77)) ⟶ x14 x75 x76 x77 ⟶ (x49 x75 x76 ⟶ False) ⟶ False) ⟶ (∀ x75 . x24 x75 ⟶ (x30 x75 ⟶ False) ⟶ x1 x75 ⟶ False) ⟶ (∀ x75 x76 x77 . x6 x77 (x8 (x7 x75 x76)) ⟶ (x34 x77 x76 ⟶ False) ⟶ False) ⟶ (∀ x75 x76 x77 . x6 x77 (x8 (x7 x76 x75)) ⟶ (x66 x77 x76 ⟶ False) ⟶ False) ⟶ (∀ x75 x76 x77 . x74 x77 ⟶ x6 x75 (x8 (x7 x77 x76)) ⟶ x14 x75 x77 x76 ⟶ (x49 x75 x77 ⟶ False) ⟶ False) ⟶ (∀ x75 . x16 x75 ⟶ (x1 x75 ⟶ False) ⟶ (x19 x75 ⟶ False) ⟶ x28 x75 ⟶ (x4 x75 ⟶ False) ⟶ False) ⟶ (∀ x75 . x16 x75 ⟶ (x1 x75 ⟶ False) ⟶ (x19 x75 ⟶ False) ⟶ x28 x75 ⟶ (x3 x75 ⟶ False) ⟶ False) ⟶ (∀ x75 . x16 x75 ⟶ (x1 x75 ⟶ False) ⟶ (x19 x75 ⟶ False) ⟶ x28 x75 ⟶ x19 x75 ⟶ False) ⟶ (∀ x75 . x16 x75 ⟶ (x1 x75 ⟶ False) ⟶ (x19 x75 ⟶ False) ⟶ x28 x75 ⟶ x1 x75 ⟶ False) ⟶ (∀ x75 . x24 x75 ⟶ x1 x75 ⟶ (x30 x75 ⟶ False) ⟶ False) ⟶ (∀ x75 x76 x77 . x6 x77 (x8 (x7 x75 x76)) ⟶ (x36 x77 ⟶ False) ⟶ False) ⟶ (∀ x75 x76 x77 . x6 x76 (x8 (x7 x77 x75)) ⟶ x49 x76 x77 ⟶ (x14 x76 x77 x75 ⟶ False) ⟶ False) ⟶ (∀ x75 . x16 x75 ⟶ (x1 x75 ⟶ False) ⟶ x30 x75 ⟶ (x19 x75 ⟶ False) ⟶ (x17 x75 ⟶ False) ⟶ False) ⟶ (∀ x75 . x16 x75 ⟶ (x1 x75 ⟶ False) ⟶ x30 x75 ⟶ (x19 x75 ⟶ False) ⟶ (x18 x75 ⟶ False) ⟶ False) ⟶ (∀ x75 . x16 x75 ⟶ (x1 x75 ⟶ False) ⟶ x30 x75 ⟶ (x19 x75 ⟶ False) ⟶ x19 x75 ⟶ False) ⟶ (∀ x75 . x16 x75 ⟶ (x1 x75 ⟶ False) ⟶ x30 x75 ⟶ (x19 x75 ⟶ False) ⟶ x1 x75 ⟶ False) ⟶ (∀ x75 . x24 x75 ⟶ (x30 x75 ⟶ False) ⟶ x1 x75 ⟶ False) ⟶ (∀ x75 . x68 x75 ⟶ x19 x75 ⟶ (x28 x75 ⟶ False) ⟶ False) ⟶ (∀ x75 . x68 x75 ⟶ (x19 x75 ⟶ False) ⟶ x26 x75 ⟶ x1 x75 ⟶ False) ⟶ (∀ x75 . x68 x75 ⟶ x1 x75 ⟶ x26 x75 ⟶ (x19 x75 ⟶ False) ⟶ False) ⟶ (∀ x75 . x68 x75 ⟶ x19 x75 ⟶ (x26 x75 ⟶ False) ⟶ False) ⟶ (∀ x75 . x68 x75 ⟶ (x1 x75 ⟶ False) ⟶ (x26 x75 ⟶ False) ⟶ False) ⟶ (∀ x75 . x24 x75 ⟶ x50 x75 x21 ⟶ (x30 x75 ⟶ False) ⟶ False) ⟶ (∀ x75 . x24 x75 ⟶ x50 x75 x21 ⟶ x1 x75 ⟶ False) ⟶ (∀ x75 . x24 x75 ⟶ (x1 x75 ⟶ False) ⟶ x30 x75 ⟶ (x50 x75 x21 ⟶ False) ⟶ False) ⟶ (∀ x75 x76 . x0 x75 x76 ⟶ x0 x76 x75 ⟶ False) ⟶ (∀ x75 . x16 x75 ⟶ x70 x75 ⟶ (x75 = x37 (x13 x75) (x15 x75) (x43 x75) (x53 x75) (x52 x75) ⟶ False) ⟶ False) ⟶ (x11 (x13 (x60 x48)) (x13 x45) (x12 (x60 x48) x45 (x62 x48 x45 x46)) x47 = x11 (x13 x48) (x13 x45) (x12 x48 x45 x46) (x61 x48 x47) ⟶ False) ⟶ ((x6 x47 (x13 (x60 x48)) ⟶ False) ⟶ False) ⟶ ((x63 x46 x48 x45 ⟶ False) ⟶ False) ⟶ ((x16 x45 ⟶ False) ⟶ False) ⟶ ((x4 x45 ⟶ False) ⟶ False) ⟶ ((x17 x45 ⟶ False) ⟶ False) ⟶ ((x3 x45 ⟶ False) ⟶ False) ⟶ ((x18 x45 ⟶ False) ⟶ False) ⟶ ((x2 x45 ⟶ False) ⟶ False) ⟶ (x19 x45 ⟶ False) ⟶ (x1 x45 ⟶ False) ⟶ ((x16 x48 ⟶ False) ⟶ False) ⟶ ((x4 x48 ⟶ False) ⟶ False) ⟶ ((x17 x48 ⟶ False) ⟶ False) ⟶ ((x3 x48 ⟶ False) ⟶ False) ⟶ ((x18 x48 ⟶ False) ⟶ False) ⟶ ((x2 x48 ⟶ False) ⟶ False) ⟶ (x19 x48 ⟶ False) ⟶ (x1 x48 ⟶ False) ⟶ False

type
prop

theory
HotG

name
-

proof
PUTAm..

Megalodon
-

proofgold address
TMLeX..

creator
35134 PrPhD../48b55..

owner
35137 PrPhD../ef36a..

term root
e3930..