YES

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

Proof:
 DP Processor:
  DPs:
   b#(b(x1)) -> d#(x1)
   b#(b(x1)) -> c#(d(x1))
   c#(c(x1)) -> d#(x1)
   c#(c(x1)) -> d#(d(x1))
   c#(c(x1)) -> d#(d(d(x1)))
   c#(x1) -> g#(x1)
   d#(d(x1)) -> f#(x1)
   d#(d(x1)) -> c#(f(x1))
   d#(d(d(x1))) -> c#(x1)
   d#(d(d(x1))) -> g#(c(x1))
   f#(x1) -> g#(x1)
   g#(x1) -> b#(x1)
   g#(x1) -> d#(a(b(x1)))
   g#(g(x1)) -> c#(x1)
   g#(g(x1)) -> b#(c(x1))
  TRS:
   b(b(x1)) -> c(d(x1))
   c(c(x1)) -> d(d(d(x1)))
   c(x1) -> g(x1)
   d(d(x1)) -> c(f(x1))
   d(d(d(x1))) -> g(c(x1))
   f(x1) -> a(g(x1))
   g(x1) -> d(a(b(x1)))
   g(g(x1)) -> b(c(x1))
  TDG Processor:
   DPs:
    b#(b(x1)) -> d#(x1)
    b#(b(x1)) -> c#(d(x1))
    c#(c(x1)) -> d#(x1)
    c#(c(x1)) -> d#(d(x1))
    c#(c(x1)) -> d#(d(d(x1)))
    c#(x1) -> g#(x1)
    d#(d(x1)) -> f#(x1)
    d#(d(x1)) -> c#(f(x1))
    d#(d(d(x1))) -> c#(x1)
    d#(d(d(x1))) -> g#(c(x1))
    f#(x1) -> g#(x1)
    g#(x1) -> b#(x1)
    g#(x1) -> d#(a(b(x1)))
    g#(g(x1)) -> c#(x1)
    g#(g(x1)) -> b#(c(x1))
   TRS:
    b(b(x1)) -> c(d(x1))
    c(c(x1)) -> d(d(d(x1)))
    c(x1) -> g(x1)
    d(d(x1)) -> c(f(x1))
    d(d(d(x1))) -> g(c(x1))
    f(x1) -> a(g(x1))
    g(x1) -> d(a(b(x1)))
    g(g(x1)) -> b(c(x1))
   graph:
    f#(x1) -> g#(x1) -> g#(g(x1)) -> b#(c(x1))
    f#(x1) -> g#(x1) -> g#(g(x1)) -> c#(x1)
    f#(x1) -> g#(x1) -> g#(x1) -> d#(a(b(x1)))
    f#(x1) -> g#(x1) -> g#(x1) -> b#(x1)
    g#(g(x1)) -> c#(x1) -> c#(x1) -> g#(x1)
    g#(g(x1)) -> c#(x1) -> c#(c(x1)) -> d#(d(d(x1)))
    g#(g(x1)) -> c#(x1) -> c#(c(x1)) -> d#(d(x1))
    g#(g(x1)) -> c#(x1) -> c#(c(x1)) -> d#(x1)
    g#(g(x1)) -> b#(c(x1)) -> b#(b(x1)) -> c#(d(x1))
    g#(g(x1)) -> b#(c(x1)) -> b#(b(x1)) -> d#(x1)
    g#(x1) -> d#(a(b(x1))) -> d#(d(d(x1))) -> g#(c(x1))
    g#(x1) -> d#(a(b(x1))) -> d#(d(d(x1))) -> c#(x1)
    g#(x1) -> d#(a(b(x1))) -> d#(d(x1)) -> c#(f(x1))
    g#(x1) -> d#(a(b(x1))) -> d#(d(x1)) -> f#(x1)
    g#(x1) -> b#(x1) -> b#(b(x1)) -> c#(d(x1))
    g#(x1) -> b#(x1) -> b#(b(x1)) -> d#(x1)
    c#(c(x1)) -> d#(d(d(x1))) -> d#(d(d(x1))) -> g#(c(x1))
    c#(c(x1)) -> d#(d(d(x1))) -> d#(d(d(x1))) -> c#(x1)
    c#(c(x1)) -> d#(d(d(x1))) -> d#(d(x1)) -> c#(f(x1))
    c#(c(x1)) -> d#(d(d(x1))) -> d#(d(x1)) -> f#(x1)
    c#(c(x1)) -> d#(d(x1)) -> d#(d(d(x1))) -> g#(c(x1))
    c#(c(x1)) -> d#(d(x1)) -> d#(d(d(x1))) -> c#(x1)
    c#(c(x1)) -> d#(d(x1)) -> d#(d(x1)) -> c#(f(x1))
    c#(c(x1)) -> d#(d(x1)) -> d#(d(x1)) -> f#(x1)
    c#(c(x1)) -> d#(x1) -> d#(d(d(x1))) -> g#(c(x1))
    c#(c(x1)) -> d#(x1) -> d#(d(d(x1))) -> c#(x1)
    c#(c(x1)) -> d#(x1) -> d#(d(x1)) -> c#(f(x1))
    c#(c(x1)) -> d#(x1) -> d#(d(x1)) -> f#(x1)
    c#(x1) -> g#(x1) -> g#(g(x1)) -> b#(c(x1))
    c#(x1) -> g#(x1) -> g#(g(x1)) -> c#(x1)
    c#(x1) -> g#(x1) -> g#(x1) -> d#(a(b(x1)))
    c#(x1) -> g#(x1) -> g#(x1) -> b#(x1)
    d#(d(d(x1))) -> g#(c(x1)) -> g#(g(x1)) -> b#(c(x1))
    d#(d(d(x1))) -> g#(c(x1)) -> g#(g(x1)) -> c#(x1)
    d#(d(d(x1))) -> g#(c(x1)) -> g#(x1) -> d#(a(b(x1)))
    d#(d(d(x1))) -> g#(c(x1)) -> g#(x1) -> b#(x1)
    d#(d(d(x1))) -> c#(x1) -> c#(x1) -> g#(x1)
    d#(d(d(x1))) -> c#(x1) -> c#(c(x1)) -> d#(d(d(x1)))
    d#(d(d(x1))) -> c#(x1) -> c#(c(x1)) -> d#(d(x1))
    d#(d(d(x1))) -> c#(x1) -> c#(c(x1)) -> d#(x1)
    d#(d(x1)) -> f#(x1) -> f#(x1) -> g#(x1)
    d#(d(x1)) -> c#(f(x1)) -> c#(x1) -> g#(x1)
    d#(d(x1)) -> c#(f(x1)) -> c#(c(x1)) -> d#(d(d(x1)))
    d#(d(x1)) -> c#(f(x1)) -> c#(c(x1)) -> d#(d(x1))
    d#(d(x1)) -> c#(f(x1)) -> c#(c(x1)) -> d#(x1)
    b#(b(x1)) -> c#(d(x1)) -> c#(x1) -> g#(x1)
    b#(b(x1)) -> c#(d(x1)) -> c#(c(x1)) -> d#(d(d(x1)))
    b#(b(x1)) -> c#(d(x1)) -> c#(c(x1)) -> d#(d(x1))
    b#(b(x1)) -> c#(d(x1)) -> c#(c(x1)) -> d#(x1)
    b#(b(x1)) -> d#(x1) -> d#(d(d(x1))) -> g#(c(x1))
    b#(b(x1)) -> d#(x1) -> d#(d(d(x1))) -> c#(x1)
    b#(b(x1)) -> d#(x1) -> d#(d(x1)) -> c#(f(x1))
    b#(b(x1)) -> d#(x1) -> d#(d(x1)) -> f#(x1)
   EDG Processor:
    DPs:
     b#(b(x1)) -> d#(x1)
     b#(b(x1)) -> c#(d(x1))
     c#(c(x1)) -> d#(x1)
     c#(c(x1)) -> d#(d(x1))
     c#(c(x1)) -> d#(d(d(x1)))
     c#(x1) -> g#(x1)
     d#(d(x1)) -> f#(x1)
     d#(d(x1)) -> c#(f(x1))
     d#(d(d(x1))) -> c#(x1)
     d#(d(d(x1))) -> g#(c(x1))
     f#(x1) -> g#(x1)
     g#(x1) -> b#(x1)
     g#(x1) -> d#(a(b(x1)))
     g#(g(x1)) -> c#(x1)
     g#(g(x1)) -> b#(c(x1))
    TRS:
     b(b(x1)) -> c(d(x1))
     c(c(x1)) -> d(d(d(x1)))
     c(x1) -> g(x1)
     d(d(x1)) -> c(f(x1))
     d(d(d(x1))) -> g(c(x1))
     f(x1) -> a(g(x1))
     g(x1) -> d(a(b(x1)))
     g(g(x1)) -> b(c(x1))
    graph:
     f#(x1) -> g#(x1) -> g#(x1) -> b#(x1)
     f#(x1) -> g#(x1) -> g#(x1) -> d#(a(b(x1)))
     f#(x1) -> g#(x1) -> g#(g(x1)) -> c#(x1)
     f#(x1) -> g#(x1) -> g#(g(x1)) -> b#(c(x1))
     g#(g(x1)) -> c#(x1) -> c#(c(x1)) -> d#(x1)
     g#(g(x1)) -> c#(x1) -> c#(c(x1)) -> d#(d(x1))
     g#(g(x1)) -> c#(x1) -> c#(c(x1)) -> d#(d(d(x1)))
     g#(g(x1)) -> c#(x1) -> c#(x1) -> g#(x1)
     g#(g(x1)) -> b#(c(x1)) -> b#(b(x1)) -> d#(x1)
     g#(g(x1)) -> b#(c(x1)) -> b#(b(x1)) -> c#(d(x1))
     g#(x1) -> b#(x1) -> b#(b(x1)) -> d#(x1)
     g#(x1) -> b#(x1) -> b#(b(x1)) -> c#(d(x1))
     c#(c(x1)) -> d#(d(d(x1))) -> d#(d(x1)) -> f#(x1)
     c#(c(x1)) -> d#(d(d(x1))) -> d#(d(x1)) -> c#(f(x1))
     c#(c(x1)) -> d#(d(d(x1))) -> d#(d(d(x1))) -> c#(x1)
     c#(c(x1)) -> d#(d(d(x1))) -> d#(d(d(x1))) -> g#(c(x1))
     c#(c(x1)) -> d#(d(x1)) -> d#(d(x1)) -> f#(x1)
     c#(c(x1)) -> d#(d(x1)) -> d#(d(x1)) -> c#(f(x1))
     c#(c(x1)) -> d#(d(x1)) -> d#(d(d(x1))) -> c#(x1)
     c#(c(x1)) -> d#(d(x1)) -> d#(d(d(x1))) -> g#(c(x1))
     c#(c(x1)) -> d#(x1) -> d#(d(x1)) -> f#(x1)
     c#(c(x1)) -> d#(x1) -> d#(d(x1)) -> c#(f(x1))
     c#(c(x1)) -> d#(x1) -> d#(d(d(x1))) -> c#(x1)
     c#(c(x1)) -> d#(x1) -> d#(d(d(x1))) -> g#(c(x1))
     c#(x1) -> g#(x1) -> g#(x1) -> b#(x1)
     c#(x1) -> g#(x1) -> g#(x1) -> d#(a(b(x1)))
     c#(x1) -> g#(x1) -> g#(g(x1)) -> c#(x1)
     c#(x1) -> g#(x1) -> g#(g(x1)) -> b#(c(x1))
     d#(d(d(x1))) -> g#(c(x1)) -> g#(x1) -> b#(x1)
     d#(d(d(x1))) -> g#(c(x1)) -> g#(x1) -> d#(a(b(x1)))
     d#(d(d(x1))) -> g#(c(x1)) -> g#(g(x1)) -> c#(x1)
     d#(d(d(x1))) -> g#(c(x1)) -> g#(g(x1)) -> b#(c(x1))
     d#(d(d(x1))) -> c#(x1) -> c#(c(x1)) -> d#(x1)
     d#(d(d(x1))) -> c#(x1) -> c#(c(x1)) -> d#(d(x1))
     d#(d(d(x1))) -> c#(x1) -> c#(c(x1)) -> d#(d(d(x1)))
     d#(d(d(x1))) -> c#(x1) -> c#(x1) -> g#(x1)
     d#(d(x1)) -> f#(x1) -> f#(x1) -> g#(x1)
     d#(d(x1)) -> c#(f(x1)) -> c#(c(x1)) -> d#(x1)
     d#(d(x1)) -> c#(f(x1)) -> c#(c(x1)) -> d#(d(x1))
     d#(d(x1)) -> c#(f(x1)) -> c#(c(x1)) -> d#(d(d(x1)))
     d#(d(x1)) -> c#(f(x1)) -> c#(x1) -> g#(x1)
     b#(b(x1)) -> c#(d(x1)) -> c#(c(x1)) -> d#(x1)
     b#(b(x1)) -> c#(d(x1)) -> c#(c(x1)) -> d#(d(x1))
     b#(b(x1)) -> c#(d(x1)) -> c#(c(x1)) -> d#(d(d(x1)))
     b#(b(x1)) -> c#(d(x1)) -> c#(x1) -> g#(x1)
     b#(b(x1)) -> d#(x1) -> d#(d(x1)) -> f#(x1)
     b#(b(x1)) -> d#(x1) -> d#(d(x1)) -> c#(f(x1))
     b#(b(x1)) -> d#(x1) -> d#(d(d(x1))) -> c#(x1)
     b#(b(x1)) -> d#(x1) -> d#(d(d(x1))) -> g#(c(x1))
    SCC Processor:
     #sccs: 1
     #rules: 14
     #arcs: 49/225
     DPs:
      f#(x1) -> g#(x1)
      g#(g(x1)) -> b#(c(x1))
      b#(b(x1)) -> c#(d(x1))
      c#(x1) -> g#(x1)
      g#(g(x1)) -> c#(x1)
      c#(c(x1)) -> d#(d(d(x1)))
      d#(d(d(x1))) -> g#(c(x1))
      g#(x1) -> b#(x1)
      b#(b(x1)) -> d#(x1)
      d#(d(d(x1))) -> c#(x1)
      c#(c(x1)) -> d#(d(x1))
      d#(d(x1)) -> c#(f(x1))
      c#(c(x1)) -> d#(x1)
      d#(d(x1)) -> f#(x1)
     TRS:
      b(b(x1)) -> c(d(x1))
      c(c(x1)) -> d(d(d(x1)))
      c(x1) -> g(x1)
      d(d(x1)) -> c(f(x1))
      d(d(d(x1))) -> g(c(x1))
      f(x1) -> a(g(x1))
      g(x1) -> d(a(b(x1)))
      g(g(x1)) -> b(c(x1))
     Arctic Interpretation Processor:
      dimension: 1
      interpretation:
       [f#](x0) = x0,
       
       [g#](x0) = x0,
       
       [c#](x0) = x0 + 2,
       
       [d#](x0) = x0 + 0,
       
       [b#](x0) = x0,
       
       [a](x0) = 1,
       
       [f](x0) = 1,
       
       [g](x0) = x0 + 4,
       
       [c](x0) = x0 + 4,
       
       [d](x0) = x0 + 4,
       
       [b](x0) = x0 + 4
      orientation:
       f#(x1) = x1 >= x1 = g#(x1)
       
       g#(g(x1)) = x1 + 4 >= x1 + 4 = b#(c(x1))
       
       b#(b(x1)) = x1 + 4 >= x1 + 4 = c#(d(x1))
       
       c#(x1) = x1 + 2 >= x1 = g#(x1)
       
       g#(g(x1)) = x1 + 4 >= x1 + 2 = c#(x1)
       
       c#(c(x1)) = x1 + 4 >= x1 + 4 = d#(d(d(x1)))
       
       d#(d(d(x1))) = x1 + 4 >= x1 + 4 = g#(c(x1))
       
       g#(x1) = x1 >= x1 = b#(x1)
       
       b#(b(x1)) = x1 + 4 >= x1 + 0 = d#(x1)
       
       d#(d(d(x1))) = x1 + 4 >= x1 + 2 = c#(x1)
       
       c#(c(x1)) = x1 + 4 >= x1 + 4 = d#(d(x1))
       
       d#(d(x1)) = x1 + 4 >= 2 = c#(f(x1))
       
       c#(c(x1)) = x1 + 4 >= x1 + 0 = d#(x1)
       
       d#(d(x1)) = x1 + 4 >= x1 = f#(x1)
       
       b(b(x1)) = x1 + 4 >= x1 + 4 = c(d(x1))
       
       c(c(x1)) = x1 + 4 >= x1 + 4 = d(d(d(x1)))
       
       c(x1) = x1 + 4 >= x1 + 4 = g(x1)
       
       d(d(x1)) = x1 + 4 >= 4 = c(f(x1))
       
       d(d(d(x1))) = x1 + 4 >= x1 + 4 = g(c(x1))
       
       f(x1) = 1 >= 1 = a(g(x1))
       
       g(x1) = x1 + 4 >= 4 = d(a(b(x1)))
       
       g(g(x1)) = x1 + 4 >= x1 + 4 = b(c(x1))
      problem:
       DPs:
        f#(x1) -> g#(x1)
        g#(g(x1)) -> b#(c(x1))
        b#(b(x1)) -> c#(d(x1))
        c#(x1) -> g#(x1)
        g#(g(x1)) -> c#(x1)
        c#(c(x1)) -> d#(d(d(x1)))
        d#(d(d(x1))) -> g#(c(x1))
        g#(x1) -> b#(x1)
        b#(b(x1)) -> d#(x1)
        d#(d(d(x1))) -> c#(x1)
        c#(c(x1)) -> d#(d(x1))
        c#(c(x1)) -> d#(x1)
        d#(d(x1)) -> f#(x1)
       TRS:
        b(b(x1)) -> c(d(x1))
        c(c(x1)) -> d(d(d(x1)))
        c(x1) -> g(x1)
        d(d(x1)) -> c(f(x1))
        d(d(d(x1))) -> g(c(x1))
        f(x1) -> a(g(x1))
        g(x1) -> d(a(b(x1)))
        g(g(x1)) -> b(c(x1))
      EDG Processor:
       DPs:
        f#(x1) -> g#(x1)
        g#(g(x1)) -> b#(c(x1))
        b#(b(x1)) -> c#(d(x1))
        c#(x1) -> g#(x1)
        g#(g(x1)) -> c#(x1)
        c#(c(x1)) -> d#(d(d(x1)))
        d#(d(d(x1))) -> g#(c(x1))
        g#(x1) -> b#(x1)
        b#(b(x1)) -> d#(x1)
        d#(d(d(x1))) -> c#(x1)
        c#(c(x1)) -> d#(d(x1))
        c#(c(x1)) -> d#(x1)
        d#(d(x1)) -> f#(x1)
       TRS:
        b(b(x1)) -> c(d(x1))
        c(c(x1)) -> d(d(d(x1)))
        c(x1) -> g(x1)
        d(d(x1)) -> c(f(x1))
        d(d(d(x1))) -> g(c(x1))
        f(x1) -> a(g(x1))
        g(x1) -> d(a(b(x1)))
        g(g(x1)) -> b(c(x1))
       graph:
        f#(x1) -> g#(x1) -> g#(g(x1)) -> b#(c(x1))
        f#(x1) -> g#(x1) -> g#(g(x1)) -> c#(x1)
        f#(x1) -> g#(x1) -> g#(x1) -> b#(x1)
        g#(g(x1)) -> c#(x1) -> c#(x1) -> g#(x1)
        g#(g(x1)) -> c#(x1) -> c#(c(x1)) -> d#(d(d(x1)))
        g#(g(x1)) -> c#(x1) -> c#(c(x1)) -> d#(d(x1))
        g#(g(x1)) -> c#(x1) -> c#(c(x1)) -> d#(x1)
        g#(g(x1)) -> b#(c(x1)) -> b#(b(x1)) -> c#(d(x1))
        g#(g(x1)) -> b#(c(x1)) -> b#(b(x1)) -> d#(x1)
        g#(x1) -> b#(x1) -> b#(b(x1)) -> c#(d(x1))
        g#(x1) -> b#(x1) -> b#(b(x1)) -> d#(x1)
        c#(c(x1)) -> d#(d(d(x1))) -> d#(d(d(x1))) -> g#(c(x1))
        c#(c(x1)) -> d#(d(d(x1))) -> d#(d(d(x1))) -> c#(x1)
        c#(c(x1)) -> d#(d(d(x1))) -> d#(d(x1)) -> f#(x1)
        c#(c(x1)) -> d#(d(x1)) -> d#(d(d(x1))) -> g#(c(x1))
        c#(c(x1)) -> d#(d(x1)) -> d#(d(d(x1))) -> c#(x1)
        c#(c(x1)) -> d#(d(x1)) -> d#(d(x1)) -> f#(x1)
        c#(c(x1)) -> d#(x1) -> d#(d(d(x1))) -> g#(c(x1))
        c#(c(x1)) -> d#(x1) -> d#(d(d(x1))) -> c#(x1)
        c#(c(x1)) -> d#(x1) -> d#(d(x1)) -> f#(x1)
        c#(x1) -> g#(x1) -> g#(g(x1)) -> b#(c(x1))
        c#(x1) -> g#(x1) -> g#(g(x1)) -> c#(x1)
        c#(x1) -> g#(x1) -> g#(x1) -> b#(x1)
        d#(d(d(x1))) -> g#(c(x1)) -> g#(g(x1)) -> b#(c(x1))
        d#(d(d(x1))) -> g#(c(x1)) -> g#(g(x1)) -> c#(x1)
        d#(d(d(x1))) -> g#(c(x1)) -> g#(x1) -> b#(x1)
        d#(d(d(x1))) -> c#(x1) -> c#(x1) -> g#(x1)
        d#(d(d(x1))) -> c#(x1) -> c#(c(x1)) -> d#(d(d(x1)))
        d#(d(d(x1))) -> c#(x1) -> c#(c(x1)) -> d#(d(x1))
        d#(d(d(x1))) -> c#(x1) -> c#(c(x1)) -> d#(x1)
        d#(d(x1)) -> f#(x1) -> f#(x1) -> g#(x1)
        b#(b(x1)) -> c#(d(x1)) -> c#(x1) -> g#(x1)
        b#(b(x1)) -> c#(d(x1)) -> c#(c(x1)) -> d#(d(d(x1)))
        b#(b(x1)) -> c#(d(x1)) -> c#(c(x1)) -> d#(d(x1))
        b#(b(x1)) -> c#(d(x1)) -> c#(c(x1)) -> d#(x1)
        b#(b(x1)) -> d#(x1) -> d#(d(d(x1))) -> g#(c(x1))
        b#(b(x1)) -> d#(x1) -> d#(d(d(x1))) -> c#(x1)
        b#(b(x1)) -> d#(x1) -> d#(d(x1)) -> f#(x1)
       Arctic Interpretation Processor:
        dimension: 1
        interpretation:
         [f#](x0) = -3x0 + 4,
         
         [g#](x0) = -4x0 + 0,
         
         [c#](x0) = -3x0 + 3,
         
         [d#](x0) = -5x0 + 4,
         
         [b#](x0) = -4x0 + 0,
         
         [a](x0) = -14x0 + 5,
         
         [f](x0) = x0 + 5,
         
         [g](x0) = 3x0 + 7,
         
         [c](x0) = 3x0 + 7,
         
         [d](x0) = 2x0 + 6,
         
         [b](x0) = 3x0 + 9
        orientation:
         f#(x1) = -3x1 + 4 >= -4x1 + 0 = g#(x1)
         
         g#(g(x1)) = -1x1 + 3 >= -1x1 + 3 = b#(c(x1))
         
         b#(b(x1)) = -1x1 + 5 >= -1x1 + 3 = c#(d(x1))
         
         c#(x1) = -3x1 + 3 >= -4x1 + 0 = g#(x1)
         
         g#(g(x1)) = -1x1 + 3 >= -3x1 + 3 = c#(x1)
         
         c#(c(x1)) = x1 + 4 >= -1x1 + 4 = d#(d(d(x1)))
         
         d#(d(d(x1))) = -1x1 + 4 >= -1x1 + 3 = g#(c(x1))
         
         g#(x1) = -4x1 + 0 >= -4x1 + 0 = b#(x1)
         
         b#(b(x1)) = -1x1 + 5 >= -5x1 + 4 = d#(x1)
         
         d#(d(d(x1))) = -1x1 + 4 >= -3x1 + 3 = c#(x1)
         
         c#(c(x1)) = x1 + 4 >= -3x1 + 4 = d#(d(x1))
         
         c#(c(x1)) = x1 + 4 >= -5x1 + 4 = d#(x1)
         
         d#(d(x1)) = -3x1 + 4 >= -3x1 + 4 = f#(x1)
         
         b(b(x1)) = 6x1 + 12 >= 5x1 + 9 = c(d(x1))
         
         c(c(x1)) = 6x1 + 10 >= 6x1 + 10 = d(d(d(x1)))
         
         c(x1) = 3x1 + 7 >= 3x1 + 7 = g(x1)
         
         d(d(x1)) = 4x1 + 8 >= 3x1 + 8 = c(f(x1))
         
         d(d(d(x1))) = 6x1 + 10 >= 6x1 + 10 = g(c(x1))
         
         f(x1) = x1 + 5 >= -11x1 + 5 = a(g(x1))
         
         g(x1) = 3x1 + 7 >= -9x1 + 7 = d(a(b(x1)))
         
         g(g(x1)) = 6x1 + 10 >= 6x1 + 10 = b(c(x1))
        problem:
         DPs:
          g#(g(x1)) -> b#(c(x1))
          b#(b(x1)) -> c#(d(x1))
          g#(g(x1)) -> c#(x1)
          c#(c(x1)) -> d#(d(d(x1)))
          d#(d(d(x1))) -> g#(c(x1))
          g#(x1) -> b#(x1)
          c#(c(x1)) -> d#(d(x1))
          c#(c(x1)) -> d#(x1)
          d#(d(x1)) -> f#(x1)
         TRS:
          b(b(x1)) -> c(d(x1))
          c(c(x1)) -> d(d(d(x1)))
          c(x1) -> g(x1)
          d(d(x1)) -> c(f(x1))
          d(d(d(x1))) -> g(c(x1))
          f(x1) -> a(g(x1))
          g(x1) -> d(a(b(x1)))
          g(g(x1)) -> b(c(x1))
        EDG Processor:
         DPs:
          g#(g(x1)) -> b#(c(x1))
          b#(b(x1)) -> c#(d(x1))
          g#(g(x1)) -> c#(x1)
          c#(c(x1)) -> d#(d(d(x1)))
          d#(d(d(x1))) -> g#(c(x1))
          g#(x1) -> b#(x1)
          c#(c(x1)) -> d#(d(x1))
          c#(c(x1)) -> d#(x1)
          d#(d(x1)) -> f#(x1)
         TRS:
          b(b(x1)) -> c(d(x1))
          c(c(x1)) -> d(d(d(x1)))
          c(x1) -> g(x1)
          d(d(x1)) -> c(f(x1))
          d(d(d(x1))) -> g(c(x1))
          f(x1) -> a(g(x1))
          g(x1) -> d(a(b(x1)))
          g(g(x1)) -> b(c(x1))
         graph:
          g#(g(x1)) -> c#(x1) -> c#(c(x1)) -> d#(x1)
          g#(g(x1)) -> c#(x1) -> c#(c(x1)) -> d#(d(x1))
          g#(g(x1)) -> c#(x1) -> c#(c(x1)) -> d#(d(d(x1)))
          g#(g(x1)) -> b#(c(x1)) -> b#(b(x1)) -> c#(d(x1))
          g#(x1) -> b#(x1) -> b#(b(x1)) -> c#(d(x1))
          c#(c(x1)) -> d#(d(d(x1))) -> d#(d(x1)) -> f#(x1)
          c#(c(x1)) -> d#(d(d(x1))) -> d#(d(d(x1))) -> g#(c(x1))
          c#(c(x1)) -> d#(d(x1)) -> d#(d(x1)) -> f#(x1)
          c#(c(x1)) -> d#(d(x1)) -> d#(d(d(x1))) -> g#(c(x1))
          c#(c(x1)) -> d#(x1) -> d#(d(x1)) -> f#(x1)
          c#(c(x1)) -> d#(x1) -> d#(d(d(x1))) -> g#(c(x1))
          d#(d(d(x1))) -> g#(c(x1)) -> g#(x1) -> b#(x1)
          d#(d(d(x1))) -> g#(c(x1)) -> g#(g(x1)) -> c#(x1)
          d#(d(d(x1))) -> g#(c(x1)) -> g#(g(x1)) -> b#(c(x1))
          b#(b(x1)) -> c#(d(x1)) -> c#(c(x1)) -> d#(x1)
          b#(b(x1)) -> c#(d(x1)) -> c#(c(x1)) -> d#(d(x1))
          b#(b(x1)) -> c#(d(x1)) -> c#(c(x1)) -> d#(d(d(x1)))
         SCC Processor:
          #sccs: 1
          #rules: 8
          #arcs: 17/81
          DPs:
           g#(g(x1)) -> c#(x1)
           c#(c(x1)) -> d#(d(d(x1)))
           d#(d(d(x1))) -> g#(c(x1))
           g#(g(x1)) -> b#(c(x1))
           b#(b(x1)) -> c#(d(x1))
           c#(c(x1)) -> d#(d(x1))
           c#(c(x1)) -> d#(x1)
           g#(x1) -> b#(x1)
          TRS:
           b(b(x1)) -> c(d(x1))
           c(c(x1)) -> d(d(d(x1)))
           c(x1) -> g(x1)
           d(d(x1)) -> c(f(x1))
           d(d(d(x1))) -> g(c(x1))
           f(x1) -> a(g(x1))
           g(x1) -> d(a(b(x1)))
           g(g(x1)) -> b(c(x1))
          Arctic Interpretation Processor:
           dimension: 1
           interpretation:
            [g#](x0) = 1x0 + -16,
            
            [c#](x0) = 1x0,
            
            [d#](x0) = -2x0 + 5,
            
            [b#](x0) = 1x0,
            
            [a](x0) = 6,
            
            [f](x0) = -16x0 + 7,
            
            [g](x0) = 9x0 + 15,
            
            [c](x0) = 9x0 + 15,
            
            [d](x0) = 6x0 + 12,
            
            [b](x0) = 8x0 + 15
           orientation:
            g#(g(x1)) = 10x1 + 16 >= 1x1 = c#(x1)
            
            c#(c(x1)) = 10x1 + 16 >= 10x1 + 16 = d#(d(d(x1)))
            
            d#(d(d(x1))) = 10x1 + 16 >= 10x1 + 16 = g#(c(x1))
            
            g#(g(x1)) = 10x1 + 16 >= 10x1 + 16 = b#(c(x1))
            
            b#(b(x1)) = 9x1 + 16 >= 7x1 + 13 = c#(d(x1))
            
            c#(c(x1)) = 10x1 + 16 >= 4x1 + 10 = d#(d(x1))
            
            c#(c(x1)) = 10x1 + 16 >= -2x1 + 5 = d#(x1)
            
            g#(x1) = 1x1 + -16 >= 1x1 = b#(x1)
            
            b(b(x1)) = 16x1 + 23 >= 15x1 + 21 = c(d(x1))
            
            c(c(x1)) = 18x1 + 24 >= 18x1 + 24 = d(d(d(x1)))
            
            c(x1) = 9x1 + 15 >= 9x1 + 15 = g(x1)
            
            d(d(x1)) = 12x1 + 18 >= -7x1 + 16 = c(f(x1))
            
            d(d(d(x1))) = 18x1 + 24 >= 18x1 + 24 = g(c(x1))
            
            f(x1) = -16x1 + 7 >= 6 = a(g(x1))
            
            g(x1) = 9x1 + 15 >= 12 = d(a(b(x1)))
            
            g(g(x1)) = 18x1 + 24 >= 17x1 + 23 = b(c(x1))
           problem:
            DPs:
             c#(c(x1)) -> d#(d(d(x1)))
             d#(d(d(x1))) -> g#(c(x1))
             g#(g(x1)) -> b#(c(x1))
             g#(x1) -> b#(x1)
            TRS:
             b(b(x1)) -> c(d(x1))
             c(c(x1)) -> d(d(d(x1)))
             c(x1) -> g(x1)
             d(d(x1)) -> c(f(x1))
             d(d(d(x1))) -> g(c(x1))
             f(x1) -> a(g(x1))
             g(x1) -> d(a(b(x1)))
             g(g(x1)) -> b(c(x1))
           EDG Processor:
            DPs:
             c#(c(x1)) -> d#(d(d(x1)))
             d#(d(d(x1))) -> g#(c(x1))
             g#(g(x1)) -> b#(c(x1))
             g#(x1) -> b#(x1)
            TRS:
             b(b(x1)) -> c(d(x1))
             c(c(x1)) -> d(d(d(x1)))
             c(x1) -> g(x1)
             d(d(x1)) -> c(f(x1))
             d(d(d(x1))) -> g(c(x1))
             f(x1) -> a(g(x1))
             g(x1) -> d(a(b(x1)))
             g(g(x1)) -> b(c(x1))
            graph:
             c#(c(x1)) -> d#(d(d(x1))) -> d#(d(d(x1))) -> g#(c(x1))
             d#(d(d(x1))) -> g#(c(x1)) -> g#(g(x1)) -> b#(c(x1))
             d#(d(d(x1))) -> g#(c(x1)) -> g#(x1) -> b#(x1)
            SCC Processor:
             #sccs: 0
             #rules: 0
             #arcs: 3/16