0.00/0.00 NO 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 y x) 0.00/0.00 (RULES 0.00/0.00 f(x) -> c(x,y) | g(x) == y, y == h(x) 0.00/0.00 a -> b 0.00/0.00 g(a) -> h(b) 0.00/0.00 ) 0.00/0.00 (COMMENT doi:10.2168/LMCS-8 ( 3:4 ) 2012 [64] Example 4.8 ( R_8 ) 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 y x) 0.00/0.00 (RULES 0.00/0.00 f(x) -> c(x,y) | g(x) == y, y == h(x) 0.00/0.00 a -> b 0.00/0.00 g(a) -> h(b) 0.00/0.00 ) 0.00/0.00 (COMMENT doi:10.2168/LMCS-8 ( 3:4 ) 2012 [64] Example 4.8 ( R_8 ) 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 y x) 0.00/0.00 (RULES 0.00/0.00 f(x) -> c(x,y) | g(x) == y, y == h(x) 0.00/0.00 a -> b 0.00/0.00 g(a) -> h(b) 0.00/0.00 ) 0.00/0.00 (COMMENT doi:10.2168/LMCS-8 ( 3:4 ) 2012 [64] Example 4.8 ( R_8 ) 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 y x) 0.00/0.00 (RULES 0.00/0.00 f(x) -> c(x,y) | g(x) == y, y == h(x) 0.00/0.00 a -> b 0.00/0.00 g(a) -> h(b) 0.00/0.00 ) 0.00/0.00 (COMMENT doi:10.2168/LMCS-8 ( 3:4 ) 2012 [64] Example 4.8 ( R_8 ) submitted by: Thomas Sternagel and Aart Middeldorp) 0.00/0.00 0.00/0.00 Succeeded in disproving confluence. 0.00/0.00 0.00/0.00 Disproved via the following (C)TRS: 0.00/0.00 (CONDITIONTYPE ORIENTED) 0.00/0.00 (VAR y x) 0.00/0.00 (RULES 0.00/0.00 f(x) -> c(x,y) | g(x) == y, y == h(x) 0.00/0.00 a -> b 0.00/0.00 g(a) -> h(b) 0.00/0.00 ) 0.00/0.00 (COMMENT doi:10.2168/LMCS-8 ( 3:4 ) 2012 [64] Example 4.8 ( R_8 ) submitted by: Thomas Sternagel and Aart Middeldorp) 0.00/0.00 0.00/0.00 NO 0.00/0.00 EOF