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:
 String Reversal Processor:
  5(2(x1)) -> 0(1(0(3(3(1(x1))))))
  5(2(x1)) -> 1(0(5(0(2(2(x1))))))
  5(3(x1)) -> 1(0(0(2(3(1(x1))))))
  5(3(x1)) -> 0(3(5(0(2(3(x1))))))
  5(4(x1)) -> 1(2(3(1(2(2(x1))))))
  5(4(x1)) -> 0(0(5(0(2(3(x1))))))
  5(2(1(x1))) -> 4(5(0(5(0(1(x1))))))
  5(2(1(x1))) -> 1(0(1(2(2(1(x1))))))
  5(2(1(x1))) -> 0(1(3(1(0(2(x1))))))
  5(4(1(x1))) -> 1(2(0(4(2(1(x1))))))
  1(5(2(x1))) -> 3(2(1(2(2(2(x1))))))
  2(5(2(x1))) -> 3(3(2(2(0(4(x1))))))
  3(5(2(x1))) -> 3(3(1(4(0(2(x1))))))
  4(5(2(x1))) -> 1(0(1(5(0(2(x1))))))
  5(2(3(x1))) -> 5(0(1(0(2(3(x1))))))
  2(4(3(x1))) -> 2(2(2(0(4(3(x1))))))
  1(5(3(x1))) -> 5(0(0(2(4(0(x1))))))
  1(5(3(x1))) -> 4(3(2(2(4(0(x1))))))
  1(5(3(x1))) -> 1(0(1(4(1(2(x1))))))
  2(5(3(x1))) -> 2(2(2(3(4(0(x1))))))
  2(5(3(x1))) -> 0(3(2(2(0(2(x1))))))
  2(5(3(x1))) -> 2(1(2(3(3(2(x1))))))
  3(5(3(x1))) -> 0(3(3(4(2(0(x1))))))
  3(5(3(x1))) -> 0(3(3(4(5(0(x1))))))
  3(5(3(x1))) -> 2(4(0(4(3(2(x1))))))
  4(5(3(x1))) -> 0(0(5(0(2(0(x1))))))
  4(5(3(x1))) -> 2(1(0(0(5(0(x1))))))
  5(5(3(x1))) -> 5(0(1(4(5(0(x1))))))
  1(5(4(x1))) -> 3(3(5(0(1(2(x1))))))
  2(5(4(x1))) -> 4(0(0(1(5(0(x1))))))
  4(5(4(x1))) -> 2(4(0(1(2(2(x1))))))
  4(5(4(x1))) -> 0(2(3(0(2(3(x1))))))
  3(5(5(x1))) -> 2(2(1(0(1(5(x1))))))
  4(5(5(x1))) -> 2(2(4(0(1(5(x1))))))
  DP Processor:
   DPs:
    5#(2(x1)) -> 1#(x1)
    5#(2(x1)) -> 3#(1(x1))
    5#(2(x1)) -> 3#(3(1(x1)))
    5#(2(x1)) -> 1#(0(3(3(1(x1)))))
    5#(2(x1)) -> 2#(2(x1))
    5#(2(x1)) -> 5#(0(2(2(x1))))
    5#(2(x1)) -> 1#(0(5(0(2(2(x1))))))
    5#(3(x1)) -> 1#(x1)
    5#(3(x1)) -> 3#(1(x1))
    5#(3(x1)) -> 2#(3(1(x1)))
    5#(3(x1)) -> 1#(0(0(2(3(1(x1))))))
    5#(3(x1)) -> 2#(3(x1))
    5#(3(x1)) -> 5#(0(2(3(x1))))
    5#(3(x1)) -> 3#(5(0(2(3(x1)))))
    5#(4(x1)) -> 2#(x1)
    5#(4(x1)) -> 2#(2(x1))
    5#(4(x1)) -> 1#(2(2(x1)))
    5#(4(x1)) -> 3#(1(2(2(x1))))
    5#(4(x1)) -> 2#(3(1(2(2(x1)))))
    5#(4(x1)) -> 1#(2(3(1(2(2(x1))))))
    5#(4(x1)) -> 3#(x1)
    5#(4(x1)) -> 2#(3(x1))
    5#(4(x1)) -> 5#(0(2(3(x1))))
    5#(2(1(x1))) -> 5#(0(1(x1)))
    5#(2(1(x1))) -> 5#(0(5(0(1(x1)))))
    5#(2(1(x1))) -> 4#(5(0(5(0(1(x1))))))
    5#(2(1(x1))) -> 2#(2(1(x1)))
    5#(2(1(x1))) -> 1#(2(2(1(x1))))
    5#(2(1(x1))) -> 1#(0(1(2(2(1(x1))))))
    5#(2(1(x1))) -> 2#(x1)
    5#(2(1(x1))) -> 1#(0(2(x1)))
    5#(2(1(x1))) -> 3#(1(0(2(x1))))
    5#(2(1(x1))) -> 1#(3(1(0(2(x1)))))
    5#(4(1(x1))) -> 2#(1(x1))
    5#(4(1(x1))) -> 4#(2(1(x1)))
    5#(4(1(x1))) -> 2#(0(4(2(1(x1)))))
    5#(4(1(x1))) -> 1#(2(0(4(2(1(x1))))))
    1#(5(2(x1))) -> 2#(2(x1))
    1#(5(2(x1))) -> 2#(2(2(x1)))
    1#(5(2(x1))) -> 1#(2(2(2(x1))))
    1#(5(2(x1))) -> 2#(1(2(2(2(x1)))))
    1#(5(2(x1))) -> 3#(2(1(2(2(2(x1))))))
    2#(5(2(x1))) -> 4#(x1)
    2#(5(2(x1))) -> 2#(0(4(x1)))
    2#(5(2(x1))) -> 2#(2(0(4(x1))))
    2#(5(2(x1))) -> 3#(2(2(0(4(x1)))))
    2#(5(2(x1))) -> 3#(3(2(2(0(4(x1))))))
    3#(5(2(x1))) -> 4#(0(2(x1)))
    3#(5(2(x1))) -> 1#(4(0(2(x1))))
    3#(5(2(x1))) -> 3#(1(4(0(2(x1)))))
    3#(5(2(x1))) -> 3#(3(1(4(0(2(x1))))))
    4#(5(2(x1))) -> 5#(0(2(x1)))
    4#(5(2(x1))) -> 1#(5(0(2(x1))))
    4#(5(2(x1))) -> 1#(0(1(5(0(2(x1))))))
    5#(2(3(x1))) -> 1#(0(2(3(x1))))
    5#(2(3(x1))) -> 5#(0(1(0(2(3(x1))))))
    2#(4(3(x1))) -> 2#(0(4(3(x1))))
    2#(4(3(x1))) -> 2#(2(0(4(3(x1)))))
    2#(4(3(x1))) -> 2#(2(2(0(4(3(x1))))))
    1#(5(3(x1))) -> 4#(0(x1))
    1#(5(3(x1))) -> 2#(4(0(x1)))
    1#(5(3(x1))) -> 5#(0(0(2(4(0(x1))))))
    1#(5(3(x1))) -> 2#(2(4(0(x1))))
    1#(5(3(x1))) -> 3#(2(2(4(0(x1)))))
    1#(5(3(x1))) -> 4#(3(2(2(4(0(x1))))))
    1#(5(3(x1))) -> 2#(x1)
    1#(5(3(x1))) -> 1#(2(x1))
    1#(5(3(x1))) -> 4#(1(2(x1)))
    1#(5(3(x1))) -> 1#(4(1(2(x1))))
    1#(5(3(x1))) -> 1#(0(1(4(1(2(x1))))))
    2#(5(3(x1))) -> 4#(0(x1))
    2#(5(3(x1))) -> 3#(4(0(x1)))
    2#(5(3(x1))) -> 2#(3(4(0(x1))))
    2#(5(3(x1))) -> 2#(2(3(4(0(x1)))))
    2#(5(3(x1))) -> 2#(2(2(3(4(0(x1))))))
    2#(5(3(x1))) -> 2#(x1)
    2#(5(3(x1))) -> 2#(0(2(x1)))
    2#(5(3(x1))) -> 2#(2(0(2(x1))))
    2#(5(3(x1))) -> 3#(2(2(0(2(x1)))))
    2#(5(3(x1))) -> 3#(2(x1))
    2#(5(3(x1))) -> 3#(3(2(x1)))
    2#(5(3(x1))) -> 2#(3(3(2(x1))))
    2#(5(3(x1))) -> 1#(2(3(3(2(x1)))))
    2#(5(3(x1))) -> 2#(1(2(3(3(2(x1))))))
    3#(5(3(x1))) -> 2#(0(x1))
    3#(5(3(x1))) -> 4#(2(0(x1)))
    3#(5(3(x1))) -> 3#(4(2(0(x1))))
    3#(5(3(x1))) -> 3#(3(4(2(0(x1)))))
    3#(5(3(x1))) -> 5#(0(x1))
    3#(5(3(x1))) -> 4#(5(0(x1)))
    3#(5(3(x1))) -> 3#(4(5(0(x1))))
    3#(5(3(x1))) -> 3#(3(4(5(0(x1)))))
    3#(5(3(x1))) -> 2#(x1)
    3#(5(3(x1))) -> 3#(2(x1))
    3#(5(3(x1))) -> 4#(3(2(x1)))
    3#(5(3(x1))) -> 4#(0(4(3(2(x1)))))
    3#(5(3(x1))) -> 2#(4(0(4(3(2(x1))))))
    4#(5(3(x1))) -> 2#(0(x1))
    4#(5(3(x1))) -> 5#(0(2(0(x1))))
    4#(5(3(x1))) -> 5#(0(x1))
    4#(5(3(x1))) -> 1#(0(0(5(0(x1)))))
    4#(5(3(x1))) -> 2#(1(0(0(5(0(x1))))))
    5#(5(3(x1))) -> 5#(0(x1))
    5#(5(3(x1))) -> 4#(5(0(x1)))
    5#(5(3(x1))) -> 1#(4(5(0(x1))))
    5#(5(3(x1))) -> 5#(0(1(4(5(0(x1))))))
    1#(5(4(x1))) -> 2#(x1)
    1#(5(4(x1))) -> 1#(2(x1))
    1#(5(4(x1))) -> 5#(0(1(2(x1))))
    1#(5(4(x1))) -> 3#(5(0(1(2(x1)))))
    1#(5(4(x1))) -> 3#(3(5(0(1(2(x1))))))
    2#(5(4(x1))) -> 5#(0(x1))
    2#(5(4(x1))) -> 1#(5(0(x1)))
    2#(5(4(x1))) -> 4#(0(0(1(5(0(x1))))))
    4#(5(4(x1))) -> 2#(x1)
    4#(5(4(x1))) -> 2#(2(x1))
    4#(5(4(x1))) -> 1#(2(2(x1)))
    4#(5(4(x1))) -> 4#(0(1(2(2(x1)))))
    4#(5(4(x1))) -> 2#(4(0(1(2(2(x1))))))
    4#(5(4(x1))) -> 3#(x1)
    4#(5(4(x1))) -> 2#(3(x1))
    4#(5(4(x1))) -> 3#(0(2(3(x1))))
    4#(5(4(x1))) -> 2#(3(0(2(3(x1)))))
    3#(5(5(x1))) -> 1#(5(x1))
    3#(5(5(x1))) -> 1#(0(1(5(x1))))
    3#(5(5(x1))) -> 2#(1(0(1(5(x1)))))
    3#(5(5(x1))) -> 2#(2(1(0(1(5(x1))))))
    4#(5(5(x1))) -> 1#(5(x1))
    4#(5(5(x1))) -> 4#(0(1(5(x1))))
    4#(5(5(x1))) -> 2#(4(0(1(5(x1)))))
    4#(5(5(x1))) -> 2#(2(4(0(1(5(x1))))))
   TRS:
    5(2(x1)) -> 0(1(0(3(3(1(x1))))))
    5(2(x1)) -> 1(0(5(0(2(2(x1))))))
    5(3(x1)) -> 1(0(0(2(3(1(x1))))))
    5(3(x1)) -> 0(3(5(0(2(3(x1))))))
    5(4(x1)) -> 1(2(3(1(2(2(x1))))))
    5(4(x1)) -> 0(0(5(0(2(3(x1))))))
    5(2(1(x1))) -> 4(5(0(5(0(1(x1))))))
    5(2(1(x1))) -> 1(0(1(2(2(1(x1))))))
    5(2(1(x1))) -> 0(1(3(1(0(2(x1))))))
    5(4(1(x1))) -> 1(2(0(4(2(1(x1))))))
    1(5(2(x1))) -> 3(2(1(2(2(2(x1))))))
    2(5(2(x1))) -> 3(3(2(2(0(4(x1))))))
    3(5(2(x1))) -> 3(3(1(4(0(2(x1))))))
    4(5(2(x1))) -> 1(0(1(5(0(2(x1))))))
    5(2(3(x1))) -> 5(0(1(0(2(3(x1))))))
    2(4(3(x1))) -> 2(2(2(0(4(3(x1))))))
    1(5(3(x1))) -> 5(0(0(2(4(0(x1))))))
    1(5(3(x1))) -> 4(3(2(2(4(0(x1))))))
    1(5(3(x1))) -> 1(0(1(4(1(2(x1))))))
    2(5(3(x1))) -> 2(2(2(3(4(0(x1))))))
    2(5(3(x1))) -> 0(3(2(2(0(2(x1))))))
    2(5(3(x1))) -> 2(1(2(3(3(2(x1))))))
    3(5(3(x1))) -> 0(3(3(4(2(0(x1))))))
    3(5(3(x1))) -> 0(3(3(4(5(0(x1))))))
    3(5(3(x1))) -> 2(4(0(4(3(2(x1))))))
    4(5(3(x1))) -> 0(0(5(0(2(0(x1))))))
    4(5(3(x1))) -> 2(1(0(0(5(0(x1))))))
    5(5(3(x1))) -> 5(0(1(4(5(0(x1))))))
    1(5(4(x1))) -> 3(3(5(0(1(2(x1))))))
    2(5(4(x1))) -> 4(0(0(1(5(0(x1))))))
    4(5(4(x1))) -> 2(4(0(1(2(2(x1))))))
    4(5(4(x1))) -> 0(2(3(0(2(3(x1))))))
    3(5(5(x1))) -> 2(2(1(0(1(5(x1))))))
    4(5(5(x1))) -> 2(2(4(0(1(5(x1))))))
   TDG Processor:
    DPs:
     5#(2(x1)) -> 1#(x1)
     5#(2(x1)) -> 3#(1(x1))
     5#(2(x1)) -> 3#(3(1(x1)))
     5#(2(x1)) -> 1#(0(3(3(1(x1)))))
     5#(2(x1)) -> 2#(2(x1))
     5#(2(x1)) -> 5#(0(2(2(x1))))
     5#(2(x1)) -> 1#(0(5(0(2(2(x1))))))
     5#(3(x1)) -> 1#(x1)
     5#(3(x1)) -> 3#(1(x1))
     5#(3(x1)) -> 2#(3(1(x1)))
     5#(3(x1)) -> 1#(0(0(2(3(1(x1))))))
     5#(3(x1)) -> 2#(3(x1))
     5#(3(x1)) -> 5#(0(2(3(x1))))
     5#(3(x1)) -> 3#(5(0(2(3(x1)))))
     5#(4(x1)) -> 2#(x1)
     5#(4(x1)) -> 2#(2(x1))
     5#(4(x1)) -> 1#(2(2(x1)))
     5#(4(x1)) -> 3#(1(2(2(x1))))
     5#(4(x1)) -> 2#(3(1(2(2(x1)))))
     5#(4(x1)) -> 1#(2(3(1(2(2(x1))))))
     5#(4(x1)) -> 3#(x1)
     5#(4(x1)) -> 2#(3(x1))
     5#(4(x1)) -> 5#(0(2(3(x1))))
     5#(2(1(x1))) -> 5#(0(1(x1)))
     5#(2(1(x1))) -> 5#(0(5(0(1(x1)))))
     5#(2(1(x1))) -> 4#(5(0(5(0(1(x1))))))
     5#(2(1(x1))) -> 2#(2(1(x1)))
     5#(2(1(x1))) -> 1#(2(2(1(x1))))
     5#(2(1(x1))) -> 1#(0(1(2(2(1(x1))))))
     5#(2(1(x1))) -> 2#(x1)
     5#(2(1(x1))) -> 1#(0(2(x1)))
     5#(2(1(x1))) -> 3#(1(0(2(x1))))
     5#(2(1(x1))) -> 1#(3(1(0(2(x1)))))
     5#(4(1(x1))) -> 2#(1(x1))
     5#(4(1(x1))) -> 4#(2(1(x1)))
     5#(4(1(x1))) -> 2#(0(4(2(1(x1)))))
     5#(4(1(x1))) -> 1#(2(0(4(2(1(x1))))))
     1#(5(2(x1))) -> 2#(2(x1))
     1#(5(2(x1))) -> 2#(2(2(x1)))
     1#(5(2(x1))) -> 1#(2(2(2(x1))))
     1#(5(2(x1))) -> 2#(1(2(2(2(x1)))))
     1#(5(2(x1))) -> 3#(2(1(2(2(2(x1))))))
     2#(5(2(x1))) -> 4#(x1)
     2#(5(2(x1))) -> 2#(0(4(x1)))
     2#(5(2(x1))) -> 2#(2(0(4(x1))))
     2#(5(2(x1))) -> 3#(2(2(0(4(x1)))))
     2#(5(2(x1))) -> 3#(3(2(2(0(4(x1))))))
     3#(5(2(x1))) -> 4#(0(2(x1)))
     3#(5(2(x1))) -> 1#(4(0(2(x1))))
     3#(5(2(x1))) -> 3#(1(4(0(2(x1)))))
     3#(5(2(x1))) -> 3#(3(1(4(0(2(x1))))))
     4#(5(2(x1))) -> 5#(0(2(x1)))
     4#(5(2(x1))) -> 1#(5(0(2(x1))))
     4#(5(2(x1))) -> 1#(0(1(5(0(2(x1))))))
     5#(2(3(x1))) -> 1#(0(2(3(x1))))
     5#(2(3(x1))) -> 5#(0(1(0(2(3(x1))))))
     2#(4(3(x1))) -> 2#(0(4(3(x1))))
     2#(4(3(x1))) -> 2#(2(0(4(3(x1)))))
     2#(4(3(x1))) -> 2#(2(2(0(4(3(x1))))))
     1#(5(3(x1))) -> 4#(0(x1))
     1#(5(3(x1))) -> 2#(4(0(x1)))
     1#(5(3(x1))) -> 5#(0(0(2(4(0(x1))))))
     1#(5(3(x1))) -> 2#(2(4(0(x1))))
     1#(5(3(x1))) -> 3#(2(2(4(0(x1)))))
     1#(5(3(x1))) -> 4#(3(2(2(4(0(x1))))))
     1#(5(3(x1))) -> 2#(x1)
     1#(5(3(x1))) -> 1#(2(x1))
     1#(5(3(x1))) -> 4#(1(2(x1)))
     1#(5(3(x1))) -> 1#(4(1(2(x1))))
     1#(5(3(x1))) -> 1#(0(1(4(1(2(x1))))))
     2#(5(3(x1))) -> 4#(0(x1))
     2#(5(3(x1))) -> 3#(4(0(x1)))
     2#(5(3(x1))) -> 2#(3(4(0(x1))))
     2#(5(3(x1))) -> 2#(2(3(4(0(x1)))))
     2#(5(3(x1))) -> 2#(2(2(3(4(0(x1))))))
     2#(5(3(x1))) -> 2#(x1)
     2#(5(3(x1))) -> 2#(0(2(x1)))
     2#(5(3(x1))) -> 2#(2(0(2(x1))))
     2#(5(3(x1))) -> 3#(2(2(0(2(x1)))))
     2#(5(3(x1))) -> 3#(2(x1))
     2#(5(3(x1))) -> 3#(3(2(x1)))
     2#(5(3(x1))) -> 2#(3(3(2(x1))))
     2#(5(3(x1))) -> 1#(2(3(3(2(x1)))))
     2#(5(3(x1))) -> 2#(1(2(3(3(2(x1))))))
     3#(5(3(x1))) -> 2#(0(x1))
     3#(5(3(x1))) -> 4#(2(0(x1)))
     3#(5(3(x1))) -> 3#(4(2(0(x1))))
     3#(5(3(x1))) -> 3#(3(4(2(0(x1)))))
     3#(5(3(x1))) -> 5#(0(x1))
     3#(5(3(x1))) -> 4#(5(0(x1)))
     3#(5(3(x1))) -> 3#(4(5(0(x1))))
     3#(5(3(x1))) -> 3#(3(4(5(0(x1)))))
     3#(5(3(x1))) -> 2#(x1)
     3#(5(3(x1))) -> 3#(2(x1))
     3#(5(3(x1))) -> 4#(3(2(x1)))
     3#(5(3(x1))) -> 4#(0(4(3(2(x1)))))
     3#(5(3(x1))) -> 2#(4(0(4(3(2(x1))))))
     4#(5(3(x1))) -> 2#(0(x1))
     4#(5(3(x1))) -> 5#(0(2(0(x1))))
     4#(5(3(x1))) -> 5#(0(x1))
     4#(5(3(x1))) -> 1#(0(0(5(0(x1)))))
     4#(5(3(x1))) -> 2#(1(0(0(5(0(x1))))))
     5#(5(3(x1))) -> 5#(0(x1))
     5#(5(3(x1))) -> 4#(5(0(x1)))
     5#(5(3(x1))) -> 1#(4(5(0(x1))))
     5#(5(3(x1))) -> 5#(0(1(4(5(0(x1))))))
     1#(5(4(x1))) -> 2#(x1)
     1#(5(4(x1))) -> 1#(2(x1))
     1#(5(4(x1))) -> 5#(0(1(2(x1))))
     1#(5(4(x1))) -> 3#(5(0(1(2(x1)))))
     1#(5(4(x1))) -> 3#(3(5(0(1(2(x1))))))
     2#(5(4(x1))) -> 5#(0(x1))
     2#(5(4(x1))) -> 1#(5(0(x1)))
     2#(5(4(x1))) -> 4#(0(0(1(5(0(x1))))))
     4#(5(4(x1))) -> 2#(x1)
     4#(5(4(x1))) -> 2#(2(x1))
     4#(5(4(x1))) -> 1#(2(2(x1)))
     4#(5(4(x1))) -> 4#(0(1(2(2(x1)))))
     4#(5(4(x1))) -> 2#(4(0(1(2(2(x1))))))
     4#(5(4(x1))) -> 3#(x1)
     4#(5(4(x1))) -> 2#(3(x1))
     4#(5(4(x1))) -> 3#(0(2(3(x1))))
     4#(5(4(x1))) -> 2#(3(0(2(3(x1)))))
     3#(5(5(x1))) -> 1#(5(x1))
     3#(5(5(x1))) -> 1#(0(1(5(x1))))
     3#(5(5(x1))) -> 2#(1(0(1(5(x1)))))
     3#(5(5(x1))) -> 2#(2(1(0(1(5(x1))))))
     4#(5(5(x1))) -> 1#(5(x1))
     4#(5(5(x1))) -> 4#(0(1(5(x1))))
     4#(5(5(x1))) -> 2#(4(0(1(5(x1)))))
     4#(5(5(x1))) -> 2#(2(4(0(1(5(x1))))))
    TRS:
     5(2(x1)) -> 0(1(0(3(3(1(x1))))))
     5(2(x1)) -> 1(0(5(0(2(2(x1))))))
     5(3(x1)) -> 1(0(0(2(3(1(x1))))))
     5(3(x1)) -> 0(3(5(0(2(3(x1))))))
     5(4(x1)) -> 1(2(3(1(2(2(x1))))))
     5(4(x1)) -> 0(0(5(0(2(3(x1))))))
     5(2(1(x1))) -> 4(5(0(5(0(1(x1))))))
     5(2(1(x1))) -> 1(0(1(2(2(1(x1))))))
     5(2(1(x1))) -> 0(1(3(1(0(2(x1))))))
     5(4(1(x1))) -> 1(2(0(4(2(1(x1))))))
     1(5(2(x1))) -> 3(2(1(2(2(2(x1))))))
     2(5(2(x1))) -> 3(3(2(2(0(4(x1))))))
     3(5(2(x1))) -> 3(3(1(4(0(2(x1))))))
     4(5(2(x1))) -> 1(0(1(5(0(2(x1))))))
     5(2(3(x1))) -> 5(0(1(0(2(3(x1))))))
     2(4(3(x1))) -> 2(2(2(0(4(3(x1))))))
     1(5(3(x1))) -> 5(0(0(2(4(0(x1))))))
     1(5(3(x1))) -> 4(3(2(2(4(0(x1))))))
     1(5(3(x1))) -> 1(0(1(4(1(2(x1))))))
     2(5(3(x1))) -> 2(2(2(3(4(0(x1))))))
     2(5(3(x1))) -> 0(3(2(2(0(2(x1))))))
     2(5(3(x1))) -> 2(1(2(3(3(2(x1))))))
     3(5(3(x1))) -> 0(3(3(4(2(0(x1))))))
     3(5(3(x1))) -> 0(3(3(4(5(0(x1))))))
     3(5(3(x1))) -> 2(4(0(4(3(2(x1))))))
     4(5(3(x1))) -> 0(0(5(0(2(0(x1))))))
     4(5(3(x1))) -> 2(1(0(0(5(0(x1))))))
     5(5(3(x1))) -> 5(0(1(4(5(0(x1))))))
     1(5(4(x1))) -> 3(3(5(0(1(2(x1))))))
     2(5(4(x1))) -> 4(0(0(1(5(0(x1))))))
     4(5(4(x1))) -> 2(4(0(1(2(2(x1))))))
     4(5(4(x1))) -> 0(2(3(0(2(3(x1))))))
     3(5(5(x1))) -> 2(2(1(0(1(5(x1))))))
     4(5(5(x1))) -> 2(2(4(0(1(5(x1))))))
    graph:
     ...
    EDG Processor:
     DPs:
      5#(2(x1)) -> 1#(x1)
      5#(2(x1)) -> 3#(1(x1))
      5#(2(x1)) -> 3#(3(1(x1)))
      5#(2(x1)) -> 1#(0(3(3(1(x1)))))
      5#(2(x1)) -> 2#(2(x1))
      5#(2(x1)) -> 5#(0(2(2(x1))))
      5#(2(x1)) -> 1#(0(5(0(2(2(x1))))))
      5#(3(x1)) -> 1#(x1)
      5#(3(x1)) -> 3#(1(x1))
      5#(3(x1)) -> 2#(3(1(x1)))
      5#(3(x1)) -> 1#(0(0(2(3(1(x1))))))
      5#(3(x1)) -> 2#(3(x1))
      5#(3(x1)) -> 5#(0(2(3(x1))))
      5#(3(x1)) -> 3#(5(0(2(3(x1)))))
      5#(4(x1)) -> 2#(x1)
      5#(4(x1)) -> 2#(2(x1))
      5#(4(x1)) -> 1#(2(2(x1)))
      5#(4(x1)) -> 3#(1(2(2(x1))))
      5#(4(x1)) -> 2#(3(1(2(2(x1)))))
      5#(4(x1)) -> 1#(2(3(1(2(2(x1))))))
      5#(4(x1)) -> 3#(x1)
      5#(4(x1)) -> 2#(3(x1))
      5#(4(x1)) -> 5#(0(2(3(x1))))
      5#(2(1(x1))) -> 5#(0(1(x1)))
      5#(2(1(x1))) -> 5#(0(5(0(1(x1)))))
      5#(2(1(x1))) -> 4#(5(0(5(0(1(x1))))))
      5#(2(1(x1))) -> 2#(2(1(x1)))
      5#(2(1(x1))) -> 1#(2(2(1(x1))))
      5#(2(1(x1))) -> 1#(0(1(2(2(1(x1))))))
      5#(2(1(x1))) -> 2#(x1)
      5#(2(1(x1))) -> 1#(0(2(x1)))
      5#(2(1(x1))) -> 3#(1(0(2(x1))))
      5#(2(1(x1))) -> 1#(3(1(0(2(x1)))))
      5#(4(1(x1))) -> 2#(1(x1))
      5#(4(1(x1))) -> 4#(2(1(x1)))
      5#(4(1(x1))) -> 2#(0(4(2(1(x1)))))
      5#(4(1(x1))) -> 1#(2(0(4(2(1(x1))))))
      1#(5(2(x1))) -> 2#(2(x1))
      1#(5(2(x1))) -> 2#(2(2(x1)))
      1#(5(2(x1))) -> 1#(2(2(2(x1))))
      1#(5(2(x1))) -> 2#(1(2(2(2(x1)))))
      1#(5(2(x1))) -> 3#(2(1(2(2(2(x1))))))
      2#(5(2(x1))) -> 4#(x1)
      2#(5(2(x1))) -> 2#(0(4(x1)))
      2#(5(2(x1))) -> 2#(2(0(4(x1))))
      2#(5(2(x1))) -> 3#(2(2(0(4(x1)))))
      2#(5(2(x1))) -> 3#(3(2(2(0(4(x1))))))
      3#(5(2(x1))) -> 4#(0(2(x1)))
      3#(5(2(x1))) -> 1#(4(0(2(x1))))
      3#(5(2(x1))) -> 3#(1(4(0(2(x1)))))
      3#(5(2(x1))) -> 3#(3(1(4(0(2(x1))))))
      4#(5(2(x1))) -> 5#(0(2(x1)))
      4#(5(2(x1))) -> 1#(5(0(2(x1))))
      4#(5(2(x1))) -> 1#(0(1(5(0(2(x1))))))
      5#(2(3(x1))) -> 1#(0(2(3(x1))))
      5#(2(3(x1))) -> 5#(0(1(0(2(3(x1))))))
      2#(4(3(x1))) -> 2#(0(4(3(x1))))
      2#(4(3(x1))) -> 2#(2(0(4(3(x1)))))
      2#(4(3(x1))) -> 2#(2(2(0(4(3(x1))))))
      1#(5(3(x1))) -> 4#(0(x1))
      1#(5(3(x1))) -> 2#(4(0(x1)))
      1#(5(3(x1))) -> 5#(0(0(2(4(0(x1))))))
      1#(5(3(x1))) -> 2#(2(4(0(x1))))
      1#(5(3(x1))) -> 3#(2(2(4(0(x1)))))
      1#(5(3(x1))) -> 4#(3(2(2(4(0(x1))))))
      1#(5(3(x1))) -> 2#(x1)
      1#(5(3(x1))) -> 1#(2(x1))
      1#(5(3(x1))) -> 4#(1(2(x1)))
      1#(5(3(x1))) -> 1#(4(1(2(x1))))
      1#(5(3(x1))) -> 1#(0(1(4(1(2(x1))))))
      2#(5(3(x1))) -> 4#(0(x1))
      2#(5(3(x1))) -> 3#(4(0(x1)))
      2#(5(3(x1))) -> 2#(3(4(0(x1))))
      2#(5(3(x1))) -> 2#(2(3(4(0(x1)))))
      2#(5(3(x1))) -> 2#(2(2(3(4(0(x1))))))
      2#(5(3(x1))) -> 2#(x1)
      2#(5(3(x1))) -> 2#(0(2(x1)))
      2#(5(3(x1))) -> 2#(2(0(2(x1))))
      2#(5(3(x1))) -> 3#(2(2(0(2(x1)))))
      2#(5(3(x1))) -> 3#(2(x1))
      2#(5(3(x1))) -> 3#(3(2(x1)))
      2#(5(3(x1))) -> 2#(3(3(2(x1))))
      2#(5(3(x1))) -> 1#(2(3(3(2(x1)))))
      2#(5(3(x1))) -> 2#(1(2(3(3(2(x1))))))
      3#(5(3(x1))) -> 2#(0(x1))
      3#(5(3(x1))) -> 4#(2(0(x1)))
      3#(5(3(x1))) -> 3#(4(2(0(x1))))
      3#(5(3(x1))) -> 3#(3(4(2(0(x1)))))
      3#(5(3(x1))) -> 5#(0(x1))
      3#(5(3(x1))) -> 4#(5(0(x1)))
      3#(5(3(x1))) -> 3#(4(5(0(x1))))
      3#(5(3(x1))) -> 3#(3(4(5(0(x1)))))
      3#(5(3(x1))) -> 2#(x1)
      3#(5(3(x1))) -> 3#(2(x1))
      3#(5(3(x1))) -> 4#(3(2(x1)))
      3#(5(3(x1))) -> 4#(0(4(3(2(x1)))))
      3#(5(3(x1))) -> 2#(4(0(4(3(2(x1))))))
      4#(5(3(x1))) -> 2#(0(x1))
      4#(5(3(x1))) -> 5#(0(2(0(x1))))
      4#(5(3(x1))) -> 5#(0(x1))
      4#(5(3(x1))) -> 1#(0(0(5(0(x1)))))
      4#(5(3(x1))) -> 2#(1(0(0(5(0(x1))))))
      5#(5(3(x1))) -> 5#(0(x1))
      5#(5(3(x1))) -> 4#(5(0(x1)))
      5#(5(3(x1))) -> 1#(4(5(0(x1))))
      5#(5(3(x1))) -> 5#(0(1(4(5(0(x1))))))
      1#(5(4(x1))) -> 2#(x1)
      1#(5(4(x1))) -> 1#(2(x1))
      1#(5(4(x1))) -> 5#(0(1(2(x1))))
      1#(5(4(x1))) -> 3#(5(0(1(2(x1)))))
      1#(5(4(x1))) -> 3#(3(5(0(1(2(x1))))))
      2#(5(4(x1))) -> 5#(0(x1))
      2#(5(4(x1))) -> 1#(5(0(x1)))
      2#(5(4(x1))) -> 4#(0(0(1(5(0(x1))))))
      4#(5(4(x1))) -> 2#(x1)
      4#(5(4(x1))) -> 2#(2(x1))
      4#(5(4(x1))) -> 1#(2(2(x1)))
      4#(5(4(x1))) -> 4#(0(1(2(2(x1)))))
      4#(5(4(x1))) -> 2#(4(0(1(2(2(x1))))))
      4#(5(4(x1))) -> 3#(x1)
      4#(5(4(x1))) -> 2#(3(x1))
      4#(5(4(x1))) -> 3#(0(2(3(x1))))
      4#(5(4(x1))) -> 2#(3(0(2(3(x1)))))
      3#(5(5(x1))) -> 1#(5(x1))
      3#(5(5(x1))) -> 1#(0(1(5(x1))))
      3#(5(5(x1))) -> 2#(1(0(1(5(x1)))))
      3#(5(5(x1))) -> 2#(2(1(0(1(5(x1))))))
      4#(5(5(x1))) -> 1#(5(x1))
      4#(5(5(x1))) -> 4#(0(1(5(x1))))
      4#(5(5(x1))) -> 2#(4(0(1(5(x1)))))
      4#(5(5(x1))) -> 2#(2(4(0(1(5(x1))))))
     TRS:
      5(2(x1)) -> 0(1(0(3(3(1(x1))))))
      5(2(x1)) -> 1(0(5(0(2(2(x1))))))
      5(3(x1)) -> 1(0(0(2(3(1(x1))))))
      5(3(x1)) -> 0(3(5(0(2(3(x1))))))
      5(4(x1)) -> 1(2(3(1(2(2(x1))))))
      5(4(x1)) -> 0(0(5(0(2(3(x1))))))
      5(2(1(x1))) -> 4(5(0(5(0(1(x1))))))
      5(2(1(x1))) -> 1(0(1(2(2(1(x1))))))
      5(2(1(x1))) -> 0(1(3(1(0(2(x1))))))
      5(4(1(x1))) -> 1(2(0(4(2(1(x1))))))
      1(5(2(x1))) -> 3(2(1(2(2(2(x1))))))
      2(5(2(x1))) -> 3(3(2(2(0(4(x1))))))
      3(5(2(x1))) -> 3(3(1(4(0(2(x1))))))
      4(5(2(x1))) -> 1(0(1(5(0(2(x1))))))
      5(2(3(x1))) -> 5(0(1(0(2(3(x1))))))
      2(4(3(x1))) -> 2(2(2(0(4(3(x1))))))
      1(5(3(x1))) -> 5(0(0(2(4(0(x1))))))
      1(5(3(x1))) -> 4(3(2(2(4(0(x1))))))
      1(5(3(x1))) -> 1(0(1(4(1(2(x1))))))
      2(5(3(x1))) -> 2(2(2(3(4(0(x1))))))
      2(5(3(x1))) -> 0(3(2(2(0(2(x1))))))
      2(5(3(x1))) -> 2(1(2(3(3(2(x1))))))
      3(5(3(x1))) -> 0(3(3(4(2(0(x1))))))
      3(5(3(x1))) -> 0(3(3(4(5(0(x1))))))
      3(5(3(x1))) -> 2(4(0(4(3(2(x1))))))
      4(5(3(x1))) -> 0(0(5(0(2(0(x1))))))
      4(5(3(x1))) -> 2(1(0(0(5(0(x1))))))
      5(5(3(x1))) -> 5(0(1(4(5(0(x1))))))
      1(5(4(x1))) -> 3(3(5(0(1(2(x1))))))
      2(5(4(x1))) -> 4(0(0(1(5(0(x1))))))
      4(5(4(x1))) -> 2(4(0(1(2(2(x1))))))
      4(5(4(x1))) -> 0(2(3(0(2(3(x1))))))
      3(5(5(x1))) -> 2(2(1(0(1(5(x1))))))
      4(5(5(x1))) -> 2(2(4(0(1(5(x1))))))
     graph:
      ...
     SCC Processor:
      #sccs: 1
      #rules: 28
      #arcs: 1117/17161
      DPs:
       4#(5(4(x1))) -> 2#(3(x1))
       2#(5(3(x1))) -> 2#(1(2(3(3(2(x1))))))
       2#(5(3(x1))) -> 1#(2(3(3(2(x1)))))
       1#(5(4(x1))) -> 1#(2(x1))
       1#(5(4(x1))) -> 2#(x1)
       2#(5(3(x1))) -> 2#(3(3(2(x1))))
       2#(5(3(x1))) -> 3#(3(2(x1)))
       3#(5(5(x1))) -> 1#(5(x1))
       1#(5(3(x1))) -> 1#(4(1(2(x1))))
       1#(5(3(x1))) -> 4#(1(2(x1)))
       4#(5(5(x1))) -> 1#(5(x1))
       1#(5(3(x1))) -> 1#(2(x1))
       1#(5(3(x1))) -> 2#(x1)
       2#(5(3(x1))) -> 3#(2(x1))
       3#(5(3(x1))) -> 4#(3(2(x1)))
       4#(5(4(x1))) -> 3#(x1)
       3#(5(3(x1))) -> 3#(2(x1))
       3#(5(3(x1))) -> 2#(x1)
       2#(5(3(x1))) -> 2#(x1)
       2#(5(2(x1))) -> 4#(x1)
       4#(5(4(x1))) -> 1#(2(2(x1)))
       1#(5(2(x1))) -> 3#(2(1(2(2(2(x1))))))
       1#(5(2(x1))) -> 2#(1(2(2(2(x1)))))
       1#(5(2(x1))) -> 1#(2(2(2(x1))))
       1#(5(2(x1))) -> 2#(2(2(x1)))
       1#(5(2(x1))) -> 2#(2(x1))
       4#(5(4(x1))) -> 2#(2(x1))
       4#(5(4(x1))) -> 2#(x1)
      TRS:
       5(2(x1)) -> 0(1(0(3(3(1(x1))))))
       5(2(x1)) -> 1(0(5(0(2(2(x1))))))
       5(3(x1)) -> 1(0(0(2(3(1(x1))))))
       5(3(x1)) -> 0(3(5(0(2(3(x1))))))
       5(4(x1)) -> 1(2(3(1(2(2(x1))))))
       5(4(x1)) -> 0(0(5(0(2(3(x1))))))
       5(2(1(x1))) -> 4(5(0(5(0(1(x1))))))
       5(2(1(x1))) -> 1(0(1(2(2(1(x1))))))
       5(2(1(x1))) -> 0(1(3(1(0(2(x1))))))
       5(4(1(x1))) -> 1(2(0(4(2(1(x1))))))
       1(5(2(x1))) -> 3(2(1(2(2(2(x1))))))
       2(5(2(x1))) -> 3(3(2(2(0(4(x1))))))
       3(5(2(x1))) -> 3(3(1(4(0(2(x1))))))
       4(5(2(x1))) -> 1(0(1(5(0(2(x1))))))
       5(2(3(x1))) -> 5(0(1(0(2(3(x1))))))
       2(4(3(x1))) -> 2(2(2(0(4(3(x1))))))
       1(5(3(x1))) -> 5(0(0(2(4(0(x1))))))
       1(5(3(x1))) -> 4(3(2(2(4(0(x1))))))
       1(5(3(x1))) -> 1(0(1(4(1(2(x1))))))
       2(5(3(x1))) -> 2(2(2(3(4(0(x1))))))
       2(5(3(x1))) -> 0(3(2(2(0(2(x1))))))
       2(5(3(x1))) -> 2(1(2(3(3(2(x1))))))
       3(5(3(x1))) -> 0(3(3(4(2(0(x1))))))
       3(5(3(x1))) -> 0(3(3(4(5(0(x1))))))
       3(5(3(x1))) -> 2(4(0(4(3(2(x1))))))
       4(5(3(x1))) -> 0(0(5(0(2(0(x1))))))
       4(5(3(x1))) -> 2(1(0(0(5(0(x1))))))
       5(5(3(x1))) -> 5(0(1(4(5(0(x1))))))
       1(5(4(x1))) -> 3(3(5(0(1(2(x1))))))
       2(5(4(x1))) -> 4(0(0(1(5(0(x1))))))
       4(5(4(x1))) -> 2(4(0(1(2(2(x1))))))
       4(5(4(x1))) -> 0(2(3(0(2(3(x1))))))
       3(5(5(x1))) -> 2(2(1(0(1(5(x1))))))
       4(5(5(x1))) -> 2(2(4(0(1(5(x1))))))
      Arctic Interpretation Processor:
       dimension: 1
       interpretation:
        [4#](x0) = 3x0,
        
        [2#](x0) = x0 + 0,
        
        [3#](x0) = 3x0,
        
        [1#](x0) = x0,
        
        [4](x0) = x0,
        
        [3](x0) = x0 + 2,
        
        [1](x0) = x0,
        
        [0](x0) = 0,
        
        [2](x0) = x0,
        
        [5](x0) = 3x0 + 5
       orientation:
        4#(5(4(x1))) = 6x1 + 8 >= x1 + 2 = 2#(3(x1))
        
        2#(5(3(x1))) = 3x1 + 5 >= x1 + 2 = 2#(1(2(3(3(2(x1))))))
        
        2#(5(3(x1))) = 3x1 + 5 >= x1 + 2 = 1#(2(3(3(2(x1)))))
        
        1#(5(4(x1))) = 3x1 + 5 >= x1 = 1#(2(x1))
        
        1#(5(4(x1))) = 3x1 + 5 >= x1 + 0 = 2#(x1)
        
        2#(5(3(x1))) = 3x1 + 5 >= x1 + 2 = 2#(3(3(2(x1))))
        
        2#(5(3(x1))) = 3x1 + 5 >= 3x1 + 5 = 3#(3(2(x1)))
        
        3#(5(5(x1))) = 9x1 + 11 >= 3x1 + 5 = 1#(5(x1))
        
        1#(5(3(x1))) = 3x1 + 5 >= x1 = 1#(4(1(2(x1))))
        
        1#(5(3(x1))) = 3x1 + 5 >= 3x1 = 4#(1(2(x1)))
        
        4#(5(5(x1))) = 9x1 + 11 >= 3x1 + 5 = 1#(5(x1))
        
        1#(5(3(x1))) = 3x1 + 5 >= x1 = 1#(2(x1))
        
        1#(5(3(x1))) = 3x1 + 5 >= x1 + 0 = 2#(x1)
        
        2#(5(3(x1))) = 3x1 + 5 >= 3x1 = 3#(2(x1))
        
        3#(5(3(x1))) = 6x1 + 8 >= 3x1 + 5 = 4#(3(2(x1)))
        
        4#(5(4(x1))) = 6x1 + 8 >= 3x1 = 3#(x1)
        
        3#(5(3(x1))) = 6x1 + 8 >= 3x1 = 3#(2(x1))
        
        3#(5(3(x1))) = 6x1 + 8 >= x1 + 0 = 2#(x1)
        
        2#(5(3(x1))) = 3x1 + 5 >= x1 + 0 = 2#(x1)
        
        2#(5(2(x1))) = 3x1 + 5 >= 3x1 = 4#(x1)
        
        4#(5(4(x1))) = 6x1 + 8 >= x1 = 1#(2(2(x1)))
        
        1#(5(2(x1))) = 3x1 + 5 >= 3x1 = 3#(2(1(2(2(2(x1))))))
        
        1#(5(2(x1))) = 3x1 + 5 >= x1 + 0 = 2#(1(2(2(2(x1)))))
        
        1#(5(2(x1))) = 3x1 + 5 >= x1 = 1#(2(2(2(x1))))
        
        1#(5(2(x1))) = 3x1 + 5 >= x1 + 0 = 2#(2(2(x1)))
        
        1#(5(2(x1))) = 3x1 + 5 >= x1 + 0 = 2#(2(x1))
        
        4#(5(4(x1))) = 6x1 + 8 >= x1 + 0 = 2#(2(x1))
        
        4#(5(4(x1))) = 6x1 + 8 >= x1 + 0 = 2#(x1)
        
        5(2(x1)) = 3x1 + 5 >= 0 = 0(1(0(3(3(1(x1))))))
        
        5(2(x1)) = 3x1 + 5 >= 0 = 1(0(5(0(2(2(x1))))))
        
        5(3(x1)) = 3x1 + 5 >= 0 = 1(0(0(2(3(1(x1))))))
        
        5(3(x1)) = 3x1 + 5 >= 0 = 0(3(5(0(2(3(x1))))))
        
        5(4(x1)) = 3x1 + 5 >= x1 + 2 = 1(2(3(1(2(2(x1))))))
        
        5(4(x1)) = 3x1 + 5 >= 0 = 0(0(5(0(2(3(x1))))))
        
        5(2(1(x1))) = 3x1 + 5 >= 5 = 4(5(0(5(0(1(x1))))))
        
        5(2(1(x1))) = 3x1 + 5 >= 0 = 1(0(1(2(2(1(x1))))))
        
        5(2(1(x1))) = 3x1 + 5 >= 0 = 0(1(3(1(0(2(x1))))))
        
        5(4(1(x1))) = 3x1 + 5 >= 0 = 1(2(0(4(2(1(x1))))))
        
        1(5(2(x1))) = 3x1 + 5 >= x1 + 2 = 3(2(1(2(2(2(x1))))))
        
        2(5(2(x1))) = 3x1 + 5 >= 2 = 3(3(2(2(0(4(x1))))))
        
        3(5(2(x1))) = 3x1 + 5 >= 2 = 3(3(1(4(0(2(x1))))))
        
        4(5(2(x1))) = 3x1 + 5 >= 0 = 1(0(1(5(0(2(x1))))))
        
        5(2(3(x1))) = 3x1 + 5 >= 5 = 5(0(1(0(2(3(x1))))))
        
        2(4(3(x1))) = x1 + 2 >= 0 = 2(2(2(0(4(3(x1))))))
        
        1(5(3(x1))) = 3x1 + 5 >= 5 = 5(0(0(2(4(0(x1))))))
        
        1(5(3(x1))) = 3x1 + 5 >= 2 = 4(3(2(2(4(0(x1))))))
        
        1(5(3(x1))) = 3x1 + 5 >= 0 = 1(0(1(4(1(2(x1))))))
        
        2(5(3(x1))) = 3x1 + 5 >= 2 = 2(2(2(3(4(0(x1))))))
        
        2(5(3(x1))) = 3x1 + 5 >= 0 = 0(3(2(2(0(2(x1))))))
        
        2(5(3(x1))) = 3x1 + 5 >= x1 + 2 = 2(1(2(3(3(2(x1))))))
        
        3(5(3(x1))) = 3x1 + 5 >= 0 = 0(3(3(4(2(0(x1))))))
        
        3(5(3(x1))) = 3x1 + 5 >= 0 = 0(3(3(4(5(0(x1))))))
        
        3(5(3(x1))) = 3x1 + 5 >= 0 = 2(4(0(4(3(2(x1))))))
        
        4(5(3(x1))) = 3x1 + 5 >= 0 = 0(0(5(0(2(0(x1))))))
        
        4(5(3(x1))) = 3x1 + 5 >= 0 = 2(1(0(0(5(0(x1))))))
        
        5(5(3(x1))) = 6x1 + 8 >= 5 = 5(0(1(4(5(0(x1))))))
        
        1(5(4(x1))) = 3x1 + 5 >= 5 = 3(3(5(0(1(2(x1))))))
        
        2(5(4(x1))) = 3x1 + 5 >= 0 = 4(0(0(1(5(0(x1))))))
        
        4(5(4(x1))) = 3x1 + 5 >= 0 = 2(4(0(1(2(2(x1))))))
        
        4(5(4(x1))) = 3x1 + 5 >= 0 = 0(2(3(0(2(3(x1))))))
        
        3(5(5(x1))) = 6x1 + 8 >= 0 = 2(2(1(0(1(5(x1))))))
        
        4(5(5(x1))) = 6x1 + 8 >= 0 = 2(2(4(0(1(5(x1))))))
       problem:
        DPs:
         2#(5(3(x1))) -> 3#(3(2(x1)))
         1#(5(3(x1))) -> 4#(1(2(x1)))
         2#(5(3(x1))) -> 3#(2(x1))
         2#(5(2(x1))) -> 4#(x1)
         1#(5(2(x1))) -> 3#(2(1(2(2(2(x1))))))
        TRS:
         5(2(x1)) -> 0(1(0(3(3(1(x1))))))
         5(2(x1)) -> 1(0(5(0(2(2(x1))))))
         5(3(x1)) -> 1(0(0(2(3(1(x1))))))
         5(3(x1)) -> 0(3(5(0(2(3(x1))))))
         5(4(x1)) -> 1(2(3(1(2(2(x1))))))
         5(4(x1)) -> 0(0(5(0(2(3(x1))))))
         5(2(1(x1))) -> 4(5(0(5(0(1(x1))))))
         5(2(1(x1))) -> 1(0(1(2(2(1(x1))))))
         5(2(1(x1))) -> 0(1(3(1(0(2(x1))))))
         5(4(1(x1))) -> 1(2(0(4(2(1(x1))))))
         1(5(2(x1))) -> 3(2(1(2(2(2(x1))))))
         2(5(2(x1))) -> 3(3(2(2(0(4(x1))))))
         3(5(2(x1))) -> 3(3(1(4(0(2(x1))))))
         4(5(2(x1))) -> 1(0(1(5(0(2(x1))))))
         5(2(3(x1))) -> 5(0(1(0(2(3(x1))))))
         2(4(3(x1))) -> 2(2(2(0(4(3(x1))))))
         1(5(3(x1))) -> 5(0(0(2(4(0(x1))))))
         1(5(3(x1))) -> 4(3(2(2(4(0(x1))))))
         1(5(3(x1))) -> 1(0(1(4(1(2(x1))))))
         2(5(3(x1))) -> 2(2(2(3(4(0(x1))))))
         2(5(3(x1))) -> 0(3(2(2(0(2(x1))))))
         2(5(3(x1))) -> 2(1(2(3(3(2(x1))))))
         3(5(3(x1))) -> 0(3(3(4(2(0(x1))))))
         3(5(3(x1))) -> 0(3(3(4(5(0(x1))))))
         3(5(3(x1))) -> 2(4(0(4(3(2(x1))))))
         4(5(3(x1))) -> 0(0(5(0(2(0(x1))))))
         4(5(3(x1))) -> 2(1(0(0(5(0(x1))))))
         5(5(3(x1))) -> 5(0(1(4(5(0(x1))))))
         1(5(4(x1))) -> 3(3(5(0(1(2(x1))))))
         2(5(4(x1))) -> 4(0(0(1(5(0(x1))))))
         4(5(4(x1))) -> 2(4(0(1(2(2(x1))))))
         4(5(4(x1))) -> 0(2(3(0(2(3(x1))))))
         3(5(5(x1))) -> 2(2(1(0(1(5(x1))))))
         4(5(5(x1))) -> 2(2(4(0(1(5(x1))))))
       EDG Processor:
        DPs:
         2#(5(3(x1))) -> 3#(3(2(x1)))
         1#(5(3(x1))) -> 4#(1(2(x1)))
         2#(5(3(x1))) -> 3#(2(x1))
         2#(5(2(x1))) -> 4#(x1)
         1#(5(2(x1))) -> 3#(2(1(2(2(2(x1))))))
        TRS:
         5(2(x1)) -> 0(1(0(3(3(1(x1))))))
         5(2(x1)) -> 1(0(5(0(2(2(x1))))))
         5(3(x1)) -> 1(0(0(2(3(1(x1))))))
         5(3(x1)) -> 0(3(5(0(2(3(x1))))))
         5(4(x1)) -> 1(2(3(1(2(2(x1))))))
         5(4(x1)) -> 0(0(5(0(2(3(x1))))))
         5(2(1(x1))) -> 4(5(0(5(0(1(x1))))))
         5(2(1(x1))) -> 1(0(1(2(2(1(x1))))))
         5(2(1(x1))) -> 0(1(3(1(0(2(x1))))))
         5(4(1(x1))) -> 1(2(0(4(2(1(x1))))))
         1(5(2(x1))) -> 3(2(1(2(2(2(x1))))))
         2(5(2(x1))) -> 3(3(2(2(0(4(x1))))))
         3(5(2(x1))) -> 3(3(1(4(0(2(x1))))))
         4(5(2(x1))) -> 1(0(1(5(0(2(x1))))))
         5(2(3(x1))) -> 5(0(1(0(2(3(x1))))))
         2(4(3(x1))) -> 2(2(2(0(4(3(x1))))))
         1(5(3(x1))) -> 5(0(0(2(4(0(x1))))))
         1(5(3(x1))) -> 4(3(2(2(4(0(x1))))))
         1(5(3(x1))) -> 1(0(1(4(1(2(x1))))))
         2(5(3(x1))) -> 2(2(2(3(4(0(x1))))))
         2(5(3(x1))) -> 0(3(2(2(0(2(x1))))))
         2(5(3(x1))) -> 2(1(2(3(3(2(x1))))))
         3(5(3(x1))) -> 0(3(3(4(2(0(x1))))))
         3(5(3(x1))) -> 0(3(3(4(5(0(x1))))))
         3(5(3(x1))) -> 2(4(0(4(3(2(x1))))))
         4(5(3(x1))) -> 0(0(5(0(2(0(x1))))))
         4(5(3(x1))) -> 2(1(0(0(5(0(x1))))))
         5(5(3(x1))) -> 5(0(1(4(5(0(x1))))))
         1(5(4(x1))) -> 3(3(5(0(1(2(x1))))))
         2(5(4(x1))) -> 4(0(0(1(5(0(x1))))))
         4(5(4(x1))) -> 2(4(0(1(2(2(x1))))))
         4(5(4(x1))) -> 0(2(3(0(2(3(x1))))))
         3(5(5(x1))) -> 2(2(1(0(1(5(x1))))))
         4(5(5(x1))) -> 2(2(4(0(1(5(x1))))))
        graph:
         
        Qed