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) 0.00/0.00 (RULES 0.00/0.00 odd(0) -> false 0.00/0.00 odd(s(x)) -> true | eq(even(x),true) == eq(T,T) 0.00/0.00 odd(s(x)) -> false | eq(even(x),false) == eq(T,T) 0.00/0.00 even(0) -> true 0.00/0.00 even(s(x)) -> true | eq(odd(x),true) == eq(T,T) 0.00/0.00 even(s(x)) -> false | eq(odd(x),false) == eq(T,T) 0.00/0.00 eq(x,x) -> eq(T,T) 0.00/0.00 ) 0.00/0.00 (COMMENT doi:10.2168/LMCS-8 ( 3:4 ) 2012 [64] Example 5.10 ( Norm ( R_12 ) ) submitted by: Thomas Sternagel and Aart Middeldorp) 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 odd(0) -> false 0.00/0.00 odd(s(x)) -> true | eq(even(x),true) == eq(T,T) 0.00/0.00 odd(s(x)) -> false | eq(even(x),false) == eq(T,T) 0.00/0.00 even(0) -> true 0.00/0.00 even(s(x)) -> true | eq(odd(x),true) == eq(T,T) 0.00/0.00 even(s(x)) -> false | eq(odd(x),false) == eq(T,T) 0.00/0.00 eq(x,x) -> eq(T,T) 0.00/0.00 ) 0.00/0.00 (COMMENT doi:10.2168/LMCS-8 ( 3:4 ) 2012 [64] Example 5.10 ( Norm ( R_12 ) ) submitted by: Thomas Sternagel and Aart Middeldorp) 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 odd(0) -> false 0.00/0.00 odd(s(x)) -> true | eq(even(x),true) == eq(T,T) 0.00/0.00 odd(s(x)) -> false | eq(even(x),false) == eq(T,T) 0.00/0.00 even(0) -> true 0.00/0.00 even(s(x)) -> true | eq(odd(x),true) == eq(T,T) 0.00/0.00 even(s(x)) -> false | eq(odd(x),false) == eq(T,T) 0.00/0.00 eq(x,x) -> eq(T,T) 0.00/0.00 ) 0.00/0.00 (COMMENT doi:10.2168/LMCS-8 ( 3:4 ) 2012 [64] Example 5.10 ( Norm ( R_12 ) ) submitted by: Thomas Sternagel and Aart Middeldorp) 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 odd(0) -> false 0.00/0.00 odd(s(x)) -> true | eq(even(x),true) == eq(T,T) 0.00/0.00 odd(s(x)) -> false | eq(even(x),false) == eq(T,T) 0.00/0.00 even(0) -> true 0.00/0.00 even(s(x)) -> true | eq(odd(x),true) == eq(T,T) 0.00/0.00 even(s(x)) -> false | eq(odd(x),false) == eq(T,T) 0.00/0.00 eq(x,x) -> eq(T,T) 0.00/0.00 ) 0.00/0.00 (COMMENT doi:10.2168/LMCS-8 ( 3:4 ) 2012 [64] Example 5.10 ( Norm ( R_12 ) ) submitted by: Thomas Sternagel and Aart Middeldorp) 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 odd(0) -> false 0.00/0.00 odd(s(x1)) -> u1(eq(even(x1),true),x1) 0.00/0.00 u1(eq(T,T),x1) -> true 0.00/0.00 odd(s(x1)) -> u2(eq(even(x1),false),x1) 0.00/0.00 u2(eq(T,T),x1) -> false 0.00/0.00 even(0) -> true 0.00/0.00 even(s(x1)) -> u3(eq(odd(x1),true),x1) 0.00/0.00 u3(eq(T,T),x1) -> true 0.00/0.00 even(s(x1)) -> u4(eq(odd(x1),false),x1) 0.00/0.00 u4(eq(T,T),x1) -> false 0.00/0.00 eq(x1,x1) -> eq(T,T) 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