YES

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

Proof:
 String Reversal Processor:
  2(1(0(0(x1)))) -> 0(0(1(3(2(x1)))))
  2(1(0(0(x1)))) -> 2(0(0(1(3(x1)))))
  2(1(0(0(x1)))) -> 1(1(3(2(0(0(x1))))))
  4(0(1(0(x1)))) -> 0(0(4(1(3(x1)))))
  4(0(1(0(x1)))) -> 1(3(0(0(4(3(x1))))))
  4(0(1(0(x1)))) -> 0(5(0(1(3(4(x1))))))
  4(0(1(0(x1)))) -> 0(1(3(4(0(5(x1))))))
  5(0(1(0(x1)))) -> 0(0(1(3(5(3(x1))))))
  5(0(1(0(x1)))) -> 2(0(0(1(3(5(x1))))))
  2(4(1(0(x1)))) -> 0(4(1(3(2(x1)))))
  2(4(1(0(x1)))) -> 4(2(1(3(0(4(x1))))))
  2(4(1(0(x1)))) -> 2(0(1(1(3(4(x1))))))
  4(0(5(0(x1)))) -> 5(3(0(0(4(x1)))))
  4(0(5(0(x1)))) -> 4(3(0(0(5(x1)))))
  5(0(5(0(x1)))) -> 5(0(0(2(5(3(x1))))))
  5(0(5(0(x1)))) -> 0(0(4(5(3(5(x1))))))
  5(0(5(0(x1)))) -> 0(0(4(3(5(5(x1))))))
  2(1(0(2(x1)))) -> 2(1(4(2(0(x1)))))
  2(1(0(2(x1)))) -> 1(2(2(0(5(2(x1))))))
  2(1(0(2(x1)))) -> 0(2(2(3(1(3(x1))))))
  2(4(0(2(x1)))) -> 1(2(2(0(4(x1)))))
  2(4(0(2(x1)))) -> 1(2(1(2(0(4(x1))))))
  2(5(0(2(x1)))) -> 2(2(5(1(2(0(x1))))))
  2(4(0(3(x1)))) -> 2(1(1(4(3(0(x1))))))
  2(4(0(3(x1)))) -> 2(0(1(3(3(4(x1))))))
  2(2(1(0(0(x1))))) -> 1(2(1(2(0(0(x1))))))
  2(3(1(0(0(x1))))) -> 4(0(2(1(3(0(x1))))))
  2(3(1(0(0(x1))))) -> 0(1(3(0(5(2(x1))))))
  2(2(5(0(0(x1))))) -> 1(2(5(2(0(0(x1))))))
  2(5(0(1(0(x1))))) -> 5(3(0(1(2(0(x1))))))
  5(5(0(1(0(x1))))) -> 5(0(0(5(3(1(x1))))))
  5(0(2(1(0(x1))))) -> 0(1(2(5(0(4(x1))))))
  4(0(3(1(0(x1))))) -> 0(4(4(3(0(1(x1))))))
  2(4(3(1(0(x1))))) -> 4(3(0(1(2(4(x1))))))
  2(2(4(1(0(x1))))) -> 2(4(2(0(1(1(x1))))))
  4(2(4(1(0(x1))))) -> 4(1(3(2(0(4(x1))))))
  2(3(4(1(0(x1))))) -> 4(4(0(2(1(3(x1))))))
  5(0(0(3(0(x1))))) -> 0(0(0(1(3(5(x1))))))
  4(0(1(4(0(x1))))) -> 0(4(1(2(0(4(x1))))))
  2(2(3(4(0(x1))))) -> 2(5(3(0(2(4(x1))))))
  4(0(1(5(0(x1))))) -> 0(0(1(4(2(5(x1))))))
  2(4(1(5(0(x1))))) -> 2(1(5(3(0(4(x1))))))
  2(1(0(1(2(x1))))) -> 3(2(0(1(1(2(x1))))))
  2(5(0(4(2(x1))))) -> 2(5(3(2(4(0(x1))))))
  2(1(0(0(3(x1))))) -> 2(0(1(5(3(0(x1))))))
  2(5(0(0(3(x1))))) -> 1(5(3(0(0(2(x1))))))
  2(4(5(0(3(x1))))) -> 1(2(5(3(0(4(x1))))))
  2(1(0(2(3(x1))))) -> 2(0(1(3(1(2(x1))))))
  2(5(0(2(3(x1))))) -> 5(4(3(2(0(2(x1))))))
  2(5(0(2(3(x1))))) -> 2(2(2(0(3(5(x1))))))
  DP Processor:
   DPs:
    2#(1(0(0(x1)))) -> 2#(x1)
    2#(1(0(0(x1)))) -> 2#(0(0(1(3(x1)))))
    2#(1(0(0(x1)))) -> 2#(0(0(x1)))
    4#(0(1(0(x1)))) -> 4#(1(3(x1)))
    4#(0(1(0(x1)))) -> 4#(3(x1))
    4#(0(1(0(x1)))) -> 4#(x1)
    4#(0(1(0(x1)))) -> 5#(0(1(3(4(x1)))))
    4#(0(1(0(x1)))) -> 5#(x1)
    4#(0(1(0(x1)))) -> 4#(0(5(x1)))
    5#(0(1(0(x1)))) -> 5#(3(x1))
    5#(0(1(0(x1)))) -> 5#(x1)
    5#(0(1(0(x1)))) -> 2#(0(0(1(3(5(x1))))))
    2#(4(1(0(x1)))) -> 2#(x1)
    2#(4(1(0(x1)))) -> 4#(1(3(2(x1))))
    2#(4(1(0(x1)))) -> 4#(x1)
    2#(4(1(0(x1)))) -> 2#(1(3(0(4(x1)))))
    2#(4(1(0(x1)))) -> 4#(2(1(3(0(4(x1))))))
    2#(4(1(0(x1)))) -> 2#(0(1(1(3(4(x1))))))
    4#(0(5(0(x1)))) -> 4#(x1)
    4#(0(5(0(x1)))) -> 5#(3(0(0(4(x1)))))
    4#(0(5(0(x1)))) -> 5#(x1)
    4#(0(5(0(x1)))) -> 4#(3(0(0(5(x1)))))
    5#(0(5(0(x1)))) -> 5#(3(x1))
    5#(0(5(0(x1)))) -> 2#(5(3(x1)))
    5#(0(5(0(x1)))) -> 5#(0(0(2(5(3(x1))))))
    5#(0(5(0(x1)))) -> 5#(x1)
    5#(0(5(0(x1)))) -> 5#(3(5(x1)))
    5#(0(5(0(x1)))) -> 4#(5(3(5(x1))))
    5#(0(5(0(x1)))) -> 5#(5(x1))
    5#(0(5(0(x1)))) -> 4#(3(5(5(x1))))
    2#(1(0(2(x1)))) -> 2#(0(x1))
    2#(1(0(2(x1)))) -> 4#(2(0(x1)))
    2#(1(0(2(x1)))) -> 2#(1(4(2(0(x1)))))
    2#(1(0(2(x1)))) -> 5#(2(x1))
    2#(1(0(2(x1)))) -> 2#(0(5(2(x1))))
    2#(1(0(2(x1)))) -> 2#(2(0(5(2(x1)))))
    2#(1(0(2(x1)))) -> 2#(3(1(3(x1))))
    2#(1(0(2(x1)))) -> 2#(2(3(1(3(x1)))))
    2#(4(0(2(x1)))) -> 4#(x1)
    2#(4(0(2(x1)))) -> 2#(0(4(x1)))
    2#(4(0(2(x1)))) -> 2#(2(0(4(x1))))
    2#(4(0(2(x1)))) -> 2#(1(2(0(4(x1)))))
    2#(5(0(2(x1)))) -> 2#(0(x1))
    2#(5(0(2(x1)))) -> 5#(1(2(0(x1))))
    2#(5(0(2(x1)))) -> 2#(5(1(2(0(x1)))))
    2#(5(0(2(x1)))) -> 2#(2(5(1(2(0(x1))))))
    2#(4(0(3(x1)))) -> 4#(3(0(x1)))
    2#(4(0(3(x1)))) -> 2#(1(1(4(3(0(x1))))))
    2#(4(0(3(x1)))) -> 4#(x1)
    2#(4(0(3(x1)))) -> 2#(0(1(3(3(4(x1))))))
    2#(2(1(0(0(x1))))) -> 2#(0(0(x1)))
    2#(2(1(0(0(x1))))) -> 2#(1(2(0(0(x1)))))
    2#(3(1(0(0(x1))))) -> 2#(1(3(0(x1))))
    2#(3(1(0(0(x1))))) -> 4#(0(2(1(3(0(x1))))))
    2#(3(1(0(0(x1))))) -> 2#(x1)
    2#(3(1(0(0(x1))))) -> 5#(2(x1))
    2#(2(5(0(0(x1))))) -> 2#(0(0(x1)))
    2#(2(5(0(0(x1))))) -> 5#(2(0(0(x1))))
    2#(2(5(0(0(x1))))) -> 2#(5(2(0(0(x1)))))
    2#(5(0(1(0(x1))))) -> 2#(0(x1))
    2#(5(0(1(0(x1))))) -> 5#(3(0(1(2(0(x1))))))
    5#(5(0(1(0(x1))))) -> 5#(3(1(x1)))
    5#(5(0(1(0(x1))))) -> 5#(0(0(5(3(1(x1))))))
    5#(0(2(1(0(x1))))) -> 4#(x1)
    5#(0(2(1(0(x1))))) -> 5#(0(4(x1)))
    5#(0(2(1(0(x1))))) -> 2#(5(0(4(x1))))
    4#(0(3(1(0(x1))))) -> 4#(3(0(1(x1))))
    4#(0(3(1(0(x1))))) -> 4#(4(3(0(1(x1)))))
    2#(4(3(1(0(x1))))) -> 4#(x1)
    2#(4(3(1(0(x1))))) -> 2#(4(x1))
    2#(4(3(1(0(x1))))) -> 4#(3(0(1(2(4(x1))))))
    2#(2(4(1(0(x1))))) -> 2#(0(1(1(x1))))
    2#(2(4(1(0(x1))))) -> 4#(2(0(1(1(x1)))))
    2#(2(4(1(0(x1))))) -> 2#(4(2(0(1(1(x1))))))
    4#(2(4(1(0(x1))))) -> 4#(x1)
    4#(2(4(1(0(x1))))) -> 2#(0(4(x1)))
    4#(2(4(1(0(x1))))) -> 4#(1(3(2(0(4(x1))))))
    2#(3(4(1(0(x1))))) -> 2#(1(3(x1)))
    2#(3(4(1(0(x1))))) -> 4#(0(2(1(3(x1)))))
    2#(3(4(1(0(x1))))) -> 4#(4(0(2(1(3(x1))))))
    5#(0(0(3(0(x1))))) -> 5#(x1)
    4#(0(1(4(0(x1))))) -> 4#(x1)
    4#(0(1(4(0(x1))))) -> 2#(0(4(x1)))
    4#(0(1(4(0(x1))))) -> 4#(1(2(0(4(x1)))))
    2#(2(3(4(0(x1))))) -> 4#(x1)
    2#(2(3(4(0(x1))))) -> 2#(4(x1))
    2#(2(3(4(0(x1))))) -> 5#(3(0(2(4(x1)))))
    2#(2(3(4(0(x1))))) -> 2#(5(3(0(2(4(x1))))))
    4#(0(1(5(0(x1))))) -> 5#(x1)
    4#(0(1(5(0(x1))))) -> 2#(5(x1))
    4#(0(1(5(0(x1))))) -> 4#(2(5(x1)))
    2#(4(1(5(0(x1))))) -> 4#(x1)
    2#(4(1(5(0(x1))))) -> 5#(3(0(4(x1))))
    2#(4(1(5(0(x1))))) -> 2#(1(5(3(0(4(x1))))))
    2#(1(0(1(2(x1))))) -> 2#(0(1(1(2(x1)))))
    2#(5(0(4(2(x1))))) -> 4#(0(x1))
    2#(5(0(4(2(x1))))) -> 2#(4(0(x1)))
    2#(5(0(4(2(x1))))) -> 5#(3(2(4(0(x1)))))
    2#(5(0(4(2(x1))))) -> 2#(5(3(2(4(0(x1))))))
    2#(1(0(0(3(x1))))) -> 5#(3(0(x1)))
    2#(1(0(0(3(x1))))) -> 2#(0(1(5(3(0(x1))))))
    2#(5(0(0(3(x1))))) -> 2#(x1)
    2#(5(0(0(3(x1))))) -> 5#(3(0(0(2(x1)))))
    2#(4(5(0(3(x1))))) -> 4#(x1)
    2#(4(5(0(3(x1))))) -> 5#(3(0(4(x1))))
    2#(4(5(0(3(x1))))) -> 2#(5(3(0(4(x1)))))
    2#(1(0(2(3(x1))))) -> 2#(x1)
    2#(1(0(2(3(x1))))) -> 2#(0(1(3(1(2(x1))))))
    2#(5(0(2(3(x1))))) -> 2#(x1)
    2#(5(0(2(3(x1))))) -> 2#(0(2(x1)))
    2#(5(0(2(3(x1))))) -> 4#(3(2(0(2(x1)))))
    2#(5(0(2(3(x1))))) -> 5#(4(3(2(0(2(x1))))))
    2#(5(0(2(3(x1))))) -> 5#(x1)
    2#(5(0(2(3(x1))))) -> 2#(0(3(5(x1))))
    2#(5(0(2(3(x1))))) -> 2#(2(0(3(5(x1)))))
    2#(5(0(2(3(x1))))) -> 2#(2(2(0(3(5(x1))))))
   TRS:
    2(1(0(0(x1)))) -> 0(0(1(3(2(x1)))))
    2(1(0(0(x1)))) -> 2(0(0(1(3(x1)))))
    2(1(0(0(x1)))) -> 1(1(3(2(0(0(x1))))))
    4(0(1(0(x1)))) -> 0(0(4(1(3(x1)))))
    4(0(1(0(x1)))) -> 1(3(0(0(4(3(x1))))))
    4(0(1(0(x1)))) -> 0(5(0(1(3(4(x1))))))
    4(0(1(0(x1)))) -> 0(1(3(4(0(5(x1))))))
    5(0(1(0(x1)))) -> 0(0(1(3(5(3(x1))))))
    5(0(1(0(x1)))) -> 2(0(0(1(3(5(x1))))))
    2(4(1(0(x1)))) -> 0(4(1(3(2(x1)))))
    2(4(1(0(x1)))) -> 4(2(1(3(0(4(x1))))))
    2(4(1(0(x1)))) -> 2(0(1(1(3(4(x1))))))
    4(0(5(0(x1)))) -> 5(3(0(0(4(x1)))))
    4(0(5(0(x1)))) -> 4(3(0(0(5(x1)))))
    5(0(5(0(x1)))) -> 5(0(0(2(5(3(x1))))))
    5(0(5(0(x1)))) -> 0(0(4(5(3(5(x1))))))
    5(0(5(0(x1)))) -> 0(0(4(3(5(5(x1))))))
    2(1(0(2(x1)))) -> 2(1(4(2(0(x1)))))
    2(1(0(2(x1)))) -> 1(2(2(0(5(2(x1))))))
    2(1(0(2(x1)))) -> 0(2(2(3(1(3(x1))))))
    2(4(0(2(x1)))) -> 1(2(2(0(4(x1)))))
    2(4(0(2(x1)))) -> 1(2(1(2(0(4(x1))))))
    2(5(0(2(x1)))) -> 2(2(5(1(2(0(x1))))))
    2(4(0(3(x1)))) -> 2(1(1(4(3(0(x1))))))
    2(4(0(3(x1)))) -> 2(0(1(3(3(4(x1))))))
    2(2(1(0(0(x1))))) -> 1(2(1(2(0(0(x1))))))
    2(3(1(0(0(x1))))) -> 4(0(2(1(3(0(x1))))))
    2(3(1(0(0(x1))))) -> 0(1(3(0(5(2(x1))))))
    2(2(5(0(0(x1))))) -> 1(2(5(2(0(0(x1))))))
    2(5(0(1(0(x1))))) -> 5(3(0(1(2(0(x1))))))
    5(5(0(1(0(x1))))) -> 5(0(0(5(3(1(x1))))))
    5(0(2(1(0(x1))))) -> 0(1(2(5(0(4(x1))))))
    4(0(3(1(0(x1))))) -> 0(4(4(3(0(1(x1))))))
    2(4(3(1(0(x1))))) -> 4(3(0(1(2(4(x1))))))
    2(2(4(1(0(x1))))) -> 2(4(2(0(1(1(x1))))))
    4(2(4(1(0(x1))))) -> 4(1(3(2(0(4(x1))))))
    2(3(4(1(0(x1))))) -> 4(4(0(2(1(3(x1))))))
    5(0(0(3(0(x1))))) -> 0(0(0(1(3(5(x1))))))
    4(0(1(4(0(x1))))) -> 0(4(1(2(0(4(x1))))))
    2(2(3(4(0(x1))))) -> 2(5(3(0(2(4(x1))))))
    4(0(1(5(0(x1))))) -> 0(0(1(4(2(5(x1))))))
    2(4(1(5(0(x1))))) -> 2(1(5(3(0(4(x1))))))
    2(1(0(1(2(x1))))) -> 3(2(0(1(1(2(x1))))))
    2(5(0(4(2(x1))))) -> 2(5(3(2(4(0(x1))))))
    2(1(0(0(3(x1))))) -> 2(0(1(5(3(0(x1))))))
    2(5(0(0(3(x1))))) -> 1(5(3(0(0(2(x1))))))
    2(4(5(0(3(x1))))) -> 1(2(5(3(0(4(x1))))))
    2(1(0(2(3(x1))))) -> 2(0(1(3(1(2(x1))))))
    2(5(0(2(3(x1))))) -> 5(4(3(2(0(2(x1))))))
    2(5(0(2(3(x1))))) -> 2(2(2(0(3(5(x1))))))
   TDG Processor:
    DPs:
     2#(1(0(0(x1)))) -> 2#(x1)
     2#(1(0(0(x1)))) -> 2#(0(0(1(3(x1)))))
     2#(1(0(0(x1)))) -> 2#(0(0(x1)))
     4#(0(1(0(x1)))) -> 4#(1(3(x1)))
     4#(0(1(0(x1)))) -> 4#(3(x1))
     4#(0(1(0(x1)))) -> 4#(x1)
     4#(0(1(0(x1)))) -> 5#(0(1(3(4(x1)))))
     4#(0(1(0(x1)))) -> 5#(x1)
     4#(0(1(0(x1)))) -> 4#(0(5(x1)))
     5#(0(1(0(x1)))) -> 5#(3(x1))
     5#(0(1(0(x1)))) -> 5#(x1)
     5#(0(1(0(x1)))) -> 2#(0(0(1(3(5(x1))))))
     2#(4(1(0(x1)))) -> 2#(x1)
     2#(4(1(0(x1)))) -> 4#(1(3(2(x1))))
     2#(4(1(0(x1)))) -> 4#(x1)
     2#(4(1(0(x1)))) -> 2#(1(3(0(4(x1)))))
     2#(4(1(0(x1)))) -> 4#(2(1(3(0(4(x1))))))
     2#(4(1(0(x1)))) -> 2#(0(1(1(3(4(x1))))))
     4#(0(5(0(x1)))) -> 4#(x1)
     4#(0(5(0(x1)))) -> 5#(3(0(0(4(x1)))))
     4#(0(5(0(x1)))) -> 5#(x1)
     4#(0(5(0(x1)))) -> 4#(3(0(0(5(x1)))))
     5#(0(5(0(x1)))) -> 5#(3(x1))
     5#(0(5(0(x1)))) -> 2#(5(3(x1)))
     5#(0(5(0(x1)))) -> 5#(0(0(2(5(3(x1))))))
     5#(0(5(0(x1)))) -> 5#(x1)
     5#(0(5(0(x1)))) -> 5#(3(5(x1)))
     5#(0(5(0(x1)))) -> 4#(5(3(5(x1))))
     5#(0(5(0(x1)))) -> 5#(5(x1))
     5#(0(5(0(x1)))) -> 4#(3(5(5(x1))))
     2#(1(0(2(x1)))) -> 2#(0(x1))
     2#(1(0(2(x1)))) -> 4#(2(0(x1)))
     2#(1(0(2(x1)))) -> 2#(1(4(2(0(x1)))))
     2#(1(0(2(x1)))) -> 5#(2(x1))
     2#(1(0(2(x1)))) -> 2#(0(5(2(x1))))
     2#(1(0(2(x1)))) -> 2#(2(0(5(2(x1)))))
     2#(1(0(2(x1)))) -> 2#(3(1(3(x1))))
     2#(1(0(2(x1)))) -> 2#(2(3(1(3(x1)))))
     2#(4(0(2(x1)))) -> 4#(x1)
     2#(4(0(2(x1)))) -> 2#(0(4(x1)))
     2#(4(0(2(x1)))) -> 2#(2(0(4(x1))))
     2#(4(0(2(x1)))) -> 2#(1(2(0(4(x1)))))
     2#(5(0(2(x1)))) -> 2#(0(x1))
     2#(5(0(2(x1)))) -> 5#(1(2(0(x1))))
     2#(5(0(2(x1)))) -> 2#(5(1(2(0(x1)))))
     2#(5(0(2(x1)))) -> 2#(2(5(1(2(0(x1))))))
     2#(4(0(3(x1)))) -> 4#(3(0(x1)))
     2#(4(0(3(x1)))) -> 2#(1(1(4(3(0(x1))))))
     2#(4(0(3(x1)))) -> 4#(x1)
     2#(4(0(3(x1)))) -> 2#(0(1(3(3(4(x1))))))
     2#(2(1(0(0(x1))))) -> 2#(0(0(x1)))
     2#(2(1(0(0(x1))))) -> 2#(1(2(0(0(x1)))))
     2#(3(1(0(0(x1))))) -> 2#(1(3(0(x1))))
     2#(3(1(0(0(x1))))) -> 4#(0(2(1(3(0(x1))))))
     2#(3(1(0(0(x1))))) -> 2#(x1)
     2#(3(1(0(0(x1))))) -> 5#(2(x1))
     2#(2(5(0(0(x1))))) -> 2#(0(0(x1)))
     2#(2(5(0(0(x1))))) -> 5#(2(0(0(x1))))
     2#(2(5(0(0(x1))))) -> 2#(5(2(0(0(x1)))))
     2#(5(0(1(0(x1))))) -> 2#(0(x1))
     2#(5(0(1(0(x1))))) -> 5#(3(0(1(2(0(x1))))))
     5#(5(0(1(0(x1))))) -> 5#(3(1(x1)))
     5#(5(0(1(0(x1))))) -> 5#(0(0(5(3(1(x1))))))
     5#(0(2(1(0(x1))))) -> 4#(x1)
     5#(0(2(1(0(x1))))) -> 5#(0(4(x1)))
     5#(0(2(1(0(x1))))) -> 2#(5(0(4(x1))))
     4#(0(3(1(0(x1))))) -> 4#(3(0(1(x1))))
     4#(0(3(1(0(x1))))) -> 4#(4(3(0(1(x1)))))
     2#(4(3(1(0(x1))))) -> 4#(x1)
     2#(4(3(1(0(x1))))) -> 2#(4(x1))
     2#(4(3(1(0(x1))))) -> 4#(3(0(1(2(4(x1))))))
     2#(2(4(1(0(x1))))) -> 2#(0(1(1(x1))))
     2#(2(4(1(0(x1))))) -> 4#(2(0(1(1(x1)))))
     2#(2(4(1(0(x1))))) -> 2#(4(2(0(1(1(x1))))))
     4#(2(4(1(0(x1))))) -> 4#(x1)
     4#(2(4(1(0(x1))))) -> 2#(0(4(x1)))
     4#(2(4(1(0(x1))))) -> 4#(1(3(2(0(4(x1))))))
     2#(3(4(1(0(x1))))) -> 2#(1(3(x1)))
     2#(3(4(1(0(x1))))) -> 4#(0(2(1(3(x1)))))
     2#(3(4(1(0(x1))))) -> 4#(4(0(2(1(3(x1))))))
     5#(0(0(3(0(x1))))) -> 5#(x1)
     4#(0(1(4(0(x1))))) -> 4#(x1)
     4#(0(1(4(0(x1))))) -> 2#(0(4(x1)))
     4#(0(1(4(0(x1))))) -> 4#(1(2(0(4(x1)))))
     2#(2(3(4(0(x1))))) -> 4#(x1)
     2#(2(3(4(0(x1))))) -> 2#(4(x1))
     2#(2(3(4(0(x1))))) -> 5#(3(0(2(4(x1)))))
     2#(2(3(4(0(x1))))) -> 2#(5(3(0(2(4(x1))))))
     4#(0(1(5(0(x1))))) -> 5#(x1)
     4#(0(1(5(0(x1))))) -> 2#(5(x1))
     4#(0(1(5(0(x1))))) -> 4#(2(5(x1)))
     2#(4(1(5(0(x1))))) -> 4#(x1)
     2#(4(1(5(0(x1))))) -> 5#(3(0(4(x1))))
     2#(4(1(5(0(x1))))) -> 2#(1(5(3(0(4(x1))))))
     2#(1(0(1(2(x1))))) -> 2#(0(1(1(2(x1)))))
     2#(5(0(4(2(x1))))) -> 4#(0(x1))
     2#(5(0(4(2(x1))))) -> 2#(4(0(x1)))
     2#(5(0(4(2(x1))))) -> 5#(3(2(4(0(x1)))))
     2#(5(0(4(2(x1))))) -> 2#(5(3(2(4(0(x1))))))
     2#(1(0(0(3(x1))))) -> 5#(3(0(x1)))
     2#(1(0(0(3(x1))))) -> 2#(0(1(5(3(0(x1))))))
     2#(5(0(0(3(x1))))) -> 2#(x1)
     2#(5(0(0(3(x1))))) -> 5#(3(0(0(2(x1)))))
     2#(4(5(0(3(x1))))) -> 4#(x1)
     2#(4(5(0(3(x1))))) -> 5#(3(0(4(x1))))
     2#(4(5(0(3(x1))))) -> 2#(5(3(0(4(x1)))))
     2#(1(0(2(3(x1))))) -> 2#(x1)
     2#(1(0(2(3(x1))))) -> 2#(0(1(3(1(2(x1))))))
     2#(5(0(2(3(x1))))) -> 2#(x1)
     2#(5(0(2(3(x1))))) -> 2#(0(2(x1)))
     2#(5(0(2(3(x1))))) -> 4#(3(2(0(2(x1)))))
     2#(5(0(2(3(x1))))) -> 5#(4(3(2(0(2(x1))))))
     2#(5(0(2(3(x1))))) -> 5#(x1)
     2#(5(0(2(3(x1))))) -> 2#(0(3(5(x1))))
     2#(5(0(2(3(x1))))) -> 2#(2(0(3(5(x1)))))
     2#(5(0(2(3(x1))))) -> 2#(2(2(0(3(5(x1))))))
    TRS:
     2(1(0(0(x1)))) -> 0(0(1(3(2(x1)))))
     2(1(0(0(x1)))) -> 2(0(0(1(3(x1)))))
     2(1(0(0(x1)))) -> 1(1(3(2(0(0(x1))))))
     4(0(1(0(x1)))) -> 0(0(4(1(3(x1)))))
     4(0(1(0(x1)))) -> 1(3(0(0(4(3(x1))))))
     4(0(1(0(x1)))) -> 0(5(0(1(3(4(x1))))))
     4(0(1(0(x1)))) -> 0(1(3(4(0(5(x1))))))
     5(0(1(0(x1)))) -> 0(0(1(3(5(3(x1))))))
     5(0(1(0(x1)))) -> 2(0(0(1(3(5(x1))))))
     2(4(1(0(x1)))) -> 0(4(1(3(2(x1)))))
     2(4(1(0(x1)))) -> 4(2(1(3(0(4(x1))))))
     2(4(1(0(x1)))) -> 2(0(1(1(3(4(x1))))))
     4(0(5(0(x1)))) -> 5(3(0(0(4(x1)))))
     4(0(5(0(x1)))) -> 4(3(0(0(5(x1)))))
     5(0(5(0(x1)))) -> 5(0(0(2(5(3(x1))))))
     5(0(5(0(x1)))) -> 0(0(4(5(3(5(x1))))))
     5(0(5(0(x1)))) -> 0(0(4(3(5(5(x1))))))
     2(1(0(2(x1)))) -> 2(1(4(2(0(x1)))))
     2(1(0(2(x1)))) -> 1(2(2(0(5(2(x1))))))
     2(1(0(2(x1)))) -> 0(2(2(3(1(3(x1))))))
     2(4(0(2(x1)))) -> 1(2(2(0(4(x1)))))
     2(4(0(2(x1)))) -> 1(2(1(2(0(4(x1))))))
     2(5(0(2(x1)))) -> 2(2(5(1(2(0(x1))))))
     2(4(0(3(x1)))) -> 2(1(1(4(3(0(x1))))))
     2(4(0(3(x1)))) -> 2(0(1(3(3(4(x1))))))
     2(2(1(0(0(x1))))) -> 1(2(1(2(0(0(x1))))))
     2(3(1(0(0(x1))))) -> 4(0(2(1(3(0(x1))))))
     2(3(1(0(0(x1))))) -> 0(1(3(0(5(2(x1))))))
     2(2(5(0(0(x1))))) -> 1(2(5(2(0(0(x1))))))
     2(5(0(1(0(x1))))) -> 5(3(0(1(2(0(x1))))))
     5(5(0(1(0(x1))))) -> 5(0(0(5(3(1(x1))))))
     5(0(2(1(0(x1))))) -> 0(1(2(5(0(4(x1))))))
     4(0(3(1(0(x1))))) -> 0(4(4(3(0(1(x1))))))
     2(4(3(1(0(x1))))) -> 4(3(0(1(2(4(x1))))))
     2(2(4(1(0(x1))))) -> 2(4(2(0(1(1(x1))))))
     4(2(4(1(0(x1))))) -> 4(1(3(2(0(4(x1))))))
     2(3(4(1(0(x1))))) -> 4(4(0(2(1(3(x1))))))
     5(0(0(3(0(x1))))) -> 0(0(0(1(3(5(x1))))))
     4(0(1(4(0(x1))))) -> 0(4(1(2(0(4(x1))))))
     2(2(3(4(0(x1))))) -> 2(5(3(0(2(4(x1))))))
     4(0(1(5(0(x1))))) -> 0(0(1(4(2(5(x1))))))
     2(4(1(5(0(x1))))) -> 2(1(5(3(0(4(x1))))))
     2(1(0(1(2(x1))))) -> 3(2(0(1(1(2(x1))))))
     2(5(0(4(2(x1))))) -> 2(5(3(2(4(0(x1))))))
     2(1(0(0(3(x1))))) -> 2(0(1(5(3(0(x1))))))
     2(5(0(0(3(x1))))) -> 1(5(3(0(0(2(x1))))))
     2(4(5(0(3(x1))))) -> 1(2(5(3(0(4(x1))))))
     2(1(0(2(3(x1))))) -> 2(0(1(3(1(2(x1))))))
     2(5(0(2(3(x1))))) -> 5(4(3(2(0(2(x1))))))
     2(5(0(2(3(x1))))) -> 2(2(2(0(3(5(x1))))))
    graph:
     ...
    EDG Processor:
     DPs:
      2#(1(0(0(x1)))) -> 2#(x1)
      2#(1(0(0(x1)))) -> 2#(0(0(1(3(x1)))))
      2#(1(0(0(x1)))) -> 2#(0(0(x1)))
      4#(0(1(0(x1)))) -> 4#(1(3(x1)))
      4#(0(1(0(x1)))) -> 4#(3(x1))
      4#(0(1(0(x1)))) -> 4#(x1)
      4#(0(1(0(x1)))) -> 5#(0(1(3(4(x1)))))
      4#(0(1(0(x1)))) -> 5#(x1)
      4#(0(1(0(x1)))) -> 4#(0(5(x1)))
      5#(0(1(0(x1)))) -> 5#(3(x1))
      5#(0(1(0(x1)))) -> 5#(x1)
      5#(0(1(0(x1)))) -> 2#(0(0(1(3(5(x1))))))
      2#(4(1(0(x1)))) -> 2#(x1)
      2#(4(1(0(x1)))) -> 4#(1(3(2(x1))))
      2#(4(1(0(x1)))) -> 4#(x1)
      2#(4(1(0(x1)))) -> 2#(1(3(0(4(x1)))))
      2#(4(1(0(x1)))) -> 4#(2(1(3(0(4(x1))))))
      2#(4(1(0(x1)))) -> 2#(0(1(1(3(4(x1))))))
      4#(0(5(0(x1)))) -> 4#(x1)
      4#(0(5(0(x1)))) -> 5#(3(0(0(4(x1)))))
      4#(0(5(0(x1)))) -> 5#(x1)
      4#(0(5(0(x1)))) -> 4#(3(0(0(5(x1)))))
      5#(0(5(0(x1)))) -> 5#(3(x1))
      5#(0(5(0(x1)))) -> 2#(5(3(x1)))
      5#(0(5(0(x1)))) -> 5#(0(0(2(5(3(x1))))))
      5#(0(5(0(x1)))) -> 5#(x1)
      5#(0(5(0(x1)))) -> 5#(3(5(x1)))
      5#(0(5(0(x1)))) -> 4#(5(3(5(x1))))
      5#(0(5(0(x1)))) -> 5#(5(x1))
      5#(0(5(0(x1)))) -> 4#(3(5(5(x1))))
      2#(1(0(2(x1)))) -> 2#(0(x1))
      2#(1(0(2(x1)))) -> 4#(2(0(x1)))
      2#(1(0(2(x1)))) -> 2#(1(4(2(0(x1)))))
      2#(1(0(2(x1)))) -> 5#(2(x1))
      2#(1(0(2(x1)))) -> 2#(0(5(2(x1))))
      2#(1(0(2(x1)))) -> 2#(2(0(5(2(x1)))))
      2#(1(0(2(x1)))) -> 2#(3(1(3(x1))))
      2#(1(0(2(x1)))) -> 2#(2(3(1(3(x1)))))
      2#(4(0(2(x1)))) -> 4#(x1)
      2#(4(0(2(x1)))) -> 2#(0(4(x1)))
      2#(4(0(2(x1)))) -> 2#(2(0(4(x1))))
      2#(4(0(2(x1)))) -> 2#(1(2(0(4(x1)))))
      2#(5(0(2(x1)))) -> 2#(0(x1))
      2#(5(0(2(x1)))) -> 5#(1(2(0(x1))))
      2#(5(0(2(x1)))) -> 2#(5(1(2(0(x1)))))
      2#(5(0(2(x1)))) -> 2#(2(5(1(2(0(x1))))))
      2#(4(0(3(x1)))) -> 4#(3(0(x1)))
      2#(4(0(3(x1)))) -> 2#(1(1(4(3(0(x1))))))
      2#(4(0(3(x1)))) -> 4#(x1)
      2#(4(0(3(x1)))) -> 2#(0(1(3(3(4(x1))))))
      2#(2(1(0(0(x1))))) -> 2#(0(0(x1)))
      2#(2(1(0(0(x1))))) -> 2#(1(2(0(0(x1)))))
      2#(3(1(0(0(x1))))) -> 2#(1(3(0(x1))))
      2#(3(1(0(0(x1))))) -> 4#(0(2(1(3(0(x1))))))
      2#(3(1(0(0(x1))))) -> 2#(x1)
      2#(3(1(0(0(x1))))) -> 5#(2(x1))
      2#(2(5(0(0(x1))))) -> 2#(0(0(x1)))
      2#(2(5(0(0(x1))))) -> 5#(2(0(0(x1))))
      2#(2(5(0(0(x1))))) -> 2#(5(2(0(0(x1)))))
      2#(5(0(1(0(x1))))) -> 2#(0(x1))
      2#(5(0(1(0(x1))))) -> 5#(3(0(1(2(0(x1))))))
      5#(5(0(1(0(x1))))) -> 5#(3(1(x1)))
      5#(5(0(1(0(x1))))) -> 5#(0(0(5(3(1(x1))))))
      5#(0(2(1(0(x1))))) -> 4#(x1)
      5#(0(2(1(0(x1))))) -> 5#(0(4(x1)))
      5#(0(2(1(0(x1))))) -> 2#(5(0(4(x1))))
      4#(0(3(1(0(x1))))) -> 4#(3(0(1(x1))))
      4#(0(3(1(0(x1))))) -> 4#(4(3(0(1(x1)))))
      2#(4(3(1(0(x1))))) -> 4#(x1)
      2#(4(3(1(0(x1))))) -> 2#(4(x1))
      2#(4(3(1(0(x1))))) -> 4#(3(0(1(2(4(x1))))))
      2#(2(4(1(0(x1))))) -> 2#(0(1(1(x1))))
      2#(2(4(1(0(x1))))) -> 4#(2(0(1(1(x1)))))
      2#(2(4(1(0(x1))))) -> 2#(4(2(0(1(1(x1))))))
      4#(2(4(1(0(x1))))) -> 4#(x1)
      4#(2(4(1(0(x1))))) -> 2#(0(4(x1)))
      4#(2(4(1(0(x1))))) -> 4#(1(3(2(0(4(x1))))))
      2#(3(4(1(0(x1))))) -> 2#(1(3(x1)))
      2#(3(4(1(0(x1))))) -> 4#(0(2(1(3(x1)))))
      2#(3(4(1(0(x1))))) -> 4#(4(0(2(1(3(x1))))))
      5#(0(0(3(0(x1))))) -> 5#(x1)
      4#(0(1(4(0(x1))))) -> 4#(x1)
      4#(0(1(4(0(x1))))) -> 2#(0(4(x1)))
      4#(0(1(4(0(x1))))) -> 4#(1(2(0(4(x1)))))
      2#(2(3(4(0(x1))))) -> 4#(x1)
      2#(2(3(4(0(x1))))) -> 2#(4(x1))
      2#(2(3(4(0(x1))))) -> 5#(3(0(2(4(x1)))))
      2#(2(3(4(0(x1))))) -> 2#(5(3(0(2(4(x1))))))
      4#(0(1(5(0(x1))))) -> 5#(x1)
      4#(0(1(5(0(x1))))) -> 2#(5(x1))
      4#(0(1(5(0(x1))))) -> 4#(2(5(x1)))
      2#(4(1(5(0(x1))))) -> 4#(x1)
      2#(4(1(5(0(x1))))) -> 5#(3(0(4(x1))))
      2#(4(1(5(0(x1))))) -> 2#(1(5(3(0(4(x1))))))
      2#(1(0(1(2(x1))))) -> 2#(0(1(1(2(x1)))))
      2#(5(0(4(2(x1))))) -> 4#(0(x1))
      2#(5(0(4(2(x1))))) -> 2#(4(0(x1)))
      2#(5(0(4(2(x1))))) -> 5#(3(2(4(0(x1)))))
      2#(5(0(4(2(x1))))) -> 2#(5(3(2(4(0(x1))))))
      2#(1(0(0(3(x1))))) -> 5#(3(0(x1)))
      2#(1(0(0(3(x1))))) -> 2#(0(1(5(3(0(x1))))))
      2#(5(0(0(3(x1))))) -> 2#(x1)
      2#(5(0(0(3(x1))))) -> 5#(3(0(0(2(x1)))))
      2#(4(5(0(3(x1))))) -> 4#(x1)
      2#(4(5(0(3(x1))))) -> 5#(3(0(4(x1))))
      2#(4(5(0(3(x1))))) -> 2#(5(3(0(4(x1)))))
      2#(1(0(2(3(x1))))) -> 2#(x1)
      2#(1(0(2(3(x1))))) -> 2#(0(1(3(1(2(x1))))))
      2#(5(0(2(3(x1))))) -> 2#(x1)
      2#(5(0(2(3(x1))))) -> 2#(0(2(x1)))
      2#(5(0(2(3(x1))))) -> 4#(3(2(0(2(x1)))))
      2#(5(0(2(3(x1))))) -> 5#(4(3(2(0(2(x1))))))
      2#(5(0(2(3(x1))))) -> 5#(x1)
      2#(5(0(2(3(x1))))) -> 2#(0(3(5(x1))))
      2#(5(0(2(3(x1))))) -> 2#(2(0(3(5(x1)))))
      2#(5(0(2(3(x1))))) -> 2#(2(2(0(3(5(x1))))))
     TRS:
      2(1(0(0(x1)))) -> 0(0(1(3(2(x1)))))
      2(1(0(0(x1)))) -> 2(0(0(1(3(x1)))))
      2(1(0(0(x1)))) -> 1(1(3(2(0(0(x1))))))
      4(0(1(0(x1)))) -> 0(0(4(1(3(x1)))))
      4(0(1(0(x1)))) -> 1(3(0(0(4(3(x1))))))
      4(0(1(0(x1)))) -> 0(5(0(1(3(4(x1))))))
      4(0(1(0(x1)))) -> 0(1(3(4(0(5(x1))))))
      5(0(1(0(x1)))) -> 0(0(1(3(5(3(x1))))))
      5(0(1(0(x1)))) -> 2(0(0(1(3(5(x1))))))
      2(4(1(0(x1)))) -> 0(4(1(3(2(x1)))))
      2(4(1(0(x1)))) -> 4(2(1(3(0(4(x1))))))
      2(4(1(0(x1)))) -> 2(0(1(1(3(4(x1))))))
      4(0(5(0(x1)))) -> 5(3(0(0(4(x1)))))
      4(0(5(0(x1)))) -> 4(3(0(0(5(x1)))))
      5(0(5(0(x1)))) -> 5(0(0(2(5(3(x1))))))
      5(0(5(0(x1)))) -> 0(0(4(5(3(5(x1))))))
      5(0(5(0(x1)))) -> 0(0(4(3(5(5(x1))))))
      2(1(0(2(x1)))) -> 2(1(4(2(0(x1)))))
      2(1(0(2(x1)))) -> 1(2(2(0(5(2(x1))))))
      2(1(0(2(x1)))) -> 0(2(2(3(1(3(x1))))))
      2(4(0(2(x1)))) -> 1(2(2(0(4(x1)))))
      2(4(0(2(x1)))) -> 1(2(1(2(0(4(x1))))))
      2(5(0(2(x1)))) -> 2(2(5(1(2(0(x1))))))
      2(4(0(3(x1)))) -> 2(1(1(4(3(0(x1))))))
      2(4(0(3(x1)))) -> 2(0(1(3(3(4(x1))))))
      2(2(1(0(0(x1))))) -> 1(2(1(2(0(0(x1))))))
      2(3(1(0(0(x1))))) -> 4(0(2(1(3(0(x1))))))
      2(3(1(0(0(x1))))) -> 0(1(3(0(5(2(x1))))))
      2(2(5(0(0(x1))))) -> 1(2(5(2(0(0(x1))))))
      2(5(0(1(0(x1))))) -> 5(3(0(1(2(0(x1))))))
      5(5(0(1(0(x1))))) -> 5(0(0(5(3(1(x1))))))
      5(0(2(1(0(x1))))) -> 0(1(2(5(0(4(x1))))))
      4(0(3(1(0(x1))))) -> 0(4(4(3(0(1(x1))))))
      2(4(3(1(0(x1))))) -> 4(3(0(1(2(4(x1))))))
      2(2(4(1(0(x1))))) -> 2(4(2(0(1(1(x1))))))
      4(2(4(1(0(x1))))) -> 4(1(3(2(0(4(x1))))))
      2(3(4(1(0(x1))))) -> 4(4(0(2(1(3(x1))))))
      5(0(0(3(0(x1))))) -> 0(0(0(1(3(5(x1))))))
      4(0(1(4(0(x1))))) -> 0(4(1(2(0(4(x1))))))
      2(2(3(4(0(x1))))) -> 2(5(3(0(2(4(x1))))))
      4(0(1(5(0(x1))))) -> 0(0(1(4(2(5(x1))))))
      2(4(1(5(0(x1))))) -> 2(1(5(3(0(4(x1))))))
      2(1(0(1(2(x1))))) -> 3(2(0(1(1(2(x1))))))
      2(5(0(4(2(x1))))) -> 2(5(3(2(4(0(x1))))))
      2(1(0(0(3(x1))))) -> 2(0(1(5(3(0(x1))))))
      2(5(0(0(3(x1))))) -> 1(5(3(0(0(2(x1))))))
      2(4(5(0(3(x1))))) -> 1(2(5(3(0(4(x1))))))
      2(1(0(2(3(x1))))) -> 2(0(1(3(1(2(x1))))))
      2(5(0(2(3(x1))))) -> 5(4(3(2(0(2(x1))))))
      2(5(0(2(3(x1))))) -> 2(2(2(0(3(5(x1))))))
     graph:
      ...
     SCC Processor:
      #sccs: 1
      #rules: 37
      #arcs: 1352/13456
      DPs:
       5#(0(5(0(x1)))) -> 5#(5(x1))
       5#(0(0(3(0(x1))))) -> 5#(x1)
       5#(0(2(1(0(x1))))) -> 2#(5(0(4(x1))))
       2#(5(0(2(3(x1))))) -> 5#(x1)
       5#(0(2(1(0(x1))))) -> 5#(0(4(x1)))
       5#(0(2(1(0(x1))))) -> 4#(x1)
       4#(0(1(5(0(x1))))) -> 4#(2(5(x1)))
       4#(0(1(5(0(x1))))) -> 2#(5(x1))
       2#(5(0(2(3(x1))))) -> 2#(x1)
       2#(1(0(2(3(x1))))) -> 2#(x1)
       2#(4(5(0(3(x1))))) -> 4#(x1)
       4#(0(1(5(0(x1))))) -> 5#(x1)
       5#(0(5(0(x1)))) -> 5#(x1)
       5#(0(1(0(x1)))) -> 5#(x1)
       4#(0(1(4(0(x1))))) -> 4#(x1)
       4#(2(4(1(0(x1))))) -> 4#(x1)
       4#(0(5(0(x1)))) -> 5#(x1)
       4#(0(5(0(x1)))) -> 4#(x1)
       4#(0(1(0(x1)))) -> 4#(0(5(x1)))
       4#(0(1(0(x1)))) -> 5#(x1)
       4#(0(1(0(x1)))) -> 4#(x1)
       2#(5(0(0(3(x1))))) -> 2#(x1)
       2#(5(0(4(2(x1))))) -> 2#(4(0(x1)))
       2#(5(0(4(2(x1))))) -> 4#(0(x1))
       2#(4(1(5(0(x1))))) -> 4#(x1)
       2#(2(3(4(0(x1))))) -> 2#(4(x1))
       2#(2(3(4(0(x1))))) -> 4#(x1)
       2#(4(3(1(0(x1))))) -> 2#(4(x1))
       2#(4(3(1(0(x1))))) -> 4#(x1)
       2#(3(1(0(0(x1))))) -> 5#(2(x1))
       2#(3(1(0(0(x1))))) -> 2#(x1)
       2#(4(0(3(x1)))) -> 4#(x1)
       2#(4(0(2(x1)))) -> 4#(x1)
       2#(1(0(2(x1)))) -> 5#(2(x1))
       2#(4(1(0(x1)))) -> 4#(x1)
       2#(4(1(0(x1)))) -> 2#(x1)
       2#(1(0(0(x1)))) -> 2#(x1)
      TRS:
       2(1(0(0(x1)))) -> 0(0(1(3(2(x1)))))
       2(1(0(0(x1)))) -> 2(0(0(1(3(x1)))))
       2(1(0(0(x1)))) -> 1(1(3(2(0(0(x1))))))
       4(0(1(0(x1)))) -> 0(0(4(1(3(x1)))))
       4(0(1(0(x1)))) -> 1(3(0(0(4(3(x1))))))
       4(0(1(0(x1)))) -> 0(5(0(1(3(4(x1))))))
       4(0(1(0(x1)))) -> 0(1(3(4(0(5(x1))))))
       5(0(1(0(x1)))) -> 0(0(1(3(5(3(x1))))))
       5(0(1(0(x1)))) -> 2(0(0(1(3(5(x1))))))
       2(4(1(0(x1)))) -> 0(4(1(3(2(x1)))))
       2(4(1(0(x1)))) -> 4(2(1(3(0(4(x1))))))
       2(4(1(0(x1)))) -> 2(0(1(1(3(4(x1))))))
       4(0(5(0(x1)))) -> 5(3(0(0(4(x1)))))
       4(0(5(0(x1)))) -> 4(3(0(0(5(x1)))))
       5(0(5(0(x1)))) -> 5(0(0(2(5(3(x1))))))
       5(0(5(0(x1)))) -> 0(0(4(5(3(5(x1))))))
       5(0(5(0(x1)))) -> 0(0(4(3(5(5(x1))))))
       2(1(0(2(x1)))) -> 2(1(4(2(0(x1)))))
       2(1(0(2(x1)))) -> 1(2(2(0(5(2(x1))))))
       2(1(0(2(x1)))) -> 0(2(2(3(1(3(x1))))))
       2(4(0(2(x1)))) -> 1(2(2(0(4(x1)))))
       2(4(0(2(x1)))) -> 1(2(1(2(0(4(x1))))))
       2(5(0(2(x1)))) -> 2(2(5(1(2(0(x1))))))
       2(4(0(3(x1)))) -> 2(1(1(4(3(0(x1))))))
       2(4(0(3(x1)))) -> 2(0(1(3(3(4(x1))))))
       2(2(1(0(0(x1))))) -> 1(2(1(2(0(0(x1))))))
       2(3(1(0(0(x1))))) -> 4(0(2(1(3(0(x1))))))
       2(3(1(0(0(x1))))) -> 0(1(3(0(5(2(x1))))))
       2(2(5(0(0(x1))))) -> 1(2(5(2(0(0(x1))))))
       2(5(0(1(0(x1))))) -> 5(3(0(1(2(0(x1))))))
       5(5(0(1(0(x1))))) -> 5(0(0(5(3(1(x1))))))
       5(0(2(1(0(x1))))) -> 0(1(2(5(0(4(x1))))))
       4(0(3(1(0(x1))))) -> 0(4(4(3(0(1(x1))))))
       2(4(3(1(0(x1))))) -> 4(3(0(1(2(4(x1))))))
       2(2(4(1(0(x1))))) -> 2(4(2(0(1(1(x1))))))
       4(2(4(1(0(x1))))) -> 4(1(3(2(0(4(x1))))))
       2(3(4(1(0(x1))))) -> 4(4(0(2(1(3(x1))))))
       5(0(0(3(0(x1))))) -> 0(0(0(1(3(5(x1))))))
       4(0(1(4(0(x1))))) -> 0(4(1(2(0(4(x1))))))
       2(2(3(4(0(x1))))) -> 2(5(3(0(2(4(x1))))))
       4(0(1(5(0(x1))))) -> 0(0(1(4(2(5(x1))))))
       2(4(1(5(0(x1))))) -> 2(1(5(3(0(4(x1))))))
       2(1(0(1(2(x1))))) -> 3(2(0(1(1(2(x1))))))
       2(5(0(4(2(x1))))) -> 2(5(3(2(4(0(x1))))))
       2(1(0(0(3(x1))))) -> 2(0(1(5(3(0(x1))))))
       2(5(0(0(3(x1))))) -> 1(5(3(0(0(2(x1))))))
       2(4(5(0(3(x1))))) -> 1(2(5(3(0(4(x1))))))
       2(1(0(2(3(x1))))) -> 2(0(1(3(1(2(x1))))))
       2(5(0(2(3(x1))))) -> 5(4(3(2(0(2(x1))))))
       2(5(0(2(3(x1))))) -> 2(2(2(0(3(5(x1))))))
      Arctic Interpretation Processor:
       dimension: 1
       interpretation:
        [5#](x0) = x0,
        
        [4#](x0) = x0,
        
        [2#](x0) = 8x0 + 0,
        
        [5](x0) = x0,
        
        [4](x0) = x0,
        
        [3](x0) = x0,
        
        [0](x0) = 8x0 + 0,
        
        [1](x0) = x0,
        
        [2](x0) = x0
       orientation:
        5#(0(5(0(x1)))) = 16x1 + 8 >= x1 = 5#(5(x1))
        
        5#(0(0(3(0(x1))))) = 24x1 + 16 >= x1 = 5#(x1)
        
        5#(0(2(1(0(x1))))) = 16x1 + 8 >= 16x1 + 8 = 2#(5(0(4(x1))))
        
        2#(5(0(2(3(x1))))) = 16x1 + 8 >= x1 = 5#(x1)
        
        5#(0(2(1(0(x1))))) = 16x1 + 8 >= 8x1 + 0 = 5#(0(4(x1)))
        
        5#(0(2(1(0(x1))))) = 16x1 + 8 >= x1 = 4#(x1)
        
        4#(0(1(5(0(x1))))) = 16x1 + 8 >= x1 = 4#(2(5(x1)))
        
        4#(0(1(5(0(x1))))) = 16x1 + 8 >= 8x1 + 0 = 2#(5(x1))
        
        2#(5(0(2(3(x1))))) = 16x1 + 8 >= 8x1 + 0 = 2#(x1)
        
        2#(1(0(2(3(x1))))) = 16x1 + 8 >= 8x1 + 0 = 2#(x1)
        
        2#(4(5(0(3(x1))))) = 16x1 + 8 >= x1 = 4#(x1)
        
        4#(0(1(5(0(x1))))) = 16x1 + 8 >= x1 = 5#(x1)
        
        5#(0(5(0(x1)))) = 16x1 + 8 >= x1 = 5#(x1)
        
        5#(0(1(0(x1)))) = 16x1 + 8 >= x1 = 5#(x1)
        
        4#(0(1(4(0(x1))))) = 16x1 + 8 >= x1 = 4#(x1)
        
        4#(2(4(1(0(x1))))) = 8x1 + 0 >= x1 = 4#(x1)
        
        4#(0(5(0(x1)))) = 16x1 + 8 >= x1 = 5#(x1)
        
        4#(0(5(0(x1)))) = 16x1 + 8 >= x1 = 4#(x1)
        
        4#(0(1(0(x1)))) = 16x1 + 8 >= 8x1 + 0 = 4#(0(5(x1)))
        
        4#(0(1(0(x1)))) = 16x1 + 8 >= x1 = 5#(x1)
        
        4#(0(1(0(x1)))) = 16x1 + 8 >= x1 = 4#(x1)
        
        2#(5(0(0(3(x1))))) = 24x1 + 16 >= 8x1 + 0 = 2#(x1)
        
        2#(5(0(4(2(x1))))) = 16x1 + 8 >= 16x1 + 8 = 2#(4(0(x1)))
        
        2#(5(0(4(2(x1))))) = 16x1 + 8 >= 8x1 + 0 = 4#(0(x1))
        
        2#(4(1(5(0(x1))))) = 16x1 + 8 >= x1 = 4#(x1)
        
        2#(2(3(4(0(x1))))) = 16x1 + 8 >= 8x1 + 0 = 2#(4(x1))
        
        2#(2(3(4(0(x1))))) = 16x1 + 8 >= x1 = 4#(x1)
        
        2#(4(3(1(0(x1))))) = 16x1 + 8 >= 8x1 + 0 = 2#(4(x1))
        
        2#(4(3(1(0(x1))))) = 16x1 + 8 >= x1 = 4#(x1)
        
        2#(3(1(0(0(x1))))) = 24x1 + 16 >= x1 = 5#(2(x1))
        
        2#(3(1(0(0(x1))))) = 24x1 + 16 >= 8x1 + 0 = 2#(x1)
        
        2#(4(0(3(x1)))) = 16x1 + 8 >= x1 = 4#(x1)
        
        2#(4(0(2(x1)))) = 16x1 + 8 >= x1 = 4#(x1)
        
        2#(1(0(2(x1)))) = 16x1 + 8 >= x1 = 5#(2(x1))
        
        2#(4(1(0(x1)))) = 16x1 + 8 >= x1 = 4#(x1)
        
        2#(4(1(0(x1)))) = 16x1 + 8 >= 8x1 + 0 = 2#(x1)
        
        2#(1(0(0(x1)))) = 24x1 + 16 >= 8x1 + 0 = 2#(x1)
        
        2(1(0(0(x1)))) = 16x1 + 8 >= 16x1 + 8 = 0(0(1(3(2(x1)))))
        
        2(1(0(0(x1)))) = 16x1 + 8 >= 16x1 + 8 = 2(0(0(1(3(x1)))))
        
        2(1(0(0(x1)))) = 16x1 + 8 >= 16x1 + 8 = 1(1(3(2(0(0(x1))))))
        
        4(0(1(0(x1)))) = 16x1 + 8 >= 16x1 + 8 = 0(0(4(1(3(x1)))))
        
        4(0(1(0(x1)))) = 16x1 + 8 >= 16x1 + 8 = 1(3(0(0(4(3(x1))))))
        
        4(0(1(0(x1)))) = 16x1 + 8 >= 16x1 + 8 = 0(5(0(1(3(4(x1))))))
        
        4(0(1(0(x1)))) = 16x1 + 8 >= 16x1 + 8 = 0(1(3(4(0(5(x1))))))
        
        5(0(1(0(x1)))) = 16x1 + 8 >= 16x1 + 8 = 0(0(1(3(5(3(x1))))))
        
        5(0(1(0(x1)))) = 16x1 + 8 >= 16x1 + 8 = 2(0(0(1(3(5(x1))))))
        
        2(4(1(0(x1)))) = 8x1 + 0 >= 8x1 + 0 = 0(4(1(3(2(x1)))))
        
        2(4(1(0(x1)))) = 8x1 + 0 >= 8x1 + 0 = 4(2(1(3(0(4(x1))))))
        
        2(4(1(0(x1)))) = 8x1 + 0 >= 8x1 + 0 = 2(0(1(1(3(4(x1))))))
        
        4(0(5(0(x1)))) = 16x1 + 8 >= 16x1 + 8 = 5(3(0(0(4(x1)))))
        
        4(0(5(0(x1)))) = 16x1 + 8 >= 16x1 + 8 = 4(3(0(0(5(x1)))))
        
        5(0(5(0(x1)))) = 16x1 + 8 >= 16x1 + 8 = 5(0(0(2(5(3(x1))))))
        
        5(0(5(0(x1)))) = 16x1 + 8 >= 16x1 + 8 = 0(0(4(5(3(5(x1))))))
        
        5(0(5(0(x1)))) = 16x1 + 8 >= 16x1 + 8 = 0(0(4(3(5(5(x1))))))
        
        2(1(0(2(x1)))) = 8x1 + 0 >= 8x1 + 0 = 2(1(4(2(0(x1)))))
        
        2(1(0(2(x1)))) = 8x1 + 0 >= 8x1 + 0 = 1(2(2(0(5(2(x1))))))
        
        2(1(0(2(x1)))) = 8x1 + 0 >= 8x1 + 0 = 0(2(2(3(1(3(x1))))))
        
        2(4(0(2(x1)))) = 8x1 + 0 >= 8x1 + 0 = 1(2(2(0(4(x1)))))
        
        2(4(0(2(x1)))) = 8x1 + 0 >= 8x1 + 0 = 1(2(1(2(0(4(x1))))))
        
        2(5(0(2(x1)))) = 8x1 + 0 >= 8x1 + 0 = 2(2(5(1(2(0(x1))))))
        
        2(4(0(3(x1)))) = 8x1 + 0 >= 8x1 + 0 = 2(1(1(4(3(0(x1))))))
        
        2(4(0(3(x1)))) = 8x1 + 0 >= 8x1 + 0 = 2(0(1(3(3(4(x1))))))
        
        2(2(1(0(0(x1))))) = 16x1 + 8 >= 16x1 + 8 = 1(2(1(2(0(0(x1))))))
        
        2(3(1(0(0(x1))))) = 16x1 + 8 >= 16x1 + 8 = 4(0(2(1(3(0(x1))))))
        
        2(3(1(0(0(x1))))) = 16x1 + 8 >= 16x1 + 8 = 0(1(3(0(5(2(x1))))))
        
        2(2(5(0(0(x1))))) = 16x1 + 8 >= 16x1 + 8 = 1(2(5(2(0(0(x1))))))
        
        2(5(0(1(0(x1))))) = 16x1 + 8 >= 16x1 + 8 = 5(3(0(1(2(0(x1))))))
        
        5(5(0(1(0(x1))))) = 16x1 + 8 >= 16x1 + 8 = 5(0(0(5(3(1(x1))))))
        
        5(0(2(1(0(x1))))) = 16x1 + 8 >= 16x1 + 8 = 0(1(2(5(0(4(x1))))))
        
        4(0(3(1(0(x1))))) = 16x1 + 8 >= 16x1 + 8 = 0(4(4(3(0(1(x1))))))
        
        2(4(3(1(0(x1))))) = 8x1 + 0 >= 8x1 + 0 = 4(3(0(1(2(4(x1))))))
        
        2(2(4(1(0(x1))))) = 8x1 + 0 >= 8x1 + 0 = 2(4(2(0(1(1(x1))))))
        
        4(2(4(1(0(x1))))) = 8x1 + 0 >= 8x1 + 0 = 4(1(3(2(0(4(x1))))))
        
        2(3(4(1(0(x1))))) = 8x1 + 0 >= 8x1 + 0 = 4(4(0(2(1(3(x1))))))
        
        5(0(0(3(0(x1))))) = 24x1 + 16 >= 24x1 + 16 = 0(0(0(1(3(5(x1))))))
        
        4(0(1(4(0(x1))))) = 16x1 + 8 >= 16x1 + 8 = 0(4(1(2(0(4(x1))))))
        
        2(2(3(4(0(x1))))) = 8x1 + 0 >= 8x1 + 0 = 2(5(3(0(2(4(x1))))))
        
        4(0(1(5(0(x1))))) = 16x1 + 8 >= 16x1 + 8 = 0(0(1(4(2(5(x1))))))
        
        2(4(1(5(0(x1))))) = 8x1 + 0 >= 8x1 + 0 = 2(1(5(3(0(4(x1))))))
        
        2(1(0(1(2(x1))))) = 8x1 + 0 >= 8x1 + 0 = 3(2(0(1(1(2(x1))))))
        
        2(5(0(4(2(x1))))) = 8x1 + 0 >= 8x1 + 0 = 2(5(3(2(4(0(x1))))))
        
        2(1(0(0(3(x1))))) = 16x1 + 8 >= 16x1 + 8 = 2(0(1(5(3(0(x1))))))
        
        2(5(0(0(3(x1))))) = 16x1 + 8 >= 16x1 + 8 = 1(5(3(0(0(2(x1))))))
        
        2(4(5(0(3(x1))))) = 8x1 + 0 >= 8x1 + 0 = 1(2(5(3(0(4(x1))))))
        
        2(1(0(2(3(x1))))) = 8x1 + 0 >= 8x1 + 0 = 2(0(1(3(1(2(x1))))))
        
        2(5(0(2(3(x1))))) = 8x1 + 0 >= 8x1 + 0 = 5(4(3(2(0(2(x1))))))
        
        2(5(0(2(3(x1))))) = 8x1 + 0 >= 8x1 + 0 = 2(2(2(0(3(5(x1))))))
       problem:
        DPs:
         5#(0(2(1(0(x1))))) -> 2#(5(0(4(x1))))
         2#(5(0(4(2(x1))))) -> 2#(4(0(x1)))
        TRS:
         2(1(0(0(x1)))) -> 0(0(1(3(2(x1)))))
         2(1(0(0(x1)))) -> 2(0(0(1(3(x1)))))
         2(1(0(0(x1)))) -> 1(1(3(2(0(0(x1))))))
         4(0(1(0(x1)))) -> 0(0(4(1(3(x1)))))
         4(0(1(0(x1)))) -> 1(3(0(0(4(3(x1))))))
         4(0(1(0(x1)))) -> 0(5(0(1(3(4(x1))))))
         4(0(1(0(x1)))) -> 0(1(3(4(0(5(x1))))))
         5(0(1(0(x1)))) -> 0(0(1(3(5(3(x1))))))
         5(0(1(0(x1)))) -> 2(0(0(1(3(5(x1))))))
         2(4(1(0(x1)))) -> 0(4(1(3(2(x1)))))
         2(4(1(0(x1)))) -> 4(2(1(3(0(4(x1))))))
         2(4(1(0(x1)))) -> 2(0(1(1(3(4(x1))))))
         4(0(5(0(x1)))) -> 5(3(0(0(4(x1)))))
         4(0(5(0(x1)))) -> 4(3(0(0(5(x1)))))
         5(0(5(0(x1)))) -> 5(0(0(2(5(3(x1))))))
         5(0(5(0(x1)))) -> 0(0(4(5(3(5(x1))))))
         5(0(5(0(x1)))) -> 0(0(4(3(5(5(x1))))))
         2(1(0(2(x1)))) -> 2(1(4(2(0(x1)))))
         2(1(0(2(x1)))) -> 1(2(2(0(5(2(x1))))))
         2(1(0(2(x1)))) -> 0(2(2(3(1(3(x1))))))
         2(4(0(2(x1)))) -> 1(2(2(0(4(x1)))))
         2(4(0(2(x1)))) -> 1(2(1(2(0(4(x1))))))
         2(5(0(2(x1)))) -> 2(2(5(1(2(0(x1))))))
         2(4(0(3(x1)))) -> 2(1(1(4(3(0(x1))))))
         2(4(0(3(x1)))) -> 2(0(1(3(3(4(x1))))))
         2(2(1(0(0(x1))))) -> 1(2(1(2(0(0(x1))))))
         2(3(1(0(0(x1))))) -> 4(0(2(1(3(0(x1))))))
         2(3(1(0(0(x1))))) -> 0(1(3(0(5(2(x1))))))
         2(2(5(0(0(x1))))) -> 1(2(5(2(0(0(x1))))))
         2(5(0(1(0(x1))))) -> 5(3(0(1(2(0(x1))))))
         5(5(0(1(0(x1))))) -> 5(0(0(5(3(1(x1))))))
         5(0(2(1(0(x1))))) -> 0(1(2(5(0(4(x1))))))
         4(0(3(1(0(x1))))) -> 0(4(4(3(0(1(x1))))))
         2(4(3(1(0(x1))))) -> 4(3(0(1(2(4(x1))))))
         2(2(4(1(0(x1))))) -> 2(4(2(0(1(1(x1))))))
         4(2(4(1(0(x1))))) -> 4(1(3(2(0(4(x1))))))
         2(3(4(1(0(x1))))) -> 4(4(0(2(1(3(x1))))))
         5(0(0(3(0(x1))))) -> 0(0(0(1(3(5(x1))))))
         4(0(1(4(0(x1))))) -> 0(4(1(2(0(4(x1))))))
         2(2(3(4(0(x1))))) -> 2(5(3(0(2(4(x1))))))
         4(0(1(5(0(x1))))) -> 0(0(1(4(2(5(x1))))))
         2(4(1(5(0(x1))))) -> 2(1(5(3(0(4(x1))))))
         2(1(0(1(2(x1))))) -> 3(2(0(1(1(2(x1))))))
         2(5(0(4(2(x1))))) -> 2(5(3(2(4(0(x1))))))
         2(1(0(0(3(x1))))) -> 2(0(1(5(3(0(x1))))))
         2(5(0(0(3(x1))))) -> 1(5(3(0(0(2(x1))))))
         2(4(5(0(3(x1))))) -> 1(2(5(3(0(4(x1))))))
         2(1(0(2(3(x1))))) -> 2(0(1(3(1(2(x1))))))
         2(5(0(2(3(x1))))) -> 5(4(3(2(0(2(x1))))))
         2(5(0(2(3(x1))))) -> 2(2(2(0(3(5(x1))))))
       EDG Processor:
        DPs:
         5#(0(2(1(0(x1))))) -> 2#(5(0(4(x1))))
         2#(5(0(4(2(x1))))) -> 2#(4(0(x1)))
        TRS:
         2(1(0(0(x1)))) -> 0(0(1(3(2(x1)))))
         2(1(0(0(x1)))) -> 2(0(0(1(3(x1)))))
         2(1(0(0(x1)))) -> 1(1(3(2(0(0(x1))))))
         4(0(1(0(x1)))) -> 0(0(4(1(3(x1)))))
         4(0(1(0(x1)))) -> 1(3(0(0(4(3(x1))))))
         4(0(1(0(x1)))) -> 0(5(0(1(3(4(x1))))))
         4(0(1(0(x1)))) -> 0(1(3(4(0(5(x1))))))
         5(0(1(0(x1)))) -> 0(0(1(3(5(3(x1))))))
         5(0(1(0(x1)))) -> 2(0(0(1(3(5(x1))))))
         2(4(1(0(x1)))) -> 0(4(1(3(2(x1)))))
         2(4(1(0(x1)))) -> 4(2(1(3(0(4(x1))))))
         2(4(1(0(x1)))) -> 2(0(1(1(3(4(x1))))))
         4(0(5(0(x1)))) -> 5(3(0(0(4(x1)))))
         4(0(5(0(x1)))) -> 4(3(0(0(5(x1)))))
         5(0(5(0(x1)))) -> 5(0(0(2(5(3(x1))))))
         5(0(5(0(x1)))) -> 0(0(4(5(3(5(x1))))))
         5(0(5(0(x1)))) -> 0(0(4(3(5(5(x1))))))
         2(1(0(2(x1)))) -> 2(1(4(2(0(x1)))))
         2(1(0(2(x1)))) -> 1(2(2(0(5(2(x1))))))
         2(1(0(2(x1)))) -> 0(2(2(3(1(3(x1))))))
         2(4(0(2(x1)))) -> 1(2(2(0(4(x1)))))
         2(4(0(2(x1)))) -> 1(2(1(2(0(4(x1))))))
         2(5(0(2(x1)))) -> 2(2(5(1(2(0(x1))))))
         2(4(0(3(x1)))) -> 2(1(1(4(3(0(x1))))))
         2(4(0(3(x1)))) -> 2(0(1(3(3(4(x1))))))
         2(2(1(0(0(x1))))) -> 1(2(1(2(0(0(x1))))))
         2(3(1(0(0(x1))))) -> 4(0(2(1(3(0(x1))))))
         2(3(1(0(0(x1))))) -> 0(1(3(0(5(2(x1))))))
         2(2(5(0(0(x1))))) -> 1(2(5(2(0(0(x1))))))
         2(5(0(1(0(x1))))) -> 5(3(0(1(2(0(x1))))))
         5(5(0(1(0(x1))))) -> 5(0(0(5(3(1(x1))))))
         5(0(2(1(0(x1))))) -> 0(1(2(5(0(4(x1))))))
         4(0(3(1(0(x1))))) -> 0(4(4(3(0(1(x1))))))
         2(4(3(1(0(x1))))) -> 4(3(0(1(2(4(x1))))))
         2(2(4(1(0(x1))))) -> 2(4(2(0(1(1(x1))))))
         4(2(4(1(0(x1))))) -> 4(1(3(2(0(4(x1))))))
         2(3(4(1(0(x1))))) -> 4(4(0(2(1(3(x1))))))
         5(0(0(3(0(x1))))) -> 0(0(0(1(3(5(x1))))))
         4(0(1(4(0(x1))))) -> 0(4(1(2(0(4(x1))))))
         2(2(3(4(0(x1))))) -> 2(5(3(0(2(4(x1))))))
         4(0(1(5(0(x1))))) -> 0(0(1(4(2(5(x1))))))
         2(4(1(5(0(x1))))) -> 2(1(5(3(0(4(x1))))))
         2(1(0(1(2(x1))))) -> 3(2(0(1(1(2(x1))))))
         2(5(0(4(2(x1))))) -> 2(5(3(2(4(0(x1))))))
         2(1(0(0(3(x1))))) -> 2(0(1(5(3(0(x1))))))
         2(5(0(0(3(x1))))) -> 1(5(3(0(0(2(x1))))))
         2(4(5(0(3(x1))))) -> 1(2(5(3(0(4(x1))))))
         2(1(0(2(3(x1))))) -> 2(0(1(3(1(2(x1))))))
         2(5(0(2(3(x1))))) -> 5(4(3(2(0(2(x1))))))
         2(5(0(2(3(x1))))) -> 2(2(2(0(3(5(x1))))))
        graph:
         5#(0(2(1(0(x1))))) -> 2#(5(0(4(x1)))) ->
         2#(5(0(4(2(x1))))) -> 2#(4(0(x1)))
         2#(5(0(4(2(x1))))) -> 2#(4(0(x1))) -> 2#(5(0(4(2(x1))))) -> 2#(4(0(x1)))
        SCC Processor:
         #sccs: 1
         #rules: 1
         #arcs: 2/4
         DPs:
          2#(5(0(4(2(x1))))) -> 2#(4(0(x1)))
         TRS:
          2(1(0(0(x1)))) -> 0(0(1(3(2(x1)))))
          2(1(0(0(x1)))) -> 2(0(0(1(3(x1)))))
          2(1(0(0(x1)))) -> 1(1(3(2(0(0(x1))))))
          4(0(1(0(x1)))) -> 0(0(4(1(3(x1)))))
          4(0(1(0(x1)))) -> 1(3(0(0(4(3(x1))))))
          4(0(1(0(x1)))) -> 0(5(0(1(3(4(x1))))))
          4(0(1(0(x1)))) -> 0(1(3(4(0(5(x1))))))
          5(0(1(0(x1)))) -> 0(0(1(3(5(3(x1))))))
          5(0(1(0(x1)))) -> 2(0(0(1(3(5(x1))))))
          2(4(1(0(x1)))) -> 0(4(1(3(2(x1)))))
          2(4(1(0(x1)))) -> 4(2(1(3(0(4(x1))))))
          2(4(1(0(x1)))) -> 2(0(1(1(3(4(x1))))))
          4(0(5(0(x1)))) -> 5(3(0(0(4(x1)))))
          4(0(5(0(x1)))) -> 4(3(0(0(5(x1)))))
          5(0(5(0(x1)))) -> 5(0(0(2(5(3(x1))))))
          5(0(5(0(x1)))) -> 0(0(4(5(3(5(x1))))))
          5(0(5(0(x1)))) -> 0(0(4(3(5(5(x1))))))
          2(1(0(2(x1)))) -> 2(1(4(2(0(x1)))))
          2(1(0(2(x1)))) -> 1(2(2(0(5(2(x1))))))
          2(1(0(2(x1)))) -> 0(2(2(3(1(3(x1))))))
          2(4(0(2(x1)))) -> 1(2(2(0(4(x1)))))
          2(4(0(2(x1)))) -> 1(2(1(2(0(4(x1))))))
          2(5(0(2(x1)))) -> 2(2(5(1(2(0(x1))))))
          2(4(0(3(x1)))) -> 2(1(1(4(3(0(x1))))))
          2(4(0(3(x1)))) -> 2(0(1(3(3(4(x1))))))
          2(2(1(0(0(x1))))) -> 1(2(1(2(0(0(x1))))))
          2(3(1(0(0(x1))))) -> 4(0(2(1(3(0(x1))))))
          2(3(1(0(0(x1))))) -> 0(1(3(0(5(2(x1))))))
          2(2(5(0(0(x1))))) -> 1(2(5(2(0(0(x1))))))
          2(5(0(1(0(x1))))) -> 5(3(0(1(2(0(x1))))))
          5(5(0(1(0(x1))))) -> 5(0(0(5(3(1(x1))))))
          5(0(2(1(0(x1))))) -> 0(1(2(5(0(4(x1))))))
          4(0(3(1(0(x1))))) -> 0(4(4(3(0(1(x1))))))
          2(4(3(1(0(x1))))) -> 4(3(0(1(2(4(x1))))))
          2(2(4(1(0(x1))))) -> 2(4(2(0(1(1(x1))))))
          4(2(4(1(0(x1))))) -> 4(1(3(2(0(4(x1))))))
          2(3(4(1(0(x1))))) -> 4(4(0(2(1(3(x1))))))
          5(0(0(3(0(x1))))) -> 0(0(0(1(3(5(x1))))))
          4(0(1(4(0(x1))))) -> 0(4(1(2(0(4(x1))))))
          2(2(3(4(0(x1))))) -> 2(5(3(0(2(4(x1))))))
          4(0(1(5(0(x1))))) -> 0(0(1(4(2(5(x1))))))
          2(4(1(5(0(x1))))) -> 2(1(5(3(0(4(x1))))))
          2(1(0(1(2(x1))))) -> 3(2(0(1(1(2(x1))))))
          2(5(0(4(2(x1))))) -> 2(5(3(2(4(0(x1))))))
          2(1(0(0(3(x1))))) -> 2(0(1(5(3(0(x1))))))
          2(5(0(0(3(x1))))) -> 1(5(3(0(0(2(x1))))))
          2(4(5(0(3(x1))))) -> 1(2(5(3(0(4(x1))))))
          2(1(0(2(3(x1))))) -> 2(0(1(3(1(2(x1))))))
          2(5(0(2(3(x1))))) -> 5(4(3(2(0(2(x1))))))
          2(5(0(2(3(x1))))) -> 2(2(2(0(3(5(x1))))))
         Arctic Interpretation Processor:
          dimension: 1
          interpretation:
           [2#](x0) = x0 + 0,
           
           [5](x0) = 1x0 + 0,
           
           [4](x0) = x0 + 0,
           
           [3](x0) = 7,
           
           [0](x0) = 8,
           
           [1](x0) = x0 + 8,
           
           [2](x0) = x0 + 8
          orientation:
           2#(5(0(4(2(x1))))) = 9 >= 8 = 2#(4(0(x1)))
           
           2(1(0(0(x1)))) = 8 >= 8 = 0(0(1(3(2(x1)))))
           
           2(1(0(0(x1)))) = 8 >= 8 = 2(0(0(1(3(x1)))))
           
           2(1(0(0(x1)))) = 8 >= 8 = 1(1(3(2(0(0(x1))))))
           
           4(0(1(0(x1)))) = 8 >= 8 = 0(0(4(1(3(x1)))))
           
           4(0(1(0(x1)))) = 8 >= 8 = 1(3(0(0(4(3(x1))))))
           
           4(0(1(0(x1)))) = 8 >= 8 = 0(5(0(1(3(4(x1))))))
           
           4(0(1(0(x1)))) = 8 >= 8 = 0(1(3(4(0(5(x1))))))
           
           5(0(1(0(x1)))) = 9 >= 8 = 0(0(1(3(5(3(x1))))))
           
           5(0(1(0(x1)))) = 9 >= 8 = 2(0(0(1(3(5(x1))))))
           
           2(4(1(0(x1)))) = 8 >= 8 = 0(4(1(3(2(x1)))))
           
           2(4(1(0(x1)))) = 8 >= 8 = 4(2(1(3(0(4(x1))))))
           
           2(4(1(0(x1)))) = 8 >= 8 = 2(0(1(1(3(4(x1))))))
           
           4(0(5(0(x1)))) = 8 >= 8 = 5(3(0(0(4(x1)))))
           
           4(0(5(0(x1)))) = 8 >= 7 = 4(3(0(0(5(x1)))))
           
           5(0(5(0(x1)))) = 9 >= 9 = 5(0(0(2(5(3(x1))))))
           
           5(0(5(0(x1)))) = 9 >= 8 = 0(0(4(5(3(5(x1))))))
           
           5(0(5(0(x1)))) = 9 >= 8 = 0(0(4(3(5(5(x1))))))
           
           2(1(0(2(x1)))) = 8 >= 8 = 2(1(4(2(0(x1)))))
           
           2(1(0(2(x1)))) = 8 >= 8 = 1(2(2(0(5(2(x1))))))
           
           2(1(0(2(x1)))) = 8 >= 8 = 0(2(2(3(1(3(x1))))))
           
           2(4(0(2(x1)))) = 8 >= 8 = 1(2(2(0(4(x1)))))
           
           2(4(0(2(x1)))) = 8 >= 8 = 1(2(1(2(0(4(x1))))))
           
           2(5(0(2(x1)))) = 9 >= 9 = 2(2(5(1(2(0(x1))))))
           
           2(4(0(3(x1)))) = 8 >= 8 = 2(1(1(4(3(0(x1))))))
           
           2(4(0(3(x1)))) = 8 >= 8 = 2(0(1(3(3(4(x1))))))
           
           2(2(1(0(0(x1))))) = 8 >= 8 = 1(2(1(2(0(0(x1))))))
           
           2(3(1(0(0(x1))))) = 8 >= 8 = 4(0(2(1(3(0(x1))))))
           
           2(3(1(0(0(x1))))) = 8 >= 8 = 0(1(3(0(5(2(x1))))))
           
           2(2(5(0(0(x1))))) = 9 >= 9 = 1(2(5(2(0(0(x1))))))
           
           2(5(0(1(0(x1))))) = 9 >= 8 = 5(3(0(1(2(0(x1))))))
           
           5(5(0(1(0(x1))))) = 10 >= 9 = 5(0(0(5(3(1(x1))))))
           
           5(0(2(1(0(x1))))) = 9 >= 8 = 0(1(2(5(0(4(x1))))))
           
           4(0(3(1(0(x1))))) = 8 >= 8 = 0(4(4(3(0(1(x1))))))
           
           2(4(3(1(0(x1))))) = 8 >= 7 = 4(3(0(1(2(4(x1))))))
           
           2(2(4(1(0(x1))))) = 8 >= 8 = 2(4(2(0(1(1(x1))))))
           
           4(2(4(1(0(x1))))) = 8 >= 8 = 4(1(3(2(0(4(x1))))))
           
           2(3(4(1(0(x1))))) = 8 >= 8 = 4(4(0(2(1(3(x1))))))
           
           5(0(0(3(0(x1))))) = 9 >= 8 = 0(0(0(1(3(5(x1))))))
           
           4(0(1(4(0(x1))))) = 8 >= 8 = 0(4(1(2(0(4(x1))))))
           
           2(2(3(4(0(x1))))) = 8 >= 8 = 2(5(3(0(2(4(x1))))))
           
           4(0(1(5(0(x1))))) = 8 >= 8 = 0(0(1(4(2(5(x1))))))
           
           2(4(1(5(0(x1))))) = 9 >= 8 = 2(1(5(3(0(4(x1))))))
           
           2(1(0(1(2(x1))))) = 8 >= 7 = 3(2(0(1(1(2(x1))))))
           
           2(5(0(4(2(x1))))) = 9 >= 8 = 2(5(3(2(4(0(x1))))))
           
           2(1(0(0(3(x1))))) = 8 >= 8 = 2(0(1(5(3(0(x1))))))
           
           2(5(0(0(3(x1))))) = 9 >= 8 = 1(5(3(0(0(2(x1))))))
           
           2(4(5(0(3(x1))))) = 9 >= 8 = 1(2(5(3(0(4(x1))))))
           
           2(1(0(2(3(x1))))) = 8 >= 8 = 2(0(1(3(1(2(x1))))))
           
           2(5(0(2(3(x1))))) = 9 >= 8 = 5(4(3(2(0(2(x1))))))
           
           2(5(0(2(3(x1))))) = 9 >= 8 = 2(2(2(0(3(5(x1))))))
          problem:
           DPs:
            
           TRS:
            2(1(0(0(x1)))) -> 0(0(1(3(2(x1)))))
            2(1(0(0(x1)))) -> 2(0(0(1(3(x1)))))
            2(1(0(0(x1)))) -> 1(1(3(2(0(0(x1))))))
            4(0(1(0(x1)))) -> 0(0(4(1(3(x1)))))
            4(0(1(0(x1)))) -> 1(3(0(0(4(3(x1))))))
            4(0(1(0(x1)))) -> 0(5(0(1(3(4(x1))))))
            4(0(1(0(x1)))) -> 0(1(3(4(0(5(x1))))))
            5(0(1(0(x1)))) -> 0(0(1(3(5(3(x1))))))
            5(0(1(0(x1)))) -> 2(0(0(1(3(5(x1))))))
            2(4(1(0(x1)))) -> 0(4(1(3(2(x1)))))
            2(4(1(0(x1)))) -> 4(2(1(3(0(4(x1))))))
            2(4(1(0(x1)))) -> 2(0(1(1(3(4(x1))))))
            4(0(5(0(x1)))) -> 5(3(0(0(4(x1)))))
            4(0(5(0(x1)))) -> 4(3(0(0(5(x1)))))
            5(0(5(0(x1)))) -> 5(0(0(2(5(3(x1))))))
            5(0(5(0(x1)))) -> 0(0(4(5(3(5(x1))))))
            5(0(5(0(x1)))) -> 0(0(4(3(5(5(x1))))))
            2(1(0(2(x1)))) -> 2(1(4(2(0(x1)))))
            2(1(0(2(x1)))) -> 1(2(2(0(5(2(x1))))))
            2(1(0(2(x1)))) -> 0(2(2(3(1(3(x1))))))
            2(4(0(2(x1)))) -> 1(2(2(0(4(x1)))))
            2(4(0(2(x1)))) -> 1(2(1(2(0(4(x1))))))
            2(5(0(2(x1)))) -> 2(2(5(1(2(0(x1))))))
            2(4(0(3(x1)))) -> 2(1(1(4(3(0(x1))))))
            2(4(0(3(x1)))) -> 2(0(1(3(3(4(x1))))))
            2(2(1(0(0(x1))))) -> 1(2(1(2(0(0(x1))))))
            2(3(1(0(0(x1))))) -> 4(0(2(1(3(0(x1))))))
            2(3(1(0(0(x1))))) -> 0(1(3(0(5(2(x1))))))
            2(2(5(0(0(x1))))) -> 1(2(5(2(0(0(x1))))))
            2(5(0(1(0(x1))))) -> 5(3(0(1(2(0(x1))))))
            5(5(0(1(0(x1))))) -> 5(0(0(5(3(1(x1))))))
            5(0(2(1(0(x1))))) -> 0(1(2(5(0(4(x1))))))
            4(0(3(1(0(x1))))) -> 0(4(4(3(0(1(x1))))))
            2(4(3(1(0(x1))))) -> 4(3(0(1(2(4(x1))))))
            2(2(4(1(0(x1))))) -> 2(4(2(0(1(1(x1))))))
            4(2(4(1(0(x1))))) -> 4(1(3(2(0(4(x1))))))
            2(3(4(1(0(x1))))) -> 4(4(0(2(1(3(x1))))))
            5(0(0(3(0(x1))))) -> 0(0(0(1(3(5(x1))))))
            4(0(1(4(0(x1))))) -> 0(4(1(2(0(4(x1))))))
            2(2(3(4(0(x1))))) -> 2(5(3(0(2(4(x1))))))
            4(0(1(5(0(x1))))) -> 0(0(1(4(2(5(x1))))))
            2(4(1(5(0(x1))))) -> 2(1(5(3(0(4(x1))))))
            2(1(0(1(2(x1))))) -> 3(2(0(1(1(2(x1))))))
            2(5(0(4(2(x1))))) -> 2(5(3(2(4(0(x1))))))
            2(1(0(0(3(x1))))) -> 2(0(1(5(3(0(x1))))))
            2(5(0(0(3(x1))))) -> 1(5(3(0(0(2(x1))))))
            2(4(5(0(3(x1))))) -> 1(2(5(3(0(4(x1))))))
            2(1(0(2(3(x1))))) -> 2(0(1(3(1(2(x1))))))
            2(5(0(2(3(x1))))) -> 5(4(3(2(0(2(x1))))))
            2(5(0(2(3(x1))))) -> 2(2(2(0(3(5(x1))))))
          Qed