c launch: /data/cnf/sc2014/app/006-23-96.cnf.bz2
c host: atom14
c Lingeling SAT Solver
c 
c Version b7ztzu 7b29300825af9bcc1c8b2c5ebcf65fa1cb101cad
c 
c Copyright (C) 2010-2014 Armin Biere JKU Linz Austria.
c All rights reserved.
c 
c released Sun Apr 26 19:26:13 CEST 2015
c compiled Sun Apr 26 19:26:13 CEST 2015
c 
c gcc (Ubuntu 4.8.2-19ubuntu1) 4.8.2
c -Wall -O3 -I../yalsat -I../druplig -DNLGLOG -DNDEBUG -DNCHKSOL
c Linux cluster2 3.13.0-45-generic x86_64
c 
c piping '/data/cnf/sc2014/app/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 --queuesort=1
c --queuesortjwh=0
c --randec=0
c --randecint=1000
c --redcls=1
c --redclsglue=6
c --redclsmaxdec=5
c --redclsmaxdepth=10
c --redclsmaxlrg=10
c --redclsmaxprops=100
c --redclsatlimlo=0
c --redclsatlimhi=100
c --redclsize=30
c --redclstype=4
c --reducefixed=0
c --reduceinc=1000
c --reduceinit=50000
c --reduce=1
c --restart=4
c --restartglcint=10
c --restartglclim=115
c --restartinit=0
c --restartint=5
c --restartpen=1
c --retirenb=1
c --retireint=4
c --retiremin=1
c --reusetrail=0
c --rmincpen=4
c --rstinoutinc=110
c --satlimdelay=10000
c --scincinc=200
c --scincincsatlimhi=100
c --scincincdelta=10
c --scincincincint=100000
c --scincincmin=200
c --scincincmode=1
c --score=2
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 [score-type] VMTF (--score=2)
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 [sort-queue-1] sorted 3406 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 3406 (100%)
c [score-dist-1] max exp 0, different 1 (100%)
c [score-dist-1] median active exp 0, avg 0.0
c [simplification-1] removed 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 [decomp-3] removed 1 variables
c [simpleprobe-2] all 3405 free variables schedulable
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [simpleprobe-2] 1898 variables remain 56% (1507 retained 44%)
c [simpleprobe-2] removed 0 variables, found 3 hbrs, 0 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 6810 literals 100%
c [treelook-1] scheduling used 292714 steps
c [treelook-1] scheduled completely
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 300081 steps
c [treelook-1] 5622 literals remain 83%
c [treelook-1] 3393 variables remain to probed next time 100%
c [treelook-1] removed 0 variables, found 10 hbrs
c [basicprobe-1] limit 1000000 penalty 0 = 0 + 0
c [basicprobe-1-0] 355 sched 10%, 1 failed, 0 lifted, 22 hbrs
c [decomp-6] removed 2 variables
c [basicprobe-1-1] 355 sched 10%, 0 failed, 0 lifted, 1 hbrs
c [basicprobe-1-2] 356 sched 10%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-1-2] fully completed probing
c [basicprobe-1-2] 1 units = 1 failed (100%) + 0 lifted (0%)
c [basicprobe-1-2] removed 2 variables, found 23 hbrs
c [block-1] scheduling all variables this time
c [block-1] scheduled 3403 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 * 68052 = 680 considered unsuccessful
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 3501 clauses out of 21527 (16%) of length 7
c [cce-1-1] eliminated 447 clauses out of 20647 (2%) of length 6
c [cce-1-1] eliminated 2515 clauses out of 13702 (18%) of length 5
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 6463 large clauses in 30000013 steps
c [cce-1-1] allowing another 15000006 steps for small clauses
c [cce-1-1] scheduling 4420 clauses = 231 binary + 4189 ternary
c [cce-1-1] tried to eliminate 4420 small clauses 100%
c [cce-1-1] eliminated 3 binary clauses 1%
c [cce-1-1] eliminated 1043 ternary clauses 25%
c [cce-1-1] eliminated 1046 small clauses 24%
c [cce-1-1] eliminated 1046 small clauses in 16193990 steps
c [cce-1-1] completed small round (ATE)
c [cce-1-1] eliminated 7509 covered clauses in round 1
c [cce-1-2] incomplete large round (ATE)
c [cce-1-2] allowing another 6903028 steps for small clauses
c [cce-1-2] scheduling 3374 clauses = 228 binary + 3146 ternary
c [cce-1-2] tried to eliminate 3374 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 7509 covered clauses in TOTAL during 2 rounds
c [elim-2] scheduling all variables this time
c [elim-2] scheduled 3403 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 724 not tried 21% in round 1
c [elim-2] transition to [ all 1 rem 1 ] state
c [elim-2] eliminated 21 = 1% variables out of 3403 scheduled
c [elim-2] 21 < 1/100 * 3403 = 34 considered unsuccessful
c [bca-1] limit of 10000000 steps and 119760 added (scaled 2)
c [bca-1] 4983 out of 6766 literals actually usable 74%
c [bca-1] added 0 blocked clauses in 34304 steps
c [sweep-1] limit 1000000 penalty 0 = 0 + 0
c [sweep-1-1] 1636 pos 48.4% + 1746 neg 51.6% = 3382 sched 100.0% ret 0
c [sweep-1-1] 521055 steps 579 queries 185.93 avg class size
c [sweep-1-1] 8965 decisions 580 SAT calls 21.88 avg env size
c [sweep-1-1] fully completed sweeping round
c [decomp-8] removed 4 variables
c [sweep-1-1] removed 4 vars (0 failed, 4 eqs, 3 impls)
c [sweep-1-2] 1635 pos 48.4% + 1743 neg 51.6% = 3378 sched 100.0% ret 0
c [sweep-1-2] 479273 steps 559 queries 179.10 avg class size
c [sweep-1-2] 8676 decisions 558 SAT calls 21.89 avg env size
c [sweep-1-2] 37 variables remain 1% (3341 retained 99%)
c [decomp-9] removed 1 variables
c [sweep-1-2] removed 1 vars (0 failed, 1 eqs, 0 impls)
c [sweep-1] removed 5 vars in TOTAL (2 rounds, 1136 queries)
c [sort-queue-2] sorted 3377 enqueued variables after 1000 conflicts
c [score-dist-2] active 0 (0%), one 2987 (88%), zero 390 (12%)
c [score-dist-2] max exp 1, different 2 (100%)
c [score-dist-2] median active exp 0, avg 0.0
c [simplification-2] removed 29 variables 0.9% (3377 remain 89%)
c [simplification-2] removed 8449 irredundant clauses 12.4% (59618 remain 78%)
c [simplification-2] maximum reduction of 12% = max (1%, 12%)
c [simplification-2] large reduction 12% >= 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 3001 conflicts
c [quatres-1] found 7257 quaternary clauses 13% in total
c [quatres-1-1] added 27 double-self-subsuming ternary resolvents
c [quatres-1-2] added 103 single-self-subsuming ternary resolvents
c [quatres-1-2] added 279 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 3377 free variables schedulable
c [ternres-1] 262 ternary resolvents (19 bin, 243 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.0
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 4400 xors of average arity 4.7
c [gauss-1] connected 20582 occurrences of 905 variables (average 22.7)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] connected 1990 occurrences of 905 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 3 variables
c [unhide-2] limit 50000 with penalty 1 = 1 + 0
c [unhide-2-2] 0 units, 0 failed, 83 tauts, 0 hbrs, 161 literals
c [transred-1] limit 100000 with penalty 0 = 0 + 0
c [transred-1] removed 10 transitive binary clauses
c [cce-2] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-2-1] eliminated 2 clauses out of 16872 (0%) of length 7
c [cce-2-1] eliminated 169 clauses out of 20652 (1%) of length 6
c [cce-2-1] eliminated 144 clauses out of 11361 (1%) of length 5
c [cce-2-1] eliminated 303 clauses out of 6614 (5%) of length 4
c [cce-2-1] completed large round (ATE)
c [cce-2-1] eliminated 618 large clauses in 29846452 steps
c [cce-2-1] allowing another 14923226 steps for small clauses
c [cce-2-1] scheduling 930 clauses = 250 binary + 680 ternary
c [cce-2-1] tried to eliminate 930 small clauses 100%
c [cce-2-1] eliminated 1 binary clauses 0%
c [cce-2-1] eliminated 39 ternary clauses 6%
c [cce-2-1] eliminated 40 small clauses 4%
c [cce-2-1] eliminated 40 small clauses in 15129826 steps
c [cce-2-1] completed small round (ATE)
c [cce-2-1] completed small and large (ATE)
c [cce-2-1] eliminated 658 covered clauses in round 1
c [cce-2-2] incomplete large round (ATE)
c [cce-2-2] allowing another 7435101 steps for small clauses
c [cce-2-2] scheduling 890 clauses = 249 binary + 641 ternary
c [cce-2-2] tried to eliminate 890 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 658 covered clauses in TOTAL during 2 rounds
c [sweep-2] limit 1000000 penalty 0 = 0 + 0
c [sweep-2-1] 24 pos 64.9% + 13 neg 35.1% = 37 sched 1.1% ret 3337
c [sweep-2-1] 11335 steps 23 queries 8.30 avg class size
c [sweep-2-1] 323 decisions 22 SAT calls 19.45 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, 0 impls)
c [sweep-2-2] 1710 pos 50.7% + 1663 neg 49.3% = 3373 sched 100.0% ret 0
c [sweep-2-2] 520456 steps 546 queries 170.64 avg class size
c [sweep-2-2] 9604 decisions 548 SAT calls 24.28 avg env size
c [sweep-2-2] fully completed sweeping round
c [decomp-12] removed 1 variables
c [sweep-2-2] removed 1 vars (0 failed, 0 eqs, 0 impls)
c [sweep-2-3] 1710 pos 50.7% + 1662 neg 49.3% = 3372 sched 100.0% ret 0
c [sweep-2-3] 468493 steps 495 queries 199.11 avg class size
c [sweep-2-3] 8323 decisions 494 SAT calls 23.76 avg env size
c [sweep-2-3] 198 variables remain 6% (3174 retained 94%)
c [decomp-13] removed 1 variables
c [sweep-2-3] removed 1 vars (0 failed, 1 eqs, 1 impls)
c [sweep-2] removed 3 vars in TOTAL (3 rounds, 1061 queries)
c [sort-queue-3] sorted 3371 enqueued variables after 3001 conflicts
c [score-dist-3] active 0 (0%), one 3241 (96%), zero 130 (4%)
c [score-dist-3] max exp 1, different 2 (100%)
c [score-dist-3] median active exp 0, avg 0.0
c [simplification-3] removed 6 variables 0.2% (3371 remain 88%)
c [simplification-3] removed 675 irredundant clauses 1.1% (58942 remain 77%)
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 23001 (soft 13001 + delta 10000)
c [simplification-3] new conflict limit 13001 (hard 23001)
c 
c [simplification-4] limit 13001 conflicts (hard 23001) hit after 13001 conflicts
c [quatres-2] found 7972 quaternary clauses 13% in total
c [quatres-2-1] added 42 double-self-subsuming ternary resolvents
c [quatres-2-2] added 207 single-self-subsuming ternary resolvents
c [quatres-2-2] added 263 quaternary resolvents
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] all 3371 free variables schedulable
c [ternres-2] 77 ternary resolvents (5 bin, 72 trn)
c [ternres-2] fully completed ternary resolution
c [decomp-14] removed 1 variables
c [treelook-2] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-2] scheduled 3327 literals 49%
c [treelook-2] scheduling used 150054 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-2] used 150091 steps
c [treelook-2] 2690 literals remain 40%
c [treelook-2] 1854 variables remain to probed next time 55%
c [treelook-2] removed 0 variables, found 12 hbrs
c [transred-2] limit 263429 with penalty 0 = 0 + 0
c [transred-2] removed 3 transitive binary clauses
c [block-2] scheduling all variables this time
c [block-2] scheduled 3370 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 2 blocked clauses
c [block-2] 2 < 1/100 * 58939 = 589 considered unsuccessful
c [cce-3] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-3-1] eliminated 2 clauses out of 16774 (0%) of length 7
c [cce-3-1] eliminated 11 clauses out of 20540 (0%) of length 6
c [cce-3-1] eliminated 21 clauses out of 11230 (0%) of length 5
c [cce-3-1] eliminated 16 clauses out of 6242 (0%) of length 4
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 50 large clauses in 30000063 steps
c [cce-3-1] allowing another 15000031 steps for small clauses
c [cce-3-1] scheduling 3483 clauses = 258 binary + 3225 ternary
c [cce-3-1] tried to eliminate 3483 small clauses 100%
c [cce-3-1] eliminated 30 ternary clauses 1%
c [cce-3-1] eliminated 30 small clauses 1%
c [cce-3-1] eliminated 30 small clauses in 15984172 steps
c [cce-3-1] completed small round (ACCE)
c [cce-3-1] eliminated 80 covered clauses in round 1
c [cce-3-2] incomplete large round (ACCE)
c [cce-3-2] allowing another 7007934 steps for small clauses
c [cce-3-2] scheduling 3453 clauses = 258 binary + 3195 ternary
c [cce-3-2] tried to eliminate 3453 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 80 covered clauses in TOTAL during 2 rounds
c [cce-3] 80 < 1/100 * 58937 = 589 considered unsuccessful
c [elim-3] 724 variables 21% will be scheduled this time
c [elim-3] scheduled 724 variables 21%
c [elim-3] limit of 10000000 steps penalty 1 = 1 + 0
c [elim-3] rescheduling of touched variables disabled
c [elim-3] incomplete 307 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 724 scheduled
c [bca-2] limit of 10000000 steps and 118184 added (scaled 2)
c [bca-2] 833 out of 6742 literals actually usable 12%
c [bca-2] added 0 blocked clauses in 18767 steps
c [sweep-3] limit 1000000 penalty 0 = 0 + 0
c [sweep-3-1] 98 pos 49.5% + 100 neg 50.5% = 198 sched 5.9% ret 3172
c [sweep-3-1] 83293 steps 113 queries 24.40 avg class size
c [sweep-3-1] 2075 decisions 112 SAT calls 24.59 avg env size
c [sweep-3-1] fully completed sweeping round
c [sweep-3-1] removed 0 vars (0 failed, 0 eqs, 1 impls)
c [sweep-3-2] 1677 pos 49.8% + 1693 neg 50.2% = 3370 sched 100.0% ret 0
c [sweep-3-2] 588192 steps 460 queries 120.78 avg class size
c [sweep-3-2] 10957 decisions 459 SAT calls 32.49 avg env size
c [sweep-3-2] fully completed sweeping round
c [sweep-3-2] removed 0 vars (0 failed, 0 eqs, 1 impls)
c [sweep-3-3] 1677 pos 49.8% + 1693 neg 50.2% = 3370 sched 100.0% ret 0
c [sweep-3-3] 329135 steps 216 queries 326.30 avg class size
c [sweep-3-3] 5884 decisions 215 SAT calls 37.31 avg env size
c [sweep-3-3] 1365 variables remain 41% (2005 retained 59%)
c [sweep-3-3] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-3] removed 0 vars in TOTAL (3 rounds, 786 queries)
c [sort-queue-4] sorted 3370 enqueued variables after 13001 conflicts
c [score-dist-4] active 0 (0%), one 3308 (98%), zero 62 (2%)
c [score-dist-4] max exp 1, different 2 (100%)
c [score-dist-4] median active exp 0, avg 0.0
c [simplification-4] removed 1 variables 0.0% (3370 remain 88%)
c [simplification-4] removed 99 irredundant clauses 0.2% (58842 remain 77%)
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 58001 (soft 43001 + delta 15000)
c [simplification-4] new conflict limit 43001 (hard 58001)
c 
c [simplification-5] limit 43001 conflicts (hard 58001) hit after 43002 conflicts
c [quatres-3] found 10015 quaternary clauses 15% in total
c [quatres-3-1] added 47 double-self-subsuming ternary resolvents
c [quatres-3-2] added 342 single-self-subsuming ternary resolvents
c [quatres-3-2] added 306 quaternary resolvents
c [ternres-3] limit 4000000 with penalty 0 = 0 + 0
c [ternres-3] all 3370 free variables schedulable
c [ternres-3] 47 ternary resolvents (7 bin, 40 trn)
c [ternres-3] fully completed ternary resolution
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] extracted 1463 xors of average arity 4.0
c [gauss-2] connected 5827 occurrences of 368 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 [basicprobe-2] limit 6275365 penalty 0 = 0 + 0
c [basicprobe-2-0] 477 sched 14%, 0 failed, 0 lifted, 7 hbrs
c [basicprobe-2-1] 479 sched 14%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-2-1] fully completed probing
c [basicprobe-2-1] removed 0 variables, found 7 hbrs
c [bate-1] eliminated 10 asymmetric tautologies during probing
c [transred-3] limit 1255073 with penalty 0 = 0 + 0
c [transred-3] removed 3 transitive binary clauses
c [sort-queue-5] sorted 3370 enqueued variables after 43002 conflicts
c [score-dist-5] active 0 (0%), one 3318 (98%), zero 52 (2%)
c [score-dist-5] max exp 1, different 2 (100%)
c [score-dist-5] median active exp 0, avg 0.0
c [simplification-5] removed 0 variables 0.0% (3370 remain 88%)
c [simplification-5] removed 10 irredundant clauses 0.0% (58832 remain 77%)
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 133002 (soft 103002 + delta 30000)
c [simplification-5] new conflict limit 103002 (hard 133002)
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 -   14.9    3370    58832     74326   27888   3506   162   12   319   14   4%    689  130    8    7  116%
c 
c [simplification-6] limit 103002 conflicts (hard 133002) hit after 103003 conflicts
c [quatres-4] found 13109 quaternary clauses 16% in total
c [quatres-4-1] removed 1 duplicate quaternary clauses
c [quatres-4-1] added 52 double-self-subsuming ternary resolvents
c [quatres-4-2] added 441 single-self-subsuming ternary resolvents
c [quatres-4-2] added 328 quaternary resolvents
c [ternres-4] limit 4081808 with penalty 0 = 0 + 0
c [ternres-4] all 3370 free variables schedulable
c [ternres-4] 155 ternary resolvents (26 bin, 129 trn)
c [ternres-4] fully completed ternary resolution
c [card-3] limit 510226 penalty 2 = 2 + 0
c [card-3] found 4 at-most-one constraints of average size 3.0
c [card-3] found 24 at-most-two constraints of average size 4.0
c [card-3] using previous limit 510226 for elimination
c [card-3] 27 out of 28 constraints (96%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [decomp-21] removed 1 variables
c [unhide-3] limit 204090 with penalty 2 = 2 + 0
c [unhide-3-3] 0 units, 0 failed, 61 tauts, 0 hbrs, 1342 literals
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 12 transitive binary clauses
c [transred-4] found 1 units
c [cce-4] boosting limit by 10
c [cce-4] limit of 150000000 steps penalty 1 = 1 + 0
c [cce-4-1] eliminated 74 clauses out of 20896 (0%) of length 6
c [cce-4-1] eliminated 28 clauses out of 11264 (0%) of length 5
c [cce-4-1] eliminated 117 clauses out of 6158 (2%) of length 4
c [cce-4-1] completed large round (ATE)
c [cce-4-1] eliminated 219 large clauses in 29187646 steps
c [cce-4-1] allowing another 14593823 steps for small clauses
c [cce-4-1] scheduling 3469 clauses = 268 binary + 3201 ternary
c [cce-4-1] tried to eliminate 3469 small clauses 100%
c [cce-4-1] eliminated 1 binary clauses 0%
c [cce-4-1] eliminated 2 ternary clauses 0%
c [cce-4-1] eliminated 3 small clauses 0%
c [cce-4-1] eliminated 9 small clauses in 15501575 steps
c [cce-4-1] completed small round (ATE)
c [cce-4-1] eliminated 228 covered clauses in round 1
c [cce-4-2] completed large round (ATE)
c [cce-4-2] allowing another 14550658 steps for small clauses
c [cce-4-2] scheduling 3466 clauses = 267 binary + 3199 ternary
c [cce-4-2] tried to eliminate 3466 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 228 covered clauses in TOTAL during 2 rounds
c [cce-4] 228 < 1/100 * 58825 = 588 considered unsuccessful
c [sweep-4] limit 612271 penalty 1 = 1 + 0
c [sweep-4-1] 644 pos 47.2% + 721 neg 52.8% = 1365 sched 40.5% ret 2003
c [sweep-4-1] 616468 steps 179 queries 73.85 avg class size
c [sweep-4-1] 10296 decisions 178 SAT calls 88.96 avg env size
c [sweep-4-1] 58 variables remain 2% (3310 retained 98%)
c [sweep-4-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-4] removed 0 vars in TOTAL (1 rounds, 178 queries)
c [sort-queue-6] sorted 3368 enqueued variables after 103003 conflicts
c [score-dist-6] active 0 (0%), one 3364 (100%), zero 4 (0%)
c [score-dist-6] max exp 1, different 2 (100%)
c [score-dist-6] median active exp 0, avg 0.0
c [simplification-6] removed 2 variables 0.1% (3368 remain 88%)
c [simplification-6] removed 235 irredundant clauses 0.4% (58597 remain 77%)
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 283003 (soft 223003 + delta 60000)
c [simplification-6] new conflict limit 223003 (hard 283003)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c -   26.2    3368    58597    130941   37344   4488   198   13   320    9   4%    883   53   13   10  134%
c -   36.5    3368    58597    185484   46225   4758   204   14   330   10   4%    963   32   12   12  104%
c 
c [simplification-7] limit 223003 conflicts (hard 283003) hit after 223003 conflicts
c [quatres-5] found 17270 quaternary clauses 18% in total
c [quatres-5-1] removed 7 duplicate quaternary clauses
c [quatres-5-1] added 40 double-self-subsuming ternary resolvents
c [quatres-5-2] added 490 single-self-subsuming ternary resolvents
c [quatres-5-2] added 293 quaternary resolvents
c [ternres-5] limit 10090258 with penalty 0 = 0 + 0
c [ternres-5] all 3368 free variables schedulable
c [ternres-5] 87 ternary resolvents (5 bin, 82 trn)
c [ternres-5] fully completed ternary resolution
c [simpleprobe-3] 1874 schedulable variables 56%
c [simpleprobe-3] limit 20180517 penalty 1 = 1 + 0
c [simpleprobe-3] fully completed simple probing
c [simpleprobe-3] removed 0 variables, found 21 hbrs, 0 units
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 20 transitive binary clauses
c [block-3] scheduling all variables this time
c [block-3] scheduled 3368 variables 100%
c [block-3] limit of 25225646 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 * 58597 = 585 considered unsuccessful
c [elim-4] scheduling all variables this time
c [elim-4] scheduled 3368 variables 100%
c [elim-4] boosting limit by 20
c [elim-4] limit of 1009025870 steps penalty 2 = 2 + 0
c [elim-4] rescheduling of touched variables disabled
c [elim-4-1] eliminated 2 variables 0% in round 1 in 44467765 steps
c [elim-4-1] backward subsumption/strengthening limit 44467700
c [elim-4-1-1] backward checking 1170 touched variables 35%
c [elim-4-1-1] fully completed backward checking in 1 rounds
c [elim-4-1] subsumed 0 and strengthened 0 clauses in 591935 steps
c [elim-4] fully completed in 1 rounds
c [elim-4] transition to [ all 0 rem 0 ] state
c [elim-4] eliminated 2 = 0% variables out of 3368 scheduled
c [elim-4] 2 < 1/100 * 3368 = 33 considered unsuccessful
c [bca-3] limit of 10000000 steps and 117628 added (scaled 2)
c [bca-3] 3 out of 6734 literals actually usable 0%
c [bca-3] not enough literals usable
c [bca-3] added 0 blocked clauses in 81414 steps
c [sort-queue-7] sorted 3366 enqueued variables after 223003 conflicts
c [score-dist-7] active 0 (0%), one 3366 (100%), zero 0 (0%)
c [score-dist-7] max exp 1, different 1 (50%)
c [score-dist-7] median active exp 0, avg 0.0
c [simplification-7] removed 2 variables 0.1% (3366 remain 88%)
c [simplification-7] removed 33 irredundant clauses 0.1% (58564 remain 77%)
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 583003 (soft 463003 + delta 120000)
c [simplification-7] new conflict limit 463003 (hard 583003)
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 -   46.4    3366    58564    238303   48271   5478   206   15   332   17   5%    997   19   16   13  117%
c -   55.2    3366    58564    296124   57103   5599   206   17   320   18   5%   1013   -8   19   15  124%
c -   63.1    3366    58564    351223   62973   5688   206   18   356   19   5%   1019   21   19   16  117%
c -   71.1    3366    58564    406047   67827   5773   206   19   347   12   5%   1022    2   19   17  111%
c -   79.5    3366    58564    461604   72446   5847   206   20   348   13   6%   1023   -4   21   18  117%
c 
c [simplification-8] limit 463003 conflicts (hard 583003) hit after 463157 conflicts
c [quatres-6] found 21922 quaternary clauses 18% in total
c [quatres-6-1] removed 23 duplicate quaternary clauses
c [quatres-6-1] added 25 double-self-subsuming ternary resolvents
c [quatres-6-2] added 339 single-self-subsuming ternary resolvents
c [quatres-6-2] added 216 quaternary resolvents
c [ternres-6] limit 20053501 with penalty 0 = 0 + 0
c [ternres-6] all 3366 free variables schedulable
c [ternres-6] 5 ternary resolvents (2 bin, 3 trn)
c [ternres-6] fully completed ternary resolution
c [gauss-3] limit 1002675 penalty 2 = 2 + 0
c [gauss-3] extracted 549 xors of average arity 3.0
c [gauss-3] connected 1647 occurrences of 150 variables (average 11.0)
c [gauss-3] limit 1002675 penalty 2 = 2 + 0
c [gauss-3] fully completed
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 6 transitive binary clauses
c [sort-queue-8] sorted 3366 enqueued variables after 463157 conflicts
c [score-dist-8] active 0 (0%), one 3366 (100%), zero 0 (0%)
c [score-dist-8] max exp 1, different 1 (50%)
c [score-dist-8] median active exp 0, avg 0.0
c [simplification-8] removed 0 variables 0.0% (3366 remain 88%)
c [simplification-8] removed 0 irredundant clauses 0.0% (58564 remain 77%)
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 1183157 (soft 943157 + delta 240000)
c [simplification-8] new conflict limit 943157 (hard 1183157)
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 -   88.0    3366    58564    517524   76289   6231   202   21   347   21   6%   1024   -9   22   19  116%
c -   96.0    3366    58564    574345   80013   6265   202   21   385   13   6%   1024   22   21   20  105%
c -  104.2    3366    58564    632159   83694   6286   202   23   376   22   6%   1024    2   25   22  116%
c -  112.7    3366    58564    690781   87010   6303   202   24   394   23   6%   1024   11   21   22   92%
c -  121.5    3366    58564    750451   91054   6328   202   25   385   23   6%   1024   -1   28   23  120%
c -  130.2    3366    58564    810612   95670   6339   202   24   366   24   7%   1024  -18   29   24  121%
c -  139.3    3366    58564    870394   99405   6355   202   25   387   15   7%   1024    3   29   24  118%
c -  148.3    3366    58564    930631  103388   6371   202   25   388   25   6%   1024   -0   22   25   89%
c 
c [simplification-9] limit 943157 conflicts (hard 1183157) hit after 943157 conflicts
c [quatres-7] found 25584 quaternary clauses 17% in total
c [quatres-7-1] removed 86 duplicate quaternary clauses
c [quatres-7-1] added 14 double-self-subsuming ternary resolvents
c [quatres-7-2] added 164 single-self-subsuming ternary resolvents
c [quatres-7-2] added 104 quaternary resolvents
c [ternres-7] limit 41153904 with penalty 0 = 0 + 0
c [ternres-7] all 3366 free variables schedulable
c [ternres-7] 11 ternary resolvents (1 bin, 10 trn)
c [ternres-7] fully completed ternary resolution
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 0 transitive binary clauses
c [cce-5] limit of 51442380 steps penalty 2 = 2 + 0
c [cce-5-1] eliminated 18 clauses out of 21312 (0%) of length 6
c [cce-5-1] eliminated 23 clauses out of 11345 (0%) of length 5
c [cce-5-1] eliminated 26 clauses out of 6027 (0%) of length 4
c [cce-5-1] completed large round (ACCE)
c [cce-5-1] eliminated 67 large clauses in 31982795 steps
c [cce-5-1] allowing another 15991397 steps for small clauses
c [cce-5-1] scheduling 1096 clauses = 270 binary + 826 ternary
c [cce-5-1] tried to eliminate 1096 small clauses 100%
c [cce-5-1] eliminated 12 ternary clauses 1%
c [cce-5-1] eliminated 12 small clauses 1%
c [cce-5-1] eliminated 12 small clauses in 16280631 steps
c [cce-5-1] completed small round (ACCE)
c [cce-5-1] completed small and large (ACCE)
c [cce-5-1] eliminated 79 covered clauses in round 1
c [cce-5-2] completed large round (ACCE)
c [cce-5-2] allowing another 15947950 steps for small clauses
c [cce-5-2] scheduling 1084 clauses = 270 binary + 814 ternary
c [cce-5-2] tried to eliminate 1084 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 79 covered clauses in TOTAL during 2 rounds
c [cce-5] 79 < 1/100 * 58564 = 585 considered unsuccessful
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 30865427 penalty 2 = 2 + 0
c [sweep-5-1] 25 pos 43.1% + 33 neg 56.9% = 58 sched 1.7% ret 3308
c [sweep-5-1] 153495 steps 32 queries 9.62 avg class size
c [sweep-5-1] 2319 decisions 31 SAT calls 175.65 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] 1703 pos 50.6% + 1663 neg 49.4% = 3366 sched 100.0% ret 0
c [sweep-5-2] 1380490 steps 230 queries 84.77 avg class size
c [sweep-5-2] 18078 decisions 229 SAT calls 197.89 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] 1703 pos 50.6% + 1663 neg 49.4% = 3366 sched 100.0% ret 0
c [sweep-5-3] 1190400 steps 220 queries 95.06 avg class size
c [sweep-5-3] 17437 decisions 219 SAT calls 210.69 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, 479 queries)
c [sort-queue-9] sorted 3366 enqueued variables after 943157 conflicts
c [score-dist-9] active 0 (0%), one 3366 (100%), zero 0 (0%)
c [score-dist-9] max exp 1, different 1 (50%)
c [score-dist-9] median active exp 0, avg 0.0
c [simplification-9] removed 0 variables 0.0% (3366 remain 88%)
c [simplification-9] removed 79 irredundant clauses 0.1% (58485 remain 77%)
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 2383157 (soft 1903157 + delta 480000)
c [simplification-9] new conflict limit 1903157 (hard 2383157)
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 -  159.2    3366    58485    990606  106737   6575   203   27   400   25   7%   1024   10   34   26  135%
c -  168.9    3366    58485   1051036  109475   6578   203   26   403   16   7%   1024    7   30   26  116%
c -  178.4    3366    58485   1112586  113464   6583   203   27   397   16   7%   1024    3   31   26  120%
c -  188.0    3366    58485   1174004  117043   6590   203   27   401   16   7%   1024    6   26   26   99%
c -  198.0    3366    58485   1235733  119863   6601   203   25   413   27   6%   1024   17   25   26   96%
c -  208.4    3366    58485   1298404  123480   6609   203   27   379   28   7%   1024  -22   26   27   99%
c -  219.1    3366    58485   1360939  125978   6615   203   27   409   17   7%   1024    8   30   27  110%
c -  229.8    3366    58485   1424599  129129   6620   203   28   407   29   7%   1024    9   27   28  100%
c -  240.6    3366    58485   1488707  132908   6622   203   29   402   18   7%   1024    3   31   28  110%
c -  251.6    3366    58485   1552572  135264   6626   203   28   414   18   7%   1024   11   32   28  113%
c -  262.7    3366    58485   1617678  139209   6633   203   29   419   18   7%   1024   19   28   29   98%
c -  273.8    3366    58485   1682128  142151   6638   203   31   403   30   8%   1024   -4   30   29  103%
c -  285.0    3366    58485   1746975  145017   6645   203   30   404   19   8%   1024   -4   24   30   80%
c -  296.4    3366    58485   1812262  147912   6647   203   29   410   19   7%   1024    5   24   30   79%
c -  308.2    3366    58485   1877792  150159   6653   203   31   424   19   7%   1024   15   35   31  114%
c 
c [simplification-10] limit 1903157 conflicts (hard 2383157) hit after 1903229 conflicts
c [quatres-8] found 28399 quaternary clauses 15% in total
c [quatres-8-1] removed 156 duplicate quaternary clauses
c [quatres-8-1] added 9 double-self-subsuming ternary resolvents
c [quatres-8-2] added 85 single-self-subsuming ternary resolvents
c [quatres-8-2] added 81 quaternary resolvents
c [ternres-8] limit 93942766 with penalty 0 = 0 + 0
c [ternres-8] all 3366 free variables schedulable
c [ternres-8] 9 ternary resolvents (0 bin, 9 trn)
c [ternres-8] fully completed ternary resolution
c [card-4] limit 5871422 penalty 3 = 3 + 0
c [card-4] found 1 at-most-one constraints of average size 3.0
c [card-4] found 18 at-most-two constraints of average size 4.0
c [card-4] using previous limit 5871422 for elimination
c [card-4] 19 out of 19 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [treelook-3] limit 2348569 penalty 2 = 2 + 0 boost 1
c [treelook-3] scheduled 3809 literals 57%
c [treelook-3] scheduling used 736017 steps
c [treelook-3] scheduled completely
c [treelook-3] limit 2348569 penalty 2 = 2 + 0 boost 1
c [treelook-3] used 878777 steps
c [treelook-3] fully completed tree based probing
c [unhide-4] limit 2348569 with penalty 3 = 3 + 0
c [unhide-4-6] 0 units, 0 failed, 266 tauts, 0 hbrs, 10890 literals
c [sort-queue-10] sorted 3366 enqueued variables after 1903229 conflicts
c [score-dist-10] active 0 (0%), one 3366 (100%), zero 0 (0%)
c [score-dist-10] max exp 1, different 1 (50%)
c [score-dist-10] median active exp 0, avg 0.0
c [simplification-10] removed 0 variables 0.0% (3366 remain 88%)
c [simplification-10] removed 5 irredundant clauses 0.0% (58480 remain 77%)
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 3403229 (soft 2903229 + delta 500000)
c [simplification-10] new conflict limit 2903229 (hard 3403229)
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 -  320.7    3366    58480   1944275  152823   6551   197   30   404   19   7%   1024   -6   27   30   89%
c -  332.9    3366    58480   2011215  156456   6553   197   32   411   20   8%   1024    3   33   31  106%
c -  344.9    3366    58480   2077655  159098   6555   197   32   410   20   8%   1024    0   33   31  104%
c -  357.0    3366    58480   2144706  161140   6556   197   31   396   20   8%   1024  -14   29   31   93%
c -  369.7    3366    58480   2212959  163166   6557   197   33   410   20   8%   1024   -1   36   31  114%
c -  382.9    3366    58480   2282512  165344   6558   197   34   415   21   8%   1024    1   33   32  105%
c -  396.0    3366    58480   2353159  168871   6561   197   32   414   21   8%   1024    6   38   32  119%
c -  409.5    3366    58480   2423286  171164   6561   197   33   418   21   8%   1024    7   32   32  100%
c -  423.2    3366    58480   2494416  173651   6565   197   31   408   21   8%   1024   -2   25   32   78%
c -  437.2    3366    58480   2565949  176857   6566   197   34   425   22   8%   1024   13   37   33  114%
c -  451.2    3366    58480   2637350  178940   6570   197   33   417   36   8%   1024    3   28   33   86%
c -  465.6    3366    58480   2709990  181588   6572   197   32   406   22   8%   1024   -9   34   33  105%
c -  479.8    3366    58480   2783140  184316   6572   197   32   413   22   8%   1024   -4   37   33  113%
c -  494.6    3366    58480   2856547  186432   6574   197   34   413   23   8%   1024    4   39   33  116%
c 
c [simplification-11] limit 2903229 conflicts (hard 3403229) hit after 2906526 conflicts
c [quatres-9] found 29751 quaternary clauses 14% in total
c [quatres-9-1] removed 111 duplicate quaternary clauses
c [quatres-9-1] added 3 double-self-subsuming ternary resolvents
c [quatres-9-2] added 38 single-self-subsuming ternary resolvents
c [quatres-9-2] added 51 quaternary resolvents
c [ternres-9] limit 160735767 with penalty 0 = 0 + 0
c [ternres-9] all 3366 free variables schedulable
c [ternres-9] 28 ternary resolvents (1 bin, 27 trn)
c [ternres-9] fully completed ternary resolution
c [transred-8] limit 1000000 with penalty 1 = 1 + 0
c [transred-8] removed 0 transitive binary clauses
c [block-4] scheduling all variables this time
c [block-4] scheduled 3366 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 3366 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 44110371 steps
c [elim-5-1] backward subsumption/strengthening limit 44110300
c [elim-5-1-1] backward checking 324 touched variables 10%
c [elim-5-1-1] fully completed backward checking in 1 rounds
c [elim-5-1] subsumed 0 and strengthened 2 clauses in 214729 steps
c [elim-5-1] rescheduled 6 variables 0% by backward subsumption
c [elim-5-2] no variable eliminated in round 2 in 33131 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 3366 scheduled
c [elim-5] 2 < 1/100 * 3366 = 33 considered unsuccessful
c [bca-4] limit of 10000000 steps and 117438 added (scaled 2)
c [bca-4] 3 out of 6730 literals actually usable 0%
c [bca-4] not enough literals usable
c [bca-4] added 0 blocked clauses in 235815 steps
c [sort-queue-11] sorted 3364 enqueued variables after 2906526 conflicts
c [score-dist-11] active 0 (0%), one 3364 (100%), zero 0 (0%)
c [score-dist-11] max exp 1, different 1 (50%)
c [score-dist-11] median active exp 0, avg 0.0
c [simplification-11] removed 2 variables 0.1% (3364 remain 88%)
c [simplification-11] removed 11 irredundant clauses 0.0% (58469 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 4406526 (soft 3906526 + delta 500000)
c [simplification-11] new conflict limit 3906526 (hard 4406526)
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 -  510.6    3364    58469   2930770  188666   6615   195   33   413   23   8%   1024    3   39   33  118%
c -  525.8    3364    58469   3005752  190518   6616   195   34   403   23   9%   1024   -6   30   33   89%
c -  541.6    3364    58469   3082004  192955   6618   195   35   403   23   9%   1024   -9   30   33   89%
c -  557.5    3364    58469   3158870  195205   6622   195   34   412   38   8%   1024   -0   40   33  120%
c -  573.9    3364    58469   3236565  198947   6622   195   35   404   39   9%   1024   -6   34   34   99%
c -  589.8    3364    58469   3313711  201136   6624   195   32   386   24   8%   1024  -26   32   34   96%
c -  606.4    3364    58469   3391761  203519   6624   195   34   412   39   8%   1024    3   31   34   93%
c -  623.6    3364    58469   3470260  204827   6624   195   34   410   24   8%   1024   -1   40   34  117%
c -  640.8    3364    58469   3550708  207470   6625   195   33   421   25   8%   1024   12   28   34   82%
c -  658.5    3364    58469   3631510  210151   6626   195   34   407   25   8%   1024   -6   39   34  116%
c -  676.1    3364    58469   3712749  212986   6628   195   34   425   25   8%   1024   13   36   34  107%
c -  694.2    3364    58469   3794363  215950   6628   195   36   406   25   9%   1024   -5   38   35  108%
c -  712.5    3364    58469   3876042  217997   6629   195   36   403   26   9%   1024   -9   36   35  103%
c 
c [simplification-12] limit 3906526 conflicts (hard 4406526) hit after 3906526 conflicts
c [quatres-10] found 30684 quaternary clauses 13% in total
c [quatres-10-1] removed 118 duplicate quaternary clauses
c [quatres-10-1] added 1 double-self-subsuming ternary resolvents
c [quatres-10-2] added 21 single-self-subsuming ternary resolvents
c [quatres-10-2] added 45 quaternary resolvents
c [ternres-10] limit 200000000 with penalty 0 = 0 + 0
c [ternres-10] all 3364 free variables schedulable
c [ternres-10] 3 ternary resolvents (0 bin, 3 trn)
c [ternres-10] fully completed ternary resolution
c [gauss-4] limit 5922701 penalty 3 = 3 + 0
c [gauss-4] extracted 5323 xors of average arity 5.0
c [gauss-4] connected 26421 occurrences of 1031 variables (average 25.6)
c [gauss-4] limit 5922701 penalty 3 = 3 + 0
c [gauss-4] connected 5037 occurrences of 1031 variables (average 4.9)
c [gauss-4] fully completed
c [gauss-4] exported 0 unary, 0 binary and 0 ternary equations
c [basicprobe-3] limit 200000000 penalty 1 = 1 + 0
c [basicprobe-3-0] 523 sched 16%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-3-0] fully completed probing
c [sort-queue-12] sorted 3364 enqueued variables after 3906526 conflicts
c [score-dist-12] active 0 (0%), one 3364 (100%), zero 0 (0%)
c [score-dist-12] max exp 1, different 1 (50%)
c [score-dist-12] median active exp 0, avg 0.0
c [simplification-12] removed 0 variables 0.0% (3364 remain 88%)
c [simplification-12] removed 0 irredundant clauses 0.0% (58469 remain 77%)
c [simplification-12] maximum reduction of 0% = max (0%, 0%)
c [simplification-12] full geometric conflict interval increment 1000000
c [simplification-12] new conflict interval 2000000
c [simplification-12] penalized conflict interval 2000000 = 1 * 2000000
c [simplification-12] hard conflict limit 6906526 (soft 5906526 + delta 1000000)
c [simplification-12] new conflict limit 5906526 (hard 6906526)
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 -  731.4    3364    58469   3958509  220205   6654   195   36   439   26   8%   1024   25   43   35  123%
c -  750.0    3364    58469   4041564  222384   6655   195   35   379   26   9%   1024  -37   42   35  121%
c -  768.9    3364    58469   4125463  225055   6657   195   36   419   26   9%   1024    1   33   36   91%
c -  787.8    3364    58469   4209616  226937   6657   195   36   414   43   9%   1024   -0   41   36  114%
c -  807.0    3364    58469   4294927  229273   6660   195   35   427   27   8%   1024   11   29   35   83%
c -  827.0    3364    58469   4380902  230499   6660   195   36   420   27   9%   1024    2   35   35  100%
c -  847.3    3364    58469   4468815  233451   6660   195   32   421   27   8%   1024    6   32   35   91%
c -  867.7    3364    58469   4556629  235702   6661   195   35   415   27   8%   1024   -1   33   35   96%
c -  888.6    3364    58469   4645206  238256   6661   195   35   423   28   8%   1024    9   39   35  110%
c -  909.8    3364    58469   4734113  239980   6661   195   34   422   28   8%   1024    5   32   36   89%
c -  931.4    3364    58469   4824484  241949   6661   195   34   417   28   8%   1024    1   35   35  102%
c -  953.4    3364    58469   4915841  244664   6662   195   34   417   28   8%   1024    1   35   35  100%
c -  975.9    3364    58469   5007386  246742   6665   195   36   408   28   9%   1024   -6   34   35   95%
c -  998.4    3364    58469   5099877  249592   6665   195   36   415   29   9%   1024   -0   33   35   94%
c
c CAUGHT SIGNAL 15 SIGTERM
c
c s UNKNOWN
c bate: 10 basic ate = 10 trn 100% + 0 lrg 0% in 1 updates
c bcas: 4 count, 0 added (0 skipped), 370300 steps
c bkwd: tried 5722 clauses, 11384 lits, 1.99 lits/clause
c bkwd: checked 569242 occs, 99.48 occs/clause, 50.00 occs/lit
c bkwd: subsumed 0 binary, 1 ternary, 21 large
c bkwd: strengthened 0 binary, 3 ternary (100% self), 55 large (0% self)
c blkd: 4 bces, 202 removed, 3002822 resolutions, 6233745 steps
c blkd: 31 blocking literals 0%, 0 pure
c bump: 5066459 bumped seen, 410617341 lits 81.0 on average
c card: 4 count, 0 units, 0 am1, 9598772 steps
c card: 0 rescheduled, 0 eliminated, 0 resolved, 1496 subsumed
c card: 8 at-most-one constraints found, average size 3.00
c card: 8 at-most-one constraints used 100%, average size 3.00
c card: 54 at-most-two constraints found, average size 4.02
c card: 52 at-most-two constraints used 96%, average size 4.02
c cces: 5 cces, 8548 eliminated, 8548 ate 100%, 0 abce 0%
c cces: 0 probed, 0 lifted, 0 failed
c cces: 0 cached, 0 rsz, 0 cols 0%, 0 srch, 0 hits 0%
c clls: 1 sat, 0 simp, 0 freeze, 0 melt
c clls: 1006271 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 47 gcs, 0 rescored clauses, 0 rescored vars
c dcps: 32 decompositions, 235 equivalent 5%
c deco: 1252 decision-only clauses 0%, 43% reduction
c decs: 38832569 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 5 elims, 128 eliminated 3%, 0 pure 0%
c elms: 9 rounds, 1.8 rounds/bve
c elms: 128 small 100%, 0 large 0%
c elms: 1379 tried small, 128 succeeded 9%, 1251 failed 91%
c elms: 2105 subsumed, 3037 strengthened, 0 blocked
c elms: 1135612 copies, 2787750 resolutions, 403366 ipos
c elms: 212650 subchks, 143343 strchks
c gaus: 4 extractions, 11735 extracted, 4.6 size, 7 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 2 gc, 19851080 steps, 9925540 extr 50%, 466670 elim 2%
c glue: 30.1 orig avg, 30.1 real avg, 4.6 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 113 = 32 simple 28% + 72 trn 64% + 9 lrg 8%, 34 sub 30%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 5066459 clauses, 59.6 length
c lrnd: 302020637 lits = 317768923 orig - 15748286 removed 5%
c lrnd: 2426268 uips 48%, 2071167 flips 41%
c mins: 4672708 mins 92%, 40 bin 0%, 384984 size 8%
c mins: 237206947 poisoned searches, 19414500 hits, 8% hit rate
c mins: 489655282 used twice searches, 98612884 hits, 20% hit rate
c move: moved 1346, 5 bin 0%, 1341 trn 100%
c otfs: 44219 driving 51%, 43076 restarting 49%
c otfs: str 87295, 85565 red 98%, 1730 irr 2%
c otfs: str 87295, 0 bin 0%, 90 trn 0%, 87205 lrg 100%
c otfs: sub 493, 491 red 100%, 2 irr 0%
c otfs: sub 493, 0 bin 0%, 17 trn 3%, 476 lrg 97%
c phas: 1 computed, 3406 set, 1460 pos (43%), 1946 neg (57%)
c prbs: 3 basic, 5089 probed, 1 failed, 0 lifted
c prbs: 3 simple, 16067 probed, 56 failed, 119 eqs
c prbs: 3 treelook, 5634 probed, 0 failed, 0 lifted
c prom: 668121 locked 18% out of 3635914 tried
c prps: 556169484 props, 14 props/dec
c prps: 100% srch, 0% simp, 0% lkhd
c quat: 10 count, 1966 quat, 2230 self1, 260 self2, 510 dup
c queu: 12 sorted, 38832569 next (179 steps 0.00)
c queu: 410662083 enq (410662064 steps 1.00), 410617341 deq 100%
c redc: 1033 clauses 0%, 623961 tried 12%, 2 sat 0%
c redc: 1052 lits 0%, 5191342 tried 2%, 2 sat 0%
c redc: 52 times jump level reduced, 15.4 levels on average
c reds: 72 count, 70930.9 conflicts per reduce
c reds: 0 memlim 0%, 72 arith 100%
c reds: 3028464 collected 63%, 1749874 retired 37%
c rmbd: 28 removed, 14 red 50%
c rsts: 36207 restarts 100%, 0 skipped 0%
c rsts: 0 saturating 0%, 0 reuse 0%
c rsts: 0 kept 0.0% average 0.0%
c scnc: 0 count, 1.000 min (0/1000), 1.000 max (0/1000)
c simp: 12 count, 12 confs 100%, 0 vars 0%
c simp: 0 its 0%, 0 bin 0%, 0 trns 0%
c subl: 5066459 count (8002594 tried 1.6), 26270 sub out of 5064498 (0.5%)
c swps: 5 count, 12 rounds, 3640 queries (303.3/round)
c swps: 3645 sat calls, 12 unsat (1.0% success rate)
c swps: 102937 decisions 28.2, 3650 conflicts 1.0
c swps; 160.0 avg class size, 51.8 avg environment size
c swps: 0 failed, 6 impls, 6 equivs
c swp0: 1209 type 0 queries, 28 unsat (2.3%), 1209 sat (100.0%)
c swp1: 2431 type 1 queries, 156 unsat (6.4%), 2425 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: 87798317 calls to obtain time
c tops: 561 fixed 13%, 0 its, 0.00 confs/it
c trds: 8 transitive reductions, 54 removed, 1 failed
c trds: 53612 nodes, 3475 edges, 5014 steps
c trim: 222950 words, 0.9 MB
c trnr: 10 count, 66 bin, 618 trn, 16698938 steps
c unhd: 4 count, 6 rounds, 3578753 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: 1041 tauts, 0 bin 0%, 756 trn 73%, 284 lrg 27%
c unhd: 1041 tauts, 1 stamp 0%, 601 red 58%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 12415 str, 0 bin 0%, 62 trn 0%, 12353 lrg 100%, 12287 red 99%
c vars: 3364 remaining 78% and 924 removed 22% out of 4288
c vars: 561 fixed 13%, 128 eliminated 3%, 235 equivalent 5%
c vsts: 33925497829 visits, 100% srch, 0% simp, 0% lkhd
c vsts: 61.0 search visits per propagation, 6641.8 per conflict
c wchs: 11178848733 pushed, 15897027 enlarged, 1195 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all        5066464       3028464       1749874     223578407      43229870       2568821
c 
c  0 0        223957   4       423   0         0   0 187033859  84< 32987284  76   1974381  77     7.1
c  1 5        263646   5    125739   4    119752   7  19535109   9   3816691   9<   248267  10<    0.7
c  2 6        862400  17    463313  15    383010  22   8904401   4   2329501   5    143218   6     1.1
c  3 9        858147  17    498811  16    351269  20   2895435   1   1167231   3     56720   2     1.1
c  4 14       672215  13    429883  14    237460  14<  1655246   1    822056   2     36951   1     1.4
c  5 21       544599  11<   363456  12<   177304  10   1095676   0    601489   1     27255   1     1.7
c  6 30       423752   8    289876  10    130936   7    730967   0    426191   1     19882   1     2.1
c  7 41       337188   7    235505   8     99458   6    518511   0    315759   1     15643   1     2.5
c  8 54       269706   5    192258   6     75576   4    385763   0    242506   1     12832   0     2.9
c  9 69       212720   4    153461   5     57526   3    292612   0    187351   0     10525   0     3.1
c 10 86       277403   5    197946   7     76523   4    371371   0    238288   1     15331   1     6.3
c 11 126      115460   2     74815   2     39170   2    152279   0     90762   0      7212   0     4.4
c 12 230        5269   0      2977   0      1889   0      7176   0      4760   0       604   0     0.4
c 13 534           2   0         1   0         1   0         2   0         1   0         0   0     0.0
c 
c avg                  4.6           5.0           4.3           0.3           0.7           0.6
c std                  2.8           2.7           2.6           1.1           1.7           1.7
c 
c   35.498   4% bump
c   27.557   3% decide
c    3.015   0% cce
c 
c    4.159 < 1% rest (below)
c 
c    2.105   0% elim
c    0.918   0% sweep
c    0.892   0% quatres
c    0.690   0% probe
c    0.538   0% block
c    0.421   0% unhide
c    0.362   0% gauss
c    0.147   0% card
c    0.095   0% ternres
c    0.083   0% bca
c    0.012   0% transred
c    0.000   0% locs
c    0.000   0% queuesort
c    0.000   0% rescore
c ==================================
c    0.420   0% preprocessing     4%
c   10.047   1% inprocessing     96%
c ==================================
c   10.466   1% simplifying
c  989.506  99% search
c ==================================
c  999.973 100% all
c 
c       5107028 conflicts,        5107.2 confs/sec
c          1611 ternaries,        3170.1 confs/ternary
c            55 binaries,        92855.1 confs/binary
c             0 iterations,          0.0 confs/iteration
c 
c            72 reductions,          0.1 redus/sec,  70930.9 confs/reduction
c         36207 restarts,           36.2 rests/sec,    141.1 confs/restart
c      38832569 decisions,       38833.6 decis/sec,      7.6 decis/conflict
c     556169484 propagations,   556184.6 props/sec,     14.3 props/decision
c 
c 1000.0 seconds, 110.5 MB
c
c CAUGHT SIGNAL 15 SIGTERM
c
c launch: done
