c launch: /data/cnf/sc2014/app/6s130-opt.cnf.bz2
c host: atom26
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/6s130-opt.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/6s130-opt.cnf.bz2
c no embedded options
c found 'p cnf 49370 144361' header
c read 49370 variables, 144361 clauses, 336841 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=4
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 49326 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] VSIDS (--score=4) decay interval 256 (--vsidsdint=256)
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   49326   144360         0       0      0     0    0     0    9   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 84 at-most-one constraints of average size 3.0
c [card-1] no at-most-two constraint found
c [card-1] using previous limit 2000000 for elimination
c [card-1] 84 out of 84 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] generated 85 at-most-one constraints, 85 used 100%
c [card-1] exported 90 binary clauses, 1.1 per/constraint
c [decomp-1] removed 1 variables
c [simpleprobe-1] all 49326 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 819 variables
c [simpleprobe-1] fully completed simple probing
c [simpleprobe-1] removed 819 variables, found 1857 hbrs, 22 units
c [unhide-1] limit 100000 with penalty 0 = 0 + 0
c [unhide-1-1] 0 units, 0 failed, 9 tauts, 0 hbrs, 12 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 48507 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 35660 variables 74% in round 1 in 10021219 steps
c [elim-1-1] backward subsumption/strengthening limit 9978781
c [elim-1-1-1] backward checking 35030 touched variables 72%
c [elim-1-1-1] fully completed backward checking in 1 rounds
c [elim-1-1] subsumed 141 and strengthened 792 clauses in 7195484 steps
c [elim-1-1] rescheduled 1555 variables 3% by backward subsumption
c [elim-1-2] eliminated 35 variables 0% in round 2 in 924750 steps
c [elim-1-2] backward subsumption/strengthening limit 924700
c [elim-1-2-1] backward checking 338 touched variables 1%
c [elim-1-2-1] fully completed backward checking in 1 rounds
c [elim-1-2] subsumed 4 and strengthened 15 clauses in 698697 steps
c [elim-1-2] rescheduled 76 variables 0% by backward subsumption
c [elim-1-3] no variable eliminated in round 3 in 30893 steps
c [elim-1] fully completed in 3 rounds
c [elim-1] transition to [ all 0 rem 0 ] state
c [elim-1] eliminated 35697 = 74% variables out of 48507 scheduled
c [phase-count-1] 63823 negative 90.3% of 70697 except 6874 9.7%
c [phase-count-1] 59362 positive 84.0% of 70697 except 11335 16.0%
c [phase-1] phase bias: 3184 positive 25%, 9626 negative 75%
c [sort-queue-1] sorted 12810 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 12810 (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 36516 variables 74.0% (12810 remain 26%)
c [simplification-1] removed 73663 irredundant clauses 51.0% (70697 remain 49%)
c [simplification-1] maximum reduction of 74% = max (74%, 51%)
c [simplification-1] large reduction 74% >= 5% limit
c [simplification-1] next conflict interval 1000 = 2000/2
c [simplification-1] penalized conflict interval 1000 = 1 * 1000
c [simplification-1] hard conflict limit 11000 (soft 1000 + delta 10000)
c [simplification-1] new conflict limit 1000 (hard 11000)
c 
c [simplification-2] limit 1000 conflicts (hard 11000) hit after 1000 conflicts
c [decomp-3] removed 4 variables
c [simpleprobe-2] all 12806 free variables schedulable
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [decomp-4] removed 5 variables
c [simpleprobe-2] 6989 variables remain 55% (5812 retained 45%)
c [simpleprobe-2] removed 5 variables, found 447 hbrs, 1 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 25602 literals 100%
c [treelook-1] scheduling used 293276 steps
c [treelook-1] scheduled completely
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 305101 steps
c [treelook-1] 25434 literals remain 99%
c [treelook-1] 12796 variables remain to probed next time 100%
c [decomp-5] removed 6 variables
c [treelook-1] removed 6 variables, found 1342 hbrs
c [basicprobe-1] limit 1000000 penalty 0 = 0 + 0
c [basicprobe-1-0] 4779 probes remain 37% after last round
c [basicprobe-1-0] 1 units = 1 failed (100%) + 0 lifted (0%)
c [basicprobe-1-0] removed 1 variables, found 5794 hbrs
c [block-1] scheduling all variables this time
c [block-1] scheduled 12794 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 2250 blocked clauses
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 2 clauses out of 13 (15%) of length 15
c [cce-1-1] eliminated 2 clauses out of 36 (6%) of length 14
c [cce-1-1] eliminated 5 clauses out of 69 (7%) of length 13
c [cce-1-1] eliminated 4 clauses out of 77 (5%) of length 12
c [cce-1-1] eliminated 8 clauses out of 72 (11%) of length 11
c [cce-1-1] eliminated 16 clauses out of 227 (7%) of length 10
c [cce-1-1] eliminated 20 clauses out of 435 (5%) of length 9
c [cce-1-1] eliminated 51 clauses out of 752 (7%) of length 8
c [cce-1-1] eliminated 107 clauses out of 1448 (7%) of length 7
c [cce-1-1] eliminated 295 clauses out of 3304 (9%) of length 6
c [cce-1-1] eliminated 620 clauses out of 6394 (10%) of length 5
c [cce-1-1] eliminated 808 clauses out of 14603 (6%) of length 4
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 1938 large clauses in 30000000 steps
c [cce-1-1] allowing another 15000000 steps for small clauses
c [cce-1-1] scheduling 22612 clauses = 13906 binary + 8706 ternary
c [cce-1-1] tried to eliminate 20164 small clauses 89%
c [cce-1-1] eliminated 158 binary clauses 1%
c [cce-1-1] eliminated 286 ternary clauses 3%
c [cce-1-1] eliminated 444 small clauses 2%
c [cce-1-1] eliminated 444 small clauses in 30000000 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 2382 covered clauses in round 1
c [cce-1] eliminated 2382 covered clauses in TOTAL during 1 rounds
c [elim-2] scheduling all variables this time
c [elim-2] scheduled 12769 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 721 variables 6% in round 1 in 10869084 steps
c [elim-2-1] backward subsumption/strengthening limit 9130916
c [elim-2-1-1] backward checking 4170 touched variables 33%
c [elim-2-1-1] fully completed backward checking in 1 rounds
c [elim-2-1] subsumed 13 and strengthened 57 clauses in 2147624 steps
c [elim-2-1] rescheduled 197 variables 2% by backward subsumption
c [elim-2-2] eliminated 7 variables 0% in round 2 in 1178832 steps
c [elim-2-2] backward subsumption/strengthening limit 1178800
c [elim-2-2-1] backward checking 50 touched variables 0%
c [elim-2-2-1] fully completed backward checking in 1 rounds
c [elim-2-2] subsumed 3 and strengthened 12 clauses in 472314 steps
c [elim-2-2] rescheduled 26 variables 0% by backward subsumption
c [elim-2-3] no variable eliminated in round 3 in 24494 steps
c [elim-2] fully completed in 3 rounds
c [elim-2] transition to [ all 0 rem 0 ] state
c [elim-2] eliminated 728 = 6% variables out of 12769 scheduled
c [bca-1] limit of 10000000 steps and 131130 added (scaled 2)
c [bca-1] 22012 out of 24084 literals actually usable 91%
c [bca-1] added 492 blocked clauses in 58711 steps
c [sweep-1] limit 1000000 penalty 0 = 0 + 0
c [sweep-1-1] 5320 pos 44.2% + 6721 neg 55.8% = 12041 sched 100.0% ret 0
c [sweep-1-1] 1002541 steps 217 queries 964.30 avg class size
c [sweep-1-1] 3356 decisions 216 SAT calls 29.60 avg env size
c [sweep-1-1] 9129 variables remain 76% (2911 retained 24%)
c [decomp-6] removed 9 variables
c [sweep-1-1] removed 9 vars (0 failed, 2 eqs, 3 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 9 vars in TOTAL (1 rounds, 216 queries)
c [sort-queue-2] sorted 8464 enqueued variables after 1000 conflicts
c [score-dist-2] active 3568 (30%), one 0 (0%), zero 8464 (70%)
c [score-dist-2] max exp 509, different 11 (2%)
c [score-dist-2] median active exp 502, avg 502.4
c [simplification-2] removed 778 variables 6.1% (12032 remain 24%)
c [simplification-2] removed 5391 irredundant clauses 7.6% (65306 remain 45%)
c [simplification-2] maximum reduction of 8% = max (6%, 8%)
c [simplification-2] large reduction 8% >= 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 14191 quaternary clauses 51% in total
c [quatres-1-1] removed 4 duplicate quaternary clauses
c [quatres-1-2] added 21 single-self-subsuming ternary resolvents
c [quatres-1-2] added 1732 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 12032 free variables schedulable
c [ternres-1] 7255 ternary resolvents (185 bin, 7070 trn)
c [ternres-1] fully completed ternary resolution
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 292 at-most-one constraints of average size 3.7
c [card-2] found 56 at-most-two constraints of average size 4.0
c [card-2] using previous limit 1000000 for elimination
c [card-2] 343 out of 348 constraints (99%) meet size limits
c [card-2] no units found
c [card-2] generated 8 at-most-one constraints, 3 used 38%
c [card-2] exported 3 binary clauses, 1.0 per/constraint
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 5551 xors of average arity 3.1
c [gauss-1] connected 17093 occurrences of 1210 variables (average 14.1)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] fully completed
c [decomp-7] removed 22 variables
c [gauss-1] exported 1 unary, 0 binary and 2 ternary equations
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] scheduled 23981 literals 100%
c [treelook-2] scheduling used 300023 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] used 302913 steps
c [treelook-2] 23788 literals remain 99%
c [treelook-2] 12005 variables remain to probed next time 100%
c [treelook-2] removed 0 variables, found 481 hbrs
c [unhide-2] limit 50000 with penalty 1 = 1 + 0
c [unhide-2-2] 0 units, 0 failed, 1100 tauts, 0 hbrs, 1567 literals
c [transred-1] limit 157269 with penalty 0 = 0 + 0
c [transred-1] removed 57 transitive binary clauses
c [block-2] scheduling all variables this time
c [block-2] scheduled 12010 variables 100%
c [block-2] limit of 50000000 steps penalty 0 = 0 + 0
c [block-2] fully completed
c [block-2] transition to [ all 0 rem 0 ] state
c [block-2] eliminated 83 blocked clauses
c [block-2] 83 < 1/100 * 65259 = 652 considered unsuccessful
c [cce-2] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-2-1] eliminated 7 clauses out of 106 (7%) of length 12
c [cce-2-1] eliminated 5 clauses out of 110 (5%) of length 11
c [cce-2-1] eliminated 18 clauses out of 273 (7%) of length 10
c [cce-2-1] eliminated 14 clauses out of 458 (3%) of length 9
c [cce-2-1] eliminated 17 clauses out of 821 (2%) of length 8
c [cce-2-1] eliminated 59 clauses out of 1874 (3%) of length 7
c [cce-2-1] eliminated 103 clauses out of 3153 (3%) of length 6
c [cce-2-1] eliminated 139 clauses out of 6204 (2%) of length 5
c [cce-2-1] eliminated 7 clauses out of 13905 (0%) of length 4
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] eliminated 369 large clauses in 30000900 steps
c [cce-2-1] allowing another 15000450 steps for small clauses
c [cce-2-1] scheduling 20931 clauses = 12794 binary + 8137 ternary
c [cce-2-1] tried to eliminate 18216 small clauses 87%
c [cce-2-1] eliminated 31 binary clauses 0%
c [cce-2-1] eliminated 57 ternary clauses 1%
c [cce-2-1] eliminated 88 small clauses 0%
c [cce-2-1] eliminated 88 small clauses in 30000314 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 457 covered clauses in round 1
c [cce-2] eliminated 457 covered clauses in TOTAL during 1 rounds
c [cce-2] 457 < 1/100 * 65176 = 651 considered unsuccessful
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 11999 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 110 variables 1% in round 1 in 13319451 steps
c [elim-3-1] backward subsumption/strengthening limit 6680549
c [elim-3-1-1] backward checking 973 touched variables 8%
c [elim-3-1-1] fully completed backward checking in 1 rounds
c [elim-3-1] subsumed 1 and strengthened 19 clauses in 975424 steps
c [elim-3-1] rescheduled 34 variables 0% by backward subsumption
c [elim-3-2] eliminated 3 variables 0% in round 2 in 335591 steps
c [elim-3-2] backward subsumption/strengthening limit 335500
c [elim-3-2-1] backward checking 15 touched variables 0%
c [elim-3-2-1] fully completed backward checking in 1 rounds
c [elim-3-2] subsumed 1 and strengthened 1 clauses in 32245 steps
c [elim-3-2] rescheduled 5 variables 0% by backward subsumption
c [elim-3-3] eliminated 3 variables 0% in round 3 in 1359 steps
c [elim-3-3] backward subsumption/strengthening limit 1300
c [elim-3-3-1] backward checking 13 touched variables 0%
c [elim-3-3-1] incomplete backward checking 9 remain 69%
c [elim-3-3] subsumed 0 and strengthened 5 clauses in 1632 steps
c [elim-3] incomplete 7 not tried 0% in round 3
c [elim-3] transition to [ all 1 rem 1 ] state
c [elim-3] eliminated 116 = 1% variables out of 11999 scheduled
c [elim-3] 116 < 1/100 * 11999 = 119 considered unsuccessful
c [bca-2] limit of 10000000 steps and 129628 added (scaled 2)
c [bca-2] 16177 out of 23768 literals actually usable 68%
c [bca-2] added 5 blocked clauses in 45290 steps
c [sweep-2] limit 1000000 penalty 0 = 0 + 0
c [sweep-2-1] 3964 pos 44.0% + 5037 neg 56.0% = 9001 sched 75.7% ret 2882
c [sweep-2-1] 1000788 steps 241 queries 769.06 avg class size
c [sweep-2-1] 3205 decisions 238 SAT calls 26.11 avg env size
c [sweep-2-1] 6719 variables remain 57% (5164 retained 43%)
c [decomp-10] removed 12 variables
c [sweep-2-1] removed 12 vars (0 failed, 6 eqs, 7 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 12 vars in TOTAL (1 rounds, 240 queries)
c [sort-queue-3] sorted 5233 enqueued variables after 3000 conflicts
c [score-dist-3] active 6638 (56%), one 0 (0%), zero 5233 (44%)
c [score-dist-3] max exp 509, different 19 (4%)
c [score-dist-3] median active exp 500, avg 499.7
c [simplification-3] removed 161 variables 1.3% (11871 remain 24%)
c [simplification-3] removed 868 irredundant clauses 1.3% (64438 remain 45%)
c [simplification-3] maximum reduction of 1% = max (1%, 1%)
c [simplification-3] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-3] new conflict interval 10000
c [simplification-3] penalized conflict interval 10000 = 1 * 10000
c [simplification-3] hard conflict limit 23000 (soft 13000 + delta 10000)
c [simplification-3] new conflict limit 13000 (hard 23000)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i    6.5   11870    64438     11629   11139   7725  8194   10   132   10   8%    153  114   11    2  673%
c i    6.5   11869    64438     11722   11192   7730  8198   10   135   10   7%    138  117    9    2  586%
c 
c [simplification-4] limit 13000 conflicts (hard 23000) hit after 13000 conflicts
c [quatres-2] found 16061 quaternary clauses 52% in total
c [quatres-2-1] removed 1 duplicate quaternary clauses
c [quatres-2-1] added 2 double-self-subsuming ternary resolvents
c [quatres-2-2] added 53 single-self-subsuming ternary resolvents
c [quatres-2-2] added 844 quaternary resolvents
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] all 11869 free variables schedulable
c [ternres-2] 535 ternary resolvents (52 bin, 483 trn)
c [ternres-2] fully completed ternary resolution
c [gauss-2] limit 2000000 penalty 0 = 0 + 0
c [gauss-2] extracted 5323 xors of average arity 3.1
c [gauss-2] connected 16469 occurrences of 1176 variables (average 14.0)
c [gauss-2] limit 2000000 penalty 0 = 0 + 0
c [gauss-2] fully completed
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-11] removed 6 variables
c [basicprobe-2] limit 2670252 penalty 0 = 0 + 0
c [basicprobe-2-0] 31 probes remain 0% after last round
c [basicprobe-2-0] 3 units = 3 failed (100%) + 0 lifted (0%)
c [basicprobe-2-0] removed 3 variables, found 7979 hbrs
c [bate-1] eliminated 32 asymmetric tautologies during probing
c [transred-2] limit 534050 with penalty 0 = 0 + 0
c [transred-2] removed 393 transitive binary clauses
c [transred-2] found 1 units
c [bca-3] limit of 10000000 steps and 129460 added (scaled 2)
c [bca-3] 11049 out of 23720 literals actually usable 47%
c [bca-3] added 0 blocked clauses in 40118 steps
c [sweep-3] limit 1000000 penalty 0 = 0 + 0
c [sweep-3-1] 3135 pos 46.7% + 3577 neg 53.3% = 6712 sched 56.6% ret 5147
c [sweep-3-1] 1000867 steps 152 queries 594.27 avg class size
c [sweep-3-1] 3423 decisions 151 SAT calls 35.15 avg env size
c [sweep-3-1] 5665 variables remain 48% (6193 retained 52%)
c [decomp-12] removed 18 variables
c [sweep-3-1] removed 18 vars (0 failed, 1 eqs, 2 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 18 vars in TOTAL (1 rounds, 151 queries)
c [sort-queue-4] sorted 2215 enqueued variables after 13000 conflicts
c [score-dist-4] active 9626 (81%), one 0 (0%), zero 2215 (19%)
c [score-dist-4] max exp 510, different 58 (11%)
c [score-dist-4] median active exp 499, avg 493.2
c [simplification-4] removed 28 variables 0.2% (11841 remain 24%)
c [simplification-4] removed 97 irredundant clauses 0.2% (64341 remain 45%)
c [simplification-4] maximum reduction of 0% = max (0%, 0%)
c [simplification-4] full geometric conflict interval increment 20000
c [simplification-4] new conflict interval 30000
c [simplification-4] penalized conflict interval 30000 = 1 * 30000
c [simplification-4] hard conflict limit 58000 (soft 43000 + delta 15000)
c [simplification-4] new conflict limit 43000 (hard 58000)
c 
c [simplification-5] limit 43000 conflicts (hard 58000) hit after 43000 conflicts
c [quatres-3] found 17430 quaternary clauses 51% in total
c [quatres-3-1] removed 3 duplicate quaternary clauses
c [quatres-3-1] added 2 double-self-subsuming ternary resolvents
c [quatres-3-2] added 81 single-self-subsuming ternary resolvents
c [quatres-3-2] added 560 quaternary resolvents
c [ternres-3] limit 4000000 with penalty 0 = 0 + 0
c [ternres-3] all 11841 free variables schedulable
c [ternres-3] 361 ternary resolvents (37 bin, 324 trn)
c [ternres-3] 6 variables remain 0% (11835 retained 100%)
c [decomp-13] removed 12 variables
c [simpleprobe-3] 6472 schedulable variables 55%
c [simpleprobe-3] limit 7212515 penalty 0 = 0 + 0
c [decomp-14] removed 14 variables
c [simpleprobe-3] 935 variables remain 8% (10880 retained 92%)
c [simpleprobe-3] removed 14 variables, found 1359 hbrs, 0 units
c [transred-3] limit 1803128 with penalty 0 = 0 + 0
c [transred-3] removed 1032 transitive binary clauses
c [block-3] scheduling all variables this time
c [block-3] scheduled 11815 variables 100%
c [block-3] limit of 25000000 steps penalty 1 = 1 + 0
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 72 blocked clauses
c [block-3] 72 < 1/100 * 64248 = 642 considered unsuccessful
c [cce-3] limit of 15000000 steps penalty 1 = 1 + 0
c [cce-3-1] eliminated 2 clauses out of 103 (2%) of length 13
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 2 large clauses in 15000001 steps
c [cce-3-1] allowing another 7500000 steps for small clauses
c [cce-3-1] scheduling 29435 clauses = 12640 binary + 16795 ternary
c [cce-3-1] tried to eliminate 963 small clauses 3%
c [cce-3-1] eliminated 8 binary clauses 0%
c [cce-3-1] eliminated 26 ternary clauses 0%
c [cce-3-1] eliminated 34 small clauses 0%
c [cce-3-1] eliminated 34 small clauses in 15000001 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 36 covered clauses in round 1
c [cce-3] eliminated 36 covered clauses in TOTAL during 1 rounds
c [cce-3] 36 < 1/100 * 64176 = 641 considered unsuccessful
c [elim-4] no untried remaining variables left
c [elim-4] scheduled 11810 variables 100%
c [elim-4] boosting limit by 20
c [elim-4] limit of 360625780 steps penalty 1 = 1 + 0
c [elim-4] rescheduling of touched variables disabled
c [elim-4-1] eliminated 83 variables 1% in round 1 in 13285516 steps
c [elim-4-1] backward subsumption/strengthening limit 13285500
c [elim-4-1-1] backward checking 430 touched variables 4%
c [elim-4-1-1] fully completed backward checking in 1 rounds
c [elim-4-1] subsumed 0 and strengthened 2 clauses in 515105 steps
c [elim-4-1] rescheduled 10 variables 0% by backward subsumption
c [elim-4-2] no variable eliminated in round 2 in 43831 steps
c [elim-4] fully completed in 2 rounds
c [elim-4] transition to [ all 0 rem 0 ] state
c [elim-4] eliminated 83 = 1% variables out of 11810 scheduled
c [elim-4] 83 < 1/100 * 11810 = 118 considered unsuccessful
c [sweep-4] limit 1000000 penalty 0 = 0 + 0
c [sweep-4-1] 2556 pos 45.8% + 3019 neg 54.2% = 5575 sched 47.5% ret 6152
c [sweep-4-1] 1006614 steps 129 queries 767.66 avg class size
c [sweep-4-1] 3102 decisions 127 SAT calls 41.75 avg env size
c [sweep-4-1] 4608 variables remain 39% (7118 retained 61%)
c [decomp-15] removed 4 variables
c [sweep-4-1] removed 4 vars (0 failed, 1 eqs, 3 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 4 vars in TOTAL (1 rounds, 128 queries)
c [sort-queue-5] sorted 1550 enqueued variables after 43000 conflicts
c [score-dist-5] active 10173 (87%), one 0 (0%), zero 1550 (13%)
c [score-dist-5] max exp 510, different 156 (31%)
c [score-dist-5] median active exp 499, avg 481.1
c [simplification-5] removed 118 variables 1.0% (11723 remain 24%)
c [simplification-5] removed 439 irredundant clauses 0.7% (63899 remain 44%)
c [simplification-5] maximum reduction of 1% = max (1%, 1%)
c [simplification-5] geometric conflict interval increment 15000 = 30000 / 2
c [simplification-5] new conflict interval 45000
c [simplification-5] penalized conflict interval 45000 = 1 * 45000
c [simplification-5] hard conflict limit 110500 (soft 88000 + delta 22500)
c [simplification-5] new conflict limit 88000 (hard 110500)
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 -   17.6   11723    63899     67385   25690   8888 14933   12   132   12   9%    573   44   10    8  131%
c i   17.7   11722    63899     68283   26434   8892 14933   12   125   13   9%    579   37   12    8  157%
c 
c [simplification-6] limit 88000 conflicts (hard 110500) hit after 88000 conflicts
c [quatres-4] found 18371 quaternary clauses 49% in total
c [quatres-4-1] removed 6 duplicate quaternary clauses
c [quatres-4-1] added 13 double-self-subsuming ternary resolvents
c [quatres-4-2] added 91 single-self-subsuming ternary resolvents
c [quatres-4-2] added 299 quaternary resolvents
c [ternres-4] limit 4000000 with penalty 0 = 0 + 0
c [ternres-4] 5 schedulable variables 0%
c [ternres-4] 11 ternary resolvents (0 bin, 11 trn)
c [ternres-4] fully completed ternary resolution
c [card-3] limit 500000 penalty 2 = 2 + 0
c [card-3] found 207 at-most-one constraints of average size 3.4
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 500000 for elimination
c [card-3] 207 out of 207 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [gauss-3] limit 1000000 penalty 1 = 1 + 0
c [gauss-3] extracted 2678 xors of average arity 3.0
c [gauss-3] connected 8026 occurrences of 881 variables (average 9.1)
c [gauss-3] limit 1000000 penalty 1 = 1 + 0
c [gauss-3] fully completed
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-16] removed 4 variables
c [unhide-3] limit 182217 with penalty 2 = 2 + 0
c [unhide-3-3] 0 units, 0 failed, 258 tauts, 0 hbrs, 12780 literals
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 560 transitive binary clauses
c [bca-4] limit of 10000000 steps and 128500 added (scaled 2)
c [bca-4] 7941 out of 23438 literals actually usable 34%
c [bca-4] added 1 blocked clauses in 62122 steps
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 10933060 penalty 0 = 0 + 0
c [sweep-5-1] 2107 pos 45.8% + 2498 neg 54.2% = 4605 sched 39.3% ret 7113
c [sweep-5-1] 7536042 steps 997 queries 84.69 avg class size
c [sweep-5-1] 19994 decisions 995 SAT calls 36.78 avg env size
c [sweep-5-1] fully completed sweeping round
c [decomp-17] removed 55 variables
c [sweep-5-1] removed 55 vars (0 failed, 57 eqs, 40 impls)
c [sweep-5-2] 4869 pos 41.7% + 6794 neg 58.3% = 11663 sched 100.0% ret 0
c [sweep-5-2] 3401882 steps 383 queries 361.34 avg class size
c [sweep-5-2] 9110 decisions 377 SAT calls 47.48 avg env size
c [sweep-5-2] 4603 variables remain 39% (7060 retained 61%)
c [decomp-18] removed 9 variables
c [sweep-5-2] removed 9 vars (0 failed, 10 eqs, 13 impls)
c [sweep-5] removed 64 vars in TOTAL (2 rounds, 1378 queries)
c [sort-queue-6] sorted 1158 enqueued variables after 88000 conflicts
c [score-dist-6] active 10496 (90%), one 0 (0%), zero 1158 (10%)
c [score-dist-6] max exp 511, different 234 (46%)
c [score-dist-6] median active exp 500, avg 466.8
c [simplification-6] removed 68 variables 0.6% (11654 remain 24%)
c [simplification-6] removed 55 irredundant clauses 0.1% (63844 remain 44%)
c [simplification-6] maximum reduction of 1% = max (1%, 0%)
c [simplification-6] geometric conflict interval increment 22500 = 45000 / 2
c [simplification-6] new conflict interval 67500
c [simplification-6] penalized conflict interval 67500 = 1 * 67500
c [simplification-6] hard conflict limit 189250 (soft 155500 + delta 33750)
c [simplification-6] new conflict limit 155500 (hard 189250)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   21.7   11653    63844     91718   47426   9043 15127   12   101   16  12%     85    5   11    9  120%
c -   23.8   11653    63841    110892   33032   9135 15133   14   100   13  15%     45    3   13   10  132%
c -   27.2   11653    63840    150897   38286   9248 15143   10   229   19   4%    492  105    9   10   92%
c 
c [simplification-7] limit 155500 conflicts (hard 189250) hit after 155501 conflicts
c [quatres-5] found 19017 quaternary clauses 46% in total
c [quatres-5-1] removed 14 duplicate quaternary clauses
c [quatres-5-1] added 6 double-self-subsuming ternary resolvents
c [quatres-5-2] added 71 single-self-subsuming ternary resolvents
c [quatres-5-2] added 220 quaternary resolvents
c [ternres-5] limit 5430969 with penalty 0 = 0 + 0
c [ternres-5] all 11653 free variables schedulable
c [ternres-5] 1544 ternary resolvents (95 bin, 1449 trn)
c [ternres-5] 4 variables remain 0% (11649 retained 100%)
c [decomp-19] removed 2 variables
c [treelook-3] limit 271548 penalty 1 = 1 + 0 boost 1
c [treelook-3] scheduled 16404 literals 70%
c [treelook-3] scheduling used 271587 steps
c [treelook-3] not fully scheduled
c [treelook-3] limit 271548 penalty 1 = 1 + 0 boost 1
c [treelook-3] used 272435 steps
c [treelook-3] 16328 literals remain 70%
c [treelook-3] 10964 variables remain to probed next time 94%
c [decomp-20] removed 2 variables
c [treelook-3] removed 2 variables, found 987 hbrs
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 755 transitive binary clauses
c [transred-5] found 3 units
c [bca-5] limit of 10000000 steps and 128257 added (scaled 2)
c [bca-5] 7902 out of 23296 literals actually usable 34%
c [bca-5] added 1 blocked clauses in 61001 steps
c [sweep-6] limit 1629290 penalty 0 = 0 + 0
c [sweep-6-1] 2128 pos 46.3% + 2471 neg 53.7% = 4599 sched 39.5% ret 7048
c [sweep-6-1] 1634863 steps 206 queries 367.06 avg class size
c [sweep-6-1] 3239 decisions 194 SAT calls 35.22 avg env size
c [sweep-6-1] 3147 variables remain 27% (8500 retained 73%)
c [decomp-21] removed 15 variables
c [sweep-6-1] removed 15 vars (0 failed, 14 eqs, 11 impls)
c [sweep-6] removed 15 vars in TOTAL (1 rounds, 205 queries)
c [sort-queue-7] sorted 1650 enqueued variables after 155501 conflicts
c [score-dist-7] active 9982 (86%), one 523 (4%), zero 1127 (10%)
c [score-dist-7] max exp 510, different 309 (60%)
c [score-dist-7] median active exp 436, avg 406.3
c [simplification-7] removed 21 variables 0.2% (11632 remain 24%)
c [simplification-7] removed 90 irredundant clauses 0.1% (63750 remain 44%)
c [simplification-7] maximum reduction of 0% = max (0%, 0%)
c [simplification-7] full geometric conflict interval increment 67500
c [simplification-7] new conflict interval 135000
c [simplification-7] penalized conflict interval 135000 = 1 * 135000
c [simplification-7] hard conflict limit 358001 (soft 290501 + delta 67500)
c [simplification-7] new conflict limit 290501 (hard 358001)
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 -   30.4   11632    63750    187155   40622  10757 15536    9   415   13   2%    718  239    9   10   96%
c i   31.5   11631    63750    202025   53318  10764 15536    8   387   16   2%    780  163   11    9  123%
c -   34.1   11631    63749    222312   39524  10845 15546   15   111   19  13%   -440  -98   15   11  141%
c -   37.2   11631    63749    259893   42272  10896 15552   12   112   19  11%    199  -48    9   11   82%
c 
c [simplification-8] limit 290501 conflicts (hard 358001) hit after 292889 conflicts
c [quatres-6] found 19694 quaternary clauses 41% in total
c [quatres-6-1] added 1 double-self-subsuming ternary resolvents
c [quatres-6-2] added 117 single-self-subsuming ternary resolvents
c [quatres-6-2] added 220 quaternary resolvents
c [ternres-6] limit 9180861 with penalty 0 = 0 + 0
c [ternres-6] 4 schedulable variables 0%
c [ternres-6] 119 ternary resolvents (3 bin, 116 trn)
c [ternres-6] fully completed ternary resolution
c [decomp-22] removed 5 variables
c [basicprobe-3] limit 45904307 penalty 0 = 0 + 0
c [basicprobe-3-0] 338 sched 3%, 0 failed, 0 lifted, 32 hbrs
c [basicprobe-3-1] 6669 sched 57%, 4 failed, 0 lifted, 2687 hbrs
c [decomp-24] removed 13 variables
c [basicprobe-3-2] 6632 sched 57%, 0 failed, 0 lifted, 172 hbrs
c [basicprobe-3-3] 6629 sched 57%, 0 failed, 0 lifted, 18 hbrs
c [basicprobe-3-4] 6629 sched 57%, 0 failed, 0 lifted, 3 hbrs
c [basicprobe-3-5] 6629 sched 57%, 0 failed, 0 lifted, 8 hbrs
c [basicprobe-3-6] 6629 sched 57%, 0 failed, 0 lifted, 11 hbrs
c [basicprobe-3-7] 6629 sched 57%, 0 failed, 0 lifted, 2 hbrs
c [basicprobe-3-8] 6629 sched 57%, 0 failed, 0 lifted, 1 hbrs
c [basicprobe-3-8] round limit 8 hit
c [basicprobe-3-8] 4 units = 4 failed (100%) + 0 lifted (0%)
c [basicprobe-3-8] removed 13 variables, found 2934 hbrs
c [bate-2] eliminated 15 asymmetric tautologies during probing
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 685 transitive binary clauses
c [block-4] scheduling all variables this time
c [block-4] scheduled 11614 variables 100%
c [block-4] limit of 22952153 steps penalty 2 = 2 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 12 blocked clauses
c [block-4] 12 < 1/100 * 63664 = 636 considered unsuccessful
c [cce-4] boosting limit by 10
c [cce-4] limit of 114760767 steps penalty 2 = 2 + 0
c [cce-4-1] eliminated 1 clauses out of 100 (1%) of length 13
c [cce-4-1] eliminated 7 clauses out of 259 (3%) of length 10
c [cce-4-1] eliminated 1 clauses out of 773 (0%) of length 8
c [cce-4-1] eliminated 8 clauses out of 1812 (0%) of length 7
c [cce-4-1] eliminated 21 clauses out of 3048 (1%) of length 6
c [cce-4-1] eliminated 64 clauses out of 6140 (1%) of length 5
c [cce-4-1] eliminated 442 clauses out of 13728 (3%) of length 4
c [cce-4-1] completed large round (ATE)
c [cce-4-1] eliminated 544 large clauses in 36684887 steps
c [cce-4-1] allowing another 18342443 steps for small clauses
c [cce-4-1] scheduling 29046 clauses = 12407 binary + 16639 ternary
c [cce-4-1] tried to eliminate 29046 small clauses 100%
c [cce-4-1] eliminated 65 binary clauses 1%
c [cce-4-1] eliminated 565 ternary clauses 3%
c [cce-4-1] eliminated 630 small clauses 2%
c [cce-4-1] eliminated 630 small clauses in 42841695 steps
c [cce-4-1] completed small round (ATE)
c [cce-4-1] completed small and large (ATE)
c [cce-4-1] eliminated 1174 covered clauses in round 1
c [cce-4-2] completed large round (ATE)
c [cce-4-2] allowing another 17698149 steps for small clauses
c [cce-4-2] scheduling 28416 clauses = 12342 binary + 16074 ternary
c [cce-4-2] tried to eliminate 28416 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 1174 covered clauses in TOTAL during 2 rounds
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 11614 variables 100%
c [elim-5] limit of 45904307 steps penalty 2 = 2 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5-1] eliminated 181 variables 2% in round 1 in 14186170 steps
c [elim-5-1] backward subsumption/strengthening limit 14186100
c [elim-5-1-1] backward checking 1241 touched variables 11%
c [elim-5-1-1] fully completed backward checking in 1 rounds
c [elim-5-1] subsumed 3 and strengthened 5 clauses in 842679 steps
c [elim-5-1] rescheduled 17 variables 0% by backward subsumption
c [elim-5-2] eliminated 1 variables 0% in round 2 in 98312 steps
c [elim-5-2] backward subsumption/strengthening limit 98300
c [elim-5-2-1] backward checking 9 touched variables 0%
c [elim-5-2-1] fully completed backward checking in 1 rounds
c [elim-5-2] subsumed 0 and strengthened 0 clauses in 32724 steps
c [elim-5] fully completed in 2 rounds
c [elim-5] transition to [ all 0 rem 0 ] state
c [elim-5] eliminated 182 = 2% variables out of 11614 scheduled
c [bca-6] limit of 10000000 steps and 125145 added (scaled 2)
c [bca-6] 5947 out of 22866 literals actually usable 26%
c [bca-6] added 4 blocked clauses in 80483 steps
c [sweep-7] limit 2754258 penalty 0 = 0 + 0
c [sweep-7-1] 1344 pos 43.7% + 1732 neg 56.3% = 3076 sched 26.9% ret 8356
c [sweep-7-1] 2774450 steps 317 queries 179.34 avg class size
c [sweep-7-1] 6508 decisions 314 SAT calls 41.57 avg env size
c [sweep-7-1] 1495 variables remain 13% (9937 retained 87%)
c [decomp-31] removed 18 variables
c [sweep-7-1] removed 18 vars (0 failed, 15 eqs, 12 impls)
c [sweep-7] removed 18 vars in TOTAL (1 rounds, 316 queries)
c [sort-queue-8] sorted 1420 enqueued variables after 292889 conflicts
c [score-dist-8] active 9994 (88%), one 1073 (9%), zero 347 (3%)
c [score-dist-8] max exp 509, different 221 (43%)
c [score-dist-8] median active exp 495, avg 430.2
c [simplification-8] removed 217 variables 1.9% (11414 remain 23%)
c [simplification-8] removed 1563 irredundant clauses 2.5% (62186 remain 43%)
c [simplification-8] maximum reduction of 2% = max (2%, 2%)
c [simplification-8] geometric conflict interval increment 45000 = 135000 / 3
c [simplification-8] new conflict interval 180000
c [simplification-8] penalized conflict interval 180000 = 1 * 180000
c [simplification-8] hard conflict limit 562889 (soft 472889 + delta 90000)
c [simplification-8] new conflict limit 472889 (hard 562889)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c -   45.7   11414    62186    305874   47440  11395 16896   11    82   14  13%    615  -57   11   11  105%
c -   49.7   11414    62186    347704   52328  11592 16929   10   117   22   9%    808  -28   11   10  107%
c -   54.2   11414    62186    389101   56165  11709 16964    9    92   16  10%    909  -45   12   10  115%
c -   58.1   11414    62185    427812   55897  11757 16973   14    94   16  15%    960  -16   17   11  152%
c -   61.5   11414    62185    470333   59744  11836 16984   10    92   24  11%    991  -31   13   11  115%
c 
c [simplification-9] limit 472889 conflicts (hard 562889) hit after 476322 conflicts
c [quatres-7] found 20628 quaternary clauses 34% in total
c [quatres-7-1] removed 7 duplicate quaternary clauses
c [quatres-7-1] added 2 double-self-subsuming ternary resolvents
c [quatres-7-2] added 136 single-self-subsuming ternary resolvents
c [quatres-7-2] added 321 quaternary resolvents
c [ternres-7] limit 14206030 with penalty 0 = 0 + 0
c [ternres-7] all 11414 free variables schedulable
c [ternres-7] 1530 ternary resolvents (126 bin, 1404 trn)
c [ternres-7] fully completed ternary resolution
c [gauss-4] limit 710301 penalty 2 = 2 + 0
c [gauss-4] extracted 1719 xors of average arity 3.0
c [gauss-4] connected 5105 occurrences of 1009 variables (average 5.1)
c [gauss-4] limit 710301 penalty 2 = 2 + 0
c [gauss-4] fully completed
c [gauss-4] exported 0 unary, 0 binary and 1 ternary equations
c [decomp-32] removed 31 variables
c [simpleprobe-4] 838 schedulable variables 7%
c [simpleprobe-4] limit 56824123 penalty 0 = 0 + 0
c [decomp-33] removed 18 variables
c [simpleprobe-4] fully completed simple probing
c [simpleprobe-4] removed 18 variables, found 1788 hbrs, 2 units
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 1014 transitive binary clauses
c [transred-7] found 1 units
c [bca-7] limit of 10000000 steps and 124825 added (scaled 2)
c [bca-7] 4170 out of 22730 literals actually usable 18%
c [bca-7] added 0 blocked clauses in 74856 steps
c [sweep-8] limit 4261809 penalty 0 = 0 + 0
c [sweep-8-1] 777 pos 52.4% + 706 neg 47.6% = 1483 sched 13.0% ret 9881
c [sweep-8-1] 4263328 steps 421 queries 53.48 avg class size
c [sweep-8-1] 7431 decisions 427 SAT calls 36.30 avg env size
c [sweep-8-1] 262 variables remain 2% (11102 retained 98%)
c [decomp-34] removed 43 variables
c [sweep-8-1] removed 43 vars (0 failed, 39 eqs, 25 impls)
c [sweep-8] removed 43 vars in TOTAL (1 rounds, 420 queries)
c [sort-queue-9] sorted 374 enqueued variables after 476322 conflicts
c [score-dist-9] active 10947 (97%), one 364 (3%), zero 10 (0%)
c [score-dist-9] max exp 510, different 291 (57%)
c [score-dist-9] median active exp 497, avg 443.5
c [simplification-9] removed 93 variables 0.8% (11321 remain 23%)
c [simplification-9] removed 178 irredundant clauses 0.3% (62007 remain 43%)
c [simplification-9] maximum reduction of 1% = max (1%, 0%)
c [simplification-9] geometric conflict interval increment 90000 = 180000 / 2
c [simplification-9] new conflict interval 270000
c [simplification-9] penalized conflict interval 270000 = 1 * 270000
c [simplification-9] hard conflict limit 881322 (soft 746322 + delta 135000)
c [simplification-9] new conflict limit 746322 (hard 881322)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c -   66.9   11321    62003    513055   64256  13077 17737    9   124   16   7%   1007   -7   10   11   90%
c -   71.8   11321    62003    556326   68937  13138 17743   10   193   23   5%   1015   64   12   11  109%
c -   76.1   11321    62002    595463   69499  13191 17767   10    92   23  11%   1019  -40   12   11  116%
c -   81.3   11321    62002    637827   70437  13262 17771   18   109   16  16%   1021   -9   15   12  131%
c -   86.6   11321    62002    682745   75289  13320 17783   11    95   24  12%   1023  -22    6   11   58%
c i   88.1   11320    62002    695572   87344  13333 17785   11   114   29  10%   1023    3   10   11   88%
c -   91.5   11320    62002    723681   75806  13384 17797   13    84   24  15%  -4078  -25   11   11   98%
c -   97.9   11320    62002    770358   80117  13407 17798   10    84   25  12%  -1479   -0   10   11   93%
c -  102.6   11320    62002    815778   81759  13453 17805   12   119   19  10%   -228   40   12   10  122%
c 
c [simplification-10] limit 746322 conflicts (hard 881322) hit after 828930 conflicts
c [quatres-8] found 21825 quaternary clauses 28% in total
c [quatres-8-1] removed 19 duplicate quaternary clauses
c [quatres-8-1] added 2 double-self-subsuming ternary resolvents
c [quatres-8-2] added 197 single-self-subsuming ternary resolvents
c [quatres-8-2] added 227 quaternary resolvents
c [ternres-8] limit 29284460 with penalty 0 = 0 + 0
c [ternres-8] all 11320 free variables schedulable
c [ternres-8] 1998 ternary resolvents (199 bin, 1799 trn)
c [ternres-8] fully completed ternary resolution
c [card-4] limit 1830278 penalty 3 = 3 + 0
c [card-4] found 521 at-most-one constraints of average size 3.3
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 1830278 for elimination
c [card-4] 521 out of 521 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [decomp-35] removed 43 variables
c [treelook-4] limit 2928446 penalty 0 = 0 + 0 boost 1
c [treelook-4] scheduled 21955 literals 97%
c [treelook-4] scheduling used 575127 steps
c [treelook-4] scheduled completely
c [treelook-4] limit 2928446 penalty 0 = 0 + 0 boost 1
c [treelook-4] used 2929769 steps
c [treelook-4] 21497 literals remain 95%
c [treelook-4] 10599 variables remain to probed next time 94%
c [decomp-36] removed 5 variables
c [treelook-4] removed 8 variables, found 6210 hbrs
c [unhide-4] limit 732111 with penalty 3 = 3 + 0
c [unhide-4-4] 1 units, 0 failed, 4535 tauts, 0 hbrs, 37131 literals
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 736 transitive binary clauses
c [transred-8] found 1 units
c [cce-5] limit of 73211150 steps penalty 1 = 1 + 0
c [cce-5-1] eliminated 1 clauses out of 105 (1%) of length 12
c [cce-5-1] eliminated 5 clauses out of 97 (5%) of length 11
c [cce-5-1] eliminated 2 clauses out of 260 (1%) of length 10
c [cce-5-1] eliminated 2 clauses out of 785 (0%) of length 8
c [cce-5-1] incomplete large round (ACCE)
c [cce-5-1] eliminated 10 large clauses in 73211151 steps
c [cce-5-1] allowing another 36605575 steps for small clauses
c [cce-5-1] scheduling 27447 clauses = 11991 binary + 15456 ternary
c [cce-5-1] tried to eliminate 3005 small clauses 11%
c [cce-5-1] eliminated 15 binary clauses 0%
c [cce-5-1] eliminated 31 ternary clauses 0%
c [cce-5-1] eliminated 46 small clauses 0%
c [cce-5-1] eliminated 51 small clauses in 73211190 steps
c [cce-5-1] incomplete small round (ACCE)
c [cce-5-1] eliminated 61 covered clauses in round 1
c [cce-5] eliminated 61 covered clauses in TOTAL during 1 rounds
c [cce-5] 61 < 1/100 * 61844 = 618 considered unsuccessful
c [elim-6] scheduling all variables this time
c [elim-6] scheduled 11268 variables 100%
c [elim-6] limit of 292844602 steps penalty 1 = 1 + 0
c [elim-6] rescheduling of touched variables disabled
c [elim-6-1] eliminated 169 variables 1% in round 1 in 14211723 steps
c [elim-6-1] backward subsumption/strengthening limit 14211700
c [elim-6-1-1] backward checking 948 touched variables 8%
c [elim-6-1-1] fully completed backward checking in 1 rounds
c [elim-6-1] subsumed 6 and strengthened 13 clauses in 612218 steps
c [elim-6-1] rescheduled 50 variables 0% by backward subsumption
c [elim-6-2] eliminated 1 variables 0% in round 2 in 448829 steps
c [elim-6-2] backward subsumption/strengthening limit 448800
c [elim-6-2-1] backward checking 0 touched variables 0%
c [elim-6-2-1] fully completed backward checking in 1 rounds
c [elim-6-2] subsumed 0 and strengthened 0 clauses in 33498 steps
c [elim-6] fully completed in 2 rounds
c [elim-6] transition to [ all 0 rem 0 ] state
c [elim-6] eliminated 172 = 2% variables out of 11268 scheduled
c [sweep-9] limit 8785338 penalty 0 = 0 + 0
c [sweep-9-1] 110 pos 44.7% + 136 neg 55.3% = 246 sched 2.2% ret 10850
c [sweep-9-1] 1734220 steps 156 queries 19.94 avg class size
c [sweep-9-1] 3270 decisions 151 SAT calls 40.34 avg env size
c [sweep-9-1] fully completed sweeping round
c [decomp-37] removed 32 variables
c [sweep-9-1] removed 32 vars (0 failed, 18 eqs, 9 impls)
c [sweep-9-2] 4923 pos 44.5% + 6141 neg 55.5% = 11064 sched 100.0% ret 0
c [sweep-9-2] 7343710 steps 350 queries 271.56 avg class size
c [sweep-9-2] 9963 decisions 338 SAT calls 60.13 avg env size
c [sweep-9-2] 4685 variables remain 42% (6378 retained 58%)
c [decomp-38] removed 36 variables
c [sweep-9-2] removed 36 vars (0 failed, 30 eqs, 38 impls)
c [sweep-9] removed 68 vars in TOTAL (2 rounds, 504 queries)
c [sort-queue-10] sorted 559 enqueued variables after 828930 conflicts
c [score-dist-10] active 10469 (95%), one 557 (5%), zero 2 (0%)
c [score-dist-10] max exp 511, different 207 (40%)
c [score-dist-10] median active exp 479, avg 428.5
c [simplification-10] removed 292 variables 2.6% (11028 remain 22%)
c [simplification-10] removed 1021 irredundant clauses 1.6% (60981 remain 42%)
c [simplification-10] maximum reduction of 3% = max (3%, 2%)
c [simplification-10] geometric conflict interval increment 67500 = 270000 / 4
c [simplification-10] new conflict interval 337500
c [simplification-10] penalized conflict interval 337500 = 1 * 337500
c [simplification-10] hard conflict limit 1335180 (soft 1166430 + delta 168750)
c [simplification-10] new conflict limit 1166430 (hard 1335180)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i  112.9   11027    60981    834492   95120  13303 19280   12   123   23  10%     83   35   11   11  106%
c -  116.7   11027    60981    861281   80627  13325 19289   11    57   25  19%  -1066  -34   12   11  108%
c -  122.0   11027    60981    906470   84439  13363 19312   15   155   26  10%    -25   56   23   11  201%
c i  122.3   11026    60981    908910   86711  13368 19312   14   127   30  11%     13   27   14   11  123%
c i  122.6   11025    60981    910830   88518  13378 19313   14   123   30  11%   -924   22   13   11  114%
c i  123.3   11024    60981    918318   95436  13385 19320   10    82   31  12%   -902  -19    6   11   56%
c -  126.5   11024    60981    951939   85176  13418 19322    8    67   26  13%   -200  -27    9   11   81%
c -  130.3   11024    60979   1001908   87585  13479 19329   10   204   18   5%    453   87   12   10  119%
c i  130.4   11023    60979   1002001   87669  13479 19329   10   203   22   5%    454   86   13   10  121%
c -  135.9   11023    60976   1050400   90541  13519 19334   13   105   27  12%    117  -11   14   11  125%
c -  140.9   11023    60976   1099235   94500  13566 19341   10    97   27  10%    593  -12    9   11   80%
c -  146.0   11023    60976   1149729   94677  13581 19343   10    73   20  14%    825  -25   10   11   89%
c 
c [simplification-11] limit 1166430 conflicts (hard 1335180) hit after 1180047 conflicts
c [quatres-9] found 22513 quaternary clauses 26% in total
c [quatres-9-1] removed 21 duplicate quaternary clauses
c [quatres-9-1] added 7 double-self-subsuming ternary resolvents
c [quatres-9-2] added 290 single-self-subsuming ternary resolvents
c [quatres-9-2] added 434 quaternary resolvents
c [ternres-9] limit 42438644 with penalty 0 = 0 + 0
c [ternres-9] all 11023 free variables schedulable
c [ternres-9] 4525 ternary resolvents (232 bin, 4293 trn)
c [ternres-9] fully completed ternary resolution
c [gauss-5] limit 4243864 penalty 1 = 1 + 0
c [gauss-5] extracted 5265 xors of average arity 3.1
c [gauss-5] connected 16087 occurrences of 1175 variables (average 13.7)
c [gauss-5] limit 4243864 penalty 1 = 1 + 0
c [gauss-5] fully completed
c [decomp-39] removed 46 variables
c [gauss-5] exported 1 unary, 0 binary and 1 ternary equations
c [basicprobe-4] limit 212193220 penalty 0 = 0 + 0
c [basicprobe-4-0] 6340 sched 58%, 36 failed, 0 lifted, 4316 hbrs
c [decomp-41] removed 110 variables
c [basicprobe-4-1] 6253 sched 58%, 1 failed, 0 lifted, 435 hbrs
c [decomp-42] removed 1 variables
c [basicprobe-4-2] 6251 sched 58%, 0 failed, 0 lifted, 54 hbrs
c [basicprobe-4-3] 6251 sched 58%, 0 failed, 0 lifted, 10 hbrs
c [basicprobe-4-4] 6251 sched 58%, 0 failed, 0 lifted, 14 hbrs
c [basicprobe-4-5] 6250 sched 58%, 0 failed, 0 lifted, 16 hbrs
c [basicprobe-4-6] 6250 sched 58%, 0 failed, 0 lifted, 5 hbrs
c [basicprobe-4-7] 6250 sched 58%, 0 failed, 0 lifted, 3 hbrs
c [basicprobe-4-8] 6250 sched 58%, 0 failed, 0 lifted, 1 hbrs
c [basicprobe-4-8] round limit 8 hit
c [basicprobe-4-8] 37 units = 37 failed (100%) + 0 lifted (0%)
c [basicprobe-4-8] removed 111 variables, found 4854 hbrs
c [bate-3] eliminated 18 asymmetric tautologies during probing
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 1018 transitive binary clauses
c [elim-7] scheduling all variables this time
c [elim-7] scheduled 10866 variables 100%
c [elim-7] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-7] rescheduling of touched variables disabled
c [elim-7-1] eliminated 102 variables 1% in round 1 in 19934388 steps
c [elim-7-1] backward subsumption/strengthening limit 19934300
c [elim-7-1-1] backward checking 570 touched variables 5%
c [elim-7-1-1] fully completed backward checking in 1 rounds
c [elim-7-1] subsumed 2 and strengthened 4 clauses in 545142 steps
c [elim-7-1] rescheduled 27 variables 0% by backward subsumption
c [elim-7-2] eliminated 2 variables 0% in round 2 in 972353 steps
c [elim-7-2] backward subsumption/strengthening limit 972300
c [elim-7-2-1] backward checking 25 touched variables 0%
c [elim-7-2-1] fully completed backward checking in 1 rounds
c [elim-7-2] subsumed 0 and strengthened 2 clauses in 48036 steps
c [elim-7-2] rescheduled 16 variables 0% by backward subsumption
c [elim-7-3] no variable eliminated in round 3 in 52214 steps
c [elim-7] fully completed in 3 rounds
c [elim-7] transition to [ all 0 rem 0 ] state
c [elim-7] eliminated 104 = 1% variables out of 10866 scheduled
c [elim-7] 104 < 1/100 * 10866 = 108 considered unsuccessful
c [bca-8] limit of 10000000 steps and 120465 added (scaled 2)
c [bca-8] 3137 out of 21526 literals actually usable 15%
c [bca-8] added 12 blocked clauses in 125761 steps
c [sweep-10] limit 12731593 penalty 0 = 0 + 0
c [sweep-10-1] 2110 pos 46.7% + 2412 neg 53.3% = 4522 sched 42.0% ret 6240
c [sweep-10-1] 12815217 steps 761 queries 72.81 avg class size
c [sweep-10-1] 16093 decisions 737 SAT calls 50.54 avg env size
c [sweep-10-1] 592 variables remain 6% (10170 retained 94%)
c [decomp-49] removed 180 variables
c [sweep-10-1] removed 180 vars (0 failed, 170 eqs, 142 impls)
c [sweep-10] removed 180 vars in TOTAL (1 rounds, 760 queries)
c [sort-queue-11] sorted 1197 enqueued variables after 1180047 conflicts
c [score-dist-11] active 9385 (89%), one 1195 (11%), zero 2 (0%)
c [score-dist-11] max exp 512, different 245 (48%)
c [score-dist-11] median active exp 502, avg 402.2
c [simplification-11] removed 441 variables 4.0% (10582 remain 21%)
c [simplification-11] removed 1211 irredundant clauses 2.0% (59765 remain 41%)
c [simplification-11] maximum reduction of 4% = max (4%, 2%)
c [simplification-11] geometric conflict interval increment 67500 = 337500 / 5
c [simplification-11] new conflict interval 405000
c [simplification-11] penalized conflict interval 405000 = 1 * 405000
c [simplification-11] hard conflict limit 1787547 (soft 1585047 + delta 202500)
c [simplification-11] new conflict limit 1585047 (hard 1787547)
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 -  155.5   10582    59765   1201983   95492  14691 20700   13    76   20  17%    934   -4   13   11  112%
c i  158.7   10581    59765   1235810  124048  14718 20702   11    54   28  21%    970  -15   13   12  113%
c i  158.9   10580    59763   1237500  125574  14719 20703   13    80   28  17%  -1933   11   13   12  107%
c -  161.1   10580    59761   1254541   98770  14731 20705   15    48   30  31%  -1826  -21   16   12  134%
c i  164.6   10579    59760   1293242  132269  14753 20707   12    80   37  15%   -555   21   11   12   92%
c -  165.9   10579    59758   1304961  100036  14759 20707   16    64   30  24%  -1036   -1   17   12  137%
c i  170.4   10578    59752   1346465  136978  14797 20710   10   175   38   6%    -70  109   11   12   94%
c -  171.6   10578    59752   1356579  102463  14804 20710   10    70   30  14%   -637   -5   13   11  113%
c i  173.8   10577    59744   1374477  119080  14830 20718   11   135   36   8%   -240   53    8   11   74%
c i  174.3   10576    59744   1378125  122483  14832 20720   12   118   38  11%   -580   33   17   11  146%
c i  178.3   10575    59743   1405703  145379  14857 20722   10   130   39   7%    -75   50    8   11   69%
c -  178.9   10575    59743   1410296  105157  14859 20722   12   103   31  12%   -404   20   12   12  106%
c -  186.6   10575    59740   1465603  107372  14915 20734   10    86   31  11%    408   -4   11   11   99%
c -  195.9   10575    59740   1522811  107153  14932 20736   14    89   22  16%    767   -3   15   12  126%
c -  203.4   10575    59732   1578404  112216  14956 20742    8    50   32  16%    914  -37   13   11  112%
c 
c [simplification-12] limit 1585047 conflicts (hard 1787547) hit after 1592366 conflicts
c [quatres-10] found 22933 quaternary clauses 23% in total
c [quatres-10-1] removed 66 duplicate quaternary clauses
c [quatres-10-1] added 6 double-self-subsuming ternary resolvents
c [quatres-10-2] added 240 single-self-subsuming ternary resolvents
c [quatres-10-2] added 339 quaternary resolvents
c [ternres-10] limit 65177860 with penalty 0 = 0 + 0
c [ternres-10] all 10575 free variables schedulable
c [ternres-10] 3044 ternary resolvents (195 bin, 2849 trn)
c [ternres-10] fully completed ternary resolution
c [gauss-6] limit 13035572 penalty 0 = 0 + 0
c [gauss-6] extracted 4784 xors of average arity 3.1
c [gauss-6] connected 14638 occurrences of 1076 variables (average 13.6)
c [gauss-6] limit 13035572 penalty 0 = 0 + 0
c [gauss-6] fully completed
c [gauss-6] exported 0 unary, 0 binary and 1 ternary equations
c [decomp-50] removed 39 variables
c [simpleprobe-5] all 10536 free variables schedulable
c [simpleprobe-5] limit 200000000 penalty 0 = 0 + 0
c [decomp-51] removed 59 variables
c [simpleprobe-5] fully completed simple probing
c [simpleprobe-5] removed 59 variables, found 3421 hbrs, 9 units
c [unhide-5] limit 3258893 with penalty 2 = 2 + 0
c [unhide-5-6] 0 units, 0 failed, 4014 tauts, 0 hbrs, 51340 literals
c [transred-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 1055 transitive binary clauses
c [transred-10] found 1 units
c [block-5] scheduling all variables this time
c [block-5] scheduled 10476 variables 100%
c [block-5] limit of 81472325 steps penalty 3 = 3 + 0
c [block-5] fully completed
c [block-5] transition to [ all 0 rem 0 ] state
c [block-5] eliminated 97 blocked clauses
c [block-5] 97 < 1/100 * 59202 = 592 considered unsuccessful
c [bca-9] limit of 10000000 steps and 118959 added (scaled 2)
c [bca-9] 2925 out of 20934 literals actually usable 14%
c [bca-9] added 4 blocked clauses in 129623 steps
c [sweep-11] boosting sweeping limit by 10
c [sweep-11] limit 195533580 penalty 0 = 0 + 0
c [sweep-11-1] 240 pos 41.9% + 333 neg 58.1% = 573 sched 5.5% ret 9893
c [sweep-11-1] 4454299 steps 294 queries 23.74 avg class size
c [sweep-11-1] 5527 decisions 278 SAT calls 44.19 avg env size
c [sweep-11-1] fully completed sweeping round
c [decomp-52] removed 59 variables
c [sweep-11-1] removed 59 vars (0 failed, 53 eqs, 48 impls)
c [sweep-11-2] 4523 pos 43.5% + 5884 neg 56.5% = 10407 sched 100.0% ret 0
c [sweep-11-2] 27730182 steps 1194 queries 60.24 avg class size
c [sweep-11-2] 25894 decisions 1110 SAT calls 57.43 avg env size
c [sweep-11-2] fully completed sweeping round
c [decomp-53] removed 243 variables
c [sweep-11-2] removed 243 vars (0 failed, 242 eqs, 213 impls)
c [sweep-11-3] 4435 pos 43.6% + 5729 neg 56.4% = 10164 sched 100.0% ret 0
c [sweep-11-3] 20869981 steps 1076 queries 66.75 avg class size
c [sweep-11-3] 24049 decisions 1060 SAT calls 55.08 avg env size
c [sweep-11-3] fully completed sweeping round
c [decomp-54] removed 91 variables
c [sweep-11-3] removed 91 vars (0 failed, 98 eqs, 59 impls)
c [sweep-11] removed 393 vars in TOTAL (3 rounds, 2561 queries)
c [sort-queue-12] sorted 915 enqueued variables after 1592366 conflicts
c [score-dist-12] active 9158 (91%), one 913 (9%), zero 2 (0%)
c [score-dist-12] max exp 512, different 171 (33%)
c [score-dist-12] median active exp 504, avg 483.2
c [simplification-12] removed 502 variables 4.7% (10073 remain 20%)
c [simplification-12] removed 1078 irredundant clauses 1.8% (58653 remain 41%)
c [simplification-12] maximum reduction of 5% = max (5%, 2%)
c [simplification-12] large reduction 5% >= 5% limit
c [simplification-12] next conflict interval 15923 = min (1592366/100, 405000)
c [simplification-12] penalized conflict interval 15923 = 1 * 15923
c [simplification-12] hard conflict limit 1618289 (soft 1608289 + delta 10000)
c [simplification-12] new conflict limit 1608289 (hard 1618289)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i  211.6   10072    58650   1599579  131042  13776 20145   15    90   29  16%    944   11   16   12  134%
c 
c [simplification-13] limit 1608289 conflicts (hard 1618289) hit after 1618289 conflicts
c [quatres-11] found 22759 quaternary clauses 23% in total
c [quatres-11-1] removed 85 duplicate quaternary clauses
c [quatres-11-1] added 18 double-self-subsuming ternary resolvents
c [quatres-11-2] added 248 single-self-subsuming ternary resolvents
c [quatres-11-2] added 364 quaternary resolvents
c [ternres-11] limit 66984067 with penalty 0 = 0 + 0
c [ternres-11] all 10072 free variables schedulable
c [ternres-11] 4224 ternary resolvents (215 bin, 4009 trn)
c [ternres-11] fully completed ternary resolution
c [gauss-7] limit 13396813 penalty 0 = 0 + 0
c [gauss-7] extracted 4613 xors of average arity 3.1
c [gauss-7] connected 14191 occurrences of 991 variables (average 14.3)
c [gauss-7] limit 13396813 penalty 0 = 0 + 0
c [gauss-7] fully completed
c [decomp-55] removed 29 variables
c [gauss-7] exported 1 unary, 0 binary and 2 ternary equations
c [treelook-5] limit 6698406 penalty 0 = 0 + 0 boost 1
c [treelook-5] scheduled 19574 literals 97%
c [treelook-5] scheduling used 707892 steps
c [treelook-5] scheduled completely
c [treelook-5] limit 6698406 penalty 0 = 0 + 0 boost 1
c [treelook-5] used 6698947 steps
c [treelook-5] 16955 literals remain 85%
c [treelook-5] 9296 variables remain to probed next time 93%
c [decomp-57] removed 11 variables
c [treelook-5] removed 29 variables, found 9530 hbrs
c [transred-11] limit 2000000 with penalty 0 = 0 + 0
c [transred-11] removed 1519 transitive binary clauses
c [transred-11] found 2 units
c [cce-6] limit of 83730084 steps penalty 2 = 2 + 0
c [cce-6-1] eliminated 2 clauses out of 85 (2%) of length 12
c [cce-6-1] eliminated 10 clauses out of 91 (11%) of length 11
c [cce-6-1] eliminated 36 clauses out of 257 (14%) of length 10
c [cce-6-1] eliminated 14 clauses out of 441 (3%) of length 9
c [cce-6-1] eliminated 25 clauses out of 755 (3%) of length 8
c [cce-6-1] eliminated 82 clauses out of 1485 (6%) of length 7
c [cce-6-1] eliminated 198 clauses out of 2888 (7%) of length 6
c [cce-6-1] eliminated 616 clauses out of 5894 (10%) of length 5
c [cce-6-1] eliminated 861 clauses out of 12840 (7%) of length 4
c [cce-6-1] completed large round (ATE)
c [cce-6-1] eliminated 1844 large clauses in 31770834 steps
c [cce-6-1] allowing another 15885417 steps for small clauses
c [cce-6-1] scheduling 18995 clauses = 11056 binary + 7939 ternary
c [cce-6-1] tried to eliminate 18995 small clauses 100%
c [cce-6-1] eliminated 245 binary clauses 2%
c [cce-6-1] eliminated 396 ternary clauses 5%
c [cce-6-1] eliminated 641 small clauses 3%
c [cce-6-1] eliminated 652 small clauses in 30929426 steps
c [cce-6-1] completed small round (ATE)
c [cce-6-1] eliminated 2496 covered clauses in round 1
c [cce-6-2] completed large round (ATE)
c [cce-6-2] allowing another 14272867 steps for small clauses
c [cce-6-2] scheduling 18354 clauses = 10811 binary + 7543 ternary
c [cce-6-2] tried to eliminate 18354 small clauses 100%
c [cce-6-2] completed small round (ATE)
c [cce-6-2] eliminated 0 covered clauses in round 2
c [cce-6] eliminated 2496 covered clauses in TOTAL during 2 rounds
c [elim-8] scheduling all variables this time
c [elim-8] scheduled 10012 variables 100%
c [elim-8] boosting limit by 20
c [elim-8] limit of 8000000000 steps penalty 1 = 1 + 0
c [elim-8] rescheduling of touched variables disabled
c [elim-8-1] eliminated 472 variables 5% in round 1 in 15676533 steps
c [elim-8-1] backward subsumption/strengthening limit 15676500
c [elim-8-1-1] backward checking 1803 touched variables 18%
c [elim-8-1-1] fully completed backward checking in 1 rounds
c [elim-8-1] subsumed 2 and strengthened 10 clauses in 865454 steps
c [elim-8-1] rescheduled 53 variables 1% by backward subsumption
c [elim-8-2] eliminated 4 variables 0% in round 2 in 1015496 steps
c [elim-8-2] backward subsumption/strengthening limit 1015400
c [elim-8-2-1] backward checking 25 touched variables 0%
c [elim-8-2-1] fully completed backward checking in 1 rounds
c [elim-8-2] subsumed 0 and strengthened 2 clauses in 105850 steps
c [elim-8-2] rescheduled 5 variables 0% by backward subsumption
c [elim-8-3] eliminated 1 variables 0% in round 3 in 11211 steps
c [elim-8-3] backward subsumption/strengthening limit 11200
c [elim-8-3-1] backward checking 17 touched variables 0%
c [elim-8-3-1] incomplete backward checking 2 remain 12%
c [elim-8-3] subsumed 0 and strengthened 0 clauses in 11288 steps
c [elim-8] fully completed in 3 rounds
c [elim-8] transition to [ all 0 rem 0 ] state
c [elim-8] eliminated 477 = 5% variables out of 10012 scheduled
c [bca-10] limit of 10000000 steps and 107955 added (scaled 2)
c [bca-10] 2651 out of 19072 literals actually usable 14%
c [bca-10] added 29 blocked clauses in 140347 steps
c [sweep-12] limit 20095220 penalty 0 = 0 + 0
c [sweep-12-1] 4075 pos 42.7% + 5460 neg 57.3% = 9535 sched 100.0% ret 0
c [sweep-12-1] 20099127 steps 863 queries 75.33 avg class size
c [sweep-12-1] 23142 decisions 831 SAT calls 74.18 avg env size
c [sweep-12-1] 240 variables remain 3% (9294 retained 97%)
c [decomp-58] removed 83 variables
c [sweep-12-1] removed 83 vars (0 failed, 87 eqs, 77 impls)
c [sweep-12] removed 83 vars in TOTAL (1 rounds, 862 queries)
c [sort-queue-13] sorted 591 enqueued variables after 1618289 conflicts
c [score-dist-13] active 8861 (94%), one 589 (6%), zero 2 (0%)
c [score-dist-13] max exp 511, different 179 (35%)
c [score-dist-13] median active exp 499, avg 472.5
c [simplification-13] removed 620 variables 6.2% (9452 remain 19%)
c [simplification-13] removed 5125 irredundant clauses 8.7% (53517 remain 37%)
c [simplification-13] maximum reduction of 9% = max (6%, 9%)
c [simplification-13] large reduction 9% >= 5% limit
c [simplification-13] next conflict interval 16182 = min (1618289/100, 405000)
c [simplification-13] penalized conflict interval 16182 = 1 * 16182
c [simplification-13] hard conflict limit 1644471 (soft 1634471 + delta 10000)
c [simplification-13] new conflict limit 1634471 (hard 1644471)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i  219.0    9451    53517   1618671  135525  15097 24415   14    92   32  15%  -1335   12   15   12  118%
c -  221.5    9451    53513   1638515  105874  15118 24418   10    39   21  27%   -943  -38   14   12  115%
c 
c [simplification-14] limit 1634471 conflicts (hard 1644471) hit after 1644472 conflicts
c [quatres-12] found 21049 quaternary clauses 23% in total
c [quatres-12-1] removed 44 duplicate quaternary clauses
c [quatres-12-1] added 6 double-self-subsuming ternary resolvents
c [quatres-12-2] added 117 single-self-subsuming ternary resolvents
c [quatres-12-2] added 223 quaternary resolvents
c [ternres-12] limit 68415162 with penalty 0 = 0 + 0
c [ternres-12] all 9451 free variables schedulable
c [ternres-12] 1394 ternary resolvents (81 bin, 1313 trn)
c [ternres-12] fully completed ternary resolution
c [gauss-8] limit 13683032 penalty 0 = 0 + 0
c [gauss-8] extracted 4187 xors of average arity 3.1
c [gauss-8] connected 12909 occurrences of 871 variables (average 14.8)
c [gauss-8] limit 13683032 penalty 0 = 0 + 0
c [gauss-8] fully completed
c [gauss-8] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-59] removed 9 variables
c [basicprobe-5] limit 342075813 penalty 0 = 0 + 0
c [basicprobe-5-0] 5506 sched 58%, 4 failed, 0 lifted, 1059 hbrs
c [decomp-60] removed 9 variables
c [basicprobe-5-1] 5477 sched 58%, 0 failed, 0 lifted, 34 hbrs
c [basicprobe-5-2] 5477 sched 58%, 0 failed, 0 lifted, 1 hbrs
c [basicprobe-5-3] 5477 sched 58%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-5-3] fully completed probing
c [basicprobe-5-3] 4 units = 4 failed (100%) + 0 lifted (0%)
c [basicprobe-5-3] removed 9 variables, found 1094 hbrs
c [bate-4] eliminated 11 asymmetric tautologies during probing
c [transred-12] limit 2000000 with penalty 0 = 0 + 0
c [transred-12] removed 1034 transitive binary clauses
c [elim-9] scheduling all variables this time
c [elim-9] scheduled 9433 variables 100%
c [elim-9] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-9] rescheduling of touched variables disabled
c [elim-9-1] eliminated 66 variables 1% in round 1 in 15416763 steps
c [elim-9-1] backward subsumption/strengthening limit 15416700
c [elim-9-1-1] backward checking 303 touched variables 3%
c [elim-9-1-1] fully completed backward checking in 1 rounds
c [elim-9-1] subsumed 1 and strengthened 15 clauses in 297011 steps
c [elim-9-1] rescheduled 28 variables 0% by backward subsumption
c [elim-9-2] no variable eliminated in round 2 in 87662 steps
c [elim-9] fully completed in 2 rounds
c [elim-9] transition to [ all 0 rem 0 ] state
c [elim-9] eliminated 66 = 1% variables out of 9433 scheduled
c [elim-9] 66 < 1/100 * 9433 = 94 considered unsuccessful
c [bca-11] limit of 10000000 steps and 106682 added (scaled 2)
c [bca-11] 2670 out of 18736 literals actually usable 14%
c [bca-11] added 12 blocked clauses in 115486 steps
c [sweep-13] limit 20524548 penalty 0 = 0 + 0
c [sweep-13-1] 88 pos 38.1% + 143 neg 61.9% = 231 sched 2.5% ret 9136
c [sweep-13-1] 1300224 steps 135 queries 17.83 avg class size
c [sweep-13-1] 2575 decisions 133 SAT calls 42.95 avg env size
c [sweep-13-1] fully completed sweeping round
c [decomp-63] removed 5 variables
c [sweep-13-1] removed 5 vars (0 failed, 3 eqs, 3 impls)
c [sweep-13-2] 4049 pos 43.2% + 5313 neg 56.8% = 9362 sched 100.0% ret 0
c [sweep-13-2] 17937062 steps 965 queries 59.82 avg class size
c [sweep-13-2] 21555 decisions 957 SAT calls 57.15 avg env size
c [sweep-13-2] fully completed sweeping round
c [decomp-64] removed 56 variables
c [sweep-13-2] removed 56 vars (0 failed, 63 eqs, 49 impls)
c [sweep-13-3] 4026 pos 43.3% + 5280 neg 56.7% = 9306 sched 100.0% ret 0
c [sweep-13-3] 1375597 steps 44 queries 1070.84 avg class size
c [sweep-13-3] 1755 decisions 43 SAT calls 86.19 avg env size
c [sweep-13-3] 8479 variables remain 91% (827 retained 9%)
c [sweep-13-3] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-13] removed 61 vars in TOTAL (3 rounds, 1141 queries)
c [sort-queue-14] sorted 546 enqueued variables after 1644472 conflicts
c [score-dist-14] active 8760 (94%), one 545 (6%), zero 1 (0%)
c [score-dist-14] max exp 511, different 182 (36%)
c [score-dist-14] median active exp 502, avg 471.8
c [simplification-14] removed 145 variables 1.5% (9306 remain 19%)
c [simplification-14] removed 601 irredundant clauses 1.1% (52912 remain 37%)
c [simplification-14] maximum reduction of 2% = max (2%, 1%)
c [simplification-14] geometric conflict interval increment 135000 = 405000 / 3
c [simplification-14] new conflict interval 540000
c [simplification-14] penalized conflict interval 540000 = 1 * 540000
c [simplification-14] hard conflict limit 2454472 (soft 2184472 + delta 270000)
c [simplification-14] new conflict limit 2184472 (hard 2454472)
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 -  230.4    9306    52904   1697242  109338  15432 24358   10    83   29  12%    221  -21   13   12  111%
c -  235.9    9306    52904   1750349  112105  15441 24363   16    61   30  27%    667 -133   18   12  152%
c -  241.7    9306    52904   1803825  113438  15465 24366   11   110   30  10%    866  -17   12   12  103%
c -  248.4    9306    52903   1859866  113617  15489 24367   12    18   30  64%    957  -64   11   13   88%
c -  256.5    9306    52903   1925276  116454  15493 24367   11    23   30  48%    999  -15   10   11   92%
c -  264.4    9306    52903   1981948  115774  15547 24370   14    72   30  20%   1014   -1   13   13  102%
c -  272.0    9306    52903   2041173  121125  15568 24371    9    52   31  17%   1020  -20    8   12   69%
c -  281.2    9306    52903   2096200  120955  15588 24373   17    73   31  24%   1022    5   17   13  129%
c -  290.0    9306    52903   2155861  122937  15598 24374   11    83   48  14%   1023   17   10   13   78%
c 
c [simplification-15] limit 2184472 conflicts (hard 2454472) hit after 2184473 conflicts
c [quatres-13] found 21405 quaternary clauses 21% in total
c [quatres-13-1] removed 20 duplicate quaternary clauses
c [quatres-13-1] added 1 double-self-subsuming ternary resolvents
c [quatres-13-2] added 58 single-self-subsuming ternary resolvents
c [quatres-13-2] added 172 quaternary resolvents
c [ternres-13] limit 100795944 with penalty 0 = 0 + 0
c [ternres-13] all 9306 free variables schedulable
c [ternres-13] 2115 ternary resolvents (107 bin, 2008 trn)
c [ternres-13] fully completed ternary resolution
c [card-5] limit 3149873 penalty 4 = 4 + 0
c [card-5] found 601 at-most-one constraints of average size 3.2
c [card-5] no at-most-two constraint found
c [card-5] using previous limit 3149873 for elimination
c [card-5] 601 out of 601 constraints (100%) meet size limits
c [card-5] no units found
c [card-5] no at-most-one constraints generated
c [decomp-66] removed 6 variables
c [simpleprobe-6] all 9300 free variables schedulable
c [simpleprobe-6] limit 200000000 penalty 0 = 0 + 0
c [decomp-67] removed 14 variables
c [simpleprobe-6] fully completed simple probing
c [simpleprobe-6] removed 14 variables, found 3418 hbrs, 1 units
c [unhide-6] limit 2500000 with penalty 3 = 3 + 0
c [unhide-6-8] 0 units, 0 failed, 6148 tauts, 0 hbrs, 76844 literals
c [transred-13] limit 2000000 with penalty 0 = 0 + 0
c [transred-13] removed 1045 transitive binary clauses
c [cce-7] limit of 251989860 steps penalty 1 = 1 + 0
c [cce-7-1] eliminated 2 clauses out of 3 (67%) of length 20
c [cce-7-1] eliminated 7 clauses out of 94 (7%) of length 12
c [cce-7-1] eliminated 5 clauses out of 82 (6%) of length 11
c [cce-7-1] eliminated 17 clauses out of 255 (7%) of length 10
c [cce-7-1] eliminated 23 clauses out of 493 (5%) of length 9
c [cce-7-1] eliminated 35 clauses out of 784 (4%) of length 8
c [cce-7-1] eliminated 73 clauses out of 1405 (5%) of length 7
c [cce-7-1] eliminated 151 clauses out of 2661 (6%) of length 6
c [cce-7-1] eliminated 384 clauses out of 5362 (7%) of length 5
c [cce-7-1] eliminated 482 clauses out of 11749 (4%) of length 4
c [cce-7-1] completed large round (ACCE)
c [cce-7-1] eliminated 1179 large clauses in 98757133 steps
c [cce-7-1] allowing another 49378566 steps for small clauses
c [cce-7-1] scheduling 17246 clauses = 10023 binary + 7223 ternary
c [cce-7-1] tried to eliminate 17246 small clauses 100%
c [cce-7-1] eliminated 257 binary clauses 3%
c [cce-7-1] eliminated 230 ternary clauses 3%
c [cce-7-1] eliminated 487 small clauses 3%
c [cce-7-1] eliminated 487 small clauses in 69252111 steps
c [cce-7-1] completed small round (ACCE)
c [cce-7-1] completed small and large (ACCE)
c [cce-7-1] eliminated 1666 covered clauses in round 1
c [cce-7-2] eliminated 1 clauses out of 238 (0%) of length 10
c [cce-7-2] eliminated 1 clauses out of 749 (0%) of length 8
c [cce-7-2] eliminated 2 clauses out of 1332 (0%) of length 7
c [cce-7-2] eliminated 2 clauses out of 2510 (0%) of length 6
c [cce-7-2] eliminated 9 clauses out of 4978 (0%) of length 5
c [cce-7-2] eliminated 25 clauses out of 11267 (0%) of length 4
c [cce-7-2] completed large round (ACCE)
c [cce-7-2] eliminated 40 large clauses in 83578992 steps
c [cce-7-2] allowing another 41789496 steps for small clauses
c [cce-7-2] scheduling 16760 clauses = 9766 binary + 6994 ternary
c [cce-7-2] tried to eliminate 16760 small clauses 100%
c [cce-7-2] eliminated 12 binary clauses 0%
c [cce-7-2] eliminated 6 ternary clauses 0%
c [cce-7-2] eliminated 18 small clauses 0%
c [cce-7-2] eliminated 18 small clauses in 60919963 steps
c [cce-7-2] completed small round (ACCE)
c [cce-7-2] eliminated 58 covered clauses in round 2
c [cce-7-3] eliminated 1 clauses out of 4969 (0%) of length 5
c [cce-7-3] completed large round (ACCE)
c [cce-7-3] eliminated 1 large clauses in 83323915 steps
c [cce-7-3] allowing another 41661957 steps for small clauses
c [cce-7-3] scheduling 16742 clauses = 9754 binary + 6988 ternary
c [cce-7-3] tried to eliminate 16742 small clauses 100%
c [cce-7-3] completed small round (ACCE)
c [cce-7-3] eliminated 1 covered clauses in round 3
c [cce-7] eliminated 1725 covered clauses in TOTAL during 3 rounds
c [bca-12] limit of 10000000 steps and 102876 added (scaled 2)
c [bca-12] 2672 out of 18574 literals actually usable 14%
c [bca-12] added 10 blocked clauses in 153224 steps
c [sweep-14] limit 30238783 penalty 0 = 0 + 0
c [sweep-14-1] 3823 pos 45.2% + 4636 neg 54.8% = 8459 sched 91.1% ret 827
c [sweep-14-1] 24505821 steps 954 queries 73.90 avg class size
c [sweep-14-1] 22462 decisions 947 SAT calls 55.46 avg env size
c [sweep-14-1] fully completed sweeping round
c [decomp-68] removed 42 variables
c [sweep-14-1] removed 42 vars (0 failed, 42 eqs, 30 impls)
c [sweep-14-2] 4138 pos 44.8% + 5106 neg 55.2% = 9244 sched 100.0% ret 0
c [sweep-14-2] 5841663 steps 141 queries 320.60 avg class size
c [sweep-14-2] 4718 decisions 140 SAT calls 79.19 avg env size
c [sweep-14-2] 6141 variables remain 66% (3103 retained 34%)
c [decomp-69] removed 3 variables
c [sweep-14-2] removed 3 vars (0 failed, 2 eqs, 3 impls)
c [sweep-14] removed 45 vars in TOTAL (2 rounds, 1093 queries)
c [sort-queue-15] sorted 2217 enqueued variables after 2184473 conflicts
c [score-dist-15] active 7024 (76%), one 2216 (24%), zero 1 (0%)
c [score-dist-15] max exp 511, different 207 (40%)
c [score-dist-15] median active exp 503, avg 434.2
c [simplification-15] removed 65 variables 0.7% (9241 remain 19%)
c [simplification-15] removed 1902 irredundant clauses 3.6% (51001 remain 35%)
c [simplification-15] maximum reduction of 4% = max (1%, 4%)
c [simplification-15] geometric conflict interval increment 108000 = 540000 / 5
c [simplification-15] new conflict interval 648000
c [simplification-15] penalized conflict interval 648000 = 1 * 648000
c [simplification-15] hard conflict limit 3156473 (soft 2832473 + delta 324000)
c [simplification-15] new conflict limit 2832473 (hard 3156473)
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 -  318.1    9241    51001   2212407  123825  16098 22664   14    45   24  30%   1024  -31   13   13   99%
c -  328.1    9241    51001   2273968  126160  16101 22664   11    71   35  16%   1024    4    8   13   58%
c -  336.9    9241    51001   2333732  128545  16105 22665    8    42   36  19%   1024  -42    8   12   64%
c -  346.4    9241    51000   2390294  126330  16118 22665   20    62   35  31%   1024  -15   18   15  118%
c -  356.5    9241    51000   2452046  129017  16128 22665   12    59   35  20%   1024  -11    9   15   61%
c -  367.5    9241    51000   2519130  134231  16139 22665    8    35   36  23%   1024  -18    8   12   64%
c -  378.5    9241    51000   2578888  134970  16144 22665   11    52   36  22%   1024   -5   12   14   85%
c -  387.8    9241    51000   2639721  134327  16154 22667   14    78   36  18%   1024   13   13   16   85%
c -  396.7    9241    51000   2703008  136441  16157 22667    9    42   36  22%   1024  -15   11   14   82%
c -  406.6    9241    51000   2766378  138595  16174 22667   14   109   36  13%   1024   45   16   15  111%
c -  415.8    9241    51000   2829625  139245  16183 22668   13    19   36  72%   1024  -31   11   15   73%
c 
c [simplification-16] limit 2832473 conflicts (hard 3156473) hit after 2844356 conflicts
c [quatres-14] found 21163 quaternary clauses 19% in total
c [quatres-14-1] removed 25 duplicate quaternary clauses
c [quatres-14-1] added 6 double-self-subsuming ternary resolvents
c [quatres-14-2] added 90 single-self-subsuming ternary resolvents
c [quatres-14-2] added 227 quaternary resolvents
c [ternres-14] limit 148418511 with penalty 0 = 0 + 0
c [ternres-14] all 9241 free variables schedulable
c [ternres-14] 2761 ternary resolvents (95 bin, 2666 trn)
c [ternres-14] fully completed ternary resolution
c [gauss-9] limit 14841851 penalty 1 = 1 + 0
c [gauss-9] extracted 4013 xors of average arity 3.1
c [gauss-9] connected 12367 occurrences of 811 variables (average 15.2)
c [gauss-9] limit 14841851 penalty 1 = 1 + 0
c [gauss-9] fully completed
c [gauss-9] exported 0 unary, 0 binary and 1 ternary equations
c [decomp-70] removed 1 variables
c [treelook-6] limit 14841851 penalty 0 = 0 + 0 boost 1
c [treelook-6] scheduled 17998 literals 97%
c [treelook-6] scheduling used 699172 steps
c [treelook-6] scheduled completely
c [treelook-6] limit 14841851 penalty 0 = 0 + 0 boost 1
c [treelook-6] used 10091968 steps
c [treelook-6] fully completed tree based probing
c [decomp-71] removed 2 variables
c [treelook-6] removed 4 variables, found 3688 hbrs
c [transred-14] limit 2000000 with penalty 0 = 0 + 0
c [transred-14] removed 1224 transitive binary clauses
c [cce-8] boosting limit by 10
c [cce-8] limit of 7420925590 steps penalty 0 = 0 + 0
c [cce-8-1] eliminated 2 clauses out of 87 (2%) of length 12
c [cce-8-1] eliminated 2 clauses out of 77 (3%) of length 11
c [cce-8-1] eliminated 3 clauses out of 237 (1%) of length 10
c [cce-8-1] eliminated 2 clauses out of 467 (0%) of length 9
c [cce-8-1] eliminated 5 clauses out of 747 (1%) of length 8
c [cce-8-1] eliminated 3 clauses out of 1330 (0%) of length 7
c [cce-8-1] eliminated 34 clauses out of 2504 (1%) of length 6
c [cce-8-1] eliminated 50 clauses out of 4959 (1%) of length 5
c [cce-8-1] eliminated 44 clauses out of 11202 (0%) of length 4
c [cce-8-1] completed large round (ATE)
c [cce-8-1] eliminated 145 large clauses in 25010440 steps
c [cce-8-1] allowing another 12505220 steps for small clauses
c [cce-8-1] scheduling 16740 clauses = 9721 binary + 7019 ternary
c [cce-8-1] tried to eliminate 16740 small clauses 100%
c [cce-8-1] eliminated 11 binary clauses 0%
c [cce-8-1] eliminated 21 ternary clauses 0%
c [cce-8-1] eliminated 32 small clauses 0%
c [cce-8-1] eliminated 32 small clauses in 24181890 steps
c [cce-8-1] completed small round (ATE)
c [cce-8-1] eliminated 177 covered clauses in round 1
c [cce-8-2] completed large round (ATE)
c [cce-8-2] allowing another 12389359 steps for small clauses
c [cce-8-2] scheduling 16708 clauses = 9710 binary + 6998 ternary
c [cce-8-2] tried to eliminate 16708 small clauses 100%
c [cce-8-2] completed small round (ATE)
c [cce-8-2] eliminated 0 covered clauses in round 2
c [cce-8] eliminated 177 covered clauses in TOTAL during 2 rounds
c [cce-8] 177 < 1/100 * 50947 = 509 considered unsuccessful
c [elim-10] scheduling all variables this time
c [elim-10] scheduled 9236 variables 100%
c [elim-10] limit of 400000000 steps penalty 1 = 1 + 0
c [elim-10] rescheduling of touched variables disabled
c [elim-10-1] eliminated 315 variables 3% in round 1 in 14432094 steps
c [elim-10-1] backward subsumption/strengthening limit 14432000
c [elim-10-1-1] backward checking 1498 touched variables 16%
c [elim-10-1-1] fully completed backward checking in 1 rounds
c [elim-10-1] subsumed 1 and strengthened 7 clauses in 742265 steps
c [elim-10-1] rescheduled 31 variables 0% by backward subsumption
c [elim-10-2] eliminated 1 variables 0% in round 2 in 249909 steps
c [elim-10-2] backward subsumption/strengthening limit 249900
c [elim-10-2-1] backward checking 9 touched variables 0%
c [elim-10-2-1] fully completed backward checking in 1 rounds
c [elim-10-2] subsumed 0 and strengthened 5 clauses in 36865 steps
c [elim-10-2] rescheduled 9 variables 0% by backward subsumption
c [elim-10-3] no variable eliminated in round 3 in 13998 steps
c [elim-10] fully completed in 3 rounds
c [elim-10] transition to [ all 0 rem 0 ] state
c [elim-10] eliminated 316 = 3% variables out of 9236 scheduled
c [bca-13] limit of 10000000 steps and 101079 added (scaled 2)
c [bca-13] 2557 out of 17842 literals actually usable 14%
c [bca-13] added 22 blocked clauses in 153063 steps
c [sweep-15] limit 44525553 penalty 0 = 0 + 0
c [sweep-15-1] 2797 pos 47.4% + 3110 neg 52.6% = 5907 sched 66.2% ret 3013
c [sweep-15-1] 16717791 steps 823 queries 48.45 avg class size
c [sweep-15-1] 19601 decisions 818 SAT calls 59.78 avg env size
c [sweep-15-1] fully completed sweeping round
c [decomp-72] removed 37 variables
c [sweep-15-1] removed 37 vars (0 failed, 37 eqs, 33 impls)
c [sweep-15-2] 3957 pos 44.5% + 4926 neg 55.5% = 8883 sched 100.0% ret 0
c [sweep-15-2] 20934966 steps 933 queries 76.43 avg class size
c [sweep-15-2] 22588 decisions 948 SAT calls 60.41 avg env size
c [sweep-15-2] fully completed sweeping round
c [decomp-73] removed 44 variables
c [sweep-15-2] removed 44 vars (0 failed, 46 eqs, 29 impls)
c [sweep-15-3] 3941 pos 44.6% + 4898 neg 55.4% = 8839 sched 100.0% ret 0
c [sweep-15-3] 6877383 steps 273 queries 208.55 avg class size
c [sweep-15-3] 8171 decisions 271 SAT calls 70.00 avg env size
c [sweep-15-3] 3456 variables remain 39% (5382 retained 61%)
c [decomp-74] removed 9 variables
c [sweep-15-3] removed 9 vars (0 failed, 8 eqs, 6 impls)
c [sweep-15] removed 90 vars in TOTAL (3 rounds, 2026 queries)
c [sort-queue-16] sorted 1711 enqueued variables after 2844356 conflicts
c [score-dist-16] active 7119 (81%), one 1710 (19%), zero 1 (0%)
c [score-dist-16] max exp 512, different 158 (31%)
c [score-dist-16] median active exp 504, avg 469.1
c [simplification-16] removed 411 variables 4.4% (8830 remain 18%)
c [simplification-16] removed 904 irredundant clauses 1.8% (50096 remain 35%)
c [simplification-16] maximum reduction of 4% = max (4%, 2%)
c [simplification-16] geometric conflict interval increment 129600 = 648000 / 5
c [simplification-16] new conflict interval 777600
c [simplification-16] penalized conflict interval 777600 = 1 * 777600
c [simplification-16] hard conflict limit 4010756 (soft 3621956 + delta 388800)
c [simplification-16] new conflict limit 3621956 (hard 4010756)
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 -  427.2    8830    50084   2896262  140248  18159 21437   11   106   25  10%   1024   32   11   13   88%
c -  435.6    8830    50084   2966378  140916  18166 21437    9    10   36  90%   1024  -46    8   11   71%
c -  444.5    8830    50084   3034451  142275  18188 21438   11    19   36  58%   1024  -33   10   12   82%
c -  454.3    8830    50084   3102306  142345  18194 21438   14    85   36  16%   1024   34   10   14   69%
c -  464.5    8830    50084   3174593  146672  18212 21439   12    80   37  15%   1024   28   14   12  118%
c -  473.5    8830    50084   3239641  146674  18226 21439   17   108   37  16%   1024   34   15   14  107%
c -  483.0    8830    50084   3305820  147718  18231 21439   20    71   37  29%   1024    9   16   15  102%
c -  490.1    8830    50084   3376759  149984  18251 21440   12    48   37  24%   1024  -14   11   13   88%
c -  499.7    8830    50084   3447111  150692  18265 21442   20    79   37  25%   1024   10   28   13  213%
c -  508.7    8830    50084   3514322  151184  18269 21442   13    72   37  18%   1024    5   14   15   91%
c -  518.9    8830    50084   3582734  153037  18280 21442   15    94   37  16%   1024   24   15   16   94%
c i  527.0    8829    50084   3651720  203161  18303 21447    8    16   72  51%   1024  -32    7   12   56%
c -  529.8    8795    50084   3666664  153729  18303 21447   19    66   58  29% -24666   17   25   13  192%
c -  540.8    8795    50084   3735442  153649  18304 21448   14    36   58  39%  -7971  -16   16   16  101%
c -  552.5    8795    50084   3807866  154960  18307 21448   21    68   58  30%  -1955   26   18   16  116%
c -  563.3    8795    50084   3881664  157681  18309 21450    9    35   58  26%     58  -29    8   14   56%
c 
c [simplification-17] limit 3621956 conflicts (hard 4010756) hit after 3894715 conflicts
c [quatres-15] found 19290 quaternary clauses 18% in total
c [quatres-15-1] removed 107 duplicate quaternary clauses
c [quatres-15-1] added 1 double-self-subsuming ternary resolvents
c [quatres-15-2] added 82 single-self-subsuming ternary resolvents
c [quatres-15-2] added 301 quaternary resolvents
c [ternres-15] limit 200000000 with penalty 0 = 0 + 0
c [ternres-15] all 8795 free variables schedulable
c [ternres-15] 2576 ternary resolvents (81 bin, 2495 trn)
c [ternres-15] fully completed ternary resolution
c [gauss-10] limit 43931594 penalty 0 = 0 + 0
c [gauss-10] extracted 4665 xors of average arity 2.9
c [gauss-10] connected 13575 occurrences of 1053 variables (average 12.9)
c [gauss-10] limit 43931594 penalty 0 = 0 + 0
c [gauss-10] fully completed
c [gauss-10] exported 0 unary, 0 binary and 3 ternary equations
c [decomp-75] removed 159 variables
c [basicprobe-6] limit 400000000 penalty 0 = 0 + 0
c [basicprobe-6-0] 4975 sched 58%, 8 failed, 3 lifted, 3887 hbrs
c [decomp-76] removed 37 variables
c [basicprobe-6-1] 4849 sched 56%, 0 failed, 0 lifted, 230 hbrs
c [basicprobe-6-2] 4847 sched 56%, 0 failed, 0 lifted, 14 hbrs
c [basicprobe-6-3] 4847 sched 56%, 0 failed, 0 lifted, 2 hbrs
c [basicprobe-6-4] 4846 sched 56%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-6-4] fully completed probing
c [basicprobe-6-4] 11 units = 8 failed (73%) + 3 lifted (27%)
c [basicprobe-6-4] removed 37 variables, found 4133 hbrs
c [bate-5] eliminated 96 asymmetric tautologies during probing
c [transred-15] limit 2000000 with penalty 0 = 0 + 0
c [transred-15] removed 1374 transitive binary clauses
c [block-6] scheduling all variables this time
c [block-6] scheduled 8599 variables 100%
c [block-6] limit of 50000000 steps penalty 4 = 4 + 0
c [block-6] fully completed
c [block-6] transition to [ all 0 rem 0 ] state
c [block-6] eliminated 191 blocked clauses
c [block-6] 191 < 1/100 * 48857 = 488 considered unsuccessful
c [elim-11] scheduling all variables this time
c [elim-11] scheduled 8585 variables 100%
c [elim-11] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-11] rescheduling of touched variables disabled
c [elim-11-1] eliminated 180 variables 2% in round 1 in 12476872 steps
c [elim-11-1] backward subsumption/strengthening limit 12476800
c [elim-11-1-1] backward checking 1199 touched variables 14%
c [elim-11-1-1] fully completed backward checking in 1 rounds
c [elim-11-1] subsumed 6 and strengthened 8 clauses in 591355 steps
c [elim-11-1] rescheduled 39 variables 0% by backward subsumption
c [elim-11-2] eliminated 4 variables 0% in round 2 in 435940 steps
c [elim-11-2] backward subsumption/strengthening limit 435900
c [elim-11-2-1] backward checking 21 touched variables 0%
c [elim-11-2-1] fully completed backward checking in 1 rounds
c [elim-11-2] subsumed 0 and strengthened 6 clauses in 48245 steps
c [elim-11-2] rescheduled 12 variables 0% by backward subsumption
c [elim-11-3] eliminated 2 variables 0% in round 3 in 9164 steps
c [elim-11-3] backward subsumption/strengthening limit 9100
c [elim-11-3-1] backward checking 7 touched variables 0%
c [elim-11-3-1] incomplete backward checking 0 remain 0%
c [elim-11-3] subsumed 0 and strengthened 2 clauses in 9101 steps
c [elim-11] incomplete 6 not tried 0% in round 3
c [elim-11] transition to [ all 1 rem 1 ] state
c [elim-11] eliminated 186 = 2% variables out of 8585 scheduled
c [bca-14] limit of 10000000 steps and 96536 added (scaled 2)
c [bca-14] 2521 out of 16800 literals actually usable 15%
c [bca-14] added 15 blocked clauses in 158576 steps
c [sweep-16] limit 65897392 penalty 0 = 0 + 0
c [sweep-16-1] 1604 pos 48.6% + 1698 neg 51.4% = 3302 sched 39.3% ret 5097
c [sweep-16-1] 15145084 steps 700 queries 48.29 avg class size
c [sweep-16-1] 13170 decisions 711 SAT calls 51.08 avg env size
c [sweep-16-1] fully completed sweeping round
c [decomp-80] removed 56 variables
c [sweep-16-1] removed 56 vars (0 failed, 56 eqs, 28 impls)
c [sweep-16-2] 3596 pos 43.1% + 4747 neg 56.9% = 8343 sched 100.0% ret 0
c [sweep-16-2] 23952598 steps 940 queries 60.38 avg class size
c [sweep-16-2] 19371 decisions 955 SAT calls 57.63 avg env size
c [sweep-16-2] fully completed sweeping round
c [decomp-81] removed 45 variables
c [sweep-16-2] removed 45 vars (0 failed, 49 eqs, 21 impls)
c [sweep-16-3] 3573 pos 43.1% + 4725 neg 56.9% = 8298 sched 100.0% ret 0
c [sweep-16-3] 21361736 steps 884 queries 71.89 avg class size
c [sweep-16-3] 18101 decisions 880 SAT calls 60.79 avg env size
c [sweep-16-3] fully completed sweeping round
c [decomp-82] removed 35 variables
c [sweep-16-3] removed 35 vars (0 failed, 39 eqs, 22 impls)
c [sweep-16] removed 136 vars in TOTAL (3 rounds, 2521 queries)
c [sort-queue-17] sorted 1914 enqueued variables after 3894715 conflicts
c [score-dist-17] active 6349 (77%), one 1914 (23%), zero 0 (0%)
c [score-dist-17] max exp 512, different 169 (33%)
c [score-dist-17] median active exp 503, avg 476.2
c [simplification-17] removed 532 variables 6.0% (8263 remain 17%)
c [simplification-17] removed 2270 irredundant clauses 4.5% (47814 remain 33%)
c [simplification-17] maximum reduction of 6% = max (6%, 5%)
c [simplification-17] large reduction 6% >= 5% limit
c [simplification-17] next conflict interval 38947 = min (3894715/100, 777600)
c [simplification-17] penalized conflict interval 38947 = 1 * 38947
c [simplification-17] hard conflict limit 3953135 (soft 3933662 + delta 19473)
c [simplification-17] new conflict limit 3933662 (hard 3953135)
c 
c [simplification-18] limit 3933662 conflicts (hard 3953135) hit after 3940820 conflicts
c [quatres-16] found 20305 quaternary clauses 18% in total
c [quatres-16-1] removed 46 duplicate quaternary clauses
c [quatres-16-1] added 3 double-self-subsuming ternary resolvents
c [quatres-16-2] added 113 single-self-subsuming ternary resolvents
c [quatres-16-2] added 287 quaternary resolvents
c [ternres-16] limit 200000000 with penalty 0 = 0 + 0
c [ternres-16] all 8263 free variables schedulable
c [ternres-16] 3003 ternary resolvents (79 bin, 2924 trn)
c [ternres-16] fully completed ternary resolution
c [gauss-11] limit 44588117 penalty 0 = 0 + 0
c [gauss-11] extracted 3861 xors of average arity 3.1
c [gauss-11] connected 11839 occurrences of 753 variables (average 15.7)
c [gauss-11] limit 44588117 penalty 0 = 0 + 0
c [gauss-11] fully completed
c [gauss-11] exported 0 unary, 0 binary and 0 ternary equations
c [simpleprobe-7] all 8263 free variables schedulable
c [simpleprobe-7] limit 200000000 penalty 0 = 0 + 0
c [decomp-84] removed 4 variables
c [simpleprobe-7] fully completed simple probing
c [simpleprobe-7] removed 4 variables, found 3966 hbrs, 0 units
c [transred-16] limit 2000000 with penalty 0 = 0 + 0
c [transred-16] removed 1539 transitive binary clauses
c [cce-9] limit of 557351473 steps penalty 1 = 1 + 0
c [cce-9-1] eliminated 1 clauses out of 2 (50%) of length 19
c [cce-9-1] eliminated 1 clauses out of 17 (6%) of length 17
c [cce-9-1] eliminated 6 clauses out of 108 (6%) of length 12
c [cce-9-1] eliminated 15 clauses out of 90 (17%) of length 11
c [cce-9-1] eliminated 23 clauses out of 239 (10%) of length 10
c [cce-9-1] eliminated 50 clauses out of 518 (10%) of length 9
c [cce-9-1] eliminated 68 clauses out of 728 (9%) of length 8
c [cce-9-1] eliminated 75 clauses out of 1340 (6%) of length 7
c [cce-9-1] eliminated 191 clauses out of 2428 (8%) of length 6
c [cce-9-1] eliminated 383 clauses out of 4595 (8%) of length 5
c [cce-9-1] eliminated 702 clauses out of 10548 (7%) of length 4
c [cce-9-1] completed large round (ACCE)
c [cce-9-1] eliminated 1515 large clauses in 89771450 steps
c [cce-9-1] allowing another 44885725 steps for small clauses
c [cce-9-1] scheduling 20280 clauses = 9133 binary + 11147 ternary
c [cce-9-1] tried to eliminate 20280 small clauses 100%
c [cce-9-1] eliminated 292 binary clauses 3%
c [cce-9-1] eliminated 655 ternary clauses 6%
c [cce-9-1] eliminated 947 small clauses 5%
c [cce-9-1] eliminated 947 small clauses in 81262608 steps
c [cce-9-1] completed small round (ACCE)
c [cce-9-1] eliminated 2462 covered clauses in round 1
c [cce-9-2] eliminated 1 clauses out of 73 (1%) of length 13
c [cce-9-2] eliminated 1 clauses out of 216 (0%) of length 10
c [cce-9-2] eliminated 3 clauses out of 660 (0%) of length 8
c [cce-9-2] eliminated 17 clauses out of 1265 (1%) of length 7
c [cce-9-2] eliminated 10 clauses out of 2237 (0%) of length 6
c [cce-9-2] eliminated 36 clauses out of 4212 (1%) of length 5
c [cce-9-2] eliminated 66 clauses out of 9846 (1%) of length 4
c [cce-9-2] completed large round (ACCE)
c [cce-9-2] eliminated 134 large clauses in 98006294 steps
c [cce-9-2] allowing another 49003147 steps for small clauses
c [cce-9-2] scheduling 19333 clauses = 8841 binary + 10492 ternary
c [cce-9-2] tried to eliminate 19333 small clauses 100%
c [cce-9-2] eliminated 61 binary clauses 1%
c [cce-9-2] eliminated 43 ternary clauses 0%
c [cce-9-2] eliminated 104 small clauses 1%
c [cce-9-2] eliminated 104 small clauses in 87204455 steps
c [cce-9-2] completed small round (ACCE)
c [cce-9-2] eliminated 238 covered clauses in round 2
c [cce-9-3] eliminated 1 clauses out of 2227 (0%) of length 6
c [cce-9-3] eliminated 10 clauses out of 4176 (0%) of length 5
c [cce-9-3] eliminated 13 clauses out of 9780 (0%) of length 4
c [cce-9-3] completed large round (ACCE)
c [cce-9-3] eliminated 24 large clauses in 98549392 steps
c [cce-9-3] allowing another 49274696 steps for small clauses
c [cce-9-3] scheduling 19229 clauses = 8780 binary + 10449 ternary
c [cce-9-3] tried to eliminate 19229 small clauses 100%
c [cce-9-3] eliminated 15 binary clauses 0%
c [cce-9-3] eliminated 12 ternary clauses 0%
c [cce-9-3] eliminated 27 small clauses 0%
c [cce-9-3] eliminated 27 small clauses in 87453124 steps
c [cce-9-3] completed small round (ACCE)
c [cce-9-3] eliminated 51 covered clauses in round 3
c [cce-9] eliminated 2751 covered clauses in TOTAL during 3 rounds
c [elim-12] no untried remaining variables left
c [elim-12] scheduled 8259 variables 100%
c [elim-12] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-12] rescheduling of touched variables disabled
c [elim-12-1] eliminated 423 variables 5% in round 1 in 10858967 steps
c [elim-12-1] backward subsumption/strengthening limit 10858900
c [elim-12-1-1] backward checking 1403 touched variables 17%
c [elim-12-1-1] fully completed backward checking in 1 rounds
c [elim-12-1] subsumed 5 and strengthened 10 clauses in 640186 steps
c [elim-12-1] rescheduled 50 variables 1% by backward subsumption
c [elim-12-2] eliminated 1 variables 0% in round 2 in 280723 steps
c [elim-12-2] backward subsumption/strengthening limit 280700
c [elim-12-2-1] backward checking 20 touched variables 0%
c [elim-12-2-1] fully completed backward checking in 1 rounds
c [elim-12-2] subsumed 1 and strengthened 1 clauses in 31420 steps
c [elim-12-2] rescheduled 7 variables 0% by backward subsumption
c [elim-12-3] no variable eliminated in round 3 in 2886 steps
c [elim-12] fully completed in 3 rounds
c [elim-12] transition to [ all 0 rem 0 ] state
c [elim-12] eliminated 424 = 5% variables out of 8259 scheduled
c [bca-15] limit of 10000000 steps and 89091 added (scaled 2)
c [bca-15] 2212 out of 15672 literals actually usable 14%
c [bca-15] added 17 blocked clauses in 194714 steps
c [sweep-17] limit 66882176 penalty 0 = 0 + 0
c [sweep-17-1] 3344 pos 42.7% + 4491 neg 57.3% = 7835 sched 100.0% ret 0
c [sweep-17-1] 30548525 steps 824 queries 48.65 avg class size
c [sweep-17-1] 20993 decisions 824 SAT calls 71.02 avg env size
c [sweep-17-1] fully completed sweeping round
c [decomp-85] removed 15 variables
c [sweep-17-1] removed 15 vars (0 failed, 14 eqs, 11 impls)
c [sweep-17-2] 3340 pos 42.7% + 4480 neg 57.3% = 7820 sched 100.0% ret 0
c [sweep-17-2] 32916303 steps 837 queries 41.85 avg class size
c [sweep-17-2] 21966 decisions 845 SAT calls 73.11 avg env size
c [sweep-17-2] fully completed sweeping round
c [decomp-86] removed 22 variables
c [sweep-17-2] removed 22 vars (0 failed, 22 eqs, 14 impls)
c [sweep-17-3] 3329 pos 42.7% + 4469 neg 57.3% = 7798 sched 100.0% ret 0
c [sweep-17-3] 4200973 steps 33 queries 1060.76 avg class size
c [sweep-17-3] 1543 decisions 31 SAT calls 125.19 avg env size
c [sweep-17-3] 7057 variables remain 90% (741 retained 10%)
c [decomp-87] removed 1 variables
c [sweep-17-3] removed 1 vars (0 failed, 1 eqs, 1 impls)
c [sweep-17] removed 38 vars in TOTAL (3 rounds, 1691 queries)
c [sort-queue-18] sorted 1402 enqueued variables after 3940820 conflicts
c [score-dist-18] active 6395 (82%), one 1402 (18%), zero 0 (0%)
c [score-dist-18] max exp 512, different 152 (30%)
c [score-dist-18] median active exp 503, avg 465.2
c [simplification-18] removed 466 variables 5.6% (7797 remain 16%)
c [simplification-18] removed 3673 irredundant clauses 7.7% (44141 remain 31%)
c [simplification-18] maximum reduction of 8% = max (6%, 8%)
c [simplification-18] large reduction 8% >= 5% limit
c [simplification-18] next conflict interval 39408 = min (3940820/100, 777600)
c [simplification-18] penalized conflict interval 39408 = 1 * 39408
c [simplification-18] hard conflict limit 3999932 (soft 3980228 + delta 19704)
c [simplification-18] new conflict limit 3980228 (hard 3999932)
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 -  609.2    7797    44141   3958665  143588  18671 22358   17    55   27  31%    726   -4   15   17   89%
c 
c [simplification-19] limit 3980228 conflicts (hard 3999932) hit after 3980228 conflicts
c [quatres-17] found 19162 quaternary clauses 18% in total
c [quatres-17-1] removed 47 duplicate quaternary clauses
c [quatres-17-1] added 5 double-self-subsuming ternary resolvents
c [quatres-17-2] added 72 single-self-subsuming ternary resolvents
c [quatres-17-2] added 236 quaternary resolvents
c [ternres-17] limit 200000000 with penalty 0 = 0 + 0
c [ternres-17] all 7797 free variables schedulable
c [ternres-17] 922 ternary resolvents (82 bin, 840 trn)
c [ternres-17] fully completed ternary resolution
c [treelook-7] limit 22583290 penalty 0 = 0 + 0 boost 1
c [treelook-7] scheduled 15594 literals 100%
c [treelook-7] scheduling used 711585 steps
c [treelook-7] scheduled completely
c [treelook-7] limit 22583290 penalty 0 = 0 + 0 boost 1
c [treelook-7] used 11470924 steps
c [treelook-7] fully completed tree based probing
c [decomp-89] removed 3 variables
c [treelook-7] removed 3 variables, found 4536 hbrs
c [unhide-7] limit 1250000 with penalty 4 = 4 + 0
c [unhide-7-9] 0 units, 0 failed, 858 tauts, 0 hbrs, 50213 literals
c [transred-17] limit 2000000 with penalty 0 = 0 + 0
c [transred-17] removed 1293 transitive binary clauses
c [cce-10] limit of 1129164517 steps penalty 0 = 0 + 0
c [cce-10-1] eliminated 1 clauses out of 109 (1%) of length 12
c [cce-10-1] eliminated 4 clauses out of 90 (4%) of length 11
c [cce-10-1] eliminated 4 clauses out of 230 (2%) of length 10
c [cce-10-1] eliminated 14 clauses out of 494 (3%) of length 9
c [cce-10-1] eliminated 11 clauses out of 695 (2%) of length 8
c [cce-10-1] eliminated 41 clauses out of 1298 (3%) of length 7
c [cce-10-1] eliminated 85 clauses out of 2369 (4%) of length 6
c [cce-10-1] eliminated 121 clauses out of 4282 (3%) of length 5
c [cce-10-1] eliminated 99 clauses out of 9753 (1%) of length 4
c [cce-10-1] completed large round (ATE)
c [cce-10-1] eliminated 380 large clauses in 27375764 steps
c [cce-10-1] allowing another 13687882 steps for small clauses
c [cce-10-1] scheduling 14629 clauses = 8363 binary + 6266 ternary
c [cce-10-1] tried to eliminate 14629 small clauses 100%
c [cce-10-1] eliminated 11 binary clauses 0%
c [cce-10-1] eliminated 120 ternary clauses 2%
c [cce-10-1] eliminated 131 small clauses 1%
c [cce-10-1] eliminated 131 small clauses in 25767000 steps
c [cce-10-1] completed small round (ATE)
c [cce-10-1] eliminated 511 covered clauses in round 1
c [cce-10-2] completed large round (ATE)
c [cce-10-2] allowing another 12968919 steps for small clauses
c [cce-10-2] scheduling 14498 clauses = 8352 binary + 6146 ternary
c [cce-10-2] tried to eliminate 14498 small clauses 100%
c [cce-10-2] completed small round (ATE)
c [cce-10-2] eliminated 0 covered clauses in round 2
c [cce-10] eliminated 511 covered clauses in TOTAL during 2 rounds
c [elim-13] scheduling all variables this time
c [elim-13] scheduled 7794 variables 100%
c [elim-13] almost no limit of 100000000000 steps
c [elim-13] rescheduling of touched variables disabled
c [elim-13-1] eliminated 52 variables 1% in round 1 in 10435450 steps
c [elim-13-1] backward subsumption/strengthening limit 10435400
c [elim-13-1-1] backward checking 403 touched variables 5%
c [elim-13-1-1] fully completed backward checking in 1 rounds
c [elim-13-1] subsumed 0 and strengthened 1 clauses in 318675 steps
c [elim-13-1] rescheduled 7 variables 0% by backward subsumption
c [elim-13-2] no variable eliminated in round 2 in 128688 steps
c [elim-13] fully completed in 2 rounds
c [elim-13] transition to [ all 0 rem 0 ] state
c [elim-13] eliminated 52 = 1% variables out of 7794 scheduled
c [elim-13] 52 < 1/100 * 7794 = 77 considered unsuccessful
c [bca-16] limit of 10000000 steps and 87642 added (scaled 2)
c [bca-16] 2201 out of 15486 literals actually usable 14%
c [bca-16] added 17 blocked clauses in 166717 steps
c [sweep-18] almost no limit of 4000000000 steps
c [sweep-18-1] 3059 pos 43.7% + 3946 neg 56.3% = 7005 sched 90.5% ret 737
c [sweep-18-1] 26983969 steps 833 queries 62.34 avg class size
c [sweep-18-1] 20237 decisions 850 SAT calls 66.09 avg env size
c [sweep-18-1] fully completed sweeping round
c [decomp-90] removed 36 variables
c [sweep-18-1] removed 36 vars (0 failed, 37 eqs, 16 impls)
c [sweep-18-2] 3321 pos 43.1% + 4385 neg 56.9% = 7706 sched 100.0% ret 0
c [sweep-18-2] 27823129 steps 844 queries 51.02 avg class size
c [sweep-18-2] 20315 decisions 848 SAT calls 71.29 avg env size
c [sweep-18-2] fully completed sweeping round
c [decomp-91] removed 42 variables
c [sweep-18-2] removed 42 vars (0 failed, 43 eqs, 28 impls)
c [sweep-18-3] 3305 pos 43.1% + 4359 neg 56.9% = 7664 sched 100.0% ret 0
c [sweep-18-3] 24785740 steps 809 queries 65.97 avg class size
c [sweep-18-3] 18228 decisions 814 SAT calls 68.05 avg env size
c [sweep-18-3] fully completed sweeping round
c [decomp-92] removed 23 variables
c [sweep-18-3] removed 23 vars (0 failed, 27 eqs, 13 impls)
c [sweep-18] removed 101 vars in TOTAL (3 rounds, 2483 queries)
c [sort-queue-19] sorted 1082 enqueued variables after 3980228 conflicts
c [score-dist-19] active 6559 (86%), one 1082 (14%), zero 0 (0%)
c [score-dist-19] max exp 512, different 158 (31%)
c [score-dist-19] median active exp 503, avg 456.9
c [simplification-19] removed 156 variables 2.0% (7641 remain 15%)
c [simplification-19] removed 807 irredundant clauses 1.8% (43334 remain 30%)
c [simplification-19] maximum reduction of 2% = max (2%, 2%)
c [simplification-19] geometric conflict interval increment 259200 = 777600 / 3
c [simplification-19] conflict interval soft limit 1000000 reached
c [simplification-19] new conflict interval 1000000
c [simplification-19] penalized conflict interval 1000000 = 1 * 1000000
c [simplification-19] hard conflict limit 5480228 (soft 4980228 + delta 500000)
c [simplification-19] new conflict limit 4980228 (hard 5480228)
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 -  627.3    7641    43334   4030580  147639  17810 23264   10   110   37   9%    924   54   10   14   66%
c -  638.1    7641    43334   4102293  148061  17813 23266   22    52   37  42%    991  -13   15   17   87%
c -  649.0    7641    43334   4173185  148304  17813 23266   13    51   37  24%   1013   -9   11   16   71%
c -  659.9    7641    43334   4245111  147531  17817 23266   15    28   37  53%   1020  -33   14   18   82%
c -  671.7    7641    43334   4320573  148119  17818 23266   16    42   38  38%   1023   -8   16   18   88%
c -  682.4    7641    43334   4396195  150386  17819 23266   14    61   38  23%   1024   13   13   17   79%
c -  694.6    7641    43334   4474457  150631  17820 23266   14    37   38  37%   1024   -8   13   15   89%
c -  705.2    7641    43334   4551746  151135  17843 23266   17    59   38  28%   1024   -8   21   15  137%
c -  717.7    7641    43334   4628737  154214  17844 23269   18    48   38  39%   1024  -15   20   16  130%
c -  729.1    7641    43334   4707950  156835  17854 23269   13    51   38  25%   1024  -14   14   13  103%
c -  740.3    7641    43334   4781757  154108  17858 23269   17    49   38  36%   1024  -10   20   18  111%
c -  753.7    7641    43334   4862678  157671  17864 23269   16    66   38  24%   1024    9   14   20   70%
c -  766.0    7641    43334   4942272  159076  17866 23269   22    60   38  36%   1024    6   22   17  133%
c 
c [simplification-20] limit 4980228 conflicts (hard 5480228) hit after 4981047 conflicts
c [quatres-18] found 19407 quaternary clauses 17% in total
c [quatres-18-1] removed 37 duplicate quaternary clauses
c [quatres-18-1] added 5 double-self-subsuming ternary resolvents
c [quatres-18-2] added 113 single-self-subsuming ternary resolvents
c [quatres-18-2] added 276 quaternary resolvents
c [ternres-18] limit 200000000 with penalty 0 = 0 + 0
c [ternres-18] all 7641 free variables schedulable
c [ternres-18] 5200 ternary resolvents (105 bin, 5095 trn)
c [ternres-18] fully completed ternary resolution
c [gauss-12] limit 25000000 penalty 1 = 1 + 0
c [gauss-12] extracted 3657 xors of average arity 3.1
c [gauss-12] connected 11235 occurrences of 702 variables (average 16.0)
c [gauss-12] limit 25000000 penalty 1 = 1 + 0
c [gauss-12] fully completed
c [gauss-12] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-93] removed 3 variables
c [basicprobe-7] limit 400000000 penalty 0 = 0 + 0
c [basicprobe-7-0] 4322 sched 57%, 5 failed, 1 lifted, 284 hbrs
c [decomp-94] removed 5 variables
c [basicprobe-7-1] 4310 sched 56%, 0 failed, 0 lifted, 63 hbrs
c [basicprobe-7-2] 4304 sched 56%, 0 failed, 0 lifted, 22 hbrs
c [basicprobe-7-3] 4304 sched 56%, 0 failed, 0 lifted, 5 hbrs
c [basicprobe-7-4] 4303 sched 56%, 0 failed, 0 lifted, 1 hbrs
c [basicprobe-7-5] 4303 sched 56%, 0 failed, 0 lifted, 1 hbrs
c [basicprobe-7-6] 4303 sched 56%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-7-6] fully completed probing
c [basicprobe-7-6] 6 units = 5 failed (83%) + 1 lifted (17%)
c [basicprobe-7-6] removed 5 variables, found 376 hbrs
c [bate-6] eliminated 6 asymmetric tautologies during probing
c [transred-18] limit 2000000 with penalty 0 = 0 + 0
c [transred-18] removed 955 transitive binary clauses
c [cce-11] limit of 1541169823 steps penalty 0 = 0 + 0
c [cce-11-1] eliminated 5 clauses out of 100 (5%) of length 12
c [cce-11-1] eliminated 9 clauses out of 237 (4%) of length 10
c [cce-11-1] eliminated 5 clauses out of 487 (1%) of length 9
c [cce-11-1] eliminated 25 clauses out of 688 (4%) of length 8
c [cce-11-1] eliminated 78 clauses out of 1273 (6%) of length 7
c [cce-11-1] eliminated 121 clauses out of 2270 (5%) of length 6
c [cce-11-1] eliminated 183 clauses out of 4138 (4%) of length 5
c [cce-11-1] eliminated 363 clauses out of 9562 (4%) of length 4
c [cce-11-1] completed large round (ACCE)
c [cce-11-1] eliminated 789 large clauses in 81498684 steps
c [cce-11-1] allowing another 40749342 steps for small clauses
c [cce-11-1] scheduling 14363 clauses = 8273 binary + 6090 ternary
c [cce-11-1] tried to eliminate 14363 small clauses 100%
c [cce-11-1] eliminated 95 binary clauses 1%
c [cce-11-1] eliminated 158 ternary clauses 3%
c [cce-11-1] eliminated 253 small clauses 2%
c [cce-11-1] eliminated 253 small clauses in 60101370 steps
c [cce-11-1] completed small round (ACCE)
c [cce-11-1] eliminated 1042 covered clauses in round 1
c [cce-11-2] eliminated 1 clauses out of 228 (0%) of length 10
c [cce-11-2] eliminated 1 clauses out of 482 (0%) of length 9
c [cce-11-2] eliminated 2 clauses out of 663 (0%) of length 8
c [cce-11-2] eliminated 5 clauses out of 1195 (0%) of length 7
c [cce-11-2] eliminated 2 clauses out of 2149 (0%) of length 6
c [cce-11-2] eliminated 9 clauses out of 3955 (0%) of length 5
c [cce-11-2] eliminated 30 clauses out of 9199 (0%) of length 4
c [cce-11-2] completed large round (ACCE)
c [cce-11-2] eliminated 50 large clauses in 78469056 steps
c [cce-11-2] allowing another 39234528 steps for small clauses
c [cce-11-2] scheduling 14111 clauses = 8178 binary + 5933 ternary
c [cce-11-2] tried to eliminate 14111 small clauses 100%
c [cce-11-2] eliminated 19 binary clauses 0%
c [cce-11-2] eliminated 12 ternary clauses 0%
c [cce-11-2] eliminated 31 small clauses 0%
c [cce-11-2] eliminated 31 small clauses in 58254511 steps
c [cce-11-2] completed small round (ACCE)
c [cce-11-2] eliminated 81 covered clauses in round 2
c [cce-11-3] eliminated 1 clauses out of 96 (1%) of length 11
c [cce-11-3] eliminated 4 clauses out of 1190 (0%) of length 7
c [cce-11-3] eliminated 1 clauses out of 3946 (0%) of length 5
c [cce-11-3] eliminated 5 clauses out of 9169 (0%) of length 4
c [cce-11-3] completed large round (ACCE)
c [cce-11-3] eliminated 11 large clauses in 77237380 steps
c [cce-11-3] allowing another 38618690 steps for small clauses
c [cce-11-3] scheduling 14080 clauses = 8159 binary + 5921 ternary
c [cce-11-3] tried to eliminate 14080 small clauses 100%
c [cce-11-3] eliminated 3 binary clauses 0%
c [cce-11-3] eliminated 4 ternary clauses 0%
c [cce-11-3] eliminated 7 small clauses 0%
c [cce-11-3] eliminated 7 small clauses in 57788022 steps
c [cce-11-3] completed small round (ACCE)
c [cce-11-3] eliminated 18 covered clauses in round 3
c [cce-11] eliminated 1141 covered clauses in TOTAL during 3 rounds
c [bca-17] limit of 10000000 steps and 84992 added (scaled 2)
c [bca-17] 2062 out of 15268 literals actually usable 14%
c [bca-17] added 12 blocked clauses in 200037 steps
c [sweep-19] limit 92470189 penalty 0 = 0 + 0
c [sweep-19-1] 3295 pos 43.2% + 4338 neg 56.8% = 7633 sched 100.0% ret 0
c [sweep-19-1] 27244902 steps 821 queries 38.46 avg class size
c [sweep-19-1] 18974 decisions 824 SAT calls 69.12 avg env size
c [sweep-19-1] fully completed sweeping round
c [decomp-100] removed 25 variables
c [sweep-19-1] removed 25 vars (0 failed, 29 eqs, 17 impls)
c [sweep-19-2] 3285 pos 43.2% + 4323 neg 56.8% = 7608 sched 100.0% ret 0
c [sweep-19-2] 25613342 steps 812 queries 69.27 avg class size
c [sweep-19-2] 18444 decisions 811 SAT calls 68.21 avg env size
c [sweep-19-2] fully completed sweeping round
c [decomp-101] removed 25 variables
c [sweep-19-2] removed 25 vars (0 failed, 30 eqs, 12 impls)
c [sweep-19-3] 3279 pos 43.2% + 4304 neg 56.8% = 7583 sched 100.0% ret 0
c [sweep-19-3] 25160983 steps 763 queries 45.76 avg class size
c [sweep-19-3] 17818 decisions 759 SAT calls 69.03 avg env size
c [sweep-19-3] fully completed sweeping round
c [decomp-102] removed 16 variables
c [sweep-19-3] removed 16 vars (0 failed, 19 eqs, 7 impls)
c [sweep-19] removed 66 vars in TOTAL (3 rounds, 2393 queries)
c [sort-queue-20] sorted 2633 enqueued variables after 4981047 conflicts
c [score-dist-20] active 4934 (65%), one 2633 (35%), zero 0 (0%)
c [score-dist-20] max exp 512, different 115 (22%)
c [score-dist-20] median active exp 504, avg 490.2
c [simplification-20] removed 74 variables 1.0% (7567 remain 15%)
c [simplification-20] removed 1353 irredundant clauses 3.1% (41981 remain 29%)
c [simplification-20] maximum reduction of 3% = max (1%, 3%)
c [simplification-20] geometric conflict interval increment 250000 = 1000000 / 4
c [simplification-20] conflict interval soft limit 1000000 reached
c [simplification-20] new conflict interval 1000000
c [simplification-20] penalized conflict interval 1000000 = 1 * 1000000
c [simplification-20] hard conflict limit 6481047 (soft 5981047 + delta 500000)
c [simplification-20] new conflict limit 5981047 (hard 6481047)
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 -  803.5    7567    41981   5018631  154416  22003 22541   13    18   28  71%   1024  -23   11   17   65%
c -  819.7    7567    41981   5107061  155213  22003 22541   23    50   41  46%   1024   25   24   15  157%
c -  832.8    7567    41977   5187716  156758  22011 22542   22    66   42  33%   1024   18   21   17  125%
c -  844.7    7567    41977   5268041  156076  22011 22543   26    39   42  68%   1024   -5   27   22  122%
c -  856.0    7567    41977   5351938  156376  22011 22543   24    43   42  56%   1024    9   30   20  147%
c -  868.1    7567    41977   5437231  156472  22012 22543   20    37   42  54%   1024    3   27   20  132%
c i  869.3    7566    41972   5446891  165355  22017 22543   17    71   51  24%   1024   36   14   20   68%
c -  882.0    7566    41972   5524482  161602  22026 22543   10    43   42  23%  -7697  -52   11   16   65%
c -  897.3    7566    41972   5613405  162361  22026 22543   21    37   42  57%  -1221  -18   14   17   83%
c -  911.0    7566    41972   5700829  164454  22026 22544   10    23   42  44%    433  -21   10   15   65%
c -  932.6    7566    41972   5793005  168739  22028 22544   22    52   43  42%    879   23   22   13  170%
c -  946.2    7566    41972   5879036  166332  22028 22544   15    19   43  78%    985  -13   14   16   86%
c -  960.8    7566    41972   5970220  166474  22029 22544   16    23   43  68%   1014   -7   15   17   87%
c 
c [simplification-21] limit 5981047 conflicts (hard 6481047) hit after 5984911 conflicts
c [quatres-19] found 19267 quaternary clauses 16% in total
c [quatres-19-1] removed 17 duplicate quaternary clauses
c [quatres-19-1] added 4 double-self-subsuming ternary resolvents
c [quatres-19-2] added 80 single-self-subsuming ternary resolvents
c [quatres-19-2] added 177 quaternary resolvents
c [ternres-19] limit 200000000 with penalty 0 = 0 + 0
c [ternres-19] all 7566 free variables schedulable
c [ternres-19] 4823 ternary resolvents (113 bin, 4710 trn)
c [ternres-19] fully completed ternary resolution
c [card-6] limit 12599565 penalty 4 = 4 + 0
c [card-6] found 735 at-most-one constraints of average size 3.2
c [card-6] found 127 at-most-two constraints of average size 4.1
c [card-6] using previous limit 12599565 for elimination
c [card-6] 862 out of 862 constraints (100%) meet size limits
c [card-6] no units found
c [card-6] no at-most-one constraints generated
c [decomp-103] removed 5 variables
c [simpleprobe-8] all 7562 free variables schedulable
c [simpleprobe-8] limit 200000000 penalty 0 = 0 + 0
c [decomp-104] removed 7 variables
c [simpleprobe-8] fully completed simple probing
c [simpleprobe-8] removed 7 variables, found 3016 hbrs, 2 units
c [transred-19] limit 2000000 with penalty 0 = 0 + 0
c [transred-19] removed 1384 transitive binary clauses
c [cce-12] limit of 2015930514 steps penalty 0 = 0 + 0
c [cce-12-1] eliminated 1 clauses out of 94 (1%) of length 11
c [cce-12-1] eliminated 2 clauses out of 462 (0%) of length 9
c [cce-12-1] eliminated 2 clauses out of 649 (0%) of length 8
c [cce-12-1] eliminated 14 clauses out of 1129 (1%) of length 7
c [cce-12-1] eliminated 19 clauses out of 2157 (1%) of length 6
c [cce-12-1] eliminated 46 clauses out of 3911 (1%) of length 5
c [cce-12-1] eliminated 60 clauses out of 9132 (1%) of length 4
c [cce-12-1] completed large round (ATE)
c [cce-12-1] eliminated 144 large clauses in 22235731 steps
c [cce-12-1] allowing another 11117865 steps for small clauses
c [cce-12-1] scheduling 17981 clauses = 8126 binary + 9855 ternary
c [cce-12-1] tried to eliminate 17981 small clauses 100%
c [cce-12-1] eliminated 27 binary clauses 0%
c [cce-12-1] eliminated 136 ternary clauses 1%
c [cce-12-1] eliminated 163 small clauses 1%
c [cce-12-1] eliminated 163 small clauses in 24399075 steps
c [cce-12-1] completed small round (ATE)
c [cce-12-1] eliminated 307 covered clauses in round 1
c [cce-12-2] completed large round (ATE)
c [cce-12-2] allowing another 10944908 steps for small clauses
c [cce-12-2] scheduling 17818 clauses = 8099 binary + 9719 ternary
c [cce-12-2] tried to eliminate 17818 small clauses 100%
c [cce-12-2] completed small round (ATE)
c [cce-12-2] eliminated 0 covered clauses in round 2
c [cce-12] eliminated 307 covered clauses in TOTAL during 2 rounds
c [cce-12] 307 < 1/100 * 41905 = 419 considered unsuccessful
c [elim-14] scheduling all variables this time
c [elim-14] scheduled 7555 variables 100%
c [elim-14] limit of 400000000 steps penalty 1 = 1 + 0
c [elim-14] rescheduling of touched variables disabled
c [elim-14-1] eliminated 233 variables 3% in round 1 in 9658720 steps
c [elim-14-1] backward subsumption/strengthening limit 9658700
c [elim-14-1-1] backward checking 853 touched variables 11%
c [elim-14-1-1] fully completed backward checking in 1 rounds
c [elim-14-1] subsumed 1 and strengthened 8 clauses in 396915 steps
c [elim-14-1] rescheduled 42 variables 1% by backward subsumption
c [elim-14-2] eliminated 4 variables 0% in round 2 in 280668 steps
c [elim-14-2] backward subsumption/strengthening limit 280600
c [elim-14-2-1] backward checking 33 touched variables 0%
c [elim-14-2-1] fully completed backward checking in 1 rounds
c [elim-14-2] subsumed 0 and strengthened 2 clauses in 30010 steps
c [elim-14-2] rescheduled 7 variables 0% by backward subsumption
c [elim-14-3] eliminated 3 variables 0% in round 3 in 1765 steps
c [elim-14-3] backward subsumption/strengthening limit 1700
c [elim-14-3-1] backward checking 24 touched variables 0%
c [elim-14-3-1] incomplete backward checking 22 remain 92%
c [elim-14-3] subsumed 0 and strengthened 0 clauses in 1722 steps
c [elim-14] fully completed in 3 rounds
c [elim-14] transition to [ all 0 rem 0 ] state
c [elim-14] eliminated 240 = 3% variables out of 7555 scheduled
c [bca-18] limit of 10000000 steps and 82642 added (scaled 2)
c [bca-18] 2021 out of 14632 literals actually usable 14%
c [bca-18] added 31 blocked clauses in 181449 steps
c [sweep-20] limit 120955830 penalty 0 = 0 + 0
c [sweep-20-1] 3124 pos 42.7% + 4191 neg 57.3% = 7315 sched 100.0% ret 0
c [sweep-20-1] 24697979 steps 788 queries 62.94 avg class size
c [sweep-20-1] 17319 decisions 786 SAT calls 62.79 avg env size
c [sweep-20-1] fully completed sweeping round
c [decomp-105] removed 10 variables
c [sweep-20-1] removed 10 vars (0 failed, 11 eqs, 5 impls)
c [sweep-20-2] 3122 pos 42.7% + 4183 neg 57.3% = 7305 sched 100.0% ret 0
c [sweep-20-2] 25064271 steps 749 queries 51.97 avg class size
c [sweep-20-2] 16582 decisions 751 SAT calls 66.59 avg env size
c [sweep-20-2] fully completed sweeping round
c [decomp-106] removed 4 variables
c [sweep-20-2] removed 4 vars (0 failed, 7 eqs, 7 impls)
c [sweep-20-3] 3120 pos 42.7% + 4181 neg 57.3% = 7301 sched 100.0% ret 0
c [sweep-20-3] 26057330 steps 756 queries 56.04 avg class size
c [sweep-20-3] 17201 decisions 756 SAT calls 67.44 avg env size
c [sweep-20-3] fully completed sweeping round
c [decomp-107] removed 6 variables
c [sweep-20-3] removed 6 vars (0 failed, 8 eqs, 4 impls)
c [sweep-20] removed 20 vars in TOTAL (3 rounds, 2290 queries)
c [sort-queue-21] sorted 2625 enqueued variables after 5984911 conflicts
c [score-dist-21] active 4670 (64%), one 2625 (36%), zero 0 (0%)
c [score-dist-21] max exp 512, different 124 (24%)
c [score-dist-21] median active exp 504, avg 487.2
c [simplification-21] removed 271 variables 3.6% (7295 remain 15%)
c [simplification-21] removed 1084 irredundant clauses 2.6% (40888 remain 28%)
c [simplification-21] maximum reduction of 4% = max (4%, 3%)
c [simplification-21] geometric conflict interval increment 200000 = 1000000 / 5
c [simplification-21] conflict interval soft limit 1000000 reached
c [simplification-21] new conflict interval 1000000
c [simplification-21] penalized conflict interval 1000000 = 1 * 1000000
c [simplification-21] hard conflict limit 7484911 (soft 6984911 + delta 500000)
c [simplification-21] new conflict limit 6984911 (hard 7484911)
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 -  983.0    7295    40888   6056792  167367  23756 22674   23    32   41  73%   1021   -8   21   17  125%
c -  997.2    7295    40888   6143151  169003  23759 22674   22    46   42  49%   1023  -10   25   17  143%
c
c CAUGHT SIGNAL 15 SIGTERM
c
c s UNKNOWN
c bate: 178 basic ate = 134 trn 75% + 44 lrg 25% in 6 updates
c bcas: 18 count, 684 added (165 skipped), 2141578 steps
c bkwd: tried 199659 clauses, 398650 lits, 2.00 lits/clause
c bkwd: checked 10496140 occs, 52.57 occs/clause, 26.33 occs/lit
c bkwd: subsumed 8 binary, 33 ternary, 150 large
c bkwd: strengthened 1 binary, 14 ternary (100% self), 989 large (0% self)
c blkd: 6 bces, 2705 removed, 2022918 resolutions, 5138052 steps
c blkd: 2516 blocking literals 3%, 65 pure
c bump: 6190922 bumped seen, 430589460 lits 69.6 on average
c card: 6 count, 0 units, 93 am1, 41116343 steps
c card: 57 rescheduled, 340 eliminated, 11164 resolved, 9397 subsumed
c card: 2440 at-most-one constraints found, average size 3.32
c card: 2440 at-most-one constraints used 100%, average size 3.32
c card: 183 at-most-two constraints found, average size 4.04
c card: 178 at-most-two constraints used 97%, average size 4.04
c cces: 12 cces, 13202 eliminated, 11507 ate 87%, 1695 abce 13%
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: 481202 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 149 gcs, 0 rescored clauses, 23987 rescored vars
c dcps: 107 decompositions, 2896 equivalent 6%
c deco: 35 decision-only clauses 0%, 68% reduction
c decs: 25564716 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 14 elims, 38904 eliminated 79%, 158 pure 0%
c elms: 43 rounds, 3.1 rounds/bve
c elms: 36878 small 95%, 1803 large 5%
c elms: 64156 tried small, 36878 succeeded 57%, 27278 failed 43%
c elms: 3916 subsumed, 4278 strengthened, 529 blocked
c elms: 4123677 copies, 5584671 resolutions, 1926271 ipos
c elms: 1322447 subchks, 1197374 strchks
c gaus: 12 extractions, 50316 extracted, 3.1 size, 4 max
c gaus: exported 3 units, 0 binary and 11 ternary equations
c gaus: 0 gc, 66859000 steps, 33429500 extr 50%, 2704311 elim 4%
c glue: 14.0 orig avg, 14.0 real avg, 3.3 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 81251 = 19272 simple 24% + 45458 trn 56% + 16521 lrg 20%, 1442 sub 2%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 6190922 clauses, 28.4 length
c lrnd: 175534755 lits = 270916696 orig - 95381941 removed 35%
c lrnd: 1386929 uips 22%, 3699129 flips 60%
c mins: 6163371 mins 100%, 832 bin 0%, 26684 size 0%
c mins: 204294972 poisoned searches, 25220662 hits, 12% hit rate
c mins: 443625574 used twice searches, 40154175 hits, 9% hit rate
c move: moved 6213, 1917 bin 31%, 4296 trn 69%
c otfs: 23718 driving 33%, 48356 restarting 67%
c otfs: str 72074, 71487 red 99%, 587 irr 1%
c otfs: str 72074, 0 bin 0%, 1087 trn 2%, 70987 lrg 98%
c otfs: sub 3970, 3843 red 97%, 127 irr 3%
c otfs: sub 3970, 0 bin 0%, 138 trn 3%, 3832 lrg 97%
c phas: 1 computed, 12810 set, 3184 pos (25%), 9626 neg (75%)
c prbs: 7 basic, 386691 probed, 62 failed, 4 lifted
c prbs: 8 simple, 216477 probed, 37 failed, 1807 eqs
c prbs: 7 treelook, 37070 probed, 21 failed, 0 lifted
c prom: 1372322 locked 11% out of 12269618 tried
c prps: 1072144857 props, 41 props/dec
c prps: 97% srch, 3% simp, 0% lkhd
c quat: 19 count, 7459 quat, 2270 self1, 90 self2, 1184 dup
c queu: 21 sorted, 25564716 next (2002803 steps 0.08)
c queu: 583170817 enq (734433253 steps 1.26), 430589460 deq 74%
c redc: 78837 clauses 10%, 759511 tried 12%, 6 sat 0%
c redc: 106611 lits 1%, 11818473 tried 4%, 6 sat 0%
c redc: 1297 times jump level reduced, 9.3 levels on average
c reds: 98 count, 62863.6 conflicts per reduce
c reds: 0 memlim 0%, 98 arith 100%
c reds: 4826834 collected 91%, 479193 retired 9%
c rmbd: 2783 removed, 2578 red 93%
c rsts: 69302 restarts 100%, 0 skipped 0%
c rsts: 0 saturating 0%, 0 reuse 0%
c rsts: 0 kept 0.0% average 0.0%
c scnc: 0 count, 1.000 min (0/1000), 1.000 max (0/1000)
c simp: 21 count, 21 confs 100%, 0 vars 0%
c simp: 0 its 0%, 0 bin 0%, 0 trns 0%
c subl: 6190922 count (3478014 tried 0.6), 611174 sub out of 6182295 (9.9%)
c swps: 20 count, 39 rounds, 23379 queries (599.5/round)
c swps: 23246 sat calls, 1317 unsat (2.3% success rate)
c swps: 530993 decisions 22.8, 54007 conflicts 2.3
c swps; 102.2 avg class size, 59.4 avg environment size
c swps: 0 failed, 1061 impls, 1436 equivs
c swp0: 7779 type 0 queries, 1532 unsat (19.7%), 7470 sat (96.0%)
c swp1: 15600 type 1 queries, 4824 unsat (30.9%), 14473 sat (92.8%)
c sync: 0 produced units, 0 successful consumptions 0%
c sync: 0 consume units calls, 0 tried 0%, 0 success 0%
c sync: 0 produced clauses, 0 successful consumptions 0%
c sync: 0 consume clause calls, 0 tried 0%, 0 success 0%
c time: 63559807 calls to obtain time
c tops: 232 fixed 0%, 22 its, 280028.77 confs/it
c trds: 19 transitive reductions, 18672 removed, 9 failed
c trds: 346666 nodes, 371394 edges, 26492789 steps
c trim: 3174493 words, 12.1 MB
c trnr: 19 count, 2082 bin, 45858 trn, 493036101 steps
c unhd: 7 count, 9 rounds, 15689354 steps
c unhd: 6 non-trivial sccs of average size 2.0
c unhd: 1 units, 1 bin, 0 trn, 0 lrg
c unhd: 0 failed, 0 stamp, 0 lits, 0 bin, 0 trn, 0 lrg
c unhd: 16922 tauts, 382 bin 2%, 4636 trn 27%, 2592 lrg 15%
c unhd: 16922 tauts, 9312 stamp 55%, 16782 red 99%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 229887 str, 1 bin 0%, 513 trn 0%, 229373 lrg 100%, 227590 red 99%
c vars: 7338 remaining 15% and 42032 removed 85% out of 49370
c vars: 232 fixed 0%, 38904 eliminated 79%, 2896 equivalent 6%
c vsts: 42748418518 visits, 98% srch, 2% simp, 0% lkhd
c vsts: 40.5 search visits per propagation, 6817.9 per conflict
c wchs: 9268558376 pushed, 19243543 enlarged, 284 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all        6189754       4826834        479193     214223142      65323146       3266296
c 
c  0 0        245083   4     83220   2         0   0 128595119  60  28528039  44   1120660  34     4.4
c  1 5        242838   4    169328   4     48331  10  25814076  12<  7805762  12<   343817  11     0.8
c  2 6       1204666  19    947562  20    135223  28  36394135  17  14651469  22    804206  25<    3.7
c  3 9       2029596  33<  1626872  34<   137383  29< 15917486   7   9050382  14    626019  19     6.6
c  4 14      1440000  23   1167533  24     81195  17   5040396   2   3490646   5    253319   8     4.7
c  5 21       668617  11    545082  11     44076   9   1738124   1   1270556   2     85554   3     5.3
c  6 30       235670   4    189112   4     19841   4    509965   0    372295   1     23661   1     4.1
c  7 41        88346   1     70951   1      8296   2    155787   0    115070   0      6614   0     1.7
c  8 54        27245   0     21270   0      3490   1     45028   0     30994   0      1916   0     0.7
c  9 69         6839   0      5255   0      1201   0     11633   0      7147   0       486   0     0.2
c 10 86          854   0       649   0       157   0      1393   0       786   0        44   0     0.1
c 
c avg                  3.3           3.4           3.1           0.8           1.3           1.7
c std                  1.4           1.3           1.5           1.2           1.5           1.5
c 
c   72.442   7% cce
c   47.764   5% bump
c   27.639   3% sweep
c   19.727   2% rescore
c   17.018   2% decide
c   13.652   1% probe
c    6.137   1% ternres
c 
c   15.705 < 1% rest (below)
c 
c    5.888   1% elim
c    2.012   0% gauss
c    1.956   0% quatres
c    1.951   0% unhide
c    1.776   0% transred
c    1.095   0% bca
c    0.575   0% block
c    0.451   0% card
c    0.000   0% locs
c    0.000   0% queuesort
c ==================================
c    1.423   0% preprocessing     1%
c  136.881  14% inprocessing     99%
c ==================================
c  138.305  14% simplifying
c  861.711  86% search
c ==================================
c 1000.017 100% all
c 
c       6160633 conflicts,        6160.5 confs/sec
c          3216 ternaries,        1915.6 confs/ternary
c           377 binaries,        16341.2 confs/binary
c            22 iterations,     280028.8 confs/iteration
c 
c            98 reductions,          0.1 redus/sec,  62863.6 confs/reduction
c         69302 restarts,           69.3 rests/sec,     88.9 confs/restart
c      25564716 decisions,       25564.3 decis/sec,      4.1 decis/conflict
c    1072144857 propagations,  1072127.0 props/sec,     41.9 props/decision
c 
c 1000.0 seconds, 89.5 MB
c
c CAUGHT SIGNAL 15 SIGTERM
c
c launch: done
