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