YES (ignored inputs)COMMENT the following rules are removed from the original TRS a ( a ( b ( a ( b ( a ( b ( a ( b ( x ) ) ) ) ) ) ) ) ) -> a ( b ( a ( b ( a ( b ( a ( b ( a ( a ( a ( a ( a ( b ( x ) ) ) ) ) ) ) ) ) ) ) ) ) ) : CR Combined result: CR /tmp/file3zD4Dh.trs: Success(CR) (0 msec.)