c launch: /data/cnf/sc2014/app/MD5-27-4.cnf.bz2
c host: atom25
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/MD5-27-4.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/MD5-27-4.cnf.bz2
c no embedded options
c found 'p cnf 7965 59726' header
c read 7965 variables, 59726 clauses, 232352 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 7957 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    7957    59536         0       0      0     0    0     0    3   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 4 at-most-one constraints of average size 3.0
c [card-1] found 120 at-most-two constraints of average size 4.0
c [card-1] using previous limit 2000000 for elimination
c [card-1] 124 out of 124 constraints (100%) meet size limits
c [card-1] found 7 units
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 34 variables
c [simpleprobe-1] all 7931 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] fully completed simple probing
c [simpleprobe-1] removed 13 variables, found 318 hbrs, 4 units
c [unhide-1] limit 100000 with penalty 0 = 0 + 0
c [unhide-1-1] 0 units, 0 failed, 72 tauts, 0 hbrs, 64 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 7918 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 2529 variables 32% in round 1 in 8852101 steps
c [elim-1-1] backward subsumption/strengthening limit 8852100
c [elim-1-1-1] backward checking 5371 touched variables 68%
c [elim-1-1-1] fully completed backward checking in 1 rounds
c [elim-1-1] subsumed 95 and strengthened 192 clauses in 1172230 steps
c [elim-1-1] rescheduled 282 variables 4% by backward subsumption
c [elim-1-2] eliminated 56 variables 1% in round 2 in 751194 steps
c [elim-1-2] backward subsumption/strengthening limit 751100
c [elim-1-2-1] backward checking 290 touched variables 4%
c [elim-1-2-1] fully completed backward checking in 1 rounds
c [elim-1-2] subsumed 53 and strengthened 242 clauses in 340317 steps
c [elim-1-2] rescheduled 242 variables 3% by backward subsumption
c [elim-1-3] eliminated 2 variables 0% in round 3 in 706632 steps
c [elim-1-3] backward subsumption/strengthening limit 706600
c [elim-1-3-1] backward checking 91 touched variables 1%
c [elim-1-3-1] fully completed backward checking in 1 rounds
c [elim-1-3] subsumed 0 and strengthened 0 clauses in 169064 steps
c [elim-1] fully completed in 3 rounds
c [elim-1] transition to [ all 0 rem 0 ] state
c [elim-1] eliminated 2587 = 33% variables out of 7918 scheduled
c [phase-count-1] 54020 negative 99.1% of 54499 except 479 0.9%
c [phase-count-1] 52313 positive 96.0% of 54499 except 2186 4.0%
c [phase-count-1] less non-negative clauses 479 than limit 5400 (10.0%)
c [phase-count-1] non-pos/non-neg = 2186/479 = 4.56 >= 2.00 = 200/100
c [lucky-phase-1] forcing lucky phase -1
c [phase-1] phase bias: 0 positive 0%, 5331 negative 100%
c [score-distribution-1] 0 pos 0.00%, 0 min 0.00%, 5331 zero 100.00%
c [score-distribution-1] 1 different 0.02% out of total 5331 variables
c [simplification-1] removed 2626 variables 33.0% (5331 remain 67%)
c [simplification-1] removed 5037 irredundant clauses 8.5% (54499 remain 92%)
c [simplification-1] maximum reduction of 33% = max (33%, 8%)
c [simplification-1] large reduction 33% >= 5% limit
c [simplification-1] next conflict interval 1000 = 2000/2
c [simplification-1] penalized conflict interval 1000 = 1 * 1000
c [simplification-1] hard conflict limit 11000 (soft 1000 + delta 10000)
c [simplification-1] new conflict limit 1000 (hard 11000)
c 
c [simplification-2] limit 1000 conflicts (hard 11000) hit after 1000 conflicts
c [simpleprobe-2] all 5331 free variables schedulable
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [simpleprobe-2] 1258 variables remain 24% (4073 retained 76%)
c [simpleprobe-2] removed 0 variables, found 23 hbrs, 0 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 10662 literals 100%
c [treelook-1] scheduling used 262165 steps
c [treelook-1] scheduled completely
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 300062 steps
c [treelook-1] 7599 literals remain 71%
c [treelook-1] 5274 variables remain to probed next time 99%
c [treelook-1] removed 0 variables, found 52 hbrs
c [basicprobe-1] limit 1000000 penalty 0 = 0 + 0
c [basicprobe-1-0] 602 sched 11%, 0 failed, 0 lifted, 15 hbrs
c [basicprobe-1-1] 602 sched 11%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-1-1] fully completed probing
c [basicprobe-1-1] removed 0 variables, found 15 hbrs
c [block-1] scheduling all variables this time
c [block-1] scheduled 5331 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 243 blocked clauses
c [block-1] 243 < 1/100 * 54499 = 544 considered unsuccessful
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 60 clauses out of 684 (9%) of length 6
c [cce-1-1] eliminated 6940 clauses out of 21144 (33%) of length 5
c [cce-1-1] eliminated 292 clauses out of 18269 (2%) of length 4
c [cce-1-1] completed large round (ATE)
c [cce-1-1] eliminated 7292 large clauses in 8504506 steps
c [cce-1-1] allowing another 4252253 steps for small clauses
c [cce-1-1] scheduling 12622 clauses = 425 binary + 12197 ternary
c [cce-1-1] tried to eliminate 12622 small clauses 100%
c [cce-1-1] eliminated 1 binary clauses 0%
c [cce-1-1] eliminated 333 ternary clauses 3%
c [cce-1-1] eliminated 334 small clauses 3%
c [cce-1-1] eliminated 334 small clauses in 5896563 steps
c [cce-1-1] completed small round (ATE)
c [cce-1-1] completed small and large (ATE)
c [cce-1-1] eliminated 7626 covered clauses in round 1
c [cce-1-2] eliminated 2 clauses out of 624 (0%) of length 6
c [cce-1-2] eliminated 54 clauses out of 14204 (0%) of length 5
c [cce-1-2] eliminated 65 clauses out of 17977 (0%) of length 4
c [cce-1-2] completed large round (ABCE)
c [cce-1-2] eliminated 121 large clauses in 7585092 steps
c [cce-1-2] allowing another 3792546 steps for small clauses
c [cce-1-2] scheduling 12288 clauses = 424 binary + 11864 ternary
c [cce-1-2] tried to eliminate 12288 small clauses 100%
c [cce-1-2] eliminated 2 ternary clauses 0%
c [cce-1-2] eliminated 2 small clauses 0%
c [cce-1-2] eliminated 2 small clauses in 5475920 steps
c [cce-1-2] completed small round (ABCE)
c [cce-1-2] completed small and large (ABCE)
c [cce-1-2] eliminated 123 covered clauses in round 2
c [cce-1-3] eliminated 28 clauses out of 14150 (0%) of length 5
c [cce-1-3] eliminated 48 clauses out of 17912 (0%) of length 4
c [cce-1-3] completed large round (ACCE)
c [cce-1-3] eliminated 76 large clauses in 8600323 steps
c [cce-1-3] allowing another 4300161 steps for small clauses
c [cce-1-3] scheduling 12286 clauses = 424 binary + 11862 ternary
c [cce-1-3] tried to eliminate 12286 small clauses 100%
c [cce-1-3] eliminated 24 ternary clauses 0%
c [cce-1-3] eliminated 24 small clauses 0%
c [cce-1-3] eliminated 24 small clauses in 6141108 steps
c [cce-1-3] completed small round (ACCE)
c [cce-1-3] completed small and large (ACCE)
c [cce-1-3] eliminated 100 covered clauses in round 3
c [cce-1] eliminated 7849 covered clauses in TOTAL during 3 rounds
c [elim-2] scheduling all variables this time
c [elim-2] scheduled 5314 variables 100%
c [elim-2] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-2] rescheduling of touched variables disabled
c [elim-2-1] eliminated 282 variables 5% in round 1 in 10834225 steps
c [elim-2-1] backward subsumption/strengthening limit 9165775
c [elim-2-1-1] backward checking 706 touched variables 13%
c [elim-2-1-1] fully completed backward checking in 1 rounds
c [elim-2-1] subsumed 3 and strengthened 42 clauses in 160133 steps
c [elim-2-1] rescheduled 82 variables 2% by backward subsumption
c [elim-2-2] eliminated 2 variables 0% in round 2 in 163274 steps
c [elim-2-2] backward subsumption/strengthening limit 163200
c [elim-2-2-1] backward checking 30 touched variables 1%
c [elim-2-2-1] fully completed backward checking in 1 rounds
c [elim-2-2] subsumed 0 and strengthened 0 clauses in 54385 steps
c [elim-2] fully completed in 2 rounds
c [elim-2] transition to [ all 0 rem 0 ] state
c [elim-2] eliminated 284 = 5% variables out of 5314 scheduled
c [bca-1] limit of 10000000 steps and 88048 added (scaled 2)
c [bca-1] 8521 out of 10062 literals actually usable 85%
c [bca-1] added 0 blocked clauses in 33207 steps
c [sweep-1] limit 1000000 penalty 0 = 0 + 0
c [sweep-1-1] 1391 pos 27.7% + 3639 neg 72.3% = 5030 sched 100.0% ret 0
c [sweep-1-1] 720726 steps 966 queries 285.37 avg class size
c [sweep-1-1] 8176 decisions 967 SAT calls 14.99 avg env size
c [sweep-1-1] fully completed sweeping round
c [sweep-1-1] removed 0 vars (0 failed, 0 eqs, 2 impls)
c [sweep-1-2] 1391 pos 27.7% + 3639 neg 72.3% = 5030 sched 100.0% ret 0
c [sweep-1-2] 279613 steps 285 queries 741.53 avg class size
c [sweep-1-2] 2789 decisions 285 SAT calls 16.81 avg env size
c [sweep-1-2] 3568 variables remain 71% (1462 retained 29%)
c [sweep-1-2] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-1] removed 0 vars in TOTAL (2 rounds, 1249 queries)
c [phase-count-2] 43333 negative 99.0% of 43774 except 441 1.0%
c [phase-count-2] 41821 positive 95.5% of 43774 except 1953 4.5%
c [phase-count-2] less non-negative clauses 441 than limit 4300 (10.0%)
c [phase-count-2] non-pos/non-neg = 1953/441 = 4.43 >= 2.00 = 200/100
c [lucky-phase-2] forcing lucky phase -1
c [phase-2] phase bias: 0 positive 0%, 87 negative 100%
c [score-distribution-2] 2442 pos 48.55%, 0 min 0.00%, 2588 zero 51.45%
c [score-distribution-2] 1119 different 22.25% out of total 5030 variables
c [simplification-2] removed 301 variables 5.6% (5030 remain 63%)
c [simplification-2] removed 10725 irredundant clauses 19.7% (43774 remain 74%)
c [simplification-2] maximum reduction of 20% = max (6%, 20%)
c [simplification-2] large reduction 20% >= 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 13000 (soft 3000 + delta 10000)
c [simplification-2] new conflict limit 3000 (hard 13000)
c 
c [simplification-3] limit 3000 conflicts (hard 13000) hit after 3002 conflicts
c [quatres-1] found 17759 quaternary clauses 53% in total
c [quatres-1-1] added 1 double-self-subsuming ternary resolvents
c [quatres-1-2] added 268 single-self-subsuming ternary resolvents
c [quatres-1-2] added 416 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 5030 free variables schedulable
c [ternres-1] 3634 ternary resolvents (43 bin, 3591 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 12 at-most-two constraints of average size 4.0
c [card-2] using previous limit 1000000 for elimination
c [card-2] 14 out of 14 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] generated 1 at-most-one constraints, 0 used 0%
c [card-2] exported 0 binary clauses, 0.0 per/constraint
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 15456 xors of average arity 3.7
c [gauss-1] connected 56584 occurrences of 4498 variables (average 12.6)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-9] removed 1 variables
c [unhide-2] limit 50000 with penalty 1 = 1 + 0
c [unhide-2-2] 0 units, 0 failed, 142 tauts, 0 hbrs, 101 literals
c [transred-1] limit 100000 with penalty 0 = 0 + 0
c [transred-1] removed 18 transitive binary clauses
c [cce-2] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-2-1] eliminated 31 clauses out of 13096 (0%) of length 5
c [cce-2-1] eliminated 54 clauses out of 17066 (0%) of length 4
c [cce-2-1] completed large round (ATE)
c [cce-2-1] eliminated 85 large clauses in 6684102 steps
c [cce-2-1] allowing another 3342051 steps for small clauses
c [cce-2-1] scheduling 984 clauses = 484 binary + 500 ternary
c [cce-2-1] tried to eliminate 984 small clauses 100%
c [cce-2-1] eliminated 4 binary clauses 1%
c [cce-2-1] eliminated 39 ternary clauses 8%
c [cce-2-1] eliminated 43 small clauses 4%
c [cce-2-1] eliminated 43 small clauses in 3440287 steps
c [cce-2-1] completed small round (ATE)
c [cce-2-1] eliminated 128 covered clauses in round 1
c [cce-2-2] completed large round (ATE)
c [cce-2-2] allowing another 3326814 steps for small clauses
c [cce-2-2] scheduling 941 clauses = 480 binary + 461 ternary
c [cce-2-2] tried to eliminate 941 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 128 covered clauses in TOTAL during 2 rounds
c [cce-2] 128 < 1/100 * 43773 = 437 considered unsuccessful
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 5029 variables 100%
c [elim-3] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-3] rescheduling of touched variables disabled
c [elim-3-1] eliminated 250 variables 5% in round 1 in 10213252 steps
c [elim-3-1] backward subsumption/strengthening limit 9786748
c [elim-3-1-1] backward checking 317 touched variables 6%
c [elim-3-1-1] fully completed backward checking in 1 rounds
c [elim-3-1] subsumed 1 and strengthened 20 clauses in 93148 steps
c [elim-3-1] rescheduled 41 variables 1% by backward subsumption
c [elim-3-2] eliminated 3 variables 0% in round 2 in 94093 steps
c [elim-3-2] backward subsumption/strengthening limit 94000
c [elim-3-2-1] backward checking 7 touched variables 0%
c [elim-3-2-1] fully completed backward checking in 1 rounds
c [elim-3-2] subsumed 0 and strengthened 0 clauses in 41495 steps
c [elim-3] fully completed in 2 rounds
c [elim-3] transition to [ all 0 rem 0 ] state
c [elim-3] eliminated 253 = 5% variables out of 5029 scheduled
c [phase-count-3] 41086 negative 98.9% of 41523 except 437 1.1%
c [phase-count-3] 39677 positive 95.6% of 41523 except 1846 4.4%
c [phase-count-3] less non-negative clauses 437 than limit 4100 (10.0%)
c [phase-count-3] non-pos/non-neg = 1846/437 = 4.22 >= 2.00 = 200/100
c [lucky-phase-3] forcing lucky phase -1
c [phase-3] phase bias: 0 positive 0%, 30 negative 100%
c [score-distribution-3] 3204 pos 67.09%, 2 min 0.04%, 1570 zero 32.87%
c [score-distribution-3] 1620 different 33.92% out of total 4776 variables
c [simplification-3] removed 254 variables 5.0% (4776 remain 60%)
c [simplification-3] removed 2251 irredundant clauses 5.1% (41523 remain 70%)
c [simplification-3] maximum reduction of 5% = max (5%, 5%)
c [simplification-3] large reduction 5% >= 5% limit
c [simplification-3] next conflict interval 2000 = 2000/1
c [simplification-3] penalized conflict interval 2000 = 1 * 2000
c [simplification-3] hard conflict limit 15002 (soft 5002 + delta 10000)
c [simplification-3] new conflict limit 5002 (hard 15002)
c 
c [simplification-4] limit 5002 conflicts (hard 15002) hit after 5002 conflicts
c [quatres-2] found 17344 quaternary clauses 53% in total
c [quatres-2-1] added 2 double-self-subsuming ternary resolvents
c [quatres-2-2] added 158 single-self-subsuming ternary resolvents
c [quatres-2-2] added 420 quaternary resolvents
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] all 4776 free variables schedulable
c [ternres-2] 410 ternary resolvents (3 bin, 407 trn)
c [ternres-2] fully completed ternary resolution
c [treelook-2] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-2] scheduled 6185 literals 65%
c [treelook-2] scheduling used 150024 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-2] used 150139 steps
c [treelook-2] 4606 literals remain 48%
c [treelook-2] 2828 variables remain to probed next time 59%
c [treelook-2] removed 0 variables, found 28 hbrs
c [transred-2] limit 114919 with penalty 0 = 0 + 0
c [transred-2] removed 14 transitive binary clauses
c [block-2] scheduling all variables this time
c [block-2] scheduled 4776 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 905 blocked clauses
c [elim-4] scheduling all variables this time
c [elim-4] scheduled 4649 variables 100%
c [elim-4] boosting limit by 20
c [elim-4] limit of 400000000 steps penalty 0 = 0 + 0
c [elim-4] rescheduling of touched variables disabled
c [elim-4-1] eliminated 21 variables 0% in round 1 in 9848325 steps
c [elim-4-1] backward subsumption/strengthening limit 9848300
c [elim-4-1-1] backward checking 47 touched variables 1%
c [elim-4-1-1] fully completed backward checking in 1 rounds
c [elim-4-1] subsumed 0 and strengthened 6 clauses in 38273 steps
c [elim-4-1] rescheduled 10 variables 0% by backward subsumption
c [elim-4-2] eliminated 4 variables 0% in round 2 in 11846 steps
c [elim-4-2] backward subsumption/strengthening limit 11800
c [elim-4-2-1] backward checking 0 touched variables 0%
c [elim-4-2-1] incomplete backward checking 0 remain 0%
c [elim-4-2] subsumed 0 and strengthened 0 clauses in 11801 steps
c [elim-4-2] fully rescheduled 4624 variables 99%
c [elim-4-3] eliminated 13 variables 0% in round 3 in 9809408 steps
c [elim-4-3] backward subsumption/strengthening limit 9809400
c [elim-4-3-1] backward checking 0 touched variables 0%
c [elim-4-3-1] fully completed backward checking in 1 rounds
c [elim-4-3] subsumed 0 and strengthened 0 clauses in 30845 steps
c [elim-4] fully completed in 3 rounds
c [elim-4] transition to [ all 0 rem 0 ] state
c [elim-4] eliminated 38 = 1% variables out of 4649 scheduled
c [elim-4] 38 < 1/100 * 4649 = 46 considered unsuccessful
c [bca-2] limit of 10000000 steps and 81000 added (scaled 2)
c [bca-2] 4399 out of 9224 literals actually usable 48%
c [bca-2] added 0 blocked clauses in 19692 steps
c [sweep-2] limit 500000 penalty 1 = 1 + 0
c [sweep-2-1] 1422 pos 43.9% + 1820 neg 56.1% = 3242 sched 70.3% ret 1369
c [sweep-2-1] 479531 steps 733 queries 193.91 avg class size
c [sweep-2-1] 7329 decisions 736 SAT calls 17.33 avg env size
c [sweep-2-1] fully completed sweeping round
c [sweep-2-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-2-2] 2014 pos 43.7% + 2597 neg 56.3% = 4611 sched 100.0% ret 0
c [sweep-2-2] 20626 steps 27 queries 1488.93 avg class size
c [sweep-2-2] 180 decisions 26 SAT calls 13.19 avg env size
c [sweep-2-2] 4547 variables remain 99% (64 retained 1%)
c [sweep-2-2] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-2] removed 0 vars in TOTAL (2 rounds, 758 queries)
c [phase-count-4] 39821 negative 98.9% of 40250 except 429 1.1%
c [phase-count-4] 38419 positive 95.5% of 40250 except 1831 4.5%
c [phase-count-4] less non-negative clauses 429 than limit 4000 (10.0%)
c [phase-count-4] non-pos/non-neg = 1831/429 = 4.27 >= 2.00 = 200/100
c [lucky-phase-4] forcing lucky phase -1
c [phase-4] phase bias: 0 positive 0%, 6 negative 100%
c [score-distribution-4] 2825 pos 61.27%, 690 min 14.96%, 1096 zero 23.77%
c [score-distribution-4] 1338 different 29.02% out of total 4611 variables
c [simplification-4] removed 165 variables 3.5% (4611 remain 58%)
c [simplification-4] removed 1273 irredundant clauses 3.1% (40250 remain 68%)
c [simplification-4] maximum reduction of 3% = max (3%, 3%)
c [simplification-4] geometric conflict interval increment 5000 = 20000 / 4
c [simplification-4] new conflict interval 5000
c [simplification-4] penalized conflict interval 5000 = 1 * 5000
c [simplification-4] hard conflict limit 20002 (soft 10002 + delta 10000)
c [simplification-4] new conflict limit 10002 (hard 20002)
c 
c [simplification-5] limit 10002 conflicts (hard 20002) hit after 10003 conflicts
c [quatres-3] found 17939 quaternary clauses 52% in total
c [quatres-3-1] added 8 double-self-subsuming ternary resolvents
c [quatres-3-2] added 406 single-self-subsuming ternary resolvents
c [quatres-3-2] added 635 quaternary resolvents
c [ternres-3] limit 4000000 with penalty 0 = 0 + 0
c [ternres-3] all 4611 free variables schedulable
c [ternres-3] 535 ternary resolvents (6 bin, 529 trn)
c [ternres-3] fully completed ternary resolution
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] extracted 5043 xors of average arity 3.0
c [gauss-2] connected 15129 occurrences of 1212 variables (average 12.5)
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 264580 with penalty 0 = 0 + 0
c [transred-3] removed 2 transitive binary clauses
c [block-3] scheduling all variables this time
c [block-3] scheduled 4611 variables 100%
c [block-3] limit of 50000000 steps penalty 0 = 0 + 0
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 30 blocked clauses
c [block-3] 30 < 1/100 * 40250 = 402 considered unsuccessful
c [cce-3] limit of 15000000 steps penalty 1 = 1 + 0
c [cce-3-1] eliminated 50 clauses out of 12235 (0%) of length 5
c [cce-3-1] eliminated 127 clauses out of 15692 (1%) of length 4
c [cce-3-1] completed large round (ACCE)
c [cce-3-1] eliminated 177 large clauses in 7528774 steps
c [cce-3-1] allowing another 3764387 steps for small clauses
c [cce-3-1] scheduling 10535 clauses = 454 binary + 10081 ternary
c [cce-3-1] tried to eliminate 10535 small clauses 100%
c [cce-3-1] eliminated 2 ternary clauses 0%
c [cce-3-1] eliminated 2 small clauses 0%
c [cce-3-1] eliminated 2 small clauses in 5364023 steps
c [cce-3-1] completed small round (ACCE)
c [cce-3-1] eliminated 179 covered clauses in round 1
c [cce-3-2] eliminated 1 clauses out of 12185 (0%) of length 5
c [cce-3-2] completed large round (ACCE)
c [cce-3-2] eliminated 1 large clauses in 7460818 steps
c [cce-3-2] allowing another 3730409 steps for small clauses
c [cce-3-2] scheduling 10533 clauses = 454 binary + 10079 ternary
c [cce-3-2] tried to eliminate 10533 small clauses 100%
c [cce-3-2] completed small round (ACCE)
c [cce-3-2] eliminated 1 covered clauses in round 2
c [cce-3-3] incomplete large round (ACCE)
c [cce-3-3] allowing another 2153493 steps for small clauses
c [cce-3-3] scheduling 10533 clauses = 454 binary + 10079 ternary
c [cce-3-3] tried to eliminate 10533 small clauses 100%
c [cce-3-3] completed small round (ACCE)
c [cce-3-3] eliminated 0 covered clauses in round 3
c [cce-3] eliminated 180 covered clauses in TOTAL during 3 rounds
c [cce-3] 180 < 1/100 * 40220 = 402 considered unsuccessful
c [score-distribution-5] 3020 pos 65.54%, 1177 min 25.54%, 411 zero 8.92%
c [score-distribution-5] 1480 different 32.12% out of total 4608 variables
c [simplification-5] removed 3 variables 0.1% (4608 remain 58%)
c [simplification-5] removed 210 irredundant clauses 0.5% (40040 remain 67%)
c [simplification-5] maximum reduction of 1% = max (0%, 1%)
c [simplification-5] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-5] new conflict interval 15000
c [simplification-5] penalized conflict interval 15000 = 1 * 15000
c [simplification-5] hard conflict limit 35003 (soft 25003 + delta 10000)
c [simplification-5] new conflict limit 25003 (hard 35003)
c 
c [simplification-6] limit of 2523 ternary hit after 2523 ternaries
c [quatres-4] found 19453 quaternary clauses 50% in total
c [quatres-4-1] added 20 double-self-subsuming ternary resolvents
c [quatres-4-2] added 512 single-self-subsuming ternary resolvents
c [quatres-4-2] added 784 quaternary resolvents
c [ternres-4] limit 4000000 with penalty 0 = 0 + 0
c [ternres-4] all 4608 free variables schedulable
c [ternres-4] 610 ternary resolvents (7 bin, 603 trn)
c [ternres-4] fully completed ternary resolution
c [card-3] limit 500000 penalty 2 = 2 + 0
c [card-3] found 3 at-most-one constraints of average size 3.0
c [card-3] found 15 at-most-two constraints of average size 4.0
c [card-3] using previous limit 500000 for elimination
c [card-3] 18 out of 18 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [basicprobe-2] limit 1675700 penalty 1 = 1 + 0
c [basicprobe-2-0] 852 sched 18%, 0 failed, 0 lifted, 39 hbrs
c [basicprobe-2-1] 868 sched 19%, 0 failed, 0 lifted, 3 hbrs
c [basicprobe-2-2] 867 sched 19%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-2-2] fully completed probing
c [basicprobe-2-2] removed 0 variables, found 42 hbrs
c [unhide-3] limit 33514 with penalty 2 = 2 + 0
c [unhide-3-3] 0 units, 0 failed, 5 tauts, 0 hbrs, 134 literals
c [transred-4] limit 670280 with penalty 0 = 0 + 0
c [transred-4] removed 8 transitive binary clauses
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 4608 variables 100%
c [elim-5] limit of 10000000 steps penalty 1 = 1 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5-1] no variable eliminated in round 1 in 9659543 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 4608 scheduled
c [score-distribution-6] 3409 pos 73.98%, 948 min 20.57%, 251 zero 5.45%
c [score-distribution-6] 1640 different 35.59% out of total 4608 variables
c [simplification-6] removed 0 variables 0.0% (4608 remain 58%)
c [simplification-6] removed 48 irredundant clauses 0.1% (39992 remain 67%)
c [simplification-6] maximum reduction of 0% = max (0%, 0%)
c [simplification-6] forced so keeping old conflict interval 15000
c [simplification-6] conflict limit remains at 25003 (hard 35003)
c [simplification-6] new ternary interval 10000
c 
c [simplification-7] limit 25003 conflicts (hard 35003) hit after 25004 conflicts
c [quatres-5] found 20113 quaternary clauses 49% in total
c [quatres-5-1] added 8 double-self-subsuming ternary resolvents
c [quatres-5-2] added 217 single-self-subsuming ternary resolvents
c [quatres-5-2] added 381 quaternary resolvents
c [ternres-5] limit 4000000 with penalty 0 = 0 + 0
c [ternres-5] all 4608 free variables schedulable
c [ternres-5] 134 ternary resolvents (4 bin, 130 trn)
c [ternres-5] fully completed ternary resolution
c [transred-5] limit 846684 with penalty 0 = 0 + 0
c [transred-5] removed 3 transitive binary clauses
c [block-4] scheduling all variables this time
c [block-4] scheduled 4608 variables 100%
c [block-4] limit of 25000000 steps penalty 1 = 1 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 0 blocked clauses
c [bca-3] limit of 10000000 steps and 80484 added (scaled 2)
c [bca-3] 1122 out of 9218 literals actually usable 12%
c [bca-3] added 0 blocked clauses in 25436 steps
c [sweep-3] limit 250000 penalty 2 = 2 + 0
c [sweep-3-1] 2171 pos 47.8% + 2373 neg 52.2% = 4544 sched 98.6% ret 64
c [sweep-3-1] 251406 steps 100 queries 571.00 avg class size
c [sweep-3-1] 3552 decisions 99 SAT calls 55.18 avg env size
c [sweep-3-1] 3105 variables remain 67% (1503 retained 33%)
c [sweep-3-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-3] removed 0 vars in TOTAL (1 rounds, 99 queries)
c [score-distribution-7] 3360 pos 72.92%, 1002 min 21.74%, 246 zero 5.34%
c [score-distribution-7] 1591 different 34.53% out of total 4608 variables
c [simplification-7] removed 0 variables 0.0% (4608 remain 58%)
c [simplification-7] removed 0 irredundant clauses 0.0% (39992 remain 67%)
c [simplification-7] maximum reduction of 0% = max (0%, 0%)
c [simplification-7] full geometric conflict interval increment 20000
c [simplification-7] new conflict interval 35000
c [simplification-7] penalized conflict interval 35000 = 1 * 35000
c [simplification-7] hard conflict limit 77504 (soft 60004 + delta 17500)
c [simplification-7] new conflict limit 60004 (hard 77504)
c 
c [simplification-8] limit 60004 conflicts (hard 77504) hit after 60004 conflicts
c [quatres-6] found 23310 quaternary clauses 44% in total
c [quatres-6-1] added 9 double-self-subsuming ternary resolvents
c [quatres-6-2] added 608 single-self-subsuming ternary resolvents
c [quatres-6-2] added 848 quaternary resolvents
c [ternres-6] limit 4000000 with penalty 0 = 0 + 0
c [ternres-6] all 4608 free variables schedulable
c [ternres-6] 536 ternary resolvents (7 bin, 529 trn)
c [ternres-6] fully completed ternary resolution
c [gauss-3] limit 500000 penalty 2 = 2 + 0
c [gauss-3] extracted 1841 xors of average arity 3.0
c [gauss-3] connected 5523 occurrences of 1192 variables (average 4.6)
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 [simpleprobe-3] 1085 schedulable variables 24%
c [simpleprobe-3] limit 5736270 penalty 1 = 1 + 0
c [simpleprobe-3] fully completed simple probing
c [simpleprobe-3] removed 0 variables, found 40 hbrs, 0 units
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 37 transitive binary clauses
c [cce-4] boosting limit by 10
c [cce-4] limit of 75000000 steps penalty 2 = 2 + 0
c [cce-4-1] eliminated 69 clauses out of 12027 (1%) of length 5
c [cce-4-1] eliminated 277 clauses out of 15532 (2%) of length 4
c [cce-4-1] completed large round (ATE)
c [cce-4-1] eliminated 346 large clauses in 6017310 steps
c [cce-4-1] allowing another 3008655 steps for small clauses
c [cce-4-1] scheduling 823 clauses = 455 binary + 368 ternary
c [cce-4-1] tried to eliminate 823 small clauses 100%
c [cce-4-1] completed small round (ATE)
c [cce-4-1] eliminated 346 covered clauses in round 1
c [cce-4-2] completed large round (ATE)
c [cce-4-2] allowing another 2947734 steps for small clauses
c [cce-4-2] scheduling 823 clauses = 455 binary + 368 ternary
c [cce-4-2] tried to eliminate 823 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 346 covered clauses in TOTAL during 2 rounds
c [cce-4] 346 < 1/100 * 39992 = 399 considered unsuccessful
c [score-distribution-8] 3974 pos 86.24%, 525 min 11.39%, 109 zero 2.37%
c [score-distribution-8] 2001 different 43.42% out of total 4608 variables
c [simplification-8] removed 0 variables 0.0% (4608 remain 58%)
c [simplification-8] removed 346 irredundant clauses 0.9% (39646 remain 67%)
c [simplification-8] maximum reduction of 1% = max (0%, 1%)
c [simplification-8] geometric conflict interval increment 17500 = 35000 / 2
c [simplification-8] new conflict interval 52500
c [simplification-8] penalized conflict interval 52500 = 1 * 52500
c [simplification-8] hard conflict limit 138754 (soft 112504 + delta 26250)
c [simplification-8] new conflict limit 112504 (hard 138754)
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 -   26.2    4608    39646     91007   36782  12391   507    9   324   15   3%    765   99    9    6  162%
c 
c [simplification-9] limit 112504 conflicts (hard 138754) hit after 112505 conflicts
c [quatres-7] found 26371 quaternary clauses 39% in total
c [quatres-7-1] removed 2 duplicate quaternary clauses
c [quatres-7-1] added 9 double-self-subsuming ternary resolvents
c [quatres-7-2] added 521 single-self-subsuming ternary resolvents
c [quatres-7-2] added 742 quaternary resolvents
c [ternres-7] limit 6762274 with penalty 0 = 0 + 0
c [ternres-7] all 4608 free variables schedulable
c [ternres-7] 312 ternary resolvents (4 bin, 308 trn)
c [ternres-7] fully completed ternary resolution
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 7 transitive binary clauses
c [elim-6] scheduling all variables this time
c [elim-6] scheduled 4608 variables 100%
c [elim-6] limit of 33811371 steps penalty 2 = 2 + 0
c [elim-6] rescheduling of touched variables disabled
c [elim-6-1] no variable eliminated in round 1 in 9409415 steps
c [elim-6] fully completed in 1 rounds
c [elim-6] transition to [ all 0 rem 0 ] state
c [elim-6] eliminated 0 = 0% variables out of 4608 scheduled
c [score-distribution-9] 4145 pos 89.95%, 385 min 8.36%, 78 zero 1.69%
c [score-distribution-9] 2209 different 47.94% out of total 4608 variables
c [simplification-9] removed 0 variables 0.0% (4608 remain 58%)
c [simplification-9] removed 42 irredundant clauses 0.1% (39604 remain 67%)
c [simplification-9] maximum reduction of 0% = max (0%, 0%)
c [simplification-9] full geometric conflict interval increment 52500
c [simplification-9] new conflict interval 105000
c [simplification-9] penalized conflict interval 105000 = 1 * 105000
c [simplification-9] hard conflict limit 270005 (soft 217505 + delta 52500)
c [simplification-9] new conflict limit 217505 (hard 270005)
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 -   45.9    4608    39604    156131   53891  14064   514   10   327   18   3%    928   40   10    8  126%
c 
c [simplification-10] limit 217505 conflicts (hard 270005) hit after 217505 conflicts
c [quatres-8] found 30552 quaternary clauses 34% in total
c [quatres-8-1] removed 11 duplicate quaternary clauses
c [quatres-8-1] added 4 double-self-subsuming ternary resolvents
c [quatres-8-2] added 426 single-self-subsuming ternary resolvents
c [quatres-8-2] added 797 quaternary resolvents
c [ternres-8] limit 15247524 with penalty 0 = 0 + 0
c [ternres-8] all 4608 free variables schedulable
c [ternres-8] 287 ternary resolvents (7 bin, 280 trn)
c [ternres-8] fully completed ternary resolution
c [card-4] limit 952970 penalty 3 = 3 + 0
c [card-4] found 2 at-most-one constraints of average size 3.0
c [card-4] found 20 at-most-two constraints of average size 4.0
c [card-4] using previous limit 952970 for elimination
c [card-4] 22 out of 22 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [unhide-4] limit 381188 with penalty 3 = 3 + 0
c [unhide-4-4] 0 units, 0 failed, 624 tauts, 0 hbrs, 9645 literals
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 3 transitive binary clauses
c [block-5] scheduling all variables this time
c [block-5] scheduled 4608 variables 100%
c [block-5] limit of 38118812 steps penalty 2 = 2 + 0
c [block-5] fully completed
c [block-5] transition to [ all 0 rem 0 ] state
c [block-5] eliminated 0 blocked clauses
c [score-distribution-10] 4244 pos 92.10%, 358 min 7.77%, 6 zero 0.13%
c [score-distribution-10] 2151 different 46.68% out of total 4608 variables
c [simplification-10] removed 0 variables 0.0% (4608 remain 58%)
c [simplification-10] removed 0 irredundant clauses 0.0% (39604 remain 67%)
c [simplification-10] maximum reduction of 0% = max (0%, 0%)
c [simplification-10] full geometric conflict interval increment 105000
c [simplification-10] new conflict interval 210000
c [simplification-10] penalized conflict interval 210000 = 1 * 210000
c [simplification-10] hard conflict limit 532505 (soft 427505 + delta 105000)
c [simplification-10] new conflict limit 427505 (hard 532505)
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 -   63.6    4608    39604    217702   62113  14848   528   11   338   11   3%    986   18   11    9  114%
c -   79.3    4608    39604    285561   78727  15289   531   12   361   21   3%   1011   17   13   11  115%
c -   93.0    4608    39604    347938   89982  15624   540   14   368   22   4%   1019    9   14   12  116%
c -  105.8    4608    39604    409398   99897  15868   541   15   380   14   4%   1022   10   16   13  115%
c 
c [simplification-11] limit 427505 conflicts (hard 532505) hit after 427506 conflicts
c [quatres-9] found 35610 quaternary clauses 28% in total
c [quatres-9-1] removed 16 duplicate quaternary clauses
c [quatres-9-1] added 5 double-self-subsuming ternary resolvents
c [quatres-9-2] added 434 single-self-subsuming ternary resolvents
c [quatres-9-2] added 800 quaternary resolvents
c [ternres-9] limit 27690913 with penalty 0 = 0 + 0
c [ternres-9] all 4608 free variables schedulable
c [ternres-9] 266 ternary resolvents (5 bin, 261 trn)
c [ternres-9] fully completed ternary resolution
c [treelook-3] limit 692272 penalty 2 = 2 + 0 boost 1
c [treelook-3] scheduled 5659 literals 61%
c [treelook-3] scheduling used 562676 steps
c [treelook-3] scheduled completely
c [treelook-3] limit 692272 penalty 2 = 2 + 0 boost 1
c [treelook-3] used 574911 steps
c [treelook-3] fully completed tree based probing
c [treelook-3] removed 0 variables, found 4 hbrs
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 5 transitive binary clauses
c [bca-4] limit of 10000000 steps and 79708 added (scaled 2)
c [bca-4] 12 out of 9218 literals actually usable 0%
c [bca-4] not enough literals usable
c [bca-4] added 0 blocked clauses in 118132 steps
c [sweep-4] limit 1038409 penalty 3 = 3 + 0
c [sweep-4-1] 1434 pos 46.2% + 1671 neg 53.8% = 3105 sched 67.4% ret 1503
c [sweep-4-1] 1044480 steps 136 queries 114.82 avg class size
c [sweep-4-1] 10203 decisions 135 SAT calls 168.40 avg env size
c [sweep-4-1] 390 variables remain 8% (4218 retained 92%)
c [sweep-4-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-4] removed 0 vars in TOTAL (1 rounds, 135 queries)
c [score-distribution-11] 4555 pos 98.85%, 53 min 1.15%, 0 zero 0.00%
c [score-distribution-11] 2775 different 60.22% out of total 4608 variables
c [simplification-11] removed 0 variables 0.0% (4608 remain 58%)
c [simplification-11] removed 0 irredundant clauses 0.0% (39604 remain 67%)
c [simplification-11] maximum reduction of 0% = max (0%, 0%)
c [simplification-11] full geometric conflict interval increment 210000
c [simplification-11] new conflict interval 420000
c [simplification-11] penalized conflict interval 420000 = 1 * 420000
c [simplification-11] hard conflict limit 1057506 (soft 847506 + delta 210000)
c [simplification-11] new conflict limit 847506 (hard 1057506)
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 -  118.5    4608    39604    469985  109386  16676   546   16   375   15   4%   1023   -1   16   15  112%
c -  130.0    4608    39604    530215  119021  16805   546   17   396   16   4%   1024   14   17   16  104%
c -  141.2    4608    39604    588537  127600  16892   548   18   392   16   5%   1024    3   20   17  117%
c -  151.6    4608    39604    645734  136187  16983   551   19   399   28   5%   1024    5   21   18  118%
c 1  160.5    4608    39604    693869  183773  17064   551   19   397   31   5%   1024    1   21   18  112%
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: 0 basic ate = 0 trn 0% + 0 lrg 0% in 0 updates
c bcas: 4 count, 0 added (94 skipped), 196467 steps
c bkwd: tried 20092 clauses, 39753 lits, 1.98 lits/clause
c bkwd: checked 654773 occs, 32.59 occs/clause, 16.47 occs/lit
c bkwd: subsumed 1 binary, 14 ternary, 137 large
c bkwd: strengthened 0 binary, 0 ternary (0% self), 502 large (0% self)
c blkd: 5 bces, 1178 removed, 1885255 resolutions, 4004876 steps
c blkd: 370 blocking literals 2%, 147 pure
c bump: 686413 bumped seen, 26802466 lits 39.0 on average
c card: 4 count, 7 units, 0 am1, 3663927 steps
c card: 62 rescheduled, 278 eliminated, 29966 resolved, 1521 subsumed
c card: 11 at-most-one constraints found, average size 3.00
c card: 11 at-most-one constraints used 100%, average size 3.00
c card: 167 at-most-two constraints found, average size 4.00
c card: 167 at-most-two constraints used 100%, average size 4.00
c cces: 4 cces, 8503 eliminated, 8290 ate 97%, 213 abce 3%
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: 292078 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 45 gcs, 0 rescored clauses, 361 rescored vars
c dcps: 26 decompositions, 29 equivalent 0%
c deco: 14 decision-only clauses 0%, 39% reduction
c decs: 15367124 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c dsch: 45106492 push, 45101314 pop (45101314 dec 100%)
c dsch: 660833570 swaps, 0 down, 155094825 up
c elms: 6 elims, 3309 eliminated 42%, 13 pure 0%
c elms: 16 rounds, 2.7 rounds/bve
c elms: 3149 small 95%, 0 large 0%
c elms: 23425 tried small, 3149 succeeded 13%, 20276 failed 87%
c elms: 1004 subsumed, 1142 strengthened, 3 blocked
c elms: 1802103 copies, 3329325 resolutions, 2181328 ipos
c elms: 51836 subchks, 42950 strchks
c gaus: 3 extractions, 22340 extracted, 3.5 size, 4 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 7000050 steps, 3500025 extr 50%, 2558315 elim 37%
c glue: 13.4 orig avg, 13.4 real avg, 2.6 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 535 = 381 simple 71% + 136 trn 25% + 18 lrg 3%, 14 sub 3%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 686413 clauses, 24.4 length
c lrnd: 16751296 lits = 17561332 orig - 810036 removed 5%
c lrnd: 344069 uips 50%, 233047 flips 34%
c mins: 584005 mins 85%, 33 bin 0%, 102342 size 15%
c mins: 14862365 poisoned searches, 896682 hits, 6% hit rate
c mins: 29995465 used twice searches, 5723867 hits, 19% hit rate
c move: moved 934, 11 bin 1%, 923 trn 99%
c otfs: 8078 driving 54%, 6893 restarting 46%
c otfs: str 14971, 14418 red 96%, 553 irr 4%
c otfs: str 14971, 0 bin 0%, 241 trn 2%, 14730 lrg 98%
c otfs: sub 260, 260 red 100%, 0 irr 0%
c otfs: sub 260, 0 bin 0%, 55 trn 21%, 205 lrg 79%
c phas: 4 computed, 5454 set, 0 pos (0%), 5454 neg (100%)
c prbs: 2 basic, 7582 probed, 0 failed, 0 lifted
c prbs: 3 simple, 27186 probed, 4 failed, 25 eqs
c prbs: 3 treelook, 10301 probed, 0 failed, 0 lifted
c prom: 40329 locked 29% out of 141080 tried
c prps: 155050876 props, 10 props/dec
c prps: 100% srch, 0% simp, 0% lkhd
c quat: 9 count, 5823 quat, 3550 self1, 66 self2, 29 dup
c redc: 864 clauses 0%, 190350 tried 27%, 0 sat 0%
c redc: 878 lits 0%, 1431600 tried 8%, 0 sat 0%
c redc: 52 times jump level reduced, 18.2 levels on average
c reds: 10 count, 69386.9 conflicts per reduce
c reds: 0 memlim 0%, 10 arith 100%
c reds: 241603 collected 49%, 250459 retired 51%
c rmbd: 58 removed, 58 red 100%
c rsts: 25993 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: 11 count, 10 confs 91%, 0 vars 0%
c simp: 0 its 0%, 0 bin 0%, 1 trns 9%
c subl: 686413 count (414171 tried 0.6), 3482 sub out of 679101 (0.5%)
c swps: 4 count, 6 rounds, 2241 queries (373.5/round)
c swps: 2248 sat calls, 7 unsat (0.3% success rate)
c swps: 32229 decisions 14.3, 622 conflicts 0.3
c swps; 331.1 avg class size, 26.9 avg environment size
c swps: 0 failed, 2 impls, 0 equivs
c swp0: 745 type 0 queries, 10 unsat (1.3%), 745 sat (100.0%)
c swp1: 1496 type 1 queries, 65 unsat (4.3%), 1496 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: 32107988 calls to obtain time
c tops: 19 fixed 0%, 0 its, 0.00 confs/it
c trds: 9 transitive reductions, 97 removed, 0 failed
c trds: 83880 nodes, 8090 edges, 12750 steps
c trim: 31289 words, 0.1 MB
c trnr: 9 count, 86 bin, 6638 trn, 19162542 steps
c unhd: 4 count, 4 rounds, 1372775 steps
c unhd: 0 non-trivial sccs of average size 0.0
c unhd: 0 units, 0 bin, 0 trn, 0 lrg
c unhd: 0 failed, 0 stamp, 0 lits, 0 bin, 0 trn, 0 lrg
c unhd: 843 tauts, 0 bin 0%, 738 trn 88%, 97 lrg 12%
c unhd: 843 tauts, 8 stamp 1%, 807 red 96%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 9944 str, 0 bin 0%, 105 trn 1%, 9839 lrg 99%, 9843 red 99%
c vars: 4608 remaining 58% and 3357 removed 42% out of 7965
c vars: 19 fixed 0%, 3309 eliminated 42%, 29 equivalent 0%
c vsts: 4286509936 visits, 100% srch, 0% simp, 0% lkhd
c vsts: 27.7 search visits per propagation, 6174.4 per conflict
c wchs: 1443087607 pushed, 4095643 enlarged, 219 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all         684924        241603        250459      30932757       3436191        269123
c 
c  0 0        136370  20        64   0         0   0  28235305  91<  2884539  84<   229988  85<    3.8
c  1 5         70664  10     29668  12     30529  12   1437674   5    174478   5     15985   6     0.4
c  2 6        155768  23     63984  26     77328  31    765937   2    154294   4     10978   4     0.8
c  3 9        125225  18<    53733  22<    61351  24<   220799   1     87098   3      4531   2     0.9
c  4 14        78490  11     36990  15     34504  14    117297   0     55572   2      2940   1     0.9
c  5 21        48259   7     23537  10     19784   8     66673   0     33633   1      1872   1     1.0
c  6 30        30138   4     14943   6     11716   5     39388   0     20690   1      1099   0     1.2
c  7 41        18815   3      9271   4      6944   3     23814   0     12812   0       793   0     1.1
c  8 54        11113   2      5226   2      4161   2     13726   0      7221   0       486   0     1.1
c  9 69         5682   1      2497   1      2238   1      6936   0      3462   0       232   0     0.8
c 10 86         3817   1      1514   1      1645   1      4517   0      2102   0       187   0     0.7
c 11 126         558   0       173   0       245   0       663   0       283   0        32   0     0.2
c 12 230          25   0         3   0        14   0        28   0         7   0         0   0     0.0
c 
c avg                  2.6           3.4           3.2           0.2           0.4           0.3
c std                  2.1           1.9           1.8           0.7           1.2           1.1
c 
c   15.266  10% decide
c    2.795   2% elim
c    2.132   1% bump
c    1.478   1% cce
c    0.670   0% quatres
c 
c    1.868 < 1% rest (below)
c 
c    0.442   0% probe
c    0.409   0% sweep
c    0.285   0% block
c    0.247   0% gauss
c    0.161   0% ternres
c    0.120   0% unhide
c    0.091   0% card
c    0.057   0% bca
c    0.046   0% rescore
c    0.010   0% transred
c    0.000   0% locs
c    0.000   0% queuesort
c ==================================
c    0.655   0% preprocessing     9%
c    6.648   4% inprocessing     91%
c ==================================
c    7.303   5% simplifying
c  153.214  95% search
c ==================================
c  160.517 100% all
c 
c        693869 conflicts,        4322.7 confs/sec
c          7141 ternaries,          97.2 confs/ternary
c            43 binaries,        16136.5 confs/binary
c             0 iterations,          0.0 confs/iteration
c 
c            10 reductions,          0.1 redus/sec,  69386.9 confs/reduction
c         25993 restarts,          161.9 rests/sec,     26.7 confs/restart
c      15367124 decisions,       95735.3 decis/sec,     22.1 decis/conflict
c     155050876 propagations,   965947.8 props/sec,     10.1 props/decision
c 
c 160.5 seconds, 52.7 MB
c launch: done
