0.00/0.01 YES 0.00/0.01 0.00/0.01 0.00/0.01 Succeeded in reading "/export/starexec/sandbox/benchmark/theBenchmark.trs". 0.00/0.01 (CONDITIONTYPE ORIENTED) 0.00/0.01 (VAR x) 0.00/0.01 (RULES 0.00/0.01 e(0) -> true 0.00/0.01 e(s(x)) -> true | o(x) == true 0.00/0.01 e(s(x)) -> false | e(x) == true 0.00/0.01 o(0) -> false 0.00/0.01 o(s(x)) -> true | e(x) == true 0.00/0.01 o(s(x)) -> false | o(x) == true 0.00/0.01 ) 0.00/0.01 (COMMENT [79] Example 8; correction of Cops #404 submitted by: Thomas Sternagel) 0.00/0.01 0.00/0.01 No "->="-rules. 0.00/0.01 0.00/0.01 Decomposed conditions if possible. 0.00/0.01 (CONDITIONTYPE ORIENTED) 0.00/0.01 (VAR x) 0.00/0.01 (RULES 0.00/0.01 e(0) -> true 0.00/0.01 e(s(x)) -> true | o(x) == true 0.00/0.01 e(s(x)) -> false | e(x) == true 0.00/0.01 o(0) -> false 0.00/0.01 o(s(x)) -> true | e(x) == true 0.00/0.01 o(s(x)) -> false | o(x) == true 0.00/0.01 ) 0.00/0.01 (COMMENT [79] Example 8; correction of Cops #404 submitted by: Thomas Sternagel) 0.00/0.01 0.00/0.01 Removed infeasible rules as much as possible. 0.00/0.01 (CONDITIONTYPE ORIENTED) 0.00/0.01 (VAR x) 0.00/0.01 (RULES 0.00/0.01 e(0) -> true 0.00/0.01 e(s(x)) -> true | o(x) == true 0.00/0.01 e(s(x)) -> false | e(x) == true 0.00/0.01 o(0) -> false 0.00/0.01 o(s(x)) -> true | e(x) == true 0.00/0.01 o(s(x)) -> false | o(x) == true 0.00/0.01 ) 0.00/0.01 (COMMENT [79] Example 8; correction of Cops #404 submitted by: Thomas Sternagel) 0.00/0.01 0.00/0.01 Try to disprove confluence of the following (C)TRS: 0.00/0.01 (CONDITIONTYPE ORIENTED) 0.00/0.01 (VAR x) 0.00/0.01 (RULES 0.00/0.01 e(0) -> true 0.00/0.01 e(s(x)) -> true | o(x) == true 0.00/0.01 e(s(x)) -> false | e(x) == true 0.00/0.01 o(0) -> false 0.00/0.01 o(s(x)) -> true | e(x) == true 0.00/0.01 o(s(x)) -> false | o(x) == true 0.00/0.01 ) 0.00/0.01 (COMMENT [79] Example 8; correction of Cops #404 submitted by: Thomas Sternagel) 0.00/0.01 0.00/0.01 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.01 0.00/0.01 Try to apply SR and U for 3DCTRSs to the above CTRS. 0.00/0.01 0.00/0.01 Succeeded in applying U for 3DCTRSs to the above CTRS. 0.00/0.01 U(R) = 0.00/0.01 (VAR x1) 0.00/0.01 (RULES 0.00/0.01 e(0) -> true 0.00/0.01 e(s(x1)) -> u1(o(x1),x1) 0.00/0.01 u1(true,x1) -> true 0.00/0.01 e(s(x1)) -> u2(e(x1),x1) 0.00/0.01 u2(true,x1) -> false 0.00/0.01 o(0) -> false 0.00/0.01 o(s(x1)) -> u3(e(x1),x1) 0.00/0.01 u3(true,x1) -> true 0.00/0.01 o(s(x1)) -> u4(o(x1),x1) 0.00/0.01 u4(true,x1) -> false 0.00/0.01 ) 0.00/0.01 0.00/0.01 U for 3DCTRSs is sound for the above CTRS. 0.00/0.01 0.00/0.01 Failed to prove confluence of U(R). 0.00/0.01 0.00/0.01 Try to prove operational termination of R, i.e., termination of U(R). 0.00/0.01 0.00/0.01 Succeeded in proving operational termination of R. 0.00/0.01 0.00/0.01 Try to prove joinability of all (conditional) CPs. 0.00/0.01 0.00/0.01 Succeeded in proving joinability of conditional CPs by means of narrowing trees. 0.00/0.01 0.00/0.01 YES 0.00/0.01 EOF