Dear all, I am looking for unsatisfiable examples of first-order logic with uninterpreted functions but without equality predicates. There are benchmarks in UF but with equality. Is there something elsewhere ? regards Jean-Claude.Royer at mines-nantes.fr ASCOLA, Mines de Nantes - INRIA + 33 2 51 85 82 05