MAYBE

Problem:
 p(a(x0),p(b(a(x1)),x2)) -> p(x1,p(a(b(a(x1))),x2))
 a(b(a(x0))) -> b(a(b(x0)))

Proof:
 DP Processor:
  DPs:
   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#(x1,p(a(b(a(x1))),x2))
   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)))
  CDG Processor:
   DPs:
    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#(x1,p(a(b(a(x1))),x2))
    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)))
   graph:
    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))
    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))
   Restore Modifier:
    DPs:
     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#(x1,p(a(b(a(x1))),x2))
     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)))
    SCC Processor:
     #sccs: 2
     #rules: 3
     #arcs: 8/16
     DPs:
      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))
     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)))
     Matrix Interpretation Processor:
      dimension: 1
      interpretation:
       [p#](x0, x1) = x1 + 1,
       
       [p](x0, x1) = x1 + 1,
       
       [b](x0) = 0,
       
       [a](x0) = 1
      orientation:
       p#(a(x0),p(b(a(x1)),x2)) = x2 + 2 >= x2 + 1 = p#(a(b(a(x1))),x2)
       
       p#(a(x0),p(b(a(x1)),x2)) = x2 + 2 >= x2 + 2 = p#(x1,p(a(b(a(x1))),x2))
       
       p(a(x0),p(b(a(x1)),x2)) = x2 + 2 >= x2 + 2 = p(x1,p(a(b(a(x1))),x2))
       
       a(b(a(x0))) = 1 >= 0 = b(a(b(x0)))
      problem:
       DPs:
        p#(a(x0),p(b(a(x1)),x2)) -> p#(x1,p(a(b(a(x1))),x2))
       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)))
      Open
     
     DPs:
      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)))
     Matrix Interpretation Processor:
      dimension: 1
      interpretation:
       [a#](x0) = x0,
       
       [p](x0, x1) = 0,
       
       [b](x0) = x0,
       
       [a](x0) = x0 + 1
      orientation:
       a#(b(a(x0))) = x0 + 1 >= x0 = a#(b(x0))
       
       p(a(x0),p(b(a(x1)),x2)) = 0 >= 0 = p(x1,p(a(b(a(x1))),x2))
       
       a(b(a(x0))) = x0 + 2 >= x0 + 1 = b(a(b(x0)))
      problem:
       DPs:
        
       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)))
      Qed