MAYBE
Time: 0.019967
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}
  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)}
   SCCS (2):
    Scc:
     {a# b a x0 -> a# b x0}
    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 (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}
     POLY:
      Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
      Interpretation:
       [p](x0, x1) = x0,
       
       [a](x0) = x0 + 1,
       
       [b](x0) = x0,
       
       [a#](x0) = x0
      Strict:
       a# b a x0 -> a# b x0
       1 + 1x0 >= 0 + 1x0
      Weak:
       
     Qed
   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}
    POLY:
     Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
     Interpretation:
      [p](x0, x1) = x0 + 1,
      
      [a](x0) = 0,
      
      [b](x0) = 0,
      
      [p#](x0, x1) = x0
     Strict:
      p#(a x0, p(b a x1, x2)) -> p#(a b a x1, x2)
      1 + 0x1 + 1x2 + 0x0 >= 0 + 0x1 + 1x2
      p#(a x0, p(b a x1, x2)) -> p#(x1, p(a b a x1, x2))
      1 + 0x1 + 1x2 + 0x0 >= 1 + 0x1 + 1x2
     Weak:
      
    EDG:
     {(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)))}
     SCCS (1):
      Scc:
       {p#(a x0, p(b a x1, x2)) -> p#(x1, p(a b a x1, x2))}
      SCC (1):
       Strict:
        {p#(a x0, p(b a x1, x2)) -> p#(x1, 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}
       Fail