YES (VAR x y z) (RULES multiply(multiply(x,y),z) -> multiply(x,multiply(y,z)) ) (COMMENT Termination is shown by KBO with weight w0 = 1 w(multiply) = 0 and precedence: multiply )