System:    Bliksem
Version:   1.10
URL:       http://www.mpi-sb.mpg.de/~bliksem/
Command:   bliksem %s
Format:    bliksem
Transform: rm_equality:rstfp
Theorem:   found a proof
NonThm:    found a saturation
NoSoln:    Bliksem never gives up
CASC-17:   MIX UEQ SAT FOF SEM
Problems:  RmEq_rstfp/bliksem
Status:    READY SSCPA

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

System:    E-SETHEO
Version:   2000csp
URL:       http://www8.informatik.tu-muenchen.de/~setheo/
Command:   run-e-setheo %s %d
Format:    tptp
Transform: none
Theorem:   SUCCESS (proof
NonThm:    UnsoundForSAT SUCCESS (model
NoSoln:    FAIL (resources
CASC-17:   MIX UEQ FOF SEM
Problems:  NoTransform/tptp
Status:    READY SSCPA

System:    Gandalf
Version:   c-2.1
URL:       
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
CASC-17:   MIX UEQ
Problems:  RmEq_stfp/otter_auto
Status:    READY SSCPA

System:    GandalfFOF
Version:   1.0
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
CASC-17:   FOF SEM
Problems:  RmEq_stfp/otter_auto
Status:    READY SSCPA

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
CASC-17:   SAT
Problems:  RmEq_stfp/otter_auto
Status:    READY SSCPA

System:    MACE
Version:   1.4b
URL:       http://www.mcs.anl.gov/home/mccune/ar/mace
Command:   mace-casc %s
Format:    otter:none:set(auto),clear(print_given)
Transform: rm_equality:stfp
Theorem:   dummy_never_found
NonThm:    The set is satisfiable
NoSoln:    No models were found
CASC-17:   SAT
Problems:  RmEq_stfp/otter_auto
Status:    READY SSCPA

System:    MUSCADET
Version:   2.2
URL:       
Command:   muscadet.o %s
Format:    tptp
Transform: rm_equality:rstfp
Theorem:   proved
NonThm:    dummy_never_found
NoSoln:    no solution found
CASC-17:   FOF SEM
Problems:  RmEq_rstfp/tptp
Status:    READY

System:    Otter
Version:   3.1b
URL:       http://www.mcs.anl.gov/home/mccune/ar/otter
Command:   otter-casc %s
Format:    otter:none:set(auto),clear(print_given)
Transform: rm_equality:stfp
Theorem:   Otter has proved the theorem
NonThm:    dummy_never_found
NoSoln:    Otter has failed to prove the conjecture
CASC-17:   MIX UEQ FOF SEM
Problems:  RmEq_stfp/otter_auto
Status:    READY SSCPA

System:    OtterMACE
Version:   437
URL:       
Command:   otter-mace %s %d
Format:    otter:none:set(auto),clear(print_given)
Transform: rm_equality:stfp
Theorem:   PROOF
NonThm:    MODEL
NoSoln:    dummy_never_found
CASC-17:   SAT
Problems:  RmEq_stfp/otter_auto
Status:    READY SSCPA

System:    SCOTT
Version:   5.0.0
URL:       
Command:   scott_shell %d %s
Format:    scott:hypothesis:conjecture:none
Transform: rm_equality:stfp
Theorem:   ----- PROOF -----
NonThm:    dummy_never_found
NoSoln:    Search stopped because sos empty
CASC-17:   MIX UEQ FOF SEM
Problems:  RmEq_stfp/scott
Status:    READY SSCPA

System:    SCOTTSat
Version:   5.0.0
URL:       
Command:   scott_sat_shell %d %s
Format:    scott:hypothesis:conjecture:none
Transform: rm_equality:stfp
Theorem:   ----- PROOF -----
NonThm:    Great SCOTT: Model checks out
NoSoln:    Search stopped because sos empty
CASC-17:   SAT
Problems:  RmEq_stfp/scott
Status:    READY SSCPA

System:    SPASS
Version:   1.00T
URL:       http://spass.mpi-sb.mpg.de/
Format:    dfg
Transform: rm_equality:rstfp
Command:   SPASS -DocProof %s
Theorem:   Proof found
NonThm:    Completion found
NoSoln:    Ran out of time
CASC-17:   FOF
Problems:  RmEq_rstfp/dfg
Status:    READY

System:    Vampire
Version:   0.0
URL:       http://www.cs.man.ac.uk/~riazanoa/Vampire/
Command:   vampire -time_limit %d -output_proof %s
Format:    tptp
Transform: cnf:otter+rm_equality:rstfp
Theorem:   Proof found. Thanks to Tanya!
NonThm:    Unprovable.
NoSoln:    Proof not found.
CASC-17:   MIX
Problems:  RmEq_rstfp/tptp
Status:    READY

System:    Vampire
Version:   1.0
URL:       http://www.cs.man.ac.uk/~riazanoa/Vampire/
Command:   monstr %d 128000 %s
Format:    tptp
Transform: rm_equality:rstfp
Theorem:   Proof found
NonThm:    dummy_never_found
NoSoln:    dummy_never_found
CASC-17:   MIX UEQ
Problems:  RmEq_rstfp/tptp
Status:    READY SSCPA

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
CASC-17:   FOF SEM
Problems:  RmEq_rstfp/dfg
Status:    READY SSCPA

System:    Waldmeister
Version:   799
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.
CASC-17:   UEQ
Problems:  RmEq_rstfp/waldmeister
Status:    READY

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
CASC-17:   UEQ
Problems:  RmEq_rstfp/waldmeister
Status:    READY SSCPA