0.00/0.06	YES
0.00/0.06	(ignored inputs)COMMENT [68] p. 12 with rules for "lt" and "m" added doi:10.1007/3-540-59200-8_56 submitted by: Thomas Sternagel and Aart Middeldorp
0.00/0.06	Conditional Rewrite Rules:
0.00/0.06	   [ lt(?x,0) -> false,
0.00/0.06	     lt(0,s(?x)) -> true,
0.00/0.06	     lt(s(?x),s(?y)) -> lt(?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	     div(0,s(?x)) -> pair(0,0),
0.00/0.06	     div(s(?x),s(?y)) -> pair(0,s(?x)) | lt(?x,?y) == true,
0.00/0.06	     div(s(?x),s(?y)) -> pair(s(?q),?r) | lt(?x,?y) == false,div(m(?x,?y),s(?y)) == pair(?q,?r) ]
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	   [ lt(?x,0) -> false,
0.00/0.06	     lt(0,s(?x)) -> true,
0.00/0.06	     lt(s(?x),s(?y)) -> lt(?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	     div(0,s(?x)) -> pair(0,0),
0.00/0.06	     div(s(?x),s(?y)) -> U1(lt(?x,?y),?x,?y),
0.00/0.06	     U1(true,?x,?y) -> pair(0,s(?x)),
0.00/0.06	     U1(false,?x,?y) -> U2(div(m(?x,?y),s(?y)),?x,?y),
0.00/0.06	     U2(pair(?q,?r),?x,?y) -> pair(s(?q),?r) ]
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	(16 msec.)
0.00/0.06	EOF