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

type
prop

theory
HotG

name
-

proof
PUgy5..

Megalodon
-

proofgold address
TMcLZ..

creator
35119 PrPhD../64513..

owner
35120 PrPhD../67cd2..

term root
609ce..