MAYBE

Problem:
 a(a(f(x,y))) -> f(a(b(a(b(a(x))))),a(b(a(b(a(y))))))
 f(a(x),a(y)) -> a(f(x,y))
 f(b(x),b(y)) -> b(f(x,y))

Proof:
 DP Processor:
  DPs:
   a#(a(f(x,y))) -> a#(y)
   a#(a(f(x,y))) -> a#(b(a(y)))
   a#(a(f(x,y))) -> a#(b(a(b(a(y)))))
   a#(a(f(x,y))) -> a#(x)
   a#(a(f(x,y))) -> a#(b(a(x)))
   a#(a(f(x,y))) -> a#(b(a(b(a(x)))))
   a#(a(f(x,y))) -> f#(a(b(a(b(a(x))))),a(b(a(b(a(y))))))
   f#(a(x),a(y)) -> f#(x,y)
   f#(a(x),a(y)) -> a#(f(x,y))
   f#(b(x),b(y)) -> f#(x,y)
  TRS:
   a(a(f(x,y))) -> f(a(b(a(b(a(x))))),a(b(a(b(a(y))))))
   f(a(x),a(y)) -> a(f(x,y))
   f(b(x),b(y)) -> b(f(x,y))
  CDG Processor:
   DPs:
    a#(a(f(x,y))) -> a#(y)
    a#(a(f(x,y))) -> a#(b(a(y)))
    a#(a(f(x,y))) -> a#(b(a(b(a(y)))))
    a#(a(f(x,y))) -> a#(x)
    a#(a(f(x,y))) -> a#(b(a(x)))
    a#(a(f(x,y))) -> a#(b(a(b(a(x)))))
    a#(a(f(x,y))) -> f#(a(b(a(b(a(x))))),a(b(a(b(a(y))))))
    f#(a(x),a(y)) -> f#(x,y)
    f#(a(x),a(y)) -> a#(f(x,y))
    f#(b(x),b(y)) -> f#(x,y)
   TRS:
    a(a(f(x,y))) -> f(a(b(a(b(a(x))))),a(b(a(b(a(y))))))
    f(a(x),a(y)) -> a(f(x,y))
    f(b(x),b(y)) -> b(f(x,y))
   graph:
    f#(b(x),b(y)) -> f#(x,y) -> f#(a(x),a(y)) -> f#(x,y)
    f#(b(x),b(y)) -> f#(x,y) -> f#(a(x),a(y)) -> a#(f(x,y))
    f#(b(x),b(y)) -> f#(x,y) -> f#(b(x),b(y)) -> f#(x,y)
    f#(a(x),a(y)) -> f#(x,y) -> f#(a(x),a(y)) -> f#(x,y)
    f#(a(x),a(y)) -> f#(x,y) -> f#(a(x),a(y)) -> a#(f(x,y))
    f#(a(x),a(y)) -> f#(x,y) -> f#(b(x),b(y)) -> f#(x,y)
    f#(a(x),a(y)) -> a#(f(x,y)) -> a#(a(f(x,y))) -> a#(y)
    f#(a(x),a(y)) -> a#(f(x,y)) -> a#(a(f(x,y))) -> a#(b(a(y)))
    f#(a(x),a(y)) -> a#(f(x,y)) -> a#(a(f(x,y))) -> a#(b(a(b(a(y)))))
    f#(a(x),a(y)) -> a#(f(x,y)) -> a#(a(f(x,y))) -> a#(x)
    f#(a(x),a(y)) -> a#(f(x,y)) -> a#(a(f(x,y))) -> a#(b(a(x)))
    f#(a(x),a(y)) -> a#(f(x,y)) -> a#(a(f(x,y))) -> a#(b(a(b(a(x)))))
    f#(a(x),a(y)) -> a#(f(x,y)) ->
    a#(a(f(x,y))) -> f#(a(b(a(b(a(x))))),a(b(a(b(a(y))))))
    a#(a(f(x,y))) -> f#(a(b(a(b(a(x))))),a(b(a(b(a(y)))))) ->
    f#(a(x),a(y)) -> f#(x,y)
    a#(a(f(x,y))) -> f#(a(b(a(b(a(x))))),a(b(a(b(a(y)))))) ->
    f#(a(x),a(y)) -> a#(f(x,y))
    a#(a(f(x,y))) -> a#(y) -> a#(a(f(x,y))) -> a#(y)
    a#(a(f(x,y))) -> a#(y) -> a#(a(f(x,y))) -> a#(b(a(y)))
    a#(a(f(x,y))) -> a#(y) -> a#(a(f(x,y))) -> a#(b(a(b(a(y)))))
    a#(a(f(x,y))) -> a#(y) -> a#(a(f(x,y))) -> a#(x)
    a#(a(f(x,y))) -> a#(y) -> a#(a(f(x,y))) -> a#(b(a(x)))
    a#(a(f(x,y))) -> a#(y) -> a#(a(f(x,y))) -> a#(b(a(b(a(x)))))
    a#(a(f(x,y))) -> a#(y) ->
    a#(a(f(x,y))) -> f#(a(b(a(b(a(x))))),a(b(a(b(a(y))))))
    a#(a(f(x,y))) -> a#(x) -> a#(a(f(x,y))) -> a#(y)
    a#(a(f(x,y))) -> a#(x) -> a#(a(f(x,y))) -> a#(b(a(y)))
    a#(a(f(x,y))) -> a#(x) -> a#(a(f(x,y))) -> a#(b(a(b(a(y)))))
    a#(a(f(x,y))) -> a#(x) -> a#(a(f(x,y))) -> a#(x)
    a#(a(f(x,y))) -> a#(x) -> a#(a(f(x,y))) -> a#(b(a(x)))
    a#(a(f(x,y))) -> a#(x) -> a#(a(f(x,y))) -> a#(b(a(b(a(x)))))
    a#(a(f(x,y))) -> a#(x) -> a#(a(f(x,y))) -> f#(a(b(a(b(a(x))))),a(b(a(b(a(y))))))
   Restore Modifier:
    DPs:
     a#(a(f(x,y))) -> a#(y)
     a#(a(f(x,y))) -> a#(b(a(y)))
     a#(a(f(x,y))) -> a#(b(a(b(a(y)))))
     a#(a(f(x,y))) -> a#(x)
     a#(a(f(x,y))) -> a#(b(a(x)))
     a#(a(f(x,y))) -> a#(b(a(b(a(x)))))
     a#(a(f(x,y))) -> f#(a(b(a(b(a(x))))),a(b(a(b(a(y))))))
     f#(a(x),a(y)) -> f#(x,y)
     f#(a(x),a(y)) -> a#(f(x,y))
     f#(b(x),b(y)) -> f#(x,y)
    TRS:
     a(a(f(x,y))) -> f(a(b(a(b(a(x))))),a(b(a(b(a(y))))))
     f(a(x),a(y)) -> a(f(x,y))
     f(b(x),b(y)) -> b(f(x,y))
    SCC Processor:
     #sccs: 1
     #rules: 6
     #arcs: 29/100
     DPs:
      f#(b(x),b(y)) -> f#(x,y)
      f#(a(x),a(y)) -> a#(f(x,y))
      a#(a(f(x,y))) -> f#(a(b(a(b(a(x))))),a(b(a(b(a(y))))))
      f#(a(x),a(y)) -> f#(x,y)
      a#(a(f(x,y))) -> a#(x)
      a#(a(f(x,y))) -> a#(y)
     TRS:
      a(a(f(x,y))) -> f(a(b(a(b(a(x))))),a(b(a(b(a(y))))))
      f(a(x),a(y)) -> a(f(x,y))
      f(b(x),b(y)) -> b(f(x,y))
     Matrix Interpretation Processor:
      dimension: 1
      interpretation:
       [f#](x0, x1) = x0 + x1 + 1,
       
       [a#](x0) = x0,
       
       [b](x0) = x0,
       
       [a](x0) = x0,
       
       [f](x0, x1) = x0 + x1 + 1
      orientation:
       f#(b(x),b(y)) = x + y + 1 >= x + y + 1 = f#(x,y)
       
       f#(a(x),a(y)) = x + y + 1 >= x + y + 1 = a#(f(x,y))
       
       a#(a(f(x,y))) = x + y + 1 >= x + y + 1 = f#(a(b(a(b(a(x))))),a(b(a(b(a(y))))))
       
       f#(a(x),a(y)) = x + y + 1 >= x + y + 1 = f#(x,y)
       
       a#(a(f(x,y))) = x + y + 1 >= x = a#(x)
       
       a#(a(f(x,y))) = x + y + 1 >= y = a#(y)
       
       a(a(f(x,y))) = x + y + 1 >= x + y + 1 = f(a(b(a(b(a(x))))),a(b(a(b(a(y))))))
       
       f(a(x),a(y)) = x + y + 1 >= x + y + 1 = a(f(x,y))
       
       f(b(x),b(y)) = x + y + 1 >= x + y + 1 = b(f(x,y))
      problem:
       DPs:
        f#(b(x),b(y)) -> f#(x,y)
        f#(a(x),a(y)) -> a#(f(x,y))
        a#(a(f(x,y))) -> f#(a(b(a(b(a(x))))),a(b(a(b(a(y))))))
        f#(a(x),a(y)) -> f#(x,y)
       TRS:
        a(a(f(x,y))) -> f(a(b(a(b(a(x))))),a(b(a(b(a(y))))))
        f(a(x),a(y)) -> a(f(x,y))
        f(b(x),b(y)) -> b(f(x,y))
      Open