0.00/0.07	MAYBE
0.00/0.07	(ignored inputs)COMMENT doi: 10.1007/3-540-54317-1_80 [57] Example 5.1 submitted by: Thomas Sternagel and Aart Middeldorp
0.00/0.07	Conditional Rewrite Rules:
0.00/0.07	   [ le(0,s(?x)) -> true,
0.00/0.07	     le(?x,0) -> false,
0.00/0.07	     le(s(?x),s(?y)) -> le(?x,?y),
0.00/0.07	     min(cons(?x,nil)) -> ?x,
0.00/0.07	     min(cons(?x,?l)) -> ?x | le(?x,min(?l)) == true,
0.00/0.07	     min(cons(?x,?l)) -> min(?l) | le(?x,min(?l)) == false,
0.00/0.07	     min(cons(?x,?l)) -> min(?l) | min(?l) == ?x ]
0.00/0.07	Check whether all rules are type 3
0.00/0.07	OK
0.00/0.07	Check whether the input is deterministic
0.00/0.07	OK
0.00/0.07	Result of unraveling:
0.00/0.07	   [ le(0,s(?x)) -> true,
0.00/0.07	     le(?x,0) -> false,
0.00/0.07	     le(s(?x),s(?y)) -> le(?x,?y),
0.00/0.07	     min(cons(?x,nil)) -> ?x,
0.00/0.07	     min(cons(?x,?l)) -> U2(le(?x,min(?l)),?l,?x),
0.00/0.07	     U2(true,?l,?x) -> ?x,
0.00/0.07	     U2(false,?l,?x) -> min(?l),
0.00/0.07	     min(cons(?x,?l)) -> U2(min(?l),?l,?x),
0.00/0.07	     U2(?x,?l,?x) -> min(?l) ]
0.00/0.07	Check whether U(R) is terminating
0.00/0.07	OK
0.00/0.07	Check whether the input is weakly left-linear
0.00/0.07	OK
0.00/0.07	Check whether U(R) is confluent
0.00/0.07	U(R) is not confluent
0.00/0.07	Conditional critical pairs (CCPs):
0.00/0.07	   [ ?x_4 = ?x_4 | le(?x_4,min(nil)) == true,
0.00/0.07	     min(nil) = ?x_5 | le(?x_5,min(nil)) == false,
0.00/0.07	     min(nil) = ?x_6 | min(nil) == ?x_6,
0.00/0.07	     ?x_3 = ?x_3 | le(?x_3,min(nil)) == true,
0.00/0.07	     min(?l_5) = ?x_5 | le(?x_5,min(?l_5)) == false,le(?x_5,min(?l_5)) == true,
0.00/0.07	     min(?l_6) = ?x_6 | min(?l_6) == ?x_6,le(?x_6,min(?l_6)) == true,
0.00/0.07	     ?x_3 = min(nil) | le(?x_3,min(nil)) == false,
0.00/0.07	     ?x_4 = min(?l_4) | le(?x_4,min(?l_4)) == true,le(?x_4,min(?l_4)) == false,
0.00/0.07	     min(?l_6) = min(?l_6) | min(?l_6) == ?x_6,le(?x_6,min(?l_6)) == false,
0.00/0.07	     ?x_3 = min(nil) | min(nil) == ?x_3,
0.00/0.07	     ?x_4 = min(?l_4) | le(?x_4,min(?l_4)) == true,min(?l_4) == ?x_4,
0.00/0.07	     min(?l_5) = min(?l_5) | le(?x_5,min(?l_5)) == false,min(?l_5) == ?x_5 ]
0.00/0.07	Check whether the input is almost orthogonale
0.00/0.07	not almost orthogonal
0.00/0.07	OK
0.00/0.07	Check whether the input is absolutely irreducible
0.00/0.07	OK
0.00/0.07	Check whether all CCPs are joinable
0.00/0.07	Some ccp may be feasible but not joinable
0.00/0.07	   [ min(nil) = ?x_5 | le(?x_5,min(nil)) == false,
0.00/0.07	     min(?l_5) = ?x_5 | le(?x_5,min(?l_5)) == false,le(?x_5,min(?l_5)) == true,
0.00/0.07	     ?x_3 = min(nil) | le(?x_3,min(nil)) == false,
0.00/0.07	     ?x_4 = min(?l_4) | le(?x_4,min(?l_4)) == true,le(?x_4,min(?l_4)) == false ]
0.00/0.07	/export/starexec/sandbox2/benchmark/theBenchmark.trs: Failure(unknown CR)
0.00/0.07	(9 msec.)
0.00/0.07	EOF