public static boolean clashesWithFunctionPropositionP(Proposition nextproposition, Proposition referenceproposition) {
    { boolean alwaysP000 = true;

      { Stella_Object superarg = null;
        Iterator iter000 = referenceproposition.arguments.butLast();
        Stella_Object subarg = null;
        Iterator iter001 = nextproposition.arguments.butLast();

        loop000 : while (iter000.nextP() &&
            iter001.nextP()) {
          superarg = iter000.value;
          subarg = iter001.value;
          if (!Stella_Object.eqlP(Logic.argumentBoundTo(superarg), Logic.valueOf(subarg))) {
            alwaysP000 = false;
            break loop000;
          }
        }
      }
      if (alwaysP000) {
        { Stella_Object lastsupervalue = Logic.argumentBoundTo(referenceproposition.arguments.last());
          Stella_Object lastsubvalue = Logic.valueOf(nextproposition.arguments.last());

          if ((lastsupervalue != null) &&
              (lastsubvalue != null)) {
            if (Stella_Object.isaP(lastsubvalue, Logic.SGT_LOGIC_SKOLEM)) {
              if (Stella_Object.isaP(lastsupervalue, Logic.SGT_LOGIC_SKOLEM)) {
                return (false);
              }
              else {
                return (Skolem.valueClashesWithSkolemP(((Skolem)(lastsubvalue)), lastsupervalue));
              }
            }
            else {
              if (Stella_Object.isaP(lastsupervalue, Logic.SGT_LOGIC_SKOLEM)) {
                return (Skolem.valueClashesWithSkolemP(((Skolem)(lastsupervalue)), lastsubvalue));
              }
              else {
                return (!Stella_Object.eqlP(lastsupervalue, lastsubvalue));
              }
            }
          }
        }
      }
    }
    return (false);
  }