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