public static Keyword continueFailProof(ControlFrame frame, Keyword lastmove) {
    if (lastmove == Logic.KWD_DOWN) {
      ControlFrame.createChoicePoint(frame);
      KeyValueList.setDynamicSlotValue(frame.dynamicSlots, Logic.SYM_LOGIC_INFERENCE_CUTOFF_REASON, null, null);
      return (Logic.KWD_MOVE_DOWN);
    }
    else if (lastmove == Logic.KWD_UP_TRUE) {
      { Keyword result = (frame.reversePolarityP ? Logic.KWD_FINAL_SUCCESS : Logic.KWD_FAILURE);

        if (frame.reversePolarityP) {
          ControlFrame.setFrameTruthValue(frame, Logic.TRUE_TRUTH_VALUE);
          if (((Boolean)(Logic.$RECORD_JUSTIFICATIONSp$.get())).booleanValue()) {
            ControlFrame.recordNegatedFailJustification(frame, lastmove);
          }
        }
        else {
          ControlFrame.setFrameTruthValue(frame, Logic.FALSE_TRUTH_VALUE);
        }
        PatternRecord.unbindVariablesBeginningAt(((QueryIterator)(Logic.$QUERYITERATOR$.get())).currentPatternRecord, frame.choicePointUnbindingOffset);
        if (frame.down != null) {
          ControlFrame.popFramesUpTo(frame.down);
        }
        return (result);
      }
    }
    else if (lastmove == Logic.KWD_UP_FAIL) {
      { Keyword result = (frame.reversePolarityP ? Logic.KWD_FAILURE : Logic.KWD_FINAL_SUCCESS);

        if (((Keyword)(KeyValueList.dynamicSlotValue(frame.dynamicSlots, Logic.SYM_LOGIC_INFERENCE_CUTOFF_REASON, null))) != null) {
          ControlFrame.setFrameTruthValue(frame, Logic.UNKNOWN_TRUTH_VALUE);
          result = Logic.KWD_FAILURE;
        }
        else if (frame.result.truthValue == Logic.INCONSISTENT_TRUTH_VALUE) {
          ControlFrame.setFrameTruthValue(frame, Logic.INCONSISTENT_TRUTH_VALUE);
          result = Logic.KWD_TERMINAL_FAILURE;
        }
        else if (frame.reversePolarityP) {
          ControlFrame.setFrameTruthValue(frame, Logic.FALSE_TRUTH_VALUE);
        }
        else {
          ControlFrame.setFrameTruthValue(frame, Logic.TRUE_TRUTH_VALUE);
          if (((Boolean)(Logic.$RECORD_JUSTIFICATIONSp$.get())).booleanValue()) {
            if (frame.up.proposition.kind == Logic.KWD_NOT) {
              ControlFrame.recordClosedNotJustification(frame, lastmove);
            }
            else {
              ControlFrame.recordFailJustification(frame, lastmove);
            }
          }
        }
        PatternRecord.unbindVariablesBeginningAt(((QueryIterator)(Logic.$QUERYITERATOR$.get())).currentPatternRecord, frame.choicePointUnbindingOffset);
        return (result);
      }
    }
    else {
      { OutputStringStream stream000 = OutputStringStream.newOutputStringStream();

        stream000.nativeStream.print("`" + lastmove + "' is not a valid case option");
        throw ((StellaException)(StellaException.newStellaException(stream000.theStringReader()).fillInStackTrace()));
      }
    }
  }