c launch: /data/cnf/sc2014/app/006-22-144.cnf.bz2
c host: atom30
c Lingeling SAT Solver
c 
c Version b7ztzvv 37b745a123cb37a24a48e992b1e2073d5d4068bb
c 
c Copyright (C) 2010-2014 Armin Biere JKU Linz Austria.
c All rights reserved.
c 
c released Sat May  2 12:17:55 CEST 2015
c compiled Sat May  2 12:17:55 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 fmvx1 3.13.0-51-generic x86_64
c 
c piping '/data/cnf/sc2014/app/006-22-144.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/006-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 --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 --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 
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 784 variables
c [simpleprobe-1] all 3344 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 158 variables
c [simpleprobe-1] fully completed simple probing
c [simpleprobe-1] removed 158 variables, found 16 hbrs, 40 units
c [unhide-1] limit 100000 with penalty 0 = 0 + 0
c [unhide-1-1] 0 units, 0 failed, 680 tauts, 0 hbrs, 27 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 3186 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 74 variables 2% in round 1 in 2573715 steps
c [elim-1-1] backward subsumption/strengthening limit 2573700
c [elim-1-1-1] backward checking 1314 touched variables 41%
c [elim-1-1-1] fully completed backward checking in 1 rounds
c [elim-1-1] subsumed 8 and strengthened 63 clauses in 757527 steps
c [elim-1-1] rescheduled 132 variables 4% by backward subsumption
c [elim-1-2] eliminated 2 variables 0% in round 2 in 103987 steps
c [elim-1-2] backward subsumption/strengthening limit 103900
c [elim-1-2-1] backward checking 26 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 95230 steps
c [elim-1] fully completed in 2 rounds
c [elim-1] transition to [ all 0 rem 0 ] state
c [elim-1] eliminated 77 = 2% variables out of 3186 scheduled
c [phase-count-1] 57576 negative 99.0% of 58144 except 568 1.0%
c [phase-count-1] 57371 positive 98.7% of 58144 except 773 1.3%
c [phase-1] phase bias: 1328 positive 43%, 1781 negative 57%
c [sort-queue-1] sorted 3109 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 3109 (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 432 variables 12.2% (3109 remain 86%)
c [simplification-1] removed 14115 irredundant clauses 19.5% (58144 remain 80%)
c [simplification-1] maximum reduction of 20% = max (12%, 20%)
c [simplification-1] large reduction 20% >= 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 3108 free variables schedulable
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [decomp-4] removed 1 variables
c [simpleprobe-2] 1377 variables remain 44% (1730 retained 56%)
c [simpleprobe-2] removed 1 variables, found 2 hbrs, 0 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 6214 literals 100%
c [treelook-1] scheduling used 252466 steps
c [treelook-1] scheduled completely
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 300299 steps
c [treelook-1] 4917 literals remain 79%
c [treelook-1] 3069 variables remain to probed next time 99%
c [treelook-1] removed 1 variables, found 13 hbrs
c [basicprobe-1] limit 1000000 penalty 0 = 0 + 0
c [basicprobe-1-0] 350 sched 11%, 2 failed, 1 lifted, 9 hbrs
c [decomp-6] removed 2 variables
c [basicprobe-1-1] 349 sched 11%, 0 failed, 0 lifted, 2 hbrs
c [basicprobe-1-2] 351 sched 11%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-1-2] fully completed probing
c [basicprobe-1-2] 3 units = 2 failed (67%) + 1 lifted (33%)
c [basicprobe-1-2] removed 2 variables, found 11 hbrs
c [block-1] scheduling all variables this time
c [block-1] scheduled 3104 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 106 blocked clauses
c [block-1] 106 < 1/100 * 58100 = 581 considered unsuccessful
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 2862 clauses out of 17035 (17%) of length 7
c [cce-1-1] eliminated 366 clauses out of 17038 (2%) of length 6
c [cce-1-1] eliminated 2206 clauses out of 12631 (17%) of length 5
c [cce-1-1] eliminated 536 clauses out of 6407 (8%) of length 4
c [cce-1-1] completed large round (ATE)
c [cce-1-1] eliminated 5970 large clauses in 26412493 steps
c [cce-1-1] allowing another 13206246 steps for small clauses
c [cce-1-1] scheduling 4335 clauses = 225 binary + 4110 ternary
c [cce-1-1] tried to eliminate 4335 small clauses 100%
c [cce-1-1] eliminated 6 binary clauses 3%
c [cce-1-1] eliminated 1013 ternary clauses 25%
c [cce-1-1] eliminated 1019 small clauses 24%
c [cce-1-1] eliminated 1019 small clauses in 14278002 steps
c [cce-1-1] completed small round (ATE)
c [cce-1-1] completed small and large (ATE)
c [cce-1-1] eliminated 6989 covered clauses in round 1
c [cce-1-2] eliminated 40 clauses out of 14173 (0%) of length 7
c [cce-1-2] incomplete large round (ABCE)
c [cce-1-2] eliminated 40 large clauses in 15722032 steps
c [cce-1-2] allowing another 7861016 steps for small clauses
c [cce-1-2] scheduling 3316 clauses = 219 binary + 3097 ternary
c [cce-1-2] tried to eliminate 3316 small clauses 100%
c [cce-1-2] completed small round (ABCE)
c [cce-1-2] eliminated 40 covered clauses in round 2
c [cce-1-3] incomplete large round (ABCE)
c [cce-1-3] allowing another 3522425 steps for small clauses
c [cce-1-3] scheduling 3316 clauses = 219 binary + 3097 ternary
c [cce-1-3] tried to eliminate 3316 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 7029 covered clauses in TOTAL during 3 rounds
c [elim-2] scheduling all variables this time
c [elim-2] scheduled 3104 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 413 not tried 13% in round 1
c [elim-2] transition to [ all 1 rem 1 ] state
c [elim-2] eliminated 14 = 0% variables out of 3104 scheduled
c [elim-2] 14 < 1/100 * 3104 = 31 considered unsuccessful
c [bca-1] limit of 10000000 steps and 101880 added (scaled 2)
c [bca-1] 4339 out of 6182 literals actually usable 70%
c [bca-1] added 0 blocked clauses in 27564 steps
c [sweep-1] limit 1000000 penalty 0 = 0 + 0
c [sweep-1-1] 1436 pos 46.5% + 1654 neg 53.5% = 3090 sched 100.0% ret 0
c [sweep-1-1] 433427 steps 520 queries 176.15 avg class size
c [sweep-1-1] 8129 decisions 516 SAT calls 21.46 avg env size
c [sweep-1-1] fully completed sweeping round
c [decomp-8] removed 6 variables
c [sweep-1-1] removed 6 vars (0 failed, 6 eqs, 8 impls)
c [sweep-1-2] 1433 pos 46.5% + 1651 neg 53.5% = 3084 sched 100.0% ret 0
c [sweep-1-2] 409915 steps 517 queries 143.42 avg class size
c [sweep-1-2] 7804 decisions 516 SAT calls 21.79 avg env size
c [sweep-1-2] fully completed sweeping round
c [decomp-9] removed 1 variables
c [sweep-1-2] removed 1 vars (0 failed, 1 eqs, 2 impls)
c [sweep-1-3] 1432 pos 46.4% + 1651 neg 53.6% = 3083 sched 100.0% ret 0
c [sweep-1-3] 156827 steps 168 queries 387.52 avg class size
c [sweep-1-3] 2829 decisions 168 SAT calls 23.31 avg env size
c [sweep-1-3] 2041 variables remain 66% (1042 retained 34%)
c [decomp-10] removed 1 variables
c [sweep-1-3] removed 1 vars (0 failed, 0 eqs, 2 impls)
c [sweep-1] removed 8 vars in TOTAL (3 rounds, 1202 queries)
c [sort-queue-2] sorted 3082 enqueued variables after 1000 conflicts
c [score-dist-2] active 0 (0%), one 2739 (89%), zero 343 (11%)
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 27 variables 0.9% (3082 remain 85%)
c [simplification-2] removed 7470 irredundant clauses 12.8% (50672 remain 70%)
c [simplification-2] maximum reduction of 13% = max (1%, 13%)
c [simplification-2] large reduction 13% >= 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  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    2.0    3081    50672      1846    2553   1229    63    2    88    4   2%     15   87    6    0 4228%
c 
c [simplification-3] limit 3000 conflicts (hard 13000) hit after 3000 conflicts
c [quatres-1] found 6574 quaternary clauses 14% in total
c [quatres-1-1] added 19 double-self-subsuming ternary resolvents
c [quatres-1-2] added 114 single-self-subsuming ternary resolvents
c [quatres-1-2] added 424 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 3081 free variables schedulable
c [ternres-1] 241 ternary resolvents (15 bin, 226 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 3340 xors of average arity 5.0
c [gauss-1] connected 16586 occurrences of 773 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-11] removed 3 variables
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] scheduled 6097 literals 99%
c [treelook-2] scheduling used 239185 steps
c [treelook-2] scheduled completely
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] used 300094 steps
c [treelook-2] 4674 literals remain 76%
c [treelook-2] 2988 variables remain to probed next time 97%
c [treelook-2] removed 0 variables, found 24 hbrs
c [unhide-2] limit 50000 with penalty 1 = 1 + 0
c [unhide-2-2] 0 units, 0 failed, 91 tauts, 0 hbrs, 157 literals
c [transred-1] limit 100000 with penalty 0 = 0 + 0
c [transred-1] removed 11 transitive binary clauses
c [cce-2] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-2-1] eliminated 183 clauses out of 17017 (1%) of length 6
c [cce-2-1] eliminated 33 clauses out of 10574 (0%) of length 5
c [cce-2-1] eliminated 55 clauses out of 5902 (1%) of length 4
c [cce-2-1] completed large round (ATE)
c [cce-2-1] eliminated 271 large clauses in 23304966 steps
c [cce-2-1] allowing another 11652483 steps for small clauses
c [cce-2-1] scheduling 826 clauses = 240 binary + 586 ternary
c [cce-2-1] tried to eliminate 826 small clauses 100%
c [cce-2-1] eliminated 2 binary clauses 1%
c [cce-2-1] eliminated 60 ternary clauses 10%
c [cce-2-1] eliminated 62 small clauses 8%
c [cce-2-1] eliminated 62 small clauses in 11801608 steps
c [cce-2-1] completed small round (ATE)
c [cce-2-1] eliminated 333 covered clauses in round 1
c [cce-2-2] incomplete large round (ATE)
c [cce-2-2] allowing another 9099205 steps for small clauses
c [cce-2-2] scheduling 764 clauses = 238 binary + 526 ternary
c [cce-2-2] tried to eliminate 764 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 333 covered clauses in TOTAL during 2 rounds
c [cce-2] 333 < 1/100 * 50639 = 506 considered unsuccessful
c [sweep-2] limit 1000000 penalty 0 = 0 + 0
c [sweep-2-1] 986 pos 48.4% + 1053 neg 51.6% = 2039 sched 66.2% ret 1039
c [sweep-2-1] 343830 steps 455 queries 104.99 avg class size
c [sweep-2-1] 7014 decisions 456 SAT calls 22.06 avg env size
c [sweep-2-1] fully completed sweeping round
c [sweep-2-1] removed 0 vars (0 failed, 0 eqs, 3 impls)
c [sweep-2-2] 1506 pos 48.9% + 1572 neg 51.1% = 3078 sched 100.0% ret 0
c [sweep-2-2] 440000 steps 507 queries 148.41 avg class size
c [sweep-2-2] 8815 decisions 508 SAT calls 24.02 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] 1506 pos 48.9% + 1572 neg 51.1% = 3078 sched 100.0% ret 0
c [sweep-2-3] 217521 steps 216 queries 290.50 avg class size
c [sweep-2-3] 3929 decisions 216 SAT calls 25.95 avg env size
c [sweep-2-3] 1581 variables remain 51% (1497 retained 49%)
c [decomp-15] removed 1 variables
c [sweep-2-3] removed 1 vars (0 failed, 0 eqs, 1 impls)
c [sweep-2] 1 < 1/1000 * 3078 = 3 considered unsuccessful
c [sweep-2] removed 1 vars in TOTAL (3 rounds, 1175 queries)
c [sort-queue-3] sorted 3077 enqueued variables after 3000 conflicts
c [score-dist-3] active 0 (0%), one 2958 (96%), zero 119 (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 4 variables 0.1% (3077 remain 85%)
c [simplification-3] removed 369 irredundant clauses 0.7% (50303 remain 70%)
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 7804 quaternary clauses 15% in total
c [quatres-2-1] removed 1 duplicate quaternary clauses
c [quatres-2-1] added 41 double-self-subsuming ternary resolvents
c [quatres-2-2] added 307 single-self-subsuming ternary resolvents
c [quatres-2-2] added 482 quaternary resolvents
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] all 3077 free variables schedulable
c [ternres-2] 175 ternary resolvents (27 bin, 148 trn)
c [ternres-2] fully completed ternary resolution
c [decomp-16] removed 1 variables
c [basicprobe-2] limit 1305092 penalty 0 = 0 + 0
c [basicprobe-2-0] 509 sched 17%, 3 failed, 0 lifted, 13 hbrs
c [decomp-17] removed 3 variables
c [basicprobe-2-1] 511 sched 17%, 0 failed, 0 lifted, 6 hbrs
c [basicprobe-2-2] 512 sched 17%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-2-2] fully completed probing
c [basicprobe-2-2] 3 units = 3 failed (100%) + 0 lifted (0%)
c [basicprobe-2-2] removed 3 variables, found 19 hbrs
c [bate-1] eliminated 44 asymmetric tautologies during probing
c [transred-2] limit 261018 with penalty 0 = 0 + 0
c [transred-2] removed 11 transitive binary clauses
c [block-2] scheduling all variables this time
c [block-2] scheduled 3073 variables 100%
c [block-2] limit of 25000000 steps penalty 1 = 1 + 0
c [block-2] fully completed
c [block-2] transition to [ all 0 rem 0 ] state
c [block-2] eliminated 0 blocked clauses
c [elim-3] 413 variables 13% will be scheduled this time
c [elim-3] scheduled 413 variables 13%
c [elim-3] limit of 10000000 steps penalty 1 = 1 + 0
c [elim-3] rescheduling of touched variables disabled
c [elim-3] incomplete 130 not tried 4% in round 1
c [elim-3] transition to [ all 0 rem 1 ] state
c [elim-3] eliminated 0 = 0% variables out of 413 scheduled
c [bca-2] limit of 10000000 steps and 100918 added (scaled 2)
c [bca-2] 665 out of 6148 literals actually usable 11%
c [bca-2] added 0 blocked clauses in 17613 steps
c [sort-queue-4] sorted 3073 enqueued variables after 13000 conflicts
c [score-dist-4] active 0 (0%), one 2987 (97%), zero 86 (3%)
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 4 variables 0.1% (3073 remain 85%)
c [simplification-4] removed 94 irredundant clauses 0.2% (50209 remain 69%)
c [simplification-4] maximum reduction of 0% = max (0%, 0%)
c [simplification-4] full geometric conflict interval increment 20000
c [simplification-4] new conflict interval 30000
c [simplification-4] penalized conflict interval 30000 = 1 * 30000
c [simplification-4] hard conflict limit 58000 (soft 43000 + delta 15000)
c [simplification-4] new conflict limit 43000 (hard 58000)
c 
c [simplification-5] limit 43000 conflicts (hard 58000) hit after 43000 conflicts
c [quatres-3] found 10108 quaternary clauses 17% in total
c [quatres-3-1] removed 1 duplicate quaternary clauses
c [quatres-3-1] added 48 double-self-subsuming ternary resolvents
c [quatres-3-2] added 404 single-self-subsuming ternary resolvents
c [quatres-3-2] added 418 quaternary resolvents
c [ternres-3] limit 4000000 with penalty 0 = 0 + 0
c [ternres-3] all 3073 free variables schedulable
c [ternres-3] 131 ternary resolvents (11 bin, 120 trn)
c [ternres-3] fully completed ternary resolution
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] extracted 1012 xors of average arity 4.7
c [gauss-2] connected 4772 occurrences of 306 variables (average 15.6)
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 [simpleprobe-3] 1365 schedulable variables 44%
c [simpleprobe-3] limit 4871012 penalty 0 = 0 + 0
c [simpleprobe-3] 515 variables remain 17% (2558 retained 83%)
c [simpleprobe-3] removed 0 variables, found 17 hbrs, 0 units
c [transred-3] limit 1217753 with penalty 0 = 0 + 0
c [transred-3] removed 11 transitive binary clauses
c [cce-3] limit of 15000000 steps penalty 1 = 1 + 0
c [cce-3-1] eliminated 4 clauses out of 17098 (0%) of length 6
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 4 large clauses in 15000006 steps
c [cce-3-1] allowing another 7500003 steps for small clauses
c [cce-3-1] scheduling 884 clauses = 280 binary + 604 ternary
c [cce-3-1] tried to eliminate 884 small clauses 100%
c [cce-3-1] eliminated 1 binary clauses 0%
c [cce-3-1] eliminated 11 ternary clauses 2%
c [cce-3-1] eliminated 12 small clauses 1%
c [cce-3-1] eliminated 12 small clauses in 7705390 steps
c [cce-3-1] completed small round (ACCE)
c [cce-3-1] eliminated 16 covered clauses in round 1
c [cce-3-2] incomplete large round (ACCE)
c [cce-3-2] allowing another 3647328 steps for small clauses
c [cce-3-2] scheduling 872 clauses = 279 binary + 593 ternary
c [cce-3-2] tried to eliminate 872 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 16 covered clauses in TOTAL during 2 rounds
c [cce-3] 16 < 1/100 * 50209 = 502 considered unsuccessful
c [sweep-3] limit 500000 penalty 1 = 1 + 0
c [sweep-3-1] 777 pos 49.2% + 803 neg 50.8% = 1580 sched 51.4% ret 1493
c [sweep-3-1] 501052 steps 134 queries 110.57 avg class size
c [sweep-3-1] 8240 decisions 133 SAT calls 106.92 avg env size
c [sweep-3-1] 369 variables remain 12% (2704 retained 88%)
c [sweep-3-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-3] removed 0 vars in TOTAL (1 rounds, 133 queries)
c [sort-queue-5] sorted 3073 enqueued variables after 43000 conflicts
c [score-dist-5] active 0 (0%), one 3022 (98%), zero 51 (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% (3073 remain 85%)
c [simplification-5] removed 16 irredundant clauses 0.0% (50193 remain 69%)
c [simplification-5] maximum reduction of 0% = max (0%, 0%)
c [simplification-5] full geometric conflict interval increment 30000
c [simplification-5] new conflict interval 60000
c [simplification-5] penalized conflict interval 60000 = 1 * 60000
c [simplification-5] hard conflict limit 133000 (soft 103000 + delta 30000)
c [simplification-5] new conflict limit 103000 (hard 133000)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c -   14.5    3073    50193     76136   29171   3996   238   12   279   14   4%    689  107   12    7  174%
c 
c [simplification-6] limit 103000 conflicts (hard 133000) hit after 103000 conflicts
c [quatres-4] found 13228 quaternary clauses 19% in total
c [quatres-4-1] removed 3 duplicate quaternary clauses
c [quatres-4-1] added 48 double-self-subsuming ternary resolvents
c [quatres-4-2] added 496 single-self-subsuming ternary resolvents
c [quatres-4-2] added 491 quaternary resolvents
c [ternres-4] limit 4088258 with penalty 0 = 0 + 0
c [ternres-4] all 3073 free variables schedulable
c [ternres-4] 131 ternary resolvents (9 bin, 122 trn)
c [ternres-4] fully completed ternary resolution
c [card-3] limit 511032 penalty 2 = 2 + 0
c [card-3] found 3 at-most-one constraints of average size 3.0
c [card-3] found 25 at-most-two constraints of average size 4.1
c [card-3] using previous limit 511032 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 [unhide-3] limit 204412 with penalty 2 = 2 + 0
c [unhide-3-3] 0 units, 1 failed, 162 tauts, 0 hbrs, 1612 literals
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 19 transitive binary clauses
c [sort-queue-6] sorted 3072 enqueued variables after 103000 conflicts
c [score-dist-6] active 0 (0%), one 3072 (100%), zero 0 (0%)
c [score-dist-6] max exp 1, different 1 (50%)
c [score-dist-6] median active exp 0, avg 0.0
c [simplification-6] removed 1 variables 0.0% (3072 remain 85%)
c [simplification-6] removed 30 irredundant clauses 0.1% (50163 remain 69%)
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 283000 (soft 223000 + delta 60000)
c [simplification-6] new conflict limit 223000 (hard 283000)
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 -   24.7    3072    50163    130732   37025   5014   263   14   290   15   5%    878   56   13   10  127%
c -   35.3    3072    50163    184445   45453   5313   268   15   288   16   5%    960   27   15   13  116%
c 
c [simplification-7] limit 223000 conflicts (hard 283000) hit after 223001 conflicts
c [quatres-5] found 17053 quaternary clauses 20% in total
c [quatres-5-1] removed 7 duplicate quaternary clauses
c [quatres-5-1] added 36 double-self-subsuming ternary resolvents
c [quatres-5-2] added 488 single-self-subsuming ternary resolvents
c [quatres-5-2] added 388 quaternary resolvents
c [ternres-5] limit 10310167 with penalty 0 = 0 + 0
c [ternres-5] all 3072 free variables schedulable
c [ternres-5] 98 ternary resolvents (8 bin, 90 trn)
c [ternres-5] fully completed ternary resolution
c [treelook-3] limit 515508 penalty 1 = 1 + 0 boost 1
c [treelook-3] scheduled 5694 literals 93%
c [treelook-3] scheduling used 515581 steps
c [treelook-3] not fully scheduled
c [treelook-3] limit 515508 penalty 1 = 1 + 0 boost 1
c [treelook-3] used 515520 steps
c [treelook-3] 3430 literals remain 56%
c [treelook-3] 2266 variables remain to probed next time 74%
c [treelook-3] removed 0 variables, found 28 hbrs
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 3072 variables 100%
c [block-3] limit of 25775418 steps penalty 2 = 2 + 0
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 0 blocked clauses
c [elim-4] scheduling all variables this time
c [elim-4] scheduled 3072 variables 100%
c [elim-4] boosting limit by 20
c [elim-4] limit of 1031016740 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 35528603 steps
c [elim-4-1] backward subsumption/strengthening limit 35528600
c [elim-4-1-1] backward checking 793 touched variables 26%
c [elim-4-1-1] fully completed backward checking in 1 rounds
c [elim-4-1] subsumed 0 and strengthened 4 clauses in 411360 steps
c [elim-4-1] rescheduled 7 variables 0% by backward subsumption
c [elim-4-2] no variable eliminated in round 2 in 26265 steps
c [elim-4] fully completed in 2 rounds
c [elim-4] transition to [ all 0 rem 0 ] state
c [elim-4] eliminated 2 = 0% variables out of 3072 scheduled
c [elim-4] 2 < 1/100 * 3072 = 30 considered unsuccessful
c [bca-3] limit of 10000000 steps and 100512 added (scaled 2)
c [bca-3] 3 out of 6142 literals actually usable 0%
c [bca-3] not enough literals usable
c [bca-3] added 0 blocked clauses in 82032 steps
c [sort-queue-7] sorted 3070 enqueued variables after 223001 conflicts
c [score-dist-7] active 0 (0%), one 3070 (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% (3070 remain 85%)
c [simplification-7] removed 157 irredundant clauses 0.3% (50006 remain 69%)
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 583001 (soft 463001 + delta 120000)
c [simplification-7] new conflict limit 463001 (hard 583001)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c -   45.3    3070    50006    236383   46882   6095   300   17   302   17   5%    995   23   19   14  130%
c -   54.1    3070    50006    293995   55628   6212   301   18   289   10   6%   1012   -2   19   16  117%
c -   62.7    3070    50006    348594   61031   6302   302   19   315   18   6%   1019   13   21   17  120%
c -   71.1    3070    50006    402963   65704   6387   302   20   302   11   7%   1022   -8   22   19  116%
c -   79.4    3070    50006    457712   69747   6438   303   22   332   20   7%   1023   15   23   20  116%
c 
c [simplification-8] limit 463001 conflicts (hard 583001) hit after 463001 conflicts
c [quatres-6] found 21081 quaternary clauses 19% in total
c [quatres-6-1] removed 34 duplicate quaternary clauses
c [quatres-6-1] added 22 double-self-subsuming ternary resolvents
c [quatres-6-2] added 262 single-self-subsuming ternary resolvents
c [quatres-6-2] added 247 quaternary resolvents
c [ternres-6] limit 20858486 with penalty 0 = 0 + 0
c [ternres-6] all 3070 free variables schedulable
c [ternres-6] 42 ternary resolvents (3 bin, 39 trn)
c [ternres-6] fully completed ternary resolution
c [gauss-3] limit 1042924 penalty 2 = 2 + 0
c [gauss-3] extracted 140 xors of average arity 3.0
c [gauss-3] connected 420 occurrences of 39 variables (average 10.8)
c [gauss-3] limit 1042924 penalty 2 = 2 + 0
c [gauss-3] fully completed
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [basicprobe-3] limit 104292434 penalty 0 = 0 + 0
c [basicprobe-3-0] 627 sched 20%, 0 failed, 0 lifted, 1 hbrs
c [basicprobe-3-1] 627 sched 20%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-3-1] fully completed probing
c [basicprobe-3-1] removed 0 variables, found 1 hbrs
c [bate-2] eliminated 2 asymmetric tautologies during probing
c [unhide-4] limit 2085848 with penalty 1 = 1 + 0
c [unhide-4-8] 0 units, 0 failed, 390 tauts, 0 hbrs, 1704 literals
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 1 transitive binary clauses
c [cce-4] boosting limit by 10
c [cce-4] limit of 260731085 steps penalty 2 = 2 + 0
c [cce-4-1] eliminated 8 clauses out of 17345 (0%) of length 6
c [cce-4-1] eliminated 52 clauses out of 10580 (0%) of length 5
c [cce-4-1] eliminated 84 clauses out of 5588 (2%) of length 4
c [cce-4-1] completed large round (ATE)
c [cce-4-1] eliminated 144 large clauses in 22835301 steps
c [cce-4-1] allowing another 11417650 steps for small clauses
c [cce-4-1] scheduling 969 clauses = 297 binary + 672 ternary
c [cce-4-1] tried to eliminate 969 small clauses 100%
c [cce-4-1] eliminated 9 ternary clauses 1%
c [cce-4-1] eliminated 9 small clauses 1%
c [cce-4-1] eliminated 9 small clauses in 11611399 steps
c [cce-4-1] completed small round (ATE)
c [cce-4-1] eliminated 153 covered clauses in round 1
c [cce-4-2] completed large round (ATE)
c [cce-4-2] allowing another 11387741 steps for small clauses
c [cce-4-2] scheduling 960 clauses = 297 binary + 663 ternary
c [cce-4-2] tried to eliminate 960 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 153 covered clauses in TOTAL during 2 rounds
c [cce-4] 153 < 1/100 * 50004 = 500 considered unsuccessful
c [sweep-4] limit 1564386 penalty 2 = 2 + 0
c [sweep-4-1] 192 pos 52.0% + 177 neg 48.0% = 369 sched 12.0% ret 2701
c [sweep-4-1] 310716 steps 101 queries 20.13 avg class size
c [sweep-4-1] 5040 decisions 100 SAT calls 91.68 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] 1558 pos 50.7% + 1512 neg 49.3% = 3070 sched 100.0% ret 0
c [sweep-4-2] 1059185 steps 250 queries 90.74 avg class size
c [sweep-4-2] 14160 decisions 249 SAT calls 108.94 avg env size
c [sweep-4-2] fully completed sweeping round
c [sweep-4-2] removed 0 vars (0 failed, 0 eqs, 1 impls)
c [sweep-4-3] 1558 pos 50.7% + 1512 neg 49.3% = 3070 sched 100.0% ret 0
c [sweep-4-3] 201627 steps 42 queries 485.31 avg class size
c [sweep-4-3] 2546 decisions 41 SAT calls 130.80 avg env size
c [sweep-4-3] 2320 variables remain 76% (750 retained 24%)
c [sweep-4-3] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-4] removed 0 vars in TOTAL (3 rounds, 390 queries)
c [sort-queue-8] sorted 3070 enqueued variables after 463001 conflicts
c [score-dist-8] active 0 (0%), one 3070 (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% (3070 remain 85%)
c [simplification-8] removed 155 irredundant clauses 0.3% (49851 remain 69%)
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 1183001 (soft 943001 + delta 240000)
c [simplification-8] new conflict limit 943001 (hard 1183001)
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.6    3070    49851    512949   73107   6446   299   22   337   20   7%   1024   14   23   21  110%
c -   97.0    3070    49851    569203   77129   6478   299   24   353   12   7%   1024   22   26   23  117%
c -  105.2    3070    49851    625837   81480   6503   299   25   343   13   7%   1024    2   27   24  113%
c -  113.7    3070    49851    682045   85843   6519   299   26   350   13   7%   1024    8   29   25  116%
c -  121.7    3070    49851    737595   89882   6534   299   27   362   22   7%   1024   16   30   26  116%
c -  129.8    3070    49851    792750   93855   6551   299   27   344   14   8%   1024   -1   26   26   99%
c -  137.9    3070    49851    847530   96935   6569   299   28   360   23   8%   1024    8   31   27  115%
c -  146.1    3070    49851    902634  100533   6585   299   28   363   14   8%   1024    8   27   28   95%
c 
c [simplification-9] limit 943001 conflicts (hard 1183001) hit after 943001 conflicts
c [quatres-7] found 23913 quaternary clauses 18% in total
c [quatres-7-1] removed 64 duplicate quaternary clauses
c [quatres-7-1] added 7 double-self-subsuming ternary resolvents
c [quatres-7-2] added 101 single-self-subsuming ternary resolvents
c [quatres-7-2] added 132 quaternary resolvents
c [ternres-7] limit 43292911 with penalty 0 = 0 + 0
c [ternres-7] all 3070 free variables schedulable
c [ternres-7] 34 ternary resolvents (1 bin, 33 trn)
c [ternres-7] fully completed ternary resolution
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 1 transitive binary clauses
c [sort-queue-9] sorted 3070 enqueued variables after 943001 conflicts
c [score-dist-9] active 0 (0%), one 3070 (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% (3070 remain 85%)
c [simplification-9] removed 0 irredundant clauses 0.0% (49851 remain 69%)
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 2383001 (soft 1903001 + delta 480000)
c [simplification-9] new conflict limit 1903001 (hard 2383001)
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 -  154.6    3070    49851    957582  103622   6730   299   29   346   23   8%   1024  -10   29   29  103%
c -  162.7    3070    49851   1012676  106694   6735   299   29   369   15   8%   1024   11   28   29   97%
c -  171.2    3070    49851   1067827  109569   6745   299   31   363   15   9%   1024    2   36   30  120%
c -  179.6    3070    49851   1123211  112939   6748   299   31   376   15   8%   1024   16   36   30  119%
c -  188.4    3070    49851   1178347  114589   6756   299   31   358   25   9%   1024   -2   36   31  118%
c -  197.3    3070    49851   1234995  117240   6760   299   31   357   16   9%   1024   -5   29   31   94%
c -  206.2    3070    49851   1292100  120672   6764   299   31   352   16   9%   1024  -10   26   31   82%
c -  215.2    3070    49851   1348625  123242   6773   299   32   373   16   9%   1024   11   34   32  107%
c -  224.3    3070    49851   1405540  125196   6777   299   33   364   27   9%   1024    2   36   32  113%
c -  233.7    3070    49851   1463580  128088   6782   299   32   368   17   9%   1024    6   36   32  110%
c -  243.2    3070    49851   1521631  129825   6790   299   33   355   17   9%   1024   -9   33   33  100%
c -  253.2    3070    49851   1580603  132237   6792   299   33   353   17   9%   1024  -13   34   33  102%
c -  263.1    3070    49851   1640278  134621   6795   299   33   357   17   9%   1024   -5   26   33   77%
c -  273.4    3070    49851   1700496  136957   6798   299   35   358   17  10%   1024   -6   35   33  106%
c -  283.7    3070    49851   1761221  139485   6803   299   33   368   18   9%   1024    2   27   34   81%
c -  294.3    3070    49851   1822191  141602   6811   299   34   362   18   9%   1024   -6   36   34  107%
c -  304.5    3070    49851   1883964  144910   6817   299   36   361   18  10%   1024   -3   40   34  115%
c 
c [simplification-10] limit 1903001 conflicts (hard 2383001) hit after 1903001 conflicts
c [quatres-8] found 26210 quaternary clauses 16% in total
c [quatres-8-1] removed 115 duplicate quaternary clauses
c [quatres-8-1] added 2 double-self-subsuming ternary resolvents
c [quatres-8-2] added 56 single-self-subsuming ternary resolvents
c [quatres-8-2] added 83 quaternary resolvents
c [ternres-8] limit 98668743 with penalty 0 = 0 + 0
c [ternres-8] all 3070 free variables schedulable
c [ternres-8] 9 ternary resolvents (0 bin, 9 trn)
c [ternres-8] fully completed ternary resolution
c [card-4] limit 6166796 penalty 3 = 3 + 0
c [card-4] found 2 at-most-one constraints of average size 3.0
c [card-4] found 21 at-most-two constraints of average size 4.0
c [card-4] using previous limit 6166796 for elimination
c [card-4] 22 out of 23 constraints (96%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [simpleprobe-4] 515 schedulable variables 17%
c [simpleprobe-4] limit 100000000 penalty 1 = 1 + 0
c [simpleprobe-4] fully completed simple probing
c [simpleprobe-4] removed 0 variables, found 26 hbrs, 0 units
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 24 transitive binary clauses
c [sort-queue-10] sorted 3070 enqueued variables after 1903001 conflicts
c [score-dist-10] active 0 (0%), one 3070 (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% (3070 remain 85%)
c [simplification-10] removed 0 irredundant clauses 0.0% (49851 remain 69%)
c [simplification-10] maximum reduction of 0% = max (0%, 0%)
c [simplification-10] full geometric conflict interval increment 960000
c [simplification-10] new conflict interval 1920000
c [simplification-10] penalized conflict interval 1920000 = 1 * 1920000
c [simplification-10] hard conflict limit 4783001 (soft 3823001 + delta 960000)
c [simplification-10] new conflict limit 3823001 (hard 4783001)
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 -  315.5    3070    49851   1944921  146121   6885   301   35   356   18  10%   1024  -14   40   35  115%
c -  326.2    3070    49851   2007521  148899   6889   301   38   373   19  10%   1024    2   39   36  109%
c -  337.0    3070    49851   2069944  150694   6893   301   37   372   30  10%   1024    2   29   36   81%
c -  348.0    3070    49851   2133203  153400   6896   301   38   358   31  11%   1024  -12   33   37   90%
c -  358.7    3070    49851   2196390  156062   6897   301   36   377   19  10%   1024    7   47   36  128%
c -  369.7    3070    49851   2259577  158238   6900   301   36   385   19   9%   1024   14   36   37   98%
c -  381.0    3070    49851   2323138  159798   6900   301   39   366   32  11%   1024   -7   41   38  108%
c -  392.4    3070    49851   2387776  162242   6900   301   38   377   20  10%   1024    4   44   38  117%
c -  403.7    3070    49851   2452478  163673   6904   301   37   382   20  10%   1024    7   43   37  116%
c -  415.6    3070    49851   2518308  164718   6904   301   38   370   20  10%   1024   -6   34   37   93%
c -  427.6    3070    49851   2585723  166860   6906   301   38   376   20  10%   1024   -1   41   37  109%
c -  439.9    3070    49851   2653643  168819   6908   301   39   376   21  10%   1024    3   39   38  105%
c -  452.7    3070    49851   2722163  171074   6909   301   39   377   21  10%   1024    4   38   38   99%
c -  465.3    3070    49851   2791261  173108   6910   301   37   344   21  11%   1024  -27   40   37  106%
c -  478.4    3070    49851   2860827  175094   6912   301   39   360   21  11%   1024  -12   34   38   90%
c -  491.4    3070    49851   2931042  176963   6913   301   38   365   21  10%   1024   -9   44   38  116%
c -  504.6    3070    49851   3001982  178838   6917   301   39   375   21  10%   1024    5   45   38  118%
c -  518.1    3070    49851   3073669  181247   6920   301   40   371   22  11%   1024   -0   40   38  104%
c -  531.9    3070    49851   3145559  183643   6921   301   38   390   22  10%   1024   18   39   38  102%
c -  545.8    3070    49851   3217728  184563   6923   301   38   382   22  10%   1024    7   36   38   95%
c -  560.0    3070    49851   3291460  187016   6925   301   42   367   22  11%   1024   -8   60   39  157%
c -  574.2    3070    49851   3365258  189985   6926   301   40   390   22  10%   1024   15   51   39  130%
c -  588.6    3070    49851   3438877  191156   6926   301   39   383   23  10%   1024    8   32   39   81%
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 -  603.4    3070    49851   3513692  193334   6928   301   41   369   23  11%   1024   -2   46   39  119%
c -  618.0    3070    49851   3589048  195999   6929   301   38   375   23  10%   1024    1   41   39  105%
c -  632.6    3070    49851   3664145  197278   6930   301   37   398   23   9%   1024   21   33   39   86%
c -  647.9    3070    49851   3740536  199659   6934   301   38   361   23  11%   1024  -13   40   39  103%
c -  663.2    3070    49851   3816901  201696   6934   301   37   362   24  10%   1024  -13   46   39  115%
c 
c [simplification-11] limit 3823001 conflicts (hard 4783001) hit after 3823002 conflicts
c [quatres-9] found 27991 quaternary clauses 13% in total
c [quatres-9-1] removed 176 duplicate quaternary clauses
c [quatres-9-1] added 3 double-self-subsuming ternary resolvents
c [quatres-9-2] added 35 single-self-subsuming ternary resolvents
c [quatres-9-2] added 91 quaternary resolvents
c [ternres-9] limit 200000000 with penalty 0 = 0 + 0
c [ternres-9] all 3070 free variables schedulable
c [ternres-9] 2 ternary resolvents (0 bin, 2 trn)
c [ternres-9] fully completed ternary resolution
c [unhide-5] limit 5000000 with penalty 2 = 2 + 0
c [unhide-5-13] 0 units, 0 failed, 36 tauts, 0 hbrs, 4736 literals
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 1 transitive binary clauses
c [block-4] scheduling all variables this time
c [block-4] scheduled 3070 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 3070 variables 100%
c [elim-5] limit of 100000000 steps penalty 3 = 3 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5-1] no variable eliminated in round 1 in 35204969 steps
c [elim-5] fully completed in 1 rounds
c [elim-5] transition to [ all 0 rem 0 ] state
c [elim-5] eliminated 0 = 0% variables out of 3070 scheduled
c [bca-4] limit of 10000000 steps and 100198 added (scaled 2)
c [bca-4] 2 out of 6142 literals actually usable 0%
c [bca-4] not enough literals usable
c [bca-4] added 0 blocked clauses in 207621 steps
c [sort-queue-11] sorted 3070 enqueued variables after 3823002 conflicts
c [score-dist-11] active 0 (0%), one 3070 (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 0 variables 0.0% (3070 remain 85%)
c [simplification-11] removed 2 irredundant clauses 0.0% (49849 remain 69%)
c [simplification-11] maximum reduction of 0% = max (0%, 0%)
c [simplification-11] full geometric conflict interval increment 1920000
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 5323002 (soft 4823002 + delta 500000)
c [simplification-11] new conflict limit 4823002 (hard 5323002)
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 -  680.4    3070    49849   3893701  202583   6953   300   39   373   24  11%   1024   -3   46   39  117%
c -  696.9    3070    49849   3972120  203979   6953   300   41   374   24  11%   1024    1   34   40   87%
c -  712.7    3070    49849   4051748  206430   6954   300   39   379   24  10%   1024    7   44   39  111%
c -  729.0    3070    49849   4131340  209040   6954   300   41   374   24  11%   1024   -3   39   40   97%
c -  745.2    3070    49849   4210809  210740   6957   300   41   371   24  11%   1024   -6   39   40   98%
c -  761.9    3070    49849   4291104  212867   6961   300   40   382   25  10%   1024    5   40   40  100%
c -  778.6    3070    49849   4371638  214625   6963   300   41   381   25  11%   1024    4   40   41   97%
c -  795.4    3070    49849   4452803  216786   6965   300   41   374   25  11%   1024   -5   44   41  106%
c -  812.4    3070    49849   4534147  218604   6966   300   42   373   25  11%   1024   -9   47   41  113%
c -  829.3    3070    49849   4616017  220330   6969   300   41   376   25  11%   1024   -0   43   41  105%
c -  847.0    3070    49849   4698534  221785   6970   300   42   367   26  12%   1024  -10   55   42  133%
c -  865.2    3070    49849   4782166  223258   6971   300   43   379   26  11%   1024    3   42   42   99%
c 
c [simplification-12] limit 4823002 conflicts (hard 5323002) hit after 4823002 conflicts
c [quatres-10] found 28459 quaternary clauses 12% in total
c [quatres-10-1] removed 80 duplicate quaternary clauses
c [quatres-10-2] added 20 single-self-subsuming ternary resolvents
c [quatres-10-2] added 60 quaternary resolvents
c [ternres-10] limit 200000000 with penalty 0 = 0 + 0
c [ternres-10] all 3070 free variables schedulable
c [ternres-10] 17 ternary resolvents (0 bin, 17 trn)
c [ternres-10] fully completed ternary resolution
c [gauss-4] limit 6250000 penalty 3 = 3 + 0
c [gauss-4] extracted 4184 xors of average arity 5.3
c [gauss-4] connected 22216 occurrences of 840 variables (average 26.4)
c [gauss-4] limit 6250000 penalty 3 = 3 + 0
c [gauss-4] connected 2458 occurrences of 840 variables (average 2.9)
c [gauss-4] fully completed
c [gauss-4] exported 0 unary, 0 binary and 0 ternary equations
c [transred-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 0 transitive binary clauses
c [cce-5] limit of 202817812 steps penalty 3 = 3 + 0
c [cce-5-1] eliminated 2 clauses out of 17508 (0%) of length 6
c [cce-5-1] eliminated 10 clauses out of 10559 (0%) of length 5
c [cce-5-1] eliminated 4 clauses out of 5510 (0%) of length 4
c [cce-5-1] completed large round (ACCE)
c [cce-5-1] eliminated 16 large clauses in 25119699 steps
c [cce-5-1] allowing another 12559849 steps for small clauses
c [cce-5-1] scheduling 965 clauses = 297 binary + 668 ternary
c [cce-5-1] tried to eliminate 965 small clauses 100%
c [cce-5-1] eliminated 4 ternary clauses 1%
c [cce-5-1] eliminated 4 small clauses 0%
c [cce-5-1] eliminated 4 small clauses in 12771074 steps
c [cce-5-1] completed small round (ACCE)
c [cce-5-1] completed small and large (ACCE)
c [cce-5-1] eliminated 20 covered clauses in round 1
c [cce-5-2] completed large round (ACCE)
c [cce-5-2] allowing another 12542450 steps for small clauses
c [cce-5-2] scheduling 961 clauses = 297 binary + 664 ternary
c [cce-5-2] tried to eliminate 961 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 20 covered clauses in TOTAL during 2 rounds
c [cce-5] 20 < 1/100 * 49849 = 498 considered unsuccessful
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 121690686 penalty 3 = 3 + 0
c [sweep-5-1] 1191 pos 51.3% + 1129 neg 48.7% = 2320 sched 75.6% ret 750
c [sweep-5-1] 2238124 steps 168 queries 63.70 avg class size
c [sweep-5-1] 16097 decisions 167 SAT calls 832.62 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] 1578 pos 51.4% + 1492 neg 48.6% = 3070 sched 100.0% ret 0
c [sweep-5-2] 2286936 steps 179 queries 62.11 avg class size
c [sweep-5-2] 17379 decisions 178 SAT calls 843.27 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] 1578 pos 51.4% + 1492 neg 48.6% = 3070 sched 100.0% ret 0
c [sweep-5-3] 2188102 steps 185 queries 77.32 avg class size
c [sweep-5-3] 17595 decisions 184 SAT calls 772.65 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, 529 queries)
c [sort-queue-12] sorted 3070 enqueued variables after 4823002 conflicts
c [score-dist-12] active 0 (0%), one 3070 (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% (3070 remain 85%)
c [simplification-12] removed 20 irredundant clauses 0.0% (49829 remain 69%)
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 6323002 (soft 5823002 + delta 500000)
c [simplification-12] new conflict limit 5823002 (hard 6323002)
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 -  885.7    3070    49829   4866726  226186   7015   300   43   365   26  12%   1024   -8   48   42  113%
c -  903.9    3070    49829   4950832  227033   7015   300   42   382   26  11%   1024    6   42   42  100%
c -  922.6    3070    49829   5036644  227995   7015   300   42   376   26  11%   1024   -3   45   41  111%
c -  941.8    3070    49829   5123964  230224   7016   300   40   371   26  11%   1024   -5   33   41   81%
c -  961.0    3070    49829   5211448  232608   7016   300   42   381   26  11%   1024    2   49   41  118%
c -  980.1    3070    49829   5299197  234121   7017   300   40   379   27  10%   1024    3   39   41   97%
c -  999.8    3070    49829   5387937  235880   7021   300   40   382   27  11%   1024    7   48   40  118%
c
c CAUGHT SIGNAL 15 SIGTERM
c
c s UNKNOWN
c bate: 46 basic ate = 42 trn 91% + 4 lrg 9% in 2 updates
c bcas: 4 count, 0 added (0 skipped), 334830 steps
c bkwd: tried 5080 clauses, 10103 lits, 1.99 lits/clause
c bkwd: checked 434815 occs, 85.59 occs/clause, 43.04 occs/lit
c bkwd: subsumed 0 binary, 1 ternary, 7 large
c bkwd: strengthened 0 binary, 3 ternary (100% self), 64 large (0% self)
c blkd: 4 bces, 106 removed, 2457652 resolutions, 5173350 steps
c blkd: 32 blocking literals 0%, 0 pure
c bump: 5357220 bumped seen, 531276168 lits 99.2 on average
c card: 4 count, 0 units, 0 am1, 9901533 steps
c card: 0 rescheduled, 0 eliminated, 0 resolved, 1583 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: 57 at-most-two constraints found, average size 4.05
c card: 55 at-most-two constraints used 96%, average size 4.05
c cces: 5 cces, 7551 eliminated, 7511 ate 99%, 40 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: 49 gcs, 0 rescored clauses, 0 rescored vars
c dcps: 37 decompositions, 281 equivalent 7%
c deco: 6891 decision-only clauses 0%, 44% reduction
c decs: 32656181 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 5 elims, 92 eliminated 2%, 0 pure 0%
c elms: 8 rounds, 1.6 rounds/bve
c elms: 92 small 100%, 0 large 0%
c elms: 1510 tried small, 92 succeeded 6%, 1418 failed 94%
c elms: 2319 subsumed, 2997 strengthened, 3 blocked
c elms: 1005520 copies, 2380235 resolutions, 402682 ipos
c elms: 178579 subchks, 122886 strchks
c gaus: 4 extractions, 8676 extracted, 5.1 size, 7 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 1 gc, 18995772 steps, 9497886 extr 50%, 282391 elim 1%
c glue: 34.9 orig avg, 34.9 real avg, 5.0 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 173 = 61 simple 35% + 80 trn 46% + 32 lrg 18%, 29 sub 17%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 5357220 clauses, 73.3 length
c lrnd: 392528997 lits = 416902938 orig - 24373941 removed 6%
c lrnd: 2399533 uips 45%, 2417489 flips 45%
c mins: 5002712 mins 94%, 53 bin 0%, 335906 size 6%
c mins: 331261259 poisoned searches, 30724230 hits, 9% hit rate
c mins: 653230213 used twice searches, 116679349 hits, 18% hit rate
c move: moved 1385, 9 bin 1%, 1376 trn 99%
c otfs: 34208 driving 47%, 38281 restarting 53%
c otfs: str 72489, 70962 red 98%, 1527 irr 2%
c otfs: str 72489, 0 bin 0%, 138 trn 0%, 72351 lrg 100%
c otfs: sub 468, 465 red 99%, 3 irr 1%
c otfs: sub 468, 0 bin 0%, 23 trn 5%, 445 lrg 95%
c phas: 1 computed, 3109 set, 1328 pos (43%), 1781 neg (57%)
c prbs: 3 basic, 7668 probed, 5 failed, 1 lifted
c prbs: 4 simple, 14728 probed, 40 failed, 170 eqs
c prbs: 3 treelook, 4984 probed, 1 failed, 0 lifted
c prom: 872304 locked 17% out of 5237919 tried
c prps: 578988523 props, 18 props/dec
c prps: 100% srch, 0% simp, 0% lkhd
c quat: 10 count, 2816 quat, 2283 self1, 226 self2, 488 dup
c queu: 12 sorted, 32656181 next (140 steps 0.00)
c queu: 531317202 enq (0 steps 0.00), 531276168 deq 100%
c redc: 801 clauses 0%, 546345 tried 10%, 0 sat 0%
c redc: 824 lits 0%, 4536879 tried 1%, 0 sat 0%
c redc: 34 times jump level reduced, 19.2 levels on average
c reds: 80 count, 67357.4 conflicts per reduce
c reds: 0 memlim 0%, 80 arith 100%
c reds: 3539040 collected 70%, 1551117 retired 30%
c rmbd: 27 removed, 14 red 52%
c rsts: 36583 restarts 100%, 0 skipped 0%
c rsts: 0 saturating 0%, 0 reuse 0%
c rsts: 0 kept 0.0% average 0.0%
c simp: 12 count, 12 confs 100%, 0 vars 0%
c simp: 0 its 0%, 0 bin 0%, 0 trns 0%
c subl: 5357220 count (10270806 tried 1.9), 26036 sub out of 5354979 (0.5%)
c swps: 5 count, 13 rounds, 3429 queries (263.8/round)
c swps: 3432 sat calls, 10 unsat (0.8% success rate)
c swps: 119577 decisions 34.8, 2836 conflicts 0.8
c swps; 149.5 avg class size, 157.7 avg environment size
c swps: 0 failed, 19 impls, 7 equivs
c swp0: 1138 type 0 queries, 45 unsat (4.0%), 1134 sat (99.6%)
c swp1: 2291 type 1 queries, 173 unsat (7.6%), 2288 sat (99.9%)
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: 76027080 calls to obtain time
c tops: 685 fixed 17%, 1 its, 5388592.00 confs/it
c trds: 10 transitive reductions, 87 removed, 0 failed
c trds: 61168 nodes, 5458 edges, 8233 steps
c trim: 204007 words, 0.8 MB
c trnr: 10 count, 74 bin, 806 trn, 18178624 steps
c unhd: 5 count, 13 rounds, 8339747 steps
c unhd: 0 non-trivial sccs of average size 0.0
c unhd: 0 units, 0 bin, 0 trn, 0 lrg
c unhd: 1 failed, 0 stamp, 0 lits, 0 bin, 1 trn, 0 lrg
c unhd: 1359 tauts, 0 bin 0%, 1035 trn 76%, 306 lrg 23%
c unhd: 1359 tauts, 18 stamp 1%, 878 red 65%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 8236 str, 0 bin 0%, 75 trn 1%, 8161 lrg 99%, 8148 red 99%
c vars: 3070 remaining 74% and 1058 removed 26% out of 4128
c vars: 685 fixed 17%, 92 eliminated 2%, 281 equivalent 7%
c vsts: 37596658486 visits, 100% srch, 0% simp, 0% lkhd
c vsts: 64.9 search visits per propagation, 6975.1 per conflict
c wchs: 11090630066 pushed, 14092354 enlarged, 1193 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all        5357795       3539040       1551117     243274322      52715687       2689533
c 
c  0 0        199339   4       400   0         0   0 196764157  81< 38384965  73   1954409  73     6.3
c  1 5        229127   4     95607   3    112862   7  25396831  10   5645640  11<   311761  12<    0.7
c  2 6        754643  14    425081  12    307538  20  11172527   5   3206203   6    164399   6     1.3
c  3 9        797020  15    517745  15    273904  18   3329763   1   1480462   3     61545   2     1.0
c  4 14       704056  13    499937  14    201022  13   2050321   1   1102207   2     46418   2     1.3
c  5 21       597484  11<   435530  12<   159185  10<  1347475   1    791262   2     34643   1     1.8
c  6 30       492803   9    365931  10    124843   8    906322   0    565527   1     26288   1     2.3
c  7 41       413473   8    312220   9     99569   6    660755   0    429865   1     21455   1     2.9
c  8 54       344420   6    264288   7     78464   5    504221   0    339105   1     18291   1     3.5
c  9 69       282222   5    218638   6     61747   4    394791   0    269961   1     15668   1     4.0
c 10 86       381119   7    292569   8     85106   5    524351   0    358593   1     23633   1     8.3
c 11 126      147885   3    104290   3     41990   3    202864   0    129855   0     10096   0     5.4
c 12 230       14204   0      6804   0      4887   0     19944   0     12042   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.7           2.8           1.2           1.8           1.9
c 
c   33.478   3% bump
c   22.568   2% decide
c    2.786   0% cce
c 
c    5.041 < 1% rest (below)
c 
c    1.809   0% elim
c    1.646   0% sweep
c    0.806   0% quatres
c    0.782   0% probe
c    0.709   0% unhide
c    0.421   0% block
c    0.359   0% gauss
c    0.144   0% card
c    0.103   0% ternres
c    0.059   0% bca
c    0.013   0% transred
c    0.000   0% locs
c    0.000   0% queuesort
c    0.000   0% rescore
c ==================================
c    0.399   0% preprocessing     4%
c   10.365   1% inprocessing     96%
c ==================================
c   10.764   1% simplifying
c  989.171  99% search
c ==================================
c  999.936 100% all
c 
c       5388592 conflicts,        5388.9 confs/sec
c          1906 ternaries,        2827.2 confs/ternary
c            80 binaries,        67357.4 confs/binary
c             1 iterations,    5388592.0 confs/iteration
c 
c            80 reductions,          0.1 redus/sec,  67357.4 confs/reduction
c         36583 restarts,           36.6 rests/sec,    147.3 confs/restart
c      32656181 decisions,       32658.3 decis/sec,      6.1 decis/conflict
c     578988523 propagations,   579025.6 props/sec,     17.7 props/decision
c 
c 999.9 seconds, 106.3 MB
c
c CAUGHT SIGNAL 15 SIGTERM
c
c launch: done
