Proofgold Term Root Disambiguation

∀ x0 x1 x2 . equip (setsum (setsum (setprod 265be.. (setprod (setexp x0 50a6b..) (setprod (setexp x1 50a6b..) (setexp x2 50a6b..)))) (setsum (setprod 265be.. (setprod (setexp x0 50a6b..) (setprod (setexp x1 50a6b..) (setexp x2 33cc2..)))) (setsum (setprod 265be.. (setprod (setexp x0 50a6b..) (setprod (setexp x1 50a6b..) x2))) (setsum (setprod 265be.. (setprod (setexp x0 50a6b..) (setexp x1 50a6b..))) (setsum (setprod 265be.. (setprod (setexp x0 50a6b..) (setprod (setexp x1 33cc2..) (setexp x2 50a6b..)))) (setsum (setprod 265be.. (setprod (setexp x0 50a6b..) (setprod (setexp x1 33cc2..) (setexp x2 33cc2..)))) (setsum (setprod 265be.. (setprod (setexp x0 50a6b..) (setprod (setexp x1 33cc2..) x2))) (setsum (setprod 265be.. (setprod (setexp x0 50a6b..) (setexp x1 33cc2..))) (setsum (setprod 265be.. (setprod (setexp x0 50a6b..) (setprod x1 (setexp x2 50a6b..)))) (setsum (setprod 265be.. (setprod (setexp x0 50a6b..) (setprod x1 (setexp x2 33cc2..)))) (setsum (setprod 265be.. (setprod (setexp x0 50a6b..) (setprod x1 x2))) (setsum (setprod 265be.. (setprod (setexp x0 50a6b..) x1)) (setsum (setprod 265be.. (setprod (setexp x0 50a6b..) (setexp x2 50a6b..))) (setsum (setprod 265be.. (setprod (setexp x0 50a6b..) (setexp x2 33cc2..))) (setsum (setprod 265be.. (setprod (setexp x0 50a6b..) x2)) (setsum (setprod 265be.. (setexp x0 50a6b..)) (setsum (setprod 265be.. (setprod (setexp x0 33cc2..) (setprod (setexp x1 50a6b..) (setexp x2 50a6b..)))) (setsum (setprod 265be.. (setprod (setexp x0 33cc2..) (setprod (setexp x1 50a6b..) (setexp x2 33cc2..)))) (setsum (setprod 265be.. (setprod (setexp x0 33cc2..) (setprod (setexp x1 50a6b..) x2))) (setsum (setprod 265be.. (setprod (setexp x0 33cc2..) (setexp x1 50a6b..))) (setsum (setprod 265be.. (setprod (setexp x0 33cc2..) (setprod (setexp x1 33cc2..) (setexp x2 50a6b..)))) (setsum (setprod 265be.. (setprod (setexp x0 33cc2..) (setprod (setexp x1 33cc2..) (setexp x2 33cc2..)))) (setsum (setprod 265be.. (setprod (setexp x0 33cc2..) (setprod (setexp x1 33cc2..) x2))) (setsum (setprod 265be.. (setprod (setexp x0 33cc2..) (setexp x1 33cc2..))) (setsum (setprod 265be.. (setprod (setexp x0 33cc2..) (setprod x1 (setexp x2 50a6b..)))) (setsum (setprod 265be.. (setprod (setexp x0 33cc2..) (setprod x1 (setexp x2 33cc2..)))) (setsum (setprod 265be.. (setprod (setexp x0 33cc2..) (setprod x1 x2))) (setsum (setprod 265be.. (setprod (setexp x0 33cc2..) x1)) (setsum (setprod 265be.. (setprod (setexp x0 33cc2..) (setexp x2 50a6b..))) (setsum (setprod 265be.. (setprod (setexp x0 33cc2..) (setexp x2 33cc2..))) (setsum (setprod 265be.. (setprod (setexp x0 33cc2..) x2)) (setsum (setprod 265be.. (setexp x0 33cc2..)) (setsum (setprod 265be.. (setprod x0 (setprod (setexp x1 50a6b..) (setexp x2 50a6b..)))) (setsum (setprod 265be.. (setprod x0 (setprod (setexp x1 50a6b..) (setexp x2 33cc2..)))) (setsum (setprod 265be.. (setprod x0 (setprod (setexp x1 50a6b..) x2))) (setsum (setprod 265be.. (setprod x0 (setexp x1 50a6b..))) (setsum (setprod 265be.. (setprod x0 (setprod (setexp x1 33cc2..) (setexp x2 50a6b..)))) (setsum (setprod 265be.. (setprod x0 (setprod (setexp x1 33cc2..) (setexp x2 33cc2..)))) (setsum (setprod 265be.. (setprod x0 (setprod (setexp x1 33cc2..) x2))) (setsum (setprod 265be.. (setprod x0 (setexp x1 33cc2..))) (setsum (setprod 265be.. (setprod x0 (setprod x1 (setexp x2 50a6b..)))) (setsum (setprod 265be.. (setprod x0 (setprod x1 (setexp x2 33cc2..)))) (setsum (setprod 265be.. (setprod x0 (setprod x1 x2))) (setsum (setprod 265be.. (setprod x0 x1)) (setsum (setprod 265be.. (setprod x0 (setexp x2 50a6b..))) (setsum (setprod 265be.. (setprod x0 (setexp x2 33cc2..))) (setsum (setprod 265be.. (setprod x0 x2)) (setsum (setprod 265be.. x0) (setsum (setprod 265be.. (setprod (setexp x1 50a6b..) (setexp x2 50a6b..))) (setsum (setprod 265be.. (setprod (setexp x1 50a6b..) (setexp x2 33cc2..))) (setsum (setprod 265be.. (setprod (setexp x1 50a6b..) x2)) (setsum (setprod 265be.. (setexp x1 50a6b..)) (setsum (setprod 265be.. (setprod (setexp x1 33cc2..) (setexp x2 50a6b..))) (setsum (setprod 265be.. (setprod (setexp x1 33cc2..) (setexp x2 33cc2..))) (setsum (setprod 265be.. (setprod (setexp x1 33cc2..) x2)) (setsum (setprod 265be.. (setexp x1 33cc2..)) (setsum (setprod 265be.. (setprod x1 (setexp x2 50a6b..))) (setsum (setprod 265be.. (setprod x1 (setexp x2 33cc2..))) (setsum (setprod 265be.. (setprod x1 x2)) (setsum (setprod 265be.. x1) (setsum (setprod 265be.. (setexp x2 50a6b..)) (setsum (setprod 265be.. (setexp x2 33cc2..)) (setsum (setprod 265be.. x2) 265be..))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) 6a551..) (setsum (setprod 265be.. (setprod (setexp x0 50a6b..) (setprod (setexp x1 50a6b..) (setexp x2 50a6b..)))) (setsum (setprod 265be.. (setprod (setexp x0 50a6b..) (setprod (setexp x1 50a6b..) (setexp x2 33cc2..)))) (setsum (setprod 265be.. (setprod (setexp x0 50a6b..) (setprod (setexp x1 50a6b..) x2))) (setsum (setprod 265be.. (setprod (setexp x0 50a6b..) (setexp x1 50a6b..))) (setsum (setprod 265be.. (setprod (setexp x0 50a6b..) (setprod (setexp x1 33cc2..) (setexp x2 50a6b..)))) (setsum (setprod 265be.. (setprod (setexp x0 50a6b..) (setprod (setexp x1 33cc2..) (setexp x2 33cc2..)))) (setsum (setprod 265be.. (setprod (setexp x0 50a6b..) (setprod (setexp x1 33cc2..) x2))) (setsum (setprod 265be.. (setprod (setexp x0 50a6b..) (setexp x1 33cc2..))) (setsum (setprod 265be.. (setprod (setexp x0 50a6b..) (setprod x1 (setexp x2 50a6b..)))) (setsum (setprod 265be.. (setprod (setexp x0 50a6b..) (setprod x1 (setexp x2 33cc2..)))) (setsum (setprod 265be.. (setprod (setexp x0 50a6b..) (setprod x1 x2))) (setsum (setprod 265be.. (setprod (setexp x0 50a6b..) x1)) (setsum (setprod 265be.. (setprod (setexp x0 50a6b..) (setexp x2 50a6b..))) (setsum (setprod 265be.. (setprod (setexp x0 50a6b..) (setexp x2 33cc2..))) (setsum (setprod 265be.. (setprod (setexp x0 50a6b..) x2)) (setsum (setprod 265be.. (setexp x0 50a6b..)) (setsum (setprod 265be.. (setprod (setexp x0 33cc2..) (setprod (setexp x1 50a6b..) (setexp x2 50a6b..)))) (setsum (setprod 265be.. (setprod (setexp x0 33cc2..) (setprod (setexp x1 50a6b..) (setexp x2 33cc2..)))) (setsum (setprod 265be.. (setprod (setexp x0 33cc2..) (setprod (setexp x1 50a6b..) x2))) (setsum (setprod 265be.. (setprod (setexp x0 33cc2..) (setexp x1 50a6b..))) (setsum (setprod 265be.. (setprod (setexp x0 33cc2..) (setprod (setexp x1 33cc2..) (setexp x2 50a6b..)))) (setsum (setprod 265be.. (setprod (setexp x0 33cc2..) (setprod (setexp x1 33cc2..) (setexp x2 33cc2..)))) (setsum (setprod 265be.. (setprod (setexp x0 33cc2..) (setprod (setexp x1 33cc2..) x2))) (setsum (setprod 265be.. (setprod (setexp x0 33cc2..) (setexp x1 33cc2..))) (setsum (setprod 265be.. (setprod (setexp x0 33cc2..) (setprod x1 (setexp x2 50a6b..)))) (setsum (setprod 265be.. (setprod (setexp x0 33cc2..) (setprod x1 (setexp x2 33cc2..)))) (setsum (setprod 265be.. (setprod (setexp x0 33cc2..) (setprod x1 x2))) (setsum (setprod 265be.. (setprod (setexp x0 33cc2..) x1)) (setsum (setprod 265be.. (setprod (setexp x0 33cc2..) (setexp x2 50a6b..))) (setsum (setprod 265be.. (setprod (setexp x0 33cc2..) (setexp x2 33cc2..))) (setsum (setprod 265be.. (setprod (setexp x0 33cc2..) x2)) (setsum (setprod 265be.. (setexp x0 33cc2..)) (setsum (setprod 265be.. (setprod x0 (setprod (setexp x1 50a6b..) (setexp x2 50a6b..)))) (setsum (setprod 265be.. (setprod x0 (setprod (setexp x1 50a6b..) (setexp x2 33cc2..)))) (setsum (setprod 265be.. (setprod x0 (setprod (setexp x1 50a6b..) x2))) (setsum (setprod 265be.. (setprod x0 (setexp x1 50a6b..))) (setsum (setprod 265be.. (setprod x0 (setprod (setexp x1 33cc2..) (setexp x2 50a6b..)))) (setsum (setprod 265be.. (setprod x0 (setprod (setexp x1 33cc2..) (setexp x2 33cc2..)))) (setsum (setprod 265be.. (setprod x0 (setprod (setexp x1 33cc2..) x2))) (setsum (setprod 265be.. (setprod x0 (setexp x1 33cc2..))) (setsum (setprod 265be.. (setprod x0 (setprod x1 (setexp x2 50a6b..)))) (setsum (setprod 265be.. (setprod x0 (setprod x1 (setexp x2 33cc2..)))) (setsum (setprod 265be.. (setprod x0 (setprod x1 x2))) (setsum (setprod 265be.. (setprod x0 x1)) (setsum (setprod 265be.. (setprod x0 (setexp x2 50a6b..))) (setsum (setprod 265be.. (setprod x0 (setexp x2 33cc2..))) (setsum (setprod 265be.. (setprod x0 x2)) (setsum (setprod 265be.. x0) (setsum (setprod 265be.. (setprod (setexp x1 50a6b..) (setexp x2 50a6b..))) (setsum (setprod 265be.. (setprod (setexp x1 50a6b..) (setexp x2 33cc2..))) (setsum (setprod 265be.. (setprod (setexp x1 50a6b..) x2)) (setsum (setprod 265be.. (setexp x1 50a6b..)) (setsum (setprod 265be.. (setprod (setexp x1 33cc2..) (setexp x2 50a6b..))) (setsum (setprod 265be.. (setprod (setexp x1 33cc2..) (setexp x2 33cc2..))) (setsum (setprod 265be.. (setprod (setexp x1 33cc2..) x2)) (setsum (setprod 265be.. (setexp x1 33cc2..)) (setsum (setprod 265be.. (setprod x1 (setexp x2 50a6b..))) (setsum (setprod 265be.. (setprod x1 (setexp x2 33cc2..))) (setsum (setprod 265be.. (setprod x1 x2)) (setsum (setprod 265be.. x1) (setsum (setprod 265be.. (setexp x2 50a6b..)) (setsum (setprod 265be.. (setexp x2 33cc2..)) (setsum (setprod 265be.. x2) 265be..))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ⟶ False

as obj
-

as prop
13a2e..

theory
HF

stx
7bbfe..

address
TMa6U..