c launch: /data/cnf/sc2014/app/009-80-4.cnf.bz2
c host: atom17
c Lingeling SAT Solver
c 
c Version b7ztzud 55d9a3e9649fc56eacf3e72d8e2e2d5c615d5f18
c 
c Copyright (C) 2010-2014 Armin Biere JKU Linz Austria.
c All rights reserved.
c 
c released Fri May  1 11:44:04 CEST 2015
c compiled Fri May  1 11:44:04 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-49-generic x86_64
c 
c piping '/data/cnf/sc2014/app/009-80-4.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/009-80-4.cnf.bz2
c no embedded options
c found 'p cnf 13408 478480' header
c read 13408 variables, 478480 clauses, 3138512 literals in 0.00 seconds
c
c --abstime=0
c --bate=1
c --batewait=2
c --bca=1
c --bcaddlimldscale=2
c --bcamaxeff=10000000
c --bcaminuse=100
c --bcawait=2
c --bkwdscale=100
c --bkwdroundlim=7
c --bkwdresched=1
c --blkboost=10
c --blkboostvlim=10000000
c --blkclslim=1000000
c --blklarge=1
c --blkmaxeff=800000000
c --blkmineff=50000000
c --blkocclim1=100000
c --blkocclim=1000000
c --blkocclim2=10000
c --blkreleff=100
c --blkresched=1
c --blkrtc=0
c --blksmall=1
c --blksuccessmaxwortc=6
c --blksuccessrat=100
c --block=1
c --blockwait=1
c --boost=1
c --bumpsimp=1
c --card=1
c --cardcut=2
c --cardexpam1=3
c --cardglue=0
c --cardignused=0
c --cardmaxeff=300000000
c --cardmaxlen=1000
c --cardmineff=2000000
c --cardminlen=3
c --cardocclim1=300
c --cardocclim2=15
c --cardreleff=5
c --cardreschedint=10
c --carduse=2
c --cardwait=0
c --cce2wait=1
c --cce=3
c --cceateint=2
c --cceboost=10
c --cceboostdel=3
c --cceboostint=5
c --cceboostvlim=10000000
c --cce3wait=2
c --ccemaxround=3
c --ccemaxeff=2147483647
c --ccemineff=30000000
c --ccereleff=50
c --ccertc=0
c --ccertcint=15
c --ccertcintvlim=2000000
c --ccesuccessrat=100
c --ccewait=2
c --clim=-1
c --compact=0
c --deco=1
c --decolim=100
c --deco1opt=1
c --decompose=1
c --defragfree=50
c --defragint=10000000
c --delmax=10
c --dlim=-1
c --druplig=0
c --drupligcheck=0
c --drupligtrace=0
c --drupligtraceorig=0
c --elim=1
c --elmaxeff=800000000
c --elmblk=1
c --elmblkwait=1
c --elmboost=20
c --elmboostdel=3
c --elmboostint=5
c --elmboostvlim=4000000
c --elmclslim=1000000
c --elmfull=0
c --elmineff=20000000
c --elmlitslim=200
c --elmocclim1=1000
c --elmocclim=1000000
c --elmocclim2=100
c --elmoccsumforced=0
c --elmreleff=200
c --elmresched=0
c --elmroundlim=3
c --elmrtc=0
c --elmrtcint=10
c --elmrtcintvlim=500000
c --elmsuccessmaxwortc=4
c --elmsuccessrat=100
c --exitonabort=0
c --factmax=100000
c --factor=3
c --gauss=1
c --gaussexptrn=1
c --gaussextrall=1
c --gaussmaxeff=50000000
c --gaussmaxor=20
c --gaussmineff=2000000
c --gaussreleff=2
c --gausswait=2
c --gluekeep=4
c --gluekeepsize=15
c --gluescale=4
c --hbrdom=2
c --import=1
c --incredcint=1
c --incredconfslim=0
c --incsavevisits=0
c --inprocessing=1
c --irrlim=1
c --jwhred=1
c --keepmaxglue=1
c --keepmaxglueint=100
c --lhbr=1
c --lkhd=2
c --locs=0
c --locsbanner=0
c --locsclim=1000000
c --locsboost=2
c --locscint=10000
c --locset=2
c --locsexport=1
c --locsmaxeff=100000
c --locsmineff=1000
c --locsred=0
c --locsreleff=5
c --locsrtc=0
c --locsvared=100
c --locswait=2
c --maxscaledglue=15
c --memlim=-1
c --minimize=2
c --minlocalgluelim=200
c --minlocalsizelim=3000
c --minrecgluelim=100
c --minrecsizelim=1000
c --norestartsatlimlo=85
c --move=2
c --otfs=1
c --penmax=4
c --phase=0
c --phaseluckfactor=200
c --phaselucklim=100
c --phaseluckmaxround=10
c --phasesave=1
c --plain=0
c --plim=-1
c --poison=1
c --prbasic=1
c --prbasicmaxeff=400000000
c --prbasicmineff=1000000
c --prbasicreleff=50
c --prbasicroundlim=8
c --prbasicrtc=0
c --prbrtc=0
c --prbsimple=2
c --prbsimpleboost=10
c --prbsimpleliftdepth=2
c --prbsimplemaxeff=200000000
c --prbsimplemineff=2000000
c --prbsimplereleff=40
c --prbsimplertc=0
c --probe=1
c --promote=1
c --promotegluelim=8
c --pure=1
c --quatres=1
c --quatreswait=2
c --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 --scoreshift=0
c --scoreresetint=2147483647
c --seed=0
c --simpbintinc=100
c --simpbintinclim=10000
c --simpcintdelay=2000
c --simpcintinc=20000
c --simpcintincdiv=1
c --simpcintmaxhard=10000000
c --simpcintmaxsoft=1000000
c --simpincdelmaxfact=50
c --simpincdelmaxmin=10000
c --simpinitdelay=0
c --simpintsizepen=0
c --simpen=0
c --simpidiv=3
c --simpiscale=100
c --simpitdelay=10
c --simpitintinc=10
c --simpitintinclim=1000
c --simplify=2
c --simprtc=5
c --simptintinc=1000
c --simptintinclim=10000
c --simpvarchg=100
c --simpvarlim=100
c --sizemaxpen=5
c --sizepen=1000000
c --sleeponabort=0
c --smallirr=90
c --smallve=1
c --smallvevars=10
c --smallvewait=0
c --sortlits=0
c --subl=9
c --sweep=1
c --sweepboost=10
c --sweepboostdel=4
c --sweepboostint=7
c --sweepboostvlim=1000000
c --sweepfacdec=10
c --sweepforgive=2
c --sweepirr=3
c --sweepmaxeff=200000000
c --sweepmaxdec=10000
c --sweepmaxround=3
c --sweepmindec=100
c --sweepmineff=1000000
c --sweepred=3
c --sweepreleff=3
c --sweeprtc=0
c --sweeprtcint=14
c --sweeprtcintvlim=100000
c --sweepsuccessmaxwortc=6
c --sweepsuccessrat=1000
c --sweepwait=2
c --synclsall=1
c --synclsglue=8
c --synclsint=100
c --synclslen=40
c --syncunint=111111
c --termint=122222
c --ternres=1
c --ternresboost=5
c --ternresrtc=0
c --ternreswait=2
c --transred=1
c --transredwait=2
c --trapiflush=0
c --trdmaxeff=2000000
c --trdmineff=100000
c --trdreleff=10
c --treelook=1
c --treelookboost=10
c --treelookfull=0
c --treelookmaxeff=50000000
c --treelookmineff=300000
c --treelookreleff=2
c --treelookrtc=0
c --trep=1
c --trepint=55555
c --trnreleff=10
c --trnrmaxeff=200000000
c --trnrmineff=4000000
c --unhdatrn=2
c --unhdextstamp=1
c --unhdhbr=0
c --unhdlnpr=3
c --unhdmaxeff=20000000
c --unhdmineff=100000
c --unhdreleff=2
c --unhdroundlim=20
c --unhide=1
c --unhidewait=0
c --usedtwice=1
c --vsidsdint=256
c --wait=1
c --waitmax=4
c --witness=0
c --check=0
c --log=-1
c --profile=1
c --profilelong=1
c --verbose=1
c [freezer] frozen 0 variables out of 13025 free variables 0%
c [limits] no decision limit
c [limits] no conflict limit
c [limits] no propagation limit
c [limits] simplification not delayed since 'simpdelay' zero
c [set-maximum-score] maximum score limit 1.000000d+500
c [set-minimum-score] minimum score limit 1.000000d-500
c [set-score-increment-1] factor 1.200000d+00 (200/1000) after 0 conflicts
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c *    0.0   13025   308391         0       0      0     0    0     0   17   0%      0    0    0    0    0%
c 
c [simplification-1] limit 0 conflicts (hard 0) hit after 0 conflicts
c [card-1] limit 2000000 penalty 0 = 0 + 0
c [card-1] found 3 at-most-one constraints of average size 3.0
c [card-1] found 6 at-most-two constraints of average size 4.0
c [card-1] using previous limit 2000000 for elimination
c [card-1] 9 out of 9 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 404 variables
c [simpleprobe-1] all 13004 free variables schedulable
c [simpleprobe-1] boosting simple probing limit by 10
c [simpleprobe-1] limit 20000000 penalty 0 = 0 + 0
c [decomp-2] removed 10 variables
c [simpleprobe-1] 5745 variables remain 44% (7249 retained 56%)
c [simpleprobe-1] removed 10 variables, found 2 hbrs, 4 units
c [unhide-1] limit 100000 with penalty 0 = 0 + 0
c [unhide-1-1] 0 units, 9 failed, 777 tauts, 0 hbrs, 15 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 12991 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 473 variables 4% in round 1 in 2078280 steps
c [elim-1-1] backward subsumption/strengthening limit 2078200
c [elim-1-1-1] backward checking 2410 touched variables 19%
c [elim-1-1-1] fully completed backward checking in 1 rounds
c [elim-1-1] subsumed 7 and strengthened 76 clauses in 1423313 steps
c [elim-1-1] rescheduled 122 variables 1% by backward subsumption
c [elim-1-2] eliminated 2 variables 0% in round 2 in 55611 steps
c [elim-1-2] backward subsumption/strengthening limit 55600
c [elim-1-2-1] backward checking 19 touched variables 0%
c [elim-1-2-1] incomplete backward checking 0 remain 0%
c [elim-1-2] subsumed 0 and strengthened 0 clauses in 55601 steps
c [elim-1-2] fully rescheduled 12515 variables 96%
c [elim-1-3] no variable eliminated in round 3 in 1604030 steps
c [elim-1] fully completed in 3 rounds
c [elim-1] transition to [ all 0 rem 0 ] state
c [elim-1] eliminated 476 = 4% variables out of 12991 scheduled
c [phase-count-1] 301704 negative 99.5% of 303167 except 1463 0.5%
c [phase-count-1] 299578 positive 98.8% of 303167 except 3589 1.2%
c [phase-count-1] less non-negative clauses 1463 than limit 30300 (10.0%)
c [phase-count-1] non-pos/non-neg = 3589/1463 = 2.45 >= 2.00 = 200/100
c [lucky-phase-1] forcing lucky phase -1
c [phase-1] phase bias: 0 positive 0%, 12515 negative 100%
c [score-distribution-1] 0 pos 0.00%, 0 min 0.00%, 12515 zero 100.00%
c [score-distribution-1] 1 different 0.01% out of total 12515 variables
c [simplification-1] removed 510 variables 3.9% (12515 remain 96%)
c [simplification-1] removed 5224 irredundant clauses 1.7% (303167 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 [simplification-2] limit 4000 conflicts (hard 14000) hit after 4000 conflicts
c [simpleprobe-2] 5539 schedulable variables 44%
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [simpleprobe-2] 5539 variables remain 44% (6976 retained 56%)
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 5985 literals 24%
c [treelook-1] scheduling used 300011 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 300019 steps
c [treelook-1] 4995 literals remain 20%
c [treelook-1] 4419 variables remain to probed next time 35%
c [treelook-1] removed 1 variables, found 0 hbrs
c [basicprobe-1] limit 2425256 based on 303157 irredundant clauses
c [basicprobe-1-0] 513 sched 4%, 2 failed, 0 lifted, 17 hbrs
c [decomp-5] removed 2 variables
c [basicprobe-1-1] 525 sched 4%, 0 failed, 0 lifted, 2 hbrs
c [basicprobe-1-2] 525 sched 4%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-1-2] fully completed probing
c [basicprobe-1-2] 2 units = 2 failed (100%) + 0 lifted (0%)
c [basicprobe-1-2] removed 2 variables, found 19 hbrs
c [unhide-2] limit 100000 with penalty 0 = 0 + 0
c [unhide-2-2] 0 units, 0 failed, 2 tauts, 0 hbrs, 21 literals
c [block-1] scheduling all variables this time
c [block-1] scheduled 12512 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 1234 blocked clauses
c [block-1] 1234 < 1/100 * 303132 = 3031 considered unsuccessful
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 8027 clauses out of 103641 (8%) of length 7
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 8027 large clauses in 30000019 steps
c [cce-1-1] allowing another 15000009 steps for small clauses
c [cce-1-1] scheduling 717 clauses = 311 binary + 406 ternary
c [cce-1-1] tried to eliminate 717 small clauses 100%
c [cce-1-1] eliminated 6 binary clauses 2%
c [cce-1-1] eliminated 43 ternary clauses 11%
c [cce-1-1] eliminated 49 small clauses 7%
c [cce-1-1] eliminated 49 small clauses in 15167355 steps
c [cce-1-1] completed small round (ATE)
c [cce-1-1] eliminated 8076 covered clauses in round 1
c [cce-1-2] incomplete large round (ATE)
c [cce-1-2] allowing another 7416380 steps for small clauses
c [cce-1-2] scheduling 668 clauses = 305 binary + 363 ternary
c [cce-1-2] tried to eliminate 668 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 8076 covered clauses in TOTAL during 2 rounds
c [elim-2] scheduling all variables this time
c [elim-2] scheduled 12512 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 9283 not tried 74% in round 1
c [elim-2] transition to [ all 1 rem 1 ] state
c [elim-2] eliminated 201 = 2% variables out of 12512 scheduled
c [bca-1] limit of 10000000 steps and 561940 added (scaled 2)
c [bca-1] 21175 out of 24624 literals actually usable 86%
c [bca-1] added 0 blocked clauses in 185721 steps
c [sweep-1] limit 1000000 penalty 0 = 0 + 0
c [sweep-1-1] 1329 pos 10.8% + 10982 neg 89.2% = 12311 sched 100.0% ret 0
c [sweep-1-1] 1002315 steps 437 queries 2509.46 avg class size
c [sweep-1-1] 7847 decisions 436 SAT calls 24.46 avg env size
c [sweep-1-1] 9949 variables remain 81% (2362 retained 19%)
c [decomp-7] removed 1 variables
c [sweep-1-1] removed 1 vars (0 failed, 0 eqs, 0 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 1 vars in TOTAL (1 rounds, 436 queries)
c [phase-count-2] 279175 negative 99.5% of 280718 except 1543 0.5%
c [phase-count-2] 277182 positive 98.7% of 280718 except 3536 1.3%
c [phase-count-2] less non-negative clauses 1543 than limit 28000 (10.0%)
c [phase-count-2] non-pos/non-neg = 3536/1543 = 2.29 >= 2.00 = 200/100
c [lucky-phase-2] forcing lucky phase -1
c [phase-2] phase bias: 0 positive 0%, 4636 negative 100%
c [score-distribution-2] 3709 pos 30.13%, 214 min 1.74%, 8387 zero 68.13%
c [score-distribution-2] 1402 different 11.39% out of total 12310 variables
c [simplification-2] removed 205 variables 1.6% (12310 remain 95%)
c [simplification-2] removed 22449 irredundant clauses 7.4% (280718 remain 91%)
c [simplification-2] maximum reduction of 7% = max (2%, 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 34301 quaternary clauses 13% in total
c [quatres-1-1] added 40 double-self-subsuming ternary resolvents
c [quatres-1-2] added 59 single-self-subsuming ternary resolvents
c [quatres-1-2] added 300 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 12310 free variables schedulable
c [ternres-1] 217 ternary resolvents (12 bin, 205 trn)
c [ternres-1] fully completed ternary resolution
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] no at-most-one constraint found
c [card-2] found 4 at-most-two constraints of average size 4.2
c [card-2] using previous limit 1000000 for elimination
c [card-2] 4 out of 4 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 5.0
c [gauss-1] connected 5349 occurrences of 336 variables (average 15.9)
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-8] removed 1 variables
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] scheduled 3267 literals 13%
c [treelook-2] scheduling used 300016 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] used 300141 steps
c [treelook-2] 2204 literals remain 9%
c [treelook-2] 1830 variables remain to probed next time 15%
c [treelook-2] removed 0 variables, found 5 hbrs
c [transred-1] limit 280711 based on 280711 irredundant clauses
c [transred-1] removed 3 transitive binary clauses
c [cce-2] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-2-1] eliminated 210 clauses out of 87899 (0%) of length 7
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] eliminated 210 large clauses in 30000046 steps
c [cce-2-1] allowing another 15000023 steps for small clauses
c [cce-2-1] scheduling 10780 clauses = 302 binary + 10478 ternary
c [cce-2-1] tried to eliminate 10780 small clauses 100%
c [cce-2-1] eliminated 1038 ternary clauses 10%
c [cce-2-1] eliminated 1038 small clauses 10%
c [cce-2-1] eliminated 1038 small clauses in 18706846 steps
c [cce-2-1] completed small round (ATE)
c [cce-2-1] eliminated 1248 covered clauses in round 1
c [cce-2-2] incomplete large round (ATE)
c [cce-2-2] allowing another 5646625 steps for small clauses
c [cce-2-2] scheduling 9742 clauses = 302 binary + 9440 ternary
c [cce-2-2] tried to eliminate 9742 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 1248 covered clauses in TOTAL during 2 rounds
c [cce-2] 1248 < 1/100 * 280711 = 2807 considered unsuccessful
c [elim-3] 9283 variables 75% will be scheduled this time
c [elim-3] scheduled 9283 variables 75%
c [elim-3] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-3] rescheduling of touched variables disabled
c [elim-3] incomplete 7241 not tried 59% in round 1
c [elim-3] transition to [ all 0 rem 1 ] state
c [elim-3] eliminated 0 = 0% variables out of 9283 scheduled
c [sweep-2] limit 1000000 penalty 0 = 0 + 0
c [sweep-2-1] 1502 pos 15.1% + 8445 neg 84.9% = 9947 sched 80.8% ret 2362
c [sweep-2-1] 1001278 steps 492 queries 1750.66 avg class size
c [sweep-2-1] 8972 decisions 491 SAT calls 24.61 avg env size
c [sweep-2-1] 7584 variables remain 62% (4725 retained 38%)
c [sweep-2-1] removed 0 vars (0 failed, 0 eqs, 1 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 0 vars in TOTAL (1 rounds, 491 queries)
c [phase-count-3] 271783 negative 99.4% of 273386 except 1603 0.6%
c [phase-count-3] 269837 positive 98.7% of 273386 except 3549 1.3%
c [phase-count-3] less non-negative clauses 1603 than limit 27300 (10.0%)
c [phase-count-3] non-pos/non-neg = 3549/1603 = 2.21 >= 2.00 = 200/100
c [lucky-phase-3] forcing lucky phase -1
c [phase-3] phase bias: 0 positive 0%, 1852 negative 100%
c [score-distribution-3] 4623 pos 37.56%, 1500 min 12.19%, 6186 zero 50.26%
c [score-distribution-3] 1535 different 12.47% out of total 12309 variables
c [simplification-3] removed 1 variables 0.0% (12309 remain 95%)
c [simplification-3] removed 7332 irredundant clauses 2.6% (273386 remain 89%)
c [simplification-3] maximum reduction of 3% = max (0%, 3%)
c [simplification-3] geometric conflict interval increment 5000 = 20000 / 4
c [simplification-3] new conflict interval 9000
c [simplification-3] penalized conflict interval 9000 = 1 * 9000
c [simplification-3] hard conflict limit 25000 (soft 15000 + delta 10000)
c [simplification-3] new conflict limit 15000 (hard 25000)
c 
c [simplification-4] limit 15000 conflicts (hard 25000) hit after 15000 conflicts
c [quatres-2] found 34900 quaternary clauses 13% in total
c [quatres-2-1] removed 1 duplicate quaternary clauses
c [quatres-2-1] added 44 double-self-subsuming ternary resolvents
c [quatres-2-2] added 111 single-self-subsuming ternary resolvents
c [quatres-2-2] added 208 quaternary resolvents
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] all 12309 free variables schedulable
c [ternres-2] 77 ternary resolvents (6 bin, 71 trn)
c [ternres-2] fully completed ternary resolution
c [decomp-11] removed 1 variables
c [basicprobe-2] limit 2187064 based on 273383 irredundant clauses
c [basicprobe-2-0] 544 sched 4%, 0 failed, 0 lifted, 21 hbrs
c [basicprobe-2-1] 555 sched 5%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-2-1] fully completed probing
c [basicprobe-2-1] removed 0 variables, found 21 hbrs
c [bate-1] eliminated 2 asymmetric tautologies during probing
c [unhide-3] limit 50000 with penalty 1 = 1 + 0
c [unhide-3-3] 0 units, 0 failed, 4 tauts, 0 hbrs, 18 literals
c [transred-2] limit 273381 based on 273381 irredundant clauses
c [transred-2] removed 4 transitive binary clauses
c [block-2] scheduling all variables this time
c [block-2] scheduled 12308 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 170 blocked clauses
c [block-2] 170 < 1/100 * 273381 = 2733 considered unsuccessful
c [bca-2] limit of 10000000 steps and 546922 added (scaled 2)
c [bca-2] 13860 out of 24602 literals actually usable 56%
c [bca-2] added 0 blocked clauses in 125219 steps
c [sweep-3] limit 1000000 penalty 0 = 0 + 0
c [sweep-3-1] 2044 pos 27.0% + 5534 neg 73.0% = 7578 sched 61.6% ret 4722
c [sweep-3-1] 1000155 steps 571 queries 1183.32 avg class size
c [sweep-3-1] 12192 decisions 570 SAT calls 28.14 avg env size
c [sweep-3-1] 4851 variables remain 39% (7449 retained 61%)
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, 570 queries)
c [phase-count-4] 271547 negative 99.4% of 273211 except 1664 0.6%
c [phase-count-4] 269654 positive 98.7% of 273211 except 3557 1.3%
c [phase-count-4] less non-negative clauses 1664 than limit 27300 (10.0%)
c [phase-count-4] non-pos/non-neg = 3557/1664 = 2.14 >= 2.00 = 200/100
c [lucky-phase-4] forcing lucky phase -1
c [phase-4] phase bias: 0 positive 0%, 516 negative 100%
c [score-distribution-4] 4011 pos 32.61%, 4402 min 35.79%, 3887 zero 31.60%
c [score-distribution-4] 1431 different 11.63% out of total 12300 variables
c [simplification-4] removed 9 variables 0.1% (12300 remain 94%)
c [simplification-4] removed 175 irredundant clauses 0.1% (273211 remain 89%)
c [simplification-4] maximum reduction of 0% = max (0%, 0%)
c [simplification-4] full geometric conflict interval increment 20000
c [simplification-4] new conflict interval 29000
c [simplification-4] penalized conflict interval 29000 = 1 * 29000
c [simplification-4] hard conflict limit 58500 (soft 44000 + delta 14500)
c [simplification-4] new conflict limit 44000 (hard 58500)
c 
c [simplification-5] limit 44000 conflicts (hard 58500) hit after 44000 conflicts
c [quatres-3] found 36655 quaternary clauses 13% in total
c [quatres-3-1] added 58 double-self-subsuming ternary resolvents
c [quatres-3-2] added 268 single-self-subsuming ternary resolvents
c [quatres-3-2] added 422 quaternary resolvents
c [ternres-3] limit 4000000 with penalty 0 = 0 + 0
c [ternres-3] all 12300 free variables schedulable
c [ternres-3] 103 ternary resolvents (2 bin, 101 trn)
c [ternres-3] fully completed ternary resolution
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] extracted 4 xors of average arity 3.0
c [gauss-2] connected 12 occurrences of 3 variables (average 4.0)
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 [transred-3] limit 947025 with penalty 0 = 0 + 0
c [transred-3] removed 0 transitive binary clauses
c [cce-3] limit of 15000000 steps penalty 1 = 1 + 0
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] allowing another 7500000 steps for small clauses
c [cce-3-1] scheduling 766 clauses = 310 binary + 456 ternary
c [cce-3-1] tried to eliminate 766 small clauses 100%
c [cce-3-1] eliminated 19 ternary clauses 4%
c [cce-3-1] eliminated 19 small clauses 2%
c [cce-3-1] eliminated 19 small clauses in 7726248 steps
c [cce-3-1] completed small round (ACCE)
c [cce-3-1] eliminated 19 covered clauses in round 1
c [cce-3-2] incomplete large round (ACCE)
c [cce-3-2] allowing another 3636877 steps for small clauses
c [cce-3-2] scheduling 747 clauses = 310 binary + 437 ternary
c [cce-3-2] tried to eliminate 747 small clauses 100%
c [cce-3-2] completed small round (ACCE)
c [cce-3-2] eliminated 0 covered clauses in round 2
c [cce-3] eliminated 19 covered clauses in TOTAL during 2 rounds
c [cce-3] 19 < 1/100 * 273210 = 2732 considered unsuccessful
c [elim-4] scheduling all variables this time
c [elim-4] scheduled 12300 variables 100%
c [elim-4] boosting limit by 20
c [elim-4] limit of 200000000 steps penalty 1 = 1 + 0
c [elim-4] rescheduling of touched variables disabled
c [elim-4] incomplete 747 not tried 6% in round 1
c [elim-4] transition to [ all 1 rem 1 ] state
c [elim-4] eliminated 51 = 0% variables out of 12300 scheduled
c [elim-4] 51 < 1/100 * 12300 = 123 considered unsuccessful
c [sweep-4] limit 1000000 penalty 0 = 0 + 0
c [sweep-4-1] 1963 pos 40.8% + 2847 neg 59.2% = 4810 sched 39.3% ret 7439
c [sweep-4-1] 1000486 steps 636 queries 645.17 avg class size
c [sweep-4-1] 16285 decisions 635 SAT calls 34.82 avg env size
c [sweep-4-1] 2282 variables remain 19% (9966 retained 81%)
c [decomp-15] removed 1 variables
c [sweep-4-1] removed 1 vars (0 failed, 0 eqs, 1 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 1 vars in TOTAL (1 rounds, 635 queries)
c [phase-count-5] 268452 negative 99.2% of 270513 except 2061 0.8%
c [phase-count-5] 266940 positive 98.7% of 270513 except 3573 1.3%
c [phase-5] phase bias: 18 positive 100%, 0 negative 0%
c [score-distribution-5] 4662 pos 38.06%, 5806 min 47.40%, 1780 zero 14.53%
c [score-distribution-5] 1859 different 15.18% out of total 12248 variables
c [simplification-5] removed 52 variables 0.4% (12248 remain 94%)
c [simplification-5] removed 2698 irredundant clauses 1.0% (270513 remain 88%)
c [simplification-5] maximum reduction of 1% = max (0%, 1%)
c [simplification-5] geometric conflict interval increment 14500 = 29000 / 2
c [simplification-5] new conflict interval 43500
c [simplification-5] penalized conflict interval 43500 = 1 * 43500
c [simplification-5] hard conflict limit 109250 (soft 87500 + delta 21750)
c [simplification-5] new conflict limit 87500 (hard 109250)
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 -   25.4   12248   270513     79163   26042   3157   163   10   385   24   3%    713  146   12    6  203%
c 
c [simplification-6] limit 87500 conflicts (hard 109250) hit after 87500 conflicts
c [quatres-4] found 38935 quaternary clauses 14% in total
c [quatres-4-1] removed 4 duplicate quaternary clauses
c [quatres-4-1] added 52 double-self-subsuming ternary resolvents
c [quatres-4-2] added 303 single-self-subsuming ternary resolvents
c [quatres-4-2] added 512 quaternary resolvents
c [ternres-4] limit 4000000 with penalty 0 = 0 + 0
c [ternres-4] all 12248 free variables schedulable
c [ternres-4] 52 ternary resolvents (6 bin, 46 trn)
c [ternres-4] fully completed ternary resolution
c [card-3] limit 500000 penalty 2 = 2 + 0
c [card-3] no at-most-one constraint found
c [card-3] found 5 at-most-two constraints of average size 4.0
c [card-3] using previous limit 500000 for elimination
c [card-3] 5 out of 5 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [decomp-16] removed 1 variables
c [simpleprobe-3] 5422 schedulable variables 44%
c [simpleprobe-3] limit 5196893 penalty 1 = 1 + 0
c [decomp-17] removed 1 variables
c [simpleprobe-3] 5427 variables remain 44% (6819 retained 56%)
c [simpleprobe-3] removed 1 variables, found 3 hbrs, 0 units
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 10000000 penalty 0 = 0 + 0
c [sweep-5-1] 1005 pos 44.0% + 1277 neg 56.0% = 2282 sched 18.6% ret 9964
c [sweep-5-1] 749118 steps 1046 queries 223.46 avg class size
c [sweep-5-1] 15803 decisions 1046 SAT calls 20.58 avg env size
c [sweep-5-1] fully completed sweeping round
c [sweep-5-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-5-2] 5738 pos 46.9% + 6508 neg 53.1% = 12246 sched 100.0% ret 0
c [sweep-5-2] 3356796 steps 1899 queries 576.90 avg class size
c [sweep-5-2] 38097 decisions 1897 SAT calls 28.02 avg env size
c [sweep-5-2] fully completed sweeping round
c [decomp-19] removed 1 variables
c [sweep-5-2] removed 1 vars (0 failed, 1 eqs, 3 impls)
c [sweep-5-3] 5738 pos 46.9% + 6507 neg 53.1% = 12245 sched 100.0% ret 0
c [sweep-5-3] 3284654 steps 1866 queries 594.65 avg class size
c [sweep-5-3] 38489 decisions 1866 SAT calls 28.74 avg env size
c [sweep-5-3] fully completed sweeping round
c [sweep-5-3] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-5] 1 < 1/1000 * 12246 = 12 considered unsuccessful
c [sweep-5] removed 1 vars in TOTAL (3 rounds, 4808 queries)
c [score-distribution-6] 6636 pos 54.19%, 5222 min 42.65%, 387 zero 3.16%
c [score-distribution-6] 1867 different 15.25% out of total 12245 variables
c [simplification-6] removed 3 variables 0.0% (12245 remain 94%)
c [simplification-6] removed 8 irredundant clauses 0.0% (270505 remain 88%)
c [simplification-6] maximum reduction of 0% = max (0%, 0%)
c [simplification-6] full geometric conflict interval increment 43500
c [simplification-6] new conflict interval 87000
c [simplification-6] penalized conflict interval 87000 = 1 * 87000
c [simplification-6] hard conflict limit 218000 (soft 174500 + delta 43500)
c [simplification-6] new conflict limit 174500 (hard 218000)
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 -   37.2   12245   270505    141476   38421   4278   232   12   348   25   4%    904   43   13    9  154%
c 
c [simplification-7] limit 174500 conflicts (hard 218000) hit after 174501 conflicts
c [quatres-5] found 43310 quaternary clauses 15% in total
c [quatres-5-1] removed 3 duplicate quaternary clauses
c [quatres-5-1] added 77 double-self-subsuming ternary resolvents
c [quatres-5-2] added 469 single-self-subsuming ternary resolvents
c [quatres-5-2] added 460 quaternary resolvents
c [ternres-5] limit 5260509 with penalty 0 = 0 + 0
c [ternres-5] all 12245 free variables schedulable
c [ternres-5] 188 ternary resolvents (11 bin, 177 trn)
c [ternres-5] fully completed ternary resolution
c [decomp-21] removed 1 variables
c [unhide-4] limit 263025 with penalty 2 = 2 + 0
c [unhide-4-4] 0 units, 0 failed, 271 tauts, 0 hbrs, 401 literals
c [transred-4] limit 1000000 with penalty 1 = 1 + 0
c [transred-4] removed 11 transitive binary clauses
c [block-3] scheduling all variables this time
c [block-3] scheduled 12244 variables 100%
c [block-3] limit of 13151272 steps penalty 2 = 2 + 0
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 94 blocked clauses
c [block-3] 94 < 1/100 * 270502 = 2705 considered unsuccessful
c [bca-3] limit of 10000000 steps and 541316 added (scaled 2)
c [bca-3] 5661 out of 24472 literals actually usable 23%
c [bca-3] added 0 blocked clauses in 114422 steps
c [score-distribution-7] 4877 pos 39.86%, 7027 min 57.43%, 331 zero 2.71%
c [score-distribution-7] 2382 different 19.47% out of total 12235 variables
c [simplification-7] removed 10 variables 0.1% (12235 remain 94%)
c [simplification-7] removed 97 irredundant clauses 0.0% (270408 remain 88%)
c [simplification-7] maximum reduction of 0% = max (0%, 0%)
c [simplification-7] full geometric conflict interval increment 87000
c [simplification-7] new conflict interval 174000
c [simplification-7] penalized conflict interval 174000 = 1 * 174000
c [simplification-7] hard conflict limit 435501 (soft 348501 + delta 87000)
c [simplification-7] new conflict limit 348501 (hard 435501)
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 -   48.5   12235   270408    204520   45441   5023   256   12   401   26   3%    978   44   14   10  132%
c i   54.4   12234   270408    252047   87553   5231   258   13   493   31   3%   1002   98   12   11  103%
c -   56.7   12234   270408    270941   56585   5359   259   12   518   27   2%  -1991   88   11   11   97%
c -   64.5   12234   270408    339773   70124   5781   277   10   654   28   2%    -31  159    9   12   81%
c 
c [simplification-8] limit 348501 conflicts (hard 435501) hit after 348502 conflicts
c [quatres-6] found 49622 quaternary clauses 15% in total
c [quatres-6-1] removed 8 duplicate quaternary clauses
c [quatres-6-1] added 122 double-self-subsuming ternary resolvents
c [quatres-6-2] added 701 single-self-subsuming ternary resolvents
c [quatres-6-2] added 557 quaternary resolvents
c [ternres-6] limit 9628074 with penalty 0 = 0 + 0
c [ternres-6] all 12234 free variables schedulable
c [ternres-6] 69 ternary resolvents (4 bin, 65 trn)
c [ternres-6] fully completed ternary resolution
c [gauss-3] limit 500000 penalty 2 = 2 + 0
c [gauss-3] extracted 1 xors of average arity 2.0
c [gauss-3] connected 2 occurrences of 2 variables (average 1.0)
c [gauss-3] limit 500000 penalty 2 = 2 + 0
c [gauss-3] fully completed
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-22] removed 1 variables
c [treelook-3] limit 481403 penalty 1 = 1 + 0 boost 1
c [treelook-3] scheduled 2112 literals 9%
c [treelook-3] scheduling used 481449 steps
c [treelook-3] not fully scheduled
c [treelook-3] limit 481403 penalty 1 = 1 + 0 boost 1
c [treelook-3] used 481577 steps
c [treelook-3] 403 literals remain 2%
c [treelook-3] 397 variables remain to probed next time 3%
c [treelook-3] removed 0 variables, found 9 hbrs
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 4 transitive binary clauses
c [cce-4] boosting limit by 10
c [cce-4] limit of 120350930 steps penalty 2 = 2 + 0
c [cce-4-1] eliminated 75 clauses out of 77135 (0%) of length 7
c [cce-4-1] eliminated 1049 clauses out of 88836 (1%) of length 6
c [cce-4-1] incomplete large round (ATE)
c [cce-4-1] eliminated 1124 large clauses in 120350970 steps
c [cce-4-1] allowing another 60175485 steps for small clauses
c [cce-4-1] scheduling 10071 clauses = 328 binary + 9743 ternary
c [cce-4-1] tried to eliminate 10071 small clauses 100%
c [cce-4-1] eliminated 5 binary clauses 2%
c [cce-4-1] eliminated 29 ternary clauses 0%
c [cce-4-1] eliminated 34 small clauses 0%
c [cce-4-1] eliminated 34 small clauses in 63793095 steps
c [cce-4-1] completed small round (ATE)
c [cce-4-1] eliminated 1158 covered clauses in round 1
c [cce-4-2] incomplete large round (ATE)
c [cce-4-2] allowing another 28278918 steps for small clauses
c [cce-4-2] scheduling 10038 clauses = 323 binary + 9715 ternary
c [cce-4-2] tried to eliminate 10038 small clauses 100%
c [cce-4-2] eliminated 1 ternary clauses 0%
c [cce-4-2] eliminated 1 small clauses 0%
c [cce-4-2] eliminated 1 small clauses in 31870365 steps
c [cce-4-2] completed small round (ATE)
c [cce-4-2] eliminated 1 covered clauses in round 2
c [cce-4-3] incomplete large round (ATE)
c [cce-4-3] allowing another 12343748 steps for small clauses
c [cce-4-3] scheduling 10037 clauses = 323 binary + 9714 ternary
c [cce-4-3] tried to eliminate 10037 small clauses 100%
c [cce-4-3] completed small round (ATE)
c [cce-4-3] eliminated 0 covered clauses in round 3
c [cce-4] eliminated 1159 covered clauses in TOTAL during 3 rounds
c [cce-4] 1159 < 1/100 * 270395 = 2703 considered unsuccessful
c [elim-5] 747 variables 6% will be scheduled this time
c [elim-5] scheduled 747 variables 6%
c [elim-5] limit of 48140372 steps penalty 2 = 2 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5-1] no variable eliminated in round 1 in 44324483 steps
c [elim-5] fully completed in 1 rounds
c [elim-5] transition to [ all 0 rem 0 ] state
c [elim-5] eliminated 0 = 0% variables out of 747 scheduled
c [sweep-6] limit 1444211 penalty 1 = 1 + 0
c [sweep-6-1] 6083 pos 49.7% + 6150 neg 50.3% = 12233 sched 100.0% ret 0
c [sweep-6-1] 1446546 steps 453 queries 1576.38 avg class size
c [sweep-6-1] 16755 decisions 452 SAT calls 51.54 avg env size
c [sweep-6-1] 7808 variables remain 64% (4425 retained 36%)
c [sweep-6-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-6] removed 0 vars in TOTAL (1 rounds, 452 queries)
c [score-distribution-8] 4477 pos 36.60%, 7700 min 62.94%, 56 zero 0.46%
c [score-distribution-8] 1995 different 16.31% out of total 12233 variables
c [simplification-8] removed 1 variables 0.0% (12233 remain 94%)
c [simplification-8] removed 1219 irredundant clauses 0.5% (269189 remain 87%)
c [simplification-8] maximum reduction of 0% = max (0%, 0%)
c [simplification-8] full geometric conflict interval increment 174000
c [simplification-8] new conflict interval 348000
c [simplification-8] penalized conflict interval 348000 = 1 * 348000
c [simplification-8] hard conflict limit 870502 (soft 696502 + delta 174000)
c [simplification-8] new conflict limit 696502 (hard 870502)
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 -   76.6   12233   269189    409535   83551   6975   307   12   529   29   2%    660  -17   13   12  109%
c -   84.0   12233   269189    474322   93544   7227   313   14   497   30   3%    889  -24   15   13  119%
c -   90.8   12233   269189    537318  103281   7494   321   13   590   30   2%    972   53   16   14  116%
c -   96.1   12233   269189    596139  113692   7759   326   14   579   31   2%   1003  -10   14   14   99%
c -  100.7   12233   269189    650015  118673   7942   328   14   609   31   2%   1015   24   14   14   95%
c 
c [simplification-9] limit 696502 conflicts (hard 870502) hit after 696503 conflicts
c [quatres-7] found 60681 quaternary clauses 16% in total
c [quatres-7-1] removed 15 duplicate quaternary clauses
c [quatres-7-1] added 134 double-self-subsuming ternary resolvents
c [quatres-7-2] added 1193 single-self-subsuming ternary resolvents
c [quatres-7-2] added 748 quaternary resolvents
c [ternres-7] limit 17245545 with penalty 0 = 0 + 0
c [ternres-7] all 12233 free variables schedulable
c [ternres-7] 36 ternary resolvents (4 bin, 32 trn)
c [ternres-7] fully completed ternary resolution
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 7 transitive binary clauses
c [score-distribution-9] 3804 pos 31.10%, 8417 min 68.81%, 12 zero 0.10%
c [score-distribution-9] 1836 different 15.01% out of total 12233 variables
c [simplification-9] removed 0 variables 0.0% (12233 remain 94%)
c [simplification-9] removed 0 irredundant clauses 0.0% (269189 remain 87%)
c [simplification-9] maximum reduction of 0% = max (0%, 0%)
c [simplification-9] full geometric conflict interval increment 348000
c [simplification-9] new conflict interval 696000
c [simplification-9] penalized conflict interval 696000 = 1 * 696000
c [simplification-9] hard conflict limit 1740503 (soft 1392503 + delta 348000)
c [simplification-9] new conflict limit 1392503 (hard 1740503)
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.0   12233   269189    710685  122781   9594   326   14   544   32   3%   1020  -17   13   14   99%
c -  113.2   12233   269189    774498  133020   9738   327   15   572   32   3%   1023    7   15   14  111%
c -  119.2   12233   269189    832499  139500   9798   327   16   547   33   3%   1023  -21   18   15  123%
c -  124.4   12233   269189    888797  144601   9877   328   15   588   33   3%   1024    8   15   15   97%
c -  130.9   12233   269189    952609  150678  10193   328   14   793   34   2%   1024  170   13   14   91%
c -  137.0   12233   269189   1016566  158657  10380   329   16   562   35   3%   1024  -69   17   15  117%
c -  145.1   12233   269189   1082806  164720  10666   331   13   590   35   2%   1024  -48   10   14   69%
c -  153.5   12233   269189   1153704  171580  11032   332   15   625   36   2%   1024    4   16   15  106%
c -  164.4   12233   269189   1229181  179958  11377   333   15   504   37   3%   1024 -106   14   15   97%
c -  172.8   12233   269189   1303167  192653  11498   333   17   544   37   3%   1024  -41   18   16  111%
c -  181.1   12233   269189   1371265  199727  11672   333   17   629   38   3%   1024   27   14   16   85%
c 
c [simplification-10] limit 1392503 conflicts (hard 1740503) hit after 1392875 conflicts
c [quatres-8] found 79755 quaternary clauses 18% in total
c [quatres-8-1] removed 47 duplicate quaternary clauses
c [quatres-8-1] added 131 double-self-subsuming ternary resolvents
c [quatres-8-2] added 1394 single-self-subsuming ternary resolvents
c [quatres-8-2] added 598 quaternary resolvents
c [ternres-8] limit 34979016 with penalty 0 = 0 + 0
c [ternres-8] all 12233 free variables schedulable
c [ternres-8] 20 ternary resolvents (2 bin, 18 trn)
c [ternres-8] fully completed ternary resolution
c [card-4] limit 2186188 penalty 3 = 3 + 0
c [card-4] found 3 at-most-one constraints of average size 3.0
c [card-4] found 33 at-most-two constraints of average size 4.1
c [card-4] using previous limit 2186188 for elimination
c [card-4] 33 out of 36 constraints (92%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [basicprobe-3] limit 87447540 penalty 1 = 1 + 0
c [basicprobe-3-0] 786 sched 6%, 0 failed, 0 lifted, 3 hbrs
c [basicprobe-3-1] 786 sched 6%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-3-1] fully completed probing
c [basicprobe-3-1] removed 0 variables, found 3 hbrs
c [bate-2] eliminated 14 asymmetric tautologies during probing
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 4 transitive binary clauses
c [score-distribution-10] 5995 pos 49.01%, 6238 min 50.99%, 0 zero 0.00%
c [score-distribution-10] 3072 different 25.11% out of total 12233 variables
c [simplification-10] removed 0 variables 0.0% (12233 remain 94%)
c [simplification-10] removed 14 irredundant clauses 0.0% (269175 remain 87%)
c [simplification-10] maximum reduction of 0% = max (0%, 0%)
c [simplification-10] full geometric conflict interval increment 696000
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 2892875 (soft 2392875 + delta 500000)
c [simplification-10] new conflict limit 2392875 (hard 2892875)
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 -  189.9   12233   269175   1438378  205807  13212   334   18   603   39   3%   1024   11   18   17  107%
c -  197.7   12233   269175   1504661  212086  13284   334   18   626   39   3%   1024   17   21   17  122%
c -  206.2   12233   269175   1570796  216395  13373   334   17   593   39   3%   1024  -20   17   17   98%
c 1  214.0   12233   269175   1626523  267939  13444   334   16   536   55   3%   1024  -84    8   17   47%
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: 16 basic ate = 15 trn 94% + 1 lrg 6% in 2 updates
c bcas: 3 count, 0 added (2 skipped), 425362 steps
c bkwd: tried 3692 clauses, 7331 lits, 1.99 lits/clause
c bkwd: checked 408338 occs, 110.60 occs/clause, 55.70 occs/lit
c bkwd: subsumed 0 binary, 2 ternary, 5 large
c bkwd: strengthened 0 binary, 1 ternary (100% self), 75 large (0% self)
c blkd: 3 bces, 1498 removed, 15601605 resolutions, 27044296 steps
c blkd: 178 blocking literals 1%, 17 pure
c bump: 1497593 bumped seen, 48531233 lits 32.4 on average
c card: 4 count, 0 units, 0 am1, 6277912 steps
c card: 0 rescheduled, 0 eliminated, 0 resolved, 1453 subsumed
c card: 6 at-most-one constraints found, average size 3.00
c card: 6 at-most-one constraints used 100%, average size 3.00
c card: 48 at-most-two constraints found, average size 4.06
c card: 45 at-most-two constraints used 94%, average size 4.07
c cces: 4 cces, 10502 eliminated, 10502 ate 100%, 0 abce 0%
c cces: 0 probed, 0 lifted, 0 failed
c cces: 0 cached, 0 rsz, 0 cols 0%, 0 srch, 0 hits 0%
c clls: 1 sat, 0 simp, 0 freeze, 0 melt
c clls: 3616992 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 44 gcs, 0 rescored clauses, 787 rescored vars
c dcps: 27 decompositions, 35 equivalent 0%
c deco: 54 decision-only clauses 0%, 52% reduction
c decs: 33440890 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c dsch: 79311051 push, 79309528 pop (79309528 dec 100%)
c dsch: 1295218724 swaps, 0 down, 277064200 up
c elms: 5 elims, 744 eliminated 6%, 1 pure 0%
c elms: 7 rounds, 1.4 rounds/bve
c elms: 723 small 97%, 3 large 0%
c elms: 2233 tried small, 723 succeeded 32%, 1510 failed 68%
c elms: 17614 subsumed, 9664 strengthened, 0 blocked
c elms: 2356724 copies, 6602961 resolutions, 595332 ipos
c elms: 614525 subchks, 373649 strchks
c gaus: 3 extractions, 1082 extracted, 5.0 size, 5 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 7000346 steps, 3500173 extr 50%, 19515 elim 0%
c glue: 14.0 orig avg, 14.0 real avg, 2.9 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 91 = 5 simple 5% + 75 trn 82% + 11 lrg 12%, 54 sub 59%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 1497593 clauses, 23.1 length
c lrnd: 34607736 lits = 35463470 orig - 855734 removed 2%
c lrnd: 578919 uips 39%, 687940 flips 46%
c mins: 1219850 mins 81%, 99 bin 0%, 277446 size 19%
c mins: 18589460 poisoned searches, 1314633 hits, 7% hit rate
c mins: 48972328 used twice searches, 14206956 hits, 29% hit rate
c move: moved 1431, 13 bin 1%, 1418 trn 99%
c otfs: 136896 driving 48%, 148354 restarting 52%
c otfs: str 285250, 279753 red 98%, 5497 irr 2%
c otfs: str 285250, 0 bin 0%, 130 trn 0%, 285120 lrg 100%
c otfs: sub 2591, 2591 red 100%, 0 irr 0%
c otfs: sub 2591, 0 bin 0%, 31 trn 1%, 2560 lrg 99%
c phas: 5 computed, 19537 set, 18 pos (0%), 19519 neg (100%)
c prbs: 3 basic, 8468 probed, 2 failed, 0 lifted
c prbs: 3 simple, 25157 probed, 4 failed, 1 eqs
c prbs: 3 treelook, 3761 probed, 1 failed, 0 lifted
c prom: 121563 locked 40% out of 306414 tried
c prps: 194581483 props, 6 props/dec
c prps: 100% srch, 0% simp, 0% lkhd
c quat: 8 count, 3805 quat, 4498 self1, 658 self2, 82 dup
c redc: 127 clauses 0%, 310994 tried 19%, 0 sat 0%
c redc: 131 lits 0%, 2259830 tried 6%, 0 sat 0%
c redc: 17 times jump level reduced, 57.1 levels on average
c reds: 24 count, 67771.8 conflicts per reduce
c reds: 0 memlim 0%, 24 arith 100%
c reds: 723281 collected 61%, 470935 retired 39%
c rmbd: 10 removed, 0 red 0%
c rsts: 30434 restarts 100%, 0 skipped 0%
c rsts: 0 saturating 0%, 0 reuse 0%
c rsts: 0 kept 0.0% average 0.0%
c scnc: 1 count, 1.200 min (200/1000), 1.200 max (200/1000)
c simp: 10 count, 10 confs 100%, 0 vars 0%
c simp: 0 its 0%, 0 bin 0%, 0 trns 0%
c subl: 1497593 count (1003129 tried 0.7), 23195 sub out of 1493905 (1.6%)
c swps: 6 count, 8 rounds, 7392 queries (924.0/round)
c swps: 7393 sat calls, 2 unsat (1.1% success rate)
c swps: 154440 decisions 20.9, 7966 conflicts 1.1
c swps; 838.3 avg class size, 28.7 avg environment size
c swps: 0 failed, 5 impls, 1 equivs
c swp0: 2460 type 0 queries, 12 unsat (0.5%), 2459 sat (100.0%)
c swp1: 4932 type 1 queries, 66 unsat (1.3%), 4932 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: 69878733 calls to obtain time
c tops: 396 fixed 3%, 1 its, 1626523.00 confs/it
c trds: 7 transitive reductions, 33 removed, 0 failed
c trds: 169493 nodes, 3672 edges, 4411 steps
c trim: 328205 words, 1.3 MB
c trnr: 8 count, 47 bin, 715 trn, 14844403 steps
c unhd: 4 count, 4 rounds, 2124727 steps
c unhd: 0 non-trivial sccs of average size 0.0
c unhd: 0 units, 0 bin, 0 trn, 0 lrg
c unhd: 9 failed, 9 stamp, 0 lits, 0 bin, 0 trn, 0 lrg
c unhd: 1054 tauts, 0 bin 0%, 806 trn 76%, 243 lrg 23%
c unhd: 1054 tauts, 5 stamp 0%, 550 red 52%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 455 str, 0 bin 0%, 38 trn 8%, 417 lrg 92%, 386 red 85%
c vars: 12233 remaining 91% and 1175 removed 9% out of 13408
c vars: 396 fixed 3%, 744 eliminated 6%, 35 equivalent 0%
c vsts: 4185923704 visits, 100% srch, 0% simp, 0% lkhd
c vsts: 21.5 search visits per propagation, 2569.6 per conflict
c wchs: 1811822750 pushed, 18292404 enlarged, 231 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all        1497710        723281        470935      32248792       4230941        614045
c 
c  0 0        222927  15      1710   0         0   0  26319915  82<  2518829  60    304123  50     6.0
c  1 5        182878  12     70709  10     95535  20   3129298  10    378218   9<    67261  11<    0.6
c  2 6        262617  18    136396  19    109868  23   1445589   4    423974  10     92722  15     0.8
c  3 9        292596  20<   176992  24    100669  21<   598263   2    366470   9     71660  12     1.3
c  4 14       243963  16    163502  23<    67274  14    366659   1    287792   7     49339   8     1.6
c  5 21       151382  10     96963  13     44359   9    207069   1    150199   4     19637   3     1.4
c  6 30        73557   5     42176   6     25536   5     96264   0     59835   1      5792   1     1.0
c  7 41        35499   2     19099   3     13786   3     45456   0     25293   1      1927   0     0.7
c  8 54        17232   1      8762   1      7155   2     21811   0     11382   0       824   0     0.6
c  9 69         8317   1      4039   1      3549   1     10252   0      5152   0       382   0     0.4
c 10 86         5420   0      2375   0      2565   1      6623   0      3034   0       259   0     0.4
c 11 126        1168   0       485   0       588   0      1401   0       629   0        89   0     0.2
c 12 230          63   0        37   0        23   0        77   0        74   0        23   0     0.1
c 13 534          91   0        36   0        28   0       115   0        60   0         7   0     0.1
c 
c avg                  2.9           3.5           3.1           0.4           1.2           1.3
c std                  2.0           1.7           1.9           1.0           1.7           1.7
c 
c   30.634  14% decide
c    4.813   2% elim
c    4.721   2% cce
c    3.977   2% bump
c    2.583   1% sweep
c    2.084   1% probe
c    1.940   1% block
c 
c    3.061 < 1% rest (below)
c 
c    1.227   1% quatres
c    0.547   0% gauss
c    0.449   0% bca
c    0.333   0% rescore
c    0.205   0% unhide
c    0.158   0% card
c    0.108   0% ternres
c    0.035   0% transred
c    0.000   0% locs
c    0.000   0% queuesort
c ==================================
c    1.301   1% preprocessing     6%
c   19.789   9% inprocessing     94%
c ==================================
c   21.090  10% simplifying
c  192.920  90% search
c ==================================
c  214.012 100% all
c 
c       1626523 conflicts,        7600.2 confs/sec
c          3185 ternaries,         510.7 confs/ternary
c           127 binaries,        12807.3 confs/binary
c             1 iterations,    1626523.0 confs/iteration
c 
c            24 reductions,          0.1 redus/sec,  67771.8 confs/reduction
c         30434 restarts,          142.2 rests/sec,     53.4 confs/restart
c      33440890 decisions,      156257.4 decis/sec,     20.6 decis/conflict
c     194581483 propagations,   909209.9 props/sec,      5.8 props/decision
c 
c 214.0 seconds, 75.0 MB
c launch: done
