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

as obj
-

as prop
55aff..

theory
HotG

stx
c60cd..

address
TMJab..