Loading optimisation7.pri ...
Preprocessing ...
Proving ...

Cancelled or timeout

Loading predicates3.pri ...
Preprocessing ...
Proving ...

Cancelled or timeout

Loading simpleEq7.pri ...
Preprocessing ...
Constructing countermodel ...

Formula is invalid, found a countermodel:
c = -3

Loading simpleEq8.pri ...
Preprocessing ...
Constructing satisfying assignment for the existential constants ...

No satisfying assignment for the existential constants exists, formula is invalid

Loading simpleEq10.pri ...
Preprocessing ...
Proving ...

No proof found

Loading splitEqBug.pri ...
Preprocessing ...
Constructing countermodel ...

Formula is invalid, found a countermodel:
previous(1, 0) & previous(0, 1) & next(0, 1) & !next(1, 0)

Loading splitEqBug2.pri ...
Preprocessing ...
Constructing countermodel ...

Formula is invalid, found a countermodel:
store(0, 0, 13, 1) & select(1, 0, 13) & select(1, 0, -1)

Loading wrongEqualities0.pri ...
Preprocessing ...
Constructing countermodel ...

Formula is invalid, found a countermodel:
true

Loading wrongEqualities1.pri ...
Preprocessing ...
Constructing countermodel ...

Formula is invalid, found a countermodel:
true

Loading wrongInequalities0.pri ...
Preprocessing ...
Constructing countermodel ...

Formula is invalid, found a countermodel:
b = -2 & a = 2

Loading wrongInequalities1.pri ...
Preprocessing ...
Constructing countermodel ...

Formula is invalid, found a countermodel:
a = 2

Loading wrongInequalities2.pri ...
Preprocessing ...
Constructing countermodel ...

Formula is invalid, found a countermodel:
true

Loading wrongInequalities3.pri ...
Preprocessing ...
Constructing countermodel ...

Formula is invalid, found a countermodel:
c = 1

Loading wrongInequalities4.pri ...
Preprocessing ...
Constructing countermodel ...

Formula is invalid, found a countermodel:
true

Loading wrongInequalities5.pri ...
Preprocessing ...
Constructing countermodel ...

Formula is invalid, found a countermodel:
!p(0)

Loading wrongInequalities6.pri ...
Preprocessing ...
Constructing countermodel ...

Formula is invalid, found a countermodel:
x = 0 & y = 0

Loading wrongNameResolution.pri ...
Preprocessing ...
Constructing countermodel ...

Formula is invalid, found a countermodel:
true

Loading reduceWithConjunctionBug.pri ...
Preprocessing ...
Proving ...

Cancelled or timeout

Loading wrongFunctionAxioms.pri ...
Preprocessing ...
Proving ...

Cancelled or timeout

Loading relationalFun2.pri ...
Preprocessing ...
Proving ...

Cancelled or timeout

Loading omegaBug.pri ...
Preprocessing ...
Constructing countermodel ...

No countermodel exists, formula is valid

Loading uniExConstants1.pri ...
Preprocessing ...
Proving ...

No proof found

Loading uniExConstantsBug.pri ...
Preprocessing ...
Proving ...

No proof found

Loading wrongModel.pri ...
Preprocessing ...
Constructing countermodel ...

Formula is invalid, found a countermodel:
!p(0)

Loading cryptarithm.pri ...
Preprocessing ...
Constructing countermodel ...

Formula is invalid, found a countermodel:

Loading cryptarithm4.pri ...
Preprocessing ...
Constructing countermodel ...

Formula is invalid, found a countermodel:

Loading ricart-agrawala7.smt2 ...
Checking satisfiability ...
Warning: ignoring (set-logic AUFLIA)
Warning: ignoring (set-info :source | An Optimal Algorithm for Mutual Exclusion in Computer Networks. Glenn Ricart and Ashok K. Agrawala. Communications of the ACM Vol.: 24 Number: 1. This is a benchmark of the haRVey theorem prover. It was translated to SMT-LIB by Leonardo  de Moura |)
Warning: ignoring (set-info :smt-lib-version 2.0)
Warning: ignoring (set-info :category "industrial")
Warning: ignoring (set-info :status unsat)
Preprocessing ...
Proving ...

unknown
Cancelled or timeout

