c launch: /data/cnf/sc2014/app/8pipe_k.cnf.bz2
c host: atom14
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/8pipe_k.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/8pipe_k.cnf.bz2
c no embedded options
c found 'p cnf 35065 1332773' header
c read 35065 variables, 1332773 clauses, 3936683 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=3
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 35064 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] SUM (--score=3)
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   35064  1332772         0       0      0     0    0     0   41   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 6 at-most-one constraints of average size 3.2
c [card-1] no at-most-two constraint found
c [card-1] using previous limit 2000000 for elimination
c [card-1] 6 out of 6 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 10 variables
c [simpleprobe-1] all 35055 free variables schedulable
c [simpleprobe-1] boosting simple probing limit by 10
c [simpleprobe-1] limit 20000000 penalty 0 = 0 + 0
c [simpleprobe-1] 17648 variables remain 50% (17407 retained 50%)
c [simpleprobe-1] removed 0 variables, found 33586 hbrs, 0 units
c [unhide-1] limit 83276 based on 1332429 irredundant clauses
c [unhide-1-1] 0 units, 0 failed, 0 tauts, 0 hbrs, 0 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 35055 variables 100%
c [elim-1] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-1] rescheduling of touched variables disabled
c [elim-1] incomplete 23138 not tried 66% in round 1
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 4032 = 12% variables out of 35055 scheduled
c [elim-1] considered successful since not run to completion yet
c [phase-count-1] 1323956 negative 100.0% of 1324582 except 626 0.0%
c [phase-count-1] 154804 positive 11.7% of 1324582 except 1169778 88.3%
c [phase-count-1] less non-negative clauses 626 than limit 132400 (10.0%)
c [phase-count-1] non-pos/non-neg = 1169778/626 = 1868.65 >= 2.00 = 200/100
c [lucky-phase-1] forcing lucky phase -1
c [phase-1] phase bias: 0 positive 0%, 31023 negative 100%
c [sort-queue-1] sorted 31023 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 31023 (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 4032 variables 11.5% (31023 remain 88%)
c [simplification-1] removed 8190 irredundant clauses 0.6% (1324582 remain 99%)
c [simplification-1] maximum reduction of 12% = max (12%, 1%)
c [simplification-1] large reduction 12% >= 5% limit
c [simplification-1] next conflict interval 1000 = 2000/2
c [simplification-1] penalized conflict interval 1000 = 1 * 1000
c [simplification-1] hard conflict limit 11000 (soft 1000 + delta 10000)
c [simplification-1] new conflict limit 1000 (hard 11000)
c 
c [simplification-2] limit 1000 conflicts (hard 11000) hit after 1001 conflicts
c [treelook-1] limit 331145 based on 1324582 irredundant clauses
c [treelook-1] scheduled 27831 literals 45%
c [treelook-1] scheduling used 331356 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 331145 based on 1324582 irredundant clauses
c [treelook-1] used 488212 steps
c [treelook-1] 27827 literals remain 45%
c [treelook-1] 26834 variables remain to probed next time 86%
c [treelook-1] removed 0 variables, found 1 hbrs
c [basicprobe-1] limit 10596656 based on 1324582 irredundant clauses
c [basicprobe-1-0] 28408 probes remain 92% after last round
c [basicprobe-1-0] 125 units = 125 failed (100%) + 0 lifted (0%)
c [basicprobe-1-0] removed 187 variables, found 242 hbrs
c [elim-2] 22977 variables 75% will be scheduled this time
c [elim-2] scheduled 22977 variables 75%
c [elim-2] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-2] rescheduling of touched variables disabled
c [elim-2] incomplete 16947 not tried 55% in round 1
c [elim-2] transition to [ all 0 rem 1 ] state
c [elim-2] eliminated 73 = 0% variables out of 22977 scheduled
c [elim-2] considered successful since not run to completion yet
c [sort-queue-2] sorted 27851 enqueued variables after 1001 conflicts
c [score-dist-2] active 2912 (9%), one 0 (0%), zero 27851 (91%)
c [score-dist-2] max exp 520, different 18 (3%)
c [score-dist-2] median active exp 512, avg 512.1
c [simplification-2] removed 260 variables 0.8% (30763 remain 88%)
c [simplification-2] removed 13175 irredundant clauses 1.0% (1311407 remain 98%)
c [simplification-2] maximum reduction of 1% = max (1%, 1%)
c [simplification-2] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-2] new conflict interval 10000
c [simplification-2] penalized conflict interval 10000 = 1 * 10000
c [simplification-2] hard conflict limit 21001 (soft 11001 + delta 10000)
c [simplification-2] new conflict limit 11001 (hard 21001)
c 
c [simplification-3] limit 11001 conflicts (hard 21001) hit after 11001 conflicts
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 2 at-most-one constraints of average size 3.0
c [card-2] no at-most-two constraint found
c [card-2] using previous limit 1000000 for elimination
c [card-2] 2 out of 2 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [simpleprobe-2] 16967 schedulable variables 55%
c [simpleprobe-2] limit 2622814 based on 1311407 irredundant clauses
c [simpleprobe-2] 16929 variables remain 55% (13834 retained 45%)
c [unhide-2] limit 81962 based on 1311407 irredundant clauses
c [unhide-2-2] 0 units, 1 failed, 284 tauts, 0 hbrs, 21214 literals
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 30762 variables 100%
c [elim-3] limit of 24888439 steps penalty 0 = 0 + 0
c [elim-3] rescheduling of touched variables disabled
c [elim-3] incomplete 18857 not tried 61% in round 1
c [elim-3] transition to [ all 1 rem 1 ] state
c [elim-3] eliminated 293 = 1% variables out of 30762 scheduled
c [elim-3] considered successful since not run to completion yet
c [sort-queue-3] sorted 19607 enqueued variables after 11001 conflicts
c [score-dist-3] active 10862 (36%), one 0 (0%), zero 19607 (64%)
c [score-dist-3] max exp 527, different 25 (5%)
c [score-dist-3] median active exp 518, avg 518.3
c [simplification-3] removed 294 variables 1.0% (30469 remain 87%)
c [simplification-3] removed 3236 irredundant clauses 0.2% (1308171 remain 98%)
c [simplification-3] maximum reduction of 1% = max (1%, 0%)
c [simplification-3] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-3] new conflict interval 20000
c [simplification-3] penalized conflict interval 20000 = 1 * 20000
c [simplification-3] hard conflict limit 41001 (soft 31001 + delta 10000)
c [simplification-3] new conflict limit 31001 (hard 41001)
c 
c [simplification-4] limit 31001 conflicts (hard 41001) hit after 31001 conflicts
c [unhide-3] limit 155859 with penalty 2 = 0 + 2
c [unhide-3-3] 0 units, 0 failed, 607 tauts, 0 hbrs, 16838 literals
c [elim-4] 16936 variables 56% will be scheduled this time
c [elim-4] scheduled 16936 variables 56%
c [elim-4] boosting limit by 20
c [elim-4] limit of 1246872240 steps penalty 0 = 0 + 0
c [elim-4] rescheduling of touched variables disabled
c [elim-4-1] eliminated 288 variables 1% in round 1 in 248792611 steps
c [elim-4-1] backward subsumption/strengthening limit 248792600
c [elim-4-1-1] backward checking 13536 touched variables 44%
c [elim-4-1-1] incomplete backward checking 13512 remain 100%
c [elim-4-1] subsumed 0 and strengthened 225 clauses in 248795297 steps
c [elim-4-1] rescheduled 1326 variables 4% by backward subsumption
c [elim-4-2] no variable eliminated in round 2 in 6197070 steps
c [elim-4] fully completed in 2 rounds
c [elim-4] transition to [ all 0 rem 0 ] state
c [elim-4] eliminated 288 = 2% variables out of 16936 scheduled
c [elim-4] 288 < 1/100 * 16936 = 169 considered unsuccessful
c [sort-queue-4] sorted 16813 enqueued variables after 31001 conflicts
c [score-dist-4] active 13368 (44%), one 0 (0%), zero 16813 (56%)
c [score-dist-4] max exp 530, different 28 (5%)
c [score-dist-4] median active exp 522, avg 521.0
c [simplification-4] removed 288 variables 0.9% (30181 remain 86%)
c [simplification-4] removed 9303 irredundant clauses 0.7% (1298868 remain 97%)
c [simplification-4] maximum reduction of 1% = max (1%, 1%)
c [simplification-4] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-4] new conflict interval 30000
c [simplification-4] penalized conflict interval 30000 = 1 * 30000
c [simplification-4] hard conflict limit 76001 (soft 61001 + delta 15000)
c [simplification-4] new conflict limit 61001 (hard 76001)
c 
c [simplification-5] limit 61001 conflicts (hard 76001) hit after 61002 conflicts
c [quatres-1] found 5510 quaternary clauses 9% in total
c [quatres-1-2] added 9 single-self-subsuming ternary resolvents
c [quatres-1-2] added 222 quaternary resolvents
c [ternres-1] boosting ternary resolution limit by 5
c [ternres-1] limit 26638675 with penalty 0 = 0 + 0
c [ternres-1] all 30181 free variables schedulable
c [ternres-1] 5533 ternary resolvents (1 bin, 5532 trn)
c [ternres-1] fully completed ternary resolution
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 0 xors of average arity 0.0
c [gauss-1] exported 0 unary, 0 binary and 0 ternary equations
c [treelook-2] limit 324717 based on 1298868 irredundant clauses
c [treelook-2] scheduled 26878 literals 45%
c [treelook-2] scheduling used 325400 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 324717 based on 1298868 irredundant clauses
c [treelook-2] used 2012038 steps
c [treelook-2] 26871 literals remain 45%
c [treelook-2] 25113 variables remain to probed next time 83%
c [treelook-2] removed 0 variables, found 51 hbrs
c [transred-1] limit 2000000 with penalty 0 = 0 + 0
c [transred-1] removed 0 transitive binary clauses
c [block-1] scheduling all variables this time
c [block-1] scheduled 30181 variables 100%
c [block-1] boosting limit by 10
c [block-1] limit of 532773510 steps penalty 0 = 0 + 0
c [block-1] fully completed
c [block-1] transition to [ all 0 rem 0 ] state
c [block-1] eliminated 62383 blocked clauses
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 2 clauses out of 6 (33%) of length 178
c [cce-1-1] eliminated 2 clauses out of 2 (100%) of length 177
c [cce-1-1] eliminated 3 clauses out of 5 (60%) of length 176
c [cce-1-1] eliminated 3 clauses out of 3 (100%) of length 175
c [cce-1-1] eliminated 4 clauses out of 6 (67%) of length 174
c [cce-1-1] eliminated 6 clauses out of 6 (100%) of length 173
c [cce-1-1] eliminated 8 clauses out of 10 (80%) of length 172
c [cce-1-1] eliminated 4 clauses out of 4 (100%) of length 171
c [cce-1-1] eliminated 6 clauses out of 8 (75%) of length 170
c [cce-1-1] eliminated 3 clauses out of 3 (100%) of length 169
c [cce-1-1] eliminated 5 clauses out of 7 (71%) of length 168
c [cce-1-1] eliminated 2 clauses out of 2 (100%) of length 167
c [cce-1-1] eliminated 1 clauses out of 3 (33%) of length 166
c [cce-1-1] eliminated 1 clauses out of 1 (100%) of length 165
c [cce-1-1] eliminated 2 clauses out of 2 (100%) of length 163
c [cce-1-1] eliminated 2 clauses out of 4 (50%) of length 162
c [cce-1-1] eliminated 4 clauses out of 4 (100%) of length 161
c [cce-1-1] eliminated 2 clauses out of 4 (50%) of length 160
c [cce-1-1] eliminated 5 clauses out of 5 (100%) of length 159
c [cce-1-1] eliminated 5 clauses out of 7 (71%) of length 158
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 70 large clauses in 30004485 steps
c [cce-1-1] allowing another 15002242 steps for small clauses
c [cce-1-1] scheduling 1173238 clauses = 1171348 binary + 1890 ternary
c [cce-1-1] tried to eliminate 287 small clauses 0%
c [cce-1-1] eliminated 45 binary clauses 0%
c [cce-1-1] eliminated 45 small clauses 0%
c [cce-1-1] eliminated 45 small clauses in 30000002 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 115 covered clauses in round 1
c [cce-1] eliminated 115 covered clauses in TOTAL during 1 rounds
c [cce-1] 115 < 1/100 * 1236485 = 12364 considered unsuccessful
c [bca-1] limit of 10000000 steps and 2473240 added (scaled 2)
c [bca-1] 51925 out of 59624 literals actually usable 87%
c [bca-1] added 9021 blocked clauses in 218614 steps
c [sweep-1] limit 2472740 based on 1236370 irredundant clauses
c [sweep-1-1] 669 pos 2.2% + 29142 neg 97.8% = 29811 sched 100.0% ret 0
c [sweep-1-1] 2512814 steps 67 queries 1935.37 avg class size
c [sweep-1-1] 2078 decisions 63 SAT calls 247.57 avg env size
c [sweep-1-1] 24005 variables remain 81% (5806 retained 19%)
c [decomp-10] removed 4 variables
c [sweep-1-1] removed 4 vars (0 failed, 4 eqs, 17 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 4 vars in TOTAL (1 rounds, 66 queries)
c [sort-queue-5] sorted 16358 enqueued variables after 61002 conflicts
c [score-dist-5] active 13449 (45%), one 0 (0%), zero 16358 (55%)
c [score-dist-5] max exp 532, different 30 (6%)
c [score-dist-5] median active exp 522, avg 522.0
c [simplification-5] removed 374 variables 1.2% (29807 remain 85%)
c [simplification-5] removed 62498 irredundant clauses 4.8% (1236370 remain 93%)
c [simplification-5] maximum reduction of 5% = max (1%, 5%)
c [simplification-5] large reduction 5% >= 5% limit
c [simplification-5] next conflict interval 2000 = 2000/1
c [simplification-5] penalized conflict interval 2000 = 1 * 2000
c [simplification-5] hard conflict limit 73002 (soft 63002 + delta 10000)
c [simplification-5] new conflict limit 63002 (hard 73002)
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 -   52.8   29807  1236370     61565   24589   6451 85423   86    88   57  98%    617   29   86   53  161%
c 
c [simplification-6] limit 63002 conflicts (hard 73002) hit after 63002 conflicts
c [quatres-2] found 5439 quaternary clauses 9% in total
c [quatres-2-2] added 3 single-self-subsuming ternary resolvents
c [quatres-2-2] added 158 quaternary resolvents
c [ternres-2] limit 5493044 with penalty 0 = 0 + 0
c [ternres-2] all 29807 free variables schedulable
c [ternres-2] 2 ternary resolvents (0 bin, 2 trn)
c [ternres-2] 8044 variables remain 27% (21763 retained 73%)
c [card-3] limit 686630 penalty 2 = 2 + 0
c [card-3] found 2 at-most-one constraints of average size 3.0
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 686630 for elimination
c [card-3] 2 out of 2 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [basicprobe-2] limit 27465221 penalty 0 = 0 + 0
c [basicprobe-2-0] 24791 probes remain 85% after last round
c [basicprobe-2-0] 321 units = 321 failed (100%) + 0 lifted (0%)
c [basicprobe-2-0] removed 545 variables, found 432 hbrs
c [bate-1] eliminated 77 asymmetric tautologies during probing
c [unhide-4] limit 137326 with penalty 3 = 1 + 2
c [unhide-4-4] 0 units, 0 failed, 1000 tauts, 0 hbrs, 36739 literals
c [block-2] scheduling all variables this time
c [block-2] scheduled 29262 variables 100%
c [block-2] limit of 54930442 steps penalty 0 = 0 + 0
c [block-2] fully completed
c [block-2] transition to [ all 0 rem 0 ] state
c [block-2] eliminated 106501 blocked clauses
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 27044 variables 100%
c [elim-5] limit of 54930442 steps penalty 1 = 1 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5] incomplete 8152 not tried 30% in round 1
c [elim-5] transition to [ all 1 rem 1 ] state
c [elim-5] eliminated 1282 = 5% variables out of 27044 scheduled
c [bca-2] limit of 10000000 steps and 2188282 added (scaled 2)
c [bca-2] 45529 out of 51526 literals actually usable 88%
c [bca-2] added 3477 blocked clauses in 178074 steps
c [sweep-2] limit 2183272 based on 1091636 irredundant clauses
c [sweep-2-1] 605 pos 2.9% + 20495 neg 97.1% = 21100 sched 81.9% ret 4662
c [sweep-2-1] 2207714 steps 71 queries 1136.75 avg class size
c [sweep-2-1] 1588 decisions 66 SAT calls 263.12 avg env size
c [sweep-2-1] 18056 variables remain 70% (7706 retained 30%)
c [decomp-12] removed 7 variables
c [sweep-2-1] removed 7 vars (0 failed, 7 eqs, 14 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 7 vars in TOTAL (1 rounds, 70 queries)
c [sort-queue-6] sorted 12864 enqueued variables after 63002 conflicts
c [score-dist-6] active 12891 (50%), one 0 (0%), zero 12864 (50%)
c [score-dist-6] max exp 532, different 30 (6%)
c [score-dist-6] median active exp 522, avg 522.0
c [simplification-6] removed 4052 variables 13.6% (25755 remain 73%)
c [simplification-6] removed 144734 irredundant clauses 11.7% (1091636 remain 82%)
c [simplification-6] maximum reduction of 14% = max (14%, 12%)
c [simplification-6] large reduction 14% >= 5% limit
c [simplification-6] next conflict interval 2000 = 2000/1
c [simplification-6] penalized conflict interval 2000 = 1 * 2000
c [simplification-6] hard conflict limit 75002 (soft 65002 + delta 10000)
c [simplification-6] new conflict limit 65002 (hard 75002)
c 
c [simplification-7] limit 65002 conflicts (hard 75002) hit after 65003 conflicts
c [quatres-3] found 5169 quaternary clauses 10% in total
c [quatres-3-2] added 159 single-self-subsuming ternary resolvents
c [quatres-3-2] added 133 quaternary resolvents
c [ternres-3] limit 5610200 with penalty 0 = 0 + 0
c [ternres-3] 6945 schedulable variables 27%
c [ternres-3] 11 ternary resolvents (0 bin, 11 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-2] limit 1091636 based on 1091636 irredundant clauses
c [transred-2] removed 9 transitive binary clauses
c [block-3] scheduling all variables this time
c [block-3] scheduled 25755 variables 100%
c [block-3] limit of 56102005 steps penalty 0 = 0 + 0
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 6365 blocked clauses
c [block-3] 6365 < 1/100 * 1091633 = 10916 considered unsuccessful
c [cce-2] limit of 15000000 steps penalty 1 = 1 + 0
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] allowing another 7501064 steps for small clauses
c [cce-2-1] scheduling 1026274 clauses = 1024152 binary + 2122 ternary
c [cce-2-1] tried to eliminate 140 small clauses 0%
c [cce-2-1] eliminated 6 binary clauses 0%
c [cce-2-1] eliminated 6 small clauses 0%
c [cce-2-1] eliminated 6 small clauses in 15000049 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 6 covered clauses in round 1
c [cce-2] eliminated 6 covered clauses in TOTAL during 1 rounds
c [cce-2] 6 < 1/100 * 1085268 = 10852 considered unsuccessful
c [elim-6] 8140 variables 32% will be scheduled this time
c [elim-6] scheduled 8140 variables 32%
c [elim-6] limit of 112204010 steps penalty 0 = 0 + 0
c [elim-6] rescheduling of touched variables disabled
c [elim-6] incomplete 848 not tried 3% in round 1
c [elim-6] transition to [ all 0 rem 1 ] state
c [elim-6] eliminated 45 = 1% variables out of 8140 scheduled
c [elim-6] 45 < 1/100 * 8140 = 81 considered unsuccessful
c [bca-3] limit of 10000000 steps and 2175093 added (scaled 2)
c [bca-3] 45263 out of 51408 literals actually usable 88%
c [bca-3] added 105 blocked clauses in 177707 steps
c [sweep-3] limit 2168344 based on 1084172 irredundant clauses
c [sweep-3-1] 769 pos 4.3% + 17244 neg 95.7% = 18013 sched 70.1% ret 7690
c [sweep-3-1] 2208235 steps 79 queries 958.16 avg class size
c [sweep-3-1] 1977 decisions 70 SAT calls 137.03 avg env size
c [sweep-3-1] 15653 variables remain 61% (10050 retained 39%)
c [decomp-14] removed 7 variables
c [sweep-3-1] removed 7 vars (0 failed, 8 eqs, 22 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 7 vars in TOTAL (1 rounds, 78 queries)
c [sort-queue-7] sorted 12803 enqueued variables after 65003 conflicts
c [score-dist-7] active 12893 (50%), one 0 (0%), zero 12803 (50%)
c [score-dist-7] max exp 532, different 30 (6%)
c [score-dist-7] median active exp 522, avg 522.0
c [simplification-7] removed 59 variables 0.2% (25696 remain 73%)
c [simplification-7] removed 7464 irredundant clauses 0.7% (1084172 remain 81%)
c [simplification-7] maximum reduction of 1% = max (0%, 1%)
c [simplification-7] geometric conflict interval increment 15000 = 30000 / 2
c [simplification-7] new conflict interval 45000
c [simplification-7] penalized conflict interval 45000 = 1 * 45000
c [simplification-7] hard conflict limit 132503 (soft 110003 + delta 22500)
c [simplification-7] new conflict limit 110003 (hard 132503)
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 -   74.8   25696  1084172     93578   25904   5348 36323   86    88   53  98%    775   18   86   65  132%
c 
c [simplification-8] limit 110003 conflicts (hard 132503) hit after 110003 conflicts
c [quatres-4] found 5429 quaternary clauses 10% in total
c [quatres-4-2] added 116 quaternary resolvents
c [ternres-4] limit 8825860 with penalty 0 = 0 + 0
c [ternres-4] all 25696 free variables schedulable
c [ternres-4] 106 ternary resolvents (0 bin, 106 trn)
c [ternres-4] fully completed ternary resolution
c [transred-3] limit 2000000 with penalty 0 = 0 + 0
c [transred-3] removed 1 transitive binary clauses
c [bca-4] limit of 10000000 steps and 2175145 added (scaled 2)
c [bca-4] 45412 out of 51394 literals actually usable 88%
c [bca-4] added 65 blocked clauses in 192662 steps
c [sweep-4] limit 2647758 penalty 0 = 0 + 0
c [sweep-4-1] 756 pos 4.8% + 14893 neg 95.2% = 15649 sched 60.9% ret 10047
c [sweep-4-1] 2691112 steps 69 queries 782.93 avg class size
c [sweep-4-1] 1755 decisions 60 SAT calls 130.52 avg env size
c [sweep-4-1] 14609 variables remain 57% (11087 retained 43%)
c [decomp-16] removed 13 variables
c [sweep-4-1] removed 13 vars (0 failed, 13 eqs, 28 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 13 vars in TOTAL (1 rounds, 68 queries)
c [sort-queue-8] sorted 12793 enqueued variables after 110003 conflicts
c [score-dist-8] active 12890 (50%), one 0 (0%), zero 12793 (50%)
c [score-dist-8] max exp 534, different 32 (6%)
c [score-dist-8] median active exp 523, avg 522.4
c [simplification-8] removed 13 variables 0.1% (25683 remain 73%)
c [simplification-8] removed 0 irredundant clauses 0.0% (1084172 remain 81%)
c [simplification-8] maximum reduction of 0% = max (0%, 0%)
c [simplification-8] full geometric conflict interval increment 45000
c [simplification-8] new conflict interval 90000
c [simplification-8] penalized conflict interval 90000 = 1 * 90000
c [simplification-8] hard conflict limit 245003 (soft 200003 + delta 45000)
c [simplification-8] new conflict limit 200003 (hard 245003)
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 -   81.0   25683  1084172    123164   26606   5381 36516   82    84   53  98%    865    8   81   72  113%
c -   85.9   25683  1084172    153644   25496   5381 36519   81    85   53  96%    924    6   83   75  110%
c -   91.4   25683  1084172    186535   25915   5381 36519   80    82   53  98%    964    1   78   77  100%
c 
c [simplification-9] limit 200003 conflicts (hard 245003) hit after 200004 conflicts
c [quatres-5] found 5547 quaternary clauses 10% in total
c [quatres-5-2] added 120 quaternary resolvents
c [ternres-5] limit 15081475 with penalty 0 = 0 + 0
c [ternres-5] all 25683 free variables schedulable
c [ternres-5] 1 ternary resolvents (0 bin, 1 trn)
c [ternres-5] fully completed ternary resolution
c [simpleprobe-3] 13774 schedulable variables 54%
c [simpleprobe-3] limit 15081475 penalty 2 = 2 + 0
c [simpleprobe-3] 13159 variables remain 51% (12524 retained 49%)
c [simpleprobe-3] removed 0 variables, found 129 hbrs, 0 units
c [unhide-5] limit 188518 with penalty 4 = 2 + 2
c [unhide-5-5] 0 units, 0 failed, 6392 tauts, 0 hbrs, 69804 literals
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 2 transitive binary clauses
c [block-4] scheduling all variables this time
c [block-4] scheduled 25683 variables 100%
c [block-4] limit of 75407375 steps penalty 1 = 1 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 51 blocked clauses
c [block-4] 51 < 1/100 * 1076482 = 10764 considered unsuccessful
c [elim-7] scheduling all variables this time
c [elim-7] scheduled 25683 variables 100%
c [elim-7] limit of 150814750 steps penalty 1 = 1 + 0
c [elim-7] rescheduling of touched variables disabled
c [elim-7-1] eliminated 14 variables 0% in round 1 in 146105458 steps
c [elim-7-1] backward subsumption/strengthening limit 4709292
c [elim-7-1-1] backward checking 1429 touched variables 6%
c [elim-7-1-1] incomplete backward checking 1445 remain 101%
c [elim-7-1] subsumed 0 and strengthened 30 clauses in 4709557 steps
c [elim-7] incomplete 32 not tried 0% in round 1
c [elim-7] transition to [ all 1 rem 1 ] state
c [elim-7] eliminated 14 = 0% variables out of 25683 scheduled
c [elim-7] 14 < 1/100 * 25683 = 256 considered unsuccessful
c [bca-5] limit of 10000000 steps and 2158534 added (scaled 2)
c [bca-5] 45726 out of 51340 literals actually usable 89%
c [bca-5] added 58 blocked clauses in 196852 steps
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 45244420 penalty 0 = 0 + 0
c [sweep-5-1] 531 pos 3.6% + 14071 neg 96.4% = 14602 sched 56.9% ret 11067
c [sweep-5-1] 45247089 steps 1306 queries 98.48 avg class size
c [sweep-5-1] 26567 decisions 987 SAT calls 115.05 avg env size
c [sweep-5-1] 4707 variables remain 18% (20962 retained 82%)
c [decomp-19] removed 324 variables
c [sweep-5-1] removed 324 vars (0 failed, 328 eqs, 704 impls)
c [sweep-5] considered successful since not run to completion yet
c [sweep-5] removed 324 vars in TOTAL (1 rounds, 1305 queries)
c [sort-queue-9] sorted 12557 enqueued variables after 200004 conflicts
c [score-dist-9] active 12788 (50%), one 0 (0%), zero 12557 (50%)
c [score-dist-9] max exp 536, different 33 (6%)
c [score-dist-9] median active exp 523, avg 522.9
c [simplification-9] removed 338 variables 1.3% (25345 remain 72%)
c [simplification-9] removed 8338 irredundant clauses 0.8% (1075834 remain 81%)
c [simplification-9] maximum reduction of 1% = max (1%, 1%)
c [simplification-9] geometric conflict interval increment 45000 = 90000 / 2
c [simplification-9] new conflict interval 135000
c [simplification-9] penalized conflict interval 135000 = 1 * 135000
c [simplification-9] hard conflict limit 402504 (soft 335004 + delta 67500)
c [simplification-9] new conflict limit 335004 (hard 402504)
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 -  107.5   25345  1075834    220195   26501   5111 36407   82    84   53  97%    988    2   84   79  106%
c -  113.6   25345  1075834    253877   27437   5111 36407   81    84   54  97%   1002    1   80   80  101%
c -  119.5   25345  1075834    288848   27450   5111 36407   80    82   54  97%   1011    0   80   80  100%
c -  125.2   25345  1075834    324524   27688   5111 36407   81    84   54  97%   1017    1   82   80  102%
c 
c [simplification-10] limit 335004 conflicts (hard 402504) hit after 335005 conflicts
c [quatres-6] found 5698 quaternary clauses 11% in total
c [quatres-6-2] added 21 single-self-subsuming ternary resolvents
c [quatres-6-2] added 111 quaternary resolvents
c [ternres-6] limit 25083931 with penalty 0 = 0 + 0
c [ternres-6] all 25345 free variables schedulable
c [ternres-6] 89 ternary resolvents (2 bin, 87 trn)
c [ternres-6] fully completed ternary resolution
c [card-4] limit 1567745 penalty 3 = 3 + 0
c [card-4] found 4 at-most-one constraints of average size 3.8
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 1567745 for elimination
c [card-4] 4 out of 4 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [gauss-3] limit 1254196 penalty 2 = 2 + 0
c [gauss-3] extracted 2 xors of average arity 2.0
c [gauss-3] connected 4 occurrences of 2 variables (average 2.0)
c [gauss-3] limit 1254196 penalty 2 = 2 + 0
c [gauss-3] fully completed
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 18 transitive binary clauses
c [cce-3] limit of 31354914 steps penalty 2 = 2 + 0
c [cce-3-1] eliminated 2 clauses out of 4 (50%) of length 156
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 155
c [cce-3-1] eliminated 3 clauses out of 5 (60%) of length 154
c [cce-3-1] eliminated 2 clauses out of 2 (100%) of length 153
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 151
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 147
c [cce-3-1] eliminated 1 clauses out of 3 (33%) of length 146
c [cce-3-1] eliminated 2 clauses out of 2 (100%) of length 145
c [cce-3-1] eliminated 1 clauses out of 4 (25%) of length 143
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 14 large clauses in 31358773 steps
c [cce-3-1] allowing another 15679386 steps for small clauses
c [cce-3-1] scheduling 1021400 clauses = 1015473 binary + 5927 ternary
c [cce-3-1] tried to eliminate 144 small clauses 0%
c [cce-3-1] eliminated 49 binary clauses 0%
c [cce-3-1] eliminated 49 small clauses 0%
c [cce-3-1] eliminated 49 small clauses in 31354916 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 63 covered clauses in round 1
c [cce-3] eliminated 63 covered clauses in TOTAL during 1 rounds
c [cce-3] 63 < 1/100 * 1075829 = 10758 considered unsuccessful
c [bca-6] limit of 10000000 steps and 2158395 added (scaled 2)
c [bca-6] 45991 out of 50692 literals actually usable 91%
c [bca-6] added 347 blocked clauses in 191266 steps
c [sweep-6] limit 7525179 penalty 0 = 0 + 0
c [sweep-6-1] 97 pos 2.1% + 4506 neg 97.9% = 4603 sched 18.2% ret 20742
c [sweep-6-1] 7554745 steps 236 queries 351.90 avg class size
c [sweep-6-1] 3639 decisions 175 SAT calls 74.24 avg env size
c [sweep-6-1] 4104 variables remain 16% (21241 retained 84%)
c [decomp-21] removed 60 variables
c [sweep-6-1] removed 60 vars (0 failed, 60 eqs, 122 impls)
c [sweep-6] considered successful since not run to completion yet
c [sweep-6] removed 60 vars in TOTAL (1 rounds, 235 queries)
c [sort-queue-10] sorted 12525 enqueued variables after 335005 conflicts
c [score-dist-10] active 12760 (50%), one 0 (0%), zero 12525 (50%)
c [score-dist-10] max exp 537, different 34 (6%)
c [score-dist-10] median active exp 523, avg 523.5
c [simplification-10] removed 60 variables 0.2% (25285 remain 72%)
c [simplification-10] removed 68 irredundant clauses 0.0% (1075766 remain 81%)
c [simplification-10] maximum reduction of 0% = max (0%, 0%)
c [simplification-10] full geometric conflict interval increment 135000
c [simplification-10] new conflict interval 270000
c [simplification-10] penalized conflict interval 270000 = 1 * 270000
c [simplification-10] hard conflict limit 740005 (soft 605005 + delta 135000)
c [simplification-10] new conflict limit 605005 (hard 740005)
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 -  133.4   25285  1075766    361285   28932   5197 36783   81    82   54  98%   1020   -0   81   80  101%
c -  139.9   25285  1075766    396049   29851   5197 36783   79    79   55  99%   1022   -2   77   80   97%
c -  146.5   25285  1075766    433632   30514   5198 36801   80    82   54  98%   1023   -1   80   80  101%
c -  152.9   25285  1075766    473934   30959   5198 36802   80    82   54  97%   1023   -1   82   80  102%
c -  159.8   25285  1075766    516288   31432   5199 36802   79    81   54  98%   1024   -1   78   79   99%
c -  166.8   25285  1075766    558820   30830   5199 36802   78    80   54  98%   1024   -1   78   79   99%
c -  174.1   25285  1075766    602108   30505   5199 36803   76    87   53  87%   1024    6   79   78  101%
c 
c [simplification-11] limit 605005 conflicts (hard 740005) hit after 605005 conflicts
c [quatres-7] found 5790 quaternary clauses 11% in total
c [quatres-7-2] added 102 quaternary resolvents
c [ternres-7] limit 46140390 with penalty 0 = 0 + 0
c [ternres-7] all 25285 free variables schedulable
c [ternres-7] 0 ternary resolvents (0 bin, 0 trn)
c [ternres-7] fully completed ternary resolution
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 42 transitive binary clauses
c [bca-7] limit of 10000000 steps and 2158524 added (scaled 2)
c [bca-7] 45832 out of 50572 literals actually usable 91%
c [bca-7] added 25 blocked clauses in 187437 steps
c [sweep-7] limit 13842117 penalty 0 = 0 + 0
c [sweep-7-1] 2 pos 0.0% + 4071 neg 100.0% = 4073 sched 16.1% ret 21212
c [sweep-7-1] 13858353 steps 410 queries 384.02 avg class size
c [sweep-7-1] 3452 decisions 327 SAT calls 76.41 avg env size
c [sweep-7-1] 3354 variables remain 13% (21905 retained 87%)
c [decomp-23] removed 107 variables
c [sweep-7-1] removed 107 vars (0 failed, 83 eqs, 164 impls)
c [sweep-7] removed 107 vars in TOTAL (1 rounds, 409 queries)
c [sort-queue-11] sorted 12472 enqueued variables after 605005 conflicts
c [score-dist-11] active 12706 (50%), one 0 (0%), zero 12472 (50%)
c [score-dist-11] max exp 539, different 36 (7%)
c [score-dist-11] median active exp 525, avg 525.0
c [simplification-11] removed 107 variables 0.4% (25178 remain 72%)
c [simplification-11] removed 1484 irredundant clauses 0.1% (1074282 remain 81%)
c [simplification-11] maximum reduction of 0% = max (0%, 0%)
c [simplification-11] full geometric conflict interval increment 270000
c [simplification-11] new conflict interval 540000
c [simplification-11] penalized conflict interval 540000 = 1 * 540000
c [simplification-11] hard conflict limit 1415005 (soft 1145005 + delta 270000)
c [simplification-11] new conflict limit 1145005 (hard 1415005)
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 -  182.2   25178  1074282    642427   30242   5162 36540   79    81   53  98%   1024   -1   76   78   98%
c -  189.8   25178  1074282    684058   32066   5162 36540   77    78   54  98%   1024   -2   75   78   96%
c -  196.6   25178  1074282    724318   33308   5162 36540   76    79   55  97%   1024   -1   76   77   98%
c -  203.8   25178  1074282    766288   33503   5162 36540   75    78   54  95%   1024   -2   77   76  101%
c -  211.5   25178  1074282    812411   33147   5162 36540   72    77   54  93%   1024   -1   66   75   89%
c -  219.7   25178  1074282    859201   34682   5162 36545   74    81   54  91%   1024    3   75   74  101%
c -  227.4   25178  1074282    903330   34942   5162 36548   74    78   54  95%   1024    0   77   74  104%
c -  235.6   25178  1074282    948550   35075   5162 36550   74    77   54  97%   1024   -0   76   74  102%
c -  244.0   25178  1074282    994857   34978   5162 36550   73    75   54  97%   1024   -2   71   74   97%
c -  252.6   25178  1074282   1042885   35761   5162 36550   73    75   55  98%   1024   -1   74   73  100%
c -  261.6   25178  1074282   1091676   36020   5162 36550   73    74   55  98%   1024   -1   72   73   99%
c -  270.6   25178  1074282   1140733   36161   5162 36557   79    83   55  94%   1024    6   77   74  104%
c 
c [simplification-12] limit 1145005 conflicts (hard 1415005) hit after 1145005 conflicts
c [quatres-8] found 5863 quaternary clauses 11% in total
c [quatres-8-2] added 4 single-self-subsuming ternary resolvents
c [quatres-8-2] added 94 quaternary resolvents
c [treelook-3] limit 2250750 penalty 2 = 2 + 0 boost 1
c [treelook-3] scheduled 45194 literals 90%
c [treelook-3] scheduling used 2250811 steps
c [treelook-3] not fully scheduled
c [treelook-3] limit 2250750 penalty 2 = 2 + 0 boost 1
c [treelook-3] used 2535637 steps
c [treelook-3] 45175 literals remain 90%
c [treelook-3] 20956 variables remain to probed next time 83%
c [treelook-3] removed 0 variables, found 111 hbrs
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 24 transitive binary clauses
c [block-5] scheduling all variables this time
c [block-5] scheduled 25178 variables 100%
c [block-5] limit of 200000000 steps penalty 2 = 2 + 0
c [block-5] fully completed
c [block-5] transition to [ all 0 rem 0 ] state
c [block-5] eliminated 12764 blocked clauses
c [elim-8] no untried remaining variables left
c [elim-8] scheduled 24906 variables 100%
c [elim-8] boosting limit by 20
c [elim-8] limit of 4000000000 steps penalty 2 = 2 + 0
c [elim-8] rescheduling of touched variables disabled
c [elim-8-1] eliminated 21 variables 0% in round 1 in 199761861 steps
c [elim-8-1] backward subsumption/strengthening limit 199761800
c [elim-8-1-1] backward checking 4172 touched variables 17%
c [elim-8-1-1] incomplete backward checking 3664 remain 88%
c [elim-8-1] subsumed 16 and strengthened 417 clauses in 199764797 steps
c [elim-8-1] rescheduled 355 variables 1% by backward subsumption
c [elim-8-2] no variable eliminated in round 2 in 4671838 steps
c [elim-8] fully completed in 2 rounds
c [elim-8] transition to [ all 0 rem 0 ] state
c [elim-8] eliminated 21 = 0% variables out of 24906 scheduled
c [elim-8] 21 < 1/100 * 24906 = 249 considered unsuccessful
c [bca-8] limit of 10000000 steps and 2076207 added (scaled 2)
c [bca-8] 44751 out of 49772 literals actually usable 90%
c [bca-8] added 123 blocked clauses in 192915 steps
c [sweep-8] limit 27009004 penalty 0 = 0 + 0
c [sweep-8-1] 0 pos 0.0% + 3294 neg 100.0% = 3294 sched 13.2% ret 21591
c [sweep-8-1] 27023338 steps 1260 queries 1184.97 avg class size
c [sweep-8-1] 2977 decisions 510 SAT calls 85.72 avg env size
c [sweep-8-1] 1569 variables remain 6% (23316 retained 94%)
c [decomp-26] removed 748 variables
c [sweep-8-1] removed 748 vars (0 failed, 749 eqs, 1492 impls)
c [sweep-8] removed 748 vars in TOTAL (1 rounds, 1259 queries)
c [sort-queue-12] sorted 12165 enqueued variables after 1145005 conflicts
c [score-dist-12] active 11972 (50%), one 0 (0%), zero 12165 (50%)
c [score-dist-12] max exp 541, different 38 (7%)
c [score-dist-12] median active exp 527, avg 526.3
c [simplification-12] removed 1041 variables 4.1% (24137 remain 69%)
c [simplification-12] removed 39719 irredundant clauses 3.7% (1034563 remain 78%)
c [simplification-12] maximum reduction of 4% = max (4%, 4%)
c [simplification-12] geometric conflict interval increment 108000 = 540000 / 5
c [simplification-12] new conflict interval 648000
c [simplification-12] penalized conflict interval 648000 = 1 * 648000
c [simplification-12] hard conflict limit 2117005 (soft 1793005 + delta 324000)
c [simplification-12] new conflict limit 1793005 (hard 2117005)
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 -  293.7   24137  1034563   1196501   37186   5027 35458   77    80   54  96%   1024    1   78   76  102%
c -  303.5   24137  1034563   1252760   38135   5027 35462   72    82   54  88%   1024    2   70   76   93%
c -  314.0   24137  1034563   1310267   38232   5027 35462   77    79   53  98%   1024   -0   79   76  104%
c -  324.7   24137  1034563   1369670   39159   5027 35462   75    77   54  98%   1024   -2   74   76   97%
c -  334.7   24137  1034563   1427146   39678   5027 35462   76    77   55  98%   1024   -2   75   76   99%
c -  345.2   24137  1034563   1488407   40435   5027 35462   74    76   54  98%   1024   -3   74   75   99%
c -  355.2   24137  1034563   1547228   40331   5027 35462   75    77   54  98%   1024   -1   75   75   99%
c -  365.7   24137  1034563   1608367   41068   5027 35462   74    76   54  98%   1024   -2   73   74   98%
c -  376.0   24137  1034563   1670016   41670   5027 35484   78    80   55  97%   1024    0   78   76  103%
c -  386.3   24137  1034563   1732139   42385   5027 35484   77    78   55  98%   1024   -2   76   77  100%
c -  397.1   24137  1034563   1796343   41854   5027 35484   77    79   55  98%   1024   -1   78   76  103%
c 
c [simplification-13] limit 1793005 conflicts (hard 2117005) hit after 1798013 conflicts
c [quatres-9] found 5959 quaternary clauses 11% in total
c [quatres-9-2] added 84 quaternary resolvents
c [ternres-8] limit 72501771 with penalty 1 = 1 + 0
c [ternres-8] all 24137 free variables schedulable
c [ternres-8] 124 ternary resolvents (0 bin, 124 trn)
c [ternres-8] fully completed ternary resolution
c [basicprobe-3] limit 400000000 penalty 0 = 0 + 0
c [basicprobe-3-0] 19692 sched 89%, 2084 failed, 0 lifted, 4121 hbrs
c [decomp-28] removed 2087 variables
c [basicprobe-3-1] 3429 probes remain 16% after last round
c [basicprobe-3-1] 2084 units = 2084 failed (100%) + 0 lifted (0%)
c [basicprobe-3-1] removed 2087 variables, found 4206 hbrs
c [bate-2] eliminated 1919 asymmetric tautologies during probing
c [unhide-6] limit 625000 with penalty 5 = 3 + 2
c [unhide-6-6] 0 units, 0 failed, 651 tauts, 0 hbrs, 57775 literals
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 5 transitive binary clauses
c [bca-9] limit of 10000000 steps and 1651218 added (scaled 2)
c [bca-9] 39619 out of 44102 literals actually usable 90%
c [bca-9] added 140 blocked clauses in 275378 steps
c [sweep-9] limit 43501062 penalty 0 = 0 + 0
c [sweep-9-1] 0 pos 0.0% + 2 neg 100.0% = 2 sched 0.0% ret 22048
c [sweep-9-1] 7198 steps 2 queries 1.00 avg class size
c [sweep-9-1] 0 decisions 0 SAT calls 0.00 avg env size
c [sweep-9-1] fully completed sweeping round
c [decomp-29] removed 1 variables
c [sweep-9-1] removed 1 vars (0 failed, 1 eqs, 1 impls)
c [sweep-9-2] 880 pos 4.0% + 21169 neg 96.0% = 22049 sched 100.0% ret 0
c [sweep-9-2] 43515643 steps 1768 queries 86.21 avg class size
c [sweep-9-2] 31666 decisions 1740 SAT calls 103.96 avg env size
c [sweep-9-2] 849 variables remain 4% (21200 retained 96%)
c [decomp-30] removed 29 variables
c [sweep-9-2] removed 29 vars (0 failed, 38 eqs, 155 impls)
c [sweep-9] removed 30 vars in TOTAL (2 rounds, 1768 queries)
c [sort-queue-13] sorted 11918 enqueued variables after 1798013 conflicts
c [score-dist-13] active 10102 (46%), one 0 (0%), zero 11918 (54%)
c [score-dist-13] max exp 542, different 38 (7%)
c [score-dist-13] median active exp 527, avg 527.4
c [simplification-13] removed 2117 variables 8.8% (22020 remain 63%)
c [simplification-13] removed 212529 irredundant clauses 20.5% (822034 remain 62%)
c [simplification-13] maximum reduction of 21% = max (9%, 21%)
c [simplification-13] large reduction 21% >= 5% limit
c [simplification-13] next conflict interval 17980 = min (1798013/100, 648000)
c [simplification-13] penalized conflict interval 17980 = 1 * 17980
c [simplification-13] hard conflict limit 1825993 (soft 1815993 + delta 10000)
c [simplification-13] new conflict limit 1815993 (hard 1825993)
c 
c [simplification-14] limit 1815993 conflicts (hard 1825993) hit after 1823840 conflicts
c [quatres-10] found 6098 quaternary clauses 12% in total
c [quatres-10-2] added 14 single-self-subsuming ternary resolvents
c [quatres-10-2] added 93 quaternary resolvents
c [ternres-9] limit 146736317 with penalty 0 = 0 + 0
c [ternres-9] all 22020 free variables schedulable
c [ternres-9] 64 ternary resolvents (0 bin, 64 trn)
c [ternres-9] fully completed ternary resolution
c [gauss-4] limit 3668407 penalty 3 = 3 + 0
c [gauss-4] extracted 2 xors of average arity 2.0
c [gauss-4] connected 4 occurrences of 2 variables (average 2.0)
c [gauss-4] limit 3668407 penalty 3 = 3 + 0
c [gauss-4] fully completed
c [gauss-4] exported 0 unary, 0 binary and 0 ternary equations
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 8 transitive binary clauses
c [block-6] scheduling all variables this time
c [block-6] scheduled 22020 variables 100%
c [block-6] limit of 400000000 steps penalty 1 = 1 + 0
c [block-6] fully completed
c [block-6] transition to [ all 0 rem 0 ] state
c [block-6] eliminated 863 blocked clauses
c [block-6] 863 < 1/100 * 822030 = 8220 considered unsuccessful
c [cce-4] boosting limit by 10
c [cce-4] limit of 917101985 steps penalty 3 = 3 + 0
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 143
c [cce-4-1] eliminated 1 clauses out of 3 (33%) of length 142
c [cce-4-1] eliminated 2 clauses out of 4 (50%) of length 141
c [cce-4-1] eliminated 20 clauses out of 20 (100%) of length 139
c [cce-4-1] eliminated 2 clauses out of 4 (50%) of length 138
c [cce-4-1] eliminated 1 clauses out of 1 (100%) of length 137
c [cce-4-1] eliminated 30 clauses out of 30 (100%) of length 131
c [cce-4-1] eliminated 1 clauses out of 3 (33%) of length 130
c [cce-4-1] eliminated 3 clauses out of 5 (60%) of length 129
c [cce-4-1] eliminated 2 clauses out of 6 (33%) of length 127
c [cce-4-1] eliminated 2 clauses out of 4 (50%) of length 125
c [cce-4-1] eliminated 4 clauses out of 4 (100%) of length 124
c [cce-4-1] eliminated 2 clauses out of 4 (50%) of length 123
c [cce-4-1] eliminated 2 clauses out of 3 (67%) of length 119
c [cce-4-1] eliminated 3 clauses out of 3 (100%) of length 118
c [cce-4-1] eliminated 1 clauses out of 3 (33%) of length 117
c [cce-4-1] eliminated 3 clauses out of 5 (60%) of length 116
c [cce-4-1] eliminated 2 clauses out of 4 (50%) of length 115
c [cce-4-1] eliminated 2 clauses out of 4 (50%) of length 114
c [cce-4-1] eliminated 1 clauses out of 5 (20%) of length 113
c [cce-4-1] eliminated 2 clauses out of 4 (50%) of length 112
c [cce-4-1] eliminated 3 clauses out of 8 (38%) of length 111
c [cce-4-1] eliminated 1 clauses out of 2 (50%) of length 110
c [cce-4-1] eliminated 4 clauses out of 8 (50%) of length 109
c [cce-4-1] eliminated 1 clauses out of 1 (100%) of length 108
c [cce-4-1] eliminated 3 clauses out of 8 (38%) of length 105
c [cce-4-1] eliminated 1 clauses out of 5 (20%) of length 104
c [cce-4-1] eliminated 1 clauses out of 19 (5%) of length 103
c [cce-4-1] eliminated 3 clauses out of 17 (18%) of length 102
c [cce-4-1] eliminated 392 clauses out of 975 (40%) of length 101
c [cce-4-1] eliminated 119 clauses out of 128 (93%) of length 100
c [cce-4-1] eliminated 4 clauses out of 16 (25%) of length 99
c [cce-4-1] eliminated 6 clauses out of 13 (46%) of length 98
c [cce-4-1] eliminated 3 clauses out of 33 (9%) of length 97
c [cce-4-1] eliminated 1 clauses out of 5 (20%) of length 96
c [cce-4-1] eliminated 2 clauses out of 23 (9%) of length 95
c [cce-4-1] eliminated 5 clauses out of 8 (62%) of length 94
c [cce-4-1] eliminated 1 clauses out of 4 (25%) of length 93
c [cce-4-1] eliminated 21 clauses out of 28 (75%) of length 92
c [cce-4-1] eliminated 2 clauses out of 11 (18%) of length 91
c [cce-4-1] eliminated 21 clauses out of 28 (75%) of length 90
c [cce-4-1] eliminated 1 clauses out of 21 (5%) of length 89
c [cce-4-1] eliminated 5 clauses out of 14 (36%) of length 88
c [cce-4-1] eliminated 373 clauses out of 943 (40%) of length 86
c [cce-4-1] eliminated 147 clauses out of 160 (92%) of length 85
c [cce-4-1] eliminated 16 clauses out of 26 (62%) of length 84
c [cce-4-1] eliminated 3 clauses out of 38 (8%) of length 83
c [cce-4-1] eliminated 17 clauses out of 24 (71%) of length 82
c [cce-4-1] eliminated 2 clauses out of 16 (12%) of length 81
c [cce-4-1] eliminated 3 clauses out of 37 (8%) of length 80
c [cce-4-1] eliminated 1 clauses out of 19 (5%) of length 79
c [cce-4-1] eliminated 17 clauses out of 78 (22%) of length 78
c [cce-4-1] eliminated 17 clauses out of 48 (35%) of length 77
c [cce-4-1] eliminated 21 clauses out of 97 (22%) of length 76
c [cce-4-1] eliminated 14 clauses out of 83 (17%) of length 75
c [cce-4-1] eliminated 15 clauses out of 116 (13%) of length 74
c [cce-4-1] eliminated 12 clauses out of 165 (7%) of length 73
c [cce-4-1] incomplete large round (ATE)
c [cce-4-1] eliminated 1346 large clauses in 917102849 steps
c [cce-4-1] allowing another 458551424 steps for small clauses
c [cce-4-1] scheduling 766481 clauses = 764470 binary + 2011 ternary
c [cce-4-1] tried to eliminate 2109 small clauses 0%
c [cce-4-1] eliminated 1247 binary clauses 0%
c [cce-4-1] eliminated 1247 small clauses 0%
c [cce-4-1] eliminated 1247 small clauses in 917102025 steps
c [cce-4-1] incomplete small round (ATE)
c [cce-4-1] eliminated 2593 covered clauses in round 1
c [cce-4] eliminated 2593 covered clauses in TOTAL during 1 rounds
c [cce-4] 2593 < 1/100 * 821167 = 8211 considered unsuccessful
c [bca-10] limit of 10000000 steps and 1644328 added (scaled 2)
c [bca-10] 39202 out of 43922 literals actually usable 89%
c [bca-10] added 7 blocked clauses in 183007 steps
c [sweep-10] limit 44020895 penalty 0 = 0 + 0
c [sweep-10-1] 1 pos 0.1% + 848 neg 99.9% = 849 sched 3.9% ret 21111
c [sweep-10-1] 9921681 steps 438 queries 68.16 avg class size
c [sweep-10-1] 2387 decisions 437 SAT calls 73.96 avg env size
c [sweep-10-1] fully completed sweeping round
c [sweep-10-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-10-2] 805 pos 3.7% + 21155 neg 96.3% = 21960 sched 100.0% ret 0
c [sweep-10-2] 34117452 steps 1367 queries 102.29 avg class size
c [sweep-10-2] 27562 decisions 1356 SAT calls 100.17 avg env size
c [sweep-10-2] 1667 variables remain 8% (20293 retained 92%)
c [decomp-33] removed 7 variables
c [sweep-10-2] removed 7 vars (0 failed, 18 eqs, 128 impls)
c [sweep-10] 7 < 1/1000 * 21960 = 21 considered unsuccessful
c [sweep-10] removed 7 vars in TOTAL (2 rounds, 1803 queries)
c [sort-queue-14] sorted 11794 enqueued variables after 1823840 conflicts
c [score-dist-14] active 10159 (46%), one 0 (0%), zero 11794 (54%)
c [score-dist-14] max exp 542, different 38 (7%)
c [score-dist-14] median active exp 527, avg 527.4
c [simplification-14] removed 67 variables 0.3% (21953 remain 63%)
c [simplification-14] removed 3460 irredundant clauses 0.4% (818574 remain 61%)
c [simplification-14] maximum reduction of 0% = max (0%, 0%)
c [simplification-14] full geometric conflict interval increment 648000
c [simplification-14] conflict interval soft limit 1000000 reached
c [simplification-14] new conflict interval 1000000
c [simplification-14] penalized conflict interval 1000000 = 1 * 1000000
c [simplification-14] hard conflict limit 3323840 (soft 2823840 + delta 500000)
c [simplification-14] new conflict limit 2823840 (hard 3323840)
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 -  436.5   21953   818574   1862946   42169   4649 35321   78    80   50  97%   1024    1   79   76  103%
c -  448.3   21953   818574   1931362   44298   4649 35321   76    78   51  98%   1024   -1   76   76  100%
c -  459.4   21953   818574   1997715   44534   4649 35321   76    78   51  97%   1024   -2   76   75  101%
c -  471.1   21953   818574   2065321   44058   4649 35322   76    82   51  93%   1024    3   77   75  103%
c -  482.0   21953   818574   2132591   45239   4649 35322   76    78   51  97%   1024   -1   76   75  101%
c -  493.3   21953   818574   2199889   44885   4649 35322   77    78   51  98%   1024   -1   75   75  100%
c -  504.9   21953   818574   2270574   45251   4649 35322   75    76   51  98%   1024   -3   74   74  100%
c -  516.7   21953   818574   2341523   47081   4649 35322   75    78   52  97%   1024   -1   75   75  100%
c -  528.5   21953   818574   2411188   46609   4649 35322   76    77   52  98%   1024   -1   74   75  100%
c -  541.2   21953   818574   2483948   44762   4649 35327   76    86   51  89%   1024    8   80   74  108%
c -  553.5   21953   818574   2558694   47874   4649 35329   76    78   52  97%   1024   -1   77   76  102%
c -  566.1   21953   818574   2632943   49048   4649 35329   76    78   53  97%   1024   -0   75   76   99%
c -  578.5   21953   818574   2706588   48681   4649 35329   76    78   52  98%   1024   -1   77   75  102%
c -  591.8   21953   818574   2785380   48474   4649 35329   75    77   52  98%   1024   -1   75   75   99%
c 
c [simplification-15] limit 2823840 conflicts (hard 3323840) hit after 2859196 conflicts
c [quatres-11] found 6175 quaternary clauses 13% in total
c [quatres-11-2] added 80 quaternary resolvents
c [ternres-10] limit 200000000 with penalty 0 = 0 + 0
c [ternres-10] all 21953 free variables schedulable
c [ternres-10] 2 ternary resolvents (0 bin, 2 trn)
c [ternres-10] fully completed ternary resolution
c [card-5] limit 7395162 penalty 4 = 4 + 0
c [card-5] found 34 at-most-one constraints of average size 3.0
c [card-5] no at-most-two constraint found
c [card-5] using previous limit 7395162 for elimination
c [card-5] 34 out of 34 constraints (100%) meet size limits
c [card-5] no units found
c [card-5] no at-most-one constraints generated
c [transred-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 2 transitive binary clauses
c [bca-11] limit of 10000000 steps and 1644332 added (scaled 2)
c [bca-11] 39353 out of 43908 literals actually usable 90%
c [bca-11] added 0 blocked clauses in 328645 steps
c [sort-queue-15] sorted 11784 enqueued variables after 2859196 conflicts
c [score-dist-15] active 10169 (46%), one 0 (0%), zero 11784 (54%)
c [score-dist-15] max exp 543, different 39 (7%)
c [score-dist-15] median active exp 528, avg 528.3
c [simplification-15] removed 0 variables 0.0% (21953 remain 63%)
c [simplification-15] removed 0 irredundant clauses 0.0% (818574 remain 61%)
c [simplification-15] maximum reduction of 0% = max (0%, 0%)
c [simplification-15] full geometric conflict interval increment 1000000
c [simplification-15] new conflict interval 2000000
c [simplification-15] penalized conflict interval 2000000 = 1 * 2000000
c [simplification-15] hard conflict limit 5859196 (soft 4859196 + delta 1000000)
c [simplification-15] new conflict limit 4859196 (hard 5859196)
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 -  606.9   21953   818574   2866288   49258   4651 35327   75    81   54  92%   1024    4   77   74  104%
c -  619.9   21953   818574   2942060   49906   4651 35327   75    76   55  98%   1024   -1   76   75  101%
c -  633.9   21953   818574   3023817   50562   4651 35327   74    75   55  98%   1024   -2   73   75   98%
c -  648.3   21953   818574   3109179   48874   4651 35327   74    76   54  98%   1024   -1   74   74   99%
c -  663.8   21953   818574   3201571   52097   4651 35327   73    75   55  99%   1024   -1   73   74   99%
c -  677.6   21953   818574   3283661   51302   4651 35328   76    77   55  98%   1024   -1   76   75  102%
c -  691.9   21953   818574   3368374   51694   4651 35328   75    76   55  98%   1024   -1   76   75  102%
c -  706.9   21953   818574   3457623   52115   4651 35328   75    76   56  99%   1024   -1   74   74   99%
c -  721.8   21953   818574   3547263   52393   4651 35328   74    75   55  99%   1024   -1   75   74  101%
c -  736.7   21953   818574   3637033   53528   4651 35328   75    76   56  98%   1024   -0   76   74  103%
c -  752.3   21953   818574   3729007   54394   4651 35328   74    75   56  99%   1024   -2   75   74  101%
c -  767.8   21953   818574   3820236   53704   4651 35328   74    75   56  99%   1024   -1   76   74  103%
c -  785.1   21953   818574   3922747   54725   4651 35328   73    74   56  99%   1024   -1   74   73  101%
c -  801.9   21953   818574   4022383   56242   4651 35332   77    79   57  98%   1024    1   77   73  105%
c -  818.5   21953   818574   4117682   57118   4651 35333   77    78   57  98%   1024   -0   76   75  101%
c -  834.2   21953   818574   4207038   55902   4651 35333   75    76   57  98%   1024   -2   75   75  100%
c -  850.6   21953   818574   4301087   55212   4651 35333   75    77   57  98%   1024   -1   75   75  101%
c -  867.1   21953   818574   4395143   58420   4651 35333   75    76   58  98%   1024   -1   74   75   99%
c -  882.5   21953   818574   4482026   57996   4651 35333   75    76   58  99%   1024   -2   73   75   98%
c -  898.7   21953   818574   4572561   58851   4651 35333   75    76   58  98%   1024   -1   75   75  100%
c -  914.9   21953   818574   4664139   59283   4651 35333   75    76   58  98%   1024   -1   74   74  100%
c -  931.1   21953   818574   4756998   58199   4651 35333   75    76   57  99%   1024   -1   75   74  101%
c -  948.5   21953   818574   4856647   58218   4651 35334   76    78   57  97%   1024    2   77   74  105%
c 
c [simplification-16] limit 4859196 conflicts (hard 5859196) hit after 4859198 conflicts
c [quatres-12] found 6255 quaternary clauses 13% in total
c [quatres-12-2] added 52 quaternary resolvents
c [ternres-11] limit 200000000 with penalty 0 = 0 + 0
c [ternres-11] all 21953 free variables schedulable
c [ternres-11] 0 ternary resolvents (0 bin, 0 trn)
c [ternres-11] fully completed ternary resolution
c [transred-11] limit 2000000 with penalty 0 = 0 + 0
c [transred-11] removed 34 transitive binary clauses
c [elim-9] scheduling all variables this time
c [elim-9] scheduled 21953 variables 100%
c [elim-9] limit of 100000000 steps penalty 3 = 3 + 0
c [elim-9] rescheduling of touched variables disabled
c [elim-9] incomplete 1125 not tried 5% in round 1
c [elim-9] transition to [ all 1 rem 1 ] state
c [elim-9] eliminated 67 = 0% variables out of 21953 scheduled
c [elim-9] 67 < 1/100 * 21953 = 219 considered unsuccessful
c [sweep-11] boosting sweeping limit by 10
c [sweep-11] limit 657835770 penalty 1 = 1 + 0
c [sweep-11-1] 25 pos 1.5% + 1639 neg 98.5% = 1664 sched 7.6% ret 20222
c [sweep-11-1] 19797845 steps 851 queries 95.26 avg class size
c [sweep-11-1] 6884 decisions 850 SAT calls 76.41 avg env size
c [sweep-11-1] fully completed sweeping round
c [sweep-11-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-11-2] 729 pos 3.3% + 21157 neg 96.7% = 21886 sched 100.0% ret 0
c [sweep-11-2] 54804443 steps 2219 queries 87.54 avg class size
c [sweep-11-2] 32365 decisions 2209 SAT calls 93.32 avg env size
c [sweep-11-2] fully completed sweeping round
c [decomp-37] removed 4 variables
c [sweep-11-2] removed 4 vars (0 failed, 11 eqs, 101 impls)
c [sweep-11-3] 729 pos 3.3% + 21153 neg 96.7% = 21882 sched 100.0% ret 0
c [sweep-11-3] 53217578 steps 2180 queries 79.56 avg class size
c [sweep-11-3] 31898 decisions 2167 SAT calls 98.19 avg env size
c [sweep-11-3] fully completed sweeping round
c [decomp-38] removed 13 variables
c [sweep-11-3] removed 13 vars (0 failed, 22 eqs, 130 impls)
c [sweep-11] 17 < 1/1000 * 21886 = 21 considered unsuccessful
c [sweep-11] removed 17 vars in TOTAL (3 rounds, 5247 queries)
c [sort-queue-16] sorted 11355 enqueued variables after 4859198 conflicts
c [score-dist-16] active 10514 (48%), one 0 (0%), zero 11355 (52%)
c [score-dist-16] max exp 545, different 41 (8%)
c [score-dist-16] median active exp 529, avg 529.5
c [simplification-16] removed 84 variables 0.4% (21869 remain 62%)
c [simplification-16] removed 2343 irredundant clauses 0.3% (816231 remain 61%)
c [simplification-16] maximum reduction of 0% = max (0%, 0%)
c [simplification-16] full geometric conflict interval increment 2000000
c [simplification-16] conflict interval soft limit 1000000 reached
c [simplification-16] new conflict interval 1000000
c [simplification-16] penalized conflict interval 1000000 = 1 * 1000000
c [simplification-16] hard conflict limit 6359198 (soft 5859198 + delta 500000)
c [simplification-16] new conflict limit 5859198 (hard 6359198)
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 -  971.8   21869   816231   4945264   59935   3515 35619   75    77   56  99%   1024   -2   75   75   99%
c -  987.0   21869   816231   5031141   59948   3515 35619   75    77   56  98%   1024   -2   76   75  101%
c
c CAUGHT SIGNAL 15 SIGTERM
c
c s UNKNOWN
c bate: 1996 basic ate = 291 trn 15% + 1705 lrg 85% in 2 updates
c bcas: 11 count, 13368 added (2293 skipped), 2322557 steps
c bkwd: tried 266275 clauses, 532089 lits, 2.00 lits/clause
c bkwd: checked 329567766 occs, 1237.70 occs/clause, 619.38 occs/lit
c bkwd: subsumed 0 binary, 0 ternary, 16 large
c bkwd: strengthened 0 binary, 0 ternary (0% self), 672 large (0% self)
c blkd: 6 bces, 188927 removed, 45167323 resolutions, 147932831 steps
c blkd: 7549 blocking literals 11%, 2927 pure
c bump: 4923889 bumped seen, 916537989 lits 186.1 on average
c card: 5 count, 0 units, 0 am1, 35974369 steps
c card: 4 rescheduled, 36 eliminated, 37092 resolved, 264 subsumed
c card: 48 at-most-one constraints found, average size 3.08
c card: 48 at-most-one constraints used 100%, average size 3.08
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: 4 cces, 2777 eliminated, 2775 ate 100%, 2 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: 5269456 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 62 gcs, 0 rescored clauses, 0 rescored vars
c dcps: 38 decompositions, 1298 equivalent 4%
c deco: 3363 decision-only clauses 0%, 68% reduction
c decs: 13771636 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 9 elims, 9042 eliminated 26%, 11 pure 0%
c elms: 12 rounds, 1.3 rounds/bve
c elms: 2297 small 25%, 3807 large 42%
c elms: 2312 tried small, 2297 succeeded 99%, 15 failed 1%
c elms: 30228 subsumed, 159181 strengthened, 1986 blocked
c elms: 7510715 copies, 17910160 resolutions, 42765 ipos
c elms: 40841046 subchks, 17940074 strchks
c gaus: 4 extractions, 4 extracted, 2.0 size, 2 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 16400388 steps, 8200194 extr 50%, 18 elim 0%
c glue: 75.3 orig avg, 75.3 real avg, 9.0 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 39734 = 33715 simple 85% + 5970 trn 15% + 49 lrg 0%, 1492 sub 4%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 4923888 clauses, 95.4 length
c lrnd: 469559127 lits = 724489037 orig - 254929910 removed 35%
c lrnd: 1240974 uips 25%, 2149744 flips 44%
c mins: 4919924 mins 100%, 103 bin 0%, 497 size 0%
c mins: 288283891 poisoned searches, 30419749 hits, 11% hit rate
c mins: 975723668 used twice searches, 302611564 hits, 31% hit rate
c move: moved 176204, 174314 bin 99%, 1890 trn 1%
c otfs: 179278 driving 60%, 118358 restarting 40%
c otfs: str 297636, 296032 red 99%, 1604 irr 1%
c otfs: str 297636, 0 bin 0%, 2 trn 0%, 297634 lrg 100%
c otfs: sub 802, 802 red 100%, 0 irr 0%
c otfs: sub 802, 0 bin 0%, 0 trn 0%, 802 lrg 100%
c phas: 1 computed, 31023 set, 0 pos (0%), 31023 neg (100%)
c prbs: 3 basic, 76339 probed, 2530 failed, 0 lifted
c prbs: 3 simple, 68752 probed, 0 failed, 0 eqs
c prbs: 3 treelook, 30 probed, 0 failed, 0 lifted
c prom: 5396 locked 0% out of 1191908 tried
c prps: 2874409846 props, 199 props/dec
c prps: 95% srch, 5% simp, 0% lkhd
c quat: 12 count, 1365 quat, 210 self1, 0 self2, 0 dup
c queu: 16 sorted, 13771636 next (698364 steps 0.05)
c queu: 916819736 enq (1161954831 steps 1.27), 916537989 deq 100%
c redc: 358 clauses 45%, 792 tried 0%, 44 sat 6%
c redc: 3146 lits 34%, 9370 tried 0%, 44 sat 0%
c redc: 86 times jump level reduced, 92.4 levels on average
c reds: 78 count, 65411.8 conflicts per reduce
c reds: 0 memlim 0%, 78 arith 100%
c reds: 3451680 collected 93%, 253965 retired 7%
c rmbd: 3357 removed, 1424 red 42%
c rsts: 1807 restarts 45%, 2252 skipped 55%
c rsts: 2252 saturating 100%, 0 reuse 0%
c rsts: 0 kept 0.0% average 0.0%
c scnc: 0 count, 1.000 min (0/1000), 1.000 max (0/1000)
c simp: 16 count, 16 confs 100%, 0 vars 0%
c simp: 0 its 0%, 0 bin 0%, 0 trns 0%
c subl: 4923888 count (17912339 tried 3.6), 1099068 sub out of 4923482 (22.3%)
c swps: 11 count, 15 rounds, 12308 queries (820.5/round)
c swps: 11017 sat calls, 51 unsat (0.1% success rate)
c swps: 176795 decisions 16.0, 1049 conflicts 0.1
c swps; 241.6 avg class size, 97.9 avg environment size
c swps: 0 failed, 3078 impls, 1342 equivs
c swp0: 4098 type 0 queries, 1525 unsat (37.2%), 3427 sat (83.6%)
c swp1: 8210 type 1 queries, 1968 unsat (24.0%), 7539 sat (91.8%)
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: 37391384 calls to obtain time
c tops: 2856 fixed 8%, 0 its, 0.00 confs/it
c trds: 11 transitive reductions, 145 removed, 0 failed
c trds: 3109 nodes, 39124 edges, 21096403 steps
c trim: 2333335 words, 8.9 MB
c trnr: 11 count, 3 bin, 5929 trn, 68920132 steps
c unhd: 6 count, 6 rounds, 11554166 steps
c unhd: 8 non-trivial sccs of average size 2.0
c unhd: 0 units, 0 bin, 0 trn, 0 lrg
c unhd: 1 failed, 0 stamp, 0 lits, 0 bin, 0 trn, 0 lrg
c unhd: 8934 tauts, 4 bin 0%, 141 trn 2%, 3 lrg 0%
c unhd: 8934 tauts, 8786 stamp 98%, 1940 red 22%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 202370 str, 0 bin 0%, 352 trn 0%, 202018 lrg 100%, 195260 red 96%
c vars: 21869 remaining 62% and 13196 removed 38% out of 35065
c vars: 2856 fixed 8%, 9042 eliminated 26%, 1298 equivalent 4%
c vsts: 47036046572 visits, 99% srch, 1% simp, 0% lkhd
c vsts: 16.9 search visits per propagation, 9108.9 per conflict
c wchs: 3974322518 pushed, 103505104 enlarged, 116 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all        4924847       3451680        253965      97769504      48074186       3316280
c 
c  0 0          2081   0        41   0         0   0  36323603  37   3940576   8     17343   1     0.1
c  1 5           133   0         7   0        82   0    220561   0    143835   0       588   0     0.0
c  2 6           635   0        75   0       411   0   2701984   3   2160949   4      8331   0     0.0
c  3 9           589   0       183   0       359   0    471603   0    427812   1      9375   0     0.0
c  4 14          485   0       140   0       240   0   3208084   3<  1159492   2     18551   1     0.0
c  5 21        10441   0      7134   0      1638   1  20344148  21  14227733  30    832802  25     0.2
c  6 30        57464   1     50542   1      1857   1   2911732   3   2358600   5<   155183   5     0.6
c  7 41        14677   0      9784   0      2489   1   2336237   2   1302551   3     42438   1     0.3
c  8 54        76285   2     47705   1     15446   6   6153637   6   3604916   7    160968   5<    2.3
c  9 69      4655364  95<  3248772  94<   229412  90< 22746600  23  18468276  38   2046582  62    48.9
c 10 86       104199   2     87262   3      1979   1    347895   0    277499   1     24107   1    17.4
c 11 126        2221   0        33   0        40   0      3086   0      1740   0        12   0     1.3
c 12 230         273   0         2   0        12   0       334   0       207   0         0   0     0.3
c 
c avg                  9.0           9.0           8.9           4.2           6.3           7.7
c std                  0.5           0.5           0.7           3.7           2.8           1.9
c 
c  108.021  11% bump
c   35.639   4% elim
c   24.538   2% probe
c   20.827   2% block
c   15.007   2% sweep
c    8.665   1% decide
c    6.538   1% cce
c 
c   11.104 < 1% rest (below)
c 
c    4.126   0% unhide
c    2.743   0% bca
c    1.646   0% quatres
c    1.021   0% card
c    0.813   0% gauss
c    0.428   0% transred
c    0.325   0% ternres
c    0.000   0% locs
c    0.000   0% queuesort
c    0.000   0% rescore
c ==================================
c    8.890   1% preprocessing     7%
c  111.409  11% inprocessing     93%
c ==================================
c  120.298  12% simplifying
c  879.064  88% search
c ==================================
c  999.366 100% all
c 
c       5102118 conflicts,        5105.4 confs/sec
c            19 ternaries,      268532.5 confs/ternary
c           131 binaries,        38947.5 confs/binary
c             0 iterations,          0.0 confs/iteration
c 
c            78 reductions,          0.1 redus/sec,  65411.8 confs/reduction
c          1807 restarts,            1.8 rests/sec,   2823.5 confs/restart
c      13771636 decisions,       13780.4 decis/sec,      2.7 decis/conflict
c    2874409846 propagations,  2876233.5 props/sec,    208.7 props/decision
c 
c 999.4 seconds, 129.3 MB
c
c CAUGHT SIGNAL 15 SIGTERM
c
c launch: done
