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 . x75 x77(x77 = x76False)x75 x76False)(∀ x76 x77 . x0 x76 x77x75 x77False)(∀ x76 . x75 x76(x76 = x74False)False)(∀ x76 x77 x78 x79 . x1 x79x8 x79 x76 x77x2 x79 (x3 (x4 x76 x77))x1 x78x8 x78 x76 x77x2 x78 (x3 (x4 x76 x77))x5 x79 (x6 x78 x79 x77 x76) = x5 x78 (x6 x78 x79 x77 x76)(x7 x76 x77 x79 x78False)False)(∀ x76 x77 x78 x79 . x1 x79x8 x79 x76 x77x2 x79 (x3 (x4 x76 x77))x1 x78x8 x78 x76 x77x2 x78 (x3 (x4 x76 x77))(x2 (x6 x78 x79 x77 x76) x76False)(x7 x76 x77 x79 x78False)False)(∀ x76 x77 x78 . x0 x76 x77x2 x77 (x3 x78)x75 x78False)(∀ x76 x77 x78 . x0 x77 x78x2 x78 (x3 x76)(x2 x77 x76False)False)(∀ x76 x77 . x9 x77 x76(x2 x77 (x3 x76)False)False)(∀ x76 x77 . x2 x77 (x3 x76)(x9 x77 x76False)False)(∀ x76 x77 . x1 x77x8 x77 x12 x13x2 x77 (x3 (x4 x12 x13))x1 x76x8 x76 x12 x13x2 x76 (x3 (x4 x12 x13))(x7 x12 x13 (x11 x12 x13 x13 (x10 x12 x13 x77) (x10 x12 x13 x76)) (x10 x12 x13 (x11 x12 x13 x13 x77 x76))False)False)(∀ x76 x77 . x2 x76 x77(x75 x77False)(x0 x76 x77False)False)(∀ x76 x77 . x0 x77 x76(x2 x77 x76False)False)((x2 x74 x73False)False)(∀ x76 x77 x78 x79 . x2 x79 (x3 (x4 x78 x77))x2 x76 (x3 (x4 x78 x77))x7 x78 x77 x79 x76(x7 x78 x77 x76 x79False)False)(∀ x76 x77 x78 x79 . x2 x79 (x3 (x4 x78 x77))x2 x76 (x3 (x4 x78 x77))(x7 x78 x77 x79 x79False)False)(∀ x76 . (x9 x76 x76False)False)(∀ x76 x77 x78 x79 . x2 x79 (x3 (x4 x78 x77))x2 x76 (x3 (x4 x78 x77))x79 = x76(x7 x78 x77 x79 x76False)False)(∀ x76 x77 x78 x79 . x2 x79 (x3 (x4 x78 x77))x2 x76 (x3 (x4 x78 x77))x7 x78 x77 x79 x76(x79 = x76False)False)(∀ x76 x77 x78 . (x75 x78False)(x75 x76False)x2 x76 (x3 x78)x2 x77 x76(x72 x77 x78 x76False)False)(∀ x76 x77 x78 . (x75 x78False)(x75 x76False)x2 x76 (x3 x78)x72 x77 x78 x76(x2 x77 x76False)False)(∀ x76 x77 x78 . x1 x78x8 x78 x12 x76x2 x78 (x3 (x4 x12 x76))x71 x77(x70 x76 x78 x77 = x5 x78 x77False)False)((x12 = x73False)False)(∀ x76 x77 x78 x79 x80 . x69 x80x69 x76x1 x79x2 x79 (x3 (x4 x77 x80))x1 x78x2 x78 (x3 (x4 x77 x76))(x67 x77 x80 x76 x79 x78 = x68 x79 x78False)False)(∀ x76 x77 x78 . x69 x78x1 x76x2 x76 (x3 (x4 x77 x78))(x10 x77 x78 x76 = x14 x76False)False)(∀ x76 x77 x78 x79 x80 . x69 x80x69 x76x1 x79x2 x79 (x3 (x4 x77 x80))x1 x78x2 x78 (x3 (x4 x77 x76))(x11 x77 x80 x76 x79 x78 = x66 x79 x78False)False)(∀ x76 . (x15 (x16 x76)False)False)(∀ x76 . (x65 (x16 x76) x76False)False)(∀ x76 . (x1 (x16 x76)False)False)(∀ x76 . (x64 (x16 x76) x76False)False)(∀ x76 . (x17 (x16 x76)False)False)(∀ x76 . (x15 (x63 x76)False)False)(∀ x76 . (x18 (x63 x76)False)False)(∀ x76 . (x62 (x63 x76)False)False)(∀ x76 . (x19 (x63 x76)False)False)(∀ x76 . (x65 (x63 x76) x76False)False)(∀ x76 . (x1 (x63 x76)False)False)(∀ x76 . (x60 (x63 x76) x61False)False)(∀ x76 . (x64 (x63 x76) x76False)False)(∀ x76 . (x17 (x63 x76)False)False)((x71 x20False)False)(x75 x20False)((x71 x21False)False)((x59 x58False)False)(x75 x58False)((x1 x58False)False)((x64 x58 x12False)False)((x17 x58False)False)(∀ x76 . (x22 (x23 x76)False)False)(∀ x76 . (x1 (x23 x76)False)False)(∀ x76 . (x60 (x23 x76) x76False)False)(∀ x76 . (x17 (x23 x76)False)False)((x24 x25False)False)((x57 x25False)False)(x75 x25False)((x56 x55False)False)(x75 x55False)(x75 x54False)(x75 x26False)((x1 x26False)False)((x64 x26 x12False)False)((x17 x26False)False)((x27 x28False)False)((x53 x28False)False)((x29 x28False)False)(x75 x28False)((x57 x30False)False)(x75 x30False)((x56 x31False)False)((x75 x52False)False)((x15 x32False)False)((x1 x32False)False)((x17 x32False)False)(∀ x76 x77 . (x60 (x51 x76 x77) x76False)False)(∀ x76 x77 . (x64 (x51 x77 x76) x76False)False)(∀ x76 x77 . (x17 (x51 x76 x77)False)False)(∀ x76 x77 . (x75 (x51 x76 x77)False)False)(∀ x76 x77 . (x2 (x51 x76 x77) (x3 (x4 x77 x76))False)False)((x27 x33False)False)((x57 x50False)False)(x75 x50False)(∀ x76 x77 . (x8 (x49 x76 x77) x77 x76False)False)(∀ x76 x77 . (x1 (x49 x76 x77)False)False)(∀ x76 x77 . (x60 (x49 x76 x77) x76False)False)(∀ x76 x77 . (x64 (x49 x77 x76) x76False)False)(∀ x76 x77 . (x17 (x49 x76 x77)False)False)(∀ x76 x77 . (x2 (x49 x76 x77) (x3 (x4 x77 x76))False)False)(∀ x76 x77 x78 . x69 x78x1 x76x2 x76 (x3 (x4 x77 x78))(x10 x77 x78 (x10 x77 x78 x76) = x76False)False)(∀ x76 . x17 x76x1 x76x19 x76(x14 (x14 x76) = x76False)False)(x59 x13False)(∀ x76 x77 x78 x79 x80 . (x75 x80False)x34 x80(x75 x79False)x34 x79x1 x78x8 x78 x76 x80x2 x78 (x3 (x4 x76 x80))x1 x77x8 x77 x76 x79x2 x77 (x3 (x4 x76 x79))(x65 (x68 x78 x77) x76False)False)(∀ x76 x77 x78 x79 x80 . (x75 x80False)x34 x80(x75 x79False)x34 x79x1 x78x8 x78 x76 x80x2 x78 (x3 (x4 x76 x80))x1 x77x8 x77 x76 x79x2 x77 (x3 (x4 x76 x79))(x1 (x68 x78 x77)False)False)(∀ x76 x77 x78 x79 x80 . (x75 x80False)x35 x80(x75 x79False)x35 x79x1 x78x8 x78 x76 x80x2 x78 (x3 (x4 x76 x80))x1 x77x8 x77 x76 x79x2 x77 (x3 (x4 x76 x79))(x65 (x68 x78 x77) x76False)False)(∀ x76 x77 x78 x79 x80 . (x75 x80False)x35 x80(x75 x79False)x35 x79x1 x78x8 x78 x76 x80x2 x78 (x3 (x4 x76 x80))x1 x77x8 x77 x76 x79x2 x77 (x3 (x4 x76 x79))(x1 (x68 x78 x77)False)False)(∀ x76 x77 x78 x79 x80 . (x75 x80False)x69 x80(x75 x79False)x69 x79x1 x78x8 x78 x76 x80x2 x78 (x3 (x4 x76 x80))x1 x77x8 x77 x76 x79x2 x77 (x3 (x4 x76 x79))(x65 (x68 x78 x77) x76False)False)(∀ x76 x77 x78 x79 x80 . (x75 x80False)x69 x80(x75 x79False)x69 x79x1 x78x8 x78 x76 x80x2 x78 (x3 (x4 x76 x80))x1 x77x8 x77 x76 x79x2 x77 (x3 (x4 x76 x79))(x1 (x68 x78 x77)False)False)(∀ x76 x77 . x17 x77x60 x77 x61x1 x77x17 x76x60 x76 x61x1 x76(x1 (x68 x77 x76)False)False)(∀ x76 x77 . x17 x77x60 x77 x61x1 x77x17 x76x60 x76 x61x1 x76(x60 (x68 x77 x76) x61False)False)(∀ x76 x77 . x17 x77x60 x77 x61x1 x77x17 x76x60 x76 x61x1 x76(x17 (x68 x77 x76)False)False)(∀ x76 x77 . x17 x77x1 x77x18 x77x17 x76x1 x76x18 x76(x18 (x68 x77 x76)False)False)(∀ x76 x77 . x17 x77x1 x77x18 x77x17 x76x1 x76x18 x76(x1 (x68 x77 x76)False)False)(∀ x76 x77 . x17 x77x1 x77x18 x77x17 x76x1 x76x18 x76(x17 (x68 x77 x76)False)False)(∀ x76 x77 . x17 x77x1 x77x19 x77x17 x76x1 x76x19 x76(x19 (x68 x77 x76)False)False)(∀ x76 x77 . x17 x77x1 x77x19 x77x17 x76x1 x76x19 x76(x1 (x68 x77 x76)False)False)(∀ x76 x77 . x17 x77x1 x77x19 x77x17 x76x1 x76x19 x76(x17 (x68 x77 x76)False)False)(∀ x76 x77 . x57 x77(x15 (x4 x76 x77)False)False)(x59 x36False)(∀ x76 x77 . x48 x77(x60 (x4 x76 x77) x47False)False)(∀ x76 x77 . x34 x77(x60 (x4 x76 x77) x61False)False)(∀ x76 x77 . x35 x77(x18 (x4 x76 x77)False)False)(∀ x76 x77 . x37 x77(x62 (x4 x76 x77)False)False)(∀ x76 x77 . x69 x77(x19 (x4 x76 x77)False)False)(x59 x61False)((x27 x73False)False)(x75 x73False)(x59 x47False)((x57 x73False)False)(∀ x76 x77 x78 . (x75 x78False)x34 x78x1 x77x8 x77 x76 x78x2 x77 (x3 (x4 x76 x78))(x65 (x14 x77) x76False)False)(∀ x76 x77 x78 . (x75 x78False)x34 x78x1 x77x8 x77 x76 x78x2 x77 (x3 (x4 x76 x78))(x1 (x14 x77)False)False)(∀ x76 x77 x78 . (x75 x78False)x35 x78x1 x77x8 x77 x76 x78x2 x77 (x3 (x4 x76 x78))(x65 (x14 x77) x76False)False)(∀ x76 x77 x78 . (x75 x78False)x35 x78x1 x77x8 x77 x76 x78x2 x77 (x3 (x4 x76 x78))(x1 (x14 x77)False)False)(∀ x76 x77 x78 . (x75 x78False)x69 x78x1 x77x8 x77 x76 x78x2 x77 (x3 (x4 x76 x78))(x65 (x14 x77) x76False)False)(∀ x76 x77 x78 . (x75 x78False)x69 x78x1 x77x8 x77 x76 x78x2 x77 (x3 (x4 x76 x78))(x1 (x14 x77)False)False)(∀ x76 x77 . x17 x77x1 x77x15 x77(x71 (x5 x77 x76)False)False)(∀ x76 . x17 x76x60 x76 x61x1 x76(x19 (x14 x76)False)False)(∀ x76 . x17 x76x60 x76 x61x1 x76(x1 (x14 x76)False)False)(∀ x76 . x17 x76x60 x76 x61x1 x76(x60 (x14 x76) x61False)False)(∀ x76 . x17 x76x60 x76 x61x1 x76(x17 (x14 x76)False)False)(∀ x76 x77 . x17 x77x60 x77 x47x1 x77(x38 (x5 x77 x76)False)False)(∀ x76 . x17 x76x1 x76x18 x76(x18 (x14 x76)False)False)(∀ x76 . x17 x76x1 x76x18 x76(x19 (x14 x76)False)False)(∀ x76 . x17 x76x1 x76x18 x76(x1 (x14 x76)False)False)(∀ x76 . x17 x76x1 x76x18 x76(x17 (x14 x76)False)False)(∀ x76 x77 . x17 x77x60 x77 x61x1 x77(x46 (x5 x77 x76)False)False)(∀ x76 x77 . x17 x77x1 x77x18 x77(x39 (x5 x77 x76)False)False)(∀ x76 x77 . x17 x77x1 x77x62 x77(x45 (x5 x77 x76)False)False)(∀ x76 x77 . x17 x77x1 x77x19 x77(x56 (x5 x77 x76)False)False)((x48 x47False)False)((x24 x73False)False)((x24 x47False)False)((x24 x61False)False)((x24 x36False)False)((x24 x13False)False)(x75 x47False)((x34 x61False)False)(∀ x76 x77 x78 x79 x80 . (x75 x80False)x57 x80(x75 x79False)x57 x79x1 x78x8 x78 x76 x80x2 x78 (x3 (x4 x76 x80))x1 x77x8 x77 x76 x79x2 x77 (x3 (x4 x76 x79))(x65 (x66 x78 x77) x76False)False)(∀ x76 x77 x78 x79 x80 . (x75 x80False)x57 x80(x75 x79False)x57 x79x1 x78x8 x78 x76 x80x2 x78 (x3 (x4 x76 x80))x1 x77x8 x77 x76 x79x2 x77 (x3 (x4 x76 x79))(x1 (x66 x78 x77)False)False)(∀ x76 x77 x78 x79 x80 . (x75 x80False)x48 x80(x75 x79False)x48 x79x1 x78x8 x78 x76 x80x2 x78 (x3 (x4 x76 x80))x1 x77x8 x77 x76 x79x2 x77 (x3 (x4 x76 x79))(x65 (x66 x78 x77) x76False)False)(∀ x76 x77 x78 x79 x80 . (x75 x80False)x48 x80(x75 x79False)x48 x79x1 x78x8 x78 x76 x80x2 x78 (x3 (x4 x76 x80))x1 x77x8 x77 x76 x79x2 x77 (x3 (x4 x76 x79))(x1 (x66 x78 x77)False)False)(∀ x76 x77 x78 x79 x80 . (x75 x80False)x34 x80(x75 x79False)x34 x79x1 x78x8 x78 x76 x80x2 x78 (x3 (x4 x76 x80))x1 x77x8 x77 x76 x79x2 x77 (x3 (x4 x76 x79))(x65 (x66 x78 x77) x76False)False)(∀ x76 x77 x78 x79 x80 . (x75 x80False)x34 x80(x75 x79False)x34 x79x1 x78x8 x78 x76 x80x2 x78 (x3 (x4 x76 x80))x1 x77x8 x77 x76 x79x2 x77 (x3 (x4 x76 x79))(x1 (x66 x78 x77)False)False)(x75 x61False)((x35 x36False)False)(∀ x76 x77 x78 x79 x80 . (x75 x80False)x35 x80(x75 x79False)x35 x79x1 x78x8 x78 x76 x80x2 x78 (x3 (x4 x76 x80))x1 x77x8 x77 x76 x79x2 x77 (x3 (x4 x76 x79))(x65 (x66 x78 x77) x76False)False)(∀ x76 x77 x78 x79 x80 . (x75 x80False)x35 x80(x75 x79False)x35 x79x1 x78x8 x78 x76 x80x2 x78 (x3 (x4 x76 x80))x1 x77x8 x77 x76 x79x2 x77 (x3 (x4 x76 x79))(x1 (x66 x78 x77)False)False)(∀ x76 x77 x78 x79 x80 . (x75 x80False)x69 x80(x75 x79False)x69 x79x1 x78x8 x78 x76 x80x2 x78 (x3 (x4 x76 x80))x1 x77x8 x77 x76 x79x2 x77 (x3 (x4 x76 x79))(x65 (x66 x78 x77) x76False)False)(∀ x76 x77 x78 x79 x80 . (x75 x80False)x69 x80(x75 x79False)x69 x79x1 x78x8 x78 x76 x80x2 x78 (x3 (x4 x76 x80))x1 x77x8 x77 x76 x79x2 x77 (x3 (x4 x76 x79))(x1 (x66 x78 x77)False)False)(∀ x76 x77 . x17 x77x1 x77x15 x77x17 x76x1 x76x15 x76(x15 (x66 x77 x76)False)False)(∀ x76 x77 . x17 x77x1 x77x15 x77x17 x76x1 x76x15 x76(x1 (x66 x77 x76)False)False)(∀ x76 x77 . x17 x77x1 x77x15 x77x17 x76x1 x76x15 x76(x17 (x66 x77 x76)False)False)(∀ x76 x77 . x17 x77x60 x77 x47x1 x77x17 x76x60 x76 x47x1 x76(x1 (x66 x77 x76)False)False)(∀ x76 x77 . x17 x77x60 x77 x47x1 x77x17 x76x60 x76 x47x1 x76(x60 (x66 x77 x76) x47False)False)(∀ x76 x77 . x17 x77x60 x77 x47x1 x77x17 x76x60 x76 x47x1 x76(x17 (x66 x77 x76)False)False)(∀ x76 x77 . x17 x77x60 x77 x61x1 x77x17 x76x60 x76 x61x1 x76(x1 (x66 x77 x76)False)False)(∀ x76 x77 . x17 x77x60 x77 x61x1 x77x17 x76x60 x76 x61x1 x76(x60 (x66 x77 x76) x61False)False)(∀ x76 x77 . x17 x77x60 x77 x61x1 x77x17 x76x60 x76 x61x1 x76(x17 (x66 x77 x76)False)False)(∀ x76 x77 . x17 x77x1 x77x18 x77x17 x76x1 x76x18 x76(x18 (x66 x77 x76)False)False)(∀ x76 x77 . x17 x77x1 x77x18 x77x17 x76x1 x76x18 x76(x1 (x66 x77 x76)False)False)(∀ x76 x77 . x17 x77x1 x77x18 x77x17 x76x1 x76x18 x76(x17 (x66 x77 x76)False)False)(∀ x76 x77 . x17 x77x1 x77x19 x77x17 x76x1 x76x19 x76(x19 (x66 x77 x76)False)False)(∀ x76 x77 . x17 x77x1 x77x19 x77x17 x76x1 x76x19 x76(x1 (x66 x77 x76)False)False)(∀ x76 x77 . x17 x77x1 x77x19 x77x17 x76x1 x76x19 x76(x17 (x66 x77 x76)False)False)(x75 x13False)((x75 x74False)False)(x75 x36False)((x69 x13False)False)(∀ x76 x77 x78 . x17 x78x64 x78 x76x1 x78x65 x78 x76x19 x78x17 x77x64 x77 x76x1 x77x65 x77 x76x19 x77(x65 (x68 x78 x77) x76False)False)(∀ x76 x77 x78 . x17 x78x64 x78 x76x1 x78x65 x78 x76x19 x78x17 x77x64 x77 x76x1 x77x65 x77 x76x19 x77(x1 (x68 x78 x77)False)False)(∀ x76 x77 x78 . x17 x78x64 x78 x76x1 x78x65 x78 x76x19 x78x17 x77x64 x77 x76x1 x77x65 x77 x76x19 x77(x17 (x68 x78 x77)False)False)(∀ x76 x77 x78 . x17 x78x64 x78 x76x1 x78x65 x78 x76x19 x78x17 x77x64 x77 x76x1 x77x65 x77 x76x19 x77(x65 (x66 x78 x77) x76False)False)(∀ x76 x77 x78 . x17 x78x64 x78 x76x1 x78x65 x78 x76x19 x78x17 x77x64 x77 x76x1 x77x65 x77 x76x19 x77(x1 (x66 x78 x77)False)False)(∀ x76 x77 x78 . x17 x78x64 x78 x76x1 x78x65 x78 x76x19 x78x17 x77x64 x77 x76x1 x77x65 x77 x76x19 x77(x17 (x66 x78 x77)False)False)(∀ x76 x77 x78 . x17 x78x1 x78x19 x78x17 x76x64 x76 x77x1 x76x19 x76(x1 (x68 x78 x76)False)False)(∀ x76 x77 x78 . x17 x78x1 x78x19 x78x17 x76x64 x76 x77x1 x76x19 x76(x64 (x68 x78 x76) x77False)False)(∀ x76 x77 x78 . x17 x78x1 x78x19 x78x17 x76x64 x76 x77x1 x76x19 x76(x17 (x68 x78 x76)False)False)(∀ x76 x77 x78 . x17 x78x1 x78x19 x78x17 x76x64 x76 x77x1 x76x19 x76(x1 (x66 x78 x76)False)False)(∀ x76 x77 x78 . x17 x78x1 x78x19 x78x17 x76x64 x76 x77x1 x76x19 x76(x64 (x66 x78 x76) x77False)False)(∀ x76 x77 x78 . x17 x78x1 x78x19 x78x17 x76x64 x76 x77x1 x76x19 x76(x17 (x66 x78 x76)False)False)(∀ x76 x77 . x17 x77x64 x77 x76x1 x77x65 x77 x76x19 x77(x19 (x14 x77)False)False)(∀ x76 x77 . x17 x77x64 x77 x76x1 x77x65 x77 x76x19 x77(x65 (x14 x77) x76False)False)(∀ x76 x77 . x17 x77x64 x77 x76x1 x77x65 x77 x76x19 x77(x1 (x14 x77)False)False)(∀ x76 x77 . x17 x77x64 x77 x76x1 x77x65 x77 x76x19 x77(x17 (x14 x77)False)False)(∀ x76 x77 . x17 x77x64 x77 x76x1 x77x19 x77(x19 (x14 x77)False)False)(∀ x76 x77 . x17 x77x64 x77 x76x1 x77x19 x77(x1 (x14 x77)False)False)(∀ x76 x77 . x17 x77x64 x77 x76x1 x77x19 x77(x64 (x14 x77) x76False)False)(∀ x76 x77 . x17 x77x64 x77 x76x1 x77x19 x77(x17 (x14 x77)False)False)(∀ x76 x77 . (x75 x77False)(x75 x76False)x2 x76 (x3 x77)(x72 (x40 x76 x77) x77 x76False)False)(∀ x76 . (x2 (x44 x76) x76False)False)(∀ x76 x77 x78 . (x75 x78False)(x75 x76False)x2 x76 (x3 x78)x72 x77 x78 x76(x2 x77 x78False)False)(∀ x76 x77 x78 . x1 x78x8 x78 x12 x76x2 x78 (x3 (x4 x12 x76))x71 x77(x2 (x70 x76 x78 x77) x76False)False)((x2 x12 (x3 x36)False)False)(∀ x76 x77 x78 x79 x80 . x69 x80x69 x76x1 x79x2 x79 (x3 (x4 x77 x80))x1 x78x2 x78 (x3 (x4 x77 x76))(x2 (x67 x77 x80 x76 x79 x78) (x3 (x4 x77 x13))False)False)(∀ x76 x77 x78 x79 x80 . x69 x80x69 x76x1 x79x2 x79 (x3 (x4 x77 x80))x1 x78x2 x78 (x3 (x4 x77 x76))(x1 (x67 x77 x80 x76 x79 x78)False)False)(∀ x76 x77 . x17 x77x1 x77x19 x77x17 x76x1 x76x19 x76(x1 (x68 x77 x76)False)False)(∀ x76 x77 . x17 x77x1 x77x19 x77x17 x76x1 x76x19 x76(x17 (x68 x77 x76)False)False)(∀ x76 x77 x78 . x69 x78x1 x76x2 x76 (x3 (x4 x77 x78))(x2 (x10 x77 x78 x76) (x3 (x4 x77 x13))False)False)(∀ x76 x77 x78 . x69 x78x1 x76x2 x76 (x3 (x4 x77 x78))(x1 (x10 x77 x78 x76)False)False)(∀ x76 . x17 x76x1 x76x19 x76(x19 (x14 x76)False)False)(∀ x76 . x17 x76x1 x76x19 x76(x1 (x14 x76)False)False)(∀ x76 . x17 x76x1 x76x19 x76(x17 (x14 x76)False)False)(∀ x76 x77 x78 x79 x80 . x69 x80x69 x76x1 x79x2 x79 (x3 (x4 x77 x80))x1 x78x2 x78 (x3 (x4 x77 x76))(x2 (x11 x77 x80 x76 x79 x78) (x3 (x4 x77 x13))False)False)(∀ x76 x77 x78 x79 x80 . x69 x80x69 x76x1 x79x2 x79 (x3 (x4 x77 x80))x1 x78x2 x78 (x3 (x4 x77 x76))(x1 (x11 x77 x80 x76 x79 x78)False)False)(∀ x76 x77 . x17 x77x1 x77x19 x77x17 x76x1 x76x19 x76(x1 (x66 x77 x76)False)False)(∀ x76 x77 . x17 x77x1 x77x19 x77x17 x76x1 x76x19 x76(x17 (x66 x77 x76)False)False)(∀ x76 x77 . x17 x77x1 x77x19 x77x17 x76x1 x76x19 x76(x68 x77 x76 = x66 x77 (x14 x76)False)False)(∀ x76 x77 x78 x79 x80 . x69 x80x69 x76x1 x79x2 x79 (x3 (x4 x77 x80))x1 x78x2 x78 (x3 (x4 x77 x76))(x11 x77 x80 x76 x79 x78 = x11 x77 x80 x76 x78 x79False)False)(∀ x76 x77 . x17 x77x1 x77x19 x77x17 x76x1 x76x19 x76(x66 x77 x76 = x66 x76 x77False)False)(∀ x76 . x75 x76x17 x76(x15 x76False)False)(∀ x76 . x75 x76x17 x76(x17 x76False)False)(∀ x76 . x75 x76(x43 x76False)False)(∀ x76 . x2 x76 (x3 x61)(x34 x76False)False)(∀ x76 . x17 x76x15 x76(x18 x76False)False)(∀ x76 . x17 x76x15 x76(x17 x76False)False)(∀ x76 . x2 x76 x73(x71 x76False)False)(∀ x76 . x2 x76 (x3 x36)(x35 x76False)False)(∀ x76 x77 x78 . (x75 x78False)(x75 x76False)x2 x77 (x3 (x4 x78 x76))x1 x77x8 x77 x78 x76(x8 x77 x78 x76False)False)(∀ x76 x77 x78 . (x75 x78False)(x75 x76False)x2 x77 (x3 (x4 x78 x76))x1 x77x8 x77 x78 x76x75 x77False)(∀ x76 x77 x78 . (x75 x78False)(x75 x76False)x2 x77 (x3 (x4 x78 x76))x1 x77x8 x77 x78 x76(x1 x77False)False)(∀ x76 . x17 x76x15 x76(x60 x76 x61False)False)(∀ x76 . x17 x76x15 x76(x17 x76False)False)(∀ x76 . x75 x76(x71 x76False)False)(∀ x76 . x17 x76x18 x76(x19 x76False)False)(∀ x76 . x17 x76x18 x76(x17 x76False)False)(∀ x76 . x71 x76(x27 x76False)False)(∀ x76 . x2 x76 (x3 x13)(x69 x76False)False)(∀ x76 . x17 x76x18 x76(x62 x76False)False)(∀ x76 . x17 x76x18 x76(x17 x76False)False)(∀ x76 x77 . x27 x77x2 x76 x77(x27 x76False)False)(∀ x76 . x35 x76(x69 x76False)False)(∀ x76 . x17 x76x60 x76 x61(x18 x76False)False)(∀ x76 . x17 x76x60 x76 x61(x17 x76False)False)(∀ x76 x77 x78 . x75 x78x2 x76 (x3 (x4 x77 x78))(x75 x76False)False)(∀ x76 . x75 x76(x22 x76False)False)(∀ x76 . x35 x76(x37 x76False)False)(∀ x76 x77 . x2 x77 (x3 (x4 x76 x76))x8 x77 x76 x76(x65 x77 x76False)False)(∀ x76 . x2 x76 x13(x56 x76False)False)(∀ x76 . x17 x76x60 x76 x47(x18 x76False)False)(∀ x76 . x17 x76x60 x76 x47(x17 x76False)False)(∀ x76 x77 x78 . x75 x78x2 x76 (x3 (x4 x78 x77))(x75 x76False)False)(∀ x76 . x75 x76(x27 x76False)False)(∀ x76 . x34 x76(x35 x76False)False)(∀ x76 x77 x78 . (x75 x78False)x2 x76 (x3 (x4 x77 x78))x8 x76 x77 x78(x65 x76 x77False)False)(∀ x76 . x17 x76x60 x76 x12(x15 x76False)False)(∀ x76 . x17 x76x60 x76 x12(x17 x76False)False)(∀ x76 . x17 x76x60 x76 x36(x18 x76False)False)(∀ x76 . x17 x76x60 x76 x36(x17 x76False)False)(∀ x76 . x71 x76(x56 x76False)False)(∀ x76 . x17 x76x60 x76 x47(x60 x76 x61False)False)(∀ x76 . x17 x76x60 x76 x47(x17 x76False)False)(∀ x76 x77 x78 . x2 x78 (x3 (x4 x76 x77))(x60 x78 x77False)False)(∀ x76 x77 x78 . x2 x78 (x3 (x4 x77 x76))(x64 x78 x77False)False)(∀ x76 . x29 x76x53 x76(x27 x76False)False)(∀ x76 . x48 x76(x34 x76False)False)(∀ x76 x77 x78 . x75 x78x2 x76 (x3 (x4 x78 x77))x8 x76 x78 x77(x65 x76 x78False)False)(∀ x76 . x17 x76x60 x76 x13(x19 x76False)False)(∀ x76 . x17 x76x60 x76 x13(x17 x76False)False)(∀ x76 . x75 x76(x24 x76False)False)(∀ x76 . x2 x76 x12(x57 x76False)False)(∀ x76 x77 . x57 x77x2 x76 (x3 x77)(x57 x76False)False)(∀ x76 x77 . x48 x77x2 x76 (x3 x77)(x48 x76False)False)(∀ x76 x77 . x34 x77x2 x76 (x3 x77)(x34 x76False)False)(∀ x76 x77 x78 . x57 x78x2 x76 (x3 (x4 x77 x78))(x15 x76False)False)(∀ x76 x77 . x35 x77x2 x76 (x3 x77)(x35 x76False)False)(∀ x76 x77 x78 . x48 x78x2 x76 (x3 (x4 x77 x78))(x60 x76 x47False)False)(∀ x76 x77 . x37 x77x2 x76 (x3 x77)(x37 x76False)False)(∀ x76 . x2 x76 x36(x56 x76False)False)(∀ x76 . x17 x76x15 x76(x60 x76 x47False)False)(∀ x76 . x17 x76x15 x76(x17 x76False)False)(∀ x76 x77 x78 . x2 x78 (x3 (x4 x76 x77))(x17 x78False)False)(∀ x76 . x27 x76(x53 x76False)False)(∀ x76 . x27 x76(x29 x76False)False)(∀ x76 . x57 x76(x48 x76False)False)(∀ x76 x77 x78 . x2 x77 (x3 (x4 x78 x76))x65 x77 x78(x8 x77 x78 x76False)False)(∀ x76 x77 x78 . x34 x78x2 x76 (x3 (x4 x77 x78))(x60 x76 x61False)False)(∀ x76 x77 . x69 x77x2 x76 (x3 x77)(x69 x76False)False)(∀ x76 x77 x78 . x35 x78x2 x76 (x3 (x4 x77 x78))(x18 x76False)False)(∀ x76 . x75 x76(x57 x76False)False)(∀ x76 x77 x78 . x37 x78x2 x76 (x3 (x4 x77 x78))(x62 x76False)False)(∀ x76 x77 . x57 x77x2 x76 x77(x71 x76False)False)(∀ x76 x77 x78 . x69 x78x2 x76 (x3 (x4 x77 x78))(x19 x76False)False)(∀ x76 x77 . x48 x77x2 x76 x77(x38 x76False)False)(∀ x76 x77 . x17 x77x15 x77x2 x76 (x3 x77)(x15 x76False)False)(∀ x76 x77 . x34 x77x2 x76 x77(x46 x76False)False)(∀ x76 x77 . x17 x77x60 x77 x47x2 x76 (x3 x77)(x60 x76 x47False)False)(∀ x76 x77 . x35 x77x2 x76 x77(x39 x76False)False)(∀ x76 x77 . x17 x77x60 x77 x61x2 x76 (x3 x77)(x60 x76 x61False)False)(∀ x76 x77 . x37 x77x2 x76 x77(x45 x76False)False)(∀ x76 x77 . x17 x77x18 x77x2 x76 (x3 x77)(x18 x76False)False)(∀ x76 x77 . x69 x77x2 x76 x77(x56 x76False)False)(∀ x76 x77 . x17 x77x62 x77x2 x76 (x3 x77)(x62 x76False)False)(∀ x76 . x2 x76 (x3 x12)(x57 x76False)False)(∀ x76 x77 . x17 x77x19 x77x2 x76 (x3 x77)(x19 x76False)False)(∀ x76 x77 . x43 x77x2 x76 (x3 x77)(x43 x76False)False)(∀ x76 . x2 x76 (x3 x47)(x48 x76False)False)(∀ x76 x77 . x0 x76 x77x0 x77 x76False)(x7 x12 x13 (x10 x12 x13 (x67 x12 x13 x13 x41 x42)) (x67 x12 x13 x13 x42 x41)False)((x2 x42 (x3 (x4 x12 x13))False)False)((x8 x42 x12 x13False)False)((x1 x42False)False)((x2 x41 (x3 (x4 x12 x13))False)False)((x8 x41 x12 x13False)False)((x1 x41False)False)False
as obj
-
as prop
94244..
theory
HotG
stx
b7c2b..
address
TMN4G..