public static Keyword tryScanPropositionsProof(ControlFrame frame) {
    { Proposition proposition = frame.proposition;
      boolean allkeyargumentsboundP = false;
      Iterator iterator = ((Iterator)(KeyValueList.dynamicSlotValue(frame.dynamicSlots, Logic.SYM_STELLA_ITERATOR, null)));
      Keyword result = Logic.KWD_FAILURE;

      if (iterator == null) {
        allkeyargumentsboundP = Proposition.allArgumentsBoundP(proposition) ||
            Proposition.allKeyArgumentsBoundP(proposition);
        iterator = Proposition.allMatchingPropositions(proposition);
        if (iterator == Logic.EMPTY_PROPOSITIONS_ITERATOR) {
          iterator = null;
        }
        else {
          KeyValueList.setDynamicSlotValue(frame.dynamicSlots, Logic.SYM_STELLA_ITERATOR, iterator, null);
        }
        if (((((QueryIterator)(Logic.$QUERYITERATOR$.get())) != null) &&
            (((QueryIterator)(Logic.$QUERYITERATOR$.get())).partialMatchStrategy != null)) &&
            ((frame.currentStrategy == Logic.KWD_LOOKUP_ASSERTIONS) &&
             ((proposition.arguments.length() > 1) &&
              Logic.nullInstancePropositionsExistP()))) {
          ControlFrame.pushNextStrategy(frame, Logic.KWD_SCAN_PARTIAL_PROPOSITIONS);
        }
      }
      if (iterator != null) {
        loop000 : while (iterator.nextP()) {
          if (Proposition.argumentsUnifyWithArgumentsP(((Proposition)(iterator.value)), proposition)) {
            if (allkeyargumentsboundP &&
                ((!((Boolean)(Logic.$GENERATE_ALL_PROOFSp$.get())).booleanValue()) ||
                 (((((QueryIterator)(Logic.$QUERYITERATOR$.get())) != null) &&
                (((QueryIterator)(Logic.$QUERYITERATOR$.get())).partialMatchStrategy != null)) &&
                  Stella_Object.isaP(((QueryIterator)(Logic.$QUERYITERATOR$.get())).partialMatchStrategy, Logic.SGT_LOGIC_WHYNOT_PARTIAL_MATCH)))) {
              result = Logic.KWD_FINAL_SUCCESS;
              break loop000;
            }
            else {
              result = Logic.KWD_CONTINUING_SUCCESS;
              break loop000;
            }
          }
        }
      }
      if ((result == Logic.KWD_FAILURE) &&
          (frame.reversePolarityP &&
           ((!(frame.currentStrategy == Logic.KWD_SHALLOW_DISPROOF)) &&
            (((proposition.kind == Logic.KWD_FUNCTION) ||
          Proposition.singleValuedPredicateP(proposition)) &&
             Proposition.allArgumentsBoundP(proposition))))) {
        ControlFrame.pushNextStrategy(frame, Logic.KWD_SCAN_FOR_VALUE_CLASH);
      }
      if (!(result == Logic.KWD_FAILURE)) {
        { TruthValue truthvalue = Logic.propositionsIteratorTruthValue(iterator);
          Proposition matchingProposition = ((Proposition)(iterator.value));
          double weight = ((FloatWrapper)(KeyValueList.dynamicSlotValue(matchingProposition.dynamicSlots, Logic.SYM_LOGIC_WEIGHT, Stella.NULL_FLOAT_WRAPPER))).wrapperValue;

          if ((truthvalue == Logic.DEFAULT_TRUE_TRUTH_VALUE) ||
              (truthvalue == Logic.DEFAULT_FALSE_TRUTH_VALUE)) {
            { Object old$DontusedefaultknowledgeP$000 = Logic.$DONTUSEDEFAULTKNOWLEDGEp$.get();

              try {
                Native.setBooleanSpecial(Logic.$DONTUSEDEFAULTKNOWLEDGEp$, true);
                iterator = Proposition.allMatchingPropositions(proposition);
                if (iterator.nextP()) {
                  truthvalue = Logic.propositionsIteratorTruthValue(iterator);
                  matchingProposition = ((Proposition)(iterator.value));
                  weight = ((FloatWrapper)(KeyValueList.dynamicSlotValue(matchingProposition.dynamicSlots, Logic.SYM_LOGIC_WEIGHT, Stella.NULL_FLOAT_WRAPPER))).wrapperValue;
                }

              } finally {
                Logic.$DONTUSEDEFAULTKNOWLEDGEp$.set(old$DontusedefaultknowledgeP$000);
              }
            }
          }
          frame.truthValue = truthvalue;
          if (((Boolean)(Logic.$RECORD_JUSTIFICATIONSp$.get())).booleanValue()) {
            { Justification fj = null;
              Cons iter000 = matchingProposition.forwardJustifications().theConsList;

              loop001 : for (;!(iter000 == Stella.NIL); iter000 = iter000.rest) {
                fj = ((Justification)(iter000.value));
                frame.justifications.push(fj);
                break loop001;
              }
            }
            { Justification subsetJustification = Proposition.createSubsetJustification(proposition, matchingProposition);

              if (subsetJustification != null) {
                frame.justifications.push(subsetJustification);
              }
            }
          }
          if (frame.partialMatchFrame != null) {
            if (weight == Stella.NULL_FLOAT) {
              weight = 1.0;
            }
            frame.partialMatchFrame.setFramePartialTruth(truthvalue, truthvalue.positiveScore * weight, Stella.NULL_FLOAT, true);
          }
        }
      }
      return (result);
    }
  }