c launch: /data/cnf/sc2014/app/MD5-30-1.cnf.bz2
c host: atom25
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-1.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/MD5-30-1.cnf.bz2
c no embedded options
c found 'p cnf 8906 68106' header
c read 8906 variables, 68106 clauses, 266112 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 8895 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    8895    67841         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 4 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] 124 out of 124 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 8870 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 7 variables
c [simpleprobe-1] fully completed simple probing
c [simpleprobe-1] removed 7 variables, found 333 hbrs, 1 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 8863 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 2573 variables 29% in round 1 in 9454970 steps
c [elim-1-1] backward subsumption/strengthening limit 9454900
c [elim-1-1-1] backward checking 6201 touched variables 70%
c [elim-1-1-1] fully completed backward checking in 1 rounds
c [elim-1-1] subsumed 33 and strengthened 77 clauses in 1278436 steps
c [elim-1-1] rescheduled 130 variables 1% by backward subsumption
c [elim-1-2] eliminated 23 variables 0% in round 2 in 338216 steps
c [elim-1-2] backward subsumption/strengthening limit 338200
c [elim-1-2-1] backward checking 120 touched variables 1%
c [elim-1-2-1] fully completed backward checking in 1 rounds
c [elim-1-2] subsumed 22 and strengthened 99 clauses in 225469 steps
c [elim-1-2] rescheduled 105 variables 1% by backward subsumption
c [elim-1-3] eliminated 1 variables 0% in round 3 in 306226 steps
c [elim-1-3] backward subsumption/strengthening limit 306200
c [elim-1-3-1] backward checking 42 touched variables 0%
c [elim-1-3-1] fully completed backward checking in 1 rounds
c [elim-1-3] subsumed 0 and strengthened 0 clauses in 151548 steps
c [elim-1] fully completed in 3 rounds
c [elim-1] transition to [ all 0 rem 0 ] state
c [elim-1] eliminated 2597 = 29% variables out of 8863 scheduled
c [phase-count-1] 64951 negative 99.1% of 65535 except 584 0.9%
c [phase-count-1] 63020 positive 96.2% of 65535 except 2515 3.8%
c [phase-count-1] less non-negative clauses 584 than limit 6500 (10.0%)
c [phase-count-1] non-pos/non-neg = 2515/584 = 4.31 >= 2.00 = 200/100
c [lucky-phase-1] forcing lucky phase -1
c [phase-1] phase bias: 0 positive 0%, 6266 negative 100%
c [sort-queue-1] sorted 6266 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 6266 (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 2629 variables 29.6% (6266 remain 70%)
c [simplification-1] removed 2306 irredundant clauses 3.4% (65535 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 6266 free variables schedulable
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [simpleprobe-2] 2990 variables remain 48% (3276 retained 52%)
c [simpleprobe-2] removed 0 variables, found 25 hbrs, 0 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 12532 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 300143 steps
c [treelook-1] 9554 literals remain 76%
c [treelook-1] 6184 variables remain to probed next time 99%
c [treelook-1] removed 0 variables, found 46 hbrs
c [basicprobe-1] limit 1000000 penalty 0 = 0 + 0
c [basicprobe-1-0] 734 sched 12%, 0 failed, 0 lifted, 50 hbrs
c [basicprobe-1-1] 752 sched 12%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-1-1] fully completed probing
c [basicprobe-1-1] removed 0 variables, found 50 hbrs
c [block-1] scheduling all variables this time
c [block-1] scheduled 6266 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 * 65535 = 655 considered unsuccessful
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 20 clauses out of 685 (3%) of length 6
c [cce-1-1] eliminated 8335 clauses out of 25759 (32%) of length 5
c [cce-1-1] eliminated 264 clauses out of 22354 (1%) of length 4
c [cce-1-1] completed large round (ATE)
c [cce-1-1] eliminated 8619 large clauses in 10890955 steps
c [cce-1-1] allowing another 5445477 steps for small clauses
c [cce-1-1] scheduling 14708 clauses = 557 binary + 14151 ternary
c [cce-1-1] tried to eliminate 14708 small clauses 100%
c [cce-1-1] eliminated 5 binary clauses 1%
c [cce-1-1] eliminated 339 ternary clauses 2%
c [cce-1-1] eliminated 344 small clauses 2%
c [cce-1-1] eliminated 344 small clauses in 7466460 steps
c [cce-1-1] completed small round (ATE)
c [cce-1-1] completed small and large (ATE)
c [cce-1-1] eliminated 8963 covered clauses in round 1
c [cce-1-2] eliminated 30 clauses out of 17424 (0%) of length 5
c [cce-1-2] eliminated 35 clauses out of 22090 (0%) of length 4
c [cce-1-2] completed large round (ABCE)
c [cce-1-2] eliminated 65 large clauses in 9810821 steps
c [cce-1-2] allowing another 4905410 steps for small clauses
c [cce-1-2] scheduling 14364 clauses = 552 binary + 13812 ternary
c [cce-1-2] tried to eliminate 14364 small clauses 100%
c [cce-1-2] eliminated 2 ternary clauses 0%
c [cce-1-2] eliminated 2 small clauses 0%
c [cce-1-2] eliminated 2 small clauses in 6976449 steps
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 17394 (0%) of length 5
c [cce-1-3] eliminated 28 clauses out of 22055 (0%) of length 4
c [cce-1-3] completed large round (ACCE)
c [cce-1-3] eliminated 37 large clauses in 11103823 steps
c [cce-1-3] allowing another 5551911 steps for small clauses
c [cce-1-3] scheduling 14362 clauses = 552 binary + 13810 ternary
c [cce-1-3] tried to eliminate 14362 small clauses 100%
c [cce-1-3] eliminated 12 ternary clauses 0%
c [cce-1-3] eliminated 12 small clauses 0%
c [cce-1-3] eliminated 12 small clauses in 7820573 steps
c [cce-1-3] completed small round (ACCE)
c [cce-1-3] completed small and large (ACCE)
c [cce-1-3] eliminated 49 covered clauses in round 3
c [cce-1] eliminated 9079 covered clauses in TOTAL during 3 rounds
c [elim-2] scheduling all variables this time
c [elim-2] scheduled 6256 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 189 variables 3% in round 1 in 14177590 steps
c [elim-2-1] backward subsumption/strengthening limit 5822410
c [elim-2-1-1] backward checking 507 touched variables 8%
c [elim-2-1-1] fully completed backward checking in 1 rounds
c [elim-2-1] subsumed 1 and strengthened 23 clauses in 127581 steps
c [elim-2-1] rescheduled 45 variables 1% by backward subsumption
c [elim-2-2] no variable eliminated in round 2 in 126717 steps
c [elim-2] fully completed in 2 rounds
c [elim-2] transition to [ all 0 rem 0 ] state
c [elim-2] eliminated 189 = 3% variables out of 6256 scheduled
c [bca-1] limit of 10000000 steps and 110014 added (scaled 2)
c [bca-1] 10522 out of 12136 literals actually usable 87%
c [bca-1] added 0 blocked clauses in 43641 steps
c [sweep-1] limit 1000000 penalty 0 = 0 + 0
c [sweep-1-1] 2221 pos 36.6% + 3846 neg 63.4% = 6067 sched 100.0% ret 0
c [sweep-1-1] 1000146 steps 1116 queries 369.76 avg class size
c [sweep-1-1] 9773 decisions 1119 SAT calls 15.45 avg env size
c [sweep-1-1] 141 variables remain 2% (5926 retained 98%)
c [sweep-1-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 0 vars in TOTAL (1 rounds, 1115 queries)
c [sort-queue-2] sorted 3067 enqueued variables after 1000 conflicts
c [score-dist-2] active 3000 (49%), one 0 (0%), zero 3067 (51%)
c [score-dist-2] max exp 506, different 6 (1%)
c [score-dist-2] median active exp 503, avg 503.2
c [simplification-2] removed 199 variables 3.2% (6067 remain 68%)
c [simplification-2] removed 10778 irredundant clauses 16.4% (54757 remain 81%)
c [simplification-2] maximum reduction of 16% = max (3%, 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 22157 quaternary clauses 53% in total
c [quatres-1-1] added 2 double-self-subsuming ternary resolvents
c [quatres-1-2] added 289 single-self-subsuming ternary resolvents
c [quatres-1-2] added 434 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 6067 free variables schedulable
c [ternres-1] 3901 ternary resolvents (27 bin, 3874 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 9 at-most-two constraints of average size 4.0
c [card-2] using previous limit 1000000 for elimination
c [card-2] 9 out of 9 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] generated 1 at-most-one constraints, 1 used 100%
c [card-2] exported 1 binary clauses, 1.0 per/constraint
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 12673 xors of average arity 3.5
c [gauss-1] connected 44660 occurrences of 3825 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 [decomp-8] removed 1 variables
c [unhide-2] limit 50000 with penalty 1 = 1 + 0
c [unhide-2-2] 0 units, 0 failed, 96 tauts, 0 hbrs, 160 literals
c [transred-1] limit 105937 with penalty 0 = 0 + 0
c [transred-1] removed 18 transitive binary clauses
c [cce-2] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-2-1] eliminated 10 clauses out of 16817 (0%) of length 5
c [cce-2-1] eliminated 32 clauses out of 21587 (0%) of length 4
c [cce-2-1] completed large round (ATE)
c [cce-2-1] eliminated 42 large clauses in 8998287 steps
c [cce-2-1] allowing another 4499143 steps for small clauses
c [cce-2-1] scheduling 13865 clauses = 585 binary + 13280 ternary
c [cce-2-1] tried to eliminate 13865 small clauses 100%
c [cce-2-1] eliminated 5 binary clauses 1%
c [cce-2-1] eliminated 11 ternary clauses 0%
c [cce-2-1] eliminated 16 small clauses 0%
c [cce-2-1] eliminated 16 small clauses in 6432173 steps
c [cce-2-1] completed small round (ATE)
c [cce-2-1] eliminated 58 covered clauses in round 1
c [cce-2-2] completed large round (ATE)
c [cce-2-2] allowing another 4496418 steps for small clauses
c [cce-2-2] scheduling 13849 clauses = 580 binary + 13269 ternary
c [cce-2-2] tried to eliminate 13849 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 58 covered clauses in TOTAL during 2 rounds
c [cce-2] 58 < 1/100 * 54756 = 547 considered unsuccessful
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 6066 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 142 variables 2% in round 1 in 13867275 steps
c [elim-3-1] backward subsumption/strengthening limit 6132725
c [elim-3-1-1] backward checking 214 touched variables 4%
c [elim-3-1-1] fully completed backward checking in 1 rounds
c [elim-3-1] subsumed 0 and strengthened 8 clauses in 85332 steps
c [elim-3-1] rescheduled 15 variables 0% by backward subsumption
c [elim-3-2] no variable eliminated in round 2 in 58251 steps
c [elim-3] fully completed in 2 rounds
c [elim-3] transition to [ all 0 rem 0 ] state
c [elim-3] eliminated 142 = 2% variables out of 6066 scheduled
c [sweep-2] limit 1000000 penalty 0 = 0 + 0
c [sweep-2-1] 56 pos 44.8% + 69 neg 55.2% = 125 sched 2.1% ret 5799
c [sweep-2-1] 20702 steps 75 queries 25.79 avg class size
c [sweep-2-1] 605 decisions 74 SAT calls 13.53 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] 2745 pos 46.3% + 3179 neg 53.7% = 5924 sched 100.0% ret 0
c [sweep-2-2] 967097 steps 995 queries 266.48 avg class size
c [sweep-2-2] 11983 decisions 996 SAT calls 19.45 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] 2745 pos 46.3% + 3179 neg 53.7% = 5924 sched 100.0% ret 0
c [sweep-2-3] 12866 steps 13 queries 2246.31 avg class size
c [sweep-2-3] 126 decisions 12 SAT calls 18.00 avg env size
c [sweep-2-3] 5900 variables remain 100% (24 retained 0%)
c [sweep-2-3] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-2] removed 0 vars in TOTAL (3 rounds, 1080 queries)
c [sort-queue-3] sorted 956 enqueued variables after 3000 conflicts
c [score-dist-3] active 4968 (84%), one 0 (0%), zero 956 (16%)
c [score-dist-3] max exp 507, different 7 (1%)
c [score-dist-3] median active exp 505, avg 504.4
c [simplification-3] removed 143 variables 2.4% (5924 remain 67%)
c [simplification-3] removed 1113 irredundant clauses 2.0% (53644 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 9666 conflicts
c [quatres-2] found 22331 quaternary clauses 53% in total
c [quatres-2-1] added 1 double-self-subsuming ternary resolvents
c [quatres-2-2] added 228 single-self-subsuming ternary resolvents
c [quatres-2-2] added 502 quaternary resolvents
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] all 5924 free variables schedulable
c [ternres-2] 553 ternary resolvents (5 bin, 548 trn)
c [ternres-2] fully completed ternary resolution
c [treelook-2] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-2] scheduled 5736 literals 48%
c [treelook-2] scheduling used 150038 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-2] used 150084 steps
c [treelook-2] 4153 literals remain 35%
c [treelook-2] 4006 variables remain to probed next time 68%
c [treelook-2] removed 0 variables, found 6 hbrs
c [transred-2] limit 434271 with penalty 0 = 0 + 0
c [transred-2] removed 10 transitive binary clauses
c [block-2] scheduling all variables this time
c [block-2] scheduled 5924 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 438 blocked clauses
c [block-2] 438 < 1/100 * 53644 = 536 considered unsuccessful
c [elim-4] scheduling all variables this time
c [elim-4] scheduled 5866 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 1 variables 0% in round 1 in 13689455 steps
c [elim-4-1] backward subsumption/strengthening limit 13689400
c [elim-4-1-1] backward checking 6 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 40298 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 5866 scheduled
c [elim-4] 1 < 1/100 * 5866 = 58 considered unsuccessful
c [bca-2] limit of 10000000 steps and 106878 added (scaled 2)
c [bca-2] 3272 out of 11732 literals actually usable 28%
c [bca-2] added 0 blocked clauses in 22261 steps
c [sort-queue-4] sorted 680 enqueued variables after 9666 conflicts
c [score-dist-4] active 5185 (88%), one 0 (0%), zero 680 (12%)
c [score-dist-4] max exp 511, different 11 (2%)
c [score-dist-4] median active exp 508, avg 507.7
c [simplification-4] removed 59 variables 1.0% (5865 remain 66%)
c [simplification-4] removed 455 irredundant clauses 0.8% (53189 remain 78%)
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 36332 (soft 26332 + delta 10000)
c [simplification-4] new conflict limit 26332 (hard 36332)
c 
c [simplification-5] limit 26332 conflicts (hard 36332) hit after 26333 conflicts
c [quatres-3] found 22556 quaternary clauses 52% in total
c [quatres-3-1] added 2 double-self-subsuming ternary resolvents
c [quatres-3-2] added 122 single-self-subsuming ternary resolvents
c [quatres-3-2] added 322 quaternary resolvents
c [ternres-3] limit 4000000 with penalty 0 = 0 + 0
c [ternres-3] all 5865 free variables schedulable
c [ternres-3] 175 ternary resolvents (3 bin, 172 trn)
c [ternres-3] fully completed ternary resolution
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] extracted 5769 xors of average arity 3.0
c [gauss-2] connected 17307 occurrences of 1420 variables (average 12.2)
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 1737721 with penalty 0 = 0 + 0
c [transred-3] removed 3 transitive binary clauses
c [cce-3] limit of 15000000 steps penalty 1 = 1 + 0
c [cce-3-1] eliminated 1 clauses out of 16515 (0%) of length 5
c [cce-3-1] eliminated 24 clauses out of 20970 (0%) of length 4
c [cce-3-1] completed large round (ACCE)
c [cce-3-1] eliminated 25 large clauses in 10601776 steps
c [cce-3-1] allowing another 5300888 steps for small clauses
c [cce-3-1] scheduling 13304 clauses = 556 binary + 12748 ternary
c [cce-3-1] tried to eliminate 13304 small clauses 100%
c [cce-3-1] eliminated 1 binary clauses 0%
c [cce-3-1] eliminated 2 ternary clauses 0%
c [cce-3-1] eliminated 3 small clauses 0%
c [cce-3-1] eliminated 3 small clauses in 7423589 steps
c [cce-3-1] completed small round (ACCE)
c [cce-3-1] eliminated 28 covered clauses in round 1
c [cce-3-2] incomplete large round (ACCE)
c [cce-3-2] allowing another 3788210 steps for small clauses
c [cce-3-2] scheduling 13301 clauses = 555 binary + 12746 ternary
c [cce-3-2] tried to eliminate 13301 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 28 covered clauses in TOTAL during 2 rounds
c [cce-3] 28 < 1/100 * 53189 = 531 considered unsuccessful
c [sweep-3] limit 500000 penalty 1 = 1 + 0
c [sweep-3-1] 2784 pos 47.6% + 3060 neg 52.4% = 5844 sched 99.6% ret 21
c [sweep-3-1] 502446 steps 159 queries 386.45 avg class size
c [sweep-3-1] 10967 decisions 158 SAT calls 448.19 avg env size
c [sweep-3-1] 2880 variables remain 49% (2985 retained 51%)
c [sweep-3-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-3] removed 0 vars in TOTAL (1 rounds, 158 queries)
c [sort-queue-5] sorted 475 enqueued variables after 26333 conflicts
c [score-dist-5] active 5390 (92%), one 0 (0%), zero 475 (8%)
c [score-dist-5] max exp 514, different 14 (3%)
c [score-dist-5] median active exp 511, avg 510.1
c [simplification-5] removed 0 variables 0.0% (5865 remain 66%)
c [simplification-5] removed 28 irredundant clauses 0.1% (53161 remain 78%)
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 [simplification-6] limit 62999 conflicts (hard 81332) hit after 63001 conflicts
c [quatres-4] found 22854 quaternary clauses 51% in total
c [quatres-4-1] added 13 double-self-subsuming ternary resolvents
c [quatres-4-2] added 71 single-self-subsuming ternary resolvents
c [quatres-4-2] added 228 quaternary resolvents
c [ternres-4] limit 5922927 with penalty 0 = 0 + 0
c [ternres-4] all 5865 free variables schedulable
c [ternres-4] 95 ternary resolvents (3 bin, 92 trn)
c [ternres-4] fully completed ternary resolution
c [card-3] limit 740365 penalty 2 = 2 + 0
c [card-3] no at-most-one constraint found
c [card-3] found 8 at-most-two constraints of average size 4.0
c [card-3] using previous limit 740365 for elimination
c [card-3] 8 out of 8 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [basicprobe-2] limit 14807319 penalty 1 = 1 + 0
c [basicprobe-2-0] 823 sched 14%, 0 failed, 0 lifted, 17 hbrs
c [basicprobe-2-1] 835 sched 14%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-2-1] fully completed probing
c [basicprobe-2-1] removed 0 variables, found 17 hbrs
c [unhide-3] limit 148073 with penalty 3 = 2 + 1
c [unhide-3-3] 0 units, 0 failed, 2 tauts, 0 hbrs, 80364 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 5865 variables 100%
c [elim-5] limit of 59229277 steps penalty 1 = 1 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5-1] no variable eliminated in round 1 in 13667879 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 5865 scheduled
c [sort-queue-6] sorted 275 enqueued variables after 63001 conflicts
c [score-dist-6] active 5590 (95%), one 0 (0%), zero 275 (5%)
c [score-dist-6] max exp 516, different 16 (3%)
c [score-dist-6] median active exp 513, avg 512.1
c [simplification-6] removed 0 variables 0.0% (5865 remain 66%)
c [simplification-6] removed 9 irredundant clauses 0.0% (53152 remain 78%)
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 172999 (soft 136333 + delta 36666)
c [simplification-6] new conflict limit 136333 (hard 172999)
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 -   32.1    5865    53152     65248   26278   6135   366  262   475   17  55%    640  194  246  112  219%
c -   55.2    5865    53152    112281   30004   6173   366  316   454   19  70%    836   82  330  192  171%
c 
c [simplification-7] limit 136333 conflicts (hard 172999) hit after 136333 conflicts
c [quatres-5] found 23066 quaternary clauses 51% in total
c [quatres-5-1] added 7 double-self-subsuming ternary resolvents
c [quatres-5-2] added 81 single-self-subsuming ternary resolvents
c [quatres-5-2] added 124 quaternary resolvents
c [ternres-5] limit 14397513 with penalty 0 = 0 + 0
c [ternres-5] all 5865 free variables schedulable
c [ternres-5] 53 ternary resolvents (3 bin, 50 trn)
c [ternres-5] fully completed ternary resolution
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 3 transitive binary clauses
c [block-3] scheduling all variables this time
c [block-3] scheduled 5865 variables 100%
c [block-3] limit of 35993783 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 106804 added (scaled 2)
c [bca-3] 2351 out of 11732 literals actually usable 20%
c [bca-3] added 0 blocked clauses in 55682 steps
c [sort-queue-7] sorted 207 enqueued variables after 136333 conflicts
c [score-dist-7] active 5658 (96%), one 0 (0%), zero 207 (4%)
c [score-dist-7] max exp 518, different 18 (3%)
c [score-dist-7] median active exp 515, avg 513.2
c [simplification-7] removed 0 variables 0.0% (5865 remain 66%)
c [simplification-7] removed 0 irredundant clauses 0.0% (53152 remain 78%)
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 -   78.2    5865    53152    155467   31428   6321   366  276   469   22  59%    927   51  253  233  108%
c -   97.0    5865    53152    194626   30505   6339   366  243   470   23  52%    971   29  193  246   78%
c -  118.9    5865    53152    238763   31531   6363   366  280   479   25  58%    997   20  306  265  116%
c -  136.9    5865    53152    276497   32991   6372   366  253   485   28  52%   1009   14  265  253  104%
c 
c [simplification-8] limit 282997 conflicts (hard 356329) hit after 282998 conflicts
c [quatres-6] found 23203 quaternary clauses 50% in total
c [quatres-6-1] added 1 double-self-subsuming ternary resolvents
c [quatres-6-2] added 94 single-self-subsuming ternary resolvents
c [quatres-6-2] added 90 quaternary resolvents
c [ternres-6] limit 32298968 with penalty 0 = 0 + 0
c [ternres-6] all 5865 free variables schedulable
c [ternres-6] 45 ternary resolvents (5 bin, 40 trn)
c [ternres-6] fully completed ternary resolution
c [gauss-3] limit 1614948 penalty 2 = 2 + 0
c [gauss-3] extracted 5895 xors of average arity 3.0
c [gauss-3] connected 17685 occurrences of 1420 variables (average 12.5)
c [gauss-3] limit 1614948 penalty 2 = 2 + 0
c [gauss-3] fully completed
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [simpleprobe-3] 2803 schedulable variables 48%
c [simpleprobe-3] limit 64597936 penalty 1 = 1 + 0
c [simpleprobe-3] fully completed simple probing
c [simpleprobe-3] removed 0 variables, found 15 hbrs, 0 units
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 15 transitive binary clauses
c [cce-4] boosting limit by 10
c [cce-4] limit of 403737102 steps penalty 2 = 2 + 0
c [cce-4-1] eliminated 3 clauses out of 16495 (0%) of length 5
c [cce-4-1] eliminated 15 clauses out of 20948 (0%) of length 4
c [cce-4-1] completed large round (ATE)
c [cce-4-1] eliminated 18 large clauses in 8771584 steps
c [cce-4-1] allowing another 4385792 steps for small clauses
c [cce-4-1] scheduling 13307 clauses = 555 binary + 12752 ternary
c [cce-4-1] tried to eliminate 13307 small clauses 100%
c [cce-4-1] completed small round (ATE)
c [cce-4-1] eliminated 18 covered clauses in round 1
c [cce-4-2] completed large round (ATE)
c [cce-4-2] allowing another 4381954 steps for small clauses
c [cce-4-2] scheduling 13307 clauses = 555 binary + 12752 ternary
c [cce-4-2] tried to eliminate 13307 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 18 covered clauses in TOTAL during 2 rounds
c [cce-4] 18 < 1/100 * 53152 = 531 considered unsuccessful
c [sweep-4] limit 2422422 penalty 2 = 2 + 0
c [sweep-4-1] 1410 pos 49.0% + 1470 neg 51.0% = 2880 sched 49.1% ret 2985
c [sweep-4-1] 976029 steps 587 queries 125.44 avg class size
c [sweep-4-1] 21445 decisions 588 SAT calls 146.82 avg env size
c [sweep-4-1] fully completed sweeping round
c [sweep-4-1] removed 0 vars (0 failed, 0 eqs, 1 impls)
c [sweep-4-2] 2860 pos 48.8% + 3005 neg 51.2% = 5865 sched 100.0% ret 0
c [sweep-4-2] 1356957 steps 673 queries 152.30 avg class size
c [sweep-4-2] 27468 decisions 676 SAT calls 184.64 avg env size
c [sweep-4-2] fully completed sweeping round
c [sweep-4-2] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-4-3] 2860 pos 48.8% + 3005 neg 51.2% = 5865 sched 100.0% ret 0
c [sweep-4-3] 92349 steps 40 queries 1100.45 avg class size
c [sweep-4-3] 1724 decisions 39 SAT calls 176.79 avg env size
c [sweep-4-3] 5567 variables remain 95% (298 retained 5%)
c [sweep-4-3] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-4] removed 0 vars in TOTAL (3 rounds, 1297 queries)
c [sort-queue-8] sorted 72 enqueued variables after 282998 conflicts
c [score-dist-8] active 5793 (99%), one 0 (0%), zero 72 (1%)
c [score-dist-8] max exp 519, different 19 (4%)
c [score-dist-8] median active exp 516, avg 514.3
c [simplification-8] removed 0 variables 0.0% (5865 remain 66%)
c [simplification-8] removed 18 irredundant clauses 0.0% (53134 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 -  162.8    5865    53134    321580   32658   6694   402  351   488   27  72%   1016    8  347  282  123%
c -  184.0    5865    53134    365953   33364   6711   402  267   488   22  55%   1020    5  239  286   83%
c -  209.1    5865    53134    413801   35182   6720   402  337   482   31  70%   1022   -1  269  298   90%
c -  231.4    5865    53134    457875   35710   6735   402  304   478   30  64%   1023   -4  286  291   98%
c -  258.8    5865    53134    509947   35312   6741   403  358   475   29  75%   1024   -4  369  314  118%
c -  293.7    5865    53134    574189   36336   6747   404  349   476   30  73%   1024   -1  312  336   93%
c 
c [simplification-9] limit 576326 conflicts (hard 722990) hit after 590761 conflicts
c [quatres-7] found 23498 quaternary clauses 49% in total
c [quatres-7-1] added 2 double-self-subsuming ternary resolvents
c [quatres-7-2] added 129 single-self-subsuming ternary resolvents
c [quatres-7-2] added 258 quaternary resolvents
c [ternres-7] limit 68762210 with penalty 0 = 0 + 0
c [ternres-7] all 5865 free variables schedulable
c [ternres-7] 179 ternary resolvents (4 bin, 175 trn)
c [ternres-7] fully completed ternary resolution
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 5 transitive binary clauses
c [elim-6] scheduling all variables this time
c [elim-6] scheduled 5865 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] no variable eliminated in round 1 in 13640151 steps
c [elim-6] fully completed in 1 rounds
c [elim-6] transition to [ all 0 rem 0 ] state
c [elim-6] eliminated 0 = 0% variables out of 5865 scheduled
c [sort-queue-9] sorted 68 enqueued variables after 590761 conflicts
c [score-dist-9] active 5797 (99%), one 0 (0%), zero 68 (1%)
c [score-dist-9] max exp 520, different 20 (4%)
c [score-dist-9] median active exp 517, avg 515.2
c [simplification-9] removed 0 variables 0.0% (5865 remain 66%)
c [simplification-9] removed 18 irredundant clauses 0.0% (53116 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 1470745 (soft 1177417 + delta 293328)
c [simplification-9] new conflict limit 1177417 (hard 1470745)
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 -  328.8    5865    53116    635043   37511   7054   403  372   472   29  79%   1024   -4  357  337  106%
c -  364.8    5865    53116    697295   38078   7057   403  375   473   32  79%   1024   -1  420  336  125%
c -  400.4    5865    53116    757923   38961   7063   403  337   472   34  71%   1024   -2  337  327  103%
c -  430.6    5865    53116    813450   38875   7070   403  330   472   35  70%   1024   -1  296  313   94%
c -  470.3    5865    53116    880148   39596   7078   403  368   468   35  79%   1024   -3  332  328  101%
c -  506.8    5865    53116    942519   39954   7079   403  260   471   31  55%   1024   -1  270  319   84%
c -  539.0    5865    53116   1000583   40823   7085   403  332   469   36  71%   1024   -3  319  307  104%
c -  578.2    5865    53116   1063494   41314   7090   403  351   474   38  74%   1024    2  363  314  115%
c -  607.9    5865    53116   1118912   41831   7102   403  295   469   37  63%   1024   -3  293  297   99%
c -  637.0    5865    53116   1174725   43342   7104   403  289   472   40  61%   1024   -1  284  289   98%
c 
c [simplification-10] limit 1177417 conflicts (hard 1470745) hit after 1177417 conflicts
c [quatres-8] found 23715 quaternary clauses 48% in total
c [quatres-8-1] added 4 double-self-subsuming ternary resolvents
c [quatres-8-2] added 43 single-self-subsuming ternary resolvents
c [quatres-8-2] added 67 quaternary resolvents
c [ternres-8] limit 152138249 with penalty 0 = 0 + 0
c [ternres-8] all 5865 free variables schedulable
c [ternres-8] 54 ternary resolvents (4 bin, 50 trn)
c [ternres-8] fully completed ternary resolution
c [card-4] limit 9508640 penalty 3 = 3 + 0
c [card-4] no at-most-one constraint found
c [card-4] found 9 at-most-two constraints of average size 4.0
c [card-4] using previous limit 9508640 for elimination
c [card-4] 9 out of 9 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] generated 2 at-most-one constraints, 1 used 50%
c [card-4] exported 1 binary clauses, 1.0 per/constraint
c [unhide-4] limit 2500000 with penalty 3 = 3 + 0
c [unhide-4-8] 0 units, 0 failed, 160 tauts, 0 hbrs, 28063 literals
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 1 transitive binary clauses
c [sort-queue-10] sorted 61 enqueued variables after 1177417 conflicts
c [score-dist-10] active 5804 (99%), one 0 (0%), zero 61 (1%)
c [score-dist-10] max exp 521, different 21 (4%)
c [score-dist-10] median active exp 518, avg 516.3
c [simplification-10] removed 0 variables 0.0% (5865 remain 66%)
c [simplification-10] removed 4 irredundant clauses 0.0% (53112 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 2677417 (soft 2177417 + delta 500000)
c [simplification-10] new conflict limit 2177417 (hard 2677417)
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 -  669.7    5865    53112   1233400   42914   7076   400  316   475   35  66%   1024    2  284  302   94%
c -  702.0    5865    53112   1293677   43867   7080   400  253   475   32  53%   1024   -0  204  294   69%
c -  737.0    5865    53112   1356243   45219   7089   400  314   477   41  66%   1024    2  331  299  110%
c -  773.3    5865    53112   1421078   44773   7099   400  276   473   36  58%   1024   -1  357  309  116%
c -  817.8    5865    53112   1496531   46057   7111   400  301   469   37  64%   1024   -3  249  321   77%
c -  865.6    5865    53112   1573765   47298   7120   400  319   472   38  68%   1024    1  329  327  101%
c -  918.6    5865    53112   1654889   48014   7125   400  349   467   39  75%   1024   -4  315  340   92%
c -  974.1    5865    53112   1738631   48349   7127   400  308   470   42  65%   1024    1  252  345   73%
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 (52 skipped), 121584 steps
c bkwd: tried 18342 clauses, 36516 lits, 1.99 lits/clause
c bkwd: checked 609783 occs, 33.25 occs/clause, 16.70 occs/lit
c bkwd: subsumed 0 binary, 5 ternary, 51 large
c bkwd: strengthened 0 binary, 0 ternary (0% self), 207 large (0% self)
c blkd: 3 bces, 571 removed, 1581261 resolutions, 3290026 steps
c blkd: 172 blocking literals 1%, 68 pure
c bump: 1779745 bumped seen, 1299272644 lits 730.0 on average
c card: 4 count, 5 units, 2 am1, 34993797 steps
c card: 63 rescheduled, 294 eliminated, 129505 resolved, 6825 subsumed
c card: 4 at-most-one constraints found, average size 3.00
c card: 4 at-most-one constraints used 100%, average size 3.00
c card: 146 at-most-two constraints found, average size 4.00
c card: 146 at-most-two constraints used 100%, average size 4.00
c cces: 4 cces, 9183 eliminated, 9069 ate 99%, 114 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: 334218 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: 25 decompositions, 27 equivalent 0%
c deco: 758531 decision-only clauses 43%, 49% reduction
c decs: 8952017 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 6 elims, 2997 eliminated 34%, 7 pure 0%
c elms: 12 rounds, 2.0 rounds/bve
c elms: 2922 small 97%, 0 large 0%
c elms: 24489 tried small, 2922 succeeded 12%, 21567 failed 88%
c elms: 558 subsumed, 658 strengthened, 5 blocked
c elms: 1929592 copies, 3615098 resolutions, 2361377 ipos
c elms: 64461 subchks, 60617 strchks
c gaus: 3 extractions, 24337 extracted, 3.3 size, 4 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 9230332 steps, 4615166 extr 50%, 2775815 elim 30%
c glue: 304.8 orig avg, 304.8 real avg, 10.8 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 529 = 373 simple 71% + 152 trn 29% + 4 lrg 1%, 13 sub 2%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 1779744 clauses, 390.2 length
c lrnd: 694501585 lits = 1039031050 orig - 344529465 removed 33%
c lrnd: 448189 uips 25%, 1198729 flips 67%
c mins: 579858 mins 43%, 14 bin 0%, 5749 size 0%
c mins: 65331868 poisoned searches, 4612958 hits, 7% hit rate
c mins: 136548835 used twice searches, 45897551 hits, 34% hit rate
c move: moved 635, 17 bin 3%, 618 trn 97%
c otfs: 2529 driving 14%, 15719 restarting 86%
c otfs: str 18248, 18108 red 99%, 140 irr 1%
c otfs: str 18248, 0 bin 0%, 117 trn 1%, 18131 lrg 99%
c otfs: sub 150, 150 red 100%, 0 irr 0%
c otfs: sub 150, 0 bin 0%, 5 trn 3%, 145 lrg 97%
c phas: 1 computed, 6266 set, 0 pos (0%), 6266 neg (100%)
c prbs: 2 basic, 6288 probed, 0 failed, 0 lifted
c prbs: 3 simple, 33441 probed, 1 failed, 19 eqs
c prbs: 2 treelook, 4561 probed, 0 failed, 0 lifted
c prom: 63849 locked 1% out of 4594225 tried
c prps: 1210800986 props, 135 props/dec
c prps: 100% srch, 0% simp, 0% lkhd
c quat: 8 count, 2025 quat, 1057 self1, 32 self2, 0 dup
c queu: 10 sorted, 8952017 next (226455 steps 0.03)
c queu: 1299293677 enq (2527079923 steps 1.94), 1299272644 deq 100%
c redc: 22 clauses 0%, 15654 tried 1%, 0 sat 0%
c redc: 22 lits 0%, 162012 tried 0%, 0 sat 0%
c redc: 0 times jump level reduced, 0.0 levels on average
c reds: 30 count, 59346.3 conflicts per reduce
c reds: 0 memlim 0%, 30 arith 100%
c reds: 967972 collected 92%, 79989 retired 8%
c rmbd: 70 removed, 70 red 100%
c rsts: 14002 restarts 100%, 32 skipped 0%
c rsts: 32 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: 1779744 count (6725261 tried 3.8), 660590 sub out of 1778151 (37.2%)
c swps: 4 count, 8 rounds, 3650 queries (456.2/round)
c swps: 3662 sat calls, 12 unsat (0.5% success rate)
c swps: 84091 decisions 23.0, 1886 conflicts 0.5
c swps; 271.4 avg class size, 89.2 avg environment size
c swps: 0 failed, 1 impls, 0 equivs
c swp0: 1214 type 0 queries, 10 unsat (0.8%), 1214 sat (100.0%)
c swp1: 2436 type 1 queries, 78 unsat (3.2%), 2436 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: 21463715 calls to obtain time
c tops: 17 fixed 0%, 0 its, 0.00 confs/it
c trds: 8 transitive reductions, 65 removed, 0 failed
c trds: 93991 nodes, 7438 edges, 11194 steps
c trim: 19737 words, 0.1 MB
c trnr: 8 count, 54 bin, 5001 trn, 11346781 steps
c unhd: 4 count, 8 rounds, 3542209 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: 342 tauts, 0 bin 0%, 317 trn 93%, 14 lrg 4%
c unhd: 342 tauts, 11 stamp 3%, 296 red 87%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 108650 str, 0 bin 0%, 123 trn 0%, 108527 lrg 100%, 108536 red 100%
c vars: 5865 remaining 66% and 3041 removed 34% out of 8906
c vars: 17 fixed 0%, 2997 eliminated 34%, 27 equivalent 0%
c vsts: 24101939147 visits, 100% srch, 0% simp, 0% lkhd
c vsts: 19.9 search visits per propagation, 13535.6 per conflict
c wchs: 4683724652 pushed, 4136122 enlarged, 80 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all        1780176        967972         79989     261695060      81206405        790156
c 
c  0 0         14326   1      1059   0         0   0 102664789  39  23897363  29    176631  22     0.4
c  1 5          3582   0      1009   0      1058   1  21758003   8   5835110   7     40105   5     0.1
c  2 6         10409   1      4048   0      2822   4  33145966  13<  9394253  12     66654   8     0.2
c  3 9         17536   1      8840   1      3912   5  36217853  14  11991946  15<    84286  11     0.4
c  4 14        26099   1     17148   2      3835   5  23579862   9   8617222  11     79759  10     0.6
c  5 21        32083   2     24631   3      3140   4  15071342   6   5853883   7     55029   7<    0.8
c  6 30        38367   2     32451   3      2498   3  10148802   4   4187689   5     42408   5     0.9
c  7 41        43038   2     38170   4      2170   3   6151539   2   2878095   4     33423   4     1.2
c  8 54        48259   3     43822   5      1929   2   3171793   1   1708583   2     26217   3     1.4
c  9 69        50033   3     46107   5      1902   2   2182609   1   1246526   2     20550   3     1.8
c 10 86       109543   6    102372  11<     3659   5<  2683231   1   1714582   2     31899   4     4.3
c 11 126      267070  15<   253454  26      7375   9   2311628   1   1710397   2     48713   6    16.3
c 12 230     1119831  63    394861  41     45689  57   2607643   1   2170756   3     84482  11   127.9
c 
c avg                 10.8          10.3           9.7           2.3           3.2           4.8
c std                  2.4           2.3           3.4           2.6           3.2           4.1
c 
c  260.257  26% bump
c    5.700   1% decide
c    3.241   0% elim
c 
c    5.355 < 1% rest (below)
c 
c    2.402   0% unhide
c    1.936   0% cce
c    0.984   0% sweep
c    0.683   0% probe
c    0.461   0% card
c    0.367   0% quatres
c    0.360   0% gauss
c    0.285   0% block
c    0.167   0% bca
c    0.102   0% ternres
c    0.012   0% transred
c    0.000   0% locs
c    0.000   0% queuesort
c    0.000   0% rescore
c ==================================
c    0.754   0% preprocessing     6%
c   11.675   1% inprocessing     94%
c ==================================
c   12.429   1% simplifying
c  987.577  99% search
c ==================================
c 1000.006 100% all
c 
c       1780388 conflicts,        1780.4 confs/sec
c          1266 ternaries,        1406.3 confs/ternary
c            21 binaries,        84780.4 confs/binary
c             0 iterations,          0.0 confs/iteration
c 
c            30 reductions,          0.0 redus/sec,  59346.3 confs/reduction
c         14002 restarts,           14.0 rests/sec,    127.2 confs/restart
c       8952017 decisions,        8952.0 decis/sec,      5.0 decis/conflict
c    1210800986 propagations,  1210794.0 props/sec,    135.3 props/decision
c 
c 1000.0 seconds, 283.9 MB
c
c CAUGHT SIGNAL 15 SIGTERM
c
c launch: done
