YES

Problem:
 a(b(x1)) -> c(b(x1))
 c(c(x1)) -> d(b(x1))
 d(x1) -> c(e(x1))
 b(b(x1)) -> f(x1)
 c(b(x1)) -> g(x1)
 e(x1) -> f(x1)
 e(x1) -> b(b(x1))
 f(g(x1)) -> a(c(x1))
 g(f(x1)) -> e(x1)
 a(x1) -> b(c(x1))

Proof:
 DP Processor:
  DPs:
   a#(b(x1)) -> c#(b(x1))
   c#(c(x1)) -> b#(x1)
   c#(c(x1)) -> d#(b(x1))
   d#(x1) -> e#(x1)
   d#(x1) -> c#(e(x1))
   b#(b(x1)) -> f#(x1)
   c#(b(x1)) -> g#(x1)
   e#(x1) -> f#(x1)
   e#(x1) -> b#(x1)
   e#(x1) -> b#(b(x1))
   f#(g(x1)) -> c#(x1)
   f#(g(x1)) -> a#(c(x1))
   g#(f(x1)) -> e#(x1)
   a#(x1) -> c#(x1)
   a#(x1) -> b#(c(x1))
  TRS:
   a(b(x1)) -> c(b(x1))
   c(c(x1)) -> d(b(x1))
   d(x1) -> c(e(x1))
   b(b(x1)) -> f(x1)
   c(b(x1)) -> g(x1)
   e(x1) -> f(x1)
   e(x1) -> b(b(x1))
   f(g(x1)) -> a(c(x1))
   g(f(x1)) -> e(x1)
   a(x1) -> b(c(x1))
  TDG Processor:
   DPs:
    a#(b(x1)) -> c#(b(x1))
    c#(c(x1)) -> b#(x1)
    c#(c(x1)) -> d#(b(x1))
    d#(x1) -> e#(x1)
    d#(x1) -> c#(e(x1))
    b#(b(x1)) -> f#(x1)
    c#(b(x1)) -> g#(x1)
    e#(x1) -> f#(x1)
    e#(x1) -> b#(x1)
    e#(x1) -> b#(b(x1))
    f#(g(x1)) -> c#(x1)
    f#(g(x1)) -> a#(c(x1))
    g#(f(x1)) -> e#(x1)
    a#(x1) -> c#(x1)
    a#(x1) -> b#(c(x1))
   TRS:
    a(b(x1)) -> c(b(x1))
    c(c(x1)) -> d(b(x1))
    d(x1) -> c(e(x1))
    b(b(x1)) -> f(x1)
    c(b(x1)) -> g(x1)
    e(x1) -> f(x1)
    e(x1) -> b(b(x1))
    f(g(x1)) -> a(c(x1))
    g(f(x1)) -> e(x1)
    a(x1) -> b(c(x1))
   graph:
    g#(f(x1)) -> e#(x1) -> e#(x1) -> b#(b(x1))
    g#(f(x1)) -> e#(x1) -> e#(x1) -> b#(x1)
    g#(f(x1)) -> e#(x1) -> e#(x1) -> f#(x1)
    f#(g(x1)) -> c#(x1) -> c#(b(x1)) -> g#(x1)
    f#(g(x1)) -> c#(x1) -> c#(c(x1)) -> d#(b(x1))
    f#(g(x1)) -> c#(x1) -> c#(c(x1)) -> b#(x1)
    f#(g(x1)) -> a#(c(x1)) -> a#(x1) -> b#(c(x1))
    f#(g(x1)) -> a#(c(x1)) -> a#(x1) -> c#(x1)
    f#(g(x1)) -> a#(c(x1)) -> a#(b(x1)) -> c#(b(x1))
    e#(x1) -> f#(x1) -> f#(g(x1)) -> a#(c(x1))
    e#(x1) -> f#(x1) -> f#(g(x1)) -> c#(x1)
    e#(x1) -> b#(b(x1)) -> b#(b(x1)) -> f#(x1)
    e#(x1) -> b#(x1) -> b#(b(x1)) -> f#(x1)
    d#(x1) -> e#(x1) -> e#(x1) -> b#(b(x1))
    d#(x1) -> e#(x1) -> e#(x1) -> b#(x1)
    d#(x1) -> e#(x1) -> e#(x1) -> f#(x1)
    d#(x1) -> c#(e(x1)) -> c#(b(x1)) -> g#(x1)
    d#(x1) -> c#(e(x1)) -> c#(c(x1)) -> d#(b(x1))
    d#(x1) -> c#(e(x1)) -> c#(c(x1)) -> b#(x1)
    b#(b(x1)) -> f#(x1) -> f#(g(x1)) -> a#(c(x1))
    b#(b(x1)) -> f#(x1) -> f#(g(x1)) -> c#(x1)
    c#(c(x1)) -> d#(b(x1)) -> d#(x1) -> c#(e(x1))
    c#(c(x1)) -> d#(b(x1)) -> d#(x1) -> e#(x1)
    c#(c(x1)) -> b#(x1) -> b#(b(x1)) -> f#(x1)
    c#(b(x1)) -> g#(x1) -> g#(f(x1)) -> e#(x1)
    a#(b(x1)) -> c#(b(x1)) -> c#(b(x1)) -> g#(x1)
    a#(b(x1)) -> c#(b(x1)) -> c#(c(x1)) -> d#(b(x1))
    a#(b(x1)) -> c#(b(x1)) -> c#(c(x1)) -> b#(x1)
    a#(x1) -> b#(c(x1)) -> b#(b(x1)) -> f#(x1)
    a#(x1) -> c#(x1) -> c#(b(x1)) -> g#(x1)
    a#(x1) -> c#(x1) -> c#(c(x1)) -> d#(b(x1))
    a#(x1) -> c#(x1) -> c#(c(x1)) -> b#(x1)
   Arctic Interpretation Processor:
    dimension: 2
    usable rules:
     a(b(x1)) -> c(b(x1))
     c(c(x1)) -> d(b(x1))
     d(x1) -> c(e(x1))
     b(b(x1)) -> f(x1)
     c(b(x1)) -> g(x1)
     e(x1) -> f(x1)
     e(x1) -> b(b(x1))
     f(g(x1)) -> a(c(x1))
     g(f(x1)) -> e(x1)
     a(x1) -> b(c(x1))
    interpretation:
     [g#](x0) = [0 1]x0 + [0],
     
     [f#](x0) = [1 1]x0 + [0],
     
     [e#](x0) = [1 1]x0 + [0],
     
     [d#](x0) = [1 1]x0 + [0],
     
     [b#](x0) = [1 0]x0 + [0],
     
     [c#](x0) = [1 0]x0 + [0],
     
     [a#](x0) = [3 1]x0 + [0],
     
               [0  -&]     [-&]
     [g](x0) = [3  3 ]x0 + [0 ],
     
               [0 0]  
     [f](x0) = [0 0]x0,
     
               [0 0]     [-&]
     [e](x0) = [0 0]x0 + [0 ],
     
               [0 0]     [0]
     [d](x0) = [3 3]x0 + [0],
     
               [0 0]     [-&]
     [c](x0) = [3 0]x0 + [0 ],
     
               [3 0]     [0]
     [a](x0) = [3 0]x0 + [0],
     
               [0 0]  
     [b](x0) = [0 0]x0
    orientation:
     a#(b(x1)) = [3 3]x1 + [0] >= [1 1]x1 + [0] = c#(b(x1))
     
     c#(c(x1)) = [3 1]x1 + [0] >= [1 0]x1 + [0] = b#(x1)
     
     c#(c(x1)) = [3 1]x1 + [0] >= [1 1]x1 + [0] = d#(b(x1))
     
     d#(x1) = [1 1]x1 + [0] >= [1 1]x1 + [0] = e#(x1)
     
     d#(x1) = [1 1]x1 + [0] >= [1 1]x1 + [0] = c#(e(x1))
     
     b#(b(x1)) = [1 1]x1 + [0] >= [1 1]x1 + [0] = f#(x1)
     
     c#(b(x1)) = [1 1]x1 + [0] >= [0 1]x1 + [0] = g#(x1)
     
     e#(x1) = [1 1]x1 + [0] >= [1 1]x1 + [0] = f#(x1)
     
     e#(x1) = [1 1]x1 + [0] >= [1 0]x1 + [0] = b#(x1)
     
     e#(x1) = [1 1]x1 + [0] >= [1 1]x1 + [0] = b#(b(x1))
     
     f#(g(x1)) = [4 4]x1 + [1] >= [1 0]x1 + [0] = c#(x1)
     
     f#(g(x1)) = [4 4]x1 + [1] >= [4 3]x1 + [1] = a#(c(x1))
     
     g#(f(x1)) = [1 1]x1 + [0] >= [1 1]x1 + [0] = e#(x1)
     
     a#(x1) = [3 1]x1 + [0] >= [1 0]x1 + [0] = c#(x1)
     
     a#(x1) = [3 1]x1 + [0] >= [3 1]x1 + [0] = b#(c(x1))
     
                [3 3]     [0]    [0 0]     [-&]           
     a(b(x1)) = [3 3]x1 + [0] >= [3 3]x1 + [0 ] = c(b(x1))
     
                [3 0]     [0]    [0 0]     [0]           
     c(c(x1)) = [3 3]x1 + [0] >= [3 3]x1 + [0] = d(b(x1))
     
             [0 0]     [0]    [0 0]     [0]           
     d(x1) = [3 3]x1 + [0] >= [3 3]x1 + [0] = c(e(x1))
     
                [0 0]      [0 0]          
     b(b(x1)) = [0 0]x1 >= [0 0]x1 = f(x1)
     
                [0 0]     [-&]    [0  -&]     [-&]        
     c(b(x1)) = [3 3]x1 + [0 ] >= [3  3 ]x1 + [0 ] = g(x1)
     
             [0 0]     [-&]    [0 0]          
     e(x1) = [0 0]x1 + [0 ] >= [0 0]x1 = f(x1)
     
             [0 0]     [-&]    [0 0]             
     e(x1) = [0 0]x1 + [0 ] >= [0 0]x1 = b(b(x1))
     
                [3 3]     [0]    [3 3]     [0]           
     f(g(x1)) = [3 3]x1 + [0] >= [3 3]x1 + [0] = a(c(x1))
     
                [0 0]     [-&]    [0 0]     [-&]        
     g(f(x1)) = [3 3]x1 + [0 ] >= [0 0]x1 + [0 ] = e(x1)
     
             [3 0]     [0]    [3 0]     [0]           
     a(x1) = [3 0]x1 + [0] >= [3 0]x1 + [0] = b(c(x1))
    problem:
     DPs:
      a#(b(x1)) -> c#(b(x1))
      c#(c(x1)) -> b#(x1)
      c#(c(x1)) -> d#(b(x1))
      d#(x1) -> e#(x1)
      d#(x1) -> c#(e(x1))
      b#(b(x1)) -> f#(x1)
      c#(b(x1)) -> g#(x1)
      e#(x1) -> f#(x1)
      e#(x1) -> b#(x1)
      e#(x1) -> b#(b(x1))
      f#(g(x1)) -> a#(c(x1))
      g#(f(x1)) -> e#(x1)
      a#(x1) -> c#(x1)
      a#(x1) -> b#(c(x1))
     TRS:
      a(b(x1)) -> c(b(x1))
      c(c(x1)) -> d(b(x1))
      d(x1) -> c(e(x1))
      b(b(x1)) -> f(x1)
      c(b(x1)) -> g(x1)
      e(x1) -> f(x1)
      e(x1) -> b(b(x1))
      f(g(x1)) -> a(c(x1))
      g(f(x1)) -> e(x1)
      a(x1) -> b(c(x1))
    Restore Modifier:
     DPs:
      a#(b(x1)) -> c#(b(x1))
      c#(c(x1)) -> b#(x1)
      c#(c(x1)) -> d#(b(x1))
      d#(x1) -> e#(x1)
      d#(x1) -> c#(e(x1))
      b#(b(x1)) -> f#(x1)
      c#(b(x1)) -> g#(x1)
      e#(x1) -> f#(x1)
      e#(x1) -> b#(x1)
      e#(x1) -> b#(b(x1))
      f#(g(x1)) -> a#(c(x1))
      g#(f(x1)) -> e#(x1)
      a#(x1) -> c#(x1)
      a#(x1) -> b#(c(x1))
     TRS:
      a(b(x1)) -> c(b(x1))
      c(c(x1)) -> d(b(x1))
      d(x1) -> c(e(x1))
      b(b(x1)) -> f(x1)
      c(b(x1)) -> g(x1)
      e(x1) -> f(x1)
      e(x1) -> b(b(x1))
      f(g(x1)) -> a(c(x1))
      g(f(x1)) -> e(x1)
      a(x1) -> b(c(x1))
     EDG Processor:
      DPs:
       a#(b(x1)) -> c#(b(x1))
       c#(c(x1)) -> b#(x1)
       c#(c(x1)) -> d#(b(x1))
       d#(x1) -> e#(x1)
       d#(x1) -> c#(e(x1))
       b#(b(x1)) -> f#(x1)
       c#(b(x1)) -> g#(x1)
       e#(x1) -> f#(x1)
       e#(x1) -> b#(x1)
       e#(x1) -> b#(b(x1))
       f#(g(x1)) -> a#(c(x1))
       g#(f(x1)) -> e#(x1)
       a#(x1) -> c#(x1)
       a#(x1) -> b#(c(x1))
      TRS:
       a(b(x1)) -> c(b(x1))
       c(c(x1)) -> d(b(x1))
       d(x1) -> c(e(x1))
       b(b(x1)) -> f(x1)
       c(b(x1)) -> g(x1)
       e(x1) -> f(x1)
       e(x1) -> b(b(x1))
       f(g(x1)) -> a(c(x1))
       g(f(x1)) -> e(x1)
       a(x1) -> b(c(x1))
      graph:
       g#(f(x1)) -> e#(x1) -> e#(x1) -> f#(x1)
       g#(f(x1)) -> e#(x1) -> e#(x1) -> b#(x1)
       g#(f(x1)) -> e#(x1) -> e#(x1) -> b#(b(x1))
       f#(g(x1)) -> a#(c(x1)) -> a#(b(x1)) -> c#(b(x1))
       f#(g(x1)) -> a#(c(x1)) -> a#(x1) -> c#(x1)
       f#(g(x1)) -> a#(c(x1)) -> a#(x1) -> b#(c(x1))
       e#(x1) -> f#(x1) -> f#(g(x1)) -> a#(c(x1))
       e#(x1) -> b#(b(x1)) -> b#(b(x1)) -> f#(x1)
       e#(x1) -> b#(x1) -> b#(b(x1)) -> f#(x1)
       d#(x1) -> e#(x1) -> e#(x1) -> f#(x1)
       d#(x1) -> e#(x1) -> e#(x1) -> b#(x1)
       d#(x1) -> e#(x1) -> e#(x1) -> b#(b(x1))
       d#(x1) -> c#(e(x1)) -> c#(c(x1)) -> b#(x1)
       d#(x1) -> c#(e(x1)) -> c#(c(x1)) -> d#(b(x1))
       d#(x1) -> c#(e(x1)) -> c#(b(x1)) -> g#(x1)
       b#(b(x1)) -> f#(x1) -> f#(g(x1)) -> a#(c(x1))
       c#(c(x1)) -> d#(b(x1)) -> d#(x1) -> e#(x1)
       c#(c(x1)) -> d#(b(x1)) -> d#(x1) -> c#(e(x1))
       c#(c(x1)) -> b#(x1) -> b#(b(x1)) -> f#(x1)
       c#(b(x1)) -> g#(x1) -> g#(f(x1)) -> e#(x1)
       a#(b(x1)) -> c#(b(x1)) -> c#(c(x1)) -> b#(x1)
       a#(b(x1)) -> c#(b(x1)) -> c#(c(x1)) -> d#(b(x1))
       a#(b(x1)) -> c#(b(x1)) -> c#(b(x1)) -> g#(x1)
       a#(x1) -> b#(c(x1)) -> b#(b(x1)) -> f#(x1)
       a#(x1) -> c#(x1) -> c#(c(x1)) -> b#(x1)
       a#(x1) -> c#(x1) -> c#(c(x1)) -> d#(b(x1))
       a#(x1) -> c#(x1) -> c#(b(x1)) -> g#(x1)
      Arctic Interpretation Processor:
       dimension: 2
       usable rules:
        a(b(x1)) -> c(b(x1))
        c(c(x1)) -> d(b(x1))
        d(x1) -> c(e(x1))
        b(b(x1)) -> f(x1)
        c(b(x1)) -> g(x1)
        e(x1) -> f(x1)
        e(x1) -> b(b(x1))
        f(g(x1)) -> a(c(x1))
        g(f(x1)) -> e(x1)
        a(x1) -> b(c(x1))
       interpretation:
        [g#](x0) = [0 0]x0 + [0],
        
        [f#](x0) = [0 0]x0 + [0],
        
        [e#](x0) = [0 0]x0 + [0],
        
        [d#](x0) = [0 0]x0 + [0],
        
        [b#](x0) = [0 0]x0 + [0],
        
        [c#](x0) = [0 0]x0 + [0],
        
        [a#](x0) = [2 0]x0 + [0],
        
                  [0 0]     [0]
        [g](x0) = [2 2]x0 + [2],
        
                  [0  0 ]     [-&]
        [f](x0) = [-& 0 ]x0 + [0 ],
        
                  [0 0]     [0]
        [e](x0) = [0 0]x0 + [0],
        
                  [0 0]     [0]
        [d](x0) = [2 2]x0 + [2],
        
                  [0 0]     [0]
        [c](x0) = [2 0]x0 + [0],
        
                  [2 0]     [0]
        [a](x0) = [2 0]x0 + [1],
        
                  [0  0 ]     [0]
        [b](x0) = [-& 0 ]x0 + [0]
       orientation:
        a#(b(x1)) = [2 2]x1 + [2] >= [0 0]x1 + [0] = c#(b(x1))
        
        c#(c(x1)) = [2 0]x1 + [0] >= [0 0]x1 + [0] = b#(x1)
        
        c#(c(x1)) = [2 0]x1 + [0] >= [0 0]x1 + [0] = d#(b(x1))
        
        d#(x1) = [0 0]x1 + [0] >= [0 0]x1 + [0] = e#(x1)
        
        d#(x1) = [0 0]x1 + [0] >= [0 0]x1 + [0] = c#(e(x1))
        
        b#(b(x1)) = [0 0]x1 + [0] >= [0 0]x1 + [0] = f#(x1)
        
        c#(b(x1)) = [0 0]x1 + [0] >= [0 0]x1 + [0] = g#(x1)
        
        e#(x1) = [0 0]x1 + [0] >= [0 0]x1 + [0] = f#(x1)
        
        e#(x1) = [0 0]x1 + [0] >= [0 0]x1 + [0] = b#(x1)
        
        e#(x1) = [0 0]x1 + [0] >= [0 0]x1 + [0] = b#(b(x1))
        
        f#(g(x1)) = [2 2]x1 + [2] >= [2 2]x1 + [2] = a#(c(x1))
        
        g#(f(x1)) = [0 0]x1 + [0] >= [0 0]x1 + [0] = e#(x1)
        
        a#(x1) = [2 0]x1 + [0] >= [0 0]x1 + [0] = c#(x1)
        
        a#(x1) = [2 0]x1 + [0] >= [2 0]x1 + [0] = b#(c(x1))
        
                   [2 2]     [2]    [0 0]     [0]           
        a(b(x1)) = [2 2]x1 + [2] >= [2 2]x1 + [2] = c(b(x1))
        
                   [2 0]     [0]    [0 0]     [0]           
        c(c(x1)) = [2 2]x1 + [2] >= [2 2]x1 + [2] = d(b(x1))
        
                [0 0]     [0]    [0 0]     [0]           
        d(x1) = [2 2]x1 + [2] >= [2 2]x1 + [2] = c(e(x1))
        
                   [0  0 ]     [0]    [0  0 ]     [-&]        
        b(b(x1)) = [-& 0 ]x1 + [0] >= [-& 0 ]x1 + [0 ] = f(x1)
        
                   [0 0]     [0]    [0 0]     [0]        
        c(b(x1)) = [2 2]x1 + [2] >= [2 2]x1 + [2] = g(x1)
        
                [0 0]     [0]    [0  0 ]     [-&]        
        e(x1) = [0 0]x1 + [0] >= [-& 0 ]x1 + [0 ] = f(x1)
        
                [0 0]     [0]    [0  0 ]     [0]           
        e(x1) = [0 0]x1 + [0] >= [-& 0 ]x1 + [0] = b(b(x1))
        
                   [2 2]     [2]    [2 2]     [2]           
        f(g(x1)) = [2 2]x1 + [2] >= [2 2]x1 + [2] = a(c(x1))
        
                   [0 0]     [0]    [0 0]     [0]        
        g(f(x1)) = [2 2]x1 + [2] >= [0 0]x1 + [0] = e(x1)
        
                [2 0]     [0]    [2 0]     [0]           
        a(x1) = [2 0]x1 + [1] >= [2 0]x1 + [0] = b(c(x1))
       problem:
        DPs:
         c#(c(x1)) -> b#(x1)
         c#(c(x1)) -> d#(b(x1))
         d#(x1) -> e#(x1)
         d#(x1) -> c#(e(x1))
         b#(b(x1)) -> f#(x1)
         c#(b(x1)) -> g#(x1)
         e#(x1) -> f#(x1)
         e#(x1) -> b#(x1)
         e#(x1) -> b#(b(x1))
         f#(g(x1)) -> a#(c(x1))
         g#(f(x1)) -> e#(x1)
         a#(x1) -> c#(x1)
         a#(x1) -> b#(c(x1))
        TRS:
         a(b(x1)) -> c(b(x1))
         c(c(x1)) -> d(b(x1))
         d(x1) -> c(e(x1))
         b(b(x1)) -> f(x1)
         c(b(x1)) -> g(x1)
         e(x1) -> f(x1)
         e(x1) -> b(b(x1))
         f(g(x1)) -> a(c(x1))
         g(f(x1)) -> e(x1)
         a(x1) -> b(c(x1))
       Restore Modifier:
        DPs:
         c#(c(x1)) -> b#(x1)
         c#(c(x1)) -> d#(b(x1))
         d#(x1) -> e#(x1)
         d#(x1) -> c#(e(x1))
         b#(b(x1)) -> f#(x1)
         c#(b(x1)) -> g#(x1)
         e#(x1) -> f#(x1)
         e#(x1) -> b#(x1)
         e#(x1) -> b#(b(x1))
         f#(g(x1)) -> a#(c(x1))
         g#(f(x1)) -> e#(x1)
         a#(x1) -> c#(x1)
         a#(x1) -> b#(c(x1))
        TRS:
         a(b(x1)) -> c(b(x1))
         c(c(x1)) -> d(b(x1))
         d(x1) -> c(e(x1))
         b(b(x1)) -> f(x1)
         c(b(x1)) -> g(x1)
         e(x1) -> f(x1)
         e(x1) -> b(b(x1))
         f(g(x1)) -> a(c(x1))
         g(f(x1)) -> e(x1)
         a(x1) -> b(c(x1))
        EDG Processor:
         DPs:
          c#(c(x1)) -> b#(x1)
          c#(c(x1)) -> d#(b(x1))
          d#(x1) -> e#(x1)
          d#(x1) -> c#(e(x1))
          b#(b(x1)) -> f#(x1)
          c#(b(x1)) -> g#(x1)
          e#(x1) -> f#(x1)
          e#(x1) -> b#(x1)
          e#(x1) -> b#(b(x1))
          f#(g(x1)) -> a#(c(x1))
          g#(f(x1)) -> e#(x1)
          a#(x1) -> c#(x1)
          a#(x1) -> b#(c(x1))
         TRS:
          a(b(x1)) -> c(b(x1))
          c(c(x1)) -> d(b(x1))
          d(x1) -> c(e(x1))
          b(b(x1)) -> f(x1)
          c(b(x1)) -> g(x1)
          e(x1) -> f(x1)
          e(x1) -> b(b(x1))
          f(g(x1)) -> a(c(x1))
          g(f(x1)) -> e(x1)
          a(x1) -> b(c(x1))
         graph:
          g#(f(x1)) -> e#(x1) -> e#(x1) -> b#(b(x1))
          g#(f(x1)) -> e#(x1) -> e#(x1) -> b#(x1)
          g#(f(x1)) -> e#(x1) -> e#(x1) -> f#(x1)
          f#(g(x1)) -> a#(c(x1)) -> a#(x1) -> b#(c(x1))
          f#(g(x1)) -> a#(c(x1)) -> a#(x1) -> c#(x1)
          e#(x1) -> f#(x1) -> f#(g(x1)) -> a#(c(x1))
          e#(x1) -> b#(b(x1)) -> b#(b(x1)) -> f#(x1)
          e#(x1) -> b#(x1) -> b#(b(x1)) -> f#(x1)
          d#(x1) -> e#(x1) -> e#(x1) -> b#(b(x1))
          d#(x1) -> e#(x1) -> e#(x1) -> b#(x1)
          d#(x1) -> e#(x1) -> e#(x1) -> f#(x1)
          d#(x1) -> c#(e(x1)) -> c#(b(x1)) -> g#(x1)
          d#(x1) -> c#(e(x1)) -> c#(c(x1)) -> d#(b(x1))
          d#(x1) -> c#(e(x1)) -> c#(c(x1)) -> b#(x1)
          b#(b(x1)) -> f#(x1) -> f#(g(x1)) -> a#(c(x1))
          c#(c(x1)) -> d#(b(x1)) -> d#(x1) -> c#(e(x1))
          c#(c(x1)) -> d#(b(x1)) -> d#(x1) -> e#(x1)
          c#(c(x1)) -> b#(x1) -> b#(b(x1)) -> f#(x1)
          c#(b(x1)) -> g#(x1) -> g#(f(x1)) -> e#(x1)
          a#(x1) -> b#(c(x1)) -> b#(b(x1)) -> f#(x1)
          a#(x1) -> c#(x1) -> c#(b(x1)) -> g#(x1)
          a#(x1) -> c#(x1) -> c#(c(x1)) -> d#(b(x1))
          a#(x1) -> c#(x1) -> c#(c(x1)) -> b#(x1)
         Arctic Interpretation Processor:
          dimension: 2
          usable rules:
           a(b(x1)) -> c(b(x1))
           c(c(x1)) -> d(b(x1))
           d(x1) -> c(e(x1))
           b(b(x1)) -> f(x1)
           c(b(x1)) -> g(x1)
           e(x1) -> f(x1)
           e(x1) -> b(b(x1))
           f(g(x1)) -> a(c(x1))
           g(f(x1)) -> e(x1)
           a(x1) -> b(c(x1))
          interpretation:
           [g#](x0) = [1 0]x0 + [1],
           
           [f#](x0) = [1 0]x0 + [0],
           
           [e#](x0) = [1 0]x0 + [1],
           
           [d#](x0) = [1 1]x0 + [1],
           
           [b#](x0) = [1 0]x0 + [0],
           
           [c#](x0) = [0 1]x0,
           
           [a#](x0) = [1 2]x0 + [0],
           
                     [1 1]     [1]
           [g](x0) = [0 0]x0 + [0],
           
                     [0  -&]  
           [f](x0) = [0  0 ]x0,
           
                     [0 0]     [0]
           [e](x0) = [0 0]x0 + [0],
           
                     [1 1]     [1]
           [d](x0) = [0 0]x0 + [0],
           
                     [0 1]     [-&]
           [c](x0) = [0 0]x0 + [0 ],
           
                     [0 1]     [1]
           [a](x0) = [0 1]x0 + [0],
           
                     [0  -&]     [-&]
           [b](x0) = [0  0 ]x0 + [0 ]
          orientation:
           c#(c(x1)) = [1 1]x1 + [1] >= [1 0]x1 + [0] = b#(x1)
           
           c#(c(x1)) = [1 1]x1 + [1] >= [1 1]x1 + [1] = d#(b(x1))
           
           d#(x1) = [1 1]x1 + [1] >= [1 0]x1 + [1] = e#(x1)
           
           d#(x1) = [1 1]x1 + [1] >= [1 1]x1 + [1] = c#(e(x1))
           
           b#(b(x1)) = [1 0]x1 + [0] >= [1 0]x1 + [0] = f#(x1)
           
           c#(b(x1)) = [1 1]x1 + [1] >= [1 0]x1 + [1] = g#(x1)
           
           e#(x1) = [1 0]x1 + [1] >= [1 0]x1 + [0] = f#(x1)
           
           e#(x1) = [1 0]x1 + [1] >= [1 0]x1 + [0] = b#(x1)
           
           e#(x1) = [1 0]x1 + [1] >= [1 0]x1 + [0] = b#(b(x1))
           
           f#(g(x1)) = [2 2]x1 + [2] >= [2 2]x1 + [2] = a#(c(x1))
           
           g#(f(x1)) = [1 0]x1 + [1] >= [1 0]x1 + [1] = e#(x1)
           
           a#(x1) = [1 2]x1 + [0] >= [0 1]x1 = c#(x1)
           
           a#(x1) = [1 2]x1 + [0] >= [1 2]x1 + [0] = b#(c(x1))
           
                      [1 1]     [1]    [1 1]     [1]           
           a(b(x1)) = [1 1]x1 + [1] >= [0 0]x1 + [0] = c(b(x1))
           
                      [1 1]     [1]    [1 1]     [1]           
           c(c(x1)) = [0 1]x1 + [0] >= [0 0]x1 + [0] = d(b(x1))
           
                   [1 1]     [1]    [1 1]     [1]           
           d(x1) = [0 0]x1 + [0] >= [0 0]x1 + [0] = c(e(x1))
           
                      [0  -&]     [-&]    [0  -&]          
           b(b(x1)) = [0  0 ]x1 + [0 ] >= [0  0 ]x1 = f(x1)
           
                      [1 1]     [1]    [1 1]     [1]        
           c(b(x1)) = [0 0]x1 + [0] >= [0 0]x1 + [0] = g(x1)
           
                   [0 0]     [0]    [0  -&]          
           e(x1) = [0 0]x1 + [0] >= [0  0 ]x1 = f(x1)
           
                   [0 0]     [0]    [0  -&]     [-&]           
           e(x1) = [0 0]x1 + [0] >= [0  0 ]x1 + [0 ] = b(b(x1))
           
                      [1 1]     [1]    [1 1]     [1]           
           f(g(x1)) = [1 1]x1 + [1] >= [1 1]x1 + [1] = a(c(x1))
           
                      [1 1]     [1]    [0 0]     [0]        
           g(f(x1)) = [0 0]x1 + [0] >= [0 0]x1 + [0] = e(x1)
           
                   [0 1]     [1]    [0 1]     [-&]           
           a(x1) = [0 1]x1 + [0] >= [0 1]x1 + [0 ] = b(c(x1))
          problem:
           DPs:
            c#(c(x1)) -> b#(x1)
            c#(c(x1)) -> d#(b(x1))
            d#(x1) -> e#(x1)
            d#(x1) -> c#(e(x1))
            b#(b(x1)) -> f#(x1)
            c#(b(x1)) -> g#(x1)
            e#(x1) -> f#(x1)
            e#(x1) -> b#(x1)
            e#(x1) -> b#(b(x1))
            f#(g(x1)) -> a#(c(x1))
            g#(f(x1)) -> e#(x1)
            a#(x1) -> b#(c(x1))
           TRS:
            a(b(x1)) -> c(b(x1))
            c(c(x1)) -> d(b(x1))
            d(x1) -> c(e(x1))
            b(b(x1)) -> f(x1)
            c(b(x1)) -> g(x1)
            e(x1) -> f(x1)
            e(x1) -> b(b(x1))
            f(g(x1)) -> a(c(x1))
            g(f(x1)) -> e(x1)
            a(x1) -> b(c(x1))
          Restore Modifier:
           DPs:
            c#(c(x1)) -> b#(x1)
            c#(c(x1)) -> d#(b(x1))
            d#(x1) -> e#(x1)
            d#(x1) -> c#(e(x1))
            b#(b(x1)) -> f#(x1)
            c#(b(x1)) -> g#(x1)
            e#(x1) -> f#(x1)
            e#(x1) -> b#(x1)
            e#(x1) -> b#(b(x1))
            f#(g(x1)) -> a#(c(x1))
            g#(f(x1)) -> e#(x1)
            a#(x1) -> b#(c(x1))
           TRS:
            a(b(x1)) -> c(b(x1))
            c(c(x1)) -> d(b(x1))
            d(x1) -> c(e(x1))
            b(b(x1)) -> f(x1)
            c(b(x1)) -> g(x1)
            e(x1) -> f(x1)
            e(x1) -> b(b(x1))
            f(g(x1)) -> a(c(x1))
            g(f(x1)) -> e(x1)
            a(x1) -> b(c(x1))
           EDG Processor:
            DPs:
             c#(c(x1)) -> b#(x1)
             c#(c(x1)) -> d#(b(x1))
             d#(x1) -> e#(x1)
             d#(x1) -> c#(e(x1))
             b#(b(x1)) -> f#(x1)
             c#(b(x1)) -> g#(x1)
             e#(x1) -> f#(x1)
             e#(x1) -> b#(x1)
             e#(x1) -> b#(b(x1))
             f#(g(x1)) -> a#(c(x1))
             g#(f(x1)) -> e#(x1)
             a#(x1) -> b#(c(x1))
            TRS:
             a(b(x1)) -> c(b(x1))
             c(c(x1)) -> d(b(x1))
             d(x1) -> c(e(x1))
             b(b(x1)) -> f(x1)
             c(b(x1)) -> g(x1)
             e(x1) -> f(x1)
             e(x1) -> b(b(x1))
             f(g(x1)) -> a(c(x1))
             g(f(x1)) -> e(x1)
             a(x1) -> b(c(x1))
            graph:
             g#(f(x1)) -> e#(x1) -> e#(x1) -> f#(x1)
             g#(f(x1)) -> e#(x1) -> e#(x1) -> b#(x1)
             g#(f(x1)) -> e#(x1) -> e#(x1) -> b#(b(x1))
             f#(g(x1)) -> a#(c(x1)) -> a#(x1) -> b#(c(x1))
             e#(x1) -> f#(x1) -> f#(g(x1)) -> a#(c(x1))
             e#(x1) -> b#(b(x1)) -> b#(b(x1)) -> f#(x1)
             e#(x1) -> b#(x1) -> b#(b(x1)) -> f#(x1)
             d#(x1) -> e#(x1) -> e#(x1) -> f#(x1)
             d#(x1) -> e#(x1) -> e#(x1) -> b#(x1)
             d#(x1) -> e#(x1) -> e#(x1) -> b#(b(x1))
             d#(x1) -> c#(e(x1)) -> c#(c(x1)) -> b#(x1)
             d#(x1) -> c#(e(x1)) -> c#(c(x1)) -> d#(b(x1))
             d#(x1) -> c#(e(x1)) -> c#(b(x1)) -> g#(x1)
             b#(b(x1)) -> f#(x1) -> f#(g(x1)) -> a#(c(x1))
             c#(c(x1)) -> d#(b(x1)) -> d#(x1) -> e#(x1)
             c#(c(x1)) -> d#(b(x1)) -> d#(x1) -> c#(e(x1))
             c#(c(x1)) -> b#(x1) -> b#(b(x1)) -> f#(x1)
             c#(b(x1)) -> g#(x1) -> g#(f(x1)) -> e#(x1)
             a#(x1) -> b#(c(x1)) -> b#(b(x1)) -> f#(x1)
            SCC Processor:
             #sccs: 2
             #rules: 5
             #arcs: 19/144
             DPs:
              d#(x1) -> c#(e(x1))
              c#(c(x1)) -> d#(b(x1))
             TRS:
              a(b(x1)) -> c(b(x1))
              c(c(x1)) -> d(b(x1))
              d(x1) -> c(e(x1))
              b(b(x1)) -> f(x1)
              c(b(x1)) -> g(x1)
              e(x1) -> f(x1)
              e(x1) -> b(b(x1))
              f(g(x1)) -> a(c(x1))
              g(f(x1)) -> e(x1)
              a(x1) -> b(c(x1))
             Arctic Interpretation Processor:
              dimension: 3
              usable rules:
               a(b(x1)) -> c(b(x1))
               c(c(x1)) -> d(b(x1))
               d(x1) -> c(e(x1))
               b(b(x1)) -> f(x1)
               c(b(x1)) -> g(x1)
               e(x1) -> f(x1)
               e(x1) -> b(b(x1))
               f(g(x1)) -> a(c(x1))
               g(f(x1)) -> e(x1)
               a(x1) -> b(c(x1))
              interpretation:
               [d#](x0) = [0 0 1]x0 + [0],
               
               [c#](x0) = [0 1 0]x0 + [0],
               
                         [0  -& 0 ]     [0 ]
               [g](x0) = [0  -& -&]x0 + [-&]
                         [1  -& 1 ]     [1 ],
               
                         [0  -& 0 ]  
               [f](x0) = [-& -& 0 ]x0
                         [-& -& 0 ]  ,
               
                         [0  -& 0 ]     [0 ]
               [e](x0) = [-& -& 0 ]x0 + [-&]
                         [0  -& 0 ]     [0 ],
               
                         [0 0 0]     [1]
               [d](x0) = [1 1 1]x0 + [1]
                         [1 1 1]     [1],
               
                         [0  -& 0 ]     [-&]
               [c](x0) = [0  0  1 ]x0 + [0 ]
                         [1  -& 0 ]     [1 ],
               
                         [1  -& 0 ]     [1]
               [a](x0) = [1  -& 0 ]x0 + [1]
                         [1  -& 0 ]     [1],
               
                         [0  -& 0 ]     [0 ]
               [b](x0) = [-& -& 0 ]x0 + [-&]
                         [-& -& 0 ]     [-&]
              orientation:
               d#(x1) = [0 0 1]x1 + [0] >= [0  -& 1 ]x1 + [0] = c#(e(x1))
               
               c#(c(x1)) = [1 1 2]x1 + [1] >= [0  -& 1 ]x1 + [0] = d#(b(x1))
               
                          [1  -& 1 ]     [1]    [0  -& 0 ]     [0]           
               a(b(x1)) = [1  -& 1 ]x1 + [1] >= [0  -& 1 ]x1 + [0] = c(b(x1))
                          [1  -& 1 ]     [1]    [1  -& 1 ]     [1]           
               
                          [1  -& 0 ]     [1]    [0  -& 0 ]     [1]           
               c(c(x1)) = [2  0  1 ]x1 + [2] >= [1  -& 1 ]x1 + [1] = d(b(x1))
                          [1  -& 1 ]     [1]    [1  -& 1 ]     [1]           
               
                       [0 0 0]     [1]    [0  -& 0 ]     [0]           
               d(x1) = [1 1 1]x1 + [1] >= [1  -& 1 ]x1 + [1] = c(e(x1))
                       [1 1 1]     [1]    [1  -& 1 ]     [1]           
               
                          [0  -& 0 ]     [0 ]    [0  -& 0 ]          
               b(b(x1)) = [-& -& 0 ]x1 + [-&] >= [-& -& 0 ]x1 = f(x1)
                          [-& -& 0 ]     [-&]    [-& -& 0 ]          
               
                          [0  -& 0 ]     [0]    [0  -& 0 ]     [0 ]        
               c(b(x1)) = [0  -& 1 ]x1 + [0] >= [0  -& -&]x1 + [-&] = g(x1)
                          [1  -& 1 ]     [1]    [1  -& 1 ]     [1 ]        
               
                       [0  -& 0 ]     [0 ]    [0  -& 0 ]          
               e(x1) = [-& -& 0 ]x1 + [-&] >= [-& -& 0 ]x1 = f(x1)
                       [0  -& 0 ]     [0 ]    [-& -& 0 ]          
               
                       [0  -& 0 ]     [0 ]    [0  -& 0 ]     [0 ]           
               e(x1) = [-& -& 0 ]x1 + [-&] >= [-& -& 0 ]x1 + [-&] = b(b(x1))
                       [0  -& 0 ]     [0 ]    [-& -& 0 ]     [-&]           
               
                          [1  -& 1 ]     [1]    [1  -& 1 ]     [1]           
               f(g(x1)) = [1  -& 1 ]x1 + [1] >= [1  -& 1 ]x1 + [1] = a(c(x1))
                          [1  -& 1 ]     [1]    [1  -& 1 ]     [1]           
               
                          [0  -& 0 ]     [0 ]    [0  -& 0 ]     [0 ]        
               g(f(x1)) = [0  -& 0 ]x1 + [-&] >= [-& -& 0 ]x1 + [-&] = e(x1)
                          [1  -& 1 ]     [1 ]    [0  -& 0 ]     [0 ]        
               
                       [1  -& 0 ]     [1]    [1  -& 0 ]     [1]           
               a(x1) = [1  -& 0 ]x1 + [1] >= [1  -& 0 ]x1 + [1] = b(c(x1))
                       [1  -& 0 ]     [1]    [1  -& 0 ]     [1]           
              problem:
               DPs:
                d#(x1) -> c#(e(x1))
               TRS:
                a(b(x1)) -> c(b(x1))
                c(c(x1)) -> d(b(x1))
                d(x1) -> c(e(x1))
                b(b(x1)) -> f(x1)
                c(b(x1)) -> g(x1)
                e(x1) -> f(x1)
                e(x1) -> b(b(x1))
                f(g(x1)) -> a(c(x1))
                g(f(x1)) -> e(x1)
                a(x1) -> b(c(x1))
              Restore Modifier:
               DPs:
                d#(x1) -> c#(e(x1))
               TRS:
                a(b(x1)) -> c(b(x1))
                c(c(x1)) -> d(b(x1))
                d(x1) -> c(e(x1))
                b(b(x1)) -> f(x1)
                c(b(x1)) -> g(x1)
                e(x1) -> f(x1)
                e(x1) -> b(b(x1))
                f(g(x1)) -> a(c(x1))
                g(f(x1)) -> e(x1)
                a(x1) -> b(c(x1))
               EDG Processor:
                DPs:
                 d#(x1) -> c#(e(x1))
                TRS:
                 a(b(x1)) -> c(b(x1))
                 c(c(x1)) -> d(b(x1))
                 d(x1) -> c(e(x1))
                 b(b(x1)) -> f(x1)
                 c(b(x1)) -> g(x1)
                 e(x1) -> f(x1)
                 e(x1) -> b(b(x1))
                 f(g(x1)) -> a(c(x1))
                 g(f(x1)) -> e(x1)
                 a(x1) -> b(c(x1))
                graph:
                 
                Qed
             
             DPs:
              b#(b(x1)) -> f#(x1)
              f#(g(x1)) -> a#(c(x1))
              a#(x1) -> b#(c(x1))
             TRS:
              a(b(x1)) -> c(b(x1))
              c(c(x1)) -> d(b(x1))
              d(x1) -> c(e(x1))
              b(b(x1)) -> f(x1)
              c(b(x1)) -> g(x1)
              e(x1) -> f(x1)
              e(x1) -> b(b(x1))
              f(g(x1)) -> a(c(x1))
              g(f(x1)) -> e(x1)
              a(x1) -> b(c(x1))
             Arctic Interpretation Processor:
              dimension: 4
              usable rules:
               a(b(x1)) -> c(b(x1))
               c(c(x1)) -> d(b(x1))
               d(x1) -> c(e(x1))
               b(b(x1)) -> f(x1)
               c(b(x1)) -> g(x1)
               e(x1) -> f(x1)
               e(x1) -> b(b(x1))
               f(g(x1)) -> a(c(x1))
               g(f(x1)) -> e(x1)
               a(x1) -> b(c(x1))
              interpretation:
               [f#](x0) = [0 0 0 0]x0 + [0],
               
               [b#](x0) = [1  0  0  -&]x0 + [0],
               
               [a#](x0) = [1 1 0 1]x0 + [1],
               
                         [0  0  0  0 ]     [0]
                         [-& 0  0  0 ]     [0]
               [g](x0) = [1  1  1  1 ]x0 + [1]
                         [0  0  0  0 ]     [0],
               
                         [0 0 0 0]  
                         [0 0 0 0]  
               [f](x0) = [0 0 0 0]x0
                         [0 0 0 0]  ,
               
                         [0 0 0 0]     [0]
                         [0 0 0 0]     [0]
               [e](x0) = [0 0 0 0]x0 + [0]
                         [0 0 0 0]     [0],
               
                         [0 0 0 0]     [0]
                         [0 0 0 0]     [0]
               [d](x0) = [1 1 1 1]x0 + [1]
                         [0 0 0 0]     [0],
               
                         [0  0  -& 0 ]     [-&]
                         [0  0  0  0 ]     [-&]
               [c](x0) = [1  0  0  1 ]x0 + [1 ]
                         [-& 0  0  0 ]     [0 ],
               
                         [1 1 0 1]     [1]
                         [1 0 0 1]     [1]
               [a](x0) = [1 0 0 1]x0 + [1]
                         [1 1 0 1]     [1],
               
                         [0  0  0  0 ]     [0 ]
                         [0  0  0  0 ]     [0 ]
               [b](x0) = [0  0  0  0 ]x0 + [0 ]
                         [-& 0  0  0 ]     [-&]
              orientation:
               b#(b(x1)) = [1 1 1 1]x1 + [1] >= [0 0 0 0]x1 + [0] = f#(x1)
               
               f#(g(x1)) = [1 1 1 1]x1 + [1] >= [1 1 1 1]x1 + [1] = a#(c(x1))
               
               a#(x1) = [1 1 0 1]x1 + [1] >= [1 1 0 1]x1 + [1] = b#(c(x1))
               
                          [1 1 1 1]     [1]    [0 0 0 0]     [0]           
                          [1 1 1 1]     [1]    [0 0 0 0]     [0]           
               a(b(x1)) = [1 1 1 1]x1 + [1] >= [1 1 1 1]x1 + [1] = c(b(x1))
                          [1 1 1 1]     [1]    [0 0 0 0]     [0]           
               
                          [0 0 0 0]     [0]    [0 0 0 0]     [0]           
                          [1 0 0 1]     [1]    [0 0 0 0]     [0]           
               c(c(x1)) = [1 1 1 1]x1 + [1] >= [1 1 1 1]x1 + [1] = d(b(x1))
                          [1 0 0 1]     [1]    [0 0 0 0]     [0]           
               
                       [0 0 0 0]     [0]    [0 0 0 0]     [0]           
                       [0 0 0 0]     [0]    [0 0 0 0]     [0]           
               d(x1) = [1 1 1 1]x1 + [1] >= [1 1 1 1]x1 + [1] = c(e(x1))
                       [0 0 0 0]     [0]    [0 0 0 0]     [0]           
               
                          [0 0 0 0]     [0]    [0 0 0 0]          
                          [0 0 0 0]     [0]    [0 0 0 0]          
               b(b(x1)) = [0 0 0 0]x1 + [0] >= [0 0 0 0]x1 = f(x1)
                          [0 0 0 0]     [0]    [0 0 0 0]          
               
                          [0 0 0 0]     [0]    [0  0  0  0 ]     [0]        
                          [0 0 0 0]     [0]    [-& 0  0  0 ]     [0]        
               c(b(x1)) = [1 1 1 1]x1 + [1] >= [1  1  1  1 ]x1 + [1] = g(x1)
                          [0 0 0 0]     [0]    [0  0  0  0 ]     [0]        
               
                       [0 0 0 0]     [0]    [0 0 0 0]          
                       [0 0 0 0]     [0]    [0 0 0 0]          
               e(x1) = [0 0 0 0]x1 + [0] >= [0 0 0 0]x1 = f(x1)
                       [0 0 0 0]     [0]    [0 0 0 0]          
               
                       [0 0 0 0]     [0]    [0 0 0 0]     [0]           
                       [0 0 0 0]     [0]    [0 0 0 0]     [0]           
               e(x1) = [0 0 0 0]x1 + [0] >= [0 0 0 0]x1 + [0] = b(b(x1))
                       [0 0 0 0]     [0]    [0 0 0 0]     [0]           
               
                          [1 1 1 1]     [1]    [1 1 1 1]     [1]           
                          [1 1 1 1]     [1]    [1 1 1 1]     [1]           
               f(g(x1)) = [1 1 1 1]x1 + [1] >= [1 1 1 1]x1 + [1] = a(c(x1))
                          [1 1 1 1]     [1]    [1 1 1 1]     [1]           
               
                          [0 0 0 0]     [0]    [0 0 0 0]     [0]        
                          [0 0 0 0]     [0]    [0 0 0 0]     [0]        
               g(f(x1)) = [1 1 1 1]x1 + [1] >= [0 0 0 0]x1 + [0] = e(x1)
                          [0 0 0 0]     [0]    [0 0 0 0]     [0]        
               
                       [1 1 0 1]     [1]    [1 0 0 1]     [1]           
                       [1 0 0 1]     [1]    [1 0 0 1]     [1]           
               a(x1) = [1 0 0 1]x1 + [1] >= [1 0 0 1]x1 + [1] = b(c(x1))
                       [1 1 0 1]     [1]    [1 0 0 1]     [1]           
              problem:
               DPs:
                f#(g(x1)) -> a#(c(x1))
                a#(x1) -> b#(c(x1))
               TRS:
                a(b(x1)) -> c(b(x1))
                c(c(x1)) -> d(b(x1))
                d(x1) -> c(e(x1))
                b(b(x1)) -> f(x1)
                c(b(x1)) -> g(x1)
                e(x1) -> f(x1)
                e(x1) -> b(b(x1))
                f(g(x1)) -> a(c(x1))
                g(f(x1)) -> e(x1)
                a(x1) -> b(c(x1))
              Restore Modifier:
               DPs:
                f#(g(x1)) -> a#(c(x1))
                a#(x1) -> b#(c(x1))
               TRS:
                a(b(x1)) -> c(b(x1))
                c(c(x1)) -> d(b(x1))
                d(x1) -> c(e(x1))
                b(b(x1)) -> f(x1)
                c(b(x1)) -> g(x1)
                e(x1) -> f(x1)
                e(x1) -> b(b(x1))
                f(g(x1)) -> a(c(x1))
                g(f(x1)) -> e(x1)
                a(x1) -> b(c(x1))
               EDG Processor:
                DPs:
                 f#(g(x1)) -> a#(c(x1))
                 a#(x1) -> b#(c(x1))
                TRS:
                 a(b(x1)) -> c(b(x1))
                 c(c(x1)) -> d(b(x1))
                 d(x1) -> c(e(x1))
                 b(b(x1)) -> f(x1)
                 c(b(x1)) -> g(x1)
                 e(x1) -> f(x1)
                 e(x1) -> b(b(x1))
                 f(g(x1)) -> a(c(x1))
                 g(f(x1)) -> e(x1)
                 a(x1) -> b(c(x1))
                graph:
                 f#(g(x1)) -> a#(c(x1)) -> a#(x1) -> b#(c(x1))
                SCC Processor:
                 #sccs: 0
                 #rules: 0
                 #arcs: 1/4