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