Search for blocks/addresses/...

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 : ι → ι . ∀ x77 . ∀ x78 : ι → ι → ο . ∀ x79 : ι → ο . (∀ x80 x81 . x79 x81(x81 = x80False)x79 x80False)(∀ x80 x81 x82 x83 . x0 x83x0 x80x0 x82x0 x81(x2 (x2 x83 x80) (x2 x82 x81) = x2 (x1 x83 x81) (x1 x80 x82)False)False)(∀ x80 x81 . x78 x80 x81x79 x81False)(∀ x80 x81 x82 x83 . x0 x83x0 x80x0 x82x0 x81(x1 (x2 x83 x80) (x2 x82 x81) = x2 (x1 x83 x82) (x1 x80 x81)False)False)(∀ x80 . x79 x80(x80 = x77False)False)(∀ x80 . x0 x80(x2 x80 x3 = x80False)False)(∀ x80 x81 x82 . x78 x80 x81x75 x81 (x76 x82)x79 x82False)(∀ x80 x81 x82 . x78 x81 x82x75 x82 (x76 x80)(x75 x81 x80False)False)(∀ x80 x81 . x74 x81 x80(x75 x81 (x76 x80)False)False)(∀ x80 x81 . x75 x81 (x76 x80)(x74 x81 x80False)False)(∀ x80 . x0 x80(x1 x3 x80 = x80False)False)(∀ x80 x81 . x75 x80 x81(x79 x81False)(x78 x80 x81False)False)(∀ x80 x81 . x78 x81 x80(x75 x81 x80False)False)((x75 x77 x4False)False)(∀ x80 x81 . x0 x81x0 x80(x72 (x73 x81) (x73 x80) = x72 x80 x81False)False)(∀ x80 x81 . x0 x81x0 x80(x5 (x73 x81) (x73 x80) = x73 (x5 x81 x80)False)False)(∀ x80 x81 x82 . x0 x82x0 x80x0 x81(x1 (x1 x82 x80) x81 = x1 x82 (x1 x80 x81)False)False)(∀ x80 x81 x82 . x0 x82x0 x80x0 x81(x5 (x5 x82 x80) x81 = x5 x82 (x5 x80 x81)False)False)(∀ x80 x81 x82 . x0 x82x0 x80x0 x81(x1 (x5 x82 x80) x81 = x5 (x1 x82 x81) (x1 x80 x81)False)False)(∀ x80 x81 x82 . x0 x82x0 x80x0 x81(x1 x82 (x2 x80 x81) = x2 (x1 x82 x80) x81False)False)(∀ x80 . x0 x80(x2 x3 x80 = x71 x80False)False)(∀ x80 . x0 x80(x1 x80 (x73 x3) = x73 x80False)False)((x75 x3 x70False)False)((x75 x3 x6False)False)((x69 x3 x70 x6False)False)((x7 x3False)False)(x79 x3False)(∀ x80 x81 . x0 x81x0 x80(x5 x81 (x73 x80) = x72 x81 x80False)False)(∀ x80 x81 . x0 x81x0 x80(x1 x81 (x71 x80) = x2 x81 x80False)False)(∀ x80 x81 . x0 x81x0 x80(x2 (x71 x81) (x71 x80) = x2 x80 x81False)False)(∀ x80 x81 . x0 x81x0 x80(x1 (x71 x81) (x71 x80) = x71 (x1 x81 x80)False)False)((x75 x8 x70False)False)((x75 x8 x6False)False)((x69 x8 x70 x6False)False)((x79 x8False)False)((x73 (x73 x3) = x3False)False)((x73 x3 = x73 x3False)False)((x73 x8 = x8False)False)((x1 x3 x3 = x3False)False)((x1 x3 x8 = x8False)False)((x1 x8 x3 = x8False)False)((x1 x8 x8 = x8False)False)((x2 (x73 x3) x3 = x73 x3False)False)((x2 x3 (x73 x3) = x73 x3False)False)((x2 x3 x3 = x3False)False)((x72 (x73 x3) (x73 x3) = x8False)False)((x72 (x73 x3) x8 = x73 x3False)False)((x72 x3 x3 = x8False)False)((x72 x3 x8 = x3False)False)((x72 x8 (x73 x3) = x3False)False)((x72 x8 x3 = x73 x3False)False)((x72 x8 x8 = x8False)False)((x5 (x73 x3) x3 = x8False)False)((x5 (x73 x3) x8 = x73 x3False)False)((x5 x3 (x73 x3) = x8False)False)((x5 x3 x8 = x3False)False)((x5 x8 (x73 x3) = x73 x3False)False)((x5 x8 x3 = x3False)False)((x5 x8 x8 = x8False)False)(∀ x80 . (x74 x80 x80False)False)(∀ x80 x81 x82 . (x79 x82False)(x79 x80False)x75 x80 (x76 x82)x75 x81 x80(x69 x81 x82 x80False)False)(∀ x80 x81 x82 . (x79 x82False)(x79 x80False)x75 x80 (x76 x82)x69 x81 x82 x80(x75 x81 x80False)False)(∀ x80 x81 . x75 x81 x70x67 x80(x68 x81 x80 = x1 x81 x80False)False)((x6 = x4False)False)(∀ x80 x81 . x75 x81 x70x67 x80(x66 x81 x80 = x2 x81 x80False)False)((x9 x10False)False)(x79 x10False)((x11 x12False)False)(x79 x12False)(x7 x13False)((x65 x13False)False)((x67 x13False)False)((x0 x13False)False)((x75 x13 x70False)False)((x65 x64False)False)((x79 x64False)False)((x67 x63False)False)((x65 x63False)False)((x0 x63False)False)((x79 x63False)False)(∀ x80 . (x79 x80False)(x61 (x62 x80) x80False)False)(∀ x80 . (x79 x80False)(x75 (x62 x80) (x76 x80)False)False)((x11 x60False)False)(x14 x15False)((x65 x15False)False)((x67 x15False)False)((x0 x15False)False)((x75 x15 x70False)False)((x14 x59False)False)((x65 x59False)False)((x67 x58False)False)((x14 x58False)False)((x65 x58False)False)((x0 x58False)False)(∀ x80 . x61 (x57 x80) x80False)(∀ x80 . (x75 (x57 x80) (x76 x80)False)False)((x56 x55False)False)((x16 x55False)False)(x79 x55False)((x7 x17False)False)((x65 x17False)False)((x67 x18False)False)((x7 x18False)False)((x65 x18False)False)((x0 x18False)False)(x79 x19False)(∀ x80 . (x79 (x54 x80)False)False)(∀ x80 . (x75 (x54 x80) (x76 x80)False)False)((x53 x52False)False)((x20 x52False)False)((x51 x52False)False)(x79 x52False)((x53 x50False)False)(x79 x50False)((x75 x50 (x76 x70)False)False)((x16 x21False)False)(x79 x21False)((x22 x23False)False)((x14 x49False)False)((x65 x49False)False)((x67 x49False)False)((x0 x49False)False)((x75 x49 x70False)False)((x65 x24False)False)((x67 x48False)False)((x79 x25False)False)(∀ x80 . (x79 x80False)x79 (x47 x80)False)(∀ x80 . (x79 x80False)(x75 (x47 x80) (x76 x80)False)False)((x53 x46False)False)((x16 x26False)False)(x79 x26False)((x22 x27False)False)((x67 x27False)False)((x0 x27False)False)((x65 x27False)False)((x75 x27 x70False)False)((x7 x45False)False)((x65 x45False)False)((x67 x45False)False)((x0 x45False)False)((x75 x45 x70False)False)(∀ x80 . x0 x80(x71 (x71 x80) = x80False)False)(∀ x80 . x0 x80(x73 (x73 x80) = x80False)False)(∀ x80 x81 . (x14 x81False)x67 x81(x14 x80False)x67 x80x14 (x5 x81 x80)False)(∀ x80 x81 . x67 x81x67 x80(x67 (x2 x81 x80)False)False)(x28 x70False)(∀ x80 x81 . x67 x81x67 x80(x67 (x72 x81 x80)False)False)(∀ x80 x81 . x67 x81x67 x80(x67 (x1 x81 x80)False)False)((x53 x4False)False)(x79 x4False)((x16 x4False)False)(∀ x80 x81 . x67 x81x67 x80(x67 (x5 x81 x80)False)False)((x56 x4False)False)((x56 x70False)False)(∀ x80 . x67 x80(x67 (x71 x80)False)False)(∀ x80 . x67 x80(x0 (x71 x80)False)False)(∀ x80 x81 . x11 x81(x79 x80False)x11 x80x79 (x5 x80 x81)False)(∀ x80 x81 . x22 x81x22 x80(x22 (x72 x81 x80)False)False)(∀ x80 . x67 x80(x67 (x73 x80)False)False)(∀ x80 . x67 x80(x0 (x73 x80)False)False)(∀ x80 x81 . x11 x81(x79 x80False)x11 x80x79 (x5 x81 x80)False)((x29 x70False)False)(∀ x80 . x22 x80(x22 (x73 x80)False)False)(∀ x80 . x22 x80(x0 (x73 x80)False)False)(∀ x80 x81 . (x7 x81False)x67 x81(x7 x80False)x67 x80x14 (x2 x81 x80)False)(∀ x80 x81 . (x14 x81False)x67 x81(x14 x80False)x67 x80x14 (x2 x81 x80)False)(∀ x80 x81 . (x14 x81False)x67 x81(x7 x80False)x67 x80x7 (x2 x80 x81)False)(∀ x80 x81 . (x14 x81False)x67 x81(x7 x80False)x67 x80x7 (x2 x81 x80)False)(∀ x80 . (x14 x80False)x67 x80x14 (x71 x80)False)(∀ x80 . (x14 x80False)x67 x80(x0 (x71 x80)False)False)(∀ x80 x81 . x11 x81x11 x80(x11 (x1 x81 x80)False)False)(∀ x80 x81 . x22 x81x22 x80(x22 (x1 x81 x80)False)False)(∀ x80 . x14 x80x67 x80(x14 (x71 x80)False)False)(∀ x80 . x14 x80x67 x80(x0 (x71 x80)False)False)(∀ x80 . (x7 x80False)x67 x80x7 (x71 x80)False)(∀ x80 . (x7 x80False)x67 x80(x0 (x71 x80)False)False)(∀ x80 . x7 x80x67 x80(x7 (x71 x80)False)False)(∀ x80 . x7 x80x67 x80(x0 (x71 x80)False)False)(∀ x80 x81 . (x14 x81False)x67 x81(x14 x80False)x67 x80x14 (x1 x81 x80)False)(∀ x80 x81 . (x7 x81False)x67 x81(x7 x80False)x67 x80x14 (x1 x81 x80)False)(∀ x80 x81 . (x7 x81False)x67 x81(x14 x80False)x67 x80x7 (x1 x80 x81)False)(∀ x80 x81 . (x7 x81False)x67 x81(x14 x80False)x67 x80x7 (x1 x81 x80)False)(∀ x80 x81 . x14 x81x67 x81(x14 x80False)x67 x80(x7 (x72 x80 x81)False)False)(∀ x80 x81 . x14 x81x67 x81(x14 x80False)x67 x80(x14 (x72 x81 x80)False)False)(∀ x80 x81 . x7 x81x67 x81(x7 x80False)x67 x80(x14 (x72 x80 x81)False)False)((x79 x77False)False)(∀ x80 . x79 (x76 x80)False)(x79 x70False)(∀ x80 x81 . x11 x81x11 x80(x11 (x5 x81 x80)False)False)(∀ x80 x81 . x22 x81x22 x80(x22 (x5 x81 x80)False)False)(∀ x80 x81 . x7 x81x67 x81(x7 x80False)x67 x80(x7 (x72 x81 x80)False)False)(∀ x80 x81 . (x14 x81False)x67 x81(x7 x80False)x67 x80x7 (x72 x80 x81)False)(∀ x80 x81 . (x14 x81False)x67 x81(x7 x80False)x67 x80x14 (x72 x81 x80)False)(∀ x80 . (x14 x80False)x67 x80x7 (x73 x80)False)(∀ x80 . (x14 x80False)x67 x80(x0 (x73 x80)False)False)(∀ x80 . (x7 x80False)x67 x80x14 (x73 x80)False)(∀ x80 . (x7 x80False)x67 x80(x0 (x73 x80)False)False)(∀ x80 x81 . x14 x81x67 x81(x7 x80False)x67 x80(x14 (x5 x80 x81)False)False)(∀ x80 x81 . x14 x81x67 x81(x7 x80False)x67 x80(x14 (x5 x81 x80)False)False)(∀ x80 x81 . x7 x81x67 x81(x14 x80False)x67 x80(x7 (x5 x80 x81)False)False)(∀ x80 x81 . x7 x81x67 x81(x14 x80False)x67 x80(x7 (x5 x81 x80)False)False)(∀ x80 x81 . (x7 x81False)x67 x81(x7 x80False)x67 x80x7 (x5 x81 x80)False)(∀ x80 x81 . (x79 x81False)(x79 x80False)x75 x80 (x76 x81)(x69 (x44 x80 x81) x81 x80False)False)(∀ x80 . (x75 (x30 x80) x80False)False)(∀ x80 x81 x82 . (x79 x82False)(x79 x80False)x75 x80 (x76 x82)x69 x81 x82 x80(x75 x81 x82False)False)(∀ x80 x81 . x75 x81 x70x67 x80(x75 (x68 x81 x80) x70False)False)(∀ x80 . x0 x80(x0 (x71 x80)False)False)((x75 x6 (x76 x70)False)False)(∀ x80 . x0 x80(x0 (x73 x80)False)False)(∀ x80 x81 . x75 x81 x70x67 x80(x75 (x66 x81 x80) x70False)False)(∀ x80 x81 . x0 x81x0 x80(x2 x81 x80 = x1 x81 (x71 x80)False)False)(∀ x80 x81 . x0 x81x0 x80(x72 x81 x80 = x5 x81 (x73 x80)False)False)(∀ x80 x81 . x75 x81 x70x67 x80(x68 x81 x80 = x68 x80 x81False)False)(∀ x80 x81 . x0 x81x0 x80(x1 x81 x80 = x1 x80 x81False)False)(∀ x80 x81 . x0 x81x0 x80(x5 x81 x80 = x5 x80 x81False)False)(∀ x80 . x79 x80(x31 x80False)False)(∀ x80 . x9 x80(x43 x80False)False)(∀ x80 . x65 x80(x7 x80False)(x14 x80False)(x65 x80False)False)(∀ x80 . x65 x80(x7 x80False)(x14 x80False)(x79 x80False)False)(∀ x80 . x75 x80 x4(x11 x80False)False)(∀ x80 . x75 x80 (x76 x70)(x29 x80False)False)(∀ x80 . x79 x80(x9 x80False)False)(∀ x80 . x79 x80x65 x80x14 x80False)(∀ x80 . x79 x80x65 x80x7 x80False)(∀ x80 . x79 x80x65 x80(x65 x80False)False)(∀ x80 . x79 x80(x11 x80False)False)(∀ x80 . (x79 x80False)x65 x80(x7 x80False)(x14 x80False)False)(∀ x80 . (x79 x80False)x65 x80(x7 x80False)(x65 x80False)False)(∀ x80 . x11 x80(x53 x80False)False)(∀ x80 . x65 x80x14 x80x7 x80False)(∀ x80 . x65 x80x14 x80(x65 x80False)False)(∀ x80 . x65 x80x14 x80x79 x80False)(∀ x80 x81 . x53 x81x75 x80 x81(x53 x80False)False)(∀ x80 . x29 x80(x32 x80False)False)(∀ x80 . (x79 x80False)x65 x80(x14 x80False)(x7 x80False)False)(∀ x80 . (x79 x80False)x65 x80(x14 x80False)(x65 x80False)False)(∀ x80 . x67 x80(x65 x80False)False)(∀ x80 x81 . x79 x81x75 x80 (x76 x81)x61 x80 x81False)(∀ x80 . x79 x80(x42 x80False)False)(∀ x80 . x29 x80(x33 x80False)False)(∀ x80 . x65 x80x7 x80x14 x80False)(∀ x80 . x65 x80x7 x80(x65 x80False)False)(∀ x80 . x65 x80x7 x80x79 x80False)(∀ x80 . x67 x80(x0 x80False)False)(∀ x80 x81 . (x79 x81False)x75 x80 (x76 x81)x79 x80(x61 x80 x81False)False)(∀ x80 . x79 x80(x53 x80False)False)(∀ x80 . x11 x80x14 x80False)(∀ x80 . x11 x80(x11 x80False)False)(∀ x80 . x41 x80(x29 x80False)False)(∀ x80 . x22 x80(x67 x80False)False)(∀ x80 . x11 x80(x65 x80False)False)(∀ x80 . x11 x80(x67 x80False)False)(∀ x80 x81 . (x79 x81False)x75 x80 (x76 x81)(x61 x80 x81False)x79 x80False)(∀ x80 . x51 x80x20 x80(x53 x80False)False)(∀ x80 . x75 x80 x6x14 x80False)(∀ x80 . x34 x80(x41 x80False)False)(∀ x80 . x11 x80(x22 x80False)False)(∀ x80 . x79 x80(x56 x80False)False)(∀ x80 . x75 x80 x6(x16 x80False)False)(∀ x80 x81 . x16 x81x75 x80 (x76 x81)(x16 x80False)False)(∀ x80 x81 . x34 x81x75 x80 (x76 x81)(x34 x80False)False)(∀ x80 x81 . x41 x81x75 x80 (x76 x81)(x41 x80False)False)(∀ x80 x81 . x29 x81x75 x80 (x76 x81)(x29 x80False)False)(∀ x80 x81 . x33 x81x75 x80 (x76 x81)(x33 x80False)False)(∀ x80 . x75 x80 x70(x67 x80False)False)(∀ x80 x81 . x79 x81x75 x80 (x76 x81)(x79 x80False)False)(∀ x80 . x53 x80(x20 x80False)False)(∀ x80 . x53 x80(x51 x80False)False)(∀ x80 . x11 x80(x11 x80False)False)(∀ x80 . x11 x80(x53 x80False)False)(∀ x80 . x16 x80(x34 x80False)False)(∀ x80 x81 . x32 x81x75 x80 (x76 x81)(x32 x80False)False)(∀ x80 . x79 x80(x16 x80False)False)(∀ x80 x81 . x16 x81x75 x80 x81(x11 x80False)False)(∀ x80 x81 . x34 x81x75 x80 x81(x22 x80False)False)(∀ x80 x81 . x41 x81x75 x80 x81(x35 x80False)False)(∀ x80 x81 . x29 x81x75 x80 x81(x67 x80False)False)(∀ x80 x81 . x33 x81x75 x80 x81(x65 x80False)False)(∀ x80 x81 . x32 x81x75 x80 x81(x0 x80False)False)(∀ x80 . x75 x80 (x76 x6)(x16 x80False)False)(∀ x80 x81 . x9 x81x75 x80 (x76 x81)(x9 x80False)False)(∀ x80 x81 . x31 x81x75 x80 (x76 x81)(x31 x80False)False)(∀ x80 x81 . x9 x81x75 x80 x81(x40 x80False)False)(∀ x80 x81 . x78 x80 x81x78 x81 x80False)(x66 (x66 x38 x37) (x66 x36 x39) = x68 (x66 x38 x36) (x66 x39 x37)False)((x75 x39 x70False)False)((x75 x36 x70False)False)((x75 x37 x70False)False)((x75 x38 x70False)False)False
type
prop
theory
HotG
name
-
proof
PUWUm..
Megalodon
-
proofgold address
TMM3b..
creator
35119 PrPhD../4eb7a..
owner
35120 PrPhD../f9302..
term root
b8b5d..