public static void signalUnificationClash(Proposition prop, Stella_Object term1, Stella_Object term2) {
    { String message = "Unification clash.";
      UnificationClash clashObject = null;

      if (prop != null) {
        Proposition.assignTruthValue(prop, Logic.INCONSISTENT_TRUTH_VALUE);
      }
      else {
        Stella.STANDARD_WARNING.nativeStream.println("Warning: Internal: SIGNAL-UNIFICATION-CLASH doesn't have responsible proposition available.");
      }
      if (((Boolean)(Logic.$RECORD_JUSTIFICATIONSp$.get())).booleanValue()) {
        Stella.STANDARD_WARNING.nativeStream.println("Warning: SIGNAL-UNIFICATION-CLASH doesn't yet have justification support");
      }
      if ((term1 != null) &&
          (term2 != null)) {
        { String message000 = null;

          { Object old$PrintreadablyP$000 = Stella.$PRINTREADABLYp$.get();

            try {
              Native.setBooleanSpecial(Stella.$PRINTREADABLYp$, true);
              message000 = "`" + Native.stringify(term1) + "'" + " clashes with " + "`" + Native.stringify(term2) + "'";

            } finally {
              Stella.$PRINTREADABLYp$.set(old$PrintreadablyP$000);
            }
          }
          message = message000;
        }
      }
      clashObject = UnificationClash.newUnificationClash(message);
      clashObject.proposition = prop;
      clashObject.context = ((Context)(Stella.$CONTEXT$.get()));
      clashObject.value1 = term1;
      clashObject.value2 = term2;
      throw ((UnificationClash)(clashObject.fillInStackTrace()));
    }
  }