public static List getVariablesFromPropositionList(List props) {
    { List theList = List.newList();
      Symbol variable = null;

      { Proposition prop = null;
        Cons iter000 = props.theConsList;

        for (;!(iter000 == Stella.NIL); iter000 = iter000.rest) {
          prop = ((Proposition)(iter000.value));
          { Keyword testValue000 = prop.kind;

            if ((testValue000 == Logic.KWD_OR) ||
                ((testValue000 == Logic.KWD_NOT) ||
                 (testValue000 == Logic.KWD_AND))) {
              { Symbol var = null;
                Cons iter001 = Logic.getVariablesFromPropositionList(((List)(prop.arguments.listify()))).theConsList;

                for (;!(iter001 == Stella.NIL); iter001 = iter001.rest) {
                  var = ((Symbol)(iter001.value));
                  theList.insertNew(var);
                }
              }
            }
            else {
              { Stella_Object arg = null;
                Vector vector000 = prop.arguments;
                int index000 = 0;
                int length000 = vector000.length();

                for (;index000 < length000; index000 = index000 + 1) {
                  arg = (vector000.theArray)[index000];
                  { Surrogate testValue001 = Stella_Object.safePrimaryType(arg);

                    if (Surrogate.subtypeOfP(testValue001, Logic.SGT_LOGIC_PATTERN_VARIABLE)) {
                      { PatternVariable arg000 = ((PatternVariable)(arg));

                        variable = arg000.skolemName;
                      }
                    }
                    else if (Surrogate.subtypeOfSymbolP(testValue001)) {
                      { Symbol arg000 = ((Symbol)(arg));

                        variable = arg000;
                      }
                    }
                    else if (Surrogate.subtypeOfSurrogateP(testValue001)) {
                      { Surrogate arg000 = ((Surrogate)(arg));

                        variable = Symbol.internSymbol(arg000.symbolName);
                      }
                    }
                    else if (Surrogate.subtypeOfFloatP(testValue001)) {
                      { FloatWrapper arg000 = ((FloatWrapper)(arg));

                        variable = null;
                      }
                    }
                    else if (Surrogate.subtypeOfIntegerP(testValue001)) {
                      { IntegerWrapper arg000 = ((IntegerWrapper)(arg));

                        variable = null;
                      }
                    }
                    else if (Surrogate.subtypeOfStringP(testValue001)) {
                      { StringWrapper arg000 = ((StringWrapper)(arg));

                        variable = null;
                      }
                    }
                    else if (Surrogate.subtypeOfP(testValue001, Logic.SGT_LOGIC_PROPOSITION)) {
                      { Proposition arg000 = ((Proposition)(arg));

                        System.out.println("Dave, you've got a proposition");
                      }
                    }
                    else if (Surrogate.subtypeOfP(testValue001, Logic.SGT_LOGIC_LOGIC_OBJECT)) {
                      { LogicObject arg000 = ((LogicObject)(arg));

                        variable = Logic.objectName(arg000);
                      }
                    }
                    else {
                      { OutputStringStream stream000 = OutputStringStream.newOutputStringStream();

                        stream000.nativeStream.print("`" + testValue001 + "' is not a valid case option");
                        throw ((StellaException)(StellaException.newStellaException(stream000.theStringReader()).fillInStackTrace()));
                      }
                    }
                  }
                  if (variable != null) {
                    theList.insertNew(variable);
                  }
                }
              }
            }
          }
        }
      }
      return (theList);
    }
  }