c launch: /data/cnf/sc2014/app/dimacs.cnf.bz2
c host: atom11
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 Wed Apr 29 14:26:58 CEST 2015
c compiled Fri May  1 18:19:30 CEST 2015
c 
c gcc (Ubuntu 4.8.2-19ubuntu1) 4.8.2
c -Wall -O3 -DNLGLOG -DNDEBUG -DNCHKSOL -DNLGLDRUPLIG -DNLGLYALSAT
c Linux fmvx1 3.13.0-49-generic x86_64
c 
c piping '/data/cnf/sc2014/app/dimacs.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/dimacs.cnf.bz2
c no embedded options
c found 'p cnf 2835 9747' header
c read 2835 variables, 9747 clauses, 26101 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=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 2834 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] INC (--score=1)
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    2834     9746         0       0      0     0    0     0    1   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] no at-most-one constraint found
c [card-1] no at-most-two constraint found
c [decomp-1] removed 3 variables
c [simpleprobe-1] all 2832 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 3 variables
c [simpleprobe-1] fully completed simple probing
c [simpleprobe-1] removed 3 variables, found 1078 hbrs, 0 units
c [unhide-1] limit 100000 with penalty 0 = 0 + 0
c [unhide-1-3] 0 units, 16 failed, 9 tauts, 0 hbrs, 13 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 2821 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 1182 variables 42% in round 1 in 589156 steps
c [elim-1-1] backward subsumption/strengthening limit 589100
c [elim-1-1-1] backward checking 2185 touched variables 77%
c [elim-1-1-1] fully completed backward checking in 1 rounds
c [elim-1-1] subsumed 1 and strengthened 51 clauses in 198355 steps
c [elim-1-1] rescheduled 65 variables 2% by backward subsumption
c [elim-1-2] eliminated 2 variables 0% in round 2 in 50030 steps
c [elim-1-2] backward subsumption/strengthening limit 50000
c [elim-1-2-1] backward checking 20 touched variables 1%
c [elim-1-2-1] fully completed backward checking in 1 rounds
c [elim-1-2] subsumed 2 and strengthened 12 clauses in 31131 steps
c [elim-1-2] rescheduled 15 variables 1% by backward subsumption
c [elim-1-3] no variable eliminated in round 3 in 7374 steps
c [elim-1] fully completed in 3 rounds
c [elim-1] transition to [ all 0 rem 0 ] state
c [elim-1] eliminated 1184 = 42% variables out of 2821 scheduled
c [phase-count-1] 6316 negative 80.5% of 7846 except 1530 19.5%
c [phase-count-1] 6678 positive 85.1% of 7846 except 1168 14.9%
c [phase-1] phase bias: 1484 positive 91%, 153 negative 9%
c [sort-queue-1] sorted 1637 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 1637 (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 1196 variables 42.2% (1637 remain 58%)
c [simplification-1] removed 1900 irredundant clauses 19.5% (7846 remain 81%)
c [simplification-1] maximum reduction of 42% = max (42%, 19%)
c [simplification-1] large reduction 42% >= 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 1001 conflicts
c [decomp-3] removed 5 variables
c [simpleprobe-2] all 1632 free variables schedulable
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [decomp-4] removed 1 variables
c [simpleprobe-2] fully completed simple probing
c [simpleprobe-2] removed 1 variables, found 63 hbrs, 0 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 3262 literals 100%
c [treelook-1] scheduling used 54237 steps
c [treelook-1] scheduled completely
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 147952 steps
c [treelook-1] fully completed tree based probing
c [decomp-5] removed 6 variables
c [treelook-1] removed 8 variables, found 828 hbrs
c [basicprobe-1] limit 1000000 penalty 0 = 0 + 0
c [basicprobe-1-0] 314 sched 19%, 0 failed, 0 lifted, 81 hbrs
c [basicprobe-1-1] 331 sched 20%, 0 failed, 0 lifted, 4 hbrs
c [basicprobe-1-2] 331 sched 20%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-1-2] fully completed probing
c [basicprobe-1-2] removed 0 variables, found 85 hbrs
c [unhide-2] limit 100000 with penalty 0 = 0 + 0
c [unhide-2-8] 0 units, 0 failed, 386 tauts, 0 hbrs, 181 literals
c [block-1] scheduling all variables this time
c [block-1] scheduled 1623 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 2 blocked clauses
c [block-1] 2 < 1/100 * 7773 = 77 considered unsuccessful
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 5 clauses out of 52 (10%) of length 5
c [cce-1-1] eliminated 14 clauses out of 495 (3%) of length 4
c [cce-1-1] completed large round (ATE)
c [cce-1-1] eliminated 19 large clauses in 192387 steps
c [cce-1-1] allowing another 96193 steps for small clauses
c [cce-1-1] scheduling 4599 clauses = 148 binary + 4451 ternary
c [cce-1-1] tried to eliminate 4599 small clauses 100%
c [cce-1-1] eliminated 17 binary clauses 11%
c [cce-1-1] eliminated 13 ternary clauses 0%
c [cce-1-1] eliminated 30 small clauses 1%
c [cce-1-1] eliminated 30 small clauses in 502525 steps
c [cce-1-1] completed small round (ATE)
c [cce-1-1] completed small and large (ATE)
c [cce-1-1] eliminated 49 covered clauses in round 1
c [cce-1-2] completed large round (ABCE)
c [cce-1-2] allowing another 93672 steps for small clauses
c [cce-1-2] scheduling 4569 clauses = 131 binary + 4438 ternary
c [cce-1-2] tried to eliminate 4569 small clauses 100%
c [cce-1-2] eliminated 3 binary clauses 2%
c [cce-1-2] eliminated 3 small clauses 0%
c [cce-1-2] eliminated 3 small clauses in 495416 steps
c [cce-1-2] completed small round (ABCE)
c [cce-1-2] completed small and large (ABCE)
c [cce-1-2] eliminated 3 covered clauses in round 2
c [cce-1-3] completed large round (ACCE)
c [cce-1-3] allowing another 100287 steps for small clauses
c [cce-1-3] scheduling 4566 clauses = 128 binary + 4438 ternary
c [cce-1-3] tried to eliminate 4566 small clauses 100%
c [cce-1-3] eliminated 3 binary clauses 2%
c [cce-1-3] eliminated 3 small clauses 0%
c [cce-1-3] eliminated 3 small clauses in 548764 steps
c [cce-1-3] completed small round (ACCE)
c [cce-1-3] completed small and large (ACCE)
c [cce-1-3] eliminated 3 covered clauses in round 3
c [cce-1] eliminated 55 covered clauses in TOTAL during 3 rounds
c [cce-1] 55 < 1/100 * 7771 = 77 considered unsuccessful
c [elim-2] scheduling all variables this time
c [elim-2] scheduled 1623 variables 100%
c [elim-2] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-2] rescheduling of touched variables disabled
c [elim-2-1] eliminated 469 variables 29% in round 1 in 1844294 steps
c [elim-2-1] backward subsumption/strengthening limit 1844200
c [elim-2-1-1] backward checking 1093 touched variables 67%
c [elim-2-1-1] fully completed backward checking in 1 rounds
c [elim-2-1] subsumed 1 and strengthened 14 clauses in 130910 steps
c [elim-2-1] rescheduled 52 variables 3% by backward subsumption
c [elim-2-2] no variable eliminated in round 2 in 318151 steps
c [elim-2] fully completed in 2 rounds
c [elim-2] transition to [ all 0 rem 0 ] state
c [elim-2] eliminated 469 = 29% variables out of 1623 scheduled
c [bca-1] limit of 10000000 steps and 14956 added (scaled 2)
c [bca-1] 2138 out of 2310 literals actually usable 93%
c [bca-1] added 0 blocked clauses in 4983 steps
c [sweep-1] limit 1000000 penalty 0 = 0 + 0
c [sweep-1-1] 566 pos 49.0% + 588 neg 51.0% = 1154 sched 100.0% ret 0
c [sweep-1-1] 171696 steps 177 queries 38.63 avg class size
c [sweep-1-1] 1735 decisions 177 SAT calls 17.02 avg env size
c [sweep-1-1] fully completed sweeping round
c [decomp-8] removed 1 variables
c [sweep-1-1] removed 1 vars (0 failed, 1 eqs, 1 impls)
c [sweep-1-2] 566 pos 49.1% + 587 neg 50.9% = 1153 sched 100.0% ret 0
c [sweep-1-2] 184272 steps 184 queries 38.28 avg class size
c [sweep-1-2] 1983 decisions 183 SAT calls 17.67 avg env size
c [sweep-1-2] fully completed sweeping round
c [sweep-1-2] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-1-3] 566 pos 49.1% + 587 neg 50.9% = 1153 sched 100.0% ret 0
c [sweep-1-3] 153139 steps 188 queries 38.08 avg class size
c [sweep-1-3] 1771 decisions 187 SAT calls 16.31 avg env size
c [sweep-1-3] fully completed sweeping round
c [sweep-1-3] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-1] removed 1 vars in TOTAL (3 rounds, 546 queries)
c [sort-queue-2] sorted 53 enqueued variables after 1001 conflicts
c [score-dist-2] active 1100 (95%), one 0 (0%), zero 53 (5%)
c [score-dist-2] max exp 511, different 11 (2%)
c [score-dist-2] median active exp 509, avg 508.0
c [simplification-2] removed 484 variables 29.6% (1153 remain 41%)
c [simplification-2] removed 618 irredundant clauses 7.9% (7228 remain 74%)
c [simplification-2] maximum reduction of 30% = max (30%, 8%)
c [simplification-2] large reduction 30% >= 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 13001 (soft 3001 + delta 10000)
c [simplification-2] new conflict limit 3001 (hard 13001)
c 
c [simplification-3] limit 3001 conflicts (hard 13001) hit after 3001 conflicts
c [quatres-1] found 4045 quaternary clauses 94% in total
c [quatres-1-2] added 134 single-self-subsuming ternary resolvents
c [quatres-1-2] added 63 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 1153 free variables schedulable
c [ternres-1] 486 ternary resolvents (2 bin, 484 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 3 at-most-two constraints of average size 4.0
c [card-2] using previous limit 1000000 for elimination
c [card-2] 3 out of 3 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 4260 xors of average arity 3.8
c [gauss-1] connected 16188 occurrences of 1045 variables (average 15.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 [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] scheduled 2306 literals 100%
c [treelook-2] scheduling used 50846 steps
c [treelook-2] scheduled completely
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] used 132404 steps
c [treelook-2] fully completed tree based probing
c [treelook-2] removed 0 variables, found 9 hbrs
c [transred-1] limit 100000 with penalty 0 = 0 + 0
c [transred-1] removed 24 transitive binary clauses
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 1153 variables 100%
c [elim-3] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-3] rescheduling of touched variables disabled
c [elim-3-1] eliminated 5 variables 0% in round 1 in 1721806 steps
c [elim-3-1] backward subsumption/strengthening limit 1721800
c [elim-3-1-1] backward checking 15 touched variables 1%
c [elim-3-1-1] fully completed backward checking in 1 rounds
c [elim-3-1] subsumed 0 and strengthened 0 clauses in 8860 steps
c [elim-3] fully completed in 1 rounds
c [elim-3] transition to [ all 0 rem 0 ] state
c [elim-3] eliminated 5 = 0% variables out of 1153 scheduled
c [elim-3] 5 < 1/100 * 1153 = 11 considered unsuccessful
c [sweep-2] limit 1000000 penalty 0 = 0 + 0
c [sweep-2-1] 600 pos 52.3% + 548 neg 47.7% = 1148 sched 100.0% ret 0
c [sweep-2-1] 657385 steps 126 queries 23.62 avg class size
c [sweep-2-1] 2270 decisions 125 SAT calls 30.46 avg env size
c [sweep-2-1] fully completed sweeping round
c [sweep-2-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-2-2] 600 pos 52.3% + 548 neg 47.7% = 1148 sched 100.0% ret 0
c [sweep-2-2] 387002 steps 29 queries 119.86 avg class size
c [sweep-2-2] 1264 decisions 28 SAT calls 53.21 avg env size
c [sweep-2-2] 603 variables remain 53% (545 retained 47%)
c [sweep-2-2] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-2] removed 0 vars in TOTAL (2 rounds, 153 queries)
c [sort-queue-3] sorted 29 enqueued variables after 3001 conflicts
c [score-dist-3] active 1119 (97%), one 0 (0%), zero 29 (3%)
c [score-dist-3] max exp 513, different 13 (3%)
c [score-dist-3] median active exp 511, avg 509.4
c [simplification-3] removed 5 variables 0.4% (1148 remain 41%)
c [simplification-3] removed 21 irredundant clauses 0.3% (7207 remain 74%)
c [simplification-3] maximum reduction of 0% = max (0%, 0%)
c [simplification-3] full geometric conflict interval increment 20000
c [simplification-3] new conflict interval 20000
c [simplification-3] penalized conflict interval 20000 = 1 * 20000
c [simplification-3] hard conflict limit 33001 (soft 23001 + delta 10000)
c [simplification-3] new conflict limit 23001 (hard 33001)
c 
c [simplification-4] limit 23001 conflicts (hard 33001) hit after 23002 conflicts
c [quatres-2] found 4045 quaternary clauses 89% in total
c [quatres-2-2] added 83 single-self-subsuming ternary resolvents
c [quatres-2-2] added 65 quaternary resolvents
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] all 1148 free variables schedulable
c [ternres-2] 39 ternary resolvents (0 bin, 39 trn)
c [ternres-2] fully completed ternary resolution
c [unhide-3] limit 167155 with penalty 1 = 1 + 0
c [unhide-3-9] 0 units, 0 failed, 0 tauts, 0 hbrs, 267 literals
c [transred-2] limit 1671551 with penalty 0 = 0 + 0
c [transred-2] removed 4 transitive binary clauses
c [block-2] scheduling all variables this time
c [block-2] scheduled 1148 variables 100%
c [block-2] limit of 25000000 steps penalty 1 = 1 + 0
c [block-2] fully completed
c [block-2] transition to [ all 0 rem 0 ] state
c [block-2] eliminated 0 blocked clauses
c [cce-2] limit of 15000000 steps penalty 1 = 1 + 0
c [cce-2-1] eliminated 1 clauses out of 99 (1%) of length 5
c [cce-2-1] eliminated 5 clauses out of 3901 (0%) of length 4
c [cce-2-1] completed large round (ATE)
c [cce-2-1] eliminated 6 large clauses in 763765 steps
c [cce-2-1] allowing another 381882 steps for small clauses
c [cce-2-1] scheduling 1861 clauses = 93 binary + 1768 ternary
c [cce-2-1] tried to eliminate 1861 small clauses 100%
c [cce-2-1] eliminated 3 binary clauses 3%
c [cce-2-1] eliminated 182 ternary clauses 10%
c [cce-2-1] eliminated 185 small clauses 10%
c [cce-2-1] eliminated 185 small clauses in 662424 steps
c [cce-2-1] completed small round (ATE)
c [cce-2-1] eliminated 191 covered clauses in round 1
c [cce-2-2] completed large round (ATE)
c [cce-2-2] allowing another 370373 steps for small clauses
c [cce-2-2] scheduling 1676 clauses = 90 binary + 1586 ternary
c [cce-2-2] tried to eliminate 1676 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 191 covered clauses in TOTAL during 2 rounds
c [bca-2] limit of 10000000 steps and 14532 added (scaled 2)
c [bca-2] 645 out of 2298 literals actually usable 28%
c [bca-2] added 0 blocked clauses in 23867 steps
c [score-dist-4] active 1148 (100%), one 0 (0%), zero 0 (0%)
c [score-dist-4] max exp 516, different 15 (3%)
c [score-dist-4] median active exp 515, avg 513.2
c [simplification-4] removed 0 variables 0.0% (1148 remain 41%)
c [simplification-4] removed 191 irredundant clauses 2.7% (7016 remain 72%)
c [simplification-4] maximum reduction of 3% = max (0%, 3%)
c [simplification-4] geometric conflict interval increment 5000 = 20000 / 4
c [simplification-4] new conflict interval 25000
c [simplification-4] penalized conflict interval 25000 = 1 * 25000
c [simplification-4] hard conflict limit 60502 (soft 48002 + delta 12500)
c [simplification-4] new conflict limit 48002 (hard 60502)
c 
c [simplification-5] limit 48002 conflicts (hard 60502) hit after 48003 conflicts
c [quatres-3] found 4065 quaternary clauses 86% in total
c [quatres-3-2] added 55 single-self-subsuming ternary resolvents
c [quatres-3-2] added 41 quaternary resolvents
c [ternres-3] limit 5112398 with penalty 0 = 0 + 0
c [ternres-3] all 1148 free variables schedulable
c [ternres-3] 41 ternary resolvents (0 bin, 41 trn)
c [ternres-3] fully completed ternary resolution
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] extracted 4224 xors of average arity 3.8
c [gauss-2] connected 16080 occurrences of 1041 variables (average 15.4)
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 12780996 penalty 1 = 1 + 0
c [basicprobe-2-0] 247 sched 22%, 0 failed, 0 lifted, 6 hbrs
c [basicprobe-2-1] 247 sched 22%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-2-1] fully completed probing
c [basicprobe-2-1] removed 0 variables, found 6 hbrs
c [transred-3] limit 2000000 with penalty 0 = 0 + 0
c [transred-3] removed 1 transitive binary clauses
c [cce-3] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-3-1] eliminated 1 clauses out of 3895 (0%) of length 4
c [cce-3-1] completed large round (ACCE)
c [cce-3-1] eliminated 1 large clauses in 835035 steps
c [cce-3-1] allowing another 417517 steps for small clauses
c [cce-3-1] scheduling 1677 clauses = 90 binary + 1587 ternary
c [cce-3-1] tried to eliminate 1677 small clauses 100%
c [cce-3-1] completed small round (ACCE)
c [cce-3-1] eliminated 1 covered clauses in round 1
c [cce-3-2] completed large round (ACCE)
c [cce-3-2] allowing another 416566 steps for small clauses
c [cce-3-2] scheduling 1677 clauses = 90 binary + 1587 ternary
c [cce-3-2] tried to eliminate 1677 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 1 covered clauses in TOTAL during 2 rounds
c [cce-3] 1 < 1/100 * 7016 = 70 considered unsuccessful
c [elim-4] scheduling all variables this time
c [elim-4] scheduled 1148 variables 100%
c [elim-4] boosting limit by 20
c [elim-4] limit of 1022479700 steps penalty 1 = 1 + 0
c [elim-4] rescheduling of touched variables disabled
c [elim-4-1] eliminated 1 variables 0% in round 1 in 1633869 steps
c [elim-4-1] backward subsumption/strengthening limit 1633800
c [elim-4-1-1] backward checking 13 touched variables 1%
c [elim-4-1-1] fully completed backward checking in 1 rounds
c [elim-4-1] subsumed 0 and strengthened 0 clauses in 13323 steps
c [elim-4] fully completed in 1 rounds
c [elim-4] transition to [ all 0 rem 0 ] state
c [elim-4] eliminated 1 = 0% variables out of 1148 scheduled
c [elim-4] 1 < 1/100 * 1148 = 11 considered unsuccessful
c [sweep-3] limit 766859 penalty 1 = 1 + 0
c [sweep-3-1] 274 pos 45.5% + 328 neg 54.5% = 602 sched 52.5% ret 545
c [sweep-3-1] 849568 steps 17 queries 74.06 avg class size
c [sweep-3-1] 659 decisions 16 SAT calls 62.12 avg env size
c [sweep-3-1] 497 variables remain 43% (650 retained 57%)
c [sweep-3-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-3] removed 0 vars in TOTAL (1 rounds, 16 queries)
c [score-dist-5] active 1147 (100%), one 0 (0%), zero 0 (0%)
c [score-dist-5] max exp 517, different 14 (3%)
c [score-dist-5] median active exp 516, avg 514.4
c [simplification-5] removed 1 variables 0.1% (1147 remain 40%)
c [simplification-5] removed 2 irredundant clauses 0.0% (7014 remain 72%)
c [simplification-5] maximum reduction of 0% = max (0%, 0%)
c [simplification-5] full geometric conflict interval increment 25000
c [simplification-5] new conflict interval 50000
c [simplification-5] penalized conflict interval 50000 = 1 * 50000
c [simplification-5] hard conflict limit 123003 (soft 98003 + delta 25000)
c [simplification-5] new conflict limit 98003 (hard 123003)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c -   16.1    1147     7014     51509   25573   1502   233   16    16    8  98%    550    7   16    9  184%
c -   24.8    1147     7014     78061   26264   1518   233   15    15    8  98%    708    4   15   11  143%
c 
c [simplification-6] limit 98003 conflicts (hard 123003) hit after 98005 conflicts
c [quatres-4] found 4088 quaternary clauses 85% in total
c [quatres-4-2] added 41 single-self-subsuming ternary resolvents
c [quatres-4-2] added 24 quaternary resolvents
c [ternres-4] limit 12454005 with penalty 0 = 0 + 0
c [ternres-4] all 1147 free variables schedulable
c [ternres-4] 10 ternary resolvents (0 bin, 10 trn)
c [ternres-4] fully completed ternary resolution
c [card-3] limit 1556750 penalty 2 = 2 + 0
c [card-3] no at-most-one constraint found
c [card-3] found 3 at-most-two constraints of average size 4.0
c [card-3] using previous limit 1556750 for elimination
c [card-3] 3 out of 3 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [simpleprobe-3] all 1147 free variables schedulable
c [simpleprobe-3] limit 49816020 penalty 0 = 0 + 0
c [simpleprobe-3] fully completed simple probing
c [simpleprobe-3] removed 0 variables, found 49 hbrs, 0 units
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 37 transitive binary clauses
c [score-dist-6] active 1147 (100%), one 0 (0%), zero 0 (0%)
c [score-dist-6] max exp 518, different 15 (3%)
c [score-dist-6] median active exp 517, avg 515.3
c [simplification-6] removed 0 variables 0.0% (1147 remain 40%)
c [simplification-6] removed 0 irredundant clauses 0.0% (7014 remain 72%)
c [simplification-6] maximum reduction of 0% = max (0%, 0%)
c [simplification-6] full geometric conflict interval increment 50000
c [simplification-6] new conflict interval 100000
c [simplification-6] penalized conflict interval 100000 = 1 * 100000
c [simplification-6] hard conflict limit 248005 (soft 198005 + delta 50000)
c [simplification-6] new conflict limit 198005 (hard 248005)
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 -   34.1    1147     7014    105676   26803   1576   245   15    15    8  99%    817    3   15   12  122%
c -   43.4    1147     7014    133750   24744   1579   245   14    14    8  99%    889    1   13   13   99%
c -   55.2    1147     7014    173976   25651   1628   245   14    14   10  97%    951    1   15   13  115%
c 
c [simplification-7] limit 198005 conflicts (hard 248005) hit after 198006 conflicts
c [quatres-5] found 4144 quaternary clauses 79% in total
c [quatres-5-2] added 115 single-self-subsuming ternary resolvents
c [quatres-5-2] added 57 quaternary resolvents
c [ternres-5] limit 27589201 with penalty 0 = 0 + 0
c [ternres-5] all 1147 free variables schedulable
c [ternres-5] 1 ternary resolvents (0 bin, 1 trn)
c [ternres-5] fully completed ternary resolution
c [unhide-4] limit 1379460 with penalty 2 = 2 + 0
c [unhide-4-12] 0 units, 0 failed, 17 tauts, 0 hbrs, 2037 literals
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 1 transitive binary clauses
c [block-3] scheduling all variables this time
c [block-3] scheduled 1147 variables 100%
c [block-3] limit of 68973002 steps penalty 2 = 2 + 0
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 0 blocked clauses
c [cce-4] boosting limit by 10
c [cce-4] limit of 689730025 steps penalty 1 = 1 + 0
c [cce-4-1] eliminated 2 clauses out of 3896 (0%) of length 4
c [cce-4-1] completed large round (ATE)
c [cce-4-1] eliminated 2 large clauses in 746132 steps
c [cce-4-1] allowing another 373066 steps for small clauses
c [cce-4-1] scheduling 1677 clauses = 93 binary + 1584 ternary
c [cce-4-1] tried to eliminate 1677 small clauses 100%
c [cce-4-1] eliminated 1 binary clauses 1%
c [cce-4-1] eliminated 1 small clauses 0%
c [cce-4-1] eliminated 1 small clauses in 617834 steps
c [cce-4-1] completed small round (ATE)
c [cce-4-1] eliminated 3 covered clauses in round 1
c [cce-4-2] completed large round (ATE)
c [cce-4-2] allowing another 371651 steps for small clauses
c [cce-4-2] scheduling 1676 clauses = 92 binary + 1584 ternary
c [cce-4-2] tried to eliminate 1676 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 3 covered clauses in TOTAL during 2 rounds
c [cce-4] 3 < 1/100 * 7014 = 70 considered unsuccessful
c [bca-3] limit of 10000000 steps and 14522 added (scaled 2)
c [bca-3] 667 out of 2296 literals actually usable 29%
c [bca-3] added 0 blocked clauses in 49567 steps
c [score-dist-7] active 1147 (100%), one 0 (0%), zero 0 (0%)
c [score-dist-7] max exp 519, different 16 (3%)
c [score-dist-7] median active exp 518, avg 516.2
c [simplification-7] removed 0 variables 0.0% (1147 remain 40%)
c [simplification-7] removed 3 irredundant clauses 0.0% (7011 remain 72%)
c [simplification-7] maximum reduction of 0% = max (0%, 0%)
c [simplification-7] full geometric conflict interval increment 100000
c [simplification-7] new conflict interval 200000
c [simplification-7] penalized conflict interval 200000 = 1 * 200000
c [simplification-7] hard conflict limit 498006 (soft 398006 + delta 100000)
c [simplification-7] new conflict limit 398006 (hard 498006)
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 -   66.7    1147     7011    206546   26940   1747   225   13    13    8  99%    979   -1   12   13   91%
c -   77.3    1147     7011    237834   27971   1763   225   13    13    9  98%    996   -0   12   13   91%
c -   88.6    1147     7011    272157   27076   1768   225   12    13   11  98%   1008   -1   13   13   97%
c -  100.1    1147     7011    306726   25390   1771   225   14    14   10  99%   1014    0   14   13  108%
c -  112.8    1147     7011    343867   28717   1776   225   13    13   10  98%   1019   -0   12   13   95%
c -  124.6    1147     7011    377963   29351   1777   225   13    13    9  98%   1021   -0   13   13  101%
c -  137.5    1147     7011    414872   28682   1778   225   12    12   12  98%   1022   -1   11   12   90%
c 
c [simplification-8] limit 398006 conflicts (hard 498006) hit after 431499 conflicts
c [quatres-6] found 4137 quaternary clauses 70% in total
c [quatres-6-2] added 78 single-self-subsuming ternary resolvents
c [quatres-6-2] added 41 quaternary resolvents
c [ternres-6] limit 65206028 with penalty 0 = 0 + 0
c [ternres-6] all 1147 free variables schedulable
c [ternres-6] 27 ternary resolvents (0 bin, 27 trn)
c [ternres-6] fully completed ternary resolution
c [gauss-3] limit 3260301 penalty 2 = 2 + 0
c [gauss-3] extracted 4212 xors of average arity 3.8
c [gauss-3] connected 16044 occurrences of 1040 variables (average 15.4)
c [gauss-3] limit 3260301 penalty 2 = 2 + 0
c [gauss-3] fully completed
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [treelook-3] limit 3260301 penalty 1 = 1 + 0 boost 1
c [treelook-3] scheduled 2294 literals 100%
c [treelook-3] scheduling used 195647 steps
c [treelook-3] scheduled completely
c [treelook-3] limit 3260301 penalty 1 = 1 + 0 boost 1
c [treelook-3] used 139948 steps
c [treelook-3] fully completed tree based probing
c [treelook-3] removed 0 variables, found 3 hbrs
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 1 transitive binary clauses
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 1147 variables 100%
c [elim-5] limit of 200000000 steps penalty 2 = 2 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5-1] eliminated 2 variables 0% in round 1 in 1631597 steps
c [elim-5-1] backward subsumption/strengthening limit 1631500
c [elim-5-1-1] backward checking 15 touched variables 1%
c [elim-5-1-1] fully completed backward checking in 1 rounds
c [elim-5-1] subsumed 0 and strengthened 0 clauses in 5338 steps
c [elim-5] fully completed in 1 rounds
c [elim-5] transition to [ all 0 rem 0 ] state
c [elim-5] eliminated 2 = 0% variables out of 1147 scheduled
c [elim-5] 2 < 1/100 * 1147 = 11 considered unsuccessful
c [sweep-4] limit 4890452 penalty 2 = 2 + 0
c [sweep-4-1] 242 pos 48.8% + 254 neg 51.2% = 496 sched 43.3% ret 649
c [sweep-4-1] 2021466 steps 74 queries 21.03 avg class size
c [sweep-4-1] 1724 decisions 73 SAT calls 38.53 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] 540 pos 47.2% + 605 neg 52.8% = 1145 sched 100.0% ret 0
c [sweep-4-2] 2871936 steps 53 queries 39.38 avg class size
c [sweep-4-2] 2157 decisions 52 SAT calls 78.33 avg env size
c [sweep-4-2] 126 variables remain 11% (1019 retained 89%)
c [sweep-4-2] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-4] removed 0 vars in TOTAL (2 rounds, 125 queries)
c [score-dist-8] active 1145 (100%), one 0 (0%), zero 0 (0%)
c [score-dist-8] max exp 520, different 16 (3%)
c [score-dist-8] median active exp 519, avg 517.2
c [simplification-8] removed 2 variables 0.2% (1145 remain 40%)
c [simplification-8] removed 4 irredundant clauses 0.1% (7007 remain 72%)
c [simplification-8] maximum reduction of 0% = max (0%, 0%)
c [simplification-8] full geometric conflict interval increment 200000
c [simplification-8] new conflict interval 400000
c [simplification-8] penalized conflict interval 400000 = 1 * 400000
c [simplification-8] hard conflict limit 1031499 (soft 831499 + delta 200000)
c [simplification-8] new conflict limit 831499 (hard 1031499)
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 -  152.4    1145     7007    454402   28195   1954   222   15    15   10  99%   1023    2   15   13  115%
c -  167.9    1145     7007    496355   31198   1954   222   13    13   11  99%   1023   -0   13   13   96%
c -  181.7    1145     7007    532385   30764   1954   222   13    13   10  99%   1024   -1   13   13   99%
c -  196.8    1145     7007    571790   31019   1955   222   11    12   10  98%   1024   -2   13   13  101%
c -  211.9    1145     7007    610376   32178   1955   222   13    13   10  99%   1024    0   14   13  107%
c -  227.5    1145     7007    650605   32334   1955   222   13    13   13  98%   1024    0   13   13  100%
c -  244.4    1145     7007    695118   33866   1958   222   12    12   13  99%   1024   -1   11   12   91%
c -  260.9    1145     7007    738223   33953   1958   222   13    13   12  99%   1024    0   12   13   99%
c -  277.6    1145     7007    780943   35353   1959   222   13    13   12  99%   1024    0   13   13  106%
c -  293.3    1145     7007    821290   34275   1961   222   12    12   12  99%   1024   -0   12   12   99%
c 
c [simplification-9] limit 831499 conflicts (hard 1031499) hit after 848081 conflicts
c [quatres-7] found 4192 quaternary clauses 63% in total
c [quatres-7-2] added 114 single-self-subsuming ternary resolvents
c [quatres-7-2] added 58 quaternary resolvents
c [ternres-7] limit 146311442 with penalty 0 = 0 + 0
c [ternres-7] all 1145 free variables schedulable
c [ternres-7] 47 ternary resolvents (0 bin, 47 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 [score-dist-9] active 1145 (100%), one 0 (0%), zero 0 (0%)
c [score-dist-9] max exp 521, different 15 (3%)
c [score-dist-9] median active exp 520, avg 518.2
c [simplification-9] removed 0 variables 0.0% (1145 remain 40%)
c [simplification-9] removed 0 irredundant clauses 0.0% (7007 remain 72%)
c [simplification-9] maximum reduction of 0% = max (0%, 0%)
c [simplification-9] full geometric conflict interval increment 400000
c [simplification-9] new conflict interval 800000
c [simplification-9] penalized conflict interval 800000 = 1 * 800000
c [simplification-9] hard conflict limit 2048081 (soft 1648081 + delta 400000)
c [simplification-9] new conflict limit 1648081 (hard 2048081)
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 -  309.5    1145     7007    863172   35781   2121   222   12    12   10  99%   1024    0   11   12   93%
c -  326.2    1145     7007    904524   36241   2121   222   12    12   14  99%   1024   -0   11   12   91%
c -  342.8    1145     7007    947465   36222   2122   222   11    11   11  99%   1024   -1   10   12   89%
c -  360.3    1145     7007    991399   35233   2125   222   12    13   14  94%   1024    2   13   11  119%
c -  378.8    1145     7007   1037874   38331   2127   222   11    11   13  99%   1024   -0   12   12  104%
c -  396.8    1145     7007   1084233   37411   2128   222   11    11   12  99%   1024   -1   11   11   94%
c -  416.6    1145     7007   1132710   39348   2128   222   12    12   16  98%   1024    1   11   11  103%
c -  434.8    1145     7007   1178988   39214   2128   222   11    11   14  99%   1024   -0   11   11   97%
c -  456.5    1145     7007   1235614   38907   2128   222   10    10   14  99%   1024   -1   10   11   99%
c -  476.7    1145     7007   1287494   40785   2140   222   13    13   12  99%   1024    2   12   11  109%
c -  496.1    1145     7007   1335616   40922   2143   222   13    13   15  98%   1024    1   14   12  118%
c -  515.4    1145     7007   1382772   41575   2143   222   11    12   13  99%   1024   -1   13   12  106%
c -  535.8    1145     7007   1434359   39257   2144   222   11    11   16  99%   1024   -1   10   12   84%
c -  556.0    1145     7007   1488662   43480   2152   222   11    11   15  99%   1024   -1   13   12  109%
c -  576.9    1145     7007   1540998   43539   2155   222   11    12   15  96%   1024    0   13   11  120%
c -  599.2    1145     7007   1596013   43102   2156   222   12    12   12  99%   1024   -0   11   12   98%
c -  628.2    1145     7007   1663316   43741   2159   222   11    11   16  99%   1024   -1   11   11  100%
c 
c [simplification-10] limit 1648081 conflicts (hard 2048081) hit after 1679988 conflicts
c [quatres-8] found 4205 quaternary clauses 53% in total
c [quatres-8-2] added 70 single-self-subsuming ternary resolvents
c [quatres-8-2] added 34 quaternary resolvents
c [ternres-8] limit 200000000 with penalty 0 = 0 + 0
c [ternres-8] all 1145 free variables schedulable
c [ternres-8] 2 ternary resolvents (0 bin, 2 trn)
c [ternres-8] fully completed ternary resolution
c [card-4] limit 21066385 penalty 3 = 3 + 0
c [card-4] no at-most-one constraint found
c [card-4] found 3 at-most-two constraints of average size 4.0
c [card-4] using previous limit 21066385 for elimination
c [card-4] 3 out of 3 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [cce-5] limit of 421327707 steps penalty 2 = 2 + 0
c [cce-5-1] eliminated 1 clauses out of 101 (1%) of length 5
c [cce-5-1] completed large round (ACCE)
c [cce-5-1] eliminated 1 large clauses in 841102 steps
c [cce-5-1] allowing another 420551 steps for small clauses
c [cce-5-1] scheduling 1672 clauses = 88 binary + 1584 ternary
c [cce-5-1] tried to eliminate 1672 small clauses 100%
c [cce-5-1] completed small round (ACCE)
c [cce-5-1] eliminated 1 covered clauses in round 1
c [cce-5-2] completed large round (ACCE)
c [cce-5-2] allowing another 419420 steps for small clauses
c [cce-5-2] scheduling 1672 clauses = 88 binary + 1584 ternary
c [cce-5-2] tried to eliminate 1672 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 1 covered clauses in TOTAL during 2 rounds
c [cce-5] 1 < 1/100 * 7007 = 70 considered unsuccessful
c [score-dist-10] active 1145 (100%), one 0 (0%), zero 0 (0%)
c [score-dist-10] max exp 522, different 15 (3%)
c [score-dist-10] median active exp 521, avg 519.2
c [simplification-10] removed 0 variables 0.0% (1145 remain 40%)
c [simplification-10] removed 1 irredundant clauses 0.0% (7006 remain 72%)
c [simplification-10] maximum reduction of 0% = max (0%, 0%)
c [simplification-10] full geometric conflict interval increment 800000
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 3179988 (soft 2679988 + delta 500000)
c [simplification-10] new conflict limit 2679988 (hard 3179988)
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 -  658.0    1145     7006   1729933   44166   2232   222   10    10   14  99%   1024   -1   11   11  100%
c -  694.8    1145     7006   1815772   45643   2235   222    8     9   15  94%   1024   -1   11   10  106%
c -  716.2    1145     7006   1866408   44674   2236   222   12    12   12  98%   1024    0   11   11   98%
c -  739.4    1145     7006   1920019   45341   2236   222   10    10   16  99%   1024   -1   12   11  107%
c -  762.3    1145     7006   1974580   41716   2237   222   12    12   16  99%   1024    0   11   11  100%
c -  800.8    1145     7006   2060707   47136   2237   222   10    10   17  99%   1024   -1   10   11   94%
c -  828.7    1145     7006   2128360   48623   2239   222   11    11   17  98%   1024    1   12   11  109%
c -  858.6    1145     7006   2195285   48332   2240   222   10    10   12  99%   1024   -0   11   10  104%
c -  886.6    1145     7006   2262408   45854   2242   222   10    10   16  98%   1024   -0   11   10  107%
c -  925.7    1145     7006   2349589   48024   2245   222    9     9   16  99%   1024   -1    8    9   90%
c -  953.0    1145     7006   2414475   51008   2270   222   12    13   13  96%   1024    1   13   11  113%
c -  979.5    1145     7006   2471849   50404   2270   222   12    12   17  99%   1024    0   12   12  103%
c
c CAUGHT SIGNAL 15 SIGTERM
c
c s UNKNOWN
c bate: 0 basic ate = 0 trn 0% + 0 lrg 0% in 0 updates
c bcas: 3 count, 0 added (0 skipped), 78417 steps
c bkwd: tried 16353 clauses, 32634 lits, 2.00 lits/clause
c bkwd: checked 227691 occs, 13.92 occs/clause, 6.98 occs/lit
c bkwd: subsumed 0 binary, 3 ternary, 1 large
c bkwd: strengthened 0 binary, 0 ternary (0% self), 77 large (0% self)
c blkd: 3 bces, 2 removed, 112360 resolutions, 279082 steps
c blkd: 9 blocking literals 0%, 0 pure
c bump: 2521924 bumped seen, 1204585816 lits 477.6 on average
c card: 4 count, 0 units, 0 am1, 143633609 steps
c card: 5 rescheduled, 26 eliminated, 213857 resolved, 3858 subsumed
c card: 0 at-most-one constraints found, average size 0.00
c card: 0 at-most-one constraints used 0%, average size 0.00
c card: 9 at-most-two constraints found, average size 4.00
c card: 9 at-most-two constraints used 100%, average size 4.00
c cces: 5 cces, 251 eliminated, 245 ate 98%, 6 abce 2%
c cces: 0 probed, 0 lifted, 0 failed
c cces: 0 cached, 0 rsz, 0 cols 0%, 0 srch, 0 hits 0%
c clls: 1 sat, 0 simp, 0 freeze, 0 melt
c clls: 35848 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 44 gcs, 0 rescored clauses, 0 rescored vars
c dcps: 27 decompositions, 17 equivalent 1%
c deco: 0 decision-only clauses 0%, 0% reduction
c decs: 2554100 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 5 elims, 1661 eliminated 59%, 0 pure 0%
c elms: 11 rounds, 2.2 rounds/bve
c elms: 1661 small 100%, 0 large 0%
c elms: 7460 tried small, 1661 succeeded 22%, 5799 failed 78%
c elms: 473 subsumed, 577 strengthened, 2 blocked
c elms: 233854 copies, 279922 resolutions, 459713 ipos
c elms: 17315 subchks, 19437 strchks
c gaus: 3 extractions, 12696 extracted, 3.8 size, 4 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 2546210 steps, 1273105 extr 50%, 898636 elim 35%
c glue: 11.8 orig avg, 11.8 real avg, 3.1 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 2150 = 1190 simple 55% + 913 trn 42% + 47 lrg 2%, 3 sub 0%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 2521923 clauses, 27.1 length
c lrnd: 68386869 lits = 121634816 orig - 53247947 removed 44%
c lrnd: 24408 uips 1%, 2494993 flips 99%
c mins: 2520125 mins 100%, 10 bin 0%, 1788 size 0%
c mins: 231080957 poisoned searches, 21208746 hits, 9% hit rate
c mins: 328976697 used twice searches, 14240364 hits, 4% hit rate
c move: moved 241, 29 bin 12%, 212 trn 88%
c otfs: 397 driving 20%, 1632 restarting 80%
c otfs: str 2029, 2026 red 100%, 3 irr 0%
c otfs: str 2029, 0 bin 0%, 4 trn 0%, 2025 lrg 100%
c otfs: sub 38, 38 red 100%, 0 irr 0%
c otfs: sub 38, 0 bin 0%, 0 trn 0%, 38 lrg 100%
c phas: 1 computed, 1637 set, 1484 pos (91%), 153 neg (9%)
c prbs: 2 basic, 2940 probed, 0 failed, 0 lifted
c prbs: 3 simple, 12970 probed, 0 failed, 10 eqs
c prbs: 3 treelook, 7859 probed, 1 failed, 0 lifted
c prom: 106648 locked 1% out of 11223827 tried
c prps: 1339727150 props, 524 props/dec
c prps: 100% srch, 0% simp, 0% lkhd
c quat: 8 count, 383 quat, 690 self1, 0 self2, 0 dup
c queu: 3 sorted, 2554100 next (36793 steps 0.01)
c queu: 1204590914 enq (1331099454 steps 1.11), 1204586471 deq 100%
c redc: 308 clauses 1%, 43376 tried 2%, 0 sat 0%
c redc: 350 lits 0%, 584210 tried 0%, 0 sat 0%
c redc: 2 times jump level reduced, 1.0 levels on average
c reds: 51 count, 49416.2 conflicts per reduce
c reds: 0 memlim 0%, 51 arith 100%
c reds: 1912558 collected 91%, 181464 retired 9%
c rmbd: 95 removed, 89 red 94%
c rsts: 1040 restarts 8%, 11879 skipped 92%
c rsts: 11879 saturating 100%, 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: 10 count, 10 confs 100%, 0 vars 0%
c simp: 0 its 0%, 0 bin 0%, 0 trns 0%
c subl: 2521923 count (898649 tried 0.4), 331443 sub out of 2521118 (13.1%)
c swps: 4 count, 8 rounds, 840 queries (105.0/round)
c swps: 841 sat calls, 2 unsat (2.5% success rate)
c swps: 13563 decisions 16.1, 2097 conflicts 2.5
c swps; 38.6 avg class size, 26.7 avg environment size
c swps: 0 failed, 1 impls, 1 equivs
c swp0: 277 type 0 queries, 3 unsat (1.1%), 277 sat (100.0%)
c swp1: 563 type 1 queries, 14 unsat (2.5%), 562 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: 10152260 calls to obtain time
c tops: 12 fixed 0%, 0 its, 0.00 confs/it
c trds: 7 transitive reductions, 68 removed, 0 failed
c trds: 16069 nodes, 2191 edges, 78160 steps
c trim: 2612957 words, 10.0 MB
c trnr: 8 count, 2 bin, 651 trn, 37808433 steps
c unhd: 4 count, 12 rounds, 2150687 steps
c unhd: 4 non-trivial sccs of average size 2.0
c unhd: 0 units, 0 bin, 0 trn, 0 lrg
c unhd: 16 failed, 16 stamp, 0 lits, 0 bin, 0 trn, 0 lrg
c unhd: 412 tauts, 2 bin 0%, 35 trn 8%, 1 lrg 0%
c unhd: 412 tauts, 374 stamp 91%, 386 red 94%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 2498 str, 0 bin 0%, 72 trn 3%, 2426 lrg 97%, 2404 red 96%
c vars: 1145 remaining 40% and 1690 removed 60% out of 2835
c vars: 12 fixed 0%, 1661 eliminated 59%, 17 equivalent 1%
c vsts: 55988317359 visits, 100% srch, 0% simp, 0% lkhd
c vsts: 41.8 search visits per propagation, 22212.6 per conflict
c wchs: 7237387537 pushed, 847738 enlarged, 128 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all        2521501       1912558        181464      94961187      76918917       1112623
c 
c  0 0          8874   0      1597   0         0   0  63668520  67  49845550  65    281347  25     0.2
c  1 5         11997   0      3365   0      2267   1  15019896  16< 12473236  16<   197216  18<    0.2
c  2 6        222802   9    101724   5     36151  20  12905445  14  11206339  15    479235  43     2.4
c  3 9       1668104  66<  1263964  66<   123503  68<  2731632   3   2764491   4    151969  14     7.7
c  4 14       607236  24    539959  28     19497  11    631832   1    626451   1      2757   0     6.0
c  5 21         2457   0      1947   0        43   0      3801   0      2812   0        96   0     0.3
c  6 30           31   0         2   0         3   0        61   0        38   0         3   0     0.0
c 
c avg                  3.1           3.2           2.9           0.5           0.6           1.5
c std                  0.6           0.6           0.6           0.9           0.9           1.0
c 
c  202.547  20% bump
c    1.633   0% card
c    1.164   0% decide
c 
c    1.675 < 1% rest (below)
c 
c    0.496   0% elim
c    0.392   0% sweep
c    0.314   0% cce
c    0.204   0% unhide
c    0.203   0% probe
c    0.185   0% quatres
c    0.180   0% ternres
c    0.102   0% gauss
c    0.044   0% bca
c    0.044   0% block
c    0.007   0% transred
c    0.000   0% locs
c    0.000   0% queuesort
c    0.000   0% rescore
c ==================================
c    0.108   0% preprocessing     3%
c    4.059   0% inprocessing     97%
c ==================================
c    4.167   0% simplifying
c  995.909 100% search
c ==================================
c 1000.076 100% all
c 
c       2520224 conflicts,        2520.0 confs/sec
c           363 ternaries,        6942.8 confs/ternary
c             9 binaries,       280024.9 confs/binary
c             0 iterations,          0.0 confs/iteration
c 
c            51 reductions,          0.1 redus/sec,  49416.2 confs/reduction
c          1040 restarts,            1.0 rests/sec,   2423.3 confs/restart
c       2554100 decisions,        2553.9 decis/sec,      1.0 decis/conflict
c    1339727150 propagations,  1339625.2 props/sec,    524.5 props/decision
c 
c 1000.1 seconds, 33.2 MB
c
c CAUGHT SIGNAL 15 SIGTERM
c
c launch: done
