clasp-3.0.4-p8
  CSSC-LABS-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/LABS/LABS_n025_goal004.cnf SATISFIABLE 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' -@1:2:Geo:restarts '1.5' -@0:4:sat-prepro '100' -@1:F:sign-fix 'no' -@0:S:sat-prepro 'yes' -@1:otfs '2' -@1:rand-freq '0.0' -@1:update-lbd '0' -@1:3:deletion '0' -@1:0:strengthen 'local' -@1:1:lookahead 'no' -@1:del-max '250000' -@1:1:del-cfl '2000' -@1:2:A:del-cfl '100' -@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 '2' -@1:del-on-restart '0' -@1:1:deletion 'basic' -@1:3:del-cfl '15' -@1:S:del-grow 'yes' -@1:vsids-decay '95' -@1:sign-def '1' -@0:2:sat-prepro '25' -@1:0:del-cfl '+' -@1:1:del-glue '2' -@1:2:del-grow '20.0' -@1:2:del-init '1023' -@1:reverse-arcs '1' -@1:0:restarts 'x' -@1:S:Geo:aryrestarts '2' -@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-GI-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/GI/iso_m2D_s36.AB23.cnf SATISFIABLE 300.0 2147483647 375162 -@1:F:update-act 'yes' -@1:S:deletion 'no' -@1:F:local-restarts 'yes' -@1:del-grow '0' -@1:F:sign-fix 'no' -@0:S:sat-prepro 'no' -@1:otfs '0' -@1:rand-freq '0.0' -@1:update-lbd '1' -@1:0:strengthen 'no' -@1:1:lookahead 'atom' -@1:save-progress '167' -@1:contraction '4' -@0:sat-prepro '0' -@1:S:counterCond 'no' -@1:init-watches '0' -@1:2:Ari:restarts '1' -@1:S:del-grow 'no' -@1:S:contraction 'yes' -@1:sign-def '1' -@1:S:Ari:aryrestarts '2' -@1:deletion 'no' -@1:reverse-arcs '1' -@1:0:restarts '+' -@1:2:lookahead '6' -@1:heuristic 'None' -@1:1:Simp:restarts '20' -@1:F:init-moms 'yes' 
  CSSC-Queens-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/nqueen/nqueen_40_1_0_1_1_pairwise.cnf 0 300.0 2147483647 375162 -@1:F:update-act 'yes' -@1:S:Luby:aryrestarts '2' -@1:1:del-init '15.830644315582374' -@1:F:berk-huang 'yes' -@1:S:deletion 'yes' -@1:F:local-restarts 'no' -@1:del-grow '0' -@1:2:del-glue '1' -@1:F:sign-fix 'yes' -@0:S:sat-prepro 'no' -@1:otfs '2' -@1:counter-restarts '1' -@1:2:Luby:restarts '5' -@1:rand-freq '0.01' -@1:update-lbd '0' -@1:3:deletion '1' -@1:0:strengthen 'recursive' -@1:1:lookahead 'body' -@1:del-max '723822861' -@1:1:del-cfl '16' -@1:3:del-init '17373' -@1:save-progress '86' -@1:contraction '5' -@0:sat-prepro '0' -@1:S:counterCond 'yes' -@1:init-watches '0' -@1:del-on-restart '17' -@1:1:deletion 'basic' -@1:S:del-grow 'no' -@1:S:contraction 'yes' -@1:sign-def '2' -@1:0:del-cfl 'L' -@1:1:del-glue '6' -@1:2:del-init '190' -@1:counter-bump '28' -@1:F:berk-once 'yes' -@1:reverse-arcs '0' -@1:0:restarts 'L' -@1:2:lookahead '1262' -@1:heuristic 'Berkmin' -@1:1:Simp:restarts '38' -@1:2:deletion '100' -@1:F:init-moms 'no' -@1:berk-max '49' -@1:1:strengthen '0' 

lingeling
  CSSC-LABS-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/LABS/LABS_n025_goal004.cnf SATISFIABLE 300.0 2147483647 375162 -treelookrtc '0' -cce '3' -megaint '23727384' -redlminrel '13' -acts '1' -redfixed '1' -otfsconf '0' -redlmaxabs '242543561' -score '4' -rephase '0' -smallvevars '7' -plim '985704000' -keepmaxglue '0' -elmschedsum '1' -locscint '1' -subl '8035' -gaussreleff '9804' -unhidewait '1' -flipvlim '1637394818' -itlocsdel '73075' -elmsuccessrat '9' -gaussmineff '635014057' -prbasicreleff '919' -elim '1' -cgrmaxeff '432460899' -redlmaxrel '2158' -blkocclim1 '2' -elmboost '105' -otfsbump '0' -irrlim '1' -locsboost '52' -binlocsdel '118' -blkocclim2 '845' -blksmall '1' -ternres '0' -cardcut '0' -boost '0' -agile '1' -minrecgluelim '1337666464' -blkrtc '1' -cgrmaxority '17' -redlbound '1' -bca '0' -mega '0' -sortlits '0' -treelookmaxeff '1908361039' -seed '1138551482' -cliff '0' -simpdelay '77732180' -simpvarchg '196' -maxscorexp '660903876' -ternreswait '0' -locsred '0' -phasegluebit '1137640249' -trdmineff '917022543' -elmclslim '1061084' -prbrtc '1' -prbasicmineff '1933301237' -simpvarlim '1338555467' -trdreleff '1692' -fliplevels '4' -lftreleff '5515' -elmocclim '32987' -syncunint '370175' -actstdmax '111' -blkmaxeff '2015099598' -redlminabs '18' -elmschedmin '0' -redoutclim '156365218' -minimize '2' -flipint '1016664485' -simpiscale '546' -unhdmaxeff '189194798' -redlinit '397' -jwhred '0' -prbsimpleboost '430' -bumpclslits '1' -minlocalgluelim '1891867724' -restartinit '2090366908' -blklarge '0' -redlexpfac '469' -blkschedpure '1' -flipdur '34659749' -treelookmineff '1795940729' -cintmaxhard '1440574862' -locsrtc '1' -tabrkeep '1' -rephaseinc '1011' -gaussmaxeff '1592275878' -rdp '0' -agilesinint '67306' -elmreleff '5958' -deco '2' -cceboostvlim '1404205196' -elmblk '0' -tabrvfactor '8451981' -lkhd '3' -bva '1' -redlinc '837' -blkboostvlim '1246285816' -cliffwait '1' -trnrmineff '891470530' -bias '2' -cardignused '0' -liftlrg '2104626402' -elmsuccesslim '1516672704' -actgeomlim '5' -gluescale '4' -ccemaxeff '1690293080' -cgrextunits '1' -ccertc '0' -transred '1' -inprocessing '0' -sizemaxpen '6' -rstinoutinc '38' -unhide '0' -elmroundlim '5' -redlmininc '3' -lftroundlim '1422697832' -lftmaxeff '794590956' -prbsimple '2' -import '1' -decompose '0' -phaseflip '1' -psm '2' -pure '0' -prbsimplemaxeff '267408709' -simpinterdelay '91191881' -cardglue '2' -synclsall '0' -simpen '11' -factor '1' -trnreleff '131' -cceonlyifstuck '0' -bate '1' -cliffmineff '876765503' -phaseneginit '1026939745' -cardexpam1 '5801' -elmocclim2 '4508658' -elmocclim1 '1269' -cgrclsrwait '0' -cardreschedint '737689915' -prbasicmaxeff '1329216749' -unhdreleff '3679' -actavgmax '31' -elmsched2b2 '0' -cgrmineff '521928038' -sizepen '368761' -blkreleff '855' -lhbr '1' -smallve '1' -locs '936913894' -mocint '37406421' -cardmaxeff '1481687706' -elmschedpure '1' -scincinc '110' -cgreleff '8980' -actgsdul '61' -bcawait '0' -blkschedmin '1' -liftwait '1' -agilelim '81' -cardminlen '1812331653' -rdpmodelm '0' -cardwait '1' -gluekeep '109819444' -block '1' -blkschedsum '0' -delmax '3' -phase '-1' -redinoutinc '55' -reduce '1' -prbasicroundlim '236977' -cgrextite '1' -termint '545329' -actvlim '786131988' -decolim '1976483745' -incredcint '48717670' -blksuccesslim '2055382363' -lift '1' -trepint '27014' -force '1347961624' -flipping '1' -cardocclim2 '176743205' -cintmaxsoft '108216571' -cardocclim1 '325751358' -actdblarithlim '9' -card '0' -cce3wait '1093642536' -defragint '9498218' -treelooklrg '0' -synclslen '1565351767' -wait '0' -blkclslim '181' -actstdmin '6' -ccewait '2' -locsclim '3478659' -otfs '0' -waitmax '1762584993' -rdpmaxeff '34493550' -bkwdscale '1' -elmineff '479876832' -redoutvlim '1353981024' -penmax '11' -bcaminuse '2079004993' -prbasicrtc '1' -tabr '3' -locsmaxeff '1304283906' -batewait '0' -bumpseenminsize '476623069' -redloutinc '423178' -bcamaxeff '1071580384' -cgrclsr '0' -cardmaxlen '2060790438' -memlim '2054650943' -smallvewait '1' -ccereleff '566' -cliffmaxeff '814209664' -blkboost '7326' -locsmineff '795970705' -clim '91753457' -rdpclslim '1191112069' -elmfull '1' -restart '0' -locswait '0' -bumpseenbeforemin '0' -restartintscale '-1' -synclsglue '1343894974' -cardreleff '1426' -cgrextxor '1' -cintincdiv '1' -rdplim '76' -elmlitslim '1837014535' -simpidiv '67' -carduse '1' -gaussexptrn '1' -rdpmineff '1099469742' -unhdatrn '0' -gaussextrall '1' -synclsint '135' -rdpwait '2' -itsimpdel '49263' -dlim '2058764426' -blksched2b2 '1' -compact '0' -elmrtc '0' -simprtc '40' -transredwait '1' -defragfree '141' -randec '1' -blockwait '0' -blkmineff '1966160855' -factmax '7126' -unhdroundlim '61' -blksuccessrat '436' -unhdhbr '1' -plain '1' -gaussmaxor '30' -randecint '128' -treelook '2' -trep '0' -incredconfslim '55' -gauss '0' -lkhdmisifelmrtc '1' -bumpbcplits '0' -ternresrtc '0' -prbsimplereleff '3' -bumpseenaftermin '1' -cce2wait '881104669' -ccesuccesslim '964151554' -gausswait '2' -prbsimplemineff '52263550' -cliffreleff '3140' -cceboost '251' -restartint '190247680' -elmblkwait '0' -locset '0' -binsimpdel '828' -blkocclim '2056546373' -treelookboost '1' -unhdmineff '625067502' -ternresboost '80' -cgrexteq '1' -prbasic '1' -bumpseenlits '0' -rmincpen '25' -maxglue '1059382339' -prbsimplertc '1' -ccemineff '659645651' -elmschediff '0' -locsvared '990' -cintinc '122' -incsavevisits '1' -fliptop '0' -randecflipint '339745853' -flipldmod '22' -treelookreleff '5075' -unhdextstamp '1' -trnrmaxeff '1395739267' -blkschedprod '1' -ccesuccessrat '14932291' -rdpreleff '6479' -smallirr '97' -unhdlnpr '1633502168' -locsdec '1' -tabrcfactor '23213' -megawait '2' -prbsimpleliftdepth '3' -trdmaxeff '1706347412' -move '1' -cgrextand '1' -cardmineff '786747632' -elmschedprod '1' -lftmineff '731348649' -reusetrail '0' -locsreleff '12' -redlmaxinc '7560' -treelookfull '0' -elmaxeff '1033696819' -saturating '987' -probe '1' -locsexport '1' -simplify '0' 
  CSSC-GI-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/GI/iso_m2D_s36.AB23.cnf SATISFIABLE 300.0 2147483647 375162 -treelookrtc '0' -cce '3' -megaint '4' -redlminrel '10' -acts '2' -redfixed '0' -otfsconf '0' -redlmaxabs '1000000' -score '4' -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 '9740' -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 '1237851481' -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 '439424' -actstdmax '112' -blkmaxeff '666095051' -redlminabs '500' -elmschedmin '0' -redoutclim '5000' -minimize '2' -flipint '10' -simpiscale '100' -unhdmaxeff '615417944' -redlinit '4000' -jwhred '1' -prbsimpleboost '10' -bumpclslits '0' -minlocalgluelim '30' -restartinit '0' -blklarge '1' -redlexpfac '131' -blkschedpure '1' -flipdur '10' -treelookmineff '300000' -cintmaxhard '10000000' -locsrtc '0' -tabrkeep '3' -rephaseinc '10000' -gaussmaxeff '50000000' -rdp '0' -agilesinint '3007633' -elmreleff '200' -deco '1' -cceboostvlim '1000000' -elmblk '1' -tabrvfactor '4' -lkhd '1' -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 '135' -unhide '1' -elmroundlim '3' -redlmininc '10' -lftroundlim '1019633314' -lftmaxeff '20000000' -prbsimple '2' -import '1' -decompose '1' -phaseflip '0' -psm '3' -pure '0' -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 '11914060' -blkreleff '100' -lhbr '1' -smallve '1' -locs '309517807' -mocint '1000' -cardmaxeff '300000000' -elmschedpure '1' -scincinc '200' -cgreleff '1' -actgsdul '7' -bcawait '2' -blkschedmin '0' -liftwait '2' -agilelim '30' -cardminlen '181074193' -rdpmodelm '0' -cardwait '0' -gluekeep '3' -block '1' -blkschedsum '1' -delmax '10' -phase '0' -redinoutinc '100' -reduce '1' -prbasicroundlim '236' -cgrextite '1' -termint '122222' -actvlim '169133023' -decolim '30' -incredcint '1' -blksuccesslim '10000' -lift '1' -trepint '55555' -force '0' -flipping '1' -cardocclim2 '15' -cintmaxsoft '438400341' -cardocclim1 '300' -actdblarithlim '3' -card '1' -cce3wait '2' -defragint '1937183975' -treelooklrg '1' -synclslen '40' -wait '1' -blkclslim '1000000' -actstdmin '10' -ccewait '2' -locsclim '4812804' -otfs '1' -waitmax '4' -rdpmaxeff '10000000' -bkwdscale '2' -elmineff '20000000' -redoutvlim '1000' -penmax '4' -bcaminuse '100' -prbasicrtc '0' -tabr '1' -locsmaxeff '100000' -batewait '2' -bumpseenminsize '3' -redloutinc '10000' -bcamaxeff '10000000' -cgrclsr '1' -cardmaxlen '1000' -memlim '-1' -smallvewait '0' -ccereleff '137' -cliffmaxeff '100000000' -blkboost '2539' -locsmineff '930082428' -clim '-1' -rdpclslim '444808145' -elmfull '0' -restart '2' -locswait '2' -bumpseenbeforemin '1' -restartintscale '0' -synclsglue '8' -cardreleff '5' -cgrextxor '1' -cintincdiv '2' -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 '113' -randec '0' -blockwait '1' -blkmineff '1930951988' -factmax '100000' -unhdroundlim '43' -blksuccessrat '41111' -unhdhbr '0' -plain '0' -gaussmaxor '20' -randecint '17790' -treelook '1' -trep '0' -incredconfslim '0' -gauss '1' -lkhdmisifelmrtc '0' -bumpbcplits '0' -ternresrtc '0' -prbsimplereleff '4634' -bumpseenaftermin '0' -cce2wait '1' -ccesuccesslim '10000' -gausswait '2' -prbsimplemineff '750031617' -cliffreleff '8' -cceboost '10' -restartint '5' -elmblkwait '1' -locset '2' -binsimpdel '2' -blkocclim '1000000' -treelookboost '1' -unhdmineff '345815310' -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 '97775439' -flipldmod '4' -treelookreleff '1' -unhdextstamp '1' -trnrmaxeff '13279633' -blkschedprod '0' -ccesuccessrat '1000' -rdpreleff '2' -smallirr '90' -unhdlnpr '3' -locsdec '2' -tabrcfactor '25' -megawait '2' -prbsimpleliftdepth '2' -trdmaxeff '2000000' -move '2' -cgrextand '1' -cardmineff '2000000' -elmschedprod '0' -lftmineff '500000' -reusetrail '1' -locsreleff '5' -redlmaxinc '31' -treelookfull '0' -elmaxeff '194654227' -saturating '70' -probe '1' -locsexport '1' -simplify '2' 
  CSSC-Queens-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/nqueen/nqueen_40_1_0_1_1_pairwise.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 '-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 '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 '1' -minlocalgluelim '30' -restartinit '0' -blklarge '1' -redlexpfac '510' -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 '200000000' -simpinterdelay '2000' -cardglue '0' -synclsall '1' -simpen '0' -factor '3' -trnreleff '10' -cceonlyifstuck '1' -bate '1' -cliffmineff '10000000' -phaseneginit '0' -cardexpam1 '3' -elmocclim2 '100' -elmocclim1 '1000' -cgrclsrwait '2' -cardreschedint '10' -prbasicmaxeff '100000000' -unhdreleff '2' -actavgmax '112' -elmsched2b2 '1' -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 '-1' -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 '-1' -rdpclslim '3' -elmfull '0' -restart '2' -locswait '2' -bumpseenbeforemin '1' -restartintscale '0' -synclsglue '4' -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' 

cryptominisat
  CSSC-LABS-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/LABS/LABS_n025_goal004.cnf SATISFIABLE 300.0 2147483647 375162 -elimcoststrategy '0' -flippolf '400' -blkrestlen '3606' -calcpolarall '0' -dompickf '556' -freq '0.019223090303259346' -eratio '0.08038344893298639' -cachecutoff '669' -cachesize '2363' -blkrestmultip '1.7453431841675044' -calcpolar1st '0' -occredmax '102' -startclean '29836' -clbtwsimp '5' -moreminimbin '38' -presimp '0' -updateglue '1' -cleanconflmult '0' -moreminimcache '86' -bva2lit '1' -lockuip '170' -restart 'agility' -perfmult '1.1418169141907972E-5' -clean 'glue' -calcreach '1' -blkrest '1' -morebump '0' -viviffastmaxm '116' -viviflongmaxm '6' -incclean '1.0371226750505667' -gluehist '141' -ltclean '0.6490122579174101' -locktop '1395' -sccperc '0.0016350504958103943' -burst '100' -probemaxm '3866' 
  CSSC-GI-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/GI/iso_m2D_s36.AB23.cnf SATISFIABLE 300.0 2147483647 375162 -elimcoststrategy '1' -flippolf '400' -calcpolarall '0' -dompickf '3618' -freq '0.024912371223690614' -eratio '0.9155715749545057' -cachecutoff '607' -cachesize '2487' -calcpolar1st '0' -occredmax '114' -startclean '7809' -clbtwsimp '5' -moreminimbin '4727' -presimp '0' -updateglue '1' -cleanconflmult '0' -moreminimcache '22' -bva2lit '1' -lockuip '561' -restart 'geom' -perfmult '0.6310402857899134' -clean 'confdep' -calcreach '0' -blkrest '0' -morebump '0' -viviffastmaxm '647' -viviflongmaxm '6' -incclean '1.1228698988857637' -gluehist '80' -ltclean '0.467953542778599' -locktop '1931' -sccperc '0.008561938004522185' -burst '300' -probemaxm '1128' 
  CSSC-Queens-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/nqueen/nqueen_40_1_0_1_1_pairwise.cnf 0 300.0 2147483647 375162 -elimcoststrategy '1' -flippolf '0' -calcpolarall '0' -dompickf '103' -freq '0.0499956702445943' -eratio '0.12893402226628603' -cachecutoff '1756' -cachesize '3032' -calcpolar1st '0' -occredmax '191' -startclean '23956' -clbtwsimp '4' -moreminimbin '749' -presimp '0' -updateglue '0' -cleanconflmult '0' -moreminimcache '62' -bva2lit '1' -lockuip '377' -restart 'glue' -perfmult '1.0298406542082357E-4' -clean 'size' -calcreach '1' -blkrest '0' -morebump '1' -viviffastmaxm '117' -viviflongmaxm '26' -incclean '1.034347210789115' -gluehist '82' -ltclean '0.5460628486303287' -locktop '1251' -sccperc '0.014829804097617983' -burst '300' -probemaxm '2877' 

Riss-4.27
  CSSC-LABS-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/LABS/LABS_n025_goal004.cnf SATISFIABLE 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 '50' -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 'yes' -pr-lhbr 'no' -cp3_fm_grow '0' -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 '30' -szTrailQueue '3500' -cp3_fm_growT '100000' -sUhdPrSh '0' -incReduceDB '300' -bve_red_lits '1' -cp3_ee_level '0' -pr-uips '0' -dyn 'yes' -enabled_cp3 'yes' -cp3_uhdIters '5' -hlabound '16000' -pr-nce 'no' -bve_cgrow_t '0' -cp3_limited 'yes' -cp3_fm_newAlo '2' -bce-bce 'no' -bva 'no' -minLBDMinimizingClause '6' -pr-probeL '7500000' -bve 'yes' -keepWorst '0.001' -ics 'no' -incLBD 'no' -up 'no' -lbdIgnL0 'yes' -rer 'no' -vsids-e '1.0' -ee 'yes' -card_Elimit '1200000' -lhbr-sub 'yes' -vsids-d '2147483647' -cp3_ee_it 'no' -vsids-i '1.0' -bce-cle 'yes' -cp3_fm_newAmo '2' -rMax '-1' -cp3_ee_limit '1000000' -cp3_fm_Slimit '12000000' -specialIncReduceDB '2000' -dense 'no' -hlaTop '512' -symm 'no' -cp3_iters '1' -cp3_bve_limit '50000000' -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 '2' -actStart '1024.0' -minLBDFrozenClause '30' -cla-decay '0.995' -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 '1' -lhbr-max '2147483647' -init-pol '0' -lhbr '3' -rnd-freq '0.005' 
  CSSC-GI-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/GI/iso_m2D_s36.AB23.cnf SATISFIABLE 300.0 2147483647 375162 -sym-prop 'no' -cp3_uhdUHTE 'no' -cp3_uhdTrans 'yes' -cce 'no' -quickRed 'yes' -agil-r 'no' -szLBDQueue '50' -hack '0' -otfss 'no' -longConflict 'no' -firstReduceDB '8000' -subsimp 'yes' -sym-consT '1000' -3resolve 'yes' -cp3_vars '1000000' -biAsserting 'yes' -laEEp '0' -pr-csize '4' -cp3_inp_cons '1000000' -laEEl 'yes' -cp3_res_bin 'no' -sUHLEsize '30' -cp3_uhdUHLE '3' -pr-keepL '0' -sls 'no' -pr-keepI '2' -bce 'yes' -var-decay-i '0.01' -K '0.85' -cp3_res3_steps '1000000' -vsids-s '1.0' -R '1.4' -dontTrust 'yes' -pr-lhbr 'no' -pr-keepLHBR '1' -learnDecP '66' -pr-double 'yes' -var-decay-e '0.99' -xor 'no' -pr-viviP '80' -var-decay-d '15000' -cp3_sub_limit '300000000' -var-decay-b '0.95' -pr-viviL '5000000' -pr-vivi 'yes' -lbdupd '0' -minSizeMinimizingClause '30' -szTrailQueue '4000' -incReduceDB '300' -pr-uips '0' -cp3_strength 'no' -dyn 'no' -enabled_cp3 'yes' -cp3_uhdIters '5' -hlabound '4096' -pr-nce 'no' -cp3_limited 'yes' -sym-clLearn 'yes' -bce-bce 'yes' -bva 'no' -minLBDMinimizingClause '6' -pr-probeL '7500000' -bve 'no' -keepWorst '0.01' -rMaxInc '1.1' -ics 'no' -incLBD 'yes' -up 'yes' -lbdIgnL0 'no' -rer 'no' -vsids-e '1.0' -ee 'no' -lhbr-sub 'yes' -vsids-d '2147483647' -vsids-i '1.0' -bce-cle 'yes' -rMax '32' -specialIncReduceDB '1100' -dense 'yes' -hlaTop '1024' -symm 'yes' -cp3_iters '3' -sym-min '4' -tabu 'yes' -hlaevery '64' -sym-pol 'no' -init-act '4' -varActB '0' -unhide 'yes' -sInterval '0' -phase-saving '2' -cp3_uhdProbe '0' -fm 'no' -sUHLElbd '12' -alluiphack '0' -randInp 'yes' -hlaMax '50' -inc-inp 'no' -rtype '0' -rate 'no' -sym-cons '0' -hte 'no' -hlaLevel '5' -sUhdProbe '0' -cp3_res_percent '0.01' -pr-bins 'yes' -actStart '2048.0' -minLBDFrozenClause '15' -cla-decay '0.999' -cp3_res3_ncls '100000' -cp3_ee_bIter '10' -cp3_uhdEE 'yes' -sym-size 'no' -probe 'yes' -laHack 'yes' -cp3_cls '30000000' -biAsFreq '8' -sym-ratio '0.1' -inprocess 'yes' -rlevel '1' -bce-limit '100000000' -sym-iter '2' -clsActB '0' -lhbr-max '2147483647' -init-pol '5' -lhbr '3' -rnd-freq '0.005' 
  CSSC-Queens-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/nqueen/nqueen_40_1_0_1_1_pairwise.cnf 0 300.0 2147483647 375162 -sUhdPrRb 'no' -quickRed 'yes' -agil-r 'yes' -minLBDMinimizingClause '9' -pr-probeL '7500000' -szLBDQueue '60' -hack '0' -otfss 'yes' -longConflict 'no' -keepWorst '0.0' -firstReduceDB '4000' -rMaxInc '1.05' -ics 'no' -incLBD 'no' -lbdIgnL0 'yes' -rer 'no' -vsids-e '1.0' -vsids-d '2147483647' -biAsserting 'no' -vsids-i '1.0' -rMax '128' -specialIncReduceDB '1100' -sUHLEsize '8' -agil-add '32' -otfssMLDB '64' -init-act '1' -pr-keepL '2' -varActB '0' -pr-keepI '0' -sInterval '0' -phase-saving '2' -var-decay-i '0.01' -sUHLElbd '6' -K '0.85' -alluiphack '0' -rtype '0' -vsids-s '1.0' -R '1.2' -dontTrust 'yes' -otfssL 'yes' -pr-lhbr 'yes' -sUhdProbe '1' -learnDecP '-1' -pr-double 'yes' -var-decay-e '0.99' -var-decay-d '10000' -var-decay-b '0.85' -actStart '1024.0' -lbdupd '1' -minLBDFrozenClause '30' -minSizeMinimizingClause '50' -agil-decay '0.9999' -szTrailQueue '3500' -cla-decay '0.999' -cp3_ee_bIter '400000000' -sUhdPrSh '0' -incReduceDB '300' -pr-uips '0' -agil-limit '0.22' -laHack 'no' -rlevel '1' -agil-init '0.11' -enabled_cp3 'no' -clsActB '0' -init-pol '1' -lhbr '0' -pr-nce 'yes' -rnd-freq '0.01' 

SparrowToRiss
  CSSC-LABS-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/LABS/LABS_n025_goal004.cnf SATISFIABLE 300.0 2147483647 375162 -quickRed 'no' -minLBDMinimizingClause '9' -pr-probeL '526885' -hack '0' -SPARROW-k 'no' -longConflict 'no' -keepWorst '0.04929114671945245' -firstReduceDB '3833' -incLBD 'yes' -lbdIgnL0 'no' -vsids-e '1.0' -vsids-d '2147483647' -biAsserting 'yes' -vsids-i '1.0' -specialIncReduceDB '1000' -SPARROW--sp '0.9400553291281718' -sUHLEsize '64' -init-act '0' -pr-keepL '2' -varActB '1' -pr-keepI '2' -sInterval '2' -phase-saving '0' -var-decay-i '0.01' -sUHLElbd '6' -alluiphack '2' -SPARROW--randomc '1' -vsids-s '1.0' -dontTrust 'no' -pr-lhbr 'yes' -SPARROW--luby '0' -learnDecP '50' -pr-double 'yes' -var-decay-e '0.99' -var-decay-d '5000' -var-decay-b '0.95' -actStart '2048.0' -lbdupd '1' -minLBDFrozenClause '15' -minSizeMinimizingClause '45' -cla-decay '0.995' -cp3_ee_bIter '2' -incReduceDB '440' -pr-uips '0' -biAsFreq '10' -rlevel '1' -strFlips '-2' -SPARROW--c1 '2.314904483492456' -clsActB '1' -init-pol '5' -pr-nce 'yes' -rnd-freq '3.7144971616404346E-5' 
  CSSC-GI-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/GI/iso_m2D_s36.AB23.cnf SATISFIABLE 300.0 2147483647 375162 -sUhdPrRb 'yes' -quickRed 'yes' -agil-r 'no' -minLBDMinimizingClause '8' -pr-probeL '860582' -hack '0' -SPARROW-k 'no' -otfss 'no' -longConflict 'yes' -keepWorst '0.015613776383347228' -firstReduceDB '7744' -strSseconds '250' -ics 'no' -incLBD 'yes' -lbdIgnL0 'no' -rer 'no' -vsids-e '1.0' -vsids-d '2147483647' -biAsserting 'yes' -vsids-i '1.0' -laEEp '100' -laEEl 'no' -rfirst '424' -specialIncReduceDB '2000' -SPARROW--sp '0.027703678993347136' -hlaTop '1024' -sUHLEsize '8' -tabu 'yes' -hlaevery '8' -init-act '5' -pr-keepL '2' -varActB '0' -pr-keepI '2' -sInterval '3' -phase-saving '0' -var-decay-i '0.01' -sUHLElbd '2' -alluiphack '0' -SPARROW--randomc '1' -hlaMax '482' -rtype '1' -vsids-s '1.0' -dontTrust 'no' -pr-lhbr 'yes' -SPARROW--luby '0' -hlaLevel '5' -sUhdProbe '3' -learnDecP '100' -pr-double 'no' -var-decay-e '0.99' -var-decay-d '5000' -var-decay-b '0.95' -actStart '1024.0' -lbdupd '0' -minLBDFrozenClause '15' -minSizeMinimizingClause '24' -cla-decay '0.5' -cp3_ee_bIter '107806587' -sUhdPrSh '2' -incReduceDB '432' -pr-uips '0' -laHack 'yes' -biAsFreq '2' -rlevel '2' -dyn 'yes' -strFlips '1000000000' -enabled_cp3 'no' -hlabound '4096' -SPARROW--c1 '5.020546008461361' -clsActB '1' -init-pol '2' -pr-nce 'no' -lhbr '0' -rnd-freq '1.0582866768342191E-4' 
  CSSC-Queens-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/nqueen/nqueen_40_1_0_1_1_pairwise.cnf 0 300.0 2147483647 375162 -quickRed 'yes' -minLBDMinimizingClause '9' -pr-probeL '7461186' -hack '1' -SPARROW-k 'no' -longConflict 'no' -keepWorst '0.01487182116024649' -firstReduceDB '2890' -incLBD 'yes' -lbdIgnL0 'yes' -hack-cost 'yes' -vsids-e '1.0' -vsids-d '2147483647' -biAsserting 'yes' -vsids-i '1.0' -specialIncReduceDB '1100' -SPARROW--luby_base '352223.1362916069' -sUHLEsize '8' -init-act '4' -pr-keepL '2' -varActB '0' -pr-keepI '2' -sInterval '0' -phase-saving '0' -var-decay-i '0.01' -sUHLElbd '6' -alluiphack '2' -SPARROW--randomc '0' -vsids-s '1.0' -dontTrust 'no' -pr-lhbr 'no' -SPARROW--luby '1' -learnDecP '66' -pr-double 'yes' -var-decay-e '0.95' -var-decay-d '15000' -var-decay-b '0.85' -actStart '2048.0' -lbdupd '1' -minLBDFrozenClause '30' -minSizeMinimizingClause '49' -cla-decay '0.999' -cp3_ee_bIter '1' -incReduceDB '436' -pr-uips '-1' -biAsFreq '4' -rlevel '1' -strFlips '-1' -SPARROW--c1 '4.713596618657206' -clsActB '2' -init-pol '1' -pr-nce 'no' -rnd-freq '0.009934282207117633' 

minisat-HACK-999ED-CSSC
  CSSC-LABS-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/LABS/LABS_n025_goal004.cnf SATISFIABLE 300.0 2147483647 375162 -ccmin-mode '1' -lbd-cut '5' -luby '0' -core-tolerance '0.04' -K-val '0.7' -cla-decay '0.9' -cp-increase '25000' -lbd-cut-max '5' -R-val '1.3' 
  CSSC-GI-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/GI/iso_m2D_s36.AB23.cnf SATISFIABLE 300.0 2147483647 375162 -ccmin-mode '1' -lbd-cut '6' -luby '0' -core-tolerance '0.02' -K-val '0.7' -cla-decay '0.8' -cp-increase '5000' -lbd-cut-max '8' -R-val '1.5' 
  CSSC-Queens-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/nqueen/nqueen_40_1_0_1_1_pairwise.cnf 0 300.0 2147483647 375162 -ccmin-mode '2' -lbd-cut '4' -luby '0' -core-tolerance '0.01' -K-val '0.8' -cla-decay '0.9' -cp-increase '10000' -lbd-cut-max '4' -R-val '1.4' 

YalSAT
  CSSC-LABS-300s-2day
	  python -u scripts/SATCSSCWrapper.py --mem-limit 3072 --script None --ext-callstring "ruby ./solvers/yalsat/callstring_generator.rb" --sat-checker ./scripts/SAT --sol-file ./instances/true_solubility.txt --log True instances/Sat_Data/LABS/LABS_n025_goal004.cnf SATISFIABLE 300.0 2147483647 375162 -correct '1' -cacheduni '1' -best '0' -cachemax '30205' -pol '0' -defrag '1' -pick '0' -cached '0' -prep '1' -reluctant '1' -rbfsrate '34318' -minchunksize '229700' -restart '100000' -unfairfreq '93' -restartouterfactor '107' -weight '6' -hitlim '804769962' -toggleuniform '0' -uni '-1' -crit '1' -keep '0' -cachemin '472' -fixed '4' -unirestarts '0' -unipick '4' -geomfreq '91' -restartouter '1' 
  CSSC-GI-300s-2day
	  python -u scripts/SATCSSCWrapper.py --mem-limit 3072 --script None --ext-callstring "ruby ./solvers/yalsat/callstring_generator.rb" --sat-checker ./scripts/SAT --sol-file ./instances/true_solubility.txt --log True instances/Sat_Data/GI/iso_m2D_s36.AB23.cnf SATISFIABLE 300.0 2147483647 375162 -correct '1' -cacheduni '1' -best '1' -cachemax '40394' -pol '-1' -defrag '1' -pick '4' -cached '0' -prep '0' -reluctant '1' -rbfsrate '1692' -minchunksize '622553' -restart '143472324' -unfairfreq '30' -restartouterfactor '6330' -weight '7' -hitlim '756079041' -toggleuniform '0' -uni '1' -crit '1' -keep '0' -cachemin '757' -fixed '995588665' -unirestarts '407271487' -unipick '-1' -geomfreq '5' -restartouter '1' 
  CSSC-Queens-300s-2day
	  python -u scripts/SATCSSCWrapper.py --mem-limit 3072 --script None --ext-callstring "ruby ./solvers/yalsat/callstring_generator.rb" --sat-checker ./scripts/SAT --sol-file ./instances/true_solubility.txt --log True instances/Sat_Data/nqueen/nqueen_40_1_0_1_1_pairwise.cnf 0 300.0 2147483647 375162 -correct '0' -cacheduni '0' -best '0' -cachemax '1024' -pol '0' -defrag '1' -pick '4' -cached '1' -prep '1' -reluctant '1' -rbfsrate '10' -minchunksize '256' -restart '100000' -unfairfreq '50' -restartouterfactor '100' -weight '5' -hitlim '-1' -toggleuniform '0' -uni '0' -crit '1' -keep '0' -cachemin '1' -fixed '4' -unirestarts '0' -unipick '-1' -geomfreq '66' -restartouter '0'