MAYBE
Time: 0.009550
TRS:
 {p(p(b a x0, x1), p(x2, x3)) -> p(p(x3, a x2), p(b a x1, b x0))}
 DP:
  DP:
   {p#(p(b a x0, x1), p(x2, x3)) -> p#(x3, a x2),
    p#(p(b a x0, x1), p(x2, x3)) -> p#(p(x3, a x2), p(b a x1, b x0)),
    p#(p(b a x0, x1), p(x2, x3)) -> p#(b a x1, b x0)}
  TRS:
  {p(p(b a x0, x1), p(x2, x3)) -> p(p(x3, a x2), p(b a x1, b x0))}
  EDG:
   {(p#(p(b a x0, x1), p(x2, x3)) -> p#(p(x3, a x2), p(b a x1, b x0)), p#(p(b a x0, x1), p(x2, x3)) -> p#(x3, a x2))
    (p#(p(b a x0, x1), p(x2, x3)) -> p#(p(x3, a x2), p(b a x1, b x0)), p#(p(b a x0, x1), p(x2, x3)) -> p#(p(x3, a x2), p(b a x1, b x0)))
    (p#(p(b a x0, x1), p(x2, x3)) -> p#(p(x3, a x2), p(b a x1, b x0)), p#(p(b a x0, x1), p(x2, x3)) -> p#(b a x1, b x0))}
   STATUS:
    arrows: 0.666667
    SCCS (1):
     Scc:
      {p#(p(b a x0, x1), p(x2, x3)) -> p#(p(x3, a x2), p(b a x1, b x0))}
     
     SCC (1):
      Strict:
       {p#(p(b a x0, x1), p(x2, x3)) -> p#(p(x3, a x2), p(b a x1, b x0))}
      Weak:
      {p(p(b a x0, x1), p(x2, x3)) -> p(p(x3, a x2), p(b a x1, b x0))}
      Fail