(COMMENT
 Example 11 in the paper "Maximal termination" published at RTA '08
)
(VAR x)
(RULES 
 f(s(x),x) -> f(s(x),round(s(x)))
 round(0) -> 0
 round(0) -> s(0)
 round(s(0)) -> s(0)
 round(s(s(x))) -> s(s(round(x))) 
)