(GOAL COMPLEXITY)
(STARTTERM CONSTRUCTORBASED)
(VAR a k ls x )
(STRATEGY INNERMOST)
(RULES 
        rev(ls) -> r1(ls, empty)
        r1(empty, a) -> a
        r1(cons(x, k), a) -> r1(k, cons(x, a))
        
)