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
    interpretation:
     [g#](x0) = [0 0]x0 + [1],
     
     [f#](x0) = [0 0]x0 + [0],
     
     [e#](x0) = [0 0]x0 + [1],
     
     [d#](x0) = [0 0]x0 + [1],
     
     [b#](x0) = [0 0]x0 + [1],
     
     [c#](x0) = [0 0]x0 + [0],
     
     [a#](x0) = [1 0]x0 + [3],
     
               [0  -&]     [1]
     [g](x0) = [1  1 ]x0 + [3],
     
               [0 0]     [-&]
     [f](x0) = [0 0]x0 + [1 ],
     
               [0 0]     [1]
     [e](x0) = [0 0]x0 + [1],
     
               [0 0]     [2]
     [d](x0) = [1 1]x0 + [3],
     
               [0 0]     [2]
     [c](x0) = [1 0]x0 + [3],
     
               [1 0]     [3]
     [a](x0) = [1 0]x0 + [3],
     
               [0 0]     [0]
     [b](x0) = [0 0]x0 + [1]
    orientation:
     a#(b(x1)) = [1 1]x1 + [3] >= [0 0]x1 + [1] = c#(b(x1))
     
     c#(c(x1)) = [1 0]x1 + [3] >= [0 0]x1 + [1] = b#(x1)
     
     c#(c(x1)) = [1 0]x1 + [3] >= [0 0]x1 + [1] = d#(b(x1))
     
     d#(x1) = [0 0]x1 + [1] >= [0 0]x1 + [1] = e#(x1)
     
     d#(x1) = [0 0]x1 + [1] >= [0 0]x1 + [1] = c#(e(x1))
     
     b#(b(x1)) = [0 0]x1 + [1] >= [0 0]x1 + [0] = f#(x1)
     
     c#(b(x1)) = [0 0]x1 + [1] >= [0 0]x1 + [1] = g#(x1)
     
     e#(x1) = [0 0]x1 + [1] >= [0 0]x1 + [0] = f#(x1)
     
     e#(x1) = [0 0]x1 + [1] >= [0 0]x1 + [1] = b#(x1)
     
     e#(x1) = [0 0]x1 + [1] >= [0 0]x1 + [1] = b#(b(x1))
     
     f#(g(x1)) = [1 1]x1 + [3] >= [0 0]x1 + [0] = c#(x1)
     
     f#(g(x1)) = [1 1]x1 + [3] >= [1 1]x1 + [3] = a#(c(x1))
     
     g#(f(x1)) = [0 0]x1 + [1] >= [0 0]x1 + [1] = e#(x1)
     
     a#(x1) = [1 0]x1 + [3] >= [0 0]x1 + [0] = c#(x1)
     
     a#(x1) = [1 0]x1 + [3] >= [1 0]x1 + [3] = b#(c(x1))
     
                [1 1]     [3]    [0 0]     [2]           
     a(b(x1)) = [1 1]x1 + [3] >= [1 1]x1 + [3] = c(b(x1))
     
                [1 0]     [3]    [0 0]     [2]           
     c(c(x1)) = [1 1]x1 + [3] >= [1 1]x1 + [3] = d(b(x1))
     
             [0 0]     [2]    [0 0]     [2]           
     d(x1) = [1 1]x1 + [3] >= [1 1]x1 + [3] = c(e(x1))
     
                [0 0]     [1]    [0 0]     [-&]        
     b(b(x1)) = [0 0]x1 + [1] >= [0 0]x1 + [1 ] = f(x1)
     
                [0 0]     [2]    [0  -&]     [1]        
     c(b(x1)) = [1 1]x1 + [3] >= [1  1 ]x1 + [3] = g(x1)
     
             [0 0]     [1]    [0 0]     [-&]        
     e(x1) = [0 0]x1 + [1] >= [0 0]x1 + [1 ] = f(x1)
     
             [0 0]     [1]    [0 0]     [1]           
     e(x1) = [0 0]x1 + [1] >= [0 0]x1 + [1] = b(b(x1))
     
                [1 1]     [3]    [1 1]     [3]           
     f(g(x1)) = [1 1]x1 + [3] >= [1 1]x1 + [3] = a(c(x1))
     
                [0 0]     [1]    [0 0]     [1]        
     g(f(x1)) = [1 1]x1 + [3] >= [0 0]x1 + [1] = e(x1)
     
             [1 0]     [3]    [1 0]     [3]           
     a(x1) = [1 0]x1 + [3] >= [1 0]x1 + [3] = 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))
    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) -> 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) -> 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#(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
      interpretation:
       [g#](x0) = [2 2]x0 + [2],
       
       [f#](x0) = [0 0]x0,
       
       [e#](x0) = [0 2]x0 + [0],
       
       [d#](x0) = [2 2]x0 + [2],
       
       [b#](x0) = [0 0]x0 + [0],
       
       [c#](x0) = [0 2]x0,
       
       [a#](x0) = [0 2]x0 + [0],
       
                 [2 2]     [2]
       [g](x0) = [0 0]x0 + [0],
       
                 [0  -&]     [0]
       [f](x0) = [0  0 ]x0 + [0],
       
                 [0  -&]     [0]
       [e](x0) = [0  0 ]x0 + [0],
       
                 [2 2]     [2]
       [d](x0) = [0 0]x0 + [0],
       
                 [0 2]     [-&]
       [c](x0) = [0 0]x0 + [0 ],
       
                 [0 2]     [0]
       [a](x0) = [0 2]x0 + [2],
       
                 [0  -&]     [0]
       [b](x0) = [0  0 ]x0 + [0]
      orientation:
       c#(c(x1)) = [2 2]x1 + [2] >= [0 0]x1 + [0] = b#(x1)
       
       c#(c(x1)) = [2 2]x1 + [2] >= [2 2]x1 + [2] = d#(b(x1))
       
       d#(x1) = [2 2]x1 + [2] >= [0 2]x1 + [0] = e#(x1)
       
       d#(x1) = [2 2]x1 + [2] >= [2 2]x1 + [2] = c#(e(x1))
       
       b#(b(x1)) = [0 0]x1 + [0] >= [0 0]x1 = f#(x1)
       
       c#(b(x1)) = [2 2]x1 + [2] >= [2 2]x1 + [2] = g#(x1)
       
       e#(x1) = [0 2]x1 + [0] >= [0 0]x1 = f#(x1)
       
       e#(x1) = [0 2]x1 + [0] >= [0 0]x1 + [0] = b#(x1)
       
       e#(x1) = [0 2]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)) = [2 2]x1 + [2] >= [0 2]x1 + [0] = e#(x1)
       
       a#(x1) = [0 2]x1 + [0] >= [0 2]x1 = c#(x1)
       
       a#(x1) = [0 2]x1 + [0] >= [0 2]x1 + [0] = b#(c(x1))
       
                  [2 2]     [2]    [2 2]     [2]           
       a(b(x1)) = [2 2]x1 + [2] >= [0 0]x1 + [0] = c(b(x1))
       
                  [2 2]     [2]    [2 2]     [2]           
       c(c(x1)) = [0 2]x1 + [0] >= [0 0]x1 + [0] = d(b(x1))
       
               [2 2]     [2]    [2 2]     [2]           
       d(x1) = [0 0]x1 + [0] >= [0 0]x1 + [0] = c(e(x1))
       
                  [0  -&]     [0]    [0  -&]     [0]        
       b(b(x1)) = [0  0 ]x1 + [0] >= [0  0 ]x1 + [0] = f(x1)
       
                  [2 2]     [2]    [2 2]     [2]        
       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 + [0] = f(x1)
       
               [0  -&]     [0]    [0  -&]     [0]           
       e(x1) = [0  0 ]x1 + [0] >= [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))
       
                  [2 2]     [2]    [0  -&]     [0]        
       g(f(x1)) = [0 0]x1 + [0] >= [0  0 ]x1 + [0] = e(x1)
       
               [0 2]     [0]    [0 2]     [0]           
       a(x1) = [0 2]x1 + [2] >= [0 2]x1 + [0] = b(c(x1))
      problem:
       DPs:
        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)) -> 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))
        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#(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))
       Arctic Interpretation Processor:
        dimension: 2
        interpretation:
         [g#](x0) = [0 0]x0,
         
         [f#](x0) = [0 0]x0,
         
         [e#](x0) = [0 0]x0,
         
         [d#](x0) = [1 1]x0,
         
         [b#](x0) = [0 0]x0,
         
         [c#](x0) = [0 1]x0,
         
         [a#](x0) = [0 1]x0 + [0],
         
                   [1  1 ]     [0 ]
         [g](x0) = [0  -&]x0 + [-&],
         
                   [0 0]  
         [f](x0) = [0 0]x0,
         
                   [0 0]  
         [e](x0) = [0 0]x0,
         
                   [1 1]     [0 ]
         [d](x0) = [0 0]x0 + [-&],
         
                   [0 1]     [0 ]
         [c](x0) = [0 0]x0 + [-&],
         
                   [0 1]     [0]
         [a](x0) = [0 1]x0 + [0],
         
                   [0 0]  
         [b](x0) = [0 0]x0
        orientation:
         c#(c(x1)) = [1 1]x1 + [0] >= [1 1]x1 = d#(b(x1))
         
         d#(x1) = [1 1]x1 >= [0 0]x1 = e#(x1)
         
         d#(x1) = [1 1]x1 >= [1 1]x1 = c#(e(x1))
         
         b#(b(x1)) = [0 0]x1 >= [0 0]x1 = f#(x1)
         
         c#(b(x1)) = [1 1]x1 >= [0 0]x1 = g#(x1)
         
         e#(x1) = [0 0]x1 >= [0 0]x1 = f#(x1)
         
         e#(x1) = [0 0]x1 >= [0 0]x1 = b#(x1)
         
         e#(x1) = [0 0]x1 >= [0 0]x1 = b#(b(x1))
         
         f#(g(x1)) = [1 1]x1 + [0] >= [1 1]x1 + [0] = a#(c(x1))
         
         g#(f(x1)) = [0 0]x1 >= [0 0]x1 = e#(x1)
         
         a#(x1) = [0 1]x1 + [0] >= [0 1]x1 = c#(x1)
         
         a#(x1) = [0 1]x1 + [0] >= [0 1]x1 + [0] = b#(c(x1))
         
                    [1 1]     [0]    [1 1]     [0 ]           
         a(b(x1)) = [1 1]x1 + [0] >= [0 0]x1 + [-&] = c(b(x1))
         
                    [1 1]     [0]    [1 1]     [0 ]           
         c(c(x1)) = [0 1]x1 + [0] >= [0 0]x1 + [-&] = d(b(x1))
         
                 [1 1]     [0 ]    [1 1]     [0 ]           
         d(x1) = [0 0]x1 + [-&] >= [0 0]x1 + [-&] = c(e(x1))
         
                    [0 0]      [0 0]          
         b(b(x1)) = [0 0]x1 >= [0 0]x1 = f(x1)
         
                    [1 1]     [0 ]    [1  1 ]     [0 ]        
         c(b(x1)) = [0 0]x1 + [-&] >= [0  -&]x1 + [-&] = g(x1)
         
                 [0 0]      [0 0]          
         e(x1) = [0 0]x1 >= [0 0]x1 = f(x1)
         
                 [0 0]      [0 0]             
         e(x1) = [0 0]x1 >= [0 0]x1 = b(b(x1))
         
                    [1 1]     [0]    [1 1]     [0]           
         f(g(x1)) = [1 1]x1 + [0] >= [1 1]x1 + [0] = a(c(x1))
         
                    [1 1]     [0 ]    [0 0]          
         g(f(x1)) = [0 0]x1 + [-&] >= [0 0]x1 = e(x1)
         
                 [0 1]     [0]    [0 1]     [0]           
         a(x1) = [0 1]x1 + [0] >= [0 1]x1 + [0] = b(c(x1))
        problem:
         DPs:
          c#(c(x1)) -> d#(b(x1))
          d#(x1) -> c#(e(x1))
          b#(b(x1)) -> f#(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)) -> d#(b(x1))
          d#(x1) -> c#(e(x1))
          b#(b(x1)) -> f#(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#(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) -> c#(e(x1)) -> c#(c(x1)) -> d#(b(x1))
          b#(b(x1)) -> f#(x1) -> f#(g(x1)) -> a#(c(x1))
          c#(c(x1)) -> d#(b(x1)) -> d#(x1) -> c#(e(x1))
          a#(x1) -> b#(c(x1)) -> b#(b(x1)) -> f#(x1)
          a#(x1) -> c#(x1) -> c#(c(x1)) -> d#(b(x1))
         SCC Processor:
          #sccs: 2
          #rules: 5
          #arcs: 13/100
          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: 3
           interpretation:
            [f#](x0) = [1  0  -&]x0,
            
            [b#](x0) = [-& -& 0 ]x0 + [0],
            
            [a#](x0) = [0 1 0]x0 + [1],
            
                      [1  0  0 ]     [1 ]
            [g](x0) = [-& 0  -&]x0 + [1 ]
                      [0  -& 0 ]     [-&],
            
                      [0  -& -&]     [-&]
            [f](x0) = [1  0  -&]x0 + [-&]
                      [1  -& 0 ]     [1 ],
            
                      [0  0  -&]     [0]
            [e](x0) = [1  0  -&]x0 + [1]
                      [1  -& 0 ]     [1],
            
                      [1  0  0 ]     [1]
            [d](x0) = [1  1  0 ]x0 + [1]
                      [1  0  -&]     [1],
            
                      [0  0  0 ]     [0]
            [c](x0) = [1  -& 0 ]x0 + [1]
                      [-& 0  -&]     [0],
            
                      [0 0 0]     [1]
            [a](x0) = [0 1 0]x0 + [1]
                      [1 1 1]     [1],
            
                      [0  -& -&]     [-&]
            [b](x0) = [0  -& 0 ]x0 + [0 ]
                      [1  0  -&]     [1 ]
           orientation:
            b#(b(x1)) = [1  0  -&]x1 + [1] >= [1  0  -&]x1 = f#(x1)
            
            f#(g(x1)) = [2 1 1]x1 + [2] >= [2 0 1]x1 + [2] = a#(c(x1))
            
            a#(x1) = [0 1 0]x1 + [1] >= [-& 0  -&]x1 + [0] = b#(c(x1))
            
                       [1 0 0]     [1]    [1  0  0 ]     [1]           
            a(b(x1)) = [1 0 1]x1 + [1] >= [1  0  -&]x1 + [1] = c(b(x1))
                       [2 1 1]     [2]    [0  -& 0 ]     [0]           
            
                       [1  0  0 ]     [1]    [1  0  0 ]     [1]           
            c(c(x1)) = [1  1  1 ]x1 + [1] >= [1  0  1 ]x1 + [1] = d(b(x1))
                       [1  -& 0 ]     [1]    [1  -& 0 ]     [1]           
            
                    [1  0  0 ]     [1]    [1  0  0 ]     [1]           
            d(x1) = [1  1  0 ]x1 + [1] >= [1  1  0 ]x1 + [1] = c(e(x1))
                    [1  0  -&]     [1]    [1  0  -&]     [1]           
            
                       [0  -& -&]     [-&]    [0  -& -&]     [-&]        
            b(b(x1)) = [1  0  -&]x1 + [1 ] >= [1  0  -&]x1 + [-&] = f(x1)
                       [1  -& 0 ]     [1 ]    [1  -& 0 ]     [1 ]        
            
                       [1  0  0 ]     [1]    [1  0  0 ]     [1 ]        
            c(b(x1)) = [1  0  -&]x1 + [1] >= [-& 0  -&]x1 + [1 ] = g(x1)
                       [0  -& 0 ]     [0]    [0  -& 0 ]     [-&]        
            
                    [0  0  -&]     [0]    [0  -& -&]     [-&]        
            e(x1) = [1  0  -&]x1 + [1] >= [1  0  -&]x1 + [-&] = f(x1)
                    [1  -& 0 ]     [1]    [1  -& 0 ]     [1 ]        
            
                    [0  0  -&]     [0]    [0  -& -&]     [-&]           
            e(x1) = [1  0  -&]x1 + [1] >= [1  0  -&]x1 + [1 ] = b(b(x1))
                    [1  -& 0 ]     [1]    [1  -& 0 ]     [1 ]           
            
                       [1 0 0]     [1]    [1 0 0]     [1]           
            f(g(x1)) = [2 1 1]x1 + [2] >= [2 0 1]x1 + [2] = a(c(x1))
                       [2 1 1]     [2]    [2 1 1]     [2]           
            
                       [1  0  0 ]     [1]    [0  0  -&]     [0]        
            g(f(x1)) = [1  0  -&]x1 + [1] >= [1  0  -&]x1 + [1] = e(x1)
                       [1  -& 0 ]     [1]    [1  -& 0 ]     [1]        
            
                    [0 0 0]     [1]    [0 0 0]     [0]           
            a(x1) = [0 1 0]x1 + [1] >= [0 0 0]x1 + [0] = b(c(x1))
                    [1 1 1]     [1]    [1 1 1]     [1]           
           problem:
            DPs:
             b#(b(x1)) -> f#(x1)
             f#(g(x1)) -> a#(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:
             b#(b(x1)) -> f#(x1)
             f#(g(x1)) -> a#(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:
             b#(b(x1)) -> f#(x1) -> f#(g(x1)) -> a#(c(x1))
            SCC Processor:
             #sccs: 0
             #rules: 0
             #arcs: 1/4
             
          
          DPs:
           c#(c(x1)) -> d#(b(x1))
           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))
          Arctic Interpretation Processor:
           dimension: 3
           interpretation:
            [d#](x0) = [0 0 0]x0 + [0],
            
            [c#](x0) = [0 0 0]x0 + [0],
            
                      [-& 1  -&]     [0 ]
            [g](x0) = [-& 1  1 ]x0 + [1 ]
                      [-& 0  0 ]     [-&],
            
                      [-& 0  0 ]     [0 ]
            [f](x0) = [-& 0  0 ]x0 + [-&]
                      [-& 0  0 ]     [0 ],
            
                      [-& 0  0 ]     [0]
            [e](x0) = [-& 0  0 ]x0 + [0]
                      [-& 0  0 ]     [0],
            
                      [0 1 1]     [1]
            [d](x0) = [1 1 1]x0 + [1]
                      [0 0 0]     [0],
            
                      [0  1  1 ]     [1 ]
            [c](x0) = [-& 0  1 ]x0 + [-&]
                      [-& 0  0 ]     [0 ],
            
                      [-& 0  1 ]     [0]
            [a](x0) = [-& 0  1 ]x0 + [0]
                      [-& 0  1 ]     [0],
            
                      [-& 0  0 ]     [0 ]
            [b](x0) = [-& 0  0 ]x0 + [-&]
                      [-& 0  0 ]     [0 ]
           orientation:
            c#(c(x1)) = [0 1 1]x1 + [1] >= [-& 0  0 ]x1 + [0] = d#(b(x1))
            
            d#(x1) = [0 0 0]x1 + [0] >= [-& 0  0 ]x1 + [0] = c#(e(x1))
            
                       [-& 1  1 ]     [1]    [-& 1  1 ]     [1]           
            a(b(x1)) = [-& 1  1 ]x1 + [1] >= [-& 1  1 ]x1 + [1] = c(b(x1))
                       [-& 1  1 ]     [1]    [-& 0  0 ]     [0]           
            
                       [0  1  2 ]     [1]    [-& 1  1 ]     [1]           
            c(c(x1)) = [-& 1  1 ]x1 + [1] >= [-& 1  1 ]x1 + [1] = d(b(x1))
                       [-& 0  1 ]     [0]    [-& 0  0 ]     [0]           
            
                    [0 1 1]     [1]    [-& 1  1 ]     [1]           
            d(x1) = [1 1 1]x1 + [1] >= [-& 1  1 ]x1 + [1] = c(e(x1))
                    [0 0 0]     [0]    [-& 0  0 ]     [0]           
            
                       [-& 0  0 ]     [0]    [-& 0  0 ]     [0 ]        
            b(b(x1)) = [-& 0  0 ]x1 + [0] >= [-& 0  0 ]x1 + [-&] = f(x1)
                       [-& 0  0 ]     [0]    [-& 0  0 ]     [0 ]        
            
                       [-& 1  1 ]     [1]    [-& 1  -&]     [0 ]        
            c(b(x1)) = [-& 1  1 ]x1 + [1] >= [-& 1  1 ]x1 + [1 ] = g(x1)
                       [-& 0  0 ]     [0]    [-& 0  0 ]     [-&]        
            
                    [-& 0  0 ]     [0]    [-& 0  0 ]     [0 ]        
            e(x1) = [-& 0  0 ]x1 + [0] >= [-& 0  0 ]x1 + [-&] = f(x1)
                    [-& 0  0 ]     [0]    [-& 0  0 ]     [0 ]        
            
                    [-& 0  0 ]     [0]    [-& 0  0 ]     [0]           
            e(x1) = [-& 0  0 ]x1 + [0] >= [-& 0  0 ]x1 + [0] = b(b(x1))
                    [-& 0  0 ]     [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]           
            
                       [-& 1  1 ]     [0]    [-& 0  0 ]     [0]        
            g(f(x1)) = [-& 1  1 ]x1 + [1] >= [-& 0  0 ]x1 + [0] = e(x1)
                       [-& 0  0 ]     [0]    [-& 0  0 ]     [0]        
            
                    [-& 0  1 ]     [0]    [-& 0  1 ]     [0]           
            a(x1) = [-& 0  1 ]x1 + [0] >= [-& 0  1 ]x1 + [0] = b(c(x1))
                    [-& 0  1 ]     [0]    [-& 0  1 ]     [0]           
           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))
           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