YES (VAR ) (RULES response(a(),b()) -> b() ) (COMMENT Termination is shown by LPO with precedence: response > a > b )