0.00/0.04	MAYBE
0.00/0.04	(ignored inputs)COMMENT [121] Example 5.15; inlined version of Cops #551 submitted by: Thomas Sternagel
0.00/0.04	Conditional Rewrite Rules:
0.00/0.04	   [ le(?x,0) -> false,
0.00/0.04	     le(0,s(?y)) -> true,
0.00/0.04	     le(s(?x),s(?y)) -> le(?x,?y),
0.00/0.04	     min(cons(?x,nil)) -> ?x,
0.00/0.04	     min(cons(?x,?xs)) -> ?x | le(?x,min(?xs)) == true,
0.00/0.04	     min(cons(?x,?xs)) -> min(?xs) | le(?x,min(?xs)) == false ]
0.00/0.04	Check whether all rules are type 3
0.00/0.04	OK
0.00/0.04	Check whether the input is deterministic
0.00/0.04	OK
0.00/0.04	Result of unraveling:
0.00/0.04	   [ le(?x,0) -> false,
0.00/0.04	     le(0,s(?y)) -> true,
0.00/0.04	     le(s(?x),s(?y)) -> le(?x,?y),
0.00/0.04	     min(cons(?x,nil)) -> ?x,
0.00/0.04	     min(cons(?x,?xs)) -> U1(le(?x,min(?xs)),?x,?xs),
0.00/0.04	     U1(true,?x,?xs) -> ?x,
0.00/0.04	     U1(false,?x,?xs) -> min(?xs) ]
0.00/0.04	Check whether U(R) is terminating
0.00/0.04	OK
0.00/0.04	Check whether the input is weakly left-linear
0.00/0.04	OK
0.00/0.04	Check whether U(R) is confluent
0.00/0.04	U(R) is not confluent
0.00/0.04	Conditional critical pairs (CCPs):
0.00/0.04	   [ ?x_4 = ?x_4 | le(?x_4,min(nil)) == true,
0.00/0.04	     min(nil) = ?x_5 | le(?x_5,min(nil)) == false,
0.00/0.04	     ?x_3 = ?x_3 | le(?x_3,min(nil)) == true,
0.00/0.04	     min(?xs_5) = ?x_5 | le(?x_5,min(?xs_5)) == false,le(?x_5,min(?xs_5)) == true,
0.00/0.04	     ?x_3 = min(nil) | le(?x_3,min(nil)) == false,
0.00/0.04	     ?x_4 = min(?xs_4) | le(?x_4,min(?xs_4)) == true,le(?x_4,min(?xs_4)) == false ]
0.00/0.04	Check whether the input is almost orthogonale
0.00/0.04	not almost orthogonal
0.00/0.04	OK
0.00/0.04	Check whether the input is absolutely irreducible
0.00/0.04	OK
0.00/0.04	Check whether all CCPs are joinable
0.00/0.04	Some ccp may be feasible but not joinable
0.00/0.04	   [ min(nil) = ?x_5 | le(?x_5,min(nil)) == false,
0.00/0.04	     min(?xs_5) = ?x_5 | le(?x_5,min(?xs_5)) == false,le(?x_5,min(?xs_5)) == true,
0.00/0.04	     ?x_3 = min(nil) | le(?x_3,min(nil)) == false,
0.00/0.04	     ?x_4 = min(?xs_4) | le(?x_4,min(?xs_4)) == true,le(?x_4,min(?xs_4)) == false ]
0.00/0.04	/export/starexec/sandbox2/benchmark/theBenchmark.trs: Failure(unknown CR)
0.00/0.04	(8 msec.)
0.00/0.04	EOF