SVN (r6068+) or 0.9.2 version of Nemerle is required.

It doesn't even compile at the moment, go a few revisions back if you
want to compile it.

Initial timing (on 1.8Ghz amd64/linux box) -> benchmark categories.

0-3        01
3-20       02
20-120     03
120-600    04
600-1800   05
1800-7200  06

timeout    09

timings as of rev134
0-1       01  sum=5
1-5       02  sum=38
4-15      03  sum=107
10-60     04  sum=406
60-140    05  sum=about 1200
140-400   06  sum=about 3600
400-1500  07  sum=about 3800



SMT-AUFLIA division status:

problems:
AUFLIA/misc/set1.smt     UNSAT, very large MQI (1790), MIR = 12, 53s
AUFLIA/misc/set2.smt     SAT/TIMEOUT
AUFLIA/Burns/burns4.smt  UNSAT/ problems with p!=q -> (p<q || q<p)

AUFLIA/piVC/piVC_982830.smt  UNSAT/ only quantified formulas to prove

Within 3 minutes:
AUFLIA/piVC/piVC_5581bd.smt
AUFLIA/piVC/piVC_a04477.smt
AUFLIA/piVC/piVC_dab5a0.smt