0.00/0.06	YES
0.00/0.06	(ignored inputs)COMMENT doi:10.1007/978-1-4757-3661-8 [18] Example 7.4.9; correction of Cops #328 submitted by: Thomas Sternagel
0.00/0.06	Conditional Rewrite Rules:
0.00/0.06	   [ eq(0,0) -> true,
0.00/0.06	     eq(s(?x),0) -> false,
0.00/0.06	     eq(0,s(?y)) -> false,
0.00/0.06	     eq(s(?x),s(?y)) -> eq(?x,?y),
0.00/0.06	     lte(0,?y) -> true,
0.00/0.06	     lte(s(?x),0) -> false,
0.00/0.06	     lte(s(?x),s(?y)) -> lte(?x,?y),
0.00/0.06	     m(0,s(?y)) -> 0,
0.00/0.06	     m(?x,0) -> ?x,
0.00/0.06	     m(s(?x),s(?y)) -> m(?x,?y),
0.00/0.06	     mod(0,?y) -> 0,
0.00/0.06	     mod(s(?x),0) -> 0,
0.00/0.06	     mod(s(?x),s(?y)) -> mod(m(?x,?y),s(?y)) | lte(?y,?x) == true,
0.00/0.06	     mod(s(?x),s(?y)) -> s(?x) | lte(?y,?x) == false,
0.00/0.06	     filter(?n,?r,nil) -> nil,
0.00/0.06	     filter(?n,?r,cons(?x,?xs)) -> cons(?x,filter(?n,?r,?xs)) | mod(?x,?n) == ?r',eq(?r,?r') == true,
0.00/0.06	     filter(?n,?r,cons(?x,?xs)) -> filter(?n,?r,?xs) | mod(?x,?n) == ?r',eq(?r,?r') == false ]
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	   [ eq(0,0) -> true,
0.00/0.06	     eq(s(?x),0) -> false,
0.00/0.06	     eq(0,s(?y)) -> false,
0.00/0.06	     eq(s(?x),s(?y)) -> eq(?x,?y),
0.00/0.06	     lte(0,?y) -> true,
0.00/0.06	     lte(s(?x),0) -> false,
0.00/0.06	     lte(s(?x),s(?y)) -> lte(?x,?y),
0.00/0.06	     m(0,s(?y)) -> 0,
0.00/0.06	     m(?x,0) -> ?x,
0.00/0.06	     m(s(?x),s(?y)) -> m(?x,?y),
0.00/0.06	     mod(0,?y) -> 0,
0.00/0.06	     mod(s(?x),0) -> 0,
0.00/0.06	     mod(s(?x),s(?y)) -> U1(lte(?y,?x),?x,?y),
0.00/0.06	     U1(true,?x,?y) -> mod(m(?x,?y),s(?y)),
0.00/0.06	     U1(false,?x,?y) -> s(?x),
0.00/0.06	     filter(?n,?r,nil) -> nil,
0.00/0.06	     filter(?n,?r,cons(?x,?xs)) -> U4(mod(?x,?n),?n,?r,?x,?xs),
0.00/0.06	     U4(?r',?n,?r,?x,?xs) -> U5(eq(?r,?r'),?n,?r,?x,?xs,?r'),
0.00/0.06	     U5(true,?n,?r,?x,?xs,?r') -> cons(?x,filter(?n,?r,?xs)),
0.00/0.06	     U5(false,?n,?r,?x,?xs,?r') -> filter(?n,?r,?xs) ]
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	(25 msec.)
0.00/0.06	EOF