MAYBE
TRS:
 {p(a(x0), p(a(a(a(x1))), x2)) -> p(a(x2), p(a(a(b(x0))), x2))}
 DP:
  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))}
  EDG:
   {(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))
    (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(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))}
   SCCS:
    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:
     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:
      Argument Filtering:
       pi(b) = [], pi(a) = [], pi(p#) = 1, pi(p) = [0,1]
      Usable Rules:
       {}
      Interpretation:
       [p](x0, x1) = x0 + x1 + 1,
       [a] = 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))}
      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:
        Scc:
         {p#(a(x0), p(a(a(a(x1))), x2)) -> p#(a(x2), p(a(a(b(x0))), x2))}
        SCC:
         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