YES (VAR x y z) (RULES multiply(multiply(x,y),z) -> multiply(x,multiply(y,z)) ) (COMMENT Termination is shown by ELPO with interpretations on natural numbers multiply_A(x1,x2) = 1 multiply#_A(x1,x2) = 0 and precedence: multiply )