0.00/0.06	YES
0.00/0.06	(ignored inputs)COMMENT doi:10.1007/978-1-4757-3661-8 [18] p. 205 submitted by: Thomas Sternagel and Aart Middeldorp
0.00/0.06	Conditional Rewrite Rules:
0.00/0.06	   [ le(0,?x) -> true,
0.00/0.06	     le(s(?x),0) -> false,
0.00/0.06	     le(s(?x),s(?y)) -> le(?x,?y),
0.00/0.06	     app(nil,?x) -> ?x,
0.00/0.06	     app(cons(?x,?xs),?ys) -> cons(?x,app(?xs,?ys)),
0.00/0.06	     split(?x,nil) -> pair(nil,nil),
0.00/0.06	     qsort(nil) -> nil,
0.00/0.06	     split(?x,cons(?y,?ys)) -> pair(?xs,cons(?y,?zs)) | split(?x,?ys) == pair(?xs,?zs),le(?x,?y) == true,
0.00/0.06	     split(?x,cons(?y,?ys)) -> pair(cons(?y,?xs),?zs) | split(?x,?ys) == pair(?xs,?zs),le(?x,?y) == false,
0.00/0.06	     qsort(cons(?x,?xs)) -> app(qsort(?ys),cons(?x,qsort(?zs))) | split(?x,?xs) == pair(?ys,?zs) ]
0.00/0.06	Check whether all rules are type 3
0.00/0.06	OK
0.00/0.06	Check whether the input is deterministic
0.00/0.06	OK
0.00/0.06	Result of unraveling:
0.00/0.06	   [ le(0,?x) -> true,
0.00/0.06	     le(s(?x),0) -> false,
0.00/0.06	     le(s(?x),s(?y)) -> le(?x,?y),
0.00/0.06	     app(nil,?x) -> ?x,
0.00/0.06	     app(cons(?x,?xs),?ys) -> cons(?x,app(?xs,?ys)),
0.00/0.06	     split(?x,nil) -> pair(nil,nil),
0.00/0.06	     qsort(nil) -> nil,
0.00/0.06	     split(?x,cons(?y,?ys)) -> U2(split(?x,?ys),?x,?y,?ys),
0.00/0.06	     U2(pair(?xs,?zs),?x,?y,?ys) -> U3(le(?x,?y),?x,?y,?ys,?xs,?zs),
0.00/0.06	     U3(true,?x,?y,?ys,?xs,?zs) -> pair(?xs,cons(?y,?zs)),
0.00/0.06	     U3(false,?x,?y,?ys,?xs,?zs) -> pair(cons(?y,?xs),?zs),
0.00/0.06	     qsort(cons(?x,?xs)) -> U4(split(?x,?xs),?x,?xs),
0.00/0.06	     U4(pair(?ys,?zs),?x,?xs) -> app(qsort(?ys),cons(?x,qsort(?zs))) ]
0.00/0.06	Check whether U(R) is terminating
0.00/0.06	OK
0.00/0.06	Check whether the input is weakly left-linear
0.00/0.06	OK
0.00/0.06	Check whether U(R) is confluent
0.00/0.06	OK
0.00/0.06	R is deterministic, weakly left-linear and U(R) is confluent
0.00/0.06	/export/starexec/sandbox/benchmark/theBenchmark.trs: Success(CR)
0.00/0.06	(20 msec.)
0.00/0.06	EOF