c launch: /data/cnf/sc2014/app/006-23-96.cnf.bz2
c host: atom05
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/006-23-96.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/006-23-96.cnf.bz2
c no embedded options
c found 'p cnf 4288 132608' header
c read 4288 variables, 132608 clauses, 873663 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 3813 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    3813    76353         0       0      0     0    0     0    4   0%      0    0    0    0    0%
c 
c [simplification-1] limit 0 conflicts (hard 0) hit after 0 conflicts
c [card-1] limit 2000000 penalty 0 = 0 + 0
c [card-1] found 3 at-most-one constraints of average size 3.0
c [card-1] found 7 at-most-two constraints of average size 4.0
c [card-1] using previous limit 2000000 for elimination
c [card-1] 9 out of 10 constraints (90%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 642 variables
c [simpleprobe-1] all 3646 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 136 variables
c [simpleprobe-1] fully completed simple probing
c [simpleprobe-1] removed 136 variables, found 8 hbrs, 56 units
c [unhide-1] limit 100000 with penalty 0 = 0 + 0
c [unhide-1-1] 0 units, 0 failed, 631 tauts, 0 hbrs, 22 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 3510 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 101 variables 3% in round 1 in 2141727 steps
c [elim-1-1] backward subsumption/strengthening limit 2141700
c [elim-1-1-1] backward checking 1171 touched variables 33%
c [elim-1-1-1] fully completed backward checking in 1 rounds
c [elim-1-1] subsumed 22 and strengthened 56 clauses in 791191 steps
c [elim-1-1] rescheduled 136 variables 4% by backward subsumption
c [elim-1-2] eliminated 2 variables 0% in round 2 in 131804 steps
c [elim-1-2] backward subsumption/strengthening limit 131800
c [elim-1-2-1] backward checking 33 touched variables 1%
c [elim-1-2-1] fully completed backward checking in 1 rounds
c [elim-1-2] subsumed 0 and strengthened 0 clauses in 103894 steps
c [elim-1] fully completed in 2 rounds
c [elim-1] transition to [ all 0 rem 0 ] state
c [elim-1] eliminated 104 = 3% variables out of 3510 scheduled
c [phase-count-1] 67543 negative 99.2% of 68067 except 524 0.8%
c [phase-count-1] 67237 positive 98.8% of 68067 except 830 1.2%
c [phase-1] phase bias: 1460 positive 43%, 1946 negative 57%
c [score-distribution-1] 0 pos 0.00%, 0 min 0.00%, 3406 zero 100.00%
c [score-distribution-1] 1 different 0.03% out of total 3406 variables
c [simplification-1] removed 393 variables 10.3% (3406 remain 89%)
c [simplification-1] removed 8286 irredundant clauses 10.9% (68067 remain 89%)
c [simplification-1] maximum reduction of 11% = max (10%, 11%)
c [simplification-1] large reduction 11% >= 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 3406 free variables schedulable
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [simpleprobe-2] 1203 variables remain 35% (2203 retained 65%)
c [simpleprobe-2] removed 0 variables, found 1 hbrs, 0 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 6812 literals 100%
c [treelook-1] scheduling used 292646 steps
c [treelook-1] scheduled completely
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 300895 steps
c [treelook-1] 5603 literals remain 82%
c [treelook-1] 3398 variables remain to probed next time 100%
c [treelook-1] removed 0 variables, found 6 hbrs
c [basicprobe-1] limit 1000000 penalty 0 = 0 + 0
c [basicprobe-1-0] 349 sched 10%, 0 failed, 0 lifted, 13 hbrs
c [basicprobe-1-1] 355 sched 10%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-1-1] fully completed probing
c [basicprobe-1-1] removed 0 variables, found 13 hbrs
c [block-1] scheduling all variables this time
c [block-1] scheduled 3406 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 199 blocked clauses
c [block-1] 199 < 1/100 * 68066 = 680 considered unsuccessful
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 3500 clauses out of 21489 (16%) of length 7
c [cce-1-1] eliminated 448 clauses out of 20705 (2%) of length 6
c [cce-1-1] eliminated 2457 clauses out of 13692 (18%) of length 5
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 6405 large clauses in 30000061 steps
c [cce-1-1] allowing another 15000030 steps for small clauses
c [cce-1-1] scheduling 885 clauses = 231 binary + 654 ternary
c [cce-1-1] tried to eliminate 885 small clauses 100%
c [cce-1-1] eliminated 2 binary clauses 1%
c [cce-1-1] eliminated 44 ternary clauses 7%
c [cce-1-1] eliminated 46 small clauses 5%
c [cce-1-1] eliminated 46 small clauses in 15206627 steps
c [cce-1-1] completed small round (ATE)
c [cce-1-1] eliminated 6451 covered clauses in round 1
c [cce-1-2] incomplete large round (ATE)
c [cce-1-2] allowing another 7396702 steps for small clauses
c [cce-1-2] scheduling 839 clauses = 229 binary + 610 ternary
c [cce-1-2] tried to eliminate 839 small clauses 100%
c [cce-1-2] completed small round (ATE)
c [cce-1-2] eliminated 0 covered clauses in round 2
c [cce-1] eliminated 6451 covered clauses in TOTAL during 2 rounds
c [elim-2] scheduling all variables this time
c [elim-2] scheduled 3406 variables 100%
c [elim-2] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-2] rescheduling of touched variables disabled
c [elim-2] incomplete 736 not tried 22% in round 1
c [elim-2] transition to [ all 1 rem 1 ] state
c [elim-2] eliminated 20 = 1% variables out of 3406 scheduled
c [elim-2] 20 < 1/100 * 3406 = 34 considered unsuccessful
c [bca-1] limit of 10000000 steps and 121876 added (scaled 2)
c [bca-1] 5269 out of 6774 literals actually usable 78%
c [bca-1] added 0 blocked clauses in 35140 steps
c [sweep-1] limit 1000000 penalty 0 = 0 + 0
c [sweep-1-1] 932 pos 27.5% + 2454 neg 72.5% = 3386 sched 100.0% ret 0
c [sweep-1-1] 512111 steps 571 queries 181.86 avg class size
c [sweep-1-1] 8814 decisions 570 SAT calls 21.38 avg env size
c [sweep-1-1] fully completed sweeping round
c [decomp-7] removed 3 variables
c [sweep-1-1] removed 3 vars (0 failed, 3 eqs, 2 impls)
c [sweep-1-2] 1512 pos 44.7% + 1871 neg 55.3% = 3383 sched 100.0% ret 0
c [sweep-1-2] 473609 steps 542 queries 128.65 avg class size
c [sweep-1-2] 8830 decisions 542 SAT calls 22.69 avg env size
c [sweep-1-2] fully completed sweeping round
c [decomp-8] removed 3 variables
c [sweep-1-2] removed 3 vars (0 failed, 2 eqs, 3 impls)
c [sweep-1-3] 1526 pos 45.1% + 1854 neg 54.9% = 3380 sched 100.0% ret 0
c [sweep-1-3] 14874 steps 15 queries 1086.07 avg class size
c [sweep-1-3] 239 decisions 14 SAT calls 26.07 avg env size
c [sweep-1-3] 3335 variables remain 99% (45 retained 1%)
c [decomp-9] removed 1 variables
c [sweep-1-3] removed 1 vars (0 failed, 0 eqs, 0 impls)
c [sweep-1] removed 7 vars in TOTAL (3 rounds, 1125 queries)
c [phase-count-2] 60077 negative 99.0% of 60657 except 580 1.0%
c [phase-count-2] 59808 positive 98.6% of 60657 except 849 1.4%
c [phase-2] phase bias: 0 positive 0%, 0 negative 0%
c [score-distribution-2] 3038 pos 89.91%, 0 min 0.00%, 341 zero 10.09%
c [score-distribution-2] 1240 different 36.70% out of total 3379 variables
c [simplification-2] removed 27 variables 0.8% (3379 remain 89%)
c [simplification-2] removed 7409 irredundant clauses 10.9% (60657 remain 79%)
c [simplification-2] maximum reduction of 11% = max (1%, 11%)
c [simplification-2] large reduction 11% >= 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 7321 quaternary clauses 13% in total
c [quatres-1-1] added 29 double-self-subsuming ternary resolvents
c [quatres-1-2] added 75 single-self-subsuming ternary resolvents
c [quatres-1-2] added 283 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 3379 free variables schedulable
c [ternres-1] 222 ternary resolvents (31 bin, 191 trn)
c [ternres-1] fully completed ternary resolution
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] no at-most-one constraint found
c [card-2] found 5 at-most-two constraints of average size 4.2
c [card-2] using previous limit 1000000 for elimination
c [card-2] 5 out of 5 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 4428 xors of average arity 4.7
c [gauss-1] connected 20650 occurrences of 912 variables (average 22.6)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] connected 2013 occurrences of 912 variables (average 2.2)
c [gauss-1] fully completed
c [gauss-1] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-10] removed 6 variables
c [unhide-2] limit 50000 with penalty 1 = 1 + 0
c [unhide-2-2] 0 units, 4 failed, 58 tauts, 0 hbrs, 140 literals
c [transred-1] limit 100000 with penalty 0 = 0 + 0
c [transred-1] removed 8 transitive binary clauses
c [cce-2] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-2-1] eliminated 4 clauses out of 16839 (0%) of length 7
c [cce-2-1] eliminated 171 clauses out of 20709 (1%) of length 6
c [cce-2-1] eliminated 177 clauses out of 11377 (2%) of length 5
c [cce-2-1] eliminated 246 clauses out of 6603 (4%) of length 4
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] eliminated 598 large clauses in 30000065 steps
c [cce-2-1] allowing another 15000032 steps for small clauses
c [cce-2-1] scheduling 891 clauses = 253 binary + 638 ternary
c [cce-2-1] tried to eliminate 891 small clauses 100%
c [cce-2-1] eliminated 6 binary clauses 2%
c [cce-2-1] eliminated 15 ternary clauses 2%
c [cce-2-1] eliminated 21 small clauses 2%
c [cce-2-1] eliminated 29 small clauses in 15209870 steps
c [cce-2-1] completed small round (ATE)
c [cce-2-1] eliminated 627 covered clauses in round 1
c [cce-2-2] incomplete large round (ATE)
c [cce-2-2] allowing another 7395118 steps for small clauses
c [cce-2-2] scheduling 870 clauses = 247 binary + 623 ternary
c [cce-2-2] tried to eliminate 870 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 627 covered clauses in TOTAL during 2 rounds
c [sweep-2] limit 1000000 penalty 0 = 0 + 0
c [sweep-2-1] 1575 pos 47.3% + 1752 neg 52.7% = 3327 sched 98.7% ret 45
c [sweep-2-1] 514590 steps 542 queries 152.42 avg class size
c [sweep-2-1] 9128 decisions 542 SAT calls 23.43 avg env size
c [sweep-2-1] fully completed sweeping round
c [decomp-11] removed 1 variables
c [sweep-2-1] removed 1 vars (0 failed, 1 eqs, 0 impls)
c [sweep-2-2] 1598 pos 47.4% + 1773 neg 52.6% = 3371 sched 100.0% ret 0
c [sweep-2-2] 485568 steps 523 queries 178.78 avg class size
c [sweep-2-2] 8430 decisions 522 SAT calls 23.07 avg env size
c [sweep-2-2] 98 variables remain 3% (3273 retained 97%)
c [sweep-2-2] removed 0 vars (0 failed, 0 eqs, 1 impls)
c [sweep-2] 1 < 1/1000 * 3372 = 3 considered unsuccessful
c [sweep-2] removed 1 vars in TOTAL (2 rounds, 1063 queries)
c [score-distribution-3] 3137 pos 93.06%, 138 min 4.09%, 96 zero 2.85%
c [score-distribution-3] 1387 different 41.15% out of total 3371 variables
c [simplification-3] removed 8 variables 0.2% (3371 remain 88%)
c [simplification-3] removed 643 irredundant clauses 1.1% (60014 remain 79%)
c [simplification-3] maximum reduction of 1% = max (0%, 1%)
c [simplification-3] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-3] new conflict interval 10000
c [simplification-3] penalized conflict interval 10000 = 1 * 10000
c [simplification-3] hard conflict limit 23000 (soft 13000 + delta 10000)
c [simplification-3] new conflict limit 13000 (hard 23000)
c 
c [simplification-4] limit 13000 conflicts (hard 23000) hit after 13000 conflicts
c [quatres-2] found 8197 quaternary clauses 13% in total
c [quatres-2-1] added 43 double-self-subsuming ternary resolvents
c [quatres-2-2] added 201 single-self-subsuming ternary resolvents
c [quatres-2-2] added 303 quaternary resolvents
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] all 3371 free variables schedulable
c [ternres-2] 157 ternary resolvents (9 bin, 148 trn)
c [ternres-2] fully completed ternary resolution
c [decomp-13] removed 1 variables
c [treelook-2] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-2] scheduled 3330 literals 49%
c [treelook-2] scheduling used 150004 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-2] used 150166 steps
c [treelook-2] 2704 literals remain 40%
c [treelook-2] 1590 variables remain to probed next time 47%
c [treelook-2] removed 0 variables, found 16 hbrs
c [unhide-3] limit 100000 with penalty 0 = 0 + 0
c [unhide-3-3] 1 units, 0 failed, 86 tauts, 0 hbrs, 176 literals
c [transred-2] limit 233946 with penalty 0 = 0 + 0
c [transred-2] removed 12 transitive binary clauses
c [block-2] scheduling all variables this time
c [block-2] scheduled 3369 variables 100%
c [block-2] limit of 25000000 steps penalty 1 = 1 + 0
c [block-2] fully completed
c [block-2] transition to [ all 0 rem 0 ] state
c [block-2] eliminated 0 blocked clauses
c [cce-3] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-3-1] eliminated 2 clauses out of 16727 (0%) of length 7
c [cce-3-1] eliminated 7 clauses out of 20579 (0%) of length 6
c [cce-3-1] eliminated 16 clauses out of 11233 (0%) of length 5
c [cce-3-1] eliminated 17 clauses out of 6282 (0%) of length 4
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 42 large clauses in 30000019 steps
c [cce-3-1] allowing another 15000009 steps for small clauses
c [cce-3-1] scheduling 944 clauses = 262 binary + 682 ternary
c [cce-3-1] tried to eliminate 944 small clauses 100%
c [cce-3-1] eliminated 1 binary clauses 0%
c [cce-3-1] eliminated 7 ternary clauses 1%
c [cce-3-1] eliminated 8 small clauses 1%
c [cce-3-1] eliminated 8 small clauses in 15246258 steps
c [cce-3-1] completed small round (ACCE)
c [cce-3-1] eliminated 50 covered clauses in round 1
c [cce-3-2] incomplete large round (ACCE)
c [cce-3-2] allowing another 7376904 steps for small clauses
c [cce-3-2] scheduling 936 clauses = 261 binary + 675 ternary
c [cce-3-2] tried to eliminate 936 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 50 covered clauses in TOTAL during 2 rounds
c [cce-3] 50 < 1/100 * 59974 = 599 considered unsuccessful
c [elim-3] 736 variables 22% will be scheduled this time
c [elim-3] scheduled 736 variables 22%
c [elim-3] limit of 10000000 steps penalty 1 = 1 + 0
c [elim-3] rescheduling of touched variables disabled
c [elim-3] incomplete 320 not tried 9% in round 1
c [elim-3] transition to [ all 0 rem 1 ] state
c [elim-3] eliminated 0 = 0% variables out of 736 scheduled
c [bca-2] limit of 10000000 steps and 120322 added (scaled 2)
c [bca-2] 469 out of 6740 literals actually usable 7%
c [bca-2] added 0 blocked clauses in 16816 steps
c [score-distribution-4] 2130 pos 63.22%, 1185 min 35.17%, 54 zero 1.60%
c [score-distribution-4] 1038 different 30.81% out of total 3369 variables
c [simplification-4] removed 2 variables 0.1% (3369 remain 88%)
c [simplification-4] removed 101 irredundant clauses 0.2% (59911 remain 78%)
c [simplification-4] maximum reduction of 0% = max (0%, 0%)
c [simplification-4] full geometric conflict interval increment 20000
c [simplification-4] new conflict interval 30000
c [simplification-4] penalized conflict interval 30000 = 1 * 30000
c [simplification-4] hard conflict limit 58000 (soft 43000 + delta 15000)
c [simplification-4] new conflict limit 43000 (hard 58000)
c 
c [simplification-5] limit 43000 conflicts (hard 58000) hit after 43000 conflicts
c [quatres-3] found 10152 quaternary clauses 15% in total
c [quatres-3-1] added 45 double-self-subsuming ternary resolvents
c [quatres-3-2] added 345 single-self-subsuming ternary resolvents
c [quatres-3-2] added 299 quaternary resolvents
c [ternres-3] limit 4000000 with penalty 0 = 0 + 0
c [ternres-3] all 3369 free variables schedulable
c [ternres-3] 71 ternary resolvents (5 bin, 66 trn)
c [ternres-3] fully completed ternary resolution
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] extracted 1478 xors of average arity 4.0
c [gauss-2] connected 5902 occurrences of 373 variables (average 15.8)
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 [unhide-4] limit 242677 with penalty 0 = 0 + 0
c [unhide-4-4] 0 units, 0 failed, 132 tauts, 0 hbrs, 1165 literals
c [transred-3] limit 1213386 with penalty 0 = 0 + 0
c [transred-3] removed 5 transitive binary clauses
c [sweep-3] limit 500000 penalty 1 = 1 + 0
c [sweep-3-1] 53 pos 54.1% + 45 neg 45.9% = 98 sched 2.9% ret 3271
c [sweep-3-1] 122905 steps 55 queries 14.75 avg class size
c [sweep-3-1] 2367 decisions 54 SAT calls 73.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] 1740 pos 51.6% + 1629 neg 48.4% = 3369 sched 100.0% ret 0
c [sweep-3-2] 377813 steps 131 queries 270.37 avg class size
c [sweep-3-2] 7130 decisions 130 SAT calls 88.81 avg env size
c [sweep-3-2] 1235 variables remain 37% (2134 retained 63%)
c [sweep-3-2] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-3] removed 0 vars in TOTAL (2 rounds, 184 queries)
c [score-distribution-5] 2857 pos 84.80%, 467 min 13.86%, 45 zero 1.34%
c [score-distribution-5] 1488 different 44.17% out of total 3369 variables
c [simplification-5] removed 0 variables 0.0% (3369 remain 88%)
c [simplification-5] removed 0 irredundant clauses 0.0% (59911 remain 78%)
c [simplification-5] maximum reduction of 0% = max (0%, 0%)
c [simplification-5] full geometric conflict interval increment 30000
c [simplification-5] new conflict interval 60000
c [simplification-5] penalized conflict interval 60000 = 1 * 60000
c [simplification-5] hard conflict limit 133000 (soft 103000 + delta 30000)
c [simplification-5] new conflict limit 103000 (hard 133000)
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 -   16.6    3369    59911     75442   28472   2369   153   12   307    9   4%    695  115   10    7  153%
c 
c [simplification-6] limit 103000 conflicts (hard 133000) hit after 103000 conflicts
c [quatres-4] found 12942 quaternary clauses 16% in total
c [quatres-4-1] removed 4 duplicate quaternary clauses
c [quatres-4-1] added 38 double-self-subsuming ternary resolvents
c [quatres-4-2] added 439 single-self-subsuming ternary resolvents
c [quatres-4-2] added 244 quaternary resolvents
c [ternres-4] limit 4130950 with penalty 0 = 0 + 0
c [ternres-4] all 3369 free variables schedulable
c [ternres-4] 40 ternary resolvents (5 bin, 35 trn)
c [ternres-4] fully completed ternary resolution
c [card-3] limit 516368 penalty 2 = 2 + 0
c [card-3] found 3 at-most-one constraints of average size 3.0
c [card-3] found 12 at-most-two constraints of average size 4.1
c [card-3] using previous limit 516368 for elimination
c [card-3] 15 out of 15 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [basicprobe-2] limit 10327376 penalty 1 = 1 + 0
c [basicprobe-2-0] 498 sched 15%, 0 failed, 0 lifted, 6 hbrs
c [basicprobe-2-1] 499 sched 15%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-2-1] fully completed probing
c [basicprobe-2-1] removed 0 variables, found 6 hbrs
c [bate-1] eliminated 19 asymmetric tautologies during probing
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 8 transitive binary clauses
c [cce-4] boosting limit by 10
c [cce-4] limit of 150000000 steps penalty 1 = 1 + 0
c [cce-4-1] eliminated 6 clauses out of 16243 (0%) of length 7
c [cce-4-1] eliminated 68 clauses out of 20876 (0%) of length 6
c [cce-4-1] eliminated 30 clauses out of 11300 (0%) of length 5
c [cce-4-1] eliminated 174 clauses out of 6173 (3%) of length 4
c [cce-4-1] completed large round (ATE)
c [cce-4-1] eliminated 278 large clauses in 29449267 steps
c [cce-4-1] allowing another 14724633 steps for small clauses
c [cce-4-1] scheduling 4544 clauses = 278 binary + 4266 ternary
c [cce-4-1] tried to eliminate 4544 small clauses 100%
c [cce-4-1] eliminated 1030 ternary clauses 24%
c [cce-4-1] eliminated 1030 small clauses 23%
c [cce-4-1] eliminated 1030 small clauses in 15881407 steps
c [cce-4-1] completed small round (ATE)
c [cce-4-1] completed small and large (ATE)
c [cce-4-1] eliminated 1308 covered clauses in round 1
c [cce-4-2] completed large round (ATE)
c [cce-4-2] allowing another 14540840 steps for small clauses
c [cce-4-2] scheduling 3514 clauses = 278 binary + 3236 ternary
c [cce-4-2] tried to eliminate 3514 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 1308 covered clauses in TOTAL during 2 rounds
c [score-distribution-6] 2910 pos 86.38%, 438 min 13.00%, 21 zero 0.62%
c [score-distribution-6] 1513 different 44.91% out of total 3369 variables
c [simplification-6] removed 0 variables 0.0% (3369 remain 88%)
c [simplification-6] removed 1328 irredundant clauses 2.2% (58583 remain 77%)
c [simplification-6] maximum reduction of 2% = max (0%, 2%)
c [simplification-6] geometric conflict interval increment 20000 = 60000 / 3
c [simplification-6] new conflict interval 80000
c [simplification-6] penalized conflict interval 80000 = 1 * 80000
c [simplification-6] hard conflict limit 223000 (soft 183000 + delta 40000)
c [simplification-6] new conflict limit 183000 (hard 223000)
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 -   29.2    3369    58583    129635   35881   4244   168   14   311   16   4%    880   52   15   10  152%
c 
c [simplification-7] limit 183000 conflicts (hard 223000) hit after 183000 conflicts
c [quatres-5] found 15365 quaternary clauses 17% in total
c [quatres-5-1] removed 7 duplicate quaternary clauses
c [quatres-5-1] added 23 double-self-subsuming ternary resolvents
c [quatres-5-2] added 317 single-self-subsuming ternary resolvents
c [quatres-5-2] added 205 quaternary resolvents
c [ternres-5] limit 8681442 with penalty 0 = 0 + 0
c [ternres-5] all 3369 free variables schedulable
c [ternres-5] 32 ternary resolvents (2 bin, 30 trn)
c [ternres-5] fully completed ternary resolution
c [unhide-5] limit 868144 with penalty 1 = 1 + 0
c [unhide-5-6] 0 units, 0 failed, 101 tauts, 0 hbrs, 4086 literals
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 6 transitive binary clauses
c [block-3] scheduling all variables this time
c [block-3] scheduled 3369 variables 100%
c [block-3] limit of 21703607 steps penalty 2 = 2 + 0
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 0 blocked clauses
c [cce-5] limit of 43407214 steps penalty 0 = 0 + 0
c [cce-5-1] eliminated 4 clauses out of 20861 (0%) of length 6
c [cce-5-1] eliminated 2 clauses out of 11291 (0%) of length 5
c [cce-5-1] eliminated 19 clauses out of 5987 (0%) of length 4
c [cce-5-1] completed large round (ACCE)
c [cce-5-1] eliminated 25 large clauses in 32076089 steps
c [cce-5-1] allowing another 16038044 steps for small clauses
c [cce-5-1] scheduling 1037 clauses = 279 binary + 758 ternary
c [cce-5-1] tried to eliminate 1037 small clauses 100%
c [cce-5-1] eliminated 6 ternary clauses 1%
c [cce-5-1] eliminated 6 small clauses 1%
c [cce-5-1] eliminated 6 small clauses in 16310029 steps
c [cce-5-1] completed small round (ACCE)
c [cce-5-1] completed small and large (ACCE)
c [cce-5-1] eliminated 31 covered clauses in round 1
c [cce-5-2] incomplete large round (ACCE)
c [cce-5-2] allowing another 13548611 steps for small clauses
c [cce-5-2] scheduling 1031 clauses = 279 binary + 752 ternary
c [cce-5-2] tried to eliminate 1031 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 31 covered clauses in TOTAL during 2 rounds
c [cce-5] 31 < 1/100 * 58583 = 585 considered unsuccessful
c [elim-4] scheduling all variables this time
c [elim-4] scheduled 3369 variables 100%
c [elim-4] boosting limit by 20
c [elim-4] limit of 868144295 steps penalty 2 = 2 + 0
c [elim-4] rescheduling of touched variables disabled
c [elim-4-1] eliminated 4 variables 0% in round 1 in 44451379 steps
c [elim-4-1] backward subsumption/strengthening limit 44451300
c [elim-4-1-1] backward checking 1273 touched variables 38%
c [elim-4-1-1] fully completed backward checking in 1 rounds
c [elim-4-1] subsumed 1 and strengthened 6 clauses in 640589 steps
c [elim-4-1] rescheduled 12 variables 0% by backward subsumption
c [elim-4-2] no variable eliminated in round 2 in 47102 steps
c [elim-4] fully completed in 2 rounds
c [elim-4] transition to [ all 0 rem 0 ] state
c [elim-4] eliminated 4 = 0% variables out of 3369 scheduled
c [elim-4] 4 < 1/100 * 3369 = 33 considered unsuccessful
c [bca-3] limit of 10000000 steps and 117558 added (scaled 2)
c [bca-3] 39 out of 6732 literals actually usable 1%
c [bca-3] not enough literals usable
c [bca-3] added 0 blocked clauses in 85985 steps
c [score-distribution-7] 2999 pos 89.12%, 365 min 10.85%, 1 zero 0.03%
c [score-distribution-7] 1631 different 48.47% out of total 3365 variables
c [simplification-7] removed 4 variables 0.1% (3365 remain 88%)
c [simplification-7] removed 54 irredundant clauses 0.1% (58529 remain 77%)
c [simplification-7] maximum reduction of 0% = max (0%, 0%)
c [simplification-7] full geometric conflict interval increment 80000
c [simplification-7] new conflict interval 160000
c [simplification-7] penalized conflict interval 160000 = 1 * 160000
c [simplification-7] hard conflict limit 423000 (soft 343000 + delta 80000)
c [simplification-7] new conflict limit 343000 (hard 423000)
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 -   42.9    3365    58529    183653   34898   4782   169   14   331   10   4%    961   37   15   12  128%
c -   52.6    3365    58529    249325   49525   5029   172   15   355   18   4%   1001   28   16   13  120%
c -   62.0    3365    58529    307594   57431   5241   178   17   349   19   5%   1014   14   17   15  116%
c 
c [simplification-8] limit 343000 conflicts (hard 423000) hit after 343001 conflicts
c [quatres-6] found 19886 quaternary clauses 18% in total
c [quatres-6-1] removed 23 duplicate quaternary clauses
c [quatres-6-1] added 26 double-self-subsuming ternary resolvents
c [quatres-6-2] added 370 single-self-subsuming ternary resolvents
c [quatres-6-2] added 253 quaternary resolvents
c [ternres-6] limit 14957353 with penalty 0 = 0 + 0
c [ternres-6] all 3365 free variables schedulable
c [ternres-6] 26 ternary resolvents (3 bin, 23 trn)
c [ternres-6] fully completed ternary resolution
c [gauss-3] limit 747867 penalty 2 = 2 + 0
c [gauss-3] extracted 445 xors of average arity 3.0
c [gauss-3] connected 1335 occurrences of 150 variables (average 8.9)
c [gauss-3] limit 747867 penalty 2 = 2 + 0
c [gauss-3] fully completed
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [simpleprobe-3] 1188 schedulable variables 35%
c [simpleprobe-3] limit 29914707 penalty 1 = 1 + 0
c [simpleprobe-3] fully completed simple probing
c [simpleprobe-3] removed 0 variables, found 19 hbrs, 0 units
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 13 transitive binary clauses
c [sweep-4] limit 1121801 penalty 2 = 2 + 0
c [sweep-4-1] 626 pos 50.7% + 608 neg 49.3% = 1234 sched 36.7% ret 2131
c [sweep-4-1] 836262 steps 147 queries 40.86 avg class size
c [sweep-4-1] 12693 decisions 146 SAT calls 239.33 avg env size
c [sweep-4-1] fully completed sweeping round
c [sweep-4-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-4-2] 1673 pos 49.7% + 1692 neg 50.3% = 3365 sched 100.0% ret 0
c [sweep-4-2] 293227 steps 50 queries 402.96 avg class size
c [sweep-4-2] 4470 decisions 49 SAT calls 319.69 avg env size
c [sweep-4-2] 2096 variables remain 62% (1269 retained 38%)
c [sweep-4-2] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-4] removed 0 vars in TOTAL (2 rounds, 195 queries)
c [score-distribution-8] 3310 pos 98.37%, 55 min 1.63%, 0 zero 0.00%
c [score-distribution-8] 1926 different 57.24% out of total 3365 variables
c [simplification-8] removed 0 variables 0.0% (3365 remain 88%)
c [simplification-8] removed 0 irredundant clauses 0.0% (58529 remain 77%)
c [simplification-8] maximum reduction of 0% = max (0%, 0%)
c [simplification-8] full geometric conflict interval increment 160000
c [simplification-8] new conflict interval 320000
c [simplification-8] penalized conflict interval 320000 = 1 * 320000
c [simplification-8] hard conflict limit 823001 (soft 663001 + delta 160000)
c [simplification-8] new conflict limit 663001 (hard 823001)
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 -   71.6    3365    58529    363896   60650   5732   192   18   359   12   5%   1020   16   20   16  122%
c -   80.3    3365    58529    423272   67840   5793   193   19   341   12   5%   1022  -10   18   17  106%
c -   89.0    3365    58529    481047   73049   5848   193   20   341   13   6%   1023  -16   20   18  108%
c -   97.8    3365    58529    538504   77069   5896   193   21   383   13   6%   1024   18   22   19  116%
c -  106.6    3365    58529    596820   81115   5945   193   22   375   22   6%   1024    5   21   20  101%
c -  115.2    3365    58529    655878   85556   5975   193   23   401   23   6%   1024   23   24   22  112%
c 
c [simplification-9] limit 663001 conflicts (hard 823001) hit after 663001 conflicts
c [quatres-7] found 24029 quaternary clauses 18% in total
c [quatres-7-1] removed 49 duplicate quaternary clauses
c [quatres-7-1] added 14 double-self-subsuming ternary resolvents
c [quatres-7-2] added 229 single-self-subsuming ternary resolvents
c [quatres-7-2] added 134 quaternary resolvents
c [ternres-7] limit 28478394 with penalty 0 = 0 + 0
c [ternres-7] all 3365 free variables schedulable
c [ternres-7] 3 ternary resolvents (0 bin, 3 trn)
c [ternres-7] fully completed ternary resolution
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 1 transitive binary clauses
c [cce-6] limit of 71195985 steps penalty 1 = 1 + 0
c [cce-6-1] eliminated 5 clauses out of 21265 (0%) of length 6
c [cce-6-1] eliminated 27 clauses out of 11368 (0%) of length 5
c [cce-6-1] eliminated 35 clauses out of 5977 (1%) of length 4
c [cce-6-1] completed large round (ATE)
c [cce-6-1] eliminated 67 large clauses in 28949331 steps
c [cce-6-1] allowing another 14474665 steps for small clauses
c [cce-6-1] scheduling 3544 clauses = 280 binary + 3264 ternary
c [cce-6-1] tried to eliminate 3544 small clauses 100%
c [cce-6-1] eliminated 1 binary clauses 0%
c [cce-6-1] eliminated 6 ternary clauses 0%
c [cce-6-1] eliminated 7 small clauses 0%
c [cce-6-1] eliminated 7 small clauses in 15411862 steps
c [cce-6-1] completed small round (ATE)
c [cce-6-1] eliminated 74 covered clauses in round 1
c [cce-6-2] completed large round (ATE)
c [cce-6-2] allowing another 14469906 steps for small clauses
c [cce-6-2] scheduling 3537 clauses = 279 binary + 3258 ternary
c [cce-6-2] tried to eliminate 3537 small clauses 100%
c [cce-6-2] completed small round (ATE)
c [cce-6-2] eliminated 0 covered clauses in round 2
c [cce-6] eliminated 74 covered clauses in TOTAL during 2 rounds
c [cce-6] 74 < 1/100 * 58529 = 585 considered unsuccessful
c [score-distribution-9] 3361 pos 99.88%, 4 min 0.12%, 0 zero 0.00%
c [score-distribution-9] 2394 different 71.14% out of total 3365 variables
c [simplification-9] removed 0 variables 0.0% (3365 remain 88%)
c [simplification-9] removed 74 irredundant clauses 0.1% (58455 remain 77%)
c [simplification-9] maximum reduction of 0% = max (0%, 0%)
c [simplification-9] full geometric conflict interval increment 320000
c [simplification-9] new conflict interval 640000
c [simplification-9] penalized conflict interval 640000 = 1 * 640000
c [simplification-9] hard conflict limit 1623001 (soft 1303001 + delta 320000)
c [simplification-9] new conflict limit 1303001 (hard 1623001)
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 -  125.0    3365    58455    715022   89567   6235   193   23   389   14   6%   1024    3   21   23   95%
c -  134.1    3365    58455    774471   93978   6249   193   25   392   14   6%   1024    2   26   23  109%
c -  143.2    3365    58455    833734   98067   6261   193   25   406   24   6%   1024   13   22   24   89%
c -  152.6    3365    58455    892987  102092   6276   193   26   396   15   7%   1024    1   30   25  121%
c -  162.0    3365    58455    952184  105292   6289   193   26   411   25   6%   1024   14   25   25   98%
c -  171.5    3365    58455   1012121  109129   6302   193   27   401   16   7%   1024   -0   24   26   95%
c -  181.2    3365    58455   1071942  112682   6310   193   26   400   16   7%   1024   -1   26   26   99%
c -  191.2    3365    58455   1131954  115803   6321   193   27   400   26   7%   1024    1   26   27   97%
c -  201.4    3365    58455   1192325  118951   6332   193   28   418   16   7%   1024   14   28   27  101%
c -  211.8    3365    58455   1253160  121712   6338   193   28   400   27   7%   1024   -6   31   28  113%
c 
c [simplification-10] limit 1303001 conflicts (hard 1623001) hit after 1303001 conflicts
c [quatres-8] found 27214 quaternary clauses 16% in total
c [quatres-8-1] removed 104 duplicate quaternary clauses
c [quatres-8-1] added 5 double-self-subsuming ternary resolvents
c [quatres-8-2] added 108 single-self-subsuming ternary resolvents
c [quatres-8-2] added 80 quaternary resolvents
c [ternres-8] limit 60684187 with penalty 0 = 0 + 0
c [ternres-8] all 3365 free variables schedulable
c [ternres-8] 6 ternary resolvents (1 bin, 5 trn)
c [ternres-8] fully completed ternary resolution
c [card-4] limit 3792761 penalty 3 = 3 + 0
c [card-4] found 1 at-most-one constraints of average size 3.0
c [card-4] found 11 at-most-two constraints of average size 4.0
c [card-4] using previous limit 3792761 for elimination
c [card-4] 12 out of 12 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [unhide-6] limit 3034209 with penalty 2 = 2 + 0
c [unhide-6-9] 0 units, 0 failed, 66 tauts, 0 hbrs, 17731 literals
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 2 transitive binary clauses
c [score-distribution-10] 3351 pos 99.58%, 14 min 0.42%, 0 zero 0.00%
c [score-distribution-10] 2455 different 72.96% out of total 3365 variables
c [simplification-10] removed 0 variables 0.0% (3365 remain 88%)
c [simplification-10] removed 1 irredundant clauses 0.0% (58454 remain 77%)
c [simplification-10] maximum reduction of 0% = max (0%, 0%)
c [simplification-10] full geometric conflict interval increment 640000
c [simplification-10] conflict interval soft limit 1000000 reached
c [simplification-10] new conflict interval 1000000
c [simplification-10] penalized conflict interval 1000000 = 1 * 1000000
c [simplification-10] hard conflict limit 2803001 (soft 2303001 + delta 500000)
c [simplification-10] new conflict limit 2303001 (hard 2803001)
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 -  223.2    3365    58454   1314823  124532   6451   190   28   414   28   7%   1024    5   21   28   76%
c -  233.8    3365    58454   1376637  127061   6457   190   30   399   17   7%   1024  -13   34   28  120%
c -  244.7    3365    58454   1439423  130326   6461   190   29   404   29   7%   1024   -6   33   29  115%
c -  255.7    3365    58454   1502592  133713   6465   190   28   425   18   7%   1024   13   34   29  117%
c -  267.2    3365    58454   1565858  136359   6469   190   29   402   29   7%   1024   -9   31   29  105%
c -  278.5    3365    58454   1629688  139942   6471   190   32   415   18   8%   1024    1   30   30   98%
c -  289.5    3365    58454   1693178  143534   6477   190   30   415   18   7%   1024    1   23   31   73%
c -  300.7    3365    58454   1756262  145635   6481   190   32   415   31   8%   1024    2   33   31  105%
c -  312.0    3365    58454   1820319  149012   6485   190   32   411   19   8%   1024   -6   32   32  100%
c -  323.6    3365    58454   1884157  151319   6487   190   33   410   19   8%   1024   -8   33   32  103%
c -  335.0    3365    58454   1948693  153977   6491   190   34   423   32   8%   1024    3   39   32  119%
c -  346.9    3365    58454   2013630  156713   6494   190   33   404   32   8%   1024  -15   38   32  116%
c -  358.9    3365    58454   2078852  158420   6496   190   33   431   20   8%   1024   10   36   32  112%
c -  371.3    3365    58454   2145372  160406   6498   190   32   430   20   7%   1024    9   24   32   75%
c -  383.8    3365    58454   2213041  163407   6502   190   33   416   20   8%   1024   -2   34   33  103%
c -  396.5    3365    58454   2280575  166392   6507   190   34   421   21   8%   1024    3   37   33  110%
c 
c [simplification-11] limit 2303001 conflicts (hard 2803001) hit after 2303001 conflicts
c [quatres-9] found 29324 quaternary clauses 15% in total
c [quatres-9-1] removed 122 duplicate quaternary clauses
c [quatres-9-1] added 5 double-self-subsuming ternary resolvents
c [quatres-9-2] added 51 single-self-subsuming ternary resolvents
c [quatres-9-2] added 34 quaternary resolvents
c [ternres-9] limit 121926235 with penalty 0 = 0 + 0
c [ternres-9] all 3365 free variables schedulable
c [ternres-9] 24 ternary resolvents (1 bin, 23 trn)
c [ternres-9] fully completed ternary resolution
c [treelook-3] limit 3048155 penalty 2 = 2 + 0 boost 1
c [treelook-3] scheduled 3275 literals 49%
c [treelook-3] scheduling used 733076 steps
c [treelook-3] scheduled completely
c [treelook-3] limit 3048155 penalty 2 = 2 + 0 boost 1
c [treelook-3] used 753945 steps
c [treelook-3] fully completed tree based probing
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 0 transitive binary clauses
c [block-4] scheduling all variables this time
c [block-4] scheduled 3365 variables 100%
c [block-4] limit of 100000000 steps penalty 3 = 3 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 0 blocked clauses
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 3365 variables 100%
c [elim-5] limit of 100000000 steps penalty 3 = 3 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5-1] no variable eliminated in round 1 in 44079175 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 3365 scheduled
c [bca-4] limit of 10000000 steps and 117402 added (scaled 2)
c [bca-4] 1 out of 6732 literals actually usable 0%
c [bca-4] not enough literals usable
c [bca-4] added 0 blocked clauses in 188476 steps
c [score-distribution-11] 3330 pos 98.96%, 35 min 1.04%, 0 zero 0.00%
c [score-distribution-11] 2454 different 72.93% out of total 3365 variables
c [simplification-11] removed 0 variables 0.0% (3365 remain 88%)
c [simplification-11] removed 3 irredundant clauses 0.0% (58451 remain 77%)
c [simplification-11] maximum reduction of 0% = max (0%, 0%)
c [simplification-11] full geometric conflict interval increment 1000000
c [simplification-11] conflict interval soft limit 1000000 reached
c [simplification-11] new conflict interval 1000000
c [simplification-11] penalized conflict interval 1000000 = 1 * 1000000
c [simplification-11] hard conflict limit 3803001 (soft 3303001 + delta 500000)
c [simplification-11] new conflict limit 3303001 (hard 3803001)
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 -  410.6    3365    58451   2347906  167840   6585   191   34   426   21   8%   1024    3   38   34  113%
c -  423.7    3365    58451   2416666  169969   6586   191   34   414   34   8%   1024   -5   30   33   90%
c -  437.3    3365    58451   2486435  172900   6588   191   33   426   35   8%   1024    6   26   34   76%
c -  451.1    3365    58451   2556218  175524   6588   191   35   423   35   8%   1024    4   37   34  109%
c -  464.9    3365    58451   2626168  177369   6589   191   34   419   35   8%   1024   -0   38   34  112%
c -  478.9    3365    58451   2697238  179873   6591   191   34   426   22   8%   1024    4   34   34   99%
c -  493.2    3365    58451   2768705  181993   6592   191   34   410   22   8%   1024  -11   35   34  100%
c -  507.9    3365    58451   2840968  184198   6594   191   33   409   36   8%   1024  -14   35   34  102%
c -  522.8    3365    58451   2913922  185851   6596   191   35   426   23   8%   1024    5   37   34  108%
c -  537.9    3365    58451   2988226  188663   6598   191   35   404   23   9%   1024  -14   39   35  113%
c -  553.0    3365    58451   3062651  190671   6600   191   36   418   37   9%   1024   -0   34   34  100%
c -  568.8    3365    58451   3137888  192485   6601   191   34   430   23   8%   1024    8   28   34   82%
c -  584.8    3365    58451   3214322  194733   6602   191   35   422   23   8%   1024    3   41   34  119%
c -  601.1    3365    58451   3291505  196943   6604   191   35   407   23   9%   1024  -10   38   34  109%
c 
c [simplification-12] limit 3303001 conflicts (hard 3803001) hit after 3303002 conflicts
c [quatres-10] found 30453 quaternary clauses 14% in total
c [quatres-10-1] removed 117 duplicate quaternary clauses
c [quatres-10-1] added 1 double-self-subsuming ternary resolvents
c [quatres-10-2] added 28 single-self-subsuming ternary resolvents
c [quatres-10-2] added 28 quaternary resolvents
c [ternres-10] limit 193748746 with penalty 0 = 0 + 0
c [ternres-10] all 3365 free variables schedulable
c [ternres-10] 0 ternary resolvents (0 bin, 0 trn)
c [ternres-10] fully completed ternary resolution
c [gauss-4] limit 4843718 penalty 3 = 3 + 0
c [gauss-4] extracted 4689 xors of average arity 4.8
c [gauss-4] connected 22605 occurrences of 974 variables (average 23.2)
c [gauss-4] limit 4843718 penalty 3 = 3 + 0
c [gauss-4] connected 3005 occurrences of 974 variables (average 3.1)
c [gauss-4] fully completed
c [gauss-4] exported 0 unary, 0 binary and 0 ternary equations
c [cce-7] limit of 242185932 steps penalty 2 = 2 + 0
c [cce-7-1] eliminated 2 clauses out of 21395 (0%) of length 6
c [cce-7-1] eliminated 13 clauses out of 11357 (0%) of length 5
c [cce-7-1] eliminated 7 clauses out of 5969 (0%) of length 4
c [cce-7-1] completed large round (ACCE)
c [cce-7-1] eliminated 22 large clauses in 31858854 steps
c [cce-7-1] allowing another 15929427 steps for small clauses
c [cce-7-1] scheduling 1054 clauses = 282 binary + 772 ternary
c [cce-7-1] tried to eliminate 1054 small clauses 100%
c [cce-7-1] eliminated 5 ternary clauses 1%
c [cce-7-1] eliminated 5 small clauses 0%
c [cce-7-1] eliminated 5 small clauses in 16210320 steps
c [cce-7-1] completed small round (ACCE)
c [cce-7-1] eliminated 27 covered clauses in round 1
c [cce-7-2] completed large round (ACCE)
c [cce-7-2] allowing another 15911635 steps for small clauses
c [cce-7-2] scheduling 1049 clauses = 282 binary + 767 ternary
c [cce-7-2] tried to eliminate 1049 small clauses 100%
c [cce-7-2] completed small round (ACCE)
c [cce-7-2] eliminated 0 covered clauses in round 2
c [cce-7] eliminated 27 covered clauses in TOTAL during 2 rounds
c [cce-7] 27 < 1/100 * 58451 = 584 considered unsuccessful
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 72655778 penalty 3 = 3 + 0
c [sweep-5-1] 1020 pos 48.7% + 1076 neg 51.3% = 2096 sched 62.3% ret 1269
c [sweep-5-1] 1740250 steps 199 queries 42.05 avg class size
c [sweep-5-1] 16620 decisions 198 SAT calls 286.70 avg env size
c [sweep-5-1] fully completed sweeping round
c [sweep-5-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-5-2] 1648 pos 49.0% + 1717 neg 51.0% = 3365 sched 100.0% ret 0
c [sweep-5-2] 1987596 steps 220 queries 71.64 avg class size
c [sweep-5-2] 18153 decisions 219 SAT calls 287.79 avg env size
c [sweep-5-2] fully completed sweeping round
c [sweep-5-2] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-5-3] 1648 pos 49.0% + 1717 neg 51.0% = 3365 sched 100.0% ret 0
c [sweep-5-3] 1787181 steps 214 queries 73.39 avg class size
c [sweep-5-3] 18013 decisions 213 SAT calls 289.27 avg env size
c [sweep-5-3] fully completed sweeping round
c [sweep-5-3] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-5] removed 0 vars in TOTAL (3 rounds, 630 queries)
c [score-distribution-12] 3328 pos 98.90%, 37 min 1.10%, 0 zero 0.00%
c [score-distribution-12] 2274 different 67.58% out of total 3365 variables
c [simplification-12] removed 0 variables 0.0% (3365 remain 88%)
c [simplification-12] removed 27 irredundant clauses 0.0% (58424 remain 77%)
c [simplification-12] maximum reduction of 0% = max (0%, 0%)
c [simplification-12] full geometric conflict interval increment 1000000
c [simplification-12] conflict interval soft limit 1000000 reached
c [simplification-12] new conflict interval 1000000
c [simplification-12] penalized conflict interval 1000000 = 1 * 1000000
c [simplification-12] hard conflict limit 4803002 (soft 4303002 + delta 500000)
c [simplification-12] new conflict limit 4303002 (hard 4803002)
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 -  619.9    3365    58424   3369269  199287   6640   191   36   413   39   9%   1024   -6   34   35   97%
c -  636.7    3365    58424   3447469  201262   6642   191   36   421   24   9%   1024   -3   37   35  107%
c -  653.9    3365    58424   3526428  203436   6642   191   35   423   24   8%   1024   -2   41   35  115%
c -  671.0    3365    58424   3606136  206344   6642   191   36   427   40   8%   1024    5   39   36  109%
c -  688.3    3365    58424   3685842  208240   6644   191   34   429   25   8%   1024    7   25   35   72%
c -  705.9    3365    58424   3766422  210455   6645   191   36   438   25   8%   1024   18   35   35   99%
c -  724.0    3365    58424   3847644  212898   6645   191   37   439   25   8%   1024   16   45   36  127%
c -  742.4    3365    58424   3929182  215271   6645   191   36   438   25   8%   1024   15   43   36  118%
c -  761.0    3365    58424   4011173  216701   6648   191   37   431   41   8%   1024    8   41   35  116%
c -  779.9    3365    58424   4094749  218851   6648   191   35   427   26   8%   1024    4   36   35  102%
c -  799.1    3365    58424   4178957  221395   6648   191   36   427   26   9%   1024    6   27   36   75%
c -  818.3    3365    58424   4263336  223621   6648   191   37   409   26   9%   1024  -14   33   36   90%
c 
c [simplification-13] limit 4303002 conflicts (hard 4803002) hit after 4304275 conflicts
c [quatres-11] found 31157 quaternary clauses 13% in total
c [quatres-11-1] removed 86 duplicate quaternary clauses
c [quatres-11-1] added 1 double-self-subsuming ternary resolvents
c [quatres-11-2] added 10 single-self-subsuming ternary resolvents
c [quatres-11-2] added 25 quaternary resolvents
c [transred-10] limit 1000000 with penalty 1 = 1 + 0
c [transred-10] removed 0 transitive binary clauses
c [score-distribution-13] 3357 pos 99.76%, 8 min 0.24%, 0 zero 0.00%
c [score-distribution-13] 2383 different 70.82% out of total 3365 variables
c [simplification-13] removed 0 variables 0.0% (3365 remain 88%)
c [simplification-13] removed 0 irredundant clauses 0.0% (58424 remain 77%)
c [simplification-13] maximum reduction of 0% = max (0%, 0%)
c [simplification-13] full geometric conflict interval increment 1000000
c [simplification-13] new conflict interval 2000000
c [simplification-13] penalized conflict interval 2000000 = 1 * 2000000
c [simplification-13] hard conflict limit 7304275 (soft 6304275 + delta 1000000)
c [simplification-13] new conflict limit 6304275 (hard 7304275)
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 -  838.3    3365    58424   4348339  225807   6658   191   36   415   26   9%   1024   -8   41   37  111%
c -  857.6    3365    58424   4433838  229491   6659   191   37   414   26   9%   1024   -9   37   37  102%
c -  877.0    3365    58424   4518283  230705   6660   191   38   414   27   9%   1024  -12   37   37  100%
c -  896.4    3365    58424   4604343  233516   6660   191   39   429   27   9%   1024    8   44   37  118%
c -  916.7    3365    58424   4690391  234304   6662   191   37   400   27   9%   1024  -23   40   37  108%
c -  937.0    3365    58424   4778523  236995   6663   191   37   424   27   9%   1024    3   35   36   96%
c -  958.3    3365    58424   4866896  238416   6664   191   36   409   27   9%   1024  -15   35   36   97%
c -  979.7    3365    58424   4956723  241292   6664   191   36   411   28   9%   1024   -9   41   36  113%
c
c CAUGHT SIGNAL 15 SIGTERM
c
c s UNKNOWN
c bate: 19 basic ate = 16 trn 84% + 3 lrg 16% in 1 updates
c bcas: 4 count, 0 added (0 skipped), 326417 steps
c bkwd: tried 5335 clauses, 10606 lits, 1.99 lits/clause
c bkwd: checked 526054 occs, 98.60 occs/clause, 49.60 occs/lit
c bkwd: subsumed 0 binary, 2 ternary, 21 large
c bkwd: strengthened 0 binary, 3 ternary (100% self), 59 large (0% self)
c blkd: 4 bces, 199 removed, 3008552 resolutions, 6245221 steps
c blkd: 31 blocking literals 0%, 0 pure
c bump: 5001446 bumped seen, 417464109 lits 83.5 on average
c card: 4 count, 0 units, 0 am1, 7516084 steps
c card: 0 rescheduled, 0 eliminated, 0 resolved, 1344 subsumed
c card: 7 at-most-one constraints found, average size 3.00
c card: 7 at-most-one constraints used 100%, average size 3.00
c card: 35 at-most-two constraints found, average size 4.06
c card: 34 at-most-two constraints used 97%, average size 4.06
c cces: 7 cces, 8560 eliminated, 8558 ate 100%, 2 abce 0%
c cces: 0 probed, 0 lifted, 0 failed
c cces: 0 cached, 0 rsz, 0 cols 0%, 0 srch, 0 hits 0%
c clls: 1 sat, 0 simp, 0 freeze, 0 melt
c clls: 1006271 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 52 gcs, 0 rescored clauses, 2631 rescored vars
c dcps: 32 decompositions, 235 equivalent 5%
c deco: 1159 decision-only clauses 0%, 42% reduction
c decs: 39097530 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c dsch: 119605009 push, 119601496 pop (119601496 dec 100%)
c dsch: 1776881792 swaps, 0 down, 531187229 up
c elms: 5 elims, 127 eliminated 3%, 0 pure 0%
c elms: 8 rounds, 1.6 rounds/bve
c elms: 127 small 100%, 0 large 0%
c elms: 1393 tried small, 127 succeeded 9%, 1266 failed 91%
c elms: 2105 subsumed, 3022 strengthened, 0 blocked
c elms: 1136596 copies, 2784926 resolutions, 405945 ipos
c elms: 216305 subchks, 148074 strchks
c gaus: 4 extractions, 11040 extracted, 4.6 size, 7 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 2 gc, 17184330 steps, 8592165 extr 50%, 438017 elim 3%
c glue: 30.9 orig avg, 30.9 real avg, 4.6 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 90 = 28 simple 31% + 51 trn 57% + 11 lrg 12%, 22 sub 24%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 5001446 clauses, 61.5 length
c lrnd: 307433012 lits = 323690748 orig - 16257736 removed 5%
c lrnd: 2404206 uips 48%, 2013842 flips 40%
c mins: 4604775 mins 92%, 42 bin 0%, 387895 size 8%
c mins: 233947073 poisoned searches, 19438484 hits, 8% hit rate
c mins: 487048071 used twice searches, 100214873 hits, 21% hit rate
c move: moved 1367, 10 bin 1%, 1357 trn 99%
c otfs: 43806 driving 51%, 42512 restarting 49%
c otfs: str 86318, 84578 red 98%, 1740 irr 2%
c otfs: str 86318, 0 bin 0%, 95 trn 0%, 86223 lrg 100%
c otfs: sub 541, 538 red 99%, 3 irr 1%
c otfs: sub 541, 0 bin 0%, 21 trn 4%, 520 lrg 96%
c phas: 2 computed, 3406 set, 1460 pos (43%), 1946 neg (57%)
c prbs: 2 basic, 3402 probed, 0 failed, 0 lifted
c prbs: 3 simple, 14482 probed, 56 failed, 119 eqs
c prbs: 3 treelook, 5110 probed, 0 failed, 0 lifted
c prom: 618212 locked 21% out of 2950875 tried
c prps: 563178071 props, 14 props/dec
c prps: 100% srch, 0% simp, 0% lkhd
c quat: 11 count, 1888 quat, 2173 self1, 230 self2, 516 dup
c redc: 912 clauses 0%, 599428 tried 12%, 0 sat 0%
c redc: 933 lits 0%, 4956737 tried 2%, 0 sat 0%
c redc: 43 times jump level reduced, 14.0 levels on average
c reds: 71 count, 71012.4 conflicts per reduce
c reds: 0 memlim 0%, 71 arith 100%
c reds: 2980288 collected 64%, 1663518 retired 36%
c rmbd: 20 removed, 8 red 40%
c rsts: 35793 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: 13 count, 13 confs 100%, 0 vars 0%
c simp: 0 its 0%, 0 bin 0%, 0 trns 0%
c subl: 5001446 count (8022432 tried 1.6), 26607 sub out of 4999555 (0.5%)
c swps: 5 count, 12 rounds, 3197 queries (266.4/round)
c swps: 3199 sat calls, 8 unsat (1.1% success rate)
c swps: 114887 decisions 35.9, 3374 conflicts 1.1
c swps; 146.4 avg class size, 92.9 avg environment size
c swps: 0 failed, 6 impls, 6 equivs
c swp0: 1063 type 0 queries, 26 unsat (2.4%), 1063 sat (100.0%)
c swp1: 2134 type 1 queries, 103 unsat (4.8%), 2128 sat (99.7%)
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: 88203490 calls to obtain time
c tops: 561 fixed 13%, 0 its, 0.00 confs/it
c trds: 10 transitive reductions, 55 removed, 0 failed
c trds: 66993 nodes, 4360 edges, 6197 steps
c trim: 224226 words, 0.9 MB
c trnr: 10 count, 57 bin, 524 trn, 15559885 steps
c unhd: 6 count, 9 rounds, 5088534 steps
c unhd: 0 non-trivial sccs of average size 0.0
c unhd: 1 units, 1 bin, 0 trn, 0 lrg
c unhd: 4 failed, 4 stamp, 0 lits, 0 bin, 0 trn, 0 lrg
c unhd: 1074 tauts, 0 bin 0%, 764 trn 71%, 300 lrg 28%
c unhd: 1074 tauts, 10 stamp 1%, 608 red 57%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 23320 str, 1 bin 0%, 76 trn 0%, 23243 lrg 100%, 23174 red 99%
c vars: 3365 remaining 78% and 923 removed 22% out of 4288
c vars: 561 fixed 13%, 127 eliminated 3%, 235 equivalent 5%
c vsts: 33934777589 visits, 100% srch, 0% simp, 0% lkhd
c vsts: 60.3 search visits per propagation, 6728.9 per conflict
c wchs: 10909154762 pushed, 16096627 enlarged, 1171 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all        5001443       2980288       1663518     224883779      43203887       2519325
c 
c  0 0        215614   4       371   0         0   0 191262892  85< 33582600  78   1962972  78     6.8
c  1 5        255816   5    118274   4    115603   7  17119254   8   3359254   8<   218577   9<    0.7
c  2 6        841896  17    445130  15    368742  22   8504093   4   2229573   5    135526   5     1.1
c  3 9        847154  17    487363  16    338718  20   2876322   1   1143657   3     54851   2     1.1
c  4 14       664363  13    422049  14    227024  14<  1627126   1    804757   2     35825   1     1.3
c  5 21       533576  11<   353518  12<   167655  10   1068081   0    582758   1     25898   1     1.7
c  6 30       412724   8    280630   9    122199   7    701496   0    408399   1     19087   1     2.0
c  7 41       326667   7    228252   8     90602   5    496331   0    303467   1     15035   1     2.4
c  8 54       262815   5    188225   6     68158   4    371331   0    235915   1     12904   1     2.8
c  9 69       210607   4    153186   5     51793   3    285137   0    185835   0     11412   0     3.1
c 10 86       285729   6    207780   7     69614   4    379216   0    248926   1     16953   1     6.2
c 11 126      140230   3     93346   3     41807   3    186849   0    115152   0      9773   0     5.3
c 12 230        4249   0      2163   0      1601   0      5648   0      3593   0       512   0     0.3
c 13 534           3   0         1   0         2   0         3   0         1   0         0   0     0.0
c 
c avg                  4.6           5.1           4.3           0.3           0.7           0.6
c std                  2.8           2.7           2.6           1.1           1.7           1.7
c 
c   38.731   4% decide
c   24.328   2% bump
c    4.771   0% cce
c 
c    4.999 < 1% rest (below)
c 
c    2.040   0% elim
c    1.325   0% sweep
c    1.058   0% quatres
c    0.656   0% unhide
c    0.619   0% probe
c    0.518   0% block
c    0.324   0% gauss
c    0.197   0% rescore
c    0.123   0% card
c    0.089   0% ternres
c    0.075   0% bca
c    0.015   0% transred
c    0.000   0% locs
c    0.000   0% queuesort
c ==================================
c    0.403   0% preprocessing     3%
c   12.522   1% inprocessing     97%
c ==================================
c   12.925   1% simplifying
c  987.012  99% search
c ==================================
c  999.937 100% all
c 
c       5041878 conflicts,        5042.2 confs/sec
c          1626 ternaries,        3100.8 confs/ternary
c            57 binaries,        88454.0 confs/binary
c             0 iterations,          0.0 confs/iteration
c 
c            71 reductions,          0.1 redus/sec,  71012.4 confs/reduction
c         35793 restarts,           35.8 rests/sec,    140.9 confs/restart
c      39097530 decisions,       39100.0 decis/sec,      7.8 decis/conflict
c     563178071 propagations,   563213.3 props/sec,     14.4 props/decision
c 
c 999.9 seconds, 111.7 MB
c
c CAUGHT SIGNAL 15 SIGTERM
c
c launch: done
