public static boolean propositionReferencesTermsP(Proposition self, HashSet terms) {
    { Stella_Object arg = null;
      Vector vector000 = self.arguments;
      int index000 = 0;
      int length000 = vector000.length();

      for (;index000 < length000; index000 = index000 + 1) {
        arg = (vector000.theArray)[index000];
        if (terms.memberP(arg)) {
          return (true);
        }
        { Surrogate testValue000 = Stella_Object.safePrimaryType(arg);

          if (Surrogate.subtypeOfP(testValue000, Logic.SGT_LOGIC_PROPOSITION)) {
            { Proposition arg000 = ((Proposition)(arg));

              if (Proposition.propositionReferencesTermsP(arg000, terms)) {
                return (true);
              }
            }
          }
          else if (Surrogate.subtypeOfP(testValue000, Logic.SGT_LOGIC_SKOLEM)) {
            { Skolem arg000 = ((Skolem)(arg));

              { Proposition definingprop = arg000.definingProposition;

                if ((definingprop != null) &&
                    ((!(definingprop == self)) &&
                     Proposition.propositionReferencesTermsP(definingprop, terms))) {
                  return (true);
                }
              }
            }
          }
          else {
          }
        }
      }
    }
    return (false);
  }