MAYBE
Time: 0.017195
TRS:
 {p(a x0, p(a a a x1, x2)) -> p(a x2, p(a a b x0, x2))}
 DP:
  DP:
   {p#(a x0, p(a a a x1, x2)) -> p#(a x2, p(a a b x0, x2)),
    p#(a x0, p(a a a x1, x2)) -> p#(a a b x0, x2)}
  TRS:
  {p(a x0, p(a a a x1, x2)) -> p(a x2, p(a a b x0, x2))}
  EDG:
   {(p#(a x0, p(a a a x1, x2)) -> p#(a x2, p(a a b x0, x2)), p#(a x0, p(a a a x1, x2)) -> p#(a a b x0, x2))
    (p#(a x0, p(a a a x1, x2)) -> p#(a x2, p(a a b x0, x2)), p#(a x0, p(a a a x1, x2)) -> p#(a x2, p(a a b x0, x2)))
    (p#(a x0, p(a a a x1, x2)) -> p#(a a b x0, x2), p#(a x0, p(a a a x1, x2)) -> p#(a x2, p(a a b x0, x2)))
    (p#(a x0, p(a a a x1, x2)) -> p#(a a b x0, x2), p#(a x0, p(a a a x1, x2)) -> p#(a a b x0, x2))}
   SCCS (1):
    Scc:
     {p#(a x0, p(a a a x1, x2)) -> p#(a x2, p(a a b x0, x2)),
      p#(a x0, p(a a a x1, x2)) -> p#(a a b x0, x2)}
    SCC (2):
     Strict:
      {p#(a x0, p(a a a x1, x2)) -> p#(a x2, p(a a b x0, x2)),
       p#(a x0, p(a a a x1, x2)) -> p#(a a b x0, x2)}
     Weak:
     {p(a x0, p(a a a x1, x2)) -> p(a x2, p(a a b x0, x2))}
     POLY:
      Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
      Interpretation:
       [p](x0, x1) = x0 + 1,
       
       [a](x0) = 0,
       
       [b](x0) = 0,
       
       [p#](x0, x1) = x0
      Strict:
       p#(a x0, p(a a a x1, x2)) -> p#(a a b x0, x2)
       1 + 1x2 + 0x0 + 0x1 >= 0 + 1x2 + 0x0
       p#(a x0, p(a a a x1, x2)) -> p#(a x2, p(a a b x0, x2))
       1 + 1x2 + 0x0 + 0x1 >= 1 + 1x2 + 0x0
      Weak:
       
     EDG:
      {(p#(a x0, p(a a a x1, x2)) -> p#(a x2, p(a a b x0, x2)), p#(a x0, p(a a a x1, x2)) -> p#(a x2, p(a a b x0, x2)))}
      SCCS (1):
       Scc:
        {p#(a x0, p(a a a x1, x2)) -> p#(a x2, p(a a b x0, x2))}
       SCC (1):
        Strict:
         {p#(a x0, p(a a a x1, x2)) -> p#(a x2, p(a a b x0, x2))}
        Weak:
        {p(a x0, p(a a a x1, x2)) -> p(a x2, p(a a b x0, x2))}
        Fail