0.00/0.03	YES
0.00/0.03	(ignored inputs)COMMENT submitted by: Christian Sternagel
0.00/0.03	Conditional Rewrite Rules:
0.00/0.03	   [ last(cons(?x,?y)) -> ?x | ?y == nil,
0.00/0.03	     last(cons(?x,?y)) -> ?z | ?y == cons(?u,?v),last(?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	   [ last(cons(?x,?y)) -> U1(?y,?x,?y),
0.00/0.03	     U1(nil,?x,?y) -> ?x,
0.00/0.03	     U1(cons(?u,?v),?x,?y) -> U2(last(?y),?x,?y,?u,?v),
0.00/0.03	     U2(?z,?x,?y,?u,?v) -> ?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	(5 msec.)
0.00/0.03	EOF