0.00/0.03	YES
0.00/0.03	(ignored inputs)COMMENT doi:10.1007/3-540-58216-9_40 [45] Example 2.1 ( a ) submitted by: Thomas Sternagel
0.00/0.03	Conditional Rewrite Rules:
0.00/0.03	   [ f(cons(?x,nil)) -> pair(?x,nil),
0.00/0.03	     f(cons(?x,cons(?y,?l))) -> pair(?z,cons(?x,?l1)) | f(cons(?y,?l)) == pair(?z,?l1) ]
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	   [ f(cons(?x,nil)) -> pair(?x,nil),
0.00/0.03	     f(cons(?x,cons(?y,?l))) -> U0(f(cons(?y,?l)),?l,?x,?y),
0.00/0.03	     U0(pair(?z,?l1),?l,?x,?y) -> pair(?z,cons(?x,?l1)) ]
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