YES (VAR ) (RULES response(a(),b()) -> b() ) (COMMENT Termination is shown by KBO with weight w0 = 1 w(response) = 0 w(a) = 1 w(b) = 1 and precedence: a > response > b )