GitHub - gapt/SuperInd

Branches Tags

Name		Name	Last commit message	Last commit date
Latest commit History 8 Commits
TODO		TODO
apps.examples		apps.examples
apps.src		apps.src
benchmarks		benchmarks
bob		bob
ladr		ladr
mace4.examples		mace4.examples
mace4.src		mace4.src
manpages		manpages
prover9.examples		prover9.examples
provers.src		provers.src
test.src		test.src
utilities-old		utilities-old
utilities		utilities
.gdb_history		.gdb_history
.gitignore		.gitignore
COPYING		COPYING
Changelog		Changelog
Makefile		Makefile
Outils.rtf		Outils.rtf
README.AMD_64		README.AMD_64
README.first		README.first
README.make		README.make
README.release-reminder		README.release-reminder
VERSION_DATE.h		VERSION_DATE.h
adder4.stab		adder4.stab
arith5.in		arith5.in
arith5.txt		arith5.txt
libtoolize.patch		libtoolize.patch
res.out		res.out
rev.py		rev.py
search.c		search.c
sed.gnu-blurb		sed.gnu-blurb
stab.in		stab.in
stab1.in		stab1.in
stab2.in		stab2.in
x1.doc		x1.doc
x1.rtf		x1.rtf
x10serie.in		x10serie.in
x11somme.in		x11somme.in
x12Fur.in		x12Fur.in
x13Prop1.in		x13Prop1.in
x14RegStabAdd1.in		x14RegStabAdd1.in
x15.in		x15.in
x16AssRC.txt		x16AssRC.txt
x17adder4ripplecarry.in		x17adder4ripplecarry.in
x18Ceres.in		x18Ceres.in
x18Ceres1.in		x18Ceres1.in
x18Ceres1e.in		x18Ceres1e.in
x19Complexity_10.in		x19Complexity_10.in
x19Complexity_2.in		x19Complexity_2.in
x19Complexity_3.in		x19Complexity_3.in
x19Complexity_3e.in		x19Complexity_3e.in
x1Triv.in		x1Triv.in
x1tab.in		x1tab.in
x20production.in		x20production.in
x2socrate.in		x2socrate.in
x4.in		x4.in
x6tab.in		x6tab.in
x7Fur.in		x7Fur.in
x8ACO.in		x8ACO.in
x8ACOe.in		x8ACOe.in
x9paire.in		x9paire.in
xTPTP1.in		xTPTP1.in
xTPTP1Part1.in		xTPTP1Part1.in
xTest.in		xTest.in

Repository files navigation

A few quick tests on an AMD-64 (939, 1MB cache).

Comparing 64- and 32-bit versions of Prover9 and Mace4.

64-bit versions: compiled with gcc defaults on AMD-64.
32-bit versions: compiled with gcc defaults on i386.

Both run on AMD-64.

Nearly all of the data for both Mace4 and Prover9 consists of
pointers, so the jobs on the 64-bit versions take twice the memory.

Prover9: the 64-bit version seems faster.

  ord-rev.out.32:-------- Proof 1 -------- (27.30 + 0.36 seconds)
  ord-rev.out.32:Megabytes=13.05.

  ord-rev.out.64:-------- Proof 1 -------- (22.70 + 0.43 seconds)
  ord-rev.out.64:Megabytes=25.70.

Mace4:   the 32-bit version seems faster.

  m.out.32:-------- Model 1 at 18.13 seconds --------
  m.out.32:Memory report, 1 @ 20 = 20 megs (13.53 megs used).

  m.out.64:-------- Model 1 at 22.96 seconds --------
  m.out.64:Memory report, 2 @ 20 = 40 megs (26.60 megs used).

Your mileage may vary.