c launch: /data/cnf/sc2014/app/007-80-12.cnf.bz2
c host: atom19
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/007-80-12.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/007-80-12.cnf.bz2
c no embedded options
c found 'p cnf 13408 478488' header
c read 13408 variables, 478488 clauses, 3138520 literals in 0.00 seconds
c
c --abstime=0
c --bate=1
c --batewait=2
c --bca=1
c --bcaddlimldscale=2
c --bcamaxeff=10000000
c --bcaminuse=100
c --bcawait=2
c --bkwdscale=100
c --bkwdroundlim=7
c --bkwdresched=1
c --blkboost=10
c --blkboostvlim=10000000
c --blkclslim=1000000
c --blklarge=1
c --blkmaxeff=800000000
c --blkmineff=50000000
c --blkocclim1=100000
c --blkocclim=1000000
c --blkocclim2=10000
c --blkreleff=100
c --blkresched=1
c --blkrtc=0
c --blksmall=1
c --blksuccessmaxwortc=6
c --blksuccessrat=100
c --block=1
c --blockwait=1
c --boost=1
c --bumpsimp=1
c --card=1
c --cardcut=2
c --cardexpam1=3
c --cardglue=0
c --cardignused=0
c --cardmaxeff=300000000
c --cardmaxlen=1000
c --cardmineff=2000000
c --cardminlen=3
c --cardocclim1=300
c --cardocclim2=15
c --cardreleff=5
c --cardreschedint=10
c --carduse=2
c --cardwait=0
c --cce2wait=1
c --cce=3
c --cceateint=2
c --cceboost=10
c --cceboostdel=3
c --cceboostint=5
c --cceboostvlim=10000000
c --cce3wait=2
c --ccemaxround=3
c --ccemaxeff=2147483647
c --ccemineff=30000000
c --ccereleff=50
c --ccertc=0
c --ccertcint=15
c --ccertcintvlim=2000000
c --ccesuccessrat=100
c --ccewait=2
c --clim=-1
c --compact=0
c --deco=1
c --decolim=100
c --deco1opt=1
c --decompose=1
c --defragfree=50
c --defragint=10000000
c --delmax=10
c --dlim=-1
c --druplig=0
c --drupligcheck=0
c --drupligtrace=0
c --drupligtraceorig=0
c --elim=1
c --elmaxeff=800000000
c --elmblk=1
c --elmblkwait=1
c --elmboost=20
c --elmboostdel=3
c --elmboostint=5
c --elmboostvlim=4000000
c --elmclslim=1000000
c --elmfull=0
c --elmineff=20000000
c --elmlitslim=200
c --elmocclim1=1000
c --elmocclim=1000000
c --elmocclim2=100
c --elmoccsumforced=0
c --elmreleff=200
c --elmresched=0
c --elmroundlim=3
c --elmrtc=0
c --elmrtcint=10
c --elmrtcintvlim=500000
c --elmsuccessmaxwortc=4
c --elmsuccessrat=100
c --exitonabort=0
c --factmax=100000
c --factor=3
c --gauss=1
c --gaussexptrn=1
c --gaussextrall=1
c --gaussmaxeff=50000000
c --gaussmaxor=20
c --gaussmineff=2000000
c --gaussreleff=2
c --gausswait=2
c --gluekeep=4
c --gluekeepsize=15
c --gluescale=4
c --hbrdom=2
c --import=1
c --incredcint=1
c --incredconfslim=0
c --incsavevisits=0
c --inprocessing=1
c --irrlim=1
c --jwhred=1
c --keepmaxglue=1
c --keepmaxglueint=100
c --lhbr=1
c --lkhd=2
c --locs=0
c --locsbanner=0
c --locsclim=1000000
c --locsboost=2
c --locscint=10000
c --locset=2
c --locsexport=1
c --locsmaxeff=100000
c --locsmineff=1000
c --locsred=0
c --locsreleff=5
c --locsrtc=0
c --locsvared=100
c --locswait=2
c --maxscaledglue=15
c --memlim=-1
c --minimize=2
c --minlocalgluelim=200
c --minlocalsizelim=3000
c --minrecgluelim=100
c --minrecsizelim=1000
c --norestartsatlimlo=85
c --move=2
c --otfs=1
c --penmax=4
c --phase=0
c --phaseluckfactor=200
c --phaselucklim=100
c --phaseluckmaxround=10
c --phasesave=1
c --plain=0
c --plim=-1
c --poison=1
c --prbasic=1
c --prbasicmaxeff=400000000
c --prbasicmineff=1000000
c --prbasicreleff=50
c --prbasicroundlim=8
c --prbasicrtc=0
c --prbrtc=0
c --prbsimple=2
c --prbsimpleboost=10
c --prbsimpleliftdepth=2
c --prbsimplemaxeff=200000000
c --prbsimplemineff=2000000
c --prbsimplereleff=40
c --prbsimplertc=0
c --probe=1
c --promote=1
c --promotegluelim=8
c --pure=1
c --quatres=1
c --quatreswait=2
c --queuesort=1
c --queuesortjwh=0
c --randec=0
c --randecint=1000
c --redcls=1
c --redclsglue=6
c --redclsmaxdec=5
c --redclsmaxdepth=10
c --redclsmaxlrg=10
c --redclsmaxprops=100
c --redclsatlimlo=0
c --redclsatlimhi=100
c --redclsize=30
c --redclstype=4
c --reducefixed=0
c --reduceinc=1000
c --reduceinit=50000
c --reduce=1
c --restart=4
c --restartglcint=10
c --restartglclim=115
c --restartinit=0
c --restartint=5
c --restartpen=1
c --retirenb=1
c --retireint=4
c --retiremin=1
c --reusetrail=0
c --rmincpen=4
c --rstinoutinc=110
c --satlimdelay=10000
c --scincinc=200
c --scincincsatlimhi=100
c --scincincdelta=10
c --scincincincint=100000
c --scincincmin=200
c --scincincmode=1
c --score=5
c --scoreshift=0
c --scoreresetint=2147483647
c --seed=0
c --simpbintinc=100
c --simpbintinclim=10000
c --simpcintdelay=2000
c --simpcintinc=20000
c --simpcintincdiv=1
c --simpcintmaxhard=10000000
c --simpcintmaxsoft=1000000
c --simpincdelmaxfact=50
c --simpincdelmaxmin=10000
c --simpinitdelay=0
c --simpintsizepen=0
c --simpen=0
c --simpidiv=3
c --simpiscale=100
c --simpitdelay=10
c --simpitintinc=10
c --simpitintinclim=1000
c --simplify=2
c --simprtc=5
c --simptintinc=1000
c --simptintinclim=10000
c --simpvarchg=100
c --simpvarlim=100
c --sizemaxpen=5
c --sizepen=1000000
c --sleeponabort=0
c --smallirr=90
c --smallve=1
c --smallvevars=10
c --smallvewait=0
c --sortlits=0
c --subl=9
c --sweep=1
c --sweepboost=10
c --sweepboostdel=4
c --sweepboostint=7
c --sweepboostvlim=1000000
c --sweepfacdec=10
c --sweepforgive=2
c --sweepirr=3
c --sweepmaxeff=200000000
c --sweepmaxdec=10000
c --sweepmaxround=3
c --sweepmindec=100
c --sweepmineff=1000000
c --sweepred=3
c --sweepreleff=3
c --sweeprtc=0
c --sweeprtcint=14
c --sweeprtcintvlim=100000
c --sweepsuccessmaxwortc=6
c --sweepsuccessrat=1000
c --sweepwait=2
c --synclsall=1
c --synclsglue=8
c --synclsint=100
c --synclslen=40
c --syncunint=111111
c --termint=122222
c --ternres=1
c --ternresboost=5
c --ternresrtc=0
c --ternreswait=2
c --transred=1
c --transredwait=2
c --trapiflush=0
c --trdmaxeff=2000000
c --trdmineff=100000
c --trdreleff=10
c --treelook=1
c --treelookboost=10
c --treelookfull=0
c --treelookmaxeff=50000000
c --treelookmineff=300000
c --treelookreleff=2
c --treelookrtc=0
c --trep=1
c --trepint=55555
c --trnreleff=10
c --trnrmaxeff=200000000
c --trnrmineff=4000000
c --unhdatrn=2
c --unhdextstamp=1
c --unhdhbr=0
c --unhdlnpr=3
c --unhdmaxeff=20000000
c --unhdmineff=100000
c --unhdreleff=2
c --unhdroundlim=20
c --unhide=1
c --unhidewait=0
c --usedtwice=1
c --vsidsdint=256
c --wait=1
c --waitmax=4
c --witness=0
c --check=0
c --log=-1
c --profile=1
c --profilelong=1
c --verbose=1
c [freezer] frozen 0 variables out of 13017 free variables 0%
c [limits] no decision limit
c [limits] no conflict limit
c [limits] no propagation limit
c [limits] simplification not delayed since 'simpdelay' zero
c [set-maximum-score] maximum score limit 1.000000d+500
c [set-minimum-score] minimum score limit 1.000000d-500
c [score-type] EVSIDS (--score=5)
c [set-score-increment-1] factor 1.200000d+00 (200/1000) after 0 conflicts
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c *    0.0   13017   308391         0       0      0     0    0     0   17   0%      0    0    0    0    0%
c 
c [simplification-1] limit 0 conflicts (hard 0) hit after 0 conflicts
c [card-1] limit 2000000 penalty 0 = 0 + 0
c [card-1] found 3 at-most-one constraints of average size 3.0
c [card-1] found 6 at-most-two constraints of average size 4.0
c [card-1] using previous limit 2000000 for elimination
c [card-1] 9 out of 9 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 427 variables
c [simpleprobe-1] all 12981 free variables schedulable
c [simpleprobe-1] boosting simple probing limit by 10
c [simpleprobe-1] limit 20000000 penalty 0 = 0 + 0
c [decomp-2] removed 13 variables
c [simpleprobe-1] 4964 variables remain 38% (8004 retained 62%)
c [simpleprobe-1] removed 13 variables, found 4 hbrs, 5 units
c [unhide-1] limit 100000 with penalty 0 = 0 + 0
c [unhide-1-1] 0 units, 8 failed, 801 tauts, 0 hbrs, 17 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 12965 variables 100%
c [elim-1] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-1] rescheduling of touched variables disabled
c [elim-1-1] eliminated 445 variables 3% in round 1 in 2103518 steps
c [elim-1-1] backward subsumption/strengthening limit 2103500
c [elim-1-1-1] backward checking 2323 touched variables 18%
c [elim-1-1-1] fully completed backward checking in 1 rounds
c [elim-1-1] subsumed 9 and strengthened 114 clauses in 1448421 steps
c [elim-1-1] rescheduled 185 variables 1% by backward subsumption
c [elim-1-2] eliminated 2 variables 0% in round 2 in 46722 steps
c [elim-1-2] backward subsumption/strengthening limit 46700
c [elim-1-2-1] backward checking 19 touched variables 0%
c [elim-1-2-1] incomplete backward checking 0 remain 0%
c [elim-1-2] subsumed 0 and strengthened 0 clauses in 46701 steps
c [elim-1-2] fully rescheduled 12517 variables 97%
c [elim-1-3] no variable eliminated in round 3 in 1623135 steps
c [elim-1] fully completed in 3 rounds
c [elim-1] transition to [ all 0 rem 0 ] state
c [elim-1] eliminated 448 = 3% variables out of 12965 scheduled
c [phase-count-1] 301755 negative 99.5% of 303227 except 1472 0.5%
c [phase-count-1] 299629 positive 98.8% of 303227 except 3598 1.2%
c [phase-count-1] less non-negative clauses 1472 than limit 30300 (10.0%)
c [phase-count-1] non-pos/non-neg = 3598/1472 = 2.44 >= 2.00 = 200/100
c [lucky-phase-1] forcing lucky phase -1
c [phase-1] phase bias: 0 positive 0%, 12517 negative 100%
c [sort-queue-1] sorted 12517 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 12517 (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 498 variables 3.8% (12517 remain 96%)
c [simplification-1] removed 5164 irredundant clauses 1.7% (303227 remain 98%)
c [simplification-1] maximum reduction of 4% = max (4%, 2%)
c [simplification-1] geometric conflict interval increment 4000 = 20000 / 5
c [simplification-1] new conflict interval 4000
c [simplification-1] penalized conflict interval 4000 = 1 * 4000
c [simplification-1] hard conflict limit 14000 (soft 4000 + delta 10000)
c [simplification-1] new conflict limit 4000 (hard 14000)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i    1.6   12516   303226       929     709     60    10    2    75   25   2%      5   74    8    0 6913%
c i    1.9   12515   303226      3847    2967    204    36    4   163   25   2%     30  158    6    0 1769%
c 
c [simplification-2] limit 4000 conflicts (hard 14000) hit after 4000 conflicts
c [decomp-3] removed 7 variables
c [simpleprobe-2] 4789 schedulable variables 38%
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [simpleprobe-2] 4791 variables remain 38% (7719 retained 62%)
c [simpleprobe-2] removed 0 variables, found 3 hbrs, 0 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 5977 literals 24%
c [treelook-1] scheduling used 300018 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 300078 steps
c [treelook-1] 5000 literals remain 20%
c [treelook-1] 4959 variables remain to probed next time 40%
c [treelook-1] removed 0 variables, found 1 hbrs
c [basicprobe-1] limit 2425512 based on 303189 irredundant clauses
c [basicprobe-1-0] 539 sched 4%, 3 failed, 0 lifted, 42 hbrs
c [decomp-6] removed 5 variables
c [basicprobe-1-1] 547 sched 4%, 0 failed, 0 lifted, 1 hbrs
c [basicprobe-1-2] 547 sched 4%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-1-2] fully completed probing
c [basicprobe-1-2] 3 units = 3 failed (100%) + 0 lifted (0%)
c [basicprobe-1-2] removed 5 variables, found 43 hbrs
c [unhide-2] limit 100000 with penalty 0 = 0 + 0
c [unhide-2-2] 0 units, 0 failed, 26 tauts, 0 hbrs, 118 literals
c [block-1] scheduling all variables this time
c [block-1] scheduled 12505 variables 100%
c [block-1] boosting limit by 10
c [block-1] limit of 500000000 steps penalty 0 = 0 + 0
c [block-1] fully completed
c [block-1] transition to [ all 0 rem 0 ] state
c [block-1] eliminated 525 blocked clauses
c [block-1] 525 < 1/100 * 303148 = 3031 considered unsuccessful
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 8087 clauses out of 104219 (8%) of length 7
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 8087 large clauses in 30000081 steps
c [cce-1-1] allowing another 15000040 steps for small clauses
c [cce-1-1] scheduling 10815 clauses = 334 binary + 10481 ternary
c [cce-1-1] tried to eliminate 10815 small clauses 100%
c [cce-1-1] eliminated 14 binary clauses 4%
c [cce-1-1] eliminated 1046 ternary clauses 10%
c [cce-1-1] eliminated 1060 small clauses 10%
c [cce-1-1] eliminated 1060 small clauses in 19023087 steps
c [cce-1-1] completed small round (ATE)
c [cce-1-1] eliminated 9147 covered clauses in round 1
c [cce-1-2] incomplete large round (ATE)
c [cce-1-2] allowing another 5488458 steps for small clauses
c [cce-1-2] scheduling 9755 clauses = 320 binary + 9435 ternary
c [cce-1-2] tried to eliminate 9755 small clauses 100%
c [cce-1-2] completed small round (ATE)
c [cce-1-2] eliminated 0 covered clauses in round 2
c [cce-1] eliminated 9147 covered clauses in TOTAL during 2 rounds
c [elim-2] scheduling all variables this time
c [elim-2] scheduled 12505 variables 100%
c [elim-2] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-2] rescheduling of touched variables disabled
c [elim-2] incomplete 9388 not tried 75% in round 1
c [elim-2] transition to [ all 1 rem 1 ] state
c [elim-2] eliminated 78 = 1% variables out of 12505 scheduled
c [elim-2] 78 < 1/100 * 12505 = 125 considered unsuccessful
c [bca-1] limit of 10000000 steps and 566312 added (scaled 2)
c [bca-1] 20337 out of 24856 literals actually usable 82%
c [bca-1] added 0 blocked clauses in 193244 steps
c [sweep-1] limit 1000000 penalty 0 = 0 + 0
c [sweep-1-1] 2993 pos 24.1% + 9434 neg 75.9% = 12427 sched 100.0% ret 0
c [sweep-1-1] 1000836 steps 405 queries 2610.78 avg class size
c [sweep-1-1] 8855 decisions 404 SAT calls 29.10 avg env size
c [sweep-1-1] 9725 variables remain 78% (2702 retained 22%)
c [decomp-8] removed 1 variables
c [sweep-1-1] removed 1 vars (0 failed, 1 eqs, 2 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 1 vars in TOTAL (1 rounds, 404 queries)
c [sort-queue-2] sorted 8785 enqueued variables after 4000 conflicts
c [score-dist-2] active 3641 (29%), one 853 (7%), zero 7932 (64%)
c [score-dist-2] max exp 552, different 344 (62%)
c [score-dist-2] median active exp 443, avg 416.2
c [simplification-2] removed 89 variables 0.7% (12426 remain 95%)
c [simplification-2] removed 20323 irredundant clauses 6.7% (282903 remain 92%)
c [simplification-2] maximum reduction of 7% = max (1%, 7%)
c [simplification-2] large reduction 7% >= 5% limit
c [simplification-2] next conflict interval 2000 = 2000/1
c [simplification-2] penalized conflict interval 2000 = 1 * 2000
c [simplification-2] hard conflict limit 16000 (soft 6000 + delta 10000)
c [simplification-2] new conflict limit 6000 (hard 16000)
c 
c [simplification-3] limit 6000 conflicts (hard 16000) hit after 6000 conflicts
c [quatres-1] found 34832 quaternary clauses 13% in total
c [quatres-1-1] added 23 double-self-subsuming ternary resolvents
c [quatres-1-2] added 133 single-self-subsuming ternary resolvents
c [quatres-1-2] added 251 quaternary resolvents
c [ternres-1] boosting ternary resolution limit by 5
c [ternres-1] limit 20000000 with penalty 0 = 0 + 0
c [ternres-1] all 12426 free variables schedulable
c [ternres-1] 178 ternary resolvents (10 bin, 168 trn)
c [ternres-1] fully completed ternary resolution
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] found 9 at-most-two constraints of average size 4.1
c [card-2] using previous limit 1000000 for elimination
c [card-2] 11 out of 11 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 1077 xors of average arity 4.8
c [gauss-1] connected 5199 occurrences of 329 variables (average 15.8)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] fully completed
c [gauss-1] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-9] removed 1 variables
c [transred-1] limit 282898 based on 282898 irredundant clauses
c [transred-1] removed 4 transitive binary clauses
c [cce-2] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-2-1] eliminated 191 clauses out of 89711 (0%) of length 7
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] eliminated 191 large clauses in 30000134 steps
c [cce-2-1] allowing another 15000067 steps for small clauses
c [cce-2-1] scheduling 9773 clauses = 321 binary + 9452 ternary
c [cce-2-1] tried to eliminate 9773 small clauses 100%
c [cce-2-1] eliminated 2 binary clauses 1%
c [cce-2-1] eliminated 12 ternary clauses 0%
c [cce-2-1] eliminated 14 small clauses 0%
c [cce-2-1] eliminated 14 small clauses in 18420163 steps
c [cce-2-1] completed small round (ATE)
c [cce-2-1] eliminated 205 covered clauses in round 1
c [cce-2-2] incomplete large round (ATE)
c [cce-2-2] allowing another 5789954 steps for small clauses
c [cce-2-2] scheduling 9759 clauses = 319 binary + 9440 ternary
c [cce-2-2] tried to eliminate 9759 small clauses 100%
c [cce-2-2] completed small round (ATE)
c [cce-2-2] eliminated 0 covered clauses in round 2
c [cce-2] eliminated 205 covered clauses in TOTAL during 2 rounds
c [cce-2] 205 < 1/100 * 282898 = 2828 considered unsuccessful
c [sweep-2] limit 1000000 penalty 0 = 0 + 0
c [sweep-2-1] 2533 pos 26.0% + 7192 neg 74.0% = 9725 sched 78.3% ret 2700
c [sweep-2-1] 1001240 steps 463 queries 1674.43 avg class size
c [sweep-2-1] 10177 decisions 463 SAT calls 28.80 avg env size
c [sweep-2-1] 7139 variables remain 57% (5286 retained 43%)
c [sweep-2-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 0 vars in TOTAL (1 rounds, 462 queries)
c [sort-queue-3] sorted 7630 enqueued variables after 6000 conflicts
c [score-dist-3] active 4795 (39%), one 1615 (13%), zero 6015 (48%)
c [score-dist-3] max exp 729, different 454 (62%)
c [score-dist-3] median active exp 547, avg 482.9
c [simplification-3] removed 1 variables 0.0% (12425 remain 95%)
c [simplification-3] removed 210 irredundant clauses 0.1% (282693 remain 92%)
c [simplification-3] maximum reduction of 0% = max (0%, 0%)
c [simplification-3] full geometric conflict interval increment 20000
c [simplification-3] new conflict interval 24000
c [simplification-3] penalized conflict interval 24000 = 1 * 24000
c [simplification-3] hard conflict limit 42000 (soft 30000 + delta 12000)
c [simplification-3] new conflict limit 30000 (hard 42000)
c 
c [simplification-4] limit 30000 conflicts (hard 42000) hit after 30001 conflicts
c [quatres-2] found 36493 quaternary clauses 13% in total
c [quatres-2-1] added 71 double-self-subsuming ternary resolvents
c [quatres-2-2] added 182 single-self-subsuming ternary resolvents
c [quatres-2-2] added 196 quaternary resolvents
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] all 12425 free variables schedulable
c [ternres-2] 10 ternary resolvents (1 bin, 9 trn)
c [ternres-2] fully completed ternary resolution
c [treelook-2] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-2] scheduled 1946 literals 8%
c [treelook-2] scheduling used 150025 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-2] used 150202 steps
c [treelook-2] 1413 literals remain 6%
c [treelook-2] 1409 variables remain to probed next time 11%
c [treelook-2] removed 0 variables, found 1 hbrs
c [unhide-3] limit 70539 with penalty 1 = 1 + 0
c [unhide-3-3] 0 units, 0 failed, 31 tauts, 0 hbrs, 100 literals
c [transred-2] limit 705390 with penalty 0 = 0 + 0
c [transred-2] removed 5 transitive binary clauses
c [block-2] scheduling all variables this time
c [block-2] scheduled 12425 variables 100%
c [block-2] limit of 25000000 steps penalty 1 = 1 + 0
c [block-2] fully completed
c [block-2] transition to [ all 0 rem 0 ] state
c [block-2] eliminated 0 blocked clauses
c [elim-3] 9388 variables 76% will be scheduled this time
c [elim-3] scheduled 9388 variables 76%
c [elim-3] limit of 10000000 steps penalty 1 = 1 + 0
c [elim-3] rescheduling of touched variables disabled
c [elim-3] incomplete 8320 not tried 67% in round 1
c [elim-3] transition to [ all 0 rem 1 ] state
c [elim-3] eliminated 0 = 0% variables out of 9388 scheduled
c [bca-2] limit of 10000000 steps and 557674 added (scaled 2)
c [bca-2] 11711 out of 24852 literals actually usable 47%
c [bca-2] added 0 blocked clauses in 132168 steps
c [sweep-3] limit 1000000 penalty 0 = 0 + 0
c [sweep-3-1] 2324 pos 32.6% + 4815 neg 67.4% = 7139 sched 57.5% ret 5286
c [sweep-3-1] 1001421 steps 533 queries 1124.94 avg class size
c [sweep-3-1] 14635 decisions 532 SAT calls 34.71 avg env size
c [sweep-3-1] 4588 variables remain 37% (7837 retained 63%)
c [sweep-3-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 0 vars in TOTAL (1 rounds, 532 queries)
c [sort-queue-4] sorted 8644 enqueued variables after 30001 conflicts
c [score-dist-4] active 3781 (30%), one 4991 (40%), zero 3653 (29%)
c [score-dist-4] max exp 653, different 373 (57%)
c [score-dist-4] median active exp 530, avg 509.7
c [simplification-4] removed 0 variables 0.0% (12425 remain 95%)
c [simplification-4] removed 4106 irredundant clauses 1.5% (278587 remain 90%)
c [simplification-4] maximum reduction of 1% = max (0%, 1%)
c [simplification-4] geometric conflict interval increment 12000 = 24000 / 2
c [simplification-4] new conflict interval 36000
c [simplification-4] penalized conflict interval 36000 = 1 * 36000
c [simplification-4] hard conflict limit 84001 (soft 66001 + delta 18000)
c [simplification-4] new conflict limit 66001 (hard 84001)
c 
c [simplification-5] limit 66001 conflicts (hard 84001) hit after 66001 conflicts
c [quatres-3] found 38164 quaternary clauses 13% in total
c [quatres-3-1] added 51 double-self-subsuming ternary resolvents
c [quatres-3-2] added 243 single-self-subsuming ternary resolvents
c [quatres-3-2] added 270 quaternary resolvents
c [ternres-3] limit 4000000 with penalty 0 = 0 + 0
c [ternres-3] all 12425 free variables schedulable
c [ternres-3] 7 ternary resolvents (1 bin, 6 trn)
c [ternres-3] fully completed ternary resolution
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] extracted 40 xors of average arity 3.0
c [gauss-2] connected 120 occurrences of 21 variables (average 5.7)
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] fully completed
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [basicprobe-2] limit 10114149 penalty 0 = 0 + 0
c [basicprobe-2-0] 633 sched 5%, 0 failed, 0 lifted, 14 hbrs
c [basicprobe-2-1] 642 sched 5%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-2-1] fully completed probing
c [basicprobe-2-1] removed 0 variables, found 14 hbrs
c [bate-1] eliminated 7 asymmetric tautologies during probing
c [transred-3] limit 2000000 with penalty 0 = 0 + 0
c [transred-3] removed 4 transitive binary clauses
c [cce-3] limit of 15000000 steps penalty 1 = 1 + 0
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] allowing another 7500043 steps for small clauses
c [cce-3-1] scheduling 9863 clauses = 328 binary + 9535 ternary
c [cce-3-1] tried to eliminate 9863 small clauses 100%
c [cce-3-1] eliminated 5 ternary clauses 0%
c [cce-3-1] eliminated 5 small clauses 0%
c [cce-3-1] eliminated 5 small clauses in 11565432 steps
c [cce-3-1] completed small round (ACCE)
c [cce-3-1] eliminated 5 covered clauses in round 1
c [cce-3-2] incomplete large round (ACCE)
c [cce-3-2] allowing another 1717284 steps for small clauses
c [cce-3-2] scheduling 9858 clauses = 328 binary + 9530 ternary
c [cce-3-2] tried to eliminate 4054 small clauses 41%
c [cce-3-2] incomplete small round (ACCE)
c [cce-3-2] eliminated 0 covered clauses in round 2
c [cce-3] eliminated 5 covered clauses in TOTAL during 2 rounds
c [cce-3] 5 < 1/100 * 278580 = 2785 considered unsuccessful
c [sweep-4] limit 1000000 penalty 0 = 0 + 0
c [sweep-4-1] 1647 pos 35.9% + 2941 neg 64.1% = 4588 sched 36.9% ret 7837
c [sweep-4-1] 1001172 steps 644 queries 622.03 avg class size
c [sweep-4-1] 14513 decisions 643 SAT calls 30.11 avg env size
c [sweep-4-1] 2241 variables remain 18% (10184 retained 82%)
c [sweep-4-1] removed 0 vars (0 failed, 0 eqs, 1 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 0 vars in TOTAL (1 rounds, 643 queries)
c [sort-queue-5] sorted 7559 enqueued variables after 66001 conflicts
c [score-dist-5] active 4866 (39%), one 5583 (45%), zero 1976 (16%)
c [score-dist-5] max exp 978, different 479 (49%)
c [score-dist-5] median active exp 806, avg 772.3
c [simplification-5] removed 0 variables 0.0% (12425 remain 95%)
c [simplification-5] removed 12 irredundant clauses 0.0% (278575 remain 90%)
c [simplification-5] maximum reduction of 0% = max (0%, 0%)
c [simplification-5] full geometric conflict interval increment 36000
c [simplification-5] new conflict interval 72000
c [simplification-5] penalized conflict interval 72000 = 1 * 72000
c [simplification-5] hard conflict limit 174001 (soft 138001 + delta 36000)
c [simplification-5] new conflict limit 138001 (hard 174001)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c -   22.0   12425   278575     82525   25456   3306   175    7   477   27   1%    711  211    7    5  135%
c 
c [simplification-6] limit 138001 conflicts (hard 174001) hit after 138001 conflicts
c [quatres-4] found 42939 quaternary clauses 14% in total
c [quatres-4-1] removed 1 duplicate quaternary clauses
c [quatres-4-1] added 101 double-self-subsuming ternary resolvents
c [quatres-4-2] added 490 single-self-subsuming ternary resolvents
c [quatres-4-2] added 536 quaternary resolvents
c [ternres-4] limit 5541070 with penalty 0 = 0 + 0
c [ternres-4] all 12425 free variables schedulable
c [ternres-4] 11 ternary resolvents (5 bin, 6 trn)
c [ternres-4] fully completed ternary resolution
c [card-3] limit 692633 penalty 2 = 2 + 0
c [card-3] found 2 at-most-one constraints of average size 3.0
c [card-3] found 9 at-most-two constraints of average size 4.1
c [card-3] using previous limit 692633 for elimination
c [card-3] 11 out of 11 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 1 transitive binary clauses
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 16623210 penalty 0 = 0 + 0
c [sweep-5-1] 925 pos 41.3% + 1316 neg 58.7% = 2241 sched 18.0% ret 10184
c [sweep-5-1] 909626 steps 852 queries 177.26 avg class size
c [sweep-5-1] 19229 decisions 851 SAT calls 29.90 avg env size
c [sweep-5-1] fully completed sweeping round
c [sweep-5-1] removed 0 vars (0 failed, 0 eqs, 1 impls)
c [sweep-5-2] 5792 pos 46.6% + 6633 neg 53.4% = 12425 sched 100.0% ret 0
c [sweep-5-2] 3532349 steps 1802 queries 538.27 avg class size
c [sweep-5-2] 45375 decisions 1801 SAT calls 37.16 avg env size
c [sweep-5-2] fully completed sweeping round
c [sweep-5-2] removed 0 vars (0 failed, 0 eqs, 1 impls)
c [sweep-5-3] 5792 pos 46.6% + 6633 neg 53.4% = 12425 sched 100.0% ret 0
c [sweep-5-3] 3474259 steps 1747 queries 530.01 avg class size
c [sweep-5-3] 44628 decisions 1746 SAT calls 37.87 avg env size
c [sweep-5-3] fully completed sweeping round
c [sweep-5-3] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-5] removed 0 vars in TOTAL (3 rounds, 4398 queries)
c [sort-queue-6] sorted 4034 enqueued variables after 138001 conflicts
c [score-dist-6] active 8391 (68%), one 3843 (31%), zero 191 (2%)
c [score-dist-6] max exp 907, different 769 (85%)
c [score-dist-6] median active exp 601, avg 556.7
c [simplification-6] removed 0 variables 0.0% (12425 remain 95%)
c [simplification-6] removed 0 irredundant clauses 0.0% (278575 remain 90%)
c [simplification-6] maximum reduction of 0% = max (0%, 0%)
c [simplification-6] full geometric conflict interval increment 72000
c [simplification-6] new conflict interval 144000
c [simplification-6] penalized conflict interval 144000 = 1 * 144000
c [simplification-6] hard conflict limit 354001 (soft 282001 + delta 72000)
c [simplification-6] new conflict limit 282001 (hard 354001)
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 -   36.8   12425   278575    157110   44832   5097   234    8   352   28   2%    924  -45    9    7  119%
c -   47.1   12425   278575    231277   60470   5724   265   13   376   29   4%    992   -4   12   10  124%
c 
c [simplification-7] limit 282001 conflicts (hard 354001) hit after 282001 conflicts
c [quatres-5] found 48963 quaternary clauses 15% in total
c [quatres-5-1] added 100 double-self-subsuming ternary resolvents
c [quatres-5-2] added 592 single-self-subsuming ternary resolvents
c [quatres-5-2] added 518 quaternary resolvents
c [ternres-5] limit 9608522 with penalty 0 = 0 + 0
c [ternres-5] all 12425 free variables schedulable
c [ternres-5] 41 ternary resolvents (5 bin, 36 trn)
c [ternres-5] fully completed ternary resolution
c [simpleprobe-3] 4751 schedulable variables 38%
c [simpleprobe-3] limit 19217044 penalty 1 = 1 + 0
c [simpleprobe-3] 2491 variables remain 20% (9934 retained 80%)
c [simpleprobe-3] removed 0 variables, found 16 hbrs, 0 units
c [unhide-4] limit 480426 with penalty 2 = 2 + 0
c [unhide-4-4] 0 units, 0 failed, 137 tauts, 0 hbrs, 337 literals
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 5 transitive binary clauses
c [block-3] scheduling all variables this time
c [block-3] scheduled 12425 variables 100%
c [block-3] limit of 24021305 steps penalty 2 = 2 + 0
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 1 blocked clauses
c [block-3] 1 < 1/100 * 278575 = 2785 considered unsuccessful
c [elim-4] scheduling all variables this time
c [elim-4] scheduled 12425 variables 100%
c [elim-4] boosting limit by 20
c [elim-4] limit of 960852235 steps penalty 2 = 2 + 0
c [elim-4] rescheduling of touched variables disabled
c [elim-4-1] eliminated 2 variables 0% in round 1 in 248967474 steps
c [elim-4-1] backward subsumption/strengthening limit 248967400
c [elim-4-1-1] backward checking 10384 touched variables 84%
c [elim-4-1-1] fully completed backward checking in 1 rounds
c [elim-4-1] subsumed 2 and strengthened 4 clauses in 4067932 steps
c [elim-4-1] rescheduled 10 variables 0% by backward subsumption
c [elim-4-2] no variable eliminated in round 2 in 41079 steps
c [elim-4] fully completed in 2 rounds
c [elim-4] transition to [ all 0 rem 0 ] state
c [elim-4] eliminated 2 = 0% variables out of 12425 scheduled
c [elim-4] 2 < 1/100 * 12425 = 124 considered unsuccessful
c [bca-3] limit of 10000000 steps and 550450 added (scaled 2)
c [bca-3] 3196 out of 24848 literals actually usable 13%
c [bca-3] added 0 blocked clauses in 128793 steps
c [sort-queue-7] sorted 8113 enqueued variables after 282001 conflicts
c [score-dist-7] active 4310 (35%), one 7998 (64%), zero 115 (1%)
c [score-dist-7] max exp 755, different 398 (53%)
c [score-dist-7] median active exp 657, avg 577.5
c [simplification-7] removed 2 variables 0.0% (12423 remain 95%)
c [simplification-7] removed 3600 irredundant clauses 1.3% (274975 remain 89%)
c [simplification-7] maximum reduction of 1% = max (0%, 1%)
c [simplification-7] geometric conflict interval increment 72000 = 144000 / 2
c [simplification-7] new conflict interval 216000
c [simplification-7] penalized conflict interval 216000 = 1 * 216000
c [simplification-7] hard conflict limit 606001 (soft 498001 + delta 108000)
c [simplification-7] new conflict limit 498001 (hard 606001)
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 -   60.1   12423   274975    296017   67602   6539   289   13   533   30   2%   1012  114   13   12  107%
c -   67.5   12423   274975    362270   80102   6816   294   12   611   31   2%   1020   76   14   12  116%
c -   76.4   12423   274975    431188   95195   7302   295   13   572   32   2%   1022  -10   14   12  117%
c -   83.4   12423   274975    499615  104030   7768   309   15   464   33   3%   1023  -95   15   13  115%
c 
c [simplification-8] limit 498001 conflicts (hard 606001) hit after 506589 conflicts
c [quatres-6] found 59203 quaternary clauses 16% in total
c [quatres-6-1] removed 20 duplicate quaternary clauses
c [quatres-6-1] added 127 double-self-subsuming ternary resolvents
c [quatres-6-2] added 882 single-self-subsuming ternary resolvents
c [quatres-6-2] added 681 quaternary resolvents
c [ternres-6] limit 15899245 with penalty 0 = 0 + 0
c [ternres-6] all 12423 free variables schedulable
c [ternres-6] 39 ternary resolvents (0 bin, 39 trn)
c [ternres-6] fully completed ternary resolution
c [gauss-3] limit 794962 penalty 2 = 2 + 0
c [gauss-3] extracted 21 xors of average arity 3.0
c [gauss-3] connected 63 occurrences of 15 variables (average 4.2)
c [gauss-3] limit 794962 penalty 2 = 2 + 0
c [gauss-3] fully completed
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 7 transitive binary clauses
c [cce-4] boosting limit by 10
c [cce-4] limit of 198740562 steps penalty 2 = 2 + 0
c [cce-4-1] eliminated 77 clauses out of 77851 (0%) of length 7
c [cce-4-1] eliminated 956 clauses out of 91766 (1%) of length 6
c [cce-4-1] eliminated 6186 clauses out of 61056 (10%) of length 5
c [cce-4-1] eliminated 333 clauses out of 33324 (1%) of length 4
c [cce-4-1] completed large round (ATE)
c [cce-4-1] eliminated 7552 large clauses in 155619840 steps
c [cce-4-1] allowing another 77809920 steps for small clauses
c [cce-4-1] scheduling 9993 clauses = 343 binary + 9650 ternary
c [cce-4-1] tried to eliminate 9993 small clauses 100%
c [cce-4-1] eliminated 2 binary clauses 1%
c [cce-4-1] eliminated 5 ternary clauses 0%
c [cce-4-1] eliminated 7 small clauses 0%
c [cce-4-1] eliminated 7 small clauses in 81144444 steps
c [cce-4-1] completed small round (ATE)
c [cce-4-1] completed small and large (ATE)
c [cce-4-1] eliminated 7559 covered clauses in round 1
c [cce-4-2] incomplete large round (ATE)
c [cce-4-2] allowing another 58798062 steps for small clauses
c [cce-4-2] scheduling 9986 clauses = 341 binary + 9645 ternary
c [cce-4-2] tried to eliminate 9986 small clauses 100%
c [cce-4-2] completed small round (ATE)
c [cce-4-2] eliminated 0 covered clauses in round 2
c [cce-4] eliminated 7559 covered clauses in TOTAL during 2 rounds
c [sweep-6] limit 2384886 penalty 1 = 1 + 0
c [sweep-6-1] 6128 pos 49.3% + 6295 neg 50.7% = 12423 sched 100.0% ret 0
c [sweep-6-1] 2385062 steps 747 queries 1087.22 avg class size
c [sweep-6-1] 22396 decisions 746 SAT calls 42.53 avg env size
c [sweep-6-1] 4969 variables remain 40% (7454 retained 60%)
c [sweep-6-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-6] removed 0 vars in TOTAL (1 rounds, 746 queries)
c [sort-queue-8] sorted 5705 enqueued variables after 506589 conflicts
c [score-dist-8] active 6718 (54%), one 5655 (46%), zero 50 (0%)
c [score-dist-8] max exp 845, different 495 (59%)
c [score-dist-8] median active exp 676, avg 630.6
c [simplification-8] removed 0 variables 0.0% (12423 remain 95%)
c [simplification-8] removed 7559 irredundant clauses 2.7% (267416 remain 87%)
c [simplification-8] maximum reduction of 3% = max (0%, 3%)
c [simplification-8] geometric conflict interval increment 54000 = 216000 / 4
c [simplification-8] new conflict interval 270000
c [simplification-8] penalized conflict interval 270000 = 1 * 270000
c [simplification-8] hard conflict limit 911589 (soft 776589 + delta 135000)
c [simplification-8] new conflict limit 776589 (hard 911589)
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 -   94.1   12423   267416    574501  121240   9424   311   13   490   34   3%   1024  -44   14   12  116%
c -  102.7   12423   267416    642892  130084   9762   312   14   537   34   3%   1024  -11   11   13   81%
c -  108.1   12423   267416    711021  146363   9872   312   16   567   35   3%   1024   34   17   15  113%
c -  111.3   12423   267416    759797  155315   9919   312   13   687   36   2%   1024   98   15   15  100%
c 
c [simplification-9] limit 776589 conflicts (hard 911589) hit after 776589 conflicts
c [quatres-7] found 66857 quaternary clauses 17% in total
c [quatres-7-1] removed 6 duplicate quaternary clauses
c [quatres-7-1] added 115 double-self-subsuming ternary resolvents
c [quatres-7-2] added 910 single-self-subsuming ternary resolvents
c [quatres-7-2] added 628 quaternary resolvents
c [ternres-7] limit 21795239 with penalty 0 = 0 + 0
c [ternres-7] all 12423 free variables schedulable
c [ternres-7] 31 ternary resolvents (0 bin, 31 trn)
c [ternres-7] fully completed ternary resolution
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 1 transitive binary clauses
c [sort-queue-9] sorted 10778 enqueued variables after 776589 conflicts
c [score-dist-9] active 1645 (13%), one 10772 (87%), zero 6 (0%)
c [score-dist-9] max exp 846, different 77 (9%)
c [score-dist-9] median active exp 543, avg 574.7
c [simplification-9] removed 0 variables 0.0% (12423 remain 95%)
c [simplification-9] removed 0 irredundant clauses 0.0% (267416 remain 87%)
c [simplification-9] maximum reduction of 0% = max (0%, 0%)
c [simplification-9] full geometric conflict interval increment 270000
c [simplification-9] new conflict interval 540000
c [simplification-9] penalized conflict interval 540000 = 1 * 540000
c [simplification-9] hard conflict limit 1586589 (soft 1316589 + delta 270000)
c [simplification-9] new conflict limit 1316589 (hard 1586589)
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 -  116.8   12423   267416    803897  153751  10948   312   15   613   36   2%   1024  -13   15   15  100%
c -  123.7   12423   267416    863628  153820  11311   315   14   642   36   2%   1024   61   13   14   89%
c -  132.1   12423   267416    937376  164119  11650   316   14   550   37   3%   1024  -45   16   14  109%
c -  141.4   12423   267416   1009026  173718  11793   316   16   688   38   2%   1024   88   17   15  111%
c -  150.9   12423   267416   1079425  180727  11910   317   17   608   38   3%   1024  -28   18   16  111%
c -  159.6   12423   267416   1148439  190403  12023   317   17   778   39   2%   1024  115   19   17  115%
c -  164.1   12423   267416   1211917  203654  12091   318   17   681   40   3%   1024  -13   19   17  112%
c -  167.5   12423   267416   1261935  209648  12138   318   14   852   40   2%   1024  121   14   16   85%
c -  170.7   12423   267416   1308365  209539  12191   320   16   792   41   2%   1024   12   16   16  101%
c -  179.2   12423   267416   1363445  200459  12403   320   17   618   40   3%   1024  -58   17   16  108%
c -  192.0   12423   267416   1442959  209672  12730   321   17   546   41   3%   1024  -38   13   16   83%
c 
c [simplification-10] limit 1316589 conflicts (hard 1586589) hit after 1451935 conflicts
c [quatres-8] found 86577 quaternary clauses 19% in total
c [quatres-8-1] removed 52 duplicate quaternary clauses
c [quatres-8-1] added 93 double-self-subsuming ternary resolvents
c [quatres-8-2] added 1212 single-self-subsuming ternary resolvents
c [quatres-8-2] added 408 quaternary resolvents
c [ternres-8] limit 41228510 with penalty 0 = 0 + 0
c [ternres-8] all 12423 free variables schedulable
c [ternres-8] 10 ternary resolvents (1 bin, 9 trn)
c [ternres-8] fully completed ternary resolution
c [card-4] limit 2576781 penalty 3 = 3 + 0
c [card-4] found 1 at-most-one constraints of average size 3.0
c [card-4] found 13 at-most-two constraints of average size 4.0
c [card-4] using previous limit 2576781 for elimination
c [card-4] 14 out of 14 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [treelook-3] limit 1030712 penalty 2 = 2 + 0 boost 1
c [treelook-3] scheduled 2595 literals 10%
c [treelook-3] scheduling used 1030787 steps
c [treelook-3] not fully scheduled
c [treelook-3] limit 1030712 penalty 2 = 2 + 0 boost 1
c [treelook-3] used 760567 steps
c [treelook-3] 0 literals remain 0%
c [treelook-3] 0 variables remain to probed next time 0%
c [treelook-3] removed 0 variables, found 2 hbrs
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 1 transitive binary clauses
c [cce-5] limit of 103071275 steps penalty 1 = 1 + 0
c [cce-5-1] eliminated 4 clauses out of 76885 (0%) of length 7
c [cce-5-1] eliminated 8 clauses out of 91640 (0%) of length 6
c [cce-5-1] incomplete large round (ACCE)
c [cce-5-1] eliminated 12 large clauses in 103071276 steps
c [cce-5-1] allowing another 51535638 steps for small clauses
c [cce-5-1] scheduling 10135 clauses = 347 binary + 9788 ternary
c [cce-5-1] tried to eliminate 10135 small clauses 100%
c [cce-5-1] eliminated 7 ternary clauses 0%
c [cce-5-1] eliminated 7 small clauses 0%
c [cce-5-1] eliminated 7 small clauses in 55384413 steps
c [cce-5-1] completed small round (ACCE)
c [cce-5-1] eliminated 19 covered clauses in round 1
c [cce-5-2] incomplete large round (ACCE)
c [cce-5-2] allowing another 23843481 steps for small clauses
c [cce-5-2] scheduling 10128 clauses = 347 binary + 9781 ternary
c [cce-5-2] tried to eliminate 10128 small clauses 100%
c [cce-5-2] completed small round (ACCE)
c [cce-5-2] eliminated 0 covered clauses in round 2
c [cce-5] eliminated 19 covered clauses in TOTAL during 2 rounds
c [cce-5] 19 < 1/100 * 267416 = 2674 considered unsuccessful
c [sort-queue-10] sorted 521 enqueued variables after 1451935 conflicts
c [score-dist-10] active 11902 (96%), one 521 (4%), zero 0 (0%)
c [score-dist-10] max exp 893, different 294 (33%)
c [score-dist-10] median active exp 790, avg 740.2
c [simplification-10] removed 0 variables 0.0% (12423 remain 95%)
c [simplification-10] removed 19 irredundant clauses 0.0% (267397 remain 87%)
c [simplification-10] maximum reduction of 0% = max (0%, 0%)
c [simplification-10] full geometric conflict interval increment 540000
c [simplification-10] conflict interval soft limit 1000000 reached
c [simplification-10] new conflict interval 1000000
c [simplification-10] penalized conflict interval 1000000 = 1 * 1000000
c [simplification-10] hard conflict limit 2951935 (soft 2451935 + delta 500000)
c [simplification-10] new conflict limit 2451935 (hard 2951935)
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 -  206.9   12423   267397   1523386  220967  14065   323   17   611   42   3%   1024  -34   12   16   75%
c -  216.8   12423   267397   1597940  232497  14104   323   17   609   42   3%   1024  -24   15   17   90%
c -  222.6   12423   267397   1665380  245299  14141   323   17   559   43   3%   1024  -75   21   17  120%
c -  231.9   12423   267397   1722588  240524  14192   323   19   533   43   4%   1024  -73   18   18   98%
c -  236.0   12423   267397   1788290  255738  14208   323   18   614   44   3%   1024   -5   19   18  107%
c -  240.6   12423   267397   1841079  257763  14231   323   19   594   44   3%   1024  -42   20   18  113%
c -  247.3   12423   267397   1894251  253162  14260   323   18   782   44   2%   1024  123   17   18   96%
c -  250.8   12423   267397   1955050  262610  14270   323   17   553   45   3%   1024  -91   12   17   68%
c -  255.0   12423   267397   2009063  263344  14284   323   18   560   45   3%   1024  -48   20   17  117%
c -  260.3   12423   267397   2065752  259655  14312   323   18   541   44   3%   1024  -47   20   17  116%
c -  269.2   12423   267397   2131986  258082  14374   324   19   708   45   3%   1024   71   17   18   94%
c -  277.2   12423   267397   2204865  266525  14423   324   18   609   45   3%   1024  -15   18   18   99%
c -  288.1   12423   267397   2275260  266433  14505   324   19   575   45   3%   1024  -15   16   18   85%
c -  296.9   12423   267397   2350183  276510  14538   324   16   605   45   3%   1024  -16   18   18   99%
c -  303.4   12423   267397   2416459  284773  14555   324   18   563   46   3%   1024  -62   18   18  101%
c -  308.2   12423   267397   2477039  288749  14567   324   16   463   47   4%   1024  -97   18   17  108%
c 
c [simplification-11] limit 2451935 conflicts (hard 2951935) hit after 2487027 conflicts
c [quatres-9] found 98482 quaternary clauses 19% in total
c [quatres-9-1] removed 86 duplicate quaternary clauses
c [quatres-9-1] added 32 double-self-subsuming ternary resolvents
c [quatres-9-2] added 645 single-self-subsuming ternary resolvents
c [quatres-9-2] added 170 quaternary resolvents
c [ternres-9] limit 67640494 with penalty 0 = 0 + 0
c [ternres-9] all 12423 free variables schedulable
c [ternres-9] 8 ternary resolvents (1 bin, 7 trn)
c [ternres-9] fully completed ternary resolution
c [unhide-5] limit 1691012 with penalty 3 = 3 + 0
c [unhide-5-6] 0 units, 0 failed, 61 tauts, 0 hbrs, 454 literals
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 3 transitive binary clauses
c [block-4] scheduling all variables this time
c [block-4] scheduled 12423 variables 100%
c [block-4] limit of 84550618 steps penalty 3 = 3 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 0 blocked clauses
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 12423 variables 100%
c [elim-5] limit of 100000000 steps penalty 3 = 3 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5] incomplete 3255 not tried 26% in round 1
c [elim-5] transition to [ all 1 rem 1 ] state
c [elim-5] eliminated 1 = 0% variables out of 12423 scheduled
c [elim-5] 1 < 1/100 * 12423 = 124 considered unsuccessful
c [bca-4] limit of 10000000 steps and 534940 added (scaled 2)
c [bca-4] 43 out of 24846 literals actually usable 0%
c [bca-4] not enough literals usable
c [bca-4] added 0 blocked clauses in 296874 steps
c [sweep-7] limit 5073037 penalty 2 = 2 + 0
c [sweep-7-1] 2544 pos 51.2% + 2425 neg 48.8% = 4969 sched 40.0% ret 7453
c [sweep-7-1] 3280584 steps 1243 queries 230.88 avg class size
c [sweep-7-1] 36222 decisions 1242 SAT calls 44.56 avg env size
c [sweep-7-1] fully completed sweeping round
c [sweep-7-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-7-2] 6261 pos 50.4% + 6161 neg 49.6% = 12422 sched 100.0% ret 0
c [sweep-7-2] 1795391 steps 350 queries 1296.02 avg class size
c [sweep-7-2] 17325 decisions 349 SAT calls 77.64 avg env size
c [sweep-7-2] 7148 variables remain 58% (5274 retained 42%)
c [sweep-7-2] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-7] removed 0 vars in TOTAL (2 rounds, 1591 queries)
c [sort-queue-11] sorted 9571 enqueued variables after 2487027 conflicts
c [score-dist-11] active 2851 (23%), one 9571 (77%), zero 0 (0%)
c [score-dist-11] max exp 676, different 132 (19%)
c [score-dist-11] median active exp 623, avg 617.5
c [simplification-11] removed 1 variables 0.0% (12422 remain 95%)
c [simplification-11] removed 177 irredundant clauses 0.1% (267220 remain 87%)
c [simplification-11] maximum reduction of 0% = max (0%, 0%)
c [simplification-11] full geometric conflict interval increment 1000000
c [simplification-11] conflict interval soft limit 1000000 reached
c [simplification-11] new conflict interval 1000000
c [simplification-11] penalized conflict interval 1000000 = 1 * 1000000
c [simplification-11] hard conflict limit 3987027 (soft 3487027 + delta 500000)
c [simplification-11] new conflict limit 3487027 (hard 3987027)
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 -  317.6   12422   267220   2534763  286475  15196   324   17   549   47   3%   1024    4   15   17   89%
c -  322.0   12422   267220   2599822  289322  15201   324   16   549   47   3%   1024  -38   13   17   76%
c -  327.2   12422   267220   2663461  291930  15203   324   18   653   47   3%   1024   58   19   17  110%
c -  332.4   12422   267220   2726780  293080  15216   324   16   709   47   2%   1024   79   17   17   95%
c -  337.9   12422   267220   2789756  296776  15223   324   18   628   48   3%   1024  -34   22   17  131%
c -  344.0   12422   267220   2851069  293392  15227   324   17   560   47   3%   1024  -52   15   18   88%
c -  348.4   12422   267220   2919058  298776  15231   324   18   529   48   3%   1024  -35   18   17  104%
c -  359.8   12422   267220   2984856  292720  15243   324   20   558   48   4%   1024  -18   16   18   89%
c -  366.7   12422   267220   3059625  301596  15250   324   18   590   49   3%   1024   13   20   18  112%
c -  371.5   12422   267220   3130481  309352  15257   324   18   583   49   3%   1024   26   21   17  126%
c -  380.3   12422   267220   3433999  310635  15260   324   22   650   50   3%   1024  371   27   27  101%
c 
c [simplification-12] limit 3487027 conflicts (hard 3987027) hit after 3487028 conflicts
c [quatres-10] found 100804 quaternary clauses 19% in total
c [quatres-10-1] removed 46 duplicate quaternary clauses
c [quatres-10-1] added 5 double-self-subsuming ternary resolvents
c [quatres-10-2] added 211 single-self-subsuming ternary resolvents
c [quatres-10-2] added 76 quaternary resolvents
c [ternres-10] limit 87920971 with penalty 0 = 0 + 0
c [ternres-10] all 12422 free variables schedulable
c [ternres-10] 4 ternary resolvents (0 bin, 4 trn)
c [ternres-10] fully completed ternary resolution
c [gauss-4] limit 2198024 penalty 3 = 3 + 0
c [gauss-4] extracted 37 xors of average arity 3.0
c [gauss-4] connected 111 occurrences of 21 variables (average 5.3)
c [gauss-4] limit 2198024 penalty 3 = 3 + 0
c [gauss-4] fully completed
c [gauss-4] exported 0 unary, 0 binary and 0 ternary equations
c [basicprobe-3] limit 200000000 penalty 1 = 1 + 0
c [basicprobe-3-0] 805 sched 6%, 0 failed, 0 lifted, 2 hbrs
c [basicprobe-3-1] 805 sched 6%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-3-1] fully completed probing
c [basicprobe-3-1] removed 0 variables, found 2 hbrs
c [transred-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 0 transitive binary clauses
c [sort-queue-12] sorted 8930 enqueued variables after 3487028 conflicts
c [score-dist-12] active 3492 (28%), one 8930 (72%), zero 0 (0%)
c [score-dist-12] max exp 873, different 237 (27%)
c [score-dist-12] median active exp 737, avg 630.3
c [simplification-12] removed 0 variables 0.0% (12422 remain 95%)
c [simplification-12] removed 0 irredundant clauses 0.0% (267220 remain 87%)
c [simplification-12] maximum reduction of 0% = max (0%, 0%)
c [simplification-12] full geometric conflict interval increment 1000000
c [simplification-12] new conflict interval 2000000
c [simplification-12] penalized conflict interval 2000000 = 1 * 2000000
c [simplification-12] hard conflict limit 6487028 (soft 5487028 + delta 1000000)
c [simplification-12] new conflict limit 5487028 (hard 6487028)
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 -  386.5   12422   267220   3496838  309238  15486   326   20   684   49   3%   1024  233   21   23   90%
c -  390.7   12422   267220   3563229  312090  15491   326   13   610   49   2%   1024   38   12   20   64%
c -  398.2   12422   267220   3632410  309864  15498   326   20   592   49   3%   1024    0   12   19   65%
c -  403.8   12422   267220   3703407  316034  15504   326   15   783   50   2%   1024  133   17   18   95%
c -  408.6   12422   267220   3771573  317898  15504   326   18   527   50   3%   1024  -99   19   17  116%
c -  413.6   12422   267220   3839994  318520  15509   326   17   473   49   4%   1024 -104   16   17   94%
c -  420.7   12422   267220   3911293  317553  15515   326   20   627   50   3%   1024   48   19   16  116%
c -  429.7   12422   267220   3986244  317355  15524   326   16   554   49   3%   1024   -2   19   18  106%
c -  435.6   12422   267220   4064945  325454  15531   326   18   570   50   3%   1024   -4   19   18  103%
c -  442.4   12422   267220   4136154  324740  15535   326   19   644   51   3%   1024   41   21   19  114%
c -  449.8   12422   267220   4210830  327544  15540   326   21   559   51   4%   1024  -57   21   19  110%
c -  456.1   12422   267220   4284705  330484  15542   326   19   613   51   3%   1024   -1   22   19  117%
c -  465.8   12422   267220   4359322  327371  15553   326   17   402   50   4%   1024 -189   21   20  104%
c -  471.2   12422   267220   4439800  338253  15558   326   15   739   51   2%   1024  113   17   18   90%
c -  476.6   12422   267220   4509867  339395  15565   326   16   717   51   2%   1024  102   18   18  101%
c -  489.7   12422   267220   4583127  329756  15582   326   15   647   51   2%   1024   38   12   20   64%
c -  500.6   12422   267220   4674103  338360  15595   326   18   572   52   3%   1024  -29   20   19  105%
c -  506.8   12422   267220   4758060  349356  15601   326   18   661   52   3%   1024   62   15   19   83%
c -  519.2   12422   267220   4835106  341961  15619   326   23   610   52   4%   1024   43   34   21  164%
c -  528.6   12422   267220   4922934  351707  15624   326   18   593   53   3%   1024   56   19   20   96%
c -  535.1   12422   267220   5010061  359145  15627   326   16   403   54   4%   1024 -228   16   18   89%
c -  542.8   12422   267220   5085130  355331  15635   326   19   589   54   3%   1024   65   18   18  103%
c -  549.7   12422   267220   5167671  355743  15639   326   18   643   53   3%   1024   57   18   18  101%
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 -  562.3   12422   267220   5252877  351682  15652   326   24   621   53   4%   1024   -5   22   20  109%
c -  570.5   12422   267220   5341923  365169  15657   326   20   625   54   3%   1024   17   20   19  102%
c -  576.8   12422   267220   5421636  369365  15659   326   20   613   55   3%   1024  -12   32   19  174%
c 
c [simplification-13] limit 5487028 conflicts (hard 6487028) hit after 5487028 conflicts
c [quatres-11] found 108743 quaternary clauses 19% in total
c [quatres-11-1] removed 103 duplicate quaternary clauses
c [quatres-11-1] added 13 double-self-subsuming ternary resolvents
c [quatres-11-2] added 218 single-self-subsuming ternary resolvents
c [quatres-11-2] added 59 quaternary resolvents
c [ternres-11] limit 141355899 with penalty 0 = 0 + 0
c [ternres-11] all 12422 free variables schedulable
c [ternres-11] 1 ternary resolvents (0 bin, 1 trn)
c [ternres-11] fully completed ternary resolution
c [cce-6] limit of 176694873 steps penalty 2 = 2 + 0
c [cce-6-1] eliminated 12 clauses out of 92189 (0%) of length 6
c [cce-6-1] eliminated 26 clauses out of 54695 (0%) of length 5
c [cce-6-1] eliminated 68 clauses out of 32724 (0%) of length 4
c [cce-6-1] completed large round (ATE)
c [cce-6-1] eliminated 106 large clauses in 147973971 steps
c [cce-6-1] allowing another 73986985 steps for small clauses
c [cce-6-1] scheduling 10154 clauses = 347 binary + 9807 ternary
c [cce-6-1] tried to eliminate 10154 small clauses 100%
c [cce-6-1] completed small round (ATE)
c [cce-6-1] eliminated 106 covered clauses in round 1
c [cce-6-2] incomplete large round (ATE)
c [cce-6-2] allowing another 49556836 steps for small clauses
c [cce-6-2] scheduling 10154 clauses = 347 binary + 9807 ternary
c [cce-6-2] tried to eliminate 10154 small clauses 100%
c [cce-6-2] completed small round (ATE)
c [cce-6-2] eliminated 0 covered clauses in round 2
c [cce-6] eliminated 106 covered clauses in TOTAL during 2 rounds
c [cce-6] 106 < 1/100 * 267220 = 2672 considered unsuccessful
c [sort-queue-13] sorted 9386 enqueued variables after 5487028 conflicts
c [score-dist-13] active 3036 (24%), one 9386 (76%), zero 0 (0%)
c [score-dist-13] max exp 955, different 181 (19%)
c [score-dist-13] median active exp 356, avg 319.6
c [simplification-13] removed 0 variables 0.0% (12422 remain 95%)
c [simplification-13] removed 106 irredundant clauses 0.0% (267114 remain 87%)
c [simplification-13] maximum reduction of 0% = max (0%, 0%)
c [simplification-13] full geometric conflict interval increment 2000000
c [simplification-13] conflict interval soft limit 1000000 reached
c [simplification-13] new conflict interval 1000000
c [simplification-13] penalized conflict interval 1000000 = 1 * 1000000
c [simplification-13] hard conflict limit 6987028 (soft 6487028 + delta 500000)
c [simplification-13] new conflict limit 6487028 (hard 6987028)
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 -  591.9   12422   267114   5499193  360832  15891   326   19   677   54   3%   1024   32   19   20   97%
c -  601.1   12422   267114   5590124  367219  15893   326   21   634   54   3%   1024  -55   23   20  116%
c -  613.7   12422   267114   5676812  363175  15905   326   21   588   54   4%   1024  -52   14   21   66%
c -  620.3   12422   267114   5769420  378081  15906   326   19   576   55   3%   1024  -51   20   19  106%
c -  634.1   12422   267114   5850036  372255  15911   326   22   600   55   4%   1024  -26   21   21   97%
c -  652.2   12422   267114   5940832  368531  15920   326   23   604   55   4%   1024  -12   23   23   99%
c -  669.2   12422   267114   6040375  376423  15924   326   23   563   55   4%   1024  -62   26   24  109%
c -  682.0   12422   267114   6136735  386751  15927   326   19   703   56   3%   1024   59   17   22   79%
c -  690.7   12422   267114   6234044  395128  15927   326   15   720   57   2%   1024   22   18   17  102%
c -  697.9   12422   267114   6317088  389260  15929   326   16   666   56   2%   1024   21   15   17   93%
c -  709.2   12422   267114   6404073  387513  15931   326   14   607   56   2%   1024   15   11   18   60%
c 
c [simplification-14] limit 6487028 conflicts (hard 6987028) hit after 6489236 conflicts
c [quatres-12] found 112399 quaternary clauses 19% in total
c [quatres-12-1] removed 89 duplicate quaternary clauses
c [quatres-12-1] added 6 double-self-subsuming ternary resolvents
c [quatres-12-2] added 143 single-self-subsuming ternary resolvents
c [quatres-12-2] added 47 quaternary resolvents
c [ternres-12] limit 187571460 with penalty 0 = 0 + 0
c [ternres-12] all 12422 free variables schedulable
c [ternres-12] 5 ternary resolvents (0 bin, 5 trn)
c [ternres-12] fully completed ternary resolution
c [transred-11] limit 1000000 with penalty 1 = 1 + 0
c [transred-11] removed 0 transitive binary clauses
c [sort-queue-14] sorted 1043 enqueued variables after 6489236 conflicts
c [score-dist-14] active 11379 (92%), one 1043 (8%), zero 0 (0%)
c [score-dist-14] max exp 589, different 322 (55%)
c [score-dist-14] median active exp 89, avg 225.2
c [simplification-14] removed 0 variables 0.0% (12422 remain 95%)
c [simplification-14] removed 0 irredundant clauses 0.0% (267114 remain 87%)
c [simplification-14] maximum reduction of 0% = max (0%, 0%)
c [simplification-14] full geometric conflict interval increment 1000000
c [simplification-14] new conflict interval 2000000
c [simplification-14] penalized conflict interval 2000000 = 1 * 2000000
c [simplification-14] hard conflict limit 9489236 (soft 8489236 + delta 1000000)
c [simplification-14] new conflict limit 8489236 (hard 9489236)
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 -  731.2   12422   267114   6497227  383429  16089   326   27   568   56   5%   1024  -27   29   23  125%
c -  738.7   12422   267114   6597871  400561  16089   326   20   585   57   3%   1024  -32   18   20   87%
c -  755.0   12422   267114   6683284  393879  16092   326   29   590   57   5%   1024    6   30   24  126%
c -  764.0   12422   267114   6776977  402314  16092   326   19   625   55   3%   1024   -6   16   22   76%
c -  773.0   12422   267114   6865524  403996  16095   326   19   615   58   3%   1024   -3   20   20   99%
c -  782.0   12422   267114   6956301  404864  16099   326   29   533   58   5%   1024   -5   30   20  152%
c -  794.7   12422   267114   7048306  405743  16102   326   20   581   58   3%   1024   -4   18   21   85%
c -  803.1   12422   267114   7141066  411156  16102   326   17   494   58   3%   1024 -115   15   19   81%
c -  814.1   12422   267114   7233464  411187  16102   326   32   528   59   6%   1024  -56   53   20  258%
c -  860.5   12422   267114   7329226  397212  16111   326   34   531   58   6%   1024  -54   29   32   92%
c -  895.8   12422   267114   7444450  417184  16111   326   23   665   58   3%   1024   32   16   27   58%
c -  904.6   12422   267114   7540759  429612  16111   326   17   583   59   3%   1024  -27   15   22   69%
c -  911.8   12422   267114   7623180  427413  16111   326   15   706   59   2%   1024   57   12   19   64%
c -  924.0   12422   267114   7716081  422838  16114   326   20   503   60   4%   1024 -105   18   20   88%
c 1  941.3   12422   267114   7784969  487226  16119   326   54   507   87  11%   1024 -108   75   25  300%
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
s SATISFIABLE
c
c bate: 7 basic ate = 7 trn 100% + 0 lrg 0% in 1 updates
c bcas: 4 count, 0 added (0 skipped), 751079 steps
c bkwd: tried 13780 clauses, 27515 lits, 2.00 lits/clause
c bkwd: checked 1620254 occs, 117.58 occs/clause, 58.89 occs/lit
c bkwd: subsumed 0 binary, 5 ternary, 6 large
c bkwd: strengthened 0 binary, 1 ternary (100% self), 117 large (0% self)
c blkd: 4 bces, 526 removed, 20481997 resolutions, 35689254 steps
c blkd: 79 blocking literals 0%, 0 pure
c bump: 7358574 bumped seen, 423989834 lits 57.6 on average
c card: 4 count, 0 units, 0 am1, 6867524 steps
c card: 0 rescheduled, 0 eliminated, 0 resolved, 1489 subsumed
c card: 8 at-most-one constraints found, average size 3.00
c card: 8 at-most-one constraints used 100%, average size 3.00
c card: 37 at-most-two constraints found, average size 4.05
c card: 37 at-most-two constraints used 100%, average size 4.05
c cces: 6 cces, 17041 eliminated, 17039 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: 3617008 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 52 gcs, 0 rescored clauses, 3871 rescored vars
c dcps: 34 decompositions, 51 equivalent 0%
c deco: 3985 decision-only clauses 0%, 63% reduction
c decs: 64981712 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 5 elims, 528 eliminated 4%, 0 pure 0%
c elms: 8 rounds, 1.6 rounds/bve
c elms: 521 small 99%, 7 large 1%
c elms: 2413 tried small, 522 succeeded 22%, 1891 failed 78%
c elms: 18193 subsumed, 7509 strengthened, 0 blocked
c elms: 3313597 copies, 9592485 resolutions, 727402 ipos
c elms: 801850 subchks, 457787 strchks
c gaus: 4 extractions, 1175 extracted, 4.7 size, 5 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 11986752 steps, 5993376 extr 50%, 20288 elim 0%
c glue: 18.9 orig avg, 18.9 real avg, 3.7 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 102 = 23 simple 23% + 78 trn 76% + 1 lrg 1%, 47 sub 46%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 7358574 clauses, 37.4 length
c lrnd: 275350377 lits = 290736905 orig - 15386528 removed 5%
c lrnd: 1545779 uips 21%, 5245201 flips 71%
c mins: 6883528 mins 94%, 105 bin 0%, 466338 size 6%
c mins: 166423447 poisoned searches, 21224492 hits, 13% hit rate
c mins: 412480648 used twice searches, 92588923 hits, 22% hit rate
c move: moved 1384, 18 bin 1%, 1366 trn 99%
c otfs: 435312 driving 36%, 788807 restarting 64%
c otfs: str 1224119, 1216697 red 99%, 7422 irr 1%
c otfs: str 1224119, 0 bin 0%, 119 trn 0%, 1224000 lrg 100%
c otfs: sub 7721, 7720 red 100%, 1 irr 0%
c otfs: sub 7721, 0 bin 0%, 22 trn 0%, 7699 lrg 100%
c phas: 1 computed, 12517 set, 0 pos (0%), 12517 neg (100%)
c prbs: 3 basic, 9036 probed, 3 failed, 0 lifted
c prbs: 3 simple, 28095 probed, 5 failed, 1 eqs
c prbs: 3 treelook, 4105 probed, 0 failed, 0 lifted
c prom: 563147 locked 23% out of 2498924 tried
c prps: 630978830 props, 10 props/dec
c prps: 100% srch, 0% simp, 0% lkhd
c quat: 12 count, 3840 quat, 5861 self1, 737 self2, 415 dup
c queu: 14 sorted, 64981712 next (74755484 steps 1.15)
c queu: 440576398 enq (438825625 steps 1.00), 423989834 deq 96%
c redc: 219 clauses 0%, 759670 tried 10%, 2 sat 0%
c redc: 225 lits 0%, 6876413 tried 2%, 2 sat 0%
c redc: 19 times jump level reduced, 35.6 levels on average
c reds: 100 count, 77849.7 conflicts per reduce
c reds: 0 memlim 0%, 100 arith 100%
c reds: 4951053 collected 77%, 1487965 retired 23%
c rmbd: 11 removed, 1 red 9%
c rsts: 48723 restarts 98%, 784 skipped 2%
c rsts: 784 saturating 100%, 0 reuse 0%
c rsts: 0 kept 0.0% average 0.0%
c scnc: 1 count, 1.200 min (200/1000), 1.200 max (200/1000)
c simp: 14 count, 14 confs 100%, 0 vars 0%
c simp: 0 its 0%, 0 bin 0%, 0 trns 0%
c subl: 7358574 count (9868517 tried 1.3), 411935 sub out of 7354261 (5.6%)
c swps: 7 count, 10 rounds, 8776 queries (877.6/round)
c swps: 8777 sat calls, 2 unsat (1.0% success rate)
c swps: 233355 decisions 26.6, 8917 conflicts 1.0
c swps; 733.0 avg class size, 38.2 avg environment size
c swps: 0 failed, 5 impls, 1 equivs
c swp0: 2922 type 0 queries, 15 unsat (0.5%), 2922 sat (100.0%)
c swp1: 5854 type 1 queries, 95 unsat (1.6%), 5853 sat (100.0%)
c sync: 0 produced units, 0 successful consumptions 0%
c sync: 0 consume units calls, 0 tried 0%, 0 success 0%
c sync: 0 produced clauses, 0 successful consumptions 0%
c sync: 0 consume clause calls, 0 tried 0%, 0 success 0%
c time: 144688638 calls to obtain time
c tops: 407 fixed 3%, 2 its, 3892484.50 confs/it
c trds: 11 transitive reductions, 31 removed, 0 failed
c trds: 271733 nodes, 6460 edges, 7876 steps
c trim: 7794549 words, 29.7 MB
c trnr: 12 count, 24 bin, 321 trn, 33864960 steps
c unhd: 5 count, 6 rounds, 4180997 steps
c unhd: 0 non-trivial sccs of average size 0.0
c unhd: 0 units, 0 bin, 0 trn, 0 lrg
c unhd: 8 failed, 8 stamp, 0 lits, 0 bin, 0 trn, 0 lrg
c unhd: 1056 tauts, 0 bin 0%, 772 trn 73%, 275 lrg 26%
c unhd: 1056 tauts, 9 stamp 1%, 527 red 50%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 1026 str, 0 bin 0%, 37 trn 4%, 989 lrg 96%, 947 red 92%
c vars: 12422 remaining 93% and 986 removed 7% out of 13408
c vars: 407 fixed 3%, 528 eliminated 4%, 51 equivalent 0%
c vsts: 24692454923 visits, 100% srch, 0% simp, 0% lkhd
c vsts: 39.1 search visits per propagation, 3170.3 per conflict
c wchs: 9104243153 pushed, 35655232 enlarged, 775 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all        7358101       4951053       1487965     132134825      33219307       2580324
c 
c  0 0        393311   5     11388   0         0   0 107862202  82< 19389813  58    969892  38    11.2
c  1 5        362499   5    115284   2    228482  15   6436631   5   1497126   5<   186426   7     0.7
c  2 6        936139  13    433043   9    451200  30   8642723   7   4289798  13    524861  20<    2.4
c  3 9       1631407  22   1270307  26    313836  21<  3553625   3   2986122   9    440186  17     3.9
c  4 14      1821154  25<  1569214  32<   180095  12   2711796   2   2604328   8    299272  12     7.9
c  5 21      1054163  14    855138  17    121988   8   1490137   1   1305128   4     98636   4     5.6
c  6 30       712889  10    392686   8     77681   5    865177   1    753931   2     40050   2    10.5
c  7 41       225220   3    161802   3     48447   3    290883   0    212390   1     10244   0     1.8
c  8 54       102675   1     68605   1     28424   2    132998   0     87655   0      4244   0     1.6
c  9 69        52099   1     33669   1     16215   1     65933   0     41112   0      2279   0     1.6
c 10 86        43132   1     27005   1     14601   1     53735   0     32236   0      2139   0     2.8
c 11 126       15933   0      9938   0      5507   0     19879   0     12271   0      1148   0     2.4
c 12 230        4355   0      1800   0       834   0      5316   0      4613   0       704   0     1.9
c 13 534        3125   0      1174   0       655   0      3790   0      2784   0       243   0     1.8
c 
c avg                  3.7           4.1           3.2           0.5           1.3           1.8
c std                  1.9           1.5           2.0           1.2           1.9           1.8
c 
c   63.478   7% bump
c   39.337   4% decide
c   10.192   1% cce
c    6.364   1% elim
c    4.039   0% quatres
c    3.685   0% sweep
c 
c   10.312 < 1% rest (below)
c 
c    3.028   0% rescore
c    2.637   0% block
c    2.542   0% probe
c    0.748   0% gauss
c    0.479   0% bca
c    0.433   0% unhide
c    0.208   0% ternres
c    0.173   0% card
c    0.064   0% transred
c    0.000   0% locs
c    0.000   0% queuesort
c ==================================
c    1.337   0% preprocessing     4%
c   34.265   4% inprocessing     96%
c ==================================
c   35.602   4% simplifying
c  905.719  96% search
c ==================================
c  941.322 100% all
c 
c       7784969 conflicts,        8270.3 confs/sec
c          3793 ternaries,        2052.5 confs/ternary
c           159 binaries,        48962.1 confs/binary
c             2 iterations,    3892484.5 confs/iteration
c 
c           100 reductions,          0.1 redus/sec,  77849.7 confs/reduction
c         48723 restarts,           51.8 rests/sec,    159.8 confs/restart
c      64981712 decisions,       69032.4 decis/sec,      8.3 decis/conflict
c     630978830 propagations,   670311.6 props/sec,      9.7 props/decision
c 
c 941.3 seconds, 147.9 MB
c launch: done
