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

System:    E
Version:   0.5
URL:       http://wwwjessen.informatik.tu-muenchen.de/~schulz/WORK/eprover.html
Command:   eprover --tptp-in -s -xAuto --memory-limit=320 %s
Format:    tptp
Transform: rm_equality:rstfp
Theorem:   Proof found!
NonThm:    No proof found!
NoSoln:    Failure:
CASC-16:   MIX UEQ
Problems:  RmEq_rstfp/tptp
Status:    CASC READY

System:    E-SETHEO
Version:   99csp
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
CASC-16:   MIX UEQ SAT FOF
Problems:  NoTransform/tptp
Status:    READY

System:    FDP
Version:   0.9
URL:       http://www.uni-koblenz.de/~peter/FDP/
Command:   fdp-casc %s %d
Format:    protein
Transform: none
Theorem:   REFUTATION FOUND
NonThm:    SATISFIABLE
NoSoln:    UNKNOWN
CASC-16:   MIX SAT
Problems:  NoTransform/protein
Status:    CASC READY

System:    Fiesta
Version:   2
URL:
Command:   fiesta-wrapper %s
Format:    dedam
Transform: rm_equality:rstfp
Theorem:   Theorem Proved
NonThm:    satisfiable
NoSoln:    give up
CASC-16:   UEQ
Problems:  RmEq_rstfp/dedam
Status:    CASC READY RECOMPILE

System:    Gandalf
Version:   c-1.8c
URL:       http://www.cs.chalmers.se/~tammet/gandalf/
Command:   gandalf-wrapper %s %d
Format:    otter:hypothesis:assign(max_seconds,300),set(auto2),set(tptp_eq),clear(print_given)
Transform: rm_equality:stfp
Theorem:   EMPTY CLAUSE
NonThm:    dummy_never_found
NoSoln:    dummy_never_found
CASC-16:   MIX
Problems:  RmEq_stfp/otter_auto
Status:    CASC READY SSCPA

System:    Gandalf
Version:   c-2.0
URL:       http://www.cs.chalmers.se/~tammet/gandalf/
Command:   gandalf2 %s %d
Format:    otter:hypothesis:assign(max_seconds,300),set(auto2),set(tptp_eq),clear(print_given)
Transform: rm_equality:stfp
Theorem:   EMPTY CLAUSE
NonThm:    dummy_never_found
NoSoln:    dummy_never_found
CASC-16:   MIX UEQ
Problems:  RmEq_stfp/otter_auto
Status:    CASC READY

System:    HOTTER
Version:   0.0
URL:
Command:   hotter %s
Format:    otter:hypothesis:set(auto2),set(tptp_eq),clear(print_given)
Transform: rm_equality:stfp
Theorem:   unsatisfiable
NonThm:    have models
NoSoln:    failed to find a proof
CASC-16:   MIX
Problems:  RmEq_stfp/otter_auto
Status:    CASC UNSOUND

System:    MHOTTER
Version:   0.0
URL:
Command:   mhotter %s
Format:    otter:hypothesis:set(auto2),set(tptp_eq),clear(print_given)
Transform: rm_equality:stfp
Theorem:   failed to find a model
NonThm:    have models
NoSoln:    dummy_never_found
CASC-16:   SAT
Problems:  RmEq_stfp/otter_auto
Status:    CASC UNSOUND

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

System:    OtterMACE
Version:   437
URL:
Command:   otter-mace %s %d
Format:    otter:hypothesis:assign(max_seconds,300),set(auto2),set(tptp_eq),clear(print_given)
Transform: rm_equality:stfp
Theorem:   PROOF
NonThm:    MODEL
NoSoln:    dummy_never_found
CASC-16:   MIX UEQ SAT FOF
Problems:  RmEq_stfp/otter_auto
Status:    CASC READY SSCPA

System:    SCOTT
Version:   4.6.4
URL:
Command:   casc_shell %s
Format:    'finder:all:special_equality:time_limit(1):5'
Transform: none
Format2:   scott:hypothesis:conjecture:none
Transform2: rm_equality:stfp
Theorem:   That finishes the proof
NonThm:    Model checks out
NoSoln:    sos empty
CASC-16:   MIX UEQ
Problems:  RmEq_stfp/scott
Status:    CASC READY

System:    SPASS
Version:   0.95T
URL:       http://spass.mpi-sb.mpg.de/
Format:    dfg
Transform: rm_equality:rstfp
Command:   SPASS -PGiven=0 -PProblem=0 -TimeLimit=%d %s
Theorem:   Proof found
NonThm:    Completion found
NoSoln:    Ran out of time
CASC-16:   SAT FOF
Problems:  RmEq_rstfp/dfg
Status:    CASC READY

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

System:    Vampire
Version:   0.0
URL:
Command:   vampire -time_limit %d -output_proof %s
Format:    tptp
Transform: rm_equality:rstfp
Theorem:   Proof found. Thanks to Tanya!
NonThm:    Unprovable.
NoSoln:    Proof not found.
CASC-16:   MIX UEQ
Problems:  RmEq_rstfp/tptp
Status:    CASC READY

System:    Waldmeister
Version:   798
URL:       http://www-avenhaus.informatik.uni-kl.de/waldmeister
Command:   WaldmeisterII.gcc.comp %s
Format:    waldmeister
Transform: rm_equality:rstfp
Theorem:   Goal proved.
NonThm:    System completed.
NoSoln:    Unfair completion run out of critical pairs.
CASC-16:   UEQ
Problems:  RmEq_rstfp/waldmeister
Status:    CASC 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-16:   UEQ
Problems:  RmEq_rstfp/waldmeister
Status:    CASC READY