YES
(ignored inputs)COMMENT the following rules are removed from the original TRS Ap ( Ap ( Ap ( S ( ) , x ) , y ) , z ) -> Ap ( Ap ( x , z ) , Ap ( y , z ) ) Ap ( Ap ( K ( ) , x ) , y ) -> x Ap ( I ( ) , x ) -> x
: CR

Combined result: CR
/tmp/fileTzIXom.trs: Success(CR)
(0 msec.)