YES

Problem:
 3(1(x1)) -> 4(1(x1))
 5(9(x1)) -> 2(6(5(x1)))
 3(5(x1)) -> 8(9(7(x1)))
 9(x1) -> 3(2(3(x1)))
 8(4(x1)) -> 6(x1)
 2(6(x1)) -> 4(3(x1))
 3(8(x1)) -> 3(2(7(x1)))
 9(x1) -> 5(0(2(x1)))
 8(8(4(x1))) -> 1(9(x1))
 7(1(x1)) -> 6(9(x1))
 3(9(x1)) -> 9(3(x1))
 7(5(x1)) -> 1(0(x1))

Proof:
 DP Processor:
  DPs:
   5#(9(x1)) -> 5#(x1)
   5#(9(x1)) -> 2#(6(5(x1)))
   3#(5(x1)) -> 7#(x1)
   3#(5(x1)) -> 9#(7(x1))
   3#(5(x1)) -> 8#(9(7(x1)))
   9#(x1) -> 3#(x1)
   9#(x1) -> 2#(3(x1))
   9#(x1) -> 3#(2(3(x1)))
   2#(6(x1)) -> 3#(x1)
   3#(8(x1)) -> 7#(x1)
   3#(8(x1)) -> 2#(7(x1))
   3#(8(x1)) -> 3#(2(7(x1)))
   9#(x1) -> 2#(x1)
   9#(x1) -> 5#(0(2(x1)))
   8#(8(4(x1))) -> 9#(x1)
   7#(1(x1)) -> 9#(x1)
   3#(9(x1)) -> 3#(x1)
   3#(9(x1)) -> 9#(3(x1))
  TRS:
   3(1(x1)) -> 4(1(x1))
   5(9(x1)) -> 2(6(5(x1)))
   3(5(x1)) -> 8(9(7(x1)))
   9(x1) -> 3(2(3(x1)))
   8(4(x1)) -> 6(x1)
   2(6(x1)) -> 4(3(x1))
   3(8(x1)) -> 3(2(7(x1)))
   9(x1) -> 5(0(2(x1)))
   8(8(4(x1))) -> 1(9(x1))
   7(1(x1)) -> 6(9(x1))
   3(9(x1)) -> 9(3(x1))
   7(5(x1)) -> 1(0(x1))
  TDG Processor:
   DPs:
    5#(9(x1)) -> 5#(x1)
    5#(9(x1)) -> 2#(6(5(x1)))
    3#(5(x1)) -> 7#(x1)
    3#(5(x1)) -> 9#(7(x1))
    3#(5(x1)) -> 8#(9(7(x1)))
    9#(x1) -> 3#(x1)
    9#(x1) -> 2#(3(x1))
    9#(x1) -> 3#(2(3(x1)))
    2#(6(x1)) -> 3#(x1)
    3#(8(x1)) -> 7#(x1)
    3#(8(x1)) -> 2#(7(x1))
    3#(8(x1)) -> 3#(2(7(x1)))
    9#(x1) -> 2#(x1)
    9#(x1) -> 5#(0(2(x1)))
    8#(8(4(x1))) -> 9#(x1)
    7#(1(x1)) -> 9#(x1)
    3#(9(x1)) -> 3#(x1)
    3#(9(x1)) -> 9#(3(x1))
   TRS:
    3(1(x1)) -> 4(1(x1))
    5(9(x1)) -> 2(6(5(x1)))
    3(5(x1)) -> 8(9(7(x1)))
    9(x1) -> 3(2(3(x1)))
    8(4(x1)) -> 6(x1)
    2(6(x1)) -> 4(3(x1))
    3(8(x1)) -> 3(2(7(x1)))
    9(x1) -> 5(0(2(x1)))
    8(8(4(x1))) -> 1(9(x1))
    7(1(x1)) -> 6(9(x1))
    3(9(x1)) -> 9(3(x1))
    7(5(x1)) -> 1(0(x1))
   graph:
    8#(8(4(x1))) -> 9#(x1) -> 9#(x1) -> 5#(0(2(x1)))
    8#(8(4(x1))) -> 9#(x1) -> 9#(x1) -> 2#(x1)
    8#(8(4(x1))) -> 9#(x1) -> 9#(x1) -> 3#(2(3(x1)))
    8#(8(4(x1))) -> 9#(x1) -> 9#(x1) -> 2#(3(x1))
    8#(8(4(x1))) -> 9#(x1) -> 9#(x1) -> 3#(x1)
    9#(x1) -> 2#(3(x1)) -> 2#(6(x1)) -> 3#(x1)
    9#(x1) -> 2#(x1) -> 2#(6(x1)) -> 3#(x1)
    9#(x1) -> 5#(0(2(x1))) -> 5#(9(x1)) -> 2#(6(5(x1)))
    9#(x1) -> 5#(0(2(x1))) -> 5#(9(x1)) -> 5#(x1)
    9#(x1) -> 3#(2(3(x1))) -> 3#(9(x1)) -> 9#(3(x1))
    9#(x1) -> 3#(2(3(x1))) -> 3#(9(x1)) -> 3#(x1)
    9#(x1) -> 3#(2(3(x1))) -> 3#(8(x1)) -> 3#(2(7(x1)))
    9#(x1) -> 3#(2(3(x1))) -> 3#(8(x1)) -> 2#(7(x1))
    9#(x1) -> 3#(2(3(x1))) -> 3#(8(x1)) -> 7#(x1)
    9#(x1) -> 3#(2(3(x1))) -> 3#(5(x1)) -> 8#(9(7(x1)))
    9#(x1) -> 3#(2(3(x1))) -> 3#(5(x1)) -> 9#(7(x1))
    9#(x1) -> 3#(2(3(x1))) -> 3#(5(x1)) -> 7#(x1)
    9#(x1) -> 3#(x1) -> 3#(9(x1)) -> 9#(3(x1))
    9#(x1) -> 3#(x1) -> 3#(9(x1)) -> 3#(x1)
    9#(x1) -> 3#(x1) -> 3#(8(x1)) -> 3#(2(7(x1)))
    9#(x1) -> 3#(x1) -> 3#(8(x1)) -> 2#(7(x1))
    9#(x1) -> 3#(x1) -> 3#(8(x1)) -> 7#(x1)
    9#(x1) -> 3#(x1) -> 3#(5(x1)) -> 8#(9(7(x1)))
    9#(x1) -> 3#(x1) -> 3#(5(x1)) -> 9#(7(x1))
    9#(x1) -> 3#(x1) -> 3#(5(x1)) -> 7#(x1)
    7#(1(x1)) -> 9#(x1) -> 9#(x1) -> 5#(0(2(x1)))
    7#(1(x1)) -> 9#(x1) -> 9#(x1) -> 2#(x1)
    7#(1(x1)) -> 9#(x1) -> 9#(x1) -> 3#(2(3(x1)))
    7#(1(x1)) -> 9#(x1) -> 9#(x1) -> 2#(3(x1))
    7#(1(x1)) -> 9#(x1) -> 9#(x1) -> 3#(x1)
    2#(6(x1)) -> 3#(x1) -> 3#(9(x1)) -> 9#(3(x1))
    2#(6(x1)) -> 3#(x1) -> 3#(9(x1)) -> 3#(x1)
    2#(6(x1)) -> 3#(x1) -> 3#(8(x1)) -> 3#(2(7(x1)))
    2#(6(x1)) -> 3#(x1) -> 3#(8(x1)) -> 2#(7(x1))
    2#(6(x1)) -> 3#(x1) -> 3#(8(x1)) -> 7#(x1)
    2#(6(x1)) -> 3#(x1) -> 3#(5(x1)) -> 8#(9(7(x1)))
    2#(6(x1)) -> 3#(x1) -> 3#(5(x1)) -> 9#(7(x1))
    2#(6(x1)) -> 3#(x1) -> 3#(5(x1)) -> 7#(x1)
    5#(9(x1)) -> 2#(6(5(x1))) -> 2#(6(x1)) -> 3#(x1)
    5#(9(x1)) -> 5#(x1) -> 5#(9(x1)) -> 2#(6(5(x1)))
    5#(9(x1)) -> 5#(x1) -> 5#(9(x1)) -> 5#(x1)
    3#(8(x1)) -> 7#(x1) -> 7#(1(x1)) -> 9#(x1)
    3#(8(x1)) -> 2#(7(x1)) -> 2#(6(x1)) -> 3#(x1)
    3#(8(x1)) -> 3#(2(7(x1))) -> 3#(9(x1)) -> 9#(3(x1))
    3#(8(x1)) -> 3#(2(7(x1))) -> 3#(9(x1)) -> 3#(x1)
    3#(8(x1)) -> 3#(2(7(x1))) -> 3#(8(x1)) -> 3#(2(7(x1)))
    3#(8(x1)) -> 3#(2(7(x1))) -> 3#(8(x1)) -> 2#(7(x1))
    3#(8(x1)) -> 3#(2(7(x1))) -> 3#(8(x1)) -> 7#(x1)
    3#(8(x1)) -> 3#(2(7(x1))) -> 3#(5(x1)) -> 8#(9(7(x1)))
    3#(8(x1)) -> 3#(2(7(x1))) -> 3#(5(x1)) -> 9#(7(x1))
    3#(8(x1)) -> 3#(2(7(x1))) -> 3#(5(x1)) -> 7#(x1)
    3#(5(x1)) -> 8#(9(7(x1))) -> 8#(8(4(x1))) -> 9#(x1)
    3#(5(x1)) -> 9#(7(x1)) -> 9#(x1) -> 5#(0(2(x1)))
    3#(5(x1)) -> 9#(7(x1)) -> 9#(x1) -> 2#(x1)
    3#(5(x1)) -> 9#(7(x1)) -> 9#(x1) -> 3#(2(3(x1)))
    3#(5(x1)) -> 9#(7(x1)) -> 9#(x1) -> 2#(3(x1))
    3#(5(x1)) -> 9#(7(x1)) -> 9#(x1) -> 3#(x1)
    3#(5(x1)) -> 7#(x1) -> 7#(1(x1)) -> 9#(x1)
    3#(9(x1)) -> 9#(3(x1)) -> 9#(x1) -> 5#(0(2(x1)))
    3#(9(x1)) -> 9#(3(x1)) -> 9#(x1) -> 2#(x1)
    3#(9(x1)) -> 9#(3(x1)) -> 9#(x1) -> 3#(2(3(x1)))
    3#(9(x1)) -> 9#(3(x1)) -> 9#(x1) -> 2#(3(x1))
    3#(9(x1)) -> 9#(3(x1)) -> 9#(x1) -> 3#(x1)
    3#(9(x1)) -> 3#(x1) -> 3#(9(x1)) -> 9#(3(x1))
    3#(9(x1)) -> 3#(x1) -> 3#(9(x1)) -> 3#(x1)
    3#(9(x1)) -> 3#(x1) -> 3#(8(x1)) -> 3#(2(7(x1)))
    3#(9(x1)) -> 3#(x1) -> 3#(8(x1)) -> 2#(7(x1))
    3#(9(x1)) -> 3#(x1) -> 3#(8(x1)) -> 7#(x1)
    3#(9(x1)) -> 3#(x1) -> 3#(5(x1)) -> 8#(9(7(x1)))
    3#(9(x1)) -> 3#(x1) -> 3#(5(x1)) -> 9#(7(x1))
    3#(9(x1)) -> 3#(x1) -> 3#(5(x1)) -> 7#(x1)
   EDG Processor:
    DPs:
     5#(9(x1)) -> 5#(x1)
     5#(9(x1)) -> 2#(6(5(x1)))
     3#(5(x1)) -> 7#(x1)
     3#(5(x1)) -> 9#(7(x1))
     3#(5(x1)) -> 8#(9(7(x1)))
     9#(x1) -> 3#(x1)
     9#(x1) -> 2#(3(x1))
     9#(x1) -> 3#(2(3(x1)))
     2#(6(x1)) -> 3#(x1)
     3#(8(x1)) -> 7#(x1)
     3#(8(x1)) -> 2#(7(x1))
     3#(8(x1)) -> 3#(2(7(x1)))
     9#(x1) -> 2#(x1)
     9#(x1) -> 5#(0(2(x1)))
     8#(8(4(x1))) -> 9#(x1)
     7#(1(x1)) -> 9#(x1)
     3#(9(x1)) -> 3#(x1)
     3#(9(x1)) -> 9#(3(x1))
    TRS:
     3(1(x1)) -> 4(1(x1))
     5(9(x1)) -> 2(6(5(x1)))
     3(5(x1)) -> 8(9(7(x1)))
     9(x1) -> 3(2(3(x1)))
     8(4(x1)) -> 6(x1)
     2(6(x1)) -> 4(3(x1))
     3(8(x1)) -> 3(2(7(x1)))
     9(x1) -> 5(0(2(x1)))
     8(8(4(x1))) -> 1(9(x1))
     7(1(x1)) -> 6(9(x1))
     3(9(x1)) -> 9(3(x1))
     7(5(x1)) -> 1(0(x1))
    graph:
     8#(8(4(x1))) -> 9#(x1) -> 9#(x1) -> 3#(x1)
     8#(8(4(x1))) -> 9#(x1) -> 9#(x1) -> 2#(3(x1))
     8#(8(4(x1))) -> 9#(x1) -> 9#(x1) -> 3#(2(3(x1)))
     8#(8(4(x1))) -> 9#(x1) -> 9#(x1) -> 2#(x1)
     8#(8(4(x1))) -> 9#(x1) -> 9#(x1) -> 5#(0(2(x1)))
     9#(x1) -> 2#(3(x1)) -> 2#(6(x1)) -> 3#(x1)
     9#(x1) -> 2#(x1) -> 2#(6(x1)) -> 3#(x1)
     9#(x1) -> 3#(2(3(x1))) -> 3#(5(x1)) -> 7#(x1)
     9#(x1) -> 3#(2(3(x1))) -> 3#(5(x1)) -> 9#(7(x1))
     9#(x1) -> 3#(2(3(x1))) -> 3#(5(x1)) -> 8#(9(7(x1)))
     9#(x1) -> 3#(2(3(x1))) -> 3#(8(x1)) -> 7#(x1)
     9#(x1) -> 3#(2(3(x1))) -> 3#(8(x1)) -> 2#(7(x1))
     9#(x1) -> 3#(2(3(x1))) -> 3#(8(x1)) -> 3#(2(7(x1)))
     9#(x1) -> 3#(2(3(x1))) -> 3#(9(x1)) -> 3#(x1)
     9#(x1) -> 3#(2(3(x1))) -> 3#(9(x1)) -> 9#(3(x1))
     9#(x1) -> 3#(x1) -> 3#(5(x1)) -> 7#(x1)
     9#(x1) -> 3#(x1) -> 3#(5(x1)) -> 9#(7(x1))
     9#(x1) -> 3#(x1) -> 3#(5(x1)) -> 8#(9(7(x1)))
     9#(x1) -> 3#(x1) -> 3#(8(x1)) -> 7#(x1)
     9#(x1) -> 3#(x1) -> 3#(8(x1)) -> 2#(7(x1))
     9#(x1) -> 3#(x1) -> 3#(8(x1)) -> 3#(2(7(x1)))
     9#(x1) -> 3#(x1) -> 3#(9(x1)) -> 3#(x1)
     9#(x1) -> 3#(x1) -> 3#(9(x1)) -> 9#(3(x1))
     7#(1(x1)) -> 9#(x1) -> 9#(x1) -> 3#(x1)
     7#(1(x1)) -> 9#(x1) -> 9#(x1) -> 2#(3(x1))
     7#(1(x1)) -> 9#(x1) -> 9#(x1) -> 3#(2(3(x1)))
     7#(1(x1)) -> 9#(x1) -> 9#(x1) -> 2#(x1)
     7#(1(x1)) -> 9#(x1) -> 9#(x1) -> 5#(0(2(x1)))
     2#(6(x1)) -> 3#(x1) -> 3#(5(x1)) -> 7#(x1)
     2#(6(x1)) -> 3#(x1) -> 3#(5(x1)) -> 9#(7(x1))
     2#(6(x1)) -> 3#(x1) -> 3#(5(x1)) -> 8#(9(7(x1)))
     2#(6(x1)) -> 3#(x1) -> 3#(8(x1)) -> 7#(x1)
     2#(6(x1)) -> 3#(x1) -> 3#(8(x1)) -> 2#(7(x1))
     2#(6(x1)) -> 3#(x1) -> 3#(8(x1)) -> 3#(2(7(x1)))
     2#(6(x1)) -> 3#(x1) -> 3#(9(x1)) -> 3#(x1)
     2#(6(x1)) -> 3#(x1) -> 3#(9(x1)) -> 9#(3(x1))
     5#(9(x1)) -> 2#(6(5(x1))) -> 2#(6(x1)) -> 3#(x1)
     5#(9(x1)) -> 5#(x1) -> 5#(9(x1)) -> 5#(x1)
     5#(9(x1)) -> 5#(x1) -> 5#(9(x1)) -> 2#(6(5(x1)))
     3#(8(x1)) -> 7#(x1) -> 7#(1(x1)) -> 9#(x1)
     3#(8(x1)) -> 2#(7(x1)) -> 2#(6(x1)) -> 3#(x1)
     3#(8(x1)) -> 3#(2(7(x1))) -> 3#(5(x1)) -> 7#(x1)
     3#(8(x1)) -> 3#(2(7(x1))) -> 3#(5(x1)) -> 9#(7(x1))
     3#(8(x1)) -> 3#(2(7(x1))) -> 3#(5(x1)) -> 8#(9(7(x1)))
     3#(8(x1)) -> 3#(2(7(x1))) -> 3#(8(x1)) -> 7#(x1)
     3#(8(x1)) -> 3#(2(7(x1))) -> 3#(8(x1)) -> 2#(7(x1))
     3#(8(x1)) -> 3#(2(7(x1))) -> 3#(8(x1)) -> 3#(2(7(x1)))
     3#(8(x1)) -> 3#(2(7(x1))) -> 3#(9(x1)) -> 3#(x1)
     3#(8(x1)) -> 3#(2(7(x1))) -> 3#(9(x1)) -> 9#(3(x1))
     3#(5(x1)) -> 8#(9(7(x1))) -> 8#(8(4(x1))) -> 9#(x1)
     3#(5(x1)) -> 9#(7(x1)) -> 9#(x1) -> 3#(x1)
     3#(5(x1)) -> 9#(7(x1)) -> 9#(x1) -> 2#(3(x1))
     3#(5(x1)) -> 9#(7(x1)) -> 9#(x1) -> 3#(2(3(x1)))
     3#(5(x1)) -> 9#(7(x1)) -> 9#(x1) -> 2#(x1)
     3#(5(x1)) -> 9#(7(x1)) -> 9#(x1) -> 5#(0(2(x1)))
     3#(5(x1)) -> 7#(x1) -> 7#(1(x1)) -> 9#(x1)
     3#(9(x1)) -> 9#(3(x1)) -> 9#(x1) -> 3#(x1)
     3#(9(x1)) -> 9#(3(x1)) -> 9#(x1) -> 2#(3(x1))
     3#(9(x1)) -> 9#(3(x1)) -> 9#(x1) -> 3#(2(3(x1)))
     3#(9(x1)) -> 9#(3(x1)) -> 9#(x1) -> 2#(x1)
     3#(9(x1)) -> 9#(3(x1)) -> 9#(x1) -> 5#(0(2(x1)))
     3#(9(x1)) -> 3#(x1) -> 3#(5(x1)) -> 7#(x1)
     3#(9(x1)) -> 3#(x1) -> 3#(5(x1)) -> 9#(7(x1))
     3#(9(x1)) -> 3#(x1) -> 3#(5(x1)) -> 8#(9(7(x1)))
     3#(9(x1)) -> 3#(x1) -> 3#(8(x1)) -> 7#(x1)
     3#(9(x1)) -> 3#(x1) -> 3#(8(x1)) -> 2#(7(x1))
     3#(9(x1)) -> 3#(x1) -> 3#(8(x1)) -> 3#(2(7(x1)))
     3#(9(x1)) -> 3#(x1) -> 3#(9(x1)) -> 3#(x1)
     3#(9(x1)) -> 3#(x1) -> 3#(9(x1)) -> 9#(3(x1))
    SCC Processor:
     #sccs: 2
     #rules: 16
     #arcs: 69/324
     DPs:
      5#(9(x1)) -> 5#(x1)
     TRS:
      3(1(x1)) -> 4(1(x1))
      5(9(x1)) -> 2(6(5(x1)))
      3(5(x1)) -> 8(9(7(x1)))
      9(x1) -> 3(2(3(x1)))
      8(4(x1)) -> 6(x1)
      2(6(x1)) -> 4(3(x1))
      3(8(x1)) -> 3(2(7(x1)))
      9(x1) -> 5(0(2(x1)))
      8(8(4(x1))) -> 1(9(x1))
      7(1(x1)) -> 6(9(x1))
      3(9(x1)) -> 9(3(x1))
      7(5(x1)) -> 1(0(x1))
     KBO Processor:
      argument filtering:
       pi(1) = []
       pi(3) = 0
       pi(4) = []
       pi(9) = [0]
       pi(5) = []
       pi(6) = []
       pi(2) = 0
       pi(7) = []
       pi(8) = []
       pi(0) = []
       pi(5#) = 0
      weight function:
       w0 = 1
       w(5#) = w(0) = w(8) = w(7) = w(6) = w(5) = w(9) = w(4) = w(1) = 1
       w(2) = w(3) = 0
      precedence:
       0 ~ 5 ~ 9 > 8 > 7 > 1 > 6 > 5# ~ 2 ~ 4 ~ 3
      problem:
       DPs:
        
       TRS:
        3(1(x1)) -> 4(1(x1))
        5(9(x1)) -> 2(6(5(x1)))
        3(5(x1)) -> 8(9(7(x1)))
        9(x1) -> 3(2(3(x1)))
        8(4(x1)) -> 6(x1)
        2(6(x1)) -> 4(3(x1))
        3(8(x1)) -> 3(2(7(x1)))
        9(x1) -> 5(0(2(x1)))
        8(8(4(x1))) -> 1(9(x1))
        7(1(x1)) -> 6(9(x1))
        3(9(x1)) -> 9(3(x1))
        7(5(x1)) -> 1(0(x1))
      Qed
     
     DPs:
      8#(8(4(x1))) -> 9#(x1)
      9#(x1) -> 2#(x1)
      2#(6(x1)) -> 3#(x1)
      3#(9(x1)) -> 9#(3(x1))
      9#(x1) -> 3#(2(3(x1)))
      3#(9(x1)) -> 3#(x1)
      3#(8(x1)) -> 3#(2(7(x1)))
      3#(8(x1)) -> 2#(7(x1))
      3#(8(x1)) -> 7#(x1)
      7#(1(x1)) -> 9#(x1)
      9#(x1) -> 2#(3(x1))
      9#(x1) -> 3#(x1)
      3#(5(x1)) -> 8#(9(7(x1)))
      3#(5(x1)) -> 9#(7(x1))
      3#(5(x1)) -> 7#(x1)
     TRS:
      3(1(x1)) -> 4(1(x1))
      5(9(x1)) -> 2(6(5(x1)))
      3(5(x1)) -> 8(9(7(x1)))
      9(x1) -> 3(2(3(x1)))
      8(4(x1)) -> 6(x1)
      2(6(x1)) -> 4(3(x1))
      3(8(x1)) -> 3(2(7(x1)))
      9(x1) -> 5(0(2(x1)))
      8(8(4(x1))) -> 1(9(x1))
      7(1(x1)) -> 6(9(x1))
      3(9(x1)) -> 9(3(x1))
      7(5(x1)) -> 1(0(x1))
     Matrix Interpretation Processor: dim=2
      
      interpretation:
       [8#](x0) = [4 0]x0 + [2],
       
       [9#](x0) = [0 4]x0 + [4],
       
       [7#](x0) = [4 0]x0 + [1],
       
       [2#](x0) = [0 4]x0 + [2],
       
       [3#](x0) = [0 4]x0 + [1],
       
                 [0 0]  
       [0](x0) = [0 5]x0,
       
                 [1 0]     [1]
       [8](x0) = [1 0]x0 + [1],
       
                 [1 1]  
       [7](x0) = [1 0]x0,
       
                 [1 3]  
       [2](x0) = [0 0]x0,
       
                 [0 1]  
       [6](x0) = [0 1]x0,
       
                 [4 4]     [0]
       [5](x0) = [1 1]x0 + [1],
       
                      [0]
       [9](x0) = x0 + [1],
       
                 [0 1]  
       [4](x0) = [0 0]x0,
       
                 [0 4]  
       [3](x0) = [0 1]x0,
       
                 [0 1]     [1]
       [1](x0) = [0 0]x0 + [0]
      orientation:
       8#(8(4(x1))) = [0 4]x1 + [6] >= [0 4]x1 + [4] = 9#(x1)
       
       9#(x1) = [0 4]x1 + [4] >= [0 4]x1 + [2] = 2#(x1)
       
       2#(6(x1)) = [0 4]x1 + [2] >= [0 4]x1 + [1] = 3#(x1)
       
       3#(9(x1)) = [0 4]x1 + [5] >= [0 4]x1 + [4] = 9#(3(x1))
       
       9#(x1) = [0 4]x1 + [4] >= [1] = 3#(2(3(x1)))
       
       3#(9(x1)) = [0 4]x1 + [5] >= [0 4]x1 + [1] = 3#(x1)
       
       3#(8(x1)) = [4 0]x1 + [5] >= [1] = 3#(2(7(x1)))
       
       3#(8(x1)) = [4 0]x1 + [5] >= [4 0]x1 + [2] = 2#(7(x1))
       
       3#(8(x1)) = [4 0]x1 + [5] >= [4 0]x1 + [1] = 7#(x1)
       
       7#(1(x1)) = [0 4]x1 + [5] >= [0 4]x1 + [4] = 9#(x1)
       
       9#(x1) = [0 4]x1 + [4] >= [0 4]x1 + [2] = 2#(3(x1))
       
       9#(x1) = [0 4]x1 + [4] >= [0 4]x1 + [1] = 3#(x1)
       
       3#(5(x1)) = [4 4]x1 + [5] >= [4 4]x1 + [2] = 8#(9(7(x1)))
       
       3#(5(x1)) = [4 4]x1 + [5] >= [4 0]x1 + [4] = 9#(7(x1))
       
       3#(5(x1)) = [4 4]x1 + [5] >= [4 0]x1 + [1] = 7#(x1)
       
                  [0]    [0]           
       3(1(x1)) = [0] >= [0] = 4(1(x1))
       
                  [4 4]     [4]    [4 4]     [4]              
       5(9(x1)) = [1 1]x1 + [2] >= [0 0]x1 + [0] = 2(6(5(x1)))
       
                  [4 4]     [4]    [1 1]     [1]              
       3(5(x1)) = [1 1]x1 + [1] >= [1 1]x1 + [1] = 8(9(7(x1)))
       
                    [0]    [0]              
       9(x1) = x1 + [1] >= [0] = 3(2(3(x1)))
       
                  [0 1]     [1]    [0 1]          
       8(4(x1)) = [0 1]x1 + [1] >= [0 1]x1 = 6(x1)
       
                  [0 4]      [0 1]             
       2(6(x1)) = [0 0]x1 >= [0 0]x1 = 4(3(x1))
       
                  [4 0]     [4]    [0]              
       3(8(x1)) = [1 0]x1 + [1] >= [0] = 3(2(7(x1)))
       
                    [0]    [0]              
       9(x1) = x1 + [1] >= [1] = 5(0(2(x1)))
       
                     [0 1]     [2]    [0 1]     [2]           
       8(8(4(x1))) = [0 1]x1 + [2] >= [0 0]x1 + [0] = 1(9(x1))
       
                  [0 1]     [1]    [0 1]     [1]           
       7(1(x1)) = [0 1]x1 + [1] >= [0 1]x1 + [1] = 6(9(x1))
       
                  [0 4]     [4]    [0 4]     [0]           
       3(9(x1)) = [0 1]x1 + [1] >= [0 1]x1 + [1] = 9(3(x1))
       
                  [5 5]     [1]    [0 5]     [1]           
       7(5(x1)) = [4 4]x1 + [0] >= [0 0]x1 + [0] = 1(0(x1))
      problem:
       DPs:
        
       TRS:
        3(1(x1)) -> 4(1(x1))
        5(9(x1)) -> 2(6(5(x1)))
        3(5(x1)) -> 8(9(7(x1)))
        9(x1) -> 3(2(3(x1)))
        8(4(x1)) -> 6(x1)
        2(6(x1)) -> 4(3(x1))
        3(8(x1)) -> 3(2(7(x1)))
        9(x1) -> 5(0(2(x1)))
        8(8(4(x1))) -> 1(9(x1))
        7(1(x1)) -> 6(9(x1))
        3(9(x1)) -> 9(3(x1))
        7(5(x1)) -> 1(0(x1))
      Qed