public static void resolveUnresolvedSlotReferences(Stella_Object formula) {
    { Proposition proposition = null;
      Cons unresolvedpropositions = null;
      KeyValueList variabletypestable = null;
      Cons unresolvablepropositions = Stella.NIL;

      { Surrogate testValue000 = Stella_Object.safePrimaryType(formula);

        if (Surrogate.subtypeOfP(testValue000, Logic.SGT_LOGIC_DESCRIPTION)) {
          { Description formula000 = ((Description)(formula));

            proposition = formula000.proposition;
          }
        }
        else if (Surrogate.subtypeOfP(testValue000, Logic.SGT_LOGIC_PROPOSITION)) {
          { Proposition formula000 = ((Proposition)(formula));

            proposition = formula000;
          }
        }
        else {
          { OutputStringStream stream000 = OutputStringStream.newOutputStringStream();

            stream000.nativeStream.print("`" + testValue000 + "' is not a valid case option");
            throw ((StellaException)(StellaException.newStellaException(stream000.theStringReader()).fillInStackTrace()));
          }
        }
      }
      unresolvedpropositions = Proposition.collectUnresolvedSlotReferences(proposition);
      if (unresolvedpropositions == Stella.NIL) {
        return;
      }
      { Surrogate testValue001 = Stella_Object.safePrimaryType(formula);

        if (Surrogate.subtypeOfP(testValue001, Logic.SGT_LOGIC_DESCRIPTION)) {
          { Description formula000 = ((Description)(formula));

            variabletypestable = Description.inferVariableTypesInDescription(formula000);
          }
        }
        else if (Surrogate.subtypeOfP(testValue001, Logic.SGT_LOGIC_PROPOSITION)) {
          { Proposition formula000 = ((Proposition)(formula));

            variabletypestable = Proposition.inferVariableTypesInProposition(formula000, Stella.NIL);
          }
        }
        else {
          { OutputStringStream stream001 = OutputStringStream.newOutputStringStream();

            stream001.nativeStream.print("`" + testValue001 + "' is not a valid case option");
            throw ((StellaException)(StellaException.newStellaException(stream001.theStringReader()).fillInStackTrace()));
          }
        }
      }
      { Proposition prop = null;
        Cons iter000 = unresolvedpropositions;
        Cons collect000 = null;

        for (;!(iter000 == Stella.NIL); iter000 = iter000.rest) {
          prop = ((Proposition)(iter000.value));
          if (Stella_Object.symbolP(prop.operator) &&
              (!Proposition.resolveOneSlotReferenceP(prop, variabletypestable))) {
            if (collect000 == null) {
              {
                collect000 = Cons.cons(prop, Stella.NIL);
                if (unresolvablepropositions == Stella.NIL) {
                  unresolvablepropositions = collect000;
                }
                else {
                  Cons.addConsToEndOfConsList(unresolvablepropositions, collect000);
                }
              }
            }
            else {
              {
                collect000.rest = Cons.cons(prop, Stella.NIL);
                collect000 = collect000.rest;
              }
            }
          }
        }
      }
      if (!(unresolvablepropositions == Stella.NIL)) {
        { Proposition p = null;
          Cons iter001 = unresolvablepropositions;

          for (;!(iter001 == Stella.NIL); iter001 = iter001.rest) {
            p = ((Proposition)(iter001.value));
            Proposition.complainAboutUndeclaredReference(p);
            Proposition.createDummyRelation(p);
          }
        }
      }
    }
  }