c launch: /data/cnf/sc2014/app/6s17-opt.cnf.bz2
c host: atom10
c Lingeling SAT Solver
c 
c Version b7ztzud 55d9a3e9649fc56eacf3e72d8e2e2d5c615d5f18
c 
c Copyright (C) 2010-2014 Armin Biere JKU Linz Austria.
c All rights reserved.
c 
c released Fri May  1 11:44:04 CEST 2015
c compiled Fri May  1 11:44:04 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-49-generic x86_64
c 
c piping '/data/cnf/sc2014/app/6s17-opt.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/6s17-opt.cnf.bz2
c no embedded options
c found 'p cnf 47657 139163' header
c read 47657 variables, 139163 clauses, 324711 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 --randec=0
c --randecint=1000
c --redcls=1
c --redclsglue=6
c --redclsmaxdec=5
c --redclsmaxdepth=10
c --redclsmaxlrg=10
c --redclsmaxprops=100
c --redclsatlimlo=0
c --redclsatlimhi=100
c --redclsize=30
c --redclstype=4
c --reducefixed=0
c --reduceinc=1000
c --reduceinit=50000
c --reduce=1
c --restart=4
c --restartglcint=10
c --restartglclim=115
c --restartinit=0
c --restartint=5
c --restartpen=1
c --retirenb=1
c --retireint=4
c --retiremin=1
c --reusetrail=0
c --rmincpen=4
c --rstinoutinc=110
c --satlimdelay=10000
c --scincinc=200
c --scincincsatlimhi=100
c --scincincdelta=10
c --scincincincint=100000
c --scincincmin=200
c --scincincmode=1
c --scoreshift=0
c --scoreresetint=2147483647
c --seed=0
c --simpbintinc=100
c --simpbintinclim=10000
c --simpcintdelay=2000
c --simpcintinc=20000
c --simpcintincdiv=1
c --simpcintmaxhard=10000000
c --simpcintmaxsoft=1000000
c --simpincdelmaxfact=50
c --simpincdelmaxmin=10000
c --simpinitdelay=0
c --simpintsizepen=0
c --simpen=0
c --simpidiv=3
c --simpiscale=100
c --simpitdelay=10
c --simpitintinc=10
c --simpitintinclim=1000
c --simplify=2
c --simprtc=5
c --simptintinc=1000
c --simptintinclim=10000
c --simpvarchg=100
c --simpvarlim=100
c --sizemaxpen=5
c --sizepen=1000000
c --sleeponabort=0
c --smallirr=90
c --smallve=1
c --smallvevars=10
c --smallvewait=0
c --sortlits=0
c --subl=9
c --sweep=1
c --sweepboost=10
c --sweepboostdel=4
c --sweepboostint=7
c --sweepboostvlim=1000000
c --sweepfacdec=10
c --sweepforgive=2
c --sweepirr=3
c --sweepmaxeff=200000000
c --sweepmaxdec=10000
c --sweepmaxround=3
c --sweepmindec=100
c --sweepmineff=1000000
c --sweepred=3
c --sweepreleff=3
c --sweeprtc=0
c --sweeprtcint=14
c --sweeprtcintvlim=100000
c --sweepsuccessmaxwortc=6
c --sweepsuccessrat=1000
c --sweepwait=2
c --synclsall=1
c --synclsglue=8
c --synclsint=100
c --synclslen=40
c --syncunint=111111
c --termint=122222
c --ternres=1
c --ternresboost=5
c --ternresrtc=0
c --ternreswait=2
c --transred=1
c --transredwait=2
c --trapiflush=0
c --trdmaxeff=2000000
c --trdmineff=100000
c --trdreleff=10
c --treelook=1
c --treelookboost=10
c --treelookfull=0
c --treelookmaxeff=50000000
c --treelookmineff=300000
c --treelookreleff=2
c --treelookrtc=0
c --trep=1
c --trepint=55555
c --trnreleff=10
c --trnrmaxeff=200000000
c --trnrmineff=4000000
c --unhdatrn=2
c --unhdextstamp=1
c --unhdhbr=0
c --unhdlnpr=3
c --unhdmaxeff=20000000
c --unhdmineff=100000
c --unhdreleff=2
c --unhdroundlim=20
c --unhide=1
c --unhidewait=0
c --usedtwice=1
c --vsidsdint=256
c --wait=1
c --waitmax=4
c --witness=0
c --check=0
c --log=-1
c --profile=1
c --profilelong=1
c --verbose=1
c [freezer] frozen 0 variables out of 47271 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 [set-score-increment-1] factor 1.200000d+00 (200/1000) after 0 conflicts
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   47271   137669         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 17 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] 17 out of 17 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] generated 37 at-most-one constraints, 26 used 70%
c [card-1] exported 37 binary clauses, 1.4 per/constraint
c [decomp-1] removed 748 variables
c [simpleprobe-1] all 46898 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 1214 variables
c [simpleprobe-1] fully completed simple probing
c [simpleprobe-1] removed 1214 variables, found 1969 hbrs, 161 units
c [unhide-1] limit 100000 with penalty 0 = 0 + 0
c [unhide-1-1] 1 units, 1 failed, 18 tauts, 0 hbrs, 6 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 45647 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 33377 variables 73% in round 1 in 9763130 steps
c [elim-1-1] backward subsumption/strengthening limit 9763100
c [elim-1-1-1] backward checking 32926 touched variables 72%
c [elim-1-1-1] incomplete backward checking 32884 remain 100%
c [elim-1-1] subsumed 12 and strengthened 70 clauses in 9764708 steps
c [elim-1-1] rescheduled 181 variables 0% by backward subsumption
c [elim-1-2] eliminated 4 variables 0% in round 2 in 193712 steps
c [elim-1-2] backward subsumption/strengthening limit 193700
c [elim-1-2-1] backward checking 32889 touched variables 72%
c [elim-1-2-1] incomplete backward checking 32864 remain 100%
c [elim-1-2] subsumed 0 and strengthened 1 clauses in 193855 steps
c [elim-1-2] rescheduled 4 variables 0% by backward subsumption
c [elim-1-3] no variable eliminated in round 3 in 3281 steps
c [elim-1] fully completed in 3 rounds
c [elim-1] transition to [ all 0 rem 0 ] state
c [elim-1] eliminated 33384 = 73% variables out of 45647 scheduled
c [phase-count-1] 60341 negative 90.0% of 67077 except 6736 10.0%
c [phase-count-1] 56202 positive 83.8% of 67077 except 10875 16.2%
c [phase-1] phase bias: 3109 positive 25%, 9154 negative 75%
c [score-distribution-1] 0 pos 0.00%, 0 min 0.00%, 12263 zero 100.00%
c [score-distribution-1] 1 different 0.01% out of total 12263 variables
c [simplification-1] removed 35008 variables 74.1% (12263 remain 26%)
c [simplification-1] removed 70592 irredundant clauses 51.3% (67077 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 32 variables
c [simpleprobe-2] all 12231 free variables schedulable
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [decomp-4] removed 53 variables
c [simpleprobe-2] 3193 variables remain 26% (8985 retained 74%)
c [simpleprobe-2] removed 53 variables, found 663 hbrs, 8 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 24356 literals 100%
c [treelook-1] scheduling used 275174 steps
c [treelook-1] scheduled completely
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 397262 steps
c [treelook-1] 24312 literals remain 100%
c [treelook-1] 12177 variables remain to probed next time 100%
c [treelook-1] removed 1 variables, found 3660 hbrs
c [basicprobe-1] limit 1000000 penalty 0 = 0 + 0
c [basicprobe-1-0] 6067 probes remain 50% after last round
c [basicprobe-1-0] 1 units = 1 failed (100%) + 0 lifted (0%)
c [basicprobe-1-0] removed 2 variables, found 3679 hbrs
c [unhide-2] limit 100000 with penalty 0 = 0 + 0
c [unhide-2-2] 2 units, 0 failed, 1392 tauts, 0 hbrs, 1255 literals
c [block-1] scheduling all variables this time
c [block-1] scheduled 12173 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 2352 blocked clauses
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 2 clauses out of 26 (8%) of length 16
c [cce-1-1] eliminated 2 clauses out of 34 (6%) of length 15
c [cce-1-1] eliminated 2 clauses out of 45 (4%) of length 14
c [cce-1-1] eliminated 1 clauses out of 59 (2%) of length 13
c [cce-1-1] eliminated 3 clauses out of 69 (4%) of length 12
c [cce-1-1] eliminated 4 clauses out of 55 (7%) of length 11
c [cce-1-1] eliminated 17 clauses out of 173 (10%) of length 10
c [cce-1-1] eliminated 12 clauses out of 310 (4%) of length 9
c [cce-1-1] eliminated 44 clauses out of 634 (7%) of length 8
c [cce-1-1] eliminated 72 clauses out of 1236 (6%) of length 7
c [cce-1-1] eliminated 258 clauses out of 3061 (8%) of length 6
c [cce-1-1] eliminated 321 clauses out of 6125 (5%) of length 5
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 738 large clauses in 30000013 steps
c [cce-1-1] allowing another 15000006 steps for small clauses
c [cce-1-1] scheduling 21458 clauses = 13368 binary + 8090 ternary
c [cce-1-1] tried to eliminate 12296 small clauses 57%
c [cce-1-1] eliminated 128 binary clauses 1%
c [cce-1-1] eliminated 196 ternary clauses 2%
c [cce-1-1] eliminated 324 small clauses 2%
c [cce-1-1] eliminated 324 small clauses in 30000118 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 1062 covered clauses in round 1
c [cce-1] eliminated 1062 covered clauses in TOTAL during 1 rounds
c [elim-2] scheduling all variables this time
c [elim-2] scheduled 12145 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 649 variables 5% in round 1 in 9730499 steps
c [elim-2-1] backward subsumption/strengthening limit 9730400
c [elim-2-1-1] backward checking 3818 touched variables 31%
c [elim-2-1-1] incomplete backward checking 3649 remain 96%
c [elim-2-1] subsumed 2 and strengthened 26 clauses in 9732933 steps
c [elim-2-1] rescheduled 93 variables 1% by backward subsumption
c [elim-2-2] no variable eliminated in round 2 in 442240 steps
c [elim-2] fully completed in 2 rounds
c [elim-2] transition to [ all 0 rem 0 ] state
c [elim-2] eliminated 649 = 5% variables out of 12145 scheduled
c [bca-1] limit of 10000000 steps and 125334 added (scaled 2)
c [bca-1] 20637 out of 22994 literals actually usable 90%
c [bca-1] added 761 blocked clauses in 54948 steps
c [sweep-1] limit 1000000 penalty 0 = 0 + 0
c [sweep-1-1] 4891 pos 42.5% + 6605 neg 57.5% = 11496 sched 100.0% ret 0
c [sweep-1-1] 1016513 steps 114 queries 549.30 avg class size
c [sweep-1-1] 1647 decisions 112 SAT calls 59.00 avg env size
c [sweep-1-1] 9639 variables remain 84% (1857 retained 16%)
c [decomp-6] removed 23 variables
c [sweep-1-1] removed 23 vars (0 failed, 4 eqs, 2 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 23 vars in TOTAL (1 rounds, 113 queries)
c [score-distribution-2] 4250 pos 37.04%, 0 min 0.00%, 7223 zero 62.96%
c [score-distribution-2] 1706 different 14.87% out of total 11473 variables
c [simplification-2] removed 790 variables 6.4% (11473 remain 24%)
c [simplification-2] removed 4687 irredundant clauses 7.0% (62390 remain 45%)
c [simplification-2] maximum reduction of 7% = max (6%, 7%)
c [simplification-2] large reduction 7% >= 5% limit
c [simplification-2] next conflict interval 2000 = 2000/1
c [simplification-2] penalized conflict interval 2000 = 1 * 2000
c [simplification-2] hard conflict limit 13000 (soft 3000 + delta 10000)
c [simplification-2] new conflict limit 3000 (hard 13000)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i    3.4   11472    62390      1730    1231   1189  7946    2    56    7   4%     14   55    7    0 4387%
c 
c [simplification-3] limit 3000 conflicts (hard 13000) hit after 3001 conflicts
c [quatres-1] found 13436 quaternary clauses 51% in total
c [quatres-1-1] added 1 double-self-subsuming ternary resolvents
c [quatres-1-2] added 26 single-self-subsuming ternary resolvents
c [quatres-1-2] added 1157 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 11472 free variables schedulable
c [ternres-1] 6489 ternary resolvents (149 bin, 6340 trn)
c [ternres-1] fully completed ternary resolution
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 303 at-most-one constraints of average size 4.0
c [card-2] found 49 at-most-two constraints of average size 4.1
c [card-2] using previous limit 1000000 for elimination
c [card-2] 352 out of 352 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] generated 17 at-most-one constraints, 5 used 29%
c [card-2] exported 5 binary clauses, 1.0 per/constraint
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 5575 xors of average arity 3.1
c [gauss-1] connected 17083 occurrences of 1225 variables (average 13.9)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] fully completed
c [gauss-1] exported 0 unary, 0 binary and 1 ternary equations
c [decomp-7] removed 14 variables
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] scheduled 22916 literals 100%
c [treelook-2] scheduling used 296670 steps
c [treelook-2] scheduled completely
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] used 306417 steps
c [treelook-2] 22856 literals remain 100%
c [treelook-2] 11458 variables remain to probed next time 100%
c [decomp-8] removed 5 variables
c [treelook-2] removed 5 variables, found 1830 hbrs
c [unhide-3] limit 100000 with penalty 0 = 0 + 0
c [unhide-3-3] 0 units, 0 failed, 285 tauts, 0 hbrs, 1031 literals
c [transred-1] limit 126800 with penalty 0 = 0 + 0
c [transred-1] removed 62 transitive binary clauses
c [transred-1] found 1 units
c [block-2] scheduling all variables this time
c [block-2] scheduled 11452 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 4 blocked clauses
c [block-2] 4 < 1/100 * 62285 = 622 considered unsuccessful
c [cce-2] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-2-1] eliminated 1 clauses out of 50 (2%) of length 14
c [cce-2-1] eliminated 2 clauses out of 77 (3%) of length 12
c [cce-2-1] eliminated 3 clauses out of 77 (4%) of length 11
c [cce-2-1] eliminated 16 clauses out of 194 (8%) of length 10
c [cce-2-1] eliminated 3 clauses out of 313 (1%) of length 9
c [cce-2-1] eliminated 33 clauses out of 781 (4%) of length 8
c [cce-2-1] eliminated 63 clauses out of 1680 (4%) of length 7
c [cce-2-1] eliminated 86 clauses out of 2837 (3%) of length 6
c [cce-2-1] eliminated 1 clauses out of 6189 (0%) of length 5
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] eliminated 208 large clauses in 30000004 steps
c [cce-2-1] allowing another 15000002 steps for small clauses
c [cce-2-1] scheduling 29122 clauses = 12371 binary + 16751 ternary
c [cce-2-1] tried to eliminate 702 small clauses 2%
c [cce-2-1] eliminated 17 binary clauses 0%
c [cce-2-1] eliminated 3 ternary clauses 0%
c [cce-2-1] eliminated 20 small clauses 0%
c [cce-2-1] eliminated 20 small clauses in 30000004 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 228 covered clauses in round 1
c [cce-2] eliminated 228 covered clauses in TOTAL during 1 rounds
c [cce-2] 228 < 1/100 * 62279 = 622 considered unsuccessful
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 11452 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 111 variables 1% in round 1 in 11659647 steps
c [elim-3-1] backward subsumption/strengthening limit 8340353
c [elim-3-1-1] backward checking 869 touched variables 8%
c [elim-3-1-1] incomplete backward checking 858 remain 99%
c [elim-3-1] subsumed 1 and strengthened 5 clauses in 8341893 steps
c [elim-3] incomplete 20 not tried 0% in round 1
c [elim-3] transition to [ all 1 rem 1 ] state
c [elim-3] eliminated 111 = 1% variables out of 11452 scheduled
c [elim-3] 111 < 1/100 * 11452 = 114 considered unsuccessful
c [bca-2] limit of 10000000 steps and 124558 added (scaled 2)
c [bca-2] 15751 out of 22684 literals actually usable 69%
c [bca-2] added 3 blocked clauses in 44371 steps
c [sweep-2] limit 1000000 penalty 0 = 0 + 0
c [sweep-2-1] 4105 pos 43.2% + 5407 neg 56.8% = 9512 sched 83.9% ret 1829
c [sweep-2-1] 1034128 steps 130 queries 868.08 avg class size
c [sweep-2-1] 1855 decisions 129 SAT calls 28.47 avg env size
c [sweep-2-1] 8370 variables remain 74% (2971 retained 26%)
c [decomp-9] removed 26 variables
c [sweep-2-1] removed 26 vars (0 failed, 13 eqs, 8 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 26 vars in TOTAL (1 rounds, 129 queries)
c [score-distribution-3] 6735 pos 59.52%, 0 min 0.00%, 4580 zero 40.48%
c [score-distribution-3] 2866 different 25.33% out of total 11315 variables
c [simplification-3] removed 157 variables 1.4% (11315 remain 24%)
c [simplification-3] removed 581 irredundant clauses 0.9% (61809 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 23001 (soft 13001 + delta 10000)
c [simplification-3] new conflict limit 13001 (hard 23001)
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    5.6   11314    61809      3570    3735   7194 10094    4    91    8   4%     17   88    7    0 2068%
c i    5.7   11313    61809      4038    4120   7212 10098    4   100    8   4%     12   96    7    0 1896%
c i    5.7   11312    61809      4083    4140   7217 10101    4    99    8   4%     12   95    7    0 1755%
c i    6.2   11311    61808      7058    6642   7334 10155    6   116    8   5%     31  108    7    1 1045%
c i    6.5   11310    61808      8503    7868   7414 10172    6   118    8   5%     17  108    7    1  890%
c i    6.5   11309    61808      8679    8000   7430 10175    6   122    8   5%     14  111    7    1  822%
c i    6.6   11308    61807      9256    8474   7449 10182    6   123    8   5%      9  111    8    1  883%
c 
c [simplification-4] limit of 138 binary hit after 138 binaries
c [quatres-2] found 15046 quaternary clauses 51% in total
c [quatres-2-1] added 4 double-self-subsuming ternary resolvents
c [quatres-2-2] added 46 single-self-subsuming ternary resolvents
c [quatres-2-2] added 534 quaternary resolvents
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] all 11308 free variables schedulable
c [ternres-2] 1029 ternary resolvents (72 bin, 957 trn)
c [ternres-2] fully completed ternary resolution
c [gauss-2] limit 2000000 penalty 0 = 0 + 0
c [gauss-2] extracted 5622 xors of average arity 3.0
c [gauss-2] connected 17100 occurrences of 1233 variables (average 13.9)
c [gauss-2] limit 2000000 penalty 0 = 0 + 0
c [gauss-2] fully completed
c [gauss-2] exported 0 unary, 0 binary and 8 ternary equations
c [decomp-10] removed 39 variables
c [basicprobe-2] limit 2613532 penalty 0 = 0 + 0
c [basicprobe-2-0] 3246 probes remain 29% after last round
c [basicprobe-2-0] 7 units = 7 failed (100%) + 0 lifted (0%)
c [basicprobe-2-0] removed 7 variables, found 4557 hbrs
c [bate-1] eliminated 28 asymmetric tautologies during probing
c [transred-2] limit 522706 with penalty 0 = 0 + 0
c [transred-2] removed 376 transitive binary clauses
c [transred-2] found 3 units
c [bca-3] limit of 10000000 steps and 124108 added (scaled 2)
c [bca-3] 10075 out of 22520 literals actually usable 45%
c [bca-3] added 3 blocked clauses in 35965 steps
c [sweep-3] limit 1000000 penalty 0 = 0 + 0
c [sweep-3-1] 3628 pos 43.6% + 4695 neg 56.4% = 8323 sched 73.9% ret 2936
c [sweep-3-1] 1016034 steps 79 queries 737.25 avg class size
c [sweep-3-1] 1293 decisions 76 SAT calls 32.79 avg env size
c [sweep-3-1] 7650 variables remain 68% (3609 retained 32%)
c [decomp-11] removed 40 variables
c [sweep-3-1] removed 40 vars (0 failed, 3 eqs, 0 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 40 vars in TOTAL (1 rounds, 78 queries)
c [score-distribution-4] 6928 pos 61.75%, 2535 min 22.60%, 1756 zero 15.65%
c [score-distribution-4] 3089 different 27.53% out of total 11219 variables
c [simplification-4] removed 89 variables 0.8% (11219 remain 24%)
c [simplification-4] removed 204 irredundant clauses 0.3% (61602 remain 45%)
c [simplification-4] maximum reduction of 1% = max (1%, 0%)
c [simplification-4] forced so keeping old conflict interval 10000
c [simplification-4] conflict limit remains at 13001 (hard 23001)
c [simplification-4] new binary interval 1000
c 
c [simplification-5] limit 13001 conflicts (hard 23001) hit after 13001 conflicts
c [quatres-3] found 15544 quaternary clauses 52% in total
c [quatres-3-1] added 1 double-self-subsuming ternary resolvents
c [quatres-3-2] added 21 single-self-subsuming ternary resolvents
c [quatres-3-2] added 173 quaternary resolvents
c [ternres-3] limit 4000000 with penalty 0 = 0 + 0
c [ternres-3] all 11219 free variables schedulable
c [ternres-3] 351 ternary resolvents (39 bin, 312 trn)
c [ternres-3] 1 variables remain 0% (11218 retained 100%)
c [gauss-3] limit 2000000 penalty 0 = 0 + 0
c [gauss-3] extracted 5455 xors of average arity 3.1
c [gauss-3] connected 16715 occurrences of 1161 variables (average 14.4)
c [gauss-3] limit 2000000 penalty 0 = 0 + 0
c [gauss-3] fully completed
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-12] removed 11 variables
c [simpleprobe-3] 2936 schedulable variables 26%
c [simpleprobe-3] limit 2247362 penalty 0 = 0 + 0
c [decomp-13] removed 18 variables
c [simpleprobe-3] 2381 variables remain 21% (8809 retained 79%)
c [simpleprobe-3] removed 18 variables, found 661 hbrs, 2 units
c [unhide-4] limit 56184 with penalty 1 = 1 + 0
c [unhide-4-4] 1 units, 0 failed, 1736 tauts, 0 hbrs, 5483 literals
c [transred-3] limit 561840 with penalty 0 = 0 + 0
c [transred-3] removed 311 transitive binary clauses
c [block-3] scheduling all variables this time
c [block-3] scheduled 11189 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 83 blocked clauses
c [block-3] 83 < 1/100 * 61461 = 614 considered unsuccessful
c [cce-3] limit of 15000000 steps penalty 1 = 1 + 0
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] allowing another 7500000 steps for small clauses
c [cce-3-1] scheduling 19739 clauses = 12142 binary + 7597 ternary
c [cce-3-1] tried to eliminate 1016 small clauses 5%
c [cce-3-1] eliminated 24 binary clauses 0%
c [cce-3-1] eliminated 14 ternary clauses 0%
c [cce-3-1] eliminated 38 small clauses 0%
c [cce-3-1] eliminated 38 small clauses in 15000001 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 38 covered clauses in round 1
c [cce-3] eliminated 38 covered clauses in TOTAL during 1 rounds
c [cce-3] 38 < 1/100 * 61377 = 613 considered unsuccessful
c [elim-4] no untried remaining variables left
c [elim-4] scheduled 11177 variables 100%
c [elim-4] boosting limit by 20
c [elim-4] limit of 200000000 steps penalty 1 = 1 + 0
c [elim-4] rescheduling of touched variables disabled
c [elim-4-1] eliminated 98 variables 1% in round 1 in 12671218 steps
c [elim-4-1] backward subsumption/strengthening limit 12671200
c [elim-4-1-1] backward checking 768 touched variables 7%
c [elim-4-1-1] fully completed backward checking in 1 rounds
c [elim-4-1] subsumed 5 and strengthened 21 clauses in 6075675 steps
c [elim-4-1] rescheduled 49 variables 0% by backward subsumption
c [elim-4-2] eliminated 2 variables 0% in round 2 in 446210 steps
c [elim-4-2] backward subsumption/strengthening limit 446200
c [elim-4-2-1] backward checking 19 touched variables 0%
c [elim-4-2-1] fully completed backward checking in 1 rounds
c [elim-4-2] subsumed 0 and strengthened 11 clauses in 41680 steps
c [elim-4-2] rescheduled 18 variables 0% by backward subsumption
c [elim-4-3] eliminated 1 variables 0% in round 3 in 38601 steps
c [elim-4-3] backward subsumption/strengthening limit 38600
c [elim-4-3-1] backward checking 5 touched variables 0%
c [elim-4-3-1] fully completed backward checking in 1 rounds
c [elim-4-3] subsumed 0 and strengthened 0 clauses in 31808 steps
c [elim-4] fully completed in 3 rounds
c [elim-4] transition to [ all 0 rem 0 ] state
c [elim-4] eliminated 101 = 1% variables out of 11177 scheduled
c [elim-4] 101 < 1/100 * 11177 = 111 considered unsuccessful
c [bca-4] limit of 10000000 steps and 122751 added (scaled 2)
c [bca-4] 9804 out of 22154 literals actually usable 44%
c [bca-4] added 7 blocked clauses in 35375 steps
c [sweep-4] limit 1000000 penalty 0 = 0 + 0
c [sweep-4-1] 3288 pos 43.6% + 4246 neg 56.4% = 7534 sched 68.0% ret 3542
c [sweep-4-1] 1017464 steps 75 queries 599.37 avg class size
c [sweep-4-1] 1426 decisions 71 SAT calls 32.14 avg env size
c [sweep-4-1] 6943 variables remain 63% (4132 retained 37%)
c [decomp-14] removed 27 variables
c [sweep-4-1] removed 27 vars (0 failed, 6 eqs, 4 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 27 vars in TOTAL (1 rounds, 74 queries)
c [score-distribution-5] 7424 pos 67.19%, 1958 min 17.72%, 1667 zero 15.09%
c [score-distribution-5] 3377 different 30.56% out of total 11049 variables
c [simplification-5] removed 170 variables 1.5% (11049 remain 23%)
c [simplification-5] removed 702 irredundant clauses 1.1% (60900 remain 44%)
c [simplification-5] maximum reduction of 2% = max (2%, 1%)
c [simplification-5] geometric conflict interval increment 6666 = 20000 / 3
c [simplification-5] new conflict interval 16666
c [simplification-5] penalized conflict interval 16666 = 1 * 16666
c [simplification-5] hard conflict limit 39667 (soft 29667 + delta 10000)
c [simplification-5] new conflict limit 29667 (hard 39667)
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   12.1   11048    60900     21380   18892   7911 13192    8   145    9   5%    158  112    9    2  444%
c i   12.6   11047    60900     23701   20929   7987 13211    8   141   10   5%     22  104    8    2  347%
c i   13.7   11046    60899     28273   24816   8148 13257    8   147   10   5%     37  104    8    3  298%
c 
c [simplification-6] limit 29667 conflicts (hard 39667) hit after 29668 conflicts
c [quatres-4] found 16287 quaternary clauses 49% in total
c [quatres-4-1] removed 2 duplicate quaternary clauses
c [quatres-4-1] added 3 double-self-subsuming ternary resolvents
c [quatres-4-2] added 121 single-self-subsuming ternary resolvents
c [quatres-4-2] added 220 quaternary resolvents
c [ternres-4] limit 4000000 with penalty 0 = 0 + 0
c [ternres-4] 1 schedulable variables 0%
c [ternres-4] 262 ternary resolvents (10 bin, 252 trn)
c [ternres-4] fully completed ternary resolution
c [card-3] limit 500000 penalty 2 = 2 + 0
c [card-3] found 228 at-most-one constraints of average size 3.6
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 500000 for elimination
c [card-3] 228 out of 228 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [decomp-15] removed 28 variables
c [treelook-3] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-3] scheduled 20013 literals 91%
c [treelook-3] scheduling used 300017 steps
c [treelook-3] not fully scheduled
c [treelook-3] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-3] used 304040 steps
c [treelook-3] 19984 literals remain 91%
c [treelook-3] 10958 variables remain to probed next time 99%
c [decomp-16] removed 1 variables
c [treelook-3] removed 4 variables, found 611 hbrs
c [unhide-5] limit 275796 with penalty 0 = 0 + 0
c [unhide-5-5] 2 units, 0 failed, 227 tauts, 0 hbrs, 6722 literals
c [transred-4] limit 1378983 with penalty 0 = 0 + 0
c [transred-4] removed 263 transitive binary clauses
c [transred-4] found 4 units
c [bca-5] limit of 10000000 steps and 122355 added (scaled 2)
c [bca-5] 5833 out of 22024 literals actually usable 26%
c [bca-5] added 0 blocked clauses in 39200 steps
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 10000000 penalty 0 = 0 + 0
c [sweep-5-1] 3155 pos 45.7% + 3751 neg 54.3% = 6906 sched 62.7% ret 4105
c [sweep-5-1] 10090650 steps 845 queries 52.38 avg class size
c [sweep-5-1] 15996 decisions 792 SAT calls 39.79 avg env size
c [sweep-5-1] 672 variables remain 6% (10331 retained 94%)
c [decomp-17] removed 179 variables
c [sweep-5-1] removed 179 vars (0 failed, 154 eqs, 133 impls)
c [sweep-5] considered successful since not run to completion yet
c [sweep-5] removed 179 vars in TOTAL (1 rounds, 844 queries)
c [score-distribution-6] 8259 pos 76.25%, 2397 min 22.13%, 176 zero 1.62%
c [score-distribution-6] 3528 different 32.57% out of total 10832 variables
c [simplification-6] removed 214 variables 1.9% (10832 remain 23%)
c [simplification-6] removed 276 irredundant clauses 0.5% (60623 remain 44%)
c [simplification-6] maximum reduction of 2% = max (2%, 0%)
c [simplification-6] geometric conflict interval increment 6666 = 20000 / 3
c [simplification-6] new conflict interval 23332
c [simplification-6] penalized conflict interval 23332 = 1 * 23332
c [simplification-6] hard conflict limit 64666 (soft 53000 + delta 11666)
c [simplification-6] new conflict limit 53000 (hard 64666)
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   14.9   10831    60622     30131   26954   8188 14955    8   140   12   5%      6   95    7    3  252%
c i   15.0   10830    60622     30532   27290   8202 14959    8   134   12   6%     -1   87    7    3  243%
c i   15.5   10829    60621     33318   29719   8264 14972    8   127   12   6%     11   77    9    3  294%
c i   16.2   10828    60616     36690   32583   8363 14998    8   125   12   6%     19   72    7    3  219%
c i   16.5   10827    60616     38253   33917   8398 15004    8   133   12   6%      1   78    8    3  242%
c i   16.5   10826    60616     38381   34012   8407 15007    8   133   12   6%     -1   78    8    3  240%
c i   16.6   10825    60616     38853   34411   8420 15009    8   136   12   6%     -7   80    9    3  262%
c i   17.4   10824    60610     42134   37278   8532 15023    8   130   12   6%     17   71    8    4  236%
c i   17.4   10823    60609     42422   37528   8544 15025    8   131   12   6%      9   72    9    4  245%
c i   17.9   10822    60609     44382   39284   8611 15037    8   122   12   6%      2   61    7    4  181%
c 
c [simplification-7] limit of 21 iterations hit after 21 iterations
c [quatres-5] found 17076 quaternary clauses 47% in total
c [quatres-5-1] removed 11 duplicate quaternary clauses
c [quatres-5-1] added 7 double-self-subsuming ternary resolvents
c [quatres-5-2] added 107 single-self-subsuming ternary resolvents
c [quatres-5-2] added 191 quaternary resolvents
c [ternres-5] limit 4000000 with penalty 0 = 0 + 0
c [ternres-5] all 10822 free variables schedulable
c [ternres-5] 1787 ternary resolvents (106 bin, 1681 trn)
c [ternres-5] fully completed ternary resolution
c [gauss-4] limit 1000000 penalty 1 = 1 + 0
c [gauss-4] extracted 2510 xors of average arity 3.0
c [gauss-4] connected 7458 occurrences of 1032 variables (average 7.2)
c [gauss-4] limit 1000000 penalty 1 = 1 + 0
c [gauss-4] fully completed
c [gauss-4] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-18] removed 29 variables
c [basicprobe-3] limit 10641762 penalty 0 = 0 + 0
c [basicprobe-3-0] 3158 sched 29%, 25 failed, 1 lifted, 5520 hbrs
c [decomp-19] removed 58 variables
c [basicprobe-3-1] 2333 probes remain 22% after last round
c [basicprobe-3-1] 37 units = 36 failed (97%) + 1 lifted (3%)
c [basicprobe-3-1] removed 69 variables, found 7085 hbrs
c [bate-2] eliminated 44 asymmetric tautologies during probing
c [unhide-6] limit 425670 with penalty 0 = 0 + 0
c [unhide-6-6] 0 units, 2 failed, 2176 tauts, 0 hbrs, 14660 literals
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 587 transitive binary clauses
c [transred-5] found 1 units
c [sweep-6] limit 1000000 penalty 0 = 0 + 0
c [sweep-6-1] 250 pos 38.6% + 397 neg 61.4% = 647 sched 6.0% ret 10075
c [sweep-6-1] 1008049 steps 59 queries 59.12 avg class size
c [sweep-6-1] 1158 decisions 54 SAT calls 51.15 avg env size
c [sweep-6-1] 521 variables remain 5% (10201 retained 95%)
c [decomp-20] removed 29 variables
c [sweep-6-1] removed 29 vars (0 failed, 7 eqs, 4 impls)
c [sweep-6] considered successful since not run to completion yet
c [sweep-6] removed 29 vars in TOTAL (1 rounds, 58 queries)
c [score-distribution-7] 7850 pos 73.41%, 2751 min 25.73%, 92 zero 0.86%
c [score-distribution-7] 3493 different 32.67% out of total 10693 variables
c [simplification-7] removed 129 variables 1.2% (10693 remain 23%)
c [simplification-7] removed 560 irredundant clauses 0.9% (60049 remain 44%)
c [simplification-7] maximum reduction of 1% = max (1%, 1%)
c [simplification-7] forced so keeping old conflict interval 23332
c [simplification-7] conflict limit remains at 53000 (hard 64666)
c [simplification-7] new iteration interval 100
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   19.0   10692    60049     45017   39593   9291 18093    8   126   14   6%     -5   64    8    4  221%
c i   19.0   10691    60049     45213   39753   9301 18094    8   126   14   6%     -8   64    8    4  220%
c i   20.1   10690    60047     50472   44252   9475 18127    8   129   14   6%     46   61    7    4  168%
c 
c [simplification-8] limit 53000 conflicts (hard 64666) hit after 53001 conflicts
c [quatres-6] found 17454 quaternary clauses 46% in total
c [quatres-6-1] removed 4 duplicate quaternary clauses
c [quatres-6-1] added 5 double-self-subsuming ternary resolvents
c [quatres-6-2] added 76 single-self-subsuming ternary resolvents
c [quatres-6-2] added 152 quaternary resolvents
c [ternres-6] limit 4000000 with penalty 0 = 0 + 0
c [ternres-6] all 10690 free variables schedulable
c [ternres-6] 1000 ternary resolvents (74 bin, 926 trn)
c [ternres-6] fully completed ternary resolution
c [decomp-21] removed 18 variables
c [simpleprobe-4] 2237 schedulable variables 21%
c [simpleprobe-4] limit 10313131 penalty 0 = 0 + 0
c [decomp-22] removed 45 variables
c [simpleprobe-4] 156 variables remain 1% (10474 retained 99%)
c [simpleprobe-4] removed 45 variables, found 2298 hbrs, 5 units
c [unhide-7] limit 515656 with penalty 0 = 0 + 0
c [unhide-7-7] 1 units, 0 failed, 524 tauts, 0 hbrs, 7138 literals
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 586 transitive binary clauses
c [block-4] scheduling all variables this time
c [block-4] scheduled 10629 variables 100%
c [block-4] limit of 12500000 steps penalty 2 = 2 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 162 blocked clauses
c [block-4] 162 < 1/100 * 59767 = 597 considered unsuccessful
c [cce-4] boosting limit by 10
c [cce-4] limit of 75000000 steps penalty 2 = 2 + 0
c [cce-4-1] eliminated 1 clauses out of 33 (3%) of length 14
c [cce-4-1] eliminated 2 clauses out of 90 (2%) of length 13
c [cce-4-1] eliminated 3 clauses out of 202 (1%) of length 10
c [cce-4-1] eliminated 1 clauses out of 337 (0%) of length 9
c [cce-4-1] eliminated 4 clauses out of 694 (1%) of length 8
c [cce-4-1] eliminated 11 clauses out of 1501 (1%) of length 7
c [cce-4-1] eliminated 66 clauses out of 2707 (2%) of length 6
c [cce-4-1] eliminated 609 clauses out of 6099 (10%) of length 5
c [cce-4-1] eliminated 784 clauses out of 12761 (6%) of length 4
c [cce-4-1] incomplete large round (ATE)
c [cce-4-1] eliminated 1481 large clauses in 75000018 steps
c [cce-4-1] allowing another 37500009 steps for small clauses
c [cce-4-1] scheduling 27504 clauses = 11588 binary + 15916 ternary
c [cce-4-1] tried to eliminate 10958 small clauses 40%
c [cce-4-1] eliminated 123 binary clauses 1%
c [cce-4-1] eliminated 373 ternary clauses 2%
c [cce-4-1] eliminated 496 small clauses 2%
c [cce-4-1] eliminated 496 small clauses in 75000003 steps
c [cce-4-1] incomplete small round (ATE)
c [cce-4-1] eliminated 1977 covered clauses in round 1
c [cce-4] eliminated 1977 covered clauses in TOTAL during 1 rounds
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 10615 variables 100%
c [elim-5] limit of 12891414 steps penalty 2 = 2 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5-1] eliminated 442 variables 4% in round 1 in 12374910 steps
c [elim-5-1] backward subsumption/strengthening limit 516504
c [elim-5-1-1] backward checking 2356 touched variables 22%
c [elim-5-1-1] incomplete backward checking 2017 remain 86%
c [elim-5-1] subsumed 3 and strengthened 6 clauses in 516820 steps
c [elim-5] incomplete 27 not tried 0% in round 1
c [elim-5] transition to [ all 1 rem 1 ] state
c [elim-5] eliminated 442 = 4% variables out of 10615 scheduled
c [bca-6] limit of 10000000 steps and 114391 added (scaled 2)
c [bca-6] 3733 out of 20348 literals actually usable 18%
c [bca-6] added 2 blocked clauses in 50966 steps
c [sweep-7] limit 1000000 penalty 0 = 0 + 0
c [sweep-7-1] 216 pos 45.7% + 257 neg 54.3% = 473 sched 4.6% ret 9700
c [sweep-7-1] 1036565 steps 69 queries 53.93 avg class size
c [sweep-7-1] 1253 decisions 61 SAT calls 42.20 avg env size
c [sweep-7-1] 342 variables remain 3% (9831 retained 97%)
c [decomp-23] removed 15 variables
c [sweep-7-1] removed 15 vars (0 failed, 12 eqs, 13 impls)
c [sweep-7] removed 15 vars in TOTAL (1 rounds, 68 queries)
c [score-distribution-8] 8414 pos 82.83%, 1696 min 16.70%, 48 zero 0.47%
c [score-distribution-8] 3547 different 34.92% out of total 10158 variables
c [simplification-8] removed 532 variables 5.0% (10158 remain 21%)
c [simplification-8] removed 3306 irredundant clauses 5.5% (56740 remain 41%)
c [simplification-8] maximum reduction of 6% = max (5%, 6%)
c [simplification-8] large reduction 6% >= 5% limit
c [simplification-8] next conflict interval 2000 = 2000/1
c [simplification-8] penalized conflict interval 2000 = 1 * 2000
c [simplification-8] hard conflict limit 65001 (soft 55001 + delta 10000)
c [simplification-8] new conflict limit 55001 (hard 65001)
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   23.7   10157    56736     54529   44135   9548 16960    8   128   14   6%     28   57    8    4  196%
c 
c [simplification-9] limit 55001 conflicts (hard 65001) hit after 55002 conflicts
c [quatres-7] found 16529 quaternary clauses 46% in total
c [quatres-7-1] removed 9 duplicate quaternary clauses
c [quatres-7-1] added 4 double-self-subsuming ternary resolvents
c [quatres-7-2] added 56 single-self-subsuming ternary resolvents
c [quatres-7-2] added 214 quaternary resolvents
c [ternres-7] limit 4000000 with penalty 0 = 0 + 0
c [ternres-7] all 10157 free variables schedulable
c [ternres-7] 877 ternary resolvents (66 bin, 811 trn)
c [ternres-7] 2 variables remain 0% (10155 retained 100%)
c [decomp-24] removed 12 variables
c [treelook-4] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-4] scheduled 16399 literals 81%
c [treelook-4] scheduling used 300076 steps
c [treelook-4] not fully scheduled
c [treelook-4] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-4] used 304759 steps
c [treelook-4] 16349 literals remain 81%
c [treelook-4] 9793 variables remain to probed next time 97%
c [treelook-4] removed 0 variables, found 289 hbrs
c [unhide-8] limit 539964 with penalty 0 = 0 + 0
c [unhide-8-8] 1 units, 4 failed, 1619 tauts, 0 hbrs, 7190 literals
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 361 transitive binary clauses
c [transred-7] found 1 units
c [bca-7] limit of 10000000 steps and 114266 added (scaled 2)
c [bca-7] 3545 out of 20286 literals actually usable 17%
c [bca-7] added 0 blocked clauses in 52234 steps
c [sweep-8] limit 1000000 penalty 0 = 0 + 0
c [sweep-8-1] 169 pos 49.6% + 172 neg 50.4% = 341 sched 3.4% ret 9801
c [sweep-8-1] 1010261 steps 132 queries 40.98 avg class size
c [sweep-8-1] 2158 decisions 117 SAT calls 36.03 avg env size
c [sweep-8-1] 94 variables remain 1% (10048 retained 99%)
c [decomp-26] removed 28 variables
c [sweep-8-1] removed 28 vars (0 failed, 21 eqs, 18 impls)
c [sweep-8] removed 28 vars in TOTAL (1 rounds, 131 queries)
c [score-distribution-9] 6826 pos 67.49%, 3268 min 32.31%, 20 zero 0.20%
c [score-distribution-9] 3372 different 33.34% out of total 10114 variables
c [simplification-9] removed 43 variables 0.4% (10114 remain 21%)
c [simplification-9] removed 63 irredundant clauses 0.1% (56673 remain 41%)
c [simplification-9] maximum reduction of 0% = max (0%, 0%)
c [simplification-9] full geometric conflict interval increment 23332
c [simplification-9] new conflict interval 46664
c [simplification-9] penalized conflict interval 46664 = 1 * 46664
c [simplification-9] hard conflict limit 124998 (soft 101666 + delta 23332)
c [simplification-9] new conflict limit 101666 (hard 124998)
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   24.5   10113    56673     55370   44799   9747 15784    8   141   14   6%      4   69    8    4  182%
c i   25.0   10112    56673     57434   46595   9803 15801    8   143   14   6%      1   69    7    4  153%
c i   25.1   10111    56673     57910   47013   9817 15805    8   136   14   6%     -6   61    6    4  141%
c i   25.1   10110    56673     58098   47167   9828 15810    8   132   14   6%     -8   58    6    4  129%
c i   25.6   10109    56673     59872   48723   9894 15824    8   142   14   5%     -4   66    8    5  168%
c i   25.7   10108    56673     60276   49047   9916 15833    8   136   14   6%     -8   59    7    5  156%
c i   27.2   10107    56673     66745   54891  10058 15862    8   122   15   7%     62   40    8    5  160%
c i   29.0   10106    56673     75742   62905  10230 15912    8   120   15   7%     96   33    8    5  150%
c -   30.0   10106    56673     79921   26810  10291 15936    8   109   12   8%     22   20    9    6  163%
c i   31.8   10105    56673     88697   34751  10426 15964    8   110   13   7%    145   18    7    6  126%
c i   32.0   10104    56673     89469   35439  10445 15974    8   110   13   7%     49   18    8    6  136%
c i   32.0   10103    56673     89687   35639  10451 15974    8   108   13   7%     32   16    8    6  135%
c 
c [simplification-10] limit 101666 conflicts (hard 124998) hit after 101666 conflicts
c [quatres-8] found 18063 quaternary clauses 41% in total
c [quatres-8-1] removed 8 duplicate quaternary clauses
c [quatres-8-1] added 1 double-self-subsuming ternary resolvents
c [quatres-8-2] added 152 single-self-subsuming ternary resolvents
c [quatres-8-2] added 254 quaternary resolvents
c [ternres-8] limit 5373805 with penalty 0 = 0 + 0
c [ternres-8] 2 schedulable variables 0%
c [ternres-8] 557 ternary resolvents (51 bin, 506 trn)
c [ternres-8] fully completed ternary resolution
c [card-4] limit 335862 penalty 3 = 3 + 0
c [card-4] found 155 at-most-one constraints of average size 3.3
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 335862 for elimination
c [card-4] 155 out of 155 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [gauss-5] limit 500000 penalty 2 = 2 + 0
c [gauss-5] extracted 1138 xors of average arity 3.0
c [gauss-5] connected 3373 occurrences of 815 variables (average 4.1)
c [gauss-5] limit 500000 penalty 2 = 2 + 0
c [gauss-5] fully completed
c [gauss-5] exported 0 unary, 0 binary and 1 ternary equations
c [decomp-27] removed 45 variables
c [basicprobe-4] limit 26869025 penalty 0 = 0 + 0
c [basicprobe-4-0] 2330 sched 23%, 20 failed, 0 lifted, 2677 hbrs
c [decomp-28] removed 29 variables
c [basicprobe-4-1] 5831 sched 58%, 31 failed, 0 lifted, 3621 hbrs
c [decomp-29] removed 52 variables
c [basicprobe-4-2] 5763 sched 58%, 3 failed, 0 lifted, 450 hbrs
c [decomp-30] removed 5 variables
c [basicprobe-4-3] 2620 probes remain 26% after last round
c [basicprobe-4-3] 54 units = 54 failed (100%) + 0 lifted (0%)
c [basicprobe-4-3] removed 86 variables, found 6771 hbrs
c [bate-3] eliminated 37 asymmetric tautologies during probing
c [unhide-9] limit 1074761 with penalty 0 = 0 + 0
c [unhide-9-10] 0 units, 0 failed, 1904 tauts, 0 hbrs, 23004 literals
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 454 transitive binary clauses
c [cce-5] limit of 15000000 steps penalty 1 = 1 + 0
c [cce-5-1] eliminated 4 clauses out of 92 (4%) of length 11
c [cce-5-1] eliminated 3 clauses out of 197 (2%) of length 10
c [cce-5-1] incomplete large round (ACCE)
c [cce-5-1] eliminated 7 large clauses in 15000001 steps
c [cce-5-1] allowing another 7500000 steps for small clauses
c [cce-5-1] scheduling 25398 clauses = 10753 binary + 14645 ternary
c [cce-5-1] tried to eliminate 583 small clauses 2%
c [cce-5-1] eliminated 11 binary clauses 0%
c [cce-5-1] eliminated 18 ternary clauses 0%
c [cce-5-1] eliminated 29 small clauses 0%
c [cce-5-1] eliminated 29 small clauses in 15000001 steps
c [cce-5-1] incomplete small round (ACCE)
c [cce-5-1] eliminated 36 covered clauses in round 1
c [cce-5] eliminated 36 covered clauses in TOTAL during 1 rounds
c [cce-5] 36 < 1/100 * 56181 = 561 considered unsuccessful
c [elim-6] no untried remaining variables left
c [elim-6] scheduled 9972 variables 100%
c [elim-6] limit of 53738051 steps penalty 1 = 1 + 0
c [elim-6] rescheduling of touched variables disabled
c [elim-6-1] eliminated 124 variables 1% in round 1 in 12172129 steps
c [elim-6-1] backward subsumption/strengthening limit 12172100
c [elim-6-1-1] backward checking 778 touched variables 8%
c [elim-6-1-1] fully completed backward checking in 1 rounds
c [elim-6-1] subsumed 11 and strengthened 22 clauses in 10112106 steps
c [elim-6-1] rescheduled 59 variables 1% by backward subsumption
c [elim-6-2] eliminated 4 variables 0% in round 2 in 290125 steps
c [elim-6-2] backward subsumption/strengthening limit 290100
c [elim-6-2-1] backward checking 25 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 35891 steps
c [elim-6] fully completed in 2 rounds
c [elim-6] transition to [ all 0 rem 0 ] state
c [elim-6] eliminated 128 = 1% variables out of 9972 scheduled
c [sweep-9] limit 1612141 penalty 0 = 0 + 0
c [sweep-9-1] 50 pos 58.1% + 36 neg 41.9% = 86 sched 0.9% ret 9758
c [sweep-9-1] 543028 steps 57 queries 9.16 avg class size
c [sweep-9-1] 1045 decisions 50 SAT calls 43.64 avg env size
c [sweep-9-1] fully completed sweeping round
c [decomp-31] removed 32 variables
c [sweep-9-1] removed 32 vars (0 failed, 11 eqs, 4 impls)
c [sweep-9-2] 4363 pos 44.5% + 5449 neg 55.5% = 9812 sched 100.0% ret 0
c [sweep-9-2] 1078228 steps 47 queries 744.91 avg class size
c [sweep-9-2] 1441 decisions 46 SAT calls 65.50 avg env size
c [sweep-9-2] 9173 variables remain 93% (639 retained 7%)
c [decomp-32] removed 3 variables
c [sweep-9-2] removed 3 vars (0 failed, 3 eqs, 2 impls)
c [sweep-9] removed 35 vars in TOTAL (2 rounds, 102 queries)
c [score-distribution-10] 6472 pos 65.98%, 3336 min 34.01%, 1 zero 0.01%
c [score-distribution-10] 3454 different 35.21% out of total 9809 variables
c [simplification-10] removed 294 variables 2.9% (9809 remain 21%)
c [simplification-10] removed 1238 irredundant clauses 2.2% (55434 remain 40%)
c [simplification-10] maximum reduction of 3% = max (3%, 2%)
c [simplification-10] geometric conflict interval increment 11666 = 46664 / 4
c [simplification-10] new conflict interval 58330
c [simplification-10] penalized conflict interval 58330 = 1 * 58330
c [simplification-10] hard conflict limit 189161 (soft 159996 + delta 29165)
c [simplification-10] new conflict limit 159996 (hard 189161)
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   38.6    9808    55434    105075   47555   9673 17426    8    90   14   9%    167   -3    8    6  119%
c i   40.1    9807    55434    114569   56283   9775 17436    8    99   14   8%     71    7    8    7  130%
c i   40.3    9806    55434    115476   57115   9788 17439    8   100   14   8%     -2    8    8    7  130%
c i   42.9    9805    55432    126947   67676   9936 17474    9    88   16  10%     99   -4    9    7  133%
c i   44.2    9803    55432    133006   73249   9990 17484    9    86   17  10%     15   -6    9    7  126%
c i   44.9    9802    55432    135851   75855  10038 17490    9    81   17  11%    -29  -11    9    7  124%
c -   45.0    9802    55432    136219   39388  10041 17490    9    79   12  11%    -38  -13    9    7  128%
c i   46.1    9801    55432    146499   49029  10092 17495    8    75   21  11%     85  -13    9    7  120%
c i   48.1    9800    55431    158718   60076  10216 17519    8   115   15   7%    105   28    9    7  120%
c 
c [simplification-11] limit 159996 conflicts (hard 189161) hit after 164122 conflicts
c [quatres-9] found 18747 quaternary clauses 36% in total
c [quatres-9-1] removed 16 duplicate quaternary clauses
c [quatres-9-1] added 5 double-self-subsuming ternary resolvents
c [quatres-9-2] added 222 single-self-subsuming ternary resolvents
c [quatres-9-2] added 317 quaternary resolvents
c [ternres-9] limit 8332846 with penalty 0 = 0 + 0
c [ternres-9] all 9800 free variables schedulable
c [ternres-9] 3222 ternary resolvents (192 bin, 3030 trn)
c [ternres-9] fully completed ternary resolution
c [decomp-33] removed 95 variables
c [simpleprobe-5] 135 schedulable variables 1%
c [simpleprobe-5] limit 33331385 penalty 0 = 0 + 0
c [decomp-34] removed 42 variables
c [simpleprobe-5] 6 variables remain 0% (9666 retained 100%)
c [simpleprobe-5] removed 42 variables, found 2251 hbrs, 18 units
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 816 transitive binary clauses
c [transred-9] found 2 units
c [elim-7] scheduling all variables this time
c [elim-7] scheduled 9670 variables 100%
c [elim-7] limit of 166656926 steps penalty 0 = 0 + 0
c [elim-7] rescheduling of touched variables disabled
c [elim-7-1] eliminated 125 variables 1% in round 1 in 19399733 steps
c [elim-7-1] backward subsumption/strengthening limit 19399700
c [elim-7-1-1] backward checking 589 touched variables 6%
c [elim-7-1-1] fully completed backward checking in 1 rounds
c [elim-7-1] subsumed 4 and strengthened 13 clauses in 3249214 steps
c [elim-7-1] rescheduled 27 variables 0% by backward subsumption
c [elim-7-2] no variable eliminated in round 2 in 7307594 steps
c [elim-7] fully completed in 2 rounds
c [elim-7] transition to [ all 0 rem 0 ] state
c [elim-7] eliminated 125 = 1% variables out of 9670 scheduled
c [bca-8] limit of 10000000 steps and 109192 added (scaled 2)
c [bca-8] 2822 out of 19092 literals actually usable 15%
c [bca-8] added 10 blocked clauses in 67649 steps
c [sweep-10] limit 2499853 penalty 0 = 0 + 0
c [sweep-10-1] 4004 pos 44.9% + 4916 neg 55.1% = 8920 sched 93.5% ret 625
c [sweep-10-1] 3216811 steps 71 queries 538.42 avg class size
c [sweep-10-1] 2555 decisions 66 SAT calls 80.12 avg env size
c [sweep-10-1] 7669 variables remain 80% (1876 retained 20%)
c [decomp-35] removed 9 variables
c [sweep-10-1] removed 9 vars (0 failed, 6 eqs, 8 impls)
c [sweep-10] removed 9 vars in TOTAL (1 rounds, 70 queries)
c [score-distribution-11] 5769 pos 60.50%, 3766 min 39.49%, 1 zero 0.01%
c [score-distribution-11] 3293 different 34.53% out of total 9536 variables
c [simplification-11] removed 264 variables 2.7% (9536 remain 20%)
c [simplification-11] removed 1287 irredundant clauses 2.3% (54144 remain 39%)
c [simplification-11] maximum reduction of 3% = max (3%, 2%)
c [simplification-11] geometric conflict interval increment 14582 = 58330 / 4
c [simplification-11] new conflict interval 72912
c [simplification-11] penalized conflict interval 72912 = 1 * 72912
c [simplification-11] hard conflict limit 273490 (soft 237034 + delta 36456)
c [simplification-11] new conflict limit 237034 (hard 273490)
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   50.4    9535    54144    165324   62947  12262 18194    8   120   17   7%     18   32    9    7  120%
c i   52.1    9534    54144    183909   80189  12324 18216    7    80   17   9%    187   -4    7    7   89%
c -   52.6    9534    54144    187630   52265  12343 18220    8   146   13   5%    -38   60    9    7  118%
c i   52.8    9533    54144    190134   54556  12359 18221    8   130   15   6%     -5   42    9    8  120%
c i   53.4    9532    54144    196771   60647  12367 18226    8    63   22  12%      5  -24    8    7  113%
c i   54.7    9531    54144    207013   70199  12405 18234    8    70   23  12%     62  -15    9    8  121%
c -   57.6    9531    54144    227498   57407  12494 18246    9    63   14  14%    201  -26   10    8  132%
c -   62.3    9531    54144    268190   64379  12565 18254    8    50   22  17%    582  -16    8    8  109%
c 
c [simplification-12] limit 237034 conflicts (hard 273490) hit after 273491 conflicts
c [quatres-10] found 19027 quaternary clauses 30% in total
c [quatres-10-1] removed 29 duplicate quaternary clauses
c [quatres-10-1] added 3 double-self-subsuming ternary resolvents
c [quatres-10-2] added 158 single-self-subsuming ternary resolvents
c [quatres-10-2] added 205 quaternary resolvents
c [ternres-10] limit 12499679 with penalty 0 = 0 + 0
c [ternres-10] all 9531 free variables schedulable
c [ternres-10] 1590 ternary resolvents (101 bin, 1489 trn)
c [ternres-10] 1 variables remain 0% (9530 retained 100%)
c [gauss-6] limit 1249967 penalty 1 = 1 + 0
c [gauss-6] extracted 2222 xors of average arity 3.0
c [gauss-6] connected 6568 occurrences of 855 variables (average 7.7)
c [gauss-6] limit 1249967 penalty 1 = 1 + 0
c [gauss-6] fully completed
c [gauss-6] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-36] removed 38 variables
c [unhide-10] limit 1249967 with penalty 1 = 1 + 0
c [unhide-10-11] 1 units, 3 failed, 2457 tauts, 0 hbrs, 23225 literals
c [transred-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 650 transitive binary clauses
c [transred-10] found 2 units
c [block-5] scheduling all variables this time
c [block-5] scheduled 9487 variables 100%
c [block-5] limit of 15624599 steps penalty 3 = 3 + 0
c [block-5] fully completed
c [block-5] transition to [ all 0 rem 0 ] state
c [block-5] eliminated 447 blocked clauses
c [block-5] 447 < 1/100 * 54069 = 540 considered unsuccessful
c [elim-8] scheduling all variables this time
c [elim-8] scheduled 9453 variables 100%
c [elim-8] boosting limit by 20
c [elim-8] limit of 4999871880 steps penalty 0 = 0 + 0
c [elim-8] rescheduling of touched variables disabled
c [elim-8-1] eliminated 136 variables 1% in round 1 in 18848693 steps
c [elim-8-1] backward subsumption/strengthening limit 18848600
c [elim-8-1-1] backward checking 534 touched variables 6%
c [elim-8-1-1] fully completed backward checking in 1 rounds
c [elim-8-1] subsumed 1 and strengthened 9 clauses in 1686912 steps
c [elim-8-1] rescheduled 35 variables 0% by backward subsumption
c [elim-8-2] eliminated 6 variables 0% in round 2 in 53330 steps
c [elim-8-2] backward subsumption/strengthening limit 53300
c [elim-8-2-1] backward checking 11 touched variables 0%
c [elim-8-2-1] fully completed backward checking in 1 rounds
c [elim-8-2] subsumed 0 and strengthened 0 clauses in 27826 steps
c [elim-8] fully completed in 2 rounds
c [elim-8] transition to [ all 0 rem 0 ] state
c [elim-8] eliminated 142 = 2% variables out of 9453 scheduled
c [bca-9] limit of 10000000 steps and 106561 added (scaled 2)
c [bca-9] 3006 out of 18624 literals actually usable 16%
c [bca-9] added 21 blocked clauses in 73598 steps
c [sweep-11] boosting sweeping limit by 10
c [sweep-11] limit 37499030 penalty 0 = 0 + 0
c [sweep-11-1] 3264 pos 43.7% + 4203 neg 56.3% = 7467 sched 80.2% ret 1844
c [sweep-11-1] 33479053 steps 1341 queries 40.90 avg class size
c [sweep-11-1] 19106 decisions 1092 SAT calls 44.46 avg env size
c [sweep-11-1] fully completed sweeping round
c [decomp-37] removed 533 variables
c [sweep-11-1] removed 533 vars (0 failed, 541 eqs, 523 impls)
c [sweep-11-2] 3824 pos 43.6% + 4954 neg 56.4% = 8778 sched 100.0% ret 0
c [sweep-11-2] 4047897 steps 136 queries 187.46 avg class size
c [sweep-11-2] 3458 decisions 130 SAT calls 69.93 avg env size
c [sweep-11-2] 5851 variables remain 67% (2927 retained 33%)
c [decomp-38] removed 7 variables
c [sweep-11-2] removed 7 vars (0 failed, 6 eqs, 11 impls)
c [sweep-11] removed 540 vars in TOTAL (2 rounds, 1475 queries)
c [score-distribution-12] 3995 pos 45.55%, 4775 min 54.44%, 1 zero 0.01%
c [score-distribution-12] 2231 different 25.44% out of total 8771 variables
c [simplification-12] removed 760 variables 8.0% (8771 remain 19%)
c [simplification-12] removed 1848 irredundant clauses 3.4% (52296 remain 38%)
c [simplification-12] maximum reduction of 8% = max (8%, 3%)
c [simplification-12] large reduction 8% >= 5% limit
c [simplification-12] next conflict interval 2734 = min (273491/100, 72912)
c [simplification-12] penalized conflict interval 2734 = 1 * 2734
c [simplification-12] hard conflict limit 286225 (soft 276225 + delta 10000)
c [simplification-12] new conflict limit 276225 (hard 286225)
c 
c [simplification-13] limit 276225 conflicts (hard 286225) hit after 280375 conflicts
c [quatres-11] found 18543 quaternary clauses 31% in total
c [quatres-11-1] removed 118 duplicate quaternary clauses
c [quatres-11-1] added 18 double-self-subsuming ternary resolvents
c [quatres-11-2] added 132 single-self-subsuming ternary resolvents
c [quatres-11-2] added 233 quaternary resolvents
c [ternres-11] limit 12707997 with penalty 0 = 0 + 0
c [ternres-11] 1 schedulable variables 0%
c [ternres-11] 0 ternary resolvents (0 bin, 0 trn)
c [ternres-11] fully completed ternary resolution
c [treelook-5] limit 635399 penalty 1 = 1 + 0 boost 1
c [treelook-5] scheduled 17210 literals 98%
c [treelook-5] scheduling used 453104 steps
c [treelook-5] scheduled completely
c [treelook-5] limit 635399 penalty 1 = 1 + 0 boost 1
c [treelook-5] used 663617 steps
c [treelook-5] 17185 literals remain 98%
c [treelook-5] 8458 variables remain to probed next time 96%
c [decomp-40] removed 1 variables
c [treelook-5] removed 2 variables, found 895 hbrs
c [unhide-11] limit 2541599 with penalty 0 = 0 + 0
c [unhide-11-13] 6 units, 42 failed, 2268 tauts, 0 hbrs, 22404 literals
c [transred-11] limit 2000000 with penalty 0 = 0 + 0
c [transred-11] removed 237 transitive binary clauses
c [transred-11] found 1 units
c [cce-6] limit of 15884996 steps penalty 2 = 2 + 0
c [cce-6-1] eliminated 4 clauses out of 57 (7%) of length 12
c [cce-6-1] eliminated 5 clauses out of 74 (7%) of length 11
c [cce-6-1] eliminated 13 clauses out of 169 (8%) of length 10
c [cce-6-1] eliminated 11 clauses out of 349 (3%) of length 9
c [cce-6-1] eliminated 26 clauses out of 564 (5%) of length 8
c [cce-6-1] eliminated 82 clauses out of 1354 (6%) of length 7
c [cce-6-1] eliminated 271 clauses out of 2644 (10%) of length 6
c [cce-6-1] eliminated 35 clauses out of 5352 (1%) of length 5
c [cce-6-1] incomplete large round (ATE)
c [cce-6-1] eliminated 447 large clauses in 15885233 steps
c [cce-6-1] allowing another 7942616 steps for small clauses
c [cce-6-1] scheduling 23059 clauses = 9740 binary + 13319 ternary
c [cce-6-1] tried to eliminate 318 small clauses 1%
c [cce-6-1] eliminated 2 binary clauses 0%
c [cce-6-1] eliminated 2 small clauses 0%
c [cce-6-1] eliminated 7 small clauses in 15885002 steps
c [cce-6-1] incomplete small round (ATE)
c [cce-6-1] eliminated 454 covered clauses in round 1
c [cce-6] eliminated 454 covered clauses in TOTAL during 1 rounds
c [cce-6] 454 < 1/100 * 51615 = 516 considered unsuccessful
c [elim-9] scheduling all variables this time
c [elim-9] scheduled 8746 variables 100%
c [elim-9] limit of 254159948 steps penalty 0 = 0 + 0
c [elim-9] rescheduling of touched variables disabled
c [elim-9-1] eliminated 337 variables 4% in round 1 in 17109313 steps
c [elim-9-1] backward subsumption/strengthening limit 17109300
c [elim-9-1-1] backward checking 1277 touched variables 15%
c [elim-9-1-1] fully completed backward checking in 1 rounds
c [elim-9-1] subsumed 4 and strengthened 4 clauses in 1869217 steps
c [elim-9-1] rescheduled 30 variables 0% by backward subsumption
c [elim-9-2] eliminated 12 variables 0% in round 2 in 590964 steps
c [elim-9-2] backward subsumption/strengthening limit 590900
c [elim-9-2-1] backward checking 68 touched variables 1%
c [elim-9-2-1] fully completed backward checking in 1 rounds
c [elim-9-2] subsumed 0 and strengthened 0 clauses in 100914 steps
c [elim-9] fully completed in 2 rounds
c [elim-9] transition to [ all 0 rem 0 ] state
c [elim-9] eliminated 349 = 4% variables out of 8746 scheduled
c [bca-10] limit of 10000000 steps and 99121 added (scaled 2)
c [bca-10] 2746 out of 16796 literals actually usable 16%
c [bca-10] added 26 blocked clauses in 73434 steps
c [sweep-12] limit 3812399 penalty 0 = 0 + 0
c [sweep-12-1] 2461 pos 44.1% + 3125 neg 55.9% = 5586 sched 66.5% ret 2811
c [sweep-12-1] 3820470 steps 167 queries 200.34 avg class size
c [sweep-12-1] 4074 decisions 157 SAT calls 60.52 avg env size
c [sweep-12-1] 3532 variables remain 42% (4865 retained 58%)
c [decomp-41] removed 40 variables
c [sweep-12-1] removed 40 vars (0 failed, 27 eqs, 24 impls)
c [sweep-12] removed 40 vars in TOTAL (1 rounds, 166 queries)
c [score-distribution-13] 3648 pos 43.65%, 4708 min 56.34%, 1 zero 0.01%
c [score-distribution-13] 2228 different 26.66% out of total 8357 variables
c [simplification-13] removed 414 variables 4.7% (8357 remain 18%)
c [simplification-13] removed 3192 irredundant clauses 6.1% (49090 remain 36%)
c [simplification-13] maximum reduction of 6% = max (5%, 6%)
c [simplification-13] large reduction 6% >= 5% limit
c [simplification-13] next conflict interval 2803 = min (280375/100, 72912)
c [simplification-13] penalized conflict interval 2803 = 1 * 2803
c [simplification-13] hard conflict limit 293178 (soft 283178 + delta 10000)
c [simplification-13] new conflict limit 283178 (hard 293178)
c 
c [simplification-14] limit 283178 conflicts (hard 293178) hit after 283179 conflicts
c [quatres-12] found 17592 quaternary clauses 31% in total
c [quatres-12-1] removed 21 duplicate quaternary clauses
c [quatres-12-1] added 2 double-self-subsuming ternary resolvents
c [quatres-12-2] added 39 single-self-subsuming ternary resolvents
c [quatres-12-2] added 134 quaternary resolvents
c [basicprobe-5] limit 63903928 penalty 0 = 0 + 0
c [basicprobe-5-0] 2333 sched 28%, 3 failed, 0 lifted, 1287 hbrs
c [decomp-43] removed 5 variables
c [basicprobe-5-1] 4849 sched 58%, 6 failed, 0 lifted, 1243 hbrs
c [decomp-44] removed 12 variables
c [basicprobe-5-2] 4823 sched 58%, 0 failed, 0 lifted, 51 hbrs
c [basicprobe-5-3] 4822 sched 58%, 0 failed, 0 lifted, 4 hbrs
c [basicprobe-5-4] 4822 sched 58%, 0 failed, 0 lifted, 3 hbrs
c [basicprobe-5-5] 4822 sched 58%, 0 failed, 0 lifted, 4 hbrs
c [basicprobe-5-6] 4822 sched 58%, 0 failed, 0 lifted, 1 hbrs
c [basicprobe-5-7] 4822 sched 58%, 0 failed, 0 lifted, 2 hbrs
c [basicprobe-5-8] 4822 sched 58%, 0 failed, 0 lifted, 2 hbrs
c [basicprobe-5-8] round limit 8 hit
c [basicprobe-5-8] 9 units = 9 failed (100%) + 0 lifted (0%)
c [basicprobe-5-8] removed 17 variables, found 2597 hbrs
c [bate-4] eliminated 22 asymmetric tautologies during probing
c [unhide-12] limit 2556157 with penalty 0 = 0 + 0
c [unhide-12-15] 0 units, 0 failed, 1226 tauts, 0 hbrs, 8998 literals
c [transred-12] limit 2000000 with penalty 0 = 0 + 0
c [transred-12] removed 315 transitive binary clauses
c [elim-10] scheduling all variables this time
c [elim-10] scheduled 8340 variables 100%
c [elim-10] limit of 255615715 steps penalty 0 = 0 + 0
c [elim-10] rescheduling of touched variables disabled
c [elim-10-1] eliminated 110 variables 1% in round 1 in 16509027 steps
c [elim-10-1] backward subsumption/strengthening limit 16509000
c [elim-10-1-1] backward checking 454 touched variables 5%
c [elim-10-1-1] fully completed backward checking in 1 rounds
c [elim-10-1] subsumed 10 and strengthened 14 clauses in 4978959 steps
c [elim-10-1] rescheduled 28 variables 0% by backward subsumption
c [elim-10-2] eliminated 12 variables 0% in round 2 in 5415042 steps
c [elim-10-2] backward subsumption/strengthening limit 5415000
c [elim-10-2-1] backward checking 32 touched variables 0%
c [elim-10-2-1] fully completed backward checking in 1 rounds
c [elim-10-2] subsumed 0 and strengthened 0 clauses in 1287670 steps
c [elim-10] fully completed in 2 rounds
c [elim-10] transition to [ all 0 rem 0 ] state
c [elim-10] eliminated 122 = 1% variables out of 8340 scheduled
c [bca-11] limit of 10000000 steps and 97528 added (scaled 2)
c [bca-11] 2667 out of 16438 literals actually usable 16%
c [bca-11] added 27 blocked clauses in 74862 steps
c [sweep-13] limit 3834235 penalty 0 = 0 + 0
c [sweep-13-1] 1571 pos 45.9% + 1852 neg 54.1% = 3423 sched 41.7% ret 4795
c [sweep-13-1] 3838193 steps 121 queries 124.33 avg class size
c [sweep-13-1] 2774 decisions 119 SAT calls 62.71 avg env size
c [sweep-13-1] 2571 variables remain 31% (5647 retained 69%)
c [decomp-51] removed 12 variables
c [sweep-13-1] removed 12 vars (0 failed, 12 eqs, 10 impls)
c [sweep-13] removed 12 vars in TOTAL (1 rounds, 120 queries)
c [score-distribution-14] 3377 pos 41.15%, 4828 min 58.83%, 1 zero 0.01%
c [score-distribution-14] 2090 different 25.47% out of total 8206 variables
c [simplification-14] removed 151 variables 1.8% (8206 remain 17%)
c [simplification-14] removed 799 irredundant clauses 1.6% (48288 remain 35%)
c [simplification-14] maximum reduction of 2% = max (2%, 2%)
c [simplification-14] geometric conflict interval increment 24304 = 72912 / 3
c [simplification-14] new conflict interval 97216
c [simplification-14] penalized conflict interval 97216 = 1 * 97216
c [simplification-14] hard conflict limit 429003 (soft 380395 + delta 48608)
c [simplification-14] new conflict limit 380395 (hard 429003)
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 -   75.5    8206    48287    313369   64971   8610 13726    7    42   19  16%    802  -12    8    8  105%
c -   80.9    8206    48287    349183   64928   8685 13730    7    26   19  28%    896  -20    7    8   88%
c -   87.5    8206    48287    389162   67566   8727 13732   10    34   20  29%    954   -6   10    8  122%
c 
c [simplification-15] limit 380395 conflicts (hard 429003) hit after 398727 conflicts
c [quatres-13] found 17818 quaternary clauses 27% in total
c [quatres-13-1] removed 11 duplicate quaternary clauses
c [quatres-13-1] added 1 double-self-subsuming ternary resolvents
c [quatres-13-2] added 59 single-self-subsuming ternary resolvents
c [quatres-13-2] added 128 quaternary resolvents
c [ternres-12] limit 9555214 with penalty 1 = 1 + 0
c [ternres-12] all 8206 free variables schedulable
c [ternres-12] 2527 ternary resolvents (88 bin, 2439 trn)
c [ternres-12] fully completed ternary resolution
c [card-5] limit 597200 penalty 4 = 4 + 0
c [card-5] found 168 at-most-one constraints of average size 3.1
c [card-5] no at-most-two constraint found
c [card-5] using previous limit 597200 for elimination
c [card-5] 168 out of 168 constraints (100%) meet size limits
c [card-5] no units found
c [card-5] no at-most-one constraints generated
c [gauss-7] limit 955521 penalty 2 = 2 + 0
c [gauss-7] extracted 1601 xors of average arity 3.0
c [gauss-7] connected 4745 occurrences of 628 variables (average 7.6)
c [gauss-7] limit 955521 penalty 2 = 2 + 0
c [gauss-7] fully completed
c [gauss-7] exported 0 unary, 0 binary and 1 ternary equations
c [decomp-52] removed 17 variables
c [simpleprobe-6] 5 schedulable variables 0%
c [simpleprobe-6] limit 76441715 penalty 0 = 0 + 0
c [decomp-53] removed 18 variables
c [simpleprobe-6] fully completed simple probing
c [simpleprobe-6] removed 18 variables, found 1162 hbrs, 7 units
c [transred-13] limit 2000000 with penalty 0 = 0 + 0
c [transred-13] removed 439 transitive binary clauses
c [elim-11] scheduling all variables this time
c [elim-11] scheduled 8171 variables 100%
c [elim-11] limit of 382208576 steps penalty 0 = 0 + 0
c [elim-11] rescheduling of touched variables disabled
c [elim-11-1] eliminated 30 variables 0% in round 1 in 16142989 steps
c [elim-11-1] backward subsumption/strengthening limit 16142900
c [elim-11-1-1] backward checking 185 touched variables 2%
c [elim-11-1-1] fully completed backward checking in 1 rounds
c [elim-11-1] subsumed 0 and strengthened 0 clauses in 1343214 steps
c [elim-11] fully completed in 1 rounds
c [elim-11] transition to [ all 0 rem 0 ] state
c [elim-11] eliminated 30 = 0% variables out of 8171 scheduled
c [elim-11] 30 < 1/100 * 8171 = 81 considered unsuccessful
c [bca-12] limit of 10000000 steps and 96828 added (scaled 2)
c [bca-12] 2791 out of 16284 literals actually usable 17%
c [bca-12] added 7 blocked clauses in 82463 steps
c [sweep-14] limit 5733128 penalty 0 = 0 + 0
c [sweep-14-1] 1232 pos 48.6% + 1302 neg 51.4% = 2534 sched 31.1% ret 5607
c [sweep-14-1] 5737970 steps 263 queries 114.86 avg class size
c [sweep-14-1] 5052 decisions 245 SAT calls 49.70 avg env size
c [sweep-14-1] 1307 variables remain 16% (6834 retained 84%)
c [decomp-54] removed 41 variables
c [sweep-14-1] removed 41 vars (0 failed, 43 eqs, 36 impls)
c [sweep-14] removed 41 vars in TOTAL (1 rounds, 262 queries)
c [score-distribution-15] 4215 pos 52.04%, 3884 min 47.95%, 1 zero 0.01%
c [score-distribution-15] 2461 different 30.38% out of total 8100 variables
c [simplification-15] removed 106 variables 1.3% (8100 remain 17%)
c [simplification-15] removed 361 irredundant clauses 0.7% (47926 remain 35%)
c [simplification-15] maximum reduction of 1% = max (1%, 1%)
c [simplification-15] geometric conflict interval increment 48608 = 97216 / 2
c [simplification-15] new conflict interval 145824
c [simplification-15] penalized conflict interval 145824 = 1 * 145824
c [simplification-15] hard conflict limit 617463 (soft 544551 + delta 72912)
c [simplification-15] new conflict limit 544551 (hard 617463)
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 -   96.0    8100    47926    431083   70853  10704 14246   10    39   20  26%    987    3   10    9  108%
c i  101.7    8099    47926    472422  110042  10725 14247    9    46   28  21%   1004    9   13    9  149%
c -  102.1    8099    47926    473362   76230  10726 14247   10    43   21  23%  -1468    6   12    9  140%
c i  105.6    8098    47925    497700   99430  10741 14248   10    40   29  26%  -1854    2   11    9  120%
c -  107.8    8098    47925    512091   78125  10745 14248    7    25   21  29%  -1609  -12    7    9   78%
c -  114.3    8098    47925    551319   79181  10767 14250   10    39   21  25%   -423    1    9    9   96%
c 
c [simplification-16] limit 544551 conflicts (hard 617463) hit after 573974 conflicts
c [quatres-14] found 18017 quaternary clauses 24% in total
c [quatres-14-1] removed 31 duplicate quaternary clauses
c [quatres-14-1] added 3 double-self-subsuming ternary resolvents
c [quatres-14-2] added 59 single-self-subsuming ternary resolvents
c [quatres-14-2] added 80 quaternary resolvents
c [ternres-13] limit 29119147 with penalty 0 = 0 + 0
c [ternres-13] all 8098 free variables schedulable
c [ternres-13] 2125 ternary resolvents (151 bin, 1974 trn)
c [ternres-13] fully completed ternary resolution
c [decomp-55] removed 9 variables
c [treelook-6] limit 2911914 penalty 0 = 0 + 0 boost 1
c [treelook-6] scheduled 15857 literals 98%
c [treelook-6] scheduling used 507837 steps
c [treelook-6] scheduled completely
c [treelook-6] limit 2911914 penalty 0 = 0 + 0 boost 1
c [treelook-6] used 2914443 steps
c [treelook-6] 14947 literals remain 92%
c [treelook-6] 7787 variables remain to probed next time 96%
c [decomp-56] removed 4 variables
c [treelook-6] removed 8 variables, found 6017 hbrs
c [unhide-13] limit 2911914 with penalty 1 = 1 + 0
c [unhide-13-17] 0 units, 3 failed, 3106 tauts, 0 hbrs, 59697 literals
c [transred-14] limit 2000000 with penalty 0 = 0 + 0
c [transred-14] removed 227 transitive binary clauses
c [bca-13] limit of 10000000 steps and 96569 added (scaled 2)
c [bca-13] 2942 out of 16166 literals actually usable 18%
c [bca-13] added 4 blocked clauses in 106375 steps
c [sweep-15] limit 8735744 penalty 0 = 0 + 0
c [sweep-15-1] 608 pos 46.6% + 696 neg 53.4% = 1304 sched 16.1% ret 6778
c [sweep-15-1] 8741957 steps 445 queries 37.66 avg class size
c [sweep-15-1] 7985 decisions 429 SAT calls 41.15 avg env size
c [sweep-15-1] 90 variables remain 1% (7992 retained 99%)
c [decomp-57] removed 73 variables
c [sweep-15-1] removed 73 vars (0 failed, 84 eqs, 50 impls)
c [sweep-15] removed 73 vars in TOTAL (1 rounds, 444 queries)
c [score-distribution-16] 2664 pos 33.26%, 5345 min 66.74%, 0 zero 0.00%
c [score-distribution-16] 1512 different 18.88% out of total 8009 variables
c [simplification-16] removed 89 variables 1.1% (8009 remain 17%)
c [simplification-16] removed 151 irredundant clauses 0.3% (47774 remain 35%)
c [simplification-16] maximum reduction of 1% = max (1%, 0%)
c [simplification-16] geometric conflict interval increment 72912 = 145824 / 2
c [simplification-16] new conflict interval 218736
c [simplification-16] penalized conflict interval 218736 = 1 * 218736
c [simplification-16] hard conflict limit 902078 (soft 792710 + delta 109368)
c [simplification-16] new conflict limit 792710 (hard 902078)
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 -  122.1    8009    47774    592621   83414  10769 18097    8    31   16  25%    254   -4    8    9   86%
c -  127.9    8009    47772    632293   85518  10782 18097    9    19   23  48%    603  -14   11    9  118%
c -  134.9    8009    47772    671802   86010  10800 18098   10    36   24  29%    794    2   13   10  139%
c -  142.1    8009    47772    714761   90407  10809 18099    9    25   24  36%    905   -8   11    9  116%
c -  149.0    8009    47772    755049   90950  10822 18100    9    40   24  24%    959    6    9    9   99%
c 
c [simplification-17] limit 792710 conflicts (hard 902078) hit after 793936 conflicts
c [quatres-15] found 18220 quaternary clauses 22% in total
c [quatres-15-1] removed 28 duplicate quaternary clauses
c [quatres-15-1] added 4 double-self-subsuming ternary resolvents
c [quatres-15-2] added 60 single-self-subsuming ternary resolvents
c [quatres-15-2] added 106 quaternary resolvents
c [ternres-14] limit 43857531 with penalty 0 = 0 + 0
c [ternres-14] all 8009 free variables schedulable
c [ternres-14] 1022 ternary resolvents (57 bin, 965 trn)
c [ternres-14] fully completed ternary resolution
c [gauss-8] limit 4385753 penalty 1 = 1 + 0
c [gauss-8] extracted 3446 xors of average arity 3.1
c [gauss-8] connected 10582 occurrences of 704 variables (average 15.0)
c [gauss-8] limit 4385753 penalty 1 = 1 + 0
c [gauss-8] fully completed
c [gauss-8] exported 0 unary, 0 binary and 1 ternary equations
c [decomp-58] removed 3 variables
c [basicprobe-6] limit 219287656 penalty 0 = 0 + 0
c [basicprobe-6-0] 4606 sched 58%, 5 failed, 0 lifted, 1252 hbrs
c [decomp-59] removed 14 variables
c [basicprobe-6-1] 4587 sched 57%, 0 failed, 0 lifted, 18 hbrs
c [basicprobe-6-2] 4587 sched 57%, 0 failed, 0 lifted, 3 hbrs
c [basicprobe-6-3] 4587 sched 57%, 0 failed, 0 lifted, 1 hbrs
c [basicprobe-6-4] 4587 sched 57%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-6-4] fully completed probing
c [basicprobe-6-4] 5 units = 5 failed (100%) + 0 lifted (0%)
c [basicprobe-6-4] removed 14 variables, found 1274 hbrs
c [bate-5] eliminated 11 asymmetric tautologies during probing
c [unhide-14] limit 8771506 with penalty 0 = 0 + 0
c [unhide-14-22] 0 units, 0 failed, 2381 tauts, 0 hbrs, 78639 literals
c [transred-15] limit 2000000 with penalty 0 = 0 + 0
c [transred-15] removed 247 transitive binary clauses
c [block-6] scheduling all variables this time
c [block-6] scheduled 7992 variables 100%
c [block-6] limit of 27410957 steps penalty 4 = 4 + 0
c [block-6] fully completed
c [block-6] transition to [ all 0 rem 0 ] state
c [block-6] eliminated 96 blocked clauses
c [block-6] 96 < 1/100 * 47616 = 476 considered unsuccessful
c [cce-7] limit of 27410957 steps penalty 3 = 3 + 0
c [cce-7-1] eliminated 4 clauses out of 13 (31%) of length 17
c [cce-7-1] eliminated 14 clauses out of 84 (17%) of length 13
c [cce-7-1] eliminated 8 clauses out of 52 (15%) of length 12
c [cce-7-1] eliminated 4 clauses out of 61 (7%) of length 11
c [cce-7-1] eliminated 30 clauses out of 179 (17%) of length 10
c [cce-7-1] eliminated 34 clauses out of 343 (10%) of length 9
c [cce-7-1] eliminated 27 clauses out of 508 (5%) of length 8
c [cce-7-1] eliminated 73 clauses out of 1185 (6%) of length 7
c [cce-7-1] eliminated 226 clauses out of 2311 (10%) of length 6
c [cce-7-1] eliminated 290 clauses out of 5038 (6%) of length 5
c [cce-7-1] incomplete large round (ACCE)
c [cce-7-1] eliminated 710 large clauses in 27410970 steps
c [cce-7-1] allowing another 13705485 steps for small clauses
c [cce-7-1] scheduling 20693 clauses = 8886 binary + 11807 ternary
c [cce-7-1] tried to eliminate 9169 small clauses 44%
c [cce-7-1] eliminated 238 binary clauses 3%
c [cce-7-1] eliminated 624 ternary clauses 5%
c [cce-7-1] eliminated 862 small clauses 4%
c [cce-7-1] eliminated 862 small clauses in 27410993 steps
c [cce-7-1] incomplete small round (ACCE)
c [cce-7-1] eliminated 1572 covered clauses in round 1
c [cce-7] eliminated 1572 covered clauses in TOTAL during 1 rounds
c [elim-12] scheduling all variables this time
c [elim-12] scheduled 7985 variables 100%
c [elim-12] limit of 400000000 steps penalty 1 = 1 + 0
c [elim-12] rescheduling of touched variables disabled
c [elim-12-1] eliminated 269 variables 3% in round 1 in 14798027 steps
c [elim-12-1] backward subsumption/strengthening limit 14798000
c [elim-12-1-1] backward checking 1370 touched variables 17%
c [elim-12-1-1] fully completed backward checking in 1 rounds
c [elim-12-1] subsumed 4 and strengthened 10 clauses in 3886718 steps
c [elim-12-1] rescheduled 47 variables 1% by backward subsumption
c [elim-12-2] eliminated 5 variables 0% in round 2 in 4611849 steps
c [elim-12-2] backward subsumption/strengthening limit 4611800
c [elim-12-2-1] backward checking 36 touched variables 0%
c [elim-12-2-1] fully completed backward checking in 1 rounds
c [elim-12-2] subsumed 0 and strengthened 0 clauses in 1145008 steps
c [elim-12] fully completed in 2 rounds
c [elim-12] transition to [ all 0 rem 0 ] state
c [elim-12] eliminated 274 = 3% variables out of 7985 scheduled
c [bca-14] limit of 10000000 steps and 91231 added (scaled 2)
c [bca-14] 2883 out of 15424 literals actually usable 19%
c [bca-14] added 27 blocked clauses in 130350 steps
c [sweep-16] limit 13157259 penalty 0 = 0 + 0
c [sweep-16-1] 31 pos 34.8% + 58 neg 65.2% = 89 sched 1.2% ret 7622
c [sweep-16-1] 868599 steps 51 queries 9.00 avg class size
c [sweep-16-1] 762 decisions 47 SAT calls 33.38 avg env size
c [sweep-16-1] fully completed sweeping round
c [decomp-63] removed 8 variables
c [sweep-16-1] removed 8 vars (0 failed, 4 eqs, 4 impls)
c [sweep-16-2] 3456 pos 44.9% + 4247 neg 55.1% = 7703 sched 100.0% ret 0
c [sweep-16-2] 12312062 steps 275 queries 116.08 avg class size
c [sweep-16-2] 7182 decisions 270 SAT calls 70.98 avg env size
c [sweep-16-2] 2857 variables remain 37% (4845 retained 63%)
c [decomp-64] removed 19 variables
c [sweep-16-2] removed 19 vars (0 failed, 15 eqs, 11 impls)
c [sweep-16] removed 27 vars in TOTAL (2 rounds, 324 queries)
c [score-distribution-17] 3230 pos 42.04%, 4454 min 57.96%, 0 zero 0.00%
c [score-distribution-17] 1742 different 22.67% out of total 7684 variables
c [simplification-17] removed 325 variables 4.1% (7684 remain 16%)
c [simplification-17] removed 2649 irredundant clauses 5.5% (45123 remain 33%)
c [simplification-17] maximum reduction of 6% = max (4%, 6%)
c [simplification-17] large reduction 6% >= 5% limit
c [simplification-17] next conflict interval 7939 = min (793936/100, 218736)
c [simplification-17] penalized conflict interval 7939 = 1 * 7939
c [simplification-17] hard conflict limit 811875 (soft 801875 + delta 10000)
c [simplification-17] new conflict limit 801875 (hard 811875)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c -  162.4    7684    45122    798512   90232  10830 14724    9    57   16  16%    991   22    7   10   75%
c 
c [simplification-18] limit 801875 conflicts (hard 811875) hit after 801878 conflicts
c [quatres-16] found 17607 quaternary clauses 22% in total
c [quatres-16-1] removed 18 duplicate quaternary clauses
c [quatres-16-1] added 1 double-self-subsuming ternary resolvents
c [quatres-16-2] added 44 single-self-subsuming ternary resolvents
c [quatres-16-2] added 158 quaternary resolvents
c [ternres-15] limit 44225969 with penalty 0 = 0 + 0
c [ternres-15] all 7684 free variables schedulable
c [ternres-15] 939 ternary resolvents (79 bin, 860 trn)
c [ternres-15] fully completed ternary resolution
c [gauss-9] limit 8845193 penalty 0 = 0 + 0
c [gauss-9] extracted 3322 xors of average arity 3.1
c [gauss-9] connected 10230 occurrences of 667 variables (average 15.3)
c [gauss-9] limit 8845193 penalty 0 = 0 + 0
c [gauss-9] fully completed
c [gauss-9] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-65] removed 1 variables
c [simpleprobe-7] all 7683 free variables schedulable
c [simpleprobe-7] limit 176903879 penalty 0 = 0 + 0
c [decomp-66] removed 16 variables
c [simpleprobe-7] fully completed simple probing
c [simpleprobe-7] removed 16 variables, found 1939 hbrs, 1 units
c [transred-16] limit 2000000 with penalty 0 = 0 + 0
c [transred-16] removed 671 transitive binary clauses
c [elim-13] scheduling all variables this time
c [elim-13] scheduled 7667 variables 100%
c [elim-13] almost no limit of 100000000000 steps
c [elim-13] rescheduling of touched variables disabled
c [elim-13-1] eliminated 63 variables 1% in round 1 in 14780561 steps
c [elim-13-1] backward subsumption/strengthening limit 14780500
c [elim-13-1-1] backward checking 262 touched variables 3%
c [elim-13-1-1] fully completed backward checking in 1 rounds
c [elim-13-1] subsumed 1 and strengthened 2 clauses in 1297282 steps
c [elim-13-1] rescheduled 13 variables 0% by backward subsumption
c [elim-13-2] eliminated 2 variables 0% in round 2 in 344269 steps
c [elim-13-2] backward subsumption/strengthening limit 344200
c [elim-13-2-1] backward checking 17 touched variables 0%
c [elim-13-2-1] fully completed backward checking in 1 rounds
c [elim-13-2] subsumed 1 and strengthened 3 clauses in 25742 steps
c [elim-13-2] rescheduled 13 variables 0% by backward subsumption
c [elim-13-3] eliminated 3 variables 0% in round 3 in 6712 steps
c [elim-13-3] backward subsumption/strengthening limit 6700
c [elim-13-3-1] backward checking 9 touched variables 0%
c [elim-13-3-1] incomplete backward checking 0 remain 0%
c [elim-13-3] subsumed 0 and strengthened 0 clauses in 6701 steps
c [elim-13] fully completed in 3 rounds
c [elim-13] transition to [ all 0 rem 0 ] state
c [elim-13] eliminated 68 = 1% variables out of 7667 scheduled
c [elim-13] 68 < 1/100 * 7667 = 76 considered unsuccessful
c [bca-15] limit of 10000000 steps and 90247 added (scaled 2)
c [bca-15] 2746 out of 15200 literals actually usable 18%
c [bca-15] added 3 blocked clauses in 99266 steps
c [sweep-17] limit 13267790 penalty 0 = 0 + 0
c [sweep-17-1] 1272 pos 45.7% + 1510 neg 54.3% = 2782 sched 36.6% ret 4817
c [sweep-17-1] 12761185 steps 638 queries 29.63 avg class size
c [sweep-17-1] 12699 decisions 635 SAT calls 45.19 avg env size
c [sweep-17-1] fully completed sweeping round
c [decomp-67] removed 65 variables
c [sweep-17-1] removed 65 vars (0 failed, 69 eqs, 45 impls)
c [sweep-17-2] 3379 pos 44.9% + 4155 neg 55.1% = 7534 sched 100.0% ret 0
c [sweep-17-2] 514963 steps 25 queries 1182.60 avg class size
c [sweep-17-2] 748 decisions 24 SAT calls 76.88 avg env size
c [sweep-17-2] 7236 variables remain 96% (298 retained 4%)
c [sweep-17-2] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-17] removed 65 vars in TOTAL (2 rounds, 661 queries)
c [score-distribution-18] 3408 pos 45.23%, 4126 min 54.77%, 0 zero 0.00%
c [score-distribution-18] 1889 different 25.07% out of total 7534 variables
c [simplification-18] removed 150 variables 2.0% (7534 remain 16%)
c [simplification-18] removed 507 irredundant clauses 1.1% (44615 remain 32%)
c [simplification-18] maximum reduction of 2% = max (2%, 1%)
c [simplification-18] geometric conflict interval increment 72912 = 218736 / 3
c [simplification-18] new conflict interval 291648
c [simplification-18] penalized conflict interval 291648 = 1 * 291648
c [simplification-18] hard conflict limit 1239350 (soft 1093526 + delta 145824)
c [simplification-18] new conflict limit 1093526 (hard 1239350)
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 -  169.4    7534    44615    849423   93988  11470 15982    8     9   16  90%   1009  -15    9    9   97%
c i  171.3    7533    44615    867754  106598  11528 15997    7     8   20  90%   1012  -13    5    9   57%
c i  173.2    5837    44615    880932  119006  11539 16000    9    35   30  26%  -3789   12    9    9  103%
c -  175.4    5837    44614    896141   96626  11548 16002    8    40   24  21%  -2958   11    8    9   91%
c i  177.9    5836    44614    913808  112535  11559 16002    8    32   29  25%  -2017    2   10    8  117%
c -  182.4    5836    44612    940841   99243  11580 16008    8    34   24  24%  -1335    1    8    8   96%
c -  192.0    5836    44612    985997  100158  11619 16016    9    42   24  21%   -160    8    9    9  104%
c -  204.9    5836    44612   1033217  100663  11658 16021   10    39   24  25%    448    2    8    9   88%
c -  216.1    5836    44612   1084561  107378  11669 16025   11    38   24  28%    761   -1   11    9  119%
c 
c [simplification-19] limit 1093526 conflicts (hard 1239350) hit after 1095193 conflicts
c [quatres-17] found 9746 quaternary clauses 15% in total
c [quatres-17-1] removed 4 duplicate quaternary clauses
c [quatres-17-1] added 2 double-self-subsuming ternary resolvents
c [quatres-17-2] added 88 single-self-subsuming ternary resolvents
c [quatres-17-2] added 575 quaternary resolvents
c [ternres-16] limit 66853268 with penalty 0 = 0 + 0
c [ternres-16] all 5836 free variables schedulable
c [ternres-16] 326 ternary resolvents (42 bin, 284 trn)
c [ternres-16] fully completed ternary resolution
c [decomp-69] removed 2635 variables
c [treelook-7] limit 6685326 penalty 0 = 0 + 0 boost 1
c [treelook-7] scheduled 9571 literals 98%
c [treelook-7] scheduling used 426959 steps
c [treelook-7] scheduled completely
c [treelook-7] limit 6685326 penalty 0 = 0 + 0 boost 1
c [treelook-7] used 6696749 steps
c [treelook-7] 7546 literals remain 77%
c [treelook-7] 4537 variables remain to probed next time 93%
c [decomp-70] removed 69 variables
c [treelook-7] removed 96 variables, found 11742 hbrs
c [unhide-15] limit 6685326 with penalty 1 = 1 + 0
c [unhide-15-27] 0 units, 1 failed, 8164 tauts, 0 hbrs, 63629 literals
c [transred-17] limit 2000000 with penalty 0 = 0 + 0
c [transred-17] removed 987 transitive binary clauses
c [cce-8] boosting limit by 10
c [cce-8] limit of 835665860 steps penalty 2 = 2 + 0
c [cce-8-1] eliminated 3 clauses out of 14 (21%) of length 12
c [cce-8-1] eliminated 7 clauses out of 37 (19%) of length 11
c [cce-8-1] eliminated 8 clauses out of 46 (17%) of length 10
c [cce-8-1] eliminated 13 clauses out of 71 (18%) of length 9
c [cce-8-1] eliminated 23 clauses out of 241 (10%) of length 8
c [cce-8-1] eliminated 32 clauses out of 418 (8%) of length 7
c [cce-8-1] eliminated 111 clauses out of 877 (13%) of length 6
c [cce-8-1] eliminated 454 clauses out of 2050 (22%) of length 5
c [cce-8-1] eliminated 1128 clauses out of 6133 (18%) of length 4
c [cce-8-1] completed large round (ATE)
c [cce-8-1] eliminated 1779 large clauses in 10892184 steps
c [cce-8-1] allowing another 5446092 steps for small clauses
c [cce-8-1] scheduling 12201 clauses = 5250 binary + 6951 ternary
c [cce-8-1] tried to eliminate 12201 small clauses 100%
c [cce-8-1] eliminated 189 binary clauses 4%
c [cce-8-1] eliminated 366 ternary clauses 5%
c [cce-8-1] eliminated 555 small clauses 5%
c [cce-8-1] eliminated 555 small clauses in 14677852 steps
c [cce-8-1] completed small round (ATE)
c [cce-8-1] completed small and large (ATE)
c [cce-8-1] eliminated 2334 covered clauses in round 1
c [cce-8-2] completed large round (ATE)
c [cce-8-2] allowing another 4106040 steps for small clauses
c [cce-8-2] scheduling 11646 clauses = 5061 binary + 6585 ternary
c [cce-8-2] tried to eliminate 11646 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 2334 covered clauses in TOTAL during 2 rounds
c [bca-16] limit of 10000000 steps and 49302 added (scaled 2)
c [bca-16] 1914 out of 9606 literals actually usable 20%
c [bca-16] added 1 blocked clauses in 106851 steps
c [sweep-18] almost no limit of 4000000000 steps
c [sweep-18-1] 2170 pos 47.2% + 2431 neg 52.8% = 4601 sched 95.8% ret 201
c [sweep-18-1] 18894140 steps 647 queries 31.93 avg class size
c [sweep-18-1] 9861 decisions 555 SAT calls 57.45 avg env size
c [sweep-18-1] fully completed sweeping round
c [decomp-71] removed 177 variables
c [sweep-18-1] removed 177 vars (0 failed, 174 eqs, 153 impls)
c [sweep-18-2] 2177 pos 47.1% + 2448 neg 52.9% = 4625 sched 100.0% ret 0
c [sweep-18-2] 15747007 steps 527 queries 39.83 avg class size
c [sweep-18-2] 9423 decisions 505 SAT calls 56.49 avg env size
c [sweep-18-2] fully completed sweeping round
c [decomp-72] removed 56 variables
c [sweep-18-2] removed 56 vars (0 failed, 66 eqs, 56 impls)
c [sweep-18-3] 2153 pos 47.1% + 2416 neg 52.9% = 4569 sched 100.0% ret 0
c [sweep-18-3] 15796700 steps 501 queries 30.35 avg class size
c [sweep-18-3] 9069 decisions 481 SAT calls 57.32 avg env size
c [sweep-18-3] fully completed sweeping round
c [decomp-73] removed 26 variables
c [sweep-18-3] removed 26 vars (0 failed, 43 eqs, 25 impls)
c [sweep-18] removed 259 vars in TOTAL (3 rounds, 1672 queries)
c [score-distribution-19] 2968 pos 65.33%, 1575 min 34.67%, 0 zero 0.00%
c [score-distribution-19] 1670 different 36.76% out of total 4543 variables
c [simplification-19] removed 1293 variables 22.2% (4543 remain 10%)
c [simplification-19] removed 20757 irredundant clauses 46.5% (23855 remain 17%)
c [simplification-19] maximum reduction of 47% = max (22%, 47%)
c [simplification-19] large reduction 47% >= 5% limit
c [simplification-19] next conflict interval 10951 = min (1095193/100, 291648)
c [simplification-19] penalized conflict interval 10951 = 1 * 10951
c [simplification-19] hard conflict limit 1116144 (soft 1106144 + delta 10000)
c [simplification-19] new conflict limit 1106144 (hard 1116144)
c 
c [simplification-20] limit 1106144 conflicts (hard 1116144) hit after 1109416 conflicts
c [quatres-18] found 11159 quaternary clauses 16% in total
c [quatres-18-1] removed 127 duplicate quaternary clauses
c [quatres-18-1] added 7 double-self-subsuming ternary resolvents
c [quatres-18-2] added 204 single-self-subsuming ternary resolvents
c [quatres-18-2] added 312 quaternary resolvents
c [ternres-17] limit 67999700 with penalty 0 = 0 + 0
c [ternres-17] all 4543 free variables schedulable
c [ternres-17] 2520 ternary resolvents (96 bin, 2424 trn)
c [ternres-17] fully completed ternary resolution
c [gauss-10] limit 6799970 penalty 1 = 1 + 0
c [gauss-10] extracted 1995 xors of average arity 3.1
c [gauss-10] connected 6162 occurrences of 437 variables (average 14.1)
c [gauss-10] limit 6799970 penalty 1 = 1 + 0
c [gauss-10] fully completed
c [decomp-74] removed 9 variables
c [gauss-10] exported 1 unary, 0 binary and 1 ternary equations
c [basicprobe-7] limit 339998501 penalty 0 = 0 + 0
c [basicprobe-7-0] 2318 sched 51%, 21 failed, 0 lifted, 695 hbrs
c [decomp-76] removed 30 variables
c [basicprobe-7-1] 2281 sched 51%, 0 failed, 0 lifted, 91 hbrs
c [decomp-77] removed 2 variables
c [basicprobe-7-2] 2276 sched 51%, 0 failed, 0 lifted, 83 hbrs
c [basicprobe-7-3] 2278 sched 51%, 0 failed, 0 lifted, 9 hbrs
c [basicprobe-7-4] 2278 sched 51%, 0 failed, 0 lifted, 2 hbrs
c [basicprobe-7-5] 2278 sched 51%, 0 failed, 0 lifted, 2 hbrs
c [basicprobe-7-6] 2278 sched 51%, 0 failed, 0 lifted, 2 hbrs
c [basicprobe-7-7] 2278 sched 51%, 0 failed, 0 lifted, 2 hbrs
c [basicprobe-7-8] 2278 sched 51%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-7-8] round limit 8 hit
c [basicprobe-7-8] 21 units = 21 failed (100%) + 0 lifted (0%)
c [basicprobe-7-8] removed 32 variables, found 886 hbrs
c [bate-6] eliminated 29 asymmetric tautologies during probing
c [unhide-16] limit 13599940 with penalty 0 = 0 + 0
c [unhide-16-35] 0 units, 0 failed, 3638 tauts, 0 hbrs, 49906 literals
c [transred-18] limit 2000000 with penalty 0 = 0 + 0
c [transred-18] removed 599 transitive binary clauses
c [cce-9] limit of 169999250 steps penalty 1 = 1 + 0
c [cce-9-1] eliminated 1 clauses out of 23 (4%) of length 11
c [cce-9-1] eliminated 3 clauses out of 31 (10%) of length 10
c [cce-9-1] eliminated 18 clauses out of 58 (31%) of length 9
c [cce-9-1] eliminated 47 clauses out of 213 (22%) of length 8
c [cce-9-1] eliminated 45 clauses out of 383 (12%) of length 7
c [cce-9-1] eliminated 93 clauses out of 669 (14%) of length 6
c [cce-9-1] eliminated 216 clauses out of 1516 (14%) of length 5
c [cce-9-1] eliminated 463 clauses out of 4813 (10%) of length 4
c [cce-9-1] completed large round (ACCE)
c [cce-9-1] eliminated 886 large clauses in 12402995 steps
c [cce-9-1] allowing another 6201497 steps for small clauses
c [cce-9-1] scheduling 9077 clauses = 4792 binary + 4285 ternary
c [cce-9-1] tried to eliminate 9077 small clauses 100%
c [cce-9-1] eliminated 710 binary clauses 15%
c [cce-9-1] eliminated 690 ternary clauses 16%
c [cce-9-1] eliminated 1400 small clauses 15%
c [cce-9-1] eliminated 1400 small clauses in 13915261 steps
c [cce-9-1] completed small round (ACCE)
c [cce-9-1] completed small and large (ACCE)
c [cce-9-1] eliminated 2286 covered clauses in round 1
c [cce-9-2] eliminated 1 clauses out of 28 (4%) of length 10
c [cce-9-2] eliminated 2 clauses out of 40 (5%) of length 9
c [cce-9-2] eliminated 27 clauses out of 166 (16%) of length 8
c [cce-9-2] eliminated 25 clauses out of 338 (7%) of length 7
c [cce-9-2] eliminated 23 clauses out of 576 (4%) of length 6
c [cce-9-2] eliminated 36 clauses out of 1300 (3%) of length 5
c [cce-9-2] eliminated 94 clauses out of 4350 (2%) of length 4
c [cce-9-2] completed large round (ACCE)
c [cce-9-2] eliminated 208 large clauses in 10845106 steps
c [cce-9-2] allowing another 5422553 steps for small clauses
c [cce-9-2] scheduling 7683 clauses = 4082 binary + 3601 ternary
c [cce-9-2] tried to eliminate 7683 small clauses 100%
c [cce-9-2] eliminated 105 binary clauses 3%
c [cce-9-2] eliminated 92 ternary clauses 3%
c [cce-9-2] eliminated 197 small clauses 3%
c [cce-9-2] eliminated 197 small clauses in 11731340 steps
c [cce-9-2] completed small round (ACCE)
c [cce-9-2] eliminated 405 covered clauses in round 2
c [cce-9-3] eliminated 4 clauses out of 313 (1%) of length 7
c [cce-9-3] eliminated 2 clauses out of 553 (0%) of length 6
c [cce-9-3] eliminated 12 clauses out of 1264 (1%) of length 5
c [cce-9-3] eliminated 19 clauses out of 4256 (0%) of length 4
c [cce-9-3] completed large round (ACCE)
c [cce-9-3] eliminated 37 large clauses in 10764257 steps
c [cce-9-3] allowing another 5382128 steps for small clauses
c [cce-9-3] scheduling 7488 clauses = 3977 binary + 3511 ternary
c [cce-9-3] tried to eliminate 7488 small clauses 100%
c [cce-9-3] eliminated 13 binary clauses 0%
c [cce-9-3] eliminated 27 ternary clauses 1%
c [cce-9-3] eliminated 40 small clauses 1%
c [cce-9-3] eliminated 40 small clauses in 11529269 steps
c [cce-9-3] completed small round (ACCE)
c [cce-9-3] eliminated 77 covered clauses in round 3
c [cce-9] eliminated 2768 covered clauses in TOTAL during 3 rounds
c [elim-14] scheduling all variables this time
c [elim-14] scheduled 4502 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 1268 variables 28% in round 1 in 3197560 steps
c [elim-14-1] backward subsumption/strengthening limit 3197500
c [elim-14-1-1] backward checking 1867 touched variables 41%
c [elim-14-1-1] fully completed backward checking in 1 rounds
c [elim-14-1] subsumed 6 and strengthened 39 clauses in 342165 steps
c [elim-14-1] rescheduled 106 variables 2% by backward subsumption
c [elim-14-2] eliminated 10 variables 0% in round 2 in 261138 steps
c [elim-14-2] backward subsumption/strengthening limit 261100
c [elim-14-2-1] backward checking 81 touched variables 2%
c [elim-14-2-1] fully completed backward checking in 1 rounds
c [elim-14-2] subsumed 0 and strengthened 2 clauses in 64916 steps
c [elim-14-2] rescheduled 10 variables 0% by backward subsumption
c [elim-14-3] no variable eliminated in round 3 in 46202 steps
c [elim-14] fully completed in 3 rounds
c [elim-14] transition to [ all 0 rem 0 ] state
c [elim-14] eliminated 1278 = 28% variables out of 4502 scheduled
c [bca-17] limit of 10000000 steps and 36667 added (scaled 2)
c [bca-17] 927 out of 6450 literals actually usable 14%
c [bca-17] added 6 blocked clauses in 108830 steps
c [sweep-19] limit 20399910 penalty 0 = 0 + 0
c [sweep-19-1] 1449 pos 44.9% + 1775 neg 55.1% = 3224 sched 100.0% ret 0
c [sweep-19-1] 15135878 steps 347 queries 28.04 avg class size
c [sweep-19-1] 8123 decisions 343 SAT calls 65.93 avg env size
c [sweep-19-1] fully completed sweeping round
c [decomp-84] removed 20 variables
c [sweep-19-1] removed 20 vars (0 failed, 19 eqs, 8 impls)
c [sweep-19-2] 1440 pos 44.9% + 1764 neg 55.1% = 3204 sched 100.0% ret 0
c [sweep-19-2] 5271429 steps 56 queries 129.66 avg class size
c [sweep-19-2] 2154 decisions 55 SAT calls 126.27 avg env size
c [sweep-19-2] 1848 variables remain 58% (1356 retained 42%)
c [decomp-85] removed 2 variables
c [sweep-19-2] removed 2 vars (0 failed, 2 eqs, 3 impls)
c [sweep-19] removed 22 vars in TOTAL (2 rounds, 401 queries)
c [score-distribution-20] 2136 pos 66.71%, 1066 min 33.29%, 0 zero 0.00%
c [score-distribution-20] 1319 different 41.19% out of total 3202 variables
c [simplification-20] removed 1341 variables 29.5% (3202 remain 7%)
c [simplification-20] removed 6015 irredundant clauses 25.2% (17840 remain 13%)
c [simplification-20] maximum reduction of 30% = max (30%, 25%)
c [simplification-20] large reduction 30% >= 5% limit
c [simplification-20] next conflict interval 11094 = min (1109416/100, 291648)
c [simplification-20] penalized conflict interval 11094 = 1 * 11094
c [simplification-20] hard conflict limit 1130510 (soft 1120510 + delta 10000)
c [simplification-20] new conflict limit 1120510 (hard 1130510)
c 
c [simplification-21] limit 1120510 conflicts (hard 1130510) hit after 1121857 conflicts
c [quatres-19] found 9257 quaternary clauses 14% in total
c [quatres-19-1] removed 29 duplicate quaternary clauses
c [quatres-19-1] added 1 double-self-subsuming ternary resolvents
c [quatres-19-2] added 38 single-self-subsuming ternary resolvents
c [quatres-19-2] added 186 quaternary resolvents
c [ternres-18] limit 69130275 with penalty 0 = 0 + 0
c [ternres-18] all 3202 free variables schedulable
c [ternres-18] 749 ternary resolvents (35 bin, 714 trn)
c [ternres-18] fully completed ternary resolution
c [card-6] limit 2160321 penalty 4 = 4 + 0
c [card-6] found 163 at-most-one constraints of average size 3.0
c [card-6] found 41 at-most-two constraints of average size 4.0
c [card-6] using previous limit 2160321 for elimination
c [card-6] 203 out of 204 constraints (100%) meet size limits
c [card-6] no units found
c [card-6] no at-most-one constraints generated
c [gauss-11] limit 13826055 penalty 0 = 0 + 0
c [gauss-11] extracted 1681 xors of average arity 3.1
c [gauss-11] connected 5283 occurrences of 353 variables (average 15.0)
c [gauss-11] limit 13826055 penalty 0 = 0 + 0
c [gauss-11] fully completed
c [gauss-11] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-86] removed 2 variables
c [simpleprobe-8] all 3200 free variables schedulable
c [simpleprobe-8] limit 200000000 penalty 0 = 0 + 0
c [decomp-87] removed 5 variables
c [simpleprobe-8] fully completed simple probing
c [simpleprobe-8] removed 5 variables, found 1165 hbrs, 1 units
c [transred-19] limit 2000000 with penalty 0 = 0 + 0
c [transred-19] removed 557 transitive binary clauses
c [cce-10] limit of 345651377 steps penalty 0 = 0 + 0
c [cce-10-1] eliminated 1 clauses out of 1 (100%) of length 17
c [cce-10-1] eliminated 1 clauses out of 1 (100%) of length 16
c [cce-10-1] eliminated 2 clauses out of 3 (67%) of length 15
c [cce-10-1] eliminated 2 clauses out of 8 (25%) of length 12
c [cce-10-1] eliminated 4 clauses out of 34 (12%) of length 11
c [cce-10-1] eliminated 5 clauses out of 37 (14%) of length 10
c [cce-10-1] eliminated 6 clauses out of 71 (8%) of length 9
c [cce-10-1] eliminated 9 clauses out of 172 (5%) of length 8
c [cce-10-1] eliminated 19 clauses out of 385 (5%) of length 7
c [cce-10-1] eliminated 66 clauses out of 778 (8%) of length 6
c [cce-10-1] eliminated 80 clauses out of 1538 (5%) of length 5
c [cce-10-1] eliminated 148 clauses out of 4304 (3%) of length 4
c [cce-10-1] completed large round (ATE)
c [cce-10-1] eliminated 343 large clauses in 5268707 steps
c [cce-10-1] allowing another 2634353 steps for small clauses
c [cce-10-1] scheduling 5772 clauses = 2994 binary + 2778 ternary
c [cce-10-1] tried to eliminate 5772 small clauses 100%
c [cce-10-1] eliminated 15 binary clauses 1%
c [cce-10-1] eliminated 39 ternary clauses 1%
c [cce-10-1] eliminated 54 small clauses 1%
c [cce-10-1] eliminated 54 small clauses in 5385241 steps
c [cce-10-1] completed small round (ATE)
c [cce-10-1] eliminated 397 covered clauses in round 1
c [cce-10-2] completed large round (ATE)
c [cce-10-2] allowing another 2478695 steps for small clauses
c [cce-10-2] scheduling 5718 clauses = 2979 binary + 2739 ternary
c [cce-10-2] tried to eliminate 5718 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 397 covered clauses in TOTAL during 2 rounds
c [elim-15] scheduling all variables this time
c [elim-15] scheduled 3195 variables 100%
c [elim-15] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-15] rescheduling of touched variables disabled
c [elim-15-1] eliminated 78 variables 2% in round 1 in 2800010 steps
c [elim-15-1] backward subsumption/strengthening limit 2800000
c [elim-15-1-1] backward checking 462 touched variables 14%
c [elim-15-1-1] fully completed backward checking in 1 rounds
c [elim-15-1] subsumed 0 and strengthened 22 clauses in 134802 steps
c [elim-15-1] rescheduled 44 variables 1% by backward subsumption
c [elim-15-2] eliminated 3 variables 0% in round 2 in 199751 steps
c [elim-15-2] backward subsumption/strengthening limit 199700
c [elim-15-2-1] backward checking 13 touched variables 0%
c [elim-15-2-1] fully completed backward checking in 1 rounds
c [elim-15-2] subsumed 9 and strengthened 2 clauses in 14323 steps
c [elim-15-2] rescheduled 13 variables 0% by backward subsumption
c [elim-15-3] eliminated 2 variables 0% in round 3 in 30209 steps
c [elim-15-3] backward subsumption/strengthening limit 30200
c [elim-15-3-1] backward checking 25 touched variables 1%
c [elim-15-3-1] fully completed backward checking in 1 rounds
c [elim-15-3] subsumed 0 and strengthened 0 clauses in 16059 steps
c [elim-15] fully completed in 3 rounds
c [elim-15] transition to [ all 0 rem 0 ] state
c [elim-15] eliminated 83 = 3% variables out of 3195 scheduled
c [bca-18] limit of 10000000 steps and 35168 added (scaled 2)
c [bca-18] 795 out of 6226 literals actually usable 13%
c [bca-18] added 9 blocked clauses in 121036 steps
c [sweep-20] limit 20739082 penalty 0 = 0 + 0
c [sweep-20-1] 788 pos 44.2% + 995 neg 55.8% = 1783 sched 57.3% ret 1329
c [sweep-20-1] 9729785 steps 281 queries 28.96 avg class size
c [sweep-20-1] 6169 decisions 279 SAT calls 59.94 avg env size
c [sweep-20-1] fully completed sweeping round
c [decomp-88] removed 9 variables
c [sweep-20-1] removed 9 vars (0 failed, 10 eqs, 11 impls)
c [sweep-20-2] 1341 pos 43.2% + 1762 neg 56.8% = 3103 sched 100.0% ret 0
c [sweep-20-2] 11151035 steps 146 queries 58.92 avg class size
c [sweep-20-2] 5115 decisions 147 SAT calls 99.01 avg env size
c [sweep-20-2] 626 variables remain 20% (2477 retained 80%)
c [decomp-89] removed 4 variables
c [sweep-20-2] removed 4 vars (0 failed, 4 eqs, 4 impls)
c [sweep-20] removed 13 vars in TOTAL (2 rounds, 425 queries)
c [score-distribution-21] 2314 pos 74.67%, 785 min 25.33%, 0 zero 0.00%
c [score-distribution-21] 1471 different 47.47% out of total 3099 variables
c [simplification-21] removed 103 variables 3.2% (3099 remain 7%)
c [simplification-21] removed 732 irredundant clauses 4.1% (17107 remain 12%)
c [simplification-21] maximum reduction of 4% = max (3%, 4%)
c [simplification-21] geometric conflict interval increment 58329 = 291648 / 5
c [simplification-21] new conflict interval 349977
c [simplification-21] penalized conflict interval 349977 = 1 * 349977
c [simplification-21] hard conflict limit 1646822 (soft 1471834 + delta 174988)
c [simplification-21] new conflict limit 1471834 (hard 1646822)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c -  242.1    3099    17107   1135187   90543   6737  5492    9    21   21  40%    902  -15    8    9   88%
c -  252.6    3099    17107   1184323   95685   6756  5497    9    43   22  21%    967    9   11    9  124%
c i  257.3    3098    17107   1206602  116814   6758  5499    9    33   28  28%    983   -1   10    9  113%
c -  264.0    3098    17107   1230645   95678   6771  5499    9    37   22  25%  -2225    3    7    9   74%
c -  277.4    3098    17107   1280567   97299   6795  5501   10    40   22  26%   -493    6   11   10  116%
c -  289.6    3098    17107   1333801  100680   6817  5505   12    38   24  32%    351    4   12   10  121%
c -  302.4    3098    17107   1384858  104123   6839  5506   10    35   24  28%    715    1    9   10   88%
c -  316.6    3098    17107   1435283  105225   6859  5509   12    35   24  33%    881    3   13   10  125%
c 
c [simplification-22] limit 1471834 conflicts (hard 1646822) hit after 1471836 conflicts
c [quatres-20] found 9484 quaternary clauses 12% in total
c [quatres-20-1] removed 13 duplicate quaternary clauses
c [quatres-20-1] added 4 double-self-subsuming ternary resolvents
c [quatres-20-2] added 45 single-self-subsuming ternary resolvents
c [quatres-20-2] added 71 quaternary resolvents
c [ternres-19] limit 100472686 with penalty 0 = 0 + 0
c [ternres-19] all 3098 free variables schedulable
c [ternres-19] 346 ternary resolvents (36 bin, 310 trn)
c [ternres-19] fully completed ternary resolution
c [decomp-90] removed 1 variables
c [treelook-8] limit 10047268 penalty 0 = 0 + 0 boost 1
c [treelook-8] scheduled 6017 literals 97%
c [treelook-8] scheduling used 463174 steps
c [treelook-8] scheduled completely
c [treelook-8] limit 10047268 penalty 0 = 0 + 0 boost 1
c [treelook-8] used 2491981 steps
c [treelook-8] fully completed tree based probing
c [decomp-91] removed 1 variables
c [treelook-8] removed 3 variables, found 946 hbrs
c [unhide-17] limit 10000000 with penalty 1 = 1 + 0
c [unhide-17-40] 0 units, 0 failed, 2722 tauts, 0 hbrs, 117022 literals
c [transred-20] limit 2000000 with penalty 0 = 0 + 0
c [transred-20] removed 292 transitive binary clauses
c [cce-11] limit of 502363430 steps penalty 0 = 0 + 0
c [cce-11-1] eliminated 1 clauses out of 28 (4%) of length 11
c [cce-11-1] eliminated 1 clauses out of 29 (3%) of length 10
c [cce-11-1] eliminated 6 clauses out of 50 (12%) of length 9
c [cce-11-1] eliminated 6 clauses out of 187 (3%) of length 8
c [cce-11-1] eliminated 8 clauses out of 362 (2%) of length 7
c [cce-11-1] eliminated 39 clauses out of 714 (5%) of length 6
c [cce-11-1] eliminated 60 clauses out of 1476 (4%) of length 5
c [cce-11-1] eliminated 149 clauses out of 4108 (4%) of length 4
c [cce-11-1] completed large round (ACCE)
c [cce-11-1] eliminated 270 large clauses in 10371057 steps
c [cce-11-1] allowing another 5185528 steps for small clauses
c [cce-11-1] scheduling 5590 clauses = 2906 binary + 2684 ternary
c [cce-11-1] tried to eliminate 5590 small clauses 100%
c [cce-11-1] eliminated 86 binary clauses 3%
c [cce-11-1] eliminated 55 ternary clauses 2%
c [cce-11-1] eliminated 141 small clauses 3%
c [cce-11-1] eliminated 141 small clauses in 8719086 steps
c [cce-11-1] completed small round (ACCE)
c [cce-11-1] eliminated 411 covered clauses in round 1
c [cce-11-2] eliminated 1 clauses out of 28 (4%) of length 10
c [cce-11-2] eliminated 1 clauses out of 181 (1%) of length 8
c [cce-11-2] eliminated 10 clauses out of 354 (3%) of length 7
c [cce-11-2] eliminated 7 clauses out of 675 (1%) of length 6
c [cce-11-2] eliminated 8 clauses out of 1416 (1%) of length 5
c [cce-11-2] eliminated 18 clauses out of 3959 (0%) of length 4
c [cce-11-2] completed large round (ACCE)
c [cce-11-2] eliminated 45 large clauses in 9733025 steps
c [cce-11-2] allowing another 4866512 steps for small clauses
c [cce-11-2] scheduling 5449 clauses = 2820 binary + 2629 ternary
c [cce-11-2] tried to eliminate 5449 small clauses 100%
c [cce-11-2] eliminated 25 binary clauses 1%
c [cce-11-2] eliminated 11 ternary clauses 0%
c [cce-11-2] eliminated 36 small clauses 1%
c [cce-11-2] eliminated 36 small clauses in 8346658 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 4 clauses out of 1408 (0%) of length 5
c [cce-11-3] eliminated 2 clauses out of 3941 (0%) of length 4
c [cce-11-3] completed large round (ACCE)
c [cce-11-3] eliminated 6 large clauses in 9728132 steps
c [cce-11-3] allowing another 4864066 steps for small clauses
c [cce-11-3] scheduling 5413 clauses = 2795 binary + 2618 ternary
c [cce-11-3] tried to eliminate 5413 small clauses 100%
c [cce-11-3] eliminated 9 binary clauses 0%
c [cce-11-3] eliminated 9 small clauses 0%
c [cce-11-3] eliminated 9 small clauses in 8334809 steps
c [cce-11-3] completed small round (ACCE)
c [cce-11-3] eliminated 15 covered clauses in round 3
c [cce-11] eliminated 507 covered clauses in TOTAL during 3 rounds
c [elim-16] scheduling all variables this time
c [elim-16] scheduled 3095 variables 100%
c [elim-16] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-16] rescheduling of touched variables disabled
c [elim-16-1] eliminated 109 variables 4% in round 1 in 2635286 steps
c [elim-16-1] backward subsumption/strengthening limit 2635200
c [elim-16-1-1] backward checking 430 touched variables 14%
c [elim-16-1-1] fully completed backward checking in 1 rounds
c [elim-16-1] subsumed 0 and strengthened 0 clauses in 105177 steps
c [elim-16] fully completed in 1 rounds
c [elim-16] transition to [ all 0 rem 0 ] state
c [elim-16] eliminated 109 = 4% variables out of 3095 scheduled
c [bca-19] limit of 10000000 steps and 33786 added (scaled 2)
c [bca-19] 775 out of 5974 literals actually usable 13%
c [bca-19] added 5 blocked clauses in 139151 steps
c [sweep-21] limit 30141805 penalty 0 = 0 + 0
c [sweep-21-1] 268 pos 45.1% + 326 neg 54.9% = 594 sched 19.9% ret 2392
c [sweep-21-1] 8811728 steps 181 queries 14.09 avg class size
c [sweep-21-1] 4265 decisions 180 SAT calls 54.24 avg env size
c [sweep-21-1] fully completed sweeping round
c [decomp-92] removed 11 variables
c [sweep-21-1] removed 11 vars (0 failed, 10 eqs, 10 impls)
c [sweep-21-2] 1267 pos 42.6% + 1708 neg 57.4% = 2975 sched 100.0% ret 0
c [sweep-21-2] 21362837 steps 285 queries 23.45 avg class size
c [sweep-21-2] 8745 decisions 290 SAT calls 83.28 avg env size
c [sweep-21-2] 25 variables remain 1% (2950 retained 99%)
c [decomp-93] removed 13 variables
c [sweep-21-2] removed 13 vars (0 failed, 14 eqs, 4 impls)
c [sweep-21] removed 24 vars in TOTAL (2 rounds, 464 queries)
c [score-distribution-22] 1866 pos 63.00%, 1096 min 37.00%, 0 zero 0.00%
c [score-distribution-22] 1196 different 40.38% out of total 2962 variables
c [simplification-22] removed 136 variables 4.4% (2962 remain 6%)
c [simplification-22] removed 709 irredundant clauses 4.1% (16398 remain 12%)
c [simplification-22] maximum reduction of 4% = max (4%, 4%)
c [simplification-22] geometric conflict interval increment 69995 = 349977 / 5
c [simplification-22] new conflict interval 419972
c [simplification-22] penalized conflict interval 419972 = 1 * 419972
c [simplification-22] hard conflict limit 2101794 (soft 1891808 + delta 209986)
c [simplification-22] new conflict limit 1891808 (hard 2101794)
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 -  333.2    2962    16398   1489460  107234   6367  4581    8    11   24  70%    961  -20   10   10   99%
c i  337.5    2961    16398   1510621  125989   6370  4581   11    44   31  24%    979   15   12   10  122%
c -  346.0    2961    16395   1542396  108191   6374  4583   10    30   24  33%  -1975   -3   10   10  101%
c -  357.6    2961    16395   1596289  112301   6388  4585   11    32   25  34%   -294   -1    9   10   90%
c -  370.9    2961    16395   1650031  115064   6412  4586   10    29   25  34%    444   -4   14   10  139%
c -  384.3    2961    16395   1702273  115069   6436  4591   11    32   26  35%    762   -1   11   10  106%
c -  398.4    2961    16395   1756967  116785   6460  4594   11    36   26  31%    910    3    9   11   87%
c -  411.0    2961    16395   1811962  119551   6490  4600   11    33   26  35%    975   -0   13   11  122%
c -  423.8    2961    16395   1866489  121477   6514  4602   11    26   26  43%   1003   -7   13   11  115%
c 
c [simplification-23] limit 1891808 conflicts (hard 2101794) hit after 1911740 conflicts
c [quatres-21] found 9556 quaternary clauses 11% in total
c [quatres-21-1] removed 9 duplicate quaternary clauses
c [quatres-21-1] added 1 double-self-subsuming ternary resolvents
c [quatres-21-2] added 45 single-self-subsuming ternary resolvents
c [quatres-21-2] added 113 quaternary resolvents
c [ternres-20] limit 140577371 with penalty 0 = 0 + 0
c [ternres-20] all 2961 free variables schedulable
c [ternres-20] 771 ternary resolvents (43 bin, 728 trn)
c [ternres-20] fully completed ternary resolution
c [gauss-12] limit 14057737 penalty 1 = 1 + 0
c [gauss-12] extracted 1610 xors of average arity 3.1
c [gauss-12] connected 5062 occurrences of 335 variables (average 15.1)
c [gauss-12] limit 14057737 penalty 1 = 1 + 0
c [gauss-12] fully completed
c [gauss-12] exported 0 unary, 0 binary and 1 ternary equations
c [decomp-94] removed 2 variables
c [basicprobe-8] limit 400000000 penalty 0 = 0 + 0
c [basicprobe-8-0] 1602 sched 54%, 6 failed, 0 lifted, 423 hbrs
c [decomp-95] removed 11 variables
c [basicprobe-8-1] 1585 sched 54%, 0 failed, 0 lifted, 73 hbrs
c [basicprobe-8-2] 1584 sched 54%, 0 failed, 0 lifted, 18 hbrs
c [basicprobe-8-3] 1584 sched 54%, 0 failed, 0 lifted, 3 hbrs
c [basicprobe-8-4] 1584 sched 54%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-8-4] fully completed probing
c [basicprobe-8-4] 6 units = 6 failed (100%) + 0 lifted (0%)
c [basicprobe-8-4] removed 11 variables, found 517 hbrs
c [bate-7] eliminated 8 asymmetric tautologies during probing
c [transred-21] limit 2000000 with penalty 0 = 0 + 0
c [transred-21] removed 310 transitive binary clauses
c [block-7] scheduling all variables this time
c [block-7] scheduled 2948 variables 100%
c [block-7] limit of 50000000 steps penalty 4 = 4 + 0
c [block-7] fully completed
c [block-7] transition to [ all 0 rem 0 ] state
c [block-7] eliminated 50 blocked clauses
c [block-7] 50 < 1/100 * 16317 = 163 considered unsuccessful
c [cce-12] limit of 702886857 steps penalty 0 = 0 + 0
c [cce-12-1] eliminated 1 clauses out of 176 (1%) of length 8
c [cce-12-1] eliminated 3 clauses out of 352 (1%) of length 7
c [cce-12-1] eliminated 19 clauses out of 694 (3%) of length 6
c [cce-12-1] eliminated 42 clauses out of 1451 (3%) of length 5
c [cce-12-1] eliminated 44 clauses out of 3895 (1%) of length 4
c [cce-12-1] completed large round (ATE)
c [cce-12-1] eliminated 109 large clauses in 4369012 steps
c [cce-12-1] allowing another 2184506 steps for small clauses
c [cce-12-1] scheduling 7029 clauses = 2701 binary + 4328 ternary
c [cce-12-1] tried to eliminate 7029 small clauses 100%
c [cce-12-1] eliminated 9 binary clauses 0%
c [cce-12-1] eliminated 74 ternary clauses 2%
c [cce-12-1] eliminated 83 small clauses 1%
c [cce-12-1] eliminated 83 small clauses in 5216980 steps
c [cce-12-1] completed small round (ATE)
c [cce-12-1] eliminated 192 covered clauses in round 1
c [cce-12-2] completed large round (ATE)
c [cce-12-2] allowing another 2133181 steps for small clauses
c [cce-12-2] scheduling 6946 clauses = 2692 binary + 4254 ternary
c [cce-12-2] tried to eliminate 6946 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 192 covered clauses in TOTAL during 2 rounds
c [elim-17] scheduling all variables this time
c [elim-17] scheduled 2948 variables 100%
c [elim-17] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-17] rescheduling of touched variables disabled
c [elim-17-1] eliminated 35 variables 1% in round 1 in 2550866 steps
c [elim-17-1] backward subsumption/strengthening limit 2550800
c [elim-17-1-1] backward checking 294 touched variables 10%
c [elim-17-1-1] fully completed backward checking in 1 rounds
c [elim-17-1] subsumed 0 and strengthened 2 clauses in 82766 steps
c [elim-17-1] rescheduled 6 variables 0% by backward subsumption
c [elim-17-2] eliminated 2 variables 0% in round 2 in 7948 steps
c [elim-17-2] backward subsumption/strengthening limit 7900
c [elim-17-2-1] backward checking 9 touched variables 0%
c [elim-17-2-1] incomplete backward checking 0 remain 0%
c [elim-17-2] subsumed 0 and strengthened 0 clauses in 7901 steps
c [elim-17-2] fully rescheduled 2911 variables 99%
c [elim-17-3] eliminated 5 variables 0% in round 3 in 2529748 steps
c [elim-17-3] backward subsumption/strengthening limit 2529700
c [elim-17-3-1] backward checking 41 touched variables 1%
c [elim-17-3-1] fully completed backward checking in 1 rounds
c [elim-17-3] subsumed 0 and strengthened 0 clauses in 20414 steps
c [elim-17] fully completed in 3 rounds
c [elim-17] transition to [ all 0 rem 0 ] state
c [elim-17] eliminated 42 = 1% variables out of 2948 scheduled
c [bca-20] limit of 10000000 steps and 32851 added (scaled 2)
c [bca-20] 713 out of 5814 literals actually usable 12%
c [bca-20] added 11 blocked clauses in 163874 steps
c [sweep-22] limit 42173211 penalty 0 = 0 + 0
c [sweep-22-1] 7 pos 28.0% + 18 neg 72.0% = 25 sched 0.9% ret 2881
c [sweep-22-1] 510944 steps 18 queries 4.61 avg class size
c [sweep-22-1] 234 decisions 17 SAT calls 37.59 avg env size
c [sweep-22-1] fully completed sweeping round
c [decomp-99] removed 2 variables
c [sweep-22-1] removed 2 vars (0 failed, 1 eqs, 1 impls)
c [sweep-22-2] 1232 pos 42.4% + 1672 neg 57.6% = 2904 sched 100.0% ret 0
c [sweep-22-2] 35818482 steps 323 queries 25.91 avg class size
c [sweep-22-2] 10143 decisions 318 SAT calls 87.09 avg env size
c [sweep-22-2] fully completed sweeping round
c [decomp-100] removed 44 variables
c [sweep-22-2] removed 44 vars (0 failed, 52 eqs, 33 impls)
c [sweep-22-3] 1211 pos 42.3% + 1649 neg 57.7% = 2860 sched 100.0% ret 0
c [sweep-22-3] 5853194 steps 16 queries 442.75 avg class size
c [sweep-22-3] 1682 decisions 16 SAT calls 246.56 avg env size
c [sweep-22-3] 2540 variables remain 89% (320 retained 11%)
c [decomp-101] removed 1 variables
c [sweep-22-3] removed 1 vars (0 failed, 1 eqs, 0 impls)
c [sweep-22] removed 47 vars in TOTAL (3 rounds, 354 queries)
c [score-distribution-23] 1531 pos 53.55%, 1328 min 46.45%, 0 zero 0.00%
c [score-distribution-23] 1100 different 38.47% out of total 2859 variables
c [simplification-23] removed 102 variables 3.4% (2859 remain 6%)
c [simplification-23] removed 519 irredundant clauses 3.2% (15876 remain 12%)
c [simplification-23] maximum reduction of 3% = max (3%, 3%)
c [simplification-23] geometric conflict interval increment 104993 = 419972 / 4
c [simplification-23] new conflict interval 524965
c [simplification-23] penalized conflict interval 524965 = 1 * 524965
c [simplification-23] hard conflict limit 2699187 (soft 2436705 + delta 262482)
c [simplification-23] new conflict limit 2436705 (hard 2699187)
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 -  439.0    2859    15876   1920686  122100   6825  4283   11    32   26  34%   1015   -0    8   11   73%
c -  449.7    2859    15876   1976083  124367   6852  4286   11    33   27  32%   1020    5    9   10   86%
c -  459.8    2859    15876   2033171  125859   6857  4290    8    13   27  64%   1022  -10   11   10  117%
c -  479.2    2859    15874   2088340  122011   6891  4296   13    32   27  41%   1023    4   12   11  110%
c -  492.2    2859    15874   2149918  128878   6902  4298   11    31   28  37%   1024    2   10   11   90%
c -  504.6    2859    15874   2207295  130660   6914  4303   12    27   28  43%   1024   -2   11   11  101%
c i  508.8    2858    15874   2231155  153513   6918  4306   11    32   37  35%   1024    3   14   11  126%
c -  517.6    2858    15874   2263804  132011   6923  4306   11    29   28  38%  -5925   -2   10   11   90%
c -  529.0    2858    15874   2321475  134122   6926  4307    9    11   28  82%  -1859  -15    8   11   78%
c -  545.5    2858    15874   2379349  131535   6948  4315   11    26   28  41%   -168    1   11   11  101%
c 
c [simplification-24] limit 2436705 conflicts (hard 2699187) hit after 2436706 conflicts
c [quatres-22] found 9747 quaternary clauses 10% in total
c [quatres-22-1] removed 29 duplicate quaternary clauses
c [quatres-22-2] added 43 single-self-subsuming ternary resolvents
c [quatres-22-2] added 97 quaternary resolvents
c [ternres-21] limit 190915186 with penalty 0 = 0 + 0
c [ternres-21] all 2858 free variables schedulable
c [ternres-21] 873 ternary resolvents (38 bin, 835 trn)
c [ternres-21] fully completed ternary resolution
c [gauss-13] limit 38183037 penalty 0 = 0 + 0
c [gauss-13] extracted 1655 xors of average arity 3.1
c [gauss-13] connected 5165 occurrences of 349 variables (average 14.8)
c [gauss-13] limit 38183037 penalty 0 = 0 + 0
c [gauss-13] fully completed
c [gauss-13] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-102] removed 7 variables
c [simpleprobe-9] all 2851 free variables schedulable
c [simpleprobe-9] limit 200000000 penalty 0 = 0 + 0
c [decomp-103] removed 17 variables
c [simpleprobe-9] fully completed simple probing
c [simpleprobe-9] removed 17 variables, found 1103 hbrs, 4 units
c [transred-22] limit 2000000 with penalty 0 = 0 + 0
c [transred-22] removed 509 transitive binary clauses
c [cce-13] boosting limit by 10
c [cce-13] limit of 9545759330 steps penalty 0 = 0 + 0
c [cce-13-1] eliminated 1 clauses out of 20 (5%) of length 11
c [cce-13-1] eliminated 3 clauses out of 20 (15%) of length 10
c [cce-13-1] eliminated 10 clauses out of 48 (21%) of length 9
c [cce-13-1] eliminated 15 clauses out of 170 (9%) of length 8
c [cce-13-1] eliminated 26 clauses out of 335 (8%) of length 7
c [cce-13-1] eliminated 30 clauses out of 664 (5%) of length 6
c [cce-13-1] eliminated 84 clauses out of 1364 (6%) of length 5
c [cce-13-1] eliminated 155 clauses out of 3810 (4%) of length 4
c [cce-13-1] completed large round (ACCE)
c [cce-13-1] eliminated 324 large clauses in 6815773 steps
c [cce-13-1] allowing another 3407886 steps for small clauses
c [cce-13-1] scheduling 5181 clauses = 2605 binary + 2576 ternary
c [cce-13-1] tried to eliminate 5181 small clauses 100%
c [cce-13-1] eliminated 90 binary clauses 3%
c [cce-13-1] eliminated 98 ternary clauses 4%
c [cce-13-1] eliminated 188 small clauses 4%
c [cce-13-1] eliminated 188 small clauses in 6281430 steps
c [cce-13-1] completed small round (ACCE)
c [cce-13-1] eliminated 512 covered clauses in round 1
c [cce-13-2] eliminated 5 clauses out of 155 (3%) of length 8
c [cce-13-2] eliminated 4 clauses out of 309 (1%) of length 7
c [cce-13-2] eliminated 20 clauses out of 634 (3%) of length 6
c [cce-13-2] eliminated 30 clauses out of 1280 (2%) of length 5
c [cce-13-2] eliminated 36 clauses out of 3655 (1%) of length 4
c [cce-13-2] completed large round (ACCE)
c [cce-13-2] eliminated 95 large clauses in 6480036 steps
c [cce-13-2] allowing another 3240018 steps for small clauses
c [cce-13-2] scheduling 4993 clauses = 2515 binary + 2478 ternary
c [cce-13-2] tried to eliminate 4993 small clauses 100%
c [cce-13-2] eliminated 29 binary clauses 1%
c [cce-13-2] eliminated 18 ternary clauses 1%
c [cce-13-2] eliminated 47 small clauses 1%
c [cce-13-2] eliminated 47 small clauses in 5979997 steps
c [cce-13-2] completed small round (ACCE)
c [cce-13-2] eliminated 142 covered clauses in round 2
c [cce-13-3] eliminated 32 clauses out of 614 (5%) of length 6
c [cce-13-3] eliminated 66 clauses out of 1250 (5%) of length 5
c [cce-13-3] eliminated 44 clauses out of 3619 (1%) of length 4
c [cce-13-3] completed large round (ACCE)
c [cce-13-3] eliminated 142 large clauses in 6453277 steps
c [cce-13-3] allowing another 3226638 steps for small clauses
c [cce-13-3] scheduling 4946 clauses = 2486 binary + 2460 ternary
c [cce-13-3] tried to eliminate 4946 small clauses 100%
c [cce-13-3] eliminated 11 binary clauses 0%
c [cce-13-3] eliminated 6 ternary clauses 0%
c [cce-13-3] eliminated 17 small clauses 0%
c [cce-13-3] eliminated 17 small clauses in 5959272 steps
c [cce-13-3] completed small round (ACCE)
c [cce-13-3] eliminated 159 covered clauses in round 3
c [cce-13] eliminated 813 covered clauses in TOTAL during 3 rounds
c [elim-18] scheduling all variables this time
c [elim-18] scheduled 2834 variables 100%
c [elim-18] boosting limit by 20
c [elim-18] limit of 16000000000 steps penalty 0 = 0 + 0
c [elim-18] rescheduling of touched variables disabled
c [elim-18-1] eliminated 153 variables 5% in round 1 in 2429511 steps
c [elim-18-1] backward subsumption/strengthening limit 2429500
c [elim-18-1-1] backward checking 417 touched variables 15%
c [elim-18-1-1] fully completed backward checking in 1 rounds
c [elim-18-1] subsumed 4 and strengthened 34 clauses in 143203 steps
c [elim-18-1] rescheduled 54 variables 2% by backward subsumption
c [elim-18-2] eliminated 4 variables 0% in round 2 in 192859 steps
c [elim-18-2] backward subsumption/strengthening limit 192800
c [elim-18-2-1] backward checking 18 touched variables 1%
c [elim-18-2-1] fully completed backward checking in 1 rounds
c [elim-18-2] subsumed 0 and strengthened 0 clauses in 27795 steps
c [elim-18] fully completed in 2 rounds
c [elim-18] transition to [ all 0 rem 0 ] state
c [elim-18] eliminated 157 = 6% variables out of 2834 scheduled
c [bca-21] limit of 10000000 steps and 30224 added (scaled 2)
c [bca-21] 643 out of 5356 literals actually usable 12%
c [bca-21] added 10 blocked clauses in 175908 steps
c [sweep-23] limit 57274556 penalty 0 = 0 + 0
c [sweep-23-1] 1021 pos 43.2% + 1345 neg 56.8% = 2366 sched 88.4% ret 311
c [sweep-23-1] 40466291 steps 265 queries 20.37 avg class size
c [sweep-23-1] 9358 decisions 266 SAT calls 86.20 avg env size
c [sweep-23-1] fully completed sweeping round
c [decomp-104] removed 28 variables
c [sweep-23-1] removed 28 vars (0 failed, 28 eqs, 17 impls)
c [sweep-23-2] 1122 pos 42.4% + 1527 neg 57.6% = 2649 sched 100.0% ret 0
c [sweep-23-2] 16948145 steps 39 queries 149.72 avg class size
c [sweep-23-2] 3115 decisions 38 SAT calls 162.53 avg env size
c [sweep-23-2] 1480 variables remain 56% (1169 retained 44%)
c [sweep-23-2] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-23] removed 28 vars in TOTAL (2 rounds, 302 queries)
c [score-distribution-24] 1584 pos 59.80%, 1065 min 40.20%, 0 zero 0.00%
c [score-distribution-24] 1138 different 42.96% out of total 2649 variables
c [simplification-24] removed 209 variables 7.3% (2649 remain 6%)
c [simplification-24] removed 1292 irredundant clauses 8.1% (14582 remain 11%)
c [simplification-24] maximum reduction of 8% = max (7%, 8%)
c [simplification-24] large reduction 8% >= 5% limit
c [simplification-24] next conflict interval 24367 = min (2436706/100, 524965)
c [simplification-24] penalized conflict interval 24367 = 1 * 24367
c [simplification-24] hard conflict limit 2473256 (soft 2461073 + delta 12183)
c [simplification-24] new conflict limit 2461073 (hard 2473256)
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 -  566.0    2649    14582   2447632  130628   6809  4367   12    25   28  51%    604    2   14   11  131%
c 
c [simplification-25] limit 2461073 conflicts (hard 2473256) hit after 2461073 conflicts
c [quatres-23] found 9248 quaternary clauses 10% in total
c [quatres-23-1] removed 35 duplicate quaternary clauses
c [quatres-23-1] added 1 double-self-subsuming ternary resolvents
c [quatres-23-2] added 68 single-self-subsuming ternary resolvents
c [quatres-23-2] added 98 quaternary resolvents
c [ternres-22] limit 193336672 with penalty 0 = 0 + 0
c [ternres-22] all 2649 free variables schedulable
c [ternres-22] 1181 ternary resolvents (49 bin, 1132 trn)
c [ternres-22] fully completed ternary resolution
c [decomp-106] removed 2 variables
c [treelook-9] limit 19333667 penalty 0 = 0 + 0 boost 1
c [treelook-9] scheduled 5294 literals 100%
c [treelook-9] scheduling used 457925 steps
c [treelook-9] scheduled completely
c [treelook-9] limit 19333667 penalty 0 = 0 + 0 boost 1
c [treelook-9] used 2175261 steps
c [treelook-9] fully completed tree based probing
c [decomp-107] removed 2 variables
c [treelook-9] removed 6 variables, found 753 hbrs
c [unhide-18] limit 5000000 with penalty 2 = 2 + 0
c [unhide-18-43] 0 units, 0 failed, 6167 tauts, 0 hbrs, 94278 literals
c [transred-23] limit 2000000 with penalty 0 = 0 + 0
c [transred-23] removed 224 transitive binary clauses
c [cce-14] limit of 966683363 steps penalty 0 = 0 + 0
c [cce-14-1] eliminated 2 clauses out of 36 (6%) of length 9
c [cce-14-1] eliminated 1 clauses out of 145 (1%) of length 8
c [cce-14-1] eliminated 6 clauses out of 276 (2%) of length 7
c [cce-14-1] eliminated 4 clauses out of 557 (1%) of length 6
c [cce-14-1] eliminated 29 clauses out of 1184 (2%) of length 5
c [cce-14-1] eliminated 33 clauses out of 3543 (1%) of length 4
c [cce-14-1] completed large round (ATE)
c [cce-14-1] eliminated 75 large clauses in 3651461 steps
c [cce-14-1] allowing another 1825730 steps for small clauses
c [cce-14-1] scheduling 4849 clauses = 2435 binary + 2414 ternary
c [cce-14-1] tried to eliminate 4849 small clauses 100%
c [cce-14-1] eliminated 5 binary clauses 0%
c [cce-14-1] eliminated 19 ternary clauses 1%
c [cce-14-1] eliminated 24 small clauses 0%
c [cce-14-1] eliminated 24 small clauses in 3902015 steps
c [cce-14-1] completed small round (ATE)
c [cce-14-1] eliminated 99 covered clauses in round 1
c [cce-14-2] completed large round (ATE)
c [cce-14-2] allowing another 1802502 steps for small clauses
c [cce-14-2] scheduling 4826 clauses = 2430 binary + 2396 ternary
c [cce-14-2] tried to eliminate 4826 small clauses 100%
c [cce-14-2] eliminated 1 ternary clauses 0%
c [cce-14-2] eliminated 1 small clauses 0%
c [cce-14-2] eliminated 1 small clauses in 3867694 steps
c [cce-14-2] completed small round (ATE)
c [cce-14-2] eliminated 1 covered clauses in round 2
c [cce-14-3] completed large round (ATE)
c [cce-14-3] allowing another 1801599 steps for small clauses
c [cce-14-3] scheduling 4825 clauses = 2430 binary + 2395 ternary
c [cce-14-3] tried to eliminate 4825 small clauses 100%
c [cce-14-3] completed small round (ATE)
c [cce-14-3] eliminated 0 covered clauses in round 3
c [cce-14] eliminated 100 covered clauses in TOTAL during 3 rounds
c [cce-14] 100 < 1/100 * 14515 = 145 considered unsuccessful
c [elim-19] scheduling all variables this time
c [elim-19] scheduled 2641 variables 100%
c [elim-19] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-19] rescheduling of touched variables disabled
c [elim-19-1] eliminated 58 variables 2% in round 1 in 2329918 steps
c [elim-19-1] backward subsumption/strengthening limit 2329900
c [elim-19-1-1] backward checking 270 touched variables 10%
c [elim-19-1-1] fully completed backward checking in 1 rounds
c [elim-19-1] subsumed 0 and strengthened 4 clauses in 92789 steps
c [elim-19-1] rescheduled 7 variables 0% by backward subsumption
c [elim-19-2] no variable eliminated in round 2 in 11810 steps
c [elim-19] fully completed in 2 rounds
c [elim-19] transition to [ all 0 rem 0 ] state
c [elim-19] eliminated 58 = 2% variables out of 2641 scheduled
c [bca-22] limit of 10000000 steps and 29349 added (scaled 2)
c [bca-22] 619 out of 5168 literals actually usable 12%
c [bca-22] added 2 blocked clauses in 135468 steps
c [sweep-24] limit 58001001 penalty 0 = 0 + 0
c [sweep-24-1] 653 pos 45.4% + 785 neg 54.6% = 1438 sched 55.7% ret 1145
c [sweep-24-1] 26321185 steps 253 queries 16.15 avg class size
c [sweep-24-1] 7060 decisions 251 SAT calls 74.31 avg env size
c [sweep-24-1] fully completed sweeping round
c [decomp-108] removed 25 variables
c [sweep-24-1] removed 25 vars (0 failed, 22 eqs, 8 impls)
c [sweep-24-2] 1088 pos 42.5% + 1470 neg 57.5% = 2558 sched 100.0% ret 0
c [sweep-24-2] 31918007 steps 188 queries 39.96 avg class size
c [sweep-24-2] 7735 decisions 194 SAT calls 93.70 avg env size
c [sweep-24-2] 249 variables remain 10% (2308 retained 90%)
c [decomp-109] removed 12 variables
c [sweep-24-2] removed 12 vars (0 failed, 11 eqs, 6 impls)
c [sweep-24] removed 37 vars in TOTAL (2 rounds, 439 queries)
c [score-distribution-25] 1605 pos 63.04%, 941 min 36.96%, 0 zero 0.00%
c [score-distribution-25] 1007 different 39.55% out of total 2546 variables
c [simplification-25] removed 103 variables 3.9% (2546 remain 5%)
c [simplification-25] removed 452 irredundant clauses 3.1% (14127 remain 10%)
c [simplification-25] maximum reduction of 4% = max (4%, 3%)
c [simplification-25] geometric conflict interval increment 104993 = 524965 / 5
c [simplification-25] new conflict interval 629958
c [simplification-25] penalized conflict interval 629958 = 1 * 629958
c [simplification-25] hard conflict limit 3406010 (soft 3091031 + delta 314979)
c [simplification-25] new conflict limit 3091031 (hard 3406010)
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  574.9    2545    14127   2476716  150332   6491  3589   11    20   26  53%    754   -3   11   11   97%
c -  583.2    2545    14127   2513447  128733   6505  3592   12    24   25  51%  -1355    3   14   10  133%
c -  597.2    2545    14127   2582554  131218   6537  3597    8     9   25  88%    195   -7    7   10   75%
c i  598.3    2544    14127   2589618  135932   6566  3608    7     8   31  90%    280   -8    5    9   51%
c i  600.9    2541    14127   2606278  150671   6575  3610   10    14   31  71%   -943   -1   13    9  140%
c -  611.2    2540    14127   2645952  131349   6593  3613    9    13   25  68%   -194   -3   11   10  107%
c -  624.5    2540    14127   2712576  134468   6610  3618    8    13   25  67%    583   -1    9    9   97%
c i  630.3    2539    14127   2740441  157521   6655  3627    8     9   34  88%    736   -5    6    9   64%
c i  631.6    2486    14127   2747589  163141   6685  3637    7     8   34  82%  -1142   -5    6    9   63%
c i  632.5    2483    14127   2753038  167294   6705  3643    7     9   34  74%  -1075   -3    5    9   61%
c i  632.7    2296    14127   2753675  167463   6736  3651    7     9   34  76%  -1094   -4    5    9   51%
c i  632.7    2274    14127   2753846  167506   6751  3656    7     9   34  76%  -1097   -4    5    9   52%
c i  632.7    2273    14127   2753923  167511   6767  3661    7     9   34  77%  -1098   -4    4    9   49%
c i  632.7    2260    14127   2753949  167516   6770  3662    7     9   34  77%  -1098   -4    4    9   48%
c i  632.7    2249    14127   2753993  167524   6776  3665    7     8   34  77%  -1099   -4    4    9   47%
c i  632.7    2248    14127   2754000  167524   6779  3667    7     8   34  77%  -1099   -4    4    9   46%
c 0  632.7    2065    14127   2754000  167524   6779  3667    7     8   34  77%  -1099   -4    4    9   46%
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 
s UNSATISFIABLE
c
c bate: 179 basic ate = 103 trn 58% + 76 lrg 42% in 7 updates
c bcas: 22 count, 945 added (417 skipped), 1972174 steps
c bkwd: tried 126106 clauses, 251983 lits, 2.00 lits/clause
c bkwd: checked 41974977 occs, 332.85 occs/clause, 166.58 occs/lit
c bkwd: subsumed 0 binary, 23 ternary, 55 large
c bkwd: strengthened 0 binary, 9 ternary (100% self), 313 large (0% self)
c blkd: 7 bces, 3194 removed, 1986626 resolutions, 5048057 steps
c blkd: 3149 blocking literals 3%, 95 pure
c bump: 2781317 bumped seen, 168877018 lits 60.7 on average
c card: 6 count, 0 units, 42 am1, 12764574 steps
c card: 24 rescheduled, 207 eliminated, 10124 resolved, 4307 subsumed
c card: 1034 at-most-one constraints found, average size 3.48
c card: 1034 at-most-one constraints used 100%, average size 3.48
c card: 90 at-most-two constraints found, average size 4.08
c card: 89 at-most-two constraints used 99%, average size 4.08
c cces: 14 cces, 12473 eliminated, 9535 ate 76%, 2938 abce 24%
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: 463874 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 175 gcs, 0 rescored clauses, 1463 rescored vars
c dcps: 109 decompositions, 4627 equivalent 10%
c deco: 2 decision-only clauses 0%, 59% reduction
c decs: 10229882 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c dsch: 55185545 push, 55138011 pop (55138011 dec 100%)
c dsch: 916110982 swaps, 0 down, 279120565 up
c elms: 19 elims, 37744 eliminated 79%, 496 pure 1%
c elms: 54 rounds, 2.8 rounds/bve
c elms: 35375 small 94%, 1778 large 5%
c elms: 66213 tried small, 35375 succeeded 53%, 30838 failed 47%
c elms: 4445 subsumed, 4332 strengthened, 1067 blocked
c elms: 4255178 copies, 5620412 resolutions, 2060495 ipos
c elms: 2373068 subchks, 1330121 strchks
c gaus: 13 extractions, 37832 extracted, 3.1 size, 4 max
c gaus: exported 1 units, 0 binary and 14 ternary equations
c gaus: 0 gc, 36472778 steps, 18236389 extr 50%, 1979825 elim 5%
c glue: 9.6 orig avg, 9.6 real avg, 2.5 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 74775 = 13211 simple 18% + 53364 trn 71% + 8200 lrg 11%, 1242 sub 2%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 2781317 clauses, 26.2 length
c lrnd: 72789273 lits = 107219996 orig - 34430723 removed 32%
c lrnd: 548247 uips 20%, 2000835 flips 72%
c mins: 2758248 mins 99%, 781 bin 0%, 22286 size 1%
c mins: 122210408 poisoned searches, 17767320 hits, 15% hit rate
c mins: 208766095 used twice searches, 10580216 hits, 5% hit rate
c move: moved 7405, 2515 bin 34%, 4890 trn 66%
c otfs: 11659 driving 32%, 24714 restarting 68%
c otfs: str 36373, 35837 red 99%, 536 irr 1%
c otfs: str 36373, 0 bin 0%, 977 trn 3%, 35396 lrg 97%
c otfs: sub 811, 732 red 90%, 79 irr 10%
c otfs: sub 811, 0 bin 0%, 105 trn 13%, 706 lrg 87%
c phas: 1 computed, 12263 set, 3109 pos (25%), 9154 neg (75%)
c prbs: 8 basic, 240435 probed, 139 failed, 1 lifted
c prbs: 9 simple, 163123 probed, 207 failed, 2326 eqs
c prbs: 9 treelook, 14341 probed, 37 failed, 0 lifted
c prom: 901389 locked 14% out of 6526893 tried
c prps: 486867814 props, 45 props/dec
c prps: 95% srch, 5% simp, 0% lkhd
c quat: 23 count, 5708 quat, 1909 self1, 79 self2, 1099 dup
c redc: 76670 clauses 12%, 640503 tried 23%, 19 sat 0%
c redc: 102186 lits 1%, 9972570 tried 9%, 19 sat 0%
c redc: 1308 times jump level reduced, 6.7 levels on average
c reds: 53 count, 51962.3 conflicts per reduce
c reds: 0 memlim 0%, 53 arith 100%
c reds: 2014122 collected 87%, 297209 retired 13%
c rmbd: 5719 removed, 4469 red 78%
c rsts: 81687 restarts 100%, 0 skipped 0%
c rsts: 0 saturating 0%, 0 reuse 0%
c rsts: 0 kept 0.0% average 0.0%
c scnc: 1 count, 1.200 min (200/1000), 1.200 max (200/1000)
c simp: 25 count, 23 confs 92%, 0 vars 0%
c simp: 1 its 4%, 1 bin 4%, 0 trns 0%
c subl: 2781317 count (1207459 tried 0.4), 198137 sub out of 2772525 (7.1%)
c swps: 24 count, 37 rounds, 9176 queries (248.0/round)
c swps: 8657 sat calls, 994 unsat (4.5% success rate)
c swps: 197918 decisions 22.9, 38976 conflicts 4.5
c swps; 87.6 avg class size, 58.1 avg environment size
c swps: 0 failed, 1249 impls, 1498 equivs
c swp0: 3046 type 0 queries, 942 unsat (30.9%), 2737 sat (89.9%)
c swp1: 6130 type 1 queries, 3302 unsat (53.9%), 4941 sat (80.6%)
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: 26025981 calls to obtain time
c tops: 3210 fixed 7%, 69 its, 39913.04 confs/it
c trds: 23 transitive reductions, 10080 removed, 15 failed
c trds: 206450 nodes, 230875 edges, 29863182 steps
c trim: 1243282 words, 4.7 MB
c trnr: 22 count, 1574 bin, 28969 trn, 186424104 steps
c unhd: 18 count, 43 rounds, 67861660 steps
c unhd: 402 non-trivial sccs of average size 2.0
c unhd: 15 units, 13 bin, 2 trn, 0 lrg
c unhd: 56 failed, 55 stamp, 0 lits, 0 bin, 1 trn, 0 lrg
c unhd: 42010 tauts, 904 bin 2%, 10272 trn 24%, 11885 lrg 28%
c unhd: 42010 tauts, 18949 stamp 45%, 40797 red 97%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 584287 str, 13 bin 0%, 1594 trn 0%, 582680 lrg 100%, 578910 red 99%
c vars: 2076 remaining 4% and 45581 removed 96% out of 47657
c vars: 3210 fixed 7%, 37744 eliminated 79%, 4627 equivalent 10%
c vsts: 22917904264 visits, 98% srch, 2% simp, 0% lkhd
c vsts: 48.3 search visits per propagation, 8126.3 per conflict
c wchs: 8473417193 pushed, 14120778 enlarged, 318 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all        2778233       2014122        297209     101925215      28740232       1674565
c 
c  0 0        260869   9    103581   5         0   0  70306244  69  15489917  54    701690  42     4.0
c  1 5        221991   8    160367   8     30504  10  12748645  13<  4056819  14<   232298  14<    0.9
c  2 6        857206  31<   668267  33     78964  27  13954416  14   5943022  21    444970  27     3.0
c  3 9        968159  35    746868  37<    96001  32<  4006610   4   2591267   9    240600  14     4.3
c  4 14       388040  14    283023  14     67741  23    798002   1    585402   2     50139   3     2.5
c  5 21        71013   3     45951   2     19824   7     96998   0     65674   0      4319   0     0.7
c  6 30         9521   0      5307   0      3595   1     12522   0      7180   0       496   0     0.1
c  7 41         1245   0       656   0       505   0      1545   0       831   0        43   0     0.0
c  8 54          163   0        93   0        61   0       203   0       109   0         8   0     0.0
c  9 69           12   0         2   0         9   0        14   0         3   0         1   0     0.0
c 10 86           11   0         5   0         4   0        12   0         6   0         1   0     0.0
c 11 126           3   0         2   0         1   0         4   0         2   0         0   0     0.0
c 
c avg                  2.5           2.6           2.9           0.6           0.9           1.2
c std                  1.2           1.1           1.1           0.9           1.2           1.2
c 
c   16.070   3% sweep
c   13.690   2% decide
c   13.595   2% cce
c    9.786   2% probe
c    9.386   1% unhide
c    7.390   1% bump
c    7.173   1% elim
c    1.964   0% transred
c 
c    6.579 < 1% rest (below)
c 
c    1.944   0% quatres
c    1.298   0% ternres
c    1.298   0% gauss
c    0.949   0% bca
c    0.598   0% block
c    0.309   0% rescore
c    0.184   0% card
c    0.000   0% locs
c    0.000   0% queuesort
c ==================================
c    1.437   0% preprocessing     2%
c   65.246  10% inprocessing     98%
c ==================================
c   66.683  11% simplifying
c  566.059  89% search
c ==================================
c  632.742 100% all
c 
c       2754000 conflicts,        4352.5 confs/sec
c          4848 ternaries,         568.1 confs/ternary
c           763 binaries,         3609.4 confs/binary
c            69 iterations,      39913.0 confs/iteration
c 
c            53 reductions,          0.1 redus/sec,  51962.3 confs/reduction
c         81687 restarts,          129.1 rests/sec,     33.7 confs/restart
c      10229882 decisions,       16167.5 decis/sec,      3.7 decis/conflict
c     486867814 propagations,   769456.8 props/sec,     47.6 props/decision
c 
c 632.7 seconds, 53.5 MB
c launch: done
