(GOAL COMPLEXITY) (STARTTERM CONSTRUCTORBASED) (VAR x y ) (STRATEGY INNERMOST) (RULES rev(a) -> a rev(b) -> b rev(++(x, y)) -> ++(rev(y), rev(x)) rev(++(x, x)) -> rev(x) )