0.00/0.03	YES
0.00/0.03	(ignored inputs)COMMENT doi:10.1016/j.tcs.2012.09.005 [72] p. 73 submitted by: Thomas Sternagel and Aart Middeldorp
0.00/0.03	Conditional Rewrite Rules:
0.00/0.03	   [ sub(?z,0) -> ?z,
0.00/0.03	     sub(s(?z),s(?y)) -> ?x | sub(?z,?y) == ?x ]
0.00/0.03	Check whether all rules are type 3
0.00/0.03	OK
0.00/0.03	Check whether the input is deterministic
0.00/0.03	OK
0.00/0.03	Result of unraveling:
0.00/0.03	   [ sub(?z,0) -> ?z,
0.00/0.03	     sub(s(?z),s(?y)) -> U0(sub(?z,?y),?y,?z),
0.00/0.03	     U0(?x,?y,?z) -> ?x ]
0.00/0.03	Check whether U(R) is terminating
0.00/0.03	OK
0.00/0.03	Check whether the input is weakly left-linear
0.00/0.03	OK
0.00/0.03	Check whether U(R) is confluent
0.00/0.03	OK
0.00/0.03	R is deterministic, weakly left-linear and U(R) is confluent
0.00/0.03	/export/starexec/sandbox/benchmark/theBenchmark.trs: Success(CR)
0.00/0.03	(4 msec.)
0.00/0.03	EOF