YES
Time: 0.015595
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#(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))}
         POLY:
          Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
          Interpretation:
           [p](x0, x1) = x0 + x1 + 1,
           
           [b](x0) = x0 + 1,
           
           [a](x0) = x0,
           
           [p#](x0, x1) = x0 + x1
          Strict:
           p#(p(b a x0, x1), p(x2, x3)) -> p#(x3, x0)
           3 + 1x2 + 1x1 + 1x3 + 1x0 >= 0 + 1x3 + 1x0
          Weak:
           p(p(b a x0, x1), p(x2, x3)) -> p(p(b x2, a a b x1), p(x3, x0))
           4 + 1x2 + 1x1 + 1x3 + 1x0 >= 5 + 1x2 + 1x1 + 1x3 + 1x0
         Qed