c launch: /data/cnf/sc2014/app/008-80-4.cnf.bz2
c host: atom17
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/008-80-4.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/008-80-4.cnf.bz2
c no embedded options
c found 'p cnf 13408 478480' header
c read 13408 variables, 478480 clauses, 3138512 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=5
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 13025 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] EVSIDS (--score=5)
c [set-score-increment-1] factor 1.200000d+00 (200/1000) after 0 conflicts
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   13025   308391         0       0      0     0    0     0   17   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 3 at-most-one constraints of average size 3.0
c [card-1] found 6 at-most-two constraints of average size 4.0
c [card-1] using previous limit 2000000 for elimination
c [card-1] 9 out of 9 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 405 variables
c [simpleprobe-1] all 13003 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 10 variables
c [simpleprobe-1] 4379 variables remain 34% (8614 retained 66%)
c [simpleprobe-1] removed 10 variables, found 2 hbrs, 4 units
c [unhide-1] limit 100000 with penalty 0 = 0 + 0
c [unhide-1-1] 0 units, 12 failed, 775 tauts, 0 hbrs, 15 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 12989 variables 100%
c [elim-1] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-1] rescheduling of touched variables disabled
c [elim-1-1] eliminated 470 variables 4% in round 1 in 2089777 steps
c [elim-1-1] backward subsumption/strengthening limit 2089700
c [elim-1-1-1] backward checking 2373 touched variables 18%
c [elim-1-1-1] fully completed backward checking in 1 rounds
c [elim-1-1] subsumed 7 and strengthened 110 clauses in 1445524 steps
c [elim-1-1] rescheduled 166 variables 1% by backward subsumption
c [elim-1-2] eliminated 2 variables 0% in round 2 in 55604 steps
c [elim-1-2] backward subsumption/strengthening limit 55600
c [elim-1-2-1] backward checking 19 touched variables 0%
c [elim-1-2-1] incomplete backward checking 0 remain 0%
c [elim-1-2] subsumed 0 and strengthened 0 clauses in 55601 steps
c [elim-1-2] fully rescheduled 12516 variables 96%
c [elim-1-3] no variable eliminated in round 3 in 1603984 steps
c [elim-1] fully completed in 3 rounds
c [elim-1] transition to [ all 0 rem 0 ] state
c [elim-1] eliminated 473 = 4% variables out of 12989 scheduled
c [phase-count-1] 301810 negative 99.5% of 303272 except 1462 0.5%
c [phase-count-1] 299678 positive 98.8% of 303272 except 3594 1.2%
c [phase-count-1] less non-negative clauses 1462 than limit 30300 (10.0%)
c [phase-count-1] non-pos/non-neg = 3594/1462 = 2.46 >= 2.00 = 200/100
c [lucky-phase-1] forcing lucky phase -1
c [phase-1] phase bias: 0 positive 0%, 12516 negative 100%
c [sort-queue-1] sorted 12516 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 12516 (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 509 variables 3.9% (12516 remain 96%)
c [simplification-1] removed 5119 irredundant clauses 1.7% (303272 remain 98%)
c [simplification-1] maximum reduction of 4% = max (4%, 2%)
c [simplification-1] geometric conflict interval increment 4000 = 20000 / 5
c [simplification-1] new conflict interval 4000
c [simplification-1] penalized conflict interval 4000 = 1 * 4000
c [simplification-1] hard conflict limit 14000 (soft 4000 + delta 10000)
c [simplification-1] new conflict limit 4000 (hard 14000)
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    1.4   12515   303271       110      82      5     2    0    15   25   2%      0   15    4    0 21265%
c i    1.5   12514   303271       723     524     49    12    1    44   25   3%      2   44    8    0 9013%
c i    1.8   12513   303268      3553    2687    180    33    4   155   25   3%     29  150    6    0 1719%
c i    1.8   12512   303268      3558    2687    179    36    4   154   25   3%     29  150    6    0 1696%
c 
c [simplification-2] limit 4002 conflicts (hard 14000) hit after 4002 conflicts
c [decomp-3] removed 7 variables
c [simpleprobe-2] 4216 schedulable variables 34%
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [simpleprobe-2] 4171 variables remain 33% (8338 retained 67%)
c [simpleprobe-2] removed 0 variables, found 1 hbrs, 0 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 5958 literals 24%
c [treelook-1] scheduling used 300017 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 300114 steps
c [treelook-1] 4979 literals remain 20%
c [treelook-1] 4958 variables remain to probed next time 40%
c [treelook-1] removed 0 variables, found 2 hbrs
c [basicprobe-1] limit 2425688 based on 303211 irredundant clauses
c [basicprobe-1-0] 520 sched 4%, 0 failed, 0 lifted, 30 hbrs
c [basicprobe-1-1] 526 sched 4%, 0 failed, 0 lifted, 2 hbrs
c [basicprobe-1-2] 527 sched 4%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-1-2] fully completed probing
c [basicprobe-1-2] removed 0 variables, found 32 hbrs
c [unhide-2] limit 100000 with penalty 0 = 0 + 0
c [unhide-2-2] 0 units, 0 failed, 18 tauts, 0 hbrs, 123 literals
c [block-1] scheduling all variables this time
c [block-1] scheduled 12509 variables 100%
c [block-1] boosting limit by 10
c [block-1] limit of 500000000 steps penalty 0 = 0 + 0
c [block-1] fully completed
c [block-1] transition to [ all 0 rem 0 ] state
c [block-1] eliminated 1238 blocked clauses
c [block-1] 1238 < 1/100 * 303211 = 3032 considered unsuccessful
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 8043 clauses out of 103925 (8%) of length 7
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 8043 large clauses in 30000027 steps
c [cce-1-1] allowing another 15000013 steps for small clauses
c [cce-1-1] scheduling 10820 clauses = 327 binary + 10493 ternary
c [cce-1-1] tried to eliminate 10820 small clauses 100%
c [cce-1-1] eliminated 11 binary clauses 3%
c [cce-1-1] eliminated 1058 ternary clauses 10%
c [cce-1-1] eliminated 1069 small clauses 10%
c [cce-1-1] eliminated 1069 small clauses in 18949865 steps
c [cce-1-1] completed small round (ATE)
c [cce-1-1] eliminated 9112 covered clauses in round 1
c [cce-1-2] incomplete large round (ATE)
c [cce-1-2] allowing another 5525075 steps for small clauses
c [cce-1-2] scheduling 9751 clauses = 316 binary + 9435 ternary
c [cce-1-2] tried to eliminate 9751 small clauses 100%
c [cce-1-2] completed small round (ATE)
c [cce-1-2] eliminated 0 covered clauses in round 2
c [cce-1] eliminated 9112 covered clauses in TOTAL during 2 rounds
c [elim-2] scheduling all variables this time
c [elim-2] scheduled 12509 variables 100%
c [elim-2] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-2] rescheduling of touched variables disabled
c [elim-2] incomplete 9218 not tried 74% in round 1
c [elim-2] transition to [ all 1 rem 1 ] state
c [elim-2] eliminated 267 = 2% variables out of 12509 scheduled
c [bca-1] limit of 10000000 steps and 556590 added (scaled 2)
c [bca-1] 20361 out of 24486 literals actually usable 83%
c [bca-1] added 0 blocked clauses in 192634 steps
c [sweep-1] limit 1000000 penalty 0 = 0 + 0
c [sweep-1-1] 2653 pos 21.7% + 9589 neg 78.3% = 12242 sched 100.0% ret 0
c [sweep-1-1] 1000451 steps 403 queries 2199.58 avg class size
c [sweep-1-1] 9554 decisions 401 SAT calls 30.72 avg env size
c [sweep-1-1] 9413 variables remain 77% (2829 retained 23%)
c [decomp-8] removed 1 variables
c [sweep-1-1] removed 1 vars (0 failed, 1 eqs, 0 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 1 vars in TOTAL (1 rounds, 402 queries)
c [sort-queue-2] sorted 8719 enqueued variables after 4002 conflicts
c [score-dist-2] active 3522 (29%), one 759 (6%), zero 7960 (65%)
c [score-dist-2] max exp 531, different 317 (60%)
c [score-dist-2] median active exp 427, avg 396.2
c [simplification-2] removed 271 variables 2.2% (12241 remain 94%)
c [simplification-2] removed 25225 irredundant clauses 8.3% (278043 remain 90%)
c [simplification-2] maximum reduction of 8% = max (2%, 8%)
c [simplification-2] large reduction 8% >= 5% limit
c [simplification-2] next conflict interval 2000 = 2000/1
c [simplification-2] penalized conflict interval 2000 = 1 * 2000
c [simplification-2] hard conflict limit 16002 (soft 6002 + delta 10000)
c [simplification-2] new conflict limit 6002 (hard 16002)
c 
c [simplification-3] limit 6002 conflicts (hard 16002) hit after 6002 conflicts
c [quatres-1] found 34131 quaternary clauses 13% in total
c [quatres-1-1] added 14 double-self-subsuming ternary resolvents
c [quatres-1-2] added 88 single-self-subsuming ternary resolvents
c [quatres-1-2] added 270 quaternary resolvents
c [ternres-1] boosting ternary resolution limit by 5
c [ternres-1] limit 20000000 with penalty 0 = 0 + 0
c [ternres-1] all 12241 free variables schedulable
c [ternres-1] 148 ternary resolvents (14 bin, 134 trn)
c [ternres-1] fully completed ternary resolution
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 3 at-most-one constraints of average size 3.0
c [card-2] found 11 at-most-two constraints of average size 4.2
c [card-2] using previous limit 1000000 for elimination
c [card-2] 13 out of 14 constraints (93%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 1121 xors of average arity 5.0
c [gauss-1] connected 5593 occurrences of 346 variables (average 16.2)
c [gauss-1] limit 2000000 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 1 variables
c [transred-1] limit 278039 based on 278039 irredundant clauses
c [transred-1] removed 6 transitive binary clauses
c [transred-1] found 1 units
c [cce-2] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-2-1] eliminated 207 clauses out of 87677 (0%) of length 7
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] eliminated 207 large clauses in 30000095 steps
c [cce-2-1] allowing another 15000047 steps for small clauses
c [cce-2-1] scheduling 9703 clauses = 313 binary + 9390 ternary
c [cce-2-1] tried to eliminate 9703 small clauses 100%
c [cce-2-1] eliminated 2 binary clauses 1%
c [cce-2-1] eliminated 5 ternary clauses 0%
c [cce-2-1] eliminated 7 small clauses 0%
c [cce-2-1] eliminated 15 small clauses in 18422696 steps
c [cce-2-1] completed small round (ATE)
c [cce-2-1] eliminated 222 covered clauses in round 1
c [cce-2-2] incomplete large round (ATE)
c [cce-2-2] allowing another 5788687 steps for small clauses
c [cce-2-2] scheduling 9696 clauses = 311 binary + 9385 ternary
c [cce-2-2] tried to eliminate 9696 small clauses 100%
c [cce-2-2] completed small round (ATE)
c [cce-2-2] eliminated 0 covered clauses in round 2
c [cce-2] eliminated 222 covered clauses in TOTAL during 2 rounds
c [cce-2] 222 < 1/100 * 278039 = 2780 considered unsuccessful
c [elim-3] 9218 variables 75% will be scheduled this time
c [elim-3] scheduled 9218 variables 75%
c [elim-3] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-3] rescheduling of touched variables disabled
c [elim-3] incomplete 7182 not tried 59% in round 1
c [elim-3] transition to [ all 0 rem 1 ] state
c [elim-3] eliminated 0 = 0% variables out of 9218 scheduled
c [sweep-2] limit 1000000 penalty 0 = 0 + 0
c [sweep-2-1] 2353 pos 25.0% + 7059 neg 75.0% = 9412 sched 76.9% ret 2827
c [sweep-2-1] 1001596 steps 486 queries 1483.68 avg class size
c [sweep-2-1] 10746 decisions 485 SAT calls 28.93 avg env size
c [sweep-2-1] 6706 variables remain 55% (5533 retained 45%)
c [sweep-2-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 0 vars in TOTAL (1 rounds, 485 queries)
c [sort-queue-3] sorted 7241 enqueued variables after 6002 conflicts
c [score-dist-3] active 4998 (41%), one 1458 (12%), zero 5783 (47%)
c [score-dist-3] max exp 674, different 464 (69%)
c [score-dist-3] median active exp 507, avg 454.5
c [simplification-3] removed 2 variables 0.0% (12239 remain 94%)
c [simplification-3] removed 6142 irredundant clauses 2.2% (271901 remain 88%)
c [simplification-3] maximum reduction of 2% = max (0%, 2%)
c [simplification-3] geometric conflict interval increment 6666 = 20000 / 3
c [simplification-3] new conflict interval 10666
c [simplification-3] penalized conflict interval 10666 = 1 * 10666
c [simplification-3] hard conflict limit 26668 (soft 16668 + delta 10000)
c [simplification-3] new conflict limit 16668 (hard 26668)
c 
c [simplification-4] limit 16668 conflicts (hard 26668) hit after 16668 conflicts
c [quatres-2] found 34768 quaternary clauses 13% in total
c [quatres-2-1] added 42 double-self-subsuming ternary resolvents
c [quatres-2-2] added 95 single-self-subsuming ternary resolvents
c [quatres-2-2] added 173 quaternary resolvents
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] all 12239 free variables schedulable
c [ternres-2] 25 ternary resolvents (2 bin, 23 trn)
c [ternres-2] fully completed ternary resolution
c [decomp-11] removed 1 variables
c [treelook-2] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-2] scheduled 1764 literals 7%
c [treelook-2] scheduling used 150003 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-2] used 150008 steps
c [treelook-2] 1232 literals remain 5%
c [treelook-2] 1210 variables remain to probed next time 10%
c [treelook-2] removed 0 variables, found 1 hbrs
c [unhide-3] limit 50000 with penalty 1 = 1 + 0
c [unhide-3-3] 0 units, 0 failed, 14 tauts, 0 hbrs, 64 literals
c [transred-2] limit 332779 with penalty 0 = 0 + 0
c [transred-2] removed 7 transitive binary clauses
c [block-2] scheduling all variables this time
c [block-2] scheduled 12238 variables 100%
c [block-2] limit of 25000000 steps penalty 1 = 1 + 0
c [block-2] fully completed
c [block-2] transition to [ all 0 rem 0 ] state
c [block-2] eliminated 234 blocked clauses
c [block-2] 234 < 1/100 * 271894 = 2718 considered unsuccessful
c [bca-2] limit of 10000000 steps and 543820 added (scaled 2)
c [bca-2] 12497 out of 24456 literals actually usable 51%
c [bca-2] added 0 blocked clauses in 123183 steps
c [sweep-3] limit 1000000 penalty 0 = 0 + 0
c [sweep-3-1] 2137 pos 31.9% + 4557 neg 68.1% = 6694 sched 54.7% ret 5533
c [sweep-3-1] 1000700 steps 617 queries 1023.49 avg class size
c [sweep-3-1] 12674 decisions 616 SAT calls 26.52 avg env size
c [sweep-3-1] 4080 variables remain 33% (8147 retained 67%)
c [decomp-13] removed 1 variables
c [sweep-3-1] removed 1 vars (0 failed, 0 eqs, 0 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 1 vars in TOTAL (1 rounds, 616 queries)
c [sort-queue-4] sorted 7940 enqueued variables after 16668 conflicts
c [score-dist-4] active 4286 (35%), one 4536 (37%), zero 3404 (28%)
c [score-dist-4] max exp 967, different 469 (48%)
c [score-dist-4] median active exp 820, avg 770.9
c [simplification-4] removed 13 variables 0.1% (12226 remain 94%)
c [simplification-4] removed 242 irredundant clauses 0.1% (271659 remain 88%)
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 30666
c [simplification-4] penalized conflict interval 30666 = 1 * 30666
c [simplification-4] hard conflict limit 62667 (soft 47334 + delta 15333)
c [simplification-4] new conflict limit 47334 (hard 62667)
c 
c [simplification-5] limit 47334 conflicts (hard 62667) hit after 47334 conflicts
c [quatres-3] found 36449 quaternary clauses 13% in total
c [quatres-3-1] added 60 double-self-subsuming ternary resolvents
c [quatres-3-2] added 236 single-self-subsuming ternary resolvents
c [quatres-3-2] added 262 quaternary resolvents
c [ternres-3] limit 4000000 with penalty 0 = 0 + 0
c [ternres-3] all 12226 free variables schedulable
c [ternres-3] 79 ternary resolvents (6 bin, 73 trn)
c [ternres-3] fully completed ternary resolution
c [gauss-2] limit 1000000 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 1198999 with penalty 0 = 0 + 0
c [transred-3] removed 0 transitive binary clauses
c [cce-3] limit of 15000000 steps penalty 1 = 1 + 0
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] allowing another 7500000 steps for small clauses
c [cce-3-1] scheduling 812 clauses = 315 binary + 497 ternary
c [cce-3-1] tried to eliminate 812 small clauses 100%
c [cce-3-1] eliminated 1 binary clauses 0%
c [cce-3-1] eliminated 37 ternary clauses 7%
c [cce-3-1] eliminated 38 small clauses 5%
c [cce-3-1] eliminated 38 small clauses in 7745210 steps
c [cce-3-1] completed small round (ACCE)
c [cce-3-1] eliminated 38 covered clauses in round 1
c [cce-3-2] incomplete large round (ACCE)
c [cce-3-2] allowing another 3627403 steps for small clauses
c [cce-3-2] scheduling 774 clauses = 314 binary + 460 ternary
c [cce-3-2] tried to eliminate 774 small clauses 100%
c [cce-3-2] completed small round (ACCE)
c [cce-3-2] eliminated 0 covered clauses in round 2
c [cce-3] eliminated 38 covered clauses in TOTAL during 2 rounds
c [cce-3] 38 < 1/100 * 271658 = 2716 considered unsuccessful
c [elim-4] scheduling all variables this time
c [elim-4] scheduled 12226 variables 100%
c [elim-4] boosting limit by 20
c [elim-4] limit of 239799890 steps penalty 1 = 1 + 0
c [elim-4] rescheduling of touched variables disabled
c [elim-4] incomplete 68 not tried 1% in round 1
c [elim-4] transition to [ all 1 rem 1 ] state
c [elim-4] eliminated 47 = 0% variables out of 12226 scheduled
c [elim-4] 47 < 1/100 * 12226 = 122 considered unsuccessful
c [sweep-4] limit 1000000 penalty 0 = 0 + 0
c [sweep-4-1] 1493 pos 36.9% + 2550 neg 63.1% = 4043 sched 33.2% ret 8136
c [sweep-4-1] 1000285 steps 722 queries 545.52 avg class size
c [sweep-4-1] 15995 decisions 722 SAT calls 29.53 avg env size
c [sweep-4-1] 1775 variables remain 15% (10404 retained 85%)
c [sweep-4-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 0 vars in TOTAL (1 rounds, 721 queries)
c [sort-queue-5] sorted 7061 enqueued variables after 47334 conflicts
c [score-dist-5] active 5118 (42%), one 5160 (42%), zero 1901 (16%)
c [score-dist-5] max exp 934, different 498 (53%)
c [score-dist-5] median active exp 744, avg 723.5
c [simplification-5] removed 47 variables 0.4% (12179 remain 94%)
c [simplification-5] removed 2666 irredundant clauses 1.0% (268993 remain 87%)
c [simplification-5] maximum reduction of 1% = max (0%, 1%)
c [simplification-5] geometric conflict interval increment 15333 = 30666 / 2
c [simplification-5] new conflict interval 45999
c [simplification-5] penalized conflict interval 45999 = 1 * 45999
c [simplification-5] hard conflict limit 116332 (soft 93333 + delta 22999)
c [simplification-5] new conflict limit 93333 (hard 116332)
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 -   22.9   12179   268993     79163   22286   3177   170   11   337   26   3%    696  107    9    6  158%
c 
c [simplification-6] limit 93333 conflicts (hard 116332) hit after 93333 conflicts
c [quatres-4] found 38340 quaternary clauses 14% in total
c [quatres-4-1] added 64 double-self-subsuming ternary resolvents
c [quatres-4-2] added 241 single-self-subsuming ternary resolvents
c [quatres-4-2] added 422 quaternary resolvents
c [ternres-4] limit 4000000 with penalty 0 = 0 + 0
c [ternres-4] all 12179 free variables schedulable
c [ternres-4] 12 ternary resolvents (3 bin, 9 trn)
c [ternres-4] fully completed ternary resolution
c [card-3] limit 500000 penalty 2 = 2 + 0
c [card-3] found 2 at-most-one constraints of average size 3.0
c [card-3] found 8 at-most-two constraints of average size 4.0
c [card-3] using previous limit 500000 for elimination
c [card-3] 10 out of 10 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [basicprobe-2] limit 5982857 penalty 1 = 1 + 0
c [basicprobe-2-0] 640 sched 5%, 0 failed, 0 lifted, 14 hbrs
c [basicprobe-2-1] 649 sched 5%, 0 failed, 0 lifted, 1 hbrs
c [basicprobe-2-2] 649 sched 5%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-2-2] fully completed probing
c [basicprobe-2-2] removed 0 variables, found 15 hbrs
c [bate-1] eliminated 9 asymmetric tautologies during probing
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 10000000 penalty 0 = 0 + 0
c [sweep-5-1] 818 pos 46.1% + 957 neg 53.9% = 1775 sched 14.6% ret 10404
c [sweep-5-1] 609447 steps 782 queries 180.31 avg class size
c [sweep-5-1] 13471 decisions 781 SAT calls 22.98 avg env size
c [sweep-5-1] fully completed sweeping round
c [sweep-5-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-5-2] 5890 pos 48.4% + 6289 neg 51.6% = 12179 sched 100.0% ret 0
c [sweep-5-2] 3479158 steps 1919 queries 546.87 avg class size
c [sweep-5-2] 39440 decisions 1919 SAT calls 28.66 avg env size
c [sweep-5-2] fully completed sweeping round
c [sweep-5-2] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-5-3] 5890 pos 48.4% + 6289 neg 51.6% = 12179 sched 100.0% ret 0
c [sweep-5-3] 3344311 steps 1850 queries 574.77 avg class size
c [sweep-5-3] 38524 decisions 1849 SAT calls 29.74 avg env size
c [sweep-5-3] fully completed sweeping round
c [sweep-5-3] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-5] removed 0 vars in TOTAL (3 rounds, 4548 queries)
c [sort-queue-6] sorted 4335 enqueued variables after 93333 conflicts
c [score-dist-6] active 7844 (64%), one 4046 (33%), zero 289 (2%)
c [score-dist-6] max exp 805, different 683 (85%)
c [score-dist-6] median active exp 524, avg 493.0
c [simplification-6] removed 0 variables 0.0% (12179 remain 94%)
c [simplification-6] removed 9 irredundant clauses 0.0% (268984 remain 87%)
c [simplification-6] maximum reduction of 0% = max (0%, 0%)
c [simplification-6] full geometric conflict interval increment 45999
c [simplification-6] new conflict interval 91998
c [simplification-6] penalized conflict interval 91998 = 1 * 91998
c [simplification-6] hard conflict limit 231330 (soft 185331 + delta 45999)
c [simplification-6] new conflict limit 185331 (hard 231330)
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 -   32.8   12179   268984    151001   41611   4557   240   11   333   27   3%    914   15   11    8  142%
c 
c [simplification-7] limit 185331 conflicts (hard 231330) hit after 185331 conflicts
c [quatres-5] found 44198 quaternary clauses 15% in total
c [quatres-5-1] added 125 double-self-subsuming ternary resolvents
c [quatres-5-2] added 531 single-self-subsuming ternary resolvents
c [quatres-5-2] added 545 quaternary resolvents
c [ternres-5] limit 4903213 with penalty 0 = 0 + 0
c [ternres-5] all 12179 free variables schedulable
c [ternres-5] 34 ternary resolvents (7 bin, 27 trn)
c [ternres-5] fully completed ternary resolution
c [unhide-4] limit 245160 with penalty 2 = 2 + 0
c [unhide-4-4] 0 units, 0 failed, 165 tauts, 0 hbrs, 411 literals
c [transred-4] limit 1000000 with penalty 1 = 1 + 0
c [transred-4] removed 2 transitive binary clauses
c [block-3] scheduling all variables this time
c [block-3] scheduled 12179 variables 100%
c [block-3] limit of 12500000 steps penalty 2 = 2 + 0
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 304 blocked clauses
c [block-3] 304 < 1/100 * 268984 = 2689 considered unsuccessful
c [bca-3] limit of 10000000 steps and 537860 added (scaled 2)
c [bca-3] 3692 out of 24304 literals actually usable 15%
c [bca-3] added 0 blocked clauses in 103833 steps
c [sort-queue-7] sorted 8604 enqueued variables after 185331 conflicts
c [score-dist-7] active 3547 (29%), one 8457 (70%), zero 147 (1%)
c [score-dist-7] max exp 729, different 393 (54%)
c [score-dist-7] median active exp 665, avg 591.5
c [simplification-7] removed 28 variables 0.2% (12151 remain 93%)
c [simplification-7] removed 304 irredundant clauses 0.1% (268680 remain 87%)
c [simplification-7] maximum reduction of 0% = max (0%, 0%)
c [simplification-7] full geometric conflict interval increment 91998
c [simplification-7] new conflict interval 183996
c [simplification-7] penalized conflict interval 183996 = 1 * 183996
c [simplification-7] hard conflict limit 461325 (soft 369327 + delta 91998)
c [simplification-7] new conflict limit 369327 (hard 461325)
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 -   43.4   12151   268680    222084   57042   5772   270   10   617   29   2%    987  151   11    9  116%
c -   53.0   12151   268680    290462   69117   6335   277   13   466   29   3%   1011   -8   13   11  125%
c -   62.0   12151   268680    358532   82677   6910   284   11   551   30   2%   1019   36    9   11   77%
c 
c [simplification-8] limit 369327 conflicts (hard 461325) hit after 369327 conflicts
c [quatres-6] found 52904 quaternary clauses 16% in total
c [quatres-6-1] removed 4 duplicate quaternary clauses
c [quatres-6-1] added 168 double-self-subsuming ternary resolvents
c [quatres-6-2] added 854 single-self-subsuming ternary resolvents
c [quatres-6-2] added 598 quaternary resolvents
c [ternres-6] limit 10747514 with penalty 0 = 0 + 0
c [ternres-6] all 12151 free variables schedulable
c [ternres-6] 68 ternary resolvents (5 bin, 63 trn)
c [ternres-6] fully completed ternary resolution
c [gauss-3] limit 537375 penalty 2 = 2 + 0
c [gauss-3] extracted 0 xors of average arity 0.0
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [simpleprobe-3] 4047 schedulable variables 33%
c [simpleprobe-3] limit 21495029 penalty 1 = 1 + 0
c [simpleprobe-3] 2624 variables remain 22% (9527 retained 78%)
c [simpleprobe-3] removed 0 variables, found 11 hbrs, 0 units
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 4 transitive binary clauses
c [cce-4] boosting limit by 10
c [cce-4] limit of 134343935 steps penalty 2 = 2 + 0
c [cce-4-1] eliminated 73 clauses out of 76490 (0%) of length 7
c [cce-4-1] eliminated 1030 clauses out of 89185 (1%) of length 6
c [cce-4-1] eliminated 5214 clauses out of 59638 (9%) of length 5
c [cce-4-1] incomplete large round (ATE)
c [cce-4-1] eliminated 6317 large clauses in 134344051 steps
c [cce-4-1] allowing another 67172025 steps for small clauses
c [cce-4-1] scheduling 1066 clauses = 331 binary + 735 ternary
c [cce-4-1] tried to eliminate 1066 small clauses 100%
c [cce-4-1] eliminated 1 binary clauses 0%
c [cce-4-1] eliminated 15 ternary clauses 2%
c [cce-4-1] eliminated 16 small clauses 2%
c [cce-4-1] eliminated 16 small clauses in 67517050 steps
c [cce-4-1] completed small round (ATE)
c [cce-4-1] eliminated 6333 covered clauses in round 1
c [cce-4-2] incomplete large round (ATE)
c [cce-4-2] allowing another 33413450 steps for small clauses
c [cce-4-2] scheduling 1050 clauses = 330 binary + 720 ternary
c [cce-4-2] tried to eliminate 1050 small clauses 100%
c [cce-4-2] completed small round (ATE)
c [cce-4-2] eliminated 0 covered clauses in round 2
c [cce-4] eliminated 6333 covered clauses in TOTAL during 2 rounds
c [elim-5] 68 variables 1% will be scheduled this time
c [elim-5] scheduled 68 variables 1%
c [elim-5] limit of 53737574 steps penalty 2 = 2 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5-1] no variable eliminated in round 1 in 4062611 steps
c [elim-5] fully completed in 1 rounds
c [elim-5] transition to [ all 0 rem 0 ] state
c [elim-5] eliminated 0 = 0% variables out of 68 scheduled
c [sweep-6] limit 1612127 penalty 1 = 1 + 0
c [sweep-6-1] 5968 pos 49.1% + 6183 neg 50.9% = 12151 sched 100.0% ret 0
c [sweep-6-1] 1612872 steps 498 queries 1414.31 avg class size
c [sweep-6-1] 16390 decisions 497 SAT calls 46.15 avg env size
c [sweep-6-1] 6873 variables remain 57% (5278 retained 43%)
c [sweep-6-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-6] removed 0 vars in TOTAL (1 rounds, 497 queries)
c [sort-queue-8] sorted 8001 enqueued variables after 369327 conflicts
c [score-dist-8] active 4150 (34%), one 7940 (65%), zero 61 (1%)
c [score-dist-8] max exp 608, different 364 (60%)
c [score-dist-8] median active exp 514, avg 483.3
c [simplification-8] removed 0 variables 0.0% (12151 remain 93%)
c [simplification-8] removed 6341 irredundant clauses 2.4% (262339 remain 85%)
c [simplification-8] maximum reduction of 2% = max (0%, 2%)
c [simplification-8] geometric conflict interval increment 61332 = 183996 / 3
c [simplification-8] new conflict interval 245328
c [simplification-8] penalized conflict interval 245328 = 1 * 245328
c [simplification-8] hard conflict limit 737319 (soft 614655 + delta 122664)
c [simplification-8] new conflict limit 614655 (hard 737319)
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 -   71.5   12151   262339    431952   99899   8550   306   10   604   32   2%   1022   72   10   11   94%
c -   79.1   12151   262339    504570  115921   9082   311   12   532   33   2%   1024  -17   13   11  116%
c -   87.6   12151   262339    571562  124306   9308   311   14   533   34   3%   1024  -19   12   12  100%
c 
c [simplification-9] limit 614655 conflicts (hard 737319) hit after 614655 conflicts
c [quatres-7] found 63673 quaternary clauses 17% in total
c [quatres-7-1] removed 8 duplicate quaternary clauses
c [quatres-7-1] added 137 double-self-subsuming ternary resolvents
c [quatres-7-2] added 1122 single-self-subsuming ternary resolvents
c [quatres-7-2] added 685 quaternary resolvents
c [ternres-7] limit 17190863 with penalty 0 = 0 + 0
c [ternres-7] all 12151 free variables schedulable
c [ternres-7] 19 ternary resolvents (4 bin, 15 trn)
c [ternres-7] fully completed ternary resolution
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 5 transitive binary clauses
c [sort-queue-9] sorted 1305 enqueued variables after 614655 conflicts
c [score-dist-9] active 10846 (89%), one 1302 (11%), zero 3 (0%)
c [score-dist-9] max exp 664, different 434 (65%)
c [score-dist-9] median active exp 514, avg 426.4
c [simplification-9] removed 0 variables 0.0% (12151 remain 93%)
c [simplification-9] removed 0 irredundant clauses 0.0% (262339 remain 85%)
c [simplification-9] maximum reduction of 0% = max (0%, 0%)
c [simplification-9] full geometric conflict interval increment 245328
c [simplification-9] new conflict interval 490656
c [simplification-9] penalized conflict interval 490656 = 1 * 490656
c [simplification-9] hard conflict limit 1350639 (soft 1105311 + delta 245328)
c [simplification-9] new conflict limit 1105311 (hard 1350639)
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 -   96.2   12151   262339    641311  133618  10800   311   11   575   34   2%   1024   35    9   13   72%
c -  105.3   12151   262339    715679  145713  11037   312   14   572   35   2%   1024   -0   16   13  118%
c -  114.0   12151   262339    797250  157949  11321   314   14   626   36   2%   1024   71    9   14   64%
c 1  120.7   12151   262339    868160  215653  11511   314   13   552   50   2%   1024  -90    6   15   44%
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: 9 basic ate = 9 trn 100% + 0 lrg 0% in 1 updates
c bcas: 3 count, 0 added (0 skipped), 419650 steps
c bkwd: tried 3739 clauses, 7432 lits, 1.99 lits/clause
c bkwd: checked 415391 occs, 111.10 occs/clause, 55.89 occs/lit
c bkwd: subsumed 0 binary, 2 ternary, 5 large
c bkwd: strengthened 0 binary, 1 ternary (100% self), 109 large (0% self)
c blkd: 3 bces, 1776 removed, 15580633 resolutions, 26998058 steps
c blkd: 220 blocking literals 1%, 39 pure
c bump: 799843 bumped seen, 19170757 lits 24.0 on average
c card: 3 count, 0 units, 0 am1, 3929881 steps
c card: 0 rescheduled, 0 eliminated, 0 resolved, 714 subsumed
c card: 8 at-most-one constraints found, average size 3.00
c card: 8 at-most-one constraints used 100%, average size 3.00
c card: 25 at-most-two constraints found, average size 4.08
c card: 24 at-most-two constraints used 96%, average size 4.08
c cces: 4 cces, 15697 eliminated, 15697 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: 3616992 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 40 gcs, 0 rescored clauses, 420 rescored vars
c dcps: 26 decompositions, 35 equivalent 0%
c deco: 22 decision-only clauses 0%, 45% reduction
c decs: 26030726 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 5 elims, 825 eliminated 6%, 2 pure 0%
c elms: 7 rounds, 1.4 rounds/bve
c elms: 773 small 94%, 11 large 1%
c elms: 2268 tried small, 773 succeeded 34%, 1495 failed 66%
c elms: 17417 subsumed, 9473 strengthened, 0 blocked
c elms: 2349931 copies, 6647423 resolutions, 584272 ipos
c elms: 615111 subchks, 365423 strchks
c gaus: 3 extractions, 1121 extracted, 5.0 size, 5 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 7075502 steps, 3537751 extr 50%, 20520 elim 0%
c glue: 11.7 orig avg, 11.7 real avg, 2.4 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 78 = 14 simple 18% + 63 trn 81% + 1 lrg 1%, 38 sub 49%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 799843 clauses, 17.0 length
c lrnd: 13620562 lits = 14049912 orig - 429350 removed 3%
c lrnd: 353391 uips 44%, 299203 flips 37%
c mins: 586574 mins 73%, 93 bin 0%, 213109 size 27%
c mins: 6605924 poisoned searches, 416046 hits, 6% hit rate
c mins: 17946763 used twice searches, 6237289 hits, 35% hit rate
c move: moved 1416, 15 bin 1%, 1401 trn 99%
c otfs: 76976 driving 58%, 56469 restarting 42%
c otfs: str 133445, 129190 red 97%, 4255 irr 3%
c otfs: str 133445, 0 bin 0%, 126 trn 0%, 133319 lrg 100%
c otfs: sub 1744, 1740 red 100%, 4 irr 0%
c otfs: sub 1744, 0 bin 0%, 28 trn 2%, 1716 lrg 98%
c phas: 1 computed, 12516 set, 0 pos (0%), 12516 neg (100%)
c prbs: 2 basic, 7022 probed, 0 failed, 0 lifted
c prbs: 3 simple, 26807 probed, 4 failed, 1 eqs
c prbs: 2 treelook, 1511 probed, 0 failed, 0 lifted
c prom: 56426 locked 37% out of 153365 tried
c prps: 131606988 props, 5 props/dec
c prps: 100% srch, 0% simp, 0% lkhd
c quat: 7 count, 2955 quat, 3167 self1, 610 self2, 14 dup
c queu: 9 sorted, 26030726 next (19701050 steps 0.76)
c queu: 21150048 enq (20674566 steps 0.98), 19170757 deq 91%
c redc: 87 clauses 0%, 212440 tried 24%, 1 sat 0%
c redc: 88 lits 0%, 1408490 tried 10%, 1 sat 0%
c redc: 10 times jump level reduced, 11.4 levels on average
c reds: 11 count, 78923.6 conflicts per reduce
c reds: 0 memlim 0%, 11 arith 100%
c reds: 274749 collected 51%, 269042 retired 49%
c rmbd: 10 removed, 0 red 0%
c rsts: 25849 restarts 100%, 0 skipped 0%
c rsts: 0 saturating 0%, 0 reuse 0%
c rsts: 0 kept 0.0% average 0.0%
c scnc: 1 count, 1.200 min (200/1000), 1.200 max (200/1000)
c simp: 9 count, 9 confs 100%, 0 vars 0%
c simp: 0 its 0%, 0 bin 0%, 0 trns 0%
c subl: 799843 count (336305 tried 0.4), 30370 sub out of 796048 (3.8%)
c swps: 6 count, 8 rounds, 7269 queries (908.6/round)
c swps: 7270 sat calls, 2 unsat (1.2% success rate)
c swps: 156794 decisions 21.6, 8659 conflicts 1.2
c swps; 769.2 avg class size, 29.6 avg environment size
c swps: 0 failed, 0 impls, 1 equivs
c swp0: 2420 type 0 queries, 5 unsat (0.2%), 2420 sat (100.0%)
c swp1: 4849 type 1 queries, 73 unsat (1.5%), 4848 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: 53662147 calls to obtain time
c tops: 397 fixed 3%, 4 its, 217040.00 confs/it
c trds: 6 transitive reductions, 24 removed, 1 failed
c trds: 145202 nodes, 3095 edges, 3968 steps
c trim: 377948 words, 1.4 MB
c trnr: 7 count, 41 bin, 344 trn, 11742201 steps
c unhd: 4 count, 4 rounds, 2154464 steps
c unhd: 0 non-trivial sccs of average size 0.0
c unhd: 0 units, 0 bin, 0 trn, 0 lrg
c unhd: 12 failed, 12 stamp, 0 lits, 0 bin, 0 trn, 0 lrg
c unhd: 972 tauts, 0 bin 0%, 714 trn 73%, 250 lrg 26%
c unhd: 972 tauts, 8 stamp 1%, 465 red 48%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 613 str, 0 bin 0%, 32 trn 5%, 581 lrg 95%, 519 red 85%
c vars: 12151 remaining 91% and 1257 removed 9% out of 13408
c vars: 397 fixed 3%, 825 eliminated 6%, 35 equivalent 0%
c vsts: 2397847729 visits, 100% srch, 0% simp, 0% lkhd
c vsts: 18.2 search visits per propagation, 2754.6 per conflict
c wchs: 956368227 pushed, 13002304 enlarged, 139 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all         799003        274749        269042      19079706       1899072        317411
c 
c  0 0        173049  22       922   0         0   0  15095528  79<  1216221  64    177753  56     4.5
c  1 5        134622  17     63537  23     59594  22   2374838  12    215154  11<    44370  14<    0.6
c  2 6        140906  18<    61890  23     66197  25    973348   5    162307   9     40036  13     0.7
c  3 9        135054  17     58800  21<    58777  22<   310987   2    124147   7     26180   8     1.1
c  4 14        97318  12     41950  15     37242  14    162387   1     92500   5     17701   6     1.2
c  5 21        64770   8     25466   9     22849   8     93080   0     55489   3      7920   2     1.0
c  6 30        27459   3     11829   4     12036   4     36901   0     18779   1      2236   1     0.7
c  7 41        13498   2      5545   2      6275   2     17372   0      7935   0       658   0     0.5
c  8 54         6676   1      2615   1      3288   1      8336   0      3593   0       255   0     0.4
c  9 69         3069   0      1190   0      1489   1      3782   0      1619   0       155   0     0.3
c 10 86         2091   0       805   0      1060   0      2560   0      1064   0       111   0     0.3
c 11 126         437   0       178   0       220   0       512   0       224   0        28   0     0.2
c 12 230          25   0        14   0         8   0        34   0        24   0         7   0     0.0
c 13 534          29   0         8   0         7   0        41   0        16   0         1   0     0.0
c 
c avg                  2.4           3.0           3.0           0.4           0.9           1.1
c std                  2.0           1.7           1.8           0.9           1.6           1.5
c 
c   14.613  12% decide
c    4.881   4% elim
c    4.470   4% cce
c    3.059   3% bump
c    2.550   2% sweep
c    1.950   2% block
c    1.816   2% probe
c    0.888   1% quatres
c    0.482   0% gauss
c 
c    1.252 < 1% rest (below)
c 
c    0.456   0% bca
c    0.375   0% rescore
c    0.208   0% unhide
c    0.101   0% card
c    0.084   0% ternres
c    0.027   0% transred
c    0.000   0% locs
c    0.000   0% queuesort
c ==================================
c    1.318   1% preprocessing     7%
c   18.472  15% inprocessing     93%
c ==================================
c   19.791  16% simplifying
c  100.884  84% search
c ==================================
c  120.675 100% all
c 
c        868160 conflicts,        7194.2 confs/sec
c          3262 ternaries,         266.1 confs/ternary
c           144 binaries,         6028.9 confs/binary
c             4 iterations,     217040.0 confs/iteration
c 
c            11 reductions,          0.1 redus/sec,  78923.6 confs/reduction
c         25849 restarts,          214.2 rests/sec,     33.6 confs/restart
c      26030726 decisions,      215708.5 decis/sec,     30.0 decis/conflict
c     131606988 propagations,  1090585.8 props/sec,      5.1 props/decision
c 
c 120.7 seconds, 72.6 MB
c launch: done
