MAYBE
Time: 0.019156
TRS:
 {p(p(b a x0, x1), p(x2, x3)) -> p(p(b x2, a a b x1), p(x3, x0))}
 DP:
  DP:
   {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)}
  TRS:
  {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 (1):
    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 (2):
     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:
      Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
      Interpretation:
       [p](x0, x1) = x0 + x1 + 1,
       
       [b](x0) = x0,
       
       [a](x0) = x0,
       
       [p#](x0, x1) = x0 + x1
      Strict:
       p#(p(b a x0, x1), p(x2, x3)) -> p#(p(b x2, a a b x1), p(x3, x0))
       2 + 1x2 + 1x1 + 1x3 + 1x0 >= 2 + 1x2 + 1x1 + 1x3 + 1x0
       p#(p(b a x0, x1), p(x2, x3)) -> p#(x3, x0)
       2 + 1x2 + 1x1 + 1x3 + 1x0 >= 0 + 1x3 + 1x0
      Weak:
       
     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 (1):
       Scc:
        {p#(p(b a x0, x1), p(x2, x3)) -> p#(p(b x2, a a b x1), p(x3, x0))}
       SCC (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))}
        Fail