System:    Bliksem
Version:   1.12a
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:    found a saturation!
StartSoln: START OF PROOF
EndSoln:   END OF PROOF
CASCDiv:   MIX UEQ FOF
CASCProb:  RmEq_rstfp/bliksem
Status:    READY

System:    CiME
Version:   2
URL:       http://cime.lri.fr/
Command:   cime-wrapper %s
Format:    tptp
Transform: none
Theorem:   is_unsatisfiable : bool = true
NonThm:    Never find this now is_unsatisfiable : bool = false
NoSoln:    dummy_never_found
CASCDiv:   UEQ
CASCProb:  RmEq_rstfp/tptp
Status:    READY

System:    DCTP
Version:   1.2
URL:       http://wwwjessen.informatik.tu-muenchen.de/~stenzg/dctp.html
Command:   dctp-wrapper -negpref -complexity -alternate -resisol -fullrewrite %s
Format:    tptp
Transform: rm_equality:rstfp
Theorem:   PROOF
NonThm:    MODEL
NoSoln:    ERROR
CASCDiv:   MIX
CASCProb:  RmEq_rstfp/tptp
Status:    READY

System:    DCTP
Version:   1.2-SAT
URL:       http://wwwjessen.informatik.tu-muenchen.de/~stenzg/dctp.html
Command:   dctp-wrapper -alternate -resisol -fullrewrite %s
Format:    tptp
Transform: rm_equality:rstfp
Theorem:   PROOF
NonThm:    MODEL
NoSoln:    ERROR
CASCDiv:   SAT
CASCProb:  RmEq_rstfp/tptp
Status:    READY

System:    DCTP
Version:   1.2-EPR
URL:       http://wwwjessen.informatik.tu-muenchen.de/~stenzg/dctp.html
Command:   dctp-wrapper -negpref -oweight 2 -cweight 2 -alternate -resisol -fullrewrite %s
Format:    tptp
Transform: rm_equality:rstfp
Theorem:   PROOF
NonThm:    MODEL
NoSoln:    ERROR
CASCDiv:   EPR
CASCProb:  RmEq_rstfp/tptp
Status:    READY

System:    DCTP
Version:   10.1p
URL:       http://wwwjessen.informatik.tu-muenchen.de/~stenzg/dctp.html
Command:   bin/dctp-10.1p %s %d
Format:    tptp
Transform: rm_equality:rstfp
Theorem:   PROOF
NonThm:    MODEL
NoSoln:    ERROR
CASCDiv:   MIX FOF EPR
CASCProb:  RmEq_rstfp/tptp
Status:    READY

System:    DCTP
Version:   10.1p-SAT
URL:       http://wwwjessen.informatik.tu-muenchen.de/~stenzg/dctp.html
Command:   bin/dctp-10.1p-sat %s %d
Format:    tptp
Transform: rm_equality:rstfp
Theorem:   PROOF
NonThm:    MODEL
NoSoln:    ERROR
CASCDiv:   SAT
CASCProb:  RmEq_rstfp/tptp
Status:    READY

System:    E
Version:   0.7
URL:       http://wwwjessen.informatik.tu-muenchen.de/~schulz/WORK/eprover.html
Command:   eprover -s -xAuto -tAuto --memory-limit=384 --tptp-in --cpu-limit=%d %s
Format:    tptp
Transform: rm_equality:rstfp
Theorem:   Proof found!
NonThm:    No proof found!
NoSoln:    Failure:
CASCDiv:   MIX UEQ
CASCProb:  RmEq_rstfp/tptp
Status:    READY

System:    EP
Version:   0.7
URL:       http://wwwjessen.informatik.tu-muenchen.de/~schulz/WORK/eprover.html
Command:   eproof -xAuto -tAuto --memory-limit=384 --tptp-in --cpu-limit=%d %s
Format:    tptp
Transform: rm_equality:rstfp
Theorem:   "proof"
NonThm:    "final"
NoSoln:    Cannot determine problem status within resource limit
StartSoln: Proof status evidence starts here
EndSoln:   Proof status evidence ends here
CASCDiv:   MIX
CASCProb:  RmEq_rstfp/tptp
Status:    READY

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

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

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

System:    Gandalf
Version:   c-2.5-PROOF
URL:       http://www.cs.chalmers.se/~tammet/gandalf/
Command:   gandalf-wrapper -proof %s %d
Format:    otter:hypothesis:set(auto),clear(print_given),set(tptp_eq)
Transform: rm_equality:stfp
Theorem:   EMPTY 
NonThm:    SATISFIABLE
NoSoln:    time limit exhausted: proof search terminated
StartSoln: START OF PROOF
EndSoln:   END OF PROOF
CASCDiv:   MIX
CASCProb:  RmEq_stfp/otter_auto
Status:    READY

System:    Gandalf
Version:   c-2.5-SAT
URL:       http://www.cs.chalmers.se/~tammet/gandalf/
Command:   gandalf-wrapper -sat %s %d
Format:    otter:hypothesis:set(auto),clear(print_given),set(tptp_eq)
Transform: rm_equality:stfp
Theorem:   EMPTY 
NonThm:    SATISFIABLE
NoSoln:    time limit exhausted: proof search terminated
CASCDiv:   SAT EPR
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:    GrAnDe
Version:   1.1
URL:       http://www.cs.miami.edu/~tptp/ATPSystems/GrAnDe/
Command:   And %s %d
Format:    tptp
Transform: none
Theorem:   Instance unsatisfiable
NonThm:    Instance satisfiable
NoSoln:    Not enough time to decide
CASCDiv:   EPR
CASCProb:  NoTransform/tptp
Status:    READY

System:    ICGNS
Version:   2002b
URL:       http://www.mcs.anl.gov/~mccune/icgns
Command:   icgns-for-tptp %s
Format:    otter:hypothesis:set(auto),clear(print_given)
Transform: rm_equality:stfp
Theorem:   dummy_never_found
NonThm:    SATISFIABLE
NoSoln:    FAILURE
StartSoln: Model 1
EndSoln:   end of model
CASCDiv:   SAT
CASCProb:  RmEq_stfp/otter_auto
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)
ForCASC:   ,set(build_proof_object_2)
Transform: rm_equality:stfp
Theorem:   ---------------- PROOF ----------------
NonThm:    dummy_never_found
NoSoln:    PROOF NOT FOUND
StartSoln: ---------------- PROOF ----------------
EndSoln:   ------------ end of proof -------------
CASCDiv:   MIX UEQ FOF
CASCProb:  RmEq_stfp/otter_auto
Status:    READY

System:    SCOTT
Version:   6.1
URL:       http://discus.anu.edu.au/software/scott/
Command:   scott-wrapper %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 -------------
CASCDiv:   MIX UEQ SAT FOF EPR
CASCProb:  RmEq_stfp/scott
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
Theorem:   Proof found. Thanks to Tanya!
NonThm:    Unprovable
NoSoln:    I would definitely solve this problem if I had one more second
StartSoln: ====== Proof: ======
EndSoln:   =====  End of proof. ====
CASCDiv:   MIX UEQ FOF EPR
CASCProb:  RmEq_rstfp/tptp
Status:    READY

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

System:    Vampire
Version:   2.0-CASC
URL:       http://www.cs.man.ac.uk/~riazanoa/Vampire/
Command:   vampire-CASC %d %s
Format:    tptp
Transform: rm_equality:rstfp
Theorem:   Proof found
NonThm:    dummy_never_found
NoSoln:    Proof not found
StartSoln: ======================== Proof: =========================
EndSoln:   ==================  End of proof. ========================
CASCDiv:   MIX
CASCProb:  RmEq_rstfp/tptp
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
StartSoln: P R O O F   P R O T O C O L
EndSoln:   Waldmeister states: Goal proved
CASCDiv:   UEQ
CASCProb:  RmEq_rstfp/waldmeister
Status:    READY

System:    Waldmeister
Version:   702
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
StartSoln: P R O O F   P R O T O C O L
EndSoln:   Waldmeister states: Goal proved
CASCDiv:   UEQ
CASCProb:  RmEq_rstfp/waldmeister
Status:    READY