public static Keyword continueClusteredConjunctionProof(ControlFrame andframe, Keyword lastmove) {
    { Keyword state = andframe.state;
      ClusteredConjunctionProofAdjunct adjunct = ((ClusteredConjunctionProofAdjunct)(((ProofAdjunct)(KeyValueList.dynamicSlotValue(andframe.dynamicSlots, Logic.SYM_LOGIC_PROOF_ADJUNCT, null)))));
      Proposition proposition = andframe.proposition;
      Vector arguments = proposition.arguments;
      int nofarguments = arguments.length();
      ControlFrame downframe = null;

      if ((((QueryIterator)(Logic.$QUERYITERATOR$.get())) != null) &&
          (((QueryIterator)(Logic.$QUERYITERATOR$.get())).partialMatchStrategy != null)) {
        andframe.state = Logic.KWD_AND;
        lastmove = ControlFrame.oldInterpretAndScores(andframe, lastmove);
        andframe.state = state;
      }
      if (lastmove == Logic.KWD_DOWN) {
        if (adjunct == null) {
          { ClusteredConjunctionProofAdjunct self000 = ClusteredConjunctionProofAdjunct.newClusteredConjunctionProofAdjunct();

            self000.clusterFrames = Vector.newVector(nofarguments);
            adjunct = self000;
          }
          KeyValueList.setDynamicSlotValue(andframe.dynamicSlots, Logic.SYM_LOGIC_PROOF_ADJUNCT, adjunct, null);
        }
        downframe = ((ControlFrame)((adjunct.clusterFrames.theArray)[(andframe.argumentCursor)]));
        if (downframe == null) {
          ControlFrame.createSubgoalFrame(andframe, ((Proposition)((arguments.theArray)[(andframe.argumentCursor)])), null);
        }
        else {
          andframe.down = downframe;
        }
        return (Logic.KWD_MOVE_DOWN);
      }
      else if (lastmove == Logic.KWD_UP_TRUE) {
        andframe.truthValue = ((andframe.truthValue == null) ? andframe.result.truthValue : TruthValue.conjoinTruthValues(andframe.truthValue, andframe.result.truthValue));
        if (((Boolean)(Logic.$RECORD_JUSTIFICATIONSp$.get())).booleanValue()) {
          ControlFrame.recordAndIntroductionJustification(andframe, lastmove);
        }
        (adjunct.clusterFrames.theArray)[(andframe.argumentCursor)] = (andframe.down);
        if ((andframe.argumentCursor + 1) == nofarguments) {
          { int i = Stella.NULL_INTEGER;
            int iter000 = 1;
            int upperBound000 = nofarguments;
            boolean unboundedP000 = upperBound000 == Stella.NULL_INTEGER;

            for (;unboundedP000 ||
                      (iter000 <= upperBound000); iter000 = iter000 + 1) {
              i = iter000;
              if (((ControlFrame)((adjunct.clusterFrames.theArray)[(nofarguments - i)])) != null) {
                andframe.argumentCursor = nofarguments - i;
                andframe.down = ((ControlFrame)((adjunct.clusterFrames.theArray)[(andframe.argumentCursor)]));
                return (Logic.KWD_CONTINUING_SUCCESS);
              }
            }
          }
          andframe.down = null;
          return (Logic.KWD_FINAL_SUCCESS);
        }
        else {
          andframe.argumentCursor = andframe.argumentCursor + 1;
          downframe = ((ControlFrame)((adjunct.clusterFrames.theArray)[(andframe.argumentCursor)]));
          if (downframe == null) {
            ControlFrame.createSubgoalFrame(andframe, ((Proposition)((arguments.theArray)[(andframe.argumentCursor)])), null);
          }
          else {
            andframe.down = downframe;
          }
          return (Logic.KWD_MOVE_DOWN);
        }
      }
      else if (lastmove == Logic.KWD_UP_FAIL) {
        if ((((QueryIterator)(Logic.$QUERYITERATOR$.get())) != null) &&
            (((QueryIterator)(Logic.$QUERYITERATOR$.get())).partialMatchStrategy != null)) {
          andframe.down = null;
          ControlFrame.setFrameTruthValue(andframe, null);
          return (Logic.KWD_TERMINAL_FAILURE);
        }
        if (((ControlFrame)((adjunct.clusterFrames.theArray)[(andframe.argumentCursor)])) == null) {
          { Keyword testValue000 = ((Proposition)((arguments.theArray)[(andframe.argumentCursor)])).kind;

            if ((testValue000 == Logic.KWD_AND) ||
                ((testValue000 == Logic.KWD_FUNCTION) ||
                 ((testValue000 == Logic.KWD_PREDICATE) ||
                  (testValue000 == Logic.KWD_IMPLIES)))) {
              andframe.down = null;
              ControlFrame.setFrameTruthValue(andframe, null);
              return (Logic.KWD_TERMINAL_FAILURE);
            }
            else {
            }
          }
        }
        (adjunct.clusterFrames.theArray)[(andframe.argumentCursor)] = null;
        { int i = Stella.NULL_INTEGER;
          int iter001 = 1;
          int upperBound001 = andframe.argumentCursor;
          boolean unboundedP001 = upperBound001 == Stella.NULL_INTEGER;

          for (;unboundedP001 ||
                    (iter001 <= upperBound001); iter001 = iter001 + 1) {
            i = iter001;
            if (((ControlFrame)((adjunct.clusterFrames.theArray)[(andframe.argumentCursor - i)])) != null) {
              andframe.argumentCursor = andframe.argumentCursor - i;
              andframe.down = ((ControlFrame)((adjunct.clusterFrames.theArray)[(andframe.argumentCursor)]));
              return (Logic.KWD_MOVE_DOWN);
            }
          }
        }
        andframe.down = null;
        ControlFrame.setFrameTruthValue(andframe, null);
        return (Logic.KWD_TERMINAL_FAILURE);
      }
      else {
        { OutputStringStream stream000 = OutputStringStream.newOutputStringStream();

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