WEIGHTED TERM ORDER

establishes a graduated ordering similar to gradlex term order, where the exponents first are multiplied by the given weights. If there are less weight values than variables, the weight list is extended by ones. If the weighted degree comparison is not decidable, the lex term order is used.