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 . x72 x74 ⟶ (x74 = x73 ⟶ False) ⟶ x72 x73 ⟶ False) ⟶ (∀ x73 x74 . x0 x73 x74 ⟶ x72 x74 ⟶ False) ⟶ (∀ x73 . x72 x73 ⟶ (x73 = x71 ⟶ False) ⟶ False) ⟶ (∀ x73 x74 x75 . x0 x73 x74 ⟶ x2 x74 (x1 x75) ⟶ x72 x75 ⟶ False) ⟶ (∀ x73 x74 x75 . x0 x74 x75 ⟶ x2 x75 (x1 x73) ⟶ (x2 x74 x73 ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . x3 x74 x73 ⟶ (x2 x74 (x1 x73) ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . x2 x74 (x1 x73) ⟶ (x3 x74 x73 ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . x2 x73 x74 ⟶ (x72 x74 ⟶ False) ⟶ (x0 x73 x74 ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . (x70 x74 ⟶ False) ⟶ x62 x74 ⟶ x69 x74 ⟶ x63 x74 ⟶ x68 x74 ⟶ x64 x74 ⟶ x2 x73 (x65 x74) ⟶ (x66 x74 x73 (x67 x74) = x73 ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . x0 x74 x73 ⟶ (x2 x74 x73 ⟶ False) ⟶ False) ⟶ (x72 x61 ⟶ False) ⟶ (∀ x73 . (x3 x73 x73 ⟶ False) ⟶ False) ⟶ (∀ x73 x74 x75 x76 . x60 x76 ⟶ x57 x76 (x56 x73 x73) x73 ⟶ x2 x76 (x1 (x56 (x56 x73 x73) x73)) ⟶ x2 x74 x73 ⟶ x2 x75 x73 ⟶ (x59 x73 x76 x74 x75 = x58 x76 x74 x75 ⟶ False) ⟶ False) ⟶ (∀ x73 . (x72 x73 ⟶ False) ⟶ (x4 (x5 x73) x61 ⟶ False) ⟶ False) ⟶ (∀ x73 . (x72 x73 ⟶ False) ⟶ (x2 (x5 x73) (x1 x73) ⟶ False) ⟶ False) ⟶ (∀ x73 . x6 x73 ⟶ (x4 (x7 x73) x73 ⟶ False) ⟶ False) ⟶ (∀ x73 . x6 x73 ⟶ (x60 (x7 x73) ⟶ False) ⟶ False) ⟶ (∀ x73 . x6 x73 ⟶ (x8 (x7 x73) ⟶ False) ⟶ False) ⟶ (∀ x73 . x6 x73 ⟶ (x4 (x55 x73) x73 ⟶ False) ⟶ False) ⟶ (∀ x73 . (x70 x73 ⟶ False) ⟶ x10 x73 ⟶ x72 (x9 x73) ⟶ False) ⟶ (∀ x73 . (x70 x73 ⟶ False) ⟶ x10 x73 ⟶ (x2 (x9 x73) (x1 (x65 x73)) ⟶ False) ⟶ False) ⟶ (∀ x73 . (x11 x73 ⟶ False) ⟶ x11 (x12 x73) ⟶ False) ⟶ (∀ x73 . (x11 x73 ⟶ False) ⟶ (x2 (x12 x73) (x1 x73) ⟶ False) ⟶ False) ⟶ (x11 x13 ⟶ False) ⟶ ((x54 x53 ⟶ False) ⟶ False) ⟶ ((x8 x53 ⟶ False) ⟶ False) ⟶ (∀ x73 . x6 x73 ⟶ (x51 (x52 x73) x73 ⟶ False) ⟶ False) ⟶ (∀ x73 . x6 x73 ⟶ (x10 (x52 x73) ⟶ False) ⟶ False) ⟶ (∀ x73 . (x50 x73 ⟶ False) ⟶ x10 x73 ⟶ x49 (x48 x73) ⟶ False) ⟶ (∀ x73 . (x50 x73 ⟶ False) ⟶ x10 x73 ⟶ (x2 (x48 x73) (x1 (x65 x73)) ⟶ False) ⟶ False) ⟶ (∀ x73 . (x70 x73 ⟶ False) ⟶ x10 x73 ⟶ (x49 (x47 x73) ⟶ False) ⟶ False) ⟶ (∀ x73 . (x70 x73 ⟶ False) ⟶ x10 x73 ⟶ x72 (x47 x73) ⟶ False) ⟶ (∀ x73 . (x70 x73 ⟶ False) ⟶ x10 x73 ⟶ (x2 (x47 x73) (x1 (x65 x73)) ⟶ False) ⟶ False) ⟶ ((x50 x14 ⟶ False) ⟶ False) ⟶ (x70 x14 ⟶ False) ⟶ ((x15 x14 ⟶ False) ⟶ False) ⟶ ((x8 x46 ⟶ False) ⟶ False) ⟶ (x72 x46 ⟶ False) ⟶ ((x6 x45 ⟶ False) ⟶ False) ⟶ (∀ x73 . (x50 x73 ⟶ False) ⟶ x15 x73 ⟶ x16 (x17 x73) x73 ⟶ False) ⟶ (∀ x73 . (x50 x73 ⟶ False) ⟶ x15 x73 ⟶ (x2 (x17 x73) (x65 x73) ⟶ False) ⟶ False) ⟶ (∀ x73 . x15 x73 ⟶ (x16 (x18 x73) x73 ⟶ False) ⟶ False) ⟶ (∀ x73 . x15 x73 ⟶ (x2 (x18 x73) (x65 x73) ⟶ False) ⟶ False) ⟶ (∀ x73 x74 x75 . (x70 x75 ⟶ False) ⟶ x62 x75 ⟶ x69 x75 ⟶ x63 x75 ⟶ x68 x75 ⟶ x64 x75 ⟶ x20 x75 (x19 x75) = x19 x75 ⟶ x2 x73 (x65 x75) ⟶ x2 x74 (x65 x75) ⟶ (x66 x75 x73 x74 = x66 x75 x74 x73 ⟶ False) ⟶ False) ⟶ (∀ x73 x74 x75 . (x70 x75 ⟶ False) ⟶ x62 x75 ⟶ x69 x75 ⟶ x63 x75 ⟶ x68 x75 ⟶ x64 x75 ⟶ (x2 (x19 x75) (x65 x75) ⟶ False) ⟶ x2 x73 (x65 x75) ⟶ x2 x74 (x65 x75) ⟶ (x66 x75 x73 x74 = x66 x75 x74 x73 ⟶ False) ⟶ False) ⟶ (∀ x73 . (x70 x73 ⟶ False) ⟶ x62 x73 ⟶ x69 x73 ⟶ x63 x73 ⟶ x68 x73 ⟶ x64 x73 ⟶ x66 x73 (x22 x73) (x23 x73) = x66 x73 (x23 x73) (x22 x73) ⟶ (x21 x73 ⟶ False) ⟶ False) ⟶ (∀ x73 . (x70 x73 ⟶ False) ⟶ x62 x73 ⟶ x69 x73 ⟶ x63 x73 ⟶ x68 x73 ⟶ x64 x73 ⟶ (x2 (x22 x73) (x65 x73) ⟶ False) ⟶ (x21 x73 ⟶ False) ⟶ False) ⟶ (∀ x73 . (x70 x73 ⟶ False) ⟶ x62 x73 ⟶ x69 x73 ⟶ x63 x73 ⟶ x68 x73 ⟶ x64 x73 ⟶ (x2 (x23 x73) (x65 x73) ⟶ False) ⟶ (x21 x73 ⟶ False) ⟶ False) ⟶ (∀ x73 . (x44 x73 ⟶ False) ⟶ x10 x73 ⟶ x11 (x65 x73) ⟶ False) ⟶ (∀ x73 . (x11 x73 ⟶ False) ⟶ x11 (x1 x73) ⟶ False) ⟶ (∀ x73 . x44 x73 ⟶ x10 x73 ⟶ (x11 (x65 x73) ⟶ False) ⟶ False) ⟶ (∀ x73 . x50 x73 ⟶ x10 x73 ⟶ (x49 (x65 x73) ⟶ False) ⟶ False) ⟶ (∀ x73 . (x50 x73 ⟶ False) ⟶ x10 x73 ⟶ x49 (x65 x73) ⟶ False) ⟶ (∀ x73 x74 . (x8 (x56 x73 x74) ⟶ False) ⟶ False) ⟶ (∀ x73 . (x70 x73 ⟶ False) ⟶ x10 x73 ⟶ x72 (x65 x73) ⟶ False) ⟶ (∀ x73 . x70 x73 ⟶ x10 x73 ⟶ (x72 (x65 x73) ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . x6 x74 ⟶ x51 x73 x74 ⟶ x10 x73 ⟶ (x4 (x65 x73) x74 ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . (x11 x74 ⟶ False) ⟶ (x72 x73 ⟶ False) ⟶ x11 (x56 x73 x74) ⟶ False) ⟶ (∀ x73 . x15 x73 ⟶ (x16 (x67 x73) x73 ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . (x11 x74 ⟶ False) ⟶ (x72 x73 ⟶ False) ⟶ x11 (x56 x74 x73) ⟶ False) ⟶ (∀ x73 . (x2 (x43 x73) x73 ⟶ False) ⟶ False) ⟶ ((x15 x24 ⟶ False) ⟶ False) ⟶ ((x64 x42 ⟶ False) ⟶ False) ⟶ ((x10 x25 ⟶ False) ⟶ False) ⟶ ((x41 x40 ⟶ False) ⟶ False) ⟶ (∀ x73 . x15 x73 ⟶ (x2 (x26 x73) (x65 x73) ⟶ False) ⟶ False) ⟶ (∀ x73 . x41 x73 ⟶ (x2 (x39 x73) (x1 (x56 (x56 (x65 x73) (x65 x73)) (x65 x73))) ⟶ False) ⟶ False) ⟶ (∀ x73 . x41 x73 ⟶ (x57 (x39 x73) (x56 (x65 x73) (x65 x73)) (x65 x73) ⟶ False) ⟶ False) ⟶ (∀ x73 . x41 x73 ⟶ (x60 (x39 x73) ⟶ False) ⟶ False) ⟶ ((x72 x27 ⟶ False) ⟶ False) ⟶ (∀ x73 . x15 x73 ⟶ (x10 x73 ⟶ False) ⟶ False) ⟶ (∀ x73 . x64 x73 ⟶ (x15 x73 ⟶ False) ⟶ False) ⟶ (∀ x73 . x64 x73 ⟶ (x41 x73 ⟶ False) ⟶ False) ⟶ (∀ x73 . x41 x73 ⟶ (x10 x73 ⟶ False) ⟶ False) ⟶ (∀ x73 x74 x75 x76 . x60 x76 ⟶ x57 x76 (x56 x73 x73) x73 ⟶ x2 x76 (x1 (x56 (x56 x73 x73) x73)) ⟶ x2 x74 x73 ⟶ x2 x75 x73 ⟶ (x2 (x59 x73 x76 x74 x75) x73 ⟶ False) ⟶ False) ⟶ (∀ x73 . x15 x73 ⟶ (x2 (x67 x73) (x65 x73) ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . (x70 x74 ⟶ False) ⟶ x64 x74 ⟶ x2 x73 (x65 x74) ⟶ (x2 (x20 x74 x73) (x65 x74) ⟶ False) ⟶ False) ⟶ (∀ x73 x74 x75 . x41 x75 ⟶ x2 x73 (x65 x75) ⟶ x2 x74 (x65 x75) ⟶ (x2 (x66 x75 x73 x74) (x65 x75) ⟶ False) ⟶ False) ⟶ (∀ x73 . (x70 x73 ⟶ False) ⟶ x64 x73 ⟶ x38 x73 = x37 x73 ⟶ (x68 x73 ⟶ False) ⟶ False) ⟶ (∀ x73 . (x70 x73 ⟶ False) ⟶ x64 x73 ⟶ (x66 x73 (x37 x73) (x38 x73) = x67 x73 ⟶ False) ⟶ (x68 x73 ⟶ False) ⟶ False) ⟶ (∀ x73 . (x70 x73 ⟶ False) ⟶ x64 x73 ⟶ (x66 x73 (x38 x73) (x37 x73) = x67 x73 ⟶ False) ⟶ (x68 x73 ⟶ False) ⟶ False) ⟶ (∀ x73 . (x70 x73 ⟶ False) ⟶ x64 x73 ⟶ (x2 (x37 x73) (x65 x73) ⟶ False) ⟶ (x68 x73 ⟶ False) ⟶ False) ⟶ (∀ x73 . (x70 x73 ⟶ False) ⟶ x64 x73 ⟶ (x2 (x38 x73) (x65 x73) ⟶ False) ⟶ (x68 x73 ⟶ False) ⟶ False) ⟶ (∀ x73 x74 x75 . (x70 x75 ⟶ False) ⟶ x64 x75 ⟶ x68 x75 ⟶ x2 x73 (x65 x75) ⟶ x2 x74 (x65 x75) ⟶ x66 x75 x73 x74 = x67 x75 ⟶ x66 x75 x74 x73 = x67 x75 ⟶ (x73 = x74 ⟶ False) ⟶ False) ⟶ (∀ x73 . x15 x73 ⟶ (x67 x73 = x26 x73 ⟶ False) ⟶ False) ⟶ (∀ x73 . (x70 x73 ⟶ False) ⟶ x64 x73 ⟶ x66 x73 (x28 x73) (x28 x73) = x67 x73 ⟶ (x63 x73 ⟶ False) ⟶ False) ⟶ (∀ x73 . (x70 x73 ⟶ False) ⟶ x64 x73 ⟶ (x2 (x28 x73) (x65 x73) ⟶ False) ⟶ (x63 x73 ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . (x70 x74 ⟶ False) ⟶ x64 x74 ⟶ x63 x74 ⟶ x2 x73 (x65 x74) ⟶ (x66 x74 x73 x73 = x67 x74 ⟶ False) ⟶ False) ⟶ ((x71 = x27 ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . (x70 x74 ⟶ False) ⟶ x64 x74 ⟶ x2 x73 (x65 x74) ⟶ (x20 x74 x73 = x66 x74 (x67 x74) x73 ⟶ False) ⟶ False) ⟶ (∀ x73 . (x70 x73 ⟶ False) ⟶ x62 x73 ⟶ x69 x73 ⟶ x63 x73 ⟶ x68 x73 ⟶ x64 x73 ⟶ x66 x73 (x66 x73 (x36 x73) (x34 x73)) (x35 x73) = x66 x73 (x36 x73) (x66 x73 (x34 x73) (x35 x73)) ⟶ (x21 x73 ⟶ False) ⟶ False) ⟶ (∀ x73 . (x70 x73 ⟶ False) ⟶ x62 x73 ⟶ x69 x73 ⟶ x63 x73 ⟶ x68 x73 ⟶ x64 x73 ⟶ (x2 (x35 x73) (x65 x73) ⟶ False) ⟶ (x21 x73 ⟶ False) ⟶ False) ⟶ (∀ x73 . (x70 x73 ⟶ False) ⟶ x62 x73 ⟶ x69 x73 ⟶ x63 x73 ⟶ x68 x73 ⟶ x64 x73 ⟶ (x2 (x34 x73) (x65 x73) ⟶ False) ⟶ (x21 x73 ⟶ False) ⟶ False) ⟶ (∀ x73 . (x70 x73 ⟶ False) ⟶ x62 x73 ⟶ x69 x73 ⟶ x63 x73 ⟶ x68 x73 ⟶ x64 x73 ⟶ (x2 (x36 x73) (x65 x73) ⟶ False) ⟶ (x21 x73 ⟶ False) ⟶ False) ⟶ (∀ x73 x74 x75 x76 . (x70 x76 ⟶ False) ⟶ x62 x76 ⟶ x69 x76 ⟶ x63 x76 ⟶ x68 x76 ⟶ x64 x76 ⟶ x21 x76 ⟶ x2 x73 (x65 x76) ⟶ x2 x75 (x65 x76) ⟶ x2 x74 (x65 x76) ⟶ (x66 x76 (x66 x76 x73 x75) x74 = x66 x76 x73 (x66 x76 x75 x74) ⟶ False) ⟶ False) ⟶ (∀ x73 x74 x75 . x41 x75 ⟶ x2 x73 (x65 x75) ⟶ x2 x74 (x65 x75) ⟶ (x66 x75 x73 x74 = x59 (x65 x75) (x39 x75) x73 x74 ⟶ False) ⟶ False) ⟶ (∀ x73 . x10 x73 ⟶ x51 x73 x71 ⟶ (x70 x73 ⟶ False) ⟶ False) ⟶ (∀ x73 . x4 x73 x61 ⟶ (x49 x73 ⟶ False) ⟶ False) ⟶ (∀ x73 . x4 x73 x61 ⟶ x72 x73 ⟶ False) ⟶ (∀ x73 . x10 x73 ⟶ x70 x73 ⟶ (x51 x73 x71 ⟶ False) ⟶ False) ⟶ (∀ x73 . x72 x73 ⟶ (x4 x73 x71 ⟶ False) ⟶ False) ⟶ (∀ x73 . x10 x73 ⟶ (x44 x73 ⟶ False) ⟶ x50 x73 ⟶ False) ⟶ (∀ x73 . x4 x73 x71 ⟶ (x72 x73 ⟶ False) ⟶ False) ⟶ (∀ x73 . x10 x73 ⟶ x50 x73 ⟶ (x44 x73 ⟶ False) ⟶ False) ⟶ (∀ x73 . x33 x73 ⟶ x11 x73 ⟶ (x32 x73 ⟶ False) ⟶ False) ⟶ (∀ x73 . x10 x73 ⟶ (x44 x73 ⟶ False) ⟶ x44 x73 ⟶ False) ⟶ (∀ x73 . x10 x73 ⟶ (x44 x73 ⟶ False) ⟶ x70 x73 ⟶ False) ⟶ (∀ x73 . x32 x73 ⟶ (x11 x73 ⟶ False) ⟶ False) ⟶ (∀ x73 . x10 x73 ⟶ x70 x73 ⟶ (x44 x73 ⟶ False) ⟶ False) ⟶ (∀ x73 . x10 x73 ⟶ x70 x73 ⟶ (x70 x73 ⟶ False) ⟶ False) ⟶ (∀ x73 . x72 x73 ⟶ x8 x73 ⟶ (x54 x73 ⟶ False) ⟶ False) ⟶ (∀ x73 . x72 x73 ⟶ x8 x73 ⟶ (x8 x73 ⟶ False) ⟶ False) ⟶ (∀ x73 . x72 x73 ⟶ x8 x73 ⟶ (x31 x73 ⟶ False) ⟶ False) ⟶ (∀ x73 . x72 x73 ⟶ x8 x73 ⟶ (x8 x73 ⟶ False) ⟶ False) ⟶ (∀ x73 . x32 x73 ⟶ (x6 x73 ⟶ False) ⟶ False) ⟶ (∀ x73 . x10 x73 ⟶ (x50 x73 ⟶ False) ⟶ x70 x73 ⟶ False) ⟶ (∀ x73 x74 . x8 x74 ⟶ x2 x73 (x1 x74) ⟶ (x8 x73 ⟶ False) ⟶ False) ⟶ (∀ x73 . x72 x73 ⟶ (x6 x73 ⟶ False) ⟶ False) ⟶ (∀ x73 . x10 x73 ⟶ x70 x73 ⟶ (x50 x73 ⟶ False) ⟶ False) ⟶ (∀ x73 . x72 x73 ⟶ (x8 x73 ⟶ False) ⟶ False) ⟶ (∀ x73 . x6 x73 ⟶ (x33 x73 ⟶ False) ⟶ False) ⟶ (∀ x73 . x10 x73 ⟶ (x50 x73 ⟶ False) ⟶ x70 x73 ⟶ False) ⟶ (∀ x73 . x10 x73 ⟶ x51 x73 x61 ⟶ (x50 x73 ⟶ False) ⟶ False) ⟶ (∀ x73 . x10 x73 ⟶ x51 x73 x61 ⟶ x70 x73 ⟶ False) ⟶ (∀ x73 . x10 x73 ⟶ (x70 x73 ⟶ False) ⟶ x50 x73 ⟶ (x51 x73 x61 ⟶ False) ⟶ False) ⟶ (∀ x73 . (x72 x73 ⟶ False) ⟶ x49 x73 ⟶ (x4 x73 x61 ⟶ False) ⟶ False) ⟶ (∀ x73 x74 . x0 x73 x74 ⟶ x0 x74 x73 ⟶ False) ⟶ (∀ x73 . x2 x73 (x65 x29) ⟶ (x20 x29 x73 = x73 ⟶ False) ⟶ (x21 x29 ⟶ False) ⟶ False) ⟶ (x21 x29 ⟶ x20 x29 x30 = x30 ⟶ False) ⟶ (x21 x29 ⟶ (x2 x30 (x65 x29) ⟶ False) ⟶ False) ⟶ ((x64 x29 ⟶ False) ⟶ False) ⟶ ((x68 x29 ⟶ False) ⟶ False) ⟶ ((x63 x29 ⟶ False) ⟶ False) ⟶ ((x69 x29 ⟶ False) ⟶ False) ⟶ ((x62 x29 ⟶ False) ⟶ False) ⟶ (x70 x29 ⟶ False) ⟶ False

as obj
-

as prop
4cea3..

theory
HotG

stx
60349..

address
TMMRE..