lingeling
  CSSC-IBM-300s-2day
	  python -u scripts/SATCSSCWrapper.py --mem-limit 3072 --script None --ext-callstring "ruby ./solvers/lingeling/callstring_generator.rb" --sat-checker ./scripts/SAT --sol-file ./instances/true_solubility.txt --log True instances/Sat_Data/bench/HW-verification/40randomsets/04_rule/SAT_dat.k75.cnf 0 300.0 2147483647 375162 -treelookrtc '0' -cce '3' -megaint '4' -redlminrel '10' -acts '2' -redfixed '0' -otfsconf '0' -redlmaxabs '1000000' -score '5' -rephase '1' -smallvevars '10' -plim '536870911' -keepmaxglue '1' -elmschedsum '1' -locscint '10000' -subl '9' -gaussreleff '2' -unhidewait '0' -flipvlim '100000' -itlocsdel '100' -elmsuccessrat '1000' -gaussmineff '2000000' -prbasicreleff '10' -elim '1' -cgrmaxeff '8000000' -redlmaxrel '300' -blkocclim1 '100000' -elmboost '40' -otfsbump '0' -irrlim '1' -locsboost '2' -binlocsdel '10' -blkocclim2 '10000' -blksmall '1' -ternres '1' -cardcut '2' -boost '1' -agile '1' -minrecgluelim '20' -blkrtc '0' -cgrmaxority '20' -redlbound '0' -bca '1' -mega '0' -sortlits '0' -treelookmaxeff '50000000' -seed '0' -cliff '1' -simpdelay '0' -simpvarchg '100' -maxscorexp '500' -ternreswait '2' -locsred '0' -phasegluebit '0' -trdmineff '100000' -elmclslim '1000000' -prbrtc '0' -prbasicmineff '1000000' -simpvarlim '100' -trdreleff '10' -fliplevels '6' -lftreleff '6' -elmocclim '1000000' -syncunint '111111' -actstdmax '112' -blkmaxeff '800000000' -redlminabs '500' -elmschedmin '0' -redoutclim '5000' -minimize '2' -flipint '10' -simpiscale '100' -unhdmaxeff '20000000' -redlinit '4000' -jwhred '1' -prbsimpleboost '10' -bumpclslits '0' -minlocalgluelim '30' -restartinit '0' -blklarge '1' -redlexpfac '10' -blkschedpure '1' -flipdur '10' -treelookmineff '300000' -cintmaxhard '10000000' -locsrtc '0' -tabrkeep '3' -rephaseinc '10000' -gaussmaxeff '50000000' -rdp '0' -agilesinint '100000' -elmreleff '200' -deco '1' -cceboostvlim '1000000' -elmblk '1' -tabrvfactor '4' -lkhd '2' -bva '0' -redlinc '1000' -blkboostvlim '1000000' -cliffwait '2' -trnrmineff '4000000' -bias '2' -cardignused '0' -liftlrg '3' -elmsuccesslim '1000' -actgeomlim '2' -gluescale '4' -ccemaxeff '2147483647' -cgrextunits '1' -ccertc '0' -transred '1' -inprocessing '1' -sizemaxpen '5' -rstinoutinc '110' -unhide '1' -elmroundlim '3' -redlmininc '10' -lftroundlim '5' -lftmaxeff '20000000' -prbsimple '2' -import '1' -decompose '1' -phaseflip '0' -psm '3' -pure '1' -prbsimplemaxeff '-1' -simpinterdelay '2000' -cardglue '0' -synclsall '1' -simpen '0' -factor '3' -trnreleff '10' -cceonlyifstuck '0' -bate '1' -cliffmineff '10000000' -phaseneginit '0' -cardexpam1 '3' -elmocclim2 '100' -elmocclim1 '1000' -cgrclsrwait '2' -cardreschedint '10' -prbasicmaxeff '100000000' -unhdreleff '2' -actavgmax '112' -elmsched2b2 '0' -cgrmineff '200000' -sizepen '1000000' -blkreleff '100' -lhbr '1' -smallve '1' -locs '0' -mocint '1000' -cardmaxeff '300000000' -elmschedpure '1' -scincinc '200' -cgreleff '1' -actgsdul '7' -bcawait '2' -blkschedmin '0' -liftwait '2' -agilelim '30' -cardminlen '3' -rdpmodelm '0' -cardwait '0' -gluekeep '3' -block '1' -blkschedsum '1' -delmax '10' -phase '0' -redinoutinc '100' -reduce '2' -prbasicroundlim '5' -cgrextite '1' -termint '122222' -actvlim '200000' -decolim '30' -incredcint '1' -blksuccesslim '10000' -lift '1' -trepint '55555' -force '0' -flipping '1' -cardocclim2 '15' -cintmaxsoft '1000000' -cardocclim1 '300' -actdblarithlim '3' -card '1' -cce3wait '2' -defragint '10000000' -treelooklrg '1' -synclslen '40' -wait '1' -blkclslim '1000000' -actstdmin '10' -ccewait '2' -locsclim '1000000' -otfs '1' -waitmax '4' -rdpmaxeff '10000000' -bkwdscale '2' -elmineff '0' -redoutvlim '1000' -penmax '4' -bcaminuse '100' -prbasicrtc '0' -tabr '3' -locsmaxeff '100000' -batewait '2' -bumpseenminsize '3' -redloutinc '10000' -bcamaxeff '10000000' -cgrclsr '1' -cardmaxlen '1000' -memlim '-1' -smallvewait '0' -ccereleff '20' -cliffmaxeff '100000000' -blkboost '10' -locsmineff '1000' -clim '-1' -rdpclslim '3' -elmfull '0' -restart '2' -locswait '2' -bumpseenbeforemin '1' -restartintscale '0' -synclsglue '8' -cardreleff '5' -cgrextxor '1' -cintincdiv '1' -rdplim '100' -elmlitslim '200' -simpidiv '3' -carduse '2' -gaussexptrn '1' -rdpmineff '10000' -unhdatrn '2' -gaussextrall '1' -synclsint '100' -rdpwait '2' -itsimpdel '20' -dlim '-1' -blksched2b2 '0' -compact '0' -elmrtc '0' -simprtc '5' -transredwait '2' -defragfree '50' -randec '0' -blockwait '1' -blkmineff '50000000' -factmax '100000' -unhdroundlim '20' -blksuccessrat '1000' -unhdhbr '0' -plain '0' -gaussmaxor '20' -randecint '1000' -treelook '1' -trep '0' -incredconfslim '0' -gauss '1' -lkhdmisifelmrtc '0' -bumpbcplits '0' -ternresrtc '0' -prbsimplereleff '40' -bumpseenaftermin '0' -cce2wait '1' -ccesuccesslim '10000' -gausswait '2' -prbsimplemineff '2000000' -cliffreleff '8' -cceboost '10' -restartint '5' -elmblkwait '1' -locset '2' -binsimpdel '2' -blkocclim '1000000' -treelookboost '20' -unhdmineff '100000' -ternresboost '5' -cgrexteq '1' -prbasic '1' -bumpseenlits '1' -rmincpen '4' -maxglue '2147483647' -prbsimplertc '0' -ccemineff '30000000' -elmschediff '0' -locsvared '100' -cintinc '20000' -incsavevisits '0' -fliptop '1' -randecflipint '0' -flipldmod '4' -treelookreleff '1' -unhdextstamp '1' -trnrmaxeff '200000000' -blkschedprod '0' -ccesuccessrat '1000' -rdpreleff '2' -smallirr '90' -unhdlnpr '3' -locsdec '2' -tabrcfactor '2' -megawait '2' -prbsimpleliftdepth '2' -trdmaxeff '2000000' -move '2' -cgrextand '1' -cardmineff '2000000' -elmschedprod '0' -lftmineff '500000' -reusetrail '1' -locsreleff '5' -redlmaxinc '200' -treelookfull '0' -elmaxeff '800000000' -saturating '70' -probe '1' -locsexport '1' -simplify '2' 
  CSSC-CircuitFuzz-300s-2day
	  python -u scripts/SATCSSCWrapper.py --mem-limit 3072 --script None --ext-callstring "ruby ./solvers/lingeling/callstring_generator.rb" --sat-checker ./scripts/SAT --sol-file ./instances/true_solubility.txt --log True instances/Sat_Data/circuit_fuzz/fuzz_100_6463.cnf UNSATISFIABLE 300.0 2147483647 375162 -treelookrtc '0' -cce '3' -megaint '4' -redlminrel '10' -acts '2' -redfixed '0' -otfsconf '0' -redlmaxabs '1000000' -score '5' -rephase '1' -smallvevars '10' -plim '-1' -keepmaxglue '1' -elmschedsum '1' -locscint '10000' -subl '9' -gaussreleff '2' -unhidewait '0' -flipvlim '100000' -itlocsdel '100' -elmsuccessrat '1000' -gaussmineff '2000000' -prbasicreleff '10' -elim '1' -cgrmaxeff '8000000' -redlmaxrel '300' -blkocclim1 '100000' -elmboost '40' -otfsbump '0' -irrlim '1' -locsboost '2' -binlocsdel '10' -blkocclim2 '10000' -blksmall '1' -ternres '1' -cardcut '2' -boost '1' -agile '1' -minrecgluelim '20' -blkrtc '0' -cgrmaxority '20' -redlbound '0' -bca '1' -mega '0' -sortlits '0' -treelookmaxeff '50000000' -seed '0' -cliff '1' -simpdelay '0' -simpvarchg '100' -maxscorexp '500' -ternreswait '2' -locsred '0' -phasegluebit '0' -trdmineff '100000' -elmclslim '1000000' -prbrtc '0' -prbasicmineff '1000000' -simpvarlim '100' -trdreleff '10' -fliplevels '21' -lftreleff '6' -elmocclim '1000000' -syncunint '111111' -actstdmax '112' -blkmaxeff '800000000' -redlminabs '500' -elmschedmin '0' -redoutclim '5000' -minimize '2' -flipint '10' -simpiscale '100' -unhdmaxeff '20000000' -redlinit '4000' -jwhred '1' -prbsimpleboost '10' -bumpclslits '0' -minlocalgluelim '30' -restartinit '0' -blklarge '1' -redlexpfac '10' -blkschedpure '1' -flipdur '10' -treelookmineff '300000' -cintmaxhard '4999999' -locsrtc '0' -tabrkeep '3' -rephaseinc '10000' -gaussmaxeff '50000000' -rdp '0' -agilesinint '100000' -elmreleff '200' -deco '1' -cceboostvlim '1000000' -elmblk '1' -tabrvfactor '4' -lkhd '2' -bva '0' -redlinc '1000' -blkboostvlim '1000000' -cliffwait '2' -trnrmineff '4000000' -bias '2' -cardignused '0' -liftlrg '3' -elmsuccesslim '1000' -actgeomlim '2' -gluescale '4' -ccemaxeff '2147483647' -cgrextunits '1' -ccertc '0' -transred '1' -inprocessing '1' -sizemaxpen '5' -rstinoutinc '110' -unhide '1' -elmroundlim '3' -redlmininc '10' -lftroundlim '5' -lftmaxeff '20000000' -prbsimple '2' -import '1' -decompose '1' -phaseflip '0' -psm '3' -pure '1' -prbsimplemaxeff '200000000' -simpinterdelay '2000' -cardglue '0' -synclsall '1' -simpen '0' -factor '3' -trnreleff '10' -cceonlyifstuck '0' -bate '1' -cliffmineff '1083741823' -phaseneginit '0' -cardexpam1 '3' -elmocclim2 '100' -elmocclim1 '1000' -cgrclsrwait '2' -cardreschedint '10' -prbasicmaxeff '100000000' -unhdreleff '2' -actavgmax '112' -elmsched2b2 '0' -cgrmineff '200000' -sizepen '1' -blkreleff '100' -lhbr '1' -smallve '1' -locs '0' -mocint '1000' -cardmaxeff '300000000' -elmschedpure '1' -scincinc '100' -cgreleff '1' -actgsdul '3' -bcawait '2' -blkschedmin '0' -liftwait '2' -agilelim '30' -cardminlen '3' -rdpmodelm '0' -cardwait '0' -gluekeep '3' -block '1' -blkschedsum '1' -delmax '10' -phase '0' -redinoutinc '100' -reduce '2' -prbasicroundlim '5' -cgrextite '1' -termint '122222' -actvlim '200000' -decolim '0' -incredcint '1' -blksuccesslim '10000' -lift '1' -trepint '55555' -force '0' -flipping '1' -cardocclim2 '15' -cintmaxsoft '1000000' -cardocclim1 '300' -actdblarithlim '3' -card '1' -cce3wait '2' -defragint '10000000' -treelooklrg '1' -synclslen '40' -wait '1' -blkclslim '1000000' -actstdmin '0' -ccewait '2' -locsclim '1000000' -otfs '1' -waitmax '4' -rdpmaxeff '10000000' -bkwdscale '2' -elmineff '20000000' -redoutvlim '1000' -penmax '4' -bcaminuse '100' -prbasicrtc '0' -tabr '3' -locsmaxeff '100000' -batewait '2' -bumpseenminsize '3' -redloutinc '10000' -bcamaxeff '10000000' -cgrclsr '1' -cardmaxlen '1000' -memlim '-1' -smallvewait '0' -ccereleff '20' -cliffmaxeff '100000000' -blkboost '10' -locsmineff '1000' -clim '1073741823' -rdpclslim '3' -elmfull '0' -restart '2' -locswait '1' -bumpseenbeforemin '1' -restartintscale '0' -synclsglue '8' -cardreleff '5' -cgrextxor '1' -cintincdiv '1' -rdplim '100' -elmlitslim '200' -simpidiv '3' -carduse '2' -gaussexptrn '1' -rdpmineff '10000' -unhdatrn '2' -gaussextrall '1' -synclsint '100' -rdpwait '2' -itsimpdel '20' -dlim '-1' -blksched2b2 '0' -compact '0' -elmrtc '0' -simprtc '5' -transredwait '2' -defragfree '50' -randec '0' -blockwait '1' -blkmineff '50000000' -factmax '100000' -unhdroundlim '20' -blksuccessrat '1000' -unhdhbr '0' -plain '0' -gaussmaxor '20' -randecint '1000' -treelook '1' -trep '0' -incredconfslim '0' -gauss '1' -lkhdmisifelmrtc '0' -bumpbcplits '0' -ternresrtc '0' -prbsimplereleff '40' -bumpseenaftermin '0' -cce2wait '1' -ccesuccesslim '10000' -gausswait '2' -prbsimplemineff '2000000' -cliffreleff '8' -cceboost '10' -restartint '5' -elmblkwait '1' -locset '2' -binsimpdel '2' -blkocclim '1000000' -treelookboost '20' -unhdmineff '100000' -ternresboost '5' -cgrexteq '1' -prbasic '1' -bumpseenlits '1' -rmincpen '4' -maxglue '2147483647' -prbsimplertc '0' -ccemineff '30000000' -elmschediff '0' -locsvared '100' -cintinc '1000000' -incsavevisits '0' -fliptop '1' -randecflipint '0' -flipldmod '4' -treelookreleff '1' -unhdextstamp '1' -trnrmaxeff '200000000' -blkschedprod '0' -ccesuccessrat '1000' -rdpreleff '2' -smallirr '90' -unhdlnpr '3' -locsdec '2' -tabrcfactor '2' -megawait '2' -prbsimpleliftdepth '2' -trdmaxeff '2000000' -move '2' -cgrextand '1' -cardmineff '2000000' -elmschedprod '0' -lftmineff '500000' -reusetrail '1' -locsreleff '5' -redlmaxinc '200' -treelookfull '0' -elmaxeff '800000000' -saturating '70' -probe '1' -locsexport '1' -simplify '2' 
  CSSC-BMC08-300s-2day
	  python -u scripts/SATCSSCWrapper.py --mem-limit 3072 --script None --ext-callstring "ruby ./solvers/lingeling/callstring_generator.rb" --sat-checker ./scripts/SAT --sol-file ./instances/true_solubility.txt --log True instances/Sat_Data/bmc/bmc08-50/abp4ptimoneg.k50.cnf SATISFIABLE 300.0 2147483647 375162 -treelookrtc '0' -cce '3' -megaint '4' -redlminrel '10' -acts '2' -redfixed '0' -otfsconf '0' -redlmaxabs '1000000' -score '5' -rephase '1' -smallvevars '10' -plim '-1' -keepmaxglue '1' -elmschedsum '1' -locscint '10000' -subl '9' -gaussreleff '2' -unhidewait '0' -flipvlim '100000' -itlocsdel '100' -elmsuccessrat '1000' -gaussmineff '2000000' -prbasicreleff '10' -elim '1' -cgrmaxeff '8000000' -redlmaxrel '300' -blkocclim1 '100000' -elmboost '40' -otfsbump '0' -irrlim '1' -locsboost '2' -binlocsdel '10' -blkocclim2 '10000' -blksmall '1' -ternres '1' -cardcut '2' -boost '1' -agile '1' -minrecgluelim '20' -blkrtc '0' -cgrmaxority '2' -redlbound '0' -bca '1' -mega '0' -sortlits '0' -treelookmaxeff '50000000' -seed '0' -cliff '0' -simpdelay '0' -simpvarchg '100' -maxscorexp '500' -ternreswait '2' -locsred '0' -phasegluebit '0' -trdmineff '100000' -elmclslim '1000000' -prbrtc '0' -prbasicmineff '1000000' -simpvarlim '100' -trdreleff '10' -fliplevels '6' -lftreleff '6' -elmocclim '1000000' -syncunint '111111' -actstdmax '112' -blkmaxeff '800000000' -redlminabs '500' -elmschedmin '0' -redoutclim '5000' -minimize '2' -flipint '10' -simpiscale '100' -unhdmaxeff '20000000' -redlinit '4000' -jwhred '1' -prbsimpleboost '10' -bumpclslits '0' -minlocalgluelim '30' -restartinit '0' -blklarge '1' -redlexpfac '10' -blkschedpure '1' -flipdur '10' -treelookmineff '300000' -cintmaxhard '10000000' -locsrtc '0' -tabrkeep '3' -rephaseinc '10000' -gaussmaxeff '50000000' -rdp '0' -agilesinint '100000' -elmreleff '200' -deco '1' -cceboostvlim '1000000' -elmblk '1' -tabrvfactor '4' -lkhd '2' -bva '0' -redlinc '1000' -blkboostvlim '1000000' -cliffwait '2' -trnrmineff '4000000' -bias '2' -cardignused '0' -liftlrg '3' -elmsuccesslim '1000' -actgeomlim '2' -gluescale '4' -ccemaxeff '2147483647' -cgrextunits '1' -ccertc '0' -transred '1' -inprocessing '1' -sizemaxpen '5' -rstinoutinc '110' -unhide '1' -elmroundlim '3' -redlmininc '5' -lftroundlim '2' -lftmaxeff '20000000' -prbsimple '2' -import '1' -decompose '1' -phaseflip '0' -psm '3' -pure '1' -prbsimplemaxeff '200000000' -simpinterdelay '2000' -cardglue '0' -synclsall '1' -simpen '0' -factor '3' -trnreleff '10' -cceonlyifstuck '0' -bate '1' -cliffmineff '10000000' -phaseneginit '0' -cardexpam1 '3' -elmocclim2 '100' -elmocclim1 '1000' -cgrclsrwait '2' -cardreschedint '10' -prbasicmaxeff '100000000' -unhdreleff '2' -actavgmax '112' -elmsched2b2 '0' -cgrmineff '200000' -sizepen '1000000' -blkreleff '100' -lhbr '1' -smallve '1' -locs '0' -mocint '1000' -cardmaxeff '300000000' -elmschedpure '1' -scincinc '200' -cgreleff '1' -actgsdul '7' -bcawait '2' -blkschedmin '0' -liftwait '2' -agilelim '30' -cardminlen '3' -rdpmodelm '0' -cardwait '0' -gluekeep '3' -block '1' -blkschedsum '1' -delmax '10' -phase '0' -redinoutinc '100' -reduce '2' -prbasicroundlim '9' -cgrextite '1' -termint '122222' -actvlim '200000' -decolim '30' -incredcint '1' -blksuccesslim '10000' -lift '1' -trepint '55555' -force '0' -flipping '1' -cardocclim2 '15' -cintmaxsoft '1000000' -cardocclim1 '300' -actdblarithlim '3' -card '1' -cce3wait '2' -defragint '10000000' -treelooklrg '1' -synclslen '40' -wait '1' -blkclslim '1000000' -actstdmin '10' -ccewait '2' -locsclim '1000000' -otfs '1' -waitmax '4' -rdpmaxeff '10000000' -bkwdscale '2' -elmineff '20000000' -redoutvlim '1000' -penmax '4' -bcaminuse '100' -prbasicrtc '0' -tabr '3' -locsmaxeff '100000' -batewait '2' -bumpseenminsize '3' -redloutinc '10000' -bcamaxeff '10000000' -cgrclsr '1' -cardmaxlen '1000' -memlim '-1' -smallvewait '0' -ccereleff '20' -cliffmaxeff '100000000' -blkboost '10' -locsmineff '1000' -clim '2147483647' -rdpclslim '3' -elmfull '0' -restart '2' -locswait '2' -bumpseenbeforemin '1' -restartintscale '0' -synclsglue '8' -cardreleff '5' -cgrextxor '1' -cintincdiv '1' -rdplim '100' -elmlitslim '200' -simpidiv '3' -carduse '2' -gaussexptrn '1' -rdpmineff '10000' -unhdatrn '2' -gaussextrall '1' -synclsint '100' -rdpwait '2' -itsimpdel '20' -dlim '-1' -blksched2b2 '0' -compact '0' -elmrtc '0' -simprtc '5' -transredwait '2' -defragfree '50' -randec '0' -blockwait '1' -blkmineff '50000000' -factmax '100000' -unhdroundlim '20' -blksuccessrat '1000' -unhdhbr '0' -plain '0' -gaussmaxor '20' -randecint '1000' -treelook '1' -trep '0' -incredconfslim '0' -gauss '1' -lkhdmisifelmrtc '0' -bumpbcplits '0' -ternresrtc '0' -prbsimplereleff '40' -bumpseenaftermin '0' -cce2wait '1' -ccesuccesslim '10000' -gausswait '2' -prbsimplemineff '2000000' -cliffreleff '8' -cceboost '10' -restartint '5' -elmblkwait '1' -locset '2' -binsimpdel '2' -blkocclim '1000000' -treelookboost '20' -unhdmineff '100000' -ternresboost '5' -cgrexteq '1' -prbasic '1' -bumpseenlits '1' -rmincpen '4' -maxglue '2147483647' -prbsimplertc '0' -ccemineff '30000000' -elmschediff '0' -locsvared '100' -cintinc '20000' -incsavevisits '0' -fliptop '1' -randecflipint '0' -flipldmod '4' -treelookreleff '1' -unhdextstamp '1' -trnrmaxeff '200000000' -blkschedprod '0' -ccesuccessrat '1000' -rdpreleff '2' -smallirr '90' -unhdlnpr '0' -locsdec '2' -tabrcfactor '2' -megawait '2' -prbsimpleliftdepth '2' -trdmaxeff '2000000' -move '2' -cgrextand '1' -cardmineff '2000000' -elmschedprod '0' -lftmineff '500000' -reusetrail '1' -locsreleff '5' -redlmaxinc '200' -treelookfull '0' -elmaxeff '800000000' -saturating '70' -probe '1' -locsexport '1' -simplify '2' 

minisat-HACK-999ED-CSSC
  CSSC-IBM-300s-2day
	  python -u scripts/SATCSSCWrapper.py --mem-limit 3072 --script ./solvers/minisat_HACK_999ED_CSSC/minisat_HACK_999ED_CSSCWrapper.py --sat-checker ./scripts/SAT --sol-file ./instances/true_solubility.txt --log True instances/Sat_Data/bench/HW-verification/40randomsets/04_rule/SAT_dat.k75.cnf 0 300.0 2147483647 375162 -ccmin-mode '2' -lbd-cut '5' -luby '0' -core-tolerance '0.02' -K-val '0.7' -cla-decay '0.995' -cp-increase '15000' -lbd-cut-max '9' -R-val '1.4' 
  CSSC-CircuitFuzz-300s-2day
	  python -u scripts/SATCSSCWrapper.py --mem-limit 3072 --script ./solvers/minisat_HACK_999ED_CSSC/minisat_HACK_999ED_CSSCWrapper.py --sat-checker ./scripts/SAT --sol-file ./instances/true_solubility.txt --log True instances/Sat_Data/circuit_fuzz/fuzz_100_6463.cnf UNSATISFIABLE 300.0 2147483647 375162 -ccmin-mode '2' -lbd-cut '6' -luby '0' -core-tolerance '0.01' -K-val '0.7' -cla-decay '0.995' -cp-increase '5000' -lbd-cut-max '9' -R-val '1.4' 
  CSSC-BMC08-300s-2day
	  python -u scripts/SATCSSCWrapper.py --mem-limit 3072 --script ./solvers/minisat_HACK_999ED_CSSC/minisat_HACK_999ED_CSSCWrapper.py --sat-checker ./scripts/SAT --sol-file ./instances/true_solubility.txt --log True instances/Sat_Data/bmc/bmc08-50/abp4ptimoneg.k50.cnf SATISFIABLE 300.0 2147483647 375162 -ccmin-mode '2' -lbd-cut '5' -luby '0' -core-tolerance '0.02' -K-val '0.7' -cla-decay '0.999' -cp-increase '15000' -lbd-cut-max '10' -R-val '1.4' 

clasp-3.0.4-p8
  CSSC-IBM-300s-2day
	  python -u scripts/SATCSSCWrapper.py --mem-limit 3072 --script ./solvers/clasp-cssc/claspCSSCWrapper.py --sat-checker ./scripts/SAT --sol-file ./instances/true_solubility.txt --log True instances/Sat_Data/bench/HW-verification/40randomsets/04_rule/SAT_dat.k75.cnf 0 300.0 2147483647 375162 -@1:F:update-act 'no' -@1:1:del-init '3.0' -@1:S:deletion 'yes' -@1:F:local-restarts 'no' -@1:1:del-grow '1.1' -@1:2:del-glue '0' -@0:4:sat-prepro '100' -@1:F:sign-fix 'no' -@0:S:sat-prepro 'yes' -@1:otfs '1' -@1:counter-restarts '3' -@1:rand-freq '0.0' -@1:update-lbd '3' -@1:3:deletion '0' -@1:0:strengthen 'local' -@1:1:lookahead 'no' -@1:del-max '250000' -@1:3:del-init '9000' -@1:save-progress '136' -@0:1:sat-prepro '10' -@1:contraction '250' -@0:5:sat-prepro '0' -@1:S:counterCond 'yes' -@1:init-watches '0' -@1:del-on-restart '0' -@1:1:deletion 'basic' -@1:S:del-grow 'yes' -@1:vsids-decay '92' -@1:S:contraction 'yes' -@1:sign-def '2' -@0:2:sat-prepro '9' -@1:0:del-cfl 'no' -@1:1:del-glue '2' -@1:2:del-grow '20.0' -@1:2:del-init '1000' -@1:counter-bump '10' -@1:reverse-arcs '1' -@1:0:restarts 'F' -@1:S:growSched 'no' -@1:heuristic 'Vsids' -@0:3:sat-prepro '-1' -@1:1:Simp:restarts '7651' -@1:2:deletion '75' -@1:F:init-moms 'yes' -@1:1:strengthen '0' 
  CSSC-CircuitFuzz-300s-2day
	  python -u scripts/SATCSSCWrapper.py --mem-limit 3072 --script ./solvers/clasp-cssc/claspCSSCWrapper.py --sat-checker ./scripts/SAT --sol-file ./instances/true_solubility.txt --log True instances/Sat_Data/circuit_fuzz/fuzz_100_6463.cnf UNSATISFIABLE 300.0 2147483647 375162 -@1:F:update-act 'no' -@1:1:del-init '3.0' -@1:S:deletion 'yes' -@1:F:local-restarts 'yes' -@1:1:del-grow '1.1' -@1:2:del-glue '0' -@1:2:Geo:restarts '1.5' -@0:4:sat-prepro '100' -@1:F:sign-fix 'yes' -@0:S:sat-prepro 'yes' -@1:otfs '2' -@1:counter-restarts '3' -@1:rand-freq '0.0' -@1:update-lbd '1' -@1:3:deletion '0' -@1:0:strengthen 'recursive' -@1:1:lookahead 'atom' -@1:del-max '250000' -@1:3:del-init '9000' -@1:save-progress '180' -@0:1:sat-prepro '10' -@1:contraction '250' -@0:5:sat-prepro '1' -@1:S:counterCond 'yes' -@1:init-watches '2' -@1:del-on-restart '0' -@1:1:deletion 'basic' -@1:S:del-grow 'yes' -@1:vsids-decay '95' -@1:S:contraction 'yes' -@1:sign-def '1' -@0:2:sat-prepro '25' -@1:0:del-cfl 'no' -@1:1:del-glue '2' -@1:2:del-grow '20.0' -@1:2:del-init '1000' -@1:counter-bump '10' -@1:reverse-arcs '0' -@1:0:restarts 'x' -@1:S:Geo:aryrestarts '2' -@1:2:lookahead '1' -@1:S:growSched 'no' -@1:heuristic 'Vsids' -@0:3:sat-prepro '-1' -@1:1:Simp:restarts '128' -@1:2:deletion '75' -@1:F:init-moms 'no' -@1:1:strengthen '0' 
  CSSC-BMC08-300s-2day
	  python -u scripts/SATCSSCWrapper.py --mem-limit 3072 --script ./solvers/clasp-cssc/claspCSSCWrapper.py --sat-checker ./scripts/SAT --sol-file ./instances/true_solubility.txt --log True instances/Sat_Data/bmc/bmc08-50/abp4ptimoneg.k50.cnf SATISFIABLE 300.0 2147483647 375162 -@1:F:update-act 'yes' -@1:1:del-init '3.0' -@1:S:deletion 'yes' -@1:F:local-restarts 'no' -@1:1:del-grow '1.1' -@1:2:del-glue '0' -@0:4:sat-prepro '100' -@1:F:sign-fix 'no' -@0:S:sat-prepro 'yes' -@1:otfs '2' -@1:rand-freq '0.01' -@1:update-lbd '2' -@1:3:deletion '0' -@1:0:strengthen 'no' -@1:1:lookahead 'body' -@1:del-max '901714858' -@1:3:del-init '9000' -@1:save-progress '180' -@0:1:sat-prepro '10' -@1:contraction '250' -@0:5:sat-prepro '1' -@1:S:counterCond 'no' -@1:init-watches '1' -@1:del-on-restart '0' -@1:S:Dyn:aryrestarts '2' -@1:1:deletion 'basic' -@1:S:del-grow 'yes' -@1:vsids-decay '96' -@1:S:contraction 'yes' -@1:sign-def '3' -@0:2:sat-prepro '25' -@1:0:del-cfl 'no' -@1:1:Dyn:restarts '100' -@1:1:del-glue '2' -@1:2:del-grow '40.654454297154885' -@1:2:Dyn:restarts '0.7' -@1:3:Dyn:restarts '30' -@1:2:del-init '191' -@1:reverse-arcs '2' -@1:0:restarts 'D' -@1:2:lookahead '1' -@1:S:growSched 'no' -@1:heuristic 'Vsids' -@0:3:sat-prepro '-1' -@1:2:deletion '75' -@1:F:init-moms 'yes' 

Riss-4.27
  CSSC-IBM-300s-2day
	  python -u scripts/SATCSSCWrapper.py --mem-limit 3072 --script ./solvers/riss427/rissWrapper.py --sat-checker ./scripts/SAT --sol-file ./instances/true_solubility.txt --log True instances/Sat_Data/bench/HW-verification/40randomsets/04_rule/SAT_dat.k75.cnf 0 300.0 2147483647 375162 -cp3_uhdUHTE 'yes' -cp3_uhdTrans 'yes' -cce 'no' -sUhdPrRb 'no' -quickRed 'no' -agil-r 'yes' -ics_dyn 'no' -ics_relSIZE '1.0' -szLBDQueue '60' -hack '1' -bve_gates 'yes' -otfss 'no' -longConflict 'no' -firstReduceDB '4000' -subsimp 'yes' -3resolve 'no' -cp3_vars '5000000' -biAsserting 'no' -laEEp '0' -cp3_inp_cons '1000000' -ics_shrinkNew 'no' -laEEl 'yes' -sUHLEsize '8' -bve_BCElim 'yes' -cp3_uhdUHLE '3' -pr-keepL '0' -sls 'no' -pr-keepI '0' -bce 'yes' -var-decay-i '0.001' -K '0.8' -cp3_bve_heap '0' -vsids-s '1.0' -R '1.2' -cp3_str_limit '300000000' -dontTrust 'no' -pr-lhbr 'no' -learnDecP '100' -pr-double 'no' -var-decay-e '0.99' -xor 'no' -bve_cgrow '0' -var-decay-d '15000' -cp3_sub_limit '300000000' -var-decay-b '0.95' -lbdupd '0' -ics_processLast '5050' -minSizeMinimizingClause '30' -szTrailQueue '3500' -sUhdPrSh '0' -incReduceDB '450' -ics_window '5050' -bve_red_lits '1' -pr-uips '-1' -agil-limit '0.22' -cp3_strength 'yes' -agil-init '0.11' -dyn 'yes' -enabled_cp3 'yes' -cp3_uhdIters '5' -hlabound '-1' -pr-nce 'no' -bve_cgrow_t '0' -cp3_limited 'yes' -bce-bce 'no' -bva 'no' -minLBDMinimizingClause '3' -pr-probeL '5000000' -bve 'yes' -keepWorst '0.001' -ics 'yes' -incLBD 'no' -up 'yes' -lbdIgnL0 'yes' -hack-cost 'no' -rer 'no' -vsids-e '1.0' -ee 'no' -lhbr-sub 'yes' -vsids-d '2147483647' -vsids-i '1.0' -bce-cle 'yes' -rMax '-1' -specialIncReduceDB '2000' -dense 'yes' -hlaTop '512' -symm 'no' -cp3_iters '1' -cp3_bve_limit '25000000' -agil-add '128' -tabu 'yes' -hlaevery '32' -init-act '3' -varActB '0' -unhide 'yes' -sInterval '0' -phase-saving '2' -bve_totalG 'no' -cp3_uhdProbe '0' -fm 'no' -sUHLElbd '12' -ics_relLBD '1.0' -alluiphack '2' -hlaMax '50' -rtype '0' -rate 'no' -hte 'no' -hlaLevel '1' -sUhdProbe '2' -actStart '1024.0' -all_strength_res '0' -minLBDFrozenClause '15' -agil-decay '0.9999' -cla-decay '0.999' -cp3_ee_bIter '400000000' -ics_keepNew 'no' -cp3_uhdEE 'yes' -probe 'no' -laHack 'yes' -cp3_cls '30000000' -inprocess 'no' -rlevel '1' -bce-limit '100000000' -clsActB '1' -lhbr-max '2147483647' -init-pol '0' -lhbr '3' -rnd-freq '0.005' 
  CSSC-CircuitFuzz-300s-2day
	  python -u scripts/SATCSSCWrapper.py --mem-limit 3072 --script ./solvers/riss427/rissWrapper.py --sat-checker ./scripts/SAT --sol-file ./instances/true_solubility.txt --log True instances/Sat_Data/circuit_fuzz/fuzz_100_6463.cnf UNSATISFIABLE 300.0 2147483647 375162 -cp3_fm_vMulAMO 'no' -cp3_uhdUHTE 'yes' -cp3_uhdTrans 'yes' -cce 'no' -sUhdPrRb 'no' -quickRed 'yes' -agil-r 'no' -szLBDQueue '60' -hack '0' -cp3_fm_maxA '200' -bve_gates 'yes' -otfss 'no' -longConflict 'no' -firstReduceDB '4000' -subsimp 'no' -3resolve 'no' -cp3_fm_keepM 'yes' -cp3_vars '5000000' -biAsserting 'no' -laEEp '0' -cp3_inp_cons '500000' -laEEl 'yes' -cp3_fm_maxConstraints '200000' -card_max '2' -sUHLEsize '30' -bve_BCElim 'yes' -cp3_uhdUHLE '3' -cp3_fm_limit '6000000' -pr-keepL '2' -sls 'no' -pr-keepI '0' -bce 'yes' -var-decay-i '0.01' -K '0.8' -cp3_bve_heap '0' -card_maxC '7' -vsids-s '1.0' -R '1.2' -dontTrust 'no' -pr-lhbr 'no' -cp3_fm_grow '40' -learnDecP '80' -pr-double 'yes' -var-decay-e '0.99' -xor 'no' -bve_cgrow '0' -var-decay-d '10000' -var-decay-b '0.85' -card_minC '3' -lbdupd '1' -minSizeMinimizingClause '15' -szTrailQueue '3500' -cp3_fm_growT '100000' -sUhdPrSh '0' -incReduceDB '300' -bve_red_lits '1' -pr-uips '0' -dyn 'yes' -enabled_cp3 'yes' -cp3_uhdIters '5' -hlabound '-1' -pr-nce 'no' -bve_cgrow_t '0' -cp3_limited 'yes' -cp3_fm_newAlo '2' -bce-bce 'no' -bva 'no' -minLBDMinimizingClause '6' -pr-probeL '5000000' -bve 'yes' -keepWorst '0.001' -ics 'no' -incLBD 'no' -up 'no' -lbdIgnL0 'yes' -rer 'no' -vsids-e '1.0' -ee 'no' -card_Elimit '1200000' -lhbr-sub 'yes' -vsids-d '2147483647' -vsids-i '1.0' -bce-cle 'yes' -cp3_fm_newAmo '2' -rMax '-1' -cp3_fm_Slimit '12000000' -specialIncReduceDB '1000' -dense 'no' -hlaTop '512' -symm 'no' -cp3_iters '1' -cp3_bve_limit '25000000' -tabu 'yes' -hlaevery '32' -init-act '1' -varActB '0' -unhide 'yes' -sInterval '1' -phase-saving '2' -bve_totalG 'no' -cp3_uhdProbe '0' -fm 'yes' -sUHLElbd '12' -alluiphack '2' -hlaMax '50' -rtype '0' -rate 'no' -hte 'no' -hlaLevel '1' -sUhdProbe '1' -actStart '1024.0' -minLBDFrozenClause '30' -cla-decay '0.999' -cp3_ee_bIter '400000000' -cp3_uhdEE 'yes' -probe 'no' -laHack 'yes' -cp3_cls '30000000' -inprocess 'no' -rlevel '1' -bce-limit '100000000' -cp3_fm_newAlk '2' -clsActB '2' -lhbr-max '2147483647' -init-pol '2' -lhbr '3' -rnd-freq '0.005' 
  CSSC-BMC08-300s-2day
	  python -u scripts/SATCSSCWrapper.py --mem-limit 3072 --script ./solvers/riss427/rissWrapper.py --sat-checker ./scripts/SAT --sol-file ./instances/true_solubility.txt --log True instances/Sat_Data/bmc/bmc08-50/abp4ptimoneg.k50.cnf SATISFIABLE 300.0 2147483647 375162 -rer-minLBD '15' -sUhdPrRb 'yes' -quickRed 'yes' -agil-r 'yes' -minLBDMinimizingClause '9' -pr-probeL '500000' -szLBDQueue '70' -hack '1' -otfss 'no' -longConflict 'no' -keepWorst '0.001' -firstReduceDB '8000' -ics 'no' -incLBD 'yes' -rer-maxLBD '15' -rer-max-size '2' -lbdIgnL0 'yes' -hack-cost 'yes' -rer 'yes' -vsids-e '1.0' -lhbr-sub 'no' -vsids-d '2147483647' -biAsserting 'yes' -vsids-i '1.0' -rMax '-1' -rer-freq '1.0' -specialIncReduceDB '1000' -rer-r '0' -sUHLEsize '0' -agil-add '32' -init-act '3' -pr-keepL '2' -varActB '1' -pr-keepI '0' -sInterval '2' -phase-saving '2' -var-decay-i '0.01' -rer-l 'no' -K '0.8' -alluiphack '2' -rer-f 'yes' -rer-min-size '2' -rtype '0' -vsids-s '1.0' -R '1.5' -dontTrust 'yes' -pr-lhbr 'no' -sUhdProbe '1' -learnDecP '-1' -pr-double 'yes' -var-decay-e '0.99' -var-decay-d '15000' -var-decay-b '0.85' -actStart '2048.0' -lbdupd '0' -minLBDFrozenClause '30' -minSizeMinimizingClause '15' -agil-decay '0.9999' -rer-rn 'no' -szTrailQueue '4000' -cla-decay '0.999' -cp3_ee_bIter '400000000' -sUhdPrSh '4' -incReduceDB '300' -pr-uips '-1' -agil-limit '0.44' -laHack 'no' -biAsFreq '8' -rlevel '0' -agil-init '0.01' -enabled_cp3 'no' -clsActB '1' -lhbr-max '2147483647' -init-pol '1' -lhbr '3' -pr-nce 'yes' -rer-new-act '3' -rnd-freq '0' 

cryptominisat
  CSSC-IBM-300s-2day
	  python -u scripts/SATCSSCWrapper.py --mem-limit 3072 --script None --ext-callstring "ruby ./solvers/cryptominisat/callstring_generator.rb" --sat-checker ./scripts/SAT --sol-file ./instances/true_solubility.txt --log True instances/Sat_Data/bench/HW-verification/40randomsets/04_rule/SAT_dat.k75.cnf 0 300.0 2147483647 375162 -elimcoststrategy '0' -flippolf '0' -blkrestlen '4447' -calcpolarall '1' -dompickf '630' -freq '0.007952764044192847' -eratio '0.3378308335657559' -cachecutoff '2040' -cachesize '1392' -blkrestmultip '1.616462490539555' -calcpolar1st '0' -occredmax '171' -startclean '437' -clbtwsimp '2' -moreminimbin '86' -presimp '0' -updateglue '1' -cleanconflmult '0' -moreminimcache '546' -bva2lit '1' -lockuip '722' -restart 'glue' -perfmult '0.17508489465599686' -clean 'activity' -calcreach '1' -blkrest '1' -morebump '0' -viviffastmaxm '204' -viviflongmaxm '21' -incclean '1.3895828182615204' -gluehist '104' -ltclean '0.5197314748950986' -locktop '941' -sccperc '0.0076618491996387275' -burst '100' -probemaxm '1248' 
  CSSC-CircuitFuzz-300s-2day
	  python -u scripts/SATCSSCWrapper.py --mem-limit 3072 --script None --ext-callstring "ruby ./solvers/cryptominisat/callstring_generator.rb" --sat-checker ./scripts/SAT --sol-file ./instances/true_solubility.txt --log True instances/Sat_Data/circuit_fuzz/fuzz_100_6463.cnf UNSATISFIABLE 300.0 2147483647 375162 -elimcoststrategy '1' -flippolf '0' -blkrestlen '4849' -calcpolarall '0' -dompickf '9491' -freq '5.474823965577194E-5' -eratio '0.10200928223347491' -cachecutoff '1108' -cachesize '3885' -blkrestmultip '1.8498764669832206' -calcpolar1st '0' -occredmax '102' -startclean '12286' -clbtwsimp '5' -moreminimbin '65' -presimp '0' -updateglue '1' -cleanconflmult '1' -moreminimcache '101' -bva2lit '0' -lockuip '50' -restart 'glueagility' -perfmult '0.7745563937070647' -clean 'confdep' -calcreach '0' -blkrest '1' -morebump '1' -viviffastmaxm '102' -viviflongmaxm '5' -incclean '1.0240474891647424' -gluehist '265' -ltclean '0.6966893360266746' -locktop '1518' -sccperc '0.0012685992222550633' -burst '100' -probemaxm '3728' 
  CSSC-BMC08-300s-2day
	  python -u scripts/SATCSSCWrapper.py --mem-limit 3072 --script None --ext-callstring "ruby ./solvers/cryptominisat/callstring_generator.rb" --sat-checker ./scripts/SAT --sol-file ./instances/true_solubility.txt --log True instances/Sat_Data/bmc/bmc08-50/abp4ptimoneg.k50.cnf SATISFIABLE 300.0 2147483647 375162 -elimcoststrategy '1' -flippolf '0' -calcpolarall '1' -dompickf '1365' -freq '0.019290074427378723' -eratio '0.16635761338160282' -cachecutoff '1875' -cachesize '1084' -calcpolar1st '1' -occredmax '159' -startclean '6200' -clbtwsimp '2' -moreminimbin '173' -presimp '1' -updateglue '0' -cleanconflmult '0' -moreminimcache '309' -bva2lit '0' -lockuip '489' -restart 'glue' -perfmult '0.16717187573960673' -clean 'confdep' -calcreach '0' -blkrest '0' -morebump '1' -viviffastmaxm '220' -viviflongmaxm '54' -incclean '1.0312929369185146' -gluehist '108' -ltclean '0.3579850446605391' -locktop '455' -sccperc '0.05382648800362666' -burst '300' -probemaxm '3914' 

SparrowToRiss
  CSSC-IBM-300s-2day
	  python -u scripts/SATCSSCWrapper.py --mem-limit 3072 --script ./solvers/SparrowToRiss/StrWrapper.py --sat-checker ./scripts/SAT --sol-file ./instances/true_solubility.txt --log True instances/Sat_Data/bench/HW-verification/40randomsets/04_rule/SAT_dat.k75.cnf 0 300.0 2147483647 375162 -cp3_fm_vMulAMO 'no' -cp3_uhdUHTE 'yes' -cp3_uhdTrans 'yes' -cce 'no' -sUhdPrRb 'no' -quickRed 'no' -agil-r 'no' -szLBDQueue '60' -hack '1' -cp3_fm_maxA '200' -bve_gates 'yes' -SPARROW-k 'no' -otfss 'no' -longConflict 'no' -firstReduceDB '2192' -strSseconds '150' -subsimp 'no' -3resolve 'no' -cp3_fm_keepM 'yes' -cp3_vars '5000000' -biAsserting 'no' -laEEp '0' -cp3_inp_cons '500000' -laEEl 'yes' -cp3_fm_maxConstraints '200000' -card_max '2' -sUHLEsize '0' -bve_BCElim 'yes' -cp3_uhdUHLE '3' -cp3_fm_limit '6000000' -pr-keepL '0' -sls 'no' -pr-keepI '0' -bce 'yes' -var-decay-i '0.01' -K '0.8' -cp3_bve_heap '0' -SPARROW--randomc '0' -card_maxC '7' -vsids-s '1.0' -R '1.2' -dontTrust 'yes' -pr-lhbr 'yes' -SPARROW--luby '0' -cp3_fm_grow '40' -learnDecP '80' -pr-double 'yes' -var-decay-e '0.95' -xor 'no' -bve_cgrow '0' -var-decay-d '5000' -var-decay-b '0.75' -card_minC '3' -lbdupd '1' -minSizeMinimizingClause '28' -szTrailQueue '3500' -cp3_fm_growT '100000' -sUhdPrSh '0' -incReduceDB '431' -bve_red_lits '1' -pr-uips '0' -dyn 'yes' -enabled_cp3 'yes' -cp3_uhdIters '5' -hlabound '-1' -SPARROW--c1 '2.0' -pr-nce 'no' -bve_cgrow_t '0' -cp3_limited 'yes' -cp3_fm_newAlo '2' -bce-bce 'no' -bva 'no' -minLBDMinimizingClause '8' -pr-probeL '6726809' -bve 'yes' -keepWorst '0.020539666964070082' -ics 'no' -incLBD 'no' -up 'no' -lbdIgnL0 'yes' -hack-cost 'no' -rer 'no' -vsids-e '1.0' -ee 'no' -card_Elimit '1200000' -vsids-d '2147483647' -lhbr-sub 'yes' -vsids-i '1.0' -bce-cle 'yes' -cp3_fm_newAmo '2' -rMax '-1' -cp3_fm_Slimit '12000000' -specialIncReduceDB '1100' -SPARROW--sp '0.347' -dense 'no' -hlaTop '512' -symm 'no' -cp3_iters '1' -cp3_bve_limit '25000000' -tabu 'yes' -hlaevery '32' -init-act '1' -varActB '1' -unhide 'yes' -sInterval '1' -phase-saving '2' -bve_totalG 'no' -cp3_uhdProbe '0' -fm 'yes' -alluiphack '0' -hlaMax '50' -rtype '0' -rate 'no' -hte 'no' -hlaLevel '1' -sUhdProbe '1' -actStart '1024.0' -minLBDFrozenClause '30' -cla-decay '0.999' -cp3_ee_bIter '876' -cp3_uhdEE 'yes' -probe 'no' -laHack 'yes' -cp3_cls '30000000' -inprocess 'no' -rlevel '0' -strFlips '100000000' -bce-limit '100000000' -cp3_fm_newAlk '2' -clsActB '2' -lhbr-max '2147483647' -init-pol '0' -lhbr '3' -rnd-freq '0.005' 
  CSSC-CircuitFuzz-300s-2day
	  python -u scripts/SATCSSCWrapper.py --mem-limit 3072 --script ./solvers/SparrowToRiss/StrWrapper.py --sat-checker ./scripts/SAT --sol-file ./instances/true_solubility.txt --log True instances/Sat_Data/circuit_fuzz/fuzz_100_6463.cnf UNSATISFIABLE 300.0 2147483647 375162 -sUhdPrRb 'no' -quickRed 'yes' -agil-r 'no' -ics_dyn 'no' -ics_relSIZE '0.01' -minLBDMinimizingClause '5' -pr-probeL '2261805' -hack '0' -SPARROW-k 'no' -otfss 'yes' -longConflict 'no' -keepWorst '0.04782894641580293' -firstReduceDB '2873' -strSseconds '150' -ics 'yes' -incLBD 'yes' -rinc '1.6583835467172323' -lbdIgnL0 'no' -rer 'no' -vsids-e '1.0' -vsids-d '2147483647' -lhbr-sub 'yes' -biAsserting 'no' -vsids-i '1.0' -ics_shrinkNew 'no' -specialIncReduceDB '1000' -SPARROW--sp '0.5884802407553079' -sUHLEsize '30' -otfssMLDB '16' -init-act '2' -pr-keepL '0' -varActB '0' -pr-keepI '0' -sInterval '1' -phase-saving '2' -var-decay-i '0.01' -sUHLElbd '2' -ics_relLBD '0.01' -alluiphack '2' -SPARROW--randomc '1' -rtype '2' -vsids-s '1.0' -dontTrust 'yes' -otfssL 'no' -pr-lhbr 'yes' -SPARROW--luby '0' -sUhdProbe '1' -learnDecP '66' -pr-double 'no' -var-decay-e '0.99' -var-decay-d '15000' -var-decay-b '0.95' -actStart '2048.0' -lbdupd '1' -minLBDFrozenClause '15' -minSizeMinimizingClause '41' -ics_processLast '5050' -cla-decay '0.999' -cp3_ee_bIter '174631' -ics_keepNew 'no' -sUhdPrSh '2' -incReduceDB '439' -ics_window '200000' -pr-uips '0' -laHack 'no' -rlevel '1' -strFlips '1000000000' -enabled_cp3 'no' -SPARROW--c1 '4.4057474875830955' -clsActB '0' -lhbr-max '4096' -init-pol '2' -pr-nce 'no' -lhbr '3' -rnd-freq '0.008279881137777887' 
  CSSC-BMC08-300s-2day
	  python -u scripts/SATCSSCWrapper.py --mem-limit 3072 --script ./solvers/SparrowToRiss/StrWrapper.py --sat-checker ./scripts/SAT --sol-file ./instances/true_solubility.txt --log True instances/Sat_Data/bmc/bmc08-50/abp4ptimoneg.k50.cnf SATISFIABLE 300.0 2147483647 375162 -quickRed 'yes' -minLBDMinimizingClause '7' -pr-probeL '4733342' -hack '1' -SPARROW-k 'no' -longConflict 'no' -keepWorst '0.028358172129142156' -firstReduceDB '7800' -incLBD 'yes' -lbdIgnL0 'no' -hack-cost 'yes' -vsids-e '1.0' -vsids-d '2147483647' -biAsserting 'no' -vsids-i '1.0' -specialIncReduceDB '1100' -SPARROW--luby_base '468621.53482946195' -sUHLEsize '30' -init-act '3' -pr-keepL '0' -varActB '2' -pr-keepI '2' -sInterval '3' -phase-saving '2' -var-decay-i '0.01' -sUHLElbd '0' -alluiphack '0' -SPARROW--randomc '0' -vsids-s '1.0' -dontTrust 'no' -pr-lhbr 'yes' -SPARROW--luby '1' -learnDecP '80' -pr-double 'yes' -var-decay-e '0.95' -var-decay-d '10000' -var-decay-b '0.85' -actStart '1024.0' -lbdupd '1' -minLBDFrozenClause '30' -minSizeMinimizingClause '14' -cla-decay '0.5' -cp3_ee_bIter '109265051' -incReduceDB '369' -pr-uips '-1' -rlevel '2' -strFlips '-2' -SPARROW--c1 '7.259444170500145' -clsActB '2' -init-pol '1' -pr-nce 'yes' -rnd-freq '0.002237629829307388'