MAYBE

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

Proof:
 DP Processor:
  DPs:
   p#(p(b(a(x0)),x1),p(x2,x3)) -> p#(x3,x0)
   p#(p(b(a(x0)),x1),p(x2,x3)) -> p#(b(x2),a(a(b(x1))))
   p#(p(b(a(x0)),x1),p(x2,x3)) -> p#(p(b(x2),a(a(b(x1)))),p(x3,x0))
  TRS:
   p(p(b(a(x0)),x1),p(x2,x3)) -> p(p(b(x2),a(a(b(x1)))),p(x3,x0))
  CDG Processor:
   DPs:
    p#(p(b(a(x0)),x1),p(x2,x3)) -> p#(x3,x0)
    p#(p(b(a(x0)),x1),p(x2,x3)) -> p#(b(x2),a(a(b(x1))))
    p#(p(b(a(x0)),x1),p(x2,x3)) -> p#(p(b(x2),a(a(b(x1)))),p(x3,x0))
   TRS:
    p(p(b(a(x0)),x1),p(x2,x3)) -> p(p(b(x2),a(a(b(x1)))),p(x3,x0))
   graph:
    p#(p(b(a(x0)),x1),p(x2,x3)) -> p#(p(b(x2),a(a(b(x1)))),p(x3,x0)) ->
    p#(p(b(a(x0)),x1),p(x2,x3)) -> p#(x3,x0)
    p#(p(b(a(x0)),x1),p(x2,x3)) -> p#(p(b(x2),a(a(b(x1)))),p(x3,x0)) ->
    p#(p(b(a(x0)),x1),p(x2,x3)) -> p#(b(x2),a(a(b(x1))))
    p#(p(b(a(x0)),x1),p(x2,x3)) -> p#(p(b(x2),a(a(b(x1)))),p(x3,x0)) ->
    p#(p(b(a(x0)),x1),p(x2,x3)) -> p#(p(b(x2),a(a(b(x1)))),p(x3,x0))
    p#(p(b(a(x0)),x1),p(x2,x3)) -> p#(x3,x0) ->
    p#(p(b(a(x0)),x1),p(x2,x3)) -> p#(x3,x0)
    p#(p(b(a(x0)),x1),p(x2,x3)) -> p#(x3,x0) ->
    p#(p(b(a(x0)),x1),p(x2,x3)) -> p#(b(x2),a(a(b(x1))))
    p#(p(b(a(x0)),x1),p(x2,x3)) -> p#(x3,x0) ->
    p#(p(b(a(x0)),x1),p(x2,x3)) -> p#(p(b(x2),a(a(b(x1)))),p(x3,x0))
   Restore Modifier:
    DPs:
     p#(p(b(a(x0)),x1),p(x2,x3)) -> p#(x3,x0)
     p#(p(b(a(x0)),x1),p(x2,x3)) -> p#(b(x2),a(a(b(x1))))
     p#(p(b(a(x0)),x1),p(x2,x3)) -> p#(p(b(x2),a(a(b(x1)))),p(x3,x0))
    TRS:
     p(p(b(a(x0)),x1),p(x2,x3)) -> p(p(b(x2),a(a(b(x1)))),p(x3,x0))
    SCC Processor:
     #sccs: 1
     #rules: 2
     #arcs: 6/9
     DPs:
      p#(p(b(a(x0)),x1),p(x2,x3)) -> p#(p(b(x2),a(a(b(x1)))),p(x3,x0))
      p#(p(b(a(x0)),x1),p(x2,x3)) -> p#(x3,x0)
     TRS:
      p(p(b(a(x0)),x1),p(x2,x3)) -> p(p(b(x2),a(a(b(x1)))),p(x3,x0))
     Matrix Interpretation Processor:
      dimension: 1
      interpretation:
       [p#](x0, x1) = x0 + x1,
       
       [p](x0, x1) = x0 + x1 + 1,
       
       [b](x0) = x0,
       
       [a](x0) = x0
      orientation:
       p#(p(b(a(x0)),x1),p(x2,x3)) = x0 + x1 + x2 + x3 + 2 >= x0 + x1 + x2 + x3 + 2 = p#(p(b(x2),a(a(b(x1)))),p(x3,x0))
       
       p#(p(b(a(x0)),x1),p(x2,x3)) = x0 + x1 + x2 + x3 + 2 >= x0 + x3 = p#(x3,x0)
       
       p(p(b(a(x0)),x1),p(x2,x3)) = x0 + x1 + x2 + x3 + 3 >= x0 + x1 + x2 + x3 + 3 = p(p(b(x2),a(a(b(x1)))),p(x3,x0))
      problem:
       DPs:
        p#(p(b(a(x0)),x1),p(x2,x3)) -> p#(p(b(x2),a(a(b(x1)))),p(x3,x0))
       TRS:
        p(p(b(a(x0)),x1),p(x2,x3)) -> p(p(b(x2),a(a(b(x1)))),p(x3,x0))
      Open