NO
(ignored inputs)COMMENT TPDB SRS_Standard/Waldmann_07_size12/size-12-alpha-3-num-412
Rewrite Rules:
   [ a(?x) -> b(?x),
     b(b(c(?x))) -> c(a(c(a(a(?x))))),
     c(c(?x)) -> ?x ]
Apply Direct Methods...
Inner CPs:
   [ b(b(?x_2)) = c(a(c(a(a(c(?x_2)))))),
     c(?x) = c(?x) ]
Outer CPs:
   [  ]
not Overlay, check Termination...
unknown/not Terminating
unknown Knuth & Bendix
Linear
unknown Development Closed
unknown Strongly Closed
unknown Weakly-Non-Overlapping & Non-Collapsing & Shallow
inner CP cond (upside-parallel)
innter CP Cond (outside)
unknown Upside-Parallel-Closed/Outside-Closed
(inner) Parallel CPs: (not computed)
unknown Toyama (Parallel CPs)
Simultaneous CPs:
   [ b(b(?x_3)) = c(a(c(a(a(c(?x_3)))))),
     c(?x_1) = c(?x_1),
     ?x_1 = c(c(?x_1)),
     c(a(c(a(a(?x_1))))) = b(b(c(?x_1))),
     c(a(c(a(a(c(?x)))))) = b(b(?x)) ]
unknown Okui (Simultaneous CPs)
unknown Strongly Depth-Preserving & Root-E-Closed/Non-E-Overlapping
unknown Strongly Weight-Preserving & Root-E-Closed/Non-E-Overlapping
check Locally Decreasing Diagrams by Rule Labelling...
Critical Pair <b(b(?x_2)), c(a(c(a(a(c(?x_2))))))> by Rules <2, 1> preceded by [(b,1),(b,1)]
unknown Diagram Decreasing
check Non-Confluence...
obtain 7 rules by 3 steps unfolding
obtain 59 candidates for checking non-joinability
check by TCAP-Approximation (failure)
check by Ordering(rpo), check by Tree-Automata Approximation (success)
<F,Q,Q_f,Delta> where
   F = {(a,1),(b,1),(c,1),(c_1,0)}
   Q = {q_0,q_1,q_{a(c(a(a(*))))},q_{a(c(c_1))},q_{c(a(a(c(c_1))))},q_{a(a(*))},q_{b(c_1)},q_{c_1},q_{a(c(a(a(c(c_1)))))},q_{*},q_{a(*)},q_{c(a(a(*)))},q_{a(a(c(c_1)))},q_{c(c_1)}}
   Qf = {q_0,q_1}
   Delta = 
   [ a(q_{a(c(c_1))}) -> q_{a(a(c(c_1)))},
     a(q_{c(a(a(c(c_1))))}) -> q_{a(c(a(a(c(c_1)))))},
     a(q_{b(c_1)}) -> q_1,
     a(q_{*}) -> q_{*},
     a(q_{*}) -> q_{a(*)},
     a(q_{a(*)}) -> q_{a(a(*))},
     a(q_{c(a(a(*)))}) -> q_0,
     a(q_{c(a(a(*)))}) -> q_{a(c(a(a(*))))},
     a(q_{c(a(a(*)))}) -> q_{c(a(a(c(c_1))))},
     a(q_{c(a(a(*)))}) -> q_{a(a(*))},
     a(q_{c(a(a(*)))}) -> q_{a(c(a(a(c(c_1)))))},
     a(q_{c(a(a(*)))}) -> q_{a(*)},
     a(q_{c(a(a(*)))}) -> q_{c(a(a(*)))},
     a(q_{c(a(a(*)))}) -> q_{a(a(c(c_1)))},
     a(q_{c(c_1)}) -> q_{a(c(c_1))},
     b(q_{a(c(c_1))}) -> q_{a(a(c(c_1)))},
     b(q_{c(a(a(c(c_1))))}) -> q_{a(c(a(a(c(c_1)))))},
     b(q_{b(c_1)}) -> q_1,
     b(q_{c_1}) -> q_{b(c_1)},
     b(q_{*}) -> q_{*},
     b(q_{*}) -> q_{a(*)},
     b(q_{a(*)}) -> q_{a(a(*))},
     b(q_{c(a(a(*)))}) -> q_0,
     b(q_{c(a(a(*)))}) -> q_{a(c(a(a(*))))},
     b(q_{c(a(a(*)))}) -> q_{c(a(a(c(c_1))))},
     b(q_{c(a(a(*)))}) -> q_{a(a(*))},
     b(q_{c(a(a(*)))}) -> q_{a(c(a(a(c(c_1)))))},
     b(q_{c(a(a(*)))}) -> q_{a(*)},
     b(q_{c(a(a(*)))}) -> q_{c(a(a(*)))},
     b(q_{c(a(a(*)))}) -> q_{a(a(c(c_1)))},
     b(q_{c(c_1)}) -> q_{a(c(c_1))},
     c(q_{a(c(a(a(*))))}) -> q_0,
     c(q_{a(c(a(a(*))))}) -> q_{a(c(a(a(*))))},
     c(q_{a(c(a(a(*))))}) -> q_{c(a(a(c(c_1))))},
     c(q_{a(c(a(a(*))))}) -> q_{a(a(*))},
     c(q_{a(c(a(a(*))))}) -> q_{a(c(a(a(c(c_1)))))},
     c(q_{a(c(a(a(*))))}) -> q_{a(*)},
     c(q_{a(c(a(a(*))))}) -> q_{c(a(a(*)))},
     c(q_{a(c(a(a(*))))}) -> q_{a(a(c(c_1)))},
     c(q_{a(a(*))}) -> q_{c(a(a(*)))},
     c(q_{c_1}) -> q_{c(c_1)},
     c(q_{a(c(a(a(c(c_1)))))}) -> q_0,
     c(q_{*}) -> q_{*},
     c(q_{a(a(c(c_1)))}) -> q_{c(a(a(c(c_1))))},
     c_1 -> q_{c_1},
     c_1 -> q_{*} ]
 (failure)
check by Interpretation(mod2) (failure)
check by Descendants-Approximation, check by Ordering(poly) (success)
Polynomial Interpretation:
  a:= (2)*x1
  b:= (2)*x1
  c:= (1)*x1
  c_1:= (1)
 [b(?x)]-[a(?x)] = 0 >= 0
 [?x]-[c(c(?x))] = 0 >= 0
 [c(a(c(a(a(?x)))))]-[b(b(c(?x)))] = (4)*x1 >= 0
 [c(a(c(a(a(c(c_1))))))]-[b(b(c_1))] = (4) > 0
 (success)
Witness for Non-Confluence: <c(a(c(a(a(c(c_1)))))) <- b(b(c(c(c(c(c_1)))))) -> b(b(c_1))>
Direct Methods: not CR

Combined result: not CR
980.trs: Success(not CR)
(586 msec.)