0.00/0.02	MAYBE
0.00/0.02	(ignored inputs)COMMENT doi:10.1016/S0747-7171 ( 08 ) 80132-0 [53] p. 77 submitted by: Thomas Sternagel and Aart Middeldorp
0.00/0.02	Conditional Rewrite Rules:
0.00/0.02	   [ lte(0,?x) -> true,
0.00/0.02	     lte(s(?x),0) -> false,
0.00/0.02	     lte(s(?x),s(?y)) -> lte(?x,?y),
0.00/0.02	     lte(?x,?x) -> true,
0.00/0.02	     lte(?x,s(?x)) -> true,
0.00/0.02	     lte(?x,s(?y)) -> true | lte(?x,?y) == true,
0.00/0.02	     lte(?y,?x) -> true | lte(?x,?y) == false,
0.00/0.02	     lte(?x,?z) -> true | lte(?x,?y) == true,lte(?y,?z) == true ]
0.00/0.02	Check whether all rules are type 3
0.00/0.02	OK
0.00/0.02	Check whether the input is deterministic
0.00/0.02	No. non-deterministic rule: lte(?x,?z) -> true | lte(?x,?y) == true,lte(?y,?z) == true
0.00/0.02	Conditional critical pairs (CCPs):
0.00/0.02	   [ true = true,
0.00/0.02	     true = true,
0.00/0.02	     true = true | lte(0,?y_5) == true,
0.00/0.02	     true = true | lte(?x_6,0) == false,
0.00/0.02	     true = true | lte(0,?y_7) == true,lte(?y_7,?z_7) == true,
0.00/0.02	     true = false | lte(0,s(?x_1)) == false,
0.00/0.02	     true = false | lte(s(?x_1),?y_7) == true,lte(?y_7,0) == true,
0.00/0.02	     true = lte(?x_2,?x_2),
0.00/0.02	     true = lte(?x_2,s(?x_2)),
0.00/0.02	     true = lte(?x_2,?y_5) | lte(s(?x_2),?y_5) == true,
0.00/0.02	     true = lte(?x_2,?y_2) | lte(s(?y_2),s(?x_2)) == false,
0.00/0.02	     true = lte(?x_2,?y_2) | lte(s(?x_2),?y_7) == true,lte(?y_7,s(?y_2)) == true,
0.00/0.02	     true = true,
0.00/0.02	     lte(?y_2,?y_2) = true,
0.00/0.02	     true = true | lte(s(?y_5),?y_5) == true,
0.00/0.02	     true = true | lte(?x_6,?x_6) == false,
0.00/0.02	     true = true | lte(?z_7,?y_7) == true,lte(?y_7,?z_7) == true,
0.00/0.02	     true = true,
0.00/0.02	     lte(?x_2,s(?x_2)) = true,
0.00/0.02	     true = true | lte(?y_5,?y_5) == true,
0.00/0.02	     true = true | lte(s(?y_6),?y_6) == false,
0.00/0.02	     true = true | lte(?x_7,?y_7) == true,lte(?y_7,s(?x_7)) == true,
0.00/0.02	     true = true | lte(0,?y_5) == true,
0.00/0.02	     lte(?x_2,?y_2) = true | lte(s(?x_2),?y_2) == true,
0.00/0.02	     true = true | lte(s(?y_5),?y_5) == true,
0.00/0.02	     true = true | lte(?x_4,?x_4) == true,
0.00/0.02	     true = true | lte(s(?y_5),?y_6) == false,lte(?y_6,?y_5) == true,
0.00/0.02	     true = true | lte(?x_7,?y_7) == true,lte(?y_7,s(?y_5)) == true,lte(?x_7,?y_5) == true,
0.00/0.02	     true = true | lte(?x,0) == false,
0.00/0.02	     false = true | lte(0,s(?x_1)) == false,
0.00/0.02	     lte(?x_2,?y_2) = true | lte(s(?y_2),s(?x_2)) == false,
0.00/0.02	     true = true | lte(?x_3,?x_3) == false,
0.00/0.02	     true = true | lte(s(?x_4),?x_4) == false,
0.00/0.02	     true = true | lte(?x_5,?y_5) == true,lte(s(?y_5),?x_5) == false,
0.00/0.02	     true = true | lte(?x_7,?y_7) == true,lte(?y_7,?z_7) == true,lte(?z_7,?x_7) == false,
0.00/0.02	     true = true | lte(0,?y_7) == true,lte(?y_7,?x) == true,
0.00/0.02	     false = true | lte(s(?x_1),?y_7) == true,lte(?y_7,0) == true,
0.00/0.02	     lte(?x_2,?y_2) = true | lte(s(?x_2),?y_7) == true,lte(?y_7,s(?y_2)) == true,
0.00/0.02	     true = true | lte(?x_3,?y_7) == true,lte(?y_7,?x_3) == true,
0.00/0.02	     true = true | lte(?x_4,?y_7) == true,lte(?y_7,s(?x_4)) == true,
0.00/0.02	     true = true | lte(?x_5,?y_5) == true,lte(?x_5,?y_7) == true,lte(?y_7,s(?y_5)) == true,
0.00/0.02	     true = true | lte(?x_6,?y_6) == false,lte(?y_6,?y_7) == true,lte(?y_7,?x_6) == true ]
0.00/0.02	Check whether the input is almost orthogonale
0.00/0.02	not almost orthogonal
0.00/0.02	/export/starexec/sandbox2/benchmark/theBenchmark.trs: Failure(unknown CR)
0.00/0.02	(0 msec.)
0.00/0.02	EOF