default: cd /global/scratch/hutter/cssc/solvers; ruby ../scripts/generic_solver_wrapper.rb lingeling instances/Sat_Data/bench/HW-verification/40randomsets/04_rule/SAT_dat.k75.cnf 0 300.0 2147483647 9207562 -actavgmax '112' -actdblarithlim '3' -actgeomlim '2' -actgsdul '7' -acts '2' -actstdmax '112' -actstdmin '10' -actvlim '2147483647' -agile '23' -bate '1' -batewait '2' -bca '1' -bcamaxeff '10000000' -bcaminuse '100' -bcawait '2' -bias '2' -blkboost '10' -blkclslim '1000' -blkmaxeff '-1' -blkmineff '50000000' -blkocclim '10000' -blkreleff '100' -blkrtc '0' -block '1' -blockwait '1' -bumpbcplits '0' -bumpbeforemin '1' -bumpclslits '0' -bumpseenlits '1' -card '1' -cardexpam1 '3' -cardglue '0' -cardignonbin '0' -cardmaxeff '20000000' -cardmaxlen '1000' -cardmineff '400000' -cardminlen '4' -cardocclim '100' -cardreleff '4' -cardreschedint '10' -carduse '2' -cce '3' -ccemaxeff '200000000' -ccemineff '3000000' -ccereleff '3' -ccewait '2' -cgrclsr '1' -cgrclsrwait '2' -cgreleff '1' -cgrextand '1' -cgrexteq '1' -cgrextite '1' -cgrextunits '1' -cgrextxor '1' -cgrmaxeff '8000000' -cgrmaxority '20' -cgrmineff '200000' -cintinc '20000' -cintincdiv '1' -cliff '1' -cliffmaxeff '100000000' -cliffmineff '10000000' -cliffreleff '8' -cliffwait '2' -clim '-1' -compact '0' -deco '2' -decolim '60' -decompose '1' -defragfree '50' -defragint '10000000' -delmax '10' -dlim '-1' -elim '1' -elmaxeff '-1' -elmblk '1' -elmblkwait '1' -elmboost '40' -elmclslim '1000' -elmineff '20000000' -elmlitslim '200' -elmocclim '10000' -elmplim1 '100' -elmplim2 '8' -elmreleff '200' -elmroundlim '3' -elmrtc '0' -elmsched2b2 '0' -elmschedprod '0' -elmschedpure '0' -elmschedsum '1' -factmax '10' -factor '1' -flipdur '10' -flipint '10' -flipping '1' -fliptop '1' -flipvlim '100000' -force '0' -gauss '1' -gaussexptrn '1' -gaussextrall '1' -gaussmaxeff '50000000' -gaussmaxor '20' -gaussmineff '2000000' -gaussreleff '2' -gausswait '2' -gluekeep '3' -gluescale '4' -import '1' -inprocessing '1' -irrlim '1' -itsimpdel '20' -keepmaxglue '0' -lftmaxeff '20000000' -lftmineff '500000' -lftreleff '6' -lftroundlim '5' -lhbr '1' -lift '1' -liftwait '2' -lkhd '2' -lkhdmisifelmrtc '0' -maxglue '10000' -maxscorexp '500' -memlim '-1' -minimize '2' -minlocalgluelim '40' -minrecgluelim '20' -mocint '1000' -move '2' -otfs '1' -otfsbump '1' -otfsconf '1' -penmax '4' -phase '0' -phaseflip '0' -phaseneginit '0' -plain '0' -prbasic '1' -prbasicmaxeff '100000000' -prbasicmineff '1000000' -prbasicreleff '10' -prbasicroundlim '9' -prbasicrtc '0' -prbrtc '0' -prbsimple '2' -prbsimpleboost '10' -prbsimpleliftdepth '2' -prbsimplemaxeff '200000000' -prbsimplemineff '2000000' -prbsimplereleff '40' -prbsimplertc '0' -probe '1' -psm '0' -randec '1' -randecint '1000' -rdp '1' -rdpclslim '5' -rdplim '80' -rdpmaxeff '200000000' -rdpmineff '200000' -rdpreleff '10' -rdpwait '2' -redfixed '0' -redinoutinc '100' -redlbound '0' -redlexpfac '10' -redlinc '1000' -redlinit '4000' -redlmaxabs '1000000' -redlmaxinc '200' -redlmaxrel '300' -redlminabs '500' -redlmininc '10' -redlminrel '10' -redloutinc '10000' -redoutvlim '1000' -reduce '2' -rephase '1' -rephaseinc '10000' -restart '2' -restartint '5' -restartintscale '0' -rmincpen '4' -rstinoutinc '110' -scincinc '200' -score '5' -seed '0' -simpdelay '0' -simpen '0' -simpinterdelay '2000' -simpirrlim '20' -simplify '2' -simprtc '5' -sizemaxpen '5' -sizepen '1000000' -smallirr '90' -smallve '1' -smallvevars '10' -smallvewait '0' -sortlits '0' -subl '9' -synclsall '1' -synclsglue '8' -synclsint '100' -synclslen '40' -syncunint '111111' -termint '122222' -ternres '1' -ternresboost '5' -ternresrtc '0' -ternreswait '2' -transred '1' -transredwait '2' -trdmaxeff '2000000' -trdmineff '100000' -trdreleff '10' -treelook '1' -treelookboost '20' -treelookfull '0' -treelooklrg '1' -treelookmaxeff '50000000' -treelookmineff '300000' -treelookreleff '1' -treelookrtc '0' -trep '0' -trepint '55555' -trnreleff '10' -trnrmaxeff '200000000' -trnrmineff '4000000' -unhdextstamp '1' -unhdhbr '0' -unhdlnpr '3' -unhdmaxeff '20000000' -unhdmineff '1000000' -unhdreleff '3' -unhdroundlim '20' -unhide '1' -unhidewait '2' -wait '1'
CSSC-IBM-300s-2day: cd /global/scratch/hutter/cssc/solvers; ruby ../scripts/generic_solver_wrapper.rb lingeling instances/Sat_Data/bench/HW-verification/40randomsets/04_rule/SAT_dat.k75.cnf 0 300.0 2147483647 9207562 -actavgmax '112' -actdblarithlim '3' -actgeomlim '2' -actgsdul '7' -acts '2' -actstdmax '112' -actstdmin '10' -actvlim '2147483647' -agile '23' -bate '1' -batewait '2' -bca '1' -bcamaxeff '10000000' -bcaminuse '100' -bcawait '2' -bias '2' -blkboost '10' -blkclslim '1000' -blkmaxeff '-1' -blkmineff '50000000' -blkocclim '10000' -blkreleff '100' -blkrtc '0' -block '1' -blockwait '1' -bumpbcplits '0' -bumpbeforemin '1' -bumpclslits '0' -bumpseenlits '1' -card '1' -cardexpam1 '3' -cardglue '0' -cardignonbin '0' -cardmaxeff '20000000' -cardmaxlen '1000' -cardmineff '400000' -cardminlen '4' -cardocclim '100' -cardreleff '4' -cardreschedint '10' -carduse '2' -cce '3' -ccemaxeff '200000000' -ccemineff '3000000' -ccereleff '3' -ccewait '2' -cgrclsr '1' -cgrclsrwait '2' -cgreleff '1' -cgrextand '1' -cgrexteq '1' -cgrextite '1' -cgrextunits '1' -cgrextxor '1' -cgrmaxeff '8000000' -cgrmaxority '20' -cgrmineff '200000' -cintinc '20000' -cintincdiv '1' -cliff '1' -cliffmaxeff '100000000' -cliffmineff '10000000' -cliffreleff '8' -cliffwait '2' -clim '-1' -compact '0' -deco '2' -decolim '60' -decompose '1' -defragfree '50' -defragint '10000000' -delmax '10' -dlim '-1' -elim '1' -elmaxeff '-1' -elmblk '1' -elmblkwait '1' -elmboost '40' -elmclslim '1000' -elmineff '20000000' -elmlitslim '200' -elmocclim '10000' -elmplim1 '100' -elmplim2 '8' -elmreleff '200' -elmroundlim '3' -elmrtc '0' -elmsched2b2 '0' -elmschedprod '0' -elmschedpure '0' -elmschedsum '1' -factmax '10' -factor '1' -flipdur '10' -flipint '10' -flipping '1' -fliptop '1' -flipvlim '100000' -force '0' -gauss '1' -gaussexptrn '1' -gaussextrall '1' -gaussmaxeff '50000000' -gaussmaxor '20' -gaussmineff '2000000' -gaussreleff '2' -gausswait '2' -gluekeep '3' -gluescale '4' -import '1' -inprocessing '1' -irrlim '1' -itsimpdel '20' -keepmaxglue '0' -lftmaxeff '20000000' -lftmineff '500000' -lftreleff '6' -lftroundlim '5' -lhbr '1' -lift '1' -liftwait '2' -lkhd '2' -lkhdmisifelmrtc '0' -maxglue '10000' -maxscorexp '500' -memlim '-1' -minimize '2' -minlocalgluelim '40' -minrecgluelim '20' -mocint '1000' -move '2' -otfs '1' -otfsbump '1' -otfsconf '1' -penmax '4' -phase '0' -phaseflip '0' -phaseneginit '0' -plain '0' -prbasic '1' -prbasicmaxeff '100000000' -prbasicmineff '1000000' -prbasicreleff '10' -prbasicroundlim '9' -prbasicrtc '0' -prbrtc '0' -prbsimple '2' -prbsimpleboost '10' -prbsimpleliftdepth '2' -prbsimplemaxeff '200000000' -prbsimplemineff '2000000' -prbsimplereleff '40' -prbsimplertc '0' -probe '1' -psm '0' -randec '1' -randecint '1000' -rdp '1' -rdpclslim '5' -rdplim '80' -rdpmaxeff '99999999' -rdpmineff '200000' -rdpreleff '10' -rdpwait '2' -redfixed '0' -redinoutinc '100' -redlbound '0' -redlexpfac '10' -redlinc '1000' -redlinit '4000' -redlmaxabs '1000000' -redlmaxinc '200' -redlmaxrel '300' -redlminabs '500' -redlmininc '10' -redlminrel '10' -redloutinc '10000' -redoutvlim '1000' -reduce '2' -rephase '1' -rephaseinc '10000' -restart '2' -restartint '5' -restartintscale '0' -rmincpen '4' -rstinoutinc '110' -scincinc '200' -score '5' -seed '0' -simpdelay '0' -simpen '0' -simpinterdelay '2000' -simpirrlim '20' -simplify '2' -simprtc '54' -sizemaxpen '5' -sizepen '1000000' -smallirr '90' -smallve '1' -smallvevars '5' -smallvewait '0' -sortlits '0' -subl '9' -synclsall '1' -synclsglue '8' -synclsint '100' -synclslen '40' -syncunint '111111' -termint '122222' -ternres '1' -ternresboost '5' -ternresrtc '0' -ternreswait '2' -transred '1' -transredwait '2' -trdmaxeff '2000000' -trdmineff '100000' -trdreleff '10' -treelook '1' -treelookboost '20' -treelookfull '0' -treelooklrg '1' -treelookmaxeff '50000000' -treelookmineff '300000' -treelookreleff '1' -treelookrtc '0' -trep '0' -trepint '55555' -trnreleff '10' -trnrmaxeff '200000000' -trnrmineff '4000000' -unhdextstamp '1' -unhdhbr '0' -unhdlnpr '3' -unhdmaxeff '20000000' -unhdmineff '1000000' -unhdreleff '3' -unhdroundlim '20' -unhide '1' -unhidewait '2' -wait '1'
CSSC-5SAT500-sat-300s-2day: cd /global/scratch/hutter/cssc/solvers; ruby ../scripts/generic_solver_wrapper.rb lingeling instances/Sat_Data/jack_instances/5sat500.test/unif-k5-r20.00-v500-c10000-S1025515093.cnf 0 300.0 2147483647 9207562 -actavgmax '112' -actdblarithlim '3' -actgeomlim '2' -actgsdul '7' -acts '2' -actstdmax '112' -actstdmin '10' -actvlim '2147483647' -agile '23' -bate '1' -batewait '2' -bca '1' -bcamaxeff '10000000' -bcaminuse '100' -bcawait '2' -bias '2' -blkboost '10' -blkclslim '1000' -blkmaxeff '-1' -blkmineff '50000000' -blkocclim '10000' -blkreleff '100' -blkrtc '0' -block '1' -blockwait '1' -bumpbcplits '0' -bumpbeforemin '1' -bumpclslits '0' -bumpseenlits '1' -card '1' -cardexpam1 '3' -cardglue '0' -cardignonbin '0' -cardmaxeff '20000000' -cardmaxlen '1000' -cardmineff '400000' -cardminlen '4' -cardocclim '100' -cardreleff '4' -cardreschedint '10' -carduse '2' -cce '3' -ccemaxeff '200000000' -ccemineff '3000000' -ccereleff '3' -ccewait '2' -cgrclsr '1' -cgrclsrwait '2' -cgreleff '1' -cgrextand '1' -cgrexteq '1' -cgrextite '1' -cgrextunits '1' -cgrextxor '1' -cgrmaxeff '8000000' -cgrmaxority '20' -cgrmineff '200000' -cintinc '20000' -cintincdiv '1' -cliff '1' -cliffmaxeff '100000000' -cliffmineff '10000000' -cliffreleff '8' -cliffwait '2' -clim '-1' -compact '0' -deco '2' -decolim '60' -decompose '1' -defragfree '50' -defragint '10000000' -delmax '10' -dlim '-1' -elim '1' -elmaxeff '-1' -elmblk '1' -elmblkwait '1' -elmboost '40' -elmclslim '1000' -elmineff '20000000' -elmlitslim '200' -elmocclim '10000' -elmplim1 '100' -elmplim2 '8' -elmreleff '200' -elmroundlim '3' -elmrtc '0' -elmsched2b2 '0' -elmschedprod '0' -elmschedpure '0' -elmschedsum '1' -factmax '10' -factor '1' -flipdur '10' -flipint '10' -flipping '1' -fliptop '1' -flipvlim '100000' -force '0' -gauss '1' -gaussexptrn '1' -gaussextrall '1' -gaussmaxeff '50000000' -gaussmaxor '20' -gaussmineff '2000000' -gaussreleff '2' -gausswait '2' -gluekeep '3' -gluescale '4' -import '1' -inprocessing '1' -irrlim '1' -itsimpdel '20' -keepmaxglue '0' -lftmaxeff '20000000' -lftmineff '500000' -lftreleff '6' -lftroundlim '5' -lhbr '1' -lift '1' -liftwait '2' -lkhd '2' -lkhdmisifelmrtc '0' -maxglue '10000' -maxscorexp '500' -memlim '-1' -minimize '2' -minlocalgluelim '40' -minrecgluelim '20' -mocint '1000' -move '2' -otfs '1' -otfsbump '1' -otfsconf '1' -penmax '4' -phase '0' -phaseflip '0' -phaseneginit '0' -plain '0' -prbasic '1' -prbasicmaxeff '100000000' -prbasicmineff '1000000' -prbasicreleff '10' -prbasicroundlim '9' -prbasicrtc '0' -prbrtc '0' -prbsimple '2' -prbsimpleboost '10' -prbsimpleliftdepth '2' -prbsimplemaxeff '200000000' -prbsimplemineff '2000000' -prbsimplereleff '40' -prbsimplertc '0' -probe '1' -psm '0' -randec '1' -randecint '1000' -rdp '1' -rdpclslim '5' -rdplim '80' -rdpmaxeff '200000000' -rdpmineff '200000' -rdpreleff '10' -rdpwait '2' -redfixed '0' -redinoutinc '100' -redlbound '0' -redlexpfac '10' -redlinc '1000' -redlinit '4000' -redlmaxabs '1000000' -redlmaxinc '200' -redlmaxrel '300' -redlminabs '500' -redlmininc '10' -redlminrel '10' -redloutinc '10000' -redoutvlim '1000' -reduce '2' -rephase '1' -rephaseinc '10000' -restart '2' -restartint '5' -restartintscale '0' -rmincpen '4' -rstinoutinc '110' -scincinc '200' -score '5' -seed '0' -simpdelay '0' -simpen '0' -simpinterdelay '2000' -simpirrlim '20' -simplify '2' -simprtc '5' -sizemaxpen '5' -sizepen '1000000' -smallirr '90' -smallve '1' -smallvevars '10' -smallvewait '0' -sortlits '0' -subl '9' -synclsall '1' -synclsglue '8' -synclsint '100' -synclslen '40' -syncunint '111111' -termint '122222' -ternres '1' -ternresboost '5' -ternresrtc '0' -ternreswait '2' -transred '1' -transredwait '2' -trdmaxeff '2000000' -trdmineff '100000' -trdreleff '10' -treelook '1' -treelookboost '20' -treelookfull '0' -treelooklrg '1' -treelookmaxeff '50000000' -treelookmineff '300000' -treelookreleff '1' -treelookrtc '0' -trep '0' -trepint '55555' -trnreleff '10' -trnrmaxeff '200000000' -trnrmineff '4000000' -unhdextstamp '1' -unhdhbr '0' -unhdlnpr '3' -unhdmaxeff '20000000' -unhdmineff '1000000' -unhdreleff '3' -unhdroundlim '20' -unhide '1' -unhidewait '2' -wait '1'
CSSC-CircuitFuzz-300s-2day: cd /global/scratch/hutter/cssc/solvers; ruby ../scripts/generic_solver_wrapper.rb lingeling instances/Sat_Data/circuit_fuzz/fuzz_100_6463.cnf UNSATISFIABLE 300.0 2147483647 9207562 -acts '0' -bate '0' -batewait '1' -bca '0' -bcawait '1' -bias '0' -blkrtc '0' -block '0' -blockwait '0' -bumpbcplits '1' -bumpbeforemin '0' -bumpclslits '1' -bumpseenlits '1' -card '1' -cardignonbin '0' -carduse '0' -cce '3' -ccewait '2' -cgrclsr '1' -cgrclsrwait '0' -cgrextand '0' -cgrexteq '0' -cgrextite '1' -cgrextunits '1' -cgrextxor '0' -cintincdiv '2' -cliff '1' -cliffwait '0' -compact '2' -deco '2' -decompose '0' -elim '1' -elmblk '0' -elmblkwait '1' -elmrtc '1' -elmsched2b2 '0' -elmschedprod '0' -elmschedpure '1' -elmschedsum '1' -factor '1' -flipping '1' -fliptop '0' -gauss '0' -gaussexptrn '1' -gaussextrall '0' -gausswait '1' -gluescale '4' -import '1' -inprocessing '1' -irrlim '0' -keepmaxglue '1' -lhbr '1' -lift '1' -liftwait '2' -lkhd '1' -lkhdmisifelmrtc '1' -minimize '2' -move '2' -otfs '0' -otfsbump '0' -otfsconf '0' -phase '-1' -phaseflip '1' -plain '0' -prbasic '2' -prbasicrtc '1' -prbrtc '0' -prbsimple '2' -prbsimplertc '1' -probe '1' -psm '3' -randec '0' -rdp '1' -rdpwait '0' -redfixed '1' -redlbound '1' -reduce '4' -rephase '2' -restart '0' -restartintscale '1' -score '1' -simplify '1' -smallve '1' -smallvevars '10' -smallvewait '0' -sortlits '1' -synclsall '0' -ternres '0' -ternresrtc '1' -ternreswait '0' -transred '1' -transredwait '1' -treelook '1' -treelookfull '1' -treelooklrg '0' -treelookrtc '1' -trep '0' -unhdextstamp '1' -unhdhbr '0' -unhide '0' -unhidewait '2' -wait '0'
CSSC-GI-300s-2day: cd /global/scratch/hutter/cssc/solvers; ruby ../scripts/generic_solver_wrapper.rb lingeling instances/Sat_Data/GI/iso_m2D_s36.AB23.cnf SATISFIABLE 300.0 2147483647 9207562 -acts '2' -bate '1' -batewait '2' -bca '1' -bcawait '2' -bias '1' -blkrtc '0' -block '1' -blockwait '1' -bumpbcplits '1' -bumpbeforemin '1' -bumpclslits '0' -bumpseenlits '0' -card '1' -cardignonbin '0' -carduse '1' -cce '0' -ccewait '1' -cgrclsr '0' -cgrclsrwait '2' -cgrextand '1' -cgrexteq '0' -cgrextite '0' -cgrextunits '0' -cgrextxor '0' -cintincdiv '2' -cliff '0' -cliffwait '1' -compact '1' -deco '0' -decompose '1' -elim '0' -elmblk '1' -elmblkwait '0' -elmrtc '1' -elmsched2b2 '1' -elmschedprod '1' -elmschedpure '1' -elmschedsum '0' -factor '1' -flipping '0' -fliptop '0' -gauss '0' -gaussexptrn '1' -gaussextrall '1' -gausswait '1' -gluescale '3' -import '0' -inprocessing '0' -irrlim '1' -keepmaxglue '1' -lhbr '1' -lift '0' -liftwait '1' -lkhd '1' -lkhdmisifelmrtc '0' -minimize '0' -move '3' -otfs '1' -otfsbump '2' -otfsconf '1' -phase '-1' -phaseflip '1' -plain '1' -prbasic '2' -prbasicrtc '1' -prbrtc '1' -prbsimple '2' -prbsimplertc '1' -probe '1' -psm '0' -randec '1' -rdp '0' -rdpwait '1' -redfixed '0' -redlbound '1' -reduce '0' -rephase '1' -restart '3' -restartintscale '0' -score '0' -simplify '1' -smallve '0' -smallvevars '9' -smallvewait '0' -sortlits '0' -synclsall '0' -ternres '1' -ternresrtc '1' -ternreswait '0' -transred '1' -transredwait '2' -treelook '0' -treelookfull '0' -treelooklrg '0' -treelookrtc '1' -trep '0' -unhdextstamp '1' -unhdhbr '0' -unhide '1' -unhidewait '1' -wait '1'
CSSC-BMC08-300s-2day: cd /global/scratch/hutter/cssc/solvers; ruby ../scripts/generic_solver_wrapper.rb lingeling instances/Sat_Data/bmc/bmc08-50/abp4ptimoneg.k50.cnf SATISFIABLE 300.0 2147483647 9207562 -acts '2' -bate '1' -batewait '2' -bca '1' -bcawait '2' -bias '2' -blkrtc '0' -block '1' -blockwait '1' -bumpbcplits '0' -bumpbeforemin '1' -bumpclslits '0' -bumpseenlits '1' -card '1' -cardignonbin '0' -carduse '2' -cce '3' -ccewait '2' -cgrclsr '1' -cgrclsrwait '2' -cgrextand '1' -cgrexteq '1' -cgrextite '1' -cgrextunits '1' -cgrextxor '1' -cintincdiv '1' -cliff '1' -cliffwait '2' -compact '0' -deco '2' -decompose '1' -elim '1' -elmblk '0' -elmblkwait '1' -elmrtc '0' -elmsched2b2 '0' -elmschedprod '0' -elmschedpure '0' -elmschedsum '1' -factor '1' -flipping '1' -fliptop '1' -gauss '1' -gaussexptrn '1' -gaussextrall '1' -gausswait '2' -gluescale '4' -import '1' -inprocessing '1' -irrlim '1' -keepmaxglue '0' -lhbr '1' -lift '1' -liftwait '2' -lkhd '2' -lkhdmisifelmrtc '0' -minimize '2' -move '2' -otfs '1' -otfsbump '1' -otfsconf '1' -phase '0' -phaseflip '0' -plain '0' -prbasic '1' -prbasicrtc '0' -prbrtc '0' -prbsimple '2' -prbsimplertc '0' -probe '1' -psm '0' -randec '1' -rdp '1' -rdpwait '2' -redfixed '0' -redlbound '0' -reduce '2' -rephase '1' -restart '2' -restartintscale '0' -score '5' -simplify '2' -smallve '1' -smallvevars '10' -smallvewait '0' -sortlits '0' -synclsall '1' -ternres '1' -ternresrtc '0' -ternreswait '2' -transred '1' -transredwait '2' -treelook '1' -treelookfull '0' -treelooklrg '1' -treelookrtc '0' -trep '0' -unhdextstamp '1' -unhdhbr '0' -unhide '1' -unhidewait '2' -wait '1'
CSSC-LABS-300s-2day: cd /global/scratch/hutter/cssc/solvers; ruby ../scripts/generic_solver_wrapper.rb lingeling instances/Sat_Data/LABS/LABS_n025_goal004.cnf SATISFIABLE 300.0 2147483647 9207562 -acts '1' -bate '1' -batewait '2' -bca '1' -bcawait '0' -bias '1' -blkrtc '1' -block '0' -blockwait '0' -bumpbcplits '0' -bumpbeforemin '1' -bumpclslits '0' -bumpseenlits '1' -card '0' -cardignonbin '0' -carduse '2' -cce '2' -ccewait '0' -cgrclsr '0' -cgrclsrwait '1' -cgrextand '0' -cgrexteq '1' -cgrextite '0' -cgrextunits '0' -cgrextxor '0' -cintincdiv '1' -cliff '0' -cliffwait '0' -compact '2' -deco '1' -decompose '0' -elim '1' -elmblk '0' -elmblkwait '0' -elmrtc '1' -elmsched2b2 '0' -elmschedprod '1' -elmschedpure '0' -elmschedsum '1' -factor '2' -flipping '1' -fliptop '1' -gauss '0' -gaussexptrn '0' -gaussextrall '0' -gausswait '2' -gluescale '2' -import '1' -inprocessing '0' -irrlim '1' -keepmaxglue '1' -lhbr '1' -lift '1' -liftwait '1' -lkhd '1' -lkhdmisifelmrtc '1' -minimize '0' -move '3' -otfs '0' -otfsbump '1' -otfsconf '1' -phase '-1' -phaseflip '1' -plain '0' -prbasic '0' -prbasicrtc '1' -prbrtc '1' -prbsimple '2' -prbsimplertc '0' -probe '0' -psm '0' -randec '0' -rdp '0' -rdpwait '1' -redfixed '1' -redlbound '1' -reduce '2' -rephase '0' -restart '3' -restartintscale '1' -score '5' -simplify '1' -smallve '0' -smallvevars '6' -smallvewait '0' -sortlits '0' -synclsall '0' -ternres '0' -ternresrtc '0' -ternreswait '2' -transred '1' -transredwait '0' -treelook '1' -treelookfull '1' -treelooklrg '1' -treelookrtc '0' -trep '1' -unhdextstamp '1' -unhdhbr '1' -unhide '0' -unhidewait '1' -wait '1'
CSSC-K3-300s-2day: cd /global/scratch/hutter/cssc/solvers; ruby ../scripts/generic_solver_wrapper.rb lingeling instances/Sat_Data/K3-inst/k3-v275-c1172/unif-v275-c1172-797-S58452150.cnf UNSATISFIABLE 300.0 2147483647 9207562 -actavgmax '150' -actdblarithlim '0' -actgeomlim '9' -actgsdul '150' -acts '2' -actstdmax '187' -actstdmin '150' -actvlim '1610612736' -agile '11' -bate '0' -batewait '0' -bca '0' -bcamaxeff '1083741823' -bcaminuse '0' -bcawait '2' -bias '0' -blkboost '10000' -blkclslim '3' -blkmaxeff '2147483647' -blkmineff '25000000' -blkocclim '1073751822' -blkreleff '100' -blkrtc '0' -block '1' -blockwait '0' -bumpbcplits '1' -bumpbeforemin '1' -bumpclslits '1' -bumpseenlits '1' -card '0' -cardexpam1 '3' -cardglue '7' -cardignonbin '1' -cardmaxeff '20000000' -cardmaxlen '1000' -cardmineff '2147483647' -cardminlen '2147483647' -cardocclim '0' -cardreleff '0' -cardreschedint '10' -carduse '2' -cce '2' -ccemaxeff '-1' -ccemineff '3000000' -ccereleff '1' -ccewait '0' -cgrclsr '1' -cgrclsrwait '2' -cgreleff '0' -cgrextand '1' -cgrexteq '0' -cgrextite '1' -cgrextunits '1' -cgrextxor '1' -cgrmaxeff '3999999' -cgrmaxority '2' -cgrmineff '2147483647' -cintinc '1000000' -cintincdiv '2' -cliff '1' -cliffmaxeff '-973741824' -cliffmineff '10000000' -cliffreleff '10000' -cliffwait '1' -clim '1073741823' -compact '0' -deco '1' -decolim '1073741883' -decompose '1' -defragfree '50' -defragint '5000050' -delmax '5' -dlim '1610612735' -elim '1' -elmaxeff '1073741823' -elmblk '0' -elmblkwait '0' -elmboost '100' -elmclslim '501' -elmineff '1093741823' -elmlitslim '100' -elmocclim '1073751822' -elmplim1 '1' -elmplim2 '2' -elmreleff '5200' -elmroundlim '3' -elmrtc '0' -elmsched2b2 '0' -elmschedprod '0' -elmschedpure '1' -elmschedsum '0' -factmax '1073741833' -factor '1' -flipdur '10' -flipint '1073741833' -flipping '0' -fliptop '1' -flipvlim '2147483647' -force '1610612736' -gauss '1' -gaussexptrn '0' -gaussextrall '0' -gaussmaxeff '2147483647' -gaussmaxor '20' -gaussmineff '2147483647' -gaussreleff '5002' -gausswait '2' -gluekeep '0' -gluescale '1' -import '1' -inprocessing '1' -irrlim '1' -itsimpdel '10' -keepmaxglue '0' -lftmaxeff '20000000' -lftmineff '0' -lftreleff '5006' -lftroundlim '2' -lhbr '1' -lift '0' -liftwait '0' -lkhd '0' -lkhdmisifelmrtc '0' -maxglue '5000' -maxscorexp '253' -memlim '536870911' -minimize '1' -minlocalgluelim '0' -minrecgluelim '20' -mocint '500' -move '3' -otfs '0' -otfsbump '2' -otfsconf '0' -penmax '16' -phase '-1' -phaseflip '1' -phaseneginit '0' -plain '1' -prbasic '2' -prbasicmaxeff '100000000' -prbasicmineff '500000' -prbasicreleff '10000' -prbasicroundlim '9' -prbasicrtc '1' -prbrtc '0' -prbsimple '0' -prbsimpleboost '5' -prbsimpleliftdepth '6' -prbsimplemaxeff '-873741824' -prbsimplemineff '0' -prbsimplereleff '40' -prbsimplertc '1' -probe '0' -psm '0' -randec '1' -randecint '536871910' -rdp '1' -rdpclslim '0' -rdplim '200' -rdpmaxeff '200000000' -rdpmineff '0' -rdpreleff '5010' -rdpwait '0' -redfixed '1' -redinoutinc '100' -redlbound '1' -redlexpfac '1000' -redlinc '1000' -redlinit '100000000' -redlmaxabs '500005' -redlmaxinc '50199' -redlmaxrel '155' -redlminabs '500' -redlmininc '1' -redlminrel '1000' -redloutinc '5000' -redoutvlim '0' -reduce '4' -rephase '2' -rephaseinc '1' -restart '3' -restartint '3' -restartintscale '0' -rmincpen '4' -rstinoutinc '55' -scincinc '200' -score '3' -seed '1073741824' -simpdelay '2147483647' -simpen '18' -simpinterdelay '2000' -simpirrlim '1' -simplify '2' -simprtc '5' -sizemaxpen '20' -sizepen '1000000' -smallirr '0' -smallve '0' -smallvevars '5' -smallvewait '1' -sortlits '0' -subl '9' -synclsall '1' -synclsglue '8' -synclsint '50' -synclslen '40' -syncunint '1000000' -termint '0' -ternres '0' -ternresboost '100' -ternresrtc '1' -ternreswait '2' -transred '0' -transredwait '2' -trdmaxeff '-1071741824' -trdmineff '100000' -trdreleff '5' -treelook '1' -treelookboost '20' -treelookfull '1' -treelooklrg '0' -treelookmaxeff '-1023741824' -treelookmineff '0' -treelookreleff '0' -treelookrtc '0' -trep '0' -trepint '2147483647' -trnreleff '0' -trnrmaxeff '99999999' -trnrmineff '1077741823' -unhdextstamp '0' -unhdhbr '0' -unhdlnpr '2147483647' -unhdmaxeff '-1' -unhdmineff '0' -unhdreleff '1' -unhdroundlim '0' -unhide '1' -unhidewait '1' -wait '0'
CSSC-unsat-unif-k5-300s-2day: cd /global/scratch/hutter/cssc/solvers; ruby ../scripts/generic_solver_wrapper.rb lingeling instances/Sat_Data/unsat-unif-k5/unif-k5-r21.117-v50-c1056-S3376777782583961866.cnf UNSATISFIABLE 300.0 2147483647 9207562 -actavgmax '112' -actdblarithlim '1' -actgeomlim '15' -actgsdul '3' -acts '1' -actstdmax '56' -actstdmin '10' -actvlim '536870912' -agile '11' -bate '1' -batewait '2' -bca '1' -bcamaxeff '2147483647' -bcaminuse '100' -bcawait '2' -bias '0' -blkboost '10000' -blkclslim '1073742822' -blkmaxeff '1610612735' -blkmineff '50000000' -blkocclim '1073751822' -blkreleff '600' -blkrtc '0' -block '1' -blockwait '1' -bumpbcplits '0' -bumpbeforemin '0' -bumpclslits '1' -bumpseenlits '1' -card '0' -cardexpam1 '2147483647' -cardglue '-1' -cardignonbin '1' -cardmaxeff '20000000' -cardmaxlen '2147483647' -cardmineff '1074141823' -cardminlen '0' -cardocclim '50' -cardreleff '2' -cardreschedint '10' -carduse '0' -cce '2' -ccemaxeff '2147483647' -ccemineff '2147483647' -ccereleff '0' -ccewait '0' -cgrclsr '1' -cgrclsrwait '2' -cgreleff '10000' -cgrextand '0' -cgrexteq '0' -cgrextite '1' -cgrextunits '0' -cgrextxor '0' -cgrmaxeff '-1065741824' -cgrmaxority '30' -cgrmineff '100000' -cintinc '519995' -cintincdiv '2' -cliff '0' -cliffmaxeff '2147483647' -cliffmineff '10000000' -cliffreleff '5008' -cliffwait '2' -clim '1610612735' -compact '0' -deco '1' -decolim '0' -decompose '0' -defragfree '10' -defragint '1083741773' -delmax '5' -dlim '2147483647' -elim '0' -elmaxeff '536870911' -elmblk '0' -elmblkwait '1' -elmboost '100' -elmclslim '1073742822' -elmineff '20000000' -elmlitslim '2147483647' -elmocclim '2147483647' -elmplim1 '2147483647' -elmplim2 '5' -elmreleff '0' -elmroundlim '2147483647' -elmrtc '0' -elmsched2b2 '0' -elmschedprod '0' -elmschedpure '1' -elmschedsum '1' -factmax '2147483647' -factor '1' -flipdur '1' -flipint '2147483647' -flipping '1' -fliptop '1' -flipvlim '0' -force '2147483647' -gauss '0' -gaussexptrn '1' -gaussextrall '0' -gaussmaxeff '2147483647' -gaussmaxor '51' -gaussmineff '2147483647' -gaussreleff '2' -gausswait '1' -gluekeep '1' -gluescale '4' -import '0' -inprocessing '0' -irrlim '1' -itsimpdel '100000' -keepmaxglue '0' -lftmaxeff '-1053741824' -lftmineff '1074241823' -lftreleff '3' -lftroundlim '2' -lhbr '0' -lift '0' -liftwait '2' -lkhd '2' -lkhdmisifelmrtc '1' -maxglue '0' -maxscorexp '1073741824' -memlim '1610612735' -minimize '1' -minlocalgluelim '40' -minrecgluelim '1073741843' -mocint '500' -move '0' -otfs '1' -otfsbump '2' -otfsconf '1' -penmax '2' -phase '0' -phaseflip '0' -phaseneginit '0' -plain '0' -prbasic '1' -prbasicmaxeff '2147483647' -prbasicmineff '1000000' -prbasicreleff '5010' -prbasicroundlim '5' -prbasicrtc '1' -prbrtc '0' -prbsimple '0' -prbsimpleboost '1000' -prbsimpleliftdepth '10' -prbsimplemaxeff '-873741824' -prbsimplemineff '0' -prbsimplereleff '40' -prbsimplertc '1' -probe '1' -psm '2' -randec '0' -randecint '2' -rdp '2' -rdpclslim '2' -rdplim '80' -rdpmaxeff '99999999' -rdpmineff '0' -rdpreleff '5010' -rdpwait '2' -redfixed '1' -redinoutinc '50' -redlbound '1' -redlexpfac '510' -redlinc '1' -redlinit '4000' -redlmaxabs '1000000' -redlmaxinc '1' -redlmaxrel '10' -redlminabs '500' -redlmininc '50009' -redlminrel '10' -redloutinc '0' -redoutvlim '1000' -reduce '1' -rephase '1' -rephaseinc '10000' -restart '3' -restartint '5' -restartintscale '1' -rmincpen '4' -rstinoutinc '609' -scincinc '100' -score '5' -seed '1610612736' -simpdelay '1073741824' -simpen '24' -simpinterdelay '1073743823' -simpirrlim '1' -simplify '1' -simprtc '54' -sizemaxpen '15' -sizepen '1' -smallirr '90' -smallve '1' -smallvevars '6' -smallvewait '1' -sortlits '1' -subl '0' -synclsall '0' -synclsglue '2147483647' -synclsint '0' -synclslen '0' -syncunint '611111' -termint '0' -ternres '1' -ternresboost '3' -ternresrtc '1' -ternreswait '0' -transred '0' -transredwait '1' -trdmaxeff '-1' -trdmineff '1073841823' -trdreleff '5' -treelook '0' -treelookboost '10' -treelookfull '0' -treelooklrg '0' -treelookmaxeff '24999999' -treelookmineff '1074041823' -treelookreleff '5000' -treelookrtc '0' -trep '1' -trepint '27778' -trnreleff '1000' -trnrmaxeff '2147483647' -trnrmineff '1077741823' -unhdextstamp '0' -unhdhbr '1' -unhdlnpr '3' -unhdmaxeff '2147483647' -unhdmineff '0' -unhdreleff '3' -unhdroundlim '0' -unhide '0' -unhidewait '2' -wait '1'
CSSC-SWV-300s-2days: cd /global/scratch/hutter/cssc/solvers; ruby ../scripts/generic_solver_wrapper.rb lingeling instances/Sat_Data/bench/SW-verification/GZIP_v1.2.4__v1.1/gzip_vc1028.cnf SATISFIABLE 300.0 2147483647 9207562 -acts '1' -bate '0' -batewait '2' -bca '0' -bcawait '0' -bias '-1' -blkrtc '0' -block '0' -blockwait '0' -bumpbcplits '0' -bumpbeforemin '1' -bumpclslits '0' -bumpseenlits '1' -card '0' -cardignonbin '1' -carduse '0' -cce '2' -ccewait '0' -cgrclsr '1' -cgrclsrwait '1' -cgrextand '1' -cgrexteq '0' -cgrextite '0' -cgrextunits '0' -cgrextxor '0' -cintincdiv '0' -cliff '0' -cliffwait '0' -compact '0' -deco '1' -decompose '0' -elim '1' -elmblk '0' -elmblkwait '1' -elmrtc '0' -elmsched2b2 '0' -elmschedprod '1' -elmschedpure '0' -elmschedsum '0' -factor '0' -flipping '1' -fliptop '0' -gauss '0' -gaussexptrn '0' -gaussextrall '0' -gausswait '2' -gluescale '1' -import '0' -inprocessing '0' -irrlim '1' -keepmaxglue '1' -lhbr '0' -lift '0' -liftwait '2' -lkhd '1' -lkhdmisifelmrtc '1' -minimize '1' -move '1' -otfs '1' -otfsbump '0' -otfsconf '1' -phase '-1' -phaseflip '1' -plain '1' -prbasic '2' -prbasicrtc '0' -prbrtc '1' -prbsimple '0' -prbsimplertc '1' -probe '1' -psm '3' -randec '0' -rdp '0' -rdpwait '1' -redfixed '0' -redlbound '1' -reduce '1' -rephase '2' -restart '0' -restartintscale '1' -score '5' -simplify '0' -smallve '1' -smallvevars '8' -smallvewait '0' -sortlits '0' -synclsall '0' -ternres '1' -ternresrtc '1' -ternreswait '1' -transred '0' -transredwait '0' -treelook '2' -treelookfull '0' -treelooklrg '0' -treelookrtc '0' -trep '0' -unhdextstamp '0' -unhdhbr '1' -unhide '1' -unhidewait '1' -wait '1'