c launch: /data/cnf/sc2014/app/bob12m02-opt.cnf.bz2
c host: atom19
c Lingeling SAT Solver
c 
c Version b7ztzu 7b29300825af9bcc1c8b2c5ebcf65fa1cb101cad
c 
c Copyright (C) 2010-2014 Armin Biere JKU Linz Austria.
c All rights reserved.
c 
c released Sun Apr 26 19:26:13 CEST 2015
c compiled Sun Apr 26 19:26:13 CEST 2015
c 
c gcc (Ubuntu 4.8.2-19ubuntu1) 4.8.2
c -Wall -O3 -I../yalsat -I../druplig -DNLGLOG -DNDEBUG -DNCHKSOL
c Linux cluster2 3.13.0-45-generic x86_64
c 
c piping '/data/cnf/sc2014/app/bob12m02-opt.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/bob12m02-opt.cnf.bz2
c no embedded options
c found 'p cnf 26256 77806' header
c read 26256 variables, 77806 clauses, 181546 literals in 0.00 seconds
c
c --abstime=0
c --bate=1
c --batewait=2
c --bca=1
c --bcaddlimldscale=2
c --bcamaxeff=10000000
c --bcaminuse=100
c --bcawait=2
c --bkwdscale=100
c --bkwdroundlim=7
c --bkwdresched=1
c --blkboost=10
c --blkboostvlim=10000000
c --blkclslim=1000000
c --blklarge=1
c --blkmaxeff=800000000
c --blkmineff=50000000
c --blkocclim1=100000
c --blkocclim=1000000
c --blkocclim2=10000
c --blkreleff=100
c --blkresched=1
c --blkrtc=0
c --blksmall=1
c --blksuccessmaxwortc=6
c --blksuccessrat=100
c --block=1
c --blockwait=1
c --boost=1
c --bumpsimp=1
c --card=1
c --cardcut=2
c --cardexpam1=3
c --cardglue=0
c --cardignused=0
c --cardmaxeff=300000000
c --cardmaxlen=1000
c --cardmineff=2000000
c --cardminlen=3
c --cardocclim1=300
c --cardocclim2=15
c --cardreleff=5
c --cardreschedint=10
c --carduse=2
c --cardwait=0
c --cce2wait=1
c --cce=3
c --cceateint=2
c --cceboost=10
c --cceboostdel=3
c --cceboostint=5
c --cceboostvlim=10000000
c --cce3wait=2
c --ccemaxround=3
c --ccemaxeff=2147483647
c --ccemineff=30000000
c --ccereleff=50
c --ccertc=0
c --ccertcint=15
c --ccertcintvlim=2000000
c --ccesuccessrat=100
c --ccewait=2
c --clim=-1
c --compact=0
c --deco=1
c --decolim=100
c --deco1opt=1
c --decompose=1
c --defragfree=50
c --defragint=10000000
c --delmax=10
c --dlim=-1
c --druplig=0
c --drupligcheck=0
c --drupligtrace=0
c --drupligtraceorig=0
c --elim=1
c --elmaxeff=800000000
c --elmblk=1
c --elmblkwait=1
c --elmboost=20
c --elmboostdel=3
c --elmboostint=5
c --elmboostvlim=4000000
c --elmclslim=1000000
c --elmfull=0
c --elmineff=20000000
c --elmlitslim=200
c --elmocclim1=1000
c --elmocclim=1000000
c --elmocclim2=100
c --elmoccsumforced=0
c --elmreleff=200
c --elmresched=0
c --elmroundlim=3
c --elmrtc=0
c --elmrtcint=10
c --elmrtcintvlim=500000
c --elmsuccessmaxwortc=4
c --elmsuccessrat=100
c --exitonabort=0
c --factmax=100000
c --factor=3
c --gauss=1
c --gaussexptrn=1
c --gaussextrall=1
c --gaussmaxeff=50000000
c --gaussmaxor=20
c --gaussmineff=2000000
c --gaussreleff=2
c --gausswait=2
c --gluekeep=4
c --gluekeepsize=15
c --gluescale=4
c --hbrdom=2
c --import=1
c --incredcint=1
c --incredconfslim=0
c --incsavevisits=0
c --inprocessing=1
c --irrlim=1
c --jwhred=1
c --keepmaxglue=1
c --keepmaxglueint=100
c --lhbr=1
c --lkhd=2
c --locs=0
c --locsbanner=0
c --locsclim=1000000
c --locsboost=2
c --locscint=10000
c --locset=2
c --locsexport=1
c --locsmaxeff=100000
c --locsmineff=1000
c --locsred=0
c --locsreleff=5
c --locsrtc=0
c --locsvared=100
c --locswait=2
c --maxscaledglue=15
c --memlim=-1
c --minimize=2
c --minlocalgluelim=200
c --minlocalsizelim=3000
c --minrecgluelim=100
c --minrecsizelim=1000
c --norestartsatlimlo=85
c --move=2
c --otfs=1
c --penmax=4
c --phase=0
c --phaseluckfactor=200
c --phaselucklim=100
c --phaseluckmaxround=10
c --phasesave=1
c --plain=0
c --plim=-1
c --poison=1
c --prbasic=1
c --prbasicmaxeff=400000000
c --prbasicmineff=1000000
c --prbasicreleff=50
c --prbasicroundlim=8
c --prbasicrtc=0
c --prbrtc=0
c --prbsimple=2
c --prbsimpleboost=10
c --prbsimpleliftdepth=2
c --prbsimplemaxeff=200000000
c --prbsimplemineff=2000000
c --prbsimplereleff=40
c --prbsimplertc=0
c --probe=1
c --promote=1
c --promotegluelim=8
c --pure=1
c --quatres=1
c --quatreswait=2
c --queuesort=1
c --queuesortjwh=0
c --randec=0
c --randecint=1000
c --redcls=1
c --redclsglue=6
c --redclsmaxdec=5
c --redclsmaxdepth=10
c --redclsmaxlrg=10
c --redclsmaxprops=100
c --redclsatlimlo=0
c --redclsatlimhi=100
c --redclsize=30
c --redclstype=4
c --reducefixed=0
c --reduceinc=1000
c --reduceinit=50000
c --reduce=1
c --restart=4
c --restartglcint=10
c --restartglclim=115
c --restartinit=0
c --restartint=5
c --restartpen=1
c --retirenb=1
c --retireint=4
c --retiremin=1
c --reusetrail=0
c --rmincpen=4
c --rstinoutinc=110
c --satlimdelay=10000
c --scincinc=200
c --scincincsatlimhi=100
c --scincincdelta=10
c --scincincincint=100000
c --scincincmin=200
c --scincincmode=1
c --score=2
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 26255 free variables 0%
c [limits] no decision limit
c [limits] no conflict limit
c [limits] no propagation limit
c [limits] simplification not delayed since 'simpdelay' zero
c [set-maximum-score] maximum score limit 1.000000d+500
c [set-minimum-score] minimum score limit 1.000000d-500
c [score-type] VMTF (--score=2)
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   26255    77805         0       0      0     0    0     0    5   0%      0    0    0    0    0%
c 
c [simplification-1] limit 0 conflicts (hard 0) hit after 0 conflicts
c [card-1] limit 2000000 penalty 0 = 0 + 0
c [card-1] no at-most-one constraint found
c [card-1] no at-most-two constraint found
c [decomp-1] removed 1 variables
c [simpleprobe-1] all 26255 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 1439 variables
c [simpleprobe-1] fully completed simple probing
c [simpleprobe-1] removed 1439 variables, found 1808 hbrs, 270 units
c [unhide-1] limit 100000 with penalty 0 = 0 + 0
c [unhide-1-1] 0 units, 0 failed, 0 tauts, 0 hbrs, 0 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 24816 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 18525 variables 75% in round 1 in 4802932 steps
c [elim-1-1] backward subsumption/strengthening limit 4802900
c [elim-1-1-1] backward checking 16746 touched variables 68%
c [elim-1-1-1] fully completed backward checking in 1 rounds
c [elim-1-1] subsumed 1 and strengthened 13 clauses in 865130 steps
c [elim-1-1] rescheduled 24 variables 0% by backward subsumption
c [elim-1-2] eliminated 2 variables 0% in round 2 in 43784 steps
c [elim-1-2] backward subsumption/strengthening limit 43700
c [elim-1-2-1] backward checking 9 touched variables 0%
c [elim-1-2-1] fully completed backward checking in 1 rounds
c [elim-1-2] subsumed 1 and strengthened 0 clauses in 42391 steps
c [elim-1-2] rescheduled 4 variables 0% by backward subsumption
c [elim-1-3] no variable eliminated in round 3 in 2471 steps
c [elim-1] fully completed in 3 rounds
c [elim-1] transition to [ all 0 rem 0 ] state
c [elim-1] eliminated 18536 = 75% variables out of 24816 scheduled
c [phase-count-1] 29490 negative 85.2% of 34619 except 5129 14.8%
c [phase-count-1] 30005 positive 86.7% of 34619 except 4614 13.3%
c [phase-1] phase bias: 1007 positive 16%, 5273 negative 84%
c [sort-queue-1] sorted 6280 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 6280 (100%)
c [score-dist-1] max exp 0, different 1 (100%)
c [score-dist-1] median active exp 0, avg 0.0
c [simplification-1] removed 19975 variables 76.1% (6280 remain 24%)
c [simplification-1] removed 43186 irredundant clauses 55.5% (34619 remain 44%)
c [simplification-1] maximum reduction of 76% = max (76%, 56%)
c [simplification-1] large reduction 76% >= 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 34 variables
c [simpleprobe-2] all 6246 free variables schedulable
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [decomp-4] removed 6 variables
c [simpleprobe-2] 444 variables remain 7% (5796 retained 93%)
c [simpleprobe-2] removed 6 variables, found 603 hbrs, 0 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 12480 literals 100%
c [treelook-1] scheduling used 175925 steps
c [treelook-1] scheduled completely
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 466091 steps
c [treelook-1] 12460 literals remain 100%
c [treelook-1] 6240 variables remain to probed next time 100%
c [treelook-1] removed 0 variables, found 5997 hbrs
c [basicprobe-1] limit 1000000 penalty 0 = 0 + 0
c [basicprobe-1-0] 4003 probes remain 64% after last round
c [basicprobe-1-0] removed 0 variables, found 1917 hbrs
c [block-1] scheduling all variables this time
c [block-1] scheduled 6240 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 179 blocked clauses
c [block-1] 179 < 1/100 * 34528 = 345 considered unsuccessful
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 25 clauses out of 140 (18%) of length 6
c [cce-1-1] eliminated 229 clauses out of 1176 (19%) of length 5
c [cce-1-1] eliminated 82 clauses out of 15554 (1%) of length 4
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 336 large clauses in 30000008 steps
c [cce-1-1] allowing another 15000004 steps for small clauses
c [cce-1-1] scheduling 3313 clauses = 2097 binary + 1216 ternary
c [cce-1-1] tried to eliminate 1346 small clauses 41%
c [cce-1-1] eliminated 4 binary clauses 0%
c [cce-1-1] eliminated 42 ternary clauses 3%
c [cce-1-1] eliminated 46 small clauses 1%
c [cce-1-1] eliminated 46 small clauses in 30000009 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 382 covered clauses in round 1
c [cce-1] eliminated 382 covered clauses in TOTAL during 1 rounds
c [elim-2] scheduling all variables this time
c [elim-2] scheduled 6240 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 115 variables 2% in round 1 in 4515597 steps
c [elim-2-1] backward subsumption/strengthening limit 4515500
c [elim-2-1-1] backward checking 435 touched variables 7%
c [elim-2-1-1] fully completed backward checking in 1 rounds
c [elim-2-1] subsumed 0 and strengthened 7 clauses in 429983 steps
c [elim-2-1] rescheduled 27 variables 0% by backward subsumption
c [elim-2-2] eliminated 1 variables 0% in round 2 in 56103 steps
c [elim-2-2] backward subsumption/strengthening limit 56100
c [elim-2-2-1] backward checking 9 touched variables 0%
c [elim-2-2-1] fully completed backward checking in 1 rounds
c [elim-2-2] subsumed 0 and strengthened 0 clauses in 28876 steps
c [elim-2] fully completed in 2 rounds
c [elim-2] transition to [ all 0 rem 0 ] state
c [elim-2] eliminated 116 = 2% variables out of 6240 scheduled
c [bca-1] limit of 10000000 steps and 68142 added (scaled 2)
c [bca-1] 10257 out of 12250 literals actually usable 84%
c [bca-1] added 13 blocked clauses in 28670 steps
c [sweep-1] limit 1000000 penalty 0 = 0 + 0
c [sweep-1-1] 3222 pos 52.6% + 2902 neg 47.4% = 6124 sched 100.0% ret 0
c [sweep-1-1] 1042010 steps 75 queries 249.43 avg class size
c [sweep-1-1] 710 decisions 83 SAT calls 34.29 avg env size
c [sweep-1-1] 5525 variables remain 90% (599 retained 10%)
c [decomp-6] removed 12 variables
c [sweep-1-1] removed 12 vars (0 failed, 11 eqs, 2 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 12 vars in TOTAL (1 rounds, 74 queries)
c [sort-queue-2] sorted 6112 enqueued variables after 1000 conflicts
c [score-dist-2] active 0 (0%), one 3054 (50%), zero 3058 (50%)
c [score-dist-2] max exp 1, different 2 (100%)
c [score-dist-2] median active exp 0, avg 0.0
c [simplification-2] removed 168 variables 2.7% (6112 remain 23%)
c [simplification-2] removed 804 irredundant clauses 2.3% (33815 remain 43%)
c [simplification-2] maximum reduction of 3% = max (3%, 2%)
c [simplification-2] geometric conflict interval increment 5000 = 20000 / 4
c [simplification-2] new conflict interval 5000
c [simplification-2] penalized conflict interval 5000 = 1 * 5000
c [simplification-2] hard conflict limit 16000 (soft 6000 + delta 10000)
c [simplification-2] new conflict limit 6000 (hard 16000)
c 
c [simplification-3] limit 6000 conflicts (hard 16000) hit after 6001 conflicts
c [quatres-1] found 15926 quaternary clauses 89% in total
c [quatres-1-2] added 8 single-self-subsuming ternary resolvents
c [quatres-1-2] added 33 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 6112 free variables schedulable
c [ternres-1] 611 ternary resolvents (59 bin, 552 trn)
c [ternres-1] fully completed ternary resolution
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 37 at-most-one constraints of average size 3.0
c [card-2] no at-most-two constraint found
c [card-2] using previous limit 1000000 for elimination
c [card-2] 37 out of 37 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] generated 5 at-most-one constraints, 2 used 40%
c [card-2] exported 2 binary clauses, 1.0 per/constraint
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 43284 xors of average arity 3.3
c [gauss-1] connected 144448 occurrences of 5174 variables (average 27.9)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-7] removed 13 variables
c [unhide-2] limit 50000 with penalty 1 = 1 + 0
c [unhide-2-2] 0 units, 5 failed, 639 tauts, 0 hbrs, 1299 literals
c [transred-1] limit 250993 with penalty 0 = 0 + 0
c [transred-1] removed 0 transitive binary clauses
c [cce-2] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-2-1] eliminated 1 clauses out of 5 (20%) of length 9
c [cce-2-1] eliminated 1 clauses out of 10 (10%) of length 7
c [cce-2-1] eliminated 6 clauses out of 156 (4%) of length 6
c [cce-2-1] eliminated 33 clauses out of 944 (3%) of length 5
c [cce-2-1] eliminated 100 clauses out of 15518 (1%) of length 4
c [cce-2-1] completed large round (ATE)
c [cce-2-1] eliminated 141 large clauses in 29569571 steps
c [cce-2-1] allowing another 14784785 steps for small clauses
c [cce-2-1] scheduling 3222 clauses = 1902 binary + 1320 ternary
c [cce-2-1] tried to eliminate 1196 small clauses 37%
c [cce-2-1] eliminated 24 binary clauses 1%
c [cce-2-1] eliminated 54 ternary clauses 4%
c [cce-2-1] eliminated 78 small clauses 2%
c [cce-2-1] eliminated 173 small clauses in 30000002 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 314 covered clauses in round 1
c [cce-2] eliminated 314 covered clauses in TOTAL during 1 rounds
c [cce-2] 314 < 1/100 * 33762 = 337 considered unsuccessful
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 6090 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 184 variables 3% in round 1 in 5631039 steps
c [elim-3-1] backward subsumption/strengthening limit 5631000
c [elim-3-1-1] backward checking 637 touched variables 10%
c [elim-3-1-1] fully completed backward checking in 1 rounds
c [elim-3-1] subsumed 0 and strengthened 10 clauses in 514508 steps
c [elim-3-1] rescheduled 16 variables 0% by backward subsumption
c [elim-3-2] no variable eliminated in round 2 in 7240 steps
c [elim-3] fully completed in 2 rounds
c [elim-3] transition to [ all 0 rem 0 ] state
c [elim-3] eliminated 184 = 3% variables out of 6090 scheduled
c [bca-2] limit of 10000000 steps and 66580 added (scaled 2)
c [bca-2] 3439 out of 11814 literals actually usable 29%
c [bca-2] added 54 blocked clauses in 12628 steps
c [sweep-2] limit 1000000 penalty 0 = 0 + 0
c [sweep-2-1] 2812 pos 52.6% + 2531 neg 47.4% = 5343 sched 90.5% ret 563
c [sweep-2-1] 1014278 steps 53 queries 256.77 avg class size
c [sweep-2-1] 833 decisions 54 SAT calls 132.17 avg env size
c [sweep-2-1] 4939 variables remain 84% (967 retained 16%)
c [decomp-8] removed 18 variables
c [sweep-2-1] removed 18 vars (0 failed, 6 eqs, 3 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 18 vars in TOTAL (1 rounds, 52 queries)
c [sort-queue-3] sorted 5888 enqueued variables after 6001 conflicts
c [score-dist-3] active 0 (0%), one 5852 (99%), zero 36 (1%)
c [score-dist-3] max exp 1, different 2 (100%)
c [score-dist-3] median active exp 0, avg 0.0
c [simplification-3] removed 224 variables 3.7% (5888 remain 22%)
c [simplification-3] removed 790 irredundant clauses 2.3% (33025 remain 42%)
c [simplification-3] maximum reduction of 4% = max (4%, 2%)
c [simplification-3] geometric conflict interval increment 4000 = 20000 / 5
c [simplification-3] new conflict interval 9000
c [simplification-3] penalized conflict interval 9000 = 1 * 9000
c [simplification-3] hard conflict limit 25001 (soft 15001 + delta 10000)
c [simplification-3] new conflict limit 15001 (hard 25001)
c 
c [simplification-4] limit 15001 conflicts (hard 25001) hit after 15001 conflicts
c [quatres-2] found 16559 quaternary clauses 85% in total
c [quatres-2-1] removed 3 duplicate quaternary clauses
c [quatres-2-1] added 1 double-self-subsuming ternary resolvents
c [quatres-2-2] added 191 single-self-subsuming ternary resolvents
c [quatres-2-2] added 61 quaternary resolvents
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] all 5888 free variables schedulable
c [ternres-2] 305 ternary resolvents (68 bin, 237 trn)
c [ternres-2] fully completed ternary resolution
c [decomp-9] removed 9 variables
c [treelook-2] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-2] scheduled 9844 literals 84%
c [treelook-2] scheduling used 150015 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-2] used 150212 steps
c [treelook-2] 9828 literals remain 84%
c [treelook-2] 5520 variables remain to probed next time 94%
c [treelook-2] removed 0 variables, found 11 hbrs
c [unhide-3] limit 133367 with penalty 0 = 0 + 0
c [unhide-3-3] 0 units, 0 failed, 6 tauts, 0 hbrs, 1594 literals
c [block-2] scheduling all variables this time
c [block-2] scheduled 5879 variables 100%
c [block-2] limit of 25000000 steps penalty 1 = 1 + 0
c [block-2] fully completed
c [block-2] transition to [ all 0 rem 0 ] state
c [block-2] eliminated 9 blocked clauses
c [block-2] 9 < 1/100 * 33001 = 330 considered unsuccessful
c [elim-4] scheduling all variables this time
c [elim-4] scheduled 5878 variables 100%
c [elim-4] boosting limit by 20
c [elim-4] limit of 400000000 steps penalty 0 = 0 + 0
c [elim-4] rescheduling of touched variables disabled
c [elim-4-1] eliminated 72 variables 1% in round 1 in 7334075 steps
c [elim-4-1] backward subsumption/strengthening limit 7334000
c [elim-4-1-1] backward checking 235 touched variables 4%
c [elim-4-1-1] fully completed backward checking in 1 rounds
c [elim-4-1] subsumed 0 and strengthened 0 clauses in 146172 steps
c [elim-4] fully completed in 1 rounds
c [elim-4] transition to [ all 0 rem 0 ] state
c [elim-4] eliminated 72 = 1% variables out of 5878 scheduled
c [bca-3] limit of 10000000 steps and 66277 added (scaled 2)
c [bca-3] 809 out of 11614 literals actually usable 7%
c [bca-3] added 0 blocked clauses in 11698 steps
c [sweep-3] limit 1000000 penalty 0 = 0 + 0
c [sweep-3-1] 2624 pos 54.0% + 2232 neg 46.0% = 4856 sched 83.6% ret 950
c [sweep-3-1] 1000362 steps 47 queries 400.57 avg class size
c [sweep-3-1] 1223 decisions 45 SAT calls 72.20 avg env size
c [sweep-3-1] 4492 variables remain 77% (1314 retained 23%)
c [decomp-11] removed 5 variables
c [sweep-3-1] removed 5 vars (0 failed, 5 eqs, 4 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 5 vars in TOTAL (1 rounds, 46 queries)
c [sort-queue-4] sorted 5801 enqueued variables after 15001 conflicts
c [score-dist-4] active 0 (0%), one 5800 (100%), zero 1 (0%)
c [score-dist-4] max exp 1, different 2 (100%)
c [score-dist-4] median active exp 0, avg 0.0
c [simplification-4] removed 87 variables 1.5% (5801 remain 22%)
c [simplification-4] removed 155 irredundant clauses 0.5% (32870 remain 42%)
c [simplification-4] maximum reduction of 1% = max (1%, 0%)
c [simplification-4] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-4] new conflict interval 19000
c [simplification-4] penalized conflict interval 19000 = 1 * 19000
c [simplification-4] hard conflict limit 44001 (soft 34001 + delta 10000)
c [simplification-4] new conflict limit 34001 (hard 44001)
c 
c [simplification-5] limit 34001 conflicts (hard 44001) hit after 34003 conflicts
c [quatres-3] found 17718 quaternary clauses 78% in total
c [quatres-3-1] removed 1 duplicate quaternary clauses
c [quatres-3-1] added 1 double-self-subsuming ternary resolvents
c [quatres-3-2] added 166 single-self-subsuming ternary resolvents
c [quatres-3-2] added 133 quaternary resolvents
c [ternres-3] limit 4000000 with penalty 0 = 0 + 0
c [ternres-3] all 5801 free variables schedulable
c [ternres-3] 464 ternary resolvents (44 bin, 420 trn)
c [ternres-3] 2 variables remain 0% (5799 retained 100%)
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] extracted 27797 xors of average arity 3.0
c [gauss-2] connected 83220 occurrences of 3496 variables (average 23.8)
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-12] removed 28 variables
c [transred-2] limit 857394 with penalty 1 = 1 + 0
c [transred-2] removed 60 transitive binary clauses
c [cce-3] limit of 15000000 steps penalty 1 = 1 + 0
c [cce-3-1] eliminated 9 clauses out of 159 (6%) of length 6
c [cce-3-1] eliminated 290 clauses out of 970 (30%) of length 5
c [cce-3-1] eliminated 2 clauses out of 15568 (0%) of length 4
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 301 large clauses in 15000024 steps
c [cce-3-1] allowing another 7500012 steps for small clauses
c [cce-3-1] scheduling 14611 clauses = 1127 binary + 13484 ternary
c [cce-3-1] tried to eliminate 2772 small clauses 19%
c [cce-3-1] eliminated 31 binary clauses 3%
c [cce-3-1] eliminated 144 ternary clauses 1%
c [cce-3-1] eliminated 175 small clauses 1%
c [cce-3-1] eliminated 175 small clauses in 15000004 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 476 covered clauses in round 1
c [cce-3] eliminated 476 covered clauses in TOTAL during 1 rounds
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 5773 variables 100%
c [elim-5] limit of 34295798 steps penalty 0 = 0 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5-1] eliminated 31 variables 1% in round 1 in 6777232 steps
c [elim-5-1] backward subsumption/strengthening limit 6777200
c [elim-5-1-1] backward checking 129 touched variables 2%
c [elim-5-1-1] fully completed backward checking in 1 rounds
c [elim-5-1] subsumed 0 and strengthened 0 clauses in 330972 steps
c [elim-5] fully completed in 1 rounds
c [elim-5] transition to [ all 0 rem 0 ] state
c [elim-5] eliminated 31 = 1% variables out of 5773 scheduled
c [elim-5] 31 < 1/100 * 5773 = 57 considered unsuccessful
c [sweep-4] limit 1000000 penalty 0 = 0 + 0
c [sweep-4-1] 2354 pos 52.8% + 2103 neg 47.2% = 4457 sched 77.6% ret 1285
c [sweep-4-1] 1039589 steps 32 queries 314.34 avg class size
c [sweep-4-1] 965 decisions 32 SAT calls 103.66 avg env size
c [sweep-4-1] 4247 variables remain 74% (1495 retained 26%)
c [decomp-13] removed 14 variables
c [sweep-4-1] removed 14 vars (0 failed, 12 eqs, 4 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 14 vars in TOTAL (1 rounds, 31 queries)
c [sort-queue-5] sorted 5728 enqueued variables after 34003 conflicts
c [score-dist-5] active 0 (0%), one 5728 (100%), zero 0 (0%)
c [score-dist-5] max exp 1, different 1 (50%)
c [score-dist-5] median active exp 0, avg 0.0
c [simplification-5] removed 73 variables 1.3% (5728 remain 22%)
c [simplification-5] removed 592 irredundant clauses 1.8% (32278 remain 41%)
c [simplification-5] maximum reduction of 2% = max (1%, 2%)
c [simplification-5] geometric conflict interval increment 6666 = 20000 / 3
c [simplification-5] new conflict interval 25666
c [simplification-5] penalized conflict interval 25666 = 1 * 25666
c [simplification-5] hard conflict limit 72502 (soft 59669 + delta 12833)
c [simplification-5] new conflict limit 59669 (hard 72502)
c 
c [simplification-6] limit 59669 conflicts (hard 72502) hit after 59669 conflicts
c [quatres-4] found 18957 quaternary clauses 72% in total
c [quatres-4-1] added 6 double-self-subsuming ternary resolvents
c [quatres-4-2] added 203 single-self-subsuming ternary resolvents
c [quatres-4-2] added 197 quaternary resolvents
c [ternres-4] limit 4000000 with penalty 0 = 0 + 0
c [ternres-4] 2 schedulable variables 0%
c [ternres-4] 8 ternary resolvents (0 bin, 8 trn)
c [ternres-4] fully completed ternary resolution
c [card-3] limit 500000 penalty 2 = 2 + 0
c [card-3] found 21 at-most-one constraints of average size 3.0
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 500000 for elimination
c [card-3] 21 out of 21 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [decomp-14] removed 44 variables
c [basicprobe-2] limit 8740626 penalty 1 = 1 + 0
c [basicprobe-2-0] 2108 probes remain 37% after last round
c [basicprobe-2-0] removed 0 variables, found 16423 hbrs
c [bate-1] eliminated 2 asymmetric tautologies during probing
c [unhide-4] limit 349625 with penalty 1 = 1 + 0
c [unhide-4-4] 0 units, 0 failed, 1867 tauts, 0 hbrs, 26193 literals
c [transred-3] limit 2000000 with penalty 0 = 0 + 0
c [transred-3] removed 3 transitive binary clauses
c [cce-4] boosting limit by 10
c [cce-4] limit of 300000000 steps penalty 0 = 0 + 0
c [cce-4-1] eliminated 6 clauses out of 156 (4%) of length 6
c [cce-4-1] eliminated 18 clauses out of 710 (3%) of length 5
c [cce-4-1] eliminated 79 clauses out of 15610 (1%) of length 4
c [cce-4-1] completed large round (ATE)
c [cce-4-1] eliminated 103 large clauses in 27571216 steps
c [cce-4-1] allowing another 13785608 steps for small clauses
c [cce-4-1] scheduling 14249 clauses = 1038 binary + 13211 ternary
c [cce-4-1] tried to eliminate 14249 small clauses 100%
c [cce-4-1] eliminated 65 binary clauses 6%
c [cce-4-1] eliminated 867 ternary clauses 7%
c [cce-4-1] eliminated 932 small clauses 7%
c [cce-4-1] eliminated 932 small clauses in 54103871 steps
c [cce-4-1] completed small round (ATE)
c [cce-4-1] completed small and large (ATE)
c [cce-4-1] eliminated 1035 covered clauses in round 1
c [cce-4-2] completed large round (ATE)
c [cce-4-2] allowing another 13036725 steps for small clauses
c [cce-4-2] scheduling 13317 clauses = 973 binary + 12344 ternary
c [cce-4-2] tried to eliminate 13317 small clauses 100%
c [cce-4-2] completed small round (ATE)
c [cce-4-2] eliminated 0 covered clauses in round 2
c [cce-4] eliminated 1035 covered clauses in TOTAL during 2 rounds
c [bca-4] limit of 10000000 steps and 62947 added (scaled 2)
c [bca-4] 292 out of 11370 literals actually usable 3%
c [bca-4] added 0 blocked clauses in 43724 steps
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 10488750 penalty 0 = 0 + 0
c [sweep-5-1] 2295 pos 54.5% + 1914 neg 45.5% = 4209 sched 74.0% ret 1475
c [sweep-5-1] 10639431 steps 153 queries 59.39 avg class size
c [sweep-5-1] 7029 decisions 156 SAT calls 270.48 avg env size
c [sweep-5-1] 1587 variables remain 28% (4097 retained 72%)
c [decomp-15] removed 146 variables
c [sweep-5-1] removed 146 vars (0 failed, 64 eqs, 31 impls)
c [sweep-5] considered successful since not run to completion yet
c [sweep-5] removed 146 vars in TOTAL (1 rounds, 152 queries)
c [sort-queue-6] sorted 5538 enqueued variables after 59669 conflicts
c [score-dist-6] active 0 (0%), one 5538 (100%), zero 0 (0%)
c [score-dist-6] max exp 1, different 1 (50%)
c [score-dist-6] median active exp 0, avg 0.0
c [simplification-6] removed 190 variables 3.3% (5538 remain 21%)
c [simplification-6] removed 1101 irredundant clauses 3.4% (31177 remain 40%)
c [simplification-6] maximum reduction of 3% = max (3%, 3%)
c [simplification-6] geometric conflict interval increment 6416 = 25666 / 4
c [simplification-6] new conflict interval 32082
c [simplification-6] penalized conflict interval 32082 = 1 * 32082
c [simplification-6] hard conflict limit 107792 (soft 91751 + delta 16041)
c [simplification-6] new conflict limit 91751 (hard 107792)
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 -   27.6    5538    31177     84118   24228   4189 27610   14   121    8  11%    736   42   13    9  138%
c 
c [simplification-7] limit 91751 conflicts (hard 107792) hit after 91752 conflicts
c [quatres-5] found 20190 quaternary clauses 67% in total
c [quatres-5-1] removed 5 duplicate quaternary clauses
c [quatres-5-1] added 4 double-self-subsuming ternary resolvents
c [quatres-5-2] added 204 single-self-subsuming ternary resolvents
c [quatres-5-2] added 401 quaternary resolvents
c [ternres-5] limit 6104238 with penalty 0 = 0 + 0
c [ternres-5] all 5538 free variables schedulable
c [ternres-5] 1144 ternary resolvents (150 bin, 994 trn)
c [ternres-5] fully completed ternary resolution
c [decomp-16] removed 168 variables
c [simpleprobe-3] 312 schedulable variables 6%
c [simpleprobe-3] limit 24416953 penalty 0 = 0 + 0
c [decomp-17] removed 50 variables
c [simpleprobe-3] 581 variables remain 11% (4739 retained 89%)
c [simpleprobe-3] removed 50 variables, found 28479 hbrs, 0 units
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 259 transitive binary clauses
c [block-3] scheduling all variables this time
c [block-3] scheduled 5320 variables 100%
c [block-3] limit of 15260595 steps penalty 2 = 2 + 0
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 1 blocked clauses
c [block-3] 1 < 1/100 * 30591 = 305 considered unsuccessful
c [cce-5] limit of 30521191 steps penalty 0 = 0 + 0
c [cce-5-1] eliminated 7 clauses out of 150 (5%) of length 6
c [cce-5-1] eliminated 83 clauses out of 691 (12%) of length 5
c [cce-5-1] eliminated 88 clauses out of 15436 (1%) of length 4
c [cce-5-1] completed large round (ACCE)
c [cce-5-1] eliminated 178 large clauses in 24831323 steps
c [cce-5-1] allowing another 12415661 steps for small clauses
c [cce-5-1] scheduling 2570 clauses = 908 binary + 1662 ternary
c [cce-5-1] tried to eliminate 2300 small clauses 89%
c [cce-5-1] eliminated 111 binary clauses 12%
c [cce-5-1] eliminated 183 ternary clauses 11%
c [cce-5-1] eliminated 294 small clauses 11%
c [cce-5-1] eliminated 294 small clauses in 30521238 steps
c [cce-5-1] incomplete small round (ACCE)
c [cce-5-1] eliminated 472 covered clauses in round 1
c [cce-5] eliminated 472 covered clauses in TOTAL during 1 rounds
c [elim-6] scheduling all variables this time
c [elim-6] scheduled 5320 variables 100%
c [elim-6] limit of 61042383 steps penalty 1 = 1 + 0
c [elim-6] rescheduling of touched variables disabled
c [elim-6-1] eliminated 150 variables 3% in round 1 in 6222074 steps
c [elim-6-1] backward subsumption/strengthening limit 6222000
c [elim-6-1-1] backward checking 506 touched variables 10%
c [elim-6-1-1] fully completed backward checking in 1 rounds
c [elim-6-1] subsumed 0 and strengthened 0 clauses in 342888 steps
c [elim-6] fully completed in 1 rounds
c [elim-6] transition to [ all 0 rem 0 ] state
c [elim-6] eliminated 150 = 3% variables out of 5320 scheduled
c [sweep-6] limit 1831271 penalty 0 = 0 + 0
c [sweep-6-1] 733 pos 54.7% + 607 neg 45.3% = 1340 sched 25.9% ret 3830
c [sweep-6-1] 1875127 steps 58 queries 72.09 avg class size
c [sweep-6-1] 1157 decisions 57 SAT calls 94.68 avg env size
c [sweep-6-1] 1162 variables remain 22% (4008 retained 78%)
c [decomp-18] removed 37 variables
c [sweep-6-1] removed 37 vars (0 failed, 26 eqs, 17 impls)
c [sweep-6] considered successful since not run to completion yet
c [sweep-6] removed 37 vars in TOTAL (1 rounds, 57 queries)
c [sort-queue-7] sorted 5133 enqueued variables after 91752 conflicts
c [score-dist-7] active 0 (0%), one 5133 (100%), zero 0 (0%)
c [score-dist-7] max exp 1, different 1 (50%)
c [score-dist-7] median active exp 0, avg 0.0
c [simplification-7] removed 405 variables 7.3% (5133 remain 20%)
c [simplification-7] removed 1915 irredundant clauses 6.1% (29262 remain 38%)
c [simplification-7] maximum reduction of 7% = max (7%, 6%)
c [simplification-7] large reduction 7% >= 5% limit
c [simplification-7] next conflict interval 2000 = 2000/1
c [simplification-7] penalized conflict interval 2000 = 1 * 2000
c [simplification-7] hard conflict limit 103752 (soft 93752 + delta 10000)
c [simplification-7] new conflict limit 93752 (hard 103752)
c 
c [simplification-8] limit 93752 conflicts (hard 103752) hit after 93753 conflicts
c [quatres-6] found 20232 quaternary clauses 67% in total
c [quatres-6-1] removed 31 duplicate quaternary clauses
c [quatres-6-1] added 15 double-self-subsuming ternary resolvents
c [quatres-6-2] added 82 single-self-subsuming ternary resolvents
c [quatres-6-2] added 352 quaternary resolvents
c [ternres-6] limit 6256532 with penalty 0 = 0 + 0
c [ternres-6] all 5133 free variables schedulable
c [ternres-6] 721 ternary resolvents (125 bin, 596 trn)
c [ternres-6] fully completed ternary resolution
c [gauss-3] limit 500000 penalty 2 = 2 + 0
c [gauss-3] extracted 6769 xors of average arity 3.0
c [gauss-3] connected 20235 occurrences of 2824 variables (average 7.2)
c [gauss-3] limit 500000 penalty 2 = 2 + 0
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-19] removed 76 variables
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 144 transitive binary clauses
c [cce-6] limit of 31282663 steps penalty 0 = 0 + 0
c [cce-6-1] eliminated 28 clauses out of 211 (13%) of length 6
c [cce-6-1] eliminated 32 clauses out of 839 (4%) of length 5
c [cce-6-1] eliminated 83 clauses out of 15726 (1%) of length 4
c [cce-6-1] completed large round (ATE)
c [cce-6-1] eliminated 143 large clauses in 25555496 steps
c [cce-6-1] allowing another 12777748 steps for small clauses
c [cce-6-1] scheduling 1936 clauses = 655 binary + 1281 ternary
c [cce-6-1] tried to eliminate 1936 small clauses 100%
c [cce-6-1] eliminated 2 binary clauses 0%
c [cce-6-1] eliminated 14 ternary clauses 1%
c [cce-6-1] eliminated 16 small clauses 1%
c [cce-6-1] eliminated 16 small clauses in 26352204 steps
c [cce-6-1] completed small round (ATE)
c [cce-6-1] eliminated 159 covered clauses in round 1
c [cce-6-2] incomplete large round (ATE)
c [cce-6-2] allowing another 2465235 steps for small clauses
c [cce-6-2] scheduling 1920 clauses = 653 binary + 1267 ternary
c [cce-6-2] tried to eliminate 284 small clauses 15%
c [cce-6-2] incomplete small round (ATE)
c [cce-6-2] eliminated 0 covered clauses in round 2
c [cce-6] eliminated 159 covered clauses in TOTAL during 2 rounds
c [cce-6] 159 < 1/100 * 29225 = 292 considered unsuccessful
c [elim-7] scheduling all variables this time
c [elim-7] scheduled 5057 variables 100%
c [elim-7] limit of 125130654 steps penalty 0 = 0 + 0
c [elim-7] rescheduling of touched variables disabled
c [elim-7-1] eliminated 18 variables 0% in round 1 in 5916365 steps
c [elim-7-1] backward subsumption/strengthening limit 5916300
c [elim-7-1-1] backward checking 95 touched variables 2%
c [elim-7-1-1] fully completed backward checking in 1 rounds
c [elim-7-1] subsumed 0 and strengthened 0 clauses in 143085 steps
c [elim-7] fully completed in 1 rounds
c [elim-7] transition to [ all 0 rem 0 ] state
c [elim-7] eliminated 18 = 0% variables out of 5057 scheduled
c [elim-7] 18 < 1/100 * 5057 = 50 considered unsuccessful
c [sweep-7] limit 1876959 penalty 0 = 0 + 0
c [sweep-7-1] 633 pos 56.1% + 495 neg 43.9% = 1128 sched 22.4% ret 3911
c [sweep-7-1] 1916449 steps 64 queries 55.58 avg class size
c [sweep-7-1] 1267 decisions 60 SAT calls 67.05 avg env size
c [sweep-7-1] 908 variables remain 18% (4131 retained 82%)
c [decomp-20] removed 23 variables
c [sweep-7-1] removed 23 vars (0 failed, 22 eqs, 21 impls)
c [sweep-7] removed 23 vars in TOTAL (1 rounds, 63 queries)
c [sort-queue-8] sorted 5016 enqueued variables after 93753 conflicts
c [score-dist-8] active 0 (0%), one 5016 (100%), zero 0 (0%)
c [score-dist-8] max exp 1, different 1 (50%)
c [score-dist-8] median active exp 0, avg 0.0
c [simplification-8] removed 117 variables 2.3% (5016 remain 19%)
c [simplification-8] removed 651 irredundant clauses 2.2% (28609 remain 37%)
c [simplification-8] maximum reduction of 2% = max (2%, 2%)
c [simplification-8] geometric conflict interval increment 10694 = 32082 / 3
c [simplification-8] new conflict interval 42776
c [simplification-8] penalized conflict interval 42776 = 1 * 42776
c [simplification-8] hard conflict limit 157917 (soft 136529 + delta 21388)
c [simplification-8] new conflict limit 136529 (hard 157917)
c 
c [simplification-9] limit 136529 conflicts (hard 157917) hit after 137781 conflicts
c [quatres-7] found 21450 quaternary clauses 59% in total
c [quatres-7-1] removed 23 duplicate quaternary clauses
c [quatres-7-1] added 12 double-self-subsuming ternary resolvents
c [quatres-7-2] added 177 single-self-subsuming ternary resolvents
c [quatres-7-2] added 414 quaternary resolvents
c [ternres-7] limit 8767828 with penalty 0 = 0 + 0
c [ternres-7] all 5016 free variables schedulable
c [ternres-7] 672 ternary resolvents (87 bin, 585 trn)
c [ternres-7] fully completed ternary resolution
c [decomp-21] removed 93 variables
c [unhide-5] limit 438391 with penalty 2 = 2 + 0
c [unhide-5-5] 0 units, 0 failed, 32 tauts, 0 hbrs, 9349 literals
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 145 transitive binary clauses
c [bca-5] limit of 10000000 steps and 57679 added (scaled 2)
c [bca-5] 201 out of 9848 literals actually usable 2%
c [bca-5] added 0 blocked clauses in 64832 steps
c [sweep-8] limit 2630348 penalty 0 = 0 + 0
c [sweep-8-1] 445 pos 50.6% + 435 neg 49.4% = 880 sched 17.9% ret 4043
c [sweep-8-1] 2683300 steps 42 queries 37.14 avg class size
c [sweep-8-1] 1854 decisions 40 SAT calls 211.85 avg env size
c [sweep-8-1] 674 variables remain 14% (4249 retained 86%)
c [decomp-22] removed 17 variables
c [sweep-8-1] removed 17 vars (0 failed, 16 eqs, 13 impls)
c [sweep-8] removed 17 vars in TOTAL (1 rounds, 41 queries)
c [sort-queue-9] sorted 4906 enqueued variables after 137781 conflicts
c [score-dist-9] active 0 (0%), one 4906 (100%), zero 0 (0%)
c [score-dist-9] max exp 1, different 1 (50%)
c [score-dist-9] median active exp 0, avg 0.0
c [simplification-9] removed 110 variables 2.2% (4906 remain 19%)
c [simplification-9] removed 38 irredundant clauses 0.1% (28571 remain 37%)
c [simplification-9] maximum reduction of 2% = max (2%, 0%)
c [simplification-9] geometric conflict interval increment 14258 = 42776 / 3
c [simplification-9] new conflict interval 57034
c [simplification-9] penalized conflict interval 57034 = 1 * 57034
c [simplification-9] hard conflict limit 223332 (soft 194815 + delta 28517)
c [simplification-9] new conflict limit 194815 (hard 223332)
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 -   41.9    4906    28571    145254   37023   4792 40288   13    94    9  14%    911   -3   12   12  105%
c 
c [simplification-10] limit 194815 conflicts (hard 223332) hit after 194816 conflicts
c [quatres-8] found 22550 quaternary clauses 52% in total
c [quatres-8-1] removed 29 duplicate quaternary clauses
c [quatres-8-1] added 13 double-self-subsuming ternary resolvents
c [quatres-8-2] added 246 single-self-subsuming ternary resolvents
c [quatres-8-2] added 464 quaternary resolvents
c [ternres-8] limit 11188151 with penalty 0 = 0 + 0
c [ternres-8] all 4906 free variables schedulable
c [ternres-8] 807 ternary resolvents (98 bin, 709 trn)
c [ternres-8] fully completed ternary resolution
c [card-4] limit 699259 penalty 3 = 3 + 0
c [card-4] found 21 at-most-one constraints of average size 3.3
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 699259 for elimination
c [card-4] 21 out of 21 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [decomp-23] removed 85 variables
c [treelook-3] limit 279703 penalty 2 = 2 + 0 boost 1
c [treelook-3] scheduled 6580 literals 68%
c [treelook-3] scheduling used 279706 steps
c [treelook-3] not fully scheduled
c [treelook-3] limit 279703 penalty 2 = 2 + 0 boost 1
c [treelook-3] used 359369 steps
c [treelook-3] 6576 literals remain 68%
c [treelook-3] 4204 variables remain to probed next time 87%
c [treelook-3] removed 0 variables, found 2073 hbrs
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 119 transitive binary clauses
c [cce-7] limit of 27970379 steps penalty 1 = 1 + 0
c [cce-7-1] eliminated 20 clauses out of 189 (11%) of length 6
c [cce-7-1] eliminated 71 clauses out of 868 (8%) of length 5
c [cce-7-1] eliminated 170 clauses out of 15453 (1%) of length 4
c [cce-7-1] completed large round (ACCE)
c [cce-7-1] eliminated 261 large clauses in 24092729 steps
c [cce-7-1] allowing another 12046364 steps for small clauses
c [cce-7-1] scheduling 10521 clauses = 622 binary + 9899 ternary
c [cce-7-1] tried to eliminate 7105 small clauses 68%
c [cce-7-1] eliminated 13 binary clauses 2%
c [cce-7-1] eliminated 133 ternary clauses 1%
c [cce-7-1] eliminated 146 small clauses 1%
c [cce-7-1] eliminated 146 small clauses in 27970383 steps
c [cce-7-1] incomplete small round (ACCE)
c [cce-7-1] eliminated 407 covered clauses in round 1
c [cce-7] eliminated 407 covered clauses in TOTAL during 1 rounds
c [elim-8] scheduling all variables this time
c [elim-8] scheduled 4821 variables 100%
c [elim-8] boosting limit by 20
c [elim-8] limit of 2237630390 steps penalty 1 = 1 + 0
c [elim-8] rescheduling of touched variables disabled
c [elim-8-1] eliminated 38 variables 1% in round 1 in 5559794 steps
c [elim-8-1] backward subsumption/strengthening limit 5559700
c [elim-8-1-1] backward checking 131 touched variables 3%
c [elim-8-1-1] fully completed backward checking in 1 rounds
c [elim-8-1] subsumed 0 and strengthened 0 clauses in 147706 steps
c [elim-8] fully completed in 1 rounds
c [elim-8] transition to [ all 0 rem 0 ] state
c [elim-8] eliminated 38 = 1% variables out of 4821 scheduled
c [elim-8] 38 < 1/100 * 4821 = 48 considered unsuccessful
c [sweep-9] limit 3356445 penalty 0 = 0 + 0
c [sweep-9-1] 372 pos 57.1% + 279 neg 42.9% = 651 sched 13.6% ret 4132
c [sweep-9-1] 3399439 steps 77 queries 31.90 avg class size
c [sweep-9-1] 2931 decisions 73 SAT calls 174.41 avg env size
c [sweep-9-1] 382 variables remain 8% (4401 retained 92%)
c [decomp-25] removed 30 variables
c [sweep-9-1] removed 30 vars (0 failed, 26 eqs, 21 impls)
c [sweep-9] removed 30 vars in TOTAL (1 rounds, 76 queries)
c [sort-queue-10] sorted 4753 enqueued variables after 194816 conflicts
c [score-dist-10] active 0 (0%), one 4753 (100%), zero 0 (0%)
c [score-dist-10] max exp 1, different 1 (50%)
c [score-dist-10] median active exp 0, avg 0.0
c [simplification-10] removed 153 variables 3.1% (4753 remain 18%)
c [simplification-10] removed 1040 irredundant clauses 3.6% (27527 remain 35%)
c [simplification-10] maximum reduction of 4% = max (3%, 4%)
c [simplification-10] geometric conflict interval increment 11406 = 57034 / 5
c [simplification-10] new conflict interval 68440
c [simplification-10] penalized conflict interval 68440 = 1 * 68440
c [simplification-10] hard conflict limit 297476 (soft 263256 + delta 34220)
c [simplification-10] new conflict limit 263256 (hard 297476)
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 -   50.3    4753    27527    198310   47490   5376 34161   13   107   10  12%    974    7   12   12  101%
c i   50.5    4752    27527    202329   51033   5400 34167   11    72   12  16%    977  -28    6   12   48%
c i   52.4    4751    27527    214514   61038   5621 34227   10    69   13  15%  -1682  -29    5   12   40%
c i   56.1    4750    27527    243726   85731   5993 34317   12    78   18  15%   -833  -17    6   12   48%
c -   56.2    4750    27527    244035   54373   5996 34317   12    78   10  15%   -943  -17   14   12  120%
c i   58.2    4749    27527    268034   74160   6142 34351   12    87   15  14%   -577   -1   12   11  105%
c i   59.6    4748    27527    279471   84073   6254 34375   11    88   16  13%   -645   -2    6   12   54%
c i   60.8    4747    27527    287233   90603   6355 34404   11    79   18  14%   -620  -11    6   12   48%
c -   61.0    4747    27527    288956   60878   6358 34404   12    76   11  15%   -674  -13   12   12  104%
c 
c [simplification-11] limit 263256 conflicts (hard 297476) hit after 297477 conflicts
c [quatres-9] found 23953 quaternary clauses 44% in total
c [quatres-9-1] removed 30 duplicate quaternary clauses
c [quatres-9-1] added 29 double-self-subsuming ternary resolvents
c [quatres-9-2] added 272 single-self-subsuming ternary resolvents
c [quatres-9-2] added 615 quaternary resolvents
c [ternres-9] limit 15417035 with penalty 0 = 0 + 0
c [ternres-9] all 4747 free variables schedulable
c [ternres-9] 943 ternary resolvents (95 bin, 848 trn)
c [ternres-9] fully completed ternary resolution
c [decomp-26] removed 118 variables
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 172 transitive binary clauses
c [block-4] scheduling all variables this time
c [block-4] scheduled 4635 variables 100%
c [block-4] limit of 19271294 steps penalty 3 = 3 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 0 blocked clauses
c [cce-8] boosting limit by 10
c [cce-8] limit of 770851790 steps penalty 0 = 0 + 0
c [cce-8-1] eliminated 22 clauses out of 233 (9%) of length 6
c [cce-8-1] eliminated 31 clauses out of 888 (3%) of length 5
c [cce-8-1] eliminated 131 clauses out of 15190 (1%) of length 4
c [cce-8-1] completed large round (ATE)
c [cce-8-1] eliminated 184 large clauses in 20019845 steps
c [cce-8-1] allowing another 10009922 steps for small clauses
c [cce-8-1] scheduling 9725 clauses = 566 binary + 9159 ternary
c [cce-8-1] tried to eliminate 9725 small clauses 100%
c [cce-8-1] eliminated 8 binary clauses 1%
c [cce-8-1] eliminated 32 ternary clauses 0%
c [cce-8-1] eliminated 40 small clauses 0%
c [cce-8-1] eliminated 40 small clauses in 27775285 steps
c [cce-8-1] completed small round (ATE)
c [cce-8-1] eliminated 224 covered clauses in round 1
c [cce-8-2] completed large round (ATE)
c [cce-8-2] allowing another 9832243 steps for small clauses
c [cce-8-2] scheduling 9685 clauses = 558 binary + 9127 ternary
c [cce-8-2] tried to eliminate 9685 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 224 covered clauses in TOTAL during 2 rounds
c [cce-8] 224 < 1/100 * 27486 = 274 considered unsuccessful
c [sweep-10] limit 4625110 penalty 0 = 0 + 0
c [sweep-10-1] 185 pos 50.4% + 182 neg 49.6% = 367 sched 7.9% ret 4268
c [sweep-10-1] 4663028 steps 145 queries 10.72 avg class size
c [sweep-10-1] 1543 decisions 106 SAT calls 69.51 avg env size
c [sweep-10-1] 68 variables remain 1% (4567 retained 99%)
c [decomp-27] removed 87 variables
c [sweep-10-1] removed 87 vars (0 failed, 85 eqs, 103 impls)
c [sweep-10] removed 87 vars in TOTAL (1 rounds, 144 queries)
c [sort-queue-11] sorted 4548 enqueued variables after 297477 conflicts
c [score-dist-11] active 0 (0%), one 4548 (100%), zero 0 (0%)
c [score-dist-11] max exp 1, different 1 (50%)
c [score-dist-11] median active exp 0, avg 0.0
c [simplification-11] removed 199 variables 4.2% (4548 remain 17%)
c [simplification-11] removed 280 irredundant clauses 1.0% (27247 remain 35%)
c [simplification-11] maximum reduction of 4% = max (4%, 1%)
c [simplification-11] geometric conflict interval increment 13688 = 68440 / 5
c [simplification-11] new conflict interval 82128
c [simplification-11] penalized conflict interval 82128 = 1 * 82128
c [simplification-11] hard conflict limit 420669 (soft 379605 + delta 41064)
c [simplification-11] new conflict limit 379605 (hard 420669)
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   64.3    4547    27247    303578   70948   6286 32661   11    87   14  13%   -353   -0    5   12   47%
c i   66.6    4546    27247    321407   86247   6425 32688   12    89   17  14%   -223    2   14   12  118%
c -   68.2    4546    27247    333849   64527   6530 32715   12    94   11  13%   -241    7   14   12  119%
c i   69.1    4545    27247    346700   75229   6639 32730    9    63   14  14%    -16  -21    5   11   46%
c i   71.4    4299    27247    364952   90647   6840 32798   11    76   16  14%    -67   -6    6   11   52%
c -   73.7    4299    27247    380389   71165   6934 32824   13    75   12  17%    -67   -6   16   12  138%
c 
c [simplification-12] limit 379605 conflicts (hard 420669) hit after 384539 conflicts
c [quatres-10] found 21708 quaternary clauses 40% in total
c [quatres-10-1] removed 45 duplicate quaternary clauses
c [quatres-10-1] added 29 double-self-subsuming ternary resolvents
c [quatres-10-2] added 188 single-self-subsuming ternary resolvents
c [quatres-10-2] added 510 quaternary resolvents
c [ternres-10] limit 19363093 with penalty 0 = 0 + 0
c [ternres-10] all 4299 free variables schedulable
c [ternres-10] 752 ternary resolvents (110 bin, 642 trn)
c [ternres-10] fully completed ternary resolution
c [gauss-4] limit 484077 penalty 3 = 3 + 0
c [gauss-4] extracted 6937 xors of average arity 3.0
c [gauss-4] connected 20562 occurrences of 2610 variables (average 7.9)
c [gauss-4] limit 484077 penalty 3 = 3 + 0
c [decomp-28] removed 219 variables
c [gauss-4] exported 0 unary, 1 binary and 0 ternary equations
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 213 transitive binary clauses
c [sweep-11] boosting sweeping limit by 10
c [sweep-11] limit 58089280 penalty 0 = 0 + 0
c [sweep-11-1] 35 pos 61.4% + 22 neg 38.6% = 57 sched 1.4% ret 4023
c [sweep-11-1] 871148 steps 34 queries 5.79 avg class size
c [sweep-11-1] 503 decisions 27 SAT calls 55.56 avg env size
c [sweep-11-1] fully completed sweeping round
c [decomp-30] removed 10 variables
c [sweep-11-1] removed 10 vars (0 failed, 10 eqs, 13 impls)
c [sweep-11-2] 2140 pos 52.6% + 1930 neg 47.4% = 4070 sched 100.0% ret 0
c [sweep-11-2] 29806145 steps 761 queries 15.71 avg class size
c [sweep-11-2] 10139 decisions 599 SAT calls 74.45 avg env size
c [sweep-11-2] fully completed sweeping round
c [decomp-31] removed 471 variables
c [sweep-11-2] removed 471 vars (0 failed, 483 eqs, 446 impls)
c [sweep-11-3] 1888 pos 52.5% + 1711 neg 47.5% = 3599 sched 100.0% ret 0
c [sweep-11-3] 13087578 steps 282 queries 35.09 avg class size
c [sweep-11-3] 7999 decisions 278 SAT calls 87.91 avg env size
c [sweep-11-3] fully completed sweeping round
c [decomp-32] removed 26 variables
c [sweep-11-3] removed 26 vars (0 failed, 38 eqs, 6 impls)
c [sweep-11] removed 507 vars in TOTAL (3 rounds, 1074 queries)
c [sort-queue-12] sorted 3573 enqueued variables after 384539 conflicts
c [score-dist-12] active 0 (0%), one 3573 (100%), zero 0 (0%)
c [score-dist-12] max exp 1, different 1 (50%)
c [score-dist-12] median active exp 0, avg 0.0
c [simplification-12] removed 726 variables 16.9% (3573 remain 14%)
c [simplification-12] removed 2550 irredundant clauses 9.4% (24697 remain 32%)
c [simplification-12] maximum reduction of 17% = max (17%, 9%)
c [simplification-12] large reduction 17% >= 5% limit
c [simplification-12] next conflict interval 3845 = min (384539/100, 82128)
c [simplification-12] penalized conflict interval 3845 = 1 * 3845
c [simplification-12] hard conflict limit 398384 (soft 388384 + delta 10000)
c [simplification-12] new conflict limit 388384 (hard 398384)
c 
c [simplification-13] limit 388384 conflicts (hard 398384) hit after 398385 conflicts
c [quatres-11] found 20363 quaternary clauses 41% in total
c [quatres-11-1] removed 202 duplicate quaternary clauses
c [quatres-11-1] added 7 double-self-subsuming ternary resolvents
c [quatres-11-2] added 34 single-self-subsuming ternary resolvents
c [quatres-11-2] added 198 quaternary resolvents
c [ternres-11] limit 19804257 with penalty 0 = 0 + 0
c [ternres-11] all 3573 free variables schedulable
c [ternres-11] 100 ternary resolvents (2 bin, 98 trn)
c [ternres-11] fully completed ternary resolution
c [decomp-33] removed 2 variables
c [basicprobe-3] limit 24755321 penalty 2 = 2 + 0
c [basicprobe-3-0] 1499 sched 42%, 2 failed, 0 lifted, 7880 hbrs
c [decomp-34] removed 3 variables
c [basicprobe-3-1] 90 probes remain 3% after last round
c [basicprobe-3-1] 2 units = 2 failed (100%) + 0 lifted (0%)
c [basicprobe-3-1] removed 3 variables, found 10870 hbrs
c [bate-2] eliminated 33 asymmetric tautologies during probing
c [unhide-6] limit 495106 with penalty 3 = 3 + 0
c [unhide-6-6] 0 units, 0 failed, 2142 tauts, 0 hbrs, 17213 literals
c [transred-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 277 transitive binary clauses
c [cce-9] limit of 49510642 steps penalty 1 = 1 + 0
c [cce-9-1] eliminated 23 clauses out of 211 (11%) of length 6
c [cce-9-1] eliminated 69 clauses out of 753 (9%) of length 5
c [cce-9-1] eliminated 258 clauses out of 12336 (2%) of length 4
c [cce-9-1] completed large round (ACCE)
c [cce-9-1] eliminated 350 large clauses in 9266065 steps
c [cce-9-1] allowing another 4633032 steps for small clauses
c [cce-9-1] scheduling 8966 clauses = 486 binary + 8480 ternary
c [cce-9-1] tried to eliminate 8966 small clauses 100%
c [cce-9-1] eliminated 52 binary clauses 11%
c [cce-9-1] eliminated 301 ternary clauses 4%
c [cce-9-1] eliminated 353 small clauses 4%
c [cce-9-1] eliminated 353 small clauses in 16029286 steps
c [cce-9-1] completed small round (ACCE)
c [cce-9-1] completed small and large (ACCE)
c [cce-9-1] eliminated 703 covered clauses in round 1
c [cce-9-2] eliminated 18 clauses out of 188 (10%) of length 6
c [cce-9-2] eliminated 42 clauses out of 684 (6%) of length 5
c [cce-9-2] eliminated 24 clauses out of 12078 (0%) of length 4
c [cce-9-2] completed large round (ACCE)
c [cce-9-2] eliminated 84 large clauses in 7354318 steps
c [cce-9-2] allowing another 3677159 steps for small clauses
c [cce-9-2] scheduling 8618 clauses = 434 binary + 8184 ternary
c [cce-9-2] tried to eliminate 8618 small clauses 100%
c [cce-9-2] eliminated 24 binary clauses 6%
c [cce-9-2] eliminated 78 ternary clauses 1%
c [cce-9-2] eliminated 102 small clauses 1%
c [cce-9-2] eliminated 102 small clauses in 11446707 steps
c [cce-9-2] completed small round (ACCE)
c [cce-9-2] eliminated 186 covered clauses in round 2
c [cce-9-3] eliminated 2 clauses out of 642 (0%) of length 5
c [cce-9-3] completed large round (ACCE)
c [cce-9-3] eliminated 2 large clauses in 5468263 steps
c [cce-9-3] allowing another 2734131 steps for small clauses
c [cce-9-3] scheduling 8518 clauses = 410 binary + 8108 ternary
c [cce-9-3] tried to eliminate 8518 small clauses 100%
c [cce-9-3] eliminated 3 binary clauses 1%
c [cce-9-3] eliminated 15 ternary clauses 0%
c [cce-9-3] eliminated 18 small clauses 0%
c [cce-9-3] eliminated 18 small clauses in 8960526 steps
c [cce-9-3] completed small round (ACCE)
c [cce-9-3] eliminated 20 covered clauses in round 3
c [cce-9] eliminated 909 covered clauses in TOTAL during 3 rounds
c [elim-9] scheduling all variables this time
c [elim-9] scheduled 3568 variables 100%
c [elim-9] limit of 99021285 steps penalty 2 = 2 + 0
c [elim-9] rescheduling of touched variables disabled
c [elim-9-1] eliminated 205 variables 6% in round 1 in 4121450 steps
c [elim-9-1] backward subsumption/strengthening limit 4121400
c [elim-9-1-1] backward checking 565 touched variables 16%
c [elim-9-1-1] fully completed backward checking in 1 rounds
c [elim-9-1] subsumed 0 and strengthened 0 clauses in 224799 steps
c [elim-9] fully completed in 1 rounds
c [elim-9] transition to [ all 0 rem 0 ] state
c [elim-9] eliminated 205 = 6% variables out of 3568 scheduled
c [bca-6] limit of 10000000 steps and 42821 added (scaled 2)
c [bca-6] 239 out of 6728 literals actually usable 4%
c [bca-6] added 0 blocked clauses in 63807 steps
c [sweep-12] limit 5941277 penalty 0 = 0 + 0
c [sweep-12-1] 1791 pos 53.3% + 1572 neg 46.7% = 3363 sched 100.0% ret 0
c [sweep-12-1] 5952767 steps 109 queries 57.15 avg class size
c [sweep-12-1] 4900 decisions 109 SAT calls 116.39 avg env size
c [sweep-12-1] 448 variables remain 13% (2914 retained 87%)
c [decomp-35] removed 7 variables
c [sweep-12-1] removed 7 vars (0 failed, 1 eqs, 0 impls)
c [sweep-12] removed 7 vars in TOTAL (1 rounds, 108 queries)
c [sort-queue-13] sorted 3356 enqueued variables after 398385 conflicts
c [score-dist-13] active 0 (0%), one 3356 (100%), zero 0 (0%)
c [score-dist-13] max exp 1, different 1 (50%)
c [score-dist-13] median active exp 0, avg 0.0
c [simplification-13] removed 217 variables 6.1% (3356 remain 13%)
c [simplification-13] removed 3555 irredundant clauses 14.4% (21142 remain 27%)
c [simplification-13] maximum reduction of 14% = max (6%, 14%)
c [simplification-13] large reduction 14% >= 5% limit
c [simplification-13] next conflict interval 3983 = min (398385/100, 82128)
c [simplification-13] penalized conflict interval 3983 = 1 * 3983
c [simplification-13] hard conflict limit 412368 (soft 402368 + delta 10000)
c [simplification-13] new conflict limit 402368 (hard 412368)
c 
c [simplification-14] limit 402368 conflicts (hard 412368) hit after 406085 conflicts
c [quatres-12] found 19173 quaternary clauses 41% in total
c [quatres-12-1] removed 14 duplicate quaternary clauses
c [quatres-12-1] added 7 double-self-subsuming ternary resolvents
c [quatres-12-2] added 62 single-self-subsuming ternary resolvents
c [quatres-12-2] added 115 quaternary resolvents
c [ternres-12] limit 20241042 with penalty 0 = 0 + 0
c [ternres-12] all 3356 free variables schedulable
c [ternres-12] 197 ternary resolvents (6 bin, 191 trn)
c [ternres-12] fully completed ternary resolution
c [gauss-5] limit 1012052 penalty 2 = 2 + 0
c [gauss-5] extracted 14911 xors of average arity 3.0
c [gauss-5] connected 44710 occurrences of 2168 variables (average 20.6)
c [gauss-5] limit 1012052 penalty 2 = 2 + 0
c [gauss-5] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-36] removed 5 variables
c [simpleprobe-4] 268 schedulable variables 8%
c [simpleprobe-4] limit 80964170 penalty 0 = 0 + 0
c [decomp-37] removed 2 variables
c [simpleprobe-4] 406 variables remain 12% (2943 retained 88%)
c [simpleprobe-4] removed 2 variables, found 74262 hbrs, 0 units
c [transred-11] limit 2000000 with penalty 0 = 0 + 0
c [transred-11] removed 159 transitive binary clauses
c [cce-10] limit of 101205212 steps penalty 0 = 0 + 0
c [cce-10-1] eliminated 22 clauses out of 41 (54%) of length 7
c [cce-10-1] eliminated 14 clauses out of 270 (5%) of length 6
c [cce-10-1] eliminated 9 clauses out of 1190 (1%) of length 5
c [cce-10-1] eliminated 102 clauses out of 12106 (1%) of length 4
c [cce-10-1] completed large round (ATE)
c [cce-10-1] eliminated 147 large clauses in 6187471 steps
c [cce-10-1] allowing another 3093735 steps for small clauses
c [cce-10-1] scheduling 1409 clauses = 317 binary + 1092 ternary
c [cce-10-1] tried to eliminate 1409 small clauses 100%
c [cce-10-1] eliminated 18 ternary clauses 2%
c [cce-10-1] eliminated 18 small clauses 1%
c [cce-10-1] eliminated 18 small clauses in 6475379 steps
c [cce-10-1] completed small round (ATE)
c [cce-10-1] eliminated 165 covered clauses in round 1
c [cce-10-2] completed large round (ATE)
c [cce-10-2] allowing another 2985777 steps for small clauses
c [cce-10-2] scheduling 1391 clauses = 317 binary + 1074 ternary
c [cce-10-2] tried to eliminate 1391 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 165 covered clauses in TOTAL during 2 rounds
c [cce-10] 165 < 1/100 * 21073 = 210 considered unsuccessful
c [sweep-13] limit 6072312 penalty 0 = 0 + 0
c [sweep-13-1] 247 pos 56.1% + 193 neg 43.9% = 440 sched 13.1% ret 2909
c [sweep-13-1] 6107140 steps 82 queries 11.88 avg class size
c [sweep-13-1] 3183 decisions 85 SAT calls 208.60 avg env size
c [sweep-13-1] 60 variables remain 2% (3289 retained 98%)
c [decomp-38] removed 8 variables
c [sweep-13-1] removed 8 vars (0 failed, 8 eqs, 3 impls)
c [sweep-13] removed 8 vars in TOTAL (1 rounds, 81 queries)
c [sort-queue-14] sorted 3341 enqueued variables after 406085 conflicts
c [score-dist-14] active 0 (0%), one 3341 (100%), zero 0 (0%)
c [score-dist-14] max exp 1, different 1 (50%)
c [score-dist-14] median active exp 0, avg 0.0
c [simplification-14] removed 15 variables 0.4% (3341 remain 13%)
c [simplification-14] removed 234 irredundant clauses 1.1% (20908 remain 27%)
c [simplification-14] maximum reduction of 1% = max (0%, 1%)
c [simplification-14] geometric conflict interval increment 41064 = 82128 / 2
c [simplification-14] new conflict interval 123192
c [simplification-14] penalized conflict interval 123192 = 1 * 123192
c [simplification-14] hard conflict limit 590873 (soft 529277 + delta 61596)
c [simplification-14] new conflict limit 529277 (hard 590873)
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   85.4    3340    20907    426067   87241   4315 99369   13    79   18  17%    481    3   10   12   87%
c i   85.9    3097    20904    428231   89028   4347 99371   14    82   18  17%   -323    5   14   12  116%
c i   86.0    3096    20904    428573   89278   4357 99372   13    78   18  17%   -358    1    7   12   62%
c -   86.2    3096    20904    432594   58693   4367 99373   11    85   12  13%   -381    8   15   12  123%
c i   87.0    3095    20904    443818   67485   4401 99380   11    72   15  16%   -162   -4   13   12  113%
c i   87.0    3094    20904    443819   67485   4401 99380   11    72   15  16%   -162   -4   13   12  112%
c i   89.0    3090    20904    462956   84335   4476 99391   10    78   16  13%    -42    2   14   12  118%
c i   90.8    3085    20904    477327   97208   4544 99415   11    65   18  17%    -76  -10   14   12  123%
c -   91.0    3081    20904    479523   66109   4548 99417   11    71   12  16%   -234   -4   10   11   91%
c i   91.5    3080    20902    492385   76925   4576 99423    7    34   15  22%    -32  -37    8   11   73%
c i   91.8    2777    20902    495645   79728   4598 99428    8    44   15  19%   -198  -25    8   11   77%
c i   91.8    2776    20902    495646   79728   4598 99428    8    44   15  19%   -198  -25    8   11   76%
c i   91.9    1476    20902    496930   80876   4602 99430    9    50   15  19%   -217  -19   16   11  152%
c i   92.2    1475    20902    497976   81770   4628 99438   11    54   16  20%   -221  -15   13   11  121%
c i   92.2    1474    20902    498003   81781   4635 99439   11    54   16  20%   -221  -15   12   11  114%
c i   92.2    1472    20902    498318   82057   4640 99439   11    52   16  20%   -223  -17   13   11  115%
c i   92.3    1471    20902    499240   82857   4653 99442   11    51   16  21%   -221  -17   11   11  105%
c i   92.6    1470    20902    505739   88456   4669 99450    9    46   17  19%   -127  -20   12   11  110%
c i   92.7    1469    20902    506144   88835   4674 99454    9    46   17  20%   -153  -21   12   11  115%
c i   93.0     995    20902    508320   90786   4712 99464   12    40   18  29%   -179  -26   16   11  148%
c i   93.1     994    20902    508686   91111   4717 99469   12    40   18  30%   -185  -26   13   11  122%
c i   93.1     992    20902    508688   91111   4718 99469   12    40   18  30%   -185  -26   13   11  121%
c i   93.1     991    20902    508849   91260   4720 99469   12    39   18  30%   -187  -26   13   11  120%
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   93.1     990    20902    508875   91281   4720 99470   12    39   18  30%   -188  -26   13   11  118%
c i   93.1     989    20902    508879   91282   4722 99470   12    39   18  30%   -188  -26   13   11  116%
c i   93.2     988    20902    509621   91901   4741 99477   12    39   18  30%   -191  -26   14   11  127%
c i   93.2     986    20902    509792   92041   4751 99485   12    39   18  30%   -192  -27   11   11  104%
c i   93.2     974    20902    509793   92041   4751 99485   12    39   18  30%   -192  -27   11   11  104%
c i   93.2     973    20902    509794   92041   4751 99485   12    39   18  30%   -192  -27   11   11  103%
c 0   93.2     957    20902    509794   92041   4751 99485   12    39   18  30%   -192  -27   11   11  103%
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: 35 basic ate = 33 trn 94% + 2 lrg 6% in 2 updates
c bcas: 6 count, 67 added (1 skipped), 225359 steps
c bkwd: tried 49192 clauses, 98380 lits, 2.00 lits/clause
c bkwd: checked 1942628 occs, 39.49 occs/clause, 19.75 occs/lit
c bkwd: subsumed 0 binary, 0 ternary, 2 large
c bkwd: strengthened 0 binary, 0 ternary (0% self), 30 large (0% self)
c blkd: 4 bces, 189 removed, 772524 resolutions, 1804530 steps
c blkd: 582 blocking literals 1%, 1 pure
c bump: 484769 bumped seen, 28343845 lits 58.5 on average
c card: 4 count, 0 units, 2 am1, 90274046 steps
c card: 4 rescheduled, 39 eliminated, 10591 resolved, 821 subsumed
c card: 79 at-most-one constraints found, average size 3.10
c card: 79 at-most-one constraints used 100%, average size 3.10
c card: 0 at-most-two constraints found, average size 0.00
c card: 0 at-most-two constraints used 0%, average size 0.00
c cces: 10 cces, 4448 eliminated, 3530 ate 79%, 918 abce 21%
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: 259352 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 68 gcs, 0 rescored clauses, 0 rescored vars
c dcps: 38 decompositions, 2890 equivalent 11%
c deco: 314 decision-only clauses 0%, 73% reduction
c decs: 4377476 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 9 elims, 19342 eliminated 74%, 71 pure 0%
c elms: 20 rounds, 2.2 rounds/bve
c elms: 19173 small 99%, 97 large 1%
c elms: 54034 tried small, 19173 succeeded 35%, 34861 failed 65%
c elms: 3375 subsumed, 510 strengthened, 10 blocked
c elms: 1710169 copies, 2384725 resolutions, 2178479 ipos
c elms: 273739 subchks, 157199 strchks
c gaus: 5 extractions, 99698 extracted, 3.1 size, 4 max
c gaus: exported 0 units, 1 binary and 0 ternary equations
c gaus: 0 gc, 9535612 steps, 4767806 extr 50%, 5100463 elim 53%
c glue: 11.9 orig avg, 11.9 real avg, 2.5 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 162683 = 105152 simple 65% + 53891 trn 33% + 3640 lrg 2%, 381 sub 0%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 484769 clauses, 28.1 length
c lrnd: 13631513 lits = 18051109 orig - 4419596 removed 24%
c lrnd: 111629 uips 23%, 305119 flips 63%
c mins: 463289 mins 96%, 401 bin 0%, 20730 size 4%
c mins: 41942046 poisoned searches, 2584773 hits, 6% hit rate
c mins: 56560093 used twice searches, 3228212 hits, 6% hit rate
c move: moved 2366, 383 bin 16%, 1983 trn 84%
c otfs: 30646 driving 35%, 56929 restarting 65%
c otfs: str 87575, 87449 red 100%, 126 irr 0%
c otfs: str 87575, 0 bin 0%, 1458 trn 2%, 86117 lrg 98%
c otfs: sub 2437, 2425 red 100%, 12 irr 0%
c otfs: sub 2437, 0 bin 0%, 302 trn 12%, 2135 lrg 88%
c phas: 1 computed, 6280 set, 1007 pos (16%), 5273 neg (84%)
c prbs: 3 basic, 10893 probed, 2 failed, 0 lifted
c prbs: 4 simple, 76965 probed, 270 failed, 2609 eqs
c prbs: 3 treelook, 40 probed, 0 failed, 0 lifted
c prom: 65820 locked 13% out of 488687 tried
c prps: 141553735 props, 31 props/dec
c prps: 95% srch, 5% simp, 0% lkhd
c quat: 12 count, 3493 quat, 1833 self1, 124 self2, 1623 dup
c queu: 14 sorted, 4377476 next (53 steps 0.00)
c queu: 28440074 enq (28440055 steps 1.00), 28343845 deq 100%
c redc: 10666 clauses 7%, 162584 tried 32%, 0 sat 0%
c redc: 14767 lits 1%, 1426038 tried 8%, 0 sat 0%
c redc: 452 times jump level reduced, 5.9 levels on average
c reds: 9 count, 56643.8 conflicts per reduce
c reds: 0 memlim 0%, 9 arith 100%
c reds: 243028 collected 81%, 55678 retired 19%
c rmbd: 2713 removed, 2622 red 97%
c rsts: 20917 restarts 100%, 0 skipped 0%
c rsts: 0 saturating 0%, 0 reuse 0%
c rsts: 0 kept 0.0% average 0.0%
c scnc: 0 count, 1.000 min (0/1000), 1.000 max (0/1000)
c simp: 14 count, 14 confs 100%, 0 vars 0%
c simp: 0 its 0%, 0 bin 0%, 0 trns 0%
c subl: 484769 count (329331 tried 0.7), 43742 sub out of 478510 (9.1%)
c swps: 13 count, 15 rounds, 1999 queries (133.3/round)
c swps: 1804 sat calls, 620 unsat (3.1% success rate)
c swps: 46236 decisions 25.6, 5621 conflicts 3.1
c swps; 56.5 avg class size, 109.6 avg environment size
c swps: 0 failed, 687 impls, 813 equivs
c swp0: 662 type 0 queries, 359 unsat (54.2%), 487 sat (73.6%)
c swp1: 1337 type 1 queries, 1294 unsat (96.8%), 699 sat (52.3%)
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: 9724791 calls to obtain time
c tops: 3067 fixed 12%, 37 its, 13778.22 confs/it
c trds: 11 transitive reductions, 1551 removed, 0 failed
c trds: 61544 nodes, 50123 edges, 17865838 steps
c trim: 310250 words, 1.2 MB
c trnr: 12 count, 844 bin, 5880 trn, 64172596 steps
c unhd: 6 count, 6 rounds, 3126215 steps
c unhd: 78 non-trivial sccs of average size 2.0
c unhd: 0 units, 0 bin, 0 trn, 0 lrg
c unhd: 5 failed, 5 stamp, 0 lits, 0 bin, 0 trn, 0 lrg
c unhd: 4686 tauts, 21 bin 0%, 968 trn 21%, 988 lrg 21%
c unhd: 4686 tauts, 2709 stamp 58%, 4684 red 100%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 55648 str, 0 bin 0%, 165 trn 0%, 55483 lrg 100%, 55563 red 100%
c vars: 957 remaining 4% and 25299 removed 96% out of 26256
c vars: 3067 fixed 12%, 19342 eliminated 74%, 2890 equivalent 11%
c vsts: 2634688333 visits, 96% srch, 4% simp, 0% lkhd
c vsts: 18.7 search visits per propagation, 4949.3 per conflict
c wchs: 599941685 pushed, 4341293 enlarged, 162 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all         482003        243028         55678      16459529       2450833        244672
c 
c  0 0         86616  18      1687   1         0   0  11405802  69<  1259690  51    115056  47     1.6
c  1 5         46367  10     17163   7      5201   9   2722869  17    391234  16<    42315  17<    0.6
c  2 6        121930  25     69150  28     12705  23   1823191  11    484174  20     60044  25     1.2
c  3 9        106739  22<    73267  30<    13520  24    347761   2    195913   8     20910   9     1.0
c  4 14        57797  12     41116  17      9011  16<    88019   1     69591   3      4993   2     0.8
c  5 21        29256   6     19534   8      6254  11     35384   0     25534   1       755   0     1.0
c  6 30        15222   3      9913   4      3776   7     17177   0     11846   0       268   0     1.3
c  7 41         8501   2      5604   2      2166   4      9151   0      6394   0       146   0     1.4
c  8 54         5254   1      3320   1      1515   3      5559   0      3716   0        89   0     1.5
c  9 69         2940   1      1705   1      1001   2      3103   0      1916   0        56   0     1.4
c 10 86          967   0       479   0       379   1      1023   0       557   0        23   0     0.5
c 11 126         339   0        70   0       129   0       396   0       213   0        10   0     0.1
c 12 230          75   0        20   0        21   0        94   0        55   0         7   0     0.0
c 
c avg                  2.5           3.2           3.6           0.5           1.0           1.0
c std                  1.9           1.6           2.0           0.9           1.3           1.2
c 
c    7.432   8% cce
c    3.130   3% bump
c    3.012   3% sweep
c    2.913   3% decide
c    2.695   3% elim
c    2.082   2% probe
c    1.013   1% transred
c    0.933   1% quatres
c    0.522   1% gauss
c 
c    1.273 < 1% rest (below)
c 
c    0.470   1% unhide
c    0.426   0% ternres
c    0.159   0% block
c    0.158   0% bca
c    0.060   0% card
c    0.000   0% locs
c    0.000   0% queuesort
c    0.000   0% rescore
c ==================================
c    0.637   1% preprocessing     3%
c   19.199  21% inprocessing     97%
c ==================================
c   19.836  21% simplifying
c   73.396  79% search
c ==================================
c   93.233 100% all
c 
c        509794 conflicts,        5468.0 confs/sec
c          4383 ternaries,         116.3 confs/ternary
c           674 binaries,          756.4 confs/binary
c            37 iterations,      13778.2 confs/iteration
c 
c             9 reductions,          0.1 redus/sec,  56643.8 confs/reduction
c         20917 restarts,          224.4 rests/sec,     24.4 confs/restart
c       4377476 decisions,       46952.1 decis/sec,      8.6 decis/conflict
c     141553735 propagations,  1518284.0 props/sec,     32.3 props/decision
c 
c 93.2 seconds, 30.4 MB
c launch: done
