c launch: /data/cnf/sc2014/app/MD5-30-5.cnf.bz2
c host: atom04
c Lingeling SAT Solver
c 
c Version b7ztzu 7b29300825af9bcc1c8b2c5ebcf65fa1cb101cad
c 
c Copyright (C) 2010-2014 Armin Biere JKU Linz Austria.
c All rights reserved.
c 
c released Sun Apr 26 19:26:13 CEST 2015
c compiled Sun Apr 26 19:26:13 CEST 2015
c 
c gcc (Ubuntu 4.8.2-19ubuntu1) 4.8.2
c -Wall -O3 -I../yalsat -I../druplig -DNLGLOG -DNDEBUG -DNCHKSOL
c Linux cluster2 3.13.0-45-generic x86_64
c 
c piping '/data/cnf/sc2014/app/MD5-30-5.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/MD5-30-5.cnf.bz2
c no embedded options
c found 'p cnf 8905 68103' header
c read 8905 variables, 68103 clauses, 266105 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=3
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 8894 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] SUM (--score=3)
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    8894    67838         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 2 at-most-one constraints of average size 3.0
c [card-1] found 120 at-most-two constraints of average size 4.0
c [card-1] using previous limit 2000000 for elimination
c [card-1] 122 out of 122 constraints (100%) meet size limits
c [card-1] found 5 units
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 36 variables
c [simpleprobe-1] all 8869 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 4 variables
c [simpleprobe-1] fully completed simple probing
c [simpleprobe-1] removed 4 variables, found 328 hbrs, 0 units
c [unhide-1] limit 100000 with penalty 0 = 0 + 0
c [unhide-1-1] 0 units, 0 failed, 84 tauts, 0 hbrs, 63 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 8865 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 2596 variables 29% in round 1 in 9290438 steps
c [elim-1-1] backward subsumption/strengthening limit 9290400
c [elim-1-1-1] backward checking 6220 touched variables 70%
c [elim-1-1-1] fully completed backward checking in 1 rounds
c [elim-1-1] subsumed 46 and strengthened 100 clauses in 1295719 steps
c [elim-1-1] rescheduled 124 variables 1% by backward subsumption
c [elim-1-2] eliminated 26 variables 0% in round 2 in 314666 steps
c [elim-1-2] backward subsumption/strengthening limit 314600
c [elim-1-2-1] backward checking 118 touched variables 1%
c [elim-1-2-1] fully completed backward checking in 1 rounds
c [elim-1-2] subsumed 27 and strengthened 128 clauses in 243442 steps
c [elim-1-2] rescheduled 101 variables 1% by backward subsumption
c [elim-1-3] eliminated 2 variables 0% in round 3 in 310070 steps
c [elim-1-3] backward subsumption/strengthening limit 310000
c [elim-1-3-1] backward checking 61 touched variables 1%
c [elim-1-3-1] fully completed backward checking in 1 rounds
c [elim-1-3] subsumed 0 and strengthened 0 clauses in 164561 steps
c [elim-1] fully completed in 3 rounds
c [elim-1] transition to [ all 0 rem 0 ] state
c [elim-1] eliminated 2624 = 30% variables out of 8865 scheduled
c [phase-count-1] 64936 negative 99.1% of 65522 except 586 0.9%
c [phase-count-1] 63012 positive 96.2% of 65522 except 2510 3.8%
c [phase-count-1] less non-negative clauses 586 than limit 6500 (10.0%)
c [phase-count-1] non-pos/non-neg = 2510/586 = 4.28 >= 2.00 = 200/100
c [lucky-phase-1] forcing lucky phase -1
c [phase-1] phase bias: 0 positive 0%, 6241 negative 100%
c [sort-queue-1] sorted 6241 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 6241 (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 2653 variables 29.8% (6241 remain 70%)
c [simplification-1] removed 2316 irredundant clauses 3.4% (65522 remain 97%)
c [simplification-1] maximum reduction of 30% = max (30%, 3%)
c [simplification-1] large reduction 30% >= 5% limit
c [simplification-1] next conflict interval 1000 = 2000/2
c [simplification-1] penalized conflict interval 1000 = 1 * 1000
c [simplification-1] hard conflict limit 11000 (soft 1000 + delta 10000)
c [simplification-1] new conflict limit 1000 (hard 11000)
c 
c [simplification-2] limit 1000 conflicts (hard 11000) hit after 1000 conflicts
c [simpleprobe-2] all 6241 free variables schedulable
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [simpleprobe-2] 1690 variables remain 27% (4551 retained 73%)
c [simpleprobe-2] removed 0 variables, found 27 hbrs, 0 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 12482 literals 100%
c [treelook-1] scheduling used 300002 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 300133 steps
c [treelook-1] 9599 literals remain 77%
c [treelook-1] 5454 variables remain to probed next time 87%
c [treelook-1] removed 0 variables, found 65 hbrs
c [basicprobe-1] limit 1000000 penalty 0 = 0 + 0
c [basicprobe-1-0] 765 sched 12%, 0 failed, 0 lifted, 26 hbrs
c [basicprobe-1-1] 765 sched 12%, 0 failed, 0 lifted, 3 hbrs
c [basicprobe-1-2] 766 sched 12%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-1-2] fully completed probing
c [basicprobe-1-2] removed 0 variables, found 29 hbrs
c [block-1] scheduling all variables this time
c [block-1] scheduled 6241 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 133 blocked clauses
c [block-1] 133 < 1/100 * 65522 = 655 considered unsuccessful
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 32 clauses out of 733 (4%) of length 6
c [cce-1-1] eliminated 8161 clauses out of 25730 (32%) of length 5
c [cce-1-1] eliminated 293 clauses out of 22390 (1%) of length 4
c [cce-1-1] completed large round (ATE)
c [cce-1-1] eliminated 8486 large clauses in 11024047 steps
c [cce-1-1] allowing another 5512023 steps for small clauses
c [cce-1-1] scheduling 914 clauses = 568 binary + 346 ternary
c [cce-1-1] tried to eliminate 914 small clauses 100%
c [cce-1-1] eliminated 5 binary clauses 1%
c [cce-1-1] eliminated 46 ternary clauses 13%
c [cce-1-1] eliminated 51 small clauses 6%
c [cce-1-1] eliminated 51 small clauses in 5609189 steps
c [cce-1-1] completed small round (ATE)
c [cce-1-1] completed small and large (ATE)
c [cce-1-1] eliminated 8537 covered clauses in round 1
c [cce-1-2] eliminated 2 clauses out of 701 (0%) of length 6
c [cce-1-2] eliminated 30 clauses out of 17569 (0%) of length 5
c [cce-1-2] eliminated 35 clauses out of 22097 (0%) of length 4
c [cce-1-2] completed large round (ABCE)
c [cce-1-2] eliminated 67 large clauses in 9933746 steps
c [cce-1-2] allowing another 4966873 steps for small clauses
c [cce-1-2] scheduling 863 clauses = 563 binary + 300 ternary
c [cce-1-2] tried to eliminate 863 small clauses 100%
c [cce-1-2] completed small round (ABCE)
c [cce-1-2] completed small and large (ABCE)
c [cce-1-2] eliminated 67 covered clauses in round 2
c [cce-1-3] eliminated 9 clauses out of 17539 (0%) of length 5
c [cce-1-3] eliminated 25 clauses out of 22062 (0%) of length 4
c [cce-1-3] completed large round (ACCE)
c [cce-1-3] eliminated 34 large clauses in 11243188 steps
c [cce-1-3] allowing another 5621594 steps for small clauses
c [cce-1-3] scheduling 863 clauses = 563 binary + 300 ternary
c [cce-1-3] tried to eliminate 863 small clauses 100%
c [cce-1-3] eliminated 2 ternary clauses 1%
c [cce-1-3] eliminated 2 small clauses 0%
c [cce-1-3] eliminated 2 small clauses in 5726701 steps
c [cce-1-3] completed small round (ACCE)
c [cce-1-3] completed small and large (ACCE)
c [cce-1-3] eliminated 36 covered clauses in round 3
c [cce-1] eliminated 8640 covered clauses in TOTAL during 3 rounds
c [elim-2] scheduling all variables this time
c [elim-2] scheduled 6231 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 209 variables 3% in round 1 in 14378823 steps
c [elim-2-1] backward subsumption/strengthening limit 5621177
c [elim-2-1-1] backward checking 565 touched variables 9%
c [elim-2-1-1] fully completed backward checking in 1 rounds
c [elim-2-1] subsumed 5 and strengthened 33 clauses in 150605 steps
c [elim-2-1] rescheduled 64 variables 1% by backward subsumption
c [elim-2-2] no variable eliminated in round 2 in 185747 steps
c [elim-2] fully completed in 2 rounds
c [elim-2] transition to [ all 0 rem 0 ] state
c [elim-2] eliminated 209 = 3% variables out of 6231 scheduled
c [bca-1] limit of 10000000 steps and 110270 added (scaled 2)
c [bca-1] 10398 out of 12046 literals actually usable 86%
c [bca-1] added 0 blocked clauses in 43965 steps
c [sweep-1] limit 1000000 penalty 0 = 0 + 0
c [sweep-1-1] 2082 pos 34.6% + 3940 neg 65.4% = 6022 sched 100.0% ret 0
c [sweep-1-1] 1000269 steps 1112 queries 297.93 avg class size
c [sweep-1-1] 9642 decisions 1111 SAT calls 15.24 avg env size
c [sweep-1-1] 174 variables remain 3% (5848 retained 97%)
c [sweep-1-1] removed 0 vars (0 failed, 0 eqs, 2 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 0 vars in TOTAL (1 rounds, 1111 queries)
c [sort-queue-2] sorted 3132 enqueued variables after 1000 conflicts
c [score-dist-2] active 2890 (48%), one 0 (0%), zero 3132 (52%)
c [score-dist-2] max exp 515, different 14 (3%)
c [score-dist-2] median active exp 512, avg 511.7
c [simplification-2] removed 219 variables 3.5% (6022 remain 68%)
c [simplification-2] removed 10637 irredundant clauses 16.2% (54885 remain 81%)
c [simplification-2] maximum reduction of 16% = max (4%, 16%)
c [simplification-2] large reduction 16% >= 5% limit
c [simplification-2] next conflict interval 2000 = 2000/1
c [simplification-2] penalized conflict interval 2000 = 1 * 2000
c [simplification-2] hard conflict limit 13000 (soft 3000 + delta 10000)
c [simplification-2] new conflict limit 3000 (hard 13000)
c 
c [simplification-3] limit 3000 conflicts (hard 13000) hit after 3000 conflicts
c [quatres-1] found 22056 quaternary clauses 53% in total
c [quatres-1-2] added 256 single-self-subsuming ternary resolvents
c [quatres-1-2] added 505 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 6022 free variables schedulable
c [ternres-1] 3833 ternary resolvents (63 bin, 3770 trn)
c [ternres-1] fully completed ternary resolution
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 4 at-most-one constraints of average size 3.0
c [card-2] found 22 at-most-two constraints of average size 4.0
c [card-2] using previous limit 1000000 for elimination
c [card-2] 26 out of 26 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] generated 3 at-most-one constraints, 2 used 67%
c [card-2] exported 2 binary clauses, 1.0 per/constraint
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 12413 xors of average arity 3.5
c [gauss-1] connected 44036 occurrences of 3772 variables (average 11.7)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] exported 0 unary, 0 binary and 0 ternary equations
c [unhide-2] limit 50000 with penalty 1 = 1 + 0
c [unhide-2-2] 0 units, 0 failed, 171 tauts, 0 hbrs, 92 literals
c [transred-1] limit 100000 with penalty 0 = 0 + 0
c [transred-1] removed 25 transitive binary clauses
c [cce-2] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-2-1] eliminated 1 clauses out of 586 (0%) of length 6
c [cce-2-1] eliminated 26 clauses out of 16932 (0%) of length 5
c [cce-2-1] eliminated 73 clauses out of 21509 (0%) of length 4
c [cce-2-1] completed large round (ATE)
c [cce-2-1] eliminated 100 large clauses in 9103947 steps
c [cce-2-1] allowing another 4551973 steps for small clauses
c [cce-2-1] scheduling 892 clauses = 589 binary + 303 ternary
c [cce-2-1] tried to eliminate 892 small clauses 100%
c [cce-2-1] eliminated 7 binary clauses 1%
c [cce-2-1] eliminated 11 ternary clauses 4%
c [cce-2-1] eliminated 18 small clauses 2%
c [cce-2-1] eliminated 18 small clauses in 4644276 steps
c [cce-2-1] completed small round (ATE)
c [cce-2-1] eliminated 118 covered clauses in round 1
c [cce-2-2] completed large round (ATE)
c [cce-2-2] allowing another 4536806 steps for small clauses
c [cce-2-2] scheduling 874 clauses = 582 binary + 292 ternary
c [cce-2-2] tried to eliminate 874 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 118 covered clauses in TOTAL during 2 rounds
c [cce-2] 118 < 1/100 * 54883 = 548 considered unsuccessful
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 6022 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 139 variables 2% in round 1 in 14024829 steps
c [elim-3-1] backward subsumption/strengthening limit 5975171
c [elim-3-1-1] backward checking 212 touched variables 4%
c [elim-3-1-1] fully completed backward checking in 1 rounds
c [elim-3-1] subsumed 3 and strengthened 15 clauses in 92441 steps
c [elim-3-1] rescheduled 25 variables 0% by backward subsumption
c [elim-3-2] eliminated 4 variables 0% in round 2 in 58569 steps
c [elim-3-2] backward subsumption/strengthening limit 58500
c [elim-3-2-1] backward checking 4 touched variables 0%
c [elim-3-2-1] fully completed backward checking in 1 rounds
c [elim-3-2] subsumed 2 and strengthened 4 clauses in 47357 steps
c [elim-3-2] rescheduled 4 variables 0% by backward subsumption
c [elim-3-3] no variable eliminated in round 3 in 12485 steps
c [elim-3] fully completed in 3 rounds
c [elim-3] transition to [ all 0 rem 0 ] state
c [elim-3] eliminated 143 = 2% variables out of 6022 scheduled
c [sweep-2] limit 1000000 penalty 0 = 0 + 0
c [sweep-2-1] 71 pos 44.7% + 88 neg 55.3% = 159 sched 2.7% ret 5720
c [sweep-2-1] 27179 steps 89 queries 30.78 avg class size
c [sweep-2-1] 858 decisions 88 SAT calls 15.78 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] 2625 pos 44.7% + 3254 neg 55.3% = 5879 sched 100.0% ret 0
c [sweep-2-2] 931905 steps 1004 queries 297.18 avg class size
c [sweep-2-2] 10607 decisions 1007 SAT calls 18.05 avg env size
c [sweep-2-2] fully completed sweeping round
c [sweep-2-2] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-2-3] 2625 pos 44.7% + 3254 neg 55.3% = 5879 sched 100.0% ret 0
c [sweep-2-3] 41306 steps 32 queries 1883.12 avg class size
c [sweep-2-3] 467 decisions 31 SAT calls 23.84 avg env size
c [sweep-2-3] 5753 variables remain 98% (126 retained 2%)
c [sweep-2-3] removed 0 vars (0 failed, 0 eqs, 1 impls)
c [sweep-2] removed 0 vars in TOTAL (3 rounds, 1122 queries)
c [sort-queue-3] sorted 1630 enqueued variables after 3000 conflicts
c [score-dist-3] active 4249 (72%), one 0 (0%), zero 1630 (28%)
c [score-dist-3] max exp 518, different 14 (3%)
c [score-dist-3] median active exp 515, avg 514.6
c [simplification-3] removed 143 variables 2.4% (5879 remain 66%)
c [simplification-3] removed 1119 irredundant clauses 2.0% (53766 remain 79%)
c [simplification-3] maximum reduction of 2% = max (2%, 2%)
c [simplification-3] geometric conflict interval increment 6666 = 20000 / 3
c [simplification-3] new conflict interval 6666
c [simplification-3] penalized conflict interval 6666 = 1 * 6666
c [simplification-3] hard conflict limit 19666 (soft 9666 + delta 10000)
c [simplification-3] new conflict limit 9666 (hard 19666)
c 
c [simplification-4] limit 9666 conflicts (hard 19666) hit after 9667 conflicts
c [quatres-2] found 22569 quaternary clauses 52% in total
c [quatres-2-1] added 6 double-self-subsuming ternary resolvents
c [quatres-2-2] added 272 single-self-subsuming ternary resolvents
c [quatres-2-2] added 543 quaternary resolvents
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] all 5879 free variables schedulable
c [ternres-2] 592 ternary resolvents (2 bin, 590 trn)
c [ternres-2] fully completed ternary resolution
c [treelook-2] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-2] scheduled 5356 literals 46%
c [treelook-2] scheduling used 150007 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-2] used 150007 steps
c [treelook-2] 3852 literals remain 33%
c [treelook-2] 3183 variables remain to probed next time 54%
c [treelook-2] removed 0 variables, found 18 hbrs
c [transred-2] limit 380074 with penalty 0 = 0 + 0
c [transred-2] removed 19 transitive binary clauses
c [block-2] scheduling all variables this time
c [block-2] scheduled 5879 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 376 blocked clauses
c [block-2] 376 < 1/100 * 53766 = 537 considered unsuccessful
c [elim-4] scheduling all variables this time
c [elim-4] scheduled 5829 variables 100%
c [elim-4] boosting limit by 20
c [elim-4] limit of 400000000 steps penalty 0 = 0 + 0
c [elim-4] rescheduling of touched variables disabled
c [elim-4-1] eliminated 2 variables 0% in round 1 in 13867040 steps
c [elim-4-1] backward subsumption/strengthening limit 13867000
c [elim-4-1-1] backward checking 19 touched variables 0%
c [elim-4-1-1] fully completed backward checking in 1 rounds
c [elim-4-1] subsumed 0 and strengthened 0 clauses in 43549 steps
c [elim-4] fully completed in 1 rounds
c [elim-4] transition to [ all 0 rem 0 ] state
c [elim-4] eliminated 2 = 0% variables out of 5829 scheduled
c [elim-4] 2 < 1/100 * 5829 = 58 considered unsuccessful
c [bca-2] limit of 10000000 steps and 107234 added (scaled 2)
c [bca-2] 3111 out of 11656 literals actually usable 27%
c [bca-2] added 0 blocked clauses in 21382 steps
c [sort-queue-4] sorted 572 enqueued variables after 9667 conflicts
c [score-dist-4] active 5255 (90%), one 0 (0%), zero 572 (10%)
c [score-dist-4] max exp 523, different 18 (3%)
c [score-dist-4] median active exp 520, avg 518.9
c [simplification-4] removed 52 variables 0.9% (5827 remain 66%)
c [simplification-4] removed 399 irredundant clauses 0.7% (53367 remain 79%)
c [simplification-4] maximum reduction of 1% = max (1%, 1%)
c [simplification-4] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-4] new conflict interval 16666
c [simplification-4] penalized conflict interval 16666 = 1 * 16666
c [simplification-4] hard conflict limit 36333 (soft 26333 + delta 10000)
c [simplification-4] new conflict limit 26333 (hard 36333)
c 
c [simplification-5] limit 26333 conflicts (hard 36333) hit after 26333 conflicts
c [quatres-3] found 23079 quaternary clauses 51% in total
c [quatres-3-1] added 8 double-self-subsuming ternary resolvents
c [quatres-3-2] added 248 single-self-subsuming ternary resolvents
c [quatres-3-2] added 427 quaternary resolvents
c [ternres-3] limit 4000000 with penalty 0 = 0 + 0
c [ternres-3] all 5827 free variables schedulable
c [ternres-3] 293 ternary resolvents (2 bin, 291 trn)
c [ternres-3] fully completed ternary resolution
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] extracted 5088 xors of average arity 3.0
c [gauss-2] connected 15264 occurrences of 1293 variables (average 11.8)
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] fully completed
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [transred-3] limit 1433355 with penalty 0 = 0 + 0
c [transred-3] removed 4 transitive binary clauses
c [cce-3] limit of 15000000 steps penalty 1 = 1 + 0
c [cce-3-1] eliminated 7 clauses out of 16633 (0%) of length 5
c [cce-3-1] eliminated 66 clauses out of 21040 (0%) of length 4
c [cce-3-1] completed large round (ACCE)
c [cce-3-1] eliminated 73 large clauses in 10731350 steps
c [cce-3-1] allowing another 5365675 steps for small clauses
c [cce-3-1] scheduling 884 clauses = 582 binary + 302 ternary
c [cce-3-1] tried to eliminate 884 small clauses 100%
c [cce-3-1] eliminated 2 binary clauses 0%
c [cce-3-1] eliminated 4 ternary clauses 1%
c [cce-3-1] eliminated 6 small clauses 1%
c [cce-3-1] eliminated 6 small clauses in 5465075 steps
c [cce-3-1] completed small round (ACCE)
c [cce-3-1] eliminated 79 covered clauses in round 1
c [cce-3-2] incomplete large round (ACCE)
c [cce-3-2] allowing another 4767469 steps for small clauses
c [cce-3-2] scheduling 878 clauses = 580 binary + 298 ternary
c [cce-3-2] tried to eliminate 878 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 79 covered clauses in TOTAL during 2 rounds
c [cce-3] 79 < 1/100 * 53367 = 533 considered unsuccessful
c [sweep-3] limit 500000 penalty 1 = 1 + 0
c [sweep-3-1] 2692 pos 47.2% + 3010 neg 52.8% = 5702 sched 97.9% ret 125
c [sweep-3-1] 500867 steps 170 queries 418.95 avg class size
c [sweep-3-1] 11379 decisions 171 SAT calls 316.85 avg env size
c [sweep-3-1] 2464 variables remain 42% (3363 retained 58%)
c [sweep-3-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-3] removed 0 vars in TOTAL (1 rounds, 169 queries)
c [sort-queue-5] sorted 208 enqueued variables after 26333 conflicts
c [score-dist-5] active 5619 (96%), one 0 (0%), zero 208 (4%)
c [score-dist-5] max exp 528, different 21 (4%)
c [score-dist-5] median active exp 524, avg 523.7
c [simplification-5] removed 0 variables 0.0% (5827 remain 66%)
c [simplification-5] removed 79 irredundant clauses 0.1% (53288 remain 79%)
c [simplification-5] maximum reduction of 0% = max (0%, 0%)
c [simplification-5] full geometric conflict interval increment 20000
c [simplification-5] new conflict interval 36666
c [simplification-5] penalized conflict interval 36666 = 1 * 36666
c [simplification-5] hard conflict limit 81332 (soft 62999 + delta 18333)
c [simplification-5] new conflict limit 62999 (hard 81332)
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 -   22.7    5827    53288     62829   27011   6573   326  176   434   14  41%    625  179  184   70  265%
c 
c [simplification-6] limit 62999 conflicts (hard 81332) hit after 63000 conflicts
c [quatres-4] found 23506 quaternary clauses 49% in total
c [quatres-4-1] added 14 double-self-subsuming ternary resolvents
c [quatres-4-2] added 186 single-self-subsuming ternary resolvents
c [quatres-4-2] added 340 quaternary resolvents
c [ternres-4] limit 4617299 with penalty 0 = 0 + 0
c [ternres-4] all 5827 free variables schedulable
c [ternres-4] 217 ternary resolvents (1 bin, 216 trn)
c [ternres-4] fully completed ternary resolution
c [card-3] limit 577162 penalty 2 = 2 + 0
c [card-3] found 6 at-most-one constraints of average size 3.0
c [card-3] found 8 at-most-two constraints of average size 4.0
c [card-3] using previous limit 577162 for elimination
c [card-3] 14 out of 14 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [basicprobe-2] limit 11543248 penalty 1 = 1 + 0
c [basicprobe-2-0] 822 sched 14%, 0 failed, 0 lifted, 23 hbrs
c [basicprobe-2-1] 835 sched 14%, 0 failed, 0 lifted, 1 hbrs
c [basicprobe-2-2] 836 sched 14%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-2-2] fully completed probing
c [basicprobe-2-2] removed 0 variables, found 24 hbrs
c [unhide-3] limit 230864 with penalty 2 = 2 + 0
c [unhide-3-3] 0 units, 0 failed, 4 tauts, 0 hbrs, 19928 literals
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 10 transitive binary clauses
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 5827 variables 100%
c [elim-5] limit of 46172992 steps penalty 1 = 1 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5-1] no variable eliminated in round 1 in 13822691 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 5827 scheduled
c [sort-queue-6] sorted 140 enqueued variables after 63000 conflicts
c [score-dist-6] active 5687 (98%), one 0 (0%), zero 140 (2%)
c [score-dist-6] max exp 531, different 23 (4%)
c [score-dist-6] median active exp 528, avg 526.9
c [simplification-6] removed 0 variables 0.0% (5827 remain 66%)
c [simplification-6] removed 8 irredundant clauses 0.0% (53280 remain 79%)
c [simplification-6] maximum reduction of 0% = max (0%, 0%)
c [simplification-6] full geometric conflict interval increment 36666
c [simplification-6] new conflict interval 73332
c [simplification-6] penalized conflict interval 73332 = 1 * 73332
c [simplification-6] hard conflict limit 172998 (soft 136332 + delta 36666)
c [simplification-6] new conflict limit 136332 (hard 172998)
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 -   40.0    5827    53280    102918   32991   7053   345  242   455   17  53%    808  110  276  126  219%
c 
c [simplification-7] limit 136332 conflicts (hard 172998) hit after 136333 conflicts
c [quatres-5] found 23805 quaternary clauses 48% in total
c [quatres-5-1] added 12 double-self-subsuming ternary resolvents
c [quatres-5-2] added 111 single-self-subsuming ternary resolvents
c [quatres-5-2] added 176 quaternary resolvents
c [ternres-5] limit 11920010 with penalty 0 = 0 + 0
c [ternres-5] all 5827 free variables schedulable
c [ternres-5] 96 ternary resolvents (3 bin, 93 trn)
c [ternres-5] fully completed ternary resolution
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 0 transitive binary clauses
c [block-3] scheduling all variables this time
c [block-3] scheduled 5827 variables 100%
c [block-3] limit of 29800027 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 [bca-3] limit of 10000000 steps and 107060 added (scaled 2)
c [bca-3] 1521 out of 11656 literals actually usable 13%
c [bca-3] added 0 blocked clauses in 63735 steps
c [sort-queue-7] sorted 127 enqueued variables after 136333 conflicts
c [score-dist-7] active 5700 (98%), one 0 (0%), zero 127 (2%)
c [score-dist-7] max exp 534, different 26 (5%)
c [score-dist-7] median active exp 530, avg 529.4
c [simplification-7] removed 0 variables 0.0% (5827 remain 66%)
c [simplification-7] removed 0 irredundant clauses 0.0% (53280 remain 79%)
c [simplification-7] maximum reduction of 0% = max (0%, 0%)
c [simplification-7] full geometric conflict interval increment 73332
c [simplification-7] new conflict interval 146664
c [simplification-7] penalized conflict interval 146664 = 1 * 146664
c [simplification-7] hard conflict limit 356329 (soft 282997 + delta 73332)
c [simplification-7] new conflict limit 282997 (hard 356329)
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 -   57.2    5827    53280    141564   33802   7310   350  245   440   18  56%    904   50  291  175  166%
c -   78.9    5827    53280    186481   33461   7332   352  248   443   19  56%    964   27  224  217  103%
c -  102.4    5827    53280    246745   34445   7389   353  248   403   21  62%   1000  -12  102  261   39%
c 
c [simplification-8] limit 282997 conflicts (hard 356329) hit after 282998 conflicts
c [quatres-6] found 24052 quaternary clauses 47% in total
c [quatres-6-1] added 3 double-self-subsuming ternary resolvents
c [quatres-6-2] added 130 single-self-subsuming ternary resolvents
c [quatres-6-2] added 199 quaternary resolvents
c [ternres-6] limit 25275288 with penalty 0 = 0 + 0
c [ternres-6] all 5827 free variables schedulable
c [ternres-6] 140 ternary resolvents (3 bin, 137 trn)
c [ternres-6] fully completed ternary resolution
c [gauss-3] limit 1263764 penalty 2 = 2 + 0
c [gauss-3] extracted 5388 xors of average arity 3.0
c [gauss-3] connected 16164 occurrences of 1293 variables (average 12.5)
c [gauss-3] limit 1263764 penalty 2 = 2 + 0
c [gauss-3] fully completed
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [simpleprobe-3] 1581 schedulable variables 27%
c [simpleprobe-3] limit 50550577 penalty 1 = 1 + 0
c [simpleprobe-3] fully completed simple probing
c [simpleprobe-3] removed 0 variables, found 11 hbrs, 0 units
c [cce-4] boosting limit by 10
c [cce-4] limit of 315941110 steps penalty 2 = 2 + 0
c [cce-4-1] eliminated 7 clauses out of 16603 (0%) of length 5
c [cce-4-1] eliminated 19 clauses out of 20971 (0%) of length 4
c [cce-4-1] completed large round (ATE)
c [cce-4-1] eliminated 26 large clauses in 8878789 steps
c [cce-4-1] allowing another 4439394 steps for small clauses
c [cce-4-1] scheduling 13227 clauses = 585 binary + 12642 ternary
c [cce-4-1] tried to eliminate 13227 small clauses 100%
c [cce-4-1] eliminated 60 ternary clauses 0%
c [cce-4-1] eliminated 60 small clauses 0%
c [cce-4-1] eliminated 60 small clauses in 6312556 steps
c [cce-4-1] completed small round (ATE)
c [cce-4-1] eliminated 86 covered clauses in round 1
c [cce-4-2] completed large round (ATE)
c [cce-4-2] allowing another 4433661 steps for small clauses
c [cce-4-2] scheduling 13167 clauses = 585 binary + 12582 ternary
c [cce-4-2] tried to eliminate 13167 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 86 covered clauses in TOTAL during 2 rounds
c [cce-4] 86 < 1/100 * 53280 = 532 considered unsuccessful
c [sweep-4] limit 1895646 penalty 2 = 2 + 0
c [sweep-4-1] 1164 pos 47.2% + 1300 neg 52.8% = 2464 sched 42.3% ret 3363
c [sweep-4-1] 1206287 steps 496 queries 84.96 avg class size
c [sweep-4-1] 24604 decisions 496 SAT calls 236.01 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] 2830 pos 48.6% + 2997 neg 51.4% = 5827 sched 100.0% ret 0
c [sweep-4-2] 690166 steps 185 queries 376.69 avg class size
c [sweep-4-2] 12081 decisions 185 SAT calls 389.08 avg env size
c [sweep-4-2] 2431 variables remain 42% (3396 retained 58%)
c [sweep-4-2] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-4] removed 0 vars in TOTAL (2 rounds, 679 queries)
c [sort-queue-8] sorted 90 enqueued variables after 282998 conflicts
c [score-dist-8] active 5737 (98%), one 0 (0%), zero 90 (2%)
c [score-dist-8] max exp 536, different 28 (5%)
c [score-dist-8] median active exp 532, avg 531.5
c [simplification-8] removed 0 variables 0.0% (5827 remain 66%)
c [simplification-8] removed 86 irredundant clauses 0.2% (53194 remain 78%)
c [simplification-8] maximum reduction of 0% = max (0%, 0%)
c [simplification-8] full geometric conflict interval increment 146664
c [simplification-8] new conflict interval 293328
c [simplification-8] penalized conflict interval 293328 = 1 * 293328
c [simplification-8] hard conflict limit 722990 (soft 576326 + delta 146664)
c [simplification-8] new conflict limit 576326 (hard 722990)
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 -  116.4    5827    53194    282998   36976   7830   389  149   424   14  35%   1010    6  150  212   70%
c -  129.4    5827    53194    319440   38232   7852   389  172   437   19  39%   1016   13  182  195   94%
c -  145.3    5827    53194    358149   38193   7877   389  244   452   19  54%   1020   18  281  199  141%
c -  166.4    5827    53194    407439   38813   7905   392  341   458   25  74%   1022   13  327  239  137%
c -  185.8    5827    53194    462997   39462   7935   393  164   440   22  37%   1023   -3  109  247   44%
c -  199.7    5827    53194    502289   41913   7963   393  157   450   19  35%   1024    5  160  208   77%
c -  216.0    5827    53194    543427   42229   7975   393  259   448   25  58%   1024    1  306  211  145%
c 
c [simplification-9] limit 576326 conflicts (hard 722990) hit after 576328 conflicts
c [quatres-7] found 24460 quaternary clauses 45% in total
c [quatres-7-1] removed 1 duplicate quaternary clauses
c [quatres-7-1] added 6 double-self-subsuming ternary resolvents
c [quatres-7-2] added 133 single-self-subsuming ternary resolvents
c [quatres-7-2] added 249 quaternary resolvents
c [ternres-7] limit 51310312 with penalty 0 = 0 + 0
c [ternres-7] all 5827 free variables schedulable
c [ternres-7] 192 ternary resolvents (2 bin, 190 trn)
c [ternres-7] fully completed ternary resolution
c [transred-6] limit 1000000 with penalty 1 = 1 + 0
c [transred-6] removed 13 transitive binary clauses
c [elim-6] scheduling all variables this time
c [elim-6] scheduled 5827 variables 100%
c [elim-6] limit of 200000000 steps penalty 2 = 2 + 0
c [elim-6] rescheduling of touched variables disabled
c [elim-6-1] eliminated 1 variables 0% in round 1 in 13780140 steps
c [elim-6-1] backward subsumption/strengthening limit 13780100
c [elim-6-1-1] backward checking 12 touched variables 0%
c [elim-6-1-1] fully completed backward checking in 1 rounds
c [elim-6-1] subsumed 0 and strengthened 0 clauses in 42365 steps
c [elim-6] fully completed in 1 rounds
c [elim-6] transition to [ all 0 rem 0 ] state
c [elim-6] eliminated 1 = 0% variables out of 5827 scheduled
c [elim-6] 1 < 1/100 * 5827 = 58 considered unsuccessful
c [sort-queue-9] sorted 67 enqueued variables after 576328 conflicts
c [score-dist-9] active 5759 (99%), one 0 (0%), zero 67 (1%)
c [score-dist-9] max exp 538, different 29 (5%)
c [score-dist-9] median active exp 534, avg 533.5
c [simplification-9] removed 1 variables 0.0% (5826 remain 66%)
c [simplification-9] removed 18 irredundant clauses 0.0% (53176 remain 78%)
c [simplification-9] maximum reduction of 0% = max (0%, 0%)
c [simplification-9] full geometric conflict interval increment 293328
c [simplification-9] new conflict interval 586656
c [simplification-9] penalized conflict interval 586656 = 1 * 586656
c [simplification-9] hard conflict limit 1456312 (soft 1162984 + delta 293328)
c [simplification-9] new conflict limit 1162984 (hard 1456312)
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 -  242.8    5826    53176    603534   41981   8312   379  319   437   17  73%   1024   -6  311  268  116%
c -  265.9    5826    53176    657989   44349   8320   379  220   441   26  50%   1024   -0  206  251   82%
c -  285.5    5826    53176    703598   45222   8334   379  243   444   28  55%   1024    3  232  242   96%
c -  308.9    5826    53176    752674   46347   8342   379  257   454   25  57%   1024    8  276  248  111%
c -  332.2    5826    53176    800445   46785   8347   379  259   464   27  56%   1024   10  230  248   93%
c -  356.0    5826    53176    848855   46476   8366   379  255   458   31  56%   1024    1  258  252  103%
c -  376.3    5826    53176    897943   46799   8376   380  281   446   29  63%   1024   -9  286  262  109%
c -  419.7    5826    53176    994989   48199   8403   381  194   448   20  43%   1024   10  191  307   62%
c -  438.4    5826    53176   1042078   50537   8415   381  190   449   24  42%   1024    6  180  250   72%
c -  461.6    5826    53176   1090541   51452   8424   381  227   448   34  51%   1024    2  233  234  100%
c -  482.4    5826    53176   1137734   51797   8436   381  178   448   35  40%   1024    1  175  219   80%
c 
c [simplification-10] limit 1162984 conflicts (hard 1456312) hit after 1162984 conflicts
c [quatres-8] found 24851 quaternary clauses 43% in total
c [quatres-8-1] added 3 double-self-subsuming ternary resolvents
c [quatres-8-2] added 128 single-self-subsuming ternary resolvents
c [quatres-8-2] added 189 quaternary resolvents
c [ternres-8] limit 117124678 with penalty 0 = 0 + 0
c [ternres-8] all 5826 free variables schedulable
c [ternres-8] 107 ternary resolvents (2 bin, 105 trn)
c [ternres-8] fully completed ternary resolution
c [card-4] limit 7320292 penalty 3 = 3 + 0
c [card-4] found 8 at-most-one constraints of average size 3.0
c [card-4] found 13 at-most-two constraints of average size 4.0
c [card-4] using previous limit 7320292 for elimination
c [card-4] 21 out of 21 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] generated 2 at-most-one constraints, 0 used 0%
c [card-4] exported 0 binary clauses, 0.0 per/constraint
c [unhide-4] limit 1250000 with penalty 4 = 3 + 1
c [unhide-4-5] 0 units, 0 failed, 204 tauts, 0 hbrs, 67212 literals
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 6 transitive binary clauses
c [sort-queue-10] sorted 48 enqueued variables after 1162984 conflicts
c [score-dist-10] active 5778 (99%), one 0 (0%), zero 48 (1%)
c [score-dist-10] max exp 540, different 31 (6%)
c [score-dist-10] median active exp 536, avg 535.5
c [simplification-10] removed 0 variables 0.0% (5826 remain 66%)
c [simplification-10] removed 1 irredundant clauses 0.0% (53175 remain 78%)
c [simplification-10] maximum reduction of 0% = max (0%, 0%)
c [simplification-10] full geometric conflict interval increment 586656
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 2662984 (soft 2162984 + delta 500000)
c [simplification-10] new conflict limit 2162984 (hard 2662984)
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 -  507.8    5826    53175   1186986   52542   8493   383  218   456   30  48%   1024    6  196  217   91%
c -  537.2    5826    53175   1241134   51119   8499   383  252   455   35  55%   1024   -0  239  235  101%
c -  574.9    5826    53175   1312716   51358   8514   383  299   452   30  66%   1024   -3  295  283  104%
c -  637.8    5826    53175   1419239   54196   8520   386  321   443   27  72%   1024   -5  263  327   80%
c -  687.7    5826    53175   1501395   55694   8528   386  334   444   36  75%   1024   -1  275  322   85%
c -  722.3    5826    53175   1563138   56815   8538   386  275   447   37  61%   1024    1  253  293   86%
c -  769.0    5826    53175   1633735   57535   8547   386  258   447   33  58%   1024    1  244  293   83%
c -  817.5    5826    53175   1710198   57396   8573   387  267   462   40  58%   1024   13  253  295   86%
c -  838.8    5826    53175   1760442   57798   8580   387  256   449   38  57%   1024   -3  236  277   85%
c -  887.0    5826    53175   1869242   57276   8588   387  326   421   34  77%   1024  -12  321  353   91%
c -  910.3    5826    53175   1924998   61310   8600   388  183   424   28  43%   1024   -5  169  259   65%
c -  934.6    5826    53175   1978418   62247   8603   388  219   427   37  51%   1024   -1  247  225  110%
c -  965.3    5826    53175   2036188   62013   8608   388  248   435   41  57%   1024    3  283  227  125%
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 (66 skipped), 129082 steps
c bkwd: tried 19306 clauses, 38377 lits, 1.99 lits/clause
c bkwd: checked 641790 occs, 33.24 occs/clause, 16.72 occs/lit
c bkwd: subsumed 0 binary, 5 ternary, 78 large
c bkwd: strengthened 0 binary, 0 ternary (0% self), 280 large (0% self)
c blkd: 3 bces, 509 removed, 1572163 resolutions, 3286512 steps
c blkd: 150 blocking literals 1%, 60 pure
c bump: 2107584 bumped seen, 1283209305 lits 608.9 on average
c card: 4 count, 5 units, 2 am1, 75595698 steps
c card: 65 rescheduled, 297 eliminated, 123849 resolved, 2071 subsumed
c card: 20 at-most-one constraints found, average size 3.00
c card: 20 at-most-one constraints used 100%, average size 3.00
c card: 163 at-most-two constraints found, average size 4.00
c card: 163 at-most-two constraints used 100%, average size 4.00
c cces: 4 cces, 8923 eliminated, 8820 ate 99%, 103 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: 334208 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 40 gcs, 0 rescored clauses, 0 rescored vars
c dcps: 26 decompositions, 24 equivalent 0%
c deco: 775592 decision-only clauses 37%, 46% reduction
c decs: 10958528 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 6 elims, 3039 eliminated 34%, 5 pure 0%
c elms: 14 rounds, 2.3 rounds/bve
c elms: 2974 small 98%, 0 large 0%
c elms: 24274 tried small, 2974 succeeded 12%, 21300 failed 88%
c elms: 674 subsumed, 781 strengthened, 0 blocked
c elms: 1935468 copies, 3609068 resolutions, 2368200 ipos
c elms: 65962 subchks, 61926 strchks
c gaus: 3 extractions, 22889 extracted, 3.3 size, 4 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 8527682 steps, 4263841 extr 50%, 2649572 elim 31%
c glue: 257.5 orig avg, 257.5 real avg, 10.3 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 548 = 366 simple 67% + 171 trn 31% + 11 lrg 2%, 18 sub 3%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 2107584 clauses, 345.4 length
c lrnd: 727902121 lits = 1031528230 orig - 303626109 removed 29%
c lrnd: 656697 uips 31%, 1218707 flips 58%
c mins: 884102 mins 53%, 16 bin 0%, 8941 size 1%
c mins: 112204852 poisoned searches, 8860330 hits, 8% hit rate
c mins: 220232681 used twice searches, 68548507 hits, 31% hit rate
c move: moved 394, 16 bin 4%, 378 trn 96%
c otfs: 4842 driving 15%, 26691 restarting 85%
c otfs: str 31533, 31353 red 99%, 180 irr 1%
c otfs: str 31533, 0 bin 0%, 109 trn 0%, 31424 lrg 100%
c otfs: sub 221, 220 red 100%, 1 irr 0%
c otfs: sub 221, 0 bin 0%, 12 trn 5%, 209 lrg 95%
c phas: 1 computed, 6241 set, 0 pos (0%), 6241 neg (100%)
c prbs: 2 basic, 9578 probed, 0 failed, 0 lifted
c prbs: 3 simple, 30990 probed, 0 failed, 15 eqs
c prbs: 2 treelook, 4387 probed, 0 failed, 0 lifted
c prom: 85161 locked 2% out of 5570409 tried
c prps: 1129749615 props, 103 props/dec
c prps: 100% srch, 0% simp, 0% lkhd
c quat: 8 count, 2628 quat, 1464 self1, 52 self2, 1 dup
c queu: 10 sorted, 10958528 next (254364 steps 0.02)
c queu: 1283230465 enq (2663265584 steps 2.08), 1283209305 deq 100%
c redc: 72 clauses 0%, 33281 tried 2%, 0 sat 0%
c redc: 73 lits 0%, 332615 tried 0%, 0 sat 0%
c redc: 1 times jump level reduced, 82.0 levels on average
c reds: 36 count, 58640.9 conflicts per reduce
c reds: 0 memlim 0%, 36 arith 100%
c reds: 1215653 collected 91%, 116309 retired 9%
c rmbd: 73 removed, 73 red 100%
c rsts: 16298 restarts 90%, 1905 skipped 10%
c rsts: 1905 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: 2107584 count (7777750 tried 3.7), 674998 sub out of 2105341 (32.1%)
c swps: 4 count, 7 rounds, 3081 queries (440.1/round)
c swps: 3089 sat calls, 8 unsat (0.4% success rate)
c swps: 69638 decisions 22.5, 1354 conflicts 0.4
c swps; 284.2 avg class size, 90.8 avg environment size
c swps: 0 failed, 3 impls, 0 equivs
c swp0: 1025 type 0 queries, 9 unsat (0.9%), 1025 sat (100.0%)
c swp1: 2056 type 1 queries, 63 unsat (3.1%), 2056 sat (100.0%)
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: 26132422 calls to obtain time
c tops: 16 fixed 0%, 0 its, 0.00 confs/it
c trds: 7 transitive reductions, 77 removed, 0 failed
c trds: 81739 nodes, 6529 edges, 9942 steps
c trim: 85748 words, 0.3 MB
c trnr: 8 count, 78 bin, 5392 trn, 13173722 steps
c unhd: 4 count, 5 rounds, 2004571 steps
c unhd: 0 non-trivial sccs of average size 0.0
c unhd: 0 units, 0 bin, 0 trn, 0 lrg
c unhd: 0 failed, 0 stamp, 0 lits, 0 bin, 0 trn, 0 lrg
c unhd: 463 tauts, 0 bin 0%, 425 trn 92%, 26 lrg 6%
c unhd: 463 tauts, 12 stamp 3%, 420 red 91%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 87295 str, 0 bin 0%, 122 trn 0%, 87173 lrg 100%, 87191 red 100%
c vars: 5826 remaining 65% and 3079 removed 35% out of 8905
c vars: 16 fixed 0%, 3039 eliminated 34%, 24 equivalent 0%
c vsts: 24514987200 visits, 100% srch, 0% simp, 0% lkhd
c vsts: 21.7 search visits per propagation, 11611.1 per conflict
c wchs: 5124935084 pushed, 4036034 enlarged, 86 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all        2107969       1215653        116309     266807018      80822375       1031349
c 
c  0 0         25817   1      1204   0         0   0 120219292  45  27077857  34    240945  23     0.8
c  1 5          8182   0      2299   0      3531   3  25191327   9   6473041   8     54827   5     0.1
c  2 6         22134   1      8799   1      8393   7  31494938  12<  9409646  12     82233   8     0.3
c  3 9         36078   2     20396   2      9770   8  32324300  12  10093014  12<    95326   9     0.5
c  4 14        45728   2     31632   3      8557   7  19485370   7   7147361   9     78172   8     0.7
c  5 21        52659   2     40516   3      7256   6  11925322   4   5101459   6     65952   6<    0.9
c  6 30        56671   3     46561   4      5693   5   8456828   3   3894970   5     55280   5     1.1
c  7 41        62218   3     53280   4      4891   4   4591140   2   2329858   3     38570   4     1.5
c  8 54        68210   3     60493   5      4172   4<  3000637   1   1789878   2     29715   3     1.8
c  9 69        72709   3     65243   5      3964   3   1824302   1   1180357   1     25034   2     2.5
c 10 86       161213   8<   146727  12<     7563   7   2419532   1   1649841   2     38110   4     8.0
c 11 126      385509  18    356301  29     14480  12   2515320   1   1891159   2     69009   7    31.8
c 12 230     1110841  53    382202  31     38039  33   3358710   1   2783934   3    158176  15   175.7
c 
c avg                 10.3          10.0           8.2           2.0           3.0           5.1
c std                  2.7           2.5           3.8           2.6           3.3           4.4
c 
c  251.380  25% bump
c    6.781   1% decide
c    3.240   0% elim
c 
c    5.118 < 1% rest (below)
c 
c    1.769   0% cce
c    1.092   0% unhide
c    1.005   0% card
c    0.947   0% sweep
c    0.679   0% probe
c    0.412   0% quatres
c    0.372   0% gauss
c    0.303   0% block
c    0.184   0% bca
c    0.113   0% ternres
c    0.011   0% transred
c    0.000   0% locs
c    0.000   0% queuesort
c    0.000   0% rescore
c ==================================
c    0.758   0% preprocessing     7%
c   10.860   1% inprocessing     93%
c ==================================
c   11.618   1% simplifying
c  988.377  99% search
c ==================================
c  999.995 100% all
c 
c       2111072 conflicts,        2111.1 confs/sec
c          1982 ternaries,        1065.1 confs/ternary
c            27 binaries,        78187.9 confs/binary
c             0 iterations,          0.0 confs/iteration
c 
c            36 reductions,          0.0 redus/sec,  58640.9 confs/reduction
c         16298 restarts,           16.3 rests/sec,    129.5 confs/restart
c      10958528 decisions,       10958.6 decis/sec,      5.2 decis/conflict
c    1129749615 propagations,  1129755.5 props/sec,    103.1 props/decision
c 
c 1000.0 seconds, 400.0 MB
c
c CAUGHT SIGNAL 15 SIGTERM
c
c launch: done
