MAYBE
Time: 0.009591
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))}
  UR:
   {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#(b x2, a a b x1), 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), 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#(b x2, a a b x1))
     (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))}
    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))}
     EDG:
      {(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))}
      EDG:
       {(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))}
       STATUS:
        arrows: 0.666667
        SCCS (1):
         Scc:
          {p#(p(b a x0, x1), p(x2, x3)) -> p#(x3, x0)}
         
         SCC (1):
          Strict:
           {p#(p(b a x0, x1), p(x2, x3)) -> p#(x3, x0)}
          Weak:
          {p(p(b a x0, x1), p(x2, x3)) -> p(p(b x2, a a b x1), p(x3, x0))}
          Open