0.00/0.00 YES 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 f(x) -> a | x == a 0.00/0.00 f(x) -> b | x == b 0.00/0.00 ) 0.00/0.00 (COMMENT COPS 547) 0.00/0.00 (COMMENT doi:10.4230/LIPIcs.FSCD.2016.29 [90] Example 3 submitted by: Raul Gutierrez and Salvador Lucas) 0.00/0.00 0.00/0.00 No "->="-rules. 0.00/0.00 0.00/0.00 (CONDITION 0.00/0.00 x == a, x == b 0.00/0.00 ) 0.00/0.00 0.00/0.00 This is ultra-RL and deterministic. 0.00/0.00 0.00/0.00 This is operationally terminating and confluent. 0.00/0.00 0.00/0.00 (RTG_of_NARROWINGTREE 0.00/0.00 (START 0.00/0.00 Gamma[x == a : { e } & x == b : { e }] 0.00/0.00 ) 0.00/0.00 (NONTERMINALS 0.00/0.00 Gamma[x == a : { e } & x == b : { e }] 0.00/0.00 ) 0.00/0.00 (RULES 0.00/0.00 Gamma[x == a : { e } & x == b : { e }] -> EmptySet 0.00/0.00 ) 0.00/0.00 ) 0.00/0.00 0.00/0.00 YES 0.00/0.00 EOF