(ignored inputs)COMMENT submitted by: Raul Gutierrez secret problem 2021 category: SRS
Rewrite Rules:
   [ a(b(?x)) -> b(c(?x)),
     a(c(?x)) -> c(a(?x)),
     b(b(?x)) -> a(c(?x)),
     c(b(?x)) -> b(c(?x)),
     c(b(?x)) -> c(c(?x)),
     c(c(?x)) -> c(b(?x)),
     P(?x) -> Q(Q(p(?x))),
     p(p(?x)) -> q(q(?x)),
     p(Q(Q(?x))) -> Q(Q(p(?x))),
     Q(p(q(?x))) -> q(p(Q(?x))),
     q(q(p(?x))) -> p(q(q(?x))),
     q(Q(?x)) -> ?x,
     Q(q(?x)) -> ?x,
     p(P(?x)) -> ?x,
     P(p(?x)) -> ?x ]
Apply Direct Methods...
Inner CPs:
   [ a(a(c(?x_2))) = b(c(b(?x_2))),
     a(b(c(?x_3))) = c(a(b(?x_3))),
     a(c(c(?x_4))) = c(a(b(?x_4))),
     a(c(b(?x_5))) = c(a(c(?x_5))),
     c(a(c(?x_2))) = b(c(b(?x_2))),
     c(a(c(?x_2))) = c(c(b(?x_2))),
     c(b(c(?x_3))) = c(b(b(?x_3))),
     c(c(c(?x_4))) = c(b(b(?x_4))),
     p(Q(Q(p(?x_8)))) = q(q(Q(Q(?x_8)))),
     p(?x_13) = q(q(P(?x_13))),
     p(Q(q(p(Q(?x_9))))) = Q(Q(p(p(q(?x_9))))),
     p(Q(?x_12)) = Q(Q(p(q(?x_12)))),
     Q(p(p(q(q(?x_10))))) = q(p(Q(q(p(?x_10))))),
     Q(p(?x_11)) = q(p(Q(Q(?x_11)))),
     q(q(q(q(?x_7)))) = p(q(q(p(?x_7)))),
     q(q(Q(Q(p(?x_8))))) = p(q(q(Q(Q(?x_8))))),
     q(q(?x_13)) = p(q(q(P(?x_13)))),
     q(q(p(Q(?x_9)))) = p(q(?x_9)),
     q(?x_12) = q(?x_12),
     Q(p(q(q(?x_10)))) = q(p(?x_10)),
     Q(?x_11) = Q(?x_11),
     p(Q(Q(p(?x_6)))) = ?x_6,
     p(?x_14) = p(?x_14),
     P(q(q(?x_7))) = p(?x_7),
     P(Q(Q(p(?x_8)))) = Q(Q(?x_8)),
     P(?x_13) = P(?x_13),
     b(a(c(?x))) = a(c(b(?x))),
     c(c(b(?x))) = c(b(c(?x))),
     p(q(q(?x))) = q(q(p(?x))) ]
Outer CPs:
   [ b(c(?x_3)) = c(c(?x_3)),
     Q(Q(p(p(?x_14)))) = ?x_14 ]
not Overlay, check Termination...
unknown/not Terminating
unknown Knuth & Bendix
Linear
unknown Development Closed
unknown Strongly Closed
unknown Weakly-Non-Overlapping & Non-Collapsing & Shallow
unknown Upside-Parallel-Closed/Outside-Closed
(inner) Parallel CPs: (not computed)
unknown Toyama (Parallel CPs)
Simultaneous CPs:
   [ a(a(c(?x_3))) = b(c(b(?x_3))),
     a(b(c(?x_4))) = c(a(b(?x_4))),
     a(c(c(?x_5))) = c(a(b(?x_5))),
     a(c(b(?x_6))) = c(a(c(?x_6))),
     b(a(c(?x_1))) = a(c(b(?x_1))),
     a(c(a(c(?x_1)))) = b(a(c(b(?x_1)))),
     b(c(a(c(?x_1)))) = a(a(c(b(?x_1)))),
     b(c(a(c(?x_1)))) = c(a(c(b(?x_1)))),
     c(c(a(c(?x_1)))) = c(a(c(b(?x_1)))),
     a(c(b(?x))) = b(a(c(?x))),
     b(c(b(?x))) = a(a(c(?x))),
     b(c(b(?x))) = c(a(c(?x))),
     c(c(b(?x))) = c(a(c(?x))),
     c(c(?x)) = b(c(?x)),
     c(a(c(?x_4))) = b(c(b(?x_4))),
     c(a(a(c(?x_4)))) = a(b(c(b(?x_4)))),
     c(b(a(c(?x_4)))) = c(b(c(b(?x_4)))),
     c(a(b(?x))) = a(b(c(?x))),
     c(b(b(?x))) = c(b(c(?x))),
     b(c(?x)) = c(c(?x)),
     c(a(c(?x_4))) = c(c(b(?x_4))),
     c(a(a(c(?x_4)))) = a(c(c(b(?x_4)))),
     c(b(a(c(?x_4)))) = c(c(c(b(?x_4)))),
     c(a(b(?x))) = a(c(c(?x))),
     c(b(b(?x))) = c(c(c(?x))),
     c(c(b(?x_1))) = c(b(c(?x_1))),
     c(b(c(?x_5))) = c(b(b(?x_5))),
     c(c(c(?x_6))) = c(b(b(?x_6))),
     c(b(c(b(?x_1)))) = c(c(b(c(?x_1)))),
     c(b(b(c(?x_5)))) = c(c(b(b(?x_5)))),
     c(b(c(c(?x_6)))) = c(c(b(b(?x_6)))),
     c(a(c(b(?x_1)))) = a(c(b(c(?x_1)))),
     c(a(b(c(?x_5)))) = a(c(b(b(?x_5)))),
     c(a(c(c(?x_6)))) = a(c(b(b(?x_6)))),
     c(b(c(?x))) = c(c(b(?x))),
     c(a(c(?x))) = a(c(b(?x))),
     ?x_14 = Q(Q(p(p(?x_14)))),
     ?x = p(Q(Q(p(?x)))),
     p(q(q(?x_1))) = q(q(p(?x_1))),
     p(Q(Q(p(?x_9)))) = q(q(Q(Q(?x_9)))),
     p(?x_14) = q(q(P(?x_14))),
     q(q(q(q(?x_1)))) = p(q(q(p(?x_1)))),
     q(q(Q(Q(p(?x_9))))) = p(q(q(Q(Q(?x_9))))),
     q(q(?x_14)) = p(q(q(P(?x_14)))),
     p(q(q(q(q(?x_1))))) = q(q(q(q(p(?x_1))))),
     p(q(q(Q(Q(p(?x_9)))))) = q(q(q(q(Q(Q(?x_9)))))),
     p(q(q(?x_14))) = q(q(q(q(P(?x_14))))),
     q(q(?x_1)) = P(q(q(p(?x_1)))),
     Q(Q(p(?x_9))) = P(q(q(Q(Q(?x_9))))),
     ?x_14 = P(q(q(P(?x_14)))),
     q(q(p(?x))) = p(q(q(?x))),
     p(q(q(p(?x)))) = q(q(q(q(?x)))),
     p(?x) = P(q(q(?x))),
     p(Q(q(p(Q(?x_10))))) = Q(Q(p(p(q(?x_10))))),
     p(Q(?x_13)) = Q(Q(p(q(?x_13)))),
     q(q(Q(q(p(Q(?x_10)))))) = p(Q(Q(p(p(q(?x_10)))))),
     q(q(Q(?x_13))) = p(Q(Q(p(q(?x_13))))),
     p(q(q(Q(q(p(Q(?x_10))))))) = q(q(Q(Q(p(p(q(?x_10))))))),
     p(q(q(Q(?x_13)))) = q(q(Q(Q(p(q(?x_13)))))),
     Q(q(p(Q(?x_10)))) = P(Q(Q(p(p(q(?x_10)))))),
     Q(?x_13) = P(Q(Q(p(q(?x_13))))),
     q(q(Q(Q(?x)))) = p(Q(Q(p(?x)))),
     p(q(q(Q(Q(?x))))) = q(q(Q(Q(p(?x))))),
     Q(Q(?x)) = P(Q(Q(p(?x)))),
     Q(p(p(q(q(?x_11))))) = q(p(Q(q(p(?x_11))))),
     Q(p(?x_12)) = q(p(Q(Q(?x_12)))),
     Q(Q(p(p(p(q(q(?x_11))))))) = p(Q(q(p(Q(q(p(?x_11))))))),
     Q(Q(p(p(?x_12)))) = p(Q(q(p(Q(Q(?x_12)))))),
     p(p(q(q(?x_11)))) = q(q(p(Q(q(p(?x_11)))))),
     p(?x_12) = q(q(p(Q(Q(?x_12))))),
     Q(Q(p(p(q(?x))))) = p(Q(q(p(Q(?x))))),
     p(q(?x)) = q(q(p(Q(?x)))),
     q(p(Q(q(q(q(?x_9)))))) = Q(p(p(q(q(p(?x_9)))))),
     q(p(Q(q(Q(Q(p(?x_10))))))) = Q(p(p(q(q(Q(Q(?x_10))))))),
     q(p(Q(q(?x_14)))) = Q(p(p(q(q(P(?x_14)))))),
     q(q(q(?x_9))) = Q(p(q(q(p(?x_9))))),
     q(Q(Q(p(?x_10)))) = Q(p(q(q(Q(Q(?x_10)))))),
     q(?x_14) = Q(p(q(q(P(?x_14))))),
     q(p(Q(q(p(?x))))) = Q(p(p(q(q(?x))))),
     q(p(?x)) = Q(p(q(q(?x)))),
     q(q(p(Q(?x_11)))) = p(q(?x_11)),
     q(?x_13) = q(?x_13),
     q(p(Q(q(p(Q(?x_11)))))) = Q(p(p(q(?x_11)))),
     q(p(Q(?x_13))) = Q(p(q(?x_13))),
     ?x_13 = Q(q(?x_13)),
     q(p(Q(Q(?x)))) = Q(p(?x)),
     Q(?x) = Q(?x),
     Q(p(q(q(?x_12)))) = q(p(?x_12)),
     Q(Q(p(p(q(q(?x_12)))))) = p(Q(q(p(?x_12)))),
     Q(Q(p(?x_13))) = p(Q(Q(?x_13))),
     ?x_13 = q(Q(?x_13)),
     Q(Q(p(q(?x)))) = p(Q(?x)),
     p(Q(Q(p(?x)))) = ?x,
     p(?x_15) = p(?x_15),
     q(q(Q(Q(p(?x))))) = p(?x),
     q(q(?x_15)) = p(p(?x_15)),
     p(q(q(Q(Q(p(?x)))))) = q(q(?x)),
     Q(Q(p(?x))) = P(?x),
     ?x_15 = P(p(?x_15)),
     q(q(P(?x))) = p(?x),
     p(q(q(P(?x)))) = q(q(?x)),
     P(?x) = P(?x),
     Q(Q(p(q(q(?x_9))))) = p(?x_9),
     Q(Q(p(Q(Q(p(?x_10)))))) = Q(Q(?x_10)),
     Q(Q(p(p(?x)))) = ?x,
     P(q(q(?x_9))) = p(?x_9),
     P(Q(Q(p(?x_10)))) = Q(Q(?x_10)),
     ?x_15 = p(P(?x_15)) ]
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 <a(a(c(?x_2))), b(c(b(?x_2)))> by Rules <2, 0> preceded by [(a,1)]
unknown Diagram Decreasing
check Non-Confluence...
obtain 17 rules by 3 steps unfolding
obtain 100 candidates for checking non-joinability
check by TCAP-Approximation (failure)
check by Ordering(rpo), check by Tree-Automata Approximation (failure)
check by Interpretation(mod2) (failure)
check by Descendants-Approximation, check by Ordering(poly) (failure)
unknown Non-Confluence
unknown Huet (modulo AC)
check by Reduction-Preserving Completion...
STEP: 1 (parallel)
S:
   [ a(b(?x)) -> b(c(?x)),
     a(c(?x)) -> c(a(?x)),
     b(b(?x)) -> a(c(?x)),
     c(b(?x)) -> b(c(?x)),
     P(?x) -> Q(Q(p(?x))),
     p(p(?x)) -> q(q(?x)),
     p(Q(Q(?x))) -> Q(Q(p(?x))),
     Q(p(q(?x))) -> q(p(Q(?x))),
     q(q(p(?x))) -> p(q(q(?x))),
     q(Q(?x)) -> ?x,
     Q(q(?x)) -> ?x,
     p(P(?x)) -> ?x,
     P(p(?x)) -> ?x ]
P:
   [ c(b(?x)) -> c(c(?x)),
     c(c(?x)) -> c(b(?x)) ]
S: unknown termination
failure(Step 1)
STEP: 2 (linear)
S:
   [ a(b(?x)) -> b(c(?x)),
     a(c(?x)) -> c(a(?x)),
     b(b(?x)) -> a(c(?x)),
     c(b(?x)) -> b(c(?x)),
     P(?x) -> Q(Q(p(?x))),
     p(p(?x)) -> q(q(?x)),
     p(Q(Q(?x))) -> Q(Q(p(?x))),
     Q(p(q(?x))) -> q(p(Q(?x))),
     q(q(p(?x))) -> p(q(q(?x))),
     q(Q(?x)) -> ?x,
     Q(q(?x)) -> ?x,
     p(P(?x)) -> ?x,
     P(p(?x)) -> ?x ]
P:
   [ c(b(?x)) -> c(c(?x)),
     c(c(?x)) -> c(b(?x)) ]
S: unknown termination
failure(Step 2)
STEP: 3 (relative)
S:
   [ a(b(?x)) -> b(c(?x)),
     a(c(?x)) -> c(a(?x)),
     b(b(?x)) -> a(c(?x)),
     c(b(?x)) -> b(c(?x)),
     P(?x) -> Q(Q(p(?x))),
     p(p(?x)) -> q(q(?x)),
     p(Q(Q(?x))) -> Q(Q(p(?x))),
     Q(p(q(?x))) -> q(p(Q(?x))),
     q(q(p(?x))) -> p(q(q(?x))),
     q(Q(?x)) -> ?x,
     Q(q(?x)) -> ?x,
     p(P(?x)) -> ?x,
     P(p(?x)) -> ?x ]
P:
   [ c(b(?x)) -> c(c(?x)),
     c(c(?x)) -> c(b(?x)) ]
Check relative termination:
   [ a(b(?x)) -> b(c(?x)),
     a(c(?x)) -> c(a(?x)),
     b(b(?x)) -> a(c(?x)),
     c(b(?x)) -> b(c(?x)),
     P(?x) -> Q(Q(p(?x))),
     p(p(?x)) -> q(q(?x)),
     p(Q(Q(?x))) -> Q(Q(p(?x))),
     Q(p(q(?x))) -> q(p(Q(?x))),
     q(q(p(?x))) -> p(q(q(?x))),
     q(Q(?x)) -> ?x,
     Q(q(?x)) -> ?x,
     p(P(?x)) -> ?x,
     P(p(?x)) -> ?x ]
   [ c(b(?x)) -> c(c(?x)),
     c(c(?x)) -> c(b(?x)) ]
Polynomial Interpretation:
  P:= (1)+(2)*x1
  Q:= (1)*x1
  a:= (2)*x1*x1
  b:= (2)*x1*x1
  c:= (2)*x1*x1
  p:= (2)*x1
  q:= (1)+(1)*x1
retract P(?x) -> Q(Q(p(?x)))
retract Q(p(q(?x))) -> q(p(Q(?x)))
retract q(Q(?x)) -> ?x
retract Q(q(?x)) -> ?x
retract p(P(?x)) -> ?x
retract P(p(?x)) -> ?x
Polynomial Interpretation:
  P:= (8)*x1*x1
  Q:= (1)*x1
  a:= (2)*x1*x1
  b:= (1)+(2)*x1*x1
  c:= (1)+(2)*x1*x1
  p:= (1)*x1*x1
  q:= (1)*x1*x1
retract a(c(?x)) -> c(a(?x))
retract b(b(?x)) -> a(c(?x))
retract P(?x) -> Q(Q(p(?x)))
retract Q(p(q(?x))) -> q(p(Q(?x)))
retract q(Q(?x)) -> ?x
retract Q(q(?x)) -> ?x
retract p(P(?x)) -> ?x
retract P(p(?x)) -> ?x
Polynomial Interpretation:
  P:= (8)*x1*x1
  Q:= (1)+(1)*x1
  a:= (2)*x1*x1
  b:= (2)*x1*x1
  c:= (2)*x1*x1
  p:= (2)*x1
  q:= (2)*x1
retract a(c(?x)) -> c(a(?x))
retract b(b(?x)) -> a(c(?x))
retract P(?x) -> Q(Q(p(?x)))
retract p(Q(Q(?x))) -> Q(Q(p(?x)))
retract Q(p(q(?x))) -> q(p(Q(?x)))
retract q(Q(?x)) -> ?x
retract Q(q(?x)) -> ?x
retract p(P(?x)) -> ?x
retract P(p(?x)) -> ?x
Polynomial Interpretation:
  P:= (8)*x1*x1
  Q:= (1)*x1*x1
  a:= (2)*x1*x1
  b:= (1)*x1*x1
  c:= (1)*x1*x1
  p:= (1)+(1)*x1*x1
  q:= (1)*x1*x1
retract a(c(?x)) -> c(a(?x))
retract b(b(?x)) -> a(c(?x))
retract P(?x) -> Q(Q(p(?x)))
retract p(p(?x)) -> q(q(?x))
retract p(Q(Q(?x))) -> Q(Q(p(?x)))
retract Q(p(q(?x))) -> q(p(Q(?x)))
retract q(Q(?x)) -> ?x
retract Q(q(?x)) -> ?x
retract p(P(?x)) -> ?x
retract P(p(?x)) -> ?x
Polynomial Interpretation:
  P:= (8)*x1*x1
  Q:= (1)*x1
  a:= (2)*x1
  b:= (1)+(2)*x1
  c:= (2)*x1
  p:= (3)*x1
  q:= (1)*x1
retract a(b(?x)) -> b(c(?x))
retract a(c(?x)) -> c(a(?x))
retract b(b(?x)) -> a(c(?x))
retract c(b(?x)) -> b(c(?x))
retract P(?x) -> Q(Q(p(?x)))
retract p(p(?x)) -> q(q(?x))
retract p(Q(Q(?x))) -> Q(Q(p(?x)))
retract Q(p(q(?x))) -> q(p(Q(?x)))
retract q(Q(?x)) -> ?x
retract Q(q(?x)) -> ?x
retract p(P(?x)) -> ?x
retract P(p(?x)) -> ?x
retract c(b(?x)) -> c(c(?x))
Polynomial Interpretation:
  P:= (8)*x1*x1
  Q:= (1)*x1
  a:= (1)+(1)*x1
  b:= (1)+(1)*x1
  c:= (2)*x1
  p:= (1)+(1)*x1
  q:= (2)*x1*x1
relatively terminating
S/P: relatively terminating
check CP condition:
failed
failure(Step 3)
failure(no possibility remains)
unknown Reduction-Preserving Completion
Direct Methods: Can't judge

Try Persistent Decomposition for...
   [ a(b(?x)) -> b(c(?x)),
     a(c(?x)) -> c(a(?x)),
     b(b(?x)) -> a(c(?x)),
     c(b(?x)) -> b(c(?x)),
     c(b(?x)) -> c(c(?x)),
     c(c(?x)) -> c(b(?x)),
     P(?x) -> Q(Q(p(?x))),
     p(p(?x)) -> q(q(?x)),
     p(Q(Q(?x))) -> Q(Q(p(?x))),
     Q(p(q(?x))) -> q(p(Q(?x))),
     q(q(p(?x))) -> p(q(q(?x))),
     q(Q(?x)) -> ?x,
     Q(q(?x)) -> ?x,
     p(P(?x)) -> ?x,
     P(p(?x)) -> ?x ]
Sort Assignment:
 P : 30=>30
 Q : 30=>30
 a : 39=>39
 b : 39=>39
 c : 39=>39
 p : 30=>30
 q : 30=>30
maximal types: {30}{39}
{30}
(ps)Rewrite Rules:
   [ P(?x) -> Q(Q(p(?x))),
     p(p(?x)) -> q(q(?x)),
     p(Q(Q(?x))) -> Q(Q(p(?x))),
     Q(p(q(?x))) -> q(p(Q(?x))),
     q(q(p(?x))) -> p(q(q(?x))),
     q(Q(?x)) -> ?x,
     Q(q(?x)) -> ?x,
     p(P(?x)) -> ?x,
     P(p(?x)) -> ?x ]
Apply Direct Methods...
Inner CPs:
   [ p(Q(Q(p(?x_2)))) = q(q(Q(Q(?x_2)))),
     p(?x_7) = q(q(P(?x_7))),
     p(Q(q(p(Q(?x_3))))) = Q(Q(p(p(q(?x_3))))),
     p(Q(?x_6)) = Q(Q(p(q(?x_6)))),
     Q(p(p(q(q(?x_4))))) = q(p(Q(q(p(?x_4))))),
     Q(p(?x_5)) = q(p(Q(Q(?x_5)))),
     q(q(q(q(?x_1)))) = p(q(q(p(?x_1)))),
     q(q(Q(Q(p(?x_2))))) = p(q(q(Q(Q(?x_2))))),
     q(q(?x_7)) = p(q(q(P(?x_7)))),
     q(q(p(Q(?x_3)))) = p(q(?x_3)),
     q(?x_6) = q(?x_6),
     Q(p(q(q(?x_4)))) = q(p(?x_4)),
     Q(?x_5) = Q(?x_5),
     p(Q(Q(p(?x)))) = ?x,
     p(?x_8) = p(?x_8),
     P(q(q(?x_1))) = p(?x_1),
     P(Q(Q(p(?x_2)))) = Q(Q(?x_2)),
     P(?x_7) = P(?x_7),
     p(q(q(?x))) = q(q(p(?x))) ]
Outer CPs:
   [ Q(Q(p(p(?x_8)))) = ?x_8 ]
not Overlay, check Termination...
unknown/not Terminating
unknown Knuth & Bendix
Linear
unknown Development Closed
unknown Strongly Closed
unknown Weakly-Non-Overlapping & Non-Collapsing & Shallow
unknown Upside-Parallel-Closed/Outside-Closed
(inner) Parallel CPs: (not computed)
unknown Toyama (Parallel CPs)
Simultaneous CPs:
   [ ?x_8 = Q(Q(p(p(?x_8)))),
     ?x = p(Q(Q(p(?x)))),
     p(q(q(?x_1))) = q(q(p(?x_1))),
     p(Q(Q(p(?x_3)))) = q(q(Q(Q(?x_3)))),
     p(?x_8) = q(q(P(?x_8))),
     q(q(q(q(?x_1)))) = p(q(q(p(?x_1)))),
     q(q(Q(Q(p(?x_3))))) = p(q(q(Q(Q(?x_3))))),
     q(q(?x_8)) = p(q(q(P(?x_8)))),
     p(q(q(q(q(?x_1))))) = q(q(q(q(p(?x_1))))),
     p(q(q(Q(Q(p(?x_3)))))) = q(q(q(q(Q(Q(?x_3)))))),
     p(q(q(?x_8))) = q(q(q(q(P(?x_8))))),
     q(q(?x_1)) = P(q(q(p(?x_1)))),
     Q(Q(p(?x_3))) = P(q(q(Q(Q(?x_3))))),
     ?x_8 = P(q(q(P(?x_8)))),
     q(q(p(?x))) = p(q(q(?x))),
     p(q(q(p(?x)))) = q(q(q(q(?x)))),
     p(?x) = P(q(q(?x))),
     p(Q(q(p(Q(?x_4))))) = Q(Q(p(p(q(?x_4))))),
     p(Q(?x_7)) = Q(Q(p(q(?x_7)))),
     q(q(Q(q(p(Q(?x_4)))))) = p(Q(Q(p(p(q(?x_4)))))),
     q(q(Q(?x_7))) = p(Q(Q(p(q(?x_7))))),
     p(q(q(Q(q(p(Q(?x_4))))))) = q(q(Q(Q(p(p(q(?x_4))))))),
     p(q(q(Q(?x_7)))) = q(q(Q(Q(p(q(?x_7)))))),
     Q(q(p(Q(?x_4)))) = P(Q(Q(p(p(q(?x_4)))))),
     Q(?x_7) = P(Q(Q(p(q(?x_7))))),
     q(q(Q(Q(?x)))) = p(Q(Q(p(?x)))),
     p(q(q(Q(Q(?x))))) = q(q(Q(Q(p(?x))))),
     Q(Q(?x)) = P(Q(Q(p(?x)))),
     Q(p(p(q(q(?x_5))))) = q(p(Q(q(p(?x_5))))),
     Q(p(?x_6)) = q(p(Q(Q(?x_6)))),
     Q(Q(p(p(p(q(q(?x_5))))))) = p(Q(q(p(Q(q(p(?x_5))))))),
     Q(Q(p(p(?x_6)))) = p(Q(q(p(Q(Q(?x_6)))))),
     p(p(q(q(?x_5)))) = q(q(p(Q(q(p(?x_5)))))),
     p(?x_6) = q(q(p(Q(Q(?x_6))))),
     Q(Q(p(p(q(?x))))) = p(Q(q(p(Q(?x))))),
     p(q(?x)) = q(q(p(Q(?x)))),
     q(p(Q(q(q(q(?x_3)))))) = Q(p(p(q(q(p(?x_3)))))),
     q(p(Q(q(Q(Q(p(?x_4))))))) = Q(p(p(q(q(Q(Q(?x_4))))))),
     q(p(Q(q(?x_8)))) = Q(p(p(q(q(P(?x_8)))))),
     q(q(q(?x_3))) = Q(p(q(q(p(?x_3))))),
     q(Q(Q(p(?x_4)))) = Q(p(q(q(Q(Q(?x_4)))))),
     q(?x_8) = Q(p(q(q(P(?x_8))))),
     q(p(Q(q(p(?x))))) = Q(p(p(q(q(?x))))),
     q(p(?x)) = Q(p(q(q(?x)))),
     q(q(p(Q(?x_5)))) = p(q(?x_5)),
     q(?x_7) = q(?x_7),
     q(p(Q(q(p(Q(?x_5)))))) = Q(p(p(q(?x_5)))),
     q(p(Q(?x_7))) = Q(p(q(?x_7))),
     ?x_7 = Q(q(?x_7)),
     q(p(Q(Q(?x)))) = Q(p(?x)),
     Q(?x) = Q(?x),
     Q(p(q(q(?x_6)))) = q(p(?x_6)),
     Q(Q(p(p(q(q(?x_6)))))) = p(Q(q(p(?x_6)))),
     Q(Q(p(?x_7))) = p(Q(Q(?x_7))),
     ?x_7 = q(Q(?x_7)),
     Q(Q(p(q(?x)))) = p(Q(?x)),
     p(Q(Q(p(?x)))) = ?x,
     p(?x_9) = p(?x_9),
     q(q(Q(Q(p(?x))))) = p(?x),
     q(q(?x_9)) = p(p(?x_9)),
     p(q(q(Q(Q(p(?x)))))) = q(q(?x)),
     Q(Q(p(?x))) = P(?x),
     ?x_9 = P(p(?x_9)),
     q(q(P(?x))) = p(?x),
     p(q(q(P(?x)))) = q(q(?x)),
     P(?x) = P(?x),
     Q(Q(p(q(q(?x_3))))) = p(?x_3),
     Q(Q(p(Q(Q(p(?x_4)))))) = Q(Q(?x_4)),
     Q(Q(p(p(?x)))) = ?x,
     P(q(q(?x_3))) = p(?x_3),
     P(Q(Q(p(?x_4)))) = Q(Q(?x_4)),
     ?x_9 = p(P(?x_9)) ]
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 <p(Q(Q(p(?x_2)))), q(q(Q(Q(?x_2))))> by Rules <2, 1> preceded by [(p,1)]
 joinable by a reduction of rules <[([],2),([(Q,1),(Q,1)],1),([(Q,1)],6),([],6)], [([(q,1)],5),([],5)]>
Critical Pair <p(?x_7), q(q(P(?x_7)))> by Rules <7, 1> preceded by [(p,1)]
 joinable by a reduction of rules <[], [([(q,1),(q,1)],0),([(q,1)],5),([],5)]>
Critical Pair <p(Q(q(p(Q(?x_3))))), Q(Q(p(p(q(?x_3)))))> by Rules <3, 2> preceded by [(p,1),(Q,1)]
 joinable by a reduction of rules <[([(p,1)],6),([],1),([(q,1)],5)], [([(Q,1),(Q,1)],1),([(Q,1)],6),([],6)]>
Critical Pair <p(Q(?x_6)), Q(Q(p(q(?x_6))))> by Rules <6, 2> preceded by [(p,1),(Q,1)]
 joinable by a reduction of rules <[], [([(Q,1)],3),([],6)]>
Critical Pair <Q(p(p(q(q(?x_4))))), q(p(Q(q(p(?x_4)))))> by Rules <4, 3> preceded by [(Q,1),(p,1)]
 joinable by a reduction of rules <[([(Q,1)],1),([],6)], [([(q,1),(p,1)],6),([(q,1)],1)]>
Critical Pair <Q(p(?x_5)), q(p(Q(Q(?x_5))))> by Rules <5, 3> preceded by [(Q,1),(p,1)]
 joinable by a reduction of rules <[], [([(q,1)],2),([],5)]>
Critical Pair <q(q(q(q(?x_1)))), p(q(q(p(?x_1))))> by Rules <1, 4> preceded by [(q,1),(q,1)]
 joinable by a reduction of rules <[], [([(p,1)],4),([],1)]>
Critical Pair <q(q(Q(Q(p(?x_2))))), p(q(q(Q(Q(?x_2)))))> by Rules <2, 4> preceded by [(q,1),(q,1)]
 joinable by a reduction of rules <[([(q,1)],5),([],5)], [([(p,1),(q,1)],5),([(p,1)],5)]>
Critical Pair <q(q(?x_7)), p(q(q(P(?x_7))))> by Rules <7, 4> preceded by [(q,1),(q,1)]
 joinable by a reduction of rules <[], [([(p,1),(q,1),(q,1)],0),([(p,1),(q,1)],5),([(p,1)],5),([],1)]>
Critical Pair <q(q(p(Q(?x_3)))), p(q(?x_3))> by Rules <3, 5> preceded by [(q,1)]
 joinable by a reduction of rules <[([],4),([(p,1),(q,1)],5)], []>
Critical Pair <q(?x_6), q(?x_6)> by Rules <6, 5> preceded by [(q,1)]
 joinable by a reduction of rules <[], []>
Critical Pair <Q(p(q(q(?x_4)))), q(p(?x_4))> by Rules <4, 6> preceded by [(Q,1)]
 joinable by a reduction of rules <[([],3),([(q,1),(p,1)],6)], []>
Critical Pair <Q(?x_5), Q(?x_5)> by Rules <5, 6> preceded by [(Q,1)]
 joinable by a reduction of rules <[], []>
Critical Pair <p(Q(Q(p(?x)))), ?x> by Rules <0, 7> preceded by [(p,1)]
 joinable by a reduction of rules <[([],2),([(Q,1),(Q,1)],1),([(Q,1)],6),([],6)], []>
Critical Pair <p(?x_8), p(?x_8)> by Rules <8, 7> preceded by [(p,1)]
 joinable by a reduction of rules <[], []>
Critical Pair <P(q(q(?x_1))), p(?x_1)> by Rules <1, 8> preceded by [(P,1)]
 joinable by a reduction of rules <[([],0),([(Q,1)],3),([(Q,1),(q,1),(p,1)],6),([],6)], []>
 joinable by a reduction of rules <[([],0),([(Q,1)],3),([],6),([(p,1)],6)], []>
Critical Pair <P(Q(Q(p(?x_2)))), Q(Q(?x_2))> by Rules <2, 8> preceded by [(P,1)]
 joinable by a reduction of rules <[([],0),([(Q,1),(Q,1)],2),([(Q,1),(Q,1),(Q,1),(Q,1)],1),([(Q,1),(Q,1),(Q,1)],6),([(Q,1),(Q,1)],6)], []>
Critical Pair <P(?x_7), P(?x_7)> by Rules <7, 8> preceded by [(P,1)]
 joinable by a reduction of rules <[], []>
Critical Pair <p(q(q(?x))), q(q(p(?x)))> by Rules <1, 1> preceded by [(p,1)]
 joinable by a reduction of rules <[], [([],4)]>
Critical Pair <?x_8, Q(Q(p(p(?x_8))))> by Rules <8, 0> preceded by []
 joinable by a reduction of rules <[], [([(Q,1),(Q,1)],1),([(Q,1)],6),([],6)]>
unknown Diagram Decreasing
check Non-Confluence...
obtain 13 rules by 3 steps unfolding
obtain 100 candidates for checking non-joinability
check by TCAP-Approximation (failure)
check by Ordering(rpo), check by Tree-Automata Approximation (failure)
check by Interpretation(mod2) (failure)
check by Descendants-Approximation, check by Ordering(poly) (failure)
unknown Non-Confluence
unknown Huet (modulo AC)
check by Reduction-Preserving Completion...
failure(empty P)
unknown Reduction-Preserving Completion
Direct Methods: Can't judge

Try Layer Preserving Decomposition for...
   [ P(?x) -> Q(Q(p(?x))),
     p(p(?x)) -> q(q(?x)),
     p(Q(Q(?x))) -> Q(Q(p(?x))),
     Q(p(q(?x))) -> q(p(Q(?x))),
     q(q(p(?x))) -> p(q(q(?x))),
     q(Q(?x)) -> ?x,
     Q(q(?x)) -> ?x,
     p(P(?x)) -> ?x,
     P(p(?x)) -> ?x ]
Layer Preserving Decomposition failed: Can't judge

Try Commutative Decomposition for...
   [ P(?x) -> Q(Q(p(?x))),
     p(p(?x)) -> q(q(?x)),
     p(Q(Q(?x))) -> Q(Q(p(?x))),
     Q(p(q(?x))) -> q(p(Q(?x))),
     q(q(p(?x))) -> p(q(q(?x))),
     q(Q(?x)) -> ?x,
     Q(q(?x)) -> ?x,
     p(P(?x)) -> ?x,
     P(p(?x)) -> ?x ]
Outside Critical Pair: <?x_8, Q(Q(p(p(?x_8))))> by Rules <8, 0>
develop reducts from lhs term...
<{}, ?x_8>
develop reducts from rhs term...
<{1}, Q(Q(q(q(?x_8))))>
<{}, Q(Q(p(p(?x_8))))>
Inside Critical Pair: <p(Q(Q(p(?x_2)))), q(q(Q(Q(?x_2))))> by Rules <2, 1>
develop reducts from lhs term...
<{2}, Q(Q(p(p(?x_2))))>
<{}, p(Q(Q(p(?x_2))))>
develop reducts from rhs term...
<{5}, q(Q(?x_2))>
<{}, q(q(Q(Q(?x_2))))>
Inside Critical Pair: <p(?x_7), q(q(P(?x_7)))> by Rules <7, 1>
develop reducts from lhs term...
<{}, p(?x_7)>
develop reducts from rhs term...
<{0}, q(q(Q(Q(p(?x_7)))))>
<{}, q(q(P(?x_7)))>
Inside Critical Pair: <p(Q(q(p(Q(?x_3))))), Q(Q(p(p(q(?x_3)))))> by Rules <3, 2>
develop reducts from lhs term...
<{6}, p(p(Q(?x_3)))>
<{}, p(Q(q(p(Q(?x_3)))))>
develop reducts from rhs term...
<{1}, Q(Q(q(q(q(?x_3)))))>
<{}, Q(Q(p(p(q(?x_3)))))>
Inside Critical Pair: <p(Q(?x_6)), Q(Q(p(q(?x_6))))> by Rules <6, 2>
develop reducts from lhs term...
<{}, p(Q(?x_6))>
develop reducts from rhs term...
<{3}, Q(q(p(Q(?x_6))))>
<{}, Q(Q(p(q(?x_6))))>
Inside Critical Pair: <Q(p(p(q(q(?x_4))))), q(p(Q(q(p(?x_4)))))> by Rules <4, 3>
develop reducts from lhs term...
<{1}, Q(q(q(q(q(?x_4)))))>
<{}, Q(p(p(q(q(?x_4)))))>
develop reducts from rhs term...
<{6}, q(p(p(?x_4)))>
<{}, q(p(Q(q(p(?x_4)))))>
Inside Critical Pair: <Q(p(?x_5)), q(p(Q(Q(?x_5))))> by Rules <5, 3>
develop reducts from lhs term...
<{}, Q(p(?x_5))>
develop reducts from rhs term...
<{2}, q(Q(Q(p(?x_5))))>
<{}, q(p(Q(Q(?x_5))))>
Inside Critical Pair: <q(q(q(q(?x_1)))), p(q(q(p(?x_1))))> by Rules <1, 4>
develop reducts from lhs term...
<{}, q(q(q(q(?x_1))))>
develop reducts from rhs term...
<{4}, p(p(q(q(?x_1))))>
<{}, p(q(q(p(?x_1))))>
Inside Critical Pair: <q(q(Q(Q(p(?x_2))))), p(q(q(Q(Q(?x_2)))))> by Rules <2, 4>
develop reducts from lhs term...
<{5}, q(Q(p(?x_2)))>
<{}, q(q(Q(Q(p(?x_2)))))>
develop reducts from rhs term...
<{5}, p(q(Q(?x_2)))>
<{}, p(q(q(Q(Q(?x_2)))))>
Inside Critical Pair: <q(q(?x_7)), p(q(q(P(?x_7))))> by Rules <7, 4>
develop reducts from lhs term...
<{}, q(q(?x_7))>
develop reducts from rhs term...
<{0}, p(q(q(Q(Q(p(?x_7))))))>
<{}, p(q(q(P(?x_7))))>
Inside Critical Pair: <q(q(p(Q(?x_3)))), p(q(?x_3))> by Rules <3, 5>
develop reducts from lhs term...
<{4}, p(q(q(Q(?x_3))))>
<{}, q(q(p(Q(?x_3))))>
develop reducts from rhs term...
<{}, p(q(?x_3))>
Inside Critical Pair: <q(?x_6), q(?x_6)> by Rules <6, 5>
develop reducts from lhs term...
<{}, q(?x_6)>
develop reducts from rhs term...
<{}, q(?x_6)>
Inside Critical Pair: <Q(p(q(q(?x_4)))), q(p(?x_4))> by Rules <4, 6>
develop reducts from lhs term...
<{3}, q(p(Q(q(?x_4))))>
<{}, Q(p(q(q(?x_4))))>
develop reducts from rhs term...
<{}, q(p(?x_4))>
Inside Critical Pair: <Q(?x_5), Q(?x_5)> by Rules <5, 6>
develop reducts from lhs term...
<{}, Q(?x_5)>
develop reducts from rhs term...
<{}, Q(?x_5)>
Inside Critical Pair: <p(Q(Q(p(?x)))), ?x> by Rules <0, 7>
develop reducts from lhs term...
<{2}, Q(Q(p(p(?x))))>
<{}, p(Q(Q(p(?x))))>
develop reducts from rhs term...
<{}, ?x>
Inside Critical Pair: <p(?x_8), p(?x_8)> by Rules <8, 7>
develop reducts from lhs term...
<{}, p(?x_8)>
develop reducts from rhs term...
<{}, p(?x_8)>
Inside Critical Pair: <P(q(q(?x_1))), p(?x_1)> by Rules <1, 8>
develop reducts from lhs term...
<{0}, Q(Q(p(q(q(?x_1)))))>
<{}, P(q(q(?x_1)))>
develop reducts from rhs term...
<{}, p(?x_1)>
Inside Critical Pair: <P(Q(Q(p(?x_2)))), Q(Q(?x_2))> by Rules <2, 8>
develop reducts from lhs term...
<{0}, Q(Q(p(Q(Q(p(?x_2))))))>
<{}, P(Q(Q(p(?x_2))))>
develop reducts from rhs term...
<{}, Q(Q(?x_2))>
Inside Critical Pair: <P(?x_7), P(?x_7)> by Rules <7, 8>
develop reducts from lhs term...
<{0}, Q(Q(p(?x_7)))>
<{}, P(?x_7)>
develop reducts from rhs term...
<{0}, Q(Q(p(?x_7)))>
<{}, P(?x_7)>
Commutative Decomposition failed: Can't judge
No further decomposition possible

{39}
(ps)Rewrite Rules:
   [ a(b(?x)) -> b(c(?x)),
     a(c(?x)) -> c(a(?x)),
     b(b(?x)) -> a(c(?x)),
     c(b(?x)) -> b(c(?x)),
     c(b(?x)) -> c(c(?x)),
     c(c(?x)) -> c(b(?x)) ]
Apply Direct Methods...
Inner CPs:
   [ a(a(c(?x_2))) = b(c(b(?x_2))),
     a(b(c(?x_3))) = c(a(b(?x_3))),
     a(c(c(?x_4))) = c(a(b(?x_4))),
     a(c(b(?x_5))) = c(a(c(?x_5))),
     c(a(c(?x_2))) = b(c(b(?x_2))),
     c(a(c(?x_2))) = c(c(b(?x_2))),
     c(b(c(?x_3))) = c(b(b(?x_3))),
     c(c(c(?x_4))) = c(b(b(?x_4))),
     b(a(c(?x))) = a(c(b(?x))),
     c(c(b(?x))) = c(b(c(?x))) ]
Outer CPs:
   [ b(c(?x_3)) = c(c(?x_3)) ]
not Overlay, check Termination...
unknown/not Terminating
unknown Knuth & Bendix
Linear
unknown Development Closed
unknown Strongly Closed
unknown Weakly-Non-Overlapping & Non-Collapsing & Shallow
unknown Upside-Parallel-Closed/Outside-Closed
(inner) Parallel CPs: (not computed)
unknown Toyama (Parallel CPs)
Simultaneous CPs:
   [ a(a(c(?x_3))) = b(c(b(?x_3))),
     a(b(c(?x_4))) = c(a(b(?x_4))),
     a(c(c(?x_5))) = c(a(b(?x_5))),
     a(c(b(?x_6))) = c(a(c(?x_6))),
     b(a(c(?x_1))) = a(c(b(?x_1))),
     a(c(a(c(?x_1)))) = b(a(c(b(?x_1)))),
     b(c(a(c(?x_1)))) = a(a(c(b(?x_1)))),
     b(c(a(c(?x_1)))) = c(a(c(b(?x_1)))),
     c(c(a(c(?x_1)))) = c(a(c(b(?x_1)))),
     a(c(b(?x))) = b(a(c(?x))),
     b(c(b(?x))) = a(a(c(?x))),
     b(c(b(?x))) = c(a(c(?x))),
     c(c(b(?x))) = c(a(c(?x))),
     c(c(?x)) = b(c(?x)),
     c(a(c(?x_4))) = b(c(b(?x_4))),
     c(a(a(c(?x_4)))) = a(b(c(b(?x_4)))),
     c(b(a(c(?x_4)))) = c(b(c(b(?x_4)))),
     c(a(b(?x))) = a(b(c(?x))),
     c(b(b(?x))) = c(b(c(?x))),
     b(c(?x)) = c(c(?x)),
     c(a(c(?x_4))) = c(c(b(?x_4))),
     c(a(a(c(?x_4)))) = a(c(c(b(?x_4)))),
     c(b(a(c(?x_4)))) = c(c(c(b(?x_4)))),
     c(a(b(?x))) = a(c(c(?x))),
     c(b(b(?x))) = c(c(c(?x))),
     c(c(b(?x_1))) = c(b(c(?x_1))),
     c(b(c(?x_5))) = c(b(b(?x_5))),
     c(c(c(?x_6))) = c(b(b(?x_6))),
     c(b(c(b(?x_1)))) = c(c(b(c(?x_1)))),
     c(b(b(c(?x_5)))) = c(c(b(b(?x_5)))),
     c(b(c(c(?x_6)))) = c(c(b(b(?x_6)))),
     c(a(c(b(?x_1)))) = a(c(b(c(?x_1)))),
     c(a(b(c(?x_5)))) = a(c(b(b(?x_5)))),
     c(a(c(c(?x_6)))) = a(c(b(b(?x_6)))),
     c(b(c(?x))) = c(c(b(?x))),
     c(a(c(?x))) = a(c(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 <a(a(c(?x_2))), b(c(b(?x_2)))> by Rules <2, 0> preceded by [(a,1)]
unknown Diagram Decreasing
check Non-Confluence...
obtain 10 rules by 3 steps unfolding
obtain 100 candidates for checking non-joinability
check by TCAP-Approximation (failure)
check by Ordering(rpo), check by Tree-Automata Approximation (failure)
check by Interpretation(mod2) (failure)
check by Descendants-Approximation, check by Ordering(poly) (failure)
unknown Non-Confluence
unknown Huet (modulo AC)
check by Reduction-Preserving Completion...
STEP: 1 (parallel)
S:
   [ a(b(?x)) -> b(c(?x)),
     a(c(?x)) -> c(a(?x)),
     b(b(?x)) -> a(c(?x)),
     c(b(?x)) -> b(c(?x)) ]
P:
   [ c(b(?x)) -> c(c(?x)),
     c(c(?x)) -> c(b(?x)) ]
S: terminating
CP(S,S):
<a(a(c(?x_2))), b(c(b(?x_2)))> --> <c(a(a(?x_2))), c(c(a(?x_2)))> => no
<a(b(c(?x_3))), c(a(b(?x_3)))> --> <b(c(c(?x_3))), b(c(c(?x_3)))> => yes
<b(a(c(?x))), a(c(b(?x)))> --> <b(c(a(?x))), b(c(c(?x)))> => no
<c(a(c(?x_2))), b(c(b(?x_2)))> --> <c(c(a(?x_2))), c(c(a(?x_2)))> => yes
PCP_in(symP,S):
<a(c(c(?x_2))), c(a(b(?x_2)))> --> <c(c(a(?x_2))), b(c(c(?x_2)))> => no
<a(c(b(?x_1))), c(a(c(?x_1)))> --> <b(c(c(?x_1))), c(c(a(?x_1)))> => no
CP(S,symP):
<c(a(c(?x))), c(c(b(?x)))> --> <c(c(a(?x))), b(c(c(?x)))> => no
<c(b(c(?x))), c(b(b(?x)))> --> <b(c(c(?x))), c(c(a(?x)))> => no
<b(c(?x)), c(c(?x))> --> <b(c(?x)), c(c(?x))> => no
check joinability condition:
check modulo joinability of c(a(a(?x_2))) and c(c(a(?x_2))): maybe not joinable
check modulo joinability of b(c(a(?x))) and b(c(c(?x))): joinable by {0}
check modulo joinability of c(c(a(?x_2))) and b(c(c(?x_2))): joinable by {0}
check modulo joinability of b(c(c(?x_1))) and c(c(a(?x_1))): joinable by {0}
check modulo joinability of c(c(a(?x))) and b(c(c(?x))): joinable by {0}
check modulo joinability of b(c(c(?x))) and c(c(a(?x))): joinable by {0}
check modulo reachablity from b(c(?x)) to c(c(?x)): maybe not reachable
failed
failure(Step 1)
   [ c(c(?x)) -> b(c(?x)) ]
Added S-Rules:
   [ c(c(?x)) -> b(c(?x)) ]
Added P-Rules:
   [ ]
STEP: 2 (linear)
S:
   [ a(b(?x)) -> b(c(?x)),
     a(c(?x)) -> c(a(?x)),
     b(b(?x)) -> a(c(?x)),
     c(b(?x)) -> b(c(?x)) ]
P:
   [ c(b(?x)) -> c(c(?x)),
     c(c(?x)) -> c(b(?x)) ]
S: terminating
CP(S,S):
<a(a(c(?x_2))), b(c(b(?x_2)))> --> <c(a(a(?x_2))), c(c(a(?x_2)))> => no
<a(b(c(?x_3))), c(a(b(?x_3)))> --> <b(c(c(?x_3))), b(c(c(?x_3)))> => yes
<b(a(c(?x))), a(c(b(?x)))> --> <b(c(a(?x))), b(c(c(?x)))> => no
<c(a(c(?x_2))), b(c(b(?x_2)))> --> <c(c(a(?x_2))), c(c(a(?x_2)))> => yes
CP_in(symP,S):
<a(c(b(?x))), c(a(c(?x)))> --> <b(c(c(?x))), c(c(a(?x)))> => no
<a(c(c(?x))), c(a(b(?x)))> --> <c(c(a(?x))), b(c(c(?x)))> => no
CP(S,symP):
<c(a(c(?x))), c(c(b(?x)))> --> <c(c(a(?x))), b(c(c(?x)))> => no
<c(b(c(?x))), c(b(b(?x)))> --> <b(c(c(?x))), c(c(a(?x)))> => no
<b(c(?x)), c(c(?x))> --> <b(c(?x)), c(c(?x))> => no
check joinability condition:
check modulo joinability of c(a(a(?x_2))) and c(c(a(?x_2))): maybe not joinable
check modulo joinability of b(c(a(?x))) and b(c(c(?x))): maybe not joinable
check modulo joinability of b(c(c(?x))) and c(c(a(?x))): joinable by {0}
check modulo joinability of c(c(a(?x))) and b(c(c(?x))): joinable by {0}
check modulo joinability of c(c(a(?x))) and b(c(c(?x))): joinable by {0}
check modulo joinability of b(c(c(?x))) and c(c(a(?x))): joinable by {0}
check modulo reachablity from b(c(?x)) to c(c(?x)): maybe not reachable
failed
failure(Step 2)
   [ c(c(?x)) -> b(c(?x)) ]
Added S-Rules:
   [ c(c(?x)) -> b(c(?x)) ]
Added P-Rules:
   [ ]
STEP: 3 (relative)
S:
   [ a(b(?x)) -> b(c(?x)),
     a(c(?x)) -> c(a(?x)),
     b(b(?x)) -> a(c(?x)),
     c(b(?x)) -> b(c(?x)) ]
P:
   [ c(b(?x)) -> c(c(?x)),
     c(c(?x)) -> c(b(?x)) ]
Check relative termination:
   [ a(b(?x)) -> b(c(?x)),
     a(c(?x)) -> c(a(?x)),
     b(b(?x)) -> a(c(?x)),
     c(b(?x)) -> b(c(?x)) ]
   [ c(b(?x)) -> c(c(?x)),
     c(c(?x)) -> c(b(?x)) ]
Polynomial Interpretation:
  a:= (2)*x1*x1
  b:= (1)+(2)*x1*x1
  c:= (1)+(2)*x1*x1
retract a(c(?x)) -> c(a(?x))
retract b(b(?x)) -> a(c(?x))
Polynomial Interpretation:
  a:= (1)+(2)*x1*x1
  b:= (2)*x1*x1
  c:= (2)*x1*x1
retract a(b(?x)) -> b(c(?x))
retract a(c(?x)) -> c(a(?x))
retract b(b(?x)) -> a(c(?x))
Polynomial Interpretation:
  a:= (2)*x1*x1
  b:= (1)+(2)*x1
  c:= (2)*x1
relatively terminating
S/P: relatively terminating
check CP condition:
failed
failure(Step 3)
STEP: 4 (parallel)
S:
   [ a(b(?x)) -> b(c(?x)),
     a(c(?x)) -> c(a(?x)),
     b(b(?x)) -> a(c(?x)),
     c(b(?x)) -> b(c(?x)),
     c(c(?x)) -> b(c(?x)) ]
P:
   [ c(b(?x)) -> c(c(?x)),
     c(c(?x)) -> c(b(?x)) ]
S: unknown termination
failure(Step 4)
STEP: 5 (linear)
S:
   [ a(b(?x)) -> b(c(?x)),
     a(c(?x)) -> c(a(?x)),
     b(b(?x)) -> a(c(?x)),
     c(b(?x)) -> b(c(?x)),
     c(c(?x)) -> b(c(?x)) ]
P:
   [ c(b(?x)) -> c(c(?x)),
     c(c(?x)) -> c(b(?x)) ]
S: unknown termination
failure(Step 5)
STEP: 6 (relative)
S:
   [ a(b(?x)) -> b(c(?x)),
     a(c(?x)) -> c(a(?x)),
     b(b(?x)) -> a(c(?x)),
     c(b(?x)) -> b(c(?x)),
     c(c(?x)) -> b(c(?x)) ]
P:
   [ c(b(?x)) -> c(c(?x)),
     c(c(?x)) -> c(b(?x)) ]
Check relative termination:
   [ a(b(?x)) -> b(c(?x)),
     a(c(?x)) -> c(a(?x)),
     b(b(?x)) -> a(c(?x)),
     c(b(?x)) -> b(c(?x)),
     c(c(?x)) -> b(c(?x)) ]
   [ c(b(?x)) -> c(c(?x)),
     c(c(?x)) -> c(b(?x)) ]