[SMT-LIB] UF unsat benchmarks without equality

[Tinelli, Cesare]

Jean-Claude,

On 12 Mar 2015, at 03:28, Jean-Claude Royer <Jean-Claude.Royer at mines-nantes.fr> wrote:

> 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 ?
> 
I do not think there are many of those in the SMT-LIB library. You may want to check the TPT library instead (which however uses a different format): http://www.cs.miami.edu/~tptp/

You could ask Geoff Sutcliffe, TPTP's main maintainer, for directions on how to extract problems with the characteristics you seek.

Cheers,


Cesare
 


> regards
> 
> 
> Jean-Claude.Royer at mines-nantes.fr
> ASCOLA, Mines de Nantes - INRIA
> + 33 2 51 85 82 05
> 
> 
> 
> 
> 
> 
> _______________________________________________
> SMT-LIB mailing list
> SMT-LIB at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/smt-lib