c launch: /data/cnf/sc2014/app/atco_enc1_opt2_10_16.cnf.bz2
c host: atom22
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/atco_enc1_opt2_10_16.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/atco_enc1_opt2_10_16.cnf.bz2
c no embedded options
c found 'p cnf 9643 152744' header
c read 9643 variables, 152744 clauses, 641139 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 9241 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    9241   143219         0       0      0     0    0     0    7   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 1807 at-most-one constraints of average size 3.1
c [card-1] found 36 at-most-two constraints of average size 4.3
c [card-1] using previous limit 2000000 for elimination
c [card-1] 1843 out of 1843 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 1190 variables
c [simpleprobe-1] all 8453 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 212 variables
c [simpleprobe-1] 5518 variables remain 67% (2723 retained 33%)
c [simpleprobe-1] removed 212 variables, found 2040 hbrs, 16 units
c [unhide-1] limit 100000 with penalty 0 = 0 + 0
c [unhide-1-1] 0 units, 6 failed, 1125 tauts, 0 hbrs, 8 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 8235 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 2287 variables 28% in round 1 in 7753328 steps
c [elim-1-1] backward subsumption/strengthening limit 7753300
c [elim-1-1-1] backward checking 5626 touched variables 68%
c [elim-1-1-1] incomplete backward checking 3444 remain 61%
c [elim-1-1] subsumed 354 and strengthened 329 clauses in 7753568 steps
c [elim-1-1] rescheduled 327 variables 4% by backward subsumption
c [elim-1-2] eliminated 4 variables 0% in round 2 in 183148 steps
c [elim-1-2] backward subsumption/strengthening limit 183100
c [elim-1-2-1] backward checking 3484 touched variables 42%
c [elim-1-2-1] incomplete backward checking 3462 remain 99%
c [elim-1-2] subsumed 0 and strengthened 5 clauses in 183228 steps
c [elim-1-2] rescheduled 18 variables 0% by backward subsumption
c [elim-1-3] no variable eliminated in round 3 in 1899 steps
c [elim-1] fully completed in 3 rounds
c [elim-1] transition to [ all 0 rem 0 ] state
c [elim-1] eliminated 2291 = 28% variables out of 8235 scheduled
c [phase-count-1] 123717 negative 92.2% of 134178 except 10461 7.8%
c [phase-count-1] 125886 positive 93.8% of 134178 except 8292 6.2%
c [phase-1] phase bias: 3363 positive 57%, 2581 negative 43%
c [score-distribution-1] 0 pos 0.00%, 0 min 0.00%, 5944 zero 100.00%
c [score-distribution-1] 1 different 0.02% out of total 5944 variables
c [simplification-1] removed 3130 variables 34.5% (5944 remain 64%)
c [simplification-1] removed 9041 irredundant clauses 6.3% (134178 remain 94%)
c [simplification-1] maximum reduction of 34% = max (34%, 6%)
c [simplification-1] large reduction 34% >= 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 12 variables
c [simpleprobe-2] 4081 schedulable variables 69%
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [decomp-4] removed 7 variables
c [simpleprobe-2] 4183 variables remain 71% (1742 retained 29%)
c [simpleprobe-2] removed 7 variables, found 240 hbrs, 0 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 9877 literals 83%
c [treelook-1] scheduling used 300134 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 306725 steps
c [treelook-1] 9816 literals remain 83%
c [treelook-1] 5800 variables remain to probed next time 98%
c [decomp-5] removed 3 variables
c [treelook-1] removed 5 variables, found 145 hbrs
c [basicprobe-1] limit 1072992 based on 134124 irredundant clauses
c [basicprobe-1-0] 525 probes remain 9% after last round
c [basicprobe-1-0] 9 units = 9 failed (100%) + 0 lifted (0%)
c [basicprobe-1-0] removed 9 variables, found 2103 hbrs
c [unhide-2] limit 100000 with penalty 0 = 0 + 0
c [unhide-2-2] 0 units, 0 failed, 825 tauts, 0 hbrs, 381 literals
c [block-1] scheduling all variables this time
c [block-1] scheduled 5911 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 1376 blocked clauses
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 6 clauses out of 6 (100%) of length 22
c [cce-1-1] eliminated 18 clauses out of 18 (100%) of length 21
c [cce-1-1] eliminated 6 clauses out of 6 (100%) of length 20
c [cce-1-1] eliminated 319 clauses out of 515 (62%) of length 13
c [cce-1-1] eliminated 115 clauses out of 867 (13%) of length 12
c [cce-1-1] eliminated 95 clauses out of 181 (52%) of length 11
c [cce-1-1] eliminated 12 clauses out of 236 (5%) of length 10
c [cce-1-1] eliminated 46 clauses out of 1148 (4%) of length 9
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 617 large clauses in 30000386 steps
c [cce-1-1] allowing another 15000193 steps for small clauses
c [cce-1-1] scheduling 14071 clauses = 12299 binary + 1772 ternary
c [cce-1-1] tried to eliminate 3702 small clauses 26%
c [cce-1-1] eliminated 401 binary clauses 3%
c [cce-1-1] eliminated 9 ternary clauses 1%
c [cce-1-1] eliminated 410 small clauses 3%
c [cce-1-1] eliminated 410 small clauses in 30000392 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 1027 covered clauses in round 1
c [cce-1] eliminated 1027 covered clauses in TOTAL during 1 rounds
c [cce-1] 1027 < 1/100 * 132714 = 1327 considered unsuccessful
c [elim-2] scheduling all variables this time
c [elim-2] scheduled 5911 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 36 variables 1% in round 1 in 17162732 steps
c [elim-2-1] backward subsumption/strengthening limit 2837268
c [elim-2-1-1] backward checking 746 touched variables 13%
c [elim-2-1-1] fully completed backward checking in 1 rounds
c [elim-2-1] subsumed 2 and strengthened 11 clauses in 2378715 steps
c [elim-2-1] rescheduled 53 variables 1% by backward subsumption
c [elim-2-2] no variable eliminated in round 2 in 212515 steps
c [elim-2] fully completed in 2 rounds
c [elim-2] transition to [ all 0 rem 0 ] state
c [elim-2] eliminated 36 = 1% variables out of 5911 scheduled
c [elim-2] 36 < 1/100 * 5911 = 59 considered unsuccessful
c [bca-1] limit of 10000000 steps and 263290 added (scaled 2)
c [bca-1] 10828 out of 11752 literals actually usable 92%
c [bca-1] added 73 blocked clauses in 27650 steps
c [sweep-1] limit 1000000 penalty 0 = 0 + 0
c [sweep-1-1] 1761 pos 30.0% + 4114 neg 70.0% = 5875 sched 100.0% ret 0
c [sweep-1-1] 1060839 steps 75 queries 526.93 avg class size
c [sweep-1-1] 1529 decisions 60 SAT calls 61.48 avg env size
c [sweep-1-1] 5228 variables remain 89% (647 retained 11%)
c [decomp-6] removed 274 variables
c [sweep-1-1] removed 274 vars (0 failed, 17 eqs, 2 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 274 vars in TOTAL (1 rounds, 74 queries)
c [phase-count-2] 118419 negative 90.4% of 131055 except 12636 9.6%
c [phase-count-2] 122467 positive 93.4% of 131055 except 8588 6.6%
c [phase-2] phase bias: 29 positive 48%, 31 negative 52%
c [score-distribution-2] 971 pos 17.34%, 0 min 0.00%, 4630 zero 82.66%
c [score-distribution-2] 733 different 13.09% out of total 5601 variables
c [simplification-2] removed 343 variables 5.8% (5601 remain 61%)
c [simplification-2] removed 3123 irredundant clauses 2.3% (131055 remain 92%)
c [simplification-2] maximum reduction of 6% = max (6%, 2%)
c [simplification-2] large reduction 6% >= 5% limit
c [simplification-2] next conflict interval 2000 = 2000/1
c [simplification-2] penalized conflict interval 2000 = 1 * 2000
c [simplification-2] hard conflict limit 13000 (soft 3000 + delta 10000)
c [simplification-2] new conflict limit 3000 (hard 13000)
c 
c [simplification-3] limit 3000 conflicts (hard 13000) hit after 3000 conflicts
c [quatres-1] found 26292 quaternary clauses 31% in total
c [quatres-1-1] removed 1 duplicate quaternary clauses
c [quatres-1-2] added 2 single-self-subsuming ternary resolvents
c [quatres-1-2] added 2 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 5601 free variables schedulable
c [ternres-1] 29 ternary resolvents (0 bin, 29 trn)
c [ternres-1] fully completed ternary resolution
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 837 at-most-one constraints of average size 3.1
c [card-2] found 57 at-most-two constraints of average size 4.2
c [card-2] using previous limit 1000000 for elimination
c [card-2] 894 out of 894 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 438 xors of average arity 3.0
c [gauss-1] connected 1307 occurrences of 541 variables (average 2.4)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] fully completed
c [gauss-1] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-7] removed 2 variables
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] scheduled 10065 literals 90%
c [treelook-2] scheduling used 301780 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] used 332686 steps
c [treelook-2] 10033 literals remain 90%
c [treelook-2] 5467 variables remain to probed next time 98%
c [treelook-2] removed 0 variables, found 219 hbrs
c [transred-1] limit 131055 based on 131055 irredundant clauses
c [transred-1] removed 395 transitive binary clauses
c [block-2] scheduling all variables this time
c [block-2] scheduled 5599 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 0 blocked clauses
c [bca-2] limit of 10000000 steps and 262262 added (scaled 2)
c [bca-2] 10029 out of 11200 literals actually usable 90%
c [bca-2] added 2 blocked clauses in 27855 steps
c [sweep-2] limit 1000000 penalty 0 = 0 + 0
c [sweep-2-1] 2055 pos 41.0% + 2953 neg 59.0% = 5008 sched 89.4% ret 591
c [sweep-2-1] 1033472 steps 52 queries 489.69 avg class size
c [sweep-2-1] 1369 decisions 49 SAT calls 62.08 avg env size
c [sweep-2-1] 4609 variables remain 82% (990 retained 18%)
c [decomp-9] removed 16 variables
c [sweep-2-1] removed 16 vars (0 failed, 5 eqs, 2 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 16 vars in TOTAL (1 rounds, 51 queries)
c [phase-count-3] 118159 negative 90.3% of 130842 except 12683 9.7%
c [phase-count-3] 122175 positive 93.4% of 130842 except 8667 6.6%
c [phase-3] phase bias: 2 positive 67%, 1 negative 33%
c [score-distribution-3] 1217 pos 21.80%, 2 min 0.04%, 4364 zero 78.17%
c [score-distribution-3] 830 different 14.87% out of total 5583 variables
c [simplification-3] removed 18 variables 0.3% (5583 remain 60%)
c [simplification-3] removed 213 irredundant clauses 0.2% (130842 remain 91%)
c [simplification-3] maximum reduction of 0% = max (0%, 0%)
c [simplification-3] full geometric conflict interval increment 20000
c [simplification-3] new conflict interval 20000
c [simplification-3] penalized conflict interval 20000 = 1 * 20000
c [simplification-3] hard conflict limit 33000 (soft 23000 + delta 10000)
c [simplification-3] new conflict limit 23000 (hard 33000)
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.7    5582   130842     10408   10008   1186  2447    9    17   10  56%    137   15   10    1  655%
c i    3.8    5577   130842     10824   10400   1190  2447   10    17   10  56%     88   15   11    2  715%
c i    4.2    5576   130842     14827   14171   1233  2452   10    18   11  56%     36   15   10    2  500%
c i    4.2    5575   130842     15031   14349   1237  2454   10    18   11  56%     27   15   10    2  464%
c 
c [simplification-4] limit 23000 conflicts (hard 33000) hit after 23001 conflicts
c [quatres-2] found 26670 quaternary clauses 30% in total
c [quatres-2-2] added 6 single-self-subsuming ternary resolvents
c [quatres-2-2] added 14 quaternary resolvents
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] all 5574 free variables schedulable
c [ternres-2] 4 ternary resolvents (0 bin, 4 trn)
c [ternres-2] 622 variables remain 11% (4952 retained 89%)
c [decomp-10] removed 25 variables
c [basicprobe-2] limit 5386915 penalty 0 = 0 + 0
c [basicprobe-2-0] 443 sched 8%, 7 failed, 0 lifted, 1019 hbrs
c [decomp-11] removed 90 variables
c [basicprobe-2-1] 1104 sched 20%, 4 failed, 0 lifted, 410 hbrs
c [decomp-12] removed 12 variables
c [basicprobe-2-2] 1092 sched 20%, 0 failed, 0 lifted, 37 hbrs
c [basicprobe-2-3] 1092 sched 20%, 0 failed, 0 lifted, 4 hbrs
c [basicprobe-2-4] 1054 probes remain 19% after last round
c [basicprobe-2-4] 11 units = 11 failed (100%) + 0 lifted (0%)
c [basicprobe-2-4] removed 102 variables, found 1470 hbrs
c [bate-1] eliminated 414 asymmetric tautologies during probing
c [unhide-3] limit 107738 with penalty 1 = 1 + 0
c [unhide-3-3] 0 units, 0 failed, 596 tauts, 0 hbrs, 5925 literals
c [transred-2] limit 1077383 with penalty 0 = 0 + 0
c [transred-2] removed 733 transitive binary clauses
c [cce-2] limit of 15000000 steps penalty 1 = 1 + 0
c [cce-2-1] eliminated 4 clauses out of 4 (100%) of length 22
c [cce-2-1] eliminated 3 clauses out of 250 (1%) of length 13
c [cce-2-1] eliminated 12 clauses out of 697 (2%) of length 12
c [cce-2-1] eliminated 12 clauses out of 110 (11%) of length 11
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] eliminated 31 large clauses in 15000000 steps
c [cce-2-1] allowing another 7500000 steps for small clauses
c [cce-2-1] scheduling 41065 clauses = 10772 binary + 30293 ternary
c [cce-2-1] tried to eliminate 2090 small clauses 5%
c [cce-2-1] eliminated 25 binary clauses 0%
c [cce-2-1] eliminated 97 ternary clauses 0%
c [cce-2-1] eliminated 122 small clauses 0%
c [cce-2-1] eliminated 122 small clauses in 15000722 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 153 covered clauses in round 1
c [cce-2] eliminated 153 covered clauses in TOTAL during 1 rounds
c [cce-2] 153 < 1/100 * 129224 = 1292 considered unsuccessful
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 5456 variables 100%
c [elim-3] limit of 10773830 steps penalty 1 = 1 + 0
c [elim-3] rescheduling of touched variables disabled
c [elim-3] incomplete 802 not tried 15% in round 1
c [elim-3] transition to [ all 1 rem 1 ] state
c [elim-3] eliminated 41 = 1% variables out of 5456 scheduled
c [elim-3] 41 < 1/100 * 5456 = 54 considered unsuccessful
c [bca-3] limit of 10000000 steps and 258271 added (scaled 2)
c [bca-3] 9479 out of 10832 literals actually usable 88%
c [bca-3] added 17 blocked clauses in 45976 steps
c [sweep-3] limit 1000000 penalty 0 = 0 + 0
c [sweep-3-1] 2291 pos 51.0% + 2201 neg 49.0% = 4492 sched 83.0% ret 923
c [sweep-3-1] 1158326 steps 64 queries 518.14 avg class size
c [sweep-3-1] 1595 decisions 63 SAT calls 61.03 avg env size
c [sweep-3-1] 3989 variables remain 74% (1426 retained 26%)
c [decomp-15] removed 8 variables
c [sweep-3-1] removed 8 vars (0 failed, 4 eqs, 2 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 8 vars in TOTAL (1 rounds, 63 queries)
c [phase-count-4] 115672 negative 89.8% of 128865 except 13193 10.2%
c [phase-count-4] 119684 positive 92.9% of 128865 except 9181 7.1%
c [phase-4] phase bias: 4 positive 50%, 4 negative 50%
c [score-distribution-4] 603 pos 11.15%, 762 min 14.09%, 4042 zero 74.75%
c [score-distribution-4] 529 different 9.78% out of total 5407 variables
c [simplification-4] removed 167 variables 3.0% (5407 remain 59%)
c [simplification-4] removed 1977 irredundant clauses 1.5% (128865 remain 90%)
c [simplification-4] maximum reduction of 3% = max (3%, 2%)
c [simplification-4] geometric conflict interval increment 5000 = 20000 / 4
c [simplification-4] new conflict interval 25000
c [simplification-4] penalized conflict interval 25000 = 1 * 25000
c [simplification-4] hard conflict limit 60501 (soft 48001 + delta 12500)
c [simplification-4] new conflict limit 48001 (hard 60501)
c 
c [simplification-5] limit 48001 conflicts (hard 60501) hit after 48003 conflicts
c [quatres-3] found 26959 quaternary clauses 30% in total
c [quatres-3-1] removed 1 duplicate quaternary clauses
c [quatres-3-2] added 5 single-self-subsuming ternary resolvents
c [quatres-3-2] added 14 quaternary resolvents
c [ternres-3] limit 4000000 with penalty 0 = 0 + 0
c [ternres-3] 598 schedulable variables 11%
c [ternres-3] 1 ternary resolvents (0 bin, 1 trn)
c [ternres-3] fully completed ternary resolution
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] extracted 176 xors of average arity 3.0
c [gauss-2] connected 527 occurrences of 350 variables (average 1.5)
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] fully completed
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-16] removed 2 variables
c [simpleprobe-3] 3830 schedulable variables 71%
c [simpleprobe-3] limit 11905657 penalty 0 = 0 + 0
c [decomp-17] removed 16 variables
c [simpleprobe-3] 2894 variables remain 54% (2495 retained 46%)
c [simpleprobe-3] removed 16 variables, found 883 hbrs, 0 units
c [transred-3] limit 2000000 with penalty 0 = 0 + 0
c [transred-3] removed 687 transitive binary clauses
c [block-3] scheduling all variables this time
c [block-3] scheduled 5389 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 3 blocked clauses
c [block-3] 3 < 1/100 * 128803 = 1288 considered unsuccessful
c [bca-4] limit of 10000000 steps and 258146 added (scaled 2)
c [bca-4] 9160 out of 10780 literals actually usable 85%
c [bca-4] added 0 blocked clauses in 68536 steps
c [sweep-4] limit 1000000 penalty 0 = 0 + 0
c [sweep-4-1] 2053 pos 51.7% + 1919 neg 48.3% = 3972 sched 73.7% ret 1417
c [sweep-4-1] 1279837 steps 50 queries 532.96 avg class size
c [sweep-4-1] 1414 decisions 47 SAT calls 73.34 avg env size
c [sweep-4-1] 3739 variables remain 69% (1650 retained 31%)
c [decomp-18] removed 5 variables
c [sweep-4-1] removed 5 vars (0 failed, 2 eqs, 1 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 5 vars in TOTAL (1 rounds, 49 queries)
c [phase-count-5] 115563 negative 89.7% of 128799 except 13236 10.3%
c [phase-count-5] 119591 positive 92.9% of 128799 except 9208 7.1%
c [phase-5] phase bias: 1 positive 100%, 0 negative 0%
c [score-distribution-5] 565 pos 10.49%, 995 min 18.48%, 3824 zero 71.03%
c [score-distribution-5] 477 different 8.86% out of total 5384 variables
c [simplification-5] removed 23 variables 0.4% (5384 remain 58%)
c [simplification-5] removed 66 irredundant clauses 0.1% (128799 remain 90%)
c [simplification-5] maximum reduction of 0% = max (0%, 0%)
c [simplification-5] full geometric conflict interval increment 25000
c [simplification-5] new conflict interval 50000
c [simplification-5] penalized conflict interval 50000 = 1 * 50000
c [simplification-5] hard conflict limit 123003 (soft 98003 + delta 25000)
c [simplification-5] new conflict limit 98003 (hard 123003)
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 -   13.1    5384   128799     58372   17777   1508  2818   11    18   12  62%    480    8   12    6  178%
c 
c [simplification-6] limit 98003 conflicts (hard 123003) hit after 98003 conflicts
c [quatres-4] found 27437 quaternary clauses 30% in total
c [quatres-4-2] added 10 single-self-subsuming ternary resolvents
c [quatres-4-2] added 19 quaternary resolvents
c [ternres-4] limit 7089373 with penalty 0 = 0 + 0
c [ternres-4] all 5384 free variables schedulable
c [ternres-4] 33 ternary resolvents (0 bin, 33 trn)
c [ternres-4] fully completed ternary resolution
c [card-3] limit 886171 penalty 2 = 2 + 0
c [card-3] found 663 at-most-one constraints of average size 3.1
c [card-3] found 34 at-most-two constraints of average size 4.3
c [card-3] using previous limit 886171 for elimination
c [card-3] 697 out of 697 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 275 transitive binary clauses
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 21268110 penalty 0 = 0 + 0
c [sweep-5-1] 1936 pos 51.8% + 1800 neg 48.2% = 3736 sched 69.4% ret 1648
c [sweep-5-1] 18088541 steps 941 queries 40.90 avg class size
c [sweep-5-1] 20927 decisions 888 SAT calls 54.59 avg env size
c [sweep-5-1] fully completed sweeping round
c [decomp-20] removed 63 variables
c [sweep-5-1] removed 63 vars (0 failed, 84 eqs, 20 impls)
c [sweep-5-2] 2900 pos 54.5% + 2421 neg 45.5% = 5321 sched 100.0% ret 0
c [sweep-5-2] 3282964 steps 85 queries 523.31 avg class size
c [sweep-5-2] 2192 decisions 84 SAT calls 76.07 avg env size
c [sweep-5-2] 4499 variables remain 85% (822 retained 15%)
c [decomp-21] removed 3 variables
c [sweep-5-2] removed 3 vars (0 failed, 4 eqs, 0 impls)
c [sweep-5] removed 66 vars in TOTAL (2 rounds, 1024 queries)
c [phase-count-6] 115514 negative 89.7% of 128759 except 13245 10.3%
c [phase-count-6] 119547 positive 92.8% of 128759 except 9212 7.2%
c [phase-6] phase bias: 0 positive 0%, 0 negative 0%
c [score-distribution-6] 1592 pos 29.94%, 672 min 12.64%, 3054 zero 57.43%
c [score-distribution-6] 1090 different 20.50% out of total 5318 variables
c [simplification-6] removed 66 variables 1.2% (5318 remain 58%)
c [simplification-6] removed 40 irredundant clauses 0.0% (128759 remain 90%)
c [simplification-6] maximum reduction of 1% = max (1%, 0%)
c [simplification-6] geometric conflict interval increment 25000 = 50000 / 2
c [simplification-6] new conflict interval 75000
c [simplification-6] penalized conflict interval 75000 = 1 * 75000
c [simplification-6] hard conflict limit 210503 (soft 173003 + delta 37500)
c [simplification-6] new conflict limit 173003 (hard 210503)
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 -   20.7    5318   128759    100388   24876   1745  2839   11    18   13  64%    738    4   12    9  141%
c -   26.5    5318   128759    142872   32047   1875  2851   11    16   13  66%    874    2   11    9  119%
c 
c [simplification-7] limit 173003 conflicts (hard 210503) hit after 177444 conflicts
c [quatres-5] found 28169 quaternary clauses 29% in total
c [quatres-5-2] added 10 single-self-subsuming ternary resolvents
c [quatres-5-2] added 51 quaternary resolvents
c [ternres-5] limit 13499861 with penalty 0 = 0 + 0
c [ternres-5] all 5318 free variables schedulable
c [ternres-5] 28 ternary resolvents (0 bin, 28 trn)
c [ternres-5] fully completed ternary resolution
c [decomp-22] removed 1 variables
c [treelook-3] limit 674993 penalty 1 = 1 + 0 boost 1
c [treelook-3] scheduled 10581 literals 100%
c [treelook-3] scheduling used 462560 steps
c [treelook-3] scheduled completely
c [treelook-3] limit 674993 penalty 1 = 1 + 0 boost 1
c [treelook-3] used 693249 steps
c [treelook-3] 10514 literals remain 99%
c [treelook-3] 5185 variables remain to probed next time 98%
c [treelook-3] removed 1 variables, found 152 hbrs
c [unhide-4] limit 674993 with penalty 2 = 2 + 0
c [unhide-4-4] 0 units, 0 failed, 371 tauts, 0 hbrs, 12519 literals
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 206 transitive binary clauses
c [cce-3] limit of 16874826 steps penalty 2 = 2 + 0
c [cce-3-1] eliminated 38 clauses out of 246 (15%) of length 13
c [cce-3-1] eliminated 52 clauses out of 685 (8%) of length 12
c [cce-3-1] eliminated 18 clauses out of 97 (19%) of length 11
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 108 large clauses in 16874884 steps
c [cce-3-1] allowing another 8437442 steps for small clauses
c [cce-3-1] scheduling 14081 clauses = 10539 binary + 3542 ternary
c [cce-3-1] tried to eliminate 1680 small clauses 12%
c [cce-3-1] eliminated 135 binary clauses 1%
c [cce-3-1] eliminated 147 ternary clauses 4%
c [cce-3-1] eliminated 282 small clauses 2%
c [cce-3-1] eliminated 282 small clauses in 16875214 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 390 covered clauses in round 1
c [cce-3] eliminated 390 covered clauses in TOTAL during 1 rounds
c [cce-3] 390 < 1/100 * 128506 = 1285 considered unsuccessful
c [elim-4] 787 variables 15% will be scheduled this time
c [elim-4] scheduled 787 variables 15%
c [elim-4] boosting limit by 20
c [elim-4] limit of 1349986120 steps penalty 2 = 2 + 0
c [elim-4] rescheduling of touched variables disabled
c [elim-4-1] no variable eliminated in round 1 in 115911022 steps
c [elim-4] fully completed in 1 rounds
c [elim-4] transition to [ all 0 rem 0 ] state
c [elim-4] eliminated 0 = 0% variables out of 787 scheduled
c [bca-5] limit of 10000000 steps and 255130 added (scaled 2)
c [bca-5] 7807 out of 10634 literals actually usable 73%
c [bca-5] added 8 blocked clauses in 80987 steps
c [sweep-6] limit 4049958 penalty 0 = 0 + 0
c [sweep-6-1] 2504 pos 55.7% + 1993 neg 44.3% = 4497 sched 84.6% ret 819
c [sweep-6-1] 4085826 steps 109 queries 298.26 avg class size
c [sweep-6-1] 3506 decisions 113 SAT calls 69.27 avg env size
c [sweep-6-1] 3544 variables remain 67% (1772 retained 33%)
c [decomp-24] removed 11 variables
c [sweep-6-1] removed 11 vars (0 failed, 9 eqs, 1 impls)
c [sweep-6] removed 11 vars in TOTAL (1 rounds, 108 queries)
c [phase-count-7] 114149 negative 89.7% of 127289 except 13140 10.3%
c [phase-count-7] 118183 positive 92.8% of 127289 except 9106 7.2%
c [phase-7] phase bias: 0 positive 0%, 0 negative 0%
c [score-distribution-7] 926 pos 17.46%, 1757 min 33.12%, 2622 zero 49.43%
c [score-distribution-7] 674 different 12.70% out of total 5305 variables
c [simplification-7] removed 13 variables 0.2% (5305 remain 57%)
c [simplification-7] removed 1470 irredundant clauses 1.1% (127289 remain 89%)
c [simplification-7] maximum reduction of 1% = max (0%, 1%)
c [simplification-7] geometric conflict interval increment 37500 = 75000 / 2
c [simplification-7] new conflict interval 112500
c [simplification-7] penalized conflict interval 112500 = 1 * 112500
c [simplification-7] hard conflict limit 346194 (soft 289944 + delta 56250)
c [simplification-7] new conflict limit 289944 (hard 346194)
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 -   33.9    5305   127289    181088   34196   2102  2687   11    18   13  62%    940    3   12   10  125%
c -   38.3    5305   127289    221200   38844   2144  2690   10    14   14  71%    979   -0   10   10  101%
c i   41.4    5304   127289    249381   63991   2296  2714   10    15   26  66%    995    0    6   10   67%
c -   43.0    5300   127289    259387   41297   2310  2715   11    18   23  60%  -2194    3   12   10  122%
c -   48.1    5300   127289    297323   42468   2351  2717   11    15   23  71%   -780    0   13   10  127%
c -   52.5    5300   127289    337251   46933   2377  2721    9    11   23  77%     43   -3    8   10   85%
c 
c [simplification-8] limit 289944 conflicts (hard 346194) hit after 346196 conflicts
c [quatres-6] found 28655 quaternary clauses 27% in total
c [quatres-6-1] removed 4 duplicate quaternary clauses
c [quatres-6-2] added 26 single-self-subsuming ternary resolvents
c [quatres-6-2] added 39 quaternary resolvents
c [ternres-6] limit 27699743 with penalty 0 = 0 + 0
c [ternres-6] all 5300 free variables schedulable
c [ternres-6] 60 ternary resolvents (1 bin, 59 trn)
c [ternres-6] fully completed ternary resolution
c [gauss-3] limit 1384987 penalty 2 = 2 + 0
c [gauss-3] extracted 264 xors of average arity 2.9
c [gauss-3] connected 778 occurrences of 424 variables (average 1.8)
c [gauss-3] limit 1384987 penalty 2 = 2 + 0
c [gauss-3] fully completed
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-25] removed 6 variables
c [basicprobe-3] limit 138498718 penalty 0 = 0 + 0
c [basicprobe-3-0] 1021 sched 19%, 8 failed, 0 lifted, 337 hbrs
c [decomp-26] removed 14 variables
c [basicprobe-3-1] 1058 sched 20%, 2 failed, 0 lifted, 79 hbrs
c [decomp-27] removed 2 variables
c [basicprobe-3-2] 1058 sched 20%, 0 failed, 0 lifted, 6 hbrs
c [basicprobe-3-3] 1058 sched 20%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-3-3] fully completed probing
c [basicprobe-3-3] 10 units = 10 failed (100%) + 0 lifted (0%)
c [basicprobe-3-3] removed 16 variables, found 422 hbrs
c [bate-2] eliminated 23 asymmetric tautologies during probing
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 221 transitive binary clauses
c [block-4] scheduling all variables this time
c [block-4] scheduled 5278 variables 100%
c [block-4] limit of 69249359 steps penalty 2 = 2 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 691 blocked clauses
c [block-4] 691 < 1/100 * 127035 = 1270 considered unsuccessful
c [bca-6] limit of 10000000 steps and 253238 added (scaled 2)
c [bca-6] 7846 out of 10520 literals actually usable 75%
c [bca-6] added 0 blocked clauses in 72702 steps
c [sweep-7] limit 8309923 penalty 0 = 0 + 0
c [sweep-7-1] 1913 pos 54.4% + 1605 neg 45.6% = 3518 sched 66.9% ret 1741
c [sweep-7-1] 8768817 steps 371 queries 67.79 avg class size
c [sweep-7-1] 8930 decisions 374 SAT calls 54.00 avg env size
c [sweep-7-1] 1218 variables remain 23% (4039 retained 77%)
c [decomp-29] removed 26 variables
c [sweep-7-1] removed 26 vars (0 failed, 24 eqs, 6 impls)
c [sweep-7] removed 26 vars in TOTAL (1 rounds, 370 queries)
c [phase-count-8] 113029 negative 89.5% of 126292 except 13263 10.5%
c [phase-count-8] 117054 positive 92.7% of 126292 except 9238 7.3%
c [phase-8] phase bias: 0 positive 0%, 0 negative 0%
c [score-distribution-8] 1099 pos 21.00%, 1714 min 32.75%, 2420 zero 46.24%
c [score-distribution-8] 762 different 14.56% out of total 5233 variables
c [simplification-8] removed 67 variables 1.3% (5233 remain 57%)
c [simplification-8] removed 997 irredundant clauses 0.8% (126292 remain 88%)
c [simplification-8] maximum reduction of 1% = max (1%, 1%)
c [simplification-8] geometric conflict interval increment 56250 = 112500 / 2
c [simplification-8] new conflict interval 168750
c [simplification-8] penalized conflict interval 168750 = 1 * 168750
c [simplification-8] hard conflict limit 599321 (soft 514946 + delta 84375)
c [simplification-8] new conflict limit 514946 (hard 599321)
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 -   59.3    5233   126292    376392   48101   2280  2730    9    12   14  80%    484   -2    9   10   95%
c -   64.3    5233   126292    416238   50593   2316  2738   11    15   22  73%    730    1   12   10  118%
c -   69.3    5233   126292    454391   51604   2356  2739   10    15   22  71%    860   -0   10   10  101%
c -   74.3    5233   126292    496713   54690   2387  2741   10    13   23  77%    938   -2   10   10   96%
c 
c [simplification-9] limit 514946 conflicts (hard 599321) hit after 514946 conflicts
c [quatres-7] found 29136 quaternary clauses 26% in total
c [quatres-7-1] removed 2 duplicate quaternary clauses
c [quatres-7-2] added 15 single-self-subsuming ternary resolvents
c [quatres-7-2] added 26 quaternary resolvents
c [ternres-7] limit 43717603 with penalty 0 = 0 + 0
c [ternres-7] all 5233 free variables schedulable
c [ternres-7] 76 ternary resolvents (1 bin, 75 trn)
c [ternres-7] fully completed ternary resolution
c [decomp-30] removed 2 variables
c [simpleprobe-4] 2804 schedulable variables 54%
c [simpleprobe-4] limit 174870415 penalty 0 = 0 + 0
c [decomp-31] removed 77 variables
c [simpleprobe-4] fully completed simple probing
c [simpleprobe-4] removed 77 variables, found 3167 hbrs, 1 units
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 1585 transitive binary clauses
c [transred-7] found 1 units
c [sweep-8] limit 13115281 penalty 0 = 0 + 0
c [sweep-8-1] 600 pos 50.0% + 601 neg 50.0% = 1201 sched 23.3% ret 3952
c [sweep-8-1] 6928779 steps 523 queries 18.81 avg class size
c [sweep-8-1] 12737 decisions 513 SAT calls 57.13 avg env size
c [sweep-8-1] fully completed sweeping round
c [decomp-32] removed 13 variables
c [sweep-8-1] removed 13 vars (0 failed, 24 eqs, 6 impls)
c [sweep-8-2] 2878 pos 56.0% + 2262 neg 44.0% = 5140 sched 100.0% ret 0
c [sweep-8-2] 6237871 steps 158 queries 244.38 avg class size
c [sweep-8-2] 4570 decisions 160 SAT calls 65.20 avg env size
c [sweep-8-2] 3201 variables remain 62% (1939 retained 38%)
c [decomp-33] removed 2 variables
c [sweep-8-2] removed 2 vars (0 failed, 3 eqs, 0 impls)
c [sweep-8] removed 15 vars in TOTAL (2 rounds, 679 queries)
c [score-distribution-9] 1286 pos 25.03%, 1667 min 32.44%, 2185 zero 42.53%
c [score-distribution-9] 925 different 18.00% out of total 5138 variables
c [simplification-9] removed 95 variables 1.8% (5138 remain 56%)
c [simplification-9] removed 495 irredundant clauses 0.4% (125797 remain 88%)
c [simplification-9] maximum reduction of 2% = max (2%, 0%)
c [simplification-9] geometric conflict interval increment 56250 = 168750 / 3
c [simplification-9] new conflict interval 225000
c [simplification-9] penalized conflict interval 225000 = 1 * 225000
c [simplification-9] hard conflict limit 852446 (soft 739946 + delta 112500)
c [simplification-9] new conflict limit 739946 (hard 852446)
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 -   81.3    5138   125797    538616   57506   2486  4372   10    13   15  75%    979   -1   10   10  105%
c i   82.1    5137   125797    543761   61472   2517  4376    8    10   17  78%    982   -4    5   10   54%
c i   84.0    5133   125797    559138   74400   2586  4381    8    11   18  77%  -2705   -3    6   10   61%
c -   88.0    5123   125797    583032   60286   2604  4383   10    16   15  65%  -1735    2   10   10  103%
c -   94.3    5123   125797    626879   63057   2627  4387   10    14   25  69%   -389    0    9   10   87%
c -  100.6    5123   125797    671280   64637   2670  4389   11    17   25  64%    306    1   11   10  105%
c -  106.6    5123   125797    717610   68307   2691  4392    9    11   25  80%    670   -3    7   10   77%
c i  107.3    5122   125797    723288   73106   2726  4403    8    10   28  78%    699   -4    5   10   55%
c -  114.3    5119   125797    762817   69127   2768  4407   10    13   25  75%   -579   -2   12   10  123%
c 
c [simplification-10] limit 739946 conflicts (hard 852446) hit after 792188 conflicts
c [quatres-8] found 29309 quaternary clauses 24% in total
c [quatres-8-1] removed 1 duplicate quaternary clauses
c [quatres-8-2] added 42 single-self-subsuming ternary resolvents
c [quatres-8-2] added 18 quaternary resolvents
c [ternres-8] limit 73519557 with penalty 0 = 0 + 0
c [ternres-8] all 5119 free variables schedulable
c [ternres-8] 58 ternary resolvents (1 bin, 57 trn)
c [ternres-8] fully completed ternary resolution
c [card-4] limit 4594972 penalty 3 = 3 + 0
c [card-4] found 604 at-most-one constraints of average size 3.2
c [card-4] found 68 at-most-two constraints of average size 4.2
c [card-4] using previous limit 4594972 for elimination
c [card-4] 671 out of 672 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [decomp-34] removed 20 variables
c [treelook-4] limit 7351955 penalty 0 = 0 + 0 boost 1
c [treelook-4] scheduled 10191 literals 100%
c [treelook-4] scheduling used 513951 steps
c [treelook-4] scheduled completely
c [treelook-4] limit 7351955 penalty 0 = 0 + 0 boost 1
c [treelook-4] used 7354903 steps
c [treelook-4] 8834 literals remain 86%
c [treelook-4] 4889 variables remain to probed next time 96%
c [decomp-35] removed 5 variables
c [treelook-4] removed 6 variables, found 1022 hbrs
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 1167 transitive binary clauses
c [transred-8] found 1 units
c [bca-7] limit of 10000000 steps and 250906 added (scaled 2)
c [bca-7] 6852 out of 10224 literals actually usable 67%
c [bca-7] added 0 blocked clauses in 105376 steps
c [sweep-9] limit 22055867 penalty 0 = 0 + 0
c [sweep-9-1] 1719 pos 53.9% + 1469 neg 46.1% = 3188 sched 62.4% ret 1923
c [sweep-9-1] 17635431 steps 788 queries 28.69 avg class size
c [sweep-9-1] 20185 decisions 801 SAT calls 57.24 avg env size
c [sweep-9-1] fully completed sweeping round
c [decomp-36] removed 20 variables
c [sweep-9-1] removed 20 vars (0 failed, 25 eqs, 1 impls)
c [sweep-9-2] 2847 pos 55.9% + 2244 neg 44.1% = 5091 sched 100.0% ret 0
c [sweep-9-2] 5513073 steps 110 queries 381.73 avg class size
c [sweep-9-2] 4317 decisions 120 SAT calls 74.97 avg env size
c [sweep-9-2] 3295 variables remain 65% (1796 retained 35%)
c [decomp-37] removed 8 variables
c [sweep-9-2] removed 8 vars (0 failed, 9 eqs, 0 impls)
c [sweep-9] removed 28 vars in TOTAL (2 rounds, 896 queries)
c [score-distribution-10] 1677 pos 32.99%, 1396 min 27.46%, 2010 zero 39.54%
c [score-distribution-10] 1042 different 20.50% out of total 5083 variables
c [simplification-10] removed 36 variables 0.7% (5083 remain 55%)
c [simplification-10] removed 620 irredundant clauses 0.5% (125177 remain 87%)
c [simplification-10] maximum reduction of 1% = max (1%, 0%)
c [simplification-10] geometric conflict interval increment 112500 = 225000 / 2
c [simplification-10] new conflict interval 337500
c [simplification-10] penalized conflict interval 337500 = 1 * 337500
c [simplification-10] hard conflict limit 1298438 (soft 1129688 + delta 168750)
c [simplification-10] new conflict limit 1129688 (hard 1298438)
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 -  123.0    5083   125177    810424   69661   2540  4167    9    12   16  75%    249   -3    9   10   93%
c -  130.1    5083   125177    858317   72135   2571  4170   10    22   26  44%    651    5    9   10   89%
c -  136.9    5083   125177    904924   74248   2627  4172   10    16   27  64%    841   -4    9   10   92%
c -  143.5    5083   125177    953662   77622   2713  4188    9    19   27  50%    937   -4    8   10   83%
c -  150.8    5083   125177   1001403   79823   2820  4200   11    33   27  33%    982    8   12   10  122%
c -  158.3    5083   125177   1049793   83201   2958  4224   11    35   27  30%   1004    5   12   10  113%
c -  166.7    5083   125177   1098744   86552   3092  4254   12    35   28  33%   1014    2   12   11  106%
c 
c [simplification-11] limit 1129688 conflicts (hard 1298438) hit after 1134266 conflicts
c [quatres-9] found 30563 quaternary clauses 22% in total
c [quatres-9-1] removed 6 duplicate quaternary clauses
c [quatres-9-2] added 73 single-self-subsuming ternary resolvents
c [quatres-9-2] added 96 quaternary resolvents
c [ternres-9] limit 105329624 with penalty 0 = 0 + 0
c [ternres-9] all 5083 free variables schedulable
c [ternres-9] 3825 ternary resolvents (45 bin, 3780 trn)
c [ternres-9] fully completed ternary resolution
c [basicprobe-4] limit 400000000 penalty 0 = 0 + 0
c [basicprobe-4-0] 938 sched 19%, 14 failed, 1 lifted, 479 hbrs
c [decomp-39] removed 17 variables
c [basicprobe-4-1] 943 sched 19%, 7 failed, 0 lifted, 182 hbrs
c [decomp-40] removed 7 variables
c [basicprobe-4-2] 943 sched 19%, 3 failed, 0 lifted, 94 hbrs
c [decomp-41] removed 3 variables
c [basicprobe-4-3] 942 sched 19%, 0 failed, 0 lifted, 16 hbrs
c [basicprobe-4-4] 942 sched 19%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-4-4] fully completed probing
c [basicprobe-4-4] 25 units = 24 failed (96%) + 1 lifted (4%)
c [basicprobe-4-4] removed 27 variables, found 771 hbrs
c [bate-3] eliminated 108 asymmetric tautologies during probing
c [unhide-5] limit 2500000 with penalty 3 = 3 + 0
c [unhide-5-5] 0 units, 0 failed, 1339 tauts, 0 hbrs, 24390 literals
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 559 transitive binary clauses
c [cce-4] boosting limit by 10
c [cce-4] limit of 658310150 steps penalty 3 = 3 + 0
c [cce-4-1] eliminated 8 clauses out of 198 (4%) of length 13
c [cce-4-1] eliminated 21 clauses out of 625 (3%) of length 12
c [cce-4-1] eliminated 19 clauses out of 96 (20%) of length 11
c [cce-4-1] eliminated 3 clauses out of 228 (1%) of length 10
c [cce-4-1] eliminated 5 clauses out of 1096 (0%) of length 9
c [cce-4-1] eliminated 135 clauses out of 3010 (4%) of length 8
c [cce-4-1] eliminated 277 clauses out of 7503 (4%) of length 7
c [cce-4-1] eliminated 939 clauses out of 17346 (5%) of length 6
c [cce-4-1] eliminated 1427 clauses out of 27235 (5%) of length 5
c [cce-4-1] eliminated 1145 clauses out of 25141 (5%) of length 4
c [cce-4-1] incomplete large round (ATE)
c [cce-4-1] eliminated 3979 large clauses in 658310159 steps
c [cce-4-1] allowing another 329155079 steps for small clauses
c [cce-4-1] scheduling 38177 clauses = 9976 binary + 28201 ternary
c [cce-4-1] tried to eliminate 38177 small clauses 100%
c [cce-4-1] eliminated 242 binary clauses 2%
c [cce-4-1] eliminated 1530 ternary clauses 5%
c [cce-4-1] eliminated 1772 small clauses 5%
c [cce-4-1] eliminated 1772 small clauses in 461792303 steps
c [cce-4-1] completed small round (ATE)
c [cce-4-1] eliminated 5751 covered clauses in round 1
c [cce-4-2] incomplete large round (ATE)
c [cce-4-2] allowing another 98258934 steps for small clauses
c [cce-4-2] scheduling 36405 clauses = 9734 binary + 26671 ternary
c [cce-4-2] tried to eliminate 28397 small clauses 78%
c [cce-4-2] incomplete small round (ATE)
c [cce-4-2] eliminated 0 covered clauses in round 2
c [cce-4] eliminated 5751 covered clauses in TOTAL during 2 rounds
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 5056 variables 100%
c [elim-5] limit of 100000000 steps penalty 3 = 3 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5] incomplete 175 not tried 3% in round 1
c [elim-5] transition to [ all 1 rem 1 ] state
c [elim-5] eliminated 73 = 1% variables out of 5056 scheduled
c [sweep-10] limit 31598887 penalty 0 = 0 + 0
c [sweep-10-1] 1785 pos 55.2% + 1447 neg 44.8% = 3232 sched 64.9% ret 1751
c [sweep-10-1] 18478491 steps 705 queries 13.35 avg class size
c [sweep-10-1] 20028 decisions 730 SAT calls 68.12 avg env size
c [sweep-10-1] fully completed sweeping round
c [decomp-43] removed 45 variables
c [sweep-10-1] removed 45 vars (0 failed, 52 eqs, 6 impls)
c [sweep-10-2] 2776 pos 56.2% + 2162 neg 43.8% = 4938 sched 100.0% ret 0
c [sweep-10-2] 13152018 steps 298 queries 57.37 avg class size
c [sweep-10-2] 10992 decisions 313 SAT calls 82.56 avg env size
c [sweep-10-2] 1339 variables remain 27% (3596 retained 73%)
c [decomp-44] removed 28 variables
c [sweep-10-2] removed 28 vars (0 failed, 30 eqs, 3 impls)
c [sweep-10] removed 73 vars in TOTAL (2 rounds, 1001 queries)
c [score-distribution-11] 2003 pos 40.79%, 1145 min 23.32%, 1762 zero 35.89%
c [score-distribution-11] 1229 different 25.03% out of total 4910 variables
c [simplification-11] removed 173 variables 3.4% (4910 remain 53%)
c [simplification-11] removed 7867 irredundant clauses 6.3% (117310 remain 82%)
c [simplification-11] maximum reduction of 6% = max (3%, 6%)
c [simplification-11] large reduction 6% >= 5% limit
c [simplification-11] next conflict interval 11342 = min (1134266/100, 337500)
c [simplification-11] penalized conflict interval 11342 = 1 * 11342
c [simplification-11] hard conflict limit 1155608 (soft 1145608 + delta 10000)
c [simplification-11] new conflict limit 1145608 (hard 1155608)
c 
c [simplification-12] limit 1145608 conflicts (hard 1155608) hit after 1145608 conflicts
c [quatres-10] found 28417 quaternary clauses 21% in total
c [quatres-10-1] removed 10 duplicate quaternary clauses
c [quatres-10-2] added 194 single-self-subsuming ternary resolvents
c [quatres-10-2] added 33 quaternary resolvents
c [ternres-10] limit 106404195 with penalty 0 = 0 + 0
c [ternres-10] all 4910 free variables schedulable
c [ternres-10] 3522 ternary resolvents (29 bin, 3493 trn)
c [ternres-10] fully completed ternary resolution
c [gauss-4] limit 2660104 penalty 3 = 3 + 0
c [gauss-4] extracted 179 xors of average arity 2.9
c [gauss-4] connected 517 occurrences of 334 variables (average 1.5)
c [gauss-4] limit 2660104 penalty 3 = 3 + 0
c [gauss-4] fully completed
c [gauss-4] exported 0 unary, 0 binary and 0 ternary equations
c [simpleprobe-5] all 4910 free variables schedulable
c [simpleprobe-5] limit 200000000 penalty 0 = 0 + 0
c [decomp-46] removed 15 variables
c [simpleprobe-5] fully completed simple probing
c [simpleprobe-5] removed 15 variables, found 2668 hbrs, 3 units
c [transred-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 1674 transitive binary clauses
c [block-5] scheduling all variables this time
c [block-5] scheduled 4895 variables 100%
c [block-5] limit of 100000000 steps penalty 3 = 3 + 0
c [block-5] fully completed
c [block-5] transition to [ all 0 rem 0 ] state
c [block-5] eliminated 7 blocked clauses
c [block-5] 7 < 1/100 * 115919 = 1159 considered unsuccessful
c [sweep-11] boosting sweeping limit by 10
c [sweep-11] limit 319212580 penalty 0 = 0 + 0
c [sweep-11-1] 716 pos 53.9% + 613 neg 46.1% = 1329 sched 27.2% ret 3566
c [sweep-11-1] 10630635 steps 476 queries 17.21 avg class size
c [sweep-11-1] 14160 decisions 513 SAT calls 73.86 avg env size
c [sweep-11-1] fully completed sweeping round
c [decomp-47] removed 33 variables
c [sweep-11-1] removed 33 vars (0 failed, 37 eqs, 1 impls)
c [sweep-11-2] 2750 pos 56.6% + 2112 neg 43.4% = 4862 sched 100.0% ret 0
c [sweep-11-2] 26923667 steps 712 queries 28.69 avg class size
c [sweep-11-2] 22904 decisions 753 SAT calls 76.52 avg env size
c [sweep-11-2] fully completed sweeping round
c [decomp-48] removed 55 variables
c [sweep-11-2] removed 55 vars (0 failed, 60 eqs, 2 impls)
c [sweep-11-3] 2707 pos 56.3% + 2100 neg 43.7% = 4807 sched 100.0% ret 0
c [sweep-11-3] 22436984 steps 732 queries 17.89 avg class size
c [sweep-11-3] 21497 decisions 749 SAT calls 72.87 avg env size
c [sweep-11-3] fully completed sweeping round
c [decomp-49] removed 37 variables
c [sweep-11-3] removed 37 vars (0 failed, 48 eqs, 4 impls)
c [sweep-11] removed 125 vars in TOTAL (3 rounds, 1917 queries)
c [score-distribution-12] 1683 pos 35.28%, 1528 min 32.03%, 1559 zero 32.68%
c [score-distribution-12] 1054 different 22.10% out of total 4770 variables
c [simplification-12] removed 140 variables 2.9% (4770 remain 52%)
c [simplification-12] removed 1811 irredundant clauses 1.5% (115499 remain 81%)
c [simplification-12] maximum reduction of 3% = max (3%, 2%)
c [simplification-12] geometric conflict interval increment 84375 = 337500 / 4
c [simplification-12] new conflict interval 421875
c [simplification-12] penalized conflict interval 421875 = 1 * 421875
c [simplification-12] hard conflict limit 1778420 (soft 1567483 + delta 210937)
c [simplification-12] new conflict limit 1567483 (hard 1778420)
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 -  193.9    4770   115499   1147803   83599  10183  5021   12    30   18  38%   1019   -2   13   11  110%
c i  197.9    4769   115499   1174988  109717  10215  5031   11    29   26  39%   1021   -1    9   11   81%
c -  202.0    4769   115499   1196928   87754  10238  5037   12    28   19  42%  -4108   -2   13   11  109%
c -  210.9    4769   115499   1245228   89687  10293  5043   11    25   31  45%  -1432   -4   11   12   91%
c i  211.7    4768   115499   1249829   94074  10299  5045   12    26   35  46%  -1265   -2   14   12  124%
c -  220.5    4768   115499   1294804   91381  10323  5057   12    29   31  40%   -727    1   13   12  107%
c -  229.9    4768   115499   1345495   94313  10351  5063   13    26   31  48%    216   -0   11   12   96%
c -  239.5    4768   115499   1395775   96621  10368  5069   12    25   31  48%    649   -1   11   12   94%
c -  248.9    4768   115499   1446414   98884  10387  5079   13    22   31  58%    851   -4   11   12   91%
c i  249.9    4767   115499   1453136  105332  10388  5080   13    24   36  54%    868   -2   14   12  114%
c -  258.4    4767   115499   1496760  100462  10411  5094   12    24   31  52%   -715   -1   14   12  113%
c -  268.6    4767   115499   1547734  102698  10424  5097   13    27   32  48%    225    2   13   13  103%
c 
c [simplification-13] limit 1567483 conflicts (hard 1778420) hit after 1573619 conflicts
c [quatres-11] found 28010 quaternary clauses 20% in total
c [quatres-11-1] removed 39 duplicate quaternary clauses
c [quatres-11-1] added 1 double-self-subsuming ternary resolvents
c [quatres-11-2] added 207 single-self-subsuming ternary resolvents
c [quatres-11-2] added 65 quaternary resolvents
c [ternres-11] limit 144583993 with penalty 0 = 0 + 0
c [ternres-11] all 4767 free variables schedulable
c [ternres-11] 14506 ternary resolvents (171 bin, 14335 trn)
c [ternres-11] fully completed ternary resolution
c [decomp-50] removed 6 variables
c [treelook-5] limit 14458399 penalty 0 = 0 + 0 boost 1
c [treelook-5] scheduled 9469 literals 99%
c [treelook-5] scheduling used 644275 steps
c [treelook-5] scheduled completely
c [treelook-5] limit 14458399 penalty 0 = 0 + 0 boost 1
c [treelook-5] used 14459620 steps
c [treelook-5] 5675 literals remain 60%
c [treelook-5] 3996 variables remain to probed next time 84%
c [decomp-51] removed 1 variables
c [treelook-5] removed 10 variables, found 1289 hbrs
c [transred-11] limit 2000000 with penalty 0 = 0 + 0
c [transred-11] removed 1207 transitive binary clauses
c [cce-5] limit of 180729991 steps penalty 2 = 2 + 0
c [cce-5-1] eliminated 84 clauses out of 84 (100%) of length 14
c [cce-5-1] eliminated 76 clauses out of 264 (29%) of length 13
c [cce-5-1] eliminated 8 clauses out of 598 (1%) of length 12
c [cce-5-1] eliminated 5 clauses out of 88 (6%) of length 11
c [cce-5-1] eliminated 52 clauses out of 216 (24%) of length 10
c [cce-5-1] eliminated 226 clauses out of 1064 (21%) of length 9
c [cce-5-1] eliminated 140 clauses out of 2791 (5%) of length 8
c [cce-5-1] eliminated 1019 clauses out of 7076 (14%) of length 7
c [cce-5-1] eliminated 3068 clauses out of 15984 (19%) of length 6
c [cce-5-1] incomplete large round (ACCE)
c [cce-5-1] eliminated 4678 large clauses in 180729992 steps
c [cce-5-1] allowing another 90364996 steps for small clauses
c [cce-5-1] scheduling 12881 clauses = 9241 binary + 3640 ternary
c [cce-5-1] tried to eliminate 12881 small clauses 100%
c [cce-5-1] eliminated 392 binary clauses 4%
c [cce-5-1] eliminated 715 ternary clauses 20%
c [cce-5-1] eliminated 1107 small clauses 9%
c [cce-5-1] eliminated 1107 small clauses in 138279525 steps
c [cce-5-1] completed small round (ACCE)
c [cce-5-1] eliminated 5785 covered clauses in round 1
c [cce-5-2] incomplete large round (ACCE)
c [cce-5-2] allowing another 21225281 steps for small clauses
c [cce-5-2] scheduling 11774 clauses = 8849 binary + 2925 ternary
c [cce-5-2] tried to eliminate 5980 small clauses 51%
c [cce-5-2] eliminated 3 binary clauses 0%
c [cce-5-2] eliminated 3 small clauses 0%
c [cce-5-2] eliminated 3 small clauses in 42450499 steps
c [cce-5-2] incomplete small round (ACCE)
c [cce-5-2] eliminated 3 covered clauses in round 2
c [cce-5] eliminated 5788 covered clauses in TOTAL during 2 rounds
c [elim-6] 174 variables 4% will be scheduled this time
c [elim-6] scheduled 174 variables 4%
c [elim-6] limit of 200000000 steps penalty 2 = 2 + 0
c [elim-6] rescheduling of touched variables disabled
c [elim-6-1] no variable eliminated in round 1 in 151925026 steps
c [elim-6] fully completed in 1 rounds
c [elim-6] transition to [ all 0 rem 0 ] state
c [elim-6] eliminated 0 = 0% variables out of 174 scheduled
c [bca-8] limit of 10000000 steps and 212128 added (scaled 2)
c [bca-8] 5431 out of 9510 literals actually usable 57%
c [bca-8] added 1 blocked clauses in 139017 steps
c [sweep-12] limit 43375197 penalty 0 = 0 + 0
c [sweep-12-1] 2691 pos 56.6% + 2063 neg 43.4% = 4754 sched 100.0% ret 0
c [sweep-12-1] 22126019 steps 711 queries 14.80 avg class size
c [sweep-12-1] 18767 decisions 714 SAT calls 65.73 avg env size
c [sweep-12-1] fully completed sweeping round
c [decomp-52] removed 20 variables
c [sweep-12-1] removed 20 vars (0 failed, 31 eqs, 0 impls)
c [sweep-12-2] 2681 pos 56.6% + 2053 neg 43.4% = 4734 sched 100.0% ret 0
c [sweep-12-2] 18929735 steps 729 queries 22.52 avg class size
c [sweep-12-2] 18637 decisions 724 SAT calls 64.64 avg env size
c [sweep-12-2] fully completed sweeping round
c [decomp-53] removed 21 variables
c [sweep-12-2] removed 21 vars (0 failed, 31 eqs, 3 impls)
c [sweep-12-3] 2664 pos 56.5% + 2049 neg 43.5% = 4713 sched 100.0% ret 0
c [sweep-12-3] 2421922 steps 21 queries 369.95 avg class size
c [sweep-12-3] 1199 decisions 20 SAT calls 166.15 avg env size
c [sweep-12-3] 4204 variables remain 89% (509 retained 11%)
c [sweep-12-3] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-12] removed 41 vars in TOTAL (3 rounds, 1458 queries)
c [score-distribution-13] 1955 pos 41.48%, 1405 min 29.81%, 1353 zero 28.71%
c [score-distribution-13] 1186 different 25.16% out of total 4713 variables
c [simplification-13] removed 54 variables 1.1% (4713 remain 51%)
c [simplification-13] removed 9727 irredundant clauses 8.4% (105772 remain 74%)
c [simplification-13] maximum reduction of 8% = max (1%, 8%)
c [simplification-13] large reduction 8% >= 5% limit
c [simplification-13] next conflict interval 15736 = min (1573619/100, 421875)
c [simplification-13] penalized conflict interval 15736 = 1 * 15736
c [simplification-13] hard conflict limit 1599355 (soft 1589355 + delta 10000)
c [simplification-13] new conflict limit 1589355 (hard 1599355)
c 
c [simplification-14] limit 1589355 conflicts (hard 1599355) hit after 1589589 conflicts
c [quatres-12] found 26348 quaternary clauses 19% in total
c [quatres-12-1] removed 12 duplicate quaternary clauses
c [quatres-12-1] added 1 double-self-subsuming ternary resolvents
c [quatres-12-2] added 194 single-self-subsuming ternary resolvents
c [quatres-12-2] added 41 quaternary resolvents
c [ternres-12] limit 146408159 with penalty 0 = 0 + 0
c [ternres-12] all 4713 free variables schedulable
c [ternres-12] 3944 ternary resolvents (37 bin, 3907 trn)
c [ternres-12] fully completed ternary resolution
c [decomp-55] removed 1 variables
c [basicprobe-5] limit 400000000 penalty 0 = 0 + 0
c [basicprobe-5-0] 917 sched 19%, 4 failed, 0 lifted, 169 hbrs
c [decomp-56] removed 4 variables
c [basicprobe-5-1] 921 sched 20%, 1 failed, 0 lifted, 19 hbrs
c [decomp-57] removed 1 variables
c [basicprobe-5-2] 921 sched 20%, 0 failed, 0 lifted, 9 hbrs
c [basicprobe-5-3] 921 sched 20%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-5-3] fully completed probing
c [basicprobe-5-3] 5 units = 5 failed (100%) + 0 lifted (0%)
c [basicprobe-5-3] removed 5 variables, found 197 hbrs
c [bate-4] eliminated 21 asymmetric tautologies during probing
c [transred-12] limit 2000000 with penalty 0 = 0 + 0
c [transred-12] removed 642 transitive binary clauses
c [cce-6] limit of 366020397 steps penalty 1 = 1 + 0
c [cce-6-1] eliminated 2 clauses out of 85 (2%) of length 11
c [cce-6-1] eliminated 3 clauses out of 838 (0%) of length 9
c [cce-6-1] eliminated 15 clauses out of 2648 (1%) of length 8
c [cce-6-1] eliminated 15 clauses out of 6060 (0%) of length 7
c [cce-6-1] eliminated 259 clauses out of 12830 (2%) of length 6
c [cce-6-1] eliminated 1877 clauses out of 24544 (8%) of length 5
c [cce-6-1] eliminated 45 clauses out of 20611 (0%) of length 4
c [cce-6-1] incomplete large round (ATE)
c [cce-6-1] eliminated 2216 large clauses in 366020444 steps
c [cce-6-1] allowing another 183010222 steps for small clauses
c [cce-6-1] scheduling 34041 clauses = 8828 binary + 25213 ternary
c [cce-6-1] tried to eliminate 34041 small clauses 100%
c [cce-6-1] eliminated 23 binary clauses 0%
c [cce-6-1] eliminated 417 ternary clauses 2%
c [cce-6-1] eliminated 440 small clauses 1%
c [cce-6-1] eliminated 440 small clauses in 285595849 steps
c [cce-6-1] completed small round (ATE)
c [cce-6-1] eliminated 2656 covered clauses in round 1
c [cce-6-2] incomplete large round (ATE)
c [cce-6-2] allowing another 40212382 steps for small clauses
c [cce-6-2] scheduling 33601 clauses = 8805 binary + 24796 ternary
c [cce-6-2] tried to eliminate 13385 small clauses 40%
c [cce-6-2] incomplete small round (ATE)
c [cce-6-2] eliminated 0 covered clauses in round 2
c [cce-6] eliminated 2656 covered clauses in TOTAL during 2 rounds
c [sweep-13] limit 43922447 penalty 0 = 0 + 0
c [sweep-13-1] 2366 pos 56.3% + 1834 neg 43.7% = 4200 sched 89.2% ret 507
c [sweep-13-1] 31763195 steps 720 queries 20.20 avg class size
c [sweep-13-1] 20358 decisions 716 SAT calls 67.31 avg env size
c [sweep-13-1] fully completed sweeping round
c [decomp-59] removed 25 variables
c [sweep-13-1] removed 25 vars (0 failed, 28 eqs, 2 impls)
c [sweep-13-2] 2638 pos 56.3% + 2044 neg 43.7% = 4682 sched 100.0% ret 0
c [sweep-13-2] 12579309 steps 176 queries 144.15 avg class size
c [sweep-13-2] 6074 decisions 179 SAT calls 86.84 avg env size
c [sweep-13-2] 1812 variables remain 39% (2865 retained 61%)
c [decomp-60] removed 9 variables
c [sweep-13-2] removed 9 vars (0 failed, 5 eqs, 0 impls)
c [sweep-13] removed 34 vars in TOTAL (2 rounds, 894 queries)
c [score-distribution-14] 1920 pos 41.09%, 1428 min 30.56%, 1325 zero 28.35%
c [score-distribution-14] 1161 different 24.84% out of total 4673 variables
c [simplification-14] removed 40 variables 0.8% (4673 remain 51%)
c [simplification-14] removed 3049 irredundant clauses 2.9% (102723 remain 72%)
c [simplification-14] maximum reduction of 3% = max (1%, 3%)
c [simplification-14] geometric conflict interval increment 105468 = 421875 / 4
c [simplification-14] new conflict interval 527343
c [simplification-14] penalized conflict interval 527343 = 1 * 527343
c [simplification-14] hard conflict limit 2380603 (soft 2116932 + delta 263671)
c [simplification-14] new conflict limit 2116932 (hard 2380603)
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 -  298.2    4673   102723   1594025  102805  22777  4927   13    28   20  46%    630    4   14   13  115%
c i  298.4    4672   102723   1595054  103793  22777  4927   13    27   25  49%    636    2   12   13   95%
c -  308.3    4672   102723   1646682  105685  22786  4932   13    27   21  47%   -177    2   13   12  102%
c -  319.3    4672   102723   1698731  107299  22800  4937   14    29   34  47%    481    4   15   12  120%
c -  329.3    4672   102723   1750762  108760  22806  4939   13    22   34  57%    779   -2   14   12  111%
c -  340.5    4672   102723   1804086  111035  22816  4941   12    25   34  49%    915    0   13   12  102%
c -  352.0    4672   102723   1856921  111931  22821  4945   14    29   34  47%    975    4   15   13  115%
c -  363.3    4672   102723   1911784  114212  22835  4948   12    21   34  57%   1003   -3   14   12  112%
c -  375.4    4672   102723   1965609  115495  22847  4949   12    28   34  43%   1015    3   11   13   92%
c -  387.8    4672   102723   2021090  117207  22851  4953   13    23   34  54%   1020   -0   12   13   94%
c -  400.8    4672   102723   2076035  117765  22860  4957   14    28   34  51%   1022    3   15   13  116%
c -  412.7    4672   102723   2132303  119877  22866  4962   13    21   34  59%   1023   -3   12   13   94%
c 
c [simplification-15] limit 2116932 conflicts (hard 2380603) hit after 2133861 conflicts
c [quatres-13] found 26073 quaternary clauses 18% in total
c [quatres-13-1] removed 7 duplicate quaternary clauses
c [quatres-13-2] added 69 single-self-subsuming ternary resolvents
c [quatres-13-2] added 54 quaternary resolvents
c [ternres-13] limit 200000000 with penalty 0 = 0 + 0
c [ternres-13] all 4672 free variables schedulable
c [ternres-13] 7538 ternary resolvents (100 bin, 7438 trn)
c [ternres-13] fully completed ternary resolution
c [card-5] limit 6396797 penalty 4 = 4 + 0
c [card-5] found 638 at-most-one constraints of average size 3.2
c [card-5] found 159 at-most-two constraints of average size 4.3
c [card-5] using previous limit 6396797 for elimination
c [card-5] 795 out of 797 constraints (100%) meet size limits
c [card-5] no units found
c [card-5] no at-most-one constraints generated
c [decomp-61] removed 2 variables
c [simpleprobe-6] all 4671 free variables schedulable
c [simpleprobe-6] limit 200000000 penalty 0 = 0 + 0
c [decomp-62] removed 12 variables
c [simpleprobe-6] fully completed simple probing
c [simpleprobe-6] removed 12 variables, found 3212 hbrs, 2 units
c [transred-13] limit 2000000 with penalty 0 = 0 + 0
c [transred-13] removed 1583 transitive binary clauses
c [cce-7] limit of 1023487562 steps penalty 0 = 0 + 0
c [cce-7-1] eliminated 2 clauses out of 585 (0%) of length 12
c [cce-7-1] eliminated 3 clauses out of 86 (3%) of length 11
c [cce-7-1] eliminated 6 clauses out of 2610 (0%) of length 8
c [cce-7-1] eliminated 17 clauses out of 6035 (0%) of length 7
c [cce-7-1] eliminated 2135 clauses out of 12488 (17%) of length 6
c [cce-7-1] eliminated 7770 clauses out of 22448 (35%) of length 5
c [cce-7-1] eliminated 7218 clauses out of 20208 (36%) of length 4
c [cce-7-1] completed large round (ACCE)
c [cce-7-1] eliminated 17151 large clauses in 432691321 steps
c [cce-7-1] allowing another 216345660 steps for small clauses
c [cce-7-1] scheduling 33507 clauses = 8766 binary + 24741 ternary
c [cce-7-1] tried to eliminate 33507 small clauses 100%
c [cce-7-1] eliminated 57 binary clauses 1%
c [cce-7-1] eliminated 2076 ternary clauses 8%
c [cce-7-1] eliminated 2133 small clauses 6%
c [cce-7-1] eliminated 2133 small clauses in 302711219 steps
c [cce-7-1] completed small round (ACCE)
c [cce-7-1] completed small and large (ACCE)
c [cce-7-1] eliminated 19284 covered clauses in round 1
c [cce-7-2] eliminated 4 clauses out of 6018 (0%) of length 7
c [cce-7-2] eliminated 78 clauses out of 10353 (1%) of length 6
c [cce-7-2] eliminated 211 clauses out of 14678 (1%) of length 5
c [cce-7-2] eliminated 56 clauses out of 12990 (0%) of length 4
c [cce-7-2] completed large round (ACCE)
c [cce-7-2] eliminated 349 large clauses in 276839636 steps
c [cce-7-2] allowing another 138419818 steps for small clauses
c [cce-7-2] scheduling 31378 clauses = 8709 binary + 22669 ternary
c [cce-7-2] tried to eliminate 31378 small clauses 100%
c [cce-7-2] eliminated 19 binary clauses 0%
c [cce-7-2] eliminated 49 ternary clauses 0%
c [cce-7-2] eliminated 68 small clauses 0%
c [cce-7-2] eliminated 68 small clauses in 215791100 steps
c [cce-7-2] completed small round (ACCE)
c [cce-7-2] eliminated 417 covered clauses in round 2
c [cce-7-3] completed large round (ACCE)
c [cce-7-3] allowing another 136698565 steps for small clauses
c [cce-7-3] scheduling 31310 clauses = 8690 binary + 22620 ternary
c [cce-7-3] tried to eliminate 31310 small clauses 100%
c [cce-7-3] eliminated 4 binary clauses 0%
c [cce-7-3] eliminated 3 ternary clauses 0%
c [cce-7-3] eliminated 7 small clauses 0%
c [cce-7-3] eliminated 7 small clauses in 213612539 steps
c [cce-7-3] completed small round (ACCE)
c [cce-7-3] eliminated 7 covered clauses in round 3
c [cce-7] eliminated 19708 covered clauses in TOTAL during 3 rounds
c [bca-9] limit of 10000000 steps and 165152 added (scaled 2)
c [bca-9] 5061 out of 9320 literals actually usable 54%
c [bca-9] added 0 blocked clauses in 130240 steps
c [sweep-14] limit 61409253 penalty 0 = 0 + 0
c [sweep-14-1] 987 pos 54.7% + 818 neg 45.3% = 1805 sched 38.7% ret 2854
c [sweep-14-1] 11377838 steps 557 queries 16.61 avg class size
c [sweep-14-1] 13288 decisions 556 SAT calls 61.04 avg env size
c [sweep-14-1] fully completed sweeping round
c [decomp-63] removed 6 variables
c [sweep-14-1] removed 6 vars (0 failed, 5 eqs, 1 impls)
c [sweep-14-2] 2671 pos 57.4% + 1982 neg 42.6% = 4653 sched 100.0% ret 0
c [sweep-14-2] 22767918 steps 730 queries 16.58 avg class size
c [sweep-14-2] 18783 decisions 729 SAT calls 63.30 avg env size
c [sweep-14-2] fully completed sweeping round
c [decomp-64] removed 3 variables
c [sweep-14-2] removed 3 vars (0 failed, 5 eqs, 3 impls)
c [sweep-14-3] 2669 pos 57.4% + 1981 neg 42.6% = 4650 sched 100.0% ret 0
c [sweep-14-3] 18012266 steps 723 queries 17.24 avg class size
c [sweep-14-3] 17646 decisions 724 SAT calls 61.53 avg env size
c [sweep-14-3] fully completed sweeping round
c [decomp-65] removed 1 variables
c [sweep-14-3] removed 1 vars (0 failed, 3 eqs, 1 impls)
c [sweep-14] removed 10 vars in TOTAL (3 rounds, 2007 queries)
c [score-distribution-15] 2138 pos 45.99%, 1367 min 29.40%, 1144 zero 24.61%
c [score-distribution-15] 1278 different 27.49% out of total 4649 variables
c [simplification-15] removed 23 variables 0.5% (4649 remain 50%)
c [simplification-15] removed 20443 irredundant clauses 19.9% (82280 remain 57%)
c [simplification-15] maximum reduction of 20% = max (0%, 20%)
c [simplification-15] large reduction 20% >= 5% limit
c [simplification-15] next conflict interval 21338 = min (2133861/100, 527343)
c [simplification-15] penalized conflict interval 21338 = 1 * 21338
c [simplification-15] hard conflict limit 2165868 (soft 2155199 + delta 10669)
c [simplification-15] new conflict limit 2155199 (hard 2165868)
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  436.8    4648    82280   2159415  146628  30290  6713   14    23   31  60%   1024   -2   13   13  100%
c 
c [simplification-16] limit 2155199 conflicts (hard 2165868) hit after 2165868 conflicts
c [quatres-14] found 18631 quaternary clauses 15% in total
c [quatres-14-1] removed 18 duplicate quaternary clauses
c [quatres-14-2] added 148 single-self-subsuming ternary resolvents
c [quatres-14-2] added 58 quaternary resolvents
c [ternres-14] limit 200000000 with penalty 0 = 0 + 0
c [ternres-14] all 4648 free variables schedulable
c [ternres-14] 4585 ternary resolvents (41 bin, 4544 trn)
c [ternres-14] fully completed ternary resolution
c [decomp-66] removed 2 variables
c [treelook-6] limit 20800925 penalty 0 = 0 + 0 boost 1
c [treelook-6] scheduled 9005 literals 97%
c [treelook-6] scheduling used 634842 steps
c [treelook-6] scheduled completely
c [treelook-6] limit 20800925 penalty 0 = 0 + 0 boost 1
c [treelook-6] used 14701282 steps
c [treelook-6] fully completed tree based probing
c [treelook-6] removed 5 variables, found 633 hbrs
c [unhide-6] limit 1250000 with penalty 4 = 4 + 0
c [unhide-6-6] 0 units, 0 failed, 6259 tauts, 0 hbrs, 42523 literals
c [transred-14] limit 2000000 with penalty 0 = 0 + 0
c [transred-14] removed 501 transitive binary clauses
c [cce-8] boosting limit by 10
c [cce-8] limit of 10400462990 steps penalty 0 = 0 + 0
c [cce-8-1] eliminated 1 clauses out of 164 (1%) of length 10
c [cce-8-1] eliminated 2 clauses out of 830 (0%) of length 9
c [cce-8-1] eliminated 9 clauses out of 2597 (0%) of length 8
c [cce-8-1] eliminated 9 clauses out of 6011 (0%) of length 7
c [cce-8-1] eliminated 20 clauses out of 10266 (0%) of length 6
c [cce-8-1] eliminated 19 clauses out of 14462 (0%) of length 5
c [cce-8-1] eliminated 46 clauses out of 12892 (0%) of length 4
c [cce-8-1] completed large round (ATE)
c [cce-8-1] eliminated 106 large clauses in 261572455 steps
c [cce-8-1] allowing another 130786227 steps for small clauses
c [cce-8-1] scheduling 11551 clauses = 8673 binary + 2878 ternary
c [cce-8-1] tried to eliminate 11551 small clauses 100%
c [cce-8-1] eliminated 9 binary clauses 0%
c [cce-8-1] eliminated 28 ternary clauses 1%
c [cce-8-1] eliminated 37 small clauses 0%
c [cce-8-1] eliminated 37 small clauses in 160102819 steps
c [cce-8-1] completed small round (ATE)
c [cce-8-1] eliminated 143 covered clauses in round 1
c [cce-8-2] completed large round (ATE)
c [cce-8-2] allowing another 130482593 steps for small clauses
c [cce-8-2] scheduling 11514 clauses = 8664 binary + 2850 ternary
c [cce-8-2] tried to eliminate 11514 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 143 covered clauses in TOTAL during 2 rounds
c [cce-8] 143 < 1/100 * 82191 = 821 considered unsuccessful
c [elim-7] scheduling all variables this time
c [elim-7] scheduled 4642 variables 100%
c [elim-7] limit of 100000000 steps penalty 3 = 3 + 0
c [elim-7] rescheduling of touched variables disabled
c [elim-7] incomplete 39 not tried 1% in round 1
c [elim-7] transition to [ all 1 rem 1 ] state
c [elim-7] eliminated 80 = 2% variables out of 4642 scheduled
c [sweep-15] limit 62402777 penalty 0 = 0 + 0
c [sweep-15-1] 2599 pos 57.0% + 1963 neg 43.0% = 4562 sched 100.0% ret 0
c [sweep-15-1] 22916080 steps 703 queries 23.71 avg class size
c [sweep-15-1] 18563 decisions 701 SAT calls 63.32 avg env size
c [sweep-15-1] fully completed sweeping round
c [decomp-68] removed 5 variables
c [sweep-15-1] removed 5 vars (0 failed, 3 eqs, 2 impls)
c [sweep-15-2] 2599 pos 57.0% + 1958 neg 43.0% = 4557 sched 100.0% ret 0
c [sweep-15-2] 15891406 steps 698 queries 26.00 avg class size
c [sweep-15-2] 16990 decisions 700 SAT calls 60.09 avg env size
c [sweep-15-2] fully completed sweeping round
c [decomp-69] removed 1 variables
c [sweep-15-2] removed 1 vars (0 failed, 0 eqs, 0 impls)
c [sweep-15-3] 2599 pos 57.0% + 1957 neg 43.0% = 4556 sched 100.0% ret 0
c [sweep-15-3] 16640888 steps 693 queries 22.80 avg class size
c [sweep-15-3] 17207 decisions 693 SAT calls 63.30 avg env size
c [sweep-15-3] fully completed sweeping round
c [decomp-70] removed 1 variables
c [sweep-15-3] removed 1 vars (0 failed, 1 eqs, 3 impls)
c [sweep-15] removed 7 vars in TOTAL (3 rounds, 2091 queries)
c [score-distribution-16] 2065 pos 45.33%, 1468 min 32.23%, 1022 zero 22.44%
c [score-distribution-16] 1199 different 26.32% out of total 4555 variables
c [simplification-16] removed 93 variables 2.0% (4555 remain 49%)
c [simplification-16] removed 1049 irredundant clauses 1.3% (81231 remain 57%)
c [simplification-16] maximum reduction of 2% = max (2%, 1%)
c [simplification-16] geometric conflict interval increment 175781 = 527343 / 3
c [simplification-16] new conflict interval 703124
c [simplification-16] penalized conflict interval 703124 = 1 * 703124
c [simplification-16] hard conflict limit 3220554 (soft 2868992 + delta 351562)
c [simplification-16] new conflict limit 2868992 (hard 3220554)
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  459.6    4554    81231   2216372  151051  27867  4728   12    23   39  54%  -2733   -1   10   13   82%
c -  461.9    4554    81231   2226060  107204  27868  4728   13    28   29  46%  -2996    4   14   13  113%
c -  473.3    4554    81231   2284174  110364  27876  4728   13    25   29  52%   -632    1   15   13  115%
c -  484.8    4554    81231   2341080  112172  27875  4732   13    23   29  55%    329   -0   13   13   99%
c -  496.2    4554    81231   2398118  112161  27883  4733   12    22   29  56%    733   -2   11   13   89%
c -  510.0    4554    81231   2457486  113974  27888  4738   13    25   30  53%    906   -0   14   13  106%
c -  523.3    4554    81231   2517623  116656  27892  4741   14    25   30  54%    977    1   15   13  110%
c -  536.5    4554    81231   2577547  118058  27900  4742   13    29   30  45%   1005    5   10   14   77%
c -  549.3    4554    81231   2638287  119795  27908  4743   13    20   30  66%   1017   -5   12   14   85%
c -  562.0    4554    81231   2699699  121661  27910  4745   14    22   30  61%   1021   -0   13   13   98%
c -  575.9    4554    81231   2760325  122647  27915  4747   14    23   30  62%   1023    1   15   13  109%
c -  588.9    4554    81231   2821968  123339  27919  4750   14    25   30  58%   1024    1   13   14   94%
c 
c [simplification-17] limit 2868992 conflicts (hard 3220554) hit after 2869965 conflicts
c [quatres-15] found 17687 quaternary clauses 14% in total
c [quatres-15-1] removed 13 duplicate quaternary clauses
c [quatres-15-1] added 1 double-self-subsuming ternary resolvents
c [quatres-15-2] added 156 single-self-subsuming ternary resolvents
c [quatres-15-2] added 60 quaternary resolvents
c [ternres-15] limit 200000000 with penalty 0 = 0 + 0
c [ternres-15] all 4554 free variables schedulable
c [ternres-15] 8238 ternary resolvents (100 bin, 8138 trn)
c [ternres-15] fully completed ternary resolution
c [gauss-5] limit 3125000 penalty 4 = 4 + 0
c [gauss-5] extracted 87 xors of average arity 3.0
c [gauss-5] connected 261 occurrences of 214 variables (average 1.2)
c [gauss-5] limit 3125000 penalty 4 = 4 + 0
c [gauss-5] fully completed
c [gauss-5] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-71] removed 1 variables
c [basicprobe-6] limit 400000000 penalty 0 = 0 + 0
c [basicprobe-6-0] 900 sched 20%, 4 failed, 0 lifted, 248 hbrs
c [decomp-72] removed 4 variables
c [basicprobe-6-1] 901 sched 20%, 0 failed, 0 lifted, 15 hbrs
c [basicprobe-6-2] 901 sched 20%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-6-2] fully completed probing
c [basicprobe-6-2] 4 units = 4 failed (100%) + 0 lifted (0%)
c [basicprobe-6-2] removed 4 variables, found 263 hbrs
c [bate-5] eliminated 9 asymmetric tautologies during probing
c [transred-15] limit 2000000 with penalty 0 = 0 + 0
c [transred-15] removed 305 transitive binary clauses
c [block-6] scheduling all variables this time
c [block-6] scheduled 4549 variables 100%
c [block-6] limit of 50000000 steps penalty 4 = 4 + 0
c [block-6] fully completed
c [block-6] transition to [ all 0 rem 0 ] state
c [block-6] eliminated 0 blocked clauses
c [sweep-16] limit 85833064 penalty 0 = 0 + 0
c [sweep-16-1] 2596 pos 57.1% + 1953 neg 42.9% = 4549 sched 100.0% ret 0
c [sweep-16-1] 31178228 steps 641 queries 19.53 avg class size
c [sweep-16-1] 19950 decisions 637 SAT calls 71.59 avg env size
c [sweep-16-1] fully completed sweeping round
c [decomp-74] removed 5 variables
c [sweep-16-1] removed 5 vars (0 failed, 4 eqs, 2 impls)
c [sweep-16-2] 2592 pos 57.0% + 1952 neg 43.0% = 4544 sched 100.0% ret 0
c [sweep-16-2] 28350902 steps 620 queries 21.94 avg class size
c [sweep-16-2] 18632 decisions 621 SAT calls 69.95 avg env size
c [sweep-16-2] fully completed sweeping round
c [decomp-75] removed 7 variables
c [sweep-16-2] removed 7 vars (0 failed, 4 eqs, 1 impls)
c [sweep-16-3] 2589 pos 57.1% + 1948 neg 42.9% = 4537 sched 100.0% ret 0
c [sweep-16-3] 26316921 steps 558 queries 41.96 avg class size
c [sweep-16-3] 17064 decisions 558 SAT calls 72.99 avg env size
c [sweep-16-3] 70 variables remain 2% (4467 retained 98%)
c [decomp-76] removed 2 variables
c [sweep-16-3] removed 2 vars (0 failed, 3 eqs, 1 impls)
c [sweep-16] removed 14 vars in TOTAL (3 rounds, 1816 queries)
c [score-distribution-17] 2338 pos 51.55%, 1265 min 27.89%, 932 zero 20.55%
c [score-distribution-17] 1511 different 33.32% out of total 4535 variables
c [simplification-17] removed 19 variables 0.4% (4535 remain 49%)
c [simplification-17] removed 170 irredundant clauses 0.2% (81061 remain 57%)
c [simplification-17] maximum reduction of 0% = max (0%, 0%)
c [simplification-17] full geometric conflict interval increment 703124
c [simplification-17] conflict interval soft limit 1000000 reached
c [simplification-17] new conflict interval 1000000
c [simplification-17] penalized conflict interval 1000000 = 1 * 1000000
c [simplification-17] hard conflict limit 4369965 (soft 3869965 + delta 500000)
c [simplification-17] new conflict limit 3869965 (hard 4369965)
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 -  611.5    4535    81061   2881672  125406  33256  4666   14    28   22  49%   1024    2   18   13  137%
c -  626.8    4535    81061   2944752  126763  33260  4671   13    21   36  62%   1024   -5   16   13  123%
c -  641.0    4535    81061   3008830  128176  33266  4672   13    23   36  56%   1024   -0   14   13  105%
c -  655.8    4535    81061   3073050  128965  33273  4674   14    24   36  57%   1024   -1   13   13  101%
c -  669.8    4535    81061   3138865  131239  33277  4675   12    22   37  56%   1024   -2   12   13   92%
c -  684.4    4535    81061   3203918  132518  33281  4676   14    22   37  63%   1024   -1   16   13  117%
c -  698.5    4535    81061   3269566  133520  33284  4676   13    22   37  63%   1024   -2   12   13   86%
c -  714.1    4535    81061   3336345  134931  33285  4678   14    22   37  65%   1024   -1   15   14  112%
c -  731.0    4535    81061   3405850  136164  33285  4678   13    18   37  73%   1024   -4   13   13  101%
c -  747.3    4535    81061   3474681  138009  33286  4679   13    22   37  60%   1024    1   12   13   94%
c -  764.1    4535    81061   3542142  138591  33291  4680   14    25   37  54%   1024    2   12   13   88%
c -  780.2    4535    81061   3611709  139885  33295  4681   14    20   37  68%   1024   -3   12   14   89%
c -  795.9    4535    81061   3681339  141681  33300  4681   14    26   37  54%   1024    3   14   14  102%
c -  813.2    4535    81061   3750477  142216  33306  4682   14    23   37  60%   1024   -1   17   14  125%
c -  830.0    4535    81061   3821156  144514  33306  4682   12    20   37  61%   1024   -3   16   13  118%
c 
c [simplification-18] limit 3869965 conflicts (hard 4369965) hit after 3881192 conflicts
c [quatres-16] found 17624 quaternary clauses 13% in total
c [quatres-16-1] removed 2 duplicate quaternary clauses
c [quatres-16-2] added 56 single-self-subsuming ternary resolvents
c [quatres-16-2] added 69 quaternary resolvents
c [ternres-16] limit 200000000 with penalty 0 = 0 + 0
c [ternres-16] all 4535 free variables schedulable
c [ternres-16] 6422 ternary resolvents (92 bin, 6330 trn)
c [ternres-16] 1 variables remain 0% (4534 retained 100%)
c [simpleprobe-7] all 4535 free variables schedulable
c [simpleprobe-7] limit 200000000 penalty 0 = 0 + 0
c [decomp-78] removed 1 variables
c [simpleprobe-7] fully completed simple probing
c [simpleprobe-7] removed 1 variables, found 2966 hbrs, 0 units
c [transred-16] limit 2000000 with penalty 0 = 0 + 0
c [transred-16] removed 1393 transitive binary clauses
c [cce-9] limit of 1031358765 steps penalty 1 = 1 + 0
c [cce-9-1] eliminated 6 clauses out of 86 (7%) of length 11
c [cce-9-1] eliminated 1 clauses out of 828 (0%) of length 9
c [cce-9-1] eliminated 2 clauses out of 2589 (0%) of length 8
c [cce-9-1] eliminated 8 clauses out of 6004 (0%) of length 7
c [cce-9-1] eliminated 16 clauses out of 10748 (0%) of length 6
c [cce-9-1] eliminated 98 clauses out of 14852 (1%) of length 5
c [cce-9-1] eliminated 61 clauses out of 12027 (1%) of length 4
c [cce-9-1] completed large round (ACCE)
c [cce-9-1] eliminated 192 large clauses in 274086879 steps
c [cce-9-1] allowing another 137043439 steps for small clauses
c [cce-9-1] scheduling 30286 clauses = 8565 binary + 21721 ternary
c [cce-9-1] tried to eliminate 30286 small clauses 100%
c [cce-9-1] eliminated 32 binary clauses 0%
c [cce-9-1] eliminated 113 ternary clauses 1%
c [cce-9-1] eliminated 145 small clauses 0%
c [cce-9-1] eliminated 145 small clauses in 210653493 steps
c [cce-9-1] completed small round (ACCE)
c [cce-9-1] eliminated 337 covered clauses in round 1
c [cce-9-2] eliminated 5 clauses out of 10732 (0%) of length 6
c [cce-9-2] eliminated 16 clauses out of 14754 (0%) of length 5
c [cce-9-2] eliminated 7 clauses out of 11966 (0%) of length 4
c [cce-9-2] completed large round (ACCE)
c [cce-9-2] eliminated 28 large clauses in 272962380 steps
c [cce-9-2] allowing another 136481190 steps for small clauses
c [cce-9-2] scheduling 30141 clauses = 8533 binary + 21608 ternary
c [cce-9-2] tried to eliminate 30141 small clauses 100%
c [cce-9-2] eliminated 1 binary clauses 0%
c [cce-9-2] eliminated 6 ternary clauses 0%
c [cce-9-2] eliminated 7 small clauses 0%
c [cce-9-2] eliminated 7 small clauses in 209779484 steps
c [cce-9-2] completed small round (ACCE)
c [cce-9-2] eliminated 35 covered clauses in round 2
c [cce-9-3] eliminated 17 clauses out of 10727 (0%) of length 6
c [cce-9-3] eliminated 5 clauses out of 14738 (0%) of length 5
c [cce-9-3] eliminated 5 clauses out of 11959 (0%) of length 4
c [cce-9-3] completed large round (ACCE)
c [cce-9-3] eliminated 27 large clauses in 272438531 steps
c [cce-9-3] allowing another 136219265 steps for small clauses
c [cce-9-3] scheduling 30135 clauses = 8532 binary + 21603 ternary
c [cce-9-3] tried to eliminate 30135 small clauses 100%
c [cce-9-3] eliminated 2 ternary clauses 0%
c [cce-9-3] eliminated 2 small clauses 0%
c [cce-9-3] eliminated 2 small clauses in 209454951 steps
c [cce-9-3] completed small round (ACCE)
c [cce-9-3] eliminated 29 covered clauses in round 3
c [cce-9] eliminated 401 covered clauses in TOTAL during 3 rounds
c [cce-9] 401 < 1/100 * 81035 = 810 considered unsuccessful
c [elim-8] 39 variables 1% will be scheduled this time
c [elim-8] scheduled 39 variables 1%
c [elim-8] boosting limit by 20
c [elim-8] limit of 4000000000 steps penalty 2 = 2 + 0
c [elim-8] rescheduling of touched variables disabled
c [elim-8-1] no variable eliminated in round 1 in 39336809 steps
c [elim-8] fully completed in 1 rounds
c [elim-8] transition to [ all 0 rem 0 ] state
c [elim-8] eliminated 0 = 0% variables out of 39 scheduled
c [bca-10] limit of 10000000 steps and 161816 added (scaled 2)
c [bca-10] 4596 out of 9070 literals actually usable 51%
c [bca-10] added 1 blocked clauses in 211412 steps
c [sweep-17] limit 123763051 penalty 0 = 0 + 0
c [sweep-17-1] 39 pos 55.7% + 31 neg 44.3% = 70 sched 1.5% ret 4464
c [sweep-17-1] 400499 steps 47 queries 7.81 avg class size
c [sweep-17-1] 1054 decisions 46 SAT calls 53.11 avg env size
c [sweep-17-1] fully completed sweeping round
c [sweep-17-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-17-2] 2610 pos 57.6% + 1924 neg 42.4% = 4534 sched 100.0% ret 0
c [sweep-17-2] 30073609 steps 669 queries 25.09 avg class size
c [sweep-17-2] 18020 decisions 666 SAT calls 64.66 avg env size
c [sweep-17-2] fully completed sweeping round
c [decomp-80] removed 4 variables
c [sweep-17-2] removed 4 vars (0 failed, 4 eqs, 2 impls)
c [sweep-17-3] 2607 pos 57.5% + 1923 neg 42.5% = 4530 sched 100.0% ret 0
c [sweep-17-3] 33676787 steps 652 queries 26.96 avg class size
c [sweep-17-3] 17443 decisions 654 SAT calls 66.50 avg env size
c [sweep-17-3] fully completed sweeping round
c [sweep-17-3] removed 0 vars (0 failed, 0 eqs, 1 impls)
c [sweep-17] removed 4 vars in TOTAL (3 rounds, 1365 queries)
c [score-distribution-18] 1990 pos 43.93%, 1654 min 36.51%, 886 zero 19.56%
c [score-distribution-18] 1235 different 27.26% out of total 4530 variables
c [simplification-18] removed 5 variables 0.1% (4530 remain 49%)
c [simplification-18] removed 430 irredundant clauses 0.5% (80631 remain 56%)
c [simplification-18] maximum reduction of 1% = max (0%, 1%)
c [simplification-18] geometric conflict interval increment 500000 = 1000000 / 2
c [simplification-18] conflict interval soft limit 1000000 reached
c [simplification-18] new conflict interval 1000000
c [simplification-18] penalized conflict interval 1000000 = 1 * 1000000
c [simplification-18] hard conflict limit 5381192 (soft 4881192 + delta 500000)
c [simplification-18] new conflict limit 4881192 (hard 5381192)
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 -  863.5    4530    80631   3888186  145326  39733  6438   13    25   25  51%   1024    3   12   13   94%
c i  865.4    4529    80631   3897035  153754  39734  6439   14    26   33  56%   1024    3   14   13  106%
c -  882.4    4529    80631   3959338  146216  39736  6441   14    23   41  62%  -9286   -1   15   14  106%
c -  900.1    4529    80631   4032254  148399  39737  6442   13    21   41  62%  -2365   -2   12   14   87%
c -  920.1    4529    80631   4104619  148904  39744  6444   15    25   42  60%    -99    1   16   14  115%
c -  938.8    4529    80631   4178454  150915  39749  6446   14    24   42  58%    660    1   13   14   99%
c -  956.5    4529    80631   4251450  151900  39755  6449   14    21   42  63%    904   -2   14   14   99%
c -  976.6    4529    80631   4325629  153101  39754  6450   14    25   42  56%    985    2   12   14   88%
c -  996.9    4529    80631   4401032  153823  39757  6450   14    20   42  68%   1012   -3   14   14   96%
c
c CAUGHT SIGNAL 15 SIGTERM
c
c s UNKNOWN
c bate: 575 basic ate = 156 trn 27% + 419 lrg 73% in 5 updates
c bcas: 10 count, 102 added (250 skipped), 909751 steps
c bkwd: tried 28353 clauses, 56106 lits, 1.98 lits/clause
c bkwd: checked 5188402 occs, 182.99 occs/clause, 92.47 occs/lit
c bkwd: subsumed 0 binary, 3 ternary, 353 large
c bkwd: strengthened 0 binary, 0 ternary (0% self), 345 large (0% self)
c blkd: 6 bces, 2077 removed, 3431157 resolutions, 10919680 steps
c blkd: 2950 blocking literals 15%, 19 pure
c bump: 4446296 bumped seen, 226451592 lits 50.9 on average
c card: 5 count, 0 units, 0 am1, 57535732 steps
c card: 0 rescheduled, 0 eliminated, 0 resolved, 9977 subsumed
c card: 4549 at-most-one constraints found, average size 3.10
c card: 4549 at-most-one constraints used 100%, average size 3.10
c card: 354 at-most-two constraints found, average size 4.25
c card: 351 at-most-two constraints used 99%, average size 4.25
c cces: 9 cces, 36017 eliminated, 13336 ate 37%, 22681 abce 63%
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: 793883 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 110 gcs, 0 rescored clauses, 2339 rescored vars
c dcps: 81 decompositions, 1801 equivalent 19%
c deco: 0 decision-only clauses 0%, 0% reduction
c decs: 6508513 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c dsch: 14304436 push, 14294925 pop (14294925 dec 100%)
c dsch: 371041578 swaps, 0 down, 172926923 up
c elms: 8 elims, 2540 eliminated 26%, 468 pure 18%
c elms: 11 rounds, 1.4 rounds/bve
c elms: 1571 small 62%, 482 large 19%
c elms: 3203 tried small, 1571 succeeded 49%, 1632 failed 51%
c elms: 4710 subsumed, 627 strengthened, 355 blocked
c elms: 1838299 copies, 2494619 resolutions, 111332 ipos
c elms: 5265795 subchks, 804912 strchks
c gaus: 5 extractions, 1144 extracted, 3.0 size, 3 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 20383030 steps, 10191515 extr 50%, 51279 elim 0%
c glue: 12.3 orig avg, 12.3 real avg, 3.1 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 25785 = 15176 simple 59% + 9197 trn 36% + 1412 lrg 5%, 737 sub 3%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 4446296 clauses, 26.5 length
c lrnd: 117848441 lits = 157344694 orig - 39496253 removed 25%
c lrnd: 1197967 uips 27%, 2923207 flips 66%
c mins: 4420027 mins 99%, 520 bin 0%, 25749 size 1%
c mins: 106378080 poisoned searches, 22334633 hits, 21% hit rate
c mins: 236781184 used twice searches, 30520502 hits, 13% hit rate
c move: moved 7959, 1388 bin 17%, 6571 trn 83%
c otfs: 11675 driving 32%, 25314 restarting 68%
c otfs: str 36989, 36687 red 99%, 302 irr 1%
c otfs: str 36989, 0 bin 0%, 410 trn 1%, 36579 lrg 99%
c otfs: sub 156, 156 red 100%, 0 irr 0%
c otfs: sub 156, 0 bin 0%, 38 trn 24%, 118 lrg 76%
c phas: 8 computed, 6016 set, 3399 pos (56%), 2617 neg (44%)
c prbs: 6 basic, 40040 probed, 63 failed, 1 lifted
c prbs: 7 simple, 58590 probed, 22 failed, 393 eqs
c prbs: 6 treelook, 14288 probed, 17 failed, 0 lifted
c prom: 1196218 locked 19% out of 6209012 tried
c prps: 808383758 props, 123 props/dec
c prps: 99% srch, 1% simp, 0% lkhd
c quat: 16 count, 659 quat, 1213 self1, 3 self2, 3407 dup
c redc: 46299 clauses 9%, 505013 tried 11%, 12 sat 0%
c redc: 58667 lits 1%, 6333377 tried 4%, 13 sat 0%
c redc: 894 times jump level reduced, 2.8 levels on average
c reds: 79 count, 55871.6 conflicts per reduce
c reds: 0 memlim 0%, 79 arith 100%
c reds: 3515616 collected 90%, 409492 retired 10%
c rmbd: 682 removed, 262 red 38%
c rsts: 34311 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: 18 count, 18 confs 100%, 0 vars 0%
c simp: 0 its 0%, 0 bin 0%, 0 trns 0%
c subl: 4446296 count (1788400 tried 0.4), 271562 sub out of 4440543 (6.1%)
c swps: 17 count, 34 rounds, 15863 queries (466.6/round)
c swps: 15968 sat calls, 683 unsat (2.8% success rate)
c swps: 432527 decisions 27.1, 44118 conflicts 2.8
c swps; 43.5 avg class size, 65.9 avg environment size
c swps: 0 failed, 79 impls, 564 equivs
c swp0: 5276 type 0 queries, 2254 unsat (42.7%), 5146 sat (97.5%)
c swp1: 10587 type 1 queries, 5447 unsat (51.4%), 10153 sat (95.9%)
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: 21914724 calls to obtain time
c tops: 773 fixed 8%, 15 its, 294256.87 confs/it
c trds: 16 transitive reductions, 13133 removed, 2 failed
c trds: 152923 nodes, 202141 edges, 4935973 steps
c trim: 1517751 words, 5.8 MB
c trnr: 16 count, 618 bin, 52251 trn, 1300872158 steps
c unhd: 6 count, 6 rounds, 10859128 steps
c unhd: 452 non-trivial sccs of average size 2.0
c unhd: 0 units, 0 bin, 0 trn, 0 lrg
c unhd: 6 failed, 6 stamp, 0 lits, 0 bin, 0 trn, 0 lrg
c unhd: 10515 tauts, 563 bin 5%, 2293 trn 22%, 4156 lrg 40%
c unhd: 10515 tauts, 3503 stamp 33%, 8951 red 85%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 85746 str, 0 bin 0%, 377 trn 0%, 85369 lrg 100%, 85581 red 100%
c vars: 4529 remaining 47% and 5114 removed 53% out of 9643
c vars: 773 fixed 8%, 2540 eliminated 26%, 1801 equivalent 19%
c vsts: 49271726386 visits, 99% srch, 1% simp, 0% lkhd
c vsts: 61.0 search visits per propagation, 11040.3 per conflict
c wchs: 13915339572 pushed, 16827328 enlarged, 209 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all        4441202       3515616        409492     106282674      35187101       2778106
c 
c  0 0        151486   3     17464   0         0   0  65532910  62  16602894  47   1169716  42     3.9
c  1 5        154982   3     88416   3     45060  11  13137540  12<  4597467  13<   379903  14<    0.7
c  2 6        841316  19    658118  19    111183  27  18282846  17   7767177  22    728601  26     2.5
c  3 9       1659306  37<  1423317  40<   119197  29<  6626425   6   4140040  12    368087  13     3.8
c  4 14      1301403  29   1080662  31     94862  23   2223485   2   1721040   5    110387   4     4.1
c  5 21       308436   7    232046   7     34090   8    445396   0    335876   1     19876   1     1.6
c  6 30        23166   1     14998   0      4741   1     32555   0     21693   0      1465   0     0.1
c  7 41         1022   0       546   0       330   0      1405   0       849   0        69   0     0.0
c  8 54           75   0        43   0        26   0       100   0        58   0         1   0     0.0
c  9 69           10   0         6   0         3   0        12   0         7   0         1   0     0.0
c 
c avg                  3.1           3.2           2.9           0.8           1.2           1.3
c std                  1.1           1.0           1.2           1.1           1.3           1.3
c 
c   41.807   4% cce
c   22.923   2% ternres
c   21.128   2% sweep
c    8.617   1% probe
c    6.472   1% bump
c    6.030   1% elim
c 
c   12.335 < 1% rest (below)
c 
c    4.703   0% decide
c    2.994   0% quatres
c    1.314   0% unhide
c    0.789   0% block
c    0.601   0% bca
c    0.591   0% card
c    0.498   0% gauss
c    0.485   0% transred
c    0.361   0% rescore
c    0.000   0% locs
c    0.000   0% queuesort
c ==================================
c    0.829   0% preprocessing     1%
c  109.595  11% inprocessing     99%
c ==================================
c  110.423  11% simplifying
c  889.531  89% search
c ==================================
c  999.954 100% all
c 
c       4413853 conflicts,        4414.1 confs/sec
c          2663 ternaries,        1657.5 confs/ternary
c           399 binaries,        11062.3 confs/binary
c            15 iterations,     294256.9 confs/iteration
c 
c            79 reductions,          0.1 redus/sec,  55871.6 confs/reduction
c         34311 restarts,           34.3 rests/sec,    128.6 confs/restart
c       6508513 decisions,        6508.8 decis/sec,      1.5 decis/conflict
c     808383758 propagations,   808420.7 props/sec,    124.2 props/decision
c 
c 1000.0 seconds, 61.9 MB
c
c CAUGHT SIGNAL 15 SIGTERM
c
c launch: done
