Search for blocks/addresses/...

Proofgold Term Root Disambiguation

∀ 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 . x77 x79(x79 = x78False)x77 x78False)(∀ x78 x79 . x0 x78 x79x77 x79False)(∀ x78 . x77 x78(x78 = x76False)False)(∀ x78 x79 x80 x81 . (x1 x81False)x8 x81x2 x81x6 x78 (x7 x81)x6 x80 (x7 x81)x6 x79 (x7 x81)x3 x81 x79 (x5 x81 x80 x78)(x3 x81 (x4 x81 x80 x79) x78False)False)(∀ x78 x79 x80 x81 . (x1 x81False)x8 x81x2 x81x6 x78 (x7 x81)x6 x80 (x7 x81)x6 x79 (x7 x81)x3 x81 (x4 x81 x80 x79) x78(x3 x81 x79 (x5 x81 x80 x78)False)False)(∀ x78 x79 x80 . x0 x78 x79x6 x79 (x9 x80)x77 x80False)(∀ x78 x79 . (x1 x79False)x71 x79x75 x79x8 x79x6 x78 (x7 x79)x72 x79(x74 x79 (x73 x79) x78 = x73 x79False)False)(∀ x78 x79 . (x1 x79False)x71 x79x75 x79x8 x79x6 x78 (x7 x79)x12 x79x10 x79x11 x79(x4 x79 (x73 x79) x78 = x78False)False)(∀ x78 x79 x80 . x0 x79 x80x6 x80 (x9 x78)(x6 x79 x78False)False)(∀ x78 x79 . (x1 x79False)x71 x79x75 x79x8 x79x6 x78 (x7 x79)(x3 x79 x78 (x73 x79)False)False)(∀ x78 x79 . x70 x79 x78(x6 x79 (x9 x78)False)False)(∀ x78 x79 . x6 x79 (x9 x78)(x70 x79 x78False)False)(∀ x78 x79 . x6 x78 x79(x77 x79False)(x0 x78 x79False)False)(∀ x78 x79 x80 . x71 x80x8 x80x6 x79 (x7 x80)x6 x78 (x7 x80)x3 x80 x79 x78x3 x80 x78 x79(x79 = x78False)False)(∀ x78 x79 . x0 x79 x78(x6 x79 x78False)False)(∀ x78 x79 . (x1 x79False)x11 x79x8 x79x6 x78 (x7 x79)(x3 x79 x78 x78False)False)(∀ x78 x79 x80 . x71 x80x12 x80x8 x80x6 x78 (x7 x80)x6 x79 (x7 x80)(x4 x80 x78 x79 = x4 x80 x79 x78False)False)(x77 x13False)(∀ x78 . (x70 x78 x78False)False)(∀ x78 x79 x80 x81 . (x77 x81False)x18 x78x14 x78 x81 x80x6 x78 (x9 (x15 x81 x80))x6 x79 x81(x16 x81 x80 x78 x79 = x17 x78 x79False)False)(∀ x78 . (x18 (x69 x78)False)False)(∀ x78 . (x19 (x69 x78) x78False)False)(∀ x78 . (x68 (x69 x78)False)False)(∀ x78 . (x20 (x69 x78)False)False)((x67 x66False)False)(x77 x66False)(∀ x78 x79 . (x18 (x65 x78 x79)False)False)(∀ x78 x79 . (x21 (x65 x78 x79) x78False)False)(∀ x78 x79 . (x19 (x65 x79 x78) x78False)False)(∀ x78 x79 . (x20 (x65 x78 x79)False)False)(x64 x63False)((x18 x63False)False)((x20 x63False)False)(∀ x78 . (x1 x78False)x23 x78x77 (x22 x78)False)(∀ x78 . (x1 x78False)x23 x78(x6 (x22 x78) (x9 (x7 x78))False)False)((x18 x24False)False)((x68 x24False)False)((x20 x24False)False)(x77 x24False)(∀ x78 x79 . (x21 (x25 x78 x79) x78False)False)(∀ x78 x79 . (x19 (x25 x79 x78) x78False)False)(∀ x78 x79 . (x20 (x25 x78 x79)False)False)((x18 x62False)False)((x68 x62False)False)((x20 x62False)False)(∀ x78 . (x1 x78False)x11 x78x8 x78(x27 (x26 x78) x78False)False)(∀ x78 . (x1 x78False)x11 x78x8 x78(x61 (x26 x78) x78False)False)(∀ x78 . (x1 x78False)x11 x78x8 x78(x28 (x26 x78)False)False)(∀ x78 . (x1 x78False)x11 x78x8 x78x77 (x26 x78)False)(∀ x78 . (x1 x78False)x11 x78x8 x78(x6 (x26 x78) (x9 (x7 x78))False)False)((x68 x60False)False)((x20 x60False)False)((x59 x58False)False)((x18 x58False)False)((x20 x58False)False)(∀ x78 . (x29 x78False)x23 x78x30 (x31 x78)False)(∀ x78 . (x29 x78False)x23 x78(x6 (x31 x78) (x9 (x7 x78))False)False)(∀ x78 . (x1 x78False)x23 x78(x30 (x32 x78)False)False)(∀ x78 . (x1 x78False)x23 x78x77 (x32 x78)False)(∀ x78 . (x1 x78False)x23 x78(x6 (x32 x78) (x9 (x7 x78))False)False)(∀ x78 . x8 x78(x27 (x57 x78) x78False)False)(∀ x78 . x8 x78(x61 (x57 x78) x78False)False)(∀ x78 . x8 x78(x6 (x57 x78) (x9 (x7 x78))False)False)(∀ x78 x79 . (x21 (x33 x78 x79) x78False)False)(∀ x78 x79 . (x19 (x33 x79 x78) x78False)False)(∀ x78 x79 . (x20 (x33 x78 x79)False)False)(∀ x78 x79 . (x77 (x33 x78 x79)False)False)(∀ x78 x79 . (x6 (x33 x78 x79) (x9 (x15 x79 x78))False)False)((x20 x56False)False)(x77 x56False)(∀ x78 x79 . (x14 (x55 x78 x79) x79 x78False)False)(∀ x78 x79 . (x18 (x55 x78 x79)False)False)(∀ x78 x79 . (x21 (x55 x78 x79) x78False)False)(∀ x78 x79 . (x19 (x55 x79 x78) x78False)False)(∀ x78 x79 . (x20 (x55 x78 x79)False)False)(∀ x78 x79 . (x6 (x55 x78 x79) (x9 (x15 x79 x78))False)False)((x18 x54False)False)((x20 x54False)False)(∀ x78 . (x53 x78False)x23 x78x28 (x7 x78)False)(∀ x78 . x53 x78x23 x78(x28 (x7 x78)False)False)(∀ x78 . x29 x78x23 x78(x30 (x7 x78)False)False)(∀ x78 . (x29 x78False)x23 x78x30 (x7 x78)False)(∀ x78 x79 . (x20 (x15 x78 x79)False)False)(∀ x78 . (x1 x78False)x23 x78x77 (x7 x78)False)(∀ x78 . x1 x78x23 x78(x77 (x7 x78)False)False)(∀ x78 x79 . x20 x79x34 x79x18 x79(x77 (x17 x79 x78)False)False)(∀ x78 x79 x80 . x67 x80x20 x78x21 x78 x80x18 x78(x18 (x17 x78 x79)False)False)(∀ x78 x79 x80 . x67 x80x20 x78x21 x78 x80x18 x78(x20 (x17 x78 x79)False)False)(∀ x78 . (x6 (x52 x78) x78False)False)((x23 x35False)False)((x8 x51False)False)((x77 x36False)False)(∀ x78 . x8 x78(x23 x78False)False)(∀ x78 x79 x80 . (x1 x80False)x8 x80x6 x79 (x7 x80)x6 x78 (x7 x80)(x6 (x5 x80 x79 x78) (x7 x80)False)False)(∀ x78 x79 . (x1 x79False)x8 x79x6 x78 (x7 x79)(x6 (x50 x79 x78) (x9 (x15 (x7 x79) (x7 x79)))False)False)(∀ x78 x79 . (x1 x79False)x8 x79x6 x78 (x7 x79)(x14 (x50 x79 x78) (x7 x79) (x7 x79)False)False)(∀ x78 x79 . (x1 x79False)x8 x79x6 x78 (x7 x79)(x18 (x50 x79 x78)False)False)(∀ x78 . x8 x78(x6 (x73 x78) (x7 x78)False)False)(∀ x78 x79 x80 x81 . (x77 x81False)x18 x78x14 x78 x81 x80x6 x78 (x9 (x15 x81 x80))x6 x79 x81(x6 (x16 x81 x80 x78 x79) x80False)False)(∀ x78 x79 . x8 x79(x6 (x37 x79 x78) (x7 x79)False)False)(∀ x78 x79 x80 . x8 x80x6 x78 (x7 x80)x6 x79 (x7 x80)(x6 (x4 x80 x78 x79) (x7 x80)False)False)(∀ x78 x79 x80 . x8 x80x6 x78 (x7 x80)x6 x79 (x7 x80)(x6 (x74 x80 x78 x79) (x7 x80)False)False)((x76 = x36False)False)(∀ x78 x79 x80 . (x1 x80False)x8 x80x6 x79 (x7 x80)x6 x78 (x7 x80)(x5 x80 x79 x78 = x16 (x7 x80) (x7 x80) (x50 x80 x79) x78False)False)(∀ x78 . x8 x78(x73 x78 = x37 x78 x76False)False)(∀ x78 . x23 x78x38 x78 x76(x1 x78False)False)(∀ x78 x79 . x67 x79x6 x78 (x9 x79)(x67 x78False)False)(∀ x78 . x23 x78x1 x78(x38 x78 x76False)False)(∀ x78 x79 . x77 x79x20 x78x21 x78 x79(x21 x78 x79False)False)(∀ x78 x79 . x77 x79x20 x78x21 x78 x79(x20 x78False)False)(∀ x78 x79 . x77 x79x20 x78x21 x78 x79(x77 x78False)False)(∀ x78 x79 x80 . (x77 x80False)(x77 x78False)x6 x79 (x9 (x15 x80 x78))x18 x79x14 x79 x80 x78(x14 x79 x80 x78False)False)(∀ x78 x79 x80 . (x77 x80False)(x77 x78False)x6 x79 (x9 (x15 x80 x78))x18 x79x14 x79 x80 x78x77 x79False)(∀ x78 x79 x80 . (x77 x80False)(x77 x78False)x6 x79 (x9 (x15 x80 x78))x18 x79x14 x79 x80 x78(x18 x79False)False)(∀ x78 x79 . x67 x79x6 x78 x79(x18 x78False)False)(∀ x78 x79 . x67 x79x6 x78 x79(x20 x78False)False)(∀ x78 . x8 x78(x1 x78False)x2 x78(x75 x78False)False)(∀ x78 . x8 x78(x1 x78False)x2 x78x1 x78False)(∀ x78 . x23 x78(x53 x78False)x29 x78False)(∀ x78 x79 . x77 x79x20 x78x19 x78 x79(x19 x78 x79False)False)(∀ x78 x79 . x77 x79x20 x78x19 x78 x79(x20 x78False)False)(∀ x78 x79 . x77 x79x20 x78x19 x78 x79(x77 x78False)False)(∀ x78 . x77 x78(x67 x78False)False)(∀ x78 . x8 x78(x1 x78False)x2 x78(x39 x78False)False)(∀ x78 . x8 x78(x1 x78False)x2 x78x1 x78False)(∀ x78 . x8 x78(x1 x78False)x29 x78x11 x78(x40 x78False)False)(∀ x78 . x8 x78(x1 x78False)x29 x78x11 x78(x11 x78False)False)(∀ x78 . x8 x78(x1 x78False)x29 x78x11 x78x1 x78False)(∀ x78 . x23 x78x29 x78(x53 x78False)False)(∀ x78 x79 x80 . x20 x80x21 x80 x78x6 x79 (x9 x80)(x21 x79 x78False)False)(∀ x78 . x30 x78x20 x78x18 x78(x64 x78False)False)(∀ x78 . x30 x78x20 x78x18 x78(x18 x78False)False)(∀ x78 . x30 x78x20 x78x18 x78(x20 x78False)False)(∀ x78 . x8 x78x42 x78x75 x78(x41 x78False)False)(∀ x78 . x8 x78(x1 x78False)x2 x78(x12 x78False)False)(∀ x78 . x8 x78(x1 x78False)x2 x78(x72 x78False)False)(∀ x78 . x8 x78(x1 x78False)x2 x78(x71 x78False)False)(∀ x78 . x8 x78(x1 x78False)x2 x78(x10 x78False)False)(∀ x78 . x8 x78(x1 x78False)x2 x78(x11 x78False)False)(∀ x78 . x8 x78(x1 x78False)x2 x78x1 x78False)(∀ x78 . x23 x78(x53 x78False)x53 x78False)(∀ x78 . x23 x78(x53 x78False)x1 x78False)(∀ x78 x79 x80 . x20 x80x19 x80 x78x6 x79 (x9 x80)(x19 x79 x78False)False)(∀ x78 . x20 x78x18 x78(x64 x78False)(x18 x78False)False)(∀ x78 . x20 x78x18 x78(x64 x78False)(x20 x78False)False)(∀ x78 . x20 x78x18 x78(x64 x78False)x30 x78False)(∀ x78 . x8 x78x41 x78(x75 x78False)False)(∀ x78 . x8 x78x41 x78(x42 x78False)False)(∀ x78 . x23 x78x1 x78(x53 x78False)False)(∀ x78 . x23 x78x1 x78(x1 x78False)False)(∀ x78 x79 x80 . x77 x80x6 x78 (x9 (x15 x79 x80))(x77 x78False)False)(∀ x78 . x77 x78x20 x78(x68 x78False)False)(∀ x78 . x77 x78x20 x78(x20 x78False)False)(∀ x78 x79 . x6 x79 (x9 (x15 x78 x78))x14 x79 x78 x78(x43 x79 x78False)False)(∀ x78 . x77 x78x20 x78x18 x78(x64 x78False)False)(∀ x78 . x77 x78x20 x78x18 x78(x18 x78False)False)(∀ x78 . x77 x78x20 x78x18 x78(x20 x78False)False)(∀ x78 . x8 x78(x1 x78False)x44 x78(x41 x78False)False)(∀ x78 . x8 x78(x1 x78False)x44 x78x1 x78False)(∀ x78 x79 x80 . x77 x80x6 x78 (x9 (x15 x80 x79))(x77 x78False)False)(∀ x78 . x77 x78x20 x78(x34 x78False)False)(∀ x78 . x77 x78x20 x78(x20 x78False)False)(∀ x78 x79 x80 . (x77 x80False)x6 x78 (x9 (x15 x79 x80))x14 x78 x79 x80(x43 x78 x79False)False)(∀ x78 x79 . x20 x79x18 x79x6 x78 (x9 x79)(x18 x78False)False)(∀ x78 . x8 x78x38 x78 x13x11 x78(x44 x78False)False)(∀ x78 . x8 x78x38 x78 x13x11 x78(x71 x78False)False)(∀ x78 . x8 x78x38 x78 x13x11 x78(x10 x78False)False)(∀ x78 . x8 x78x38 x78 x13x11 x78(x11 x78False)False)(∀ x78 . x8 x78x38 x78 x13x11 x78(x38 x78 x13False)False)(∀ x78 . x23 x78(x29 x78False)x1 x78False)(∀ x78 x79 x80 . x6 x80 (x9 (x15 x78 x79))(x21 x80 x79False)False)(∀ x78 x79 x80 . x6 x80 (x9 (x15 x79 x78))(x19 x80 x79False)False)(∀ x78 x79 . x20 x79x6 x78 (x9 x79)(x20 x78False)False)(∀ x78 . x8 x78x12 x78x1 x78False)(∀ x78 x79 x80 . x77 x80x6 x78 (x9 (x15 x80 x79))x14 x78 x80 x79(x43 x78 x80False)False)(∀ x78 . x77 x78x20 x78x18 x78(x59 x78False)False)(∀ x78 . x77 x78x20 x78x18 x78(x18 x78False)False)(∀ x78 . x77 x78x20 x78x18 x78(x20 x78False)False)(∀ x78 . x8 x78(x1 x78False)x11 x78x10 x78x71 x78x75 x78x49 x78x48 x78(x44 x78False)False)(∀ x78 . x8 x78(x1 x78False)x11 x78x10 x78x71 x78x75 x78x49 x78x48 x78(x71 x78False)False)(∀ x78 . x8 x78(x1 x78False)x11 x78x10 x78x71 x78x75 x78x49 x78x48 x78(x10 x78False)False)(∀ x78 . x8 x78(x1 x78False)x11 x78x10 x78x71 x78x75 x78x49 x78x48 x78(x11 x78False)False)(∀ x78 . x8 x78(x1 x78False)x11 x78x10 x78x71 x78x75 x78x49 x78x48 x78x1 x78False)(∀ x78 . x8 x78(x1 x78False)x44 x78(x12 x78False)False)(∀ x78 . x8 x78(x1 x78False)x44 x78(x72 x78False)False)(∀ x78 . x8 x78(x1 x78False)x44 x78x1 x78False)(∀ x78 x79 . x8 x79x6 x78 (x9 (x7 x79))x77 x78(x27 x78 x79False)False)(∀ x78 x79 . x8 x79x6 x78 (x9 (x7 x79))x77 x78(x61 x78 x79False)False)(∀ x78 . x23 x78x1 x78(x29 x78False)False)(∀ x78 x79 x80 . x6 x80 (x9 (x15 x78 x79))(x20 x80False)False)(∀ x78 . x77 x78(x20 x78False)False)(∀ x78 . x8 x78x72 x78x1 x78False)(∀ x78 x79 x80 . x6 x79 (x9 (x15 x80 x78))x43 x79 x80(x14 x79 x80 x78False)False)(∀ x78 . x77 x78(x18 x78False)False)(∀ x78 . x23 x78(x29 x78False)x1 x78False)(∀ x78 . x8 x78(x1 x78False)x11 x78x71 x78x75 x78x48 x78(x75 x78False)False)(∀ x78 . x8 x78(x1 x78False)x11 x78x71 x78x75 x78x48 x78(x72 x78False)False)(∀ x78 . x8 x78(x1 x78False)x11 x78x71 x78x75 x78x48 x78(x71 x78False)False)(∀ x78 . x8 x78(x1 x78False)x11 x78x71 x78x75 x78x48 x78(x11 x78False)False)(∀ x78 . x8 x78(x1 x78False)x11 x78x71 x78x75 x78x48 x78x1 x78False)(∀ x78 . x8 x78(x1 x78False)x11 x78x71 x78x48 x78(x12 x78False)False)(∀ x78 . x8 x78(x1 x78False)x11 x78x71 x78x48 x78(x71 x78False)False)(∀ x78 . x8 x78(x1 x78False)x11 x78x71 x78x48 x78(x11 x78False)False)(∀ x78 . x8 x78(x1 x78False)x11 x78x71 x78x48 x78x1 x78False)(∀ x78 . x8 x78(x1 x78False)x11 x78x10 x78x71 x78x72 x78x42 x78x49 x78(x44 x78False)False)(∀ x78 . x8 x78(x1 x78False)x11 x78x10 x78x71 x78x72 x78x42 x78x49 x78(x71 x78False)False)(∀ x78 . x8 x78(x1 x78False)x11 x78x10 x78x71 x78x72 x78x42 x78x49 x78(x10 x78False)False)(∀ x78 . x8 x78(x1 x78False)x11 x78x10 x78x71 x78x72 x78x42 x78x49 x78(x11 x78False)False)(∀ x78 . x8 x78(x1 x78False)x11 x78x10 x78x71 x78x72 x78x42 x78x49 x78x1 x78False)(∀ x78 . x8 x78(x1 x78False)x11 x78x48 x78(x42 x78False)False)(∀ x78 . x8 x78(x1 x78False)x11 x78x48 x78(x11 x78False)False)(∀ x78 . x8 x78(x1 x78False)x11 x78x48 x78x1 x78False)(∀ x78 . x8 x78(x1 x78False)x11 x78x44 x78(x48 x78False)False)(∀ x78 . x8 x78(x1 x78False)x11 x78x44 x78(x49 x78False)False)(∀ x78 . x8 x78(x1 x78False)x11 x78x44 x78(x11 x78False)False)(∀ x78 . x8 x78(x1 x78False)x11 x78x44 x78x1 x78False)(∀ x78 . x23 x78x38 x78 x13(x29 x78False)False)(∀ x78 . x23 x78x38 x78 x13x1 x78False)(∀ x78 . x8 x78x11 x78x72 x78x49 x78(x75 x78False)False)(∀ x78 . x8 x78x11 x78x72 x78x49 x78(x72 x78False)False)(∀ x78 . x8 x78x11 x78x72 x78x49 x78(x11 x78False)False)(∀ x78 . x23 x78(x1 x78False)x29 x78(x38 x78 x13False)False)(∀ x78 x79 . x0 x78 x79x0 x79 x78False)((x3 x47 x46 x45False)(x73 x47 = x5 x47 x46 x45False)False)(x73 x47 = x5 x47 x46 x45x3 x47 x46 x45False)((x6 x45 (x7 x47)False)False)((x6 x46 (x7 x47)False)False)((x2 x47False)False)((x8 x47False)False)(x1 x47False)False
as obj
-
as prop
e175e..
theory
HotG
stx
a8d96..
address
TML4t..