c launch: /data/cnf/sc2014/app/atco_enc2_opt2_20_11.cnf.bz2
c host: atom25
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/atco_enc2_opt2_20_11.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/atco_enc2_opt2_20_11.cnf.bz2
c no embedded options
c found 'p cnf 167075 6571833' header
c read 167075 variables, 6571833 clauses, 21183250 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=4
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 166190 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] VSIDS (--score=4) decay interval 256 (--vsidsdint=256)
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  166190  6549347         0       0      0     0    0     0  290   0%      0    0    0    0    0%
c 
c [simplification-1] limit 0 conflicts (hard 0) hit after 0 conflicts
c [card-1] limit 1637336 based on 6549347 irredundant clauses
c [card-1] found 1558 at-most-one constraints of average size 3.0
c [card-1] no at-most-two constraint found
c [card-1] using previous limit 1637336 for elimination
c [card-1] 1558 out of 1558 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 5689 variables
c [simpleprobe-1] all 161386 free variables schedulable
c [simpleprobe-1] boosting simple probing limit by 10
c [simpleprobe-1] limit 12996764 based on 6498382 irredundant clauses
c [decomp-2] removed 3 variables
c [simpleprobe-1] 161383 variables remain 100% (0 retained 0%)
c [simpleprobe-1] removed 3 variables, found 1170 hbrs, 0 units
c [unhide-1] limit 406148 based on 6498379 irredundant clauses
c [unhide-1-1] 3 units, 116 failed, 98952 tauts, 0 hbrs, 15 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 161301 variables 100%
c [elim-1] limit of 6402394 steps based on 6402394 irredundant clauses
c [elim-1] rescheduling of touched variables disabled
c [elim-1] incomplete 158434 not tried 98% in round 1
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 2867 = 2% variables out of 161301 scheduled
c [elim-1] considered successful since not run to completion yet
c [phase-count-1] 5244728 negative 83.1% of 6310279 except 1065551 16.9%
c [phase-count-1] 5367308 positive 85.1% of 6310279 except 942971 14.9%
c [phase-1] phase bias: 69404 positive 44%, 89030 negative 56%
c [sort-queue-1] sorted 158434 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 158434 (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 6206 variables 3.8% (158434 remain 95%)
c [simplification-1] removed 239068 irredundant clauses 3.7% (6310279 remain 96%)
c [simplification-1] maximum reduction of 4% = max (4%, 4%)
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 [simplification-2] limit 4000 conflicts (hard 14000) hit after 4001 conflicts
c [decomp-3] removed 19 variables
c [simpleprobe-2] all 158415 free variables schedulable
c [simpleprobe-2] limit 12620520 based on 6310260 irredundant clauses
c [decomp-4] removed 79 variables
c [simpleprobe-2] 158336 variables remain 100% (0 retained 0%)
c [simpleprobe-2] removed 79 variables, found 1230 hbrs, 0 units
c [treelook-1] limit 1577544 based on 6310179 irredundant clauses
c [treelook-1] scheduled 32513 literals 10%
c [treelook-1] scheduling used 1583281 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 1577544 based on 6310179 irredundant clauses
c [treelook-1] used 1582416 steps
c [treelook-1] 32491 literals remain 10%
c [treelook-1] 30815 variables remain to probed next time 19%
c [decomp-5] removed 3 variables
c [treelook-1] removed 3 variables, found 1191 hbrs
c [basicprobe-1] limit 50481432 based on 6310179 irredundant clauses
c [basicprobe-1-0] 5578 probes remain 4% after last round
c [basicprobe-1-0] 93 units = 93 failed (100%) + 0 lifted (0%)
c [basicprobe-1-0] removed 122 variables, found 36280 hbrs
c [unhide-2] limit 394386 based on 6310179 irredundant clauses
c [unhide-2-2] 0 units, 6 failed, 15265 tauts, 0 hbrs, 1964 literals
c [elim-2] 158205 variables 100% will be scheduled this time
c [elim-2] scheduled 158205 variables 100%
c [elim-2] limit of 6308537 steps based on 6308537 irredundant clauses
c [elim-2] rescheduling of touched variables disabled
c [elim-2] incomplete 156008 not tried 99% in round 1
c [elim-2] transition to [ all 0 rem 1 ] state
c [elim-2] eliminated 2197 = 1% variables out of 158205 scheduled
c [elim-2] considered successful since not run to completion yet
c [phase-count-2] 5145197 negative 83.0% of 6201573 except 1056376 17.0%
c [phase-count-2] 5258564 positive 84.8% of 6201573 except 943009 15.2%
c [phase-2] phase bias: 2835 positive 62%, 1718 negative 38%
c [sort-queue-2] sorted 154232 enqueued variables after 4001 conflicts
c [score-dist-2] active 1776 (1%), one 0 (0%), zero 154232 (99%)
c [score-dist-2] max exp 509, different 24 (5%)
c [score-dist-2] median active exp 502, avg 500.5
c [simplification-2] removed 2426 variables 1.5% (156008 remain 94%)
c [simplification-2] removed 108706 irredundant clauses 1.7% (6201573 remain 95%)
c [simplification-2] maximum reduction of 2% = max (2%, 2%)
c [simplification-2] geometric conflict interval increment 6666 = 20000 / 3
c [simplification-2] new conflict interval 10666
c [simplification-2] penalized conflict interval 10666 = 1 * 10666
c [simplification-2] hard conflict limit 24667 (soft 14667 + delta 10000)
c [simplification-2] new conflict limit 14667 (hard 24667)
c 
c [simplification-3] limit 14667 conflicts (hard 24667) hit after 14667 conflicts
c [card-2] limit 1550393 based on 6201573 irredundant clauses
c [card-2] found 1283 at-most-one constraints of average size 3.0
c [card-2] no at-most-two constraint found
c [card-2] using previous limit 1550393 for elimination
c [card-2] 1283 out of 1283 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [decomp-6] removed 2222 variables
c [treelook-2] limit 1550036 based on 6200144 irredundant clauses
c [treelook-2] scheduled 38170 literals 12%
c [treelook-2] scheduling used 1562144 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 1550036 based on 6200144 irredundant clauses
c [treelook-2] used 1639131 steps
c [treelook-2] 38091 literals remain 12%
c [treelook-2] 12555 variables remain to probed next time 8%
c [decomp-7] removed 7 variables
c [treelook-2] removed 7 variables, found 577 hbrs
c [unhide-3] limit 387508 based on 6200142 irredundant clauses
c [unhide-3-3] 0 units, 1 failed, 6227 tauts, 0 hbrs, 4801 literals
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 153778 variables 100%
c [elim-3] limit of 20735966 steps penalty 3 = 0 + 3
c [elim-3] rescheduling of touched variables disabled
c [elim-3] incomplete 121453 not tried 79% in round 1
c [elim-3] transition to [ all 1 rem 1 ] state
c [elim-3] eliminated 15580 = 10% variables out of 153778 scheduled
c [elim-3] considered successful since not run to completion yet
c [phase-count-3] 5001413 negative 82.6% of 6053821 except 1052408 17.4%
c [phase-count-3] 5152511 positive 85.1% of 6053821 except 901310 14.9%
c [phase-3] phase bias: 3641 positive 83%, 768 negative 17%
c [sort-queue-3] sorted 136365 enqueued variables after 14667 conflicts
c [score-dist-3] active 1833 (1%), one 0 (0%), zero 136365 (99%)
c [score-dist-3] max exp 510, different 64 (13%)
c [score-dist-3] median active exp 500, avg 491.8
c [simplification-3] removed 17810 variables 11.4% (138198 remain 83%)
c [simplification-3] removed 147752 irredundant clauses 2.4% (6053821 remain 92%)
c [simplification-3] maximum reduction of 11% = max (11%, 2%)
c [simplification-3] large reduction 11% >= 5% limit
c [simplification-3] next conflict interval 2000 = 2000/1
c [simplification-3] penalized conflict interval 2000 = 1 * 2000
c [simplification-3] hard conflict limit 26667 (soft 16667 + delta 10000)
c [simplification-3] new conflict limit 16667 (hard 26667)
c 
c [simplification-4] limit 16667 conflicts (hard 26667) hit after 16668 conflicts
c [decomp-8] removed 123 variables
c [basicprobe-2] limit 48428696 based on 6053587 irredundant clauses
c [basicprobe-2-0] 1731 probes remain 1% after last round
c [basicprobe-2-0] 6 units = 6 failed (100%) + 0 lifted (0%)
c [basicprobe-2-0] removed 7 variables, found 24213 hbrs
c [unhide-4] limit 378349 based on 6053587 irredundant clauses
c [unhide-4-4] 0 units, 0 failed, 12137 tauts, 0 hbrs, 4528 literals
c [elim-4] 121328 variables 88% will be scheduled this time
c [elim-4] scheduled 121328 variables 88%
c [elim-4] boosting limit by 20
c [elim-4] limit of 469614037 steps penalty 3 = 0 + 3
c [elim-4] rescheduling of touched variables disabled
c [elim-4] incomplete 67827 not tried 49% in round 1
c [elim-4] transition to [ all 0 rem 1 ] state
c [elim-4] eliminated 739 = 1% variables out of 121328 scheduled
c [elim-4] considered successful since not run to completion yet
c [phase-count-4] 4996980 negative 82.6% of 6047227 except 1050247 17.4%
c [phase-count-4] 5138754 positive 85.0% of 6047227 except 908473 15.0%
c [phase-4] phase bias: 1726 positive 67%, 834 negative 33%
c [sort-queue-4] sorted 135396 enqueued variables after 16668 conflicts
c [score-dist-4] active 1933 (1%), one 0 (0%), zero 135396 (99%)
c [score-dist-4] max exp 508, different 70 (14%)
c [score-dist-4] median active exp 499, avg 490.8
c [simplification-4] removed 869 variables 0.6% (137329 remain 83%)
c [simplification-4] removed 6594 irredundant clauses 0.1% (6047227 remain 92%)
c [simplification-4] maximum reduction of 1% = max (1%, 0%)
c [simplification-4] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-4] new conflict interval 20666
c [simplification-4] penalized conflict interval 20666 = 1 * 20666
c [simplification-4] hard conflict limit 47667 (soft 37334 + delta 10333)
c [simplification-4] new conflict limit 37334 (hard 47667)
c 
c [simplification-5] limit 37334 conflicts (hard 47667) hit after 37335 conflicts
c [quatres-1] found 145425 quaternary clauses 30% in total
c [quatres-1-2] added 131 single-self-subsuming ternary resolvents
c [quatres-1-2] added 264 quaternary resolvents
c [ternres-1] boosting ternary resolution limit by 5
c [ternres-1] limit 24188908 based on 6047227 irredundant clauses
c [ternres-1] all 137329 free variables schedulable
c [ternres-1] 26 ternary resolvents (0 bin, 26 trn)
c [ternres-1] 133767 variables remain 97% (3562 retained 3%)
c [gauss-1] limit 3023613 based on 6047227 irredundant clauses
c [gauss-1] extracted 32 xors of average arity 2.7
c [gauss-1] connected 86 occurrences of 85 variables (average 1.0)
c [gauss-1] limit 3023613 based on 6047227 irredundant clauses
c [gauss-1] fully completed
c [gauss-1] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-9] removed 811 variables
c [simpleprobe-3] all 136518 free variables schedulable
c [simpleprobe-3] limit 12093776 based on 6046888 irredundant clauses
c [decomp-10] removed 4 variables
c [simpleprobe-3] 136514 variables remain 100% (0 retained 0%)
c [simpleprobe-3] removed 4 variables, found 729 hbrs, 0 units
c [transred-1] limit 6046880 based on 6046880 irredundant clauses
c [transred-1] removed 1887 transitive binary clauses
c [block-1] scheduling all variables this time
c [block-1] scheduled 136514 variables 100%
c [block-1] boosting limit by 10
c [block-1] limit of 270053036 steps penalty 3 = 0 + 3
c [block-1] fully completed
c [block-1] transition to [ all 0 rem 0 ] state
c [block-1] eliminated 8938 blocked clauses
c [block-1] 8938 < 1/100 * 6045691 = 60456 considered unsuccessful
c [cce-1] limit of 13502651 steps penalty 3 = 0 + 3
c [cce-1-1] eliminated 5 clauses out of 11 (45%) of length 26
c [cce-1-1] eliminated 9 clauses out of 192 (5%) of length 25
c [cce-1-1] eliminated 7 clauses out of 755 (1%) of length 24
c [cce-1-1] eliminated 7 clauses out of 2730 (0%) of length 23
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 28 large clauses in 13502860 steps
c [cce-1-1] allowing another 6751430 steps for small clauses
c [cce-1-1] scheduling 5525713 clauses = 323897 binary + 5201816 ternary
c [cce-1-1] tried to eliminate 207 small clauses 0%
c [cce-1-1] eliminated 3 binary clauses 0%
c [cce-1-1] eliminated 4 ternary clauses 0%
c [cce-1-1] eliminated 7 small clauses 0%
c [cce-1-1] eliminated 7 small clauses in 13502663 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 35 covered clauses in round 1
c [cce-1] eliminated 35 covered clauses in TOTAL during 1 rounds
c [cce-1] 35 < 1/100 * 6036753 = 60367 considered unsuccessful
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 136514 variables 100%
c [elim-5] limit of 54010607 steps penalty 3 = 0 + 3
c [elim-5] rescheduling of touched variables disabled
c [elim-5] incomplete 102867 not tried 75% in round 1
c [elim-5] transition to [ all 1 rem 1 ] state
c [elim-5] eliminated 422 = 0% variables out of 136514 scheduled
c [elim-5] 422 < 1/100 * 136514 = 1365 considered unsuccessful
c [bca-1] limit of 10000000 steps and 12070018 added (scaled 2)
c [bca-1] 269109 out of 272186 literals actually usable 99%
c [bca-1] added 8312 blocked clauses in 727446 steps
c [sweep-1] limit 12069518 based on 6034759 irredundant clauses
c [sweep-1-1] 26255 pos 19.3% + 109837 neg 80.7% = 136092 sched 100.0% ret 0
c [sweep-1-1] 12090295 steps 114 queries 26656.74 avg class size
c [sweep-1-1] 4411 decisions 105 SAT calls 226.71 avg env size
c [sweep-1-1] 135158 variables remain 99% (934 retained 1%)
c [decomp-11] removed 55 variables
c [sweep-1-1] removed 55 vars (0 failed, 12 eqs, 7 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 55 vars in TOTAL (1 rounds, 113 queries)
c [phase-count-5] 4986729 negative 82.6% of 6034711 except 1047982 17.4%
c [phase-count-5] 5127700 positive 85.0% of 6034711 except 907011 15.0%
c [phase-5] phase bias: 656 positive 64%, 367 negative 36%
c [sort-queue-5] sorted 133357 enqueued variables after 37335 conflicts
c [score-dist-5] active 2680 (2%), one 0 (0%), zero 133357 (98%)
c [score-dist-5] max exp 509, different 135 (26%)
c [score-dist-5] median active exp 501, avg 479.2
c [simplification-5] removed 1292 variables 0.9% (136037 remain 82%)
c [simplification-5] removed 12516 irredundant clauses 0.2% (6034711 remain 92%)
c [simplification-5] maximum reduction of 1% = max (1%, 0%)
c [simplification-5] geometric conflict interval increment 10333 = 20666 / 2
c [simplification-5] new conflict interval 30999
c [simplification-5] penalized conflict interval 30999 = 1 * 30999
c [simplification-5] hard conflict limit 83833 (soft 68334 + delta 15499)
c [simplification-5] new conflict limit 68334 (hard 83833)
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 -  109.4  136037  6034711     59169   26873   8011 30559   12    20  390  61%    602    9   12    7  176%
c 
c [simplification-6] limit 68334 conflicts (hard 83833) hit after 68335 conflicts
c [quatres-2] found 146185 quaternary clauses 30% in total
c [quatres-2-1] removed 2 duplicate quaternary clauses
c [quatres-2-2] added 7 single-self-subsuming ternary resolvents
c [quatres-2-2] added 56 quaternary resolvents
c [ternres-2] limit 24138836 based on 6034709 irredundant clauses
c [ternres-2] 132495 schedulable variables 97%
c [ternres-2] 19 ternary resolvents (0 bin, 19 trn)
c [ternres-2] 129026 variables remain 95% (7011 retained 5%)
c [card-3] limit 1508677 based on 6034709 irredundant clauses
c [card-3] found 642 at-most-one constraints of average size 3.5
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 1508677 for elimination
c [card-3] 642 out of 642 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [decomp-12] removed 2 variables
c [treelook-3] limit 1508676 based on 6034707 irredundant clauses
c [treelook-3] scheduled 30677 literals 11%
c [treelook-3] scheduling used 1508679 steps
c [treelook-3] not fully scheduled
c [treelook-3] limit 1508676 based on 6034707 irredundant clauses
c [treelook-3] used 1548903 steps
c [treelook-3] 30594 literals remain 11%
c [treelook-3] 5485 variables remain to probed next time 4%
c [decomp-13] removed 2 variables
c [treelook-3] removed 12 variables, found 970 hbrs
c [unhide-5] limit 377164 based on 6034632 irredundant clauses
c [unhide-5-5] 0 units, 0 failed, 3644 tauts, 0 hbrs, 9906 literals
c [transred-2] limit 6031647 based on 6031647 irredundant clauses
c [transred-2] removed 1406 transitive binary clauses
c [bca-2] limit of 10000000 steps and 12066838 added (scaled 2)
c [bca-2] 268960 out of 272048 literals actually usable 99%
c [bca-2] added 43 blocked clauses in 727870 steps
c [sweep-2] limit 12062182 based on 6031091 irredundant clauses
c [sweep-2-1] 30382 pos 22.5% + 104721 neg 77.5% = 135103 sched 99.3% ret 920
c [sweep-2-1] 12079182 steps 111 queries 23430.64 avg class size
c [sweep-2-1] 3677 decisions 100 SAT calls 192.51 avg env size
c [sweep-2-1] 134151 variables remain 99% (1872 retained 1%)
c [decomp-14] removed 55 variables
c [sweep-2-1] removed 55 vars (0 failed, 11 eqs, 7 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 55 vars in TOTAL (1 rounds, 110 queries)
c [phase-count-6] 4983516 negative 82.6% of 6031048 except 1047532 17.4%
c [phase-count-6] 5125252 positive 85.0% of 6031048 except 905796 15.0%
c [phase-6] phase bias: 376 positive 51%, 356 negative 49%
c [sort-queue-6] sorted 132782 enqueued variables after 68335 conflicts
c [score-dist-6] active 3186 (2%), one 0 (0%), zero 132782 (98%)
c [score-dist-6] max exp 510, different 224 (44%)
c [score-dist-6] median active exp 493, avg 447.6
c [simplification-6] removed 69 variables 0.1% (135968 remain 82%)
c [simplification-6] removed 3663 irredundant clauses 0.1% (6031048 remain 92%)
c [simplification-6] maximum reduction of 0% = max (0%, 0%)
c [simplification-6] full geometric conflict interval increment 30999
c [simplification-6] new conflict interval 61998
c [simplification-6] penalized conflict interval 61998 = 1 * 61998
c [simplification-6] hard conflict limit 161332 (soft 130333 + delta 30999)
c [simplification-6] new conflict limit 130333 (hard 161332)
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 -  142.6  135968  6031048     92082   30527   8050 32421   11    19  390  58%    769    5   11    8  125%
c -  160.8  135968  6031048    125723   32961   8067 32421   11    18  390  60%    871    2   10    9  111%
c 
c [simplification-7] limit 130333 conflicts (hard 161332) hit after 130333 conflicts
c [quatres-3] found 146360 quaternary clauses 30% in total
c [quatres-3-2] added 18 quaternary resolvents
c [ternres-3] limit 24124100 based on 6031025 irredundant clauses
c [ternres-3] 128962 schedulable variables 95%
c [ternres-3] 13 ternary resolvents (0 bin, 13 trn)
c [ternres-3] 125507 variables remain 92% (10461 retained 8%)
c [gauss-2] limit 3015512 based on 6031025 irredundant clauses
c [gauss-2] extracted 30 xors of average arity 3.0
c [gauss-2] connected 90 occurrences of 90 variables (average 1.0)
c [gauss-2] limit 3015512 based on 6031025 irredundant clauses
c [gauss-2] fully completed
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [basicprobe-3] limit 48248200 based on 6031025 irredundant clauses
c [basicprobe-3-0] 2508 sched 2%, 5 failed, 0 lifted, 24675 hbrs
c [decomp-16] removed 410 variables
c [basicprobe-3-1] 8488 probes remain 6% after last round
c [basicprobe-3-1] 5 units = 5 failed (100%) + 0 lifted (0%)
c [basicprobe-3-1] removed 410 variables, found 27546 hbrs
c [bate-1] eliminated 534 asymmetric tautologies during probing
c [transred-3] limit 6030087 based on 6030087 irredundant clauses
c [transred-3] removed 4896 transitive binary clauses
c [block-2] scheduling all variables this time
c [block-2] scheduled 135558 variables 100%
c [block-2] limit of 44629706 steps penalty 4 = 1 + 3
c [block-2] incomplete 11816 not tried 9%
c [block-2] transition to [ all 1 rem 1 ] state
c [block-2] eliminated 72 blocked clauses
c [block-2] 72 < 1/100 * 6029498 = 60294 considered unsuccessful
c [cce-2] limit of 22314853 steps penalty 4 = 1 + 3
c [cce-2-1] eliminated 1 clauses out of 1 (100%) of length 27
c [cce-2-1] eliminated 3 clauses out of 9 (33%) of length 26
c [cce-2-1] eliminated 2 clauses out of 193 (1%) of length 25
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] eliminated 6 large clauses in 22314965 steps
c [cce-2-1] allowing another 11157482 steps for small clauses
c [cce-2-1] scheduling 5509790 clauses = 320575 binary + 5189215 ternary
c [cce-2-1] tried to eliminate 149 small clauses 0%
c [cce-2-1] eliminated 1 binary clauses 0%
c [cce-2-1] eliminated 4 ternary clauses 0%
c [cce-2-1] eliminated 5 small clauses 0%
c [cce-2-1] eliminated 5 small clauses in 22314944 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 11 covered clauses in round 1
c [cce-2] eliminated 11 covered clauses in TOTAL during 1 rounds
c [cce-2] 11 < 1/100 * 6029426 = 60294 considered unsuccessful
c [elim-6] 67751 variables 50% will be scheduled this time
c [elim-6] scheduled 67751 variables 50%
c [elim-6] limit of 50000000 steps penalty 4 = 1 + 3
c [elim-6] rescheduling of touched variables disabled
c [elim-6] incomplete 64354 not tried 47% in round 1
c [elim-6] transition to [ all 0 rem 1 ] state
c [elim-6] eliminated 0 = 0% variables out of 67751 scheduled
c [bca-3] limit of 10000000 steps and 12063507 added (scaled 2)
c [bca-3] 267844 out of 271118 literals actually usable 99%
c [bca-3] added 33 blocked clauses in 727645 steps
c [sweep-3] limit 12058830 based on 6029415 irredundant clauses
c [sweep-3-1] 33701 pos 25.2% + 99997 neg 74.8% = 133698 sched 98.6% ret 1860
c [sweep-3-1] 12066973 steps 115 queries 29145.72 avg class size
c [sweep-3-1] 4461 decisions 103 SAT calls 228.84 avg env size
c [sweep-3-1] 132992 variables remain 98% (2566 retained 2%)
c [decomp-17] removed 64 variables
c [sweep-3-1] removed 64 vars (0 failed, 16 eqs, 11 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 64 vars in TOTAL (1 rounds, 114 queries)
c [phase-count-7] 4981750 negative 82.6% of 6029370 except 1047620 17.4%
c [phase-count-7] 5123285 positive 85.0% of 6029370 except 906085 15.0%
c [phase-7] phase bias: 1764 positive 70%, 755 negative 30%
c [sort-queue-7] sorted 131748 enqueued variables after 130333 conflicts
c [score-dist-7] active 3746 (3%), one 27 (0%), zero 131721 (97%)
c [score-dist-7] max exp 509, different 297 (58%)
c [score-dist-7] median active exp 469, avg 391.0
c [simplification-7] removed 474 variables 0.3% (135494 remain 82%)
c [simplification-7] removed 1678 irredundant clauses 0.0% (6029370 remain 92%)
c [simplification-7] maximum reduction of 0% = max (0%, 0%)
c [simplification-7] full geometric conflict interval increment 61998
c [simplification-7] new conflict interval 123996
c [simplification-7] penalized conflict interval 123996 = 1 * 123996
c [simplification-7] hard conflict limit 316327 (soft 254329 + delta 61998)
c [simplification-7] new conflict limit 254329 (hard 316327)
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  196.1  135493  6029370    152580   55564   8336 56847    7     9  393  79%    923   -6    5    9   53%
c -  200.1  135493  6029370    160875   32580   8338 56847   12    23  390  53%  -1199    7   11   10  108%
c -  218.4  135493  6029370    198708   36119   8344 56847    9    13  390  73%   -224   -3   12   10  126%
c -  238.3  135493  6029370    237496   39367   8377 56850   10    16  390  66%    333   -0   10   10   99%
c 
c [simplification-8] limit 254329 conflicts (hard 316327) hit after 263939 conflicts
c [quatres-4] found 146469 quaternary clauses 29% in total
c [quatres-4-2] added 21 single-self-subsuming ternary resolvents
c [quatres-4-2] added 24 quaternary resolvents
c [ternres-4] limit 24117388 based on 6029347 irredundant clauses
c [ternres-4] 125074 schedulable variables 92%
c [ternres-4] 19 ternary resolvents (0 bin, 19 trn)
c [ternres-4] 121635 variables remain 90% (13858 retained 10%)
c [decomp-18] removed 1 variables
c [simpleprobe-4] all 135493 free variables schedulable
c [simpleprobe-4] limit 25000000 penalty 3 = 0 + 3
c [decomp-19] removed 13 variables
c [simpleprobe-4] 112476 variables remain 83% (23004 retained 17%)
c [simpleprobe-4] removed 13 variables, found 1610 hbrs, 0 units
c [transred-4] limit 6029080 based on 6029080 irredundant clauses
c [transred-4] removed 4260 transitive binary clauses
c [bca-4] limit of 10000000 steps and 12061818 added (scaled 2)
c [bca-4] 267398 out of 270962 literals actually usable 99%
c [bca-4] added 30 blocked clauses in 749609 steps
c [sweep-4] limit 12057124 based on 6028562 irredundant clauses
c [sweep-4-1] 36346 pos 27.3% + 96584 neg 72.7% = 132930 sched 98.1% ret 2550
c [sweep-4-1] 12143731 steps 81 queries 31388.62 avg class size
c [sweep-4-1] 3017 decisions 66 SAT calls 266.35 avg env size
c [sweep-4-1] 132346 variables remain 98% (3134 retained 2%)
c [decomp-20] removed 20 variables
c [sweep-4-1] removed 20 vars (0 failed, 15 eqs, 14 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 20 vars in TOTAL (1 rounds, 80 queries)
c [phase-count-8] 4981338 negative 82.6% of 6028550 except 1047212 17.4%
c [phase-count-8] 5122532 positive 85.0% of 6028550 except 906018 15.0%
c [phase-8] phase bias: 283 positive 43%, 377 negative 57%
c [sort-queue-8] sorted 132536 enqueued variables after 263939 conflicts
c [score-dist-8] active 2924 (2%), one 1383 (1%), zero 131153 (97%)
c [score-dist-8] max exp 509, different 318 (62%)
c [score-dist-8] median active exp 499, avg 448.0
c [simplification-8] removed 33 variables 0.0% (135460 remain 82%)
c [simplification-8] removed 820 irredundant clauses 0.0% (6028550 remain 92%)
c [simplification-8] maximum reduction of 0% = max (0%, 0%)
c [simplification-8] full geometric conflict interval increment 123996
c [simplification-8] new conflict interval 247992
c [simplification-8] penalized conflict interval 247992 = 1 * 247992
c [simplification-8] hard conflict limit 635927 (soft 511931 + delta 123996)
c [simplification-8] new conflict limit 511931 (hard 635927)
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 -  273.3  135460  6028550    278020   42524   8411 56899   10    18  391  56%    652    3   11   10  110%
c -  290.1  135460  6028550    314963   44167   8416 56903   10    18  391  58%    812    1    8   10   81%
c -  309.8  135460  6028550    353479   46872   8423 56906   12    17  391  68%    906   -0   11   11  106%
c -  329.7  135460  6028550    392633   48658   8434 56908   11    16  391  71%    959   -2   12   11  106%
c -  349.9  135460  6028550    432635   51185   8440 56911   11    20  392  55%    989    3   11   11   93%
c -  370.1  135460  6028550    473481   53288   8453 56915    9    14  392  67%   1005   -3   10   11   88%
c -  391.6  135460  6028550    515643   56311   8457 56916   10    15  392  65%   1014   -2    9   11   88%
c 
c [simplification-9] limit 511931 conflicts (hard 635927) hit after 524301 conflicts
c [quatres-5] found 146789 quaternary clauses 29% in total
c [quatres-5-1] removed 1 duplicate quaternary clauses
c [quatres-5-2] added 9 single-self-subsuming ternary resolvents
c [quatres-5-2] added 17 quaternary resolvents
c [ternres-5] limit 25000000 with penalty 3 = 0 + 3
c [ternres-5] 121606 schedulable variables 90%
c [ternres-5] 14 ternary resolvents (0 bin, 14 trn)
c [ternres-5] 118121 variables remain 87% (17339 retained 13%)
c [decomp-21] removed 8 variables
c [treelook-4] limit 3231384 penalty 3 = 0 + 3 boost 1
c [treelook-4] scheduled 59475 literals 22%
c [treelook-4] scheduling used 3289669 steps
c [treelook-4] not fully scheduled
c [treelook-4] limit 3231384 penalty 3 = 0 + 3 boost 1
c [treelook-4] used 3251591 steps
c [treelook-4] 59395 literals remain 22%
c [treelook-4] 4840 variables remain to probed next time 4%
c [decomp-22] removed 4 variables
c [treelook-4] removed 4 variables, found 1292 hbrs
c [unhide-6] limit 376782 based on 6028518 irredundant clauses
c [unhide-6-6] 0 units, 0 failed, 23542 tauts, 0 hbrs, 7682 literals
c [transred-5] limit 6028151 based on 6028151 irredundant clauses
c [transred-5] removed 1274 transitive binary clauses
c [bca-5] limit of 10000000 steps and 12060175 added (scaled 2)
c [bca-5] 267255 out of 270898 literals actually usable 99%
c [bca-5] added 62 blocked clauses in 752070 steps
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 96941520 penalty 3 = 0 + 3
c [sweep-5-1] 38041 pos 28.7% + 94289 neg 71.3% = 132330 sched 97.7% ret 3118
c [sweep-5-1] 98478549 steps 900 queries 4834.46 avg class size
c [sweep-5-1] 32141 decisions 800 SAT calls 212.35 avg env size
c [sweep-5-1] 122252 variables remain 90% (13196 retained 10%)
c [decomp-23] removed 271 variables
c [sweep-5-1] removed 271 vars (0 failed, 118 eqs, 93 impls)
c [sweep-5] considered successful since not run to completion yet
c [sweep-5] removed 271 vars in TOTAL (1 rounds, 899 queries)
c [phase-count-9] 4980442 negative 82.6% of 6027555 except 1047113 17.4%
c [phase-count-9] 5121765 positive 85.0% of 6027555 except 905790 15.0%
c [phase-9] phase bias: 451 positive 34%, 871 negative 66%
c [sort-queue-9] sorted 129732 enqueued variables after 524301 conflicts
c [score-dist-9] active 5445 (4%), one 1621 (1%), zero 128111 (95%)
c [score-dist-9] max exp 509, different 286 (56%)
c [score-dist-9] median active exp 502, avg 476.6
c [simplification-9] removed 283 variables 0.2% (135177 remain 81%)
c [simplification-9] removed 995 irredundant clauses 0.0% (6027555 remain 92%)
c [simplification-9] maximum reduction of 0% = max (0%, 0%)
c [simplification-9] full geometric conflict interval increment 247992
c [simplification-9] new conflict interval 495984
c [simplification-9] penalized conflict interval 495984 = 1 * 495984
c [simplification-9] hard conflict limit 1268277 (soft 1020285 + delta 247992)
c [simplification-9] new conflict limit 1020285 (hard 1268277)
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 -  427.2  135177  6027555    555410   58459   8497 45658   10    18  392  58%   1019    0    9   11   87%
c -  448.9  135177  6027555    599061   61964   8505 45659   10    17  392  59%   1021   -1   10   10   94%
c -  472.8  135177  6027555    644043   64587   8530 45661   10    17  392  62%   1023    0   10   10   99%
c -  497.6  135177  6027555    689672   65805   8535 45661   12    18  392  70%   1023    2   12   11  108%
c -  519.0  135177  6027555    735625   69222   8538 45661   11    18  392  61%   1024    1   11   11  103%
c -  540.9  135177  6027555    782458   73096   8554 45662   11    16  393  68%   1024   -0   12   10  119%
c i  555.7  135176  6027555    810520   95787   8637 45676    8    11  397  79%   1024   -4    7   10   70%
c -  570.9  135087  6027555    835720   78530   8648 45677    9    12  393  78%  -6086   -2    8   10   82%
c i  576.6  135086  6027555    846848   87529   8693 45687    8    11  397  77%  -4975   -3    7   10   68%
c i  586.9  135016  6027555    864957  101913   8743 45704    8    10  399  80%  -3964   -3    6    9   64%
c i  591.6  134906  6027555    873341  108484   8771 45711    9    11  399  79%  -3618   -2    7    9   73%
c i  591.8  134827  6027555    873626  108638   8784 45715    9    11  399  79%  -3630   -2    7    9   70%
c i  591.9  134734  6027555    873693  108677   8787 45717    9    11  399  79%  -3632   -2    6    9   67%
c i  592.0  134606  6027555    873832  108755   8797 45722    8    11  399  79%  -3634   -2    5    9   58%
c i  592.0  134576  6027555    873835  108755   8796 45723    8    11  399  79%  -3634   -2    5    9   58%
c i  592.0  134021  6027555    873836  108754   8796 45723    8    11  399  79%  -3634   -2    5    9   58%
c i  592.0  133541  6027555    873855  108760   8802 45726    8    11  399  79%  -3635   -2    5    9   55%
c 0  592.0  133353  6027555    873855  108760   8802 45726    8    11  399  79%  -3635   -2    5    9   55%
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 UNSATISFIABLE
c
c bate: 534 basic ate = 194 trn 36% + 340 lrg 64% in 1 updates
c bcas: 5 count, 8480 added (19464 skipped), 3684640 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, 9010 removed, 39396497 resolutions, 110366897 steps
c blkd: 2241 blocking literals 1%, 0 pure
c bump: 873659 bumped seen, 47385486 lits 54.2 on average
c card: 3 count, 0 units, 0 am1, 10931279 steps
c card: 0 rescheduled, 0 eliminated, 0 resolved, 7268 subsumed
c card: 3483 at-most-one constraints found, average size 3.10
c card: 3483 at-most-one constraints used 100%, average size 3.10
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, 46 eliminated, 46 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: 27755083 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 42 gcs, 0 rescored clauses, 3403 rescored vars
c dcps: 23 decompositions, 7408 equivalent 4%
c deco: 0 decision-only clauses 0%, 0% reduction
c decs: 1448438 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 6 elims, 21805 eliminated 13%, 7110 pure 33%
c elms: 6 rounds, 1.0 rounds/bve
c elms: 11901 small 55%, 2794 large 13%
c elms: 12470 tried small, 11901 succeeded 95%, 569 failed 5%
c elms: 7265 subsumed, 6096 strengthened, 0 blocked
c elms: 7363295 copies, 7471762 resolutions, 138557 ipos
c elms: 26712902 subchks, 2148624 strchks
c gaus: 2 extractions, 62 extracted, 2.8 size, 3 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 12080194 steps, 6040097 extr 50%, 239 elim 0%
c glue: 10.5 orig avg, 10.5 real avg, 2.7 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 121488 = 4739 simple 4% + 116254 trn 96% + 495 lrg 0%, 1783 sub 1%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 873659 clauses, 19.5 length
c lrnd: 17014735 lits = 24877900 orig - 7863165 removed 32%
c lrnd: 353414 uips 40%, 462221 flips 53%
c mins: 864859 mins 99%, 92 bin 0%, 8708 size 1%
c mins: 18759309 poisoned searches, 1583768 hits, 8% hit rate
c mins: 41123632 used twice searches, 4713452 hits, 11% hit rate
c move: moved 13785, 370 bin 3%, 13415 trn 97%
c otfs: 1192 driving 39%, 1872 restarting 61%
c otfs: str 3064, 3004 red 98%, 60 irr 2%
c otfs: str 3064, 0 bin 0%, 14 trn 0%, 3050 lrg 100%
c otfs: sub 82, 82 red 100%, 0 irr 0%
c otfs: sub 82, 0 bin 0%, 3 trn 4%, 79 lrg 96%
c phas: 9 computed, 176212 set, 81136 pos (46%), 95076 neg (54%)
c prbs: 3 basic, 25949 probed, 104 failed, 0 lifted
c prbs: 4 simple, 253302 probed, 0 failed, 94 eqs
c prbs: 4 treelook, 254 probed, 3 failed, 0 lifted
c prom: 125988 locked 18% out of 695228 tried
c prps: 630923182 props, 432 props/dec
c prps: 99% srch, 1% simp, 0% lkhd
c quat: 5 count, 379 quat, 168 self1, 0 self2, 79 dup
c queu: 9 sorted, 1448438 next (119895 steps 0.08)
c queu: 59342735 enq (69283913 steps 1.17), 47385486 deq 80%
c redc: 6270 clauses 3%, 182654 tried 21%, 1 sat 0%
c redc: 6795 lits 0%, 1993663 tried 8%, 1 sat 0%
c redc: 108 times jump level reduced, 1.8 levels on average
c reds: 20 count, 43692.8 conflicts per reduce
c reds: 0 memlim 0%, 20 arith 100%
c reds: 595041 collected 90%, 63658 retired 10%
c rmbd: 4487 removed, 2644 red 59%
c rsts: 13602 restarts 100%, 0 skipped 0%
c rsts: 0 saturating 0%, 0 reuse 0%
c rsts: 0 kept 0.0% average 0.0%
c scnc: 0 count, 1.000 min (0/1000), 1.000 max (0/1000)
c simp: 9 count, 9 confs 100%, 0 vars 0%
c simp: 0 its 0%, 0 bin 0%, 0 trns 0%
c subl: 873659 count (364225 tried 0.4), 104410 sub out of 872703 (12.0%)
c swps: 5 count, 5 rounds, 1316 queries (263.2/round)
c swps: 1174 sat calls, 54 unsat (0.8% success rate)
c swps: 47707 decisions 40.6, 996 conflicts 0.8
c swps; 12070.6 avg class size, 216.4 avg environment size
c swps: 0 failed, 132 impls, 172 equivs
c swp0: 436 type 0 queries, 75 unsat (17.2%), 432 sat (99.1%)
c swp1: 880 type 1 queries, 574 unsat (65.2%), 712 sat (80.9%)
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: 4651175 calls to obtain time
c tops: 4509 fixed 3%, 11 its, 79441.36 confs/it
c trds: 5 transitive reductions, 13723 removed, 0 failed
c trds: 294487 nodes, 377564 edges, 30166514 steps
c trim: 649432 words, 2.5 MB
c trnr: 5 count, 0 bin, 91 trn, 121569235 steps
c unhd: 6 count, 6 rounds, 56489960 steps
c unhd: 4018 non-trivial sccs of average size 2.5
c unhd: 3 units, 3 bin, 0 trn, 0 lrg
c unhd: 123 failed, 105 stamp, 0 lits, 0 bin, 0 trn, 0 lrg
c unhd: 159767 tauts, 1881 bin 1%, 10187 trn 6%, 1009 lrg 1%
c unhd: 159767 tauts, 146690 stamp 92%, 57766 red 36%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 28896 str, 3 bin 0%, 581 trn 2%, 28312 lrg 98%, 27463 red 95%
c vars: 133353 remaining 80% and 33722 removed 20% out of 167075
c vars: 4509 fixed 3%, 21805 eliminated 13%, 7408 equivalent 4%
c vsts: 42597713669 visits, 99% srch, 1% simp, 0% lkhd
c vsts: 67.6 search visits per propagation, 48448.5 per conflict
c wchs: 2399528820 pushed, 53641774 enlarged, 74 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all         873082        595041         63658      16502641       5591531        243984
c 
c  0 0         56787   7      4150   1         0   0  10014536  61   2981635  53    124284  51     2.1
c  1 5         58220   7     26656   4     14092  22   2376735  14<   753047  13<    31951  13<    0.6
c  2 6        238955  27    161796  27     30497  48<  2847877  17   1102325  20     49442  20     1.8
c  3 9        310230  36<   234293  39<    13569  21    909142   6    514532   9     23312  10     1.7
c  4 14       169824  19    134758  23      4522   7    289056   2    195715   4     11748   5     1.5
c  5 21        37653   4     32149   5       942   1     62716   0     42610   1      3129   1     0.7
c  6 30         1408   0      1236   0        35   0      2572   0      1662   0       118   0     0.1
c  7 41            5   0         3   0         1   0         7   0         5   0         0   0     0.0
c 
c avg                  2.7           3.0           2.2           0.7           1.0           1.1
c std                  1.2           1.0           0.9           1.1           1.2           1.3
c 
c   29.702   5% probe
c   18.291   3% elim
c   15.806   3% sweep
c   12.164   2% unhide
c   11.054   2% rescore
c    8.405   1% transred
c    6.378   1% bca
c    5.784   1% block
c    3.432   1% cce
c    2.688   0% bump
c 
c    6.931 < 1% rest (below)
c 
c    2.469   0% quatres
c    2.213   0% gauss
c    1.176   0% ternres
c    0.863   0% decide
c    0.210   0% card
c    0.000   0% locs
c    0.000   0% queuesort
c ==================================
c   12.455   2% preprocessing     9%
c  127.342  22% inprocessing     91%
c ==================================
c  139.797  24% simplifying
c  452.167  76% search
c ==================================
c  591.968 100% all
c 
c        873855 conflicts,        1476.2 confs/sec
c           565 ternaries,        1546.6 confs/ternary
c           131 binaries,         6670.6 confs/binary
c            11 iterations,      79441.4 confs/iteration
c 
c            20 reductions,          0.0 redus/sec,  43692.8 confs/reduction
c         13602 restarts,           23.0 rests/sec,     64.2 confs/restart
c       1448438 decisions,        2446.8 decis/sec,      1.7 decis/conflict
c     630923182 propagations,  1065806.4 props/sec,    435.6 props/decision
c 
c 592.0 seconds, 623.5 MB
c launch: done
