System:    Darwin
Version:   CASC-J2
URL:       http://www.mpi-sb.mpg.de/~baumgart/DARWIN/
Command:   darwin -v 2 %s 
Format:    protein
Transform: none
Solved:    Unsatisfiable = REFUTATION FOUND
Solved:    Satisfiable = SATISFIABLE
GaveUp:    NO SOLUTION
StartSoln: Model = START OF CONTEXT
EndSoln:   Model = END OF CONTEXT
CASCDiv:   MIX SAT EPR
CASCProb:  NoTransform/protein
Status:    READY

System:    DCTP
Version:   1.31
URL:       http://www.mpi-sb.mpg.de/~stenz/dctp-sb.html
Command:   dctp-wrapper -negpref -complexity -fullrewrite -alternate -resisol %s
Format:    tptp
Transform: rm_equality:rstfp
Solved:    Unsatisfiable = PROOF found
Solved:    Satisfiable = MODEL found
GaveUp:    ERROR
CASCDiv:   MIX
CASCProb:  RmEq_rstfp/tptp
Status:    READY

System:    DCTP
Version:   1.31-SAT
URL:       http://www.mpi-sb.mpg.de/~stenz/dctp-sb.html
Command:   dctp-wrapper -negpref -complexity -fullrewrite -alternate -resisol -global -minselect -split %s
Format:    tptp
Transform: rm_equality:rstfp
Solved:    Unsatisfiable = PROOF found
Solved:    Satisfiable = MODEL found
GaveUp:    ERROR
CASCDiv:   SAT
CASCProb:  RmEq_rstfp/tptp
Status:    READY

System:    DCTP
Version:   1.31-EPR
URL:       http://www.mpi-sb.mpg.de/~stenz/dctp-sb.html
Command:   dctp-wrapper -global -pospref -fullrewrite -alternate -resisol %s
Format:    tptp
Transform: rm_equality:rstfp
Solved:    Unsatisfiable = PROOF found
Solved:    Satisfiable = MODEL found
GaveUp:    ERROR
CASCDiv:   EPR
CASCProb:  RmEq_rstfp/tptp
Status:    READY

System:    DCTP
Version:   1.3-EPR
URL:       http://www.mpi-sb.mpg.de/~stenz/dctp-sb.html
Command:   dctp-wrapper -global -pospref -fullrewrite -alternate -resisol %s
Format:    tptp
Transform: rm_equality:rstfp
Solved:    Unsatisfiable = PROOF found
Solved:    Satisfiable = MODEL found
GaveUp:    ERROR
CASCDiv:   EPR
CASCProb:  RmEq_rstfp/tptp
Status:    READY

System:    DCTP
Version:   10.21p
URL:       http://www.mpi-sb.mpg.de/~stenz/dctp-sb.html
Command:   bin/dctp-10.21p %s %d
Format:    tptp
Transform: none
Solved:    Unsatisfiable = PROOF found
Solved:    Satisfiable = MODEL found
GaveUp:    ERROR
CASCDiv:   MIX FOF EPR
CASCProb:  NoTransform/tptp
Status:    READY

System:    DCTP
Version:   10.21p-SAT
URL:       http://www.mpi-sb.mpg.de/~stenz/dctp-sb.html
Command:   bin/dctp-10.21p-sat %s %d
Format:    tptp
Transform: none
Solved:    Unsatisfiable = PROOF found
Solved:    Satisfiable = MODEL found
GaveUp:    ERROR
CASCDiv:   SAT
CASCProb:  NoTransform/tptp
Status:    READY

System:    E
Version:   0.82
URL:       http://www.eprover.org/
Command:   eprover -s --print-statistics -xAuto -tAuto --memory-limit=384 --tptp-in %s
Format:    tptp
Transform: rm_equality:rstfp
Solved:    Unsatisfiable = TSTP exit status: Unsatisfiable
Solved:    Satisfiable = TSTP exit status: Satisfiable
GaveUp:    Failure:
CASCDiv:   MIX FOF UEQ
CASCProb:  RmEq_rstfp/tptp
Status:    READY

System:    EP
Version:   0.82
URL:       http://www.eprover.org/
Command:   eproof --print-statistics -xAuto -tAuto --memory-limit=384 --tptp-in --tstp-out %s
Format:    tptp
Transform: rm_equality:rstfp
Solved:    Unsatisfiable = TSTP exit status: Unsatisfiable
Solved:    Satisfiable = TSTP exit status: Satisfiable
GaveUp:    Failure:
StartSoln: Refutation = Proof object starts here
EndSoln:   Refutation = Proof object ends here
StartSoln: Saturation = Saturation derivation starts here
EndSoln:   Saturation = Saturation derivation ends here
CASCDiv:   MIX FOF
CASCProb:  RmEq_rstfp/tptp
Status:    READY

System:    E-SETHEO
Version:   csp04
URL:       http://www4.informatik.tu-muenchen.de/~schulz/WORK/e-setheo.html
Command:   bin/run-e-setheo %s %d
Format:    tptp
Transform: none
Solved:    Unsatisfiable = SUCCESS (proof
Solved:    Satisfiable = SUCCESS (model
GaveUp:    FAIL (resources
CASCDiv:   MIX FOF EPR UEQ
CASCProb:  NoTransform/tptp
Status:    READY

System:    E-SETHEO
Version:   csp04-SAT
URL:       http://www4.informatik.tu-muenchen.de/~schulz/WORK/e-setheo.html
Command:   bin/run-e-setheo-sat %s %d
Format:    tptp
Transform: none
Solved:    Unsatisfiable = SUCCESS (proof
Solved:    Satisfiable = SUCCESS (model
GaveUp:    FAIL (resources
CASCDiv:   SAT
CASCProb:  NoTransform/tptp
Status:    READY

System:    Gandalf
Version:   c-2.6-SAT
URL:       http://www.ttu.ee/it/gandalf/
Command:   gandalf-wrapper -time %d -sat %s
Format:    otter:hypothesis:set(auto),clear(print_given)
Transform: rm_equality:stfp
Solved:    Unsatisfiable = GANDALF_FOUND_A_REFUTATION
Solved:    Satisfiable = SATISFIABLE
GaveUp:    dummy_never_found
StartSoln: Model = MODEL STARTS
EndSoln:   Model = MODEL ENDS
CASCDiv:   SAT
CASCProb:  RmEq_stfp/otter_auto
Status:    READY

System:    Mace2
Version:   2.2
URL:       http://www.mcs.anl.gov/home/mccune/ar/mace
Command:   mace-script %s
Format:    otter:hypothesis:set(auto),clear(print_given)
Transform: rm_equality:stfp
Solved:    Satisfiable = MODEL FOUND
GaveUp:    MODEL NOT FOUND
StartSoln: Model = === Model
EndSoln:   Model = end_of_model
CASCDiv:   SAT
CASCProb:  RmEq_stfp/otter_auto
Status:    READY

System:    Mace4
Version:   2004-D
URL:       http://www-unix.mcs.anl.gov/AR/mace4/
Command:   mace-script %s
Format:    mace4
Transform: rm_equality:rstfp
Solved:    Satisfiable = Model 1
GaveUp:    MODEL NOT FOUND
StartSoln: Model = -------- Model 1
EndSoln:   Model = -------- end of model --------
CASCDiv:   SAT
CASCProb:  RmEq_rstfp/mace4
Status:    READY

System:    Otter
Version:   3.3
URL:       http://www.mcs.anl.gov/home/mccune/ar/otter
Command:   otter-script %s
Format:    otter:hypothesis:set(auto),clear(print_given)
ForCASC:   ,set(build_proof_object_2)
Transform: rm_equality:stfp
Solved:    Unsatisfiable = ---------------- PROOF ----------------
GaveUp:    Search stopped because sos empty
StartSoln: Refutation = ---------------- PROOF ----------------
EndSoln:   Refutation = ------------ end of proof -------------
CASCDiv:   MIX FOF UEQ
CASCProb:  RmEq_stfp/otter_auto
Status:    READY

System:    Paradox
Version:   1.0
URL:       http://www.cs.chalmers.se/~koen/paradox
Command:   paradox --print Model %s
Format:    tptp
Transform: rm_equality:rstfp
Solved:    Unsatisfiable = CONTRADICTION
Solved:    Satisfiable = == Model ======
GaveUp:    INCONCLUSIVE
StartSoln: Model = == Model ==============
EndSoln:   Model = == Result =============
CASCDiv:   SAT
CASCProb:  RmEq_rstfp/tptp
Status:    READY

System:    Paradox
Version:   1.1-casc
URL:       http://www.cs.chalmers.se/~koen/paradox
Command:   paradox --print Model %s
Format:    tptp
Transform: rm_equality:rstfp
Solved:    Unsatisfiable = CONTRADICTION
Solved:    Satisfiable = == Model ======
GaveUp:    INCONCLUSIVE
StartSoln: Model = == Model ==============
EndSoln:   Model = == Result =============
CASCDiv:   SAT EPR
CASCProb:  RmEq_rstfp/tptp
Status:    READY

System:    SOS
Version:   1.0
URL:       http://csl.anu.edu.au/~jks/software/sos.tar.gz
Command:   sos-script %s
Format:    otter:hypothesis:set(auto),clear(print_given)
Transform: rm_equality:stfp
Solved:    Unsatisfiable = PROOF
GaveUp:    Search stopped because sos empty
StartSoln: Refutation = ---------------- PROOF ----------------
EndSoln:   Refutation = ------------ end of proof -------------
CASCDiv:   MIX UEQ
CASCProb:  RmEq_stfp/otter_auto
Status:    READY

System:    THEO
Version:   J2004
URL:
Command:   theo %s -l r1 L1 tptp
NonCASCCommand:   theo %s -l L0 t%d tptp
Format:    tptp
Transform: none
Solved:    Unsatisfiable = Proof Found
NotLookingFor:    Satisfiable = THE RESULTS
StartSoln: Refutation = THE PROOF
EndSoln:   Refutation = END OF PROOF
CASCDiv:   MIX
CASCProb:  NoTransform/tptp
Status:    READY

System:    Vampire
Version:   5.0
URL:       http://www.cs.man.ac.uk/~riazanoa/Vampire/
Command:   vampire -t %d --casc on %s
Format:    tptp
Transform: rm_equality:rstfp
Solved:    Unsatisfiable = Proof found. Thanks to Tanya!
Solved:    Satisfiable = Unprovable
GaveUp:    I would definitely solve this problem if I had one more second
StartSoln: Refutation = ====== Proof: ======
EndSoln:   Refutation = =====  End of proof. ====
CASCDiv:   FOF
CASCProb:  RmEq_rstfp/tptp
Status:    READY

System:    Vampire
Version:   6.0
URL:       http://www.cs.man.ac.uk/~riazanoa/Vampire/
Command:   vampire --mode casc-19 -t %d %s
Format:    tptp
Transform: rm_equality:rstfp
Solved:    Unsatisfiable = --- PROVED ---
Solved:    Satisfiable = --- UNPROVABLE ---
GaveUp:    --- CANNOT PROVE ---
StartSoln: Refutation = === Refutation ===
EndSoln:   Refutation = ==== End of refutation ===
CASCDiv:   MIX
CASCProb:  RmEq_rstfp/tptp
Status:    READY

System:    Vampire
Version:   7.0
URL:       http://www.cs.man.ac.uk/~riazanoa/Vampire/
Command:   vampire --mode casc-j2 -t %d %s
Format:    tptp
Transform: rm_equality:rstfp
Solved:    Unsatisfiable = --- PROVED ---
Solved:    Satisfiable = --- UNPROVABLE ---
GaveUp:    --- CANNOT PROVE ---
StartSoln: Refutation = === Refutation ===
EndSoln:   Refutation = ==== End of refutation ===
CASCDiv:   MIX FOF EPR UEQ
CASCProb:  RmEq_rstfp/tptp
Status:    READY

System:    Waldmeister
Version:   702
URL:       http://www.mpi-sb.mpg.de/~hillen/waldmeister/
Command:   WaldmeisterII.comp %s
Format:    waldmeister
Transform: rm_equality:rstfp
Solved:    Unsatisfiable = Goal proved
Solved:    Satisfiable = System completed
GaveUp:    Unfair completion run out of critical pairs
StartSoln: Refutation = P R O O F   P R O T O C O L
EndSoln:   Refutation = Waldmeister states: Goal proved
CASCDiv:   UEQ
CASCProb:  RmEq_rstfp/waldmeister
Status:    READY

System:    Waldmeister
Version:   704
URL:       http://www.waldmeister.org/
Command:   WaldmeisterII.comp %s
Format:    waldmeister
Transform: rm_equality:rstfp
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:  RmEq_rstfp/waldmeister
Status:    READY