(VAR x ) (STRATEGY INNERMOST) (RULES a(b(a(b(x)))) -> b(a(b(a(a(b(x)))))) )