default: cd /global/scratch/hutter/cssc/solvers; ruby ../scripts/generic_solver_wrapper.rb forl-nodrup instances/Sat_Data/bench/HW-verification/40randomsets/04_rule/SAT_dat.k75.cnf 0 300.0 2147483647 9207562 -agilg '0.9999' -agillim '0.03' -agilviollim '20' -alwaysmoremin '0' -binpri '0' -block '1' -cacheenable '1' -calcreach '1' -clbtwsimp '2' -clean 'propconfl' -clearstat '1' -compsenable '1' -elimcomplexupdate '1' -eratio '0.12' -freq '0' -gluehist '100' -implicitmanip '1' -incclean '1.1' -ltclean '0.5' -moreminim '1' -otfhyper '1' -otfsubsume '1' -polar 'auto' -precleanenable '0' -precleanlim '2' -precleantime '10000' -preschedsimp '1' -probeenable '1' -probemultip '1.0' -recur '1' -restart 'glue' -rewardotfsubsume '3' -schedsimplify '1' -simplify '1' -stamp '1' -startclean '10000' -unsat '1' -updateglue '1' -vincdiv '10' -vincmult '11' -vincstart '128' -vincvary '0' -vivif '1' -xorenable '1'
CSSC-IBM-300s-2day: cd /global/scratch/hutter/cssc/solvers; ruby ../scripts/generic_solver_wrapper.rb forl-nodrup instances/Sat_Data/bench/HW-verification/40randomsets/04_rule/SAT_dat.k75.cnf 0 300.0 2147483647 9207562 -agilg '0.99999' -agillim '0.02' -agilviollim '15' -alwaysmoremin '0' -binpri '0' -block '1' -cacheenable '0' -calcreach '0' -clbtwsimp '2' -clean 'propconfl' -clearstat '1' -compsenable '1' -elimcomplexupdate '0' -eratio '0.4' -freq '0' -gluehist '30' -implicitmanip '0' -incclean '1.4' -ltclean '0.5' -moreminim '0' -otfhyper '0' -otfsubsume '0' -polar 'auto' -precleanenable '1' -precleanlim '1' -precleantime '10000' -preschedsimp '0' -probeenable '1' -probemultip '1.0' -recur '1' -restart 'glue' -rewardotfsubsume '0' -schedsimplify '1' -simplify '1' -stamp '0' -startclean '15000' -unsat '0' -updateglue '1' -vincdiv '11' -vincmult '12' -vincstart '64' -vincvary '0' -vivif '0' -xorenable '0'
CSSC-5SAT500-sat-300s-2day: cd /global/scratch/hutter/cssc/solvers; ruby ../scripts/generic_solver_wrapper.rb forl-nodrup instances/Sat_Data/jack_instances/5sat500.test/unif-k5-r20.00-v500-c10000-S1025515093.cnf 0 300.0 2147483647 9207562 -agilg '0.9999' -agillim '0.03' -agilviollim '20' -alwaysmoremin '0' -binpri '0' -block '1' -cacheenable '1' -calcreach '1' -clbtwsimp '2' -clean 'propconfl' -clearstat '1' -compsenable '1' -elimcomplexupdate '1' -eratio '0.12' -freq '0' -gluehist '100' -implicitmanip '1' -incclean '1.1' -ltclean '0.5' -moreminim '1' -otfhyper '1' -otfsubsume '1' -polar 'auto' -precleanenable '0' -precleanlim '2' -precleantime '10000' -preschedsimp '1' -probeenable '1' -probemultip '1.0' -recur '1' -restart 'glue' -rewardotfsubsume '3' -schedsimplify '1' -simplify '1' -stamp '1' -startclean '10000' -unsat '1' -updateglue '1' -vincdiv '10' -vincmult '11' -vincstart '128' -vincvary '0' -vivif '1' -xorenable '1'
CSSC-CircuitFuzz-300s-2day: cd /global/scratch/hutter/cssc/solvers; ruby ../scripts/generic_solver_wrapper.rb forl-nodrup instances/Sat_Data/circuit_fuzz/fuzz_100_6463.cnf UNSATISFIABLE 300.0 2147483647 9207562 -agilg '0.9997' -agillim '0.03' -agilviollim '20' -alwaysmoremin '0' -binpri '0' -block '1' -cacheenable '0' -calcreach '1' -clbtwsimp '4' -clean 'size' -clearstat '0' -compsenable '1' -elimcomplexupdate '1' -eratio '0.12' -freq '0' -gluehist '130' -implicitmanip '0' -incclean '1.1' -ltclean '0.5' -moreminim '0' -otfhyper '1' -otfsubsume '1' -polar 'auto' -precleanenable '0' -precleanlim '2' -precleantime '10000' -preschedsimp '1' -probeenable '1' -probemultip '1.0' -recur '1' -restart 'glueagility' -rewardotfsubsume '3' -schedsimplify '0' -simplify '1' -stamp '1' -startclean '10000' -unsat '1' -updateglue '1' -vincdiv '9' -vincmult '10' -vincstart '64' -vincvary '2' -vivif '1' -xorenable '1'
CSSC-GI-300s-2day: cd /global/scratch/hutter/cssc/solvers; ruby ../scripts/generic_solver_wrapper.rb forl-nodrup instances/Sat_Data/GI/iso_m2D_s36.AB23.cnf SATISFIABLE 300.0 2147483647 9207562 -agilg '0.9998' -agillim '0.02' -agilviollim '20' -alwaysmoremin '1' -binpri '0' -block '1' -cacheenable '0' -calcreach '0' -clbtwsimp '4' -clean 'size' -clearstat '1' -compsenable '1' -elimcomplexupdate '1' -eratio '0.12' -freq '0.01' -gluehist '100' -implicitmanip '0' -incclean '1.05' -ltclean '0.5' -moreminim '1' -otfhyper '0' -otfsubsume '1' -polar 'auto' -precleanenable '0' -precleanlim '3' -precleantime '10000' -preschedsimp '1' -probeenable '1' -probemultip '1.0' -recur '1' -restart 'glueagility' -rewardotfsubsume '0' -schedsimplify '1' -simplify '0' -stamp '0' -startclean '8000' -unsat '0' -updateglue '0' -vincdiv '11' -vincmult '12' -vincstart '64' -vincvary '2' -vivif '1' -xorenable '1'
CSSC-BMC08-300s-2day: cd /global/scratch/hutter/cssc/solvers; ruby ../scripts/generic_solver_wrapper.rb forl-nodrup instances/Sat_Data/bmc/bmc08-50/abp4ptimoneg.k50.cnf SATISFIABLE 300.0 2147483647 9207562 -agilg '0.9997' -agillim '0.02' -agilviollim '15' -alwaysmoremin '1' -binpri '0' -block '0' -cacheenable '0' -calcreach '1' -clbtwsimp '1' -clean 'propconfl' -clearstat '1' -compsenable '0' -elimcomplexupdate '0' -eratio '0.4' -freq '0.05' -gluehist '100' -implicitmanip '1' -incclean '1.4' -ltclean '0.8' -moreminim '1' -otfhyper '1' -otfsubsume '0' -polar 'auto' -precleanenable '0' -precleanlim '1' -precleantime '10000' -preschedsimp '0' -probeenable '0' -probemultip '0.6' -recur '1' -restart 'glue' -rewardotfsubsume '10' -schedsimplify '1' -simplify '1' -stamp '0' -startclean '15000' -unsat '0' -updateglue '0' -vincdiv '9' -vincmult '10' -vincstart '256' -vincvary '2' -vivif '0' -xorenable '0'
CSSC-LABS-300s-2day: cd /global/scratch/hutter/cssc/solvers; ruby ../scripts/generic_solver_wrapper.rb forl-nodrup instances/Sat_Data/LABS/LABS_n025_goal004.cnf SATISFIABLE 300.0 2147483647 9207562 -agilg '0.9998' -agillim '0.02' -agilviollim '25' -alwaysmoremin '0' -binpri '0' -block '0' -cacheenable '1' -calcreach '1' -clbtwsimp '2' -clean 'propconfl' -clearstat '0' -compsenable '1' -elimcomplexupdate '1' -eratio '0.4' -freq '0' -gluehist '100' -implicitmanip '0' -incclean '1.4' -ltclean '0.5' -moreminim '1' -otfhyper '1' -otfsubsume '1' -polar 'auto' -precleanenable '1' -precleanlim '2' -precleantime '20000' -preschedsimp '0' -probeenable '1' -probemultip '1.5' -recur '1' -restart 'glueagility' -rewardotfsubsume '3' -schedsimplify '1' -simplify '0' -stamp '1' -startclean '15000' -unsat '1' -updateglue '1' -vincdiv '10' -vincmult '12' -vincstart '64' -vincvary '1' -vivif '0' -xorenable '0'
CSSC-K3-300s-2day: cd /global/scratch/hutter/cssc/solvers; ruby ../scripts/generic_solver_wrapper.rb forl-nodrup instances/Sat_Data/K3-inst/k3-v275-c1172/unif-v275-c1172-797-S58452150.cnf UNSATISFIABLE 300.0 2147483647 9207562 -agilg '0.9998' -agillim '0.02' -agilviollim '25' -alwaysmoremin '0' -binpri '0' -block '1' -cacheenable '1' -calcreach '1' -clbtwsimp '4' -clean 'size' -clearstat '1' -compsenable '1' -elimcomplexupdate '0' -eratio '0.12' -freq '0' -gluehist '60' -implicitmanip '1' -incclean '1.1' -ltclean '0.8' -moreminim '0' -otfhyper '1' -otfsubsume '1' -polar 'auto' -precleanenable '0' -precleanlim '3' -precleantime '20000' -preschedsimp '1' -probeenable '0' -probemultip '0.6' -recur '1' -restart 'glueagility' -rewardotfsubsume '3' -schedsimplify '1' -simplify '1' -stamp '0' -startclean '20000' -unsat '0' -updateglue '1' -vincdiv '10' -vincmult '11' -vincstart '128' -vincvary '2' -vivif '1' -xorenable '0'
CSSC-unsat-unif-k5-300s-2day: cd /global/scratch/hutter/cssc/solvers; ruby ../scripts/generic_solver_wrapper.rb forl-nodrup instances/Sat_Data/unsat-unif-k5/unif-k5-r21.117-v50-c1056-S3376777782583961866.cnf UNSATISFIABLE 300.0 2147483647 9207562 -agilg '0.99999' -agillim '0.03' -agilviollim '25' -alwaysmoremin '1' -binpri '0' -block '1' -cacheenable '0' -calcreach '1' -clbtwsimp '4' -clean 'size' -clearstat '1' -compsenable '1' -elimcomplexupdate '1' -eratio '0.12' -freq '0' -gluehist '130' -implicitmanip '0' -incclean '1.05' -ltclean '0.8' -moreminim '0' -otfhyper '0' -otfsubsume '1' -polar 'auto' -precleanenable '1' -precleanlim '3' -precleantime '40000' -preschedsimp '0' -probeenable '1' -probemultip '0.6' -recur '1' -restart 'glueagility' -rewardotfsubsume '10' -schedsimplify '0' -simplify '0' -stamp '1' -startclean '8000' -unsat '0' -updateglue '0' -vincdiv '11' -vincmult '12' -vincstart '64' -vincvary '0' -vivif '1' -xorenable '1'
CSSC-SWV-300s-2days: cd /global/scratch/hutter/cssc/solvers; ruby ../scripts/generic_solver_wrapper.rb forl-nodrup instances/Sat_Data/bench/SW-verification/GZIP_v1.2.4__v1.1/gzip_vc1028.cnf SATISFIABLE 300.0 2147483647 9207562 -agilg '0.9999' -agillim '0.04' -agilviollim '25' -alwaysmoremin '0' -binpri '0' -block '1' -cacheenable '0' -calcreach '1' -clbtwsimp '1' -clean 'propconfl' -clearstat '1' -compsenable '0' -elimcomplexupdate '1' -eratio '0.4' -freq '0' -gluehist '60' -implicitmanip '0' -incclean '1.2' -ltclean '0.3' -moreminim '1' -otfhyper '0' -otfsubsume '1' -polar 'false' -precleanenable '1' -precleanlim '3' -precleantime '10000' -preschedsimp '1' -probeenable '1' -probemultip '1.2' -recur '0' -restart 'glue' -rewardotfsubsume '3' -schedsimplify '1' -simplify '1' -stamp '0' -startclean '8000' -unsat '1' -updateglue '0' -vincdiv '11' -vincmult '11' -vincstart '64' -vincvary '0' -vivif '0' -xorenable '0'