public static Keyword continueStrategiesProofs(ControlFrame frame, Keyword lastmove) {
    { Keyword result = null;

      if (lastmove == Logic.KWD_DOWN) {
        ControlFrame.unwindToChoicePoint(frame);
        frame.justifications.clear();
        if (frame.down != null) {
          return (Logic.KWD_MOVE_DOWN);
        }
      }
      else if ((lastmove == Logic.KWD_UP_TRUE) ||
          (lastmove == Logic.KWD_UP_FAIL)) {
        result = ControlFrame.resumeProofStrategyAfterSubgoal(frame, lastmove);
        if (result == Logic.KWD_FAILURE) {
          result = null;
        }
      }
      else {
        { OutputStringStream stream000 = OutputStringStream.newOutputStringStream();

          stream000.nativeStream.print("`" + lastmove + "' is not a valid case option");
          throw ((StellaException)(StellaException.newStellaException(stream000.theStringReader()).fillInStackTrace()));
        }
      }
      loop000 : for (;;) {
        if (result == null) {
          result = ControlFrame.continueCurrentOrNextStrategy(frame);
        }
        if ((result == Logic.KWD_FINAL_SUCCESS) ||
            (result == Logic.KWD_CONTINUING_SUCCESS)) {
          if ((frame.proposition != null) &&
              (((frame.truthValue == Logic.DEFAULT_TRUE_TRUTH_VALUE) ||
              (frame.truthValue == Logic.DEFAULT_FALSE_TRUTH_VALUE)) &&
               ControlFrame.hasShallowDisproofP(frame))) {
            if (Stella_Object.traceKeywordP(Logic.KWD_GOAL_TREE)) {
              { TruthValue truthvalue = frame.truthValue;
                boolean defaultP = (truthvalue == Logic.DEFAULT_TRUE_TRUTH_VALUE) ||
                    (truthvalue == Logic.DEFAULT_FALSE_TRUTH_VALUE);

                Logic.printVerticalBars(ControlFrame.computeFrameDepth(frame) + 1);
                System.out.println("CLSH: truth=" + TruthValue.truthValueToString(truthvalue, true));
              }
            }
            ControlFrame.unwindToChoicePoint(frame);
            if ((!((frame.truthValue == Logic.DEFAULT_TRUE_TRUTH_VALUE) ||
                (frame.truthValue == Logic.DEFAULT_FALSE_TRUTH_VALUE))) &&
                Proposition.allArgumentsBoundP(frame.proposition)) {
              result = Logic.KWD_FAILURE;
            }
            else {
              ControlFrame.setFrameTruthValue(frame, null);
              frame.justifications.clear();
              if (frame.partialMatchFrame != null) {
                frame.partialMatchFrame.clearFramePartialTruth();
              }
              if (frame.down != null) {
                result = Logic.KWD_MOVE_DOWN;
              }
              else {
                result = null;
                continue loop000;
              }
            }
          }
        }
        else {
        }
        if ((result == Logic.KWD_CONTINUING_SUCCESS) ||
            (result == Logic.KWD_FINAL_SUCCESS)) {
          if (frame.truthValue == null) {
            ControlFrame.setFrameTruthValue(frame, Logic.TRUE_TRUTH_VALUE);
          }
          if (((((QueryIterator)(Logic.$QUERYITERATOR$.get())) != null) &&
              (((QueryIterator)(Logic.$QUERYITERATOR$.get())).partialMatchStrategy != null)) &&
              (!((frame.partialMatchFrame != null) &&
              ((frame.partialMatchFrame.positiveScore != Stella.NULL_FLOAT) ||
               (frame.partialMatchFrame.negativeScore != Stella.NULL_FLOAT))))) {
            frame.partialMatchFrame.setFramePartialTruth(Logic.TRUE_TRUTH_VALUE, Stella.NULL_FLOAT, Stella.NULL_FLOAT, false);
          }
          if (((Boolean)(Logic.$RECORD_JUSTIFICATIONSp$.get())).booleanValue() &&
              (((Justification)(KeyValueList.dynamicSlotValue(frame.dynamicSlots, Logic.SYM_LOGIC_JUSTIFICATION, null))) == null)) {
            ControlFrame.recordPrimitiveJustification(frame, Logic.KWD_UP_TRUE);
          }
        }
        else if ((result == Logic.KWD_FAILURE) ||
            (result == Logic.KWD_TERMINAL_FAILURE)) {
          if ((((QueryIterator)(Logic.$QUERYITERATOR$.get())) != null) &&
              (((QueryIterator)(Logic.$QUERYITERATOR$.get())).partialMatchStrategy != null)) {
            {
              if (!((frame.partialMatchFrame != null) &&
                  ((frame.partialMatchFrame.positiveScore != Stella.NULL_FLOAT) ||
                   (frame.partialMatchFrame.negativeScore != Stella.NULL_FLOAT)))) {
                frame.partialMatchFrame.setFramePartialTruth(frame.truthValue, ((frame.truthValue != null) ? Stella.NULL_FLOAT : 0.0), Stella.NULL_FLOAT, frame.truthValue != null);
              }
              if (((Boolean)(Logic.$RECORD_JUSTIFICATIONSp$.get())).booleanValue() &&
                  (((Justification)(KeyValueList.dynamicSlotValue(frame.dynamicSlots, Logic.SYM_LOGIC_JUSTIFICATION, null))) == null)) {
                ControlFrame.recordPrimitiveJustification(frame, Logic.KWD_UP_FAIL);
              }
            }
          }
          else {
            if (((frame.truthValue == Logic.UNKNOWN_TRUTH_VALUE) ||
                (frame.truthValue == null)) &&
                ((((Keyword)(KeyValueList.dynamicSlotValue(frame.dynamicSlots, Logic.SYM_LOGIC_INFERENCE_CUTOFF_REASON, null))) == null) &&
                 ((frame.proposition != null) &&
                  Proposition.closedPropositionP(frame.proposition)))) {
              ControlFrame.setFrameTruthValue(frame, Logic.FALSE_TRUTH_VALUE);
              if (((Boolean)(Logic.$RECORD_JUSTIFICATIONSp$.get())).booleanValue() &&
                  (((Justification)(KeyValueList.dynamicSlotValue(frame.dynamicSlots, Logic.SYM_LOGIC_JUSTIFICATION, null))) == null)) {
                ControlFrame.recordClosedNotJustification(frame, Logic.KWD_UP_FAIL);
              }
            }
          }
        }
        else {
        }
        return (result);
      }
    }
  }