public static Keyword tryDisjunctiveImplicationProof(ControlFrame frame) {
    { ParallelThread parallelthread = ((QueryIterator)(Logic.$QUERYITERATOR$.get())).currentParallelThread;
      ParallelControlFrame parallelframe = ((ParallelControlFrame)(parallelthread.topControlFrame.up));

      { Proposition disjunctiveprop = frame.proposition;
        Vector disjuncts = disjunctiveprop.arguments;
        Proposition subgoaldisjunct = ((Proposition)((disjuncts.theArray)[0]));

        if (parallelframe.unboundVariablesP) {
          {
            subgoaldisjunct = null;
            { Proposition d = null;
              Vector vector000 = disjuncts;
              int index000 = 0;
              int length000 = vector000.length();

              for (;index000 < length000; index000 = index000 + 1) {
                d = ((Proposition)((vector000.theArray)[index000]));
                if (!Proposition.allArgumentsBoundP(d)) {
                  if (subgoaldisjunct != null) {
                    return (Logic.KWD_FAILURE);
                  }
                  subgoaldisjunct = d;
                }
              }
            }
          }
        }
        else {
          { Proposition d = null;
            Vector vector001 = disjuncts;
            int index001 = 0;
            int length001 = vector001.length();

            loop001 : for (;index001 < length001; index001 = index001 + 1) {
              d = ((Proposition)((vector001.theArray)[index001]));
              if (!(d.kind == Logic.KWD_NOT)) {
                subgoaldisjunct = d;
                break loop001;
              }
            }
          }
        }
        ParallelControlFrame.enterHypotheticalWorld(parallelframe);
        try {
          { boolean negatedtruthvalueP = frame.reversePolarityP;
            Proposition assumption = null;

            { Proposition disj = null;
              Vector vector002 = disjuncts;
              int index002 = 0;
              int length002 = vector002.length();

              for (;index002 < length002; index002 = index002 + 1) {
                disj = ((Proposition)((vector002.theArray)[index002]));
                if (!(disj == subgoaldisjunct)) {
                  assumption = Proposition.recursivelyFastenDownPropositions((negatedtruthvalueP ? Logic.conjoinPropositions(Proposition.inheritAsTopLevelProposition(disj, KeyValueMap.newKeyValueMap())) : Proposition.inheritProposition(disj, KeyValueMap.newKeyValueMap())), false);
                  if ((Stella.$TRACED_KEYWORDS$ != null) &&
                      Stella.$TRACED_KEYWORDS$.membP(Logic.KWD_GOAL_TREE)) {
                    {
                      System.out.println();
                      System.out.println("  Assume that " + assumption + " is " + ((negatedtruthvalueP ? "true" : "false")) + ".");
                      System.out.println();
                    }
;
                  }
                  Proposition.assignTruthValue(assumption, (negatedtruthvalueP ? Stella.TRUE_WRAPPER : Stella.FALSE_WRAPPER));
                }
              }
            }
          }
        } catch (Clash e000) {
          return (Logic.KWD_FINAL_SUCCESS);
        }
        { Proposition d = null;
          Vector vector003 = disjuncts;
          int index003 = 0;
          int length003 = vector003.length();
          int i = Stella.NULL_INTEGER;
          int iter000 = 0;

          loop003 : for (;index003 < length003; index003 = index003 + 1, iter000 = iter000 + 1) {
            d = ((Proposition)((vector003.theArray)[index003]));
            i = iter000;
            if (d == subgoaldisjunct) {
              frame.argumentCursor = i;
              break loop003;
            }
          }
        }
        return (Logic.KWD_MOVE_DOWN);
      }
    }
  }