Search for blocks/addresses/...

Proofgold Term Root Disambiguation

(∀ x0 x1 x2 . equip_mod (setsum (setsum (setprod (binrep (Power (Power (Power 0))) 0) (setprod (setexp x0 (binrep (Power (Power 0)) 0)) (setprod (setexp x1 (binrep (Power (Power 0)) 0)) (setexp x2 (binrep (Power (Power 0)) 0))))) (setsum (setprod (binrep (binrep (binrep (Power (binrep (Power (Power 0)) 0)) (Power (Power 0))) (Power 0)) 0) (setprod (setexp x0 (binrep (Power (Power 0)) 0)) (setprod (setexp x1 (binrep (Power (Power 0)) 0)) (setexp x2 (Power (Power 0)))))) (setsum (setprod (binrep (Power (Power 0)) 0) (setprod (setexp x0 (binrep (Power (Power 0)) 0)) (setprod (setexp x1 (binrep (Power (Power 0)) 0)) x2))) (setsum (setprod (setexp x0 (binrep (Power (Power 0)) 0)) (setexp x1 (binrep (Power (Power 0)) 0))) (setsum (setprod (Power (Power 0)) (setprod (setexp x0 (binrep (Power (Power 0)) 0)) (setprod (setexp x1 (Power (Power 0))) (setexp x2 (binrep (Power (Power 0)) 0))))) (setsum (setprod (Power (binrep (Power (Power 0)) 0)) (setprod (setexp x0 (binrep (Power (Power 0)) 0)) (setprod (setexp x1 (Power (Power 0))) (setexp x2 (Power (Power 0)))))) (setsum (setprod (binrep (binrep (Power (binrep (Power (Power 0)) 0)) (Power (Power 0))) (Power 0)) (setprod (setexp x0 (binrep (Power (Power 0)) 0)) (setprod (setexp x1 (Power (Power 0))) x2))) (setsum (setprod (binrep (binrep (Power (binrep (Power (Power 0)) 0)) (Power (Power 0))) 0) (setprod (setexp x0 (binrep (Power (Power 0)) 0)) (setexp x1 (Power (Power 0))))) (setsum (setprod (binrep (Power (Power (Power 0))) (Power 0)) (setprod (setexp x0 (binrep (Power (Power 0)) 0)) (setprod x1 (setexp x2 (binrep (Power (Power 0)) 0))))) (setsum (setprod (binrep (Power (Power 0)) 0) (setprod (setexp x0 (binrep (Power (Power 0)) 0)) (setprod x1 (setexp x2 (Power (Power 0)))))) (setsum (setprod (setexp x0 (binrep (Power (Power 0)) 0)) (setprod x1 x2)) (setsum (setprod (binrep (Power (Power 0)) 0) (setprod (setexp x0 (binrep (Power (Power 0)) 0)) x1)) (setsum (setprod (binrep (binrep (Power (binrep (Power (Power 0)) 0)) (Power 0)) 0) (setprod (setexp x0 (binrep (Power (Power 0)) 0)) (setexp x2 (binrep (Power (Power 0)) 0)))) (setsum (setprod (setexp x0 (binrep (Power (Power 0)) 0)) (setexp x2 (Power (Power 0)))) (setsum (setprod (binrep (binrep (Power (binrep (Power (Power 0)) 0)) (Power 0)) 0) (setprod (setexp x0 (binrep (Power (Power 0)) 0)) x2)) (setsum (setprod (binrep (binrep (Power (binrep (Power (Power 0)) 0)) (Power (Power 0))) 0) (setexp x0 (binrep (Power (Power 0)) 0))) (setsum (setprod (binrep (Power (binrep (Power (Power 0)) 0)) (Power (Power 0))) (setprod (setexp x0 (Power (Power 0))) (setprod (setexp x1 (binrep (Power (Power 0)) 0)) (setexp x2 (binrep (Power (Power 0)) 0))))) (setsum (setprod (setexp x0 (Power (Power 0))) (setprod (setexp x1 (binrep (Power (Power 0)) 0)) (setexp x2 (Power (Power 0))))) (setsum (setprod (Power (Power (Power 0))) (setprod (setexp x0 (Power (Power 0))) (setprod (setexp x1 (binrep (Power (Power 0)) 0)) x2))) (setsum (setprod (Power (Power 0)) (setprod (setexp x0 (Power (Power 0))) (setexp x1 (binrep (Power (Power 0)) 0)))) (setsum (setprod (binrep (binrep (binrep (Power (binrep (Power (Power 0)) 0)) (Power (Power 0))) (Power 0)) 0) (setprod (setexp x0 (Power (Power 0))) (setprod (setexp x1 (Power (Power 0))) (setexp x2 (binrep (Power (Power 0)) 0))))) (setsum (setprod (binrep (Power (Power 0)) 0) (setprod (setexp x0 (Power (Power 0))) (setprod (setexp x1 (Power (Power 0))) (setexp x2 (Power (Power 0)))))) (setsum (setprod (binrep (binrep (Power (binrep (Power (Power 0)) 0)) (Power (Power 0))) 0) (setprod (setexp x0 (Power (Power 0))) (setprod (setexp x1 (Power (Power 0))) x2))) (setsum (setprod (binrep (binrep (Power (binrep (Power (Power 0)) 0)) (Power 0)) 0) (setprod (setexp x0 (Power (Power 0))) (setexp x1 (Power (Power 0))))) (setsum (setprod (Power (Power 0)) (setprod (setexp x0 (Power (Power 0))) (setprod x1 (setexp x2 (binrep (Power (Power 0)) 0))))) (setsum (setprod (binrep (binrep (binrep (Power (binrep (Power (Power 0)) 0)) (Power (Power 0))) (Power 0)) 0) (setprod (setexp x0 (Power (Power 0))) (setprod x1 (setexp x2 (Power (Power 0)))))) (setsum (setprod (setexp x0 (Power (Power 0))) (setprod x1 x2)) (setsum (setprod (binrep (Power (Power (Power 0))) (Power 0)) (setprod (setexp x0 (Power (Power 0))) x1)) (setsum (setprod (binrep (Power (binrep (Power (Power 0)) 0)) (Power (Power 0))) (setprod (setexp x0 (Power (Power 0))) (setexp x2 (binrep (Power (Power 0)) 0)))) (setsum (setprod (binrep (Power (Power (Power 0))) 0) (setprod (setexp x0 (Power (Power 0))) (setexp x2 (Power (Power 0))))) (setsum (setprod (Power (Power (Power 0))) (setprod (setexp x0 (Power (Power 0))) x2)) (setsum (setprod (binrep (binrep (Power (binrep (Power (Power 0)) 0)) (Power 0)) 0) (setexp x0 (Power (Power 0)))) (setsum (setprod (binrep (Power (Power (Power 0))) 0) (setprod x0 (setprod (setexp x1 (binrep (Power (Power 0)) 0)) (setexp x2 (binrep (Power (Power 0)) 0))))) (setsum (setprod (binrep (Power (binrep (Power (Power 0)) 0)) (Power 0)) (setprod x0 (setprod (setexp x1 (binrep (Power (Power 0)) 0)) (setexp x2 (Power (Power 0)))))) (setsum (setprod (binrep (Power (binrep (Power (Power 0)) 0)) 0) (setprod x0 (setprod (setexp x1 (binrep (Power (Power 0)) 0)) x2))) (setsum (setprod (Power (Power 0)) (setprod x0 (setexp x1 (binrep (Power (Power 0)) 0)))) (setsum (setprod (binrep (Power (binrep (Power (Power 0)) 0)) (Power (Power 0))) (setprod x0 (setprod (setexp x1 (Power (Power 0))) (setexp x2 (binrep (Power (Power 0)) 0))))) (setsum (setprod (Power (Power (Power 0))) (setprod x0 (setprod (setexp x1 (Power (Power 0))) (setexp x2 (Power (Power 0)))))) (setsum (setprod (Power (Power 0)) (setprod x0 (setprod (setexp x1 (Power (Power 0))) x2))) (setsum (setprod (Power (binrep (Power (Power 0)) 0)) (setprod x0 (setexp x1 (Power (Power 0))))) (setsum (setprod (binrep (binrep (Power (binrep (Power (Power 0)) 0)) (Power 0)) 0) (setprod x0 (setprod x1 (setexp x2 (binrep (Power (Power 0)) 0))))) (setsum (setprod x0 (setprod x1 (setexp x2 (Power (Power 0))))) (setsum (setprod (binrep (Power (Power 0)) 0) (setprod x0 (setprod x1 x2))) (setsum (setprod (binrep (Power (Power (Power 0))) (Power 0)) (setprod x0 x1)) (setsum (setprod (Power (Power 0)) (setprod x0 (setexp x2 (binrep (Power (Power 0)) 0)))) (setsum (setprod (binrep (binrep (Power (binrep (Power (Power 0)) 0)) (Power (Power 0))) (Power 0)) (setprod x0 (setexp x2 (Power (Power 0))))) (setsum (setprod (binrep (binrep (Power (binrep (Power (Power 0)) 0)) (Power (Power 0))) 0) (setprod x0 x2)) (setsum x0 (setsum (setprod (binrep (Power (binrep (Power (Power 0)) 0)) 0) (setprod (setexp x1 (binrep (Power (Power 0)) 0)) (setexp x2 (binrep (Power (Power 0)) 0)))) (setsum (setprod (binrep (binrep (Power (Power (Power 0))) (Power 0)) 0) (setprod (setexp x1 (binrep (Power (Power 0)) 0)) x2)) (setsum (setprod (binrep (Power (Power (Power 0))) 0) (setexp x1 (binrep (Power (Power 0)) 0))) (setsum (setprod (binrep (Power (binrep (Power (Power 0)) 0)) (Power (Power 0))) (setprod (setexp x1 (Power (Power 0))) (setexp x2 (binrep (Power (Power 0)) 0)))) (setsum (setprod (binrep (Power (Power 0)) 0) (setprod (setexp x1 (Power (Power 0))) (setexp x2 (Power (Power 0))))) (setsum (setprod (binrep (Power (Power (Power 0))) 0) (setprod (setexp x1 (Power (Power 0))) x2)) (setsum (setprod (binrep (binrep (Power (binrep (Power (Power 0)) 0)) (Power (Power 0))) (Power 0)) (setexp x1 (Power (Power 0)))) (setsum (setprod (binrep (Power (binrep (Power (Power 0)) 0)) (Power (Power 0))) (setprod x1 (setexp x2 (Power (Power 0))))) (setsum (setprod (binrep (Power (Power (Power 0))) (Power 0)) (setprod x1 x2)) (setsum (setprod (Power (Power (Power 0))) x1) (setsum (setprod (binrep (Power (Power (Power 0))) (Power 0)) (setexp x2 (Power (Power 0)))) (Power 0)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (Power (Power (Power (Power 0))))) (setsum (setprod (binrep (binrep (Power (binrep (Power (Power 0)) 0)) (Power (Power 0))) 0) (setprod (setexp x0 (binrep (Power (Power 0)) 0)) (setprod (setexp x1 (binrep (Power (Power 0)) 0)) (setexp x2 (binrep (Power (Power 0)) 0))))) (setsum (setprod (binrep (binrep (Power (binrep (Power (Power 0)) 0)) (Power (Power 0))) (Power 0)) (setprod (setexp x0 (binrep (Power (Power 0)) 0)) (setprod (setexp x1 (binrep (Power (Power 0)) 0)) (setexp x2 (Power (Power 0)))))) (setsum (setprod (Power (binrep (Power (Power 0)) 0)) (setprod (setexp x0 (binrep (Power (Power 0)) 0)) (setprod (setexp x1 (binrep (Power (Power 0)) 0)) x2))) (setsum (setprod (Power (binrep (Power (Power 0)) 0)) (setprod (setexp x0 (binrep (Power (Power 0)) 0)) (setexp x1 (binrep (Power (Power 0)) 0)))) (setsum (setprod (Power (Power (Power 0))) (setprod (setexp x0 (binrep (Power (Power 0)) 0)) (setprod (setexp x1 (Power (Power 0))) (setexp x2 (binrep (Power (Power 0)) 0))))) (setsum (setprod (binrep (Power (Power (Power 0))) 0) (setprod (setexp x0 (binrep (Power (Power 0)) 0)) (setprod (setexp x1 (Power (Power 0))) (setexp x2 (Power (Power 0)))))) (setsum (setprod (binrep (Power (Power 0)) 0) (setprod (setexp x0 (binrep (Power (Power 0)) 0)) (setprod (setexp x1 (Power (Power 0))) x2))) (setsum (setprod (binrep (Power (Power (Power 0))) (Power 0)) (setprod (setexp x0 (binrep (Power (Power 0)) 0)) (setexp x1 (Power (Power 0))))) (setsum (setprod (binrep (binrep (Power (binrep (Power (Power 0)) 0)) (Power 0)) 0) (setprod (setexp x0 (binrep (Power (Power 0)) 0)) (setprod x1 (setexp x2 (binrep (Power (Power 0)) 0))))) (setsum (setprod (Power (Power 0)) (setprod (setexp x0 (binrep (Power (Power 0)) 0)) (setprod x1 x2))) (setsum (setprod (setexp x0 (binrep (Power (Power 0)) 0)) x1) (setsum (setprod (setexp x0 (binrep (Power (Power 0)) 0)) (setexp x2 (binrep (Power (Power 0)) 0))) (setsum (setprod (binrep (binrep (Power (Power (Power 0))) (Power 0)) 0) (setprod (setexp x0 (binrep (Power (Power 0)) 0)) (setexp x2 (Power (Power 0))))) (setsum (setprod (binrep (binrep (Power (binrep (Power (Power 0)) 0)) (Power (Power 0))) (Power 0)) (setprod (setexp x0 (binrep (Power (Power 0)) 0)) x2)) (setsum (setprod (Power (Power (Power 0))) (setexp x0 (binrep (Power (Power 0)) 0))) (setsum (setprod (binrep (Power (Power 0)) 0) (setprod (setexp x0 (Power (Power 0))) (setprod (setexp x1 (binrep (Power (Power 0)) 0)) (setexp x2 (binrep (Power (Power 0)) 0))))) (setsum (setprod (Power (Power (Power 0))) (setprod (setexp x0 (Power (Power 0))) (setprod (setexp x1 (binrep (Power (Power 0)) 0)) (setexp x2 (Power (Power 0)))))) (setsum (setprod (Power (binrep (Power (Power 0)) 0)) (setprod (setexp x0 (Power (Power 0))) (setprod (setexp x1 (binrep (Power (Power 0)) 0)) x2))) (setsum (setprod (Power (Power 0)) (setprod (setexp x0 (Power (Power 0))) (setexp x1 (binrep (Power (Power 0)) 0)))) (setsum (setprod (binrep (binrep (Power (Power (Power 0))) (Power 0)) 0) (setprod (setexp x0 (Power (Power 0))) (setprod (setexp x1 (Power (Power 0))) (setexp x2 (binrep (Power (Power 0)) 0))))) (setsum (setprod (Power (Power (Power 0))) (setprod (setexp x0 (Power (Power 0))) (setprod (setexp x1 (Power (Power 0))) (setexp x2 (Power (Power 0)))))) (setsum (setprod (binrep (Power (binrep (Power (Power 0)) 0)) (Power (Power 0))) (setprod (setexp x0 (Power (Power 0))) (setprod (setexp x1 (Power (Power 0))) x2))) (setsum (setprod (Power (Power 0)) (setprod (setexp x0 (Power (Power 0))) (setexp x1 (Power (Power 0))))) (setsum (setprod (setexp x0 (Power (Power 0))) (setprod x1 (setexp x2 (binrep (Power (Power 0)) 0)))) (setsum (setprod (binrep (binrep (Power (Power (Power 0))) (Power 0)) 0) (setprod (setexp x0 (Power (Power 0))) (setprod x1 (setexp x2 (Power (Power 0)))))) (setsum (setprod (binrep (Power (binrep (Power (Power 0)) 0)) (Power 0)) (setprod (setexp x0 (Power (Power 0))) (setprod x1 x2))) (setsum (setprod (binrep (binrep (Power (binrep (Power (Power 0)) 0)) (Power 0)) 0) (setprod (setexp x0 (Power (Power 0))) x1)) (setsum (setprod (Power (Power 0)) (setprod (setexp x0 (Power (Power 0))) (setexp x2 (binrep (Power (Power 0)) 0)))) (setsum (setprod (Power (Power (Power 0))) (setprod (setexp x0 (Power (Power 0))) (setexp x2 (Power (Power 0))))) (setsum (setprod (binrep (binrep (Power (binrep (Power (Power 0)) 0)) (Power (Power 0))) 0) (setprod (setexp x0 (Power (Power 0))) x2)) (setsum (setprod (binrep (Power (Power (Power 0))) 0) (setexp x0 (Power (Power 0)))) (setsum (setprod (Power (binrep (Power (Power 0)) 0)) (setprod x0 (setprod (setexp x1 (binrep (Power (Power 0)) 0)) (setexp x2 (binrep (Power (Power 0)) 0))))) (setsum (setprod (binrep (Power (binrep (Power (Power 0)) 0)) 0) (setprod x0 (setprod (setexp x1 (binrep (Power (Power 0)) 0)) (setexp x2 (Power (Power 0)))))) (setsum (setprod (binrep (Power (Power (Power 0))) (Power 0)) (setprod x0 (setprod (setexp x1 (binrep (Power (Power 0)) 0)) x2))) (setsum (setprod (Power (Power (Power 0))) (setprod x0 (setexp x1 (binrep (Power (Power 0)) 0)))) (setsum (setprod (binrep (Power (binrep (Power (Power 0)) 0)) (Power (Power 0))) (setprod x0 (setprod (setexp x1 (Power (Power 0))) (setexp x2 (binrep (Power (Power 0)) 0))))) (setsum (setprod (binrep (binrep (Power (binrep (Power (Power 0)) 0)) (Power 0)) 0) (setprod x0 (setprod (setexp x1 (Power (Power 0))) (setexp x2 (Power (Power 0)))))) (setsum (setprod (binrep (binrep (binrep (Power (binrep (Power (Power 0)) 0)) (Power (Power 0))) (Power 0)) 0) (setprod x0 (setprod (setexp x1 (Power (Power 0))) x2))) (setsum (setprod (binrep (binrep (binrep (Power (binrep (Power (Power 0)) 0)) (Power (Power 0))) (Power 0)) 0) (setprod x0 (setexp x1 (Power (Power 0))))) (setsum (setprod (Power (Power 0)) (setprod x0 (setprod x1 (setexp x2 (binrep (Power (Power 0)) 0))))) (setsum (setprod (binrep (Power (binrep (Power (Power 0)) 0)) 0) (setprod x0 (setprod x1 (setexp x2 (Power (Power 0)))))) (setsum (setprod (Power (binrep (Power (Power 0)) 0)) (setprod x0 (setprod x1 x2))) (setsum (setprod (binrep (binrep (Power (Power (Power 0))) (Power 0)) 0) (setprod x0 x1)) (setsum (setprod (Power (Power 0)) (setprod x0 (setexp x2 (binrep (Power (Power 0)) 0)))) (setsum (setprod (binrep (Power (Power (Power 0))) 0) (setprod x0 (setexp x2 (Power (Power 0))))) (setsum (setprod (binrep (Power (Power 0)) 0) (setprod x0 x2)) (setsum (setprod (binrep (binrep (Power (binrep (Power (Power 0)) 0)) (Power (Power 0))) (Power 0)) x0) (setsum (setprod (Power (Power 0)) (setprod (setexp x1 (binrep (Power (Power 0)) 0)) (setexp x2 (binrep (Power (Power 0)) 0)))) (setsum (setprod (binrep (Power (binrep (Power (Power 0)) 0)) 0) (setprod (setexp x1 (binrep (Power (Power 0)) 0)) (setexp x2 (Power (Power 0))))) (setsum (setprod (binrep (binrep (Power (binrep (Power (Power 0)) 0)) (Power (Power 0))) 0) (setprod (setexp x1 (binrep (Power (Power 0)) 0)) x2)) (setsum (setprod (binrep (binrep (Power (binrep (Power (Power 0)) 0)) (Power 0)) 0) (setexp x1 (binrep (Power (Power 0)) 0))) (setsum (setprod (binrep (Power (Power 0)) 0) (setprod (setexp x1 (Power (Power 0))) (setexp x2 (binrep (Power (Power 0)) 0)))) (setsum (setprod (binrep (binrep (Power (binrep (Power (Power 0)) 0)) (Power (Power 0))) 0) (setprod (setexp x1 (Power (Power 0))) x2)) (setsum (setprod (binrep (binrep (binrep (Power (binrep (Power (Power 0)) 0)) (Power (Power 0))) (Power 0)) 0) (setexp x1 (Power (Power 0)))) (setsum (setprod (Power (Power (Power 0))) (setprod x1 (setexp x2 (binrep (Power (Power 0)) 0)))) (setsum (setprod (binrep (Power (Power 0)) 0) (setprod x1 (setexp x2 (Power (Power 0))))) (setsum (setprod (binrep (Power (binrep (Power (Power 0)) 0)) (Power (Power 0))) (setprod x1 x2)) (setsum x1 (setsum (setprod (binrep (binrep (Power (binrep (Power (Power 0)) 0)) (Power 0)) 0) (setexp x2 (binrep (Power (Power 0)) 0))) (setsum (setprod (binrep (Power (Power 0)) 0) (setexp x2 (Power (Power 0)))) (setsum (setprod (binrep (binrep (Power (binrep (Power (Power 0)) 0)) (Power (Power 0))) 0) x2) (binrep (Power (binrep (Power (Power 0)) 0)) (Power 0))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (binrep (binrep (binrep (binrep (binrep (binrep (binrep (binrep (binrep (binrep (binrep (binrep (binrep (Power (binrep (binrep (binrep (Power (Power (Power (Power 0)))) (binrep (Power (Power 0)) 0)) (Power (Power 0))) 0)) (binrep (binrep (Power (Power (Power (Power 0)))) (binrep (Power (Power 0)) 0)) (Power (Power 0)))) (binrep (binrep (binrep (Power (Power (Power (Power 0)))) (binrep (Power (Power 0)) 0)) (Power 0)) 0)) (binrep (binrep (Power (Power (Power (Power 0)))) (binrep (Power (Power 0)) 0)) (Power 0))) (binrep (binrep (Power (Power (Power (Power 0)))) (Power (Power 0))) 0)) (binrep (Power (Power (Power (Power 0)))) (Power (Power 0)))) (binrep (binrep (Power (binrep (Power (Power 0)) 0)) (Power 0)) 0)) (binrep (Power (binrep (Power (Power 0)) 0)) (Power 0))) (binrep (Power (Power (Power 0))) (Power 0))) (binrep (Power (Power (Power 0))) 0)) (Power (Power (Power 0)))) (binrep (Power (Power 0)) 0)) (Power (Power 0))) (Power 0))False)∀ x0 : ο . x0
as obj
-
as prop
633c4..
theory
HF
stx
9b629..
address
TMUgb..