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())
   SCC Processor:
    #sccs: 2
    #rules: 9
    #arcs: 71/121
    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()))
    Arctic Interpretation Processor:
     dimension: 2
     interpretation:
      [f#](x0) = [2 0]x0 + [0],
      
                [-& 0 ]     [0]
      [f](x0) = [1  -&]x0 + [1],
      
            [0 ]
      [d] = [-&],
      
            [1]
      [e] = [0],
      
            [0]
      [c] = [0],
      
            [0]
      [b] = [0],
      
            [0]
      [a] = [0],
      
                    [0  1 ]     [-& 0 ]     [1]
      [g](x0, x1) = [-& -&]x0 + [0  1 ]x1 + [1]
     orientation:
      f#(g(x,y)) = [2 3]x + [0 2]y + [3] >= [1 2]x + [2] = f#(f(x))
      
      f#(g(x,y)) = [2 3]x + [0 2]y + [3] >= [2 0]x + [0] = f#(x)
      
               [0 1]    [1]    [1]             
      g(x,x) = [0 1]x + [1] >= [1] = g(a(),b())
      
                        [0 1]    [1]    [0 1]    [1]                  
      g(c(),g(c(),x)) = [1 2]x + [2] >= [1 2]x + [2] = g(e(),g(d(),x))
      
                        [0 1]    [1]    [0 1]    [1]                  
      g(d(),g(d(),x)) = [1 2]x + [2] >= [1 2]x + [2] = g(c(),g(e(),x))
      
                        [0 1]    [1]    [0 1]    [1]                  
      g(e(),g(e(),x)) = [1 2]x + [2] >= [1 2]x + [2] = g(d(),g(c(),x))
      
                  [-& -&]    [0  1 ]    [1]    [-& -&]    [0  1 ]    [1]                      
      f(g(x,y)) = [1  2 ]x + [-& 1 ]y + [2] >= [1  2 ]x + [-& -&]y + [2] = g(y,g(f(f(x)),a()))
     problem:
      DPs:
       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()))
     Subterm Criterion Processor:
      simple projection:
       pi(f#) = 0
      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
    
    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))
    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()))
    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))
     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:
      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))
      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:
       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: 1
       #rules: 6
       #arcs: 12/49
       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()))
       Arctic Interpretation Processor:
        dimension: 1
        interpretation:
         [g#](x0, x1) = x1,
         
         [f](x0) = x0 + 6,
         
         [d] = 3,
         
         [e] = 1,
         
         [c] = 1,
         
         [b] = 3,
         
         [a] = 1,
         
         [g](x0, x1) = 1x1 + 4
        orientation:
         g#(d(),g(d(),x)) = 1x + 4 >= x = g#(e(),x)
         
         g#(e(),g(e(),x)) = 1x + 4 >= x = g#(c(),x)
         
         g#(c(),g(c(),x)) = 1x + 4 >= x = g#(d(),x)
         
         g#(d(),g(d(),x)) = 1x + 4 >= 1x + 4 = g#(c(),g(e(),x))
         
         g#(c(),g(c(),x)) = 1x + 4 >= 1x + 4 = g#(e(),g(d(),x))
         
         g#(e(),g(e(),x)) = 1x + 4 >= 1x + 4 = g#(d(),g(c(),x))
         
         g(x,x) = 1x + 4 >= 4 = g(a(),b())
         
         g(c(),g(c(),x)) = 2x + 5 >= 2x + 5 = g(e(),g(d(),x))
         
         g(d(),g(d(),x)) = 2x + 5 >= 2x + 5 = g(c(),g(e(),x))
         
         g(e(),g(e(),x)) = 2x + 5 >= 2x + 5 = g(d(),g(c(),x))
         
         f(g(x,y)) = 1y + 6 >= 5 = g(y,g(f(f(x)),a()))
        problem:
         DPs:
          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