default: cd /global/scratch/hutter/cssc/solvers; ruby ../scripts/generic_solver_wrapper.rb sat4j instances/Sat_Data/bench/HW-verification/40randomsets/04_rule/SAT_dat.k75.cnf 0 300.0 2147483647 9207562 -CLADECAY '0.999' -CLEANING 'LBD2' -PHASE 'RSATPhaseSelectionStrategy' -RESTARTS 'Glucose21Restarts' -SIMP 'EXPENSIVE_SIMPLIFICATION' -VARDECAY '0.95' CSSC-IBM-300s-2day: cd /global/scratch/hutter/cssc/solvers; ruby ../scripts/generic_solver_wrapper.rb sat4j instances/Sat_Data/bench/HW-verification/40randomsets/04_rule/SAT_dat.k75.cnf 0 300.0 2147483647 9207562 -CLADECAY '0.99' -CLEANING 'LBD2' -PHASE 'RSATPhaseSelectionStrategy' -RESTARTS 'Glucose21Restarts' -SIMP 'SIMPLE_SIMPLIFICATION' -VARDECAY '0.95' CSSC-5SAT500-sat-300s-2day: cd /global/scratch/hutter/cssc/solvers; ruby ../scripts/generic_solver_wrapper.rb sat4j instances/Sat_Data/jack_instances/5sat500.test/unif-k5-r20.00-v500-c10000-S1025515093.cnf 0 300.0 2147483647 9207562 -CLADECAY '0.999' -CLEANING 'LBD2' -PHASE 'RSATPhaseSelectionStrategy' -RESTARTS 'Glucose21Restarts' -SIMP 'EXPENSIVE_SIMPLIFICATION' -VARDECAY '0.95' CSSC-CircuitFuzz-300s-2day: cd /global/scratch/hutter/cssc/solvers; ruby ../scripts/generic_solver_wrapper.rb sat4j instances/Sat_Data/circuit_fuzz/fuzz_100_6463.cnf UNSATISFIABLE 300.0 2147483647 9207562 -CLADECAY '0.99' -CLEANING 'LBD2' -CONFLICTBOUNDINCFACTOR '4' -INITCONFLICTBOUND '1' -PHASE 'PhaseInLastLearnedClauseSelectionStrategy' -RESTARTS 'MiniSATRestarts' -SIMP 'EXPENSIVE_SIMPLIFICATION' -VARDECAY '0.9' CSSC-GI-300s-2day: cd /global/scratch/hutter/cssc/solvers; ruby ../scripts/generic_solver_wrapper.rb sat4j instances/Sat_Data/GI/iso_m2D_s36.AB23.cnf SATISFIABLE 300.0 2147483647 9207562 -CLADECAY '0.999' -CLEANING 'ACTIVITY' -INITCONFLICTBOUND '1' -PHASE 'RandomLiteralSelectionStrategy' -RESTARTS 'ArminRestarts' -SIMP 'SIMPLE_SIMPLIFICATION' -VARDECAY '0.95' CSSC-BMC08-300s-2day: cd /global/scratch/hutter/cssc/solvers; ruby ../scripts/generic_solver_wrapper.rb sat4j instances/Sat_Data/bmc/bmc08-50/abp4ptimoneg.k50.cnf SATISFIABLE 300.0 2147483647 9207562 -CLADECAY '0.999' -CLEANING 'LBD2' -PHASE 'RSATLastLearnedClausesPhaseSelectionStrategy' -RESTARTS 'Glucose21Restarts' -SIMP 'SIMPLE_SIMPLIFICATION' -VARDECAY '0.9' CSSC-LABS-300s-2day: cd /global/scratch/hutter/cssc/solvers; ruby ../scripts/generic_solver_wrapper.rb sat4j instances/Sat_Data/LABS/LABS_n025_goal004.cnf SATISFIABLE 300.0 2147483647 9207562 -CLADECAY '0.95' -CLEANING 'LBD2' -CONFLICTBOUNDINCFACTOR '4' -INITCONFLICTBOUND '100' -PHASE 'RandomLiteralSelectionStrategy' -RESTARTS 'MiniSATRestarts' -SIMP 'NO_SIMPLIFICATION' -VARDECAY '0.95' CSSC-K3-300s-2day: cd /global/scratch/hutter/cssc/solvers; ruby ../scripts/generic_solver_wrapper.rb sat4j instances/Sat_Data/K3-inst/k3-v275-c1172/unif-v275-c1172-797-S58452150.cnf UNSATISFIABLE 300.0 2147483647 9207562 -CLADECAY '0.99' -CLEANING 'LBD' -CONFLICTBOUNDINCFACTOR '2' -INITCONFLICTBOUND '10' -PHASE 'RSATPhaseSelectionStrategy' -RESTARTS 'MiniSATRestarts' -SIMP 'EXPENSIVE_SIMPLIFICATION' -VARDECAY '0.95' CSSC-unsat-unif-k5-300s-2day: cd /global/scratch/hutter/cssc/solvers; ruby ../scripts/generic_solver_wrapper.rb sat4j instances/Sat_Data/unsat-unif-k5/unif-k5-r21.117-v50-c1056-S3376777782583961866.cnf UNSATISFIABLE 300.0 2147483647 9207562 -CLADECAY '0.95' -CLEANING 'LBD2' -CONFLICTBOUNDINCFACTOR '4' -INITCONFLICTBOUND '100' -PHASE 'RSATPhaseSelectionStrategy' -RESTARTS 'MiniSATRestarts' -SIMP 'NO_SIMPLIFICATION' -VARDECAY '0.95' CSSC-SWV-300s-2days: cd /global/scratch/hutter/cssc/solvers; ruby ../scripts/generic_solver_wrapper.rb sat4j instances/Sat_Data/bench/SW-verification/GZIP_v1.2.4__v1.1/gzip_vc1028.cnf SATISFIABLE 300.0 2147483647 9207562 -CLADECAY '0.99' -CLEANING 'LBD' -LUBYFACTOR '16' -PHASE 'RSATPhaseSelectionStrategy' -RESTARTS 'LubyRestarts' -SIMP 'SIMPLE_SIMPLIFICATION' -VARDECAY '0.95'