0.00/0.00 YES 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 g(x) -> x | x == a, b == x 0.00/0.00 ) 0.00/0.00 (COMMENT [121] Example 3.3 submitted by: Thomas Sternagel) 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 g(b) -> b | b == a 0.00/0.00 ) 0.00/0.00 (COMMENT [121] Example 3.3 submitted by: Thomas Sternagel) 0.00/0.00 0.00/0.00 Removed infeasible rules as much as possible. 0.00/0.00 (VAR x) 0.00/0.00 (COMMENT [121] Example 3.3 submitted by: Thomas Sternagel) 0.00/0.00 0.00/0.00 Try to disprove confluence of the following (C)TRS: 0.00/0.00 (VAR x) 0.00/0.00 (COMMENT [121] Example 3.3 submitted by: Thomas Sternagel) 0.00/0.00 0.00/0.00 Try to prove confluence of the following TRS: 0.00/0.00 (VAR x) 0.00/0.00 (COMMENT [121] Example 3.3 submitted by: Thomas Sternagel) 0.00/0.00 0.00/0.00 Succeeded in proving confluence due to orthogonality. 0.00/0.00 0.00/0.00 Proved via the following orthogonal TRS: 0.00/0.00 (VAR x) 0.00/0.00 (COMMENT [121] Example 3.3 submitted by: Thomas Sternagel) 0.00/0.00 0.00/0.00 YES 0.00/0.00 EOF