0.00/0.04	YES
0.00/0.04	(ignored inputs)COMMENT doi:10.1016/0022-0000 ( 86 ) 90033-4 [47] Example 2.3.i submitted by: Thomas Sternagel and Aart Middeldorp
0.00/0.04	Conditional Rewrite Rules:
0.00/0.04	   [ size(empty) -> 0,
0.00/0.04	     size(push(?x,?y)) -> s(size(?x)),
0.00/0.04	     m -> s(s(s(s(0)))),
0.00/0.04	     pop(empty) -> empty,
0.00/0.04	     pop(push(?x,?y)) -> ?x | le(size(?x),m) == true,
0.00/0.04	     top(empty) -> eentry,
0.00/0.04	     top(push(?x,?y)) -> ?y | le(size(?x),m) == true,
0.00/0.04	     le(?x,0) -> false,
0.00/0.04	     le(0,s(?x)) -> true,
0.00/0.04	     le(s(?x),s(?y)) -> le(?x,?y) ]
0.00/0.04	Check whether all rules are type 3
0.00/0.04	OK
0.00/0.04	Check whether the input is deterministic
0.00/0.04	OK
0.00/0.04	Result of unraveling:
0.00/0.04	   [ size(empty) -> 0,
0.00/0.04	     size(push(?x,?y)) -> s(size(?x)),
0.00/0.04	     m -> s(s(s(s(0)))),
0.00/0.04	     pop(empty) -> empty,
0.00/0.04	     pop(push(?x,?y)) -> U0(le(size(?x),m),?x,?y),
0.00/0.04	     U0(true,?x,?y) -> ?x,
0.00/0.04	     top(empty) -> eentry,
0.00/0.04	     top(push(?x,?y)) -> U1(le(size(?x),m),?x,?y),
0.00/0.04	     U1(true,?x,?y) -> ?y,
0.00/0.04	     le(?x,0) -> false,
0.00/0.04	     le(0,s(?x)) -> true,
0.00/0.04	     le(s(?x),s(?y)) -> le(?x,?y) ]
0.00/0.04	Check whether U(R) is terminating
0.00/0.04	OK
0.00/0.04	Check whether the input is weakly left-linear
0.00/0.04	OK
0.00/0.04	Check whether U(R) is confluent
0.00/0.04	OK
0.00/0.04	R is deterministic, weakly left-linear and U(R) is confluent
0.00/0.04	/export/starexec/sandbox/benchmark/theBenchmark.trs: Success(CR)
0.00/0.04	(8 msec.)
0.00/0.04	EOF