0.00/0.00 MAYBE 0.00/0.00 0.00/0.00 0.00/0.00 Succeeded in reading "/export/starexec/sandbox/benchmark/theBenchmark.trs". 0.00/0.00 (CONDITIONTYPE ORIENTED) 0.00/0.00 (VAR x y xs) 0.00/0.00 (RULES 0.00/0.00 le(x,0) -> false 0.00/0.00 le(0,s(y)) -> true 0.00/0.00 le(s(x),s(y)) -> le(x,y) 0.00/0.00 min(cons(x,nil)) -> x 0.00/0.00 min(cons(x,xs)) -> x | le(x,min(xs)) == true 0.00/0.00 min(cons(x,xs)) -> min(xs) | le(x,min(xs)) == false 0.00/0.00 ) 0.00/0.00 (COMMENT [121] Example 5.15; inlined version of Cops #551 submitted by: Thomas Sternagel) 0.00/0.00 0.00/0.00 No "->="-rules. 0.00/0.00 0.00/0.00 Decomposed conditions if possible. 0.00/0.00 (CONDITIONTYPE ORIENTED) 0.00/0.00 (VAR x y xs) 0.00/0.00 (RULES 0.00/0.00 le(x,0) -> false 0.00/0.00 le(0,s(y)) -> true 0.00/0.00 le(s(x),s(y)) -> le(x,y) 0.00/0.00 min(cons(x,nil)) -> x 0.00/0.00 min(cons(x,xs)) -> x | le(x,min(xs)) == true 0.00/0.00 min(cons(x,xs)) -> min(xs) | le(x,min(xs)) == false 0.00/0.00 ) 0.00/0.00 (COMMENT [121] Example 5.15; inlined version of Cops #551 submitted by: Thomas Sternagel) 0.00/0.00 0.00/0.00 Removed infeasible rules as much as possible. 0.00/0.00 (CONDITIONTYPE ORIENTED) 0.00/0.00 (VAR x y xs) 0.00/0.00 (RULES 0.00/0.00 le(x,0) -> false 0.00/0.00 le(0,s(y)) -> true 0.00/0.00 le(s(x),s(y)) -> le(x,y) 0.00/0.00 min(cons(x,nil)) -> x 0.00/0.00 min(cons(x,xs)) -> x | le(x,min(xs)) == true 0.00/0.00 min(cons(x,xs)) -> min(xs) | le(x,min(xs)) == false 0.00/0.00 ) 0.00/0.00 (COMMENT [121] Example 5.15; inlined version of Cops #551 submitted by: Thomas Sternagel) 0.00/0.00 0.00/0.00 Try to disprove confluence of the following (C)TRS: 0.00/0.00 (CONDITIONTYPE ORIENTED) 0.00/0.00 (VAR x y xs) 0.00/0.00 (RULES 0.00/0.00 le(x,0) -> false 0.00/0.00 le(0,s(y)) -> true 0.00/0.00 le(s(x),s(y)) -> le(x,y) 0.00/0.00 min(cons(x,nil)) -> x 0.00/0.00 min(cons(x,xs)) -> x | le(x,min(xs)) == true 0.00/0.00 min(cons(x,xs)) -> min(xs) | le(x,min(xs)) == false 0.00/0.00 ) 0.00/0.00 (COMMENT [121] Example 5.15; inlined version of Cops #551 submitted by: Thomas Sternagel) 0.00/0.00 0.00/0.00 Failed either to apply SR and U for normal 1CTRSs to the above CTRS or to prove confluence of any converted TRSs. 0.00/0.00 0.00/0.00 Try to apply SR and U for 3DCTRSs to the above CTRS. 0.00/0.00 0.00/0.00 Succeeded in applying U for 3DCTRSs to the above CTRS. 0.00/0.00 U(R) = 0.00/0.00 (VAR x1 x2) 0.00/0.00 (RULES 0.00/0.00 le(x1,0) -> false 0.00/0.00 le(0,s(x1)) -> true 0.00/0.00 le(s(x1),s(x2)) -> le(x1,x2) 0.00/0.00 min(cons(x1,nil)) -> x1 0.00/0.00 min(cons(x1,x2)) -> u1(le(x1,min(x2)),x1,x2) 0.00/0.00 u1(true,x1,x2) -> x1 0.00/0.00 u1(false,x1,x2) -> min(x2) 0.00/0.00 ) 0.00/0.00 0.00/0.00 U for 3DCTRSs is sound for the above CTRS. 0.00/0.00 0.00/0.00 Failed to prove confluence of U(R). 0.00/0.00 0.00/0.00 Try to prove operational termination of R, i.e., termination of U(R). 0.00/0.00 0.00/0.00 Failed to prove operational termination of R. 0.00/0.00 0.00/0.00 MAYBE 0.00/0.00 EOF