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