public static Keyword initiateAtomicGoalProofs(ControlFrame frame) {
    { Object old$ReversepolarityP$000 = Logic.$REVERSEPOLARITYp$.get();

      try {
        Native.setBooleanSpecial(Logic.$REVERSEPOLARITYp$, frame.reversePolarityP);
        { Proposition proposition = frame.proposition;
          Keyword inferencelevel = Logic.currentInferenceLevel().keyword;
          Cons strategies = null;

          { Keyword testValue000 = proposition.kind;

            if ((testValue000 == Logic.KWD_PREDICATE) ||
                ((testValue000 == Logic.KWD_ISA) ||
                 (testValue000 == Logic.KWD_FUNCTION))) {
              frame.goalBindings = Proposition.yieldGoalBindings(proposition);
              if (ControlFrame.checkForDuplicateGoalP(frame)) {
                if (Logic.$DUPLICATE_SUBGOAL_STRATEGY$ == Logic.KWD_DUPLICATE_GOALS) {
                  inferencelevel = Logic.KWD_SHALLOW;
                }
                else if (Logic.$DUPLICATE_SUBGOAL_STRATEGY$ == Logic.KWD_DUPLICATE_GOALS_WITH_CACHING) {
                  frame.state = Logic.KWD_SCAN_CACHED_BINDINGS;
                  ControlFrame.createChoicePoint(frame);
                  return (Logic.KWD_MOVE_IN_PLACE);
                }
                else {
                  { OutputStringStream stream000 = OutputStringStream.newOutputStringStream();

                    stream000.nativeStream.print("`" + Logic.$DUPLICATE_SUBGOAL_STRATEGY$ + "' is not a valid case option");
                    throw ((StellaException)(StellaException.newStellaException(stream000.theStringReader()).fillInStackTrace()));
                  }
                }
              }
              if ((inferencelevel == Logic.KWD_NORMAL) ||
                  (inferencelevel == Logic.KWD_BACKTRACKING)) {
                strategies = Stella.getQuotedTree("((:SPECIALIST :LOOKUP-GOAL-CACHES :LOOKUP-ASSERTIONS :SHALLOW-DISPROOF :ALL-SUBGOAL-STRATEGIES) \"/LOGIC\")", "/LOGIC");
              }
              else if (inferencelevel == Logic.KWD_REFUTATION) {
                strategies = Stella.getQuotedTree("((:SPECIALIST :LOOKUP-GOAL-CACHES :LOOKUP-ASSERTIONS :SHALLOW-DISPROOF :ALL-SUBGOAL-STRATEGIES :REFUTATION) \"/LOGIC\")", "/LOGIC");
              }
              else {
                strategies = Stella.getQuotedTree("((:SPECIALIST :LOOKUP-GOAL-CACHES :LOOKUP-ASSERTIONS :SHALLOW-DISPROOF) \"/LOGIC\")", "/LOGIC");
              }
              if ((proposition.kind == Logic.KWD_FUNCTION) &&
                  (!((Boolean)(Logic.$REVERSEPOLARITYp$.get())).booleanValue())) {
                strategies = Cons.copyConsList(strategies).concatenate(Cons.consList(Cons.cons(Logic.KWD_MANUFACTURE_SKOLEM, Stella.NIL)), Stella.NIL);
              }
            }
            else if (testValue000 == Logic.KWD_EQUIVALENT) {
              strategies = Stella.getQuotedTree("((:EQUIVALENCE) \"/LOGIC\")", "/LOGIC");
            }
            else if (testValue000 == Logic.KWD_IMPLIES) {
              strategies = Stella.getQuotedTree("((:SPECIALIST :ALL-SUBGOAL-STRATEGIES :IMPLIES) \"/LOGIC\")", "/LOGIC");
            }
            else {
              { OutputStringStream stream001 = OutputStringStream.newOutputStringStream();

                stream001.nativeStream.print("`" + testValue000 + "' is not a valid case option");
                throw ((StellaException)(StellaException.newStellaException(stream001.theStringReader()).fillInStackTrace()));
              }
            }
          }
          frame.nextStrategies = strategies;
          frame.state = Logic.KWD_ATOMIC_GOAL;
          ControlFrame.createChoicePoint(frame);
          return (Logic.KWD_MOVE_IN_PLACE);
        }

      } finally {
        Logic.$REVERSEPOLARITYp$.set(old$ReversepolarityP$000);
      }
    }
  }