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