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