c launch: /data/cnf/sc2014/app/grid-strips-grid-y-3.055-NOTKNOWN.cnf.bz2
c host: atom18
c Lingeling SAT Solver
c 
c Version b7ztzu 7b29300825af9bcc1c8b2c5ebcf65fa1cb101cad
c 
c Copyright (C) 2010-2014 Armin Biere JKU Linz Austria.
c All rights reserved.
c 
c released Sun Apr 26 19:26:13 CEST 2015
c compiled Sun Apr 26 19:26:13 CEST 2015
c 
c gcc (Ubuntu 4.8.2-19ubuntu1) 4.8.2
c -Wall -O3 -I../yalsat -I../druplig -DNLGLOG -DNDEBUG -DNCHKSOL
c Linux cluster2 3.13.0-45-generic x86_64
c 
c piping '/data/cnf/sc2014/app/grid-strips-grid-y-3.055-NOTKNOWN.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/grid-strips-grid-y-3.055-NOTKNOWN.cnf.bz2
c no embedded options
c found 'p cnf 404100 3361895' header
c read 404100 variables, 3361895 clauses, 8114115 literals in 0.00 seconds
c
c --abstime=0
c --bate=1
c --batewait=2
c --bca=1
c --bcaddlimldscale=2
c --bcamaxeff=10000000
c --bcaminuse=100
c --bcawait=2
c --bkwdscale=100
c --bkwdroundlim=7
c --bkwdresched=1
c --blkboost=10
c --blkboostvlim=10000000
c --blkclslim=1000000
c --blklarge=1
c --blkmaxeff=800000000
c --blkmineff=50000000
c --blkocclim1=100000
c --blkocclim=1000000
c --blkocclim2=10000
c --blkreleff=100
c --blkresched=1
c --blkrtc=0
c --blksmall=1
c --blksuccessmaxwortc=6
c --blksuccessrat=100
c --block=1
c --blockwait=1
c --boost=1
c --bumpsimp=1
c --card=1
c --cardcut=2
c --cardexpam1=3
c --cardglue=0
c --cardignused=0
c --cardmaxeff=300000000
c --cardmaxlen=1000
c --cardmineff=2000000
c --cardminlen=3
c --cardocclim1=300
c --cardocclim2=15
c --cardreleff=5
c --cardreschedint=10
c --carduse=2
c --cardwait=0
c --cce2wait=1
c --cce=3
c --cceateint=2
c --cceboost=10
c --cceboostdel=3
c --cceboostint=5
c --cceboostvlim=10000000
c --cce3wait=2
c --ccemaxround=3
c --ccemaxeff=2147483647
c --ccemineff=30000000
c --ccereleff=50
c --ccertc=0
c --ccertcint=15
c --ccertcintvlim=2000000
c --ccesuccessrat=100
c --ccewait=2
c --clim=-1
c --compact=0
c --deco=1
c --decolim=100
c --deco1opt=1
c --decompose=1
c --defragfree=50
c --defragint=10000000
c --delmax=10
c --dlim=-1
c --druplig=0
c --drupligcheck=0
c --drupligtrace=0
c --drupligtraceorig=0
c --elim=1
c --elmaxeff=800000000
c --elmblk=1
c --elmblkwait=1
c --elmboost=20
c --elmboostdel=3
c --elmboostint=5
c --elmboostvlim=4000000
c --elmclslim=1000000
c --elmfull=0
c --elmineff=20000000
c --elmlitslim=200
c --elmocclim1=1000
c --elmocclim=1000000
c --elmocclim2=100
c --elmoccsumforced=0
c --elmreleff=200
c --elmresched=0
c --elmroundlim=3
c --elmrtc=0
c --elmrtcint=10
c --elmrtcintvlim=500000
c --elmsuccessmaxwortc=4
c --elmsuccessrat=100
c --exitonabort=0
c --factmax=100000
c --factor=3
c --gauss=1
c --gaussexptrn=1
c --gaussextrall=1
c --gaussmaxeff=50000000
c --gaussmaxor=20
c --gaussmineff=2000000
c --gaussreleff=2
c --gausswait=2
c --gluekeep=4
c --gluekeepsize=15
c --gluescale=4
c --hbrdom=2
c --import=1
c --incredcint=1
c --incredconfslim=0
c --incsavevisits=0
c --inprocessing=1
c --irrlim=1
c --jwhred=1
c --keepmaxglue=1
c --keepmaxglueint=100
c --lhbr=1
c --lkhd=2
c --locs=0
c --locsbanner=0
c --locsclim=1000000
c --locsboost=2
c --locscint=10000
c --locset=2
c --locsexport=1
c --locsmaxeff=100000
c --locsmineff=1000
c --locsred=0
c --locsreleff=5
c --locsrtc=0
c --locsvared=100
c --locswait=2
c --maxscaledglue=15
c --memlim=-1
c --minimize=2
c --minlocalgluelim=200
c --minlocalsizelim=3000
c --minrecgluelim=100
c --minrecsizelim=1000
c --norestartsatlimlo=85
c --move=2
c --otfs=1
c --penmax=4
c --phase=0
c --phaseluckfactor=200
c --phaselucklim=100
c --phaseluckmaxround=10
c --phasesave=1
c --plain=0
c --plim=-1
c --poison=1
c --prbasic=1
c --prbasicmaxeff=400000000
c --prbasicmineff=1000000
c --prbasicreleff=50
c --prbasicroundlim=8
c --prbasicrtc=0
c --prbrtc=0
c --prbsimple=2
c --prbsimpleboost=10
c --prbsimpleliftdepth=2
c --prbsimplemaxeff=200000000
c --prbsimplemineff=2000000
c --prbsimplereleff=40
c --prbsimplertc=0
c --probe=1
c --promote=1
c --promotegluelim=8
c --pure=1
c --quatres=1
c --quatreswait=2
c --queuesort=1
c --queuesortjwh=0
c --randec=0
c --randecint=1000
c --redcls=1
c --redclsglue=6
c --redclsmaxdec=5
c --redclsmaxdepth=10
c --redclsmaxlrg=10
c --redclsmaxprops=100
c --redclsatlimlo=0
c --redclsatlimhi=100
c --redclsize=30
c --redclstype=4
c --reducefixed=0
c --reduceinc=1000
c --reduceinit=50000
c --reduce=1
c --restart=4
c --restartglcint=10
c --restartglclim=115
c --restartinit=0
c --restartint=5
c --restartpen=1
c --retirenb=1
c --retireint=4
c --retiremin=1
c --reusetrail=0
c --rmincpen=4
c --rstinoutinc=110
c --satlimdelay=10000
c --scincinc=200
c --scincincsatlimhi=100
c --scincincdelta=10
c --scincincincint=100000
c --scincincmin=200
c --scincincmode=1
c --score=0
c --scoreshift=0
c --scoreresetint=2147483647
c --seed=0
c --simpbintinc=100
c --simpbintinclim=10000
c --simpcintdelay=2000
c --simpcintinc=20000
c --simpcintincdiv=1
c --simpcintmaxhard=10000000
c --simpcintmaxsoft=1000000
c --simpincdelmaxfact=50
c --simpincdelmaxmin=10000
c --simpinitdelay=0
c --simpintsizepen=0
c --simpen=0
c --simpidiv=3
c --simpiscale=100
c --simpitdelay=10
c --simpitintinc=10
c --simpitintinclim=1000
c --simplify=2
c --simprtc=5
c --simptintinc=1000
c --simptintinclim=10000
c --simpvarchg=100
c --simpvarlim=100
c --sizemaxpen=5
c --sizepen=1000000
c --sleeponabort=0
c --smallirr=90
c --smallve=1
c --smallvevars=10
c --smallvewait=0
c --sortlits=0
c --subl=9
c --sweep=1
c --sweepboost=10
c --sweepboostdel=4
c --sweepboostint=7
c --sweepboostvlim=1000000
c --sweepfacdec=10
c --sweepforgive=2
c --sweepirr=3
c --sweepmaxeff=200000000
c --sweepmaxdec=10000
c --sweepmaxround=3
c --sweepmindec=100
c --sweepmineff=1000000
c --sweepred=3
c --sweepreleff=3
c --sweeprtc=0
c --sweeprtcint=14
c --sweeprtcintvlim=100000
c --sweepsuccessmaxwortc=6
c --sweepsuccessrat=1000
c --sweepwait=2
c --synclsall=1
c --synclsglue=8
c --synclsint=100
c --synclslen=40
c --syncunint=111111
c --termint=122222
c --ternres=1
c --ternresboost=5
c --ternresrtc=0
c --ternreswait=2
c --transred=1
c --transredwait=2
c --trapiflush=0
c --trdmaxeff=2000000
c --trdmineff=100000
c --trdreleff=10
c --treelook=1
c --treelookboost=10
c --treelookfull=0
c --treelookmaxeff=50000000
c --treelookmineff=300000
c --treelookreleff=2
c --treelookrtc=0
c --trep=1
c --trepint=55555
c --trnreleff=10
c --trnrmaxeff=200000000
c --trnrmineff=4000000
c --unhdatrn=2
c --unhdextstamp=1
c --unhdhbr=0
c --unhdlnpr=3
c --unhdmaxeff=20000000
c --unhdmineff=100000
c --unhdreleff=2
c --unhdroundlim=20
c --unhide=1
c --unhidewait=0
c --usedtwice=1
c --vsidsdint=256
c --wait=1
c --waitmax=4
c --witness=0
c --check=0
c --log=-1
c --profile=1
c --profilelong=1
c --verbose=1
c [freezer] frozen 0 variables out of 346585 free variables 0%
c [limits] no decision limit
c [limits] no conflict limit
c [limits] no propagation limit
c [limits] simplification not delayed since 'simpdelay' zero
c [set-maximum-score] maximum score limit 1.000000d+500
c [set-minimum-score] minimum score limit 1.000000d-500
c [score-type] STATIC (--score=0)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c *    0.0  346585  2911464         0       0      0     0    0     0   77   0%      0    0    0    0    0%
c 
c [simplification-1] limit 0 conflicts (hard 0) hit after 0 conflicts
c [card-1] limit 1000000 penalty 1 = 0 + 1
c [card-1] found 5 at-most-one constraints of average size 10.6
c [card-1] no at-most-two constraint found
c [card-1] using previous limit 1000000 for elimination
c [card-1] 5 out of 5 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] generated 1110 at-most-one constraints, 300 used 27%
c [card-1] exported 1470 binary clauses, 4.9 per/constraint
c [decomp-1] removed 65563 variables
c [simpleprobe-1] all 338537 free variables schedulable
c [simpleprobe-1] boosting simple probing limit by 10
c [simpleprobe-1] limit 10000000 penalty 1 = 0 + 1
c [decomp-2] removed 1226 variables
c [simpleprobe-1] 145509 variables remain 43% (191802 retained 57%)
c [simpleprobe-1] removed 1226 variables, found 307 hbrs, 1200 units
c [unhide-1] limit 176056 based on 2816896 irredundant clauses
c [unhide-1-1] 0 units, 5 failed, 155221 tauts, 0 hbrs, 0 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 337306 variables 100%
c [elim-1] limit of 10000000 steps penalty 1 = 0 + 1
c [elim-1] rescheduling of touched variables disabled
c [elim-1] incomplete 26982 not tried 8% in round 1
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 8343 = 2% variables out of 337306 scheduled
c [elim-1] considered successful since not run to completion yet
c [phase-count-1] 2622728 negative 100.0% of 2622893 except 165 0.0%
c [phase-count-1] 1512060 positive 57.6% of 2622893 except 1110833 42.4%
c [phase-count-1] less non-negative clauses 165 than limit 262200 (10.0%)
c [phase-count-1] non-pos/non-neg = 1110833/165 = 6732.32 >= 2.00 = 200/100
c [lucky-phase-1] forcing lucky phase -1
c [phase-1] phase bias: 0 positive 0%, 328963 negative 100%
c [sort-queue-1] sorted 328963 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 328963 (100%)
c [score-dist-1] max exp 0, different 1 (100%)
c [score-dist-1] median active exp 0, avg 0.0
c [simplification-1] removed 10357 variables 3.1% (328963 remain 95%)
c [simplification-1] removed 288571 irredundant clauses 9.9% (2622893 remain 90%)
c [simplification-1] maximum reduction of 10% = max (3%, 10%)
c [simplification-1] large reduction 10% >= 5% limit
c [simplification-1] next conflict interval 1000 = 2000/2
c [simplification-1] penalized conflict interval 1000 = 1 * 1000
c [simplification-1] hard conflict limit 11000 (soft 1000 + delta 10000)
c [simplification-1] new conflict limit 1000 (hard 11000)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   12.7  328962  2622893        66      58      0   430    3    89  105   4%      0   89   53    0 24312%
c i   13.0  328015  2622893       122     104      4   431   18   144  105  13%      0  144  266    1 23154%
c i   15.0  328009  2622893       396     344      7   436   70  1744  107   4%      1 1741  747    5 16597%
c i   17.2  328008  2622893       769     624     15   441  179  4495  109   4%      1 4475 1223   12 10242%
c 
c [simplification-2] limit 1000 conflicts (hard 11000) hit after 1001 conflicts
c [decomp-3] removed 2058 variables
c [simpleprobe-2] 141061 schedulable variables 43%
c [simpleprobe-2] limit 5213632 based on 2606816 irredundant clauses
c [decomp-4] removed 680 variables
c [simpleprobe-2] 52166 variables remain 16% (274059 retained 84%)
c [simpleprobe-2] removed 680 variables, found 2986 hbrs, 654 units
c [treelook-1] limit 650614 based on 2602458 irredundant clauses
c [treelook-1] scheduled 142266 literals 22%
c [treelook-1] scheduling used 651127 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 650614 based on 2602458 irredundant clauses
c [treelook-1] used 1336815 steps
c [treelook-1] 142263 literals remain 22%
c [treelook-1] 140713 variables remain to probed next time 43%
c [treelook-1] removed 0 variables, found 1480 hbrs
c [basicprobe-1] limit 20819664 based on 2602458 irredundant clauses
c [basicprobe-1-0] 297157 probes remain 91% after last round
c [basicprobe-1-0] 7 units = 7 failed (100%) + 0 lifted (0%)
c [basicprobe-1-0] removed 7 variables, found 90 hbrs
c [unhide-2] limit 162653 based on 2602458 irredundant clauses
c [unhide-2-2] 4 units, 4 failed, 119 tauts, 0 hbrs, 28702 literals
c [elim-2] 26966 variables 8% will be scheduled this time
c [elim-2] scheduled 26966 variables 8%
c [elim-2] limit of 13181988 steps penalty 1 = 0 + 1
c [elim-2] rescheduling of touched variables disabled
c [elim-2] incomplete 25029 not tried 8% in round 1
c [elim-2] transition to [ all 0 rem 1 ] state
c [elim-2] eliminated 0 = 0% variables out of 26966 scheduled
c [elim-2] considered successful since not run to completion yet
c [sort-queue-2] sorted 326211 enqueued variables after 1001 conflicts
c [score-dist-2] active 0 (0%), one 0 (0%), zero 326211 (100%)
c [score-dist-2] max exp 0, different 1 (100%)
c [score-dist-2] median active exp 0, avg 0.0
c [simplification-2] removed 727 variables 0.2% (326211 remain 94%)
c [simplification-2] removed 20668 irredundant clauses 0.8% (2602225 remain 89%)
c [simplification-2] maximum reduction of 1% = max (0%, 1%)
c [simplification-2] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-2] new conflict interval 10000
c [simplification-2] penalized conflict interval 10000 = 1 * 10000
c [simplification-2] hard conflict limit 21001 (soft 11001 + delta 10000)
c [simplification-2] new conflict limit 11001 (hard 21001)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   27.7  326210  2602225      1076     889     30  4794  192  4726  108   4%      2 4686  591   14 4366%
c i   28.5  326204  2602225      1171     976     35  4794  194  4844  109   4%      2 4797  495   14 3553%
c i   30.5  326203  2602225      1478    1249     43  4796  209  5279  110   4%      2 5209  549   16 3486%
c i   31.1  326173  2602225      1580    1340     46  4798  208  5339  110   4%      2 5261  421   16 2637%
c i   34.1  326172  2602225      2044    1733     55  4809  243  6265  115   4%      2 6146  458   20 2331%
c i   34.1  326171  2602225      2045    1732     56  4809  243  6264  115   4%      2 6145  457   20 2322%
c i   34.7  326163  2602225      2146    1822     57  4810  251  6593  116   4%      2 6464  499   20 2441%
c i   34.9  326162  2602225      2197    1863     60  4811  248  6523  117   4%      2 6389  419   20 2045%
c i   35.3  326147  2602225      2230    1892     61  4811  247  6495  117   4%      2 6358  382   21 1863%
c i   40.2  326139  2602225      2965    2536     73  4817  300  7576  119   4%      4 7363  722   27 2723%
c 
c [simplification-3] limit of 14 iterations hit after 14 iterations
c [card-2] limit 650556 based on 2602225 irredundant clauses
c [card-2] found 10 at-most-one constraints of average size 45.1
c [card-2] no at-most-two constraint found
c [card-2] using previous limit 650556 for elimination
c [card-2] 10 out of 10 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [decomp-6] removed 97 variables
c [unhide-3] limit 162589 based on 2601432 irredundant clauses
c [unhide-3-3] 10 units, 1 failed, 59630 tauts, 0 hbrs, 60645 literals
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 326103 variables 100%
c [elim-3] limit of 40959601 steps penalty 1 = 0 + 1
c [elim-3] rescheduling of touched variables disabled
c [elim-3] incomplete 56396 not tried 17% in round 1
c [elim-3] transition to [ all 1 rem 1 ] state
c [elim-3] eliminated 335 = 0% variables out of 326103 scheduled
c [elim-3] considered successful since not run to completion yet
c [sort-queue-3] sorted 325768 enqueued variables after 2965 conflicts
c [score-dist-3] active 0 (0%), one 0 (0%), zero 325768 (100%)
c [score-dist-3] max exp 0, different 1 (100%)
c [score-dist-3] median active exp 0, avg 0.0
c [simplification-3] removed 353 variables 0.1% (325768 remain 94%)
c [simplification-3] removed 60950 irredundant clauses 2.3% (2541275 remain 87%)
c [simplification-3] maximum reduction of 2% = max (0%, 2%)
c [simplification-3] forced so keeping old conflict interval 10000
c [simplification-3] conflict limit remains at 11011 (hard 21001)
c [simplification-3] new iteration interval 100
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   78.4  325767  2541275      3846    2745    114  4804  364  9515  120   4%      6 9191  747   34 2168%
c i   81.1  325766  2541275      4200    3063    122  4805  359  9562  121   4%      5 9187  365   36 1016%
c i   81.1  325765  2541275      4201    3063    122  4805  359  9560  121   4%      5 9185  363   36 1012%
c i   82.6  325749  2541275      4399    3231    130  4806  397 10202  121   4%      5 9799  909   39 2312%
c i   82.7  325748  2541275      4422    3248    131  4806  399 10158  121   4%      4 9752  882   39 2234%
c i   83.1  325747  2541275      4490    3310    132  4806  398 10104  121   4%      4 9688  760   40 1909%
c i   85.0  325746  2541275      4744    3527    140  4806  403 10524  122   4%      4 10070  624   41 1505%
c i   86.0  325726  2541275      4932    3692    144  4808  405 10212  123   4%      3 9731  533   43 1252%
c i   87.5  325725  2541275      5140    3872    146  4808  406 10314  127   4%      3 9803  490   44 1118%
c i   89.7  325724  2541275      5507    4172    154  4809  409 11008  134   4%      3 10441  428   46  931%
c i   89.9  325718  2541275      5543    4204    154  4809  407 10937  135   4%      3 10365  397   46  861%
c i   90.8  325717  2541275      5656    4303    155  4809  420 10991  135   4%      3 10402  543   47 1143%
c i   95.9  325716  2541275      6330    4866    169  4811  515 12216  139   4%      4 11518 1466   57 2556%
c i   97.7  325715  2541275      6636    5139    176  4811  498 11696  139   4%      4 10948  697   58 1195%
c i  100.7  325707  2541275      7093    5505    189  4814  515 11426  141   5%      4 10604  590   62  944%
c i  102.7  325706  2541275      7381    5762    196  4816  500 11003  141   5%      3 10137  367   63  579%
c i  102.8  325697  2541275      7396    5774    196  4816  499 10970  141   5%      3 10101  362   63  571%
c i  104.3  325679  2541275      7673    6001    202  4818  487 10601  141   5%      3 9691  311   65  482%
c i  109.5  325678  2541275      8378    6539    218  4822  567 12289  154   5%      4 11267  819   74 1100%
c i  117.3  325677  2541275      9640    7605    252  4837  531 12651  163   4%      9 11416  395   81  487%
c i  121.9  325658  2541275     10332    8183    274  4840  548 12532  164   4%      7 11181  562   87  647%
c i  123.4  325637  2541275     10539    8355    279  4840  581 12744  171   5%      6 11358  832   90  920%
c 
c [simplification-4] limit 11021 conflicts (hard 21001) hit after 11026 conflicts
c [decomp-7] removed 145 variables
c [treelook-2] limit 634965 based on 2539860 irredundant clauses
c [treelook-2] scheduled 178211 literals 27%
c [treelook-2] scheduling used 638912 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 634965 based on 2539860 irredundant clauses
c [treelook-2] used 1033802 steps
c [treelook-2] 178207 literals remain 27%
c [treelook-2] 137116 variables remain to probed next time 42%
c [treelook-2] removed 0 variables, found 3138 hbrs
c [unhide-4] limit 195404 with penalty 4 = 0 + 4
c [unhide-4-4] 9 units, 17 failed, 54 tauts, 0 hbrs, 364614 literals
c [elim-4] 25029 variables 8% will be scheduled this time
c [elim-4] scheduled 25029 variables 8%
c [elim-4] boosting limit by 20
c [elim-4] limit of 3126464210 steps penalty 1 = 0 + 1
c [elim-4] rescheduling of touched variables disabled
c [elim-4-1] no variable eliminated in round 1 in 330503437 steps
c [elim-4] fully completed in 1 rounds
c [elim-4] transition to [ all 0 rem 0 ] state
c [elim-4] eliminated 0 = 0% variables out of 25029 scheduled
c [sort-queue-4] sorted 325533 enqueued variables after 11026 conflicts
c [score-dist-4] active 0 (0%), one 0 (0%), zero 325533 (100%)
c [score-dist-4] max exp 0, different 1 (100%)
c [score-dist-4] median active exp 0, avg 0.0
c [simplification-4] removed 99 variables 0.0% (325533 remain 94%)
c [simplification-4] removed 8502 irredundant clauses 0.3% (2532773 remain 87%)
c [simplification-4] maximum reduction of 0% = max (0%, 0%)
c [simplification-4] full geometric conflict interval increment 20000
c [simplification-4] new conflict interval 30000
c [simplification-4] penalized conflict interval 30000 = 1 * 30000
c [simplification-4] hard conflict limit 56026 (soft 41026 + delta 15000)
c [simplification-4] new conflict limit 41026 (hard 56026)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i  147.5  325532  2532773     12352    9708    386  7909  645 14268  187   5%     15 12563  645  108  597%
c i  150.4  325526  2532773     12743   10028    393  7910  665 14623  187   5%     11 12845  755  112  672%
c i  154.2  325524  2532773     13217   10392    407  7916  669 14359  187   5%      8 12495  858  116  737%
c i  159.9  325523  2532773     13870   10936    425  7924  697 15252  187   5%      6 13266 1015  123  822%
c i  160.7  325522  2532773     13991   11036    427  7925  684 14968  187   5%      6 12959  727  124  587%
c i  161.8  325521  2532773     14149   11170    428  7925  679 14656  187   5%      5 12618  634  125  509%
c i  163.7  325520  2532773     14439   11436    432  7926  654 13971  187   5%      4 11880  403  125  321%
c i  169.3  325514  2532773     15249   12093    449  7939  648 13525  187   5%      5 11293  377  132  287%
c i  170.0  325513  2532773     15348   12179    449  7939  658 13527  187   5%      5 11277  579  133  436%
c i  170.5  325494  2532773     15408   12229    450  7939  651 13393  187   5%      4 11133  496  133  372%
c i  171.9  325473  2532773     15585   12373    453  7939  648 13726  187   5%      4 11436  533  134  398%
c i  174.9  325472  2532773     16026   12691    464  7941  665 13580  187   5%      3 11217 1000  139  721%
c i  177.4  325471  2532773     16327   12945    468  7944  672 13735  187   5%      3 11321  964  141  682%
c i  179.4  325456  2532773     16646   13229    478  7945  639 13559  199   5%      2 11091  408  142  288%
c i  183.6  325454  2532773     17266   13719    490  7950  663 13577  199   5%      3 11009  802  148  542%
c i  197.0  325453  2532773     19049   15216    533  7955  748 14922  236   5%     14 12033  432  169  256%
c i  198.5  325452  2532773     19267   15370    541  7955  763 14992  236   5%     11 12068  708  172  413%
c i  199.1  325369  2532773     19345   15441    542  7956  753 14870  236   5%     10 11932  582  172  339%
c i  199.9  325368  2532773     19443   15526    544  7956  747 14898  244   5%      9 11943  574  172  333%
c i  200.9  325367  2532773     19598   15653    551  7957  739 14928  244   5%      8 11945  534  173  309%
c i  203.1  325364  2532773     19911   15885    556  7959  735 15297  244   5%      6 12258  660  175  376%
c i  213.0  325363  2532773     21220   16970    590  7966  855 16559  260   5%      9 13269 1015  195  521%
c i  213.3  325359  2532773     21263   17000    590  7967  848 16396  260   5%      9 13097  891  195  457%
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i  214.9  325358  2532773     21437   17138    590  7967  861 16608  260   5%      8 13274 1005  197  509%
c i  224.1  325357  2532773     22870   18273    624  7970  883 17214  263   5%     11 13609 1225  212  577%
c i  225.5  325351  2532773     23076   18444    627  7970  865 17043  263   5%      9 13396  824  213  387%
c i  235.7  325350  2532773     24343   19486    663  7974  825 16690  264   5%     10 12803  796  222  358%
c i  236.7  325349  2532773     24469   19588    667  7976  830 16507  264   5%      8 12598  877  224  392%
c i  238.7  325332  2532773     24735   19815    672  7978  817 16315  264   5%      6 12356  729  225  324%
c i  238.7  325326  2532773     24736   19815    672  7978  816 16311  264   5%      6 12352  727  225  323%
c i  239.1  325318  2532773     24791   19854    675  7978  811 16346  264   5%      6 12377  666  225  295%
c i  239.6  325299  2532773     24858   19916    676  7978  801 16167  264   5%      6 12186  559  225  248%
c i  246.0  325282  2532773     25744   20650    703  7983  760 15696  269   5%      6 11559  593  230  258%
c i  261.5  325281  2532773     27935   22409    755  7994  837 15686  269   5%     19 11184  614  253  242%
c i  267.3  325266  2532773     28697   23020    774  7996  951 16142  270   6%     11 11512 1816  267  679%
c i  270.1  325265  2532773     29107   23366    781  7997  939 15936  293   6%      8 11237  974  271  360%
c i  273.2  325259  2532773     29617   23776    795  7998  882 15285  293   6%      5 10503  537  272  198%
c 
c [simplification-5] limit of 185 binary hit after 185 binaries
c [quatres-1] found 1221 quaternary clauses 2% in total
c [quatres-1-1] removed 1 duplicate quaternary clauses
c [ternres-1] boosting ternary resolution limit by 5
c [ternres-1] limit 107864987 with penalty 1 = 0 + 1
c [ternres-1] all 325259 free variables schedulable
c [ternres-1] 0 ternary resolvents (0 bin, 0 trn)
c [ternres-1] fully completed ternary resolution
c [gauss-1] limit 4314599 penalty 1 = 0 + 1
c [gauss-1] extracted 2 xors of average arity 2.0
c [gauss-1] connected 4 occurrences of 4 variables (average 1.0)
c [gauss-1] limit 4314599 penalty 1 = 0 + 1
c [gauss-1] fully completed
c [gauss-1] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-9] removed 16 variables
c [basicprobe-2] limit 107864988 penalty 1 = 0 + 1
c [basicprobe-2-0] 295884 probes remain 91% after last round
c [basicprobe-2-0] 48 units = 48 failed (100%) + 0 lifted (0%)
c [basicprobe-2-0] removed 79 variables, found 821 hbrs
c [unhide-5] limit 539324 with penalty 4 = 0 + 4
c [unhide-5-5] 5 units, 4 failed, 40373 tauts, 0 hbrs, 1270073 literals
c [transred-1] limit 2489505 based on 2489505 irredundant clauses
c [transred-1] removed 75 transitive binary clauses
c [block-1] scheduling all variables this time
c [block-1] scheduled 325155 variables 100%
c [block-1] boosting limit by 10
c [block-1] limit of 2157299760 steps penalty 1 = 0 + 1
c [block-1] fully completed
c [block-1] transition to [ all 0 rem 0 ] state
c [block-1] eliminated 849 blocked clauses
c [block-1] 849 < 1/100 * 2489430 = 24894 considered unsuccessful
c [cce-1] limit of 107864988 steps penalty 1 = 0 + 1
c [cce-1-1] eliminated 114 clauses out of 924 (12%) of length 541
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 114 large clauses in 107864991 steps
c [cce-1-1] allowing another 53932495 steps for small clauses
c [cce-1-1] scheduling 2431071 clauses = 2430950 binary + 121 ternary
c [cce-1-1] tried to eliminate 389 small clauses 0%
c [cce-1-1] eliminated 119 binary clauses 0%
c [cce-1-1] eliminated 119 small clauses 0%
c [cce-1-1] eliminated 119 small clauses in 107864989 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 233 covered clauses in round 1
c [cce-1] eliminated 233 covered clauses in TOTAL during 1 rounds
c [cce-1] 233 < 1/100 * 2488526 = 24885 considered unsuccessful
c [bca-1] limit of 10000000 steps and 4977086 added (scaled 2)
c [bca-1] 317318 out of 650310 literals actually usable 49%
c [bca-1] added 0 blocked clauses in 658429 steps
c [sweep-1] limit 6471899 penalty 1 = 0 + 1
c [sweep-1-1] 637 pos 0.2% + 324517 neg 99.8% = 325154 sched 100.0% ret 0
c [sweep-1-1] 6803214 steps 11 queries 54304.27 avg class size
c [sweep-1-1] 720 decisions 10 SAT calls 5674.80 avg env size
c [sweep-1-1] 325105 variables remain 100% (49 retained 0%)
c [decomp-10] removed 1 variables
c [sweep-1-1] removed 1 vars (0 failed, 0 eqs, 1 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 1 vars in TOTAL (1 rounds, 10 queries)
c [sort-queue-5] sorted 325153 enqueued variables after 29671 conflicts
c [score-dist-5] active 0 (0%), one 0 (0%), zero 325153 (100%)
c [score-dist-5] max exp 0, different 1 (100%)
c [score-dist-5] median active exp 0, avg 0.0
c [simplification-5] removed 106 variables 0.0% (325153 remain 94%)
c [simplification-5] removed 44482 irredundant clauses 1.8% (2488291 remain 85%)
c [simplification-5] maximum reduction of 2% = max (0%, 2%)
c [simplification-5] forced so keeping old conflict interval 30000
c [simplification-5] conflict limit remains at 41036 (hard 56026)
c [simplification-5] new binary interval 1000
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i  310.3  325152  2488291     29727   23674    927  9290  914 15400  328   6%      5 10601  990  275  360%
c i  310.6  325151  2488291     29744   23689    928  9290  912 15431  351   6%      4 10629  943  275  343%
c i  310.7  325145  2488291     29751   23693    929  9291  910 15426  351   6%      4 10623  920  275  335%
c i  315.9  325144  2488291     30346   24157    947  9294 1008 15678  359   6%      3 10781 1625  287  566%
c i  319.4  325143  2488291     30744   24447    959  9297 1045 16080  359   7%      3 11118 1449  294  493%
c i  327.7  325142  2488291     31693   25198    978  9302 1069 16048  360   7%      5 10930 1028  306  336%
c i  327.7  325136  2488291     31694   25198    978  9302 1069 16044  360   7%      4 10926 1024  306  335%
c i  329.5  325126  2488291     31920   25397    983  9304 1040 15931  360   7%      3 10776  714  307  233%
c i  331.0  325103  2488291     32098   25549    986  9306 1014 15956  360   6%      3 10771  552  307  180%
c i  333.5  325102  2488291     32401   25805    995  9307 1033 16144  360   6%      2 10910  842  312  270%
c i  334.0  325097  2488291     32438   25830    995  9307 1162 16668  360   7%      2 11427 2877  320  898%
c i  336.1  325089  2488291     32715   26058   1005  9310 1128 16154  360   7%      1 10866 1328  322  413%
c i  340.2  325066  2488291     33279   26525   1019  9312 1058 16006  360   7%      2 10628  688  324  213%
c i  344.9  325065  2488291     34226   27292   1044  9315  907 13838  360   7%      4 8321  285  324   88%
c i  345.2  325060  2488291     34309   27341   1044  9315  893 13572  360   7%      4 8045  265  323   82%
c i  350.8  325059  2488291     36314   28897   1075  9316  718 10600  360   7%     15 4897  855  326  262%
c i  353.4  325058  2488291     36638   29157   1083  9316  693 10397  360   7%     11 4671  491  326  151%
c i  358.3  325057  2488291     37286   29679   1112  9321  786 11323  360   7%      7 5549 1124  336  334%
c i  370.9  325040  2488291     38863   30993   1144  9332  901 12822  360   7%     11 6892  907  355  255%
c 1  380.2  325022  2488291     40056   31975   1182  9336  946 13463  360   7%      9 7420 1614  367  439%
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
s SATISFIABLE
c
c bate: 0 basic ate = 0 trn 0% + 0 lrg 0% in 0 updates
c bcas: 1 count, 0 added (32 skipped), 658429 steps
c bkwd: tried 0 clauses, 0 lits, 0.00 lits/clause
c bkwd: checked 0 occs, 0.00 occs/clause, 0.00 occs/lit
c bkwd: subsumed 0 binary, 0 ternary, 0 large
c bkwd: strengthened 0 binary, 0 ternary (0% self), 0 large (0% self)
c blkd: 1 bces, 849 removed, 7425979 resolutions, 19953987 steps
c blkd: 837 blocking literals 0%, 1 pure
c bump: 0 bumped seen, 0 lits 0.0 on average
c card: 2 count, 0 units, 1470 am1, 31914061 steps
c card: 6 rescheduled, 11 eliminated, 1576 resolved, 228 subsumed
c card: 15 at-most-one constraints found, average size 33.60
c card: 15 at-most-one constraints used 100%, average size 33.60
c card: 0 at-most-two constraints found, average size 0.00
c card: 0 at-most-two constraints used 0%, average size 0.00
c cces: 1 cces, 233 eliminated, 233 ate 100%, 0 abce 0%
c cces: 0 probed, 0 lifted, 0 failed
c cces: 0 cached, 0 rsz, 0 cols 0%, 0 srch, 0 hits 0%
c clls: 1 sat, 0 simp, 0 freeze, 0 melt
c clls: 11476010 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 29 gcs, 0 rescored clauses, 0 rescored vars
c dcps: 10 decompositions, 895 equivalent 0%
c deco: 5141 decision-only clauses 13%, 85% reduction
c decs: 78887640 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 4 elims, 8679 eliminated 2%, 0 pure 0%
c elms: 4 rounds, 1.0 rounds/bve
c elms: 5714 small 66%, 2964 large 34%
c elms: 6618 tried small, 5714 succeeded 86%, 904 failed 14%
c elms: 7992 subsumed, 4145 strengthened, 0 blocked
c elms: 5704806 copies, 6413493 resolutions, 111337 ipos
c elms: 22578019 subchks, 17625501 strchks
c gaus: 1 extractions, 2 extracted, 2.0 size, 2 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 8632710 steps, 4316355 extr 50%, 6 elim 0%
c glue: 798.6 orig avg, 798.6 real avg, 7.4 scaled avg
c glue: 1377 maxscaledglue=15 (4%), 14 kept 0%
c hbrs: 8872 = 3293 simple 37% + 1086 trn 12% + 4493 lrg 51%, 2 sub 0%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 39057 clauses, 2065.4 length
c lrnd: 80667215 lits = 121889638 orig - 41222423 removed 34%
c lrnd: 21986 uips 56%, 9372 flips 24%
c mins: 21739 mins 73%, 146 bin 0%, 2780 size 9%
c mins: 12238963 poisoned searches, 6106082 hits, 50% hit rate
c mins: 16527790 used twice searches, 403565 hits, 2% hit rate
c move: moved 611, 609 bin 100%, 2 trn 0%
c otfs: 1007 driving 10%, 8656 restarting 90%
c otfs: str 9663, 9657 red 100%, 6 irr 0%
c otfs: str 9663, 0 bin 0%, 11 trn 0%, 9652 lrg 100%
c otfs: sub 0, 0 red 0%, 0 irr 0%
c otfs: sub 0, 0 bin 0%, 0 trn 0%, 0 lrg 0%
c phas: 1 computed, 328963 set, 0 pos (0%), 328963 neg (100%)
c prbs: 2 basic, 820 probed, 55 failed, 0 lifted
c prbs: 2 simple, 728677 probed, 1854 failed, 4 eqs
c prbs: 2 treelook, 7 probed, 0 failed, 0 lifted
c prom: 0 locked 0% out of 59986 tried
c prps: 1338131824 props, 17 props/dec
c prps: 98% srch, 2% simp, 0% lkhd
c quat: 1 count, 0 quat, 0 self1, 0 self2, 1 dup
c queu: 5 sorted, 78887640 next (0 steps 0.00)
c queu: 2035728 enq (2035722 steps 1.00), 0 deq 0%
c redc: 1507 clauses 64%, 2351 tried 6%, 6 sat 0%
c redc: 6573 lits 27%, 24191 tried 0%, 6 sat 0%
c redc: 337 times jump level reduced, 1370.7 levels on average
c reds: 0 count, 0.0 conflicts per reduce
c reds: 0 memlim 0%, 0 arith 0%
c reds: 0 collected 0%, 0 retired 0%
c rmbd: 17128 removed, 149 red 1%
c rsts: 3350 restarts 100%, 0 skipped 0%
c rsts: 0 saturating 0%, 0 reuse 0%
c rsts: 0 kept 0.0% average 0.0%
c scnc: 0 count, 1.000 min (0/1000), 1.000 max (0/1000)
c simp: 5 count, 3 confs 60%, 0 vars 0%
c simp: 1 its 20%, 1 bin 20%, 0 trns 0%
c subl: 39057 count (34343 tried 0.9), 3590 sub out of 36535 (9.8%)
c swps: 1 count, 1 rounds, 10 queries (10.0/round)
c swps: 10 sat calls, 0 unsat (0.8% success rate)
c swps: 720 decisions 72.0, 8 conflicts 0.8
c swps; 59734.7 avg class size, 5674.8 avg environment size
c swps: 0 failed, 1 impls, 0 equivs
c swp0: 3 type 0 queries, 1 unsat (33.3%), 3 sat (100.0%)
c swp1: 7 type 1 queries, 0 unsat (0.0%), 7 sat (100.0%)
c sync: 0 produced units, 0 successful consumptions 0%
c sync: 0 consume units calls, 0 tried 0%, 0 success 0%
c sync: 0 produced clauses, 0 successful consumptions 0%
c sync: 0 consume clause calls, 0 tried 0%, 0 success 0%
c time: 157775442 calls to obtain time
c tops: 69504 fixed 17%, 92 its, 435.39 confs/it
c trds: 1 transitive reductions, 75 removed, 0 failed
c trds: 1045 nodes, 2696 edges, 2489859 steps
c trim: 273942 words, 1.0 MB
c trnr: 1 count, 0 bin, 0 trn, 5744621 steps
c unhd: 5 count, 5 rounds, 54333767 steps
c unhd: 2 non-trivial sccs of average size 2.0
c unhd: 28 units, 28 bin, 0 trn, 0 lrg
c unhd: 31 failed, 28 stamp, 0 lits, 0 bin, 0 trn, 0 lrg
c unhd: 255397 tauts, 0 bin 0%, 5 trn 0%, 267 lrg 0%
c unhd: 255397 tauts, 255125 stamp 100%, 176 red 0%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 1724034 str, 28 bin 0%, 87 trn 0%, 1723919 lrg 100%, 1723626 red 100%
c vars: 325022 remaining 80% and 79078 removed 20% out of 404100
c vars: 69504 fixed 17%, 8679 eliminated 2%, 895 equivalent 0%
c vsts: 5768184514 visits, 98% srch, 2% simp, 0% lkhd
c vsts: 4.3 search visits per propagation, 141719.1 per conflict
c wchs: 260754025 pushed, 95638883 enlarged, 44 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all          37898             0             0       1088065        169823         23592
c 
c  0 0          1890   5         0   0<        0   0<   126732  12     15810   9      1018   4     0.3
c  1 5           620   2         0   0         0   0     60958   6      8148   5       535   2     0.2
c  2 6          2414   6         0   0         0   0    218804  20     26512  16      2097   9     0.7
c  3 9          4169  11         0   0         0   0    328791  30     36542  22      3736  16     2.1
c  4 14         3251   9         0   0         0   0    101999   9<    18402  11      2402  10     4.1
c  5 21         2689   7         0   0         0   0     60063   6     14302   8<     3131  13     7.5
c  6 30         2377   6         0   0         0   0     25689   2      7052   4      1476   6<   10.3
c  7 41         2118   6         0   0         0   0     21800   2      6509   4      1470   6    13.2
c  8 54         1973   5<        0   0         0   0     23753   2      6762   4      1521   6    14.6
c  9 69         1716   5         0   0         0   0     14464   1      4306   3       968   4    17.5
c 10 86         1797   5         0   0         0   0     17956   2      4096   2       836   4    17.9
c 11 126        1459   4         0   0         0   0     17060   2      3696   2       833   4     9.4
c 12 230        4228  11         0   0         0   0     30972   3      7127   4      1241   5    20.6
c 13 534        3938  10         0   0         0   0     21017   2      6884   4      1684   7    28.5
c 14 1526       1896   5         0   0         0   0     16586   2      3675   2       563   2    31.8
c 15 5046       1363   4         0   0         0   0      1421   0         0   0        81   0     0.8
c 
c avg                  7.6           0.0           0.0           3.8           4.7           6.1
c std                  4.4           0.0           0.0           3.3           3.8           3.9
c 
c   37.819  10% elim
c   36.683  10% decide
c   16.162   4% block
c   14.977   4% probe
c   14.836   4% unhide
c    3.490   1% cce
c 
c    4.603 < 1% rest (below)
c 
c    1.551   0% sweep
c    1.399   0% gauss
c    1.060   0% bca
c    0.389   0% card
c    0.128   0% ternres
c    0.061   0% transred
c    0.015   0% quatres
c    0.000   0% bump
c    0.000   0% locs
c    0.000   0% queuesort
c    0.000   0% rescore
c ==================================
c   12.253   3% preprocessing    12%
c   87.530  23% inprocessing     88%
c ==================================
c   99.783  26% simplifying
c  280.427  74% search
c ==================================
c  380.224 100% all
c 
c         40056 conflicts,         105.3 confs/sec
c           834 ternaries,          48.0 confs/ternary
c           232 binaries,          172.7 confs/binary
c            92 iterations,        435.4 confs/iteration
c 
c             0 reductions,          0.0 redus/sec,      0.0 confs/reduction
c          3350 restarts,            8.8 rests/sec,     12.0 confs/restart
c      78887640 decisions,      207476.9 decis/sec,   1969.4 decis/conflict
c    1338131824 propagations,  3519327.3 props/sec,     17.0 props/decision
c 
c 380.2 seconds, 360.2 MB
c launch: done
