0.00/0.03	YES
0.00/0.03	(ignored inputs)COMMENT doi:10.1016/j.tcs.2012.09.005 [72] p. 72 submitted by: Thomas Sternagel and Aart Middeldorp
0.00/0.03	Conditional Rewrite Rules:
0.00/0.03	   [ add(?x,0) -> ?x,
0.00/0.03	     add(?x,s(?y)) -> s(?z) | add(?x,?y) == ?z ]
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	   [ add(?x,0) -> ?x,
0.00/0.03	     add(?x,s(?y)) -> U0(add(?x,?y),?x,?y),
0.00/0.03	     U0(?z,?x,?y) -> s(?z) ]
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/sandbox2/benchmark/theBenchmark.trs: Success(CR)
0.00/0.03	(4 msec.)
0.00/0.03	EOF