public static Cons generalizeInequality(Cons probe, Cons match, List bindings) {
    { Stella_Object operator = probe.value;
      Cons newClause = Cons.consList(Cons.cons(operator, Stella.NIL));
      Symbol var = null;

      { Stella_Object arg1 = null;
        Cons iter000 = probe.rest;
        Stella_Object arg2 = null;
        Cons iter001 = match.rest;

        for (;(!(iter000 == Stella.NIL)) &&
                  (!(iter001 == Stella.NIL)); iter000 = iter000.rest, iter001 = iter001.rest) {
          arg1 = iter000.value;
          arg2 = iter001.value;
          if (!Stella_Object.equalConsTreesP(arg1, arg2)) {
            if (Logic.bothNumbersP(arg1, arg2)) {
              { GeneralizedSymbol testValue000 = ((GeneralizedSymbol)(operator));

                if ((testValue000 == Logic.SYM_STELLA_g) ||
                    (testValue000 == Logic.SYM_STELLA_ge)) {
                  newClause = Cons.cons(((NumberWrapper)(arg1)).min(((NumberWrapper)(arg2))), newClause);
                }
                else if ((testValue000 == Logic.SYM_STELLA_l) ||
                    (testValue000 == Logic.SYM_STELLA_el)) {
                  newClause = Cons.cons(((NumberWrapper)(arg1)).max(((NumberWrapper)(arg2))), newClause);
                }
                else {
                  System.out.println("Bug in generalize-inequality.");
                }
              }
            }
            else {
              {
                var = ((Symbol)(Logic.lookupVariableInBindings(arg1, arg2, bindings)));
                if (var == null) {
                  var = Symbol.internSymbol("?X" + Native.stringify(IntegerWrapper.wrapInteger(((Integer)(Logic.$BOTTOM_UP_VARIABLE_COUNTER$.get())).intValue())));
                  if (!Logic.eitherNumbersP(arg1, arg2)) {
                    bindings.push(Cons.consList(Cons.cons(arg1, Cons.cons(arg2, Cons.cons(var, Stella.NIL)))));
                  }
                  Native.setIntSpecial(Logic.$BOTTOM_UP_VARIABLE_COUNTER$, ((Integer)(Logic.$BOTTOM_UP_VARIABLE_COUNTER$.get())).intValue() + 1);
                }
                newClause = Cons.cons(var, newClause);
              }
            }
          }
          else {
            newClause = Cons.cons(arg1, newClause);
          }
        }
      }
      return (newClause.reverse());
    }
  }