YES (ignored inputs)COMMENT the following rules are removed from the original TRS + ( x , 0 ( ) ) -> x + ( x , s ( y ) ) -> s ( + ( x , y ) ) - ( 0 ( ) , x ) -> 0 ( ) - ( x , 0 ( ) ) -> x - ( s ( x ) , s ( y ) ) -> - ( x , y ) : CR Combined result: CR /tmp/filet4OYBr.trs: Success(CR) (0 msec.)