public static Keyword tryImpliesProof(ControlFrame frame) {
    { Proposition proposition = frame.proposition;
      Stella_Object subcollectionarg = (proposition.arguments.theArray)[0];
      Stella_Object supercollectionarg = (proposition.arguments.theArray)[1];
      Stella_Object subcollection = Logic.argumentBoundTo(subcollectionarg);
      Stella_Object supercollection = Logic.argumentBoundTo(supercollectionarg);

      if ((subcollection == null) ||
          (supercollection == null)) {
        return (Logic.KWD_FAILURE);
      }
      if ((!Logic.inferableDescriptionP(subcollection)) &&
          ((!Logic.inferableDescriptionP(supercollection)) &&
           (Logic.closedTermP(subcollection) ||
            frame.reversePolarityP))) {
        { Keyword testValue000 = Logic.trySimpleContainedByProof(subcollection, supercollection, frame.reversePolarityP);

          if (testValue000 == Logic.KWD_FINAL_SUCCESS) {
            ControlFrame.setFrameTruthValue(frame, Logic.TRUE_TRUTH_VALUE);
            return (Logic.KWD_FINAL_SUCCESS);
          }
          else if (testValue000 == Logic.KWD_TERMINAL_FAILURE) {
            ControlFrame.setFrameTruthValue(frame, Logic.FALSE_TRUTH_VALUE);
            return (Logic.KWD_TERMINAL_FAILURE);
          }
          else {
          }
        }
      }
      if (Stella_Object.isaP(subcollection, Logic.SGT_LOGIC_DESCRIPTION) &&
          Stella_Object.isaP(supercollection, Logic.SGT_LOGIC_DESCRIPTION)) {
        ControlFrame.pushNextStrategy(frame, Logic.KWD_SUBSUMPTION_TEST);
      }
      if (Logic.closedTermP(subcollection)) {
        ControlFrame.pushNextStrategy(frame, Logic.KWD_CONTAINED_BY);
      }
      return (Logic.KWD_FAILURE);
    }
  }