System:    Bliksem
Version:   1.12
URL:       http://www.mpi-sb.mpg.de/~bliksem/
Command:   bliksem %s
Format:    bliksem
Transform: rm_equality:rstfp
Theorem:   found a proof
NonThm:    dummy_never_found
NoSoln:    dummy_never_found
StartSoln: Total Proof:
EndSoln:   Proof check complete!
Statistic: Terms = space for terms: *([0-9]*)
Statistic: Clauses = space for clauses: *([0-9]*)
Statistic: Generated = clauses generated: *([0-9]*)
Statistic: Kept = clauses kept: *([0-9]*)
CASCDiv:   MIX UEQ FOF
CASCProb:  RmEq_rstfp/bliksem
Status:    READY SSCPA

System:    DCTP
Version:   0.1
URL:       http://wwwjessen.informatik.tu-muenchen.de/~stenzg/dctp.html
Command:   dctp %s
Format:    tptp
Transform: none
Theorem:   PROOF
NonThm:    MODEL
NoSoln:    ERROR
Statistic: Linkings = Linking steps performed: *([0-9]*)
Statistic: ClausesInTableau = Clauses in tableau: *([0-9]*)
CASCDiv:   MIX SAT EPR
CASCProb:  NoTransform/tptp
Status:    READY

System:    E
Version:   0.62
URL:       http://wwwjessen.informatik.tu-muenchen.de/~schulz/WORK/eprover.html
Command:   eprover -xAuto -tAuto -s --tptp-in --memory-limit=192 %s
Format:    tptp
Transform: rm_equality:rstfp
Theorem:   Proof found!
NonThm:    No proof found!
NoSoln:    Failure:
Statistic: Clauses = Generated clauses *: *([0-9]*)
Statistic: NonTrivial = the previous two non-trivial *: *([0-9]*)
Statistic: Processed = Processed clauses *: *([0-9]*)
CASCDiv:   MIX UEQ EPR
CASCProb:  RmEq_rstfp/tptp
Status:    READY

System:    EP
Version:   0.62
URL:       http://wwwjessen.informatik.tu-muenchen.de/~schulz/WORK/eprover.html
Command:   eproof -xAuto -tAuto --tptp-in --memory-limit=108 --cpu-limit=%d %s
Format:    tptp
Transform: rm_equality:rstfp
Theorem:   {proof}
NonThm:    {final}
NoSoln:    dummy_never_found
StartSoln: Evidence for problem status starts
EndSoln:   Evidence for problem status ends
Statistic: Clauses = Generated clauses *: *([0-9]*)
Statistic: NonTrivial = the previous two non-trivial *: *([0-9]*)
Statistic: Processed = Processed clauses *: *([0-9]*)
CASCDiv:   MIX
CASCProb:  RmEq_rstfp/tptp
Status:    READY

System:    E
Version:   0.6
URL:       http://wwwjessen.informatik.tu-muenchen.de/~schulz/WORK/eprover.html
Command:   eprover -xAuto -tAuto -s --tptp-format -m 192 %s
CASCCommand:   eprover-wrapper %s
Format:    tptp
Transform: rm_equality:rstfp
Theorem:   Proof found!
NonThm:    No proof found!
NoSoln:    Failure:
CASCDiv:   MIX 
CASCProb:  RmEq_rstfp/tptp
Status:    READY

System:    E-SETHEO
Version:   csp01
URL:       http://www8.informatik.tu-muenchen.de/~setheo/
Command:   run-e-setheo %s %d
Format:    tptp
Transform: none
Theorem:   SUCCESS (proof
NonThm:    SUCCESS (model
NoSoln:    FAIL (resources
CASCDiv:   MIX SAT FOF EPR
CASCProb:  NoTransform/tptp
Status:    READY

System:    Gandalf
Version:   c-2.3
URL:       http://www.cs.chalmers.se/~tammet/gandalf/
Command:   gandalf-wrapper %s %d
Format:    otter:hypothesis:set(auto),clear(print_given)
Transform: rm_equality:stfp
Theorem:   EMPTY
NonThm:    SATISFIABLE
NoSoln:    time limit exhausted: proof search terminated
Statistic: Given = given clauses: *([0-9]*)
Statistic: Derived = derived clauses: *([0-9]*)
Statistic: Kept = kept clauses: *([0-9]*)
CASCDiv:   MIX UEQ EPR
CASCProb:  RmEq_stfp/otter_auto
Status:    READY

System:    GandalfFOF
Version:   c-2.3
URL:       
Command:   gandalf-wrapper -fof %s %d
Format:    otter:hypothesis:set(auto),clear(print_given)
Transform: rm_equality:stfp
Theorem:   EMPTY
NonThm:    SATISFIABLE
NoSoln:    time limit exhausted: proof search terminated
CASCDiv:   FOF
CASCProb:  RmEq_stfp/otter_auto
Status:    READY

System:    GandalfSat
Version:   1.1
URL:       http://www.cs.chalmers.se/~tammet/gandalf/
Command:   gandalf-wrapper -sat %s %d
Format:    otter:hypothesis:set(auto),clear(print_given)
Transform: rm_equality:stfp
Theorem:   EMPTY
NonThm:    SATISFIABLE
NoSoln:    time limit exhausted: proof search terminated
CASCDiv:   SAT
CASCProb:  RmEq_stfp/otter_auto
Status:    READY

System:    GandalfSat
Version:   1.0
URL:       
Command:   gandalf-wrapper -sat %s %d
Format:    otter:hypothesis:set(auto),clear(print_given)
Transform: rm_equality:stfp
Theorem:   EMPTY
NonThm:    SATISFIABLE
NoSoln:    time limit exhausted: proof search terminated
CASCDiv:   SAT
CASCProb:  RmEq_stfp/otter_auto
Status:    READY

System:    MACE
Version:   2.0
URL:       http://www.mcs.anl.gov/home/mccune/ar/mace
Command:   mace-script %s
Format:    otter:none:set(auto),clear(print_given),set(build_proof_object_2)
Transform: rm_equality:stfp
Theorem:   dummy_never_found
NonThm:    MODEL FOUND
NoSoln:    MODEL NOT FOUND
StartSoln: === Model
EndSoln:   end_of_model
CASCDiv:   SAT
CASCProb:  RmEq_stfp/otter_auto
Status:    READY

System:    MUSCADET
Version:   2.3
URL:       http://www.math-info.univ-paris5.fr/~pastre/muscadet/muscadet.html
Command:   muscadet %s
Format:    tptp
Transform: rm_equality:rstfp
Theorem:   proved
NonThm:    dummy_never_found
NoSoln:    no solution found
CASCDiv:   FOF
CASCProb:  RmEq_rstfp/tptp
Status:    READY

System:    Otter
Version:   3.2
URL:       http://www.mcs.anl.gov/home/mccune/ar/otter
Command:   otter-script %s
Format:    otter:none:set(auto),clear(print_given),set(build_proof_object_2)
Transform: rm_equality:stfp
Theorem:   PROOF FOUND
NonThm:    dummy_never_found
NoSoln:    PROOF NOT FOUND
StartSoln: BEGINNING OF PROOF OBJECT
EndSoln:   END OF PROOF OBJECT
CASCDiv:   MIX UEQ FOF
CASCProb:  RmEq_stfp/otter_auto
Status:    READY

System:    Otter-MACE
Version:   3.2-2.0
URL:       http://www.mcs.anl.gov/home/mccune/ar/otter
Command:   otter-mace-script %s %d
Format:    otter:none:set(auto),clear(print_given),set(build_proof_object_2)
Transform: rm_equality:stfp
Theorem:   SOLUTION FOUND (refutation)
NonThm:    SOLUTION FOUND (model)
NoSoln:    SOLUTION NOT FOUND
StartSoln: BEGINNING OF PROOF OBJECT
EndSoln:   END OF PROOF OBJECT
CASCDiv:   EPR
CASCProb:  RmEq_stfp/otter_auto
Status:    READY

System:    PizEAndSATO
Version:   0.2
URL:       
Command:   And %s
Format:    tptp
Transform: none
Theorem:   The clause set is unsatisfiable
NonThm:    The number of found models is
NoSoln:    The file is empty
Statistic: Models = The number of found models is *([0-9]*)
Statistic: Memory = mallocated .K bytes. *([0-9]*)
CASCDiv:   EPR
CASCProb:  NoTransform/tptp
Status:    READY

System:    SCOTT
Version:   6.0.0
URL:       http://discus.anu.edu.au/software/scott/
Command:   casc-script %d %s
Format:    scott:hypothesis:conjecture:none
Transform: rm_equality:stfp+stdfof
Theorem:   PROOF
NonThm:    Model checks out
NoSoln:    Search stopped because sos empty
StartSoln: ---------------- PROOF ----------------
EndSoln:   ------------ end of proof -------------
Statistic: Memory = Kbytes malloced *([0-9]*)
Statistic: Generated = clauses generated *([0-9]*)
Statistic: Kept = clauses kept *([0-9]*)
CASCDiv:   MIX UEQ SAT FOF EPR
CASCProb:  RmEq_stfp/scott
Status:    READY

System:    Vampire
Version:   2.0
URL:       http://www.cs.man.ac.uk/~riazanoa/Vampire/
Command:   vampire %d %s
Format:    tptp
Transform: rm_equality:rstfp
Theorem:   Proof found
NonThm:    Unprovable
NoSoln:    Proof not found
CASCDiv:   MIX UEQ
CASCProb:  RmEq_rstfp/tptp
Status:    READY

System:    VampireJC
Version:   2.0
URL:       http://www.cs.man.ac.uk/~riazanoa/Vampire/
Command:   vampireJC %d %s
Format:    tptp
Transform: rm_equality:rstfp
Theorem:   Proof found
NonThm:    dummy_never_found
NoSoln:    Proof not found
CASCDiv:   MIX
CASCProb:  RmEq_rstfp/tptp
Status:    READY

System:    VampireFOF
Version:   2.0
URL:       http://www.cs.man.ac.uk/~riazanoa/Vampire/
Command:   vampireFOF %d %s
Format:    tptp
Transform: rm_equality:rstfp
Theorem:   Proof found
NonThm:    Unprovable
NoSoln:    Proof not found
CASCDiv:   FOF
CASCProb:  RmEq_rstfp/tptp
Status:    READY

System:    VampireEPR
Version:   2.0
URL:       http://www.cs.man.ac.uk/~riazanoa/Vampire/
Command:   vampireEPR %d %s
Format:    tptp
Transform: rm_equality:rstfp
Theorem:   Proof found
NonThm:    Unprovable
NoSoln:    Proof not found
CASCDiv:   EPR
CASCProb:  RmEq_rstfp/tptp
Status:    READY

System:    VampireFOF
Version:   1.0
URL:       http://www.cs.man.ac.uk/~riazanoa/Vampire/
Command:   monstrFOF %d 128000 %s
Format:    dfg
Transform: rm_equality:rstfp
Theorem:   Proof found
NonThm:    dummy_never_found
NoSoln:    dummy_never_found
CASCDiv:   FOF
CASCProb:  RmEq_rstfp/dfg
Status:    READY

System:    Waldmeister
Version:   601
URL:       http://www-avenhaus.informatik.uni-kl.de/waldmeister
Command:   WaldmeisterII.comp %s
Format:    waldmeister
Transform: rm_equality:rstfp
Theorem:   Goal proved
NonThm:    System completed
NoSoln:    Unfair completion run out of critical pairs
CASCDiv:   UEQ
CASCProb:  RmEq_rstfp/waldmeister
Status:    READY SSCPA

System:    Waldmeister
Version:   600
URL:       http://www-avenhaus.informatik.uni-kl.de/waldmeister
Command:   WaldmeisterII.comp %s
Format:    waldmeister
Transform: rm_equality:rstfp
Theorem:   Goal proved
NonThm:    System completed
NoSoln:    Unfair completion run out of critical pairs
CASCDiv:   UEQ
CASCProb:  RmEq_rstfp/waldmeister
Status:    READY