public static Keyword trySubgoalStrategiesProof(ControlFrame frame) {
    { Description description = ControlFrame.extractSubgoalDescriptionOfFrame(frame);
      boolean reversepolarityP = frame.reversePolarityP;
      Cons strategies = Stella.NIL;

      { boolean chooseValue000 = false;

        if (reversepolarityP) {
          { boolean foundP000 = false;

            { ConsIterator p = LogicObject.applicableRulesOfDescription(description, Logic.KWD_FORWARD, true).allocateIterator();

              loop000 : while (p.nextP()) {
                foundP000 = true;
                break loop000;
              }
            }
            chooseValue000 = foundP000;
          }
        }
        else {
          chooseValue000 = Description.inferableP(description);
        }
        if (chooseValue000) {
          strategies = Cons.cons(Logic.KWD_ANTECEDENTS, strategies);
        }
      }
      if (reversepolarityP &&
          (Description.getInferableComplementDescription(description) != null)) {
        strategies = Cons.cons(Logic.KWD_GOAL_COMPLEMENT, strategies);
      }
      { Proposition proposition = frame.proposition;

        if ((proposition != null) &&
            (Proposition.allArgumentsBoundP(proposition) &&
             (Proposition.findMatchingConceivedProposition(proposition) != null))) {
          strategies = Cons.cons(Logic.KWD_FORWARD_GOALS, strategies);
        }
      }
      { Stella_Object s = null;
        Cons iter000 = strategies.reverse();

        for (;!(iter000 == Stella.NIL); iter000 = iter000.rest) {
          s = iter000.value;
          ControlFrame.pushNextStrategy(frame, ((Keyword)(s)));
        }
      }
      return (Logic.KWD_FAILURE);
    }
  }