YES

Problem:
 2(5(x1)) -> 1(3(3(0(1(0(x1))))))
 2(5(x1)) -> 2(2(0(5(0(1(x1))))))
 3(5(x1)) -> 1(3(2(0(0(1(x1))))))
 3(5(x1)) -> 3(2(0(5(3(0(x1))))))
 4(5(x1)) -> 2(2(1(3(2(1(x1))))))
 4(5(x1)) -> 3(2(0(5(0(0(x1))))))
 1(2(5(x1))) -> 1(0(5(0(5(4(x1))))))
 1(2(5(x1))) -> 1(2(2(1(0(1(x1))))))
 1(2(5(x1))) -> 2(0(1(3(1(0(x1))))))
 1(4(5(x1))) -> 1(2(4(0(2(1(x1))))))
 2(5(1(x1))) -> 2(2(2(1(2(3(x1))))))
 2(5(2(x1))) -> 4(0(2(2(3(3(x1))))))
 2(5(3(x1))) -> 2(0(4(1(3(3(x1))))))
 2(5(4(x1))) -> 2(0(5(1(0(1(x1))))))
 3(2(5(x1))) -> 3(2(0(1(0(5(x1))))))
 3(4(2(x1))) -> 3(4(0(2(2(2(x1))))))
 3(5(1(x1))) -> 0(4(2(0(0(5(x1))))))
 3(5(1(x1))) -> 0(4(2(2(3(4(x1))))))
 3(5(1(x1))) -> 2(1(4(1(0(1(x1))))))
 3(5(2(x1))) -> 0(4(3(2(2(2(x1))))))
 3(5(2(x1))) -> 2(0(2(2(3(0(x1))))))
 3(5(2(x1))) -> 2(3(3(2(1(2(x1))))))
 3(5(3(x1))) -> 0(2(4(3(3(0(x1))))))
 3(5(3(x1))) -> 0(5(4(3(3(0(x1))))))
 3(5(3(x1))) -> 2(3(4(0(4(2(x1))))))
 3(5(4(x1))) -> 0(2(0(5(0(0(x1))))))
 3(5(4(x1))) -> 0(5(0(0(1(2(x1))))))
 3(5(5(x1))) -> 0(5(4(1(0(5(x1))))))
 4(5(1(x1))) -> 2(1(0(5(3(3(x1))))))
 4(5(2(x1))) -> 0(5(1(0(0(4(x1))))))
 4(5(4(x1))) -> 2(2(1(0(4(2(x1))))))
 4(5(4(x1))) -> 3(2(0(3(2(0(x1))))))
 5(5(3(x1))) -> 5(1(0(1(2(2(x1))))))
 5(5(4(x1))) -> 5(1(0(4(2(2(x1))))))

Proof:
 DP Processor:
  DPs:
   2#(5(x1)) -> 1#(0(x1))
   2#(5(x1)) -> 3#(0(1(0(x1))))
   2#(5(x1)) -> 3#(3(0(1(0(x1)))))
   2#(5(x1)) -> 1#(3(3(0(1(0(x1))))))
   2#(5(x1)) -> 1#(x1)
   2#(5(x1)) -> 5#(0(1(x1)))
   2#(5(x1)) -> 2#(0(5(0(1(x1)))))
   2#(5(x1)) -> 2#(2(0(5(0(1(x1))))))
   3#(5(x1)) -> 1#(x1)
   3#(5(x1)) -> 2#(0(0(1(x1))))
   3#(5(x1)) -> 3#(2(0(0(1(x1)))))
   3#(5(x1)) -> 1#(3(2(0(0(1(x1))))))
   3#(5(x1)) -> 3#(0(x1))
   3#(5(x1)) -> 5#(3(0(x1)))
   3#(5(x1)) -> 2#(0(5(3(0(x1)))))
   3#(5(x1)) -> 3#(2(0(5(3(0(x1))))))
   4#(5(x1)) -> 1#(x1)
   4#(5(x1)) -> 2#(1(x1))
   4#(5(x1)) -> 3#(2(1(x1)))
   4#(5(x1)) -> 1#(3(2(1(x1))))
   4#(5(x1)) -> 2#(1(3(2(1(x1)))))
   4#(5(x1)) -> 2#(2(1(3(2(1(x1))))))
   4#(5(x1)) -> 5#(0(0(x1)))
   4#(5(x1)) -> 2#(0(5(0(0(x1)))))
   4#(5(x1)) -> 3#(2(0(5(0(0(x1))))))
   1#(2(5(x1))) -> 4#(x1)
   1#(2(5(x1))) -> 5#(4(x1))
   1#(2(5(x1))) -> 5#(0(5(4(x1))))
   1#(2(5(x1))) -> 1#(0(5(0(5(4(x1))))))
   1#(2(5(x1))) -> 1#(x1)
   1#(2(5(x1))) -> 1#(0(1(x1)))
   1#(2(5(x1))) -> 2#(1(0(1(x1))))
   1#(2(5(x1))) -> 2#(2(1(0(1(x1)))))
   1#(2(5(x1))) -> 1#(2(2(1(0(1(x1))))))
   1#(2(5(x1))) -> 1#(0(x1))
   1#(2(5(x1))) -> 3#(1(0(x1)))
   1#(2(5(x1))) -> 1#(3(1(0(x1))))
   1#(2(5(x1))) -> 2#(0(1(3(1(0(x1))))))
   1#(4(5(x1))) -> 1#(x1)
   1#(4(5(x1))) -> 2#(1(x1))
   1#(4(5(x1))) -> 4#(0(2(1(x1))))
   1#(4(5(x1))) -> 2#(4(0(2(1(x1)))))
   1#(4(5(x1))) -> 1#(2(4(0(2(1(x1))))))
   2#(5(1(x1))) -> 3#(x1)
   2#(5(1(x1))) -> 2#(3(x1))
   2#(5(1(x1))) -> 1#(2(3(x1)))
   2#(5(1(x1))) -> 2#(1(2(3(x1))))
   2#(5(1(x1))) -> 2#(2(1(2(3(x1)))))
   2#(5(1(x1))) -> 2#(2(2(1(2(3(x1))))))
   2#(5(2(x1))) -> 3#(x1)
   2#(5(2(x1))) -> 3#(3(x1))
   2#(5(2(x1))) -> 2#(3(3(x1)))
   2#(5(2(x1))) -> 2#(2(3(3(x1))))
   2#(5(2(x1))) -> 4#(0(2(2(3(3(x1))))))
   2#(5(3(x1))) -> 3#(3(x1))
   2#(5(3(x1))) -> 1#(3(3(x1)))
   2#(5(3(x1))) -> 4#(1(3(3(x1))))
   2#(5(3(x1))) -> 2#(0(4(1(3(3(x1))))))
   2#(5(4(x1))) -> 1#(x1)
   2#(5(4(x1))) -> 1#(0(1(x1)))
   2#(5(4(x1))) -> 5#(1(0(1(x1))))
   2#(5(4(x1))) -> 2#(0(5(1(0(1(x1))))))
   3#(2(5(x1))) -> 1#(0(5(x1)))
   3#(2(5(x1))) -> 2#(0(1(0(5(x1)))))
   3#(2(5(x1))) -> 3#(2(0(1(0(5(x1))))))
   3#(4(2(x1))) -> 2#(2(x1))
   3#(4(2(x1))) -> 2#(2(2(x1)))
   3#(4(2(x1))) -> 4#(0(2(2(2(x1)))))
   3#(4(2(x1))) -> 3#(4(0(2(2(2(x1))))))
   3#(5(1(x1))) -> 5#(x1)
   3#(5(1(x1))) -> 2#(0(0(5(x1))))
   3#(5(1(x1))) -> 4#(2(0(0(5(x1)))))
   3#(5(1(x1))) -> 4#(x1)
   3#(5(1(x1))) -> 3#(4(x1))
   3#(5(1(x1))) -> 2#(3(4(x1)))
   3#(5(1(x1))) -> 2#(2(3(4(x1))))
   3#(5(1(x1))) -> 4#(2(2(3(4(x1)))))
   3#(5(1(x1))) -> 1#(0(1(x1)))
   3#(5(1(x1))) -> 4#(1(0(1(x1))))
   3#(5(1(x1))) -> 1#(4(1(0(1(x1)))))
   3#(5(1(x1))) -> 2#(1(4(1(0(1(x1))))))
   3#(5(2(x1))) -> 2#(2(x1))
   3#(5(2(x1))) -> 2#(2(2(x1)))
   3#(5(2(x1))) -> 3#(2(2(2(x1))))
   3#(5(2(x1))) -> 4#(3(2(2(2(x1)))))
   3#(5(2(x1))) -> 3#(0(x1))
   3#(5(2(x1))) -> 2#(3(0(x1)))
   3#(5(2(x1))) -> 2#(2(3(0(x1))))
   3#(5(2(x1))) -> 2#(0(2(2(3(0(x1))))))
   3#(5(2(x1))) -> 1#(2(x1))
   3#(5(2(x1))) -> 2#(1(2(x1)))
   3#(5(2(x1))) -> 3#(2(1(2(x1))))
   3#(5(2(x1))) -> 3#(3(2(1(2(x1)))))
   3#(5(2(x1))) -> 2#(3(3(2(1(2(x1))))))
   3#(5(3(x1))) -> 3#(0(x1))
   3#(5(3(x1))) -> 3#(3(0(x1)))
   3#(5(3(x1))) -> 4#(3(3(0(x1))))
   3#(5(3(x1))) -> 2#(4(3(3(0(x1)))))
   3#(5(3(x1))) -> 5#(4(3(3(0(x1)))))
   3#(5(3(x1))) -> 2#(x1)
   3#(5(3(x1))) -> 4#(2(x1))
   3#(5(3(x1))) -> 4#(0(4(2(x1))))
   3#(5(3(x1))) -> 3#(4(0(4(2(x1)))))
   3#(5(3(x1))) -> 2#(3(4(0(4(2(x1))))))
   3#(5(4(x1))) -> 5#(0(0(x1)))
   3#(5(4(x1))) -> 2#(0(5(0(0(x1)))))
   3#(5(4(x1))) -> 2#(x1)
   3#(5(4(x1))) -> 1#(2(x1))
   3#(5(4(x1))) -> 5#(0(0(1(2(x1)))))
   3#(5(5(x1))) -> 1#(0(5(x1)))
   3#(5(5(x1))) -> 4#(1(0(5(x1))))
   3#(5(5(x1))) -> 5#(4(1(0(5(x1)))))
   4#(5(1(x1))) -> 3#(x1)
   4#(5(1(x1))) -> 3#(3(x1))
   4#(5(1(x1))) -> 5#(3(3(x1)))
   4#(5(1(x1))) -> 1#(0(5(3(3(x1)))))
   4#(5(1(x1))) -> 2#(1(0(5(3(3(x1))))))
   4#(5(2(x1))) -> 4#(x1)
   4#(5(2(x1))) -> 1#(0(0(4(x1))))
   4#(5(2(x1))) -> 5#(1(0(0(4(x1)))))
   4#(5(4(x1))) -> 2#(x1)
   4#(5(4(x1))) -> 4#(2(x1))
   4#(5(4(x1))) -> 1#(0(4(2(x1))))
   4#(5(4(x1))) -> 2#(1(0(4(2(x1)))))
   4#(5(4(x1))) -> 2#(2(1(0(4(2(x1))))))
   4#(5(4(x1))) -> 2#(0(x1))
   4#(5(4(x1))) -> 3#(2(0(x1)))
   4#(5(4(x1))) -> 2#(0(3(2(0(x1)))))
   4#(5(4(x1))) -> 3#(2(0(3(2(0(x1))))))
   5#(5(3(x1))) -> 2#(x1)
   5#(5(3(x1))) -> 2#(2(x1))
   5#(5(3(x1))) -> 1#(2(2(x1)))
   5#(5(3(x1))) -> 1#(0(1(2(2(x1)))))
   5#(5(3(x1))) -> 5#(1(0(1(2(2(x1))))))
   5#(5(4(x1))) -> 2#(x1)
   5#(5(4(x1))) -> 2#(2(x1))
   5#(5(4(x1))) -> 4#(2(2(x1)))
   5#(5(4(x1))) -> 1#(0(4(2(2(x1)))))
   5#(5(4(x1))) -> 5#(1(0(4(2(2(x1))))))
  TRS:
   2(5(x1)) -> 1(3(3(0(1(0(x1))))))
   2(5(x1)) -> 2(2(0(5(0(1(x1))))))
   3(5(x1)) -> 1(3(2(0(0(1(x1))))))
   3(5(x1)) -> 3(2(0(5(3(0(x1))))))
   4(5(x1)) -> 2(2(1(3(2(1(x1))))))
   4(5(x1)) -> 3(2(0(5(0(0(x1))))))
   1(2(5(x1))) -> 1(0(5(0(5(4(x1))))))
   1(2(5(x1))) -> 1(2(2(1(0(1(x1))))))
   1(2(5(x1))) -> 2(0(1(3(1(0(x1))))))
   1(4(5(x1))) -> 1(2(4(0(2(1(x1))))))
   2(5(1(x1))) -> 2(2(2(1(2(3(x1))))))
   2(5(2(x1))) -> 4(0(2(2(3(3(x1))))))
   2(5(3(x1))) -> 2(0(4(1(3(3(x1))))))
   2(5(4(x1))) -> 2(0(5(1(0(1(x1))))))
   3(2(5(x1))) -> 3(2(0(1(0(5(x1))))))
   3(4(2(x1))) -> 3(4(0(2(2(2(x1))))))
   3(5(1(x1))) -> 0(4(2(0(0(5(x1))))))
   3(5(1(x1))) -> 0(4(2(2(3(4(x1))))))
   3(5(1(x1))) -> 2(1(4(1(0(1(x1))))))
   3(5(2(x1))) -> 0(4(3(2(2(2(x1))))))
   3(5(2(x1))) -> 2(0(2(2(3(0(x1))))))
   3(5(2(x1))) -> 2(3(3(2(1(2(x1))))))
   3(5(3(x1))) -> 0(2(4(3(3(0(x1))))))
   3(5(3(x1))) -> 0(5(4(3(3(0(x1))))))
   3(5(3(x1))) -> 2(3(4(0(4(2(x1))))))
   3(5(4(x1))) -> 0(2(0(5(0(0(x1))))))
   3(5(4(x1))) -> 0(5(0(0(1(2(x1))))))
   3(5(5(x1))) -> 0(5(4(1(0(5(x1))))))
   4(5(1(x1))) -> 2(1(0(5(3(3(x1))))))
   4(5(2(x1))) -> 0(5(1(0(0(4(x1))))))
   4(5(4(x1))) -> 2(2(1(0(4(2(x1))))))
   4(5(4(x1))) -> 3(2(0(3(2(0(x1))))))
   5(5(3(x1))) -> 5(1(0(1(2(2(x1))))))
   5(5(4(x1))) -> 5(1(0(4(2(2(x1))))))
  Arctic Interpretation Processor:
   dimension: 1
   usable rules:
    2(5(x1)) -> 1(3(3(0(1(0(x1))))))
    2(5(x1)) -> 2(2(0(5(0(1(x1))))))
    3(5(x1)) -> 1(3(2(0(0(1(x1))))))
    3(5(x1)) -> 3(2(0(5(3(0(x1))))))
    4(5(x1)) -> 2(2(1(3(2(1(x1))))))
    4(5(x1)) -> 3(2(0(5(0(0(x1))))))
    1(2(5(x1))) -> 1(0(5(0(5(4(x1))))))
    1(2(5(x1))) -> 1(2(2(1(0(1(x1))))))
    1(2(5(x1))) -> 2(0(1(3(1(0(x1))))))
    1(4(5(x1))) -> 1(2(4(0(2(1(x1))))))
    2(5(1(x1))) -> 2(2(2(1(2(3(x1))))))
    2(5(2(x1))) -> 4(0(2(2(3(3(x1))))))
    2(5(3(x1))) -> 2(0(4(1(3(3(x1))))))
    2(5(4(x1))) -> 2(0(5(1(0(1(x1))))))
    3(2(5(x1))) -> 3(2(0(1(0(5(x1))))))
    3(4(2(x1))) -> 3(4(0(2(2(2(x1))))))
    3(5(1(x1))) -> 0(4(2(0(0(5(x1))))))
    3(5(1(x1))) -> 0(4(2(2(3(4(x1))))))
    3(5(1(x1))) -> 2(1(4(1(0(1(x1))))))
    3(5(2(x1))) -> 0(4(3(2(2(2(x1))))))
    3(5(2(x1))) -> 2(0(2(2(3(0(x1))))))
    3(5(2(x1))) -> 2(3(3(2(1(2(x1))))))
    3(5(3(x1))) -> 0(2(4(3(3(0(x1))))))
    3(5(3(x1))) -> 0(5(4(3(3(0(x1))))))
    3(5(3(x1))) -> 2(3(4(0(4(2(x1))))))
    3(5(4(x1))) -> 0(2(0(5(0(0(x1))))))
    3(5(4(x1))) -> 0(5(0(0(1(2(x1))))))
    3(5(5(x1))) -> 0(5(4(1(0(5(x1))))))
    4(5(1(x1))) -> 2(1(0(5(3(3(x1))))))
    4(5(2(x1))) -> 0(5(1(0(0(4(x1))))))
    4(5(4(x1))) -> 2(2(1(0(4(2(x1))))))
    4(5(4(x1))) -> 3(2(0(3(2(0(x1))))))
   interpretation:
    [4#](x0) = 1x0 + 0,
    
    [5#](x0) = 1x0 + 0,
    
    [3#](x0) = 2x0 + 0,
    
    [1#](x0) = 2x0 + 0,
    
    [2#](x0) = 1x0 + 3,
    
    [4](x0) = x0 + 0,
    
    [3](x0) = x0 + 0,
    
    [1](x0) = x0,
    
    [0](x0) = 0,
    
    [2](x0) = x0 + 2,
    
    [5](x0) = 2x0 + 15
   orientation:
    2#(5(x1)) = 3x1 + 16 >= 2 = 1#(0(x1))
    
    2#(5(x1)) = 3x1 + 16 >= 2 = 3#(0(1(0(x1))))
    
    2#(5(x1)) = 3x1 + 16 >= 2 = 3#(3(0(1(0(x1)))))
    
    2#(5(x1)) = 3x1 + 16 >= 2 = 1#(3(3(0(1(0(x1))))))
    
    2#(5(x1)) = 3x1 + 16 >= 2x1 + 0 = 1#(x1)
    
    2#(5(x1)) = 3x1 + 16 >= 1 = 5#(0(1(x1)))
    
    2#(5(x1)) = 3x1 + 16 >= 3 = 2#(0(5(0(1(x1)))))
    
    2#(5(x1)) = 3x1 + 16 >= 3 = 2#(2(0(5(0(1(x1))))))
    
    3#(5(x1)) = 4x1 + 17 >= 2x1 + 0 = 1#(x1)
    
    3#(5(x1)) = 4x1 + 17 >= 3 = 2#(0(0(1(x1))))
    
    3#(5(x1)) = 4x1 + 17 >= 4 = 3#(2(0(0(1(x1)))))
    
    3#(5(x1)) = 4x1 + 17 >= 4 = 1#(3(2(0(0(1(x1))))))
    
    3#(5(x1)) = 4x1 + 17 >= 2 = 3#(0(x1))
    
    3#(5(x1)) = 4x1 + 17 >= 1 = 5#(3(0(x1)))
    
    3#(5(x1)) = 4x1 + 17 >= 3 = 2#(0(5(3(0(x1)))))
    
    3#(5(x1)) = 4x1 + 17 >= 4 = 3#(2(0(5(3(0(x1))))))
    
    4#(5(x1)) = 3x1 + 16 >= 2x1 + 0 = 1#(x1)
    
    4#(5(x1)) = 3x1 + 16 >= 1x1 + 3 = 2#(1(x1))
    
    4#(5(x1)) = 3x1 + 16 >= 2x1 + 4 = 3#(2(1(x1)))
    
    4#(5(x1)) = 3x1 + 16 >= 2x1 + 4 = 1#(3(2(1(x1))))
    
    4#(5(x1)) = 3x1 + 16 >= 1x1 + 3 = 2#(1(3(2(1(x1)))))
    
    4#(5(x1)) = 3x1 + 16 >= 1x1 + 3 = 2#(2(1(3(2(1(x1))))))
    
    4#(5(x1)) = 3x1 + 16 >= 1 = 5#(0(0(x1)))
    
    4#(5(x1)) = 3x1 + 16 >= 3 = 2#(0(5(0(0(x1)))))
    
    4#(5(x1)) = 3x1 + 16 >= 4 = 3#(2(0(5(0(0(x1))))))
    
    1#(2(5(x1))) = 4x1 + 17 >= 1x1 + 0 = 4#(x1)
    
    1#(2(5(x1))) = 4x1 + 17 >= 1x1 + 1 = 5#(4(x1))
    
    1#(2(5(x1))) = 4x1 + 17 >= 1 = 5#(0(5(4(x1))))
    
    1#(2(5(x1))) = 4x1 + 17 >= 2 = 1#(0(5(0(5(4(x1))))))
    
    1#(2(5(x1))) = 4x1 + 17 >= 2x1 + 0 = 1#(x1)
    
    1#(2(5(x1))) = 4x1 + 17 >= 2 = 1#(0(1(x1)))
    
    1#(2(5(x1))) = 4x1 + 17 >= 3 = 2#(1(0(1(x1))))
    
    1#(2(5(x1))) = 4x1 + 17 >= 3 = 2#(2(1(0(1(x1)))))
    
    1#(2(5(x1))) = 4x1 + 17 >= 4 = 1#(2(2(1(0(1(x1))))))
    
    1#(2(5(x1))) = 4x1 + 17 >= 2 = 1#(0(x1))
    
    1#(2(5(x1))) = 4x1 + 17 >= 2 = 3#(1(0(x1)))
    
    1#(2(5(x1))) = 4x1 + 17 >= 2 = 1#(3(1(0(x1))))
    
    1#(2(5(x1))) = 4x1 + 17 >= 3 = 2#(0(1(3(1(0(x1))))))
    
    1#(4(5(x1))) = 4x1 + 17 >= 2x1 + 0 = 1#(x1)
    
    1#(4(5(x1))) = 4x1 + 17 >= 1x1 + 3 = 2#(1(x1))
    
    1#(4(5(x1))) = 4x1 + 17 >= 1 = 4#(0(2(1(x1))))
    
    1#(4(5(x1))) = 4x1 + 17 >= 3 = 2#(4(0(2(1(x1)))))
    
    1#(4(5(x1))) = 4x1 + 17 >= 4 = 1#(2(4(0(2(1(x1))))))
    
    2#(5(1(x1))) = 3x1 + 16 >= 2x1 + 0 = 3#(x1)
    
    2#(5(1(x1))) = 3x1 + 16 >= 1x1 + 3 = 2#(3(x1))
    
    2#(5(1(x1))) = 3x1 + 16 >= 2x1 + 4 = 1#(2(3(x1)))
    
    2#(5(1(x1))) = 3x1 + 16 >= 1x1 + 3 = 2#(1(2(3(x1))))
    
    2#(5(1(x1))) = 3x1 + 16 >= 1x1 + 3 = 2#(2(1(2(3(x1)))))
    
    2#(5(1(x1))) = 3x1 + 16 >= 1x1 + 3 = 2#(2(2(1(2(3(x1))))))
    
    2#(5(2(x1))) = 3x1 + 16 >= 2x1 + 0 = 3#(x1)
    
    2#(5(2(x1))) = 3x1 + 16 >= 2x1 + 2 = 3#(3(x1))
    
    2#(5(2(x1))) = 3x1 + 16 >= 1x1 + 3 = 2#(3(3(x1)))
    
    2#(5(2(x1))) = 3x1 + 16 >= 1x1 + 3 = 2#(2(3(3(x1))))
    
    2#(5(2(x1))) = 3x1 + 16 >= 1 = 4#(0(2(2(3(3(x1))))))
    
    2#(5(3(x1))) = 3x1 + 16 >= 2x1 + 2 = 3#(3(x1))
    
    2#(5(3(x1))) = 3x1 + 16 >= 2x1 + 2 = 1#(3(3(x1)))
    
    2#(5(3(x1))) = 3x1 + 16 >= 1x1 + 1 = 4#(1(3(3(x1))))
    
    2#(5(3(x1))) = 3x1 + 16 >= 3 = 2#(0(4(1(3(3(x1))))))
    
    2#(5(4(x1))) = 3x1 + 16 >= 2x1 + 0 = 1#(x1)
    
    2#(5(4(x1))) = 3x1 + 16 >= 2 = 1#(0(1(x1)))
    
    2#(5(4(x1))) = 3x1 + 16 >= 1 = 5#(1(0(1(x1))))
    
    2#(5(4(x1))) = 3x1 + 16 >= 3 = 2#(0(5(1(0(1(x1))))))
    
    3#(2(5(x1))) = 4x1 + 17 >= 2 = 1#(0(5(x1)))
    
    3#(2(5(x1))) = 4x1 + 17 >= 3 = 2#(0(1(0(5(x1)))))
    
    3#(2(5(x1))) = 4x1 + 17 >= 4 = 3#(2(0(1(0(5(x1))))))
    
    3#(4(2(x1))) = 2x1 + 4 >= 1x1 + 3 = 2#(2(x1))
    
    3#(4(2(x1))) = 2x1 + 4 >= 1x1 + 3 = 2#(2(2(x1)))
    
    3#(4(2(x1))) = 2x1 + 4 >= 1 = 4#(0(2(2(2(x1)))))
    
    3#(4(2(x1))) = 2x1 + 4 >= 2 = 3#(4(0(2(2(2(x1))))))
    
    3#(5(1(x1))) = 4x1 + 17 >= 1x1 + 0 = 5#(x1)
    
    3#(5(1(x1))) = 4x1 + 17 >= 3 = 2#(0(0(5(x1))))
    
    3#(5(1(x1))) = 4x1 + 17 >= 3 = 4#(2(0(0(5(x1)))))
    
    3#(5(1(x1))) = 4x1 + 17 >= 1x1 + 0 = 4#(x1)
    
    3#(5(1(x1))) = 4x1 + 17 >= 2x1 + 2 = 3#(4(x1))
    
    3#(5(1(x1))) = 4x1 + 17 >= 1x1 + 3 = 2#(3(4(x1)))
    
    3#(5(1(x1))) = 4x1 + 17 >= 1x1 + 3 = 2#(2(3(4(x1))))
    
    3#(5(1(x1))) = 4x1 + 17 >= 1x1 + 3 = 4#(2(2(3(4(x1)))))
    
    3#(5(1(x1))) = 4x1 + 17 >= 2 = 1#(0(1(x1)))
    
    3#(5(1(x1))) = 4x1 + 17 >= 1 = 4#(1(0(1(x1))))
    
    3#(5(1(x1))) = 4x1 + 17 >= 2 = 1#(4(1(0(1(x1)))))
    
    3#(5(1(x1))) = 4x1 + 17 >= 3 = 2#(1(4(1(0(1(x1))))))
    
    3#(5(2(x1))) = 4x1 + 17 >= 1x1 + 3 = 2#(2(x1))
    
    3#(5(2(x1))) = 4x1 + 17 >= 1x1 + 3 = 2#(2(2(x1)))
    
    3#(5(2(x1))) = 4x1 + 17 >= 2x1 + 4 = 3#(2(2(2(x1))))
    
    3#(5(2(x1))) = 4x1 + 17 >= 1x1 + 3 = 4#(3(2(2(2(x1)))))
    
    3#(5(2(x1))) = 4x1 + 17 >= 2 = 3#(0(x1))
    
    3#(5(2(x1))) = 4x1 + 17 >= 3 = 2#(3(0(x1)))
    
    3#(5(2(x1))) = 4x1 + 17 >= 3 = 2#(2(3(0(x1))))
    
    3#(5(2(x1))) = 4x1 + 17 >= 3 = 2#(0(2(2(3(0(x1))))))
    
    3#(5(2(x1))) = 4x1 + 17 >= 2x1 + 4 = 1#(2(x1))
    
    3#(5(2(x1))) = 4x1 + 17 >= 1x1 + 3 = 2#(1(2(x1)))
    
    3#(5(2(x1))) = 4x1 + 17 >= 2x1 + 4 = 3#(2(1(2(x1))))
    
    3#(5(2(x1))) = 4x1 + 17 >= 2x1 + 4 = 3#(3(2(1(2(x1)))))
    
    3#(5(2(x1))) = 4x1 + 17 >= 1x1 + 3 = 2#(3(3(2(1(2(x1))))))
    
    3#(5(3(x1))) = 4x1 + 17 >= 2 = 3#(0(x1))
    
    3#(5(3(x1))) = 4x1 + 17 >= 2 = 3#(3(0(x1)))
    
    3#(5(3(x1))) = 4x1 + 17 >= 1 = 4#(3(3(0(x1))))
    
    3#(5(3(x1))) = 4x1 + 17 >= 3 = 2#(4(3(3(0(x1)))))
    
    3#(5(3(x1))) = 4x1 + 17 >= 1 = 5#(4(3(3(0(x1)))))
    
    3#(5(3(x1))) = 4x1 + 17 >= 1x1 + 3 = 2#(x1)
    
    3#(5(3(x1))) = 4x1 + 17 >= 1x1 + 3 = 4#(2(x1))
    
    3#(5(3(x1))) = 4x1 + 17 >= 1 = 4#(0(4(2(x1))))
    
    3#(5(3(x1))) = 4x1 + 17 >= 2 = 3#(4(0(4(2(x1)))))
    
    3#(5(3(x1))) = 4x1 + 17 >= 3 = 2#(3(4(0(4(2(x1))))))
    
    3#(5(4(x1))) = 4x1 + 17 >= 1 = 5#(0(0(x1)))
    
    3#(5(4(x1))) = 4x1 + 17 >= 3 = 2#(0(5(0(0(x1)))))
    
    3#(5(4(x1))) = 4x1 + 17 >= 1x1 + 3 = 2#(x1)
    
    3#(5(4(x1))) = 4x1 + 17 >= 2x1 + 4 = 1#(2(x1))
    
    3#(5(4(x1))) = 4x1 + 17 >= 1 = 5#(0(0(1(2(x1)))))
    
    3#(5(5(x1))) = 6x1 + 19 >= 2 = 1#(0(5(x1)))
    
    3#(5(5(x1))) = 6x1 + 19 >= 1 = 4#(1(0(5(x1))))
    
    3#(5(5(x1))) = 6x1 + 19 >= 1 = 5#(4(1(0(5(x1)))))
    
    4#(5(1(x1))) = 3x1 + 16 >= 2x1 + 0 = 3#(x1)
    
    4#(5(1(x1))) = 3x1 + 16 >= 2x1 + 2 = 3#(3(x1))
    
    4#(5(1(x1))) = 3x1 + 16 >= 1x1 + 1 = 5#(3(3(x1)))
    
    4#(5(1(x1))) = 3x1 + 16 >= 2 = 1#(0(5(3(3(x1)))))
    
    4#(5(1(x1))) = 3x1 + 16 >= 3 = 2#(1(0(5(3(3(x1))))))
    
    4#(5(2(x1))) = 3x1 + 16 >= 1x1 + 0 = 4#(x1)
    
    4#(5(2(x1))) = 3x1 + 16 >= 2 = 1#(0(0(4(x1))))
    
    4#(5(2(x1))) = 3x1 + 16 >= 1 = 5#(1(0(0(4(x1)))))
    
    4#(5(4(x1))) = 3x1 + 16 >= 1x1 + 3 = 2#(x1)
    
    4#(5(4(x1))) = 3x1 + 16 >= 1x1 + 3 = 4#(2(x1))
    
    4#(5(4(x1))) = 3x1 + 16 >= 2 = 1#(0(4(2(x1))))
    
    4#(5(4(x1))) = 3x1 + 16 >= 3 = 2#(1(0(4(2(x1)))))
    
    4#(5(4(x1))) = 3x1 + 16 >= 3 = 2#(2(1(0(4(2(x1))))))
    
    4#(5(4(x1))) = 3x1 + 16 >= 3 = 2#(0(x1))
    
    4#(5(4(x1))) = 3x1 + 16 >= 4 = 3#(2(0(x1)))
    
    4#(5(4(x1))) = 3x1 + 16 >= 3 = 2#(0(3(2(0(x1)))))
    
    4#(5(4(x1))) = 3x1 + 16 >= 4 = 3#(2(0(3(2(0(x1))))))
    
    5#(5(3(x1))) = 3x1 + 16 >= 1x1 + 3 = 2#(x1)
    
    5#(5(3(x1))) = 3x1 + 16 >= 1x1 + 3 = 2#(2(x1))
    
    5#(5(3(x1))) = 3x1 + 16 >= 2x1 + 4 = 1#(2(2(x1)))
    
    5#(5(3(x1))) = 3x1 + 16 >= 2 = 1#(0(1(2(2(x1)))))
    
    5#(5(3(x1))) = 3x1 + 16 >= 1 = 5#(1(0(1(2(2(x1))))))
    
    5#(5(4(x1))) = 3x1 + 16 >= 1x1 + 3 = 2#(x1)
    
    5#(5(4(x1))) = 3x1 + 16 >= 1x1 + 3 = 2#(2(x1))
    
    5#(5(4(x1))) = 3x1 + 16 >= 1x1 + 3 = 4#(2(2(x1)))
    
    5#(5(4(x1))) = 3x1 + 16 >= 2 = 1#(0(4(2(2(x1)))))
    
    5#(5(4(x1))) = 3x1 + 16 >= 1 = 5#(1(0(4(2(2(x1))))))
    
    2(5(x1)) = 2x1 + 15 >= 0 = 1(3(3(0(1(0(x1))))))
    
    2(5(x1)) = 2x1 + 15 >= 2 = 2(2(0(5(0(1(x1))))))
    
    3(5(x1)) = 2x1 + 15 >= 2 = 1(3(2(0(0(1(x1))))))
    
    3(5(x1)) = 2x1 + 15 >= 2 = 3(2(0(5(3(0(x1))))))
    
    4(5(x1)) = 2x1 + 15 >= x1 + 2 = 2(2(1(3(2(1(x1))))))
    
    4(5(x1)) = 2x1 + 15 >= 2 = 3(2(0(5(0(0(x1))))))
    
    1(2(5(x1))) = 2x1 + 15 >= 0 = 1(0(5(0(5(4(x1))))))
    
    1(2(5(x1))) = 2x1 + 15 >= 2 = 1(2(2(1(0(1(x1))))))
    
    1(2(5(x1))) = 2x1 + 15 >= 2 = 2(0(1(3(1(0(x1))))))
    
    1(4(5(x1))) = 2x1 + 15 >= 2 = 1(2(4(0(2(1(x1))))))
    
    2(5(1(x1))) = 2x1 + 15 >= x1 + 2 = 2(2(2(1(2(3(x1))))))
    
    2(5(2(x1))) = 2x1 + 15 >= 0 = 4(0(2(2(3(3(x1))))))
    
    2(5(3(x1))) = 2x1 + 15 >= 2 = 2(0(4(1(3(3(x1))))))
    
    2(5(4(x1))) = 2x1 + 15 >= 2 = 2(0(5(1(0(1(x1))))))
    
    3(2(5(x1))) = 2x1 + 15 >= 2 = 3(2(0(1(0(5(x1))))))
    
    3(4(2(x1))) = x1 + 2 >= 0 = 3(4(0(2(2(2(x1))))))
    
    3(5(1(x1))) = 2x1 + 15 >= 0 = 0(4(2(0(0(5(x1))))))
    
    3(5(1(x1))) = 2x1 + 15 >= 0 = 0(4(2(2(3(4(x1))))))
    
    3(5(1(x1))) = 2x1 + 15 >= 2 = 2(1(4(1(0(1(x1))))))
    
    3(5(2(x1))) = 2x1 + 15 >= 0 = 0(4(3(2(2(2(x1))))))
    
    3(5(2(x1))) = 2x1 + 15 >= 2 = 2(0(2(2(3(0(x1))))))
    
    3(5(2(x1))) = 2x1 + 15 >= x1 + 2 = 2(3(3(2(1(2(x1))))))
    
    3(5(3(x1))) = 2x1 + 15 >= 0 = 0(2(4(3(3(0(x1))))))
    
    3(5(3(x1))) = 2x1 + 15 >= 0 = 0(5(4(3(3(0(x1))))))
    
    3(5(3(x1))) = 2x1 + 15 >= 2 = 2(3(4(0(4(2(x1))))))
    
    3(5(4(x1))) = 2x1 + 15 >= 0 = 0(2(0(5(0(0(x1))))))
    
    3(5(4(x1))) = 2x1 + 15 >= 0 = 0(5(0(0(1(2(x1))))))
    
    3(5(5(x1))) = 4x1 + 17 >= 0 = 0(5(4(1(0(5(x1))))))
    
    4(5(1(x1))) = 2x1 + 15 >= 2 = 2(1(0(5(3(3(x1))))))
    
    4(5(2(x1))) = 2x1 + 15 >= 0 = 0(5(1(0(0(4(x1))))))
    
    4(5(4(x1))) = 2x1 + 15 >= 2 = 2(2(1(0(4(2(x1))))))
    
    4(5(4(x1))) = 2x1 + 15 >= 2 = 3(2(0(3(2(0(x1))))))
    
    5(5(3(x1))) = 4x1 + 17 >= 15 = 5(1(0(1(2(2(x1))))))
    
    5(5(4(x1))) = 4x1 + 17 >= 15 = 5(1(0(4(2(2(x1))))))
   problem:
    DPs:
     
    TRS:
     2(5(x1)) -> 1(3(3(0(1(0(x1))))))
     2(5(x1)) -> 2(2(0(5(0(1(x1))))))
     3(5(x1)) -> 1(3(2(0(0(1(x1))))))
     3(5(x1)) -> 3(2(0(5(3(0(x1))))))
     4(5(x1)) -> 2(2(1(3(2(1(x1))))))
     4(5(x1)) -> 3(2(0(5(0(0(x1))))))
     1(2(5(x1))) -> 1(0(5(0(5(4(x1))))))
     1(2(5(x1))) -> 1(2(2(1(0(1(x1))))))
     1(2(5(x1))) -> 2(0(1(3(1(0(x1))))))
     1(4(5(x1))) -> 1(2(4(0(2(1(x1))))))
     2(5(1(x1))) -> 2(2(2(1(2(3(x1))))))
     2(5(2(x1))) -> 4(0(2(2(3(3(x1))))))
     2(5(3(x1))) -> 2(0(4(1(3(3(x1))))))
     2(5(4(x1))) -> 2(0(5(1(0(1(x1))))))
     3(2(5(x1))) -> 3(2(0(1(0(5(x1))))))
     3(4(2(x1))) -> 3(4(0(2(2(2(x1))))))
     3(5(1(x1))) -> 0(4(2(0(0(5(x1))))))
     3(5(1(x1))) -> 0(4(2(2(3(4(x1))))))
     3(5(1(x1))) -> 2(1(4(1(0(1(x1))))))
     3(5(2(x1))) -> 0(4(3(2(2(2(x1))))))
     3(5(2(x1))) -> 2(0(2(2(3(0(x1))))))
     3(5(2(x1))) -> 2(3(3(2(1(2(x1))))))
     3(5(3(x1))) -> 0(2(4(3(3(0(x1))))))
     3(5(3(x1))) -> 0(5(4(3(3(0(x1))))))
     3(5(3(x1))) -> 2(3(4(0(4(2(x1))))))
     3(5(4(x1))) -> 0(2(0(5(0(0(x1))))))
     3(5(4(x1))) -> 0(5(0(0(1(2(x1))))))
     3(5(5(x1))) -> 0(5(4(1(0(5(x1))))))
     4(5(1(x1))) -> 2(1(0(5(3(3(x1))))))
     4(5(2(x1))) -> 0(5(1(0(0(4(x1))))))
     4(5(4(x1))) -> 2(2(1(0(4(2(x1))))))
     4(5(4(x1))) -> 3(2(0(3(2(0(x1))))))
     5(5(3(x1))) -> 5(1(0(1(2(2(x1))))))
     5(5(4(x1))) -> 5(1(0(4(2(2(x1))))))
   Qed