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 : ι → ι → ι . ((x39 x37 (x38 x37) = x36 ⟶ False) ⟶ False) ⟶ ((x0 x37 x1 = x38 x37 ⟶ False) ⟶ False) ⟶ ((x0 (x38 x1) (x38 x1) = x36 ⟶ False) ⟶ False) ⟶ ((x38 (x38 x1) = x1 ⟶ False) ⟶ False) ⟶ ((x35 (x38 x1) x37 = x38 x1 ⟶ False) ⟶ False) ⟶ ((x0 (x38 x37) (x38 x1) = x37 ⟶ False) ⟶ False) ⟶ ((x0 x1 x1 = x36 ⟶ False) ⟶ False) ⟶ ((x38 x1 = x38 x1 ⟶ False) ⟶ False) ⟶ ((x35 x1 x37 = x1 ⟶ False) ⟶ False) ⟶ ((x0 (x38 x37) x37 = x38 x1 ⟶ False) ⟶ False) ⟶ ((x0 x37 (x38 x37) = x1 ⟶ False) ⟶ False) ⟶ ((x2 x37 (x38 x37) = x38 x37 ⟶ False) ⟶ False) ⟶ ((x0 (x38 x37) (x38 x37) = x36 ⟶ False) ⟶ False) ⟶ ((x0 x37 x37 = x36 ⟶ False) ⟶ False) ⟶ ((x38 (x38 x37) = x37 ⟶ False) ⟶ False) ⟶ ((x35 x37 x37 = x37 ⟶ False) ⟶ False) ⟶ ((x38 x37 = x38 x37 ⟶ False) ⟶ False) ⟶ (x3 x1 ⟶ False) ⟶ (x3 x37 ⟶ False) ⟶ ((x3 x36 ⟶ False) ⟶ False) ⟶ (∀ x40 x41 . x34 x41 ⟶ x34 x40 ⟶ (x31 x41 x40 = x33 (x32 x41 x40) ⟶ False) ⟶ False) ⟶ (∀ x40 x41 . x34 x41 ⟶ x34 x40 ⟶ (x32 x41 x40 = x33 (x4 (x33 x41) (x33 x40)) ⟶ False) ⟶ False) ⟶ (∀ x40 . x34 x40 ⟶ (x33 x40 = x0 x37 x40 ⟶ False) ⟶ False) ⟶ ((x38 (x2 (x38 x37) x1) = x2 x37 x1 ⟶ False) ⟶ False) ⟶ ((x38 (x2 x37 x1) = x2 (x38 x37) x1 ⟶ False) ⟶ False) ⟶ ((x38 x36 = x36 ⟶ False) ⟶ False) ⟶ ((x35 (x2 (x38 x37) x1) (x38 x1) = x37 ⟶ False) ⟶ False) ⟶ ((x35 (x2 (x38 x37) x1) x1 = x38 x37 ⟶ False) ⟶ False) ⟶ ((x35 (x2 (x38 x37) x1) x37 = x2 (x38 x37) x1 ⟶ False) ⟶ False) ⟶ ((x35 (x2 x37 x1) (x38 x1) = x38 x37 ⟶ False) ⟶ False) ⟶ ((x35 (x2 x37 x1) x1 = x37 ⟶ False) ⟶ False) ⟶ ((x35 (x2 x37 x1) x37 = x2 x37 x1 ⟶ False) ⟶ False) ⟶ ((x35 (x2 x37 x1) x36 = x36 ⟶ False) ⟶ False) ⟶ ((x35 (x38 x1) (x2 (x38 x37) x1) = x37 ⟶ False) ⟶ False) ⟶ ((x35 (x38 x1) (x2 x37 x1) = x38 x37 ⟶ False) ⟶ False) ⟶ ((x35 (x38 x1) x36 = x36 ⟶ False) ⟶ False) ⟶ ((x35 x1 (x2 (x38 x37) x1) = x38 x37 ⟶ False) ⟶ False) ⟶ ((x35 x1 (x2 x37 x1) = x37 ⟶ False) ⟶ False) ⟶ ((x35 x1 x36 = x36 ⟶ False) ⟶ False) ⟶ ((x35 x37 (x2 (x38 x37) x1) = x2 (x38 x37) x1 ⟶ False) ⟶ False) ⟶ ((x35 x37 (x2 x37 x1) = x2 x37 x1 ⟶ False) ⟶ False) ⟶ ((x35 x37 (x38 x1) = x38 x1 ⟶ False) ⟶ False) ⟶ ((x35 x37 x1 = x1 ⟶ False) ⟶ False) ⟶ ((x35 x37 x36 = x36 ⟶ False) ⟶ False) ⟶ ((x35 x36 (x2 x37 x1) = x36 ⟶ False) ⟶ False) ⟶ ((x35 x36 (x38 x1) = x36 ⟶ False) ⟶ False) ⟶ ((x35 x36 x1 = x36 ⟶ False) ⟶ False) ⟶ ((x35 x36 x37 = x36 ⟶ False) ⟶ False) ⟶ ((x35 x36 x36 = x36 ⟶ False) ⟶ False) ⟶ ((x2 (x38 x1) x1 = x38 x37 ⟶ False) ⟶ False) ⟶ ((x2 (x38 x37) x1 = x2 (x38 x37) x1 ⟶ False) ⟶ False) ⟶ ((x2 (x38 x37) x37 = x38 x37 ⟶ False) ⟶ False) ⟶ ((x2 x1 x1 = x37 ⟶ False) ⟶ False) ⟶ ((x2 x1 x37 = x1 ⟶ False) ⟶ False) ⟶ ((x2 x37 (x2 (x38 x37) x1) = x38 x1 ⟶ False) ⟶ False) ⟶ ((x2 x37 (x2 x37 x1) = x1 ⟶ False) ⟶ False) ⟶ ((x2 x37 (x38 x1) = x2 (x38 x37) x1 ⟶ False) ⟶ False) ⟶ ((x2 x37 x1 = x2 x37 x1 ⟶ False) ⟶ False) ⟶ ((x2 x37 x37 = x37 ⟶ False) ⟶ False) ⟶ ((x0 (x2 (x38 x37) x1) (x2 (x38 x37) x1) = x36 ⟶ False) ⟶ False) ⟶ ((x0 (x2 (x38 x37) x1) (x2 x37 x1) = x38 x37 ⟶ False) ⟶ False) ⟶ ((x0 (x2 (x38 x37) x1) (x38 x37) = x2 x37 x1 ⟶ False) ⟶ False) ⟶ ((x0 (x2 (x38 x37) x1) x36 = x2 (x38 x37) x1 ⟶ False) ⟶ False) ⟶ ((x0 (x2 x37 x1) (x2 (x38 x37) x1) = x37 ⟶ False) ⟶ False) ⟶ ((x0 (x2 x37 x1) (x2 x37 x1) = x36 ⟶ False) ⟶ False) ⟶ ((x0 (x2 x37 x1) x37 = x2 (x38 x37) x1 ⟶ False) ⟶ False) ⟶ ((x0 (x2 x37 x1) x36 = x2 x37 x1 ⟶ False) ⟶ False) ⟶ ((x0 (x38 x1) (x38 x37) = x38 x37 ⟶ False) ⟶ False) ⟶ ((x0 (x38 x1) x36 = x38 x1 ⟶ False) ⟶ False) ⟶ ((x0 (x38 x37) (x2 (x38 x37) x1) = x2 (x38 x37) x1 ⟶ False) ⟶ False) ⟶ ((x0 (x38 x37) x36 = x38 x37 ⟶ False) ⟶ False) ⟶ ((x0 x1 x37 = x37 ⟶ False) ⟶ False) ⟶ ((x0 x1 x36 = x1 ⟶ False) ⟶ False) ⟶ ((x0 x37 (x2 x37 x1) = x2 x37 x1 ⟶ False) ⟶ False) ⟶ ((x0 x37 x36 = x37 ⟶ False) ⟶ False) ⟶ ((x0 x36 (x2 (x38 x37) x1) = x2 x37 x1 ⟶ False) ⟶ False) ⟶ ((x0 x36 (x2 x37 x1) = x2 (x38 x37) x1 ⟶ False) ⟶ False) ⟶ ((x0 x36 (x38 x1) = x1 ⟶ False) ⟶ False) ⟶ ((x0 x36 (x38 x37) = x37 ⟶ False) ⟶ False) ⟶ ((x0 x36 x1 = x38 x1 ⟶ False) ⟶ False) ⟶ ((x0 x36 x37 = x38 x37 ⟶ False) ⟶ False) ⟶ ((x0 x36 x36 = x36 ⟶ False) ⟶ False) ⟶ ((x39 (x2 (x38 x37) x1) (x2 (x38 x37) x1) = x38 x37 ⟶ False) ⟶ False) ⟶ ((x39 (x2 (x38 x37) x1) (x2 x37 x1) = x36 ⟶ False) ⟶ False) ⟶ ((x39 (x2 (x38 x37) x1) x37 = x2 x37 x1 ⟶ False) ⟶ False) ⟶ ((x39 (x2 x37 x1) (x2 (x38 x37) x1) = x36 ⟶ False) ⟶ False) ⟶ ((x39 (x2 x37 x1) (x2 x37 x1) = x37 ⟶ False) ⟶ False) ⟶ ((x39 (x2 x37 x1) (x38 x37) = x2 (x38 x37) x1 ⟶ False) ⟶ False) ⟶ ((x39 (x2 x37 x1) x36 = x2 x37 x1 ⟶ False) ⟶ False) ⟶ ((x39 (x38 x1) x1 = x36 ⟶ False) ⟶ False) ⟶ ((x39 (x38 x1) x37 = x38 x37 ⟶ False) ⟶ False) ⟶ ((x39 (x38 x37) (x2 x37 x1) = x2 (x38 x37) x1 ⟶ False) ⟶ False) ⟶ ((x39 (x38 x37) (x38 x37) = x38 x1 ⟶ False) ⟶ False) ⟶ ((x39 (x38 x37) x1 = x37 ⟶ False) ⟶ False) ⟶ ((x39 (x38 x37) x37 = x36 ⟶ False) ⟶ False) ⟶ ((x39 (x38 x37) x36 = x38 x37 ⟶ False) ⟶ False) ⟶ ((x39 x1 (x38 x1) = x36 ⟶ False) ⟶ False) ⟶ ((x39 x1 (x38 x37) = x37 ⟶ False) ⟶ False) ⟶ ((x39 x1 x36 = x1 ⟶ False) ⟶ False) ⟶ ((x39 x37 (x2 (x38 x37) x1) = x2 x37 x1 ⟶ False) ⟶ False) ⟶ ((x39 x37 (x38 x1) = x38 x37 ⟶ False) ⟶ False) ⟶ ((x39 x37 x37 = x1 ⟶ False) ⟶ False) ⟶ ((x39 x37 x36 = x37 ⟶ False) ⟶ False) ⟶ ((x39 x36 (x2 (x38 x37) x1) = x2 (x38 x37) x1 ⟶ False) ⟶ False) ⟶ ((x39 x36 (x2 x37 x1) = x2 x37 x1 ⟶ False) ⟶ False) ⟶ ((x39 x36 (x38 x1) = x38 x1 ⟶ False) ⟶ False) ⟶ ((x39 x36 (x38 x37) = x38 x37 ⟶ False) ⟶ False) ⟶ ((x39 x36 x1 = x1 ⟶ False) ⟶ False) ⟶ ((x39 x36 x37 = x37 ⟶ False) ⟶ False) ⟶ ((x39 x36 x36 = x36 ⟶ False) ⟶ False) ⟶ ((x34 x30 ⟶ False) ⟶ False) ⟶ (∀ x40 x41 . x34 x41 ⟶ x34 x40 ⟶ (x34 (x31 x41 x40) ⟶ False) ⟶ False) ⟶ (∀ x40 x41 . x34 x41 ⟶ x34 x40 ⟶ (x34 (x32 x41 x40) ⟶ False) ⟶ False) ⟶ (∀ x40 . x34 x40 ⟶ (x5 x40 ⟶ False) ⟶ False) ⟶ (∀ x40 . x29 x40 ⟶ (x29 (x38 x40) ⟶ False) ⟶ False) ⟶ (∀ x40 . x34 x40 ⟶ (x34 (x33 x40) ⟶ False) ⟶ False) ⟶ (∀ x40 x41 . x34 x41 ⟶ x34 x40 ⟶ (x31 x41 x40 = x31 x40 x41 ⟶ False) ⟶ False) ⟶ (∀ x40 x41 . x34 x41 ⟶ x34 x40 ⟶ (x32 x41 x41 = x41 ⟶ False) ⟶ False) ⟶ (∀ x40 x41 . x34 x41 ⟶ x34 x40 ⟶ (x32 x41 x40 = x32 x40 x41 ⟶ False) ⟶ False) ⟶ (∀ x40 . x29 x40 ⟶ (x38 (x38 x40) = x40 ⟶ False) ⟶ False) ⟶ (∀ x40 x41 . x29 x41 ⟶ x29 x40 ⟶ (x35 x41 x40 = x35 x40 x41 ⟶ False) ⟶ False) ⟶ (∀ x40 . x34 x40 ⟶ (x33 (x33 x40) = x40 ⟶ False) ⟶ False) ⟶ (∀ x40 x41 . x29 x41 ⟶ x29 x40 ⟶ (x39 x41 x40 = x39 x40 x41 ⟶ False) ⟶ False) ⟶ (∀ x40 x41 . x34 x41 ⟶ x34 x40 ⟶ (x4 x41 x40 = x35 x41 x40 ⟶ False) ⟶ False) ⟶ (∀ x40 x41 . x3 x41 ⟶ (x41 = x40 ⟶ False) ⟶ x3 x40 ⟶ False) ⟶ (∀ x40 x41 . x6 x40 x41 ⟶ x3 x41 ⟶ False) ⟶ (∀ x40 . x3 x40 ⟶ (x40 = x28 ⟶ False) ⟶ False) ⟶ (∀ x40 . x29 x40 ⟶ (x2 x40 x37 = x40 ⟶ False) ⟶ False) ⟶ (∀ x40 . x29 x40 ⟶ (x35 x37 x40 = x40 ⟶ False) ⟶ False) ⟶ (∀ x40 x41 . x29 x41 ⟶ x29 x40 ⟶ (x0 (x38 x41) (x38 x40) = x0 x40 x41 ⟶ False) ⟶ False) ⟶ (∀ x40 x41 . x29 x41 ⟶ x29 x40 ⟶ (x39 (x38 x41) (x38 x40) = x38 (x39 x41 x40) ⟶ False) ⟶ False) ⟶ (∀ x40 x41 x42 . x29 x42 ⟶ x29 x40 ⟶ x29 x41 ⟶ (x35 (x35 x42 x40) x41 = x35 x42 (x35 x40 x41) ⟶ False) ⟶ False) ⟶ (∀ x40 x41 x42 . x29 x42 ⟶ x29 x40 ⟶ x29 x41 ⟶ (x39 (x39 x42 x40) x41 = x39 x42 (x39 x40 x41) ⟶ False) ⟶ False) ⟶ (∀ x40 x41 x42 . x29 x42 ⟶ x29 x40 ⟶ x29 x41 ⟶ (x35 (x39 x42 x40) x41 = x39 (x35 x42 x41) (x35 x40 x41) ⟶ False) ⟶ False) ⟶ (∀ x40 x41 x42 . x29 x42 ⟶ x29 x40 ⟶ x29 x41 ⟶ (x35 x42 (x2 x40 x41) = x2 (x35 x42 x40) x41 ⟶ False) ⟶ False) ⟶ (∀ x40 . x29 x40 ⟶ (x35 x40 (x38 x37) = x38 x40 ⟶ False) ⟶ False) ⟶ (∀ x40 x41 . x29 x41 ⟶ x29 x40 ⟶ (x39 x41 (x38 x40) = x0 x41 x40 ⟶ False) ⟶ False) ⟶ (∀ x40 x41 . x34 x41 ⟶ x34 x40 ⟶ (x34 (x4 x41 x40) ⟶ False) ⟶ False) ⟶ (∀ x40 . x3 x40 ⟶ (x27 x40 ⟶ False) ⟶ False) ⟶ (∀ x40 . x5 x40 ⟶ (x7 x40 ⟶ False) ⟶ False) ⟶ (∀ x40 . x3 x40 ⟶ (x26 x40 ⟶ False) ⟶ False) ⟶ (∀ x40 . x3 x40 ⟶ (x8 x40 ⟶ False) ⟶ False) ⟶ (∀ x40 x41 . x34 x41 ⟶ x34 x40 ⟶ (x4 x41 x41 = x41 ⟶ False) ⟶ False) ⟶ (∀ x40 x41 . x34 x41 ⟶ x34 x40 ⟶ (x4 x41 x40 = x4 x40 x41 ⟶ False) ⟶ False) ⟶ ((x28 = x25 ⟶ False) ⟶ False) ⟶ (∀ x40 x41 . x6 x41 x40 ⟶ (x9 x41 x40 ⟶ False) ⟶ False) ⟶ ((x27 x24 ⟶ False) ⟶ False) ⟶ (x3 x24 ⟶ False) ⟶ ((x7 x23 ⟶ False) ⟶ False) ⟶ (∀ x40 x41 . x7 x41 ⟶ x7 x40 ⟶ (x7 (x2 x41 x40) ⟶ False) ⟶ False) ⟶ (∀ x40 x41 . x7 x41 ⟶ x7 x40 ⟶ (x7 (x0 x41 x40) ⟶ False) ⟶ False) ⟶ (∀ x40 x41 . x7 x41 ⟶ x7 x40 ⟶ (x7 (x35 x41 x40) ⟶ False) ⟶ False) ⟶ (∀ x40 x41 . x7 x41 ⟶ x7 x40 ⟶ (x7 (x39 x41 x40) ⟶ False) ⟶ False) ⟶ (∀ x40 . x7 x40 ⟶ (x7 (x38 x40) ⟶ False) ⟶ False) ⟶ (∀ x40 . x7 x40 ⟶ (x29 (x38 x40) ⟶ False) ⟶ False) ⟶ (∀ x40 . x7 x40 ⟶ (x10 x40 ⟶ False) ⟶ False) ⟶ (∀ x40 . x7 x40 ⟶ (x29 x40 ⟶ False) ⟶ False) ⟶ (∀ x40 x41 . x6 x40 x41 ⟶ x6 x41 x40 ⟶ False) ⟶ (∀ x40 x41 . x9 x40 x41 ⟶ (x3 x41 ⟶ False) ⟶ (x6 x40 x41 ⟶ False) ⟶ False) ⟶ ((x7 x11 ⟶ False) ⟶ False) ⟶ ((x10 x11 ⟶ False) ⟶ False) ⟶ ((x29 x11 ⟶ False) ⟶ False) ⟶ ((x3 x11 ⟶ False) ⟶ False) ⟶ (∀ x40 x41 . x27 x41 ⟶ x9 x40 x41 ⟶ (x8 x40 ⟶ False) ⟶ False) ⟶ (∀ x40 x41 . x27 x41 ⟶ x9 x40 x41 ⟶ (x22 x40 ⟶ False) ⟶ False) ⟶ ((x3 x25 ⟶ False) ⟶ False) ⟶ (∀ x40 . (x9 (x21 x40) x40 ⟶ False) ⟶ False) ⟶ ((x8 x12 ⟶ False) ⟶ False) ⟶ ((x22 x12 ⟶ False) ⟶ False) ⟶ (∀ x40 . x3 x40 ⟶ x22 x40 ⟶ x8 x40 ⟶ (x13 x40 ⟶ False) ⟶ False) ⟶ (∀ x40 . x3 x40 ⟶ x22 x40 ⟶ x8 x40 ⟶ (x8 x40 ⟶ False) ⟶ False) ⟶ (∀ x40 . x3 x40 ⟶ x22 x40 ⟶ x8 x40 ⟶ (x22 x40 ⟶ False) ⟶ False) ⟶ (∀ x40 . x3 x40 ⟶ x22 x40 ⟶ x8 x40 ⟶ (x20 x40 ⟶ False) ⟶ False) ⟶ (∀ x40 . x3 x40 ⟶ x22 x40 ⟶ x8 x40 ⟶ (x8 x40 ⟶ False) ⟶ False) ⟶ (∀ x40 . x3 x40 ⟶ x22 x40 ⟶ x8 x40 ⟶ (x22 x40 ⟶ False) ⟶ False) ⟶ (x13 x14 ⟶ False) ⟶ ((x8 x14 ⟶ False) ⟶ False) ⟶ ((x22 x14 ⟶ False) ⟶ False) ⟶ ((x20 x19 ⟶ False) ⟶ False) ⟶ ((x8 x19 ⟶ False) ⟶ False) ⟶ ((x22 x19 ⟶ False) ⟶ False) ⟶ (∀ x40 . x22 x40 ⟶ x8 x40 ⟶ (x13 x40 ⟶ False) ⟶ (x8 x40 ⟶ False) ⟶ False) ⟶ (∀ x40 . x22 x40 ⟶ x8 x40 ⟶ (x13 x40 ⟶ False) ⟶ (x22 x40 ⟶ False) ⟶ False) ⟶ (∀ x40 . x22 x40 ⟶ x8 x40 ⟶ (x13 x40 ⟶ False) ⟶ x15 x40 ⟶ False) ⟶ (∀ x40 . x15 x40 ⟶ x22 x40 ⟶ x8 x40 ⟶ (x13 x40 ⟶ False) ⟶ False) ⟶ (∀ x40 . x15 x40 ⟶ x22 x40 ⟶ x8 x40 ⟶ (x8 x40 ⟶ False) ⟶ False) ⟶ (∀ x40 . x15 x40 ⟶ x22 x40 ⟶ x8 x40 ⟶ (x22 x40 ⟶ False) ⟶ False) ⟶ (x31 x18 (x32 x17 x16) = x33 (x32 (x32 x18 x17) x16) ⟶ False) ⟶ ((x34 x16 ⟶ False) ⟶ False) ⟶ ((x34 x17 ⟶ False) ⟶ False) ⟶ ((x34 x18 ⟶ False) ⟶ False) ⟶ False

as obj
-

as prop
54bb5..

theory
HotG

stx
d2a71..

address
TMUKQ..