c launch: /data/cnf/sc2014/app/MD5-27-4.cnf.bz2
c host: atom17
c Lingeling SAT Solver
c 
c Version b7ztzu 7b29300825af9bcc1c8b2c5ebcf65fa1cb101cad
c 
c Copyright (C) 2010-2014 Armin Biere JKU Linz Austria.
c All rights reserved.
c 
c released Sun Apr 26 19:26:13 CEST 2015
c compiled Sun Apr 26 19:26:13 CEST 2015
c 
c gcc (Ubuntu 4.8.2-19ubuntu1) 4.8.2
c -Wall -O3 -I../yalsat -I../druplig -DNLGLOG -DNDEBUG -DNCHKSOL
c Linux cluster2 3.13.0-45-generic x86_64
c 
c piping '/data/cnf/sc2014/app/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 --queuesort=1
c --queuesortjwh=0
c --randec=0
c --randecint=1000
c --redcls=1
c --redclsglue=6
c --redclsmaxdec=5
c --redclsmaxdepth=10
c --redclsmaxlrg=10
c --redclsmaxprops=100
c --redclsatlimlo=0
c --redclsatlimhi=100
c --redclsize=30
c --redclstype=4
c --reducefixed=0
c --reduceinc=1000
c --reduceinit=50000
c --reduce=1
c --restart=4
c --restartglcint=10
c --restartglclim=115
c --restartinit=0
c --restartint=5
c --restartpen=1
c --retirenb=1
c --retireint=4
c --retiremin=1
c --reusetrail=0
c --rmincpen=4
c --rstinoutinc=110
c --satlimdelay=10000
c --scincinc=200
c --scincincsatlimhi=100
c --scincincdelta=10
c --scincincincint=100000
c --scincincmin=200
c --scincincmode=1
c --score=0
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 [score-type] STATIC (--score=0)
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 [sort-queue-1] sorted 5331 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 5331 (100%)
c [score-dist-1] max exp 0, different 1 (100%)
c [score-dist-1] median active exp 0, avg 0.0
c [simplification-1] removed 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] 1211 variables remain 23% (4120 retained 77%)
c [simpleprobe-2] removed 0 variables, found 33 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 262123 steps
c [treelook-1] scheduled completely
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 300078 steps
c [treelook-1] 7625 literals remain 72%
c [treelook-1] 5271 variables remain to probed next time 99%
c [treelook-1] removed 0 variables, found 53 hbrs
c [basicprobe-1] limit 1000000 penalty 0 = 0 + 0
c [basicprobe-1-0] 602 sched 11%, 0 failed, 0 lifted, 17 hbrs
c [basicprobe-1-1] 609 sched 11%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-1-1] fully completed probing
c [basicprobe-1-1] removed 0 variables, found 17 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 6916 clauses out of 21166 (33%) of length 5
c [cce-1-1] eliminated 272 clauses out of 18245 (1%) of length 4
c [cce-1-1] completed large round (ATE)
c [cce-1-1] eliminated 7248 large clauses in 8498628 steps
c [cce-1-1] allowing another 4249314 steps for small clauses
c [cce-1-1] scheduling 12623 clauses = 464 binary + 12159 ternary
c [cce-1-1] tried to eliminate 12623 small clauses 100%
c [cce-1-1] eliminated 3 binary clauses 1%
c [cce-1-1] eliminated 403 ternary clauses 3%
c [cce-1-1] eliminated 406 small clauses 3%
c [cce-1-1] eliminated 406 small clauses in 5891336 steps
c [cce-1-1] completed small round (ATE)
c [cce-1-1] completed small and large (ATE)
c [cce-1-1] eliminated 7654 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 14250 (0%) of length 5
c [cce-1-2] eliminated 65 clauses out of 17973 (0%) of length 4
c [cce-1-2] completed large round (ABCE)
c [cce-1-2] eliminated 121 large clauses in 7613102 steps
c [cce-1-2] allowing another 3806551 steps for small clauses
c [cce-1-2] scheduling 12217 clauses = 461 binary + 11756 ternary
c [cce-1-2] tried to eliminate 12217 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 5485576 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 14196 (0%) of length 5
c [cce-1-3] eliminated 47 clauses out of 17908 (0%) of length 4
c [cce-1-3] completed large round (ACCE)
c [cce-1-3] eliminated 75 large clauses in 8631266 steps
c [cce-1-3] allowing another 4315633 steps for small clauses
c [cce-1-3] scheduling 12215 clauses = 461 binary + 11754 ternary
c [cce-1-3] tried to eliminate 12215 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 6161405 steps
c [cce-1-3] completed small round (ACCE)
c [cce-1-3] completed small and large (ACCE)
c [cce-1-3] eliminated 99 covered clauses in round 3
c [cce-1] eliminated 7876 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 267 variables 5% in round 1 in 10832719 steps
c [elim-2-1] backward subsumption/strengthening limit 9167281
c [elim-2-1-1] backward checking 640 touched variables 12%
c [elim-2-1-1] fully completed backward checking in 1 rounds
c [elim-2-1] subsumed 4 and strengthened 41 clauses in 151080 steps
c [elim-2-1] rescheduled 86 variables 2% by backward subsumption
c [elim-2-2] eliminated 1 variables 0% in round 2 in 175201 steps
c [elim-2-2] backward subsumption/strengthening limit 175200
c [elim-2-2-1] backward checking 22 touched variables 0%
c [elim-2-2-1] fully completed backward checking in 1 rounds
c [elim-2-2] subsumed 0 and strengthened 0 clauses in 53407 steps
c [elim-2] fully completed in 2 rounds
c [elim-2] transition to [ all 0 rem 0 ] state
c [elim-2] eliminated 268 = 5% variables out of 5314 scheduled
c [bca-1] limit of 10000000 steps and 87960 added (scaled 2)
c [bca-1] 8109 out of 10094 literals actually usable 80%
c [bca-1] added 0 blocked clauses in 32289 steps
c [sweep-1] limit 1000000 penalty 0 = 0 + 0
c [sweep-1-1] 2335 pos 46.3% + 2711 neg 53.7% = 5046 sched 100.0% ret 0
c [sweep-1-1] 733077 steps 979 queries 276.56 avg class size
c [sweep-1-1] 8226 decisions 979 SAT calls 14.94 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] 2335 pos 46.3% + 2711 neg 53.7% = 5046 sched 100.0% ret 0
c [sweep-1-2] 267111 steps 270 queries 868.08 avg class size
c [sweep-1-2] 2481 decisions 270 SAT calls 16.59 avg env size
c [sweep-1-2] 3782 variables remain 75% (1264 retained 25%)
c [sweep-1-2] removed 0 vars (0 failed, 0 eqs, 1 impls)
c [sweep-1] removed 0 vars in TOTAL (2 rounds, 1247 queries)
c [sort-queue-2] sorted 5046 enqueued variables after 1000 conflicts
c [score-dist-2] active 0 (0%), one 0 (0%), zero 5046 (100%)
c [score-dist-2] max exp 0, different 1 (100%)
c [score-dist-2] median active exp 0, avg 0.0
c [simplification-2] removed 285 variables 5.3% (5046 remain 63%)
c [simplification-2] removed 10769 irredundant clauses 19.8% (43730 remain 73%)
c [simplification-2] maximum reduction of 20% = max (5%, 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 3000 conflicts
c [quatres-1] found 17625 quaternary clauses 54% in total
c [quatres-1-1] added 2 double-self-subsuming ternary resolvents
c [quatres-1-2] added 269 single-self-subsuming ternary resolvents
c [quatres-1-2] added 351 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 5046 free variables schedulable
c [ternres-1] 3683 ternary resolvents (9 bin, 3674 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 5 at-most-two constraints of average size 4.0
c [card-2] using previous limit 1000000 for elimination
c [card-2] 7 out of 7 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] generated 3 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 15563 xors of average arity 3.7
c [gauss-1] connected 56832 occurrences of 4509 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, 61 tauts, 0 hbrs, 96 literals
c [transred-1] limit 100000 with penalty 0 = 0 + 0
c [transred-1] removed 13 transitive binary clauses
c [cce-2] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-2-1] eliminated 23 clauses out of 13138 (0%) of length 5
c [cce-2-1] eliminated 39 clauses out of 16926 (0%) of length 4
c [cce-2-1] completed large round (ATE)
c [cce-2-1] eliminated 62 large clauses in 6696901 steps
c [cce-2-1] allowing another 3348450 steps for small clauses
c [cce-2-1] scheduling 1014 clauses = 499 binary + 515 ternary
c [cce-2-1] tried to eliminate 1014 small clauses 100%
c [cce-2-1] eliminated 3 binary clauses 1%
c [cce-2-1] eliminated 49 ternary clauses 10%
c [cce-2-1] eliminated 52 small clauses 5%
c [cce-2-1] eliminated 52 small clauses in 3445226 steps
c [cce-2-1] completed small round (ATE)
c [cce-2-1] eliminated 114 covered clauses in round 1
c [cce-2-2] completed large round (ATE)
c [cce-2-2] allowing another 3333969 steps for small clauses
c [cce-2-2] scheduling 962 clauses = 496 binary + 466 ternary
c [cce-2-2] tried to eliminate 962 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 114 covered clauses in TOTAL during 2 rounds
c [cce-2] 114 < 1/100 * 43728 = 437 considered unsuccessful
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 5045 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 263 variables 5% in round 1 in 10230910 steps
c [elim-3-1] backward subsumption/strengthening limit 9769090
c [elim-3-1-1] backward checking 372 touched variables 7%
c [elim-3-1-1] fully completed backward checking in 1 rounds
c [elim-3-1] subsumed 0 and strengthened 20 clauses in 99835 steps
c [elim-3-1] rescheduled 38 variables 1% by backward subsumption
c [elim-3-2] eliminated 2 variables 0% in round 2 in 86577 steps
c [elim-3-2] backward subsumption/strengthening limit 86500
c [elim-3-2-1] backward checking 5 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 41340 steps
c [elim-3] fully completed in 2 rounds
c [elim-3] transition to [ all 0 rem 0 ] state
c [elim-3] eliminated 265 = 5% variables out of 5045 scheduled
c [sort-queue-3] sorted 4780 enqueued variables after 3000 conflicts
c [score-dist-3] active 0 (0%), one 0 (0%), zero 4780 (100%)
c [score-dist-3] max exp 0, different 1 (100%)
c [score-dist-3] median active exp 0, avg 0.0
c [simplification-3] removed 266 variables 5.3% (4780 remain 60%)
c [simplification-3] removed 2224 irredundant clauses 5.1% (41506 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 15000 (soft 5000 + delta 10000)
c [simplification-3] new conflict limit 5000 (hard 15000)
c 
c [simplification-4] limit 5000 conflicts (hard 15000) hit after 5001 conflicts
c [quatres-2] found 17265 quaternary clauses 54% in total
c [quatres-2-1] removed 1 duplicate quaternary clauses
c [quatres-2-1] added 1 double-self-subsuming ternary resolvents
c [quatres-2-2] added 174 single-self-subsuming ternary resolvents
c [quatres-2-2] added 372 quaternary resolvents
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] all 4780 free variables schedulable
c [ternres-2] 498 ternary resolvents (1 bin, 497 trn)
c [ternres-2] fully completed ternary resolution
c [treelook-2] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-2] scheduled 6085 literals 64%
c [treelook-2] scheduling used 150032 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-2] used 150029 steps
c [treelook-2] 4487 literals remain 47%
c [treelook-2] 3972 variables remain to probed next time 83%
c [treelook-2] removed 0 variables, found 24 hbrs
c [transred-2] limit 107113 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 4780 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 889 blocked clauses
c [elim-4] scheduling all variables this time
c [elim-4] scheduled 4656 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 25 variables 1% in round 1 in 9879488 steps
c [elim-4-1] backward subsumption/strengthening limit 9879400
c [elim-4-1-1] backward checking 66 touched variables 1%
c [elim-4-1-1] fully completed backward checking in 1 rounds
c [elim-4-1] subsumed 0 and strengthened 8 clauses in 41174 steps
c [elim-4-1] rescheduled 14 variables 0% by backward subsumption
c [elim-4-2] eliminated 4 variables 0% in round 2 in 19315 steps
c [elim-4-2] backward subsumption/strengthening limit 19300
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 19301 steps
c [elim-4-2] fully rescheduled 4627 variables 99%
c [elim-4-3] eliminated 11 variables 0% in round 3 in 9844676 steps
c [elim-4-3] backward subsumption/strengthening limit 9844600
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 30861 steps
c [elim-4] fully completed in 3 rounds
c [elim-4] transition to [ all 0 rem 0 ] state
c [elim-4] eliminated 40 = 1% variables out of 4656 scheduled
c [elim-4] 40 < 1/100 * 4656 = 46 considered unsuccessful
c [bca-2] limit of 10000000 steps and 81004 added (scaled 2)
c [bca-2] 3110 out of 9234 literals actually usable 34%
c [bca-2] added 0 blocked clauses in 15082 steps
c [sweep-2] limit 500000 penalty 1 = 1 + 0
c [sweep-2-1] 1693 pos 49.3% + 1741 neg 50.7% = 3434 sched 74.4% ret 1182
c [sweep-2-1] 500118 steps 697 queries 194.61 avg class size
c [sweep-2-1] 7501 decisions 698 SAT calls 18.28 avg env size
c [sweep-2-1] 17 variables remain 0% (4599 retained 100%)
c [sweep-2-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-2] removed 0 vars in TOTAL (1 rounds, 696 queries)
c [sort-queue-4] sorted 4616 enqueued variables after 5001 conflicts
c [score-dist-4] active 0 (0%), one 0 (0%), zero 4616 (100%)
c [score-dist-4] max exp 0, different 1 (100%)
c [score-dist-4] median active exp 0, avg 0.0
c [simplification-4] removed 164 variables 3.4% (4616 remain 58%)
c [simplification-4] removed 1254 irredundant clauses 3.0% (40252 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 20001 (soft 10001 + delta 10000)
c [simplification-4] new conflict limit 10001 (hard 20001)
c 
c [simplification-5] limit 10001 conflicts (hard 20001) hit after 10001 conflicts
c [quatres-3] found 17916 quaternary clauses 53% in total
c [quatres-3-1] added 1 double-self-subsuming ternary resolvents
c [quatres-3-2] added 299 single-self-subsuming ternary resolvents
c [quatres-3-2] added 476 quaternary resolvents
c [ternres-3] limit 4000000 with penalty 0 = 0 + 0
c [ternres-3] all 4616 free variables schedulable
c [ternres-3] 668 ternary resolvents (7 bin, 661 trn)
c [ternres-3] fully completed ternary resolution
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] extracted 5085 xors of average arity 3.0
c [gauss-2] connected 15255 occurrences of 1218 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 257970 with penalty 0 = 0 + 0
c [transred-3] removed 4 transitive binary clauses
c [block-3] scheduling all variables this time
c [block-3] scheduled 4616 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 * 40252 = 402 considered unsuccessful
c [cce-3] limit of 15000000 steps penalty 1 = 1 + 0
c [cce-3-1] eliminated 31 clauses out of 12328 (0%) of length 5
c [cce-3-1] eliminated 82 clauses out of 15614 (1%) of length 4
c [cce-3-1] completed large round (ACCE)
c [cce-3-1] eliminated 113 large clauses in 7573207 steps
c [cce-3-1] allowing another 3786603 steps for small clauses
c [cce-3-1] scheduling 789 clauses = 456 binary + 333 ternary
c [cce-3-1] tried to eliminate 789 small clauses 100%
c [cce-3-1] eliminated 1 binary clauses 0%
c [cce-3-1] eliminated 1 small clauses 0%
c [cce-3-1] eliminated 1 small clauses in 3871659 steps
c [cce-3-1] completed small round (ACCE)
c [cce-3-1] eliminated 114 covered clauses in round 1
c [cce-3-2] completed large round (ACCE)
c [cce-3-2] allowing another 3756482 steps for small clauses
c [cce-3-2] scheduling 788 clauses = 455 binary + 333 ternary
c [cce-3-2] tried to eliminate 788 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 114 covered clauses in TOTAL during 2 rounds
c [cce-3] 114 < 1/100 * 40222 = 402 considered unsuccessful
c [sort-queue-5] sorted 4613 enqueued variables after 10001 conflicts
c [score-dist-5] active 0 (0%), one 0 (0%), zero 4613 (100%)
c [score-dist-5] max exp 0, different 1 (100%)
c [score-dist-5] median active exp 0, avg 0.0
c [simplification-5] removed 3 variables 0.1% (4613 remain 58%)
c [simplification-5] removed 144 irredundant clauses 0.4% (40108 remain 67%)
c [simplification-5] maximum reduction of 0% = max (0%, 0%)
c [simplification-5] full geometric conflict interval increment 20000
c [simplification-5] new conflict interval 25000
c [simplification-5] penalized conflict interval 25000 = 1 * 25000
c [simplification-5] hard conflict limit 47501 (soft 35001 + delta 12500)
c [simplification-5] new conflict limit 35001 (hard 47501)
c 
c [simplification-6] limit of 3368 ternary hit after 3368 ternaries
c [quatres-4] found 19511 quaternary clauses 52% in total
c [quatres-4-1] added 13 double-self-subsuming ternary resolvents
c [quatres-4-2] added 383 single-self-subsuming ternary resolvents
c [quatres-4-2] added 603 quaternary resolvents
c [ternres-4] limit 4000000 with penalty 0 = 0 + 0
c [ternres-4] all 4613 free variables schedulable
c [ternres-4] 656 ternary resolvents (12 bin, 644 trn)
c [ternres-4] fully completed ternary resolution
c [card-3] limit 500000 penalty 2 = 2 + 0
c [card-3] found 2 at-most-one constraints of average size 3.0
c [card-3] found 14 at-most-two constraints of average size 4.1
c [card-3] using previous limit 500000 for elimination
c [card-3] 15 out of 16 constraints (94%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [basicprobe-2] limit 1547756 penalty 1 = 1 + 0
c [basicprobe-2-0] 756 sched 16%, 0 failed, 0 lifted, 18 hbrs
c [basicprobe-2-1] 762 sched 17%, 0 failed, 0 lifted, 1 hbrs
c [basicprobe-2-2] 763 sched 17%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-2-2] fully completed probing
c [basicprobe-2-2] removed 0 variables, found 19 hbrs
c [unhide-3] limit 30955 with penalty 2 = 2 + 0
c [unhide-3-3] 0 units, 0 failed, 16 tauts, 0 hbrs, 248 literals
c [transred-4] limit 619102 with penalty 0 = 0 + 0
c [transred-4] removed 7 transitive binary clauses
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 4613 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 9735517 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 4613 scheduled
c [sort-queue-6] sorted 4613 enqueued variables after 19540 conflicts
c [score-dist-6] active 0 (0%), one 0 (0%), zero 4613 (100%)
c [score-dist-6] max exp 0, different 1 (100%)
c [score-dist-6] median active exp 0, avg 0.0
c [simplification-6] removed 0 variables 0.0% (4613 remain 58%)
c [simplification-6] removed 40 irredundant clauses 0.1% (40067 remain 67%)
c [simplification-6] maximum reduction of 0% = max (0%, 0%)
c [simplification-6] forced so keeping old conflict interval 25000
c [simplification-6] conflict limit remains at 35001 (hard 47501)
c [simplification-6] new ternary interval 10000
c 
c [simplification-7] limit 35001 conflicts (hard 47501) hit after 35001 conflicts
c [quatres-5] found 21608 quaternary clauses 50% in total
c [quatres-5-1] added 9 double-self-subsuming ternary resolvents
c [quatres-5-2] added 403 single-self-subsuming ternary resolvents
c [quatres-5-2] added 612 quaternary resolvents
c [ternres-5] limit 4000000 with penalty 0 = 0 + 0
c [ternres-5] all 4613 free variables schedulable
c [ternres-5] 607 ternary resolvents (11 bin, 596 trn)
c [ternres-5] fully completed ternary resolution
c [transred-5] limit 1364819 with penalty 0 = 0 + 0
c [transred-5] removed 1 transitive binary clauses
c [block-4] scheduling all variables this time
c [block-4] scheduled 4613 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 80634 added (scaled 2)
c [bca-3] 243 out of 9228 literals actually usable 3%
c [bca-3] added 0 blocked clauses in 29747 steps
c [sweep-3] limit 250000 penalty 2 = 2 + 0
c [sweep-3-1] 10 pos 58.8% + 7 neg 41.2% = 17 sched 0.4% ret 4596
c [sweep-3-1] 39818 steps 10 queries 4.70 avg class size
c [sweep-3-1] 449 decisions 9 SAT calls 85.00 avg env size
c [sweep-3-1] fully completed sweeping round
c [sweep-3-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-3-2] 2263 pos 49.1% + 2350 neg 50.9% = 4613 sched 100.0% ret 0
c [sweep-3-2] 218213 steps 70 queries 688.10 avg class size
c [sweep-3-2] 2639 decisions 69 SAT calls 58.74 avg env size
c [sweep-3-2] 3575 variables remain 77% (1038 retained 23%)
c [sweep-3-2] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-3] removed 0 vars in TOTAL (2 rounds, 78 queries)
c [sort-queue-7] sorted 4613 enqueued variables after 35001 conflicts
c [score-dist-7] active 0 (0%), one 0 (0%), zero 4613 (100%)
c [score-dist-7] max exp 0, different 1 (100%)
c [score-dist-7] median active exp 0, avg 0.0
c [simplification-7] removed 0 variables 0.0% (4613 remain 58%)
c [simplification-7] removed 0 irredundant clauses 0.0% (40067 remain 67%)
c [simplification-7] maximum reduction of 0% = max (0%, 0%)
c [simplification-7] full geometric conflict interval increment 25000
c [simplification-7] new conflict interval 50000
c [simplification-7] penalized conflict interval 50000 = 1 * 50000
c [simplification-7] hard conflict limit 110001 (soft 85001 + delta 25000)
c [simplification-7] new conflict limit 85001 (hard 110001)
c 
c [simplification-8] limit 85001 conflicts (hard 110001) hit after 85001 conflicts
c [quatres-6] found 25983 quaternary clauses 45% in total
c [quatres-6-1] added 8 double-self-subsuming ternary resolvents
c [quatres-6-2] added 608 single-self-subsuming ternary resolvents
c [quatres-6-2] added 987 quaternary resolvents
c [ternres-6] limit 5004100 with penalty 0 = 0 + 0
c [ternres-6] all 4613 free variables schedulable
c [ternres-6] 568 ternary resolvents (13 bin, 555 trn)
c [ternres-6] fully completed ternary resolution
c [gauss-3] limit 500000 penalty 2 = 2 + 0
c [gauss-3] extracted 1652 xors of average arity 3.0
c [gauss-3] connected 4956 occurrences of 1057 variables (average 4.7)
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] 1054 schedulable variables 23%
c [simpleprobe-3] limit 10008201 penalty 1 = 1 + 0
c [simpleprobe-3] fully completed simple probing
c [simpleprobe-3] removed 0 variables, found 54 hbrs, 0 units
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 49 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 86 clauses out of 12135 (1%) of length 5
c [cce-4-1] eliminated 299 clauses out of 15517 (2%) of length 4
c [cce-4-1] completed large round (ATE)
c [cce-4-1] eliminated 385 large clauses in 6075309 steps
c [cce-4-1] allowing another 3037654 steps for small clauses
c [cce-4-1] scheduling 859 clauses = 456 binary + 403 ternary
c [cce-4-1] tried to eliminate 859 small clauses 100%
c [cce-4-1] completed small round (ATE)
c [cce-4-1] eliminated 385 covered clauses in round 1
c [cce-4-2] completed large round (ATE)
c [cce-4-2] allowing another 2969658 steps for small clauses
c [cce-4-2] scheduling 859 clauses = 456 binary + 403 ternary
c [cce-4-2] tried to eliminate 859 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 385 covered clauses in TOTAL during 2 rounds
c [cce-4] 385 < 1/100 * 40067 = 400 considered unsuccessful
c [sort-queue-8] sorted 4613 enqueued variables after 85001 conflicts
c [score-dist-8] active 0 (0%), one 0 (0%), zero 4613 (100%)
c [score-dist-8] max exp 0, different 1 (100%)
c [score-dist-8] median active exp 0, avg 0.0
c [simplification-8] removed 0 variables 0.0% (4613 remain 58%)
c [simplification-8] removed 385 irredundant clauses 1.0% (39682 remain 67%)
c [simplification-8] maximum reduction of 1% = max (0%, 1%)
c [simplification-8] geometric conflict interval increment 25000 = 50000 / 2
c [simplification-8] new conflict interval 75000
c [simplification-8] penalized conflict interval 75000 = 1 * 75000
c [simplification-8] hard conflict limit 197501 (soft 160001 + delta 37500)
c [simplification-8] new conflict limit 160001 (hard 197501)
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 -   33.8    4613    39682     89883   31442  14928   527    8   438    9   2%    760  120    8    6  138%
c -   62.7    4613    39682    158989   51601  16116   548   10   442   10   2%    932   45   10    8  127%
c 
c [simplification-9] limit 160001 conflicts (hard 197501) hit after 160003 conflicts
c [quatres-7] found 30463 quaternary clauses 40% in total
c [quatres-7-1] removed 3 duplicate quaternary clauses
c [quatres-7-1] added 10 double-self-subsuming ternary resolvents
c [quatres-7-2] added 381 single-self-subsuming ternary resolvents
c [quatres-7-2] added 927 quaternary resolvents
c [ternres-7] limit 11433337 with penalty 0 = 0 + 0
c [ternres-7] all 4613 free variables schedulable
c [ternres-7] 301 ternary resolvents (7 bin, 294 trn)
c [ternres-7] fully completed ternary resolution
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 11 transitive binary clauses
c [elim-6] scheduling all variables this time
c [elim-6] scheduled 4613 variables 100%
c [elim-6] limit of 57166685 steps penalty 2 = 2 + 0
c [elim-6] rescheduling of touched variables disabled
c [elim-6-1] no variable eliminated in round 1 in 9461708 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 4613 scheduled
c [sort-queue-9] sorted 4613 enqueued variables after 160003 conflicts
c [score-dist-9] active 0 (0%), one 0 (0%), zero 4613 (100%)
c [score-dist-9] max exp 0, different 1 (100%)
c [score-dist-9] median active exp 0, avg 0.0
c [simplification-9] removed 0 variables 0.0% (4613 remain 58%)
c [simplification-9] removed 29 irredundant clauses 0.1% (39653 remain 67%)
c [simplification-9] maximum reduction of 0% = max (0%, 0%)
c [simplification-9] full geometric conflict interval increment 75000
c [simplification-9] new conflict interval 150000
c [simplification-9] penalized conflict interval 150000 = 1 * 150000
c [simplification-9] hard conflict limit 385003 (soft 310003 + delta 75000)
c [simplification-9] new conflict limit 310003 (hard 385003)
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 -   89.7    4613    39653    222842   67248  17583   552   11   479   20   2%    989   35   12   10  122%
c -  114.1    4613    39653    283451   78838  18040   556   12   500   12   2%   1010   29   13   11  117%
c 
c [simplification-10] limit 310003 conflicts (hard 385003) hit after 310003 conflicts
c [quatres-8] found 37560 quaternary clauses 35% in total
c [quatres-8-1] removed 8 duplicate quaternary clauses
c [quatres-8-1] added 9 double-self-subsuming ternary resolvents
c [quatres-8-2] added 335 single-self-subsuming ternary resolvents
c [quatres-8-2] added 1211 quaternary resolvents
c [ternres-8] limit 24444336 with penalty 0 = 0 + 0
c [ternres-8] all 4613 free variables schedulable
c [ternres-8] 226 ternary resolvents (4 bin, 222 trn)
c [ternres-8] fully completed ternary resolution
c [card-4] limit 1527771 penalty 3 = 3 + 0
c [card-4] found 4 at-most-one constraints of average size 3.0
c [card-4] found 37 at-most-two constraints of average size 4.0
c [card-4] using previous limit 1527771 for elimination
c [card-4] 41 out of 41 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [unhide-4] limit 611108 with penalty 3 = 3 + 0
c [unhide-4-4] 0 units, 0 failed, 969 tauts, 0 hbrs, 5617 literals
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 14 transitive binary clauses
c [block-5] scheduling all variables this time
c [block-5] scheduled 4613 variables 100%
c [block-5] limit of 61110840 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 [sort-queue-10] sorted 4613 enqueued variables after 310003 conflicts
c [score-dist-10] active 0 (0%), one 0 (0%), zero 4613 (100%)
c [score-dist-10] max exp 0, different 1 (100%)
c [score-dist-10] median active exp 0, avg 0.0
c [simplification-10] removed 0 variables 0.0% (4613 remain 58%)
c [simplification-10] removed 0 irredundant clauses 0.0% (39653 remain 67%)
c [simplification-10] maximum reduction of 0% = max (0%, 0%)
c [simplification-10] full geometric conflict interval increment 150000
c [simplification-10] new conflict interval 300000
c [simplification-10] penalized conflict interval 300000 = 1 * 300000
c [simplification-10] hard conflict limit 760003 (soft 610003 + delta 150000)
c [simplification-10] new conflict limit 610003 (hard 760003)
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 -  136.7    4613    39653    343954   89013  18039   558   14   513   13   3%   1019   17   14   12  117%
c -  159.5    4613    39653    405677   99689  18249   558   15   521   14   3%   1022   12   15   13  112%
c -  181.8    4613    39653    466303  108439  18443   558   16   537   15   3%   1023   19   15   15  100%
c -  203.6    4613    39653    526920  116376  18569   559   17   539   16   3%   1024   16   17   16  106%
c -  225.3    4613    39653    587896  123810  18675   560   18   525   16   4%   1024   -2   19   17  110%
c 
c [simplification-11] limit 610003 conflicts (hard 760003) hit after 616356 conflicts
c [quatres-9] found 45537 quaternary clauses 30% in total
c [quatres-9-1] removed 15 duplicate quaternary clauses
c [quatres-9-1] added 4 double-self-subsuming ternary resolvents
c [quatres-9-2] added 212 single-self-subsuming ternary resolvents
c [quatres-9-2] added 1272 quaternary resolvents
c [ternres-9] limit 52218780 with penalty 0 = 0 + 0
c [ternres-9] all 4613 free variables schedulable
c [ternres-9] 159 ternary resolvents (4 bin, 155 trn)
c [ternres-9] fully completed ternary resolution
c [treelook-3] limit 1305469 penalty 2 = 2 + 0 boost 1
c [treelook-3] scheduled 7829 literals 85%
c [treelook-3] scheduling used 778111 steps
c [treelook-3] scheduled completely
c [treelook-3] limit 1305469 penalty 2 = 2 + 0 boost 1
c [treelook-3] used 798371 steps
c [treelook-3] fully completed tree based probing
c [treelook-3] removed 0 variables, found 2 hbrs
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 8 transitive binary clauses
c [bca-4] limit of 10000000 steps and 79806 added (scaled 2)
c [bca-4] 2 out of 9228 literals actually usable 0%
c [bca-4] not enough literals usable
c [bca-4] added 0 blocked clauses in 153092 steps
c [sweep-4] limit 1958204 penalty 3 = 3 + 0
c [sweep-4-1] 1794 pos 50.2% + 1781 neg 49.8% = 3575 sched 77.5% ret 1038
c [sweep-4-1] 1958492 steps 190 queries 106.60 avg class size
c [sweep-4-1] 14054 decisions 189 SAT calls 219.76 avg env size
c [sweep-4-1] 54 variables remain 1% (4559 retained 99%)
c [sweep-4-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-4] removed 0 vars in TOTAL (1 rounds, 189 queries)
c [sort-queue-11] sorted 4613 enqueued variables after 616356 conflicts
c [score-dist-11] active 0 (0%), one 0 (0%), zero 4613 (100%)
c [score-dist-11] max exp 0, different 1 (100%)
c [score-dist-11] median active exp 0, avg 0.0
c [simplification-11] removed 0 variables 0.0% (4613 remain 58%)
c [simplification-11] removed 0 irredundant clauses 0.0% (39653 remain 67%)
c [simplification-11] maximum reduction of 0% = max (0%, 0%)
c [simplification-11] full geometric conflict interval increment 300000
c [simplification-11] new conflict interval 600000
c [simplification-11] penalized conflict interval 600000 = 1 * 600000
c [simplification-11] hard conflict limit 1516356 (soft 1216356 + delta 300000)
c [simplification-11] new conflict limit 1216356 (hard 1516356)
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 -  248.1    4613    39653    649812  130792  19126   558   19   524   17   4%   1024   -3   19   18  105%
c -  271.1    4613    39653    714089  138979  19230   558   20   540   17   4%   1024   11   19   19   99%
c -  294.1    4613    39653    777963  146118  19307   558   21   525   18   4%   1024   -3   23   20  115%
c -  318.0    4613    39653    842013  152581  19364   558   21   558   18   4%   1024   25   18   21   87%
c -  342.5    4613    39653    906941  158959  19417   558   22   525   19   4%   1024   -6   19   21   91%
c -  366.9    4613    39653    972409  165166  19466   559   23   505   19   5%   1024  -30   25   22  113%
c -  391.7    4613    39653   1038624  171013  19511   559   23   558   20   4%   1024   24   25   22  111%
c -  417.7    4613    39653   1105797  176848  19549   559   23   532   20   4%   1024   -2   20   23   87%
c -  444.9    4613    39653   1173926  182672  19584   559   23   572   21   4%   1024   37   22   24   94%
c 
c [simplification-12] limit 1216356 conflicts (hard 1516356) hit after 1222831 conflicts
c [quatres-10] found 53502 quaternary clauses 25% in total
c [quatres-10-1] removed 21 duplicate quaternary clauses
c [quatres-10-1] added 1 double-self-subsuming ternary resolvents
c [quatres-10-2] added 78 single-self-subsuming ternary resolvents
c [quatres-10-2] added 1084 quaternary resolvents
c [ternres-10] limit 116639309 with penalty 0 = 0 + 0
c [ternres-10] all 4613 free variables schedulable
c [ternres-10] 140 ternary resolvents (3 bin, 137 trn)
c [ternres-10] fully completed ternary resolution
c [gauss-4] limit 2915982 penalty 3 = 3 + 0
c [gauss-4] extracted 10683 xors of average arity 3.5
c [gauss-4] connected 37647 occurrences of 3202 variables (average 11.8)
c [gauss-4] limit 2915982 penalty 3 = 3 + 0
c [gauss-4] connected 10795 occurrences of 3202 variables (average 3.4)
c [gauss-4] fully completed
c [gauss-4] exported 0 unary, 0 binary and 0 ternary equations
c [transred-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 6 transitive binary clauses
c [cce-5] limit of 72899568 steps penalty 3 = 3 + 0
c [cce-5-1] eliminated 30 clauses out of 11957 (0%) of length 5
c [cce-5-1] eliminated 168 clauses out of 15190 (1%) of length 4
c [cce-5-1] completed large round (ACCE)
c [cce-5-1] eliminated 198 large clauses in 7133298 steps
c [cce-5-1] allowing another 3566649 steps for small clauses
c [cce-5-1] scheduling 902 clauses = 461 binary + 441 ternary
c [cce-5-1] tried to eliminate 902 small clauses 100%
c [cce-5-1] eliminated 2 binary clauses 0%
c [cce-5-1] eliminated 1 ternary clauses 0%
c [cce-5-1] eliminated 3 small clauses 0%
c [cce-5-1] eliminated 3 small clauses in 3668825 steps
c [cce-5-1] completed small round (ACCE)
c [cce-5-1] eliminated 201 covered clauses in round 1
c [cce-5-2] completed large round (ACCE)
c [cce-5-2] allowing another 3527461 steps for small clauses
c [cce-5-2] scheduling 899 clauses = 459 binary + 440 ternary
c [cce-5-2] tried to eliminate 899 small clauses 100%
c [cce-5-2] completed small round (ACCE)
c [cce-5-2] eliminated 0 covered clauses in round 2
c [cce-5] eliminated 201 covered clauses in TOTAL during 2 rounds
c [cce-5] 201 < 1/100 * 39653 = 396 considered unsuccessful
c [sort-queue-12] sorted 4613 enqueued variables after 1222831 conflicts
c [score-dist-12] active 0 (0%), one 0 (0%), zero 4613 (100%)
c [score-dist-12] max exp 0, different 1 (100%)
c [score-dist-12] median active exp 0, avg 0.0
c [simplification-12] removed 0 variables 0.0% (4613 remain 58%)
c [simplification-12] removed 201 irredundant clauses 0.5% (39452 remain 66%)
c [simplification-12] maximum reduction of 1% = max (0%, 1%)
c [simplification-12] geometric conflict interval increment 300000 = 600000 / 2
c [simplification-12] new conflict interval 900000
c [simplification-12] penalized conflict interval 900000 = 1 * 900000
c [simplification-12] hard conflict limit 2572831 (soft 2122831 + delta 450000)
c [simplification-12] new conflict limit 2122831 (hard 2572831)
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 -  474.4    4613    39452   1243085  187713  19839   558   24   527   21   5%   1024   -9   24   24  100%
c -  504.8    4613    39452   1315115  194781  19876   558   24   521   22   5%   1024  -15   25   24  106%
c -  535.6    4613    39452   1386991  201027  19917   558   23   568   22   4%   1024   30   20   24   86%
c -  566.6    4613    39452   1459260  206849  19949   558   25   511   23   5%   1024  -25   27   24  111%
c -  599.6    4613    39452   1532376  212664  19980   558   25   542   23   5%   1024    0   24   24  100%
c -  633.4    4613    39452   1605990  218112  20008   558   26   519   24   5%   1024  -14   24   25   96%
c -  667.8    4613    39452   1680487  223497  20038   558   26   525   24   5%   1024   -5   27   25  107%
c -  702.2    4613    39452   1755727  228645  20061   558   27   520   25   5%   1024   -7   25   26   95%
c -  737.7    4613    39452   1831870  233777  20081   558   27   504   25   5%   1024  -25   29   26  110%
c -  775.4    4613    39452   1909194  239172  20100   558   26   536   26   5%   1024   -2   22   26   84%
c -  813.9    4613    39452   1987172  244267  20123   558   26   573   26   4%   1024   38   25   26   97%
c -  854.8    4613    39452   2066240  249492  20136   558   27   541   26   5%   1024    2   25   26   94%
c 
c [simplification-13] limit 2122831 conflicts (hard 2572831) hit after 2129694 conflicts
c [quatres-11] found 60175 quaternary clauses 22% in total
c [quatres-11-1] removed 38 duplicate quaternary clauses
c [quatres-11-1] added 6 double-self-subsuming ternary resolvents
c [quatres-11-2] added 56 single-self-subsuming ternary resolvents
c [quatres-11-2] added 926 quaternary resolvents
c [ternres-11] limit 200000000 with penalty 0 = 0 + 0
c [ternres-11] all 4613 free variables schedulable
c [ternres-11] 95 ternary resolvents (4 bin, 91 trn)
c [ternres-11] fully completed ternary resolution
c [transred-11] limit 2000000 with penalty 0 = 0 + 0
c [transred-11] removed 7 transitive binary clauses
c [elim-7] scheduling all variables this time
c [elim-7] scheduled 4613 variables 100%
c [elim-7] limit of 100000000 steps penalty 3 = 3 + 0
c [elim-7] rescheduling of touched variables disabled
c [elim-7-1] no variable eliminated in round 1 in 9336268 steps
c [elim-7] fully completed in 1 rounds
c [elim-7] transition to [ all 0 rem 0 ] state
c [elim-7] eliminated 0 = 0% variables out of 4613 scheduled
c [sort-queue-13] sorted 4613 enqueued variables after 2129694 conflicts
c [score-dist-13] active 0 (0%), one 0 (0%), zero 4613 (100%)
c [score-dist-13] max exp 0, different 1 (100%)
c [score-dist-13] median active exp 0, avg 0.0
c [simplification-13] removed 0 variables 0.0% (4613 remain 58%)
c [simplification-13] removed 6 irredundant clauses 0.0% (39446 remain 66%)
c [simplification-13] maximum reduction of 0% = max (0%, 0%)
c [simplification-13] full geometric conflict interval increment 900000
c [simplification-13] conflict interval soft limit 1000000 reached
c [simplification-13] new conflict interval 1000000
c [simplification-13] penalized conflict interval 1000000 = 1 * 1000000
c [simplification-13] hard conflict limit 3629694 (soft 3129694 + delta 500000)
c [simplification-13] new conflict limit 3129694 (hard 3629694)
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 -  896.8    4613    39446   2146418  255548  20310   555   26   537   27   5%   1024   -2   30   26  113%
c -  938.3    4613    39446   2227413  261096  20332   555   27   544   27   5%   1024   16   32   27  119%
c -  981.6    4613    39446   2308902  266312  20351   555   27   527   28   5%   1024   -5   23   27   86%
c
c CAUGHT SIGNAL 15 SIGTERM
c
c s UNKNOWN
c bate: 0 basic ate = 0 trn 0% + 0 lrg 0% in 0 updates
c bcas: 4 count, 0 added (96 skipped), 230210 steps
c bkwd: tried 20147 clauses, 39866 lits, 1.98 lits/clause
c bkwd: checked 655203 occs, 32.52 occs/clause, 16.44 occs/lit
c bkwd: subsumed 1 binary, 14 ternary, 137 large
c bkwd: strengthened 0 binary, 0 ternary (0% self), 503 large (0% self)
c blkd: 5 bces, 1162 removed, 1887177 resolutions, 4008661 steps
c blkd: 365 blocking literals 2%, 144 pure
c bump: 0 bumped seen, 0 lits 0.0 on average
c card: 4 count, 7 units, 0 am1, 4662106 steps
c card: 61 rescheduled, 260 eliminated, 37903 resolved, 1948 subsumed
c card: 12 at-most-one constraints found, average size 3.00
c card: 12 at-most-one constraints used 100%, average size 3.00
c card: 176 at-most-two constraints found, average size 4.01
c card: 175 at-most-two constraints used 99%, average size 4.01
c cces: 5 cces, 8690 eliminated, 8477 ate 98%, 213 abce 2%
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: 50 gcs, 0 rescored clauses, 0 rescored vars
c dcps: 28 decompositions, 29 equivalent 0%
c deco: 136 decision-only clauses 0%, 40% reduction
c decs: 52501513 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 7 elims, 3304 eliminated 41%, 13 pure 0%
c elms: 17 rounds, 2.4 rounds/bve
c elms: 3147 small 95%, 0 large 0%
c elms: 26248 tried small, 3147 succeeded 12%, 23101 failed 88%
c elms: 995 subsumed, 1122 strengthened, 3 blocked
c elms: 2043181 copies, 3785514 resolutions, 2473511 ipos
c elms: 58640 subchks, 49216 strchks
c gaus: 4 extractions, 32983 extracted, 3.5 size, 4 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 1 gc, 12832222 steps, 6416111 extr 50%, 4412430 elim 34%
c glue: 21.3 orig avg, 21.3 real avg, 3.6 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 538 = 405 simple 75% + 120 trn 22% + 13 lrg 2%, 5 sub 1%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 2339198 clauses, 33.5 length
c lrnd: 78266042 lits = 82332155 orig - 4066113 removed 5%
c lrnd: 1637791 uips 70%, 196115 flips 8%
c mins: 2024965 mins 87%, 61 bin 0%, 311600 size 13%
c mins: 40452537 poisoned searches, 2763392 hits, 7% hit rate
c mins: 110532522 used twice searches, 35812544 hits, 32% hit rate
c move: moved 1011, 19 bin 2%, 992 trn 98%
c otfs: 9544 driving 48%, 10218 restarting 52%
c otfs: str 19762, 19262 red 97%, 500 irr 3%
c otfs: str 19762, 0 bin 0%, 290 trn 1%, 19472 lrg 99%
c otfs: sub 317, 316 red 100%, 1 irr 0%
c otfs: sub 317, 0 bin 0%, 78 trn 25%, 239 lrg 75%
c phas: 1 computed, 5331 set, 0 pos (0%), 5331 neg (100%)
c prbs: 2 basic, 6984 probed, 0 failed, 0 lifted
c prbs: 3 simple, 27260 probed, 4 failed, 25 eqs
c prbs: 3 treelook, 12464 probed, 0 failed, 0 lifted
c prom: 152098 locked 33% out of 459387 tried
c prps: 561582683 props, 11 props/dec
c prps: 100% srch, 0% simp, 0% lkhd
c quat: 11 count, 8821 quat, 3198 self1, 64 self2, 86 dup
c queu: 13 sorted, 52501513 next (0 steps 0.00)
c queu: 69255 enq (69241 steps 1.00), 0 deq 0%
c redc: 2935 clauses 1%, 422385 tried 18%, 0 sat 0%
c redc: 3027 lits 0%, 3240428 tried 4%, 0 sat 0%
c redc: 83 times jump level reduced, 33.8 levels on average
c reds: 33 count, 71150.0 conflicts per reduce
c reds: 0 memlim 0%, 33 arith 100%
c reds: 966541 collected 48%, 1053908 retired 52%
c rmbd: 58 removed, 58 red 100%
c rsts: 31666 restarts 100%, 0 skipped 0%
c rsts: 0 saturating 0%, 0 reuse 0%
c rsts: 0 kept 0.0% average 0.0%
c scnc: 0 count, 1.000 min (0/1000), 1.000 max (0/1000)
c simp: 13 count, 12 confs 92%, 0 vars 0%
c simp: 0 its 0%, 0 bin 0%, 1 trns 8%
c subl: 2339198 count (1991686 tried 0.9), 6624 sub out of 2328846 (0.3%)
c swps: 4 count, 6 rounds, 2210 queries (368.3/round)
c swps: 2214 sat calls, 4 unsat (0.4% success rate)
c swps: 35350 decisions 16.0, 791 conflicts 0.4
c swps; 320.9 avg class size, 35.3 avg environment size
c swps: 0 failed, 3 impls, 0 equivs
c swp0: 736 type 0 queries, 7 unsat (1.0%), 736 sat (100.0%)
c swp1: 1474 type 1 queries, 40 unsat (2.7%), 1474 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: 105003265 calls to obtain time
c tops: 19 fixed 0%, 0 its, 0.00 confs/it
c trds: 11 transitive reductions, 134 removed, 0 failed
c trds: 102240 nodes, 10211 edges, 16529 steps
c trim: 43848 words, 0.2 MB
c trnr: 11 count, 75 bin, 7526 trn, 39925577 steps
c unhd: 4 count, 4 rounds, 1259360 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: 1118 tauts, 0 bin 0%, 1017 trn 91%, 86 lrg 8%
c unhd: 1118 tauts, 15 stamp 1%, 1082 red 97%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 6025 str, 0 bin 0%, 124 trn 2%, 5901 lrg 98%, 5927 red 98%
c vars: 4613 remaining 58% and 3352 removed 42% out of 7965
c vars: 19 fixed 0%, 3304 eliminated 41%, 29 equivalent 0%
c vsts: 26742963613 visits, 100% srch, 0% simp, 0% lkhd
c vsts: 47.6 search visits per propagation, 11388.5 per conflict
c wchs: 11997510885 pushed, 18672090 enlarged, 1279 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all        2337667        966541       1053908     166934258      17910458       1037583
c 
c  0 0        268303  11       123   0         0   0 156949483  94< 15694793  88<   914583  88<    7.7
c  1 5        185824   8    100702  10     79126   8   4159037   2    582919   3     37954   4     0.3
c  2 6        472328  20    233285  24    228689  22   2845943   2    603646   3     34118   3     0.8
c  3 9        425392  18    200908  21    215211  20   1227122   1    388116   2     19330   2     1.0
c  4 14       291888  12<   136641  14<   149006  14<   645305   0    231514   1     11412   1     1.1
c  5 21       207203   9     93641  10    108923  10    380996   0    142792   1      7026   1     1.2
c  6 30       151947   6     65834   7     82524   8    247346   0     92806   1      4551   0     1.4
c  7 41       110581   5     46752   5     61100   6    167225   0     62482   0      3053   0     1.5
c  8 54        78617   3     32669   3     43932   4    113867   0     42177   0      1960   0     1.5
c  9 69        54820   2     22165   2     31195   3     76583   0     27914   0      1413   0     1.4
c 10 86        61038   3     23850   2     35487   3     82791   0     29239   0      1472   0     2.4
c 11 126       28825   1      9808   1     18037   2     37538   0     11844   0       694   0     2.1
c 12 230         898   0       162   0       676   0      1017   0       215   0        17   0     0.1
c 13 534           3   0         1   0         2   0         5   0         1   0         0   0     0.0
c 
c avg                  3.6           3.8           4.2           0.1           0.4           0.3
c std                  2.6           2.3           2.5           0.7           1.2           1.2
c 
c   31.886   3% decide
c    3.289   0% elim
c    1.709   0% quatres
c 
c    2.341 < 1% rest (below)
c 
c    1.682   0% cce
c    0.503   0% sweep
c    0.498   0% probe
c    0.470   0% gauss
c    0.291   0% ternres
c    0.290   0% block
c    0.105   0% card
c    0.100   0% unhide
c    0.063   0% bca
c    0.019   0% transred
c    0.000   0% bump
c    0.000   0% locs
c    0.000   0% queuesort
c    0.000   0% rescore
c ==================================
c    0.666   0% preprocessing     7%
c    9.412   1% inprocessing     93%
c ==================================
c   10.078   1% simplifying
c  989.938  99% search
c ==================================
c 1000.017 100% all
c 
c       2347951 conflicts,        2347.9 confs/sec
c         10098 ternaries,         232.5 confs/ternary
c            90 binaries,        26088.3 confs/binary
c             0 iterations,          0.0 confs/iteration
c 
c            33 reductions,          0.0 redus/sec,  71150.0 confs/reduction
c         31666 restarts,           31.7 rests/sec,     74.1 confs/restart
c      52501513 decisions,       52500.6 decis/sec,     22.4 decis/conflict
c     561582683 propagations,   561573.2 props/sec,     10.7 props/decision
c 
c 1000.0 seconds, 73.2 MB
c
c CAUGHT SIGNAL 15 SIGTERM
c
c launch: done
