c launch: /data/cnf/sc2014/app/transport-transport-city-sequential-25nodes-1000size-3degree-100mindistance-3trucks-10packages-2008seed.030-NOTKNOWN.cnf.bz2
c host: atom24
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/transport-transport-city-sequential-25nodes-1000size-3degree-100mindistance-3trucks-10packages-2008seed.030-NOTKNOWN.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/transport-transport-city-sequential-25nodes-1000size-3degree-100mindistance-3trucks-10packages-2008seed.030-NOTKNOWN.cnf.bz2
c no embedded options
c found 'p cnf 361750 1934720' header
c read 361750 variables, 1934720 clauses, 4605620 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=1
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 330170 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] INC (--score=1)
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  330170  1661360         0       0      0     0    0     0   70   0%      0    0    0    0    0%
c 
c [simplification-1] limit 0 conflicts (hard 0) hit after 0 conflicts
c [card-1] limit 2000000 penalty 0 = 0 + 0
c [card-1] found 6247 at-most-one constraints of average size 3.0
c [card-1] no at-most-two constraint found
c [card-1] using previous limit 2000000 for elimination
c [card-1] 6247 out of 6247 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 40642 variables
c [simpleprobe-1] all 321108 free variables schedulable
c [simpleprobe-1] boosting simple probing limit by 10
c [simpleprobe-1] limit 20000000 penalty 0 = 0 + 0
c [decomp-2] removed 204 variables
c [simpleprobe-1] fully completed simple probing
c [simpleprobe-1] removed 204 variables, found 392 hbrs, 82 units
c [unhide-1] limit 97652 based on 1562434 irredundant clauses
c [unhide-1-1] 0 units, 0 failed, 45187 tauts, 0 hbrs, 0 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 320904 variables 100%
c [elim-1] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-1] rescheduling of touched variables disabled
c [elim-1] incomplete 6267 not tried 2% in round 1
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 116108 = 36% variables out of 320904 scheduled
c [elim-1] considered successful since not run to completion yet
c [phase-count-1] 1433147 negative 100.0% of 1433175 except 28 0.0%
c [phase-count-1] 878675 positive 61.3% of 1433175 except 554500 38.7%
c [phase-count-1] less non-negative clauses 28 than limit 143300 (10.0%)
c [phase-count-1] non-pos/non-neg = 554500/28 = 19803.57 >= 2.00 = 200/100
c [lucky-phase-1] forcing lucky phase -1
c [phase-1] phase bias: 0 positive 0%, 204796 negative 100%
c [sort-queue-1] sorted 204796 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 204796 (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 116374 variables 36.2% (204796 remain 62%)
c [simplification-1] removed 228185 irredundant clauses 13.7% (1433175 remain 86%)
c [simplification-1] maximum reduction of 36% = max (36%, 14%)
c [simplification-1] large reduction 36% >= 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    7.9  204795  1433175         9       7      1   385    0     1   65   4%      0    1    0    0 25216%
c i    8.3  204794  1433175       210     200      1   385    2    46   66   5%      0   46   27    0 18467%
c i    8.3  204793  1433175       219     207      1   385    2    47   66   5%      0   47   27    0 17976%
c i    9.8  204792  1433175       955     837      2   387   57   353   71  16%      3  350  461    4 12298%
c 
c [simplification-2] limit 1002 conflicts (hard 11000) hit after 1002 conflicts
c [decomp-3] removed 4 variables
c [simpleprobe-2] all 204792 free variables schedulable
c [simpleprobe-2] limit 2866282 based on 1433141 irredundant clauses
c [decomp-4] removed 1 variables
c [simpleprobe-2] 133403 variables remain 65% (71388 retained 35%)
c [simpleprobe-2] removed 1 variables, found 929 hbrs, 1 units
c [treelook-1] limit 358283 based on 1433132 irredundant clauses
c [treelook-1] scheduled 121909 literals 30%
c [treelook-1] scheduling used 359691 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 358283 based on 1433132 irredundant clauses
c [treelook-1] used 583221 steps
c [treelook-1] 121905 literals remain 30%
c [treelook-1] 121771 variables remain to probed next time 59%
c [treelook-1] removed 0 variables, found 433 hbrs
c [basicprobe-1] limit 11465056 based on 1433132 irredundant clauses
c [basicprobe-1-0] 145249 probes remain 71% after last round
c [basicprobe-1-0] 7 units = 7 failed (100%) + 0 lifted (0%)
c [basicprobe-1-0] removed 38 variables, found 1044 hbrs
c [elim-2] 6267 variables 3% will be scheduled this time
c [elim-2] scheduled 6267 variables 3%
c [elim-2] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-2] rescheduling of touched variables disabled
c [elim-2] incomplete 2599 not tried 1% in round 1
c [elim-2] transition to [ all 0 rem 1 ] state
c [elim-2] eliminated 0 = 0% variables out of 6267 scheduled
c [elim-2] considered successful since not run to completion yet
c [phase-count-2] 1431909 negative 100.0% of 1431937 except 28 0.0%
c [phase-count-2] 877668 positive 61.3% of 1431937 except 554269 38.7%
c [phase-count-2] less non-negative clauses 28 than limit 143100 (10.0%)
c [phase-count-2] non-pos/non-neg = 554269/28 = 19795.32 >= 2.00 = 200/100
c [lucky-phase-2] forcing lucky phase -1
c [phase-2] phase bias: 0 positive 0%, 48414 negative 100%
c [sort-queue-2] sorted 100010 enqueued variables after 1002 conflicts
c [score-dist-2] active 104743 (51%), one 0 (0%), zero 100010 (49%)
c [score-dist-2] max exp 509, different 9 (2%)
c [score-dist-2] median active exp 505, avg 504.4
c [simplification-2] removed 39 variables 0.0% (204753 remain 62%)
c [simplification-2] removed 1238 irredundant clauses 0.1% (1431937 remain 86%)
c [simplification-2] maximum reduction of 0% = max (0%, 0%)
c [simplification-2] full geometric conflict interval increment 20000
c [simplification-2] new conflict interval 20000
c [simplification-2] penalized conflict interval 20000 = 1 * 20000
c [simplification-2] hard conflict limit 31002 (soft 21002 + delta 10000)
c [simplification-2] new conflict limit 21002 (hard 31002)
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   22.8  204752  1431937      4379    3598      2  2788  325  1332   86  24%     37 1283  241   31  780%
c i   22.8  204751  1431937      4387    3602      2  2788  325  1331   86  24%     37 1282  245   31  790%
c i   28.8  204750  1431937      6677    4859      2  2795  506  1273  101  40%     24 1181  944   54 1736%
c i   29.4  204749  1431937      6981    5041      2  2796  522  1282  101  41%     18 1185  804   57 1398%
c i   33.3  204748  1431937      8156    5457      3  2798  656  1330  112  49%     12 1212 1182   75 1576%
c i   33.3  204747  1431937      8157    5457      3  2798  656  1330  112  49%     12 1211 1178   75 1570%
c i   48.2  204746  1431937     13654    7404     11  2812  938  1332  160  70%     66 1115 1178  148  798%
c i   49.5  204745  1431937     14125    7461     11  2812  966  1326  160  73%     41 1101 1199  155  773%
c 
c [simplification-3] limit 21013 conflicts (hard 31002) hit after 21015 conflicts
c [card-2] limit 2576969 penalty 1 = 1 + 0
c [card-2] found 2284 at-most-one constraints of average size 4.5
c [card-2] no at-most-two constraint found
c [card-2] using previous limit 2576969 for elimination
c [card-2] 2284 out of 2284 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [decomp-6] removed 9 variables
c [unhide-2] limit 128848 with penalty 4 = 1 + 3
c [unhide-2-2] 56 units, 6 failed, 3 tauts, 0 hbrs, 395405 literals
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 204648 variables 100%
c [elim-3] limit of 206157559 steps penalty 0 = 0 + 0
c [elim-3] rescheduling of touched variables disabled
c [elim-3] incomplete 274 not tried 0% in round 1
c [elim-3] transition to [ all 1 rem 1 ] state
c [elim-3] eliminated 561 = 0% variables out of 204648 scheduled
c [elim-3] considered successful since not run to completion yet
c [phase-count-3] 1425390 negative 100.0% of 1425418 except 28 0.0%
c [phase-count-3] 872028 positive 61.2% of 1425418 except 553390 38.8%
c [phase-count-3] less non-negative clauses 28 than limit 142500 (10.0%)
c [phase-count-3] non-pos/non-neg = 553390/28 = 19763.93 >= 2.00 = 200/100
c [lucky-phase-3] forcing lucky phase -1
c [phase-3] phase bias: 0 positive 0%, 42253 negative 100%
c [sort-queue-3] sorted 70146 enqueued variables after 21015 conflicts
c [score-dist-3] active 133941 (66%), one 0 (0%), zero 70146 (34%)
c [score-dist-3] max exp 515, different 15 (3%)
c [score-dist-3] median active exp 509, avg 508.2
c [simplification-3] removed 658 variables 0.3% (204087 remain 62%)
c [simplification-3] removed 6519 irredundant clauses 0.5% (1425418 remain 86%)
c [simplification-3] maximum reduction of 0% = max (0%, 0%)
c [simplification-3] full geometric conflict interval increment 20000
c [simplification-3] new conflict interval 40000
c [simplification-3] penalized conflict interval 40000 = 1 * 40000
c [simplification-3] hard conflict limit 81015 (soft 61015 + delta 20000)
c [simplification-3] new conflict limit 61015 (hard 81015)
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   90.0  204086  1425418     21292    8985     11  2807 1037  1407  124  74%     87 1066  246  259   95%
c i   90.2  204085  1425418     21386    9077     12  2807 1014  1413  124  72%     78 1070  186  259   72%
c i   90.5  204084  1425418     21510    9176     12  2807  996  1421  124  70%     68 1076  259  259  100%
c i   90.5  204083  1425418     21519    9183     13  2807  993  1421  124  70%     67 1076  251  259   97%
c i   93.7  204082  1425418     22752    9918     17  2808 1016  1567  143  65%     21 1201 1262  273  462%
c i   94.6  204065  1425418     23091   10120     17  2809 1043  1637  143  64%     13 1264 1248  279  447%
c i  103.8  204048  1425418     26252   11384     17  2811 1497  2113  171  71%     24 1668 1852  352  526%
c i  106.1  204031  1425418     26938   11502     17  2811 1598  2152  171  74%     10 1690 2163  371  583%
c i  187.0  204030  1425418     49900   16035     17  2811 2299  2489  458  92%    283 1464 1920  898  214%
c i  187.1  204015  1425418     49937   16067     17  2811 2282  2491  458  92%    271 1466 1714  898  191%
c 
c [simplification-4] limit of 22 iterations hit after 22 iterations
c [decomp-7] removed 73 variables
c [treelook-2] limit 1021791 penalty 1 = 1 + 0 boost 1
c [treelook-2] scheduled 161891 literals 40%
c [treelook-2] scheduling used 1021930 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 1021791 penalty 1 = 1 + 0 boost 1
c [treelook-2] used 1041619 steps
c [treelook-2] 161876 literals remain 40%
c [treelook-2] 121249 variables remain to probed next time 59%
c [treelook-2] removed 0 variables, found 1011 hbrs
c [unhide-3] limit 255447 with penalty 4 = 0 + 4
c [unhide-3-3] 0 units, 1 failed, 41194 tauts, 0 hbrs, 1231803 literals
c [elim-4] 274 variables 0% will be scheduled this time
c [elim-4] scheduled 274 variables 0%
c [elim-4] boosting limit by 20
c [elim-4] limit of 8174335060 steps penalty 0 = 0 + 0
c [elim-4] rescheduling of touched variables disabled
c [elim-4-1] no variable eliminated in round 1 in 368463069 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 274 scheduled
c [phase-count-4] 1383443 negative 100.0% of 1383471 except 28 0.0%
c [phase-count-4] 871626 positive 63.0% of 1383471 except 511845 37.0%
c [phase-count-4] less non-negative clauses 28 than limit 138300 (10.0%)
c [phase-count-4] non-pos/non-neg = 511845/28 = 18280.18 >= 2.00 = 200/100
c [lucky-phase-4] forcing lucky phase -1
c [phase-4] phase bias: 0 positive 0%, 40572 negative 100%
c [sort-queue-4] sorted 50391 enqueued variables after 49937 conflicts
c [score-dist-4] active 153622 (75%), one 0 (0%), zero 50391 (25%)
c [score-dist-4] max exp 516, different 16 (3%)
c [score-dist-4] median active exp 510, avg 510.0
c [simplification-4] removed 2 variables 0.0% (204013 remain 62%)
c [simplification-4] removed 41947 irredundant clauses 2.9% (1383471 remain 83%)
c [simplification-4] maximum reduction of 3% = max (0%, 3%)
c [simplification-4] forced so keeping old conflict interval 40000
c [simplification-4] conflict limit remains at 61016 (hard 81015)
c [simplification-4] 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  201.2  204012  1383471     49938   16066     18  3813 2282  2490  159  92%    270 1465 1707  898  190%
c i  201.3  204011  1383471     49939   16066     18  3813 2281  2490  159  92%    270 1465 1700  898  189%
c i  201.3  204010  1383471     49948   16074     18  3813 2276  2490  160  91%    267 1464 1642  898  183%
c i  201.3  204009  1383471     49950   16075     18  3813 2275  2489  160  91%    267 1464 1629  898  181%
c i  201.3  204008  1383471     49951   16075     18  3813 2274  2488  160  91%    266 1463 1623  898  181%
c i  201.4  204007  1383471     49953   16076     18  3813 2273  2488  165  91%    266 1463 1610  898  179%
c i  201.4  203992  1383471     49954   16076     18  3813 2273  2487  165  91%    265 1462 1604  898  179%
c i  201.4  203977  1383471     49955   16076     18  3813 2272  2487  165  91%    265 1461 1598  898  178%
c i  201.4  203962  1383471     49956   16076     18  3813 2272  2486  165  91%    265 1461 1592  898  177%
c i  201.4  203947  1383471     49957   16076     18  3813 2271  2486  165  91%    264 1460 1585  898  177%
c i  201.5  203932  1383471     49958   16076     18  3813 2270  2485  165  91%    264 1459 1579  898  176%
c i  201.5  203917  1383471     49959   16076     18  3813 2270  2484  165  91%    264 1459 1573  898  175%
c i  201.5  203902  1383471     49960   16076     18  3813 2269  2484  165  91%    263 1458 1567  898  175%
c i  201.5  203887  1383471     49961   16076     18  3813 2269  2483  165  91%    263 1458 1561  898  174%
c i  204.8  203872  1383471     51559   17189     19  3817 1874  2597  231  72%     18 1535 1421  900  158%
c i  206.4  203857  1383471     51968   17429     19  3818 1824  2613  231  70%     -8 1542 1366  903  151%
c i  206.5  203856  1383471     51969   17429     19  3818 1824  2612  231  70%     -8 1541 1360  903  151%
c i  206.5  203855  1383471     51974   17433     19  3818 1822  2612  231  70%     -8 1540 1334  903  148%
c i  206.6  203854  1383471     51991   17448     19  3818 1815  2612  231  70%     -9 1540 1271  903  141%
c i  212.3  203853  1383471     53138   17813     20  3819 1865  2657  231  70%    -37 1559 1490  922  162%
c i  212.5  203852  1383471     53164   17831     20  3819 1860  2658  231  70%    -38 1558 1442  922  156%
c i  212.7  203851  1383471     53216   17869     20  3819 1845  2659  231  69%    -39 1558 1296  922  141%
c i  225.8  203850  1383471     54911   18318     21  3819 1948  2703  278  72%    -43 1562 1881  954  197%
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  239.6  203666  1383471     56754   18702     21  3819 2083  2730  284  76%    -41 1546 1992  992  201%
c i  244.0  203665  1383471     57813   19244     21  3819 1946  2743  284  71%    -46 1534 1668  999  167%
c i  245.2  203664  1383471     58023   19318     22  3819 1950  2744  284  71%    -48 1530 1851 1003  185%
c i  247.0  203663  1383471     58276   19398     22  3819 1961  2746  284  71%    -50 1526 1982 1007  197%
c i  252.4  203662  1383471     59023   19642     22  3819 1965  2748  284  72%    -50 1511 1900 1018  187%
c i  262.5  203661  1383471     60552   20174     22  3819 1968  2752  376  71%    -44 1480 2346 1039  226%
c 
c [simplification-5] limit 61149 conflicts (hard 81015) hit after 65056 conflicts
c [quatres-1] found 676 quaternary clauses 4% in total
c [ternres-1] boosting ternary resolution limit by 5
c [ternres-1] limit 137460770 with penalty 0 = 0 + 0
c [ternres-1] all 203661 free variables schedulable
c [ternres-1] 0 ternary resolvents (0 bin, 0 trn)
c [ternres-1] fully completed ternary resolution
c [gauss-1] limit 5498430 penalty 0 = 0 + 0
c [gauss-1] extracted 5 xors of average arity 2.4
c [gauss-1] connected 12 occurrences of 12 variables (average 1.0)
c [gauss-1] limit 5498430 penalty 0 = 0 + 0
c [gauss-1] fully completed
c [gauss-1] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-9] removed 4 variables
c [basicprobe-2] limit 137460773 penalty 0 = 0 + 0
c [basicprobe-2-0] 142248 probes remain 70% after last round
c [basicprobe-2-0] 115 units = 115 failed (100%) + 0 lifted (0%)
c [basicprobe-2-0] removed 301 variables, found 9420 hbrs
c [unhide-4] limit 343651 with penalty 4 = 0 + 4
c [unhide-4-4] 67 units, 28 failed, 3 tauts, 0 hbrs, 1581957 literals
c [transred-1] limit 2000000 with penalty 0 = 0 + 0
c [transred-1] removed 7 transitive binary clauses
c [block-1] scheduling all variables this time
c [block-1] scheduled 203264 variables 100%
c [block-1] boosting limit by 10
c [block-1] limit of 2749215460 steps penalty 0 = 0 + 0
c [block-1] fully completed
c [block-1] transition to [ all 0 rem 0 ] state
c [block-1] eliminated 212 blocked clauses
c [block-1] 212 < 1/100 * 1377418 = 13774 considered unsuccessful
c [cce-1] limit of 137460773 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 171 clauses out of 342 (50%) of length 502
c [cce-1-1] eliminated 8 clauses out of 13 (62%) of length 501
c [cce-1-1] eliminated 3 clauses out of 9 (33%) of length 500
c [cce-1-1] eliminated 4 clauses out of 7 (57%) of length 499
c [cce-1-1] eliminated 3 clauses out of 7 (43%) of length 498
c [cce-1-1] eliminated 1 clauses out of 1 (100%) of length 490
c [cce-1-1] eliminated 1 clauses out of 3 (33%) of length 489
c [cce-1-1] eliminated 1 clauses out of 1 (100%) of length 488
c [cce-1-1] eliminated 1 clauses out of 3 (33%) of length 416
c [cce-1-1] eliminated 2 clauses out of 3 (67%) of length 415
c [cce-1-1] eliminated 2 clauses out of 3 (67%) of length 393
c [cce-1-1] eliminated 4 clauses out of 9 (44%) of length 391
c [cce-1-1] eliminated 2 clauses out of 3 (67%) of length 296
c [cce-1-1] eliminated 1 clauses out of 1 (100%) of length 294
c [cce-1-1] eliminated 1 clauses out of 1 (100%) of length 269
c [cce-1-1] eliminated 1 clauses out of 2 (50%) of length 268
c [cce-1-1] eliminated 3 clauses out of 7 (43%) of length 266
c [cce-1-1] eliminated 1 clauses out of 1 (100%) of length 264
c [cce-1-1] eliminated 2 clauses out of 6 (33%) of length 261
c [cce-1-1] eliminated 4 clauses out of 7 (57%) of length 260
c [cce-1-1] eliminated 1 clauses out of 1 (100%) of length 258
c [cce-1-1] eliminated 1 clauses out of 2 (50%) of length 255
c [cce-1-1] eliminated 1 clauses out of 2 (50%) of length 254
c [cce-1-1] eliminated 118 clauses out of 236 (50%) of length 252
c [cce-1-1] eliminated 7 clauses out of 15 (47%) of length 251
c [cce-1-1] eliminated 2 clauses out of 5 (40%) of length 250
c [cce-1-1] eliminated 2 clauses out of 3 (67%) of length 248
c [cce-1-1] eliminated 2 clauses out of 6 (33%) of length 241
c [cce-1-1] eliminated 2 clauses out of 2 (100%) of length 240
c [cce-1-1] eliminated 1 clauses out of 1 (100%) of length 239
c [cce-1-1] eliminated 2 clauses out of 3 (67%) of length 182
c [cce-1-1] eliminated 1 clauses out of 1 (100%) of length 177
c [cce-1-1] eliminated 1 clauses out of 2 (50%) of length 154
c [cce-1-1] eliminated 1 clauses out of 3 (33%) of length 152
c [cce-1-1] eliminated 1 clauses out of 1 (100%) of length 151
c [cce-1-1] eliminated 2 clauses out of 5 (40%) of length 148
c [cce-1-1] eliminated 2 clauses out of 2 (100%) of length 147
c [cce-1-1] eliminated 1 clauses out of 1 (100%) of length 146
c [cce-1-1] eliminated 2 clauses out of 4 (50%) of length 134
c [cce-1-1] eliminated 1 clauses out of 1 (100%) of length 117
c [cce-1-1] eliminated 1 clauses out of 1 (100%) of length 115
c [cce-1-1] eliminated 1 clauses out of 1 (100%) of length 113
c [cce-1-1] eliminated 1 clauses out of 1 (100%) of length 112
c [cce-1-1] eliminated 652 clauses out of 1291 (51%) of length 102
c [cce-1-1] eliminated 4 clauses out of 33 (12%) of length 101
c [cce-1-1] eliminated 5 clauses out of 14 (36%) of length 98
c [cce-1-1] eliminated 3 clauses out of 6 (50%) of length 97
c [cce-1-1] eliminated 1 clauses out of 2 (50%) of length 95
c [cce-1-1] eliminated 1 clauses out of 3 (33%) of length 94
c [cce-1-1] eliminated 6 clauses out of 15 (40%) of length 90
c [cce-1-1] eliminated 1 clauses out of 1 (100%) of length 89
c [cce-1-1] eliminated 1 clauses out of 2 (50%) of length 86
c [cce-1-1] eliminated 3 clauses out of 3 (100%) of length 85
c [cce-1-1] eliminated 1 clauses out of 5 (20%) of length 82
c [cce-1-1] eliminated 1 clauses out of 2 (50%) of length 81
c [cce-1-1] eliminated 1 clauses out of 1 (100%) of length 79
c [cce-1-1] eliminated 1 clauses out of 2 (50%) of length 78
c [cce-1-1] eliminated 2 clauses out of 2 (100%) of length 77
c [cce-1-1] eliminated 1 clauses out of 1 (100%) of length 75
c [cce-1-1] eliminated 3 clauses out of 7 (43%) of length 66
c [cce-1-1] eliminated 1 clauses out of 1 (100%) of length 60
c [cce-1-1] eliminated 3 clauses out of 5 (60%) of length 59
c [cce-1-1] eliminated 1 clauses out of 1 (100%) of length 56
c [cce-1-1] eliminated 1 clauses out of 1 (100%) of length 55
c [cce-1-1] eliminated 2 clauses out of 3 (67%) of length 49
c [cce-1-1] eliminated 1 clauses out of 3 (33%) of length 36
c [cce-1-1] eliminated 1 clauses out of 1 (100%) of length 32
c [cce-1-1] eliminated 1 clauses out of 1 (100%) of length 29
c [cce-1-1] eliminated 1 clauses out of 1 (100%) of length 27
c [cce-1-1] eliminated 1 clauses out of 1 (100%) of length 26
c [cce-1-1] eliminated 1 clauses out of 1 (100%) of length 25
c [cce-1-1] eliminated 1 clauses out of 1 (100%) of length 23
c [cce-1-1] eliminated 1 clauses out of 1 (100%) of length 21
c [cce-1-1] eliminated 1 clauses out of 1 (100%) of length 19
c [cce-1-1] eliminated 3 clauses out of 3 (100%) of length 18
c [cce-1-1] eliminated 2 clauses out of 4 (50%) of length 17
c [cce-1-1] eliminated 2 clauses out of 3 (67%) of length 16
c [cce-1-1] eliminated 503 clauses out of 11191 (4%) of length 14
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 1584 large clauses in 137460794 steps
c [cce-1-1] allowing another 68730397 steps for small clauses
c [cce-1-1] scheduling 1358576 clauses = 1357977 binary + 599 ternary
c [cce-1-1] tried to eliminate 1945 small clauses 0%
c [cce-1-1] eliminated 400 binary clauses 0%
c [cce-1-1] eliminated 3 ternary clauses 1%
c [cce-1-1] eliminated 403 small clauses 0%
c [cce-1-1] eliminated 403 small clauses in 137460776 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 1987 covered clauses in round 1
c [cce-1] eliminated 1987 covered clauses in TOTAL during 1 rounds
c [cce-1] 1987 < 1/100 * 1376344 = 13763 considered unsuccessful
c [bca-1] limit of 10000000 steps and 2749214 added (scaled 2)
c [bca-1] 256307 out of 406484 literals actually usable 63%
c [bca-1] added 830 blocked clauses in 548247 steps
c [sweep-1] limit 8247646 penalty 0 = 0 + 0
c [sweep-1-1] 6424 pos 3.2% + 196817 neg 96.8% = 203241 sched 100.0% ret 0
c [sweep-1-1] 8257701 steps 95 queries 22352.73 avg class size
c [sweep-1-1] 3171 decisions 93 SAT calls 3031.74 avg env size
c [sweep-1-1] 198356 variables remain 98% (4885 retained 2%)
c [decomp-10] removed 3 variables
c [sweep-1-1] removed 3 vars (0 failed, 1 eqs, 4 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 3 vars in TOTAL (1 rounds, 94 queries)
c [phase-count-5] 1374325 negative 100.0% of 1374353 except 28 0.0%
c [phase-count-5] 865855 positive 63.0% of 1374353 except 508498 37.0%
c [phase-count-5] less non-negative clauses 28 than limit 137400 (10.0%)
c [phase-count-5] non-pos/non-neg = 508498/28 = 18160.64 >= 2.00 = 200/100
c [lucky-phase-5] forcing lucky phase -1
c [phase-5] phase bias: 0 positive 0%, 39217 negative 100%
c [sort-queue-5] sorted 49166 enqueued variables after 65056 conflicts
c [score-dist-5] active 154072 (76%), one 0 (0%), zero 49166 (24%)
c [score-dist-5] max exp 516, different 16 (3%)
c [score-dist-5] median active exp 512, avg 511.7
c [simplification-5] removed 423 variables 0.2% (203238 remain 62%)
c [simplification-5] removed 9118 irredundant clauses 0.7% (1374353 remain 83%)
c [simplification-5] maximum reduction of 1% = max (0%, 1%)
c [simplification-5] geometric conflict interval increment 20000 = 40000 / 2
c [simplification-5] new conflict interval 60000
c [simplification-5] penalized conflict interval 60000 = 1 * 60000
c [simplification-5] hard conflict limit 155056 (soft 125056 + delta 30000)
c [simplification-5] new conflict limit 125056 (hard 155056)
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  410.9  203237  1374353     80587   25649     46 14584 2424  2820  537  86%    216 1133 2159 1351  160%
c i  449.3  203236  1374353     88029   27017     46 14585 2443  2790  547  88%     19  983 1898 1471  129%
c 
c [simplification-6] limit 125056 conflicts (hard 155056) hit after 125057 conflicts
c [card-3] limit 6128187 penalty 2 = 2 + 0
c [card-3] found 6153 at-most-one constraints of average size 4.0
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 6128187 for elimination
c [card-3] 6153 out of 6153 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [decomp-11] removed 2 variables
c [simpleprobe-3] 132402 schedulable variables 65%
c [simpleprobe-3] limit 196102005 penalty 0 = 0 + 0
c [decomp-12] removed 6455 variables
c [simpleprobe-3] fully completed simple probing
c [simpleprobe-3] removed 6455 variables, found 25105 hbrs, 2958 units
c [unhide-5] limit 306409 with penalty 5 = 0 + 5
c [unhide-5-5] 0 units, 0 failed, 25672 tauts, 0 hbrs, 1738553 literals
c [transred-2] limit 2000000 with penalty 0 = 0 + 0
c [transred-2] removed 13 transitive binary clauses
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 196781 variables 100%
c [elim-5] limit of 400000000 steps penalty 1 = 1 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5] incomplete 38 not tried 0% in round 1
c [elim-5] transition to [ all 1 rem 1 ] state
c [elim-5] eliminated 5415 = 3% variables out of 196781 scheduled
c [bca-2] limit of 10000000 steps and 2560895 added (scaled 2)
c [bca-2] 242548 out of 382734 literals actually usable 63%
c [bca-2] added 492 blocked clauses in 525387 steps
c [sweep-2] limit 14707650 penalty 0 = 0 + 0
c [sweep-2-1] 6547 pos 3.5% + 180023 neg 96.5% = 186570 sched 97.5% ret 4796
c [sweep-2-1] 14754121 steps 157 queries 10645.01 avg class size
c [sweep-2-1] 4860 decisions 153 SAT calls 1150.88 avg env size
c [sweep-2-1] 169390 variables remain 89% (21975 retained 11%)
c [decomp-13] removed 3 variables
c [sweep-2-1] removed 3 vars (0 failed, 2 eqs, 6 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 3 vars in TOTAL (1 rounds, 156 queries)
c [phase-count-6] 1279954 negative 100.0% of 1279982 except 28 0.0%
c [phase-count-6] 821367 positive 64.2% of 1279982 except 458615 35.8%
c [phase-count-6] less non-negative clauses 28 than limit 127900 (10.0%)
c [phase-count-6] non-pos/non-neg = 458615/28 = 16379.11 >= 2.00 = 200/100
c [lucky-phase-6] forcing lucky phase -1
c [phase-6] phase bias: 0 positive 0%, 35175 negative 100%
c [sort-queue-6] sorted 45238 enqueued variables after 125057 conflicts
c [score-dist-6] active 146125 (76%), one 0 (0%), zero 45238 (24%)
c [score-dist-6] max exp 518, different 18 (3%)
c [score-dist-6] median active exp 514, avg 512.9
c [simplification-6] removed 11873 variables 5.8% (191363 remain 58%)
c [simplification-6] removed 94371 irredundant clauses 6.9% (1279982 remain 77%)
c [simplification-6] maximum reduction of 7% = max (6%, 7%)
c [simplification-6] large reduction 7% >= 5% limit
c [simplification-6] next conflict interval 2000 = 2000/1
c [simplification-6] penalized conflict interval 2000 = 1 * 2000
c [simplification-6] hard conflict limit 137057 (soft 127057 + delta 10000)
c [simplification-6] new conflict limit 127057 (hard 137057)
c 
c [simplification-7] limit 127057 conflicts (hard 137057) hit after 127058 conflicts
c [quatres-2] found 652 quaternary clauses 4% in total
c [ternres-2] limit 24862076 with penalty 1 = 1 + 0
c [ternres-2] all 191363 free variables schedulable
c [ternres-2] 0 ternary resolvents (0 bin, 0 trn)
c [ternres-2] fully completed ternary resolution
c [gauss-2] limit 4972415 penalty 1 = 1 + 0
c [gauss-2] extracted 0 xors of average arity 0.0
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [transred-3] limit 2000000 with penalty 0 = 0 + 0
c [transred-3] removed 8 transitive binary clauses
c [block-2] scheduling all variables this time
c [block-2] scheduled 191363 variables 100%
c [block-2] limit of 248620760 steps penalty 1 = 1 + 0
c [block-2] fully completed
c [block-2] transition to [ all 0 rem 0 ] state
c [block-2] eliminated 30 blocked clauses
c [block-2] 30 < 1/100 * 1279975 = 12799 considered unsuccessful
c [cce-2] limit of 124310380 steps penalty 1 = 1 + 0
c [cce-2-1] eliminated 1 clauses out of 1 (100%) of length 215
c [cce-2-1] eliminated 1 clauses out of 1 (100%) of length 210
c [cce-2-1] eliminated 2 clauses out of 3 (67%) of length 154
c [cce-2-1] eliminated 1 clauses out of 1 (100%) of length 150
c [cce-2-1] eliminated 1 clauses out of 1 (100%) of length 86
c [cce-2-1] eliminated 3 clauses out of 3 (100%) of length 81
c [cce-2-1] eliminated 1 clauses out of 1 (100%) of length 78
c [cce-2-1] eliminated 1 clauses out of 5 (20%) of length 66
c [cce-2-1] eliminated 1 clauses out of 2 (50%) of length 62
c [cce-2-1] eliminated 1831 clauses out of 10287 (18%) of length 14
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] eliminated 1843 large clauses in 124310388 steps
c [cce-2-1] allowing another 62155194 steps for small clauses
c [cce-2-1] scheduling 1263770 clauses = 1263740 binary + 30 ternary
c [cce-2-1] tried to eliminate 1863 small clauses 0%
c [cce-2-1] eliminated 398 binary clauses 0%
c [cce-2-1] eliminated 398 small clauses 0%
c [cce-2-1] eliminated 398 small clauses in 124310381 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 2241 covered clauses in round 1
c [cce-2] eliminated 2241 covered clauses in TOTAL during 1 rounds
c [cce-2] 2241 < 1/100 * 1279945 = 12799 considered unsuccessful
c [elim-6] 38 variables 0% will be scheduled this time
c [elim-6] scheduled 38 variables 0%
c [elim-6] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-6] rescheduling of touched variables disabled
c [elim-6-1] no variable eliminated in round 1 in 86273122 steps
c [elim-6] fully completed in 1 rounds
c [elim-6] transition to [ all 0 rem 0 ] state
c [elim-6] eliminated 0 = 0% variables out of 38 scheduled
c [bca-3] limit of 10000000 steps and 2556569 added (scaled 2)
c [bca-3] 241500 out of 382728 literals actually usable 63%
c [bca-3] added 15077 blocked clauses in 540151 steps
c [sweep-3] limit 14917245 penalty 0 = 0 + 0
c [sweep-3-1] 6536 pos 3.9% + 162854 neg 96.1% = 169390 sched 88.5% ret 21973
c [sweep-3-1] 14980638 steps 172 queries 10467.66 avg class size
c [sweep-3-1] 4164 decisions 167 SAT calls 701.46 avg env size
c [sweep-3-1] 151941 variables remain 79% (39420 retained 21%)
c [decomp-15] removed 6 variables
c [sweep-3-1] removed 6 vars (0 failed, 4 eqs, 10 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 6 vars in TOTAL (1 rounds, 171 queries)
c [phase-count-7] 1277660 negative 100.0% of 1277688 except 28 0.0%
c [phase-count-7] 819376 positive 64.1% of 1277688 except 458312 35.9%
c [phase-count-7] less non-negative clauses 28 than limit 127700 (10.0%)
c [phase-count-7] non-pos/non-neg = 458312/28 = 16368.29 >= 2.00 = 200/100
c [lucky-phase-7] forcing lucky phase -1
c [phase-7] phase bias: 0 positive 0%, 34821 negative 100%
c [sort-queue-7] sorted 45209 enqueued variables after 127058 conflicts
c [score-dist-7] active 146148 (76%), one 0 (0%), zero 45209 (24%)
c [score-dist-7] max exp 518, different 18 (3%)
c [score-dist-7] median active exp 514, avg 512.9
c [simplification-7] removed 6 variables 0.0% (191357 remain 58%)
c [simplification-7] removed 2294 irredundant clauses 0.2% (1277688 remain 77%)
c [simplification-7] maximum reduction of 0% = max (0%, 0%)
c [simplification-7] full geometric conflict interval increment 60000
c [simplification-7] new conflict interval 120000
c [simplification-7] penalized conflict interval 120000 = 1 * 120000
c [simplification-7] hard conflict limit 307058 (soft 247058 + delta 60000)
c [simplification-7] new conflict limit 247058 (hard 307058)
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  794.9  191356  1277688    135880   23276     67 55471 2251  2641  410  85%    483  370 1909 1917  100%
c 
c [simplification-8] limit of 203 binary hit after 230 binaries
c [decomp-16] removed 1 variables
c [unhide-6] limit 383479 with penalty 5 = 1 + 4
c [unhide-6-6] 1 units, 4 failed, 512 tauts, 0 hbrs, 1201324 literals
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 17 transitive binary clauses
c [bca-4] limit of 10000000 steps and 2563409 added (scaled 2)
c [bca-4] 239868 out of 382658 literals actually usable 63%
c [bca-4] added 31 blocked clauses in 529928 steps
c [sweep-4] limit 18406993 penalty 0 = 0 + 0
c [sweep-4-1] 6564 pos 4.3% + 145348 neg 95.7% = 151912 sched 79.4% ret 39416
c [sweep-4-1] 18445340 steps 228 queries 8500.44 avg class size
c [sweep-4-1] 4832 decisions 223 SAT calls 1187.63 avg env size
c [sweep-4-1] 129257 variables remain 68% (62071 retained 32%)
c [decomp-17] removed 4 variables
c [sweep-4-1] removed 4 vars (0 failed, 4 eqs, 9 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 4 vars in TOTAL (1 rounds, 227 queries)
c [phase-count-8] 1277327 negative 100.0% of 1277355 except 28 0.0%
c [phase-count-8] 819214 positive 64.1% of 1277355 except 458141 35.9%
c [phase-count-8] less non-negative clauses 28 than limit 127700 (10.0%)
c [phase-count-8] non-pos/non-neg = 458141/28 = 16362.18 >= 2.00 = 200/100
c [lucky-phase-8] forcing lucky phase -1
c [phase-8] phase bias: 0 positive 0%, 34138 negative 100%
c [sort-queue-8] sorted 45106 enqueued variables after 151564 conflicts
c [score-dist-8] active 146218 (76%), one 0 (0%), zero 45106 (24%)
c [score-dist-8] max exp 518, different 18 (3%)
c [score-dist-8] median active exp 514, avg 513.2
c [simplification-8] removed 32 variables 0.0% (191324 remain 58%)
c [simplification-8] removed 333 irredundant clauses 0.0% (1277355 remain 77%)
c [simplification-8] maximum reduction of 0% = max (0%, 0%)
c [simplification-8] forced so keeping old conflict interval 120000
c [simplification-8] conflict limit remains at 247058 (hard 307058)
c [simplification-8] new binary interval 1000
c
c CAUGHT SIGNAL 15 SIGTERM
c
c s UNKNOWN
c bate: 0 basic ate = 0 trn 0% + 0 lrg 0% in 0 updates
c bcas: 4 count, 16430 added (997 skipped), 2143713 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: 2 bces, 242 removed, 7456405 resolutions, 20023069 steps
c blkd: 183 blocking literals 0%, 23 pure
c bump: 165275 bumped seen, 1576334359 lits 9537.6 on average
c card: 3 count, 0 units, 0 am1, 35033099 steps
c card: 35 rescheduled, 0 eliminated, 0 resolved, 13017 subsumed
c card: 14684 at-most-one constraints found, average size 3.67
c card: 14684 at-most-one constraints used 100%, average size 3.67
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: 2 cces, 4228 eliminated, 4228 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: 6540340 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 43 gcs, 0 rescored clauses, 0 rescored vars
c dcps: 17 decompositions, 141 equivalent 0%
c deco: 131184 decision-only clauses 79%, 77% reduction
c decs: 7385241 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 6 elims, 122107 eliminated 34%, 48680 pure 40%
c elms: 6 rounds, 1.0 rounds/bve
c elms: 68898 small 56%, 4506 large 4%
c elms: 216243 tried small, 68898 succeeded 32%, 147345 failed 68%
c elms: 8829 subsumed, 391 strengthened, 14 blocked
c elms: 8466947 copies, 9242082 resolutions, 2363882 ipos
c elms: 77225046 subchks, 45759300 strchks
c gaus: 2 extractions, 5 extracted, 2.4 size, 3 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 20945528 steps, 10472764 extr 50%, 17 elim 0%
c glue: 2064.0 orig avg, 2064.0 real avg, 12.6 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 38738 = 26426 simple 68% + 10944 trn 28% + 1368 lrg 4%, 5 sub 0%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 165274 clauses, 2426.1 length
c lrnd: 400978383 lits = 1508373287 orig - 1107394904 removed 73%
c lrnd: 60206 uips 36%, 88060 flips 53%
c mins: 20137 mins 13%, 102 bin 0%, 240 size 0%
c mins: 23516402 poisoned searches, 11889313 hits, 51% hit rate
c mins: 25956590 used twice searches, 587860 hits, 2% hit rate
c move: moved 922, 898 bin 97%, 24 trn 3%
c otfs: 1455 driving 19%, 6313 restarting 81%
c otfs: str 7768, 7768 red 100%, 0 irr 0%
c otfs: str 7768, 0 bin 0%, 0 trn 0%, 7768 lrg 100%
c otfs: sub 141, 141 red 100%, 0 irr 0%
c otfs: sub 141, 0 bin 0%, 0 trn 0%, 141 lrg 100%
c phas: 8 computed, 479386 set, 0 pos (0%), 479386 neg (100%)
c prbs: 2 basic, 4000 probed, 122 failed, 0 lifted
c prbs: 3 simple, 1085318 probed, 3041 failed, 162 eqs
c prbs: 2 treelook, 19 probed, 0 failed, 0 lifted
c prom: 0 locked 0% out of 246466 tried
c prps: 848524271 props, 110 props/dec
c prps: 96% srch, 4% simp, 0% lkhd
c quat: 2 count, 0 quat, 0 self1, 0 self2, 0 dup
c queu: 8 sorted, 7385241 next (20125 steps 0.00)
c queu: 1577307696 enq (8184465139 steps 5.19), 1576349746 deq 100%
c redc: 636 clauses 50%, 1280 tried 1%, 0 sat 0%
c redc: 2358 lits 15%, 16204 tried 0%, 0 sat 0%
c redc: 132 times jump level reduced, 457.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: 148 removed, 76 red 51%
c rsts: 2785 restarts 54%, 2336 skipped 46%
c rsts: 2336 saturating 100%, 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: 8 count, 6 confs 75%, 0 vars 0%
c simp: 1 its 12%, 1 bin 12%, 0 trns 0%
c subl: 165274 count (239000 tried 1.4), 123430 sub out of 164923 (74.8%)
c swps: 4 count, 4 rounds, 648 queries (162.0/round)
c swps: 636 sat calls, 1 unsat (0.1% success rate)
c swps: 17027 decisions 26.8, 64 conflicts 0.1
c swps; 11625.5 avg class size, 1320.8 avg environment size
c swps: 0 failed, 29 impls, 11 equivs
c swp0: 215 type 0 queries, 12 unsat (5.6%), 212 sat (98.6%)
c swp1: 433 type 1 queries, 36 unsat (8.3%), 425 sat (98.2%)
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: 15101201 calls to obtain time
c tops: 48178 fixed 13%, 54 its, 3086.41 confs/it
c trds: 4 transitive reductions, 45 removed, 0 failed
c trds: 855 nodes, 3980 edges, 8011797 steps
c trim: 738425 words, 2.8 MB
c trnr: 2 count, 0 bin, 0 trn, 6187480 steps
c unhd: 6 count, 6 rounds, 39200804 steps
c unhd: 2 non-trivial sccs of average size 2.0
c unhd: 124 units, 124 bin, 0 trn, 0 lrg
c unhd: 39 failed, 32 stamp, 0 lits, 0 bin, 0 trn, 0 lrg
c unhd: 112571 tauts, 59 bin 0%, 1 trn 0%, 0 lrg 0%
c unhd: 112571 tauts, 112511 stamp 100%, 577 red 1%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 6149042 str, 124 bin 0%, 2 trn 0%, 6148916 lrg 100%, 6148669 red 100%
c vars: 191324 remaining 53% and 170426 removed 47% out of 361750
c vars: 48178 fixed 13%, 122107 eliminated 34%, 141 equivalent 0%
c vsts: 6875878548 visits, 98% srch, 2% simp, 0% lkhd
c vsts: 8.3 search visits per propagation, 40491.2 per conflict
c wchs: 181960147 pushed, 48318792 enlarged, 68 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all         164923             0             0      10306216       3163656        106466
c 
c  0 0          1335   1         0   0<        0   0<  1111360  11    179263   6      1520   1     0.3
c  1 5           662   0         0   0         0   0    644675   6    134637   4       566   1     0.2
c  2 6          1895   1         0   0         0   0   1641563  16    409183  13      2331   2     0.6
c  3 9          2342   1         0   0         0   0   1293357  13    345196  11      3656   3     1.6
c  4 14         2140   1         0   0         0   0   1037978  10    244393   8      4029   4     2.9
c  5 21         2184   1         0   0         0   0    681148   7<   217973   7      9044   8     5.1
c  6 30         2456   1         0   0         0   0    661751   6    223657   7      4861   5     8.7
c  7 41         2303   1         0   0         0   0    379602   4    150522   5<     5849   5    14.3
c  8 54         2404   1         0   0         0   0    282251   3    132576   4      7129   7    22.7
c  9 69         2619   2         0   0         0   0    333627   3    144057   5      6635   6<   30.8
c 10 86         3808   2         0   0         0   0    353763   3    161863   5     19197  18    45.6
c 11 126        2624   2         0   0         0   0    326608   3    122422   4      9751   9    15.0
c 12 230        2403   1         0   0         0   0    611205   6    208640   7     10289  10    13.4
c 13 534       19626  12<        0   0         0   0    769206   7    386076  12     17347  16    76.3
c 14 1526     116122  70         0   0         0   0    178122   2    103198   3      4262   4   512.0
c 15 5046          0   0         0   0         0   0         0   0         0   0         0   0     0.0
c 
c avg                 12.6           0.0           0.0           5.3           6.6           9.1
c std                  3.1           0.0           0.0           4.2           4.4           3.4
c 
c  533.302  53% bump
c   41.850   4% unhide
c   35.227   4% elim
c   15.005   2% probe
c    9.156   1% sweep
c    8.715   1% block
c    7.432   1% decide
c 
c   12.503 < 1% rest (below)
c 
c    6.735   1% cce
c    3.186   0% bca
c    1.745   0% gauss
c    0.518   0% card
c    0.188   0% transred
c    0.111   0% ternres
c    0.022   0% quatres
c    0.000   0% locs
c    0.000   0% queuesort
c    0.000   0% rescore
c ==================================
c    7.870   1% preprocessing     6%
c  130.664  13% inprocessing     94%
c ==================================
c  138.534  14% simplifying
c  860.545  86% search
c ==================================
c  999.084 100% all
c 
c        166666 conflicts,         166.8 confs/sec
c            54 ternaries,        3086.4 confs/ternary
c           233 binaries,          715.3 confs/binary
c            54 iterations,       3086.4 confs/iteration
c 
c             0 reductions,          0.0 redus/sec,      0.0 confs/reduction
c          2785 restarts,            2.8 rests/sec,     59.8 confs/restart
c       7385241 decisions,        7392.0 decis/sec,     44.3 decis/conflict
c     848524271 propagations,   849301.9 props/sec,    114.9 props/decision
c 
c 999.1 seconds, 1419.2 MB
c
c CAUGHT SIGNAL 15 SIGTERM
c
c launch: done
