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 . x72 x74(x74 = x73False)x72 x73False)(∀ x73 x74 . x0 x73 x74x72 x74False)(∀ x73 . x72 x73(x73 = x71False)False)(∀ x73 x74 x75 . x0 x73 x74x2 x74 (x1 x75)x72 x75False)(∀ x73 x74 x75 . x0 x74 x75x2 x75 (x1 x73)(x2 x74 x73False)False)(∀ x73 . (x5 (x4 x73) (x3 x73)False)False)(∀ x73 x74 . x70 x74 x73(x2 x74 (x1 x73)False)False)(∀ x73 x74 . x2 x74 (x1 x73)(x70 x74 x73False)False)(∀ x73 . (x69 (x4 x73) (x3 x73)False)False)(∀ x73 . (x6 (x4 x73) (x3 x73)False)False)(∀ x73 . (x68 (x4 x73) (x3 x73)False)False)(∀ x73 x74 x75 x76 x77 x78 . (x72 x78False)(x72 x73False)x7 x77x13 x77 (x14 x78 x78) x78x2 x77 (x1 (x14 (x14 x78 x78) x78))x2 x74 (x3 x73)x7 x76x13 x76 x73 x78x2 x76 (x1 (x14 x73 x78))x68 x77 x78x6 x77 x78x69 x77 x78x5 x77 x78x2 x75 x73(x11 x73 x78 x77 (x8 x73 x74 (x9 x73 x75)) x76 = x10 x78 x77 (x11 x73 x78 x77 x74 x76) (x12 x73 x78 x76 x75)False)False)(∀ x73 x74 . x2 x73 x74(x72 x74False)(x0 x73 x74False)False)(∀ x73 x74 . x0 x74 x73(x2 x74 x73False)False)(∀ x73 . (x67 x73 x71 = x73False)False)(∀ x73 . (x70 x73 x73False)False)(∀ x73 x74 x75 . x2 x74 (x3 x75)x2 x73 (x3 x75)(x8 x75 x74 x73 = x67 x74 x73False)False)(∀ x73 x74 x75 x76 . x7 x76x13 x76 (x14 x73 x73) x73x2 x76 (x1 (x14 (x14 x73 x73) x73))x2 x74 x73x2 x75 x73(x10 x73 x76 x74 x75 = x15 x76 x74 x75False)False)(∀ x73 x74 x75 x76 . (x72 x76False)x7 x73x13 x73 x76 x75x2 x73 (x1 (x14 x76 x75))x2 x74 x76(x12 x76 x75 x73 x74 = x66 x73 x74False)False)(∀ x73 x74 . (x72 x74False)x2 x73 x74(x9 x74 x73 = x16 x73False)False)(∀ x73 x74 x75 . x7 x75x13 x75 (x14 x73 x73) x73x68 x75 x73x2 x75 (x1 (x14 (x14 x73 x73) x73))x2 x74 x73(x10 x73 x75 x74 x74 = x74False)False)((x17 x18False)False)((x7 x18False)False)((x19 x18False)False)(x72 x18False)((x20 x21False)False)((x65 x21False)False)(x72 x21False)(∀ x73 . (x64 x73False)(x65 (x63 x73)False)False)(∀ x73 . (x64 x73False)x64 (x63 x73)False)(∀ x73 . (x64 x73False)(x2 (x63 x73) (x1 x73)False)False)(∀ x73 . (x64 x73False)x64 (x22 x73)False)(∀ x73 . (x64 x73False)(x2 (x22 x73) (x1 x73)False)False)(∀ x73 x74 . (x72 x74False)(x72 x73False)(x65 (x23 x73 x74)False)False)(∀ x73 x74 . (x72 x74False)(x72 x73False)(x7 (x23 x73 x74)False)False)(∀ x73 x74 . (x72 x74False)(x72 x73False)(x24 (x23 x73 x74) x73False)False)(∀ x73 x74 . (x72 x74False)(x72 x73False)(x62 (x23 x73 x74) x74False)False)(∀ x73 x74 . (x72 x74False)(x72 x73False)(x19 (x23 x73 x74)False)False)(∀ x73 x74 . (x72 x74False)(x72 x73False)x72 (x23 x73 x74)False)(∀ x73 . (x72 x73False)(x64 (x25 x73)False)False)(∀ x73 . (x72 x73False)x72 (x25 x73)False)(∀ x73 . (x72 x73False)(x2 (x25 x73) (x1 x73)False)False)(∀ x73 x74 . (x65 (x61 x73 x74)False)False)(∀ x73 x74 . (x7 (x61 x73 x74)False)False)(∀ x73 x74 . (x24 (x61 x73 x74) x73False)False)(∀ x73 x74 . (x62 (x61 x74 x73) x73False)False)(∀ x73 x74 . (x19 (x61 x73 x74)False)False)(∀ x73 . (x72 x73False)(x27 (x26 x73) x73False)False)(∀ x73 . (x72 x73False)(x2 (x26 x73) (x1 x73)False)False)(∀ x73 . x27 (x28 x73) x73False)(∀ x73 . (x2 (x28 x73) (x1 x73)False)False)(∀ x73 x74 . (x24 (x29 x73 x74) x73False)False)(∀ x73 x74 . (x62 (x29 x74 x73) x73False)False)(∀ x73 x74 . (x19 (x29 x73 x74)False)False)((x65 x60False)False)((x7 x60False)False)((x19 x60False)False)(x72 x60False)(x72 x59False)(∀ x73 . (x72 (x30 x73)False)False)(∀ x73 . (x2 (x30 x73) (x1 x73)False)False)(∀ x73 . (x72 x73False)(x65 (x31 x73)False)False)(∀ x73 . (x72 x73False)x72 (x31 x73)False)(∀ x73 . (x72 x73False)(x2 (x31 x73) (x3 x73)False)False)((x58 x57False)False)((x19 x57False)False)(∀ x73 . (x72 x73False)(x65 (x56 x73)False)False)(∀ x73 . (x72 x73False)x72 (x56 x73)False)(∀ x73 . (x72 x73False)(x2 (x56 x73) (x1 x73)False)False)((x72 x32False)False)(∀ x73 . (x72 x73False)x72 (x55 x73)False)(∀ x73 . (x72 x73False)(x2 (x55 x73) (x1 x73)False)False)(∀ x73 . (x65 (x54 x73)False)False)(∀ x73 . (x72 (x54 x73)False)False)(∀ x73 . (x2 (x54 x73) (x3 x73)False)False)(∀ x73 x74 . (x24 (x33 x73 x74) x73False)False)(∀ x73 x74 . (x62 (x33 x74 x73) x73False)False)(∀ x73 x74 . (x19 (x33 x73 x74)False)False)(∀ x73 x74 . (x72 (x33 x73 x74)False)False)(∀ x73 x74 . (x2 (x33 x73 x74) (x1 (x14 x74 x73))False)False)((x19 x53False)False)(x72 x53False)(∀ x73 . (x68 (x52 x73) x73False)False)(∀ x73 . (x13 (x52 x73) (x14 x73 x73) x73False)False)(∀ x73 . (x7 (x52 x73)False)False)(∀ x73 . (x24 (x52 x73) x73False)False)(∀ x73 . (x62 (x52 x73) (x14 x73 x73)False)False)(∀ x73 . (x19 (x52 x73)False)False)(∀ x73 . (x2 (x52 x73) (x1 (x14 (x14 x73 x73) x73))False)False)(∀ x73 x74 . (x13 (x34 x73 x74) x74 x73False)False)(∀ x73 x74 . (x7 (x34 x73 x74)False)False)(∀ x73 x74 . (x24 (x34 x73 x74) x73False)False)(∀ x73 x74 . (x62 (x34 x74 x73) x73False)False)(∀ x73 x74 . (x19 (x34 x73 x74)False)False)(∀ x73 x74 . (x2 (x34 x73 x74) (x1 (x14 x74 x73))False)False)((x65 x35False)False)(x72 x35False)(∀ x73 x74 x75 . x2 x74 (x3 x75)x2 x73 (x3 x75)(x8 x75 x74 x74 = x74False)False)(∀ x73 . (x67 x73 x73 = x73False)False)(∀ x73 x74 . x65 x74x65 x73(x65 (x67 x74 x73)False)False)(∀ x73 x74 x75 x76 . (x19 (x51 (x50 x74 x73) (x50 x76 x75))False)False)(∀ x73 x74 . (x19 (x14 x73 x74)False)False)(∀ x73 x74 . (x72 x74False)x72 (x67 x73 x74)False)(∀ x73 x74 . (x19 (x16 (x50 x74 x73))False)False)(∀ x73 x74 . (x72 x74False)x72 (x67 x74 x73)False)(∀ x73 x74 x75 . x19 x75x24 x75 x73x19 x74x24 x74 x73(x24 (x67 x75 x74) x73False)False)(∀ x73 x74 . x72 (x51 x73 x74)False)(∀ x73 x74 . x19 x74x19 x73(x19 (x67 x74 x73)False)False)(∀ x73 x74 . x19 x74x7 x74x17 x74(x65 (x66 x74 x73)False)False)(∀ x73 x74 . x20 x74x20 x73(x20 (x67 x74 x73)False)False)(∀ x73 x74 . x65 x74x65 x73(x20 (x51 x74 x73)False)False)(∀ x73 . x65 x73(x20 (x1 x73)False)False)(∀ x73 . x65 x73(x20 (x16 x73)False)False)(∀ x73 . x72 (x16 x73)False)(∀ x73 . (x49 (x3 x73)False)False)(∀ x73 . x72 (x3 x73)False)(∀ x73 x74 . (x65 (x51 x73 x74)False)False)((x72 x71False)False)(∀ x73 . x72 (x1 x73)False)(∀ x73 x74 x75 . x19 x75x62 x75 x73x19 x74x62 x74 x73(x62 (x67 x75 x74) x73False)False)(∀ x73 . (x49 (x1 x73)False)False)(∀ x73 . (x65 (x16 x73)False)False)(∀ x73 . x65 x73(x65 (x1 x73)False)False)(∀ x73 x74 . x65 x74x65 x73(x65 (x14 x74 x73)False)False)(∀ x73 x74 . (x72 x74False)(x72 x73False)x72 (x14 x74 x73)False)(∀ x73 . (x2 (x36 x73) x73False)False)(∀ x73 . (x2 (x4 x73) (x1 (x14 (x14 (x3 x73) (x3 x73)) (x3 x73)))False)False)(∀ x73 . (x13 (x4 x73) (x14 (x3 x73) (x3 x73)) (x3 x73)False)False)(∀ x73 . (x7 (x4 x73)False)False)(∀ x73 x74 x75 x76 x77 . (x72 x77False)(x72 x73False)x7 x76x13 x76 (x14 x73 x73) x73x2 x76 (x1 (x14 (x14 x73 x73) x73))x2 x74 (x3 x77)x7 x75x13 x75 x77 x73x2 x75 (x1 (x14 x77 x73))(x2 (x11 x77 x73 x76 x74 x75) x73False)False)(∀ x73 x74 x75 . x2 x74 (x3 x75)x2 x73 (x3 x75)(x2 (x8 x75 x74 x73) (x3 x75)False)False)(∀ x73 . (x49 (x3 x73)False)False)(∀ x73 x74 x75 x76 . x7 x76x13 x76 (x14 x73 x73) x73x2 x76 (x1 (x14 (x14 x73 x73) x73))x2 x74 x73x2 x75 x73(x2 (x10 x73 x76 x74 x75) x73False)False)(∀ x73 x74 x75 x76 . (x72 x76False)x7 x73x13 x73 x76 x75x2 x73 (x1 (x14 x76 x75))x2 x74 x76(x2 (x12 x76 x75 x73 x74) x75False)False)(∀ x73 x74 . (x72 x74False)x2 x73 x74(x2 (x9 x74 x73) (x3 x74)False)False)(∀ x73 x74 x75 x76 . (x72 x76False)x2 x73 (x3 x76)x7 x75x13 x75 x76 (x3 x74)x2 x75 (x1 (x14 x76 (x3 x74)))(x2 (x37 x76 x74 x73 x75) (x3 x74)False)False)(∀ x73 x74 . (x50 x74 x73 = x51 (x51 x74 x73) (x16 x74)False)False)(∀ x73 x74 x75 x76 . (x72 x76False)x2 x73 (x3 x76)x7 x75x13 x75 x76 (x3 x74)x2 x75 (x1 (x14 x76 (x3 x74)))(x37 x76 x74 x73 x75 = x11 x76 (x3 x74) (x4 x74) x73 x75False)False)(∀ x73 x74 . x7 x74x13 x74 (x14 (x3 x73) (x3 x73)) (x3 x73)x2 x74 (x1 (x14 (x14 (x3 x73) (x3 x73)) (x3 x73)))x10 (x3 x73) x74 (x48 x74 x73) (x47 x74 x73) = x8 x73 (x48 x74 x73) (x47 x74 x73)(x74 = x4 x73False)False)(∀ x73 x74 . x7 x74x13 x74 (x14 (x3 x73) (x3 x73)) (x3 x73)x2 x74 (x1 (x14 (x14 (x3 x73) (x3 x73)) (x3 x73)))(x2 (x47 x74 x73) (x3 x73)False)(x74 = x4 x73False)False)(∀ x73 x74 . x7 x74x13 x74 (x14 (x3 x73) (x3 x73)) (x3 x73)x2 x74 (x1 (x14 (x14 (x3 x73) (x3 x73)) (x3 x73)))(x2 (x48 x74 x73) (x3 x73)False)(x74 = x4 x73False)False)(∀ x73 x74 x75 x76 . x7 x76x13 x76 (x14 (x3 x73) (x3 x73)) (x3 x73)x2 x76 (x1 (x14 (x14 (x3 x73) (x3 x73)) (x3 x73)))x76 = x4 x73x2 x75 (x3 x73)x2 x74 (x3 x73)(x10 (x3 x73) x76 x75 x74 = x8 x73 x75 x74False)False)(∀ x73 x74 x75 . x19 x75x7 x75(x15 x75 x73 x74 = x66 x75 (x50 x73 x74)False)False)(∀ x73 x74 x75 . x2 x74 (x3 x75)x2 x73 (x3 x75)(x8 x75 x74 x73 = x8 x75 x73 x74False)False)(∀ x73 x74 . (x67 x74 x73 = x67 x73 x74False)False)(∀ x73 x74 . (x51 x74 x73 = x51 x73 x74False)False)(∀ x73 . x72 x73x19 x73(x17 x73False)False)(∀ x73 . x72 x73x19 x73(x19 x73False)False)(∀ x73 x74 . x72 x74x19 x73x24 x73 x74(x24 x73 x74False)False)(∀ x73 x74 . x72 x74x19 x73x24 x73 x74(x19 x73False)False)(∀ x73 x74 . x72 x74x19 x73x24 x73 x74(x72 x73False)False)(∀ x73 x74 x75 . (x72 x75False)(x72 x73False)x2 x74 (x1 (x14 x75 x73))x7 x74x13 x74 x75 x73(x13 x74 x75 x73False)False)(∀ x73 x74 x75 . (x72 x75False)(x72 x73False)x2 x74 (x1 (x14 x75 x73))x7 x74x13 x74 x75 x73x72 x74False)(∀ x73 x74 x75 . (x72 x75False)(x72 x73False)x2 x74 (x1 (x14 x75 x73))x7 x74x13 x74 x75 x73(x7 x74False)False)(∀ x73 x74 . x20 x74x2 x73 (x1 x74)(x20 x73False)False)(∀ x73 x74 . x72 x74x19 x73x62 x73 x74(x62 x73 x74False)False)(∀ x73 x74 . x72 x74x19 x73x62 x73 x74(x19 x73False)False)(∀ x73 x74 . x72 x74x19 x73x62 x73 x74(x72 x73False)False)(∀ x73 x74 . x20 x74x2 x73 x74(x65 x73False)False)(∀ x73 x74 x75 . x19 x75x24 x75 x73x2 x74 (x1 x75)(x24 x74 x73False)False)(∀ x73 . x72 x73(x20 x73False)False)(∀ x73 x74 . x64 x74x2 x73 (x1 x74)(x64 x73False)False)(∀ x73 x74 x75 . x19 x75x62 x75 x73x2 x74 (x1 x75)(x62 x74 x73False)False)(∀ x73 . (x65 x73False)x64 x73False)(∀ x73 x74 . x72 x74x2 x73 (x1 x74)x27 x73 x74False)(∀ x73 x74 x75 . x72 x75x2 x73 (x1 (x14 x74 x75))(x72 x73False)False)(∀ x73 . x72 x73x19 x73(x58 x73False)False)(∀ x73 . x72 x73x19 x73(x19 x73False)False)(∀ x73 x74 . x2 x74 (x1 (x14 x73 x73))x13 x74 x73 x73(x46 x74 x73False)False)(∀ x73 . x64 x73(x65 x73False)False)(∀ x73 x74 . (x72 x74False)x2 x73 (x1 x74)x72 x73(x27 x73 x74False)False)(∀ x73 x74 x75 . x72 x75x2 x73 (x1 (x14 x75 x74))(x72 x73False)False)(∀ x73 . x72 x73x19 x73(x45 x73False)False)(∀ x73 . x72 x73x19 x73(x19 x73False)False)(∀ x73 x74 x75 . (x72 x75False)x2 x73 (x1 (x14 x74 x75))x13 x73 x74 x75(x46 x73 x74False)False)(∀ x73 x74 . x2 x74 (x3 x73)(x65 x74False)False)(∀ x73 x74 x75 . x65 x75x2 x73 (x1 (x14 x75 x74))x7 x73x13 x73 x75 x74(x65 x73False)False)(∀ x73 x74 x75 . x65 x75x2 x73 (x1 (x14 x75 x74))x7 x73x13 x73 x75 x74(x13 x73 x75 x74False)False)(∀ x73 x74 x75 . x65 x75x2 x73 (x1 (x14 x75 x74))x7 x73x13 x73 x75 x74(x7 x73False)False)(∀ x73 x74 . (x72 x74False)x2 x73 (x1 x74)(x27 x73 x74False)x72 x73False)(∀ x73 x74 x75 . x2 x75 (x1 (x14 x73 x74))(x24 x75 x74False)False)(∀ x73 x74 x75 . x2 x75 (x1 (x14 x74 x73))(x62 x75 x74False)False)(∀ x73 x74 . x19 x74x2 x73 (x1 x74)(x19 x73False)False)(∀ x73 x74 x75 . x72 x75x2 x73 (x1 (x14 x75 x74))x13 x73 x75 x74(x46 x73 x75False)False)(∀ x73 . x44 x73x43 x73(x49 x73False)False)(∀ x73 x74 . x65 x74x2 x73 (x1 x74)(x65 x73False)False)(∀ x73 x74 . x72 x74x2 x73 (x1 x74)(x72 x73False)False)(∀ x73 x74 x75 . x2 x75 (x1 (x14 x73 x74))(x19 x75False)False)(∀ x73 . x72 x73(x19 x73False)False)(∀ x73 x74 x75 . x2 x74 (x1 (x14 x75 x73))x46 x74 x75(x13 x74 x75 x73False)False)(∀ x73 . x49 x73(x43 x73False)False)(∀ x73 . x49 x73(x44 x73False)False)(∀ x73 . x72 x73(x65 x73False)False)(∀ x73 x74 . x0 x73 x74x0 x74 x73False)(x37 x42 x38 (x8 x42 x39 (x9 x42 x40)) x41 = x8 x38 (x37 x42 x38 x39 x41) (x12 x42 (x3 x38) x41 x40)False)((x2 x39 (x3 x42)False)False)((x2 x40 x42False)False)((x2 x41 (x1 (x14 x42 (x3 x38)))False)False)((x13 x41 x42 (x3 x38)False)False)((x7 x41False)False)(x72 x42False)False
type
prop
theory
HotG
name
-
proof
PUcPC..
Megalodon
-
proofgold address
TMLar..
creator
35128 PrPhD../e68e3..
owner
35131 PrPhD../6c9e1..
term root
e10d3..