MAYBE

Problem:
 g(x,x) -> g(a(),b())
 g(c(),g(c(),x)) -> g(e(),g(d(),x))
 g(d(),g(d(),x)) -> g(c(),g(e(),x))
 g(e(),g(e(),x)) -> g(d(),g(c(),x))
 f(g(x,y)) -> g(y,g(f(f(x)),a()))

Proof:
 DP Processor:
  DPs:
   g#(x,x) -> g#(a(),b())
   g#(c(),g(c(),x)) -> g#(d(),x)
   g#(c(),g(c(),x)) -> g#(e(),g(d(),x))
   g#(d(),g(d(),x)) -> g#(e(),x)
   g#(d(),g(d(),x)) -> g#(c(),g(e(),x))
   g#(e(),g(e(),x)) -> g#(c(),x)
   g#(e(),g(e(),x)) -> g#(d(),g(c(),x))
   f#(g(x,y)) -> f#(x)
   f#(g(x,y)) -> f#(f(x))
   f#(g(x,y)) -> g#(f(f(x)),a())
   f#(g(x,y)) -> g#(y,g(f(f(x)),a()))
  TRS:
   g(x,x) -> g(a(),b())
   g(c(),g(c(),x)) -> g(e(),g(d(),x))
   g(d(),g(d(),x)) -> g(c(),g(e(),x))
   g(e(),g(e(),x)) -> g(d(),g(c(),x))
   f(g(x,y)) -> g(y,g(f(f(x)),a()))
  TDG Processor:
   DPs:
    g#(x,x) -> g#(a(),b())
    g#(c(),g(c(),x)) -> g#(d(),x)
    g#(c(),g(c(),x)) -> g#(e(),g(d(),x))
    g#(d(),g(d(),x)) -> g#(e(),x)
    g#(d(),g(d(),x)) -> g#(c(),g(e(),x))
    g#(e(),g(e(),x)) -> g#(c(),x)
    g#(e(),g(e(),x)) -> g#(d(),g(c(),x))
    f#(g(x,y)) -> f#(x)
    f#(g(x,y)) -> f#(f(x))
    f#(g(x,y)) -> g#(f(f(x)),a())
    f#(g(x,y)) -> g#(y,g(f(f(x)),a()))
   TRS:
    g(x,x) -> g(a(),b())
    g(c(),g(c(),x)) -> g(e(),g(d(),x))
    g(d(),g(d(),x)) -> g(c(),g(e(),x))
    g(e(),g(e(),x)) -> g(d(),g(c(),x))
    f(g(x,y)) -> g(y,g(f(f(x)),a()))
   graph:
    f#(g(x,y)) -> f#(f(x)) -> f#(g(x,y)) -> g#(y,g(f(f(x)),a()))
    f#(g(x,y)) -> f#(f(x)) -> f#(g(x,y)) -> g#(f(f(x)),a())
    f#(g(x,y)) -> f#(f(x)) -> f#(g(x,y)) -> f#(f(x))
    f#(g(x,y)) -> f#(f(x)) -> f#(g(x,y)) -> f#(x)
    f#(g(x,y)) -> f#(x) -> f#(g(x,y)) -> g#(y,g(f(f(x)),a()))
    f#(g(x,y)) -> f#(x) -> f#(g(x,y)) -> g#(f(f(x)),a())
    f#(g(x,y)) -> f#(x) -> f#(g(x,y)) -> f#(f(x))
    f#(g(x,y)) -> f#(x) -> f#(g(x,y)) -> f#(x)
    f#(g(x,y)) -> g#(f(f(x)),a()) ->
    g#(e(),g(e(),x)) -> g#(d(),g(c(),x))
    f#(g(x,y)) -> g#(f(f(x)),a()) -> g#(e(),g(e(),x)) -> g#(c(),x)
    f#(g(x,y)) -> g#(f(f(x)),a()) ->
    g#(d(),g(d(),x)) -> g#(c(),g(e(),x))
    f#(g(x,y)) -> g#(f(f(x)),a()) -> g#(d(),g(d(),x)) -> g#(e(),x)
    f#(g(x,y)) -> g#(f(f(x)),a()) ->
    g#(c(),g(c(),x)) -> g#(e(),g(d(),x))
    f#(g(x,y)) -> g#(f(f(x)),a()) -> g#(c(),g(c(),x)) -> g#(d(),x)
    f#(g(x,y)) -> g#(f(f(x)),a()) -> g#(x,x) -> g#(a(),b())
    f#(g(x,y)) -> g#(y,g(f(f(x)),a())) ->
    g#(e(),g(e(),x)) -> g#(d(),g(c(),x))
    f#(g(x,y)) -> g#(y,g(f(f(x)),a())) ->
    g#(e(),g(e(),x)) -> g#(c(),x)
    f#(g(x,y)) -> g#(y,g(f(f(x)),a())) ->
    g#(d(),g(d(),x)) -> g#(c(),g(e(),x))
    f#(g(x,y)) -> g#(y,g(f(f(x)),a())) ->
    g#(d(),g(d(),x)) -> g#(e(),x)
    f#(g(x,y)) -> g#(y,g(f(f(x)),a())) ->
    g#(c(),g(c(),x)) -> g#(e(),g(d(),x))
    f#(g(x,y)) -> g#(y,g(f(f(x)),a())) ->
    g#(c(),g(c(),x)) -> g#(d(),x)
    f#(g(x,y)) -> g#(y,g(f(f(x)),a())) -> g#(x,x) -> g#(a(),b())
    g#(d(),g(d(),x)) -> g#(e(),x) ->
    g#(e(),g(e(),x)) -> g#(d(),g(c(),x))
    g#(d(),g(d(),x)) -> g#(e(),x) -> g#(e(),g(e(),x)) -> g#(c(),x)
    g#(d(),g(d(),x)) -> g#(e(),x) ->
    g#(d(),g(d(),x)) -> g#(c(),g(e(),x))
    g#(d(),g(d(),x)) -> g#(e(),x) -> g#(d(),g(d(),x)) -> g#(e(),x)
    g#(d(),g(d(),x)) -> g#(e(),x) ->
    g#(c(),g(c(),x)) -> g#(e(),g(d(),x))
    g#(d(),g(d(),x)) -> g#(e(),x) -> g#(c(),g(c(),x)) -> g#(d(),x)
    g#(d(),g(d(),x)) -> g#(e(),x) -> g#(x,x) -> g#(a(),b())
    g#(d(),g(d(),x)) -> g#(c(),g(e(),x)) ->
    g#(e(),g(e(),x)) -> g#(d(),g(c(),x))
    g#(d(),g(d(),x)) -> g#(c(),g(e(),x)) ->
    g#(e(),g(e(),x)) -> g#(c(),x)
    g#(d(),g(d(),x)) -> g#(c(),g(e(),x)) ->
    g#(d(),g(d(),x)) -> g#(c(),g(e(),x))
    g#(d(),g(d(),x)) -> g#(c(),g(e(),x)) ->
    g#(d(),g(d(),x)) -> g#(e(),x)
    g#(d(),g(d(),x)) -> g#(c(),g(e(),x)) ->
    g#(c(),g(c(),x)) -> g#(e(),g(d(),x))
    g#(d(),g(d(),x)) -> g#(c(),g(e(),x)) ->
    g#(c(),g(c(),x)) -> g#(d(),x)
    g#(d(),g(d(),x)) -> g#(c(),g(e(),x)) ->
    g#(x,x) -> g#(a(),b())
    g#(e(),g(e(),x)) -> g#(d(),g(c(),x)) ->
    g#(e(),g(e(),x)) -> g#(d(),g(c(),x))
    g#(e(),g(e(),x)) -> g#(d(),g(c(),x)) ->
    g#(e(),g(e(),x)) -> g#(c(),x)
    g#(e(),g(e(),x)) -> g#(d(),g(c(),x)) ->
    g#(d(),g(d(),x)) -> g#(c(),g(e(),x))
    g#(e(),g(e(),x)) -> g#(d(),g(c(),x)) ->
    g#(d(),g(d(),x)) -> g#(e(),x)
    g#(e(),g(e(),x)) -> g#(d(),g(c(),x)) ->
    g#(c(),g(c(),x)) -> g#(e(),g(d(),x))
    g#(e(),g(e(),x)) -> g#(d(),g(c(),x)) ->
    g#(c(),g(c(),x)) -> g#(d(),x)
    g#(e(),g(e(),x)) -> g#(d(),g(c(),x)) -> g#(x,x) -> g#(a(),b())
    g#(e(),g(e(),x)) -> g#(c(),x) ->
    g#(e(),g(e(),x)) -> g#(d(),g(c(),x))
    g#(e(),g(e(),x)) -> g#(c(),x) -> g#(e(),g(e(),x)) -> g#(c(),x)
    g#(e(),g(e(),x)) -> g#(c(),x) ->
    g#(d(),g(d(),x)) -> g#(c(),g(e(),x))
    g#(e(),g(e(),x)) -> g#(c(),x) -> g#(d(),g(d(),x)) -> g#(e(),x)
    g#(e(),g(e(),x)) -> g#(c(),x) ->
    g#(c(),g(c(),x)) -> g#(e(),g(d(),x))
    g#(e(),g(e(),x)) -> g#(c(),x) -> g#(c(),g(c(),x)) -> g#(d(),x)
    g#(e(),g(e(),x)) -> g#(c(),x) -> g#(x,x) -> g#(a(),b())
    g#(c(),g(c(),x)) -> g#(d(),x) ->
    g#(e(),g(e(),x)) -> g#(d(),g(c(),x))
    g#(c(),g(c(),x)) -> g#(d(),x) -> g#(e(),g(e(),x)) -> g#(c(),x)
    g#(c(),g(c(),x)) -> g#(d(),x) ->
    g#(d(),g(d(),x)) -> g#(c(),g(e(),x))
    g#(c(),g(c(),x)) -> g#(d(),x) -> g#(d(),g(d(),x)) -> g#(e(),x)
    g#(c(),g(c(),x)) -> g#(d(),x) ->
    g#(c(),g(c(),x)) -> g#(e(),g(d(),x))
    g#(c(),g(c(),x)) -> g#(d(),x) -> g#(c(),g(c(),x)) -> g#(d(),x)
    g#(c(),g(c(),x)) -> g#(d(),x) -> g#(x,x) -> g#(a(),b())
    g#(c(),g(c(),x)) -> g#(e(),g(d(),x)) ->
    g#(e(),g(e(),x)) -> g#(d(),g(c(),x))
    g#(c(),g(c(),x)) -> g#(e(),g(d(),x)) ->
    g#(e(),g(e(),x)) -> g#(c(),x)
    g#(c(),g(c(),x)) -> g#(e(),g(d(),x)) ->
    g#(d(),g(d(),x)) -> g#(c(),g(e(),x))
    g#(c(),g(c(),x)) -> g#(e(),g(d(),x)) ->
    g#(d(),g(d(),x)) -> g#(e(),x)
    g#(c(),g(c(),x)) -> g#(e(),g(d(),x)) ->
    g#(c(),g(c(),x)) -> g#(e(),g(d(),x))
    g#(c(),g(c(),x)) -> g#(e(),g(d(),x)) ->
    g#(c(),g(c(),x)) -> g#(d(),x)
    g#(c(),g(c(),x)) -> g#(e(),g(d(),x)) -> g#(x,x) -> g#(a(),b())
    g#(x,x) -> g#(a(),b()) -> g#(e(),g(e(),x)) -> g#(d(),g(c(),x))
    g#(x,x) -> g#(a(),b()) -> g#(e(),g(e(),x)) -> g#(c(),x)
    g#(x,x) -> g#(a(),b()) -> g#(d(),g(d(),x)) -> g#(c(),g(e(),x))
    g#(x,x) -> g#(a(),b()) -> g#(d(),g(d(),x)) -> g#(e(),x)
    g#(x,x) -> g#(a(),b()) -> g#(c(),g(c(),x)) -> g#(e(),g(d(),x))
    g#(x,x) -> g#(a(),b()) -> g#(c(),g(c(),x)) -> g#(d(),x)
    g#(x,x) -> g#(a(),b()) -> g#(x,x) -> g#(a(),b())
   EDG Processor:
    DPs:
     g#(x,x) -> g#(a(),b())
     g#(c(),g(c(),x)) -> g#(d(),x)
     g#(c(),g(c(),x)) -> g#(e(),g(d(),x))
     g#(d(),g(d(),x)) -> g#(e(),x)
     g#(d(),g(d(),x)) -> g#(c(),g(e(),x))
     g#(e(),g(e(),x)) -> g#(c(),x)
     g#(e(),g(e(),x)) -> g#(d(),g(c(),x))
     f#(g(x,y)) -> f#(x)
     f#(g(x,y)) -> f#(f(x))
     f#(g(x,y)) -> g#(f(f(x)),a())
     f#(g(x,y)) -> g#(y,g(f(f(x)),a()))
    TRS:
     g(x,x) -> g(a(),b())
     g(c(),g(c(),x)) -> g(e(),g(d(),x))
     g(d(),g(d(),x)) -> g(c(),g(e(),x))
     g(e(),g(e(),x)) -> g(d(),g(c(),x))
     f(g(x,y)) -> g(y,g(f(f(x)),a()))
    graph:
     f#(g(x,y)) -> f#(f(x)) -> f#(g(x,y)) -> f#(x)
     f#(g(x,y)) -> f#(f(x)) -> f#(g(x,y)) -> f#(f(x))
     f#(g(x,y)) -> f#(f(x)) -> f#(g(x,y)) -> g#(f(f(x)),a())
     f#(g(x,y)) -> f#(f(x)) -> f#(g(x,y)) -> g#(y,g(f(f(x)),a()))
     f#(g(x,y)) -> f#(x) -> f#(g(x,y)) -> f#(x)
     f#(g(x,y)) -> f#(x) -> f#(g(x,y)) -> f#(f(x))
     f#(g(x,y)) -> f#(x) -> f#(g(x,y)) -> g#(f(f(x)),a())
     f#(g(x,y)) -> f#(x) -> f#(g(x,y)) -> g#(y,g(f(f(x)),a()))
     f#(g(x,y)) -> g#(f(f(x)),a()) -> g#(x,x) -> g#(a(),b())
     f#(g(x,y)) -> g#(y,g(f(f(x)),a())) -> g#(x,x) -> g#(a(),b())
     f#(g(x,y)) -> g#(y,g(f(f(x)),a())) ->
     g#(c(),g(c(),x)) -> g#(d(),x)
     f#(g(x,y)) -> g#(y,g(f(f(x)),a())) ->
     g#(c(),g(c(),x)) -> g#(e(),g(d(),x))
     f#(g(x,y)) -> g#(y,g(f(f(x)),a())) ->
     g#(d(),g(d(),x)) -> g#(e(),x)
     f#(g(x,y)) -> g#(y,g(f(f(x)),a())) ->
     g#(d(),g(d(),x)) -> g#(c(),g(e(),x))
     f#(g(x,y)) -> g#(y,g(f(f(x)),a())) ->
     g#(e(),g(e(),x)) -> g#(c(),x)
     f#(g(x,y)) -> g#(y,g(f(f(x)),a())) ->
     g#(e(),g(e(),x)) -> g#(d(),g(c(),x))
     g#(d(),g(d(),x)) -> g#(e(),x) -> g#(x,x) -> g#(a(),b())
     g#(d(),g(d(),x)) -> g#(e(),x) -> g#(e(),g(e(),x)) -> g#(c(),x)
     g#(d(),g(d(),x)) -> g#(e(),x) ->
     g#(e(),g(e(),x)) -> g#(d(),g(c(),x))
     g#(d(),g(d(),x)) -> g#(c(),g(e(),x)) ->
     g#(x,x) -> g#(a(),b())
     g#(d(),g(d(),x)) -> g#(c(),g(e(),x)) ->
     g#(c(),g(c(),x)) -> g#(d(),x)
     g#(d(),g(d(),x)) -> g#(c(),g(e(),x)) ->
     g#(c(),g(c(),x)) -> g#(e(),g(d(),x))
     g#(e(),g(e(),x)) -> g#(d(),g(c(),x)) ->
     g#(x,x) -> g#(a(),b())
     g#(e(),g(e(),x)) -> g#(d(),g(c(),x)) ->
     g#(d(),g(d(),x)) -> g#(e(),x)
     g#(e(),g(e(),x)) -> g#(d(),g(c(),x)) ->
     g#(d(),g(d(),x)) -> g#(c(),g(e(),x))
     g#(e(),g(e(),x)) -> g#(c(),x) -> g#(x,x) -> g#(a(),b())
     g#(e(),g(e(),x)) -> g#(c(),x) -> g#(c(),g(c(),x)) -> g#(d(),x)
     g#(e(),g(e(),x)) -> g#(c(),x) ->
     g#(c(),g(c(),x)) -> g#(e(),g(d(),x))
     g#(c(),g(c(),x)) -> g#(d(),x) -> g#(x,x) -> g#(a(),b())
     g#(c(),g(c(),x)) -> g#(d(),x) -> g#(d(),g(d(),x)) -> g#(e(),x)
     g#(c(),g(c(),x)) -> g#(d(),x) ->
     g#(d(),g(d(),x)) -> g#(c(),g(e(),x))
     g#(c(),g(c(),x)) -> g#(e(),g(d(),x)) ->
     g#(x,x) -> g#(a(),b())
     g#(c(),g(c(),x)) -> g#(e(),g(d(),x)) ->
     g#(e(),g(e(),x)) -> g#(c(),x)
     g#(c(),g(c(),x)) -> g#(e(),g(d(),x)) -> g#(e(),g(e(),x)) -> g#(d(),g(c(),x))
    CDG Processor:
     DPs:
      g#(x,x) -> g#(a(),b())
      g#(c(),g(c(),x)) -> g#(d(),x)
      g#(c(),g(c(),x)) -> g#(e(),g(d(),x))
      g#(d(),g(d(),x)) -> g#(e(),x)
      g#(d(),g(d(),x)) -> g#(c(),g(e(),x))
      g#(e(),g(e(),x)) -> g#(c(),x)
      g#(e(),g(e(),x)) -> g#(d(),g(c(),x))
      f#(g(x,y)) -> f#(x)
      f#(g(x,y)) -> f#(f(x))
      f#(g(x,y)) -> g#(f(f(x)),a())
      f#(g(x,y)) -> g#(y,g(f(f(x)),a()))
     TRS:
      g(x,x) -> g(a(),b())
      g(c(),g(c(),x)) -> g(e(),g(d(),x))
      g(d(),g(d(),x)) -> g(c(),g(e(),x))
      g(e(),g(e(),x)) -> g(d(),g(c(),x))
      f(g(x,y)) -> g(y,g(f(f(x)),a()))
     graph:
      f#(g(x,y)) -> f#(f(x)) -> f#(g(x,y)) -> g#(y,g(f(f(x)),a()))
      f#(g(x,y)) -> f#(f(x)) -> f#(g(x,y)) -> g#(f(f(x)),a())
      f#(g(x,y)) -> f#(f(x)) -> f#(g(x,y)) -> f#(f(x))
      f#(g(x,y)) -> f#(f(x)) -> f#(g(x,y)) -> f#(x)
      f#(g(x,y)) -> f#(x) -> f#(g(x,y)) -> g#(y,g(f(f(x)),a()))
      f#(g(x,y)) -> f#(x) -> f#(g(x,y)) -> g#(f(f(x)),a())
      f#(g(x,y)) -> f#(x) -> f#(g(x,y)) -> f#(f(x))
      f#(g(x,y)) -> f#(x) -> f#(g(x,y)) -> f#(x)
      g#(d(),g(d(),x)) -> g#(e(),x) ->
      g#(e(),g(e(),x)) -> g#(d(),g(c(),x))
      g#(d(),g(d(),x)) -> g#(e(),x) ->
      g#(e(),g(e(),x)) -> g#(c(),x)
      g#(d(),g(d(),x)) -> g#(c(),g(e(),x)) ->
      g#(c(),g(c(),x)) -> g#(e(),g(d(),x))
      g#(d(),g(d(),x)) -> g#(c(),g(e(),x)) ->
      g#(c(),g(c(),x)) -> g#(d(),x)
      g#(e(),g(e(),x)) -> g#(d(),g(c(),x)) ->
      g#(d(),g(d(),x)) -> g#(c(),g(e(),x))
      g#(e(),g(e(),x)) -> g#(d(),g(c(),x)) ->
      g#(d(),g(d(),x)) -> g#(e(),x)
      g#(e(),g(e(),x)) -> g#(c(),x) ->
      g#(c(),g(c(),x)) -> g#(e(),g(d(),x))
      g#(e(),g(e(),x)) -> g#(c(),x) -> g#(c(),g(c(),x)) -> g#(d(),x)
      g#(c(),g(c(),x)) -> g#(d(),x) ->
      g#(d(),g(d(),x)) -> g#(c(),g(e(),x))
      g#(c(),g(c(),x)) -> g#(d(),x) ->
      g#(d(),g(d(),x)) -> g#(e(),x)
      g#(c(),g(c(),x)) -> g#(e(),g(d(),x)) ->
      g#(e(),g(e(),x)) -> g#(d(),g(c(),x))
      g#(c(),g(c(),x)) -> g#(e(),g(d(),x)) -> g#(e(),g(e(),x)) -> g#(c(),x)
     SCC Processor:
      #sccs: 2
      #rules: 8
      #arcs: 20/121
      DPs:
       g#(d(),g(d(),x)) -> g#(e(),x)
       g#(e(),g(e(),x)) -> g#(c(),x)
       g#(c(),g(c(),x)) -> g#(d(),x)
       g#(d(),g(d(),x)) -> g#(c(),g(e(),x))
       g#(c(),g(c(),x)) -> g#(e(),g(d(),x))
       g#(e(),g(e(),x)) -> g#(d(),g(c(),x))
      TRS:
       g(x,x) -> g(a(),b())
       g(c(),g(c(),x)) -> g(e(),g(d(),x))
       g(d(),g(d(),x)) -> g(c(),g(e(),x))
       g(e(),g(e(),x)) -> g(d(),g(c(),x))
       f(g(x,y)) -> g(y,g(f(f(x)),a()))
      Open
      
      DPs:
       f#(g(x,y)) -> f#(f(x))
       f#(g(x,y)) -> f#(x)
      TRS:
       g(x,x) -> g(a(),b())
       g(c(),g(c(),x)) -> g(e(),g(d(),x))
       g(d(),g(d(),x)) -> g(c(),g(e(),x))
       g(e(),g(e(),x)) -> g(d(),g(c(),x))
       f(g(x,y)) -> g(y,g(f(f(x)),a()))
      Matrix Interpretation Processor: dim=2
       
       interpretation:
        [f#](x0) = [0 2]x0 + [2],
        
                  [0 3]  
        [f](x0) = [1 0]x0,
        
              [0]
        [d] = [0],
        
              [0]
        [e] = [0],
        
              [0]
        [c] = [0],
        
              [0]
        [b] = [0],
        
              [0]
        [a] = [0],
        
                      [0 0]     [1 1]     [2]
        [g](x0, x1) = [1 1]x0 + [0 0]x1 + [2]
       orientation:
        f#(g(x,y)) = [2 2]x + [6] >= [2 0]x + [2] = f#(f(x))
        
        f#(g(x,y)) = [2 2]x + [6] >= [0 2]x + [2] = f#(x)
        
                 [1 1]    [2]    [2]             
        g(x,x) = [1 1]x + [2] >= [2] = g(a(),b())
        
                          [1 1]    [6]    [1 1]    [6]                  
        g(c(),g(c(),x)) = [0 0]x + [2] >= [0 0]x + [2] = g(e(),g(d(),x))
        
                          [1 1]    [6]    [1 1]    [6]                  
        g(d(),g(d(),x)) = [0 0]x + [2] >= [0 0]x + [2] = g(c(),g(e(),x))
        
                          [1 1]    [6]    [1 1]    [6]                  
        g(e(),g(e(),x)) = [0 0]x + [2] >= [0 0]x + [2] = g(d(),g(c(),x))
        
                    [3 3]    [0 0]    [6]    [3 3]    [0 0]    [6]                      
        f(g(x,y)) = [0 0]x + [1 1]y + [2] >= [0 0]x + [1 1]y + [2] = g(y,g(f(f(x)),a()))
       problem:
        DPs:
         
        TRS:
         g(x,x) -> g(a(),b())
         g(c(),g(c(),x)) -> g(e(),g(d(),x))
         g(d(),g(d(),x)) -> g(c(),g(e(),x))
         g(e(),g(e(),x)) -> g(d(),g(c(),x))
         f(g(x,y)) -> g(y,g(f(f(x)),a()))
       Qed