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)))
  ADG 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))
   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)))
    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)))
    Open