c launch: /data/cnf/sc2014/app/SAT_dat.k30-30_rule.cnf.bz2
c host: atom29
c Lingeling SAT Solver
c 
c Version b7ztzu 7b29300825af9bcc1c8b2c5ebcf65fa1cb101cad
c 
c Copyright (C) 2010-2014 Armin Biere JKU Linz Austria.
c All rights reserved.
c 
c released Sun Apr 26 19:26:13 CEST 2015
c compiled Sun Apr 26 19:26:13 CEST 2015
c 
c gcc (Ubuntu 4.8.2-19ubuntu1) 4.8.2
c -Wall -O3 -I../yalsat -I../druplig -DNLGLOG -DNDEBUG -DNCHKSOL
c Linux cluster2 3.13.0-45-generic x86_64
c 
c piping '/data/cnf/sc2014/app/SAT_dat.k30-30_rule.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/SAT_dat.k30-30_rule.cnf.bz2
c no embedded options
c found 'p cnf 63454 310323' header
c read 63454 variables, 310323 clauses, 814971 literals in 0.00 seconds
c
c --abstime=0
c --bate=1
c --batewait=2
c --bca=1
c --bcaddlimldscale=2
c --bcamaxeff=10000000
c --bcaminuse=100
c --bcawait=2
c --bkwdscale=100
c --bkwdroundlim=7
c --bkwdresched=1
c --blkboost=10
c --blkboostvlim=10000000
c --blkclslim=1000000
c --blklarge=1
c --blkmaxeff=800000000
c --blkmineff=50000000
c --blkocclim1=100000
c --blkocclim=1000000
c --blkocclim2=10000
c --blkreleff=100
c --blkresched=1
c --blkrtc=0
c --blksmall=1
c --blksuccessmaxwortc=6
c --blksuccessrat=100
c --block=1
c --blockwait=1
c --boost=1
c --bumpsimp=1
c --card=1
c --cardcut=2
c --cardexpam1=3
c --cardglue=0
c --cardignused=0
c --cardmaxeff=300000000
c --cardmaxlen=1000
c --cardmineff=2000000
c --cardminlen=3
c --cardocclim1=300
c --cardocclim2=15
c --cardreleff=5
c --cardreschedint=10
c --carduse=2
c --cardwait=0
c --cce2wait=1
c --cce=3
c --cceateint=2
c --cceboost=10
c --cceboostdel=3
c --cceboostint=5
c --cceboostvlim=10000000
c --cce3wait=2
c --ccemaxround=3
c --ccemaxeff=2147483647
c --ccemineff=30000000
c --ccereleff=50
c --ccertc=0
c --ccertcint=15
c --ccertcintvlim=2000000
c --ccesuccessrat=100
c --ccewait=2
c --clim=-1
c --compact=0
c --deco=1
c --decolim=100
c --deco1opt=1
c --decompose=1
c --defragfree=50
c --defragint=10000000
c --delmax=10
c --dlim=-1
c --druplig=0
c --drupligcheck=0
c --drupligtrace=0
c --drupligtraceorig=0
c --elim=1
c --elmaxeff=800000000
c --elmblk=1
c --elmblkwait=1
c --elmboost=20
c --elmboostdel=3
c --elmboostint=5
c --elmboostvlim=4000000
c --elmclslim=1000000
c --elmfull=0
c --elmineff=20000000
c --elmlitslim=200
c --elmocclim1=1000
c --elmocclim=1000000
c --elmocclim2=100
c --elmoccsumforced=0
c --elmreleff=200
c --elmresched=0
c --elmroundlim=3
c --elmrtc=0
c --elmrtcint=10
c --elmrtcintvlim=500000
c --elmsuccessmaxwortc=4
c --elmsuccessrat=100
c --exitonabort=0
c --factmax=100000
c --factor=3
c --gauss=1
c --gaussexptrn=1
c --gaussextrall=1
c --gaussmaxeff=50000000
c --gaussmaxor=20
c --gaussmineff=2000000
c --gaussreleff=2
c --gausswait=2
c --gluekeep=4
c --gluekeepsize=15
c --gluescale=4
c --hbrdom=2
c --import=1
c --incredcint=1
c --incredconfslim=0
c --incsavevisits=0
c --inprocessing=1
c --irrlim=1
c --jwhred=1
c --keepmaxglue=1
c --keepmaxglueint=100
c --lhbr=1
c --lkhd=2
c --locs=0
c --locsbanner=0
c --locsclim=1000000
c --locsboost=2
c --locscint=10000
c --locset=2
c --locsexport=1
c --locsmaxeff=100000
c --locsmineff=1000
c --locsred=0
c --locsreleff=5
c --locsrtc=0
c --locsvared=100
c --locswait=2
c --maxscaledglue=15
c --memlim=-1
c --minimize=2
c --minlocalgluelim=200
c --minlocalsizelim=3000
c --minrecgluelim=100
c --minrecsizelim=1000
c --norestartsatlimlo=85
c --move=2
c --otfs=1
c --penmax=4
c --phase=0
c --phaseluckfactor=200
c --phaselucklim=100
c --phaseluckmaxround=10
c --phasesave=1
c --plain=0
c --plim=-1
c --poison=1
c --prbasic=1
c --prbasicmaxeff=400000000
c --prbasicmineff=1000000
c --prbasicreleff=50
c --prbasicroundlim=8
c --prbasicrtc=0
c --prbrtc=0
c --prbsimple=2
c --prbsimpleboost=10
c --prbsimpleliftdepth=2
c --prbsimplemaxeff=200000000
c --prbsimplemineff=2000000
c --prbsimplereleff=40
c --prbsimplertc=0
c --probe=1
c --promote=1
c --promotegluelim=8
c --pure=1
c --quatres=1
c --quatreswait=2
c --queuesort=1
c --queuesortjwh=0
c --randec=0
c --randecint=1000
c --redcls=1
c --redclsglue=6
c --redclsmaxdec=5
c --redclsmaxdepth=10
c --redclsmaxlrg=10
c --redclsmaxprops=100
c --redclsatlimlo=0
c --redclsatlimhi=100
c --redclsize=30
c --redclstype=4
c --reducefixed=0
c --reduceinc=1000
c --reduceinit=50000
c --reduce=1
c --restart=4
c --restartglcint=10
c --restartglclim=115
c --restartinit=0
c --restartint=5
c --restartpen=1
c --retirenb=1
c --retireint=4
c --retiremin=1
c --reusetrail=0
c --rmincpen=4
c --rstinoutinc=110
c --satlimdelay=10000
c --scincinc=200
c --scincincsatlimhi=100
c --scincincdelta=10
c --scincincincint=100000
c --scincincmin=200
c --scincincmode=1
c --score=1
c --scoreshift=0
c --scoreresetint=2147483647
c --seed=0
c --simpbintinc=100
c --simpbintinclim=10000
c --simpcintdelay=2000
c --simpcintinc=20000
c --simpcintincdiv=1
c --simpcintmaxhard=10000000
c --simpcintmaxsoft=1000000
c --simpincdelmaxfact=50
c --simpincdelmaxmin=10000
c --simpinitdelay=0
c --simpintsizepen=0
c --simpen=0
c --simpidiv=3
c --simpiscale=100
c --simpitdelay=10
c --simpitintinc=10
c --simpitintinclim=1000
c --simplify=2
c --simprtc=5
c --simptintinc=1000
c --simptintinclim=10000
c --simpvarchg=100
c --simpvarlim=100
c --sizemaxpen=5
c --sizepen=1000000
c --sleeponabort=0
c --smallirr=90
c --smallve=1
c --smallvevars=10
c --smallvewait=0
c --sortlits=0
c --subl=9
c --sweep=1
c --sweepboost=10
c --sweepboostdel=4
c --sweepboostint=7
c --sweepboostvlim=1000000
c --sweepfacdec=10
c --sweepforgive=2
c --sweepirr=3
c --sweepmaxeff=200000000
c --sweepmaxdec=10000
c --sweepmaxround=3
c --sweepmindec=100
c --sweepmineff=1000000
c --sweepred=3
c --sweepreleff=3
c --sweeprtc=0
c --sweeprtcint=14
c --sweeprtcintvlim=100000
c --sweepsuccessmaxwortc=6
c --sweepsuccessrat=1000
c --sweepwait=2
c --synclsall=1
c --synclsglue=8
c --synclsint=100
c --synclslen=40
c --syncunint=111111
c --termint=122222
c --ternres=1
c --ternresboost=5
c --ternresrtc=0
c --ternreswait=2
c --transred=1
c --transredwait=2
c --trapiflush=0
c --trdmaxeff=2000000
c --trdmineff=100000
c --trdreleff=10
c --treelook=1
c --treelookboost=10
c --treelookfull=0
c --treelookmaxeff=50000000
c --treelookmineff=300000
c --treelookreleff=2
c --treelookrtc=0
c --trep=1
c --trepint=55555
c --trnreleff=10
c --trnrmaxeff=200000000
c --trnrmineff=4000000
c --unhdatrn=2
c --unhdextstamp=1
c --unhdhbr=0
c --unhdlnpr=3
c --unhdmaxeff=20000000
c --unhdmineff=100000
c --unhdreleff=2
c --unhdroundlim=20
c --unhide=1
c --unhidewait=0
c --usedtwice=1
c --vsidsdint=256
c --wait=1
c --waitmax=4
c --witness=0
c --check=0
c --log=-1
c --profile=1
c --profilelong=1
c --verbose=1
c [freezer] frozen 0 variables out of 63044 free variables 0%
c [limits] no decision limit
c [limits] no conflict limit
c [limits] no propagation limit
c [limits] simplification not delayed since 'simpdelay' zero
c [set-maximum-score] maximum score limit 1.000000d+500
c [set-minimum-score] minimum score limit 1.000000d-500
c [score-type] INC (--score=1)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c *    0.0   63044   309889         0       0      0     0    0     0   15   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 328 at-most-one constraints of average size 3.0
c [card-1] no at-most-two constraint found
c [card-1] using previous limit 2000000 for elimination
c [card-1] 328 out of 328 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] generated 48 at-most-one constraints, 46 used 96%
c [card-1] exported 46 binary clauses, 1.0 per/constraint
c [decomp-1] removed 12804 variables
c [simpleprobe-1] all 50650 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 6505 variables
c [simpleprobe-1] 8339 variables remain 19% (35806 retained 81%)
c [simpleprobe-1] removed 6505 variables, found 56464 hbrs, 115 units
c [unhide-1] limit 100000 with penalty 0 = 0 + 0
c [unhide-1-1] 0 units, 1 failed, 577 tauts, 0 hbrs, 522 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 44128 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 22518 variables 51% in round 1 in 14234128 steps
c [elim-1-1] backward subsumption/strengthening limit 5765872
c [elim-1-1-1] backward checking 31385 touched variables 71%
c [elim-1-1-1] incomplete backward checking 25043 remain 80%
c [elim-1-1] subsumed 284 and strengthened 1511 clauses in 5765880 steps
c [elim-1] incomplete 2146 not tried 5% in round 1
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 22520 = 51% variables out of 44128 scheduled
c [elim-1] considered successful since not run to completion yet
c [phase-count-1] 149634 negative 84.8% of 176403 except 26769 15.2%
c [phase-count-1] 167247 positive 94.8% of 176403 except 9156 5.2%
c [phase-count-1] less non-positive clauses 9156 than limit 17600 (0.1%)
c [phase-count-1] non-neg/non-pos = 26769/9156 = 2.92 >= 2.00 = 200/100
c [lucky-phase-1] forcing lucky phase 1
c [phase-1] phase bias: 21608 positive 100%, 0 negative 0%
c [sort-queue-1] sorted 21608 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 21608 (100%)
c [score-dist-1] max exp 0, different 1 (100%)
c [score-dist-1] median active exp 0, avg 0.0
c [simplification-1] removed 34753 variables 61.7% (21608 remain 34%)
c [simplification-1] removed 133486 irredundant clauses 43.1% (176403 remain 57%)
c [simplification-1] maximum reduction of 62% = max (62%, 43%)
c [simplification-1] large reduction 62% >= 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  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    1.9   21607   176403         1       0      0 14801    0     0   12   0%      0    0    0    0    0%
c i    1.9   21602   176403        54      35      2 14811    0     1   12  14%      0    1    1    0 23479%
c i    2.1   21579   176403       610     503     49 14831    1     5   13  21%      2    5    8    0 12719%
c i    2.1   21570   176403       945     738     68 14849    2     7   13  29%      2    7   13    0 9187%
c 
c [simplification-2] limit 1010 conflicts (hard 11000) hit after 1011 conflicts
c [decomp-3] removed 191 variables
c [simpleprobe-2] 5921 schedulable variables 28%
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [decomp-4] removed 89 variables
c [simpleprobe-2] 4701 variables remain 22% (16627 retained 78%)
c [simpleprobe-2] removed 89 variables, found 1783 hbrs, 1 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 28838 literals 68%
c [treelook-1] scheduling used 300044 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 300834 steps
c [treelook-1] 28797 literals remain 68%
c [treelook-1] 19451 variables remain to probed next time 91%
c [treelook-1] removed 0 variables, found 620 hbrs
c [basicprobe-1] limit 1399848 based on 174981 irredundant clauses
c [basicprobe-1-0] 13821 probes remain 65% after last round
c [basicprobe-1-0] 7 units = 7 failed (100%) + 0 lifted (0%)
c [basicprobe-1-0] removed 16 variables, found 2047 hbrs
c [unhide-2] limit 100000 with penalty 0 = 0 + 0
c [unhide-2-2] 2 units, 12 failed, 2270 tauts, 0 hbrs, 3526 literals
c [elim-2] no untried remaining variables left
c [elim-2] scheduled 21257 variables 100%
c [elim-2] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-2] rescheduling of touched variables disabled
c [elim-2] incomplete 118 not tried 1% in round 1
c [elim-2] transition to [ all 1 rem 1 ] state
c [elim-2] eliminated 795 = 4% variables out of 21257 scheduled
c [elim-2] considered successful since not run to completion yet
c [phase-count-2] 144155 negative 84.6% of 170430 except 26275 15.4%
c [phase-count-2] 161582 positive 94.8% of 170430 except 8848 5.2%
c [phase-count-2] less non-positive clauses 8848 than limit 17000 (0.1%)
c [phase-count-2] non-neg/non-pos = 26275/8848 = 2.97 >= 2.00 = 200/100
c [lucky-phase-2] forcing lucky phase 1
c [phase-2] phase bias: 95 positive 100%, 0 negative 0%
c [sort-queue-2] sorted 17326 enqueued variables after 1011 conflicts
c [score-dist-2] active 3136 (15%), one 0 (0%), zero 17326 (85%)
c [score-dist-2] max exp 510, different 10 (2%)
c [score-dist-2] median active exp 504, avg 504.2
c [simplification-2] removed 1102 variables 5.1% (20462 remain 32%)
c [simplification-2] removed 5973 irredundant clauses 3.4% (170430 remain 55%)
c [simplification-2] maximum reduction of 5% = max (5%, 3%)
c [simplification-2] large reduction 5% >= 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 13011 (soft 3011 + delta 10000)
c [simplification-2] new conflict limit 3011 (hard 13011)
c 
c [simplification-3] limit 3011 conflicts (hard 13011) hit after 3013 conflicts
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 551 at-most-one constraints of average size 3.0
c [card-2] no at-most-two constraint found
c [card-2] using previous limit 1000000 for elimination
c [card-2] 551 out of 551 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [decomp-6] removed 58 variables
c [unhide-3] limit 100000 with penalty 0 = 0 + 0
c [unhide-3-3] 2 units, 3 failed, 824 tauts, 0 hbrs, 2158 literals
c [elim-3] 118 variables 1% will be scheduled this time
c [elim-3] scheduled 118 variables 1%
c [elim-3] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-3] rescheduling of touched variables disabled
c [elim-3-1] no variable eliminated in round 1 in 3588034 steps
c [elim-3] fully completed in 1 rounds
c [elim-3] transition to [ all 0 rem 0 ] state
c [elim-3] eliminated 0 = 0% variables out of 118 scheduled
c [phase-count-3] 143327 negative 84.6% of 169383 except 26056 15.4%
c [phase-count-3] 160539 positive 94.8% of 169383 except 8844 5.2%
c [phase-count-3] less non-positive clauses 8844 than limit 16900 (0.1%)
c [phase-count-3] non-neg/non-pos = 26056/8844 = 2.95 >= 2.00 = 200/100
c [lucky-phase-3] forcing lucky phase 1
c [phase-3] phase bias: 79 positive 100%, 0 negative 0%
c [sort-queue-3] sorted 13286 enqueued variables after 3013 conflicts
c [score-dist-3] active 7106 (35%), one 0 (0%), zero 13286 (65%)
c [score-dist-3] max exp 511, different 11 (2%)
c [score-dist-3] median active exp 504, avg 504.9
c [simplification-3] removed 70 variables 0.3% (20392 remain 32%)
c [simplification-3] removed 1046 irredundant clauses 0.6% (169383 remain 55%)
c [simplification-3] maximum reduction of 1% = max (0%, 1%)
c [simplification-3] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-3] new conflict interval 10000
c [simplification-3] penalized conflict interval 10000 = 1 * 10000
c [simplification-3] hard conflict limit 23013 (soft 13013 + delta 10000)
c [simplification-3] new conflict limit 13013 (hard 23013)
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    7.0   20391   169382      8778    7169    170 14363   11    17   16  63%    101   15   12    1  804%
c 
c [simplification-4] limit 13013 conflicts (hard 23013) hit after 13013 conflicts
c [decomp-7] removed 14 variables
c [treelook-2] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-2] scheduled 18007 literals 44%
c [treelook-2] scheduling used 150007 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-2] used 172972 steps
c [treelook-2] 17997 literals remain 44%
c [treelook-2] 15164 variables remain to probed next time 74%
c [treelook-2] removed 0 variables, found 88 hbrs
c [unhide-4] limit 319535 with penalty 0 = 0 + 0
c [unhide-4-4] 1 units, 25 failed, 875 tauts, 0 hbrs, 26753 literals
c [block-1] scheduling all variables this time
c [block-1] scheduled 20342 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 1245 blocked clauses
c [block-1] 1245 < 1/100 * 168883 = 1688 considered unsuccessful
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 32 clauses out of 880 (4%) of length 19
c [cce-1-1] eliminated 32 clauses out of 864 (4%) of length 18
c [cce-1-1] eliminated 4 clauses out of 845 (0%) of length 17
c [cce-1-1] eliminated 24 clauses out of 142 (17%) of length 13
c [cce-1-1] eliminated 96 clauses out of 2582 (4%) of length 11
c [cce-1-1] eliminated 17 clauses out of 769 (2%) of length 10
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 205 large clauses in 30000002 steps
c [cce-1-1] allowing another 15000001 steps for small clauses
c [cce-1-1] scheduling 120946 clauses = 102414 binary + 18532 ternary
c [cce-1-1] tried to eliminate 3097 small clauses 3%
c [cce-1-1] eliminated 368 binary clauses 0%
c [cce-1-1] eliminated 62 ternary clauses 0%
c [cce-1-1] eliminated 430 small clauses 0%
c [cce-1-1] eliminated 430 small clauses in 30000040 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 635 covered clauses in round 1
c [cce-1] eliminated 635 covered clauses in TOTAL during 1 rounds
c [cce-1] 635 < 1/100 * 167139 = 1671 considered unsuccessful
c [bca-1] limit of 10000000 steps and 333508 added (scaled 2)
c [bca-1] 35632 out of 40568 literals actually usable 88%
c [bca-1] added 129 blocked clauses in 126813 steps
c [sweep-1] limit 1000000 penalty 0 = 0 + 0
c [sweep-1-1] 8673 pos 42.8% + 11610 neg 57.2% = 20283 sched 100.0% ret 0
c [sweep-1-1] 1006660 steps 99 queries 2732.95 avg class size
c [sweep-1-1] 1460 decisions 95 SAT calls 49.71 avg env size
c [sweep-1-1] 19285 variables remain 95% (992 retained 5%)
c [decomp-9] removed 33 variables
c [sweep-1-1] removed 33 vars (0 failed, 18 eqs, 14 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 33 vars in TOTAL (1 rounds, 98 queries)
c [phase-count-4] 140606 negative 84.5% of 166372 except 25766 15.5%
c [phase-count-4] 157565 positive 94.7% of 166372 except 8807 5.3%
c [phase-count-4] less non-positive clauses 8807 than limit 16600 (0.1%)
c [phase-count-4] non-neg/non-pos = 25766/8807 = 2.93 >= 2.00 = 200/100
c [lucky-phase-4] forcing lucky phase 1
c [phase-4] phase bias: 64 positive 100%, 0 negative 0%
c [sort-queue-4] sorted 11355 enqueued variables after 13013 conflicts
c [score-dist-4] active 8895 (44%), one 0 (0%), zero 11355 (56%)
c [score-dist-4] max exp 514, different 14 (3%)
c [score-dist-4] median active exp 508, avg 507.5
c [simplification-4] removed 141 variables 0.7% (20250 remain 32%)
c [simplification-4] removed 3010 irredundant clauses 1.8% (166372 remain 54%)
c [simplification-4] maximum reduction of 2% = max (1%, 2%)
c [simplification-4] geometric conflict interval increment 6666 = 20000 / 3
c [simplification-4] new conflict interval 16666
c [simplification-4] penalized conflict interval 16666 = 1 * 16666
c [simplification-4] hard conflict limit 39679 (soft 29679 + delta 10000)
c [simplification-4] new conflict limit 29679 (hard 39679)
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   13.0   20249   166372     17407   13958    725 14691   11    15   17  75%    106   11   10    3  376%
c i   19.9   20239   166372     28449   22569    789 14733   11    17   24  63%    132   12   11    4  275%
c 
c [simplification-5] limit 29679 conflicts (hard 39679) hit after 29679 conflicts
c [quatres-1] found 13175 quaternary clauses 35% in total
c [quatres-1-1] removed 3 duplicate quaternary clauses
c [quatres-1-1] added 1 double-self-subsuming ternary resolvents
c [quatres-1-2] added 9 single-self-subsuming ternary resolvents
c [quatres-1-2] added 753 quaternary resolvents
c [ternres-1] boosting ternary resolution limit by 5
c [ternres-1] limit 21488320 with penalty 0 = 0 + 0
c [ternres-1] all 20239 free variables schedulable
c [ternres-1] 12209 ternary resolvents (1269 bin, 10940 trn)
c [ternres-1] fully completed ternary resolution
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 11481 xors of average arity 2.9
c [gauss-1] connected 33272 occurrences of 3364 variables (average 9.9)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] exported 0 unary, 0 binary and 1 ternary equations
c [decomp-10] removed 424 variables
c [basicprobe-2] limit 21488321 penalty 0 = 0 + 0
c [basicprobe-2-0] 3786 probes remain 19% after last round
c [basicprobe-2-0] 166 units = 157 failed (95%) + 9 lifted (5%)
c [basicprobe-2-0] removed 367 variables, found 11876 hbrs
c [bate-1] eliminated 95 asymmetric tautologies during probing
c [unhide-5] limit 859532 with penalty 0 = 0 + 0
c [unhide-5-5] 5 units, 8 failed, 632 tauts, 0 hbrs, 84120 literals
c [transred-1] limit 2000000 with penalty 0 = 0 + 0
c [transred-1] removed 219 transitive binary clauses
c [transred-1] found 3 units
c [elim-4] scheduling all variables this time
c [elim-4] scheduled 19432 variables 100%
c [elim-4] boosting limit by 20
c [elim-4] limit of 859532840 steps penalty 1 = 1 + 0
c [elim-4] rescheduling of touched variables disabled
c [elim-4-1] eliminated 583 variables 3% in round 1 in 30418369 steps
c [elim-4-1] backward subsumption/strengthening limit 30418300
c [elim-4-1-1] backward checking 2394 touched variables 12%
c [elim-4-1-1] fully completed backward checking in 1 rounds
c [elim-4-1] subsumed 22 and strengthened 63 clauses in 1644073 steps
c [elim-4-1] rescheduled 172 variables 1% by backward subsumption
c [elim-4-2] eliminated 18 variables 0% in round 2 in 425187 steps
c [elim-4-2] backward subsumption/strengthening limit 425100
c [elim-4-2-1] backward checking 87 touched variables 0%
c [elim-4-2-1] fully completed backward checking in 1 rounds
c [elim-4-2] subsumed 1 and strengthened 1 clauses in 94148 steps
c [elim-4-2] rescheduled 6 variables 0% by backward subsumption
c [elim-4-3] eliminated 2 variables 0% in round 3 in 6083 steps
c [elim-4-3] backward subsumption/strengthening limit 6000
c [elim-4-3-1] backward checking 17 touched variables 0%
c [elim-4-3-1] incomplete backward checking 7 remain 41%
c [elim-4-3] subsumed 0 and strengthened 2 clauses in 6008 steps
c [elim-4] incomplete 6 not tried 0% in round 3
c [elim-4] transition to [ all 1 rem 1 ] state
c [elim-4] eliminated 618 = 3% variables out of 19432 scheduled
c [bca-2] limit of 10000000 steps and 313964 added (scaled 2)
c [bca-2] 29392 out of 37630 literals actually usable 78%
c [bca-2] added 26 blocked clauses in 109683 steps
c [sweep-2] limit 1289299 penalty 0 = 0 + 0
c [sweep-2-1] 7469 pos 41.8% + 10410 neg 58.2% = 17879 sched 95.0% ret 935
c [sweep-2-1] 1296388 steps 109 queries 2093.49 avg class size
c [sweep-2-1] 1772 decisions 105 SAT calls 52.74 avg env size
c [sweep-2-1] 16711 variables remain 89% (2101 retained 11%)
c [decomp-11] removed 107 variables
c [sweep-2-1] removed 107 vars (0 failed, 12 eqs, 12 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 107 vars in TOTAL (1 rounds, 108 queries)
c [phase-count-5] 132265 negative 84.5% of 156599 except 24334 15.5%
c [phase-count-5] 147319 positive 94.1% of 156599 except 9280 5.9%
c [phase-count-5] less non-positive clauses 9280 than limit 15600 (0.1%)
c [phase-count-5] non-neg/non-pos = 24334/9280 = 2.62 >= 2.00 = 200/100
c [lucky-phase-5] forcing lucky phase 1
c [phase-5] phase bias: 48 positive 100%, 0 negative 0%
c [sort-queue-5] sorted 7959 enqueued variables after 29679 conflicts
c [score-dist-5] active 10748 (57%), one 0 (0%), zero 7959 (43%)
c [score-dist-5] max exp 516, different 16 (3%)
c [score-dist-5] median active exp 510, avg 509.2
c [simplification-5] removed 1532 variables 7.6% (18707 remain 30%)
c [simplification-5] removed 9773 irredundant clauses 5.9% (156599 remain 51%)
c [simplification-5] maximum reduction of 8% = max (8%, 6%)
c [simplification-5] large reduction 8% >= 5% limit
c [simplification-5] next conflict interval 2000 = 2000/1
c [simplification-5] penalized conflict interval 2000 = 1 * 2000
c [simplification-5] hard conflict limit 41679 (soft 31679 + delta 10000)
c [simplification-5] new conflict limit 31679 (hard 41679)
c 
c [simplification-6] limit 31679 conflicts (hard 41679) hit after 31679 conflicts
c [quatres-2] found 13539 quaternary clauses 37% in total
c [quatres-2-1] removed 1 duplicate quaternary clauses
c [quatres-2-2] added 17 single-self-subsuming ternary resolvents
c [quatres-2-2] added 576 quaternary resolvents
c [ternres-2] limit 4638592 with penalty 0 = 0 + 0
c [ternres-2] all 18707 free variables schedulable
c [ternres-2] 1397 ternary resolvents (120 bin, 1277 trn)
c [ternres-2] fully completed ternary resolution
c [card-3] limit 579824 penalty 2 = 2 + 0
c [card-3] found 315 at-most-one constraints of average size 3.1
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 579824 for elimination
c [card-3] 315 out of 315 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [gauss-2] limit 2000000 penalty 0 = 0 + 0
c [gauss-2] extracted 7962 xors of average arity 3.0
c [gauss-2] connected 23807 occurrences of 2871 variables (average 8.3)
c [gauss-2] limit 2000000 penalty 0 = 0 + 0
c [gauss-2] connected 4848 occurrences of 2871 variables (average 1.7)
c [gauss-2] fully completed
c [gauss-2] exported 0 unary, 0 binary and 2 ternary equations
c [decomp-12] removed 26 variables
c [simpleprobe-3] 4123 schedulable variables 22%
c [simpleprobe-3] limit 18554368 penalty 0 = 0 + 0
c [decomp-13] removed 692 variables
c [simpleprobe-3] 586 variables remain 3% (17403 retained 97%)
c [simpleprobe-3] removed 692 variables, found 12229 hbrs, 46 units
c [unhide-6] limit 927718 with penalty 0 = 0 + 0
c [unhide-6-6] 0 units, 0 failed, 4445 tauts, 0 hbrs, 123940 literals
c [transred-2] limit 2000000 with penalty 0 = 0 + 0
c [transred-2] removed 376 transitive binary clauses
c [block-2] scheduling all variables this time
c [block-2] scheduled 17989 variables 100%
c [block-2] limit of 25000000 steps penalty 1 = 1 + 0
c [block-2] fully completed
c [block-2] transition to [ all 0 rem 0 ] state
c [block-2] eliminated 267 blocked clauses
c [block-2] 267 < 1/100 * 152059 = 1520 considered unsuccessful
c [cce-2] limit of 15000000 steps penalty 1 = 1 + 0
c [cce-2-1] eliminated 6 clauses out of 828 (1%) of length 19
c [cce-2-1] eliminated 10 clauses out of 818 (1%) of length 18
c [cce-2-1] eliminated 4 clauses out of 784 (1%) of length 17
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] eliminated 20 large clauses in 15000011 steps
c [cce-2-1] allowing another 7500005 steps for small clauses
c [cce-2-1] scheduling 102280 clauses = 92882 binary + 9398 ternary
c [cce-2-1] tried to eliminate 1476 small clauses 1%
c [cce-2-1] eliminated 144 binary clauses 0%
c [cce-2-1] eliminated 19 ternary clauses 0%
c [cce-2-1] eliminated 163 small clauses 0%
c [cce-2-1] eliminated 163 small clauses in 15000004 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 183 covered clauses in round 1
c [cce-2] eliminated 183 covered clauses in TOTAL during 1 rounds
c [cce-2] 183 < 1/100 * 151792 = 1517 considered unsuccessful
c [elim-5] no untried remaining variables left
c [elim-5] scheduled 17972 variables 100%
c [elim-5] limit of 92771843 steps penalty 0 = 0 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5-1] eliminated 240 variables 1% in round 1 in 29862279 steps
c [elim-5-1] backward subsumption/strengthening limit 29862200
c [elim-5-1-1] backward checking 2344 touched variables 13%
c [elim-5-1-1] fully completed backward checking in 1 rounds
c [elim-5-1] subsumed 8 and strengthened 41 clauses in 1186199 steps
c [elim-5-1] rescheduled 66 variables 0% by backward subsumption
c [elim-5-2] eliminated 1 variables 0% in round 2 in 149527 steps
c [elim-5-2] backward subsumption/strengthening limit 149500
c [elim-5-2-1] backward checking 22 touched variables 0%
c [elim-5-2-1] fully completed backward checking in 1 rounds
c [elim-5-2] subsumed 2 and strengthened 0 clauses in 67192 steps
c [elim-5-2] rescheduled 4 variables 0% by backward subsumption
c [elim-5-3] no variable eliminated in round 3 in 2510 steps
c [elim-5] fully completed in 3 rounds
c [elim-5] transition to [ all 0 rem 0 ] state
c [elim-5] eliminated 242 = 1% variables out of 17972 scheduled
c [bca-3] limit of 10000000 steps and 301437 added (scaled 2)
c [bca-3] 26982 out of 35462 literals actually usable 76%
c [bca-3] added 21 blocked clauses in 91482 steps
c [sweep-3] limit 1391577 penalty 0 = 0 + 0
c [sweep-3-1] 6405 pos 40.7% + 9320 neg 59.3% = 15725 sched 88.7% ret 2005
c [sweep-3-1] 1394953 steps 80 queries 1521.78 avg class size
c [sweep-3-1] 1436 decisions 78 SAT calls 51.76 avg env size
c [sweep-3-1] 14931 variables remain 84% (2796 retained 16%)
c [decomp-14] removed 18 variables
c [sweep-3-1] removed 18 vars (0 failed, 8 eqs, 9 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 18 vars in TOTAL (1 rounds, 79 queries)
c [phase-count-6] 126034 negative 83.8% of 150373 except 24339 16.2%
c [phase-count-6] 140776 positive 93.6% of 150373 except 9597 6.4%
c [phase-count-6] less non-positive clauses 9597 than limit 15000 (0.1%)
c [phase-count-6] non-neg/non-pos = 24339/9597 = 2.54 >= 2.00 = 200/100
c [lucky-phase-6] forcing lucky phase 1
c [phase-6] phase bias: 47 positive 100%, 0 negative 0%
c [sort-queue-6] sorted 7309 enqueued variables after 31679 conflicts
c [score-dist-6] active 10403 (59%), one 0 (0%), zero 7309 (41%)
c [score-dist-6] max exp 516, different 16 (3%)
c [score-dist-6] median active exp 510, avg 509.4
c [simplification-6] removed 995 variables 5.3% (17712 remain 28%)
c [simplification-6] removed 6226 irredundant clauses 4.0% (150373 remain 49%)
c [simplification-6] maximum reduction of 5% = max (5%, 4%)
c [simplification-6] large reduction 5% >= 5% limit
c [simplification-6] next conflict interval 2000 = 2000/1
c [simplification-6] penalized conflict interval 2000 = 1 * 2000
c [simplification-6] hard conflict limit 43679 (soft 33679 + delta 10000)
c [simplification-6] new conflict limit 33679 (hard 43679)
c 
c [simplification-7] limit 33679 conflicts (hard 43679) hit after 33680 conflicts
c [quatres-3] found 13706 quaternary clauses 38% in total
c [quatres-3-1] removed 7 duplicate quaternary clauses
c [quatres-3-1] added 1 double-self-subsuming ternary resolvents
c [quatres-3-2] added 18 single-self-subsuming ternary resolvents
c [quatres-3-2] added 352 quaternary resolvents
c [ternres-3] limit 4948007 with penalty 0 = 0 + 0
c [ternres-3] all 17712 free variables schedulable
c [ternres-3] 759 ternary resolvents (84 bin, 675 trn)
c [ternres-3] fully completed ternary resolution
c [gauss-3] limit 2000000 penalty 0 = 0 + 0
c [gauss-3] extracted 7212 xors of average arity 3.0
c [gauss-3] connected 21579 occurrences of 2636 variables (average 8.2)
c [gauss-3] limit 2000000 penalty 0 = 0 + 0
c [gauss-3] connected 3687 occurrences of 2636 variables (average 1.4)
c [gauss-3] fully completed
c [gauss-3] exported 0 unary, 0 binary and 1 ternary equations
c [decomp-15] removed 28 variables
c [transred-3] limit 2000000 with penalty 0 = 0 + 0
c [transred-3] removed 364 transitive binary clauses
c [elim-6] scheduling all variables this time
c [elim-6] scheduled 17684 variables 100%
c [elim-6] limit of 98960142 steps penalty 0 = 0 + 0
c [elim-6] rescheduling of touched variables disabled
c [elim-6-1] eliminated 59 variables 0% in round 1 in 29685402 steps
c [elim-6-1] backward subsumption/strengthening limit 29685400
c [elim-6-1-1] backward checking 422 touched variables 2%
c [elim-6-1-1] fully completed backward checking in 1 rounds
c [elim-6-1] subsumed 1 and strengthened 11 clauses in 283241 steps
c [elim-6-1] rescheduled 35 variables 0% by backward subsumption
c [elim-6-2] no variable eliminated in round 2 in 58780 steps
c [elim-6] fully completed in 2 rounds
c [elim-6] transition to [ all 0 rem 0 ] state
c [elim-6] eliminated 59 = 0% variables out of 17684 scheduled
c [elim-6] 59 < 1/100 * 17684 = 176 considered unsuccessful
c [bca-4] limit of 10000000 steps and 300758 added (scaled 2)
c [bca-4] 26276 out of 35252 literals actually usable 75%
c [bca-4] added 7 blocked clauses in 88460 steps
c [sweep-4] limit 1484402 penalty 0 = 0 + 0
c [sweep-4-1] 6090 pos 41.0% + 8759 neg 59.0% = 14849 sched 84.2% ret 2776
c [sweep-4-1] 1485262 steps 76 queries 1360.30 avg class size
c [sweep-4-1] 1608 decisions 73 SAT calls 68.19 avg env size
c [sweep-4-1] 14028 variables remain 80% (3597 retained 20%)
c [decomp-16] removed 7 variables
c [sweep-4-1] removed 7 vars (0 failed, 7 eqs, 6 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 7 vars in TOTAL (1 rounds, 75 queries)
c [phase-count-7] 125827 negative 83.8% of 150075 except 24248 16.2%
c [phase-count-7] 140429 positive 93.6% of 150075 except 9646 6.4%
c [phase-count-7] less non-positive clauses 9646 than limit 15000 (0.1%)
c [phase-count-7] non-neg/non-pos = 24248/9646 = 2.51 >= 2.00 = 200/100
c [lucky-phase-7] forcing lucky phase 1
c [phase-7] phase bias: 44 positive 100%, 0 negative 0%
c [sort-queue-7] sorted 7054 enqueued variables after 33680 conflicts
c [score-dist-7] active 10564 (60%), one 0 (0%), zero 7054 (40%)
c [score-dist-7] max exp 516, different 16 (3%)
c [score-dist-7] median active exp 510, avg 509.5
c [simplification-7] removed 94 variables 0.5% (17618 remain 28%)
c [simplification-7] removed 298 irredundant clauses 0.2% (150075 remain 48%)
c [simplification-7] maximum reduction of 1% = max (1%, 0%)
c [simplification-7] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-7] new conflict interval 26666
c [simplification-7] penalized conflict interval 26666 = 1 * 26666
c [simplification-7] hard conflict limit 73679 (soft 60346 + delta 13333)
c [simplification-7] new conflict limit 60346 (hard 73679)
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   44.6   17617   150075     53021   34704   6866 25943   16    21   34  75%    291   11   12    8  156%
c 
c [simplification-8] limit 60346 conflicts (hard 73679) hit after 60348 conflicts
c [quatres-4] found 14237 quaternary clauses 38% in total
c [quatres-4-1] removed 1 duplicate quaternary clauses
c [quatres-4-2] added 19 single-self-subsuming ternary resolvents
c [quatres-4-2] added 140 quaternary resolvents
c [ternres-4] limit 9837453 with penalty 0 = 0 + 0
c [ternres-4] all 17617 free variables schedulable
c [ternres-4] 668 ternary resolvents (63 bin, 605 trn)
c [ternres-4] fully completed ternary resolution
c [gauss-4] limit 2000000 penalty 0 = 0 + 0
c [gauss-4] extracted 6865 xors of average arity 3.0
c [gauss-4] connected 20588 occurrences of 2498 variables (average 8.2)
c [gauss-4] limit 2000000 penalty 0 = 0 + 0
c [gauss-4] fully completed
c [gauss-4] exported 0 unary, 0 binary and 1 ternary equations
c [decomp-17] removed 3 variables
c [unhide-7] limit 983745 with penalty 1 = 1 + 0
c [unhide-7-7] 0 units, 0 failed, 374 tauts, 0 hbrs, 89864 literals
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 279 transitive binary clauses
c [bca-5] limit of 10000000 steps and 300033 added (scaled 2)
c [bca-5] 25203 out of 35230 literals actually usable 72%
c [bca-5] added 4 blocked clauses in 108804 steps
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 29512350 penalty 0 = 0 + 0
c [sweep-5-1] 5845 pos 41.7% + 8179 neg 58.3% = 14024 sched 79.6% ret 3590
c [sweep-5-1] 22092557 steps 2596 queries 50.86 avg class size
c [sweep-5-1] 20781 decisions 1777 SAT calls 59.05 avg env size
c [sweep-5-1] fully completed sweeping round
c [decomp-18] removed 1067 variables
c [sweep-5-1] removed 1067 vars (0 failed, 1096 eqs, 1122 impls)
c [sweep-5-2] 6412 pos 38.8% + 10135 neg 61.2% = 16547 sched 100.0% ret 0
c [sweep-5-2] 7423108 steps 479 queries 296.10 avg class size
c [sweep-5-2] 8558 decisions 463 SAT calls 86.36 avg env size
c [sweep-5-2] 6718 variables remain 41% (9829 retained 59%)
c [decomp-19] removed 61 variables
c [sweep-5-2] removed 61 vars (0 failed, 58 eqs, 51 impls)
c [sweep-5] removed 1128 vars in TOTAL (2 rounds, 3073 queries)
c [phase-count-8] 124721 negative 83.6% of 149146 except 24425 16.4%
c [phase-count-8] 136737 positive 91.7% of 149146 except 12409 8.3%
c [phase-8] phase bias: 0 positive 0%, 1 negative 100%
c [sort-queue-8] sorted 4360 enqueued variables after 60348 conflicts
c [score-dist-8] active 12126 (74%), one 0 (0%), zero 4360 (26%)
c [score-dist-8] max exp 517, different 17 (3%)
c [score-dist-8] median active exp 511, avg 509.5
c [simplification-8] removed 1131 variables 6.4% (16486 remain 26%)
c [simplification-8] removed 929 irredundant clauses 0.6% (149146 remain 48%)
c [simplification-8] maximum reduction of 6% = max (6%, 1%)
c [simplification-8] large reduction 6% >= 5% limit
c [simplification-8] next conflict interval 2000 = 2000/1
c [simplification-8] penalized conflict interval 2000 = 1 * 2000
c [simplification-8] hard conflict limit 72348 (soft 62348 + delta 10000)
c [simplification-8] new conflict limit 62348 (hard 72348)
c 
c [simplification-9] limit 62348 conflicts (hard 72348) hit after 62349 conflicts
c [quatres-5] found 14455 quaternary clauses 38% in total
c [quatres-5-1] removed 58 duplicate quaternary clauses
c [quatres-5-1] added 4 double-self-subsuming ternary resolvents
c [quatres-5-2] added 59 single-self-subsuming ternary resolvents
c [quatres-5-2] added 104 quaternary resolvents
c [ternres-5] limit 10198125 with penalty 0 = 0 + 0
c [ternres-5] all 16486 free variables schedulable
c [ternres-5] 1728 ternary resolvents (169 bin, 1559 trn)
c [ternres-5] fully completed ternary resolution
c [gauss-5] limit 2039625 penalty 0 = 0 + 0
c [gauss-5] extracted 5343 xors of average arity 3.0
c [gauss-5] connected 15942 occurrences of 2153 variables (average 7.4)
c [gauss-5] limit 2039625 penalty 0 = 0 + 0
c [gauss-5] fully completed
c [decomp-20] removed 29 variables
c [gauss-5] exported 1 unary, 0 binary and 7 ternary equations
c [treelook-3] limit 254953 penalty 2 = 2 + 0 boost 1
c [treelook-3] scheduled 17942 literals 55%
c [treelook-3] scheduling used 254958 steps
c [treelook-3] not fully scheduled
c [treelook-3] limit 254953 penalty 2 = 2 + 0 boost 1
c [treelook-3] used 261510 steps
c [treelook-3] 17918 literals remain 54%
c [treelook-3] 11786 variables remain to probed next time 72%
c [treelook-3] removed 0 variables, found 563 hbrs
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 658 transitive binary clauses
c [block-3] scheduling all variables this time
c [block-3] scheduled 16457 variables 100%
c [block-3] limit of 25495314 steps penalty 2 = 2 + 0
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 46 blocked clauses
c [block-3] 46 < 1/100 * 148665 = 1486 considered unsuccessful
c [cce-3] limit of 12747657 steps penalty 2 = 2 + 0
c [cce-3-1] eliminated 96 clauses out of 912 (11%) of length 19
c [cce-3-1] eliminated 9 clauses out of 812 (1%) of length 18
c [cce-3-1] eliminated 118 clauses out of 771 (15%) of length 17
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 223 large clauses in 12747706 steps
c [cce-3-1] allowing another 6373853 steps for small clauses
c [cce-3-1] scheduling 106886 clauses = 91081 binary + 15805 ternary
c [cce-3-1] tried to eliminate 1248 small clauses 1%
c [cce-3-1] eliminated 231 binary clauses 0%
c [cce-3-1] eliminated 36 ternary clauses 0%
c [cce-3-1] eliminated 267 small clauses 0%
c [cce-3-1] eliminated 267 small clauses in 12747672 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 490 covered clauses in round 1
c [cce-3] eliminated 490 covered clauses in TOTAL during 1 rounds
c [cce-3] 490 < 1/100 * 148619 = 1486 considered unsuccessful
c [elim-7] scheduling all variables this time
c [elim-7] scheduled 16457 variables 100%
c [elim-7] limit of 101981259 steps penalty 1 = 1 + 0
c [elim-7] rescheduling of touched variables disabled
c [elim-7-1] eliminated 145 variables 1% in round 1 in 28837529 steps
c [elim-7-1] backward subsumption/strengthening limit 28837500
c [elim-7-1-1] backward checking 2748 touched variables 17%
c [elim-7-1-1] fully completed backward checking in 1 rounds
c [elim-7-1] subsumed 7 and strengthened 21 clauses in 1476315 steps
c [elim-7-1] rescheduled 101 variables 1% by backward subsumption
c [elim-7-2] eliminated 2 variables 0% in round 2 in 226726 steps
c [elim-7-2] backward subsumption/strengthening limit 226700
c [elim-7-2-1] backward checking 28 touched variables 0%
c [elim-7-2-1] fully completed backward checking in 1 rounds
c [elim-7-2] subsumed 6 and strengthened 0 clauses in 147630 steps
c [elim-7-2] rescheduled 12 variables 0% by backward subsumption
c [elim-7-3] no variable eliminated in round 3 in 31004 steps
c [elim-7] fully completed in 3 rounds
c [elim-7] transition to [ all 0 rem 0 ] state
c [elim-7] eliminated 149 = 1% variables out of 16457 scheduled
c [elim-7] 149 < 1/100 * 16457 = 164 considered unsuccessful
c [bca-6] limit of 10000000 steps and 284027 added (scaled 2)
c [bca-6] 21590 out of 32618 literals actually usable 66%
c [bca-6] added 5 blocked clauses in 92955 steps
c [sweep-6] limit 3059437 penalty 0 = 0 + 0
c [sweep-6-1] 2749 pos 41.5% + 3880 neg 58.5% = 6629 sched 40.6% ret 9679
c [sweep-6-1] 3071867 steps 296 queries 239.61 avg class size
c [sweep-6-1] 4443 decisions 274 SAT calls 57.76 avg env size
c [sweep-6-1] 4492 variables remain 28% (11816 retained 72%)
c [decomp-23] removed 42 variables
c [sweep-6-1] removed 42 vars (0 failed, 40 eqs, 33 impls)
c [sweep-6] removed 42 vars in TOTAL (1 rounds, 295 queries)
c [phase-count-9] 121369 negative 85.7% of 141695 except 20326 14.3%
c [phase-count-9] 130673 positive 92.2% of 141695 except 11022 7.8%
c [phase-9] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-9] sorted 4127 enqueued variables after 62349 conflicts
c [score-dist-9] active 12139 (75%), one 0 (0%), zero 4127 (25%)
c [score-dist-9] max exp 517, different 17 (3%)
c [score-dist-9] median active exp 511, avg 509.4
c [simplification-9] removed 220 variables 1.3% (16266 remain 26%)
c [simplification-9] removed 7451 irredundant clauses 5.0% (141695 remain 46%)
c [simplification-9] maximum reduction of 5% = max (1%, 5%)
c [simplification-9] large reduction 5% >= 5% limit
c [simplification-9] next conflict interval 2000 = 2000/1
c [simplification-9] penalized conflict interval 2000 = 1 * 2000
c [simplification-9] hard conflict limit 74349 (soft 64349 + delta 10000)
c [simplification-9] new conflict limit 64349 (hard 74349)
c 
c [simplification-10] limit 64349 conflicts (hard 74349) hit after 64350 conflicts
c [quatres-6] found 14712 quaternary clauses 39% in total
c [quatres-6-1] removed 8 duplicate quaternary clauses
c [quatres-6-2] added 28 single-self-subsuming ternary resolvents
c [quatres-6-2] added 373 quaternary resolvents
c [ternres-6] limit 10529777 with penalty 0 = 0 + 0
c [ternres-6] all 16266 free variables schedulable
c [ternres-6] 662 ternary resolvents (75 bin, 587 trn)
c [ternres-6] fully completed ternary resolution
c [card-4] limit 658111 penalty 3 = 3 + 0
c [card-4] found 352 at-most-one constraints of average size 7.4
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 658111 for elimination
c [card-4] 352 out of 352 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [gauss-6] limit 2105955 penalty 0 = 0 + 0
c [gauss-6] extracted 6616 xors of average arity 3.0
c [gauss-6] connected 19800 occurrences of 2465 variables (average 8.0)
c [gauss-6] limit 2105955 penalty 0 = 0 + 0
c [gauss-6] fully completed
c [gauss-6] exported 0 unary, 0 binary and 2 ternary equations
c [decomp-24] removed 8 variables
c [basicprobe-3] limit 52648886 penalty 0 = 0 + 0
c [basicprobe-3-0] 3018 sched 19%, 25 failed, 1 lifted, 3056 hbrs
c [decomp-25] removed 57 variables
c [basicprobe-3-1] 9809 sched 61%, 34 failed, 0 lifted, 3699 hbrs
c [decomp-26] removed 54 variables
c [basicprobe-3-2] 880 probes remain 5% after last round
c [basicprobe-3-2] 66 units = 65 failed (98%) + 1 lifted (2%)
c [basicprobe-3-2] removed 117 variables, found 7242 hbrs
c [bate-2] eliminated 58 asymmetric tautologies during probing
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 588 transitive binary clauses
c [bca-7] limit of 10000000 steps and 280886 added (scaled 2)
c [bca-7] 20311 out of 32284 literals actually usable 63%
c [bca-7] added 1 blocked clauses in 89602 steps
c [sweep-7] limit 3158933 penalty 0 = 0 + 0
c [sweep-7-1] 1926 pos 43.2% + 2533 neg 56.8% = 4459 sched 27.6% ret 11682
c [sweep-7-1] 3167152 steps 314 queries 175.55 avg class size
c [sweep-7-1] 3635 decisions 279 SAT calls 42.43 avg env size
c [sweep-7-1] 3128 variables remain 19% (13013 retained 81%)
c [decomp-27] removed 55 variables
c [sweep-7-1] removed 55 vars (0 failed, 59 eqs, 53 impls)
c [sweep-7] removed 55 vars in TOTAL (1 rounds, 313 queries)
c [phase-count-10] 120050 negative 85.7% of 140120 except 20070 14.3%
c [phase-count-10] 129114 positive 92.1% of 140120 except 11006 7.9%
c [phase-10] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-10] sorted 3983 enqueued variables after 64350 conflicts
c [score-dist-10] active 12103 (75%), one 0 (0%), zero 3983 (25%)
c [score-dist-10] max exp 517, different 17 (3%)
c [score-dist-10] median active exp 511, avg 509.4
c [simplification-10] removed 180 variables 1.1% (16086 remain 26%)
c [simplification-10] removed 1575 irredundant clauses 1.1% (140120 remain 45%)
c [simplification-10] maximum reduction of 1% = max (1%, 1%)
c [simplification-10] geometric conflict interval increment 13333 = 26666 / 2
c [simplification-10] new conflict interval 39999
c [simplification-10] penalized conflict interval 39999 = 1 * 39999
c [simplification-10] hard conflict limit 124348 (soft 104349 + delta 19999)
c [simplification-10] new conflict limit 104349 (hard 124348)
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 -   77.6   16086   140120     88852   30125   8616 31557   10    22   19  46%    374    9   10    9  102%
c 
c [simplification-11] limit 104349 conflicts (hard 124348) hit after 104350 conflicts
c [quatres-7] found 15168 quaternary clauses 39% in total
c [quatres-7-1] removed 12 duplicate quaternary clauses
c [quatres-7-1] added 2 double-self-subsuming ternary resolvents
c [quatres-7-2] added 42 single-self-subsuming ternary resolvents
c [quatres-7-2] added 34 quaternary resolvents
c [ternres-7] limit 17121951 with penalty 0 = 0 + 0
c [ternres-7] all 16086 free variables schedulable
c [ternres-7] 773 ternary resolvents (53 bin, 720 trn)
c [ternres-7] fully completed ternary resolution
c [gauss-7] limit 3424390 penalty 0 = 0 + 0
c [gauss-7] extracted 10115 xors of average arity 3.0
c [gauss-7] connected 30266 occurrences of 2481 variables (average 12.2)
c [gauss-7] limit 3424390 penalty 0 = 0 + 0
c [gauss-7] connected 7724 occurrences of 2481 variables (average 3.1)
c [gauss-7] fully completed
c [gauss-7] exported 0 unary, 0 binary and 2 ternary equations
c [decomp-28] removed 3 variables
c [simpleprobe-4] 500 schedulable variables 3%
c [simpleprobe-4] limit 68487807 penalty 0 = 0 + 0
c [decomp-29] removed 53 variables
c [simpleprobe-4] fully completed simple probing
c [simpleprobe-4] removed 53 variables, found 4055 hbrs, 0 units
c [unhide-8] limit 856097 with penalty 2 = 2 + 0
c [unhide-8-8] 0 units, 0 failed, 4239 tauts, 0 hbrs, 175000 literals
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 504 transitive binary clauses
c [bca-8] limit of 10000000 steps and 278860 added (scaled 2)
c [bca-8] 18809 out of 32062 literals actually usable 59%
c [bca-8] added 11 blocked clauses in 93764 steps
c [sweep-8] limit 5136585 penalty 0 = 0 + 0
c [sweep-8-1] 1445 pos 46.3% + 1674 neg 53.7% = 3119 sched 19.5% ret 12911
c [sweep-8-1] 5142292 steps 585 queries 90.53 avg class size
c [sweep-8-1] 6379 decisions 497 SAT calls 39.17 avg env size
c [sweep-8-1] 1199 variables remain 7% (14830 retained 93%)
c [decomp-30] removed 113 variables
c [sweep-8-1] removed 113 vars (0 failed, 122 eqs, 113 impls)
c [sweep-8] removed 113 vars in TOTAL (1 rounds, 584 queries)
c [phase-count-11] 119612 negative 86.0% of 139102 except 19490 14.0%
c [phase-count-11] 127941 positive 92.0% of 139102 except 11161 8.0%
c [phase-count-11] skipping relative phase luck test
c [phase-11] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-11] sorted 2812 enqueued variables after 104350 conflicts
c [score-dist-11] active 13105 (82%), one 0 (0%), zero 2812 (18%)
c [score-dist-11] max exp 518, different 18 (3%)
c [score-dist-11] median active exp 511, avg 510.0
c [simplification-11] removed 169 variables 1.1% (15917 remain 25%)
c [simplification-11] removed 1018 irredundant clauses 0.7% (139102 remain 45%)
c [simplification-11] maximum reduction of 1% = max (1%, 1%)
c [simplification-11] geometric conflict interval increment 19999 = 39999 / 2
c [simplification-11] new conflict interval 59998
c [simplification-11] penalized conflict interval 59998 = 1 * 59998
c [simplification-11] hard conflict limit 194347 (soft 164348 + delta 29999)
c [simplification-11] new conflict limit 164348 (hard 194347)
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 -   92.1   15917   139102    118320   32375   8891 30666   22    34   20  64%    609   14   24   13  192%
c -  108.5   15917   139102    147135   33685   8975 30681   29    39   20  73%    757   14   30   17  172%
c 
c [simplification-12] limit 164348 conflicts (hard 194347) hit after 164349 conflicts
c [quatres-8] found 15262 quaternary clauses 38% in total
c [quatres-8-1] removed 15 duplicate quaternary clauses
c [quatres-8-2] added 40 single-self-subsuming ternary resolvents
c [quatres-8-2] added 46 quaternary resolvents
c [ternres-8] limit 26591627 with penalty 0 = 0 + 0
c [ternres-8] all 15917 free variables schedulable
c [ternres-8] 559 ternary resolvents (63 bin, 496 trn)
c [ternres-8] fully completed ternary resolution
c [gauss-8] limit 5318325 penalty 0 = 0 + 0
c [gauss-8] extracted 12395 xors of average arity 3.0
c [gauss-8] connected 37113 occurrences of 2447 variables (average 15.2)
c [gauss-8] limit 5318325 penalty 0 = 0 + 0
c [gauss-8] connected 11040 occurrences of 2447 variables (average 4.5)
c [gauss-8] fully completed
c [gauss-8] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-31] removed 6 variables
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 558 transitive binary clauses
c [elim-8] scheduling all variables this time
c [elim-8] scheduled 15911 variables 100%
c [elim-8] boosting limit by 20
c [elim-8] limit of 2659162715 steps penalty 2 = 2 + 0
c [elim-8] rescheduling of touched variables disabled
c [elim-8-1] eliminated 124 variables 1% in round 1 in 26583812 steps
c [elim-8-1] backward subsumption/strengthening limit 26583800
c [elim-8-1-1] backward checking 1630 touched variables 10%
c [elim-8-1-1] fully completed backward checking in 1 rounds
c [elim-8-1] subsumed 16 and strengthened 33 clauses in 932475 steps
c [elim-8-1] rescheduled 164 variables 1% by backward subsumption
c [elim-8-2] eliminated 1 variables 0% in round 2 in 305845 steps
c [elim-8-2] backward subsumption/strengthening limit 305800
c [elim-8-2-1] backward checking 16 touched variables 0%
c [elim-8-2-1] fully completed backward checking in 1 rounds
c [elim-8-2] subsumed 0 and strengthened 0 clauses in 57314 steps
c [elim-8] fully completed in 2 rounds
c [elim-8] transition to [ all 0 rem 0 ] state
c [elim-8] eliminated 125 = 1% variables out of 15911 scheduled
c [elim-8] 125 < 1/100 * 15911 = 159 considered unsuccessful
c [bca-9] limit of 10000000 steps and 275268 added (scaled 2)
c [bca-9] 17457 out of 31574 literals actually usable 55%
c [bca-9] added 5 blocked clauses in 91322 steps
c [sweep-9] limit 7977488 penalty 0 = 0 + 0
c [sweep-9-1] 567 pos 47.8% + 620 neg 52.2% = 1187 sched 7.5% ret 14599
c [sweep-9-1] 4616414 steps 644 queries 42.47 avg class size
c [sweep-9-1] 5871 decisions 574 SAT calls 34.73 avg env size
c [sweep-9-1] fully completed sweeping round
c [decomp-32] removed 101 variables
c [sweep-9-1] removed 101 vars (0 failed, 108 eqs, 96 impls)
c [sweep-9-2] 5976 pos 38.1% + 9709 neg 61.9% = 15685 sched 100.0% ret 0
c [sweep-9-2] 3405112 steps 103 queries 694.17 avg class size
c [sweep-9-2] 2969 decisions 102 SAT calls 113.99 avg env size
c [sweep-9-2] 12463 variables remain 79% (3222 retained 21%)
c [decomp-33] removed 4 variables
c [sweep-9-2] removed 4 vars (0 failed, 3 eqs, 3 impls)
c [sweep-9] removed 105 vars in TOTAL (2 rounds, 745 queries)
c [sort-queue-12] sorted 2263 enqueued variables after 164349 conflicts
c [score-dist-12] active 13418 (86%), one 0 (0%), zero 2263 (14%)
c [score-dist-12] max exp 518, different 18 (3%)
c [score-dist-12] median active exp 512, avg 510.7
c [simplification-12] removed 236 variables 1.5% (15681 remain 25%)
c [simplification-12] removed 1811 irredundant clauses 1.3% (137291 remain 44%)
c [simplification-12] maximum reduction of 1% = max (1%, 1%)
c [simplification-12] geometric conflict interval increment 29999 = 59998 / 2
c [simplification-12] new conflict interval 89997
c [simplification-12] penalized conflict interval 89997 = 1 * 89997
c [simplification-12] hard conflict limit 299344 (soft 254346 + delta 44998)
c [simplification-12] new conflict limit 254346 (hard 299344)
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  125.7   15680   137291    170418   52563   8931 30043   27    41   37  65%    837   12   29   21  140%
c -  133.1   15680   137291    180131   29994   8941 30045   29    34   20  84%   -744    4   29   22  133%
c -  157.6   15680   137291    217118   34022   8973 30061   27    31   21  90%     18   -0   29   24  121%
c -  178.3   15680   137291    252058   35027   9008 30068   25    30   21  84%    434   -1   28   25  113%
c 
c [simplification-13] limit 254346 conflicts (hard 299344) hit after 254348 conflicts
c [quatres-9] found 15364 quaternary clauses 38% in total
c [quatres-9-1] removed 13 duplicate quaternary clauses
c [quatres-9-1] added 2 double-self-subsuming ternary resolvents
c [quatres-9-2] added 23 single-self-subsuming ternary resolvents
c [quatres-9-2] added 59 quaternary resolvents
c [ternres-9] limit 41885020 with penalty 0 = 0 + 0
c [ternres-9] all 15680 free variables schedulable
c [ternres-9] 458 ternary resolvents (36 bin, 422 trn)
c [ternres-9] fully completed ternary resolution
c [decomp-34] removed 6 variables
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 452 transitive binary clauses
c [block-4] scheduling all variables this time
c [block-4] scheduled 15675 variables 100%
c [block-4] limit of 52356275 steps penalty 3 = 3 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 16 blocked clauses
c [block-4] 16 < 1/100 * 137064 = 1370 considered unsuccessful
c [cce-4] boosting limit by 10
c [cce-4] limit of 261781377 steps penalty 3 = 3 + 0
c [cce-4-1] eliminated 2 clauses out of 772 (0%) of length 19
c [cce-4-1] eliminated 16 clauses out of 839 (2%) of length 18
c [cce-4-1] eliminated 42 clauses out of 176 (24%) of length 17
c [cce-4-1] eliminated 3 clauses out of 14 (21%) of length 16
c [cce-4-1] eliminated 42 clauses out of 177 (24%) of length 13
c [cce-4-1] eliminated 1 clauses out of 1128 (0%) of length 11
c [cce-4-1] eliminated 70 clauses out of 814 (9%) of length 10
c [cce-4-1] eliminated 205 clauses out of 1059 (19%) of length 9
c [cce-4-1] eliminated 125 clauses out of 2010 (6%) of length 8
c [cce-4-1] eliminated 178 clauses out of 2055 (9%) of length 7
c [cce-4-1] eliminated 445 clauses out of 4580 (10%) of length 6
c [cce-4-1] eliminated 542 clauses out of 5759 (9%) of length 5
c [cce-4-1] eliminated 1397 clauses out of 12192 (11%) of length 4
c [cce-4-1] completed large round (ATE)
c [cce-4-1] eliminated 3068 large clauses in 133815428 steps
c [cce-4-1] allowing another 66907714 steps for small clauses
c [cce-4-1] scheduling 97622 clauses = 82908 binary + 14714 ternary
c [cce-4-1] tried to eliminate 56061 small clauses 57%
c [cce-4-1] eliminated 9432 binary clauses 11%
c [cce-4-1] eliminated 1094 ternary clauses 7%
c [cce-4-1] eliminated 10526 small clauses 11%
c [cce-4-1] eliminated 10526 small clauses in 261781379 steps
c [cce-4-1] incomplete small round (ATE)
c [cce-4-1] eliminated 13594 covered clauses in round 1
c [cce-4] eliminated 13594 covered clauses in TOTAL during 1 rounds
c [bca-10] limit of 10000000 steps and 247512 added (scaled 2)
c [bca-10] 17506 out of 31352 literals actually usable 56%
c [bca-10] added 5 blocked clauses in 81422 steps
c [sweep-10] limit 12565506 penalty 0 = 0 + 0
c [sweep-10-1] 4654 pos 37.4% + 7804 neg 62.6% = 12458 sched 79.5% ret 3217
c [sweep-10-1] 12666571 steps 940 queries 154.01 avg class size
c [sweep-10-1] 12488 decisions 886 SAT calls 52.24 avg env size
c [sweep-10-1] 1990 variables remain 13% (13685 retained 87%)
c [decomp-35] removed 128 variables
c [sweep-10-1] removed 128 vars (0 failed, 144 eqs, 106 impls)
c [sweep-10] removed 128 vars in TOTAL (1 rounds, 939 queries)
c [sort-queue-13] sorted 2012 enqueued variables after 254348 conflicts
c [score-dist-13] active 13535 (87%), one 0 (0%), zero 2012 (13%)
c [score-dist-13] max exp 519, different 19 (4%)
c [score-dist-13] median active exp 512, avg 511.1
c [simplification-13] removed 133 variables 0.8% (15547 remain 25%)
c [simplification-13] removed 13863 irredundant clauses 10.1% (123428 remain 40%)
c [simplification-13] maximum reduction of 10% = max (1%, 10%)
c [simplification-13] large reduction 10% >= 5% limit
c [simplification-13] next conflict interval 2543 = min (254348/100, 89997)
c [simplification-13] penalized conflict interval 2543 = 1 * 2543
c [simplification-13] hard conflict limit 266891 (soft 256891 + delta 10000)
c [simplification-13] new conflict limit 256891 (hard 266891)
c 
c [simplification-14] limit 256891 conflicts (hard 266891) hit after 256892 conflicts
c [quatres-10] found 14068 quaternary clauses 37% in total
c [quatres-10-1] removed 5 duplicate quaternary clauses
c [quatres-10-1] added 2 double-self-subsuming ternary resolvents
c [quatres-10-2] added 21 single-self-subsuming ternary resolvents
c [quatres-10-2] added 32 quaternary resolvents
c [ternres-10] limit 42255222 with penalty 0 = 0 + 0
c [ternres-10] all 15547 free variables schedulable
c [ternres-10] 549 ternary resolvents (30 bin, 519 trn)
c [ternres-10] fully completed ternary resolution
c [gauss-9] limit 4225522 penalty 1 = 1 + 0
c [gauss-9] extracted 12145 xors of average arity 3.0
c [gauss-9] connected 36295 occurrences of 2416 variables (average 15.0)
c [gauss-9] limit 4225522 penalty 1 = 1 + 0
c [gauss-9] connected 10643 occurrences of 2416 variables (average 4.4)
c [gauss-9] fully completed
c [gauss-9] exported 0 unary, 0 binary and 4 ternary equations
c [decomp-36] removed 7 variables
c [transred-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 573 transitive binary clauses
c [bca-11] limit of 10000000 steps and 247135 added (scaled 2)
c [bca-11] 16903 out of 31082 literals actually usable 54%
c [bca-11] added 5 blocked clauses in 82679 steps
c [sweep-11] boosting sweeping limit by 10
c [sweep-11] limit 126765660 penalty 0 = 0 + 0
c [sweep-11-1] 912 pos 46.0% + 1070 neg 54.0% = 1982 sched 12.8% ret 13558
c [sweep-11-1] 6257796 steps 835 queries 36.29 avg class size
c [sweep-11-1] 7277 decisions 741 SAT calls 31.80 avg env size
c [sweep-11-1] fully completed sweeping round
c [decomp-37] removed 124 variables
c [sweep-11-1] removed 124 vars (0 failed, 153 eqs, 116 impls)
c [sweep-11-2] 5964 pos 38.7% + 9452 neg 61.3% = 15416 sched 100.0% ret 0
c [sweep-11-2] 20704933 steps 1662 queries 66.63 avg class size
c [sweep-11-2] 20016 decisions 1551 SAT calls 46.21 avg env size
c [sweep-11-2] fully completed sweeping round
c [decomp-38] removed 186 variables
c [sweep-11-2] removed 186 vars (0 failed, 237 eqs, 169 impls)
c [sweep-11-3] 5852 pos 38.4% + 9378 neg 61.6% = 15230 sched 100.0% ret 0
c [sweep-11-3] 19407261 steps 1492 queries 41.78 avg class size
c [sweep-11-3] 17830 decisions 1401 SAT calls 47.51 avg env size
c [sweep-11-3] fully completed sweeping round
c [decomp-39] removed 117 variables
c [sweep-11-3] removed 117 vars (0 failed, 175 eqs, 98 impls)
c [sweep-11] removed 427 vars in TOTAL (3 rounds, 3986 queries)
c [sort-queue-14] sorted 1504 enqueued variables after 256892 conflicts
c [score-dist-14] active 13609 (90%), one 0 (0%), zero 1504 (10%)
c [score-dist-14] max exp 519, different 19 (4%)
c [score-dist-14] median active exp 512, avg 510.9
c [simplification-14] removed 434 variables 2.8% (15113 remain 24%)
c [simplification-14] removed 518 irredundant clauses 0.4% (122910 remain 40%)
c [simplification-14] maximum reduction of 3% = max (3%, 0%)
c [simplification-14] geometric conflict interval increment 22499 = 89997 / 4
c [simplification-14] new conflict interval 112496
c [simplification-14] penalized conflict interval 112496 = 1 * 112496
c [simplification-14] hard conflict limit 425636 (soft 369388 + delta 56248)
c [simplification-14] new conflict limit 369388 (hard 425636)
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 -  208.4   15113   122910    287973   36788  10050 38784   29    31   20  91%    683    1   28   25  112%
c i  216.9   15112   122910    302001   47488  10063 38790   24    30   30  80%    749   -0   18   25   71%
c -  229.7   15112   122910    324305   37000  10124 38808   25    35   21  72%   -658    4   30   24  126%
c -  255.2   15112   122910    359707   38896  10173 38820   28    33   28  84%     44    1   27   26  105%
c -  279.0   15112   122910    394934   39191  10192 38827   23    27   28  88%    451   -4   23   24   95%
c 
c [simplification-15] limit 369388 conflicts (hard 425636) hit after 425638 conflicts
c [quatres-11] found 14540 quaternary clauses 35% in total
c [quatres-11-1] removed 13 duplicate quaternary clauses
c [quatres-11-1] added 6 double-self-subsuming ternary resolvents
c [quatres-11-2] added 42 single-self-subsuming ternary resolvents
c [quatres-11-2] added 58 quaternary resolvents
c [ternres-11] limit 73755815 with penalty 0 = 0 + 0
c [ternres-11] all 15112 free variables schedulable
c [ternres-11] 1585 ternary resolvents (101 bin, 1484 trn)
c [ternres-11] fully completed ternary resolution
c [card-5] limit 2304869 penalty 4 = 4 + 0
c [card-5] found 1007 at-most-one constraints of average size 7.2
c [card-5] no at-most-two constraint found
c [card-5] using previous limit 2304869 for elimination
c [card-5] 1007 out of 1007 constraints (100%) meet size limits
c [card-5] no units found
c [card-5] no at-most-one constraints generated
c [gauss-10] limit 14751163 penalty 0 = 0 + 0
c [gauss-10] extracted 12254 xors of average arity 3.0
c [gauss-10] connected 36474 occurrences of 2356 variables (average 15.5)
c [gauss-10] limit 14751163 penalty 0 = 0 + 0
c [gauss-10] connected 10728 occurrences of 2356 variables (average 4.6)
c [gauss-10] fully completed
c [gauss-10] exported 0 unary, 0 binary and 1 ternary equations
c [decomp-40] removed 26 variables
c [treelook-4] limit 921947 penalty 3 = 3 + 0 boost 1
c [treelook-4] scheduled 26905 literals 89%
c [treelook-4] scheduling used 588193 steps
c [treelook-4] scheduled completely
c [treelook-4] limit 921947 penalty 3 = 3 + 0 boost 1
c [treelook-4] used 927282 steps
c [treelook-4] 26777 literals remain 89%
c [treelook-4] 10893 variables remain to probed next time 72%
c [decomp-41] removed 1 variables
c [treelook-4] removed 1 variables, found 339 hbrs
c [unhide-9] limit 1843895 with penalty 3 = 3 + 0
c [unhide-9-10] 1 units, 17 failed, 5865 tauts, 0 hbrs, 299290 literals
c [transred-11] limit 2000000 with penalty 0 = 0 + 0
c [transred-11] removed 509 transitive binary clauses
c [cce-5] limit of 92194769 steps penalty 2 = 2 + 0
c [cce-5-1] eliminated 2 clauses out of 846 (0%) of length 18
c [cce-5-1] eliminated 67 clauses out of 136 (49%) of length 17
c [cce-5-1] eliminated 1 clauses out of 11 (9%) of length 14
c [cce-5-1] eliminated 6 clauses out of 141 (4%) of length 13
c [cce-5-1] eliminated 7 clauses out of 1007 (1%) of length 11
c [cce-5-1] eliminated 39 clauses out of 801 (5%) of length 10
c [cce-5-1] eliminated 51 clauses out of 842 (6%) of length 9
c [cce-5-1] eliminated 71 clauses out of 1832 (4%) of length 8
c [cce-5-1] eliminated 113 clauses out of 1765 (6%) of length 7
c [cce-5-1] eliminated 195 clauses out of 4129 (5%) of length 6
c [cce-5-1] eliminated 346 clauses out of 5275 (7%) of length 5
c [cce-5-1] incomplete large round (ACCE)
c [cce-5-1] eliminated 898 large clauses in 92194774 steps
c [cce-5-1] allowing another 46097387 steps for small clauses
c [cce-5-1] scheduling 78361 clauses = 70509 binary + 7852 ternary
c [cce-5-1] tried to eliminate 12353 small clauses 16%
c [cce-5-1] eliminated 1434 binary clauses 2%
c [cce-5-1] eliminated 154 ternary clauses 2%
c [cce-5-1] eliminated 1588 small clauses 2%
c [cce-5-1] eliminated 1736 small clauses in 92194808 steps
c [cce-5-1] incomplete small round (ACCE)
c [cce-5-1] eliminated 2634 covered clauses in round 1
c [cce-5] eliminated 2634 covered clauses in TOTAL during 1 rounds
c [bca-12] limit of 10000000 steps and 235489 added (scaled 2)
c [bca-12] 14014 out of 30144 literals actually usable 46%
c [bca-12] added 39 blocked clauses in 98081 steps
c [sweep-12] limit 22126744 penalty 0 = 0 + 0
c [sweep-12-1] 5719 pos 37.9% + 9352 neg 62.1% = 15071 sched 100.0% ret 0
c [sweep-12-1] 21300375 steps 1524 queries 56.21 avg class size
c [sweep-12-1] 20859 decisions 1392 SAT calls 58.80 avg env size
c [sweep-12-1] fully completed sweeping round
c [decomp-42] removed 200 variables
c [sweep-12-1] removed 200 vars (0 failed, 234 eqs, 153 impls)
c [sweep-12-2] 5603 pos 37.7% + 9268 neg 62.3% = 14871 sched 100.0% ret 0
c [sweep-12-2] 831195 steps 10 queries 2733.50 avg class size
c [sweep-12-2] 415 decisions 9 SAT calls 105.44 avg env size
c [sweep-12-2] 14807 variables remain 100% (64 retained 0%)
c [sweep-12-2] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-12] removed 200 vars in TOTAL (2 rounds, 1532 queries)
c [sort-queue-15] sorted 1066 enqueued variables after 425638 conflicts
c [score-dist-15] active 13805 (93%), one 0 (0%), zero 1066 (7%)
c [score-dist-15] max exp 520, different 20 (4%)
c [score-dist-15] median active exp 513, avg 511.8
c [simplification-15] removed 241 variables 1.6% (14871 remain 24%)
c [simplification-15] removed 5898 irredundant clauses 4.8% (117012 remain 38%)
c [simplification-15] maximum reduction of 5% = max (2%, 5%)
c [simplification-15] large reduction 5% >= 5% limit
c [simplification-15] next conflict interval 4256 = min (425638/100, 112496)
c [simplification-15] penalized conflict interval 4256 = 1 * 4256
c [simplification-15] hard conflict limit 439894 (soft 429894 + delta 10000)
c [simplification-15] new conflict limit 429894 (hard 439894)
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 -  310.4   14871   117012    434302   40050  10736 35542   21    24   20  87%    710   -4   20   23   90%
c 
c [simplification-16] limit 429894 conflicts (hard 439894) hit after 439895 conflicts
c [quatres-12] found 14406 quaternary clauses 36% in total
c [quatres-12-1] removed 23 duplicate quaternary clauses
c [quatres-12-1] added 2 double-self-subsuming ternary resolvents
c [quatres-12-2] added 41 single-self-subsuming ternary resolvents
c [quatres-12-2] added 46 quaternary resolvents
c [ternres-12] limit 76266952 with penalty 0 = 0 + 0
c [ternres-12] all 14871 free variables schedulable
c [ternres-12] 788 ternary resolvents (76 bin, 712 trn)
c [ternres-12] fully completed ternary resolution
c [gauss-11] limit 15253390 penalty 0 = 0 + 0
c [gauss-11] extracted 12102 xors of average arity 3.0
c [gauss-11] connected 36100 occurrences of 2276 variables (average 15.9)
c [gauss-11] limit 15253390 penalty 0 = 0 + 0
c [gauss-11] connected 10610 occurrences of 2276 variables (average 4.7)
c [gauss-11] fully completed
c [gauss-11] exported 0 unary, 0 binary and 1 ternary equations
c [decomp-44] removed 7 variables
c [basicprobe-4] limit 381334761 penalty 0 = 0 + 0
c [basicprobe-4-0] 927 sched 6%, 9 failed, 0 lifted, 589 hbrs
c [decomp-45] removed 15 variables
c [basicprobe-4-1] 8792 sched 59%, 40 failed, 0 lifted, 3456 hbrs
c [decomp-46] removed 50 variables
c [basicprobe-4-2] 8782 sched 59%, 13 failed, 0 lifted, 796 hbrs
c [decomp-47] removed 16 variables
c [basicprobe-4-3] 8757 sched 59%, 3 failed, 0 lifted, 392 hbrs
c [decomp-48] removed 3 variables
c [basicprobe-4-4] 8745 sched 59%, 1 failed, 0 lifted, 148 hbrs
c [decomp-49] removed 1 variables
c [basicprobe-4-5] 8743 sched 59%, 0 failed, 0 lifted, 53 hbrs
c [basicprobe-4-6] 8742 sched 59%, 0 failed, 0 lifted, 28 hbrs
c [basicprobe-4-7] 8742 sched 59%, 0 failed, 0 lifted, 42 hbrs
c [basicprobe-4-8] 8742 sched 59%, 0 failed, 0 lifted, 19 hbrs
c [basicprobe-4-8] round limit 8 hit
c [basicprobe-4-8] 66 units = 66 failed (100%) + 0 lifted (0%)
c [basicprobe-4-8] removed 85 variables, found 5523 hbrs
c [bate-3] eliminated 32 asymmetric tautologies during probing
c [transred-12] limit 2000000 with penalty 0 = 0 + 0
c [transred-12] removed 636 transitive binary clauses
c [cce-6] limit of 190667380 steps penalty 1 = 1 + 0
c [cce-6-1] eliminated 6 clauses out of 850 (1%) of length 18
c [cce-6-1] eliminated 4 clauses out of 78 (5%) of length 17
c [cce-6-1] eliminated 5 clauses out of 762 (1%) of length 10
c [cce-6-1] eliminated 19 clauses out of 795 (2%) of length 9
c [cce-6-1] eliminated 31 clauses out of 1756 (2%) of length 8
c [cce-6-1] eliminated 34 clauses out of 1646 (2%) of length 7
c [cce-6-1] eliminated 41 clauses out of 3924 (1%) of length 6
c [cce-6-1] eliminated 192 clauses out of 4902 (4%) of length 5
c [cce-6-1] eliminated 468 clauses out of 10264 (5%) of length 4
c [cce-6-1] completed large round (ATE)
c [cce-6-1] eliminated 800 large clauses in 107955226 steps
c [cce-6-1] allowing another 53977613 steps for small clauses
c [cce-6-1] scheduling 81487 clauses = 68346 binary + 13141 ternary
c [cce-6-1] tried to eliminate 39437 small clauses 48%
c [cce-6-1] eliminated 2330 binary clauses 3%
c [cce-6-1] eliminated 441 ternary clauses 3%
c [cce-6-1] eliminated 2771 small clauses 3%
c [cce-6-1] eliminated 2771 small clauses in 190667381 steps
c [cce-6-1] incomplete small round (ATE)
c [cce-6-1] eliminated 3571 covered clauses in round 1
c [cce-6] eliminated 3571 covered clauses in TOTAL during 1 rounds
c [elim-9] scheduling all variables this time
c [elim-9] scheduled 14779 variables 100%
c [elim-9] limit of 100000000 steps penalty 3 = 3 + 0
c [elim-9] rescheduling of touched variables disabled
c [elim-9-1] eliminated 849 variables 6% in round 1 in 20942482 steps
c [elim-9-1] backward subsumption/strengthening limit 20942400
c [elim-9-1-1] backward checking 4967 touched variables 34%
c [elim-9-1-1] fully completed backward checking in 1 rounds
c [elim-9-1] subsumed 144 and strengthened 113 clauses in 1925398 steps
c [elim-9-1] rescheduled 309 variables 2% by backward subsumption
c [elim-9-2] eliminated 34 variables 0% in round 2 in 538372 steps
c [elim-9-2] backward subsumption/strengthening limit 538300
c [elim-9-2-1] backward checking 301 touched variables 2%
c [elim-9-2-1] fully completed backward checking in 1 rounds
c [elim-9-2] subsumed 1 and strengthened 12 clauses in 248252 steps
c [elim-9-2] rescheduled 57 variables 0% by backward subsumption
c [elim-9-3] eliminated 2 variables 0% in round 3 in 125611 steps
c [elim-9-3] backward subsumption/strengthening limit 125600
c [elim-9-3-1] backward checking 24 touched variables 0%
c [elim-9-3-1] fully completed backward checking in 1 rounds
c [elim-9-3] subsumed 0 and strengthened 10 clauses in 78450 steps
c [elim-9] incomplete 22 not tried 0% in round 3
c [elim-9] transition to [ all 1 rem 1 ] state
c [elim-9] eliminated 885 = 6% variables out of 14779 scheduled
c [bca-13] limit of 10000000 steps and 218517 added (scaled 2)
c [bca-13] 14399 out of 27790 literals actually usable 52%
c [bca-13] added 57 blocked clauses in 70507 steps
c [sweep-13] limit 22880085 penalty 0 = 0 + 0
c [sweep-13-1] 5022 pos 36.3% + 8811 neg 63.7% = 13833 sched 99.6% ret 61
c [sweep-13-1] 15175371 steps 1414 queries 40.24 avg class size
c [sweep-13-1] 17046 decisions 1357 SAT calls 40.50 avg env size
c [sweep-13-1] fully completed sweeping round
c [decomp-53] removed 85 variables
c [sweep-13-1] removed 85 vars (0 failed, 121 eqs, 87 impls)
c [sweep-13-2] 4997 pos 36.2% + 8812 neg 63.8% = 13809 sched 100.0% ret 0
c [sweep-13-2] 7708639 steps 486 queries 146.03 avg class size
c [sweep-13-2] 7885 decisions 478 SAT calls 50.11 avg env size
c [sweep-13-2] 3500 variables remain 25% (10309 retained 75%)
c [decomp-54] removed 14 variables
c [sweep-13-2] removed 14 vars (0 failed, 22 eqs, 16 impls)
c [sweep-13] removed 99 vars in TOTAL (2 rounds, 1898 queries)
c [sort-queue-16] sorted 855 enqueued variables after 439895 conflicts
c [score-dist-16] active 12940 (94%), one 0 (0%), zero 855 (6%)
c [score-dist-16] max exp 520, different 20 (4%)
c [score-dist-16] median active exp 513, avg 511.9
c [simplification-16] removed 1076 variables 7.2% (13795 remain 22%)
c [simplification-16] removed 8110 irredundant clauses 6.9% (108902 remain 35%)
c [simplification-16] maximum reduction of 7% = max (7%, 7%)
c [simplification-16] large reduction 7% >= 5% limit
c [simplification-16] next conflict interval 4398 = min (439895/100, 112496)
c [simplification-16] penalized conflict interval 4398 = 1 * 4398
c [simplification-16] hard conflict limit 454293 (soft 444293 + delta 10000)
c [simplification-16] new conflict limit 444293 (hard 454293)
c 
c [simplification-17] limit 444293 conflicts (hard 454293) hit after 454296 conflicts
c [quatres-13] found 13610 quaternary clauses 35% in total
c [quatres-13-1] removed 20 duplicate quaternary clauses
c [quatres-13-1] added 2 double-self-subsuming ternary resolvents
c [quatres-13-2] added 26 single-self-subsuming ternary resolvents
c [quatres-13-2] added 175 quaternary resolvents
c [ternres-13] limit 78270972 with penalty 0 = 0 + 0
c [ternres-13] all 13795 free variables schedulable
c [ternres-13] 928 ternary resolvents (34 bin, 894 trn)
c [ternres-13] fully completed ternary resolution
c [gauss-12] limit 15654194 penalty 0 = 0 + 0
c [gauss-12] extracted 9398 xors of average arity 3.0
c [gauss-12] connected 27988 occurrences of 1858 variables (average 15.1)
c [gauss-12] limit 15654194 penalty 0 = 0 + 0
c [gauss-12] connected 6513 occurrences of 1858 variables (average 3.5)
c [gauss-12] fully completed
c [gauss-12] exported 0 unary, 0 binary and 2 ternary equations
c [decomp-55] removed 8 variables
c [simpleprobe-5] all 13787 free variables schedulable
c [simpleprobe-5] limit 200000000 penalty 0 = 0 + 0
c [decomp-56] removed 79 variables
c [simpleprobe-5] fully completed simple probing
c [simpleprobe-5] removed 79 variables, found 8704 hbrs, 3 units
c [unhide-10] limit 3913548 with penalty 2 = 2 + 0
c [unhide-10-13] 0 units, 0 failed, 11979 tauts, 0 hbrs, 114247 literals
c [transred-13] limit 2000000 with penalty 0 = 0 + 0
c [transred-13] removed 629 transitive binary clauses
c [cce-7] limit of 391354862 steps penalty 0 = 0 + 0
c [cce-7-1] eliminated 4 clauses out of 76 (5%) of length 17
c [cce-7-1] eliminated 4 clauses out of 130 (3%) of length 13
c [cce-7-1] eliminated 4 clauses out of 50 (8%) of length 12
c [cce-7-1] eliminated 130 clauses out of 894 (15%) of length 11
c [cce-7-1] eliminated 31 clauses out of 673 (5%) of length 10
c [cce-7-1] eliminated 41 clauses out of 793 (5%) of length 9
c [cce-7-1] eliminated 65 clauses out of 1956 (3%) of length 8
c [cce-7-1] eliminated 94 clauses out of 1658 (6%) of length 7
c [cce-7-1] eliminated 117 clauses out of 4099 (3%) of length 6
c [cce-7-1] eliminated 212 clauses out of 5102 (4%) of length 5
c [cce-7-1] eliminated 391 clauses out of 9943 (4%) of length 4
c [cce-7-1] completed large round (ACCE)
c [cce-7-1] eliminated 1093 large clauses in 123171052 steps
c [cce-7-1] allowing another 61585526 steps for small clauses
c [cce-7-1] scheduling 73791 clauses = 62247 binary + 11544 ternary
c [cce-7-1] tried to eliminate 73791 small clauses 100%
c [cce-7-1] eliminated 4112 binary clauses 7%
c [cce-7-1] eliminated 799 ternary clauses 7%
c [cce-7-1] eliminated 4911 small clauses 7%
c [cce-7-1] eliminated 4911 small clauses in 339458872 steps
c [cce-7-1] completed small round (ACCE)
c [cce-7-1] completed small and large (ACCE)
c [cce-7-1] eliminated 6004 covered clauses in round 1
c [cce-7-2] eliminated 13 clauses out of 126 (10%) of length 13
c [cce-7-2] eliminated 24 clauses out of 764 (3%) of length 11
c [cce-7-2] eliminated 11 clauses out of 642 (2%) of length 10
c [cce-7-2] eliminated 4 clauses out of 752 (1%) of length 9
c [cce-7-2] eliminated 11 clauses out of 1891 (1%) of length 8
c [cce-7-2] eliminated 11 clauses out of 1564 (1%) of length 7
c [cce-7-2] eliminated 28 clauses out of 3982 (1%) of length 6
c [cce-7-2] incomplete large round (ACCE)
c [cce-7-2] eliminated 102 large clauses in 51896014 steps
c [cce-7-2] allowing another 25948007 steps for small clauses
c [cce-7-2] scheduling 68881 clauses = 58135 binary + 10746 ternary
c [cce-7-2] tried to eliminate 6914 small clauses 10%
c [cce-7-2] eliminated 3 binary clauses 0%
c [cce-7-2] eliminated 3 small clauses 0%
c [cce-7-2] eliminated 3 small clauses in 51895993 steps
c [cce-7-2] incomplete small round (ACCE)
c [cce-7-2] eliminated 105 covered clauses in round 2
c [cce-7] eliminated 6109 covered clauses in TOTAL during 2 rounds
c [bca-14] limit of 10000000 steps and 204077 added (scaled 2)
c [bca-14] 12940 out of 27418 literals actually usable 47%
c [bca-14] added 53 blocked clauses in 77133 steps
c [sweep-14] limit 23481291 penalty 0 = 0 + 0
c [sweep-14-1] 1286 pos 37.2% + 2167 neg 62.8% = 3453 sched 25.2% ret 10255
c [sweep-14-1] 10593380 steps 939 queries 34.63 avg class size
c [sweep-14-1] 11552 decisions 882 SAT calls 37.78 avg env size
c [sweep-14-1] fully completed sweeping round
c [decomp-57] removed 82 variables
c [sweep-14-1] removed 82 vars (0 failed, 84 eqs, 70 impls)
c [sweep-14-2] 4991 pos 36.6% + 8635 neg 63.4% = 13626 sched 100.0% ret 0
c [sweep-14-2] 12894706 steps 744 queries 69.01 avg class size
c [sweep-14-2] 13051 decisions 719 SAT calls 59.07 avg env size
c [sweep-14-2] 1560 variables remain 11% (12061 retained 89%)
c [decomp-58] removed 46 variables
c [sweep-14-2] removed 46 vars (0 failed, 54 eqs, 34 impls)
c [sweep-14] removed 128 vars in TOTAL (2 rounds, 1681 queries)
c [sort-queue-17] sorted 801 enqueued variables after 454296 conflicts
c [score-dist-17] active 12779 (94%), one 0 (0%), zero 801 (6%)
c [score-dist-17] max exp 520, different 20 (4%)
c [score-dist-17] median active exp 513, avg 512.0
c [simplification-17] removed 215 variables 1.6% (13580 remain 22%)
c [simplification-17] removed 7270 irredundant clauses 6.7% (101632 remain 33%)
c [simplification-17] maximum reduction of 7% = max (2%, 7%)
c [simplification-17] large reduction 7% >= 5% limit
c [simplification-17] next conflict interval 4542 = min (454296/100, 112496)
c [simplification-17] penalized conflict interval 4542 = 1 * 4542
c [simplification-17] hard conflict limit 468838 (soft 458838 + delta 10000)
c [simplification-17] new conflict limit 458838 (hard 468838)
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  344.2   13579   101632    458790   50173  10413 39224   20    24   28  84%    808   -3   14   22   63%
c 
c [simplification-18] limit 458838 conflicts (hard 468838) hit after 468838 conflicts
c [quatres-14] found 13401 quaternary clauses 36% in total
c [quatres-14-1] removed 6 duplicate quaternary clauses
c [quatres-14-1] added 5 double-self-subsuming ternary resolvents
c [quatres-14-2] added 62 single-self-subsuming ternary resolvents
c [quatres-14-2] added 69 quaternary resolvents
c [ternres-14] limit 80536061 with penalty 0 = 0 + 0
c [ternres-14] all 13579 free variables schedulable
c [ternres-14] 819 ternary resolvents (71 bin, 748 trn)
c [ternres-14] fully completed ternary resolution
c [gauss-13] limit 16107212 penalty 0 = 0 + 0
c [gauss-13] extracted 8981 xors of average arity 3.0
c [gauss-13] connected 26915 occurrences of 1742 variables (average 15.5)
c [gauss-13] limit 16107212 penalty 0 = 0 + 0
c [gauss-13] connected 5992 occurrences of 1742 variables (average 3.4)
c [gauss-13] fully completed
c [gauss-13] exported 0 unary, 0 binary and 1 ternary equations
c [decomp-59] removed 3 variables
c [transred-14] limit 2000000 with penalty 0 = 0 + 0
c [transred-14] removed 756 transitive binary clauses
c [block-5] scheduling all variables this time
c [block-5] scheduled 13576 variables 100%
c [block-5] limit of 50000000 steps penalty 4 = 4 + 0
c [block-5] fully completed
c [block-5] transition to [ all 0 rem 0 ] state
c [block-5] eliminated 253 blocked clauses
c [block-5] 253 < 1/100 * 101572 = 1015 considered unsuccessful
c [cce-8] boosting limit by 10
c [cce-8] limit of 4026803090 steps penalty 0 = 0 + 0
c [cce-8-1] eliminated 1 clauses out of 631 (0%) of length 10
c [cce-8-1] eliminated 5 clauses out of 746 (1%) of length 9
c [cce-8-1] eliminated 63 clauses out of 1879 (3%) of length 8
c [cce-8-1] eliminated 26 clauses out of 1547 (2%) of length 7
c [cce-8-1] eliminated 28 clauses out of 3945 (1%) of length 6
c [cce-8-1] eliminated 58 clauses out of 4844 (1%) of length 5
c [cce-8-1] eliminated 33 clauses out of 9473 (0%) of length 4
c [cce-8-1] completed large round (ATE)
c [cce-8-1] eliminated 214 large clauses in 95860518 steps
c [cce-8-1] allowing another 47930259 steps for small clauses
c [cce-8-1] scheduling 65019 clauses = 57939 binary + 7080 ternary
c [cce-8-1] tried to eliminate 65019 small clauses 100%
c [cce-8-1] eliminated 311 binary clauses 1%
c [cce-8-1] eliminated 480 ternary clauses 7%
c [cce-8-1] eliminated 791 small clauses 1%
c [cce-8-1] eliminated 791 small clauses in 256067625 steps
c [cce-8-1] completed small round (ATE)
c [cce-8-1] eliminated 1005 covered clauses in round 1
c [cce-8-2] completed large round (ATE)
c [cce-8-2] allowing another 47170765 steps for small clauses
c [cce-8-2] scheduling 64228 clauses = 57628 binary + 6600 ternary
c [cce-8-2] tried to eliminate 64228 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 1005 covered clauses in TOTAL during 2 rounds
c [cce-8] 1005 < 1/100 * 101319 = 1013 considered unsuccessful
c [elim-10] no untried remaining variables left
c [elim-10] scheduled 13542 variables 100%
c [elim-10] limit of 200000000 steps penalty 2 = 2 + 0
c [elim-10] rescheduling of touched variables disabled
c [elim-10-1] eliminated 686 variables 5% in round 1 in 19137519 steps
c [elim-10-1] backward subsumption/strengthening limit 19137500
c [elim-10-1-1] backward checking 4618 touched variables 34%
c [elim-10-1-1] fully completed backward checking in 1 rounds
c [elim-10-1] subsumed 5 and strengthened 18 clauses in 1671745 steps
c [elim-10-1] rescheduled 67 variables 0% by backward subsumption
c [elim-10-2] eliminated 5 variables 0% in round 2 in 156357 steps
c [elim-10-2] backward subsumption/strengthening limit 156300
c [elim-10-2-1] backward checking 29 touched variables 0%
c [elim-10-2-1] fully completed backward checking in 1 rounds
c [elim-10-2] subsumed 0 and strengthened 2 clauses in 69999 steps
c [elim-10-2] rescheduled 6 variables 0% by backward subsumption
c [elim-10-3] no variable eliminated in round 3 in 15240 steps
c [elim-10] fully completed in 3 rounds
c [elim-10] transition to [ all 0 rem 0 ] state
c [elim-10] eliminated 691 = 5% variables out of 13542 scheduled
c [bca-15] limit of 10000000 steps and 199146 added (scaled 2)
c [bca-15] 12719 out of 25704 literals actually usable 49%
c [bca-15] added 72 blocked clauses in 75923 steps
c [sweep-15] limit 24160818 penalty 0 = 0 + 0
c [sweep-15-1] 531 pos 37.3% + 894 neg 62.7% = 1425 sched 11.1% ret 11426
c [sweep-15-1] 5393247 steps 607 queries 32.63 avg class size
c [sweep-15-1] 6453 decisions 573 SAT calls 34.22 avg env size
c [sweep-15-1] fully completed sweeping round
c [decomp-60] removed 54 variables
c [sweep-15-1] removed 54 vars (0 failed, 55 eqs, 49 impls)
c [sweep-15-2] 4516 pos 35.3% + 8281 neg 64.7% = 12797 sched 100.0% ret 0
c [sweep-15-2] 15214740 steps 1166 queries 48.46 avg class size
c [sweep-15-2] 16664 decisions 1150 SAT calls 46.11 avg env size
c [sweep-15-2] fully completed sweeping round
c [decomp-61] removed 44 variables
c [sweep-15-2] removed 44 vars (1 failed, 50 eqs, 37 impls)
c [sweep-15-3] 4490 pos 35.2% + 8263 neg 64.8% = 12753 sched 100.0% ret 0
c [sweep-15-3] 3611392 steps 164 queries 420.77 avg class size
c [sweep-15-3] 3765 decisions 163 SAT calls 67.79 avg env size
c [sweep-15-3] 7462 variables remain 59% (5291 retained 41%)
c [decomp-62] removed 2 variables
c [sweep-15-3] removed 2 vars (0 failed, 1 eqs, 2 impls)
c [sweep-15] removed 100 vars in TOTAL (3 rounds, 1934 queries)
c [sort-queue-18] sorted 615 enqueued variables after 468838 conflicts
c [score-dist-18] active 12136 (95%), one 0 (0%), zero 615 (5%)
c [score-dist-18] max exp 520, different 20 (4%)
c [score-dist-18] median active exp 514, avg 512.1
c [simplification-18] removed 828 variables 6.1% (12751 remain 20%)
c [simplification-18] removed 2488 irredundant clauses 2.4% (99144 remain 32%)
c [simplification-18] maximum reduction of 6% = max (6%, 2%)
c [simplification-18] large reduction 6% >= 5% limit
c [simplification-18] next conflict interval 4688 = min (468838/100, 112496)
c [simplification-18] penalized conflict interval 4688 = 1 * 4688
c [simplification-18] hard conflict limit 483526 (soft 473526 + delta 10000)
c [simplification-18] new conflict limit 473526 (hard 483526)
c 
c [simplification-19] limit 473526 conflicts (hard 483526) hit after 483527 conflicts
c [quatres-15] found 13336 quaternary clauses 36% in total
c [quatres-15-1] removed 12 duplicate quaternary clauses
c [quatres-15-1] added 1 double-self-subsuming ternary resolvents
c [quatres-15-2] added 26 single-self-subsuming ternary resolvents
c [quatres-15-2] added 163 quaternary resolvents
c [ternres-15] limit 82593504 with penalty 0 = 0 + 0
c [ternres-15] all 12751 free variables schedulable
c [ternres-15] 670 ternary resolvents (18 bin, 652 trn)
c [ternres-15] fully completed ternary resolution
c [gauss-14] limit 16518700 penalty 0 = 0 + 0
c [gauss-14] extracted 7910 xors of average arity 3.0
c [gauss-14] connected 23694 occurrences of 1519 variables (average 15.6)
c [gauss-14] limit 16518700 penalty 0 = 0 + 0
c [gauss-14] connected 4400 occurrences of 1519 variables (average 2.9)
c [gauss-14] fully completed
c [gauss-14] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-63] removed 4 variables
c [treelook-5] limit 2064837 penalty 2 = 2 + 0 boost 1
c [treelook-5] scheduled 22742 literals 89%
c [treelook-5] scheduling used 496346 steps
c [treelook-5] scheduled completely
c [treelook-5] limit 2064837 penalty 2 = 2 + 0 boost 1
c [treelook-5] used 2076843 steps
c [treelook-5] 22395 literals remain 88%
c [treelook-5] 9252 variables remain to probed next time 73%
c [treelook-5] removed 0 variables, found 611 hbrs
c [transred-15] limit 2000000 with penalty 0 = 0 + 0
c [transred-15] removed 740 transitive binary clauses
c [elim-11] scheduling all variables this time
c [elim-11] scheduled 12747 variables 100%
c [elim-11] limit of 400000000 steps penalty 1 = 1 + 0
c [elim-11] rescheduling of touched variables disabled
c [elim-11-1] eliminated 65 variables 1% in round 1 in 18802747 steps
c [elim-11-1] backward subsumption/strengthening limit 18802700
c [elim-11-1-1] backward checking 843 touched variables 7%
c [elim-11-1-1] fully completed backward checking in 1 rounds
c [elim-11-1] subsumed 1 and strengthened 4 clauses in 437673 steps
c [elim-11-1] rescheduled 12 variables 0% by backward subsumption
c [elim-11-2] eliminated 2 variables 0% in round 2 in 32881 steps
c [elim-11-2] backward subsumption/strengthening limit 32800
c [elim-11-2-1] backward checking 19 touched variables 0%
c [elim-11-2-1] incomplete backward checking 0 remain 0%
c [elim-11-2] subsumed 0 and strengthened 5 clauses in 32801 steps
c [elim-11-2] rescheduled 15 variables 0% by backward subsumption
c [elim-11-3] no variable eliminated in round 3 in 9497 steps
c [elim-11] fully completed in 3 rounds
c [elim-11] transition to [ all 0 rem 0 ] state
c [elim-11] eliminated 67 = 1% variables out of 12747 scheduled
c [elim-11] 67 < 1/100 * 12747 = 127 considered unsuccessful
c [bca-16] limit of 10000000 steps and 197832 added (scaled 2)
c [bca-16] 11699 out of 25362 literals actually usable 46%
c [bca-16] added 18 blocked clauses in 82923 steps
c [sweep-16] limit 24778051 penalty 0 = 0 + 0
c [sweep-16-1] 2468 pos 33.3% + 4953 neg 66.7% = 7421 sched 58.5% ret 5259
c [sweep-16-1] 17738279 steps 1037 queries 34.63 avg class size
c [sweep-16-1] 17142 decisions 1020 SAT calls 49.65 avg env size
c [sweep-16-1] fully completed sweeping round
c [decomp-65] removed 36 variables
c [sweep-16-1] removed 36 vars (0 failed, 41 eqs, 27 impls)
c [sweep-16-2] 4392 pos 34.7% + 8252 neg 65.3% = 12644 sched 100.0% ret 0
c [sweep-16-2] 7045124 steps 293 queries 222.07 avg class size
c [sweep-16-2] 6866 decisions 288 SAT calls 74.49 avg env size
c [sweep-16-2] 4534 variables remain 36% (8110 retained 64%)
c [decomp-66] removed 7 variables
c [sweep-16-2] removed 7 vars (0 failed, 8 eqs, 8 impls)
c [sweep-16] removed 43 vars in TOTAL (2 rounds, 1328 queries)
c [sort-queue-19] sorted 569 enqueued variables after 483527 conflicts
c [score-dist-19] active 12068 (95%), one 0 (0%), zero 569 (5%)
c [score-dist-19] max exp 520, different 20 (4%)
c [score-dist-19] median active exp 514, avg 512.2
c [simplification-19] removed 114 variables 0.9% (12637 remain 20%)
c [simplification-19] removed 669 irredundant clauses 0.7% (98475 remain 32%)
c [simplification-19] maximum reduction of 1% = max (1%, 1%)
c [simplification-19] geometric conflict interval increment 56248 = 112496 / 2
c [simplification-19] new conflict interval 168744
c [simplification-19] penalized conflict interval 168744 = 1 * 168744
c [simplification-19] hard conflict limit 736643 (soft 652271 + delta 84372)
c [simplification-19] new conflict limit 652271 (hard 736643)
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 -  380.6   12637    98475    504106   40125  10600 35881   21    25   19  82%   -331    0   22   21  105%
c i  387.1   12636    98475    516010   50125  10601 35888   18    20   30  87%   -106   -5   19   20   96%
c -  404.8   12636    98475    548969   41500  10624 35897   18    22   21  83%   -208   -1   17   19   87%
c -  429.7   12636    98475    589574   41419  10645 35900   16    19   29  88%    361   -3   19   18  104%
c -  455.3   12636    98475    639337   40657  10684 35909   15    16   27  89%    714   -3   14   16   87%
c 
c [simplification-20] limit 652271 conflicts (hard 736643) hit after 659603 conflicts
c [quatres-16] found 13764 quaternary clauses 35% in total
c [quatres-16-1] removed 7 duplicate quaternary clauses
c [quatres-16-1] added 4 double-self-subsuming ternary resolvents
c [quatres-16-2] added 31 single-self-subsuming ternary resolvents
c [quatres-16-2] added 92 quaternary resolvents
c [ternres-16] limit 111190490 with penalty 0 = 0 + 0
c [ternres-16] all 12636 free variables schedulable
c [ternres-16] 369 ternary resolvents (13 bin, 356 trn)
c [ternres-16] fully completed ternary resolution
c [decomp-67] removed 2 variables
c [basicprobe-5] limit 400000000 penalty 0 = 0 + 0
c [basicprobe-5-0] 7348 sched 58%, 15 failed, 0 lifted, 2715 hbrs
c [decomp-68] removed 18 variables
c [basicprobe-5-1] 7321 sched 58%, 1 failed, 0 lifted, 412 hbrs
c [decomp-69] removed 2 variables
c [basicprobe-5-2] 7312 sched 58%, 0 failed, 0 lifted, 138 hbrs
c [basicprobe-5-3] 7310 sched 58%, 0 failed, 0 lifted, 74 hbrs
c [decomp-71] removed 1 variables
c [basicprobe-5-4] 7309 sched 58%, 0 failed, 0 lifted, 35 hbrs
c [basicprobe-5-5] 7309 sched 58%, 0 failed, 0 lifted, 25 hbrs
c [basicprobe-5-6] 7309 sched 58%, 0 failed, 0 lifted, 20 hbrs
c [basicprobe-5-7] 7309 sched 58%, 0 failed, 0 lifted, 6 hbrs
c [basicprobe-5-8] 7309 sched 58%, 0 failed, 0 lifted, 13 hbrs
c [basicprobe-5-8] round limit 8 hit
c [basicprobe-5-8] 16 units = 16 failed (100%) + 0 lifted (0%)
c [basicprobe-5-8] removed 21 variables, found 3438 hbrs
c [bate-4] eliminated 21 asymmetric tautologies during probing
c [unhide-11] limit 2500000 with penalty 3 = 3 + 0
c [unhide-11-15] 0 units, 0 failed, 3934 tauts, 0 hbrs, 76180 literals
c [transred-16] limit 2000000 with penalty 0 = 0 + 0
c [transred-16] removed 537 transitive binary clauses
c [cce-9] limit of 277976226 steps penalty 1 = 1 + 0
c [cce-9-1] eliminated 1 clauses out of 1079 (0%) of length 18
c [cce-9-1] eliminated 2 clauses out of 83 (2%) of length 17
c [cce-9-1] eliminated 1 clauses out of 4 (25%) of length 14
c [cce-9-1] eliminated 2 clauses out of 83 (2%) of length 13
c [cce-9-1] eliminated 6 clauses out of 63 (10%) of length 12
c [cce-9-1] eliminated 118 clauses out of 868 (14%) of length 11
c [cce-9-1] eliminated 17 clauses out of 583 (3%) of length 10
c [cce-9-1] eliminated 87 clauses out of 646 (13%) of length 9
c [cce-9-1] eliminated 45 clauses out of 1787 (3%) of length 8
c [cce-9-1] eliminated 51 clauses out of 1607 (3%) of length 7
c [cce-9-1] eliminated 77 clauses out of 3869 (2%) of length 6
c [cce-9-1] eliminated 197 clauses out of 5173 (4%) of length 5
c [cce-9-1] eliminated 318 clauses out of 9794 (3%) of length 4
c [cce-9-1] completed large round (ACCE)
c [cce-9-1] eliminated 922 large clauses in 110973089 steps
c [cce-9-1] allowing another 55486544 steps for small clauses
c [cce-9-1] scheduling 61885 clauses = 55660 binary + 6225 ternary
c [cce-9-1] tried to eliminate 61885 small clauses 100%
c [cce-9-1] eliminated 603 binary clauses 1%
c [cce-9-1] eliminated 310 ternary clauses 5%
c [cce-9-1] eliminated 913 small clauses 1%
c [cce-9-1] eliminated 913 small clauses in 276058575 steps
c [cce-9-1] completed small round (ACCE)
c [cce-9-1] eliminated 1835 covered clauses in round 1
c [cce-9-2] incomplete large round (ACCE)
c [cce-9-2] allowing another 958834 steps for small clauses
c [cce-9-2] scheduling 60972 clauses = 55057 binary + 5915 ternary
c [cce-9-2] tried to eliminate 190 small clauses 0%
c [cce-9-2] eliminated 1 binary clauses 0%
c [cce-9-2] eliminated 1 small clauses 0%
c [cce-9-2] eliminated 1 small clauses in 1917664 steps
c [cce-9-2] incomplete small round (ACCE)
c [cce-9-2] eliminated 1 covered clauses in round 2
c [cce-9] eliminated 1836 covered clauses in TOTAL during 2 rounds
c [bca-17] limit of 10000000 steps and 193063 added (scaled 2)
c [bca-17] 11124 out of 25230 literals actually usable 44%
c [bca-17] added 36 blocked clauses in 80755 steps
c [sweep-17] limit 33357147 penalty 0 = 0 + 0
c [sweep-17-1] 1646 pos 36.4% + 2877 neg 63.6% = 4523 sched 35.9% ret 8091
c [sweep-17-1] 10859799 steps 964 queries 33.79 avg class size
c [sweep-17-1] 12130 decisions 959 SAT calls 36.53 avg env size
c [sweep-17-1] fully completed sweeping round
c [decomp-76] removed 40 variables
c [sweep-17-1] removed 40 vars (0 failed, 45 eqs, 35 impls)
c [sweep-17-2] 4404 pos 35.0% + 8170 neg 65.0% = 12574 sched 100.0% ret 0
c [sweep-17-2] 20128197 steps 1133 queries 39.99 avg class size
c [sweep-17-2] 18969 decisions 1118 SAT calls 47.87 avg env size
c [sweep-17-2] fully completed sweeping round
c [decomp-77] removed 30 variables
c [sweep-17-2] removed 30 vars (0 failed, 38 eqs, 37 impls)
c [sweep-17-3] 4387 pos 35.0% + 8157 neg 65.0% = 12544 sched 100.0% ret 0
c [sweep-17-3] 2403962 steps 62 queries 805.71 avg class size
c [sweep-17-3] 2682 decisions 61 SAT calls 93.98 avg env size
c [sweep-17-3] 10562 variables remain 84% (1982 retained 16%)
c [decomp-78] removed 2 variables
c [sweep-17-3] removed 2 vars (0 failed, 2 eqs, 0 impls)
c [sweep-17] removed 72 vars in TOTAL (3 rounds, 2156 queries)
c [sort-queue-20] sorted 509 enqueued variables after 659603 conflicts
c [score-dist-20] active 12033 (96%), one 0 (0%), zero 509 (4%)
c [score-dist-20] max exp 521, different 21 (4%)
c [score-dist-20] median active exp 514, avg 512.6
c [simplification-20] removed 94 variables 0.7% (12542 remain 20%)
c [simplification-20] removed 2352 irredundant clauses 2.4% (96123 remain 31%)
c [simplification-20] maximum reduction of 2% = max (1%, 2%)
c [simplification-20] geometric conflict interval increment 56248 = 168744 / 3
c [simplification-20] new conflict interval 224992
c [simplification-20] penalized conflict interval 224992 = 1 * 224992
c [simplification-20] hard conflict limit 997091 (soft 884595 + delta 112496)
c [simplification-20] new conflict limit 884595 (hard 997091)
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 -  494.9   12542    96123    686329   43541  10797 35860   16    19   19  85%    872   -0   19   16  119%
c -  524.1   12542    96123    732922   44261  10814 35873   15    16   20  90%    950   -2   14   16   86%
c -  550.4   12542    96123    774008   44258  10858 35894   17    20   30  84%    984    1   18   16  109%
c -  580.8   12542    96123    817114   44425  10876 35907   15    16   29  91%   1003   -3   13   16   77%
c 1  586.6   12542    96123    827061   53427  10884 35907   16    20   39  78%   1006    1   15   16   91%
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
s SATISFIABLE
c
c bate: 206 basic ate = 167 trn 81% + 39 lrg 19% in 4 updates
c bcas: 17 count, 494 added (758 skipped), 1542308 steps
c bkwd: tried 222579 clauses, 443446 lits, 1.99 lits/clause
c bkwd: checked 10297354 occs, 46.26 occs/clause, 23.22 occs/lit
c bkwd: subsumed 14 binary, 87 ternary, 397 large
c bkwd: strengthened 2 binary, 22 ternary (100% self), 1823 large (0% self)
c blkd: 5 bces, 1827 removed, 3808038 resolutions, 8713018 steps
c blkd: 3544 blocking literals 3%, 110 pure
c bump: 841267 bumped seen, 434390229 lits 516.4 on average
c card: 5 count, 0 units, 46 am1, 18914057 steps
c card: 90 rescheduled, 633 eliminated, 8722 resolved, 19254 subsumed
c card: 2553 at-most-one constraints found, average size 5.27
c card: 2553 at-most-one constraints used 100%, average size 5.27
c card: 0 at-most-two constraints found, average size 0.00
c card: 0 at-most-two constraints used 0%, average size 0.00
c cces: 9 cces, 29909 eliminated, 26636 ate 89%, 3273 abce 11%
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: 1125294 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 131 gcs, 0 rescored clauses, 0 rescored vars
c dcps: 78 decompositions, 16028 equivalent 25%
c deco: 0 decision-only clauses 0%, 0% reduction
c decs: 1675747 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 11 elims, 26240 eliminated 41%, 151 pure 1%
c elms: 29 rounds, 2.6 rounds/bve
c elms: 20798 small 79%, 5181 large 20%
c elms: 33231 tried small, 20798 succeeded 63%, 12433 failed 37%
c elms: 15571 subsumed, 27181 strengthened, 1232 blocked
c elms: 5473362 copies, 7523527 resolutions, 889281 ipos
c elms: 4516078 subchks, 12077320 strchks
c gaus: 14 extractions, 130779 extracted, 3.0 size, 3 max
c gaus: exported 1 units, 0 binary and 25 ternary equations
c gaus: 10 gc, 206798588 steps, 103399294 extr 50%, 17843905 elim 9%
c glue: 19.3 orig avg, 19.3 real avg, 4.1 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 125703 = 83235 simple 66% + 41427 trn 33% + 1041 lrg 1%, 1586 sub 1%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 841267 clauses, 113.7 length
c lrnd: 95687639 lits = 262978261 orig - 167290622 removed 64%
c lrnd: 182948 uips 22%, 531619 flips 63%
c mins: 836224 mins 99%, 935 bin 0%, 4108 size 0%
c mins: 728585741 poisoned searches, 45211804 hits, 6% hit rate
c mins: 930606785 used twice searches, 4703641 hits, 1% hit rate
c move: moved 24250, 19744 bin 81%, 4506 trn 19%
c otfs: 1938 driving 33%, 3951 restarting 67%
c otfs: str 5889, 5561 red 94%, 328 irr 6%
c otfs: str 5889, 0 bin 0%, 845 trn 14%, 5044 lrg 86%
c otfs: sub 121, 119 red 98%, 2 irr 2%
c otfs: sub 121, 0 bin 0%, 10 trn 8%, 111 lrg 92%
c phas: 11 computed, 21986 set, 21985 pos (100%), 1 neg (0%)
c prbs: 5 basic, 335669 probed, 311 failed, 10 lifted
c prbs: 5 simple, 207745 probed, 165 failed, 13595 eqs
c prbs: 5 treelook, 550 probed, 0 failed, 0 lifted
c prom: 79720 locked 2% out of 4176521 tried
c prps: 1416874197 props, 806 props/dec
c prps: 95% srch, 5% simp, 0% lkhd
c quat: 16 count, 3072 quat, 504 self1, 32 self2, 789 dup
c queu: 20 sorted, 1675747 next (99175 steps 0.06)
c queu: 434565056 enq (1111508857 steps 2.56), 434390229 deq 100%
c redc: 7900 clauses 22%, 36056 tried 4%, 138 sat 0%
c redc: 17633 lits 5%, 387200 tried 0%, 138 sat 0%
c redc: 373 times jump level reduced, 5.9 levels on average
c reds: 19 count, 43529.5 conflicts per reduce
c reds: 0 memlim 0%, 19 arith 100%
c reds: 560620 collected 92%, 50000 retired 8%
c rmbd: 22322 removed, 16134 red 72%
c rsts: 15432 restarts 86%, 2534 skipped 14%
c rsts: 2534 saturating 100%, 0 reuse 0%
c rsts: 0 kept 0.0% average 0.0%
c scnc: 0 count, 1.000 min (0/1000), 1.000 max (0/1000)
c simp: 20 count, 20 confs 100%, 0 vars 0%
c simp: 0 its 0%, 0 bin 0%, 0 trns 0%
c subl: 841267 count (2091870 tried 2.5), 116050 sub out of 835148 (13.9%)
c swps: 17 count, 29 rounds, 20824 queries (718.1/round)
c swps: 19065 sat calls, 1247 unsat (0.8% success rate)
c swps: 272002 decisions 14.3, 16144 conflicts 0.8
c swps; 111.5 avg class size, 49.2 avg environment size
c swps: 1 failed, 2556 impls, 2995 equivs
c swp0: 6933 type 0 queries, 2152 unsat (31.0%), 6243 sat (90.0%)
c swp1: 13891 type 1 queries, 6624 unsat (47.7%), 11586 sat (83.4%)
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: 5034449 calls to obtain time
c tops: 8644 fixed 14%, 12 its, 68921.75 confs/it
c trds: 16 transitive reductions, 8378 removed, 3 failed
c trds: 77145 nodes, 242828 edges, 32002726 steps
c trim: 1111217 words, 4.2 MB
c trnr: 16 count, 2275 bin, 22646 trn, 63894501 steps
c unhd: 11 count, 15 rounds, 18769592 steps
c unhd: 279 non-trivial sccs of average size 2.1
c unhd: 11 units, 11 bin, 0 trn, 0 lrg
c unhd: 66 failed, 56 stamp, 0 lits, 2 bin, 4 trn, 0 lrg
c unhd: 36014 tauts, 1129 bin 3%, 2870 trn 8%, 497 lrg 1%
c unhd: 36014 tauts, 31518 stamp 88%, 32337 red 90%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 995600 str, 11 bin 0%, 1181 trn 0%, 994408 lrg 100%, 985634 red 99%
c vars: 12542 remaining 20% and 50912 removed 80% out of 63454
c vars: 8644 fixed 14%, 26240 eliminated 41%, 16028 equivalent 25%
c vsts: 14615237622 visits, 96% srch, 4% simp, 0% lkhd
c vsts: 10.4 search visits per propagation, 17015.2 per conflict
c wchs: 1692641081 pushed, 39584286 enlarged, 229 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all         838220        560620         50000      78640898      27078461        402764
c 
c  0 0         23289   3       520   0         0   0  53767837  68  14998835  55     77551  19     0.5
c  1 5          8176   1      1102   0      2477   5   7141187   9<  2651997  10<    24389   6     0.2
c  2 6         35103   4     12100   2      6951  14   9663662  12   4565833  17     59192  15     1.4
c  3 9        122726  15     61639  11     12953  26   4643515   6   2390256   9     71374  18<    5.7
c  4 14       296608  35<   200893  36<    14702  29<  2210521   3   1520468   6     95078  24    21.5
c  5 21       259161  31    203836  36     10500  21    965015   1    750400   3     58621  15    14.9
c  6 30        90885  11     78557  14      2341   5    244950   0    197622   1     16369   4    12.9
c  7 41         2259   0      1970   0        68   0      4193   0      3046   0       190   0     0.6
c  8 54           12   0         3   0         8   0        17   0         4   0         0   0     0.0
c  9 69            1   0         0   0         0   0         1   0         0   0         0   0     0.0
c 
c avg                  4.2           4.5           3.6           0.7           1.1           2.8
c std                  1.3           1.0           1.2           1.2           1.5           1.8
c 
c   94.489  16% bump
c   22.952   4% cce
c   17.878   3% probe
c   14.420   2% sweep
c    8.310   1% gauss
c    6.452   1% elim
c 
c   11.756 < 1% rest (below)
c 
c    5.920   1% unhide
c    1.598   0% transred
c    1.233   0% bca
c    0.890   0% decide
c    0.846   0% block
c    0.569   0% quatres
c    0.522   0% ternres
c    0.177   0% card
c    0.000   0% locs
c    0.000   0% queuesort
c    0.000   0% rescore
c ==================================
c    1.929   0% preprocessing     2%
c   82.281  14% inprocessing     98%
c ==================================
c   84.210  14% simplifying
c  502.402  86% search
c ==================================
c  586.617 100% all
c 
c        827061 conflicts,        1409.9 confs/sec
c          1439 ternaries,         574.7 confs/ternary
c           498 binaries,         1660.8 confs/binary
c            12 iterations,      68921.8 confs/iteration
c 
c            19 reductions,          0.0 redus/sec,  43529.5 confs/reduction
c         15432 restarts,           26.3 rests/sec,     53.6 confs/restart
c       1675747 decisions,        2856.6 decis/sec,      2.0 decis/conflict
c    1416874197 propagations,  2415329.2 props/sec,    845.5 props/decision
c 
c 586.6 seconds, 70.7 MB
c launch: done
