Abstract. Well-founded orders are the most basic, but also most important ingredient to virtually all termination analyses. Numerous fully automated search algorithms for these cla...
We introduce a propositional encoding of the recursive path order with status (RPO). RPO is a combination of a multiset path order and a lexicographic path order which considers pe...