c launch: /data/cnf/sc2014/app/010-22-144.cnf.bz2
c host: atom20
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/010-22-144.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/010-22-144.cnf.bz2
c no embedded options
c found 'p cnf 4128 126564' header
c read 4128 variables, 126564 clauses, 833818 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 3605 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    3605    72259         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 6 at-most-two constraints of average size 4.0
c [card-1] using previous limit 2000000 for elimination
c [card-1] 9 out of 9 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 800 variables
c [simpleprobe-1] all 3328 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 137 variables
c [simpleprobe-1] fully completed simple probing
c [simpleprobe-1] removed 137 variables, found 13 hbrs, 32 units
c [unhide-1] limit 100000 with penalty 0 = 0 + 0
c [unhide-1-1] 0 units, 0 failed, 686 tauts, 0 hbrs, 29 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 3191 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 80 variables 3% in round 1 in 2550873 steps
c [elim-1-1] backward subsumption/strengthening limit 2550800
c [elim-1-1-1] backward checking 1290 touched variables 40%
c [elim-1-1-1] fully completed backward checking in 1 rounds
c [elim-1-1] subsumed 19 and strengthened 65 clauses in 769981 steps
c [elim-1-1] rescheduled 131 variables 4% by backward subsumption
c [elim-1-2] eliminated 2 variables 0% in round 2 in 108325 steps
c [elim-1-2] backward subsumption/strengthening limit 108300
c [elim-1-2-1] backward checking 18 touched variables 1%
c [elim-1-2-1] fully completed backward checking in 1 rounds
c [elim-1-2] subsumed 1 and strengthened 1 clauses in 92628 steps
c [elim-1-2] rescheduled 6 variables 0% by backward subsumption
c [elim-1-3] no variable eliminated in round 3 in 3673 steps
c [elim-1] fully completed in 3 rounds
c [elim-1] transition to [ all 0 rem 0 ] state
c [elim-1] eliminated 83 = 3% variables out of 3191 scheduled
c [phase-count-1] 57962 negative 99.1% of 58508 except 546 0.9%
c [phase-count-1] 57735 positive 98.7% of 58508 except 773 1.3%
c [phase-1] phase bias: 1344 positive 43%, 1764 negative 57%
c [score-distribution-1] 0 pos 0.00%, 0 min 0.00%, 3108 zero 100.00%
c [score-distribution-1] 1 different 0.03% out of total 3108 variables
c [simplification-1] removed 420 variables 11.9% (3108 remain 86%)
c [simplification-1] removed 13751 irredundant clauses 19.0% (58508 remain 81%)
c [simplification-1] maximum reduction of 19% = max (12%, 19%)
c [simplification-1] large reduction 19% >= 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 [decomp-3] removed 1 variables
c [simpleprobe-2] all 3107 free variables schedulable
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [simpleprobe-2] 1093 variables remain 35% (2014 retained 65%)
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 6214 literals 100%
c [treelook-1] scheduling used 253476 steps
c [treelook-1] scheduled completely
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 300460 steps
c [treelook-1] 4910 literals remain 79%
c [treelook-1] 3092 variables remain to probed next time 100%
c [treelook-1] removed 0 variables, found 8 hbrs
c [basicprobe-1] limit 1000000 penalty 0 = 0 + 0
c [basicprobe-1-0] 358 sched 12%, 0 failed, 0 lifted, 5 hbrs
c [basicprobe-1-1] 362 sched 12%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-1-1] fully completed probing
c [basicprobe-1-1] removed 0 variables, found 5 hbrs
c [block-1] scheduling all variables this time
c [block-1] scheduled 3107 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 105 blocked clauses
c [block-1] 105 < 1/100 * 58505 = 585 considered unsuccessful
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 2875 clauses out of 17161 (17%) of length 7
c [cce-1-1] eliminated 447 clauses out of 17147 (3%) of length 6
c [cce-1-1] eliminated 2202 clauses out of 12768 (17%) of length 5
c [cce-1-1] eliminated 586 clauses out of 6423 (9%) of length 4
c [cce-1-1] completed large round (ATE)
c [cce-1-1] eliminated 6110 large clauses in 26742315 steps
c [cce-1-1] allowing another 13371157 steps for small clauses
c [cce-1-1] scheduling 810 clauses = 234 binary + 576 ternary
c [cce-1-1] tried to eliminate 810 small clauses 100%
c [cce-1-1] eliminated 6 binary clauses 3%
c [cce-1-1] eliminated 73 ternary clauses 13%
c [cce-1-1] eliminated 79 small clauses 10%
c [cce-1-1] eliminated 79 small clauses in 13521251 steps
c [cce-1-1] completed small round (ATE)
c [cce-1-1] completed small and large (ATE)
c [cce-1-1] eliminated 6189 covered clauses in round 1
c [cce-1-2] eliminated 38 clauses out of 14286 (0%) of length 7
c [cce-1-2] incomplete large round (ABCE)
c [cce-1-2] eliminated 38 large clauses in 16478788 steps
c [cce-1-2] allowing another 8239394 steps for small clauses
c [cce-1-2] scheduling 731 clauses = 228 binary + 503 ternary
c [cce-1-2] tried to eliminate 731 small clauses 100%
c [cce-1-2] completed small round (ABCE)
c [cce-1-2] eliminated 38 covered clauses in round 2
c [cce-1-3] incomplete large round (ABCE)
c [cce-1-3] allowing another 4047412 steps for small clauses
c [cce-1-3] scheduling 731 clauses = 228 binary + 503 ternary
c [cce-1-3] tried to eliminate 731 small clauses 100%
c [cce-1-3] completed small round (ABCE)
c [cce-1-3] eliminated 0 covered clauses in round 3
c [cce-1] eliminated 6227 covered clauses in TOTAL during 3 rounds
c [elim-2] scheduling all variables this time
c [elim-2] scheduled 3107 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 428 not tried 14% in round 1
c [elim-2] transition to [ all 1 rem 1 ] state
c [elim-2] eliminated 14 = 0% variables out of 3107 scheduled
c [elim-2] 14 < 1/100 * 3107 = 31 considered unsuccessful
c [bca-1] limit of 10000000 steps and 104272 added (scaled 2)
c [bca-1] 4405 out of 6188 literals actually usable 71%
c [bca-1] added 0 blocked clauses in 28317 steps
c [sweep-1] limit 1000000 penalty 0 = 0 + 0
c [sweep-1-1] 1380 pos 44.6% + 1713 neg 55.4% = 3093 sched 100.0% ret 0
c [sweep-1-1] 431036 steps 513 queries 166.51 avg class size
c [sweep-1-1] 7850 decisions 517 SAT calls 21.64 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, 3 impls)
c [sweep-1-2] 1527 pos 49.4% + 1563 neg 50.6% = 3090 sched 100.0% ret 0
c [sweep-1-2] 413072 steps 532 queries 159.88 avg class size
c [sweep-1-2] 7855 decisions 532 SAT calls 20.90 avg env size
c [sweep-1-2] fully completed sweeping round
c [decomp-8] removed 5 variables
c [sweep-1-2] removed 5 vars (0 failed, 2 eqs, 5 impls)
c [sweep-1-3] 1528 pos 49.5% + 1557 neg 50.5% = 3085 sched 100.0% ret 0
c [sweep-1-3] 156457 steps 167 queries 466.99 avg class size
c [sweep-1-3] 2629 decisions 166 SAT calls 22.90 avg env size
c [sweep-1-3] 2023 variables remain 66% (1062 retained 34%)
c [decomp-9] removed 2 variables
c [sweep-1-3] removed 2 vars (0 failed, 0 eqs, 0 impls)
c [sweep-1] removed 10 vars in TOTAL (3 rounds, 1209 queries)
c [score-distribution-2] 2802 pos 90.89%, 0 min 0.00%, 281 zero 9.11%
c [score-distribution-2] 1233 different 39.99% out of total 3083 variables
c [simplification-2] removed 25 variables 0.8% (3083 remain 86%)
c [simplification-2] removed 6647 irredundant clauses 11.4% (51861 remain 72%)
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 6520 quaternary clauses 13% in total
c [quatres-1-1] added 24 double-self-subsuming ternary resolvents
c [quatres-1-2] added 113 single-self-subsuming ternary resolvents
c [quatres-1-2] added 331 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 3083 free variables schedulable
c [ternres-1] 302 ternary resolvents (30 bin, 272 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 6 at-most-two constraints of average size 4.5
c [card-2] using previous limit 1000000 for elimination
c [card-2] 6 out of 6 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 3310 xors of average arity 5.0
c [gauss-1] connected 16396 occurrences of 764 variables (average 21.5)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] fully completed
c [gauss-1] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-10] removed 2 variables
c [unhide-2] limit 50000 with penalty 1 = 1 + 0
c [unhide-2-2] 0 units, 0 failed, 130 tauts, 0 hbrs, 161 literals
c [transred-1] limit 100000 with penalty 0 = 0 + 0
c [transred-1] removed 12 transitive binary clauses
c [cce-2] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-2-1] eliminated 6 clauses out of 13345 (0%) of length 7
c [cce-2-1] eliminated 186 clauses out of 17055 (1%) of length 6
c [cce-2-1] eliminated 29 clauses out of 10725 (0%) of length 5
c [cce-2-1] eliminated 61 clauses out of 5848 (1%) of length 4
c [cce-2-1] completed large round (ATE)
c [cce-2-1] eliminated 282 large clauses in 23814378 steps
c [cce-2-1] allowing another 11907189 steps for small clauses
c [cce-2-1] scheduling 797 clauses = 266 binary + 531 ternary
c [cce-2-1] tried to eliminate 797 small clauses 100%
c [cce-2-1] eliminated 4 binary clauses 2%
c [cce-2-1] eliminated 18 ternary clauses 3%
c [cce-2-1] eliminated 22 small clauses 3%
c [cce-2-1] eliminated 22 small clauses in 12056140 steps
c [cce-2-1] completed small round (ATE)
c [cce-2-1] eliminated 304 covered clauses in round 1
c [cce-2-2] incomplete large round (ATE)
c [cce-2-2] allowing another 8971943 steps for small clauses
c [cce-2-2] scheduling 775 clauses = 262 binary + 513 ternary
c [cce-2-2] tried to eliminate 775 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 304 covered clauses in TOTAL during 2 rounds
c [cce-2] 304 < 1/100 * 51848 = 518 considered unsuccessful
c [sweep-2] limit 1000000 penalty 0 = 0 + 0
c [sweep-2-1] 996 pos 49.3% + 1024 neg 50.7% = 2020 sched 65.6% ret 1061
c [sweep-2-1] 359164 steps 466 queries 118.37 avg class size
c [sweep-2-1] 7180 decisions 467 SAT calls 21.85 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, 0 eqs, 2 impls)
c [sweep-2-2] 1513 pos 49.1% + 1567 neg 50.9% = 3080 sched 100.0% ret 0
c [sweep-2-2] 433144 steps 508 queries 154.11 avg class size
c [sweep-2-2] 8080 decisions 510 SAT calls 22.51 avg env size
c [sweep-2-2] fully completed sweeping round
c [sweep-2-2] removed 0 vars (0 failed, 0 eqs, 2 impls)
c [sweep-2-3] 1513 pos 49.1% + 1567 neg 50.9% = 3080 sched 100.0% ret 0
c [sweep-2-3] 207726 steps 210 queries 357.49 avg class size
c [sweep-2-3] 3585 decisions 209 SAT calls 24.75 avg env size
c [sweep-2-3] 1584 variables remain 51% (1496 retained 49%)
c [sweep-2-3] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-2] 1 < 1/1000 * 3081 = 3 considered unsuccessful
c [sweep-2] removed 1 vars in TOTAL (3 rounds, 1181 queries)
c [score-distribution-3] 2883 pos 93.60%, 117 min 3.80%, 80 zero 2.60%
c [score-distribution-3] 1256 different 40.78% out of total 3080 variables
c [simplification-3] removed 3 variables 0.1% (3080 remain 85%)
c [simplification-3] removed 335 irredundant clauses 0.6% (51524 remain 71%)
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 7648 quaternary clauses 15% in total
c [quatres-2-1] added 34 double-self-subsuming ternary resolvents
c [quatres-2-2] added 254 single-self-subsuming ternary resolvents
c [quatres-2-2] added 420 quaternary resolvents
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] all 3080 free variables schedulable
c [ternres-2] 212 ternary resolvents (20 bin, 192 trn)
c [ternres-2] fully completed ternary resolution
c [treelook-2] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-2] scheduled 3449 literals 56%
c [treelook-2] scheduling used 150051 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-2] used 150003 steps
c [treelook-2] 2788 literals remain 45%
c [treelook-2] 1681 variables remain to probed next time 55%
c [treelook-2] removed 0 variables, found 26 hbrs
c [transred-2] limit 233083 with penalty 0 = 0 + 0
c [transred-2] removed 7 transitive binary clauses
c [block-2] scheduling all variables this time
c [block-2] scheduled 3080 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 3 blocked clauses
c [block-2] 3 < 1/100 * 51523 = 515 considered unsuccessful
c [elim-3] 428 variables 14% will be scheduled this time
c [elim-3] scheduled 428 variables 14%
c [elim-3] limit of 10000000 steps penalty 1 = 1 + 0
c [elim-3] rescheduling of touched variables disabled
c [elim-3] incomplete 149 not tried 5% in round 1
c [elim-3] transition to [ all 0 rem 1 ] state
c [elim-3] eliminated 0 = 0% variables out of 428 scheduled
c [bca-2] limit of 10000000 steps and 103494 added (scaled 2)
c [bca-2] 415 out of 6162 literals actually usable 7%
c [bca-2] added 0 blocked clauses in 16051 steps
c [score-distribution-4] 1778 pos 57.73%, 1233 min 40.03%, 69 zero 2.24%
c [score-distribution-4] 1021 different 33.15% out of total 3080 variables
c [simplification-4] removed 0 variables 0.0% (3080 remain 85%)
c [simplification-4] removed 26 irredundant clauses 0.1% (51497 remain 71%)
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  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i    8.3    3079    51497     40483   37853   2054   222   10   267   12   4%    463  162   10    4  267%
c 
c [simplification-5] limit 43000 conflicts (hard 58000) hit after 51064 conflicts
c [quatres-3] found 10406 quaternary clauses 17% in total
c [quatres-3-1] removed 1 duplicate quaternary clauses
c [quatres-3-1] added 56 double-self-subsuming ternary resolvents
c [quatres-3-2] added 444 single-self-subsuming ternary resolvents
c [quatres-3-2] added 433 quaternary resolvents
c [ternres-3] limit 4000000 with penalty 0 = 0 + 0
c [ternres-3] all 3079 free variables schedulable
c [ternres-3] 177 ternary resolvents (15 bin, 162 trn)
c [ternres-3] fully completed ternary resolution
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] extracted 745 xors of average arity 4.6
c [gauss-2] connected 3443 occurrences of 217 variables (average 15.9)
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 [decomp-16] removed 1 variables
c [transred-3] limit 1510542 with penalty 0 = 0 + 0
c [transred-3] removed 10 transitive binary clauses
c [transred-3] found 1 units
c [cce-3] limit of 15000000 steps penalty 1 = 1 + 0
c [cce-3-1] eliminated 4 clauses out of 12927 (0%) of length 7
c [cce-3-1] eliminated 3 clauses out of 17092 (0%) of length 6
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 7 large clauses in 15000011 steps
c [cce-3-1] allowing another 7500005 steps for small clauses
c [cce-3-1] scheduling 870 clauses = 311 binary + 559 ternary
c [cce-3-1] tried to eliminate 870 small clauses 100%
c [cce-3-1] eliminated 25 ternary clauses 4%
c [cce-3-1] eliminated 25 small clauses 3%
c [cce-3-1] eliminated 32 small clauses in 7696882 steps
c [cce-3-1] completed small round (ACCE)
c [cce-3-1] eliminated 39 covered clauses in round 1
c [cce-3-2] incomplete large round (ACCE)
c [cce-3-2] allowing another 3651565 steps for small clauses
c [cce-3-2] scheduling 845 clauses = 311 binary + 534 ternary
c [cce-3-2] tried to eliminate 845 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 39 covered clauses in TOTAL during 2 rounds
c [cce-3] 39 < 1/100 * 51486 = 514 considered unsuccessful
c [sweep-3] limit 500000 penalty 1 = 1 + 0
c [sweep-3-1] 760 pos 48.0% + 824 neg 52.0% = 1584 sched 51.5% ret 1493
c [sweep-3-1] 500889 steps 103 queries 145.49 avg class size
c [sweep-3-1] 6956 decisions 101 SAT calls 127.93 avg env size
c [sweep-3-1] 500 variables remain 16% (2577 retained 84%)
c [decomp-17] removed 1 variables
c [sweep-3-1] removed 1 vars (0 failed, 1 eqs, 1 impls)
c [sweep-3] 1 < 1/1000 * 3077 = 3 considered unsuccessful
c [sweep-3] removed 1 vars in TOTAL (1 rounds, 102 queries)
c [score-distribution-5] 2851 pos 92.69%, 214 min 6.96%, 11 zero 0.36%
c [score-distribution-5] 1506 different 48.96% out of total 3076 variables
c [simplification-5] removed 3 variables 0.1% (3076 remain 85%)
c [simplification-5] removed 53 irredundant clauses 0.1% (51444 remain 71%)
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 141064 (soft 111064 + delta 30000)
c [simplification-5] new conflict limit 111064 (hard 141064)
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.0    3076    51444     75843   27950   3120   250   13   271   14   5%    322   98   15    7  226%
c 
c [simplification-6] limit 111064 conflicts (hard 141064) hit after 111064 conflicts
c [quatres-4] found 13158 quaternary clauses 18% in total
c [quatres-4-1] removed 1 duplicate quaternary clauses
c [quatres-4-1] added 31 double-self-subsuming ternary resolvents
c [quatres-4-2] added 441 single-self-subsuming ternary resolvents
c [quatres-4-2] added 362 quaternary resolvents
c [ternres-4] limit 4523720 with penalty 0 = 0 + 0
c [ternres-4] all 3076 free variables schedulable
c [ternres-4] 90 ternary resolvents (9 bin, 81 trn)
c [ternres-4] fully completed ternary resolution
c [card-3] limit 565465 penalty 2 = 2 + 0
c [card-3] found 5 at-most-one constraints of average size 3.0
c [card-3] found 31 at-most-two constraints of average size 4.0
c [card-3] using previous limit 565465 for elimination
c [card-3] 35 out of 36 constraints (97%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [basicprobe-2] limit 11309301 penalty 1 = 1 + 0
c [basicprobe-2-0] 625 sched 20%, 0 failed, 0 lifted, 22 hbrs
c [basicprobe-2-1] 631 sched 21%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-2-1] fully completed probing
c [basicprobe-2-1] removed 0 variables, found 22 hbrs
c [bate-1] eliminated 67 asymmetric tautologies during probing
c [unhide-3] limit 226186 with penalty 2 = 2 + 0
c [unhide-3-3] 0 units, 0 failed, 99 tauts, 0 hbrs, 2065 literals
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 23 transitive binary clauses
c [score-distribution-6] 2881 pos 93.66%, 184 min 5.98%, 11 zero 0.36%
c [score-distribution-6] 1805 different 58.68% out of total 3076 variables
c [simplification-6] removed 0 variables 0.0% (3076 remain 85%)
c [simplification-6] removed 70 irredundant clauses 0.1% (51374 remain 71%)
c [simplification-6] maximum reduction of 0% = max (0%, 0%)
c [simplification-6] full geometric conflict interval increment 60000
c [simplification-6] new conflict interval 120000
c [simplification-6] penalized conflict interval 120000 = 1 * 120000
c [simplification-6] hard conflict limit 291064 (soft 231064 + delta 60000)
c [simplification-6] new conflict limit 231064 (hard 291064)
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 -   27.9    3076    51374    131734   35496   4129   291   13   298   15   4%    725   62   14   10  132%
c -   39.7    3076    51374    187452   45236   4380   300   16   282   16   6%    896   18   16   13  128%
c 
c [simplification-7] limit 231064 conflicts (hard 291064) hit after 231064 conflicts
c [quatres-5] found 17165 quaternary clauses 20% in total
c [quatres-5-1] removed 7 duplicate quaternary clauses
c [quatres-5-1] added 38 double-self-subsuming ternary resolvents
c [quatres-5-2] added 383 single-self-subsuming ternary resolvents
c [quatres-5-2] added 328 quaternary resolvents
c [ternres-5] limit 10659992 with penalty 0 = 0 + 0
c [ternres-5] all 3076 free variables schedulable
c [ternres-5] 77 ternary resolvents (11 bin, 66 trn)
c [ternres-5] fully completed ternary resolution
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 8 transitive binary clauses
c [block-3] scheduling all variables this time
c [block-3] scheduled 3076 variables 100%
c [block-3] limit of 26649980 steps penalty 2 = 2 + 0
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 1 blocked clauses
c [block-3] 1 < 1/100 * 51374 = 513 considered unsuccessful
c [elim-4] scheduling all variables this time
c [elim-4] scheduled 3076 variables 100%
c [elim-4] boosting limit by 20
c [elim-4] limit of 1065999210 steps penalty 2 = 2 + 0
c [elim-4] rescheduling of touched variables disabled
c [elim-4-1] eliminated 3 variables 0% in round 1 in 36681644 steps
c [elim-4-1] backward subsumption/strengthening limit 36681600
c [elim-4-1-1] backward checking 845 touched variables 27%
c [elim-4-1-1] fully completed backward checking in 1 rounds
c [elim-4-1] subsumed 0 and strengthened 0 clauses in 538319 steps
c [elim-4] fully completed in 1 rounds
c [elim-4] transition to [ all 0 rem 0 ] state
c [elim-4] eliminated 3 = 0% variables out of 3076 scheduled
c [elim-4] 3 < 1/100 * 3076 = 30 considered unsuccessful
c [bca-3] limit of 10000000 steps and 102944 added (scaled 2)
c [bca-3] 3 out of 6148 literals actually usable 0%
c [bca-3] not enough literals usable
c [bca-3] added 0 blocked clauses in 86688 steps
c [score-distribution-7] 3068 pos 99.84%, 5 min 0.16%, 0 zero 0.00%
c [score-distribution-7] 2143 different 69.74% out of total 3073 variables
c [simplification-7] removed 3 variables 0.1% (3073 remain 85%)
c [simplification-7] removed 152 irredundant clauses 0.3% (51222 remain 71%)
c [simplification-7] maximum reduction of 0% = max (0%, 0%)
c [simplification-7] full geometric conflict interval increment 120000
c [simplification-7] new conflict interval 240000
c [simplification-7] penalized conflict interval 240000 = 1 * 240000
c [simplification-7] hard conflict limit 591064 (soft 471064 + delta 120000)
c [simplification-7] new conflict limit 471064 (hard 591064)
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 -   50.3    3073    51222    240365   46029   5006   300   16   298   10   5%    967   17   14   14   98%
c -   60.0    3073    51222    299425   55374   5125   301   18   302   10   6%   1001    7   18   16  116%
c -   69.3    3073    51222    354967   61169   5213   303   19   303   11   6%   1014   -4   20   17  118%
c -   78.3    3073    51222    410016   65849   5295   305   20   329   19   6%   1020   14   21   19  113%
c -   87.5    3073    51222    465144   69839   5364   305   22   321   20   7%   1022   -0   23   20  116%
c 
c [simplification-8] limit 471064 conflicts (hard 591064) hit after 471064 conflicts
c [quatres-6] found 21334 quaternary clauses 20% in total
c [quatres-6-1] removed 38 duplicate quaternary clauses
c [quatres-6-1] added 21 double-self-subsuming ternary resolvents
c [quatres-6-2] added 271 single-self-subsuming ternary resolvents
c [quatres-6-2] added 222 quaternary resolvents
c [ternres-6] limit 21283306 with penalty 0 = 0 + 0
c [ternres-6] all 3073 free variables schedulable
c [ternres-6] 39 ternary resolvents (6 bin, 33 trn)
c [ternres-6] fully completed ternary resolution
c [gauss-3] limit 1064165 penalty 2 = 2 + 0
c [gauss-3] extracted 178 xors of average arity 3.0
c [gauss-3] connected 534 occurrences of 41 variables (average 13.0)
c [gauss-3] limit 1064165 penalty 2 = 2 + 0
c [gauss-3] fully completed
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [simpleprobe-3] 1080 schedulable variables 35%
c [simpleprobe-3] limit 42566613 penalty 1 = 1 + 0
c [simpleprobe-3] fully completed simple probing
c [simpleprobe-3] removed 0 variables, found 18 hbrs, 0 units
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 16 transitive binary clauses
c [cce-4] boosting limit by 10
c [cce-4] limit of 266041330 steps penalty 2 = 2 + 0
c [cce-4-1] eliminated 16 clauses out of 17448 (0%) of length 6
c [cce-4-1] eliminated 54 clauses out of 10762 (1%) of length 5
c [cce-4-1] eliminated 71 clauses out of 5563 (1%) of length 4
c [cce-4-1] completed large round (ATE)
c [cce-4-1] eliminated 141 large clauses in 23328583 steps
c [cce-4-1] allowing another 11664291 steps for small clauses
c [cce-4-1] scheduling 881 clauses = 320 binary + 561 ternary
c [cce-4-1] tried to eliminate 881 small clauses 100%
c [cce-4-1] eliminated 9 ternary clauses 2%
c [cce-4-1] eliminated 9 small clauses 1%
c [cce-4-1] eliminated 9 small clauses in 11839988 steps
c [cce-4-1] completed small round (ATE)
c [cce-4-1] eliminated 150 covered clauses in round 1
c [cce-4-2] completed large round (ATE)
c [cce-4-2] allowing another 11635540 steps for small clauses
c [cce-4-2] scheduling 872 clauses = 320 binary + 552 ternary
c [cce-4-2] tried to eliminate 872 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 150 covered clauses in TOTAL during 2 rounds
c [cce-4] 150 < 1/100 * 51222 = 512 considered unsuccessful
c [sweep-4] limit 1596247 penalty 2 = 2 + 0
c [sweep-4-1] 266 pos 53.3% + 233 neg 46.7% = 499 sched 16.2% ret 2574
c [sweep-4-1] 449049 steps 122 queries 22.66 avg class size
c [sweep-4-1] 7110 decisions 121 SAT calls 102.87 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] 1447 pos 47.1% + 1626 neg 52.9% = 3073 sched 100.0% ret 0
c [sweep-4-2] 1105710 steps 250 queries 71.51 avg class size
c [sweep-4-2] 15709 decisions 249 SAT calls 119.74 avg env size
c [sweep-4-2] fully completed sweeping round
c [sweep-4-2] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-4-3] 1447 pos 47.1% + 1626 neg 52.9% = 3073 sched 100.0% ret 0
c [sweep-4-3] 48482 steps 11 queries 959.18 avg class size
c [sweep-4-3] 704 decisions 10 SAT calls 136.80 avg env size
c [sweep-4-3] 3010 variables remain 98% (63 retained 2%)
c [sweep-4-3] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-4] removed 0 vars in TOTAL (3 rounds, 380 queries)
c [score-distribution-8] 3071 pos 99.93%, 2 min 0.07%, 0 zero 0.00%
c [score-distribution-8] 1984 different 64.56% out of total 3073 variables
c [simplification-8] removed 0 variables 0.0% (3073 remain 85%)
c [simplification-8] removed 150 irredundant clauses 0.3% (51072 remain 71%)
c [simplification-8] maximum reduction of 0% = max (0%, 0%)
c [simplification-8] full geometric conflict interval increment 240000
c [simplification-8] new conflict interval 480000
c [simplification-8] penalized conflict interval 480000 = 1 * 480000
c [simplification-8] hard conflict limit 1191064 (soft 951064 + delta 240000)
c [simplification-8] new conflict limit 951064 (hard 1191064)
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 -   97.6    3073    51072    520936   73254   5715   315   24   344   20   7%   1023   17   25   22  118%
c -  106.4    3073    51072    577622   77915   5738   316   24   344   21   7%   1024    3   24   23  104%
c -  115.2    3073    51072    633891   82556   5760   316   26   333   13   8%   1024  -10   23   24   96%
c -  123.9    3073    51072    689228   86855   5777   317   27   361   13   7%   1024   11   28   25  111%
c -  132.6    3073    51072    743999   90674   5791   317   28   354   22   8%   1024    2   24   26   90%
c -  140.9    3073    51072    798441   94037   5809   317   27   343   14   8%   1024  -13   27   27   99%
c -  149.7    3073    51072    852857   97016   5833   317   29   356   14   8%   1024   -1   33   28  120%
c -  158.5    3073    51072    907599  100541   5845   317   28   354   14   8%   1024   -5   34   29  118%
c 
c [simplification-9] limit 951064 conflicts (hard 1191064) hit after 951391 conflicts
c [quatres-7] found 24094 quaternary clauses 18% in total
c [quatres-7-1] removed 63 duplicate quaternary clauses
c [quatres-7-1] added 2 double-self-subsuming ternary resolvents
c [quatres-7-2] added 125 single-self-subsuming ternary resolvents
c [quatres-7-2] added 171 quaternary resolvents
c [ternres-7] limit 44789953 with penalty 0 = 0 + 0
c [ternres-7] all 3073 free variables schedulable
c [ternres-7] 28 ternary resolvents (4 bin, 24 trn)
c [ternres-7] fully completed ternary resolution
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 4 transitive binary clauses
c [score-distribution-9] 3057 pos 99.48%, 16 min 0.52%, 0 zero 0.00%
c [score-distribution-9] 2176 different 70.81% out of total 3073 variables
c [simplification-9] removed 0 variables 0.0% (3073 remain 85%)
c [simplification-9] removed 0 irredundant clauses 0.0% (51072 remain 71%)
c [simplification-9] maximum reduction of 0% = max (0%, 0%)
c [simplification-9] full geometric conflict interval increment 480000
c [simplification-9] new conflict interval 960000
c [simplification-9] penalized conflict interval 960000 = 1 * 960000
c [simplification-9] hard conflict limit 2391391 (soft 1911391 + delta 480000)
c [simplification-9] new conflict limit 1911391 (hard 2391391)
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 -  167.3    3073    51072    961860  103728   6000   317   30   366   14   8%   1024    5   33   29  114%
c -  176.0    3073    51072   1016173  106437   6010   317   31   370   24   8%   1024    4   35   30  116%
c -  184.9    3073    51072   1070792  109138   6016   317   32   372   15   9%   1024    5   36   31  117%
c -  193.6    3073    51072   1125703  112226   6020   317   32   356   15   9%   1024  -13   33   31  106%
c -  202.4    3073    51072   1180462  115194   6027   317   33   388   25   8%   1024   16   33   32  102%
c -  211.2    3073    51072   1235253  117435   6033   317   32   384   16   8%   1024   12   37   32  116%
c -  220.1    3073    51072   1290667  119681   6043   317   33   378   26   9%   1024    4   39   32  120%
c -  229.2    3073    51072   1346619  122064   6046   317   35   376   26   9%   1024   -1   34   33  104%
c -  238.5    3073    51072   1403024  124151   6052   317   33   364   27   9%   1024  -11   30   33   91%
c -  248.2    3073    51072   1459926  126939   6058   317   35   378   16   9%   1024    6   35   34  104%
c -  257.9    3073    51072   1516850  128299   6064   317   33   383   27   9%   1024   10   30   34   89%
c -  267.7    3073    51072   1575058  130524   6068   317   34   368   17   9%   1024   -8   38   34  111%
c -  277.7    3073    51072   1633812  133310   6073   317   35   385   17   9%   1024    8   36   35  105%
c -  287.6    3073    51072   1692591  135696   6076   317   35   365   28   9%   1024  -12   36   35  103%
c -  297.9    3073    51072   1751606  137896   6079   317   35   388   28   9%   1024   10   34   35   96%
c -  308.1    3073    51072   1811100  139284   6085   317   35   377   29   9%   1024    0   32   35   91%
c -  318.6    3073    51072   1871764  141271   6088   317   35   394   18   9%   1024   14   41   35  116%
c 
c [simplification-10] limit 1911391 conflicts (hard 2391391) hit after 1913756 conflicts
c [quatres-8] found 26269 quaternary clauses 16% in total
c [quatres-8-1] removed 131 duplicate quaternary clauses
c [quatres-8-1] added 1 double-self-subsuming ternary resolvents
c [quatres-8-2] added 44 single-self-subsuming ternary resolvents
c [quatres-8-2] added 90 quaternary resolvents
c [ternres-8] limit 102140287 with penalty 0 = 0 + 0
c [ternres-8] all 3073 free variables schedulable
c [ternres-8] 20 ternary resolvents (4 bin, 16 trn)
c [ternres-8] fully completed ternary resolution
c [card-4] limit 6383767 penalty 3 = 3 + 0
c [card-4] found 3 at-most-one constraints of average size 3.0
c [card-4] found 35 at-most-two constraints of average size 4.0
c [card-4] using previous limit 6383767 for elimination
c [card-4] 38 out of 38 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [unhide-4] limit 2500000 with penalty 3 = 3 + 0
c [unhide-4-6] 0 units, 0 failed, 418 tauts, 0 hbrs, 25788 literals
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 4 transitive binary clauses
c [score-distribution-10] 3059 pos 99.54%, 14 min 0.46%, 0 zero 0.00%
c [score-distribution-10] 2312 different 75.24% out of total 3073 variables
c [simplification-10] removed 0 variables 0.0% (3073 remain 85%)
c [simplification-10] removed 2 irredundant clauses 0.0% (51070 remain 71%)
c [simplification-10] maximum reduction of 0% = max (0%, 0%)
c [simplification-10] full geometric conflict interval increment 960000
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 3413756 (soft 2913756 + delta 500000)
c [simplification-10] new conflict limit 2913756 (hard 3413756)
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 -  330.5    3073    51070   1933295  143411   5816   314   38   355   18  11%   1024  -20   42   36  118%
c -  341.0    3073    51070   1995107  146307   5818   314   36   382   18   9%   1024    4   32   36   89%
c -  351.8    3073    51070   2056432  148043   5820   314   37   377   18  10%   1024   -3   43   37  115%
c -  362.5    3073    51070   2118634  150243   5821   314   37   373   19  10%   1024   -5   43   37  117%
c -  373.4    3073    51070   2181165  152495   5823   314   38   381   19  10%   1024    2   41   37  108%
c -  384.7    3073    51070   2243959  154452   5825   314   39   392   19  10%   1024   12   39   38  102%
c -  395.8    3073    51070   2307263  156770   5825   314   38   388   19  10%   1024    6   33   39   85%
c -  407.0    3073    51070   2370521  158297   5826   314   37   393   19  10%   1024    8   31   38   82%
c -  418.6    3073    51070   2434763  159927   5829   314   40   381   20  10%   1024   -1   45   39  117%
c -  430.3    3073    51070   2499869  161949   5829   314   38   390   32  10%   1024    8   37   39   97%
c -  442.3    3073    51070   2565392  163409   5833   314   38   371   20  10%   1024  -12   35   38   91%
c -  454.6    3073    51070   2631975  165456   5835   314   40   370   20  11%   1024   -9   40   39  102%
c -  466.9    3073    51070   2698973  167505   5836   314   41   374   20  11%   1024   -5   42   39  109%
c -  479.3    3073    51070   2766446  169568   5841   314   39   389   21  10%   1024   11   44   39  112%
c -  491.8    3073    51070   2834215  171449   5843   314   40   376   21  11%   1024   -5   50   39  128%
c -  504.8    3073    51070   2902641  173451   5845   314   40   378   21  11%   1024   -6   42   39  107%
c 
c [simplification-11] limit 2913756 conflicts (hard 3413756) hit after 2915975 conflicts
c [quatres-9] found 27378 quaternary clauses 15% in total
c [quatres-9-1] removed 122 duplicate quaternary clauses
c [quatres-9-1] added 4 double-self-subsuming ternary resolvents
c [quatres-9-2] added 43 single-self-subsuming ternary resolvents
c [quatres-9-2] added 86 quaternary resolvents
c [ternres-9] limit 172497271 with penalty 0 = 0 + 0
c [ternres-9] all 3073 free variables schedulable
c [ternres-9] 41 ternary resolvents (0 bin, 41 trn)
c [ternres-9] fully completed ternary resolution
c [treelook-3] limit 4312431 penalty 2 = 2 + 0 boost 1
c [treelook-3] scheduled 3479 literals 57%
c [treelook-3] scheduling used 727260 steps
c [treelook-3] scheduled completely
c [treelook-3] limit 4312431 penalty 2 = 2 + 0 boost 1
c [treelook-3] used 760790 steps
c [treelook-3] fully completed tree based probing
c [treelook-3] removed 0 variables, found 8 hbrs
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 3073 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 3073 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] eliminated 2 variables 0% in round 1 in 36368055 steps
c [elim-5-1] backward subsumption/strengthening limit 36368000
c [elim-5-1-1] backward checking 207 touched variables 7%
c [elim-5-1-1] fully completed backward checking in 1 rounds
c [elim-5-1] subsumed 1 and strengthened 0 clauses in 179475 steps
c [elim-5-1] rescheduled 3 variables 0% by backward subsumption
c [elim-5-2] no variable eliminated in round 2 in 29490 steps
c [elim-5] fully completed in 2 rounds
c [elim-5] transition to [ all 0 rem 0 ] state
c [elim-5] eliminated 2 = 0% variables out of 3073 scheduled
c [elim-5] 2 < 1/100 * 3073 = 30 considered unsuccessful
c [bca-4] limit of 10000000 steps and 102618 added (scaled 2)
c [bca-4] 1 out of 6144 literals actually usable 0%
c [bca-4] not enough literals usable
c [bca-4] added 0 blocked clauses in 186558 steps
c [score-distribution-11] 2916 pos 94.95%, 155 min 5.05%, 0 zero 0.00%
c [score-distribution-11] 2315 different 75.38% out of total 3071 variables
c [simplification-11] removed 2 variables 0.1% (3071 remain 85%)
c [simplification-11] removed 11 irredundant clauses 0.0% (51059 remain 71%)
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 4415975 (soft 3915975 + delta 500000)
c [simplification-11] new conflict limit 3915975 (hard 4415975)
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 -  518.7    3071    51059   2971363  175424   5900   321   41   396   34  10%   1024   11   48   40  121%
c -  531.5    3071    51059   3040382  177703   5902   321   41   379   21  11%   1024   -4   37   40   92%
c -  544.4    3071    51059   3109339  179964   5903   321   41   405   21  10%   1024   18   38   41   93%
c -  557.3    3071    51059   3178394  181055   5904   321   41   390   22  10%   1024    5   44   41  108%
c -  570.7    3071    51059   3248692  181871   5904   321   40   375   22  11%   1024   -5   40   40  100%
c -  584.7    3071    51059   3320573  183554   5905   321   40   383   22  10%   1024   -0   41   40  101%
c -  598.6    3071    51059   3393273  185454   5905   321   40   380   22  11%   1024   -3   36   40   90%
c -  613.1    3071    51059   3466438  187445   5908   321   41   378   22  11%   1024   -3   43   40  108%
c -  627.5    3071    51059   3540093  188843   5908   321   39   396   22  10%   1024   13   42   40  104%
c -  642.2    3071    51059   3614706  190813   5911   321   42   378   23  11%   1024   -4   48   41  117%
c -  657.6    3071    51059   3689924  192018   5914   321   40   390   23  10%   1024    8   45   40  112%
c -  672.6    3071    51059   3766346  195468   5916   321   41   375   23  11%   1024   -5   35   41   87%
c -  688.1    3071    51059   3841842  195849   5917   321   41   373   23  11%   1024   -8   30   41   74%
c 
c [simplification-12] limit 3915975 conflicts (hard 4415975) hit after 3918014 conflicts
c [quatres-10] found 27981 quaternary clauses 14% in total
c [quatres-10-1] removed 86 duplicate quaternary clauses
c [quatres-10-1] added 1 double-self-subsuming ternary resolvents
c [quatres-10-2] added 12 single-self-subsuming ternary resolvents
c [quatres-10-2] added 52 quaternary resolvents
c [ternres-10] limit 200000000 with penalty 0 = 0 + 0
c [ternres-10] all 3071 free variables schedulable
c [ternres-10] 1 ternary resolvents (0 bin, 1 trn)
c [ternres-10] fully completed ternary resolution
c [gauss-4] limit 6250000 penalty 3 = 3 + 0
c [gauss-4] extracted 4224 xors of average arity 5.3
c [gauss-4] connected 22400 occurrences of 843 variables (average 26.6)
c [gauss-4] limit 6250000 penalty 3 = 3 + 0
c [gauss-4] connected 2474 occurrences of 843 variables (average 2.9)
c [gauss-4] fully completed
c [gauss-4] exported 0 unary, 0 binary and 0 ternary equations
c [cce-5] limit of 157164946 steps penalty 3 = 3 + 0
c [cce-5-1] eliminated 9 clauses out of 10745 (0%) of length 5
c [cce-5-1] eliminated 8 clauses out of 5495 (0%) of length 4
c [cce-5-1] completed large round (ACCE)
c [cce-5-1] eliminated 17 large clauses in 25679053 steps
c [cce-5-1] allowing another 12839526 steps for small clauses
c [cce-5-1] scheduling 875 clauses = 326 binary + 549 ternary
c [cce-5-1] tried to eliminate 875 small clauses 100%
c [cce-5-1] eliminated 1 binary clauses 0%
c [cce-5-1] eliminated 6 ternary clauses 1%
c [cce-5-1] eliminated 7 small clauses 1%
c [cce-5-1] eliminated 7 small clauses in 13028969 steps
c [cce-5-1] completed small round (ACCE)
c [cce-5-1] completed small and large (ACCE)
c [cce-5-1] eliminated 24 covered clauses in round 1
c [cce-5-2] completed large round (ACCE)
c [cce-5-2] allowing another 12826259 steps for small clauses
c [cce-5-2] scheduling 868 clauses = 325 binary + 543 ternary
c [cce-5-2] tried to eliminate 868 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 24 covered clauses in TOTAL during 2 rounds
c [cce-5] 24 < 1/100 * 51059 = 510 considered unsuccessful
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 94298967 penalty 3 = 3 + 0
c [sweep-5-1] 1566 pos 52.1% + 1442 neg 47.9% = 3008 sched 97.9% ret 63
c [sweep-5-1] 2394904 steps 172 queries 69.82 avg class size
c [sweep-5-1] 16457 decisions 171 SAT calls 1123.29 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] 1595 pos 51.9% + 1476 neg 48.1% = 3071 sched 100.0% ret 0
c [sweep-5-2] 2216038 steps 173 queries 85.47 avg class size
c [sweep-5-2] 16688 decisions 172 SAT calls 1128.52 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] 1595 pos 51.9% + 1476 neg 48.1% = 3071 sched 100.0% ret 0
c [sweep-5-3] 2092673 steps 175 queries 78.05 avg class size
c [sweep-5-3] 16996 decisions 174 SAT calls 1081.35 avg env size
c [sweep-5-3] fully completed sweeping round
c [sweep-5-3] removed 0 vars (0 failed, 0 eqs, 1 impls)
c [sweep-5] removed 0 vars in TOTAL (3 rounds, 517 queries)
c [score-distribution-12] 3055 pos 99.48%, 16 min 0.52%, 0 zero 0.00%
c [score-distribution-12] 2142 different 69.75% out of total 3071 variables
c [simplification-12] removed 0 variables 0.0% (3071 remain 85%)
c [simplification-12] removed 24 irredundant clauses 0.0% (51035 remain 71%)
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 5418014 (soft 4918014 + delta 500000)
c [simplification-12] new conflict limit 4918014 (hard 5418014)
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 -  706.8    3071    51035   3919305  198070   5942   323   39   375   23  10%   1024   -2   36   41   88%
c -  722.7    3071    51035   3997150  199795   5943   323   40   391   24  10%   1024   12   34   41   85%
c -  738.5    3071    51035   4075740  201863   5943   323   40   379   38  11%   1024   -2   32   41   79%
c -  754.9    3071    51035   4154554  203296   5943   323   40   386   24  10%   1024    3   38   41   92%
c -  771.6    3071    51035   4234606  205316   5945   323   40   380   24  10%   1024   -3   37   41   90%
c -  788.3    3071    51035   4315083  206779   5946   323   40   382   24  10%   1024    2   41   41  101%
c -  805.5    3071    51035   4396457  209709   5947   323   42   374   24  11%   1024   -4   42   41  100%
c -  822.5    3071    51035   4477451  210837   5948   323   40   381   25  11%   1024    1   39   41   96%
c -  839.9    3071    51035   4559659  213119   5949   323   41   382   25  11%   1024   -1   40   42   97%
c -  856.7    3071    51035   4641791  216771   5950   323   43   387   25  11%   1024   -0   42   42   99%
c -  873.9    3071    51035   4722513  216893   5950   323   44   397   25  11%   1024   12   59   42  139%
c -  891.8    3071    51035   4805718  218462   5950   323   40   376   25  11%   1024   -6   42   42   99%
c -  909.7    3071    51035   4889648  220470   5953   323   41   387   26  11%   1024    2   35   42   84%
c 
c [simplification-13] limit 4918014 conflicts (hard 5418014) hit after 4918015 conflicts
c [quatres-11] found 28528 quaternary clauses 13% in total
c [quatres-11-1] removed 83 duplicate quaternary clauses
c [quatres-11-1] added 1 double-self-subsuming ternary resolvents
c [quatres-11-2] added 8 single-self-subsuming ternary resolvents
c [quatres-11-2] added 47 quaternary resolvents
c [ternres-11] limit 200000000 with penalty 0 = 0 + 0
c [ternres-11] all 3071 free variables schedulable
c [ternres-11] 2 ternary resolvents (0 bin, 2 trn)
c [ternres-11] fully completed ternary resolution
c [transred-10] limit 1000000 with penalty 1 = 1 + 0
c [transred-10] removed 1 transitive binary clauses
c [score-distribution-13] 3042 pos 99.06%, 29 min 0.94%, 0 zero 0.00%
c [score-distribution-13] 2396 different 78.02% out of total 3071 variables
c [simplification-13] removed 0 variables 0.0% (3071 remain 85%)
c [simplification-13] removed 0 irredundant clauses 0.0% (51035 remain 71%)
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 7918015 (soft 6918015 + delta 1000000)
c [simplification-13] new conflict limit 6918015 (hard 7918015)
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 -  928.0    3071    51035   4973882  222094   5963   322   41   387   25  11%   1024    4   41   42   99%
c -  946.6    3071    51035   5058823  222990   5963   322   42   399   26  11%   1024   11   38   42   91%
c -  965.6    3071    51035   5145259  225178   5964   322   43   390   26  11%   1024    2   38   42   89%
c -  984.3    3071    51035   5231736  227463   5965   322   40   367   26  11%   1024  -19   44   43  103%
c
c CAUGHT SIGNAL 15 SIGTERM
c
c s UNKNOWN
c bate: 67 basic ate = 61 trn 91% + 6 lrg 9% in 1 updates
c bcas: 4 count, 0 added (0 skipped), 317614 steps
c bkwd: tried 5979 clauses, 11893 lits, 1.99 lits/clause
c bkwd: checked 555930 occs, 92.98 occs/clause, 46.74 occs/lit
c bkwd: subsumed 0 binary, 2 ternary, 19 large
c bkwd: strengthened 0 binary, 3 ternary (100% self), 63 large (0% self)
c blkd: 4 bces, 109 removed, 2495557 resolutions, 5245116 steps
c blkd: 33 blocking literals 0%, 0 pure
c bump: 5277125 bumped seen, 536118200 lits 101.6 on average
c card: 4 count, 0 units, 0 am1, 10183203 steps
c card: 0 rescheduled, 0 eliminated, 0 resolved, 1467 subsumed
c card: 11 at-most-one constraints found, average size 3.00
c card: 11 at-most-one constraints used 100%, average size 3.00
c card: 78 at-most-two constraints found, average size 4.05
c card: 77 at-most-two constraints used 99%, average size 4.05
c cces: 5 cces, 6737 eliminated, 6699 ate 99%, 38 abce 1%
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: 960382 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 50 gcs, 0 rescored clauses, 2776 rescored vars
c dcps: 34 decompositions, 276 equivalent 7%
c deco: 6207 decision-only clauses 0%, 43% reduction
c decs: 33081437 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c dsch: 101341483 push, 101339460 pop (101339460 dec 100%)
c dsch: 1543656396 swaps, 0 down, 507724123 up
c elms: 5 elims, 101 eliminated 2%, 0 pure 0%
c elms: 9 rounds, 1.8 rounds/bve
c elms: 101 small 100%, 0 large 0%
c elms: 1474 tried small, 102 succeeded 7%, 1372 failed 93%
c elms: 2400 subsumed, 2882 strengthened, 3 blocked
c elms: 1017556 copies, 2382806 resolutions, 406795 ipos
c elms: 215504 subchks, 162214 strchks
c gaus: 4 extractions, 8457 extracted, 5.1 size, 7 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 1 gc, 19129512 steps, 9564756 extr 50%, 275464 elim 1%
c glue: 35.7 orig avg, 35.7 real avg, 5.0 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 131 = 31 simple 24% + 76 trn 58% + 24 lrg 18%, 33 sub 25%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 5277124 clauses, 75.1 length
c lrnd: 396443064 lits = 421271939 orig - 24828875 removed 6%
c lrnd: 2366121 uips 45%, 2358687 flips 45%
c mins: 4922668 mins 93%, 65 bin 0%, 337387 size 6%
c mins: 322482950 poisoned searches, 30272121 hits, 9% hit rate
c mins: 642989663 used twice searches, 118303901 hits, 18% hit rate
c move: moved 434, 12 bin 3%, 422 trn 97%
c otfs: 32840 driving 48%, 35881 restarting 52%
c otfs: str 68721, 67097 red 98%, 1624 irr 2%
c otfs: str 68721, 0 bin 0%, 160 trn 0%, 68561 lrg 100%
c otfs: sub 442, 437 red 99%, 5 irr 1%
c otfs: sub 442, 0 bin 0%, 27 trn 6%, 415 lrg 94%
c phas: 1 computed, 3108 set, 1344 pos (43%), 1764 neg (57%)
c prbs: 2 basic, 3952 probed, 0 failed, 0 lifted
c prbs: 3 simple, 12891 probed, 32 failed, 140 eqs
c prbs: 3 treelook, 5444 probed, 0 failed, 0 lifted
c prom: 826682 locked 17% out of 4975363 tried
c prps: 586859514 props, 18 props/dec
c prps: 100% srch, 0% simp, 0% lkhd
c quat: 11 count, 2542 quat, 2138 self1, 213 self2, 541 dup
c redc: 797 clauses 0%, 521806 tried 10%, 2 sat 0%
c redc: 827 lits 0%, 4307388 tried 1%, 2 sat 0%
c redc: 24 times jump level reduced, 16.1 levels on average
c reds: 79 count, 67178.6 conflicts per reduce
c reds: 0 memlim 0%, 79 arith 100%
c reds: 3477791 collected 70%, 1466511 retired 30%
c rmbd: 35 removed, 20 red 57%
c rsts: 37038 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: 5277124 count (10183562 tried 1.9), 25686 sub out of 5274759 (0.5%)
c swps: 5 count, 13 rounds, 3389 queries (260.7/round)
c swps: 3399 sat calls, 17 unsat (0.8% success rate)
c swps: 117799 decisions 34.7, 2859 conflicts 0.8
c swps; 160.4 avg class size, 201.2 avg environment size
c swps: 0 failed, 14 impls, 6 equivs
c swp0: 1127 type 0 queries, 45 unsat (4.0%), 1126 sat (99.9%)
c swp1: 2262 type 1 queries, 173 unsat (7.6%), 2257 sat (99.8%)
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: 76722955 calls to obtain time
c tops: 680 fixed 16%, 1 its, 5307106.00 confs/it
c trds: 10 transitive reductions, 85 removed, 1 failed
c trds: 61215 nodes, 5864 edges, 8821 steps
c trim: 189933 words, 0.7 MB
c trnr: 11 count, 99 bin, 890 trn, 21900188 steps
c unhd: 4 count, 6 rounds, 4432821 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: 1333 tauts, 0 bin 0%, 1028 trn 77%, 296 lrg 22%
c unhd: 1333 tauts, 9 stamp 1%, 865 red 65%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 28043 str, 0 bin 0%, 95 trn 0%, 27948 lrg 100%, 27923 red 100%
c vars: 3071 remaining 74% and 1057 removed 26% out of 4128
c vars: 680 fixed 16%, 101 eliminated 2%, 276 equivalent 7%
c vsts: 37368588376 visits, 100% srch, 0% simp, 0% lkhd
c vsts: 63.7 search visits per propagation, 7039.3 per conflict
c wchs: 10647100834 pushed, 14128730 enlarged, 1147 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all        5277301       3477791       1466511     245235556      52676581       2629457
c 
c  0 0        190013   4       266   0         0   0 199313370  81< 38644272  73   1918777  73     6.0
c  1 5        220756   4     90515   3    108192   7  24579499  10   5423874  10<   292767  11<    0.7
c  2 6        738870  14    406865  12    299330  20  11572083   5   3255386   6    164324   6     1.3
c  3 9        789249  15    509611  15    263553  18   3346269   1   1465716   3     58263   2     1.0
c  4 14       694870  13    490160  14    191933  13   2009925   1   1070253   2     43941   2     1.2
c  5 21       584005  11<   423522  12    149364  10<  1299332   1    760911   1     33080   1     1.7
c  6 30       476907   9    352030  10<   115572   8    856543   0    533185   1     24615   1     2.1
c  7 41       396560   8    298990   9     89945   6    618150   0    403366   1     20194   1     2.8
c  8 54       330733   6    254606   7     69377   5    472201   0    319868   1     17649   1     3.4
c  9 69       274238   5    213905   6     54181   4    373941   0    258894   0     15614   1     3.8
c 10 86       388689   7    302318   9     76107   5    528084   0    367596   1     25587   1     8.3
c 11 126      180048   3    129195   4     44959   3    248866   0    162606   0     13719   1     6.0
c 12 230       12363   0      5808   0      3998   0     17293   0     10654   0       927   0     0.7
c 
c avg                  5.0           5.5           4.6           0.4           0.8           0.8
c std                  2.9           2.8           2.7           1.2           1.8           1.9
c 
c   33.019   3% decide
c   29.381   3% bump
c    2.854   0% cce
c 
c    5.665 < 1% rest (below)
c 
c    1.874   0% elim
c    1.862   0% sweep
c    1.071   0% quatres
c    0.709   0% unhide
c    0.626   0% probe
c    0.431   0% block
c    0.429   0% gauss
c    0.188   0% rescore
c    0.148   0% card
c    0.122   0% ternres
c    0.063   0% bca
c    0.015   0% transred
c    0.000   0% locs
c    0.000   0% queuesort
c ==================================
c    0.400   0% preprocessing     3%
c   11.366   1% inprocessing     97%
c ==================================
c   11.766   1% simplifying
c  988.156  99% search
c ==================================
c  999.922 100% all
c 
c       5307106 conflicts,        5307.5 confs/sec
c          1965 ternaries,        2700.8 confs/ternary
c            92 binaries,        57685.9 confs/binary
c             1 iterations,    5307106.0 confs/iteration
c 
c            79 reductions,          0.1 redus/sec,  67178.6 confs/reduction
c         37038 restarts,           37.0 rests/sec,    143.3 confs/restart
c      33081437 decisions,       33084.0 decis/sec,      6.2 decis/conflict
c     586859514 propagations,   586905.4 props/sec,     17.7 props/decision
c 
c 999.9 seconds, 112.4 MB
c
c CAUGHT SIGNAL 15 SIGTERM
c
c launch: done
