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 a -> b 0.00/0.00 f(x) -> A | x == b 0.00/0.00 g(x,x) -> h(x) 0.00/0.00 h(x) -> i(x) 0.00/0.00 ) 0.00/0.00 (COMMENT [75] Example 32 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 a -> b 0.00/0.00 f(x) -> A | x == b 0.00/0.00 g(x,x) -> h(x) 0.00/0.00 h(x) -> i(x) 0.00/0.00 ) 0.00/0.00 (COMMENT [75] Example 32 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 a -> b 0.00/0.00 f(x) -> A | x == b 0.00/0.00 g(x,x) -> h(x) 0.00/0.00 h(x) -> i(x) 0.00/0.00 ) 0.00/0.00 (COMMENT [75] Example 32 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 a -> b 0.00/0.00 f(x) -> A | x == b 0.00/0.00 g(x,x) -> h(x) 0.00/0.00 h(x) -> i(x) 0.00/0.00 ) 0.00/0.00 (COMMENT [75] Example 32 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 a -> b 0.00/0.00 f(x1) -> u1(x1,x1) 0.00/0.00 u1(b,x1) -> A 0.00/0.00 g(x1,x1) -> h(x1) 0.00/0.00 h(x1) -> i(x1) 0.00/0.00 ) 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 There is no conditional CP. 0.00/0.00 0.00/0.00 YES 0.00/0.00 EOF