MAYBE
TRS:
 {p(a(x0), p(b(a(x1)), x2)) -> p(x1, p(a(b(a(x1))), x2)),
                a(b(a(x0))) -> b(a(b(x0)))}
 DP:
  Strict:
   {p#(a(x0), p(b(a(x1)), x2)) -> p#(x1, p(a(b(a(x1))), x2)),
    p#(a(x0), p(b(a(x1)), x2)) -> p#(a(b(a(x1))), x2),
    p#(a(x0), p(b(a(x1)), x2)) -> a#(b(a(x1))),
                  a#(b(a(x0))) -> a#(b(x0))}
  Weak:
  {p(a(x0), p(b(a(x1)), x2)) -> p(x1, p(a(b(a(x1))), x2)),
                 a(b(a(x0))) -> b(a(b(x0)))}
  EDG:
   {(p#(a(x0), p(b(a(x1)), x2)) -> p#(a(b(a(x1))), x2), p#(a(x0), p(b(a(x1)), x2)) -> a#(b(a(x1))))
    (p#(a(x0), p(b(a(x1)), x2)) -> p#(a(b(a(x1))), x2), p#(a(x0), p(b(a(x1)), x2)) -> p#(a(b(a(x1))), x2))
    (p#(a(x0), p(b(a(x1)), x2)) -> p#(a(b(a(x1))), x2), p#(a(x0), p(b(a(x1)), x2)) -> p#(x1, p(a(b(a(x1))), x2)))
    (a#(b(a(x0))) -> a#(b(x0)), a#(b(a(x0))) -> a#(b(x0)))
    (p#(a(x0), p(b(a(x1)), x2)) -> p#(x1, p(a(b(a(x1))), x2)), p#(a(x0), p(b(a(x1)), x2)) -> p#(x1, p(a(b(a(x1))), x2)))
    (p#(a(x0), p(b(a(x1)), x2)) -> p#(x1, p(a(b(a(x1))), x2)), p#(a(x0), p(b(a(x1)), x2)) -> p#(a(b(a(x1))), x2))
    (p#(a(x0), p(b(a(x1)), x2)) -> p#(x1, p(a(b(a(x1))), x2)), p#(a(x0), p(b(a(x1)), x2)) -> a#(b(a(x1))))
    (p#(a(x0), p(b(a(x1)), x2)) -> a#(b(a(x1))), a#(b(a(x0))) -> a#(b(x0)))}
   SCCS:
    Scc:
     {a#(b(a(x0))) -> a#(b(x0))}
    Scc:
     {p#(a(x0), p(b(a(x1)), x2)) -> p#(x1, p(a(b(a(x1))), x2)),
      p#(a(x0), p(b(a(x1)), x2)) -> p#(a(b(a(x1))), x2)}
    SCC:
     Strict:
      {a#(b(a(x0))) -> a#(b(x0))}
     Weak:
     {p(a(x0), p(b(a(x1)), x2)) -> p(x1, p(a(b(a(x1))), x2)),
                    a(b(a(x0))) -> b(a(b(x0)))}
     POLY:
      Argument Filtering:
       pi(b) = 0, pi(a#) = 0, pi(a) = [0], pi(p) = []
      Usable Rules:
       {}
      Interpretation:
       [a](x0) = x0 + 1
      Strict:
       {}
      Weak:
       {p(a(x0), p(b(a(x1)), x2)) -> p(x1, p(a(b(a(x1))), x2)),
                      a(b(a(x0))) -> b(a(b(x0)))}
      Qed
    SCC:
     Strict:
      {p#(a(x0), p(b(a(x1)), x2)) -> p#(x1, p(a(b(a(x1))), x2)),
       p#(a(x0), p(b(a(x1)), x2)) -> p#(a(b(a(x1))), x2)}
     Weak:
     {p(a(x0), p(b(a(x1)), x2)) -> p(x1, p(a(b(a(x1))), x2)),
                    a(b(a(x0))) -> b(a(b(x0)))}
     POLY:
      Argument Filtering:
       pi(b) = [], pi(a) = [], pi(p#) = 1, pi(p) = [1]
      Usable Rules:
       {}
      Interpretation:
       [p](x0) = x0 + 1
      Strict:
       {p#(a(x0), p(b(a(x1)), x2)) -> p#(x1, p(a(b(a(x1))), x2))}
      Weak:
       {p(a(x0), p(b(a(x1)), x2)) -> p(x1, p(a(b(a(x1))), x2)),
                      a(b(a(x0))) -> b(a(b(x0)))}
      EDG:
       {(p#(a(x0), p(b(a(x1)), x2)) -> p#(x1, p(a(b(a(x1))), x2)), p#(a(x0), p(b(a(x1)), x2)) -> p#(x1, p(a(b(a(x1))), x2)))}
       SCCS:
        Scc:
         {p#(a(x0), p(b(a(x1)), x2)) -> p#(x1, p(a(b(a(x1))), x2))}
        SCC:
         Strict:
          {p#(a(x0), p(b(a(x1)), x2)) -> p#(x1, p(a(b(a(x1))), x2))}
         Weak:
         {p(a(x0), p(b(a(x1)), x2)) -> p(x1, p(a(b(a(x1))), x2)),
                        a(b(a(x0))) -> b(a(b(x0)))}
         Fail