Description of the problem on p.325: This problem decides whether we should orient the equation $(xy)^{-1}=y^{-1}x^{-1}$ into $(xy)^{-1} \to y^{-1}x^{-1}$ in order to get a terminating rewrite system for group theory. It uses a polynomial interpretation: $xy \Rightarrow x+2xy$, $x^{-1} \Rightarrow x^2$, and $1 \Rightarrow 2$.
load redlog$ rlset ofsf$
ter := ex(r,all({x,y},x>r and y>r impl x**2*(1+2*y)**2>y**2*(1+2*x**2)));
rlqe ter;
end; % of file