0.00/0.00 NO 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 a -> c 0.00/0.00 a -> d 0.00/0.00 b -> c 0.00/0.00 b -> d 0.00/0.00 g(x,x) -> h(x,x) 0.00/0.00 f(x) -> x | x == c 0.00/0.00 ) 0.00/0.00 (COMMENT [75] Example 34 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 -> c 0.00/0.00 a -> d 0.00/0.00 b -> c 0.00/0.00 b -> d 0.00/0.00 g(x,x) -> h(x,x) 0.00/0.00 f(x) -> x | x == c 0.00/0.00 ) 0.00/0.00 (COMMENT [75] Example 34 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 -> c 0.00/0.00 a -> d 0.00/0.00 b -> c 0.00/0.00 b -> d 0.00/0.00 g(x,x) -> h(x,x) 0.00/0.00 f(x) -> x | x == c 0.00/0.00 ) 0.00/0.00 (COMMENT [75] Example 34 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 -> c 0.00/0.00 a -> d 0.00/0.00 b -> c 0.00/0.00 b -> d 0.00/0.00 g(x,x) -> h(x,x) 0.00/0.00 f(x) -> x | x == c 0.00/0.00 ) 0.00/0.00 (COMMENT [75] Example 34 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 x) 0.00/0.00 (RULES 0.00/0.00 a -> c 0.00/0.00 a -> d 0.00/0.00 b -> c 0.00/0.00 b -> d 0.00/0.00 g(x,x) -> h(x,x) 0.00/0.00 f(x) -> x | x == c 0.00/0.00 ) 0.00/0.00 (COMMENT [75] Example 34 submitted by: Thomas Sternagel and Aart Middeldorp) 0.00/0.00 0.00/0.00 NO 0.00/0.00 EOF