NO
(ignored inputs)COMMENT doi:10.2168/LMCS-8 ( 3:4 ) 2012 cops number: 315 submitted by: Thomas Sternagel , Aart Middeldorp [64] Example 3.3 ( R_3 )
Conditional Rewrite Rules:
   [ f(?x) -> ?x | ?x == e,
     g(d,?x,?x) -> A,
     h(?x,?x) -> g(?x,?x,f(k)),
     a -> c,
     a -> d,
     b -> c,
     b -> d,
     c -> e,
     c -> l,
     k -> l,
     k -> m,
     d -> m ]
Check whether all rules are type 3
OK
Check whether the input is deterministic
OK
Result of unraveling:
   [ f(?x) -> U0(?x,?x),
     U0(e,?x) -> ?x,
     g(d,?x,?x) -> A,
     h(?x,?x) -> g(?x,?x,f(k)),
     a -> c,
     a -> d,
     b -> c,
     b -> d,
     c -> e,
     c -> l,
     k -> l,
     k -> m,
     d -> m ]
Check whether U(R) is terminating
OK
Check whether the input is weakly left-linear
not weakly left-linear
Check whether U(R) is confluent
U(R) is not confluent
Conditional critical pairs (CCPs):
   [ g(m,?x_1,?x_1) = A,
     d = c,
     c = d,
     d = c,
     c = d,
     l = e,
     e = l,
     m = l,
     l = m ]
Check whether the input is almost orthogonale
not almost orthogonal
not weakly left-linear
Check whether the input is absolutely irreducible
OK
Check whether all CCPs are joinable
Some ccp may be feasible but not joinable
   [ g(m,?x_1,?x_1) = A,
     d = c,
     c = d,
     d = c,
     c = d,
     l = e,
     e = l,
     m = l,
     l = m ]
A feasible but not joinable CCP: g(m,?x_1,?x_1) = A
cops-RYoQ7jVe.trs: Success(not CR)
(2 msec.)