0.00/0.05	YES
0.00/0.05	(ignored inputs)COMMENT doi:10.1007/3-540-54317-1_91 [48] p. 203 submitted by: Thomas Sternagel and Aart Middeldorp
0.00/0.05	Conditional Rewrite Rules:
0.00/0.05	   [ lte(0,?n) -> true,
0.00/0.05	     lte(s(?m),0) -> false,
0.00/0.05	     lte(s(?m),s(?n)) -> lte(?m,?n),
0.00/0.05	     insert(nil,?m) -> cons(?m,nil),
0.00/0.05	     insert(cons(?n,?l),?m) -> cons(?m,cons(?n,?l)) | lte(?m,?n) == true,
0.00/0.05	     insert(cons(?n,?l),?m) -> cons(?n,insert(?l,?m)) | lte(?m,?n) == false,
0.00/0.05	     ordered(nil) -> true,
0.00/0.05	     ordered(cons(?m,nil)) -> true,
0.00/0.05	     ordered(cons(?m,cons(?n,?l))) -> ordered(cons(?n,?l)) | lte(?m,?n) == true,
0.00/0.05	     ordered(cons(?m,cons(?n,?l))) -> false | lte(?m,?n) == false ]
0.00/0.05	Check whether all rules are type 3
0.00/0.05	OK
0.00/0.05	Check whether the input is deterministic
0.00/0.05	OK
0.00/0.05	Result of unraveling:
0.00/0.05	   [ lte(0,?n) -> true,
0.00/0.05	     lte(s(?m),0) -> false,
0.00/0.05	     lte(s(?m),s(?n)) -> lte(?m,?n),
0.00/0.05	     insert(nil,?m) -> cons(?m,nil),
0.00/0.05	     insert(cons(?n,?l),?m) -> U1(lte(?m,?n),?l,?m,?n),
0.00/0.05	     U1(true,?l,?m,?n) -> cons(?m,cons(?n,?l)),
0.00/0.05	     U1(false,?l,?m,?n) -> cons(?n,insert(?l,?m)),
0.00/0.05	     ordered(nil) -> true,
0.00/0.05	     ordered(cons(?m,nil)) -> true,
0.00/0.05	     ordered(cons(?m,cons(?n,?l))) -> U3(lte(?m,?n),?l,?m,?n),
0.00/0.05	     U3(true,?l,?m,?n) -> ordered(cons(?n,?l)),
0.00/0.05	     U3(false,?l,?m,?n) -> false ]
0.00/0.05	Check whether U(R) is terminating
0.00/0.05	OK
0.00/0.05	Check whether the input is weakly left-linear
0.00/0.05	OK
0.00/0.05	Check whether U(R) is confluent
0.00/0.05	OK
0.00/0.05	R is deterministic, weakly left-linear and U(R) is confluent
0.00/0.05	/export/starexec/sandbox2/benchmark/theBenchmark.trs: Success(CR)
0.00/0.05	(16 msec.)
0.00/0.05	EOF