default: cd /global/scratch/hutter/cssc/solvers; ruby ../scripts/generic_solver_wrapper.rb riss3g instances/Sat_Data/bench/HW-verification/40randomsets/04_rule/SAT_dat.k75.cnf 0 300.0 2147483647 9207562 -3resolve 'no' -K '0.8' -R '1.4' -all_strength_res '0' -alluiphack '0' -bva 'no' -bve 'yes' -bve_BCElim 'yes' -bve_cgrow '0' -bve_force_gates 'no' -bve_gates 'yes' -bve_heap_updates '2' -bve_red_lits '0' -bve_strength 'yes' -bve_totalG 'no' -bve_unlimited 'no' -cce 'no' -ccmin-mode '2' -cla-decay '0.999' -cp3_bve_heap '0' -cp3_bve_limit '25000000' -cp3_call_inc '100' -cp3_ptechs '""' -cp3_randomized 'no' -cp3_str_limit '300000000' -cp3_strength 'yes' -cp3_sub_limit '300000000' -cp3_uhdIters '3' -cp3_uhdNoShuffle 'no' -cp3_uhdTrans 'no' -cp3_uhdUHLE 'yes' -cp3_uhdUHTE 'yes' -dense 'yes' -ee 'no' -enabled_cp3 'yes' -firstReduceDB '4000' -gc-frac '0.2' -hack '1' -hack-cost 'yes' -hte 'no' -incReduceDB '300' -inprocess 'no' -laHack 'no' -longConflict 'no' -minLBDFrozenClause '30' -minLBDMinimizingClause '6' -minSizeMinimizingClause '30' -phase-saving '2' -probe 'no' -rMax '-1' -rew 'no' -rnd-freq '0' -rtype '0' -sls 'no' -specialIncReduceDB '1000' -subsimp 'yes' -szLBDQueue '50' -szTrailQueue '5000' -unhide 'yes' -up 'yes' -var-decay '0.95' CSSC-IBM-300s-2day: cd /global/scratch/hutter/cssc/solvers; ruby ../scripts/generic_solver_wrapper.rb riss3g instances/Sat_Data/bench/HW-verification/40randomsets/04_rule/SAT_dat.k75.cnf 0 300.0 2147483647 9207562 -3resolve 'no' -K '0.8' -R '1.4' -all_strength_res '0' -alluiphack '0' -bva 'no' -bve 'yes' -bve_BCElim 'yes' -bve_cgrow '0' -bve_force_gates 'no' -bve_gates 'yes' -bve_heap_updates '2' -bve_red_lits '1' -bve_strength 'yes' -bve_totalG 'no' -bve_unlimited 'no' -cce 'no' -ccmin-mode '2' -cla-decay '0.999' -cp3_bve_heap '0' -cp3_bve_limit '25000000' -cp3_call_inc '100' -cp3_ptechs '""' -cp3_randomized 'no' -cp3_str_limit '300000000' -cp3_strength 'yes' -cp3_sub_limit '300000' -dense 'yes' -ee 'no' -enabled_cp3 'yes' -firstReduceDB '4000' -gc-frac '0.1' -hack '0' -hte 'no' -incReduceDB '300' -inprocess 'no' -laHack 'no' -longConflict 'no' -minLBDFrozenClause '30' -minLBDMinimizingClause '3' -minSizeMinimizingClause '30' -phase-saving '2' -probe 'no' -rMax '-1' -rew 'no' -rnd-freq '0.005' -rtype '0' -sls 'no' -specialIncReduceDB '1000' -subsimp 'yes' -szLBDQueue '50' -szTrailQueue '5000' -unhide 'no' -up 'yes' -var-decay '0.85' CSSC-5SAT500-sat-300s-2day: cd /global/scratch/hutter/cssc/solvers; ruby ../scripts/generic_solver_wrapper.rb riss3g instances/Sat_Data/jack_instances/5sat500.test/unif-k5-r20.00-v500-c10000-S1025515093.cnf 0 300.0 2147483647 9207562 -3resolve 'no' -K '0.8' -R '1.4' -all_strength_res '0' -alluiphack '0' -bva 'no' -bve 'yes' -bve_BCElim 'yes' -bve_cgrow '0' -bve_force_gates 'no' -bve_gates 'yes' -bve_heap_updates '2' -bve_red_lits '0' -bve_strength 'yes' -bve_totalG 'no' -bve_unlimited 'no' -cce 'no' -ccmin-mode '2' -cla-decay '0.999' -cp3_bve_heap '0' -cp3_bve_limit '25000000' -cp3_call_inc '100' -cp3_ptechs '""' -cp3_randomized 'no' -cp3_str_limit '300000000' -cp3_strength 'yes' -cp3_sub_limit '300000000' -cp3_uhdIters '3' -cp3_uhdNoShuffle 'no' -cp3_uhdTrans 'no' -cp3_uhdUHLE 'yes' -cp3_uhdUHTE 'yes' -dense 'yes' -ee 'no' -enabled_cp3 'yes' -firstReduceDB '4000' -gc-frac '0.2' -hack '1' -hack-cost 'yes' -hte 'no' -incReduceDB '300' -inprocess 'no' -laHack 'no' -longConflict 'no' -minLBDFrozenClause '30' -minLBDMinimizingClause '6' -minSizeMinimizingClause '30' -phase-saving '2' -probe 'no' -rMax '-1' -rew 'no' -rnd-freq '0' -rtype '0' -sls 'no' -specialIncReduceDB '1000' -subsimp 'yes' -szLBDQueue '50' -szTrailQueue '5000' -unhide 'yes' -up 'yes' -var-decay '0.95' CSSC-CircuitFuzz-300s-2day: cd /global/scratch/hutter/cssc/solvers; ruby ../scripts/generic_solver_wrapper.rb riss3g instances/Sat_Data/circuit_fuzz/fuzz_100_6463.cnf UNSATISFIABLE 300.0 2147483647 9207562 -3resolve 'no' -all_strength_res '3' -alluiphack '2' -bva 'yes' -bve 'yes' -bve_BCElim 'yes' -bve_cgrow '20' -bve_gates 'no' -bve_heap_updates '2' -bve_red_lits '1' -bve_strength 'yes' -bve_totalG 'no' -bve_unlimited 'yes' -cce 'yes' -ccmin-mode '2' -cla-decay '0.995' -cp3_bva_Vlimit '3000000' -cp3_bva_compl 'no' -cp3_bva_dupli 'yes' -cp3_bva_inpInc '200' -cp3_bva_limit '12000000' -cp3_bva_push '1' -cp3_bva_subOr 'no' -cp3_bve_heap '0' -cp3_bve_limit '2500000' -cp3_call_inc '50' -cp3_cce_level '1' -cp3_cce_sizeP '40' -cp3_cce_steps '2000000' -cp3_hte_steps '214748' -cp3_ptechs '"u3svghpwc"' -cp3_randomized 'yes' -cp3_str_limit '400000000' -cp3_strength 'no' -cp3_sub_limit '300000000' -cp3_uhdIters '3' -cp3_uhdNoShuffle 'yes' -cp3_uhdTrans 'no' -cp3_uhdUHLE 'no' -cp3_uhdUHTE 'yes' -dense 'yes' -ee 'no' -enabled_cp3 'yes' -firstReduceDB '4000' -gc-frac '0.3' -hack '1' -hack-cost 'no' -hte 'yes' -incReduceDB '300' -inprocess 'no' -laHack 'no' -longConflict 'no' -minLBDFrozenClause '50' -minLBDMinimizingClause '6' -minSizeMinimizingClause '15' -phase-saving '1' -probe 'no' -rew 'no' -rfirst '1000' -rinc '2' -rnd-freq '0.005' -rtype '2' -sls 'yes' -sls-adopt-cls 'yes' -sls-ksat-flips '20000000' -sls-rnd-walk '500' -specialIncReduceDB '900' -subsimp 'yes' -unhide 'yes' -up 'yes' -var-decay '0.99' CSSC-GI-300s-2day: cd /global/scratch/hutter/cssc/solvers; ruby ../scripts/generic_solver_wrapper.rb riss3g instances/Sat_Data/GI/iso_m2D_s36.AB23.cnf SATISFIABLE 300.0 2147483647 9207562 -K '0.7' -R '1.4' -alluiphack '2' -ccmin-mode '2' -cla-decay '0.995' -enabled_cp3 'no' -firstReduceDB '4000' -gc-frac '0.1' -hack '0' -incReduceDB '300' -laHack 'no' -longConflict 'no' -minLBDFrozenClause '15' -minLBDMinimizingClause '9' -minSizeMinimizingClause '30' -phase-saving '0' -rMax '-1' -rnd-freq '0' -rtype '0' -specialIncReduceDB '1100' -szLBDQueue '30' -szTrailQueue '4000' -var-decay '0.99' CSSC-BMC08-300s-2day: cd /global/scratch/hutter/cssc/solvers; ruby ../scripts/generic_solver_wrapper.rb riss3g instances/Sat_Data/bmc/bmc08-50/abp4ptimoneg.k50.cnf SATISFIABLE 300.0 2147483647 9207562 -3resolve 'no' -K '0.8' -R '1.2' -all_strength_res '0' -alluiphack '0' -bva 'no' -bve 'yes' -bve_BCElim 'yes' -bve_cgrow '0' -bve_force_gates 'no' -bve_gates 'yes' -bve_heap_updates '2' -bve_red_lits '0' -bve_strength 'yes' -bve_totalG 'no' -bve_unlimited 'no' -cce 'yes' -ccmin-mode '2' -cla-decay '0.995' -cp3_bve_heap '0' -cp3_bve_limit '25000000' -cp3_call_inc '100' -cp3_cce_level '3' -cp3_cce_sizeP '40' -cp3_cce_steps '2000000' -cp3_ptechs '""' -cp3_randomized 'no' -cp3_str_limit '300000000' -cp3_strength 'yes' -cp3_sub_limit '3000000' -cp3_uhdIters '3' -cp3_uhdNoShuffle 'no' -cp3_uhdTrans 'no' -cp3_uhdUHLE 'yes' -cp3_uhdUHTE 'yes' -dense 'yes' -dyn 'no' -ee 'no' -enabled_cp3 'yes' -firstReduceDB '16000' -gc-frac '0.2' -hack '0' -hlaLevel '5' -hlaTop '-1' -hlabound '4096' -hlaevery '1' -hte 'no' -incReduceDB '300' -inprocess 'no' -laHack 'yes' -longConflict 'no' -minLBDFrozenClause '15' -minLBDMinimizingClause '6' -minSizeMinimizingClause '30' -phase-saving '2' -probe 'no' -rMax '-1' -rew 'no' -rnd-freq '0.005' -rtype '0' -sls 'no' -specialIncReduceDB '1000' -subsimp 'yes' -szLBDQueue '30' -szTrailQueue '5000' -tabu 'no' -unhide 'yes' -up 'yes' -var-decay '0.85' CSSC-LABS-300s-2day: cd /global/scratch/hutter/cssc/solvers; ruby ../scripts/generic_solver_wrapper.rb riss3g instances/Sat_Data/LABS/LABS_n025_goal004.cnf SATISFIABLE 300.0 2147483647 9207562 -3resolve 'yes' -all_strength_res '4' -alluiphack '2' -bva 'yes' -bve 'yes' -bve_BCElim 'no' -bve_cgrow '-1' -bve_cgrow_t '10000' -bve_gates 'no' -bve_heap_updates '1' -bve_red_lits '1' -bve_strength 'no' -bve_totalG 'yes' -bve_unlimited 'no' -cce 'no' -ccmin-mode '2' -cla-decay '0.995' -cp3_bva_Vlimit '3000000' -cp3_bva_compl 'no' -cp3_bva_dupli 'yes' -cp3_bva_inpInc '20000' -cp3_bva_limit '12000000' -cp3_bva_push '2' -cp3_bva_subOr 'yes' -cp3_bve_heap '1' -cp3_bve_limit '2500000' -cp3_call_inc '50' -cp3_ptechs '"u3sghpvwc"' -cp3_randomized 'yes' -cp3_res3_ncls '100000' -cp3_res3_reAdd 'no' -cp3_res3_steps '100000' -cp3_res_bin 'no' -cp3_res_eagerSub 'yes' -cp3_res_inpInc '2000' -cp3_str_limit '300000000' -cp3_strength 'yes' -cp3_sub_limit '400000000' -cp3_uhdIters '1' -cp3_uhdNoShuffle 'yes' -cp3_uhdTrans 'yes' -cp3_uhdUHLE 'no' -cp3_uhdUHTE 'yes' -dense 'yes' -dyn 'no' -ee 'no' -enabled_cp3 'yes' -firstReduceDB '4000' -gc-frac '0.3' -hack '0' -hlaLevel '3' -hlaTop '-1' -hlabound '1024' -hlaevery '8' -hte 'no' -incReduceDB '200' -inprocess 'no' -laHack 'yes' -longConflict 'no' -minLBDFrozenClause '50' -minLBDMinimizingClause '6' -minSizeMinimizingClause '15' -phase-saving '2' -probe 'no' -rew 'no' -rfirst '1000' -rinc '2' -rnd-freq '0.005' -rtype '2' -sls 'yes' -sls-adopt-cls 'yes' -sls-ksat-flips '-1' -sls-rnd-walk '2000' -specialIncReduceDB '1000' -subsimp 'yes' -tabu 'yes' -unhide 'yes' -up 'no' -var-decay '0.99' CSSC-K3-300s-2day: cd /global/scratch/hutter/cssc/solvers; ruby ../scripts/generic_solver_wrapper.rb riss3g instances/Sat_Data/K3-inst/k3-v275-c1172/unif-v275-c1172-797-S58452150.cnf UNSATISFIABLE 300.0 2147483647 9207562 -3resolve 'no' -all_strength_res '5' -alluiphack '2' -bva 'no' -bve 'yes' -bve_BCElim 'no' -bve_cgrow '-1' -bve_cgrow_t '0' -bve_gates 'no' -bve_heap_updates '2' -bve_red_lits '1' -bve_strength 'yes' -bve_totalG 'yes' -bve_unlimited 'no' -cce 'yes' -ccmin-mode '2' -cla-decay '0.995' -cp3_bve_heap '1' -cp3_bve_inpInc '500000' -cp3_bve_learnt_growth '1000' -cp3_bve_limit '2500000' -cp3_bve_resolve_learnts '2' -cp3_call_inc '100' -cp3_cce_inpInc '600' -cp3_cce_level '1' -cp3_cce_sizeP '80' -cp3_cce_steps '2000000' -cp3_hte_inpInc '600' -cp3_hte_steps '2147483' -cp3_inp_cons '80000' -cp3_itechs '"us"' -cp3_ptechs '""' -cp3_randomized 'yes' -cp3_str_limit '3000000' -cp3_strength 'no' -cp3_sub_inpInc '40000000' -cp3_sub_limit '400000000' -cp3_uhdIters '3' -cp3_uhdNoShuffle 'no' -cp3_uhdTrans 'yes' -cp3_uhdUHLE 'yes' -cp3_uhdUHTE 'yes' -dense 'no' -ee 'no' -enabled_cp3 'yes' -firstReduceDB '2000' -gc-frac '0.1' -hack '0' -hte 'yes' -inc-inp 'yes' -incReduceDB '200' -inprocess 'yes' -laHack 'no' -longConflict 'yes' -minLBDFrozenClause '30' -minLBDMinimizingClause '3' -minSizeMinimizingClause '15' -phase-saving '1' -probe 'no' -randInp 'no' -rew 'no' -rfirst '1' -rinc '4' -rnd-freq '0' -rtype '2' -sls 'no' -specialIncReduceDB '900' -subsimp 'yes' -unhide 'yes' -up 'no' -var-decay '0.99' CSSC-unsat-unif-k5-300s-2day: cd /global/scratch/hutter/cssc/solvers; ruby ../scripts/generic_solver_wrapper.rb riss3g instances/Sat_Data/unsat-unif-k5/unif-k5-r21.117-v50-c1056-S3376777782583961866.cnf UNSATISFIABLE 300.0 2147483647 9207562 -alluiphack '0' -ccmin-mode '2' -cla-decay '0.999' -dyn 'yes' -enabled_cp3 'no' -firstReduceDB '2000' -gc-frac '0.1' -hack '0' -hlaLevel '4' -hlaMax '25' -hlaTop '64' -hlabound '32768' -hlaevery '64' -incReduceDB '200' -laHack 'yes' -longConflict 'yes' -minLBDFrozenClause '15' -minLBDMinimizingClause '3' -minSizeMinimizingClause '3' -phase-saving '2' -rfirst '32' -rinc '4' -rnd-freq '0' -rtype '2' -specialIncReduceDB '900' -tabu 'yes' -var-decay '0.99' CSSC-SWV-300s-2days: cd /global/scratch/hutter/cssc/solvers; ruby ../scripts/generic_solver_wrapper.rb riss3g instances/Sat_Data/bench/SW-verification/GZIP_v1.2.4__v1.1/gzip_vc1028.cnf SATISFIABLE 300.0 2147483647 9207562 -3resolve 'no' -K '0.95' -R '2.0' -all_strength_res '5' -alluiphack '2' -bva 'no' -bve 'yes' -bve_BCElim 'no' -bve_cgrow '10' -bve_gates 'no' -bve_heap_updates '2' -bve_red_lits '0' -bve_strength 'yes' -bve_totalG 'no' -bve_unlimited 'no' -cce 'no' -ccmin-mode '2' -cla-decay '0.999' -cp3_bve_heap '0' -cp3_bve_limit '2500000' -cp3_call_inc '200' -cp3_ptechs '""' -cp3_randomized 'no' -cp3_str_limit '300000000' -cp3_strength 'yes' -cp3_sub_limit '300000' -dense 'yes' -ee 'no' -enabled_cp3 'yes' -firstReduceDB '16000' -gc-frac '0.3' -hack '0' -hte 'no' -incReduceDB '450' -inprocess 'no' -laHack 'no' -longConflict 'yes' -minLBDFrozenClause '15' -minLBDMinimizingClause '6' -minSizeMinimizingClause '30' -phase-saving '2' -probe 'no' -rMax '40000' -rMaxInc '1.5' -rew 'no' -rnd-freq '0' -rtype '0' -sls 'no' -specialIncReduceDB '1000' -subsimp 'yes' -szLBDQueue '30' -szTrailQueue '6000' -unhide 'no' -up 'yes' -var-decay '0.7'