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