printf ' ' | fink --no-use-binary-dist --yes --build-as-nobody rebuild prover9 2>&1 The package 'prover9' will be built without being installed. Reading build dependency for prover9-2009-11a-5... Reading dependency for prover9-2009-11a-5... Reading build conflict for prover9-2009-11a-5... The following package will be rebuilt: prover9 curl --connect-timeout 30 -f -L -A 'fink/0.37.0' -O http://distfiles.master.finkmirrors.net/distfiles/LADR-2009-11A.tar.gz % Total % Received % Xferd Average Speed Time Time Time Current Dload Upload Total Spent Left Speed 0 0 0 0 0 0 0 0 --:--:-- --:--:-- --:--:-- 0 0 1753k 0 1203 0 0 4858 0 0:06:09 --:--:-- 0:06:09 4850 22 1753k 22 391k 0 0 289k 0 0:00:06 0:00:01 0:00:05 289k 41 1753k 41 733k 0 0 313k 0 0:00:05 0:00:02 0:00:03 313k 78 1753k 78 1372k 0 0 431k 0 0:00:04 0:00:03 0:00:01 431k 100 1753k 100 1753k 0 0 492k 0 0:00:03 0:00:03 --:--:-- 492k curl --connect-timeout 30 -f -L -A 'fink/0.37.0' -O http://distfiles.master.finkmirrors.net/distfiles/prover9-manual-2009-11A.tar.gz % Total % Received % Xferd Average Speed Time Time Time Current Dload Upload Total Spent Left Speed 0 0 0 0 0 0 0 0 --:--:-- --:--:-- --:--:-- 0 13 1031k 13 134k 0 0 238k 0 0:00:04 --:--:-- 0:00:04 238k 20 1031k 20 209k 0 0 111k 0 0:00:09 0:00:01 0:00:08 111k 86 1031k 86 896k 0 0 349k 0 0:00:02 0:00:02 --:--:-- 349k 100 1031k 100 1031k 0 0 375k 0 0:00:02 0:00:02 --:--:-- 375k Setting runtime build-lock... dpkg-deb -b /sw/build.build/root-fink-buildlock-prover9-2009-11a-5 /sw/build.build dpkg-deb: building package `fink-buildlock-prover9-2009-11a-5' in `/sw/build.build/fink-buildlock-prover9-2009-11a-5_2014.08.04-22.06.03_darwin-x86_64.deb'. Installing build-lock package... /sw/bin/dpkg-lockwait -i /sw/build.build/fink-buildlock-prover9-2009-11a-5_2014.08.04-22.06.03_darwin-x86_64.deb Selecting previously deselected package fink-buildlock-prover9-2009-11a-5. (Reading database ... 4769 files and directories currently installed.) Unpacking fink-buildlock-prover9-2009-11a-5 (from .../fink-buildlock-prover9-2009-11a-5_2014.08.04-22.06.03_darwin-x86_64.deb) ... Setting up fink-buildlock-prover9-2009-11a-5 (2014.08.04-22.06.03) ... sudo -u fink-bld [ENV] sh -c /tmp/fink.sNrdI env LANG=C LC_ALL=C /sw/bin/tar --no-same-owner --no-same-permissions -xvf /sw/src/LADR-2009-11A.tar.gz LADR-2009-11A/ LADR-2009-11A/Makefile LADR-2009-11A/manpages/ LADR-2009-11A/manpages/prover9.1 LADR-2009-11A/manpages/mace4.1 LADR-2009-11A/README.make LADR-2009-11A/mace4.src/ LADR-2009-11A/mace4.src/ordercells.c LADR-2009-11A/mace4.src/help2 LADR-2009-11A/mace4.src/Makefile LADR-2009-11A/mace4.src/pub LADR-2009-11A/mace4.src/r1.in LADR-2009-11A/mace4.src/h1.in LADR-2009-11A/mace4.src/util.c LADR-2009-11A/mace4.src/estack.c LADR-2009-11A/mace4.src/msearch.c LADR-2009-11A/mace4.src/syms.h LADR-2009-11A/mace4.src/arithmetic.h LADR-2009-11A/mace4.src/temp LADR-2009-11A/mace4.src/propagate.c LADR-2009-11A/mace4.src/README.memory LADR-2009-11A/mace4.src/arithmetic.c LADR-2009-11A/mace4.src/mstate.h LADR-2009-11A/mace4.src/TAGS LADR-2009-11A/mace4.src/ground.h LADR-2009-11A/mace4.src/mace4.c LADR-2009-11A/mace4.src/negpropindex.c LADR-2009-11A/mace4.src/estack.h LADR-2009-11A/mace4.src/print.c LADR-2009-11A/mace4.src/help LADR-2009-11A/mace4.src/t1.in LADR-2009-11A/mace4.src/negprop.c LADR-2009-11A/mace4.src/h1.out LADR-2009-11A/mace4.src/propagate.h LADR-2009-11A/mace4.src/puzzles/ LADR-2009-11A/mace4.src/puzzles/f1.in~ LADR-2009-11A/mace4.src/puzzles/zebra2.out LADR-2009-11A/mace4.src/puzzles/temp LADR-2009-11A/mace4.src/puzzles/f1.in LADR-2009-11A/mace4.src/puzzles/zebra1.out LADR-2009-11A/mace4.src/puzzles/queens1.out LADR-2009-11A/mace4.src/puzzles/kenken6.in LADR-2009-11A/mace4.src/puzzles/zebra2.in LADR-2009-11A/mace4.src/puzzles/kenken6.out LADR-2009-11A/mace4.src/puzzles/queens2.in LADR-2009-11A/mace4.src/puzzles/send-money.out LADR-2009-11A/mace4.src/puzzles/queens2.out LADR-2009-11A/mace4.src/puzzles/queens1.in LADR-2009-11A/mace4.src/puzzles/send-money.in LADR-2009-11A/mace4.src/puzzles/f1.out LADR-2009-11A/mace4.src/puzzles/sudoku.out LADR-2009-11A/mace4.src/puzzles/sudoku.in LADR-2009-11A/mace4.src/puzzles/zebra1.in LADR-2009-11A/mace4.src/mstate.c LADR-2009-11A/mace4.src/msearch.c~ LADR-2009-11A/mace4.src/Changelog.old LADR-2009-11A/mace4.src/save/ LADR-2009-11A/mace4.src/save/raw-cooked~ LADR-2009-11A/mace4.src/save/raw-cooked LADR-2009-11A/mace4.src/syms.c LADR-2009-11A/mace4.src/util LADR-2009-11A/mace4.src/select.c LADR-2009-11A/mace4.src/commandline.c LADR-2009-11A/mace4.src/msearch.h LADR-2009-11A/mace4.src/ground.c LADR-2009-11A/mace4.src/index.html LADR-2009-11A/sed.gnu-blurb LADR-2009-11A/utilities-old/ LADR-2009-11A/utilities-old/proofs_to_hints LADR-2009-11A/utilities-old/oproofs_to_goals LADR-2009-11A/utilities-old/iterate LADR-2009-11A/utilities-old/oproofs_to_hints LADR-2009-11A/utilities-old/looper.pl LADR-2009-11A/utilities-old/attack2 LADR-2009-11A/utilities-old/proofs_to_goals LADR-2009-11A/ladr/ LADR-2009-11A/ladr/term.c LADR-2009-11A/ladr/discrim.c LADR-2009-11A/ladr/listterm.h LADR-2009-11A/ladr/ac_redun.h LADR-2009-11A/ladr/symbols.c LADR-2009-11A/ladr/string.c LADR-2009-11A/ladr/clist.c LADR-2009-11A/ladr/std_options.c LADR-2009-11A/ladr/dioph.h LADR-2009-11A/ladr/top_input.h LADR-2009-11A/ladr/clauses.h.bak LADR-2009-11A/ladr/btm.c LADR-2009-11A/ladr/literals.h LADR-2009-11A/ladr/basic.h LADR-2009-11A/ladr/tlist.c LADR-2009-11A/ladr/xproofs.h LADR-2009-11A/ladr/multiset.c LADR-2009-11A/ladr/discrimw.h LADR-2009-11A/ladr/btm.h LADR-2009-11A/ladr/Makefile LADR-2009-11A/ladr/order.c LADR-2009-11A/ladr/pub LADR-2009-11A/ladr/resolve.h LADR-2009-11A/ladr/formula.h LADR-2009-11A/ladr/dollar.c LADR-2009-11A/ladr/ioutil.c LADR-2009-11A/ladr/int_code.c~ LADR-2009-11A/ladr/html.tar.gz LADR-2009-11A/ladr/demod.h LADR-2009-11A/ladr/README.ac-redundancy LADR-2009-11A/ladr/formula.c LADR-2009-11A/ladr/a.out LADR-2009-11A/ladr/lindex.c LADR-2009-11A/ladr/dollar.c.save LADR-2009-11A/ladr/dollar.h LADR-2009-11A/ladr/discrim.h LADR-2009-11A/ladr/weight.h LADR-2009-11A/ladr/cycle LADR-2009-11A/ladr/discrimb.c LADR-2009-11A/ladr/ivy.h LADR-2009-11A/ladr/fpalist.c LADR-2009-11A/ladr/symbols.h LADR-2009-11A/ladr/demod.c LADR-2009-11A/ladr/attrib.h LADR-2009-11A/ladr/maximal.c LADR-2009-11A/ladr/paramod.c LADR-2009-11A/ladr/parautil.h LADR-2009-11A/ladr/pindex.h LADR-2009-11A/ladr/parautil.c LADR-2009-11A/ladr/temp LADR-2009-11A/ladr/features.c LADR-2009-11A/ladr/top_input.c LADR-2009-11A/ladr/temp25 LADR-2009-11A/ladr/fpa.h LADR-2009-11A/ladr/strbuf.c LADR-2009-11A/ladr/resolve.c LADR-2009-11A/ladr/features.h LADR-2009-11A/ladr/topform.h LADR-2009-11A/ladr/clausify.h LADR-2009-11A/ladr/termorder.c LADR-2009-11A/ladr/parse.c LADR-2009-11A/ladr/clausify.c LADR-2009-11A/ladr/term.h LADR-2009-11A/ladr/tptp_trans.h LADR-2009-11A/ladr/xproofs.c LADR-2009-11A/ladr/nonport.c LADR-2009-11A/ladr/fatal.h LADR-2009-11A/ladr/clauses.c~ LADR-2009-11A/ladr/work LADR-2009-11A/ladr/TAGS LADR-2009-11A/ladr/ivy.c LADR-2009-11A/ladr/sed.symbols LADR-2009-11A/ladr/paramod.h LADR-2009-11A/ladr/lindex.h LADR-2009-11A/ladr/just.c LADR-2009-11A/ladr/subsume.c LADR-2009-11A/ladr/options.c LADR-2009-11A/ladr/options.h LADR-2009-11A/ladr/accanon.c LADR-2009-11A/ladr/clause_eval.c LADR-2009-11A/ladr/weight.c LADR-2009-11A/ladr/complex.c LADR-2009-11A/ladr/index.h LADR-2009-11A/ladr/fpa.c LADR-2009-11A/ladr/clist.h LADR-2009-11A/ladr/discrimw.c LADR-2009-11A/ladr/mindex.h LADR-2009-11A/ladr/complex.h LADR-2009-11A/ladr/memory.c LADR-2009-11A/ladr/clauseid.h LADR-2009-11A/ladr/backdemod.h LADR-2009-11A/ladr/banner.c LADR-2009-11A/ladr/random.h LADR-2009-11A/ladr/subsume.h LADR-2009-11A/ladr/kol.pl LADR-2009-11A/ladr/fastparse.c LADR-2009-11A/ladr/clash.h LADR-2009-11A/ladr/flatterm.h LADR-2009-11A/ladr/clause_misc.h LADR-2009-11A/ladr/cnf.c LADR-2009-11A/ladr/cnf.h LADR-2009-11A/ladr/int_code.h LADR-2009-11A/ladr/interp.h LADR-2009-11A/ladr/backdemod.c LADR-2009-11A/ladr/hints.c LADR-2009-11A/ladr/order.h LADR-2009-11A/ladr/ladr.h LADR-2009-11A/ladr/glist.c LADR-2009-11A/ladr/clauses.c LADR-2009-11A/ladr/sed2 LADR-2009-11A/ladr/di_tree.h LADR-2009-11A/ladr/t1.in LADR-2009-11A/ladr/accanon.h LADR-2009-11A/ladr/weight2.c LADR-2009-11A/ladr/definitions.h LADR-2009-11A/ladr/topform.c LADR-2009-11A/ladr/clauseid.c LADR-2009-11A/ladr/compile LADR-2009-11A/ladr/flatterm.c LADR-2009-11A/ladr/clause_misc.c LADR-2009-11A/ladr/just.h LADR-2009-11A/ladr/sed3 LADR-2009-11A/ladr/header.h LADR-2009-11A/ladr/flatdemod.c LADR-2009-11A/ladr/strbuf.h LADR-2009-11A/ladr/nonport.h LADR-2009-11A/ladr/error LADR-2009-11A/ladr/interp.c LADR-2009-11A/ladr/basic.c LADR-2009-11A/ladr/sed1 LADR-2009-11A/ladr/banner.h LADR-2009-11A/ladr/weight2.h LADR-2009-11A/ladr/termorder.h LADR-2009-11A/ladr/discrimb.h LADR-2009-11A/ladr/README.char-types LADR-2009-11A/ladr/Changelog.old LADR-2009-11A/ladr/dots LADR-2009-11A/ladr/hash.h LADR-2009-11A/ladr/clock.c LADR-2009-11A/ladr/Makefile~ LADR-2009-11A/ladr/tptp_trans.c.work LADR-2009-11A/ladr/termflag.h LADR-2009-11A/ladr/random.c LADR-2009-11A/ladr/save/ LADR-2009-11A/ladr/save/term.c LADR-2009-11A/ladr/save/discrim.c LADR-2009-11A/ladr/save/clist.c LADR-2009-11A/ladr/save/weight1.c LADR-2009-11A/ladr/save/btm.c LADR-2009-11A/ladr/save/detach.c LADR-2009-11A/ladr/save/formula.c LADR-2009-11A/ladr/save/cnf.c.alarm LADR-2009-11A/ladr/save/lindex.c LADR-2009-11A/ladr/save/sos.c.old LADR-2009-11A/ladr/save/commands.c LADR-2009-11A/ladr/save/fpalist.c LADR-2009-11A/ladr/save/features.c LADR-2009-11A/ladr/save/strbuf.c LADR-2009-11A/ladr/save/printing LADR-2009-11A/ladr/save/parse.c LADR-2009-11A/ladr/save/detach.o LADR-2009-11A/ladr/save/str_toupper LADR-2009-11A/ladr/save/detach.h LADR-2009-11A/ladr/save/just.c LADR-2009-11A/ladr/save/options.c LADR-2009-11A/ladr/save/fpa.c LADR-2009-11A/ladr/save/sos.h LADR-2009-11A/ladr/save/commands2.c LADR-2009-11A/ladr/save/glist.c LADR-2009-11A/ladr/save/weight1.h LADR-2009-11A/ladr/save/detach.h.bak LADR-2009-11A/ladr/save/sos.h~ LADR-2009-11A/ladr/save/interp.c LADR-2009-11A/ladr/save/sos.c LADR-2009-11A/ladr/save/clause.c LADR-2009-11A/ladr/save/lex_compare LADR-2009-11A/ladr/save/mindex.c LADR-2009-11A/ladr/save/attrib.c LADR-2009-11A/ladr/save/fsyms_clist LADR-2009-11A/ladr/save/commands.h LADR-2009-11A/ladr/save/btu.c LADR-2009-11A/ladr/save/goals_to_denials LADR-2009-11A/ladr/save/unify.c LADR-2009-11A/ladr/save/hash.c LADR-2009-11A/ladr/save/clash.c LADR-2009-11A/ladr/save/pindex.c LADR-2009-11A/ladr/save/call_weight.c LADR-2009-11A/ladr/save/interp_remove_skolems LADR-2009-11A/ladr/save/read_tptp_file.c LADR-2009-11A/ladr/clause_eval.h LADR-2009-11A/ladr/di_tree.c LADR-2009-11A/ladr/kol.py LADR-2009-11A/ladr/ibuffer.c LADR-2009-11A/ladr/index.html.master LADR-2009-11A/ladr/fatal.c LADR-2009-11A/ladr/sed.1 LADR-2009-11A/ladr/std_options.h LADR-2009-11A/ladr/mindex.c LADR-2009-11A/ladr/hints.h LADR-2009-11A/ladr/html/ LADR-2009-11A/ladr/html/flatdemod.html LADR-2009-11A/ladr/html/listterm.html LADR-2009-11A/ladr/html/clash.html LADR-2009-11A/ladr/html/topform.html LADR-2009-11A/ladr/html/discrim.html LADR-2009-11A/ladr/html/hints.html LADR-2009-11A/ladr/html/top_input.html LADR-2009-11A/ladr/html/term.html LADR-2009-11A/ladr/html/hash.html LADR-2009-11A/ladr/html/fpalist.html LADR-2009-11A/ladr/html/nonport.html LADR-2009-11A/ladr/html/string.html LADR-2009-11A/ladr/html/random.html LADR-2009-11A/ladr/html/subsume.html LADR-2009-11A/ladr/html/memory.html LADR-2009-11A/ladr/html/tptp_trans.html LADR-2009-11A/ladr/html/fastparse.html LADR-2009-11A/ladr/html/paramod.html LADR-2009-11A/ladr/html/weight.html LADR-2009-11A/ladr/html/fpa.html LADR-2009-11A/ladr/html/avltree.html LADR-2009-11A/ladr/html/compress.html LADR-2009-11A/ladr/html/just.html LADR-2009-11A/ladr/html/demod.html LADR-2009-11A/ladr/html/accanon.html LADR-2009-11A/ladr/html/mindex.html LADR-2009-11A/ladr/html/fatal.html LADR-2009-11A/ladr/html/definitions.html LADR-2009-11A/ladr/html/ibuffer.html LADR-2009-11A/ladr/html/tlist.html LADR-2009-11A/ladr/html/termorder.html LADR-2009-11A/ladr/html/formula.html LADR-2009-11A/ladr/html/discrimw.html LADR-2009-11A/ladr/html/clauses.html LADR-2009-11A/ladr/html/features.html LADR-2009-11A/ladr/html/basic.html LADR-2009-11A/ladr/html/clause_misc.html LADR-2009-11A/ladr/html/termflag.html LADR-2009-11A/ladr/html/unify.html LADR-2009-11A/ladr/html/options.html LADR-2009-11A/ladr/html/xproofs.html LADR-2009-11A/ladr/html/std_options.html LADR-2009-11A/ladr/html/banner.html LADR-2009-11A/ladr/html/resolve.html LADR-2009-11A/ladr/html/btu.html LADR-2009-11A/ladr/html/clause_eval.html LADR-2009-11A/ladr/html/interp.html LADR-2009-11A/ladr/html/btm.html LADR-2009-11A/ladr/html/maximal.html LADR-2009-11A/ladr/html/lindex.html LADR-2009-11A/ladr/html/int_code.html LADR-2009-11A/ladr/html/ivy.html LADR-2009-11A/ladr/html/ac_redun.html LADR-2009-11A/ladr/html/ioutil.html LADR-2009-11A/ladr/html/order.html LADR-2009-11A/ladr/html/parautil.html LADR-2009-11A/ladr/html/clock.html LADR-2009-11A/ladr/html/di_tree.html LADR-2009-11A/ladr/html/backdemod.html LADR-2009-11A/ladr/html/dioph.html LADR-2009-11A/ladr/html/clausify.html LADR-2009-11A/ladr/html/strbuf.html LADR-2009-11A/ladr/html/parse.html LADR-2009-11A/ladr/html/flatterm.html LADR-2009-11A/ladr/html/multiset.html LADR-2009-11A/ladr/html/discrimb.html LADR-2009-11A/ladr/html/sos.html LADR-2009-11A/ladr/html/symbols.html LADR-2009-11A/ladr/html/attrib.html LADR-2009-11A/ladr/html/cnf.html LADR-2009-11A/ladr/html/clauseid.html LADR-2009-11A/ladr/html/literals.html LADR-2009-11A/ladr/html/index.html LADR-2009-11A/ladr/html/glist.html LADR-2009-11A/ladr/html/clist.html LADR-2009-11A/ladr/html/pindex.html LADR-2009-11A/ladr/tlist.h LADR-2009-11A/ladr/memory.h LADR-2009-11A/ladr/clock.h LADR-2009-11A/ladr/clauses.h LADR-2009-11A/ladr/fpalist.h LADR-2009-11A/ladr/symbols.c~ LADR-2009-11A/ladr/unify.h LADR-2009-11A/ladr/formula.c.work LADR-2009-11A/ladr/dioph.c LADR-2009-11A/ladr/util/ LADR-2009-11A/ladr/util/init-package LADR-2009-11A/ladr/util/make_dep LADR-2009-11A/ladr/util/temp LADR-2009-11A/ladr/util/options-for-gui.py LADR-2009-11A/ladr/util/backup LADR-2009-11A/ladr/util/new-type LADR-2009-11A/ladr/util/init-types LADR-2009-11A/ladr/util/make_htmls LADR-2009-11A/ladr/util/make_protos LADR-2009-11A/ladr/util/doc5 LADR-2009-11A/ladr/util/proto LADR-2009-11A/ladr/util/options-for-gui.py~ LADR-2009-11A/ladr/util/to-html LADR-2009-11A/ladr/ibuffer.h LADR-2009-11A/ladr/attrib.c LADR-2009-11A/ladr/tptp_trans.c LADR-2009-11A/ladr/multiset.h LADR-2009-11A/ladr/btu.c LADR-2009-11A/ladr/README.kbo LADR-2009-11A/ladr/test.c LADR-2009-11A/ladr/weighttest LADR-2009-11A/ladr/fastparse.h LADR-2009-11A/ladr/compress.h LADR-2009-11A/ladr/int_code.c LADR-2009-11A/ladr/avltree.c LADR-2009-11A/ladr/literals.c LADR-2009-11A/ladr/ioutil.h LADR-2009-11A/ladr/listterm.c LADR-2009-11A/ladr/tptp_trans.c~ LADR-2009-11A/ladr/unify.c LADR-2009-11A/ladr/hash.c LADR-2009-11A/ladr/README.termorder LADR-2009-11A/ladr/termflag.c LADR-2009-11A/ladr/clash.c LADR-2009-11A/ladr/pindex.c LADR-2009-11A/ladr/btu.h LADR-2009-11A/ladr/memory.c~ LADR-2009-11A/ladr/glist.h LADR-2009-11A/ladr/avltree.h LADR-2009-11A/ladr/string.h LADR-2009-11A/ladr/compress.c LADR-2009-11A/ladr/flatdemod.h LADR-2009-11A/ladr/definitions.c LADR-2009-11A/ladr/maximal.h LADR-2009-11A/ladr/ac_redun.c LADR-2009-11A/ladr/parse.h LADR-2009-11A/apps.examples/ LADR-2009-11A/apps.examples/Makefile LADR-2009-11A/apps.examples/distributivity LADR-2009-11A/apps.examples/interp.OL6 LADR-2009-11A/apps.examples/qg.in LADR-2009-11A/apps.examples/lattice-sax LADR-2009-11A/apps.examples/run-all LADR-2009-11A/apps.examples/BA-sheffer LADR-2009-11A/apps.examples/OL.in LADR-2009-11A/apps.examples/lattice-sax.id-check LADR-2009-11A/apps.examples/non-MOL-OML LADR-2009-11A/apps.examples/backup.Mar10/ LADR-2009-11A/apps.examples/backup.Mar10/meet-join-equations.out LADR-2009-11A/apps.examples/backup.Mar10/qg.out3 LADR-2009-11A/apps.examples/backup.Mar10/OL.8.upper-covers LADR-2009-11A/apps.examples/backup.Mar10/qg.iso3 LADR-2009-11A/apps.examples/backup.Mar10/lattice-sax.rewritten LADR-2009-11A/apps.examples/backup.Mar10/MOL-cand.238 LADR-2009-11A/apps.examples/backup.Mar10/OL.6 LADR-2009-11A/apps.examples/backup.Mar10/BA-sheffer.out LADR-2009-11A/apps.examples/backup.Mar10/OL.8.out LADR-2009-11A/apps.examples/backup.Mar10/OL.8 LADR-2009-11A/apps.examples/backup.Mar10/mjc01s-equations.out LADR-2009-11A/apps.examples/MOL-cand.296 LADR-2009-11A/apps.examples/sed1 LADR-2009-11A/apps.examples/meet-join-equations LADR-2009-11A/apps.examples/err LADR-2009-11A/apps.examples/backup.Jan14/ LADR-2009-11A/apps.examples/backup.Jan14/meet-join-equations.out LADR-2009-11A/apps.examples/backup.Jan14/qg.out3 LADR-2009-11A/apps.examples/backup.Jan14/OL.8.upper-covers LADR-2009-11A/apps.examples/backup.Jan14/qg.iso3 LADR-2009-11A/apps.examples/backup.Jan14/lattice-sax.rewritten LADR-2009-11A/apps.examples/backup.Jan14/MOL-cand.238 LADR-2009-11A/apps.examples/backup.Jan14/OL.6 LADR-2009-11A/apps.examples/backup.Jan14/BA-sheffer.out LADR-2009-11A/apps.examples/backup.Jan14/OL.8.out LADR-2009-11A/apps.examples/backup.Jan14/OL.8 LADR-2009-11A/apps.examples/backup.Jan14/mjc01s-equations.out LADR-2009-11A/apps.examples/lattice.rules LADR-2009-11A/apps.examples/README LADR-2009-11A/apps.examples/mjc01s-equations LADR-2009-11A/apps.examples/index.html LADR-2009-11A/bin/ LADR-2009-11A/README.release-reminder LADR-2009-11A/mace4.examples/ LADR-2009-11A/mace4.examples/rw1.in LADR-2009-11A/mace4.examples/group2.in LADR-2009-11A/mace4.examples/README LADR-2009-11A/.gdb_history LADR-2009-11A/bob/ LADR-2009-11A/bob/ioutil.c LADR-2009-11A/bob/just.c LADR-2009-11A/bob/ChangelogBV LADR-2009-11A/bob/prooftrans.c LADR-2009-11A/bob/ioutil.h LADR-2009-11A/libtoolize.patch LADR-2009-11A/README.AMD_64 LADR-2009-11A/VERSION_DATE.h LADR-2009-11A/rev.py LADR-2009-11A/TODO/ LADR-2009-11A/TODO/temp LADR-2009-11A/TODO/factor.in LADR-2009-11A/TODO/mace4-segv.in LADR-2009-11A/TODO/README LADR-2009-11A/TODO/ADAM_2007_loose_ends LADR-2009-11A/README.first LADR-2009-11A/COPYING LADR-2009-11A/Changelog LADR-2009-11A/provers.src/ LADR-2009-11A/provers.src/pred_elim.c LADR-2009-11A/provers.src/fof-prover9.c LADR-2009-11A/provers.src/Makefile LADR-2009-11A/provers.src/pub LADR-2009-11A/provers.src/unfold.c LADR-2009-11A/provers.src/utilities.h LADR-2009-11A/provers.src/search.h LADR-2009-11A/provers.src/forward_subsume.h LADR-2009-11A/provers.src/white_black.c LADR-2009-11A/provers.src/newauto.c LADR-2009-11A/provers.src/mprover.c LADR-2009-11A/provers.src/white_black.h LADR-2009-11A/provers.src/options LADR-2009-11A/provers.src/pred_elim.h LADR-2009-11A/provers.src/TAGS LADR-2009-11A/provers.src/actions.h LADR-2009-11A/provers.src/prover9.c LADR-2009-11A/provers.src/.gdb_history LADR-2009-11A/provers.src/semantics.c LADR-2009-11A/provers.src/semantics.h LADR-2009-11A/provers.src/forward_subsume.c LADR-2009-11A/provers.src/demodulate.h LADR-2009-11A/provers.src/foffer.h LADR-2009-11A/provers.src/foffer.c LADR-2009-11A/provers.src/autosketches.examples/ LADR-2009-11A/provers.src/autosketches.examples/n3.in LADR-2009-11A/provers.src/autosketches.examples/xhn.in LADR-2009-11A/provers.src/autosketches.examples/newauto.c.from_bob LADR-2009-11A/provers.src/autosketches.examples/go LADR-2009-11A/provers.src/autosketches.examples/BA.in LADR-2009-11A/provers.src/autosketches.examples/BA.out LADR-2009-11A/provers.src/autosketches.examples/ec.out LADR-2009-11A/provers.src/autosketches.examples/ec.in LADR-2009-11A/provers.src/autosketches.examples/err LADR-2009-11A/provers.src/autosketches.examples/README LADR-2009-11A/provers.src/autosketches.examples/newsax.c.from_bob LADR-2009-11A/provers.src/autosketches.examples/n3.out LADR-2009-11A/provers.src/autosketches.examples/xhn.out LADR-2009-11A/provers.src/README.wired-in LADR-2009-11A/provers.src/README.symbol_order LADR-2009-11A/provers.src/README.actions LADR-2009-11A/provers.src/newsax.c LADR-2009-11A/provers.src/test.p LADR-2009-11A/provers.src/giv_select.h LADR-2009-11A/provers.src/giv_select.c LADR-2009-11A/provers.src/iterate4.c LADR-2009-11A/provers.src/search.c LADR-2009-11A/provers.src/index_lits.h LADR-2009-11A/provers.src/search-structures.h LADR-2009-11A/provers.src/save/ LADR-2009-11A/provers.src/save/picker.c LADR-2009-11A/provers.src/save/control_sos.h LADR-2009-11A/provers.src/save/auto.h LADR-2009-11A/provers.src/save/fork_and_wait LADR-2009-11A/provers.src/save/auto.c LADR-2009-11A/provers.src/save/prover9-simple.c LADR-2009-11A/provers.src/save/control_sos.c LADR-2009-11A/provers.src/save/poptions.h LADR-2009-11A/provers.src/save/poptions.c LADR-2009-11A/provers.src/save/definitions.h LADR-2009-11A/provers.src/save/attributes.c LADR-2009-11A/provers.src/save/lits_index.c LADR-2009-11A/provers.src/save/ploop4.c LADR-2009-11A/provers.src/save/prover9.h LADR-2009-11A/provers.src/save/cgrep.c LADR-2009-11A/provers.src/save/picker.h LADR-2009-11A/provers.src/save/lits_index.h LADR-2009-11A/provers.src/save/loop2.c LADR-2009-11A/provers.src/save/attributes.h LADR-2009-11A/provers.src/save/definitions.c LADR-2009-11A/provers.src/demodulate.c LADR-2009-11A/provers.src/README.new-sos-limit LADR-2009-11A/provers.src/index_lits.c LADR-2009-11A/provers.src/ladr_to_tptp.c LADR-2009-11A/provers.src/README.sos LADR-2009-11A/provers.src/README.white-black LADR-2009-11A/provers.src/util LADR-2009-11A/provers.src/README.parts LADR-2009-11A/provers.src/provers.h LADR-2009-11A/provers.src/unfold.h LADR-2009-11A/provers.src/utilities.c LADR-2009-11A/provers.src/README.doc LADR-2009-11A/provers.src/tptp_to_ladr.c LADR-2009-11A/provers.src/README.process LADR-2009-11A/provers.src/actions.c LADR-2009-11A/provers.src/provers.c LADR-2009-11A/provers.src/autosketches4.c LADR-2009-11A/test.src/ LADR-2009-11A/test.src/Makefile LADR-2009-11A/test.src/tptp_test LADR-2009-11A/test.src/avltest.c LADR-2009-11A/test.src/TAGS LADR-2009-11A/test.src/t1 LADR-2009-11A/test.src/t2 LADR-2009-11A/test.src/tptp_test.c LADR-2009-11A/test.src/avltest LADR-2009-11A/test.src/t2.in LADR-2009-11A/prover9.examples/ LADR-2009-11A/prover9.examples/x2.out LADR-2009-11A/prover9.examples/x2.hints LADR-2009-11A/prover9.examples/README LADR-2009-11A/prover9.examples/x2.in LADR-2009-11A/utilities/ LADR-2009-11A/utilities/prover9-mace4 LADR-2009-11A/utilities/attack LADR-2009-11A/utilities/looper LADR-2009-11A/utilities/gvizify LADR-2009-11A/utilities/get_kept LADR-2009-11A/utilities/proof3fo.xsl LADR-2009-11A/utilities/get_givens LADR-2009-11A/utilities/get_interps LADR-2009-11A/apps.src/ LADR-2009-11A/apps.src/test_complex.c LADR-2009-11A/apps.src/proof3.dtd LADR-2009-11A/apps.src/gen_trc_defs.c LADR-2009-11A/apps.src/Makefile LADR-2009-11A/apps.src/upper-covers.c LADR-2009-11A/apps.src/demods2 LADR-2009-11A/apps.src/interp3.xsl LADR-2009-11A/apps.src/h1.in LADR-2009-11A/apps.src/sigtest.c LADR-2009-11A/apps.src/sed.db-to-queries LADR-2009-11A/apps.src/README.solaris LADR-2009-11A/apps.src/README.directproof LADR-2009-11A/apps.src/olfilter.c LADR-2009-11A/apps.src/TAGS LADR-2009-11A/apps.src/isofilter.c LADR-2009-11A/apps.src/rewriter2.c LADR-2009-11A/apps.src/g2.model LADR-2009-11A/apps.src/isofilter2.c LADR-2009-11A/apps.src/.gdb_history LADR-2009-11A/apps.src/renamer.c LADR-2009-11A/apps.src/complex.c LADR-2009-11A/apps.src/miniscope.c LADR-2009-11A/apps.src/clausefilter.c LADR-2009-11A/apps.src/demods LADR-2009-11A/apps.src/py1 LADR-2009-11A/apps.src/awk1 LADR-2009-11A/apps.src/rewriter.c LADR-2009-11A/apps.src/mirror-flip.c LADR-2009-11A/apps.src/isofilter0.c LADR-2009-11A/apps.src/old/ LADR-2009-11A/apps.src/old/deny.c LADR-2009-11A/apps.src/old/cdprover.c LADR-2009-11A/apps.src/old/latgen.c LADR-2009-11A/apps.src/old/README LADR-2009-11A/apps.src/old/modelformat.c LADR-2009-11A/apps.src/old/undeny.c LADR-2009-11A/apps.src/prooftrans.c LADR-2009-11A/apps.src/sed2 LADR-2009-11A/apps.src/clausetester.c LADR-2009-11A/apps.src/H65d.givens LADR-2009-11A/apps.src/t1.in LADR-2009-11A/apps.src/interpfilter.c LADR-2009-11A/apps.src/h1.out LADR-2009-11A/apps.src/interpformat.c LADR-2009-11A/apps.src/sed1 LADR-2009-11A/apps.src/lt.dist LADR-2009-11A/apps.src/test_clause_eval.c LADR-2009-11A/apps.src/lt.m3 LADR-2009-11A/apps.src/unfast.c LADR-2009-11A/apps.src/proof3.xsl LADR-2009-11A/apps.src/directproof.c LADR-2009-11A/apps.src/sig.py LADR-2009-11A/apps.src/idfilter.c LADR-2009-11A/apps.src/perm3.c LADR-2009-11A/apps.src/dprofiles.c LADR-2009-11A/apps.src/notes LADR-2009-11A/apps.src/problems LADR-2009-11A/apps.src/interp3.dtd LADR-2009-11A/apps.src/test-directproof/ LADR-2009-11A/apps.src/test-directproof/omlsax2.direct LADR-2009-11A/apps.src/test-directproof/bw.direct LADR-2009-11A/apps.src/test-directproof/AD-gt.direct LADR-2009-11A/apps.src/test-directproof/3.1.out LADR-2009-11A/apps.src/test-directproof/rba.out LADR-2009-11A/apps.src/test-directproof/3.6.direct LADR-2009-11A/apps.src/test-directproof/temp LADR-2009-11A/apps.src/test-directproof/3.6.out LADR-2009-11A/apps.src/test-directproof/temp0 LADR-2009-11A/apps.src/test-directproof/3b.prf LADR-2009-11A/apps.src/test-directproof/dist-short-long.out LADR-2009-11A/apps.src/test-directproof/dist-short-long.direct LADR-2009-11A/apps.src/test-directproof/3b.direct LADR-2009-11A/apps.src/test-directproof/results-on-std-examples LADR-2009-11A/apps.src/test-directproof/bw.out LADR-2009-11A/apps.src/test-directproof/AD-gt.out LADR-2009-11A/apps.src/test-directproof/omlsax2.out LADR-2009-11A/apps.src/test-directproof/rba.direct LADR-2009-11A/apps.src/test-directproof/3.1.direct LADR-2009-11A/apps.src/latfilter.c sudo -u fink-bld [ENV] sh -c /tmp/fink.niF3x env LANG=C LC_ALL=C /sw/bin/tar --no-same-owner --no-same-permissions -xvf /sw/src/prover9-manual-2009-11A.tar.gz prover9-manual-2009-11A/ prover9-manual-2009-11A/prover9-5a-256t.gif prover9-manual-2009-11A/actions.html prover9-manual-2009-11A/weight_test.in prover9-manual-2009-11A/group-terms.out prover9-manual-2009-11A/template.reference prover9-manual-2009-11A/x2.standard prover9-manual-2009-11A/PUZ031-1.in prover9-manual-2009-11A/proof3.dtd prover9-manual-2009-11A/talk-software.html prover9-manual-2009-11A/navbar-version/ prover9-manual-2009-11A/navbar-version/actions.html prover9-manual-2009-11A/navbar-version/hints.html prover9-manual-2009-11A/navbar-version/manual.css prover9-manual-2009-11A/navbar-version/sed.navbar prover9-manual-2009-11A/navbar-version/manual-index.html prover9-manual-2009-11A/navbar-version/weight.html prover9-manual-2009-11A/navbar-version/inf-rules.html prover9-manual-2009-11A/navbar-version/input.html prover9-manual-2009-11A/navbar-version/process-inf.html prover9-manual-2009-11A/navbar-version/attributes.html prover9-manual-2009-11A/navbar-version/running.html prover9-manual-2009-11A/navbar-version/syntax.html prover9-manual-2009-11A/navbar-version/glossary.html prover9-manual-2009-11A/navbar-version/install.html prover9-manual-2009-11A/navbar-version/references.html prover9-manual-2009-11A/navbar-version/term-order.html prover9-manual-2009-11A/navbar-version/fof-reduction.html prover9-manual-2009-11A/navbar-version/options.html prover9-manual-2009-11A/navbar-version/output.html prover9-manual-2009-11A/navbar-version/limits.html prover9-manual-2009-11A/navbar-version/more-prep.html prover9-manual-2009-11A/navbar-version/select.html prover9-manual-2009-11A/navbar-version/goals.html prover9-manual-2009-11A/navbar-version/prooftrans.html prover9-manual-2009-11A/navbar-version/auto.html prover9-manual-2009-11A/navbar-version/loop.html prover9-manual-2009-11A/navbar-version/semantics.html prover9-manual-2009-11A/navbar-version/index.html prover9-manual-2009-11A/navbar-version/mace4.html prover9-manual-2009-11A/white-black.html prover9-manual-2009-11A/LT-port.out2 prover9-manual-2009-11A/non-MOL-OML.interps prover9-manual-2009-11A/uc-18.interps prover9-manual-2009-11A/x2.standard2 prover9-manual-2009-11A/hints.html prover9-manual-2009-11A/LT-82-2-interp.in prover9-manual-2009-11A/portable.in prover9-manual-2009-11A/sed.version~ prover9-manual-2009-11A/subset.in prover9-manual-2009-11A/subset_trans.proof4 prover9-manual-2009-11A/BA2.interps3 prover9-manual-2009-11A/BA2.interps prover9-manual-2009-11A/interp3.xsl prover9-manual-2009-11A/x2.raw prover9-manual-2009-11A/BA2.interps5 prover9-manual-2009-11A/go.outputs prover9-manual-2009-11A/references.tex prover9-manual-2009-11A/LT-port.out prover9-manual-2009-11A/manual.css prover9-manual-2009-11A/andrews.in prover9-manual-2009-11A/sed.version prover9-manual-2009-11A/sed.glossary-color prover9-manual-2009-11A/subset_trans.proof6 prover9-manual-2009-11A/BA2.interps2 prover9-manual-2009-11A/sed.option-refs prover9-manual-2009-11A/zebra2.out prover9-manual-2009-11A/PUZ031-1.out2 prover9-manual-2009-11A/LT-port.in prover9-manual-2009-11A/BA4.out prover9-manual-2009-11A/m4-isofilter.html prover9-manual-2009-11A/subset_trans.out3 prover9-manual-2009-11A/x2.tex prover9-manual-2009-11A/LT-82-2.out prover9-manual-2009-11A/options prover9-manual-2009-11A/go.options prover9-manual-2009-11A/weight.html prover9-manual-2009-11A/inf-rules.html prover9-manual-2009-11A/input.html prover9-manual-2009-11A/m4-options.html prover9-manual-2009-11A/LT-82-2-interp.out prover9-manual-2009-11A/subset_trans.proof7 prover9-manual-2009-11A/queens3.out prover9-manual-2009-11A/redeclare.in prover9-manual-2009-11A/subset_trans.out2 prover9-manual-2009-11A/uc-hunt.clauses prover9-manual-2009-11A/PUZ031-1.tptp prover9-manual-2009-11A/weight_test.out prover9-manual-2009-11A/PUZ031-1.out prover9-manual-2009-11A/andrews.out prover9-manual-2009-11A/go prover9-manual-2009-11A/process-inf.html prover9-manual-2009-11A/BA-Sheffer.demods prover9-manual-2009-11A/stringparm prover9-manual-2009-11A/olsax.out prover9-manual-2009-11A/LT-82-2-x.in prover9-manual-2009-11A/subset_trans.proof prover9-manual-2009-11A/x2.cooked prover9-manual-2009-11A/RBA-2.tptp prover9-manual-2009-11A/intro.html prover9-manual-2009-11A/subset_trans_expand.out prover9-manual-2009-11A/MOL-cand.238 prover9-manual-2009-11A/queens3.in prover9-manual-2009-11A/queens1.out prover9-manual-2009-11A/bool-ring.in prover9-manual-2009-11A/cabbages.out prover9-manual-2009-11A/attributes.html prover9-manual-2009-11A/README.util prover9-manual-2009-11A/RBA-2q.tptp prover9-manual-2009-11A/select2.html prover9-manual-2009-11A/kenken6.in prover9-manual-2009-11A/group.demods prover9-manual-2009-11A/glo.temp prover9-manual-2009-11A/subset_trans.proof2 prover9-manual-2009-11A/subset_trans.proof8 prover9-manual-2009-11A/flag prover9-manual-2009-11A/zebra2.in prover9-manual-2009-11A/hard.in prover9-manual-2009-11A/subset_trans.out4 prover9-manual-2009-11A/proof3.xsl.0 prover9-manual-2009-11A/subset_trans.proof5.xml prover9-manual-2009-11A/running.html prover9-manual-2009-11A/syntax.html prover9-manual-2009-11A/BA2.interps4 prover9-manual-2009-11A/parm prover9-manual-2009-11A/glossary.html prover9-manual-2009-11A/andrews.out2 prover9-manual-2009-11A/x2.mace4.out prover9-manual-2009-11A/bool-ring.out prover9-manual-2009-11A/easy.in prover9-manual-2009-11A/go-part prover9-manual-2009-11A/install.html prover9-manual-2009-11A/references.html prover9-manual-2009-11A/m4-arithmetic.html prover9-manual-2009-11A/term-order.html prover9-manual-2009-11A/group-terms.in prover9-manual-2009-11A/kenken6.out prover9-manual-2009-11A/MOL.in prover9-manual-2009-11A/jugs.in prover9-manual-2009-11A/2inverter.in prover9-manual-2009-11A/MOL.interps prover9-manual-2009-11A/hard-hints.out prover9-manual-2009-11A/sed3 prover9-manual-2009-11A/queens2.in prover9-manual-2009-11A/advanced.html prover9-manual-2009-11A/options.html prover9-manual-2009-11A/output.html prover9-manual-2009-11A/m4-arithmetic.html~ prover9-manual-2009-11A/README.run prover9-manual-2009-11A/x2.xml prover9-manual-2009-11A/setup_book prover9-manual-2009-11A/JA.in prover9-manual-2009-11A/x2.prover9.out prover9-manual-2009-11A/subset_trans_expand.in prover9-manual-2009-11A/limits.html prover9-manual-2009-11A/finalbook.pdf prover9-manual-2009-11A/send-money.out prover9-manual-2009-11A/port.py prover9-manual-2009-11A/queens2.out prover9-manual-2009-11A/MOL-cand.296 prover9-manual-2009-11A/more-prep.html prover9-manual-2009-11A/m4-input.html prover9-manual-2009-11A/ring41.in prover9-manual-2009-11A/sed1 prover9-manual-2009-11A/ring41.out prover9-manual-2009-11A/select.html prover9-manual-2009-11A/list.in prover9-manual-2009-11A/goals.html prover9-manual-2009-11A/easy.out prover9-manual-2009-11A/err prover9-manual-2009-11A/assoc-comm.clauses prover9-manual-2009-11A/x2.tabular prover9-manual-2009-11A/uc-hunt.out prover9-manual-2009-11A/TODO prover9-manual-2009-11A/prooftrans.html prover9-manual-2009-11A/trans.in prover9-manual-2009-11A/queens1.in prover9-manual-2009-11A/subset_trans.out prover9-manual-2009-11A/run-and-check prover9-manual-2009-11A/bool-ring.demods prover9-manual-2009-11A/proof3.xsl prover9-manual-2009-11A/send-money.in prover9-manual-2009-11A/LT-82-2.in prover9-manual-2009-11A/others.html prover9-manual-2009-11A/list.out prover9-manual-2009-11A/checked-jobs/ prover9-manual-2009-11A/make_book prover9-manual-2009-11A/talk-semantics.html prover9-manual-2009-11A/clause-properties.html prover9-manual-2009-11A/m4-interpformat.html prover9-manual-2009-11A/sed.glossary prover9-manual-2009-11A/intro.html~ prover9-manual-2009-11A/util/ prover9-manual-2009-11A/util/glossary.py prover9-manual-2009-11A/util/sed.cite prover9-manual-2009-11A/util/sed.www-pubs prover9-manual-2009-11A/util/options-make prover9-manual-2009-11A/util/prepare-refs prover9-manual-2009-11A/util/www-pubs prover9-manual-2009-11A/util/opt4.py prover9-manual-2009-11A/jugs.out prover9-manual-2009-11A/nav.html prover9-manual-2009-11A/fof-prover9.html prover9-manual-2009-11A/qg4.interps prover9-manual-2009-11A/sed.int prover9-manual-2009-11A/RBA-2.in prover9-manual-2009-11A/subset_trans.proof3 prover9-manual-2009-11A/easy.hints prover9-manual-2009-11A/olsax.in prover9-manual-2009-11A/2inverter.out prover9-manual-2009-11A/ubset_trans.proof2 prover9-manual-2009-11A/MOL.interps2 prover9-manual-2009-11A/BA2.in prover9-manual-2009-11A/x2.in prover9-manual-2009-11A/auto.html prover9-manual-2009-11A/loop.html prover9-manual-2009-11A/dependencies prover9-manual-2009-11A/redeclare.out prover9-manual-2009-11A/non-MOL-OML2.interps prover9-manual-2009-11A/sed.options-code prover9-manual-2009-11A/BA4.in prover9-manual-2009-11A/x2.portable prover9-manual-2009-11A/outs prover9-manual-2009-11A/subset_trans.proof1 prover9-manual-2009-11A/interp3.dtd prover9-manual-2009-11A/semantics.html prover9-manual-2009-11A/hard.out prover9-manual-2009-11A/index.html prover9-manual-2009-11A/subset_trans.in prover9-manual-2009-11A/qg4-ac.interps prover9-manual-2009-11A/mace4.html prover9-manual-2009-11A/template.glossary prover9-manual-2009-11A/proof3.dtd.0 prover9-manual-2009-11A/cabbages.in prover9-manual-2009-11A/syntax.html~ prover9-manual-2009-11A/references/ prover9-manual-2009-11A/references/references.tex prover9-manual-2009-11A/references/temp prover9-manual-2009-11A/references/sed.cite prover9-manual-2009-11A/references/sed.www-pubs prover9-manual-2009-11A/references/prepare-refs prover9-manual-2009-11A/references/www-pubs prover9-manual-2009-11A/references/README prover9-manual-2009-11A/references/references-ready.tex prover9-manual-2009-11A/production.html prover9-manual-2009-11A/otter_diff sudo -u fink-bld [ENV] sh -c /tmp/fink.h91O1 [ -r /sw/fink/dists/stable/main/finkinfo/sci/prover9.patch ] sudo -u fink-bld [ENV] sh -c /tmp/fink.bPOjs sed 's|@PREFIX@|/sw/build.build/root-prover9-2009-11a-5/sw|g' < /sw/fink/dists/stable/main/finkinfo/sci/prover9.patch | patch -p1 patching file Makefile patching file apps.src/Makefile patching file ladr/Makefile patching file mace4.src/Makefile patching file provers.src/Makefile patching file provers.src/ladr_to_tptp.c sudo -u fink-bld [ENV] sh -c /tmp/fink.5tgL9 make -j 1 all /Applications/Xcode.app/Contents/Developer/usr/bin/make -C ladr lib /Applications/Xcode.app/Contents/Developer/usr/bin/make libladr.a gcc -O4 -Wall -I/sw/include -c -o order.o order.c clang: warning: -O4 is equivalent to -O3 gcc -O4 -Wall -I/sw/include -c -o clock.o clock.c clang: warning: -O4 is equivalent to -O3 gcc -O4 -Wall -I/sw/include -c -o nonport.o nonport.c clang: warning: -O4 is equivalent to -O3 gcc -O4 -Wall -I/sw/include -c -o fatal.o fatal.c clang: warning: -O4 is equivalent to -O3 gcc -O4 -Wall -I/sw/include -c -o ibuffer.o ibuffer.c clang: warning: -O4 is equivalent to -O3 gcc -O4 -Wall -I/sw/include -c -o memory.o memory.c clang: warning: -O4 is equivalent to -O3 gcc -O4 -Wall -I/sw/include -c -o hash.o hash.c clang: warning: -O4 is equivalent to -O3 gcc -O4 -Wall -I/sw/include -c -o string.o string.c clang: warning: -O4 is equivalent to -O3 gcc -O4 -Wall -I/sw/include -c -o strbuf.o strbuf.c clang: warning: -O4 is equivalent to -O3 gcc -O4 -Wall -I/sw/include -c -o glist.o glist.c clang: warning: -O4 is equivalent to -O3 gcc -O4 -Wall -I/sw/include -c -o options.o options.c clang: warning: -O4 is equivalent to -O3 gcc -O4 -Wall -I/sw/include -c -o symbols.o symbols.c clang: warning: -O4 is equivalent to -O3 gcc -O4 -Wall -I/sw/include -c -o avltree.o avltree.c clang: warning: -O4 is equivalent to -O3 gcc -O4 -Wall -I/sw/include -c -o term.o term.c clang: warning: -O4 is equivalent to -O3 gcc -O4 -Wall -I/sw/include -c -o termflag.o termflag.c clang: warning: -O4 is equivalent to -O3 gcc -O4 -Wall -I/sw/include -c -o listterm.o listterm.c clang: warning: -O4 is equivalent to -O3 gcc -O4 -Wall -I/sw/include -c -o tlist.o tlist.c clang: warning: -O4 is equivalent to -O3 gcc -O4 -Wall -I/sw/include -c -o flatterm.o flatterm.c clang: warning: -O4 is equivalent to -O3 gcc -O4 -Wall -I/sw/include -c -o multiset.o multiset.c clang: warning: -O4 is equivalent to -O3 gcc -O4 -Wall -I/sw/include -c -o termorder.o termorder.c clang: warning: -O4 is equivalent to -O3 gcc -O4 -Wall -I/sw/include -c -o parse.o parse.c clang: warning: -O4 is equivalent to -O3 gcc -O4 -Wall -I/sw/include -c -o accanon.o accanon.c clang: warning: -O4 is equivalent to -O3 gcc -O4 -Wall -I/sw/include -c -o unify.o unify.c clang: warning: -O4 is equivalent to -O3 gcc -O4 -Wall -I/sw/include -c -o fpalist.o fpalist.c clang: warning: -O4 is equivalent to -O3 gcc -O4 -Wall -I/sw/include -c -o fpa.o fpa.c clang: warning: -O4 is equivalent to -O3 gcc -O4 -Wall -I/sw/include -c -o discrim.o discrim.c clang: warning: -O4 is equivalent to -O3 gcc -O4 -Wall -I/sw/include -c -o discrimb.o discrimb.c clang: warning: -O4 is equivalent to -O3 discrimb.c:487:7: warning: function 'check_flat2' is not needed and will not be emitted [-Wunneeded-internal-declaration] Flat2 check_flat2(Flat2 f) ^ 1 warning generated. gcc -O4 -Wall -I/sw/include -c -o discrimw.o discrimw.c clang: warning: -O4 is equivalent to -O3 discrimw.c:146:6: warning: function 'check_flat' is not needed and will not be emitted [-Wunneeded-internal-declaration] Flat check_flat(Flat f) ^ 1 warning generated. gcc -O4 -Wall -I/sw/include -c -o dioph.o dioph.c clang: warning: -O4 is equivalent to -O3 gcc -O4 -Wall -I/sw/include -c -o btu.o btu.c clang: warning: -O4 is equivalent to -O3 gcc -O4 -Wall -I/sw/include -c -o btm.o btm.c clang: warning: -O4 is equivalent to -O3 gcc -O4 -Wall -I/sw/include -c -o mindex.o mindex.c clang: warning: -O4 is equivalent to -O3 gcc -O4 -Wall -I/sw/include -c -o basic.o basic.c clang: warning: -O4 is equivalent to -O3 gcc -O4 -Wall -I/sw/include -c -o attrib.o attrib.c clang: warning: -O4 is equivalent to -O3 gcc -O4 -Wall -I/sw/include -c -o formula.o formula.c clang: warning: -O4 is equivalent to -O3 formula.c:711:25: warning: implicit conversion from enumeration type 'Ftype' to different enumeration type 'BOOL' [-Wenum-conversion] case AND_FORM: return OR_FORM; ~~~~~~ ^~~~~~~ formula.c:712:24: warning: implicit conversion from enumeration type 'Ftype' to different enumeration type 'BOOL' [-Wenum-conversion] case OR_FORM: return AND_FORM; ~~~~~~ ^~~~~~~~ formula.c:713:25: warning: implicit conversion from enumeration type 'Ftype' to different enumeration type 'BOOL' [-Wenum-conversion] case ALL_FORM: return EXISTS_FORM; ~~~~~~ ^~~~~~~~~~~ formula.c:714:28: warning: implicit conversion from enumeration type 'Ftype' to different enumeration type 'BOOL' [-Wenum-conversion] case EXISTS_FORM: return ALL_FORM; ~~~~~~ ^~~~~~~~ formula.c:736:13: warning: implicit conversion from enumeration type 'BOOL' to different enumeration type 'Ftype' [-Wenum-conversion] f->type = dual_type(f->type); ~ ^~~~~~~~~~~~~~~~~~ formula.c:1002:34: warning: implicit conversion from enumeration type 'BOOL' to different enumeration type 'Ftype' [-Wenum-conversion] Formula g = formula_get(1, dual_type(h->type)); ~~~~~~~~~~~ ^~~~~~~~~~~~~~~~~~ formula.c:1010:41: warning: implicit conversion from enumeration type 'BOOL' to different enumeration type 'Ftype' [-Wenum-conversion] Formula g = formula_get(h->arity, dual_type(h->type)); ~~~~~~~~~~~ ^~~~~~~~~~~~~~~~~~ 7 warnings generated. gcc -O4 -Wall -I/sw/include -c -o definitions.o definitions.c clang: warning: -O4 is equivalent to -O3 gcc -O4 -Wall -I/sw/include -c -o literals.o literals.c clang: warning: -O4 is equivalent to -O3 gcc -O4 -Wall -I/sw/include -c -o topform.o topform.c clang: warning: -O4 is equivalent to -O3 gcc -O4 -Wall -I/sw/include -c -o clist.o clist.c clang: warning: -O4 is equivalent to -O3 gcc -O4 -Wall -I/sw/include -c -o clauseid.o clauseid.c clang: warning: -O4 is equivalent to -O3 gcc -O4 -Wall -I/sw/include -c -o clauses.o clauses.c clang: warning: -O4 is equivalent to -O3 gcc -O4 -Wall -I/sw/include -c -o just.o just.c clang: warning: -O4 is equivalent to -O3 gcc -O4 -Wall -I/sw/include -c -o cnf.o cnf.c clang: warning: -O4 is equivalent to -O3 gcc -O4 -Wall -I/sw/include -c -o clausify.o clausify.c clang: warning: -O4 is equivalent to -O3 gcc -O4 -Wall -I/sw/include -c -o parautil.o parautil.c clang: warning: -O4 is equivalent to -O3 gcc -O4 -Wall -I/sw/include -c -o pindex.o pindex.c clang: warning: -O4 is equivalent to -O3 gcc -O4 -Wall -I/sw/include -c -o compress.o compress.c clang: warning: -O4 is equivalent to -O3 gcc -O4 -Wall -I/sw/include -c -o maximal.o maximal.c clang: warning: -O4 is equivalent to -O3 gcc -O4 -Wall -I/sw/include -c -o lindex.o lindex.c clang: warning: -O4 is equivalent to -O3 gcc -O4 -Wall -I/sw/include -c -o weight.o weight.c clang: warning: -O4 is equivalent to -O3 gcc -O4 -Wall -I/sw/include -c -o weight2.o weight2.c clang: warning: -O4 is equivalent to -O3 gcc -O4 -Wall -I/sw/include -c -o int_code.o int_code.c clang: warning: -O4 is equivalent to -O3 gcc -O4 -Wall -I/sw/include -c -o features.o features.c clang: warning: -O4 is equivalent to -O3 gcc -O4 -Wall -I/sw/include -c -o di_tree.o di_tree.c clang: warning: -O4 is equivalent to -O3 gcc -O4 -Wall -I/sw/include -c -o fastparse.o fastparse.c clang: warning: -O4 is equivalent to -O3 fastparse.c:186:23: warning: format string is not a string literal (potentially insecure) [-Wformat-security] fprintf(stderr, s); ^ fastparse.c:187:23: warning: format string is not a string literal (potentially insecure) [-Wformat-security] fprintf(stdout, s); ^ 2 warnings generated. gcc -O4 -Wall -I/sw/include -c -o random.o random.c clang: warning: -O4 is equivalent to -O3 gcc -O4 -Wall -I/sw/include -c -o subsume.o subsume.c clang: warning: -O4 is equivalent to -O3 gcc -O4 -Wall -I/sw/include -c -o clause_misc.o clause_misc.c clang: warning: -O4 is equivalent to -O3 gcc -O4 -Wall -I/sw/include -c -o clause_eval.o clause_eval.c clang: warning: -O4 is equivalent to -O3 gcc -O4 -Wall -I/sw/include -c -o complex.o complex.c clang: warning: -O4 is equivalent to -O3 gcc -O4 -Wall -I/sw/include -c -o dollar.o dollar.c clang: warning: -O4 is equivalent to -O3 gcc -O4 -Wall -I/sw/include -c -o flatdemod.o flatdemod.c clang: warning: -O4 is equivalent to -O3 gcc -O4 -Wall -I/sw/include -c -o demod.o demod.c clang: warning: -O4 is equivalent to -O3 gcc -O4 -Wall -I/sw/include -c -o clash.o clash.c clang: warning: -O4 is equivalent to -O3 clash.c:221:43: warning: variable 'n' is uninitialized when used here [-Wuninitialized] for (p = first; p != NULL; p = p->next, n++) { ^ clash.c:218:8: note: initialize the variable 'n' to silence this warning int n; ^ = 0 1 warning generated. gcc -O4 -Wall -I/sw/include -c -o resolve.o resolve.c clang: warning: -O4 is equivalent to -O3 gcc -O4 -Wall -I/sw/include -c -o paramod.o paramod.c clang: warning: -O4 is equivalent to -O3 gcc -O4 -Wall -I/sw/include -c -o backdemod.o backdemod.c clang: warning: -O4 is equivalent to -O3 gcc -O4 -Wall -I/sw/include -c -o hints.o hints.c clang: warning: -O4 is equivalent to -O3 gcc -O4 -Wall -I/sw/include -c -o ac_redun.o ac_redun.c clang: warning: -O4 is equivalent to -O3 gcc -O4 -Wall -I/sw/include -c -o xproofs.o xproofs.c clang: warning: -O4 is equivalent to -O3 gcc -O4 -Wall -I/sw/include -c -o ivy.o ivy.c clang: warning: -O4 is equivalent to -O3 gcc -O4 -Wall -I/sw/include -c -o interp.o interp.c clang: warning: -O4 is equivalent to -O3 interp.c:2238:10: warning: implicit conversion from enumeration type 'BOOL' to different enumeration type 'Ordertype' [-Wenum-conversion] return TRUE; ~~~~~~ ^~~~ 1 warning generated. gcc -O4 -Wall -I/sw/include -c -o std_options.o std_options.c clang: warning: -O4 is equivalent to -O3 gcc -O4 -Wall -I/sw/include -c -o banner.o banner.c clang: warning: -O4 is equivalent to -O3 gcc -O4 -Wall -I/sw/include -c -o ioutil.o ioutil.c clang: warning: -O4 is equivalent to -O3 gcc -O4 -Wall -I/sw/include -c -o tptp_trans.o tptp_trans.c clang: warning: -O4 is equivalent to -O3 gcc -O4 -Wall -I/sw/include -c -o top_input.o top_input.c clang: warning: -O4 is equivalent to -O3 ar rs libladr.a order.o clock.o nonport.o fatal.o ibuffer.o memory.o hash.o string.o strbuf.o glist.o options.o symbols.o avltree.o term.o termflag.o listterm.o tlist.o flatterm.o multiset.o termorder.o parse.o accanon.o unify.o fpalist.o fpa.o discrim.o discrimb.o discrimw.o dioph.o btu.o btm.o mindex.o basic.o attrib.o formula.o definitions.o literals.o topform.o clist.o clauseid.o clauses.o just.o cnf.o clausify.o parautil.o pindex.o compress.o maximal.o lindex.o weight.o weight2.o int_code.o features.o di_tree.o fastparse.o random.o subsume.o clause_misc.o clause_eval.o complex.o dollar.o flatdemod.o demod.o clash.o resolve.o paramod.o backdemod.o hints.o ac_redun.o xproofs.o ivy.o interp.o std_options.o banner.o ioutil.o tptp_trans.o top_input.o ar: creating archive libladr.a /Applications/Xcode.app/Contents/Developer/usr/bin/make -C mace4.src all cd ../ladr && /Applications/Xcode.app/Contents/Developer/usr/bin/make libladr.a make[2]: `libladr.a' is up to date. /Applications/Xcode.app/Contents/Developer/usr/bin/make clean /bin/rm -f *.o /Applications/Xcode.app/Contents/Developer/usr/bin/make libmace4.a gcc -O4 -Wall -I/sw/include -c -o estack.o estack.c clang: warning: -O4 is equivalent to -O3 gcc -O4 -Wall -I/sw/include -c -o util.o util.c clang: warning: -O4 is equivalent to -O3 gcc -O4 -Wall -I/sw/include -c -o print.o print.c clang: warning: -O4 is equivalent to -O3 print.c:114:13: warning: format string is not a string literal (potentially insecure) [-Wformat-security] printf(s2); ^~ print.c:119:15: warning: format string is not a string literal (potentially insecure) [-Wformat-security] printf(s3); ^~ print.c:137:11: warning: format string is not a string literal (potentially insecure) [-Wformat-security] printf(s2); ^~ print.c:145:15: warning: format string is not a string literal (potentially insecure) [-Wformat-security] printf(s3); ^~ 4 warnings generated. gcc -O4 -Wall -I/sw/include -c -o syms.o syms.c clang: warning: -O4 is equivalent to -O3 gcc -O4 -Wall -I/sw/include -c -o ground.o ground.c clang: warning: -O4 is equivalent to -O3 gcc -O4 -Wall -I/sw/include -c -o arithmetic.o arithmetic.c clang: warning: -O4 is equivalent to -O3 gcc -O4 -Wall -I/sw/include -c -o select.o select.c clang: warning: -O4 is equivalent to -O3 gcc -O4 -Wall -I/sw/include -c -o propagate.o propagate.c clang: warning: -O4 is equivalent to -O3 gcc -O4 -Wall -I/sw/include -c -o mstate.o mstate.c clang: warning: -O4 is equivalent to -O3 gcc -O4 -Wall -I/sw/include -c -o negpropindex.o negpropindex.c clang: warning: -O4 is equivalent to -O3 gcc -O4 -Wall -I/sw/include -c -o negprop.o negprop.c clang: warning: -O4 is equivalent to -O3 gcc -O4 -Wall -I/sw/include -c -o ordercells.o ordercells.c clang: warning: -O4 is equivalent to -O3 gcc -O4 -Wall -I/sw/include -c -o commandline.o commandline.c clang: warning: -O4 is equivalent to -O3 gcc -O4 -Wall -I/sw/include -c -o msearch.o msearch.c clang: warning: -O4 is equivalent to -O3 ar rs libmace4.a estack.o util.o print.o syms.o ground.o arithmetic.o select.o propagate.o mstate.o negpropindex.o negprop.o ordercells.o commandline.o msearch.o ar: creating archive libmace4.a gcc -O4 -Wall -I/sw/include -c -o mace4.o mace4.c clang: warning: -O4 is equivalent to -O3 gcc -O4 -Wall -o mace4 mace4.o libmace4.a ../ladr/libladr.a cp mace4 ../bin /Applications/Xcode.app/Contents/Developer/usr/bin/make -C provers.src all /Applications/Xcode.app/Contents/Developer/usr/bin/make -C ../ladr libladr /Applications/Xcode.app/Contents/Developer/usr/bin/make libladr.a make[3]: `libladr.a' is up to date. /Applications/Xcode.app/Contents/Developer/usr/bin/make clean /bin/rm -f *.o /Applications/Xcode.app/Contents/Developer/usr/bin/make -C ../mace4.src libmace4 /Applications/Xcode.app/Contents/Developer/usr/bin/make libmace4.a make[3]: `libmace4.a' is up to date. /Applications/Xcode.app/Contents/Developer/usr/bin/make clean /bin/rm -f *.o gcc -O4 -Wall -I/sw/include -c -o prover9.o prover9.c clang: warning: -O4 is equivalent to -O3 gcc -O4 -Wall -I/sw/include -c -o index_lits.o index_lits.c clang: warning: -O4 is equivalent to -O3 gcc -O4 -Wall -I/sw/include -c -o forward_subsume.o forward_subsume.c clang: warning: -O4 is equivalent to -O3 gcc -O4 -Wall -I/sw/include -c -o demodulate.o demodulate.c clang: warning: -O4 is equivalent to -O3 gcc -O4 -Wall -I/sw/include -c -o pred_elim.o pred_elim.c clang: warning: -O4 is equivalent to -O3 gcc -O4 -Wall -I/sw/include -c -o unfold.o unfold.c clang: warning: -O4 is equivalent to -O3 gcc -O4 -Wall -I/sw/include -c -o semantics.o semantics.c clang: warning: -O4 is equivalent to -O3 gcc -O4 -Wall -I/sw/include -c -o giv_select.o giv_select.c clang: warning: -O4 is equivalent to -O3 gcc -O4 -Wall -I/sw/include -c -o white_black.o white_black.c clang: warning: -O4 is equivalent to -O3 gcc -O4 -Wall -I/sw/include -c -o actions.o actions.c clang: warning: -O4 is equivalent to -O3 gcc -O4 -Wall -I/sw/include -c -o search.o search.c clang: warning: -O4 is equivalent to -O3 search.c:1991:34: warning: comparison of constant 100 with expression of type 'BOOL' is always true [-Wtautological-constant-out-of-range-compare] if (Glob.number_of_clauses < 100) { ~~~~~~~~~~~~~~~~~~~~~~ ^ ~~~ 1 warning generated. gcc -O4 -Wall -I/sw/include -c -o utilities.o utilities.c clang: warning: -O4 is equivalent to -O3 gcc -O4 -Wall -I/sw/include -c -o provers.o provers.c clang: warning: -O4 is equivalent to -O3 gcc -O4 -Wall -I/sw/include -c -o foffer.o foffer.c clang: warning: -O4 is equivalent to -O3 gcc -O4 -Wall -lm -o prover9 prover9.o index_lits.o forward_subsume.o demodulate.o pred_elim.o unfold.o semantics.o giv_select.o white_black.o actions.o search.o utilities.o provers.o foffer.o ../ladr/libladr.a gcc -O4 -Wall -I/sw/include -c -o fof-prover9.o fof-prover9.c clang: warning: -O4 is equivalent to -O3 gcc -O4 -Wall -lm -o fof-prover9 fof-prover9.o index_lits.o forward_subsume.o demodulate.o pred_elim.o unfold.o semantics.o giv_select.o white_black.o actions.o search.o utilities.o provers.o foffer.o ../ladr/libladr.a gcc -O4 -Wall -I/sw/include -c -o autosketches4.o autosketches4.c clang: warning: -O4 is equivalent to -O3 gcc -O4 -Wall -lm -o autosketches4 autosketches4.o index_lits.o forward_subsume.o demodulate.o pred_elim.o unfold.o semantics.o giv_select.o white_black.o actions.o search.o utilities.o provers.o foffer.o ../ladr/libladr.a gcc -O4 -Wall -I/sw/include -c -o newauto.o newauto.c clang: warning: -O4 is equivalent to -O3 gcc -O4 -Wall -lm -o newauto newauto.o index_lits.o forward_subsume.o demodulate.o pred_elim.o unfold.o semantics.o giv_select.o white_black.o actions.o search.o utilities.o provers.o foffer.o ../ladr/libladr.a gcc -O4 -Wall -I/sw/include -c -o newsax.o newsax.c clang: warning: -O4 is equivalent to -O3 gcc -O4 -Wall -lm -o newsax newsax.o index_lits.o forward_subsume.o demodulate.o pred_elim.o unfold.o semantics.o giv_select.o white_black.o actions.o search.o utilities.o provers.o foffer.o ../ladr/libladr.a gcc -O4 -Wall -I/sw/include -c -o ladr_to_tptp.o ladr_to_tptp.c clang: warning: -O4 is equivalent to -O3 gcc -O4 -Wall -lm -o ladr_to_tptp ladr_to_tptp.o index_lits.o forward_subsume.o demodulate.o pred_elim.o unfold.o semantics.o giv_select.o white_black.o actions.o search.o utilities.o provers.o foffer.o ../ladr/libladr.a gcc -O4 -Wall -I/sw/include -c -o tptp_to_ladr.o tptp_to_ladr.c clang: warning: -O4 is equivalent to -O3 gcc -O4 -Wall -lm -o tptp_to_ladr tptp_to_ladr.o index_lits.o forward_subsume.o demodulate.o pred_elim.o unfold.o semantics.o giv_select.o white_black.o actions.o search.o utilities.o provers.o foffer.o ../ladr/libladr.a /bin/cp -p prover9 fof-prover9 autosketches4 newauto newsax ladr_to_tptp tptp_to_ladr ../bin /bin/rm -f *.o /Applications/Xcode.app/Contents/Developer/usr/bin/make -C apps.src all cd ../ladr && /Applications/Xcode.app/Contents/Developer/usr/bin/make libladr.a make[2]: `libladr.a' is up to date. gcc -O4 -Wall -I/sw/include -c -o latfilter.o latfilter.c clang: warning: -O4 is equivalent to -O3 gcc -O4 -Wall -o latfilter latfilter.o ../ladr/libladr.a gcc -O4 -Wall -I/sw/include -c -o olfilter.o olfilter.c clang: warning: -O4 is equivalent to -O3 gcc -O4 -Wall -o olfilter olfilter.o ../ladr/libladr.a gcc -O4 -Wall -I/sw/include -c -o clausefilter.o clausefilter.c clang: warning: -O4 is equivalent to -O3 gcc -O4 -Wall -o clausefilter clausefilter.o ../ladr/libladr.a gcc -O4 -Wall -I/sw/include -c -o idfilter.o idfilter.c clang: warning: -O4 is equivalent to -O3 gcc -O4 -Wall -o idfilter idfilter.o ../ladr/libladr.a gcc -O4 -Wall -I/sw/include -c -o renamer.o renamer.c clang: warning: -O4 is equivalent to -O3 gcc -O4 -Wall -o renamer renamer.o ../ladr/libladr.a gcc -O4 -Wall -I/sw/include -c -o unfast.o unfast.c clang: warning: -O4 is equivalent to -O3 gcc -O4 -Wall -o unfast unfast.o ../ladr/libladr.a gcc -O4 -Wall -I/sw/include -c -o clausetester.o clausetester.c clang: warning: -O4 is equivalent to -O3 gcc -O4 -Wall -o clausetester clausetester.o ../ladr/libladr.a gcc -O4 -Wall -I/sw/include -c -o rewriter.o rewriter.c clang: warning: -O4 is equivalent to -O3 gcc -O4 -Wall -o rewriter rewriter.o ../ladr/libladr.a gcc -O4 -Wall -I/sw/include -c -o isofilter0.o isofilter0.c clang: warning: -O4 is equivalent to -O3 gcc -O4 -Wall -o isofilter0 isofilter0.o ../ladr/libladr.a gcc -O4 -Wall -I/sw/include -c -o isofilter.o isofilter.c clang: warning: -O4 is equivalent to -O3 gcc -O4 -Wall -o isofilter isofilter.o ../ladr/libladr.a gcc -O4 -Wall -I/sw/include -c -o isofilter2.o isofilter2.c clang: warning: -O4 is equivalent to -O3 gcc -O4 -Wall -o isofilter2 isofilter2.o ../ladr/libladr.a gcc -O4 -Wall -I/sw/include -c -o dprofiles.o dprofiles.c clang: warning: -O4 is equivalent to -O3 gcc -O4 -Wall -o dprofiles dprofiles.o ../ladr/libladr.a gcc -O4 -Wall -I/sw/include -c -o interpfilter.o interpfilter.c clang: warning: -O4 is equivalent to -O3 gcc -O4 -Wall -o interpfilter interpfilter.o ../ladr/libladr.a gcc -O4 -Wall -I/sw/include -c -o upper-covers.o upper-covers.c clang: warning: -O4 is equivalent to -O3 gcc -O4 -Wall -o upper-covers upper-covers.o ../ladr/libladr.a gcc -O4 -Wall -I/sw/include -c -o miniscope.o miniscope.c clang: warning: -O4 is equivalent to -O3 gcc -O4 -Wall -o miniscope miniscope.o ../ladr/libladr.a gcc -O4 -Wall -I/sw/include -c -o interpformat.o interpformat.c clang: warning: -O4 is equivalent to -O3 gcc -O4 -Wall -o interpformat interpformat.o ../ladr/libladr.a gcc -O4 -Wall -I/sw/include -c -o prooftrans.o prooftrans.c clang: warning: -O4 is equivalent to -O3 gcc -O4 -Wall -o prooftrans prooftrans.o ../ladr/libladr.a gcc -O4 -Wall -I/sw/include -c -o mirror-flip.o mirror-flip.c clang: warning: -O4 is equivalent to -O3 gcc -O4 -Wall -o mirror-flip mirror-flip.o ../ladr/libladr.a gcc -O4 -Wall -I/sw/include -c -o perm3.o perm3.c clang: warning: -O4 is equivalent to -O3 gcc -O4 -Wall -o perm3 perm3.o ../ladr/libladr.a gcc -O4 -Wall -I/sw/include -c -o sigtest.o sigtest.c clang: warning: -O4 is equivalent to -O3 gcc -O4 -Wall -o sigtest sigtest.o ../ladr/libladr.a gcc -O4 -Wall -I/sw/include -c -o directproof.o directproof.c clang: warning: -O4 is equivalent to -O3 gcc -O4 -Wall -o directproof directproof.o ../ladr/libladr.a gcc -O4 -Wall -I/sw/include -c -o test_clause_eval.o test_clause_eval.c clang: warning: -O4 is equivalent to -O3 gcc -O4 -Wall -o test_clause_eval test_clause_eval.o ../ladr/libladr.a gcc -O4 -Wall -I/sw/include -c -o test_complex.o test_complex.c clang: warning: -O4 is equivalent to -O3 gcc -O4 -Wall -o test_complex test_complex.o ../ladr/libladr.a gcc -O4 -Wall -I/sw/include -c -o complex.o complex.c clang: warning: -O4 is equivalent to -O3 gcc -O4 -Wall -o complex complex.o ../ladr/libladr.a gcc -O4 -Wall -I/sw/include -c -o gen_trc_defs.o gen_trc_defs.c clang: warning: -O4 is equivalent to -O3 gcc -O4 -Wall -o gen_trc_defs gen_trc_defs.o ../ladr/libladr.a /bin/mv latfilter olfilter clausefilter idfilter renamer unfast clausetester rewriter isofilter0 isofilter isofilter2 dprofiles interpfilter upper-covers miniscope interpformat prooftrans mirror-flip perm3 sigtest directproof test_clause_eval test_complex complex gen_trc_defs ../bin /bin/rm -f *.o latfilter olfilter clausefilter idfilter renamer unfast clausetester rewriter isofilter0 isofilter isofilter2 dprofiles interpfilter upper-covers miniscope interpformat prooftrans mirror-flip perm3 sigtest directproof test_clause_eval test_complex complex gen_trc_defs find utilities -type f -exec cp {} /sw/build.build/root-prover9-2009-11a-5/sw/bin ';' cp: /sw/build.build/root-prover9-2009-11a-5/sw/bin: No such file or directory cp: /sw/build.build/root-prover9-2009-11a-5/sw/bin: No such file or directory cp: /sw/build.build/root-prover9-2009-11a-5/sw/bin: No such file or directory cp: /sw/build.build/root-prover9-2009-11a-5/sw/bin: No such file or directory cp: /sw/build.build/root-prover9-2009-11a-5/sw/bin: No such file or directory cp: /sw/build.build/root-prover9-2009-11a-5/sw/bin: No such file or directory cp: /sw/build.build/root-prover9-2009-11a-5/sw/bin: No such file or directory cp: /sw/build.build/root-prover9-2009-11a-5/sw/bin: No such file or directory **** Now try 'make test1'. **** make -j 1 test1 bin/prover9 -f prover9.examples/x2.in | bin/prooftrans parents_only ============================== prooftrans ============================ Prover9 (64) version 2009-11A, November 2009. Process 32972 was started by fink-bld on aurora, Mon Aug 4 22:06:27 2014 The command was "bin/prover9 -f prover9.examples/x2.in". ============================== end of head =========================== ============================== end of input ========================== -------- Proof 1 -------- THEOREM PROVED ------ process 32972 exit (max_proofs) ------  ============================== PROOF ================================= % -------- Comments from original proof -------- % Proof 1 at 0.00 (+ 0.00) seconds. % Length of proof is 16. % Level of proof is 7. % Maximum clause weight is 11.000. % Given clauses 12. 1 x * y = y * x # label(non_clause) # label(goal). []. 2 e * x = x. []. 3 x' * x = e. []. 4 (x * y) * z = x * (y * z). []. 5 x * x = e. []. 6 c2 * c1 != c1 * c2. [1]. 7 x' * (x * y) = y. [3,4,2]. 8 x * (x * y) = y. [5,4,2]. 9 x * (y * (x * y)) = e. [5,4]. 11 x'' * e = x. [3,7]. 13 x' * e = x. [5,7]. 15 x' = x. [11,13]. 16 x * e = x. [13,15]. 19 x * (y * x) = y. [9,8,16]. 24 x * y = y * x. [19,8]. 25 $F. [24,6]. ============================== end of proof ========================== **** If you see a proof, prover9 is probably okay. **** **** Next try 'make test2'. **** make -j 1 test2 bin/mace4 -v0 -f mace4.examples/group2.in | bin/interpformat tabular === Mace4 starting on domain size 2. === === Mace4 starting on domain size 3. === === Mace4 starting on domain size 4. === === Mace4 starting on domain size 5. === === Mace4 starting on domain size 6. === ------ process 32980 exit (max_models) ------ % number = 1 % seconds = 0 % Interpretation of size 6 * : | 0 1 2 3 4 5 ---+------------ 0 | 0 1 2 3 4 5 1 | 1 0 3 2 5 4 2 | 2 4 0 5 1 3 3 | 3 5 1 4 0 2 4 | 4 2 5 0 3 1 5 | 5 3 4 1 2 0 c1 : 0 c2 : 1 c3 : 2 f1 : 0 1 2 3 4 5 ---------------- 0 1 2 4 3 5 **** If you see a group table, mace4 is probably okay. **** **** Next try 'make test3'. **** make -j 1 test3 bin/mace4 -n3 -m -1 < apps.examples/qg.in | bin/interpformat | bin/isofilter === Mace4 starting on domain size 3. === ------ process 32988 exit (all_models) ------ interpretation( 3, [number = 1,seconds = 0], [ function(*(_,_), [ 0,1,2, 1,2,0, 2,0,1]), function(/(_,_), [ 0,2,1, 1,0,2, 2,1,0]), function(\(_,_), [ 0,1,2, 2,0,1, 1,2,0])]). interpretation( 3, [number = 2,seconds = 0], [ function(*(_,_), [ 0,1,2, 2,0,1, 1,2,0]), function(/(_,_), [ 0,1,2, 2,0,1, 1,2,0]), function(\(_,_), [ 0,1,2, 1,2,0, 2,0,1])]). interpretation( 3, [number = 3,seconds = 0], [ function(*(_,_), [ 0,2,1, 1,0,2, 2,1,0]), function(/(_,_), [ 0,1,2, 1,2,0, 2,0,1]), function(\(_,_), [ 0,2,1, 1,0,2, 2,1,0])]). interpretation( 3, [number = 4,seconds = 0], [ function(*(_,_), [ 0,2,1, 2,1,0, 1,0,2]), function(/(_,_), [ 0,2,1, 2,1,0, 1,0,2]), function(\(_,_), [ 0,2,1, 2,1,0, 1,0,2])]). interpretation( 3, [number = 5,seconds = 0], [ function(*(_,_), [ 1,0,2, 0,2,1, 2,1,0]), function(/(_,_), [ 1,0,2, 0,2,1, 2,1,0]), function(\(_,_), [ 1,0,2, 0,2,1, 2,1,0])]). % isofilter: input=8, kept=5, checks=16, perms=88, 0.00 seconds. *** If you see 5 interpretations, the apps are probably okay. *** /bin/rm -rf /sw/build.build/root-prover9-2009-11a-5 /bin/mkdir -p /sw/build.build/root-prover9-2009-11a-5/sw /bin/mkdir -p /sw/build.build/root-prover9-2009-11a-5/DEBIAN /usr/sbin/chown -R fink-bld:fink-bld /sw/build.build/root-prover9-2009-11a-5 sudo -u fink-bld [ENV] sh -c /tmp/fink.mQsZ1 mkdir -p /sw/build.build/root-prover9-2009-11a-5/sw/share/xml/xsl install -m 644 utilities/proof3fo.xsl /sw/build.build/root-prover9-2009-11a-5/sw/share/xml/xsl install -m 644 apps.src/interp3.xsl /sw/build.build/root-prover9-2009-11a-5/sw/share/xml/xsl install -m 644 apps.src/proof3.xsl /sw/build.build/root-prover9-2009-11a-5/sw/share/xml/xsl chmod 755 utilities/gvizify mkdir -p /sw/build.build/root-prover9-2009-11a-5/sw/bin install -m 755 bin/* /sw/build.build/root-prover9-2009-11a-5/sw/bin install -m 755 utilities/attack /sw/build.build/root-prover9-2009-11a-5/sw/bin install -m 755 utilities/get_givens /sw/build.build/root-prover9-2009-11a-5/sw/bin install -m 755 utilities/get_interps /sw/build.build/root-prover9-2009-11a-5/sw/bin install -m 755 utilities/get_kept /sw/build.build/root-prover9-2009-11a-5/sw/bin install -m 755 utilities/looper /sw/build.build/root-prover9-2009-11a-5/sw/bin install -m 755 utilities/prover9-mace4 /sw/build.build/root-prover9-2009-11a-5/sw/bin mkdir -p /sw/build.build/root-prover9-2009-11a-5/sw/share/doc/prover9 cp -R prover9-manual-2009-11A/* /sw/build.build/root-prover9-2009-11a-5/sw/share/doc/prover9 sudo -u fink-bld [ENV] sh -c /tmp/fink.bPgGR /bin/rm -f /sw/build.build/root-prover9-2009-11a-5/sw/info/dir /sw/build.build/root-prover9-2009-11a-5/sw/info/dir.old /sw/build.build/root-prover9-2009-11a-5/sw/share/info/dir /sw/build.build/root-prover9-2009-11a-5/sw/share/info/dir.old Reverting ownership of install dir to root Writing control file... Writing md5sums file... env LANG=C LC_ALL=C dpkg-deb -b root-prover9-2009-11a-5 /sw/fink/10.9/stable/main/binary-darwin-x86_64/sci dpkg-deb: building package `prover9' in `/sw/fink/10.9/stable/main/binary-darwin-x86_64/sci/prover9_2009-11a-5_darwin-x86_64.deb'. Removing runtime build-lock... Removing build-lock package... /sw/bin/dpkg-lockwait -r fink-buildlock-prover9-2009-11a-5 (Reading database ... 4770 files and directories currently installed.) Removing fink-buildlock-prover9-2009-11a-5 ...