public static Proposition extractInvertedGoal(Proposition proposition, Proposition goal) {
    if (goal.kind == Logic.KWD_NOT) {
      return (Proposition.extractInvertedGoal(proposition, ((Proposition)((goal.arguments.theArray)[0]))));
    }
    { Keyword testValue000 = proposition.kind;

      if (testValue000 == Logic.KWD_NOT) {
        if (Proposition.equivalentPropositionsP(((Proposition)((proposition.arguments.theArray)[0])), goal, null)) {
          return (proposition);
        }
        else {
          return (Proposition.extractInvertedGoal(((Proposition)((proposition.arguments.theArray)[0])), goal));
        }
      }
      else if ((testValue000 == Logic.KWD_AND) ||
          (testValue000 == Logic.KWD_OR)) {
        { Proposition result = null;

          { Stella_Object arg = null;
            Vector vector000 = proposition.arguments;
            int index000 = 0;
            int length000 = vector000.length();

            for (;index000 < length000; index000 = index000 + 1) {
              arg = (vector000.theArray)[index000];
              result = Proposition.extractInvertedGoal(((Proposition)(arg)), goal);
              if (result != null) {
                return (result);
              }
            }
          }
        }
      }
      else {
        if (Proposition.equivalentPropositionsP(proposition, goal, null)) {
          return (proposition);
        }
      }
    }
    return (null);
  }