System: Darwin Version: 1.3 URL: http://goedel.cs.uiowa.edu/Darwin/ Command: darwin -eprover /home/graph/tptp/Systems/Darwin---1.3/eprover -pl 0 -pmc true -to %d %s Format: tptp Transform: none SPCs: FOF CNF Solved: Theorem = SZS status: Theorem Solved: CounterSatisfiable = SZS status: CounterSatisfiable Solved: Unsatisfiable = SZS status: Unsatisfiable Solved: Satisfiable = SZS status: Satisfiable GaveUp: SZS status: GaveUp StartSoln: Model = START OF MODEL EndSoln: Model = END OF MODEL CASCDiv: EPR CASCProb: NoTransform/tptp Status: READY SSCPA TSTP SoTPTP CASC System: Darwin Version: 1.4.1 URL: http://goedel.cs.uiowa.edu/Darwin/ Command: darwin -eprover /home/graph/tptp/Systems/Darwin---1.4.1/eprover -pl 0 -pmc true -to %d %s Format: tptp Transform: none SPCs: FOF CNF Solved: Theorem = SZS status Theorem Solved: CounterSatisfiable = SZS status CounterSatisfiable Solved: Unsatisfiable = SZS status Unsatisfiable Solved: Satisfiable = SZS status Satisfiable GaveUp: SZS status GaveUp StartSoln: Model = SZS output start Model EndSoln: Model = SZS output end Model CASCDiv: EPR CASCProb: NoTransform/tptp Status: READY SSCPA TSTP SoTPTP CASC System: DarwinFM Version: 1.4.1 URL: http://goedel.cs.uiowa.edu/Darwin/ ContextCommand: darwin -fd true -pl 0 -pmc true %s Command: darwin -fd true -pl 0 -eprover /home/graph/tptp/Systems/Darwin---1.4.1/eprover -to %d -pmtptp true %s Format: tptp:short Transform: none SPCs: FOF_NKT FOF_NKU CNF_NKU Solved: Theorem = SZS status Theorem Solved: CounterSatisfiable = SZS status CounterSatisfiable Solved: Unsatisfiable = SZS status Unsatisfiable Solved: Satisfiable = SZS status Satisfiable GaveUp: SZS status: GaveUp StartSoln: FiniteModel = SZS output start FiniteModel EndSoln: FiniteModel = SZS output end FiniteModel CASCDiv: FNT SAT CASCProb: NoTransform/tptp Status: READY SSCPA TSTP SoTPTP CASC System: E Version: 0.999 URL: http://www.eprover.org/ Command: eprover -s --print-statistics -xAuto -tAuto --cpu-limit=%d --memory-limit=384 --tstp-in %s Format: tptp Transform: none SPCs: FOF CNF Solved: Theorem = SZS status: Theorem Solved: CounterSatisfiable = SZS status: CounterSatisfiable Solved: Unsatisfiable = SZS status: Unsatisfiable Solved: Satisfiable = SZS status: Satisfiable GaveUp: Failure: Statistic: Generated = Generated clauses *: *([0-9]*) Statistic: NonTrivial = the previous two non-trivial *: *([0-9]*) Statistic: Processed = Processed clauses *: *([0-9]*) CASCDiv: FOF CNF FNT SAT EPR UEQ CASCProb: NoTransform/tptp Status: READY SSCPA TSTP SoTPTP CASC System: EP Version: 0.999 URL: http://www.eprover.org/ Command: eproof --print-statistics -xAuto -tAuto --cpu-limit=%d --memory-limit=384 --tstp-in --tstp-out %s Format: tptp Transform: none SPCs: FOF CNF Solved: Theorem = SZS status: Theorem Solved: CounterSatisfiable = SZS status: CounterSatisfiable Solved: Unsatisfiable = SZS status: Unsatisfiable Solved: Satisfiable = SZS status: Satisfiable GaveUp: Cannot determine problem status StartSoln: CNFRefutation = SZS output start CNFRefutation EndSoln: CNFRefutation = SZS output end CNFRefutation StartSoln: Saturation = SZS output start Saturation EndSoln: Saturation = SZS output end Saturation Statistic: Clauses = Generated clauses *: *([0-9]*) Statistic: NonTrivial = the previous two non-trivial *: *([0-9]*) Statistic: Processed = Processed clauses *: *([0-9]*) CASCDiv: FOF CNF CASCProb: NoTransform/tptp Status: READY SSCPA TSTP SoTPTP CASC System: E-KRHyper Version: 1.0 URL: http://www.uni-koblenz.de/~bpelzer/ekrhyper/ Command: casc/ekrhyper %s Format: protein Transform: none SPCs: CNF Solved: Unsatisfiable = SZS status Unsatisfiable Solved: Satisfiable = SZS status Satisfiable GaveUp: dummy_never_found StartSoln: CNFRefutation = SZS output start CNFRefutation EndSoln: CNFRefutation = SZS output stop CNFRefutation Statistic: Disjuntcions = Disjunction nodes *: *([0-9]*) Statistic: Depth = Tableau depth *: *([0-9]*) Statistic: Closed = Closed branches *: *([0-9]*) Statistic: Evaluations = Evaluation rounds *: *([0-9]*) CASCDiv: CNF EPR CASCProb: NoTransform/protein Status: READY SSCPA TSTP SoTPTP CASC System: Equinox Version: 1.2 URL: http://www.cs.chalmers.se/~koen/folkung/ Command: equinox --tstp --split %s Format: tptp Transform: none SPCs: FOF CNF Solved: Theorem = SZS status Theorem Solved: CounterSatisfiable = SZS status CounterSatisfiable Solved: Unsatisfiable = SZS status Unsatisfiable Solved: Satisfiable = SZS status Satisfiable GaveUp: SZS status GaveUp CASCDiv: FOF CNF EPR UEQ CASCProb: NoTransform/tptp Status: READY TSTP SSCPA SoTPTP CASC System: Fampire Version: 1.3 URL: http://dreamers.com/lichlair/imagenes/bloodredmoon3.jpg Command: FlotterOnTPTP.pl -f oldtptp -s vampire -t %d %s Format: tptp Transform: none SPCs: FOF Solved: Theorem = --- PROVED --- Solved: CounterSatisfiable = --- UNPROVABLE --- Solved: Unsatisfiable = --- PROVED --- Solved: Satisfiable = --- UNPROVABLE --- GaveUp: --- CANNOT PROVE --- GaveUp: dummy_never_found CASCDiv: FOF CASCProb: NoTransform/tptp Status: SoTPTP TSTP CASC System: Geo Version: 2007f URL: http://www.ii.uni.wroc.pl/~nivelle/software/geo/ Command: geo -nonempty -tptp_input -inputfile %s Format: tptp Transform: none SPCs: FOF CNF Solved: Theorem = START-OF-PROOF Solved: CounterSatisfiable = START-OF-MODEL Solved: Unsatisfiable = START-OF-PROOF Solved: Satisfiable = START-OF-MODEL StartSoln: Refutation = START-OF-PROOF EndSoln: Refutation = END-OF-PROOF StartSoln: Model = START-OF-MODEL EndSoln: Model = END-OF-MODEL GaveUp: ERROR CASCDiv: FOF CNF FNT SAT EPR UEQ CASCProb: NoTransform/tptp Status: READY SSCPA TSTP SoTPTP CASC System: iProver Version: 0.2 URL: http://www.cs.man.ac.uk/~korovink/iprover/ Command: iproveropt --eprover_path /home/graph/tptp/Systems/iProver---0.2/ %s Format: tptp Transform: none SPCs: FOF CNF Solved: Theorem = PROVED Solved: CounterSatisfiable = SATISFIABLE Solved: Unsatisfiable = PROVED Solved: Satisfiable = SATISFIABLE GaveUp: Fatal error Statistic: Loops = num_of_inst_loops: *([0-9]*) Statistic: Generated = num_of_clauses_in_db: *([0-9]*) Statistic: PropCalls = num_of_solver_calls: *([0-9]*) CASCDiv: FOF CNF FNT SAT EPR CASCProb: NoTransform/tptp Status: READY SSCPA TSTP SoTPTP CASC System: leanCoP Version: 2.0 URL: http://www.leancop.de/ Command: leancop.sh %s %d Format: leancop Transform: stdfof+add_equality SPCs: FOF Solved: Theorem = SZS status Theorem for Solved: CounterSatisfiable = SZS status CounterSatisfiable for GaveUp: dummy_never_found CASCDiv: FOF CASCProb: AddEq/leancop Status: READY SSCPA TSTP SoTPTP CASC System: ileanCoP Version: 1.2 URL: http://www.leancop.de/ileancop Command: leancop.sh %s %d Format: leancop Transform: stdfof+add_equality SPCs: FOF Solved: Theorem = SZS status Theorem for Solved: CounterSatisfiable = SZS status CounterSatisfiable for GaveUp: WHAT CASCDiv: FOF CASCProb: AddEq/leancop Status: READY System: Metis Version: 2.0 URL: http://www.gilith.com/software/metis Command: metis --show proof --show saturated %s Format: tptp Transform: none SPCs: FOF CNF Solved: Theorem = SZS status Theorem Solved: CounterSatisfiable = SZS status CounterSatisfiable Solved: Unsatisfiable = SZS status Unsatisfiable Solved: Satisfiable = SZS status Satisfiable GaveUp: SZS status Unknown StartSoln: CNFRefutation = SZS output start CNFRefutation EndSoln: CNFRefutation = SZS output end CNFRefutation CASCDiv: FOF CNF FNT SAT EPR UEQ CASCProb: NoTransform/tptp Status: READY SSCPA TSTP SoTPTP CASC System: Muscadet Version: 2.7 URL: http://www.math-info.univ-paris5.fr/~pastre/muscadet/muscadet.html Command: muscadet %s Format: tptp Transform: none SPCs: FOF Solved: Theorem = SZS status proved for GaveUp: SZS status no solution found for CASCDiv: FOF CASCProb: NoTransform/tptp Status: READY SSCPA TSTP SoTPTP CASC System: Otter Version: 3.3 URL: http://www.cs.unm.edu/~mccune/otter/ Command: otter-script %s Format: otter ForCASC: ,set(build_proof_object_2) Transform: add_equality:r SPCs: FOF CNF Solved: Unsatisfiable = ---------------- PROOF ---------------- GaveUp: PROOF NOT FOUND StartSoln: Refutation = ---------------- PROOF ---------------- EndSoln: Refutation = ------------ end of proof ------------- Statistic: Given = clauses given *([0-9]*) Statistic: Generated = clauses generated *([0-9]*) Statistic: Kept = clauses kept *([0-9]*) CASCDiv: FOF CNF UEQ CASCProb: AddEq_r/otter_auto Status: READY SSCPA TSTP SoTPTP CASC System: Otter Version: 3.3-SoS URL: http://www.cs.unm.edu/~mccune/otter/ Command: otter-script %s Format: otter:hypothesis:set(binary_res),set(para_into),set(para_from),set(para_from_vars),clear(print_given) Transform: add_equality:r Solved: Unsatisfiable = ---------------- PROOF ---------------- GaveUp: PROOF NOT FOUND StartSoln: Refutation = ---------------- PROOF ---------------- EndSoln: Refutation = ------------ end of proof ------------- Status: System: Otter Version: 3.3-A URL: http://www.cs.unm.edu/~mccune/otter/ Command: otter-script %s Format: otter Transform: fofify+add_equality:r SPCs: FOF CNF Solved: Unsatisfiable = ---------------- PROOF ---------------- GaveUp: PROOF NOT FOUND StartSoln: Refutation = ---------------- PROOF ---------------- EndSoln: Refutation = ------------ end of proof ------------- Status: Comment: For AGInT System: Paradox Version: 1.3 URL: http://www.cs.chalmers.se/~koen/folkung/ Command: paradox --print Model %s Format: oldtptp Transform: none SPCs: FOF_NKT FOF_NKU_NUN CNF_NKU Solved: Unsatisfiable = CONTRADICTION Solved: Satisfiable = == Model ====== GaveUp: INCONCLUSIVE StartSoln: FiniteModel = == Model ============== EndSoln: FiniteModel = == Result ============= Statistic: Size = SATISFIABLE .size = (\d*) CASCDiv: SAT CASCProb: NoTransform/oldtptp Status: READY CASC System: Paradox Version: 2.2 URL: http://www.cs.chalmers.se/~koen/folkung/ Command: paradox --tstp --model %s Format: tptp Transform: none SPCs: FOF_NKT FOF_NKU_NUN CNF_NKU Solved: Theorem = SZS status Theorem for Solved: CounterSatisfiable = SZS status CounterSatisfiable for Solved: Unsatisfiable = SZS status Unsatisfiable for Solved: Satisfiable = SZS status Satisfiable for GaveUp: RESULT: Unknown StartSoln: FiniteModel = SZS output start FiniteModel for EndSoln: FiniteModel = SZS output end FiniteModel for Statistic: Size = domain size\s*([0-9]*) CASCDiv: FNT SAT EPR CASCProb: NoTransform/tptp Status: READY SSCPA TSTP SoTPTP CASC System: Vampire Version: 8.1 URL: http://www.vampire.fm Command: vampire --mode casc -t %d %s Format: tptp:short Transform: none SPCs: FOF CNF Solved: Unsatisfiable = --- PROVED --- Solved: Satisfiable = --- UNPROVABLE --- GaveUp: --- CANNOT PROVE --- StartSoln: Refutation = === Refutation === EndSoln: Refutation = ==== End of refutation === CASCDiv: FOF CNF CASCProb: NoTransform/tptp Status: READY CASC System: Vampire Version: 9.0 URL: http://www.vampire.fm Command: vampire -t %d %s Format: tptp:short Transform: none SPCs: FOF CNF Solved: Theorem = --- PROVED --- Solved: CounterSatisfiable = --- UNPROVABLE --- Solved: Unsatisfiable = --- PROVED --- Solved: Satisfiable = --- UNPROVABLE --- GaveUp: --- CANNOT PROVE --- StartSoln: Refutation = === Refutation === EndSoln: Refutation = ==== End of refutation === CASCDiv: FOF CNF EPR UEQ CASCProb: NoTransform/tptp Status: READY SSCPA TSTP SoTPTP CASC System: Waldmeister Version: 806 URL: http://www.waldmeister.org/ Command: WaldmeisterII.comp %s Format: waldmeister Transform: none SPCs: CNF_UEQ Solved: Unsatisfiable = Goal proved Solved: Satisfiable = System completed GaveUp: Unfair completion run out of critical pairs StartSoln: Refutation = START OF PROOF EndSoln: Refutation = END OF PROOF CASCDiv: UEQ CASCProb: NoTransform/waldmeister Status: READY SSCPA TSTP SoTPTP CASC