0.00/0.09 MAYBE 0.00/0.09 (ignored inputs)COMMENT doi:10.1016/j.jlap.2009.08.001 [73] Example 3 submitted by: Thomas Sternagel and Aart Middeldorp 0.00/0.09 Conditional Rewrite Rules: 0.00/0.09 [ a -> c, 0.00/0.09 a -> d, 0.00/0.09 b -> c, 0.00/0.09 b -> d, 0.00/0.09 c -> e, 0.00/0.09 c -> l, 0.00/0.09 d -> m, 0.00/0.09 k -> l, 0.00/0.09 k -> m, 0.00/0.09 h(?x,?x) -> g(?x,?x,f(k)), 0.00/0.09 g(d,?x,?x) -> A, 0.00/0.09 A -> h(f(a),f(b)), 0.00/0.09 f(?x) -> ?x | ?x == e ] 0.00/0.09 Check whether all rules are type 3 0.00/0.09 OK 0.00/0.09 Check whether the input is deterministic 0.00/0.09 OK 0.00/0.09 Result of unraveling: 0.00/0.09 [ a -> c, 0.00/0.09 a -> d, 0.00/0.09 b -> c, 0.00/0.09 b -> d, 0.00/0.09 c -> e, 0.00/0.09 c -> l, 0.00/0.09 d -> m, 0.00/0.09 k -> l, 0.00/0.09 k -> m, 0.00/0.09 h(?x,?x) -> g(?x,?x,f(k)), 0.00/0.09 g(d,?x,?x) -> A, 0.00/0.09 A -> h(f(a),f(b)), 0.00/0.09 f(?x) -> U0(?x,?x), 0.00/0.09 U0(e,?x) -> ?x ] 0.00/0.09 Check whether U(R) is terminating 0.00/0.09 failed to show termination 0.00/0.09 Check whether the input is weakly left-linear 0.00/0.09 not weakly left-linear 0.00/0.09 Conditional critical pairs (CCPs): 0.00/0.09 [ d = c, 0.00/0.09 c = d, 0.00/0.09 d = c, 0.00/0.09 c = d, 0.00/0.09 l = e, 0.00/0.09 e = l, 0.00/0.09 m = l, 0.00/0.09 l = m, 0.00/0.09 g(m,?x_1,?x_1) = A ] 0.00/0.09 Check whether the input is almost orthogonale 0.00/0.09 not almost orthogonal 0.00/0.09 not weakly left-linear 0.00/0.09 /export/starexec/sandbox2/benchmark/theBenchmark.trs: Failure(unknown CR) 0.00/0.09 (54 msec.) 0.00/0.09 EOF