public static Keyword continueAntecedentsProof(ControlFrame frame, Keyword lastmove) {
    { Iterator iterator = ((Iterator)(KeyValueList.dynamicSlotValue(frame.dynamicSlots, Logic.SYM_STELLA_ITERATOR, null)));
      boolean firsttimeP = iterator == null;
      boolean reversepolarityP = frame.reversePolarityP;

      if (lastmove == Logic.KWD_UP_TRUE) {
        { Proposition object000 = ((Proposition)(KeyValueList.dynamicSlotValue(frame.dynamicSlots, Logic.SYM_LOGIC_ANTECEDENTS_RULE, null)));
          Stella_Object oldValue000 = object000.truthValue;

          frame.truthValue = TruthValue.weakenTruthValue(ControlFrame.propagateFrameTruthValue(frame.result, frame), ((TruthValue)(Stella_Object.accessInContext(oldValue000, object000.homeContext, false))));
        }
        if (((Boolean)(Logic.$RECORD_JUSTIFICATIONSp$.get())).booleanValue()) {
          ControlFrame.recordModusPonensJustification(frame, lastmove);
        }
        return (Logic.KWD_CONTINUING_SUCCESS);
      }
      else {
      }
      if (firsttimeP) {
        iterator = Description.allocateAntecedentsIterator(ControlFrame.extractSubgoalDescriptionOfFrame(frame), ControlFrame.findExternalArgumentsForSubgoal(frame), reversepolarityP);
        if (iterator == null) {
          return (Logic.KWD_FAILURE);
        }
        KeyValueList.setDynamicSlotValue(frame.dynamicSlots, Logic.SYM_STELLA_ITERATOR, iterator, null);
      }
      loop000 : while (iterator.nextP()) {
        { Proposition impliesproposition = ((Proposition)(iterator.value));
          Description antecedentdescription = (reversepolarityP ? ((Description)((impliesproposition.arguments.theArray)[1])) : ((Description)((impliesproposition.arguments.theArray)[0])));

          if (ControlFrame.checkForDuplicateRuleP(frame, impliesproposition)) {
            continue loop000;
          }
          KeyValueList.setDynamicSlotValue(frame.dynamicSlots, Logic.SYM_LOGIC_ANTECEDENTS_RULE, impliesproposition, null);
          if (!Proposition.trueP(impliesproposition)) {
            if (Proposition.getForwardGoals(impliesproposition).emptyP()) {
              continue loop000;
            }
            else {
              {
                ControlFrame.createConditionalAntecedentSubframe(frame, frame.proposition, impliesproposition);
                return (Logic.KWD_MOVE_DOWN);
              }
            }
          }
          { ControlFrame downframe = ControlFrame.createSubgoalFrame(frame, null, Logic.KWD_FULL_SUBQUERY);

            KeyValueList.setDynamicSlotValue(downframe.dynamicSlots, Logic.SYM_LOGIC_DESCRIPTION, antecedentdescription, null);
            return (Logic.KWD_MOVE_DOWN);
          }
        }
      }
      return (Logic.KWD_FAILURE);
    }
  }