0.00/0.00 YES 0.00/0.00 0.00/0.00 0.00/0.00 Succeeded in reading "/export/starexec/sandbox2/benchmark/theBenchmark.trs". 0.00/0.00 (CONDITIONTYPE ORIENTED) 0.00/0.00 (VAR x) 0.00/0.00 (RULES 0.00/0.00 e(0) -> true 0.00/0.00 e(s(x)) -> true | o(x) == true 0.00/0.00 e(s(x)) -> false | e(x) == true 0.00/0.00 o(0) -> false 0.00/0.00 o(s(x)) -> true | e(x) == true 0.00/0.00 o(s(x)) -> false | o(x) == true 0.00/0.00 ) 0.00/0.00 (COMMENT [79] Example 8; correction of Cops #404 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) 0.00/0.00 (RULES 0.00/0.00 e(0) -> true 0.00/0.00 e(s(x)) -> true | o(x) == true 0.00/0.00 e(s(x)) -> false | e(x) == true 0.00/0.00 o(0) -> false 0.00/0.00 o(s(x)) -> true | e(x) == true 0.00/0.00 o(s(x)) -> false | o(x) == true 0.00/0.00 ) 0.00/0.00 (COMMENT [79] Example 8; correction of Cops #404 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) 0.00/0.00 (RULES 0.00/0.00 e(0) -> true 0.00/0.00 e(s(x)) -> true | o(x) == true 0.00/0.00 e(s(x)) -> false | e(x) == true 0.00/0.00 o(0) -> false 0.00/0.00 o(s(x)) -> true | e(x) == true 0.00/0.00 o(s(x)) -> false | o(x) == true 0.00/0.00 ) 0.00/0.00 (COMMENT [79] Example 8; correction of Cops #404 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) 0.00/0.00 (RULES 0.00/0.00 e(0) -> true 0.00/0.00 e(s(x)) -> true | o(x) == true 0.00/0.00 e(s(x)) -> false | e(x) == true 0.00/0.00 o(0) -> false 0.00/0.00 o(s(x)) -> true | e(x) == true 0.00/0.00 o(s(x)) -> false | o(x) == true 0.00/0.00 ) 0.00/0.00 (COMMENT [79] Example 8; correction of Cops #404 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) 0.00/0.00 (RULES 0.00/0.00 e(0) -> true 0.00/0.00 e(s(x1)) -> u1(o(x1),x1) 0.00/0.00 u1(true,x1) -> true 0.00/0.00 e(s(x1)) -> u2(e(x1),x1) 0.00/0.00 u2(true,x1) -> false 0.00/0.00 o(0) -> false 0.00/0.00 o(s(x1)) -> u3(e(x1),x1) 0.00/0.00 u3(true,x1) -> true 0.00/0.00 o(s(x1)) -> u4(o(x1),x1) 0.00/0.00 u4(true,x1) -> false 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 Succeeded in proving operational termination of R. 0.00/0.00 0.00/0.00 Try to prove joinability of all (conditional) CPs. 0.00/0.00 0.00/0.00 Succeeded in proving joinability of conditional CPs by means of narrowing trees. 0.00/0.00 0.00/0.00 YES 0.00/0.00 EOF