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 . x72 x76x66 x76 x73x71 x76x67 x76 x73x72 x75x66 x75 x73x71 x75x67 x75 x73x72 x74x66 x74 x73x71 x74x67 x74 x73x69 x73 (x70 x73 x76 x75) x74x69 x73 (x70 x73 x75 x76) x74(x69 x73 (x68 x73 x76 x75) x74False)False)(∀ x73 x74 . x0 x74(x74 = x73False)x0 x73False)(∀ x73 x74 . x65 x73 x74x0 x74False)(∀ x73 . x0 x73(x73 = x1False)False)(∀ x73 x74 x75 . x65 x73 x74x63 x74 (x64 x75)x0 x75False)(∀ x73 x74 x75 . x65 x74 x75x63 x75 (x64 x73)(x63 x74 x73False)False)(∀ x73 x74 . x62 x74 x73(x63 x74 (x64 x73)False)False)(∀ x73 x74 . x63 x74 (x64 x73)(x62 x74 x73False)False)(∀ x73 x74 . x63 x73 x74(x0 x74False)(x65 x73 x74False)False)(∀ x73 x74 . x65 x74 x73(x63 x74 x73False)False)(∀ x73 x74 x75 x76 . x72 x76x66 x76 x73x71 x76x67 x76 x73x72 x75x66 x75 x73x71 x75x67 x75 x73x72 x74x66 x74 x73x71 x74x67 x74 x73x69 x73 x76 x75(x69 x73 (x70 x73 x76 x74) x75False)False)(∀ x73 x74 x75 . x72 x75x66 x75 x73x71 x75x67 x75 x73x72 x74x66 x74 x73x71 x74x67 x74 x73(x69 x73 x75 x75False)False)(∀ x73 . (x62 x73 x73False)False)(∀ x73 x74 x75 x76 . x72 x76x66 x76 x73x71 x76x67 x76 x73(x0 x75False)x63 x75 (x64 (x2 x73 x76))x63 x74 x75(x3 x74 x73 x76 x75False)False)(∀ x73 x74 x75 x76 . x72 x76x66 x76 x73x71 x76x67 x76 x73(x0 x75False)x63 x75 (x64 (x2 x73 x76))x3 x74 x73 x76 x75(x63 x74 x75False)False)(∀ x73 x74 . x72 x74x66 x74 x73x71 x74x67 x74 x73(x4 x73 x74 = x2 x73 x74False)False)(∀ x73 . (x71 (x61 x73)False)False)(∀ x73 . (x66 (x61 x73) x73False)False)(∀ x73 . (x60 (x61 x73)False)False)(∀ x73 . (x72 (x61 x73)False)False)((x59 x58False)False)((x71 x58False)False)((x72 x58False)False)(x0 x58False)((x57 x56False)False)((x5 x56False)False)(x0 x56False)((x6 x7False)False)(x0 x7False)(∀ x73 . (x8 x73False)(x5 (x9 x73)False)False)(∀ x73 . (x8 x73False)x8 (x9 x73)False)(∀ x73 . (x8 x73False)(x63 (x9 x73) (x64 x73)False)False)(∀ x73 . (x8 x73False)x8 (x55 x73)False)(∀ x73 . (x8 x73False)(x63 (x55 x73) (x64 x73)False)False)(∀ x73 . (x0 x73False)(x8 (x54 x73)False)False)(∀ x73 . (x0 x73False)x0 (x54 x73)False)(∀ x73 . (x0 x73False)(x63 (x54 x73) (x64 x73)False)False)(∀ x73 x74 . x72 x74x60 x74x66 x74 x73x71 x74x67 x74 x73(x67 (x10 x74 x73) x73False)False)(∀ x73 x74 . x72 x74x60 x74x66 x74 x73x71 x74x67 x74 x73(x71 (x10 x74 x73)False)False)(∀ x73 x74 . x72 x74x60 x74x66 x74 x73x71 x74x67 x74 x73(x66 (x10 x74 x73) x73False)False)(∀ x73 x74 . x72 x74x60 x74x66 x74 x73x71 x74x67 x74 x73(x60 (x10 x74 x73)False)False)(∀ x73 x74 . x72 x74x60 x74x66 x74 x73x71 x74x67 x74 x73(x72 (x10 x74 x73)False)False)(∀ x73 x74 . x72 x74x60 x74x66 x74 x73x71 x74x67 x74 x73(x53 (x10 x74 x73) x73 x74False)False)(x11 x12False)((x71 x12False)False)((x72 x12False)False)(∀ x73 . (x0 x73False)(x51 (x52 x73) x73False)False)(∀ x73 . (x0 x73False)(x63 (x52 x73) (x64 x73)False)False)(∀ x73 . (x50 (x49 x73)False)False)(∀ x73 . (x67 (x49 x73) x73False)False)(∀ x73 . (x71 (x49 x73)False)False)(∀ x73 . (x66 (x49 x73) x73False)False)(∀ x73 . (x72 (x49 x73)False)False)((x71 x13False)False)((x60 x13False)False)((x72 x13False)False)(x0 x13False)(∀ x73 . (x67 (x14 x73) x73False)False)(∀ x73 . (x71 (x14 x73)False)False)(∀ x73 . (x66 (x14 x73) x73False)False)(∀ x73 . (x60 (x14 x73)False)False)(∀ x73 . (x72 (x14 x73)False)False)(∀ x73 . x51 (x48 x73) x73False)(∀ x73 . (x63 (x48 x73) (x64 x73)False)False)(∀ x73 . (x67 (x47 x73) x73False)False)(∀ x73 . (x71 (x47 x73)False)False)(∀ x73 . (x66 (x47 x73) x73False)False)(∀ x73 . (x60 (x47 x73)False)False)(∀ x73 . (x72 (x47 x73)False)False)((x71 x15False)False)((x60 x15False)False)((x72 x15False)False)((x5 x46False)False)((x71 x46False)False)((x72 x46False)False)(x0 x46False)(x0 x45False)(∀ x73 . (x0 (x16 x73)False)False)(∀ x73 . (x63 (x16 x73) (x64 x73)False)False)((x60 x17False)False)((x72 x17False)False)(∀ x73 . (x67 (x18 x73) x73False)False)(∀ x73 . (x71 (x18 x73)False)False)(∀ x73 . (x66 (x18 x73) x73False)False)(∀ x73 . (x44 (x18 x73)False)False)(∀ x73 . (x72 (x18 x73)False)False)((x43 x42False)False)((x71 x42False)False)((x72 x42False)False)(x0 x19False)((x11 x19False)False)((x71 x19False)False)((x72 x19False)False)(∀ x73 . (x0 x73False)(x5 (x20 x73)False)False)(∀ x73 . (x0 x73False)x0 (x20 x73)False)(∀ x73 . (x0 x73False)(x63 (x20 x73) (x64 x73)False)False)(∀ x73 x74 . x72 x74x66 x74 x73x71 x74x67 x74 x73(x5 (x41 x74 x73)False)False)(∀ x73 x74 . x72 x74x66 x74 x73x71 x74x67 x74 x73(x6 (x41 x74 x73)False)False)(∀ x73 x74 . x72 x74x66 x74 x73x71 x74x67 x74 x73(x0 (x41 x74 x73)False)False)(∀ x73 x74 . x72 x74x66 x74 x73x71 x74x67 x74 x73(x63 (x41 x74 x73) (x64 (x2 x73 x74))False)False)((x0 x40False)False)(∀ x73 . (x0 x73False)x0 (x21 x73)False)(∀ x73 . (x0 x73False)(x63 (x21 x73) (x64 x73)False)False)((x72 x22False)False)(x0 x22False)(∀ x73 . (x67 (x23 x73) x73False)False)(∀ x73 . (x71 (x23 x73)False)False)(∀ x73 . (x66 (x23 x73) x73False)False)(∀ x73 . (x72 (x23 x73)False)False)((x71 x24False)False)((x72 x24False)False)((x50 x25False)False)((x71 x25False)False)((x72 x25False)False)((x5 x39False)False)(x0 x39False)(∀ x73 x74 . x72 x74x66 x74 x73x71 x74x67 x74 x73(x38 (x37 x74 x73)False)False)(∀ x73 x74 . x72 x74x66 x74 x73x71 x74x67 x74 x73(x6 (x37 x74 x73)False)False)(∀ x73 x74 . x72 x74x66 x74 x73x71 x74x67 x74 x73x0 (x37 x74 x73)False)(∀ x73 x74 . x72 x74x66 x74 x73x71 x74x67 x74 x73(x63 (x37 x74 x73) (x64 (x2 x73 x74))False)False)(∀ x73 x74 x75 . x72 x75x66 x75 x73x71 x75x67 x75 x73x72 x74x66 x74 x73x71 x74x67 x74 x73(x36 x73 x75 x75 = x75False)False)(∀ x73 . x5 x73(x57 (x64 x73)False)False)((x0 x1False)False)(∀ x73 . x0 (x64 x73)False)(∀ x73 x74 . x72 x74x66 x74 x73x71 x74x67 x74 x73(x38 (x2 x73 x74)False)False)(∀ x73 x74 . x72 x74x66 x74 x73x71 x74x67 x74 x73(x6 (x2 x73 x74)False)False)(∀ x73 x74 . x72 x74x66 x74 x73x71 x74x67 x74 x73x0 (x2 x73 x74)False)(∀ x73 . x5 x73(x5 (x64 x73)False)False)(∀ x73 x74 . x72 x74x66 x74 x73x71 x74x67 x74 x73(x53 (x35 x74 x73) x73 x74False)False)(∀ x73 . (x63 (x26 x73) x73False)False)(∀ x73 x74 x75 . x72 x75x66 x75 x73x71 x75x67 x75 x73(x0 x74False)x63 x74 (x64 (x2 x73 x75))(x3 (x34 x74 x75 x73) x73 x75 x74False)False)((x0 x27False)False)(∀ x73 x74 x75 . x72 x75x66 x75 x73x71 x75x67 x75 x73x53 x74 x73 x75(x67 x74 x73False)False)(∀ x73 x74 x75 . x72 x75x66 x75 x73x71 x75x67 x75 x73x53 x74 x73 x75(x71 x74False)False)(∀ x73 x74 x75 . x72 x75x66 x75 x73x71 x75x67 x75 x73x53 x74 x73 x75(x66 x74 x73False)False)(∀ x73 x74 x75 . x72 x75x66 x75 x73x71 x75x67 x75 x73x53 x74 x73 x75(x72 x74False)False)(∀ x73 x74 x75 x76 . x72 x76x66 x76 x73x71 x76x67 x76 x73(x0 x75False)x63 x75 (x64 (x2 x73 x76))x3 x74 x73 x76 x75(x53 x74 x73 x76False)False)(∀ x73 x74 x75 . x72 x75x66 x75 x73x71 x75x67 x75 x73x72 x74x66 x74 x73x71 x74x67 x74 x73(x67 (x68 x73 x75 x74) x73False)False)(∀ x73 x74 x75 . x72 x75x66 x75 x73x71 x75x67 x75 x73x72 x74x66 x74 x73x71 x74x67 x74 x73(x71 (x68 x73 x75 x74)False)False)(∀ x73 x74 x75 . x72 x75x66 x75 x73x71 x75x67 x75 x73x72 x74x66 x74 x73x71 x74x67 x74 x73(x66 (x68 x73 x75 x74) x73False)False)(∀ x73 x74 x75 . x72 x75x66 x75 x73x71 x75x67 x75 x73x72 x74x66 x74 x73x71 x74x67 x74 x73(x72 (x68 x73 x75 x74)False)False)(∀ x73 x74 x75 . x72 x75x66 x75 x73x71 x75x67 x75 x73x72 x74x66 x74 x73x71 x74x67 x74 x73(x67 (x70 x73 x75 x74) x73False)False)(∀ x73 x74 x75 . x72 x75x66 x75 x73x71 x75x67 x75 x73x72 x74x66 x74 x73x71 x74x67 x74 x73(x71 (x70 x73 x75 x74)False)False)(∀ x73 x74 x75 . x72 x75x66 x75 x73x71 x75x67 x75 x73x72 x74x66 x74 x73x71 x74x67 x74 x73(x66 (x70 x73 x75 x74) x73False)False)(∀ x73 x74 x75 . x72 x75x66 x75 x73x71 x75x67 x75 x73x72 x74x66 x74 x73x71 x74x67 x74 x73(x72 (x70 x73 x75 x74)False)False)(∀ x73 x74 x75 . x72 x75x66 x75 x73x71 x75x67 x75 x73x72 x74x66 x74 x73x71 x74x67 x74 x73(x67 (x36 x73 x75 x74) x73False)False)(∀ x73 x74 x75 . x72 x75x66 x75 x73x71 x75x67 x75 x73x72 x74x66 x74 x73x71 x74x67 x74 x73(x71 (x36 x73 x75 x74)False)False)(∀ x73 x74 x75 . x72 x75x66 x75 x73x71 x75x67 x75 x73x72 x74x66 x74 x73x71 x74x67 x74 x73(x66 (x36 x73 x75 x74) x73False)False)(∀ x73 x74 x75 . x72 x75x66 x75 x73x71 x75x67 x75 x73x72 x74x66 x74 x73x71 x74x67 x74 x73(x72 (x36 x73 x75 x74)False)False)(∀ x73 x74 . x72 x74x66 x74 x73x71 x74x67 x74 x73(x63 (x4 x73 x74) (x64 (x2 x73 x74))False)False)(∀ x73 x74 x75 . x72 x75x66 x75 x73x71 x75x67 x75 x73x72 x74x66 x74 x73x71 x74x67 x74 x73(x68 x73 x75 x74 = x36 x73 (x70 x73 x75 x74) (x70 x73 x74 x75)False)False)((x1 = x27False)False)(∀ x73 x74 x75 . x72 x75x66 x75 x73x71 x75x67 x75 x73(x53 (x33 x74 x75 x73) x73 x75False)(x65 (x33 x74 x75 x73) x74False)(x74 = x2 x73 x75False)False)(∀ x73 x74 x75 . x72 x75x66 x75 x73x71 x75x67 x75 x73x65 (x33 x74 x75 x73) x74x53 (x33 x74 x75 x73) x73 x75(x74 = x2 x73 x75False)False)(∀ x73 x74 x75 x76 . x72 x76x66 x76 x73x71 x76x67 x76 x73x75 = x2 x73 x76x53 x74 x73 x76(x65 x74 x75False)False)(∀ x73 x74 x75 x76 . x72 x76x66 x76 x73x71 x76x67 x76 x73x75 = x2 x73 x76x65 x74 x75(x53 x74 x73 x76False)False)(∀ x73 x74 x75 . x72 x75x66 x75 x73x71 x75x67 x75 x73x72 x74x66 x74 x73x71 x74x67 x74 x73x69 x73 x74 x75(x53 x74 x73 x75False)False)(∀ x73 x74 x75 . x72 x75x66 x75 x73x71 x75x67 x75 x73x72 x74x66 x74 x73x71 x74x67 x74 x73x53 x74 x73 x75(x69 x73 x74 x75False)False)(∀ x73 x74 x75 . x72 x75x66 x75 x73x71 x75x67 x75 x73x72 x74x66 x74 x73x71 x74x67 x74 x73(x68 x73 x75 x74 = x68 x73 x74 x75False)False)(∀ x73 x74 x75 . x72 x75x66 x75 x73x71 x75x67 x75 x73x72 x74x66 x74 x73x71 x74x67 x74 x73(x36 x73 x75 x74 = x36 x73 x74 x75False)False)(∀ x73 x74 . x6 x74x63 x73 (x64 x74)(x6 x73False)False)(∀ x73 . x0 x73x72 x73(x59 x73False)False)(∀ x73 . x0 x73x72 x73(x72 x73False)False)(∀ x73 x74 . x6 x74x63 x73 x74(x71 x73False)False)(∀ x73 x74 . x6 x74x63 x73 x74(x72 x73False)False)(∀ x73 x74 . x57 x74x63 x73 (x64 x74)(x57 x73False)False)(∀ x73 x74 . x0 x74x72 x73x66 x73 x74(x66 x73 x74False)False)(∀ x73 x74 . x0 x74x72 x73x66 x73 x74(x72 x73False)False)(∀ x73 x74 . x0 x74x72 x73x66 x73 x74(x0 x73False)False)(∀ x73 . x0 x73(x6 x73False)False)(∀ x73 x74 . x57 x74x63 x73 x74(x5 x73False)False)(∀ x73 . x8 x73x72 x73x71 x73(x11 x73False)False)(∀ x73 . x8 x73x72 x73x71 x73(x71 x73False)False)(∀ x73 . x8 x73x72 x73x71 x73(x72 x73False)False)(∀ x73 . x0 x73(x57 x73False)False)(∀ x73 x74 . x8 x74x63 x73 (x64 x74)(x8 x73False)False)(∀ x73 x74 x75 . x72 x75x66 x75 x73x63 x74 (x64 x75)(x66 x74 x73False)False)(∀ x73 x74 . (x0 x74False)x72 x73x66 x73 x74x71 x73x67 x73 x74(x67 x73 x74False)False)(∀ x73 x74 . (x0 x74False)x72 x73x66 x73 x74x71 x73x67 x73 x74(x71 x73False)False)(∀ x73 x74 . (x0 x74False)x72 x73x66 x73 x74x71 x73x67 x73 x74(x66 x73 x74False)False)(∀ x73 x74 . (x0 x74False)x72 x73x66 x73 x74x71 x73x67 x73 x74(x72 x73False)False)(∀ x73 x74 . (x0 x74False)x72 x73x66 x73 x74x71 x73x67 x73 x74x0 x73False)(∀ x73 . x72 x73x71 x73(x11 x73False)(x71 x73False)False)(∀ x73 . x72 x73x71 x73(x11 x73False)(x72 x73False)False)(∀ x73 . x72 x73x71 x73(x11 x73False)x8 x73False)(∀ x73 . (x5 x73False)x8 x73False)(∀ x73 x74 . x0 x74x63 x73 (x64 x74)x51 x73 x74False)(∀ x73 . x0 x73x72 x73(x60 x73False)False)(∀ x73 . x0 x73x72 x73(x72 x73False)False)(∀ x73 x74 . (x0 x74False)x72 x73x60 x73x66 x73 x74x71 x73x67 x73 x74(x67 x73 x74False)False)(∀ x73 x74 . (x0 x74False)x72 x73x60 x73x66 x73 x74x71 x73x67 x73 x74(x71 x73False)False)(∀ x73 x74 . (x0 x74False)x72 x73x60 x73x66 x73 x74x71 x73x67 x73 x74(x66 x73 x74False)False)(∀ x73 x74 . (x0 x74False)x72 x73x60 x73x66 x73 x74x71 x73x67 x73 x74x44 x73False)(∀ x73 x74 . (x0 x74False)x72 x73x60 x73x66 x73 x74x71 x73x67 x73 x74(x72 x73False)False)(∀ x73 . x0 x73x72 x73x71 x73(x11 x73False)False)(∀ x73 . x0 x73x72 x73x71 x73(x71 x73False)False)(∀ x73 . x0 x73x72 x73x71 x73(x72 x73False)False)(∀ x73 . x8 x73(x5 x73False)False)(∀ x73 x74 . (x0 x74False)x63 x73 (x64 x74)x0 x73(x51 x73 x74False)False)(∀ x73 . x0 x73x72 x73(x44 x73False)False)(∀ x73 . x0 x73x72 x73(x72 x73False)False)(∀ x73 x74 . x72 x74x71 x74x63 x73 (x64 x74)(x71 x73False)False)(∀ x73 . x72 x73x71 x73x0 x73(x50 x73False)False)(∀ x73 . x72 x73x71 x73x0 x73(x71 x73False)False)(∀ x73 . x72 x73x71 x73x0 x73(x72 x73False)False)(∀ x73 x74 . (x0 x74False)x63 x73 (x64 x74)(x51 x73 x74False)x0 x73False)(∀ x73 x74 . x72 x74x63 x73 (x64 x74)(x72 x73False)False)(∀ x73 x74 . (x0 x74False)x72 x73x44 x73x66 x73 x74x71 x73x67 x73 x74(x67 x73 x74False)False)(∀ x73 x74 . (x0 x74False)x72 x73x44 x73x66 x73 x74x71 x73x67 x73 x74(x71 x73False)False)(∀ x73 x74 . (x0 x74False)x72 x73x44 x73x66 x73 x74x71 x73x67 x73 x74(x66 x73 x74False)False)(∀ x73 x74 . (x0 x74False)x72 x73x44 x73x66 x73 x74x71 x73x67 x73 x74x60 x73False)(∀ x73 x74 . (x0 x74False)x72 x73x44 x73x66 x73 x74x71 x73x67 x73 x74(x72 x73False)False)(∀ x73 . x0 x73x72 x73x71 x73(x43 x73False)False)(∀ x73 . x0 x73x72 x73x71 x73(x71 x73False)False)(∀ x73 . x0 x73x72 x73x71 x73(x72 x73False)False)(∀ x73 . x72 x73x71 x73x50 x73(x28 x73False)False)(∀ x73 . x72 x73x71 x73x50 x73(x71 x73False)False)(∀ x73 . x72 x73x71 x73x50 x73(x72 x73False)False)(∀ x73 x74 . x5 x74x63 x73 (x64 x74)(x5 x73False)False)(∀ x73 x74 . x0 x74x63 x73 (x64 x74)(x0 x73False)False)(∀ x73 . x0 x73(x72 x73False)False)(∀ x73 x74 . (x0 x74False)x72 x73x60 x73x66 x73 x74x71 x73x67 x73 x74(x67 x73 x74False)False)(∀ x73 x74 . (x0 x74False)x72 x73x60 x73x66 x73 x74x71 x73x67 x73 x74(x71 x73False)False)(∀ x73 x74 . (x0 x74False)x72 x73x60 x73x66 x73 x74x71 x73x67 x73 x74(x66 x73 x74False)False)(∀ x73 x74 . (x0 x74False)x72 x73x60 x73x66 x73 x74x71 x73x67 x73 x74x44 x73False)(∀ x73 x74 . (x0 x74False)x72 x73x60 x73x66 x73 x74x71 x73x67 x73 x74(x72 x73False)False)(∀ x73 . x0 x73(x71 x73False)False)(∀ x73 . x0 x73(x5 x73False)False)(∀ x73 x74 . x65 x73 x74x65 x74 x73False)(x65 (x68 x30 x31 x32) (x4 x30 x29)False)((x3 x32 x30 x29 (x4 x30 x29)False)False)((x3 x31 x30 x29 (x4 x30 x29)False)False)((x67 x29 x30False)False)((x71 x29False)False)((x66 x29 x30False)False)((x72 x29False)False)False
type
prop
theory
HotG
name
-
proof
PUP4k..
Megalodon
-
proofgold address
TMXrS..
creator
35125 PrPhD../2bbde..
owner
35131 PrPhD../f7ebf..
term root
86250..