* @return Proposition
   */
  public static Proposition destroyProposition(Proposition proposition) {
    if (proposition.deletedP()) {
      return (proposition);
    }
    proposition.deletedPSetter(true);
    if (((Surrogate)(KeyValueList.dynamicSlotValue(proposition.dynamicSlots, Logic.SYM_STELLA_SURROGATE_VALUE_INVERSE, null))) != null) {
      ((Surrogate)(KeyValueList.dynamicSlotValue(proposition.dynamicSlots, Logic.SYM_STELLA_SURROGATE_VALUE_INVERSE, null))).surrogateValue = null;
    }
    { Stella_Object arg = null;
      Vector vector000 = proposition.arguments;
      int index000 = 0;
      int length000 = vector000.length();

      for (;index000 < length000; index000 = index000 + 1) {
        arg = (vector000.theArray)[index000];
        if ((arg != null) &&
            (!arg.deletedP())) {
          if (Logic.skolemP(arg) &&
              (((Skolem)(arg)).definingProposition == proposition)) {
            LogicObject.destroyTerm(((LogicObject)(arg)));
          }
          Logic.removeDependentPropositionLink(arg, proposition);
        }
      }
    }
    { Stella_Object dep = null;
      Iterator iter000 = proposition.dependentPropositions.copy().allocateIterator();

      while (iter000.nextP()) {
        dep = iter000.value;
        Proposition.destroyProposition(((Proposition)(dep)));
      }
    }
    { Proposition satellite = null;
      Cons iter001 = proposition.satellitePropositions().copy().theConsList;

      for (;!(iter001 == Stella.NIL); iter001 = iter001.rest) {
        satellite = ((Proposition)(iter001.value));
        Proposition.destroyProposition(satellite);
      }
    }
    if (((Proposition)(KeyValueList.dynamicSlotValue(proposition.dynamicSlots, Logic.SYM_LOGIC_MASTER_PROPOSITION, null))) != null) {
      ((Proposition)(KeyValueList.dynamicSlotValue(proposition.dynamicSlots, Logic.SYM_LOGIC_MASTER_PROPOSITION, null))).satellitePropositions().remove(proposition);
    }
    if (!(proposition.homeContext == null)) {
      Logic.handleOutOfDateInferenceCache(Logic.KWD_RETRACT, proposition);
    }
    proposition.dependentPropositions = null;
    proposition.operator = null;
    proposition.arguments = null;
    proposition.homeContext = null;
    proposition.truthValue = null;
    proposition.dynamicSlots = null;
    return (proposition);
  }