c launch: /data/cnf/sc2014/app/SAT_dat.k30-30_rule.cnf.bz2
c host: atom23
c Lingeling SAT Solver
c 
c Version ayv 86bf266b9332599f1b876e28a02fe8427aeaa2db
c 
c Copyright (C) 2010-2014 Armin Biere JKU Linz Austria.
c All rights reserved.
c 
c released Sat Oct 11 12:11:52 CEST 2014
c compiled Sat Oct 11 12:11:52 CEST 2014
c 
c gcc (Ubuntu 4.8.2-19ubuntu1) 4.8.2
c -Wall -O3 -DNDBLSCR  -I../yalsat -DNLGLOG -DNDEBUG -DNCHKSOL -DNLGLPICOSAT
c -DNLGLDRUPLIG
c Linux cluster2 3.13.0-36-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 --actavgmax=112
c --actdblarithlim=3
c --actgeomlim=2
c --actgsdul=7
c --acts=2
c --actstdmax=112
c --actstdmin=10
c --actvlim=200000
c --agile=1
c --agilelim=30
c --agilesinint=100000
c --bate=1
c --batewait=2
c --bca=1
c --bcamaxeff=10000000
c --bcaminuse=100
c --bcawait=2
c --bva=0
c --bias=2
c --binlocsdel=10
c --binsimpdel=2
c --bkwdscale=2
c --blkboost=10
c --blkboostvlim=1000000
c --blkclslim=1000000
c --blklarge=1
c --blkmaxeff=800000000
c --blkmineff=50000000
c --blkocclim=1000000
c --blkocclim1=100000
c --blkocclim2=10000
c --blkreleff=100
c --blkrtc=0
c --blksched2b2=0
c --blkschedmin=0
c --blkschedprod=0
c --blkschedpure=1
c --blkschedsum=1
c --blksmall=1
c --blksuccesslim=10000
c --blksuccessrat=1000
c --block=1
c --blockwait=1
c --boost=1
c --bumpbcplits=0
c --bumpclslits=0
c --bumpseenaftermin=0
c --bumpseenbeforemin=1
c --bumpseenlits=1
c --bumpseenminsize=3
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 --cce=3
c --cceboost=10
c --cceboostvlim=1000000
c --cce2wait=1
c --cce3wait=2
c --ccemaxeff=2147483647
c --ccemineff=30000000
c --cceonlyifstuck=0
c --ccereleff=20
c --ccertc=0
c --ccesuccesslim=10000
c --ccesuccessrat=1000
c --ccewait=2
c --cgrclsr=1
c --cgrclsrwait=2
c --cgreleff=1
c --cgrextand=1
c --cgrexteq=1
c --cgrextite=1
c --cgrextunits=1
c --cgrextxor=1
c --cgrmaxeff=8000000
c --cgrmaxority=20
c --cgrmineff=200000
c --cintinc=20000
c --cintincdiv=1
c --cintmaxhard=10000000
c --cintmaxsoft=1000000
c --cliff=1
c --cliffmaxeff=100000000
c --cliffmineff=10000000
c --cliffreleff=8
c --cliffwait=2
c --clim=-1
c --compact=0
c --deco=1
c --decolim=30
c --decompose=1
c --defragfree=50
c --defragint=10000000
c --delmax=10
c --dlim=-1
c --drup=0
c --druplig=0
c --elim=1
c --elmaxeff=800000000
c --elmblk=1
c --elmblkwait=1
c --elmboost=40
c --elmclslim=1000000
c --elmfull=0
c --elmineff=20000000
c --elmlitslim=200
c --elmocclim=1000000
c --elmocclim1=1000
c --elmocclim2=100
c --elmreleff=200
c --elmroundlim=3
c --elmrtc=0
c --elmsched2b2=0
c --elmschediff=0
c --elmschedmin=0
c --elmschedprod=0
c --elmschedpure=1
c --elmschedsum=1
c --elmsuccesslim=1000
c --elmsuccessrat=1000
c --exitonabort=0
c --factmax=100000
c --factor=3
c --flipdur=10
c --flipint=10
c --flipldmod=4
c --fliplevels=6
c --flipping=1
c --fliptop=1
c --flipvlim=100000
c --force=0
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=3
c --gluescale=4
c --import=1
c --incredcint=1
c --incredconfslim=0
c --incsavevisits=0
c --inprocessing=1
c --irrlim=1
c --itlocsdel=100
c --itsimpdel=20
c --jwhred=1
c --keepmaxglue=1
c --lftmaxeff=20000000
c --lftmineff=500000
c --lftreleff=6
c --lftroundlim=5
c --lhbr=1
c --lift=1
c --liftlrg=3
c --liftwait=2
c --lkhd=2
c --lkhdmisifelmrtc=0
c --locs=0
c --locsboost=2
c --locscint=10000
c --locsdec=2
c --locset=2
c --locsexport=1
c --locsmaxeff=100000
c --locsmineff=1000
c --locsclim=1000000
c --locsred=0
c --locsreleff=5
c --locsrtc=0
c --locsvared=100
c --locswait=2
c --maxglue=2147483647
c --maxscorexp=500
c --mega=0
c --megaint=4
c --megawait=2
c --memlim=-1
c --minimize=2
c --minlocalgluelim=30
c --minrecgluelim=20
c --mocint=1000
c --move=2
c --otfs=1
c --otfsbump=0
c --otfsconf=0
c --penmax=4
c --phase=0
c --phaseflip=0
c --phasegluebit=0
c --phaseneginit=0
c --plain=0
c --plim=-1
c --prbasic=1
c --prbasicmaxeff=100000000
c --prbasicmineff=1000000
c --prbasicreleff=10
c --prbasicroundlim=9
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 --psm=3
c --pure=1
c --randec=0
c --randecflipint=0
c --randecint=1000
c --rdp=0
c --rdpclslim=3
c --rdplim=100
c --rdpmaxeff=10000000
c --rdpmineff=10000
c --rdpmodelm=0
c --rdpreleff=2
c --rdpwait=2
c --redfixed=0
c --redinoutinc=100
c --redlbound=0
c --redlexpfac=10
c --redlinc=1000
c --redlinit=4000
c --redlmaxabs=1000000
c --redlmaxinc=200
c --redlmaxrel=300
c --redlminabs=500
c --redlmininc=10
c --redlminrel=10
c --redloutinc=10000
c --redoutclim=5000
c --redoutvlim=1000
c --reduce=2
c --rephase=1
c --rephaseinc=10000
c --restart=2
c --restartinit=0
c --restartint=5
c --restartintscale=0
c --reusetrail=1
c --rmincpen=4
c --rstinoutinc=110
c --saturating=70
c --scincinc=200
c --score=5
c --seed=0
c --simpdelay=0
c --simpen=0
c --simpidiv=3
c --simpinterdelay=2000
c --simpiscale=100
c --simplify=2
c --simprtc=5
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 --synclsall=1
c --synclsglue=8
c --synclsint=100
c --synclslen=40
c --syncunint=111111
c --tabr=3
c --tabrcfactor=2
c --tabrkeep=3
c --tabrvfactor=4
c --termint=122222
c --ternres=1
c --ternresboost=5
c --ternresrtc=0
c --ternreswait=2
c --transred=1
c --transredwait=2
c --trdmaxeff=2000000
c --trdmineff=100000
c --trdreleff=10
c --treelook=1
c --treelookboost=20
c --treelookfull=0
c --treelooklrg=1
c --treelookmaxeff=50000000
c --treelookmineff=300000
c --treelookreleff=1
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 --wait=1
c --waitmax=4
c --witness=0
c --check=0
c --log=-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 [init-scores] score increment factor 1.200000d+00 (--scincinc=200)
c [init-scores] maxium score limit 1.000000d+500 (--maxscorexp=500)
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c *    0.0   63044   309889         0       0      0     0   0  0.0   0.0   15
c 
c [simplification-1] limit of 0 conflicts hit after 0 conflicts
c [card-1] limit 2000000 penalty 0 = 0 + 0
c [card-1] found 809 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] 809 out of 809 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] generated 93 at-most-one constraints, 87 used 94%
c [card-1] exported 87 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 6889 variables
c [simpleprobe-1] 6975 variables remain 16% (36786 retained)
c [simpleprobe-1] removed 6889 variables, found 60254 hbrs, 127 units
c [unhide-1] limit 115261 based on 230522 irredundant clauses
c [unhide-1-1] 0 units, 3 failed, 583 tauts, 0 hbrs, 659 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 43748 variables 100%
c [elim-1] boosting limit by 40
c [elim-1] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-1-1] eliminated 22955 variables 52% in round 1 in 22499585 steps
c [elim-1-1] backward subsumption/strengthening limit 44999170
c [elim-1-1] subsumed 265 and strengthened 2031 clauses in 12680953 steps
c [elim-1-1] rescheduled 3530 variables 8% by backward subsumption
c [elim-1-2] eliminated 300 variables 1% in round 2 in 3028080 steps
c [elim-1-2] backward subsumption/strengthening limit 6056160
c [elim-1-2] subsumed 0 and strengthened 0 clauses in 6056214 steps
c [elim-1] fully completed in 2 rounds
c [elim-1] transition to [ all 0 rem 0 ] state
c [elim-1] eliminated 23255 = 53% variables out of 43748
c [phase-1] phase bias: 10581 positive 52%, 9912 negative 48%
c [simplification-1] removed 35868 variables 63.6% (20493 remain 33%)
c [simplification-1] removed 138928 irredundant clauses 44.8% (170961 remain 55%)
c [simplification-1] maximum reduction of 64% = max (64%, 45%)
c [simplification-1] large reduction 64% >= 5% limit
c [simplification-1] new conflict interval 1000 = 2000/2
c [simplification-1] penalized conflict interval 1000 = 1 * 1000
c [simplification-1] new conflict limit 1000
c [cut-width] 9286, max 13974, min4 7141 at 60%, min10 6439 at 88%
c [cut-width] cut-width based bias 1
c [decision-order] bias 1, old 1
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c R    2.6   20493   170961         5       4      0 14252   7  3.2  32.0   11
c R    2.6   20493   170961        20      15      2 14252   8  3.7  30.2   11
c R    2.6   20493   170961        61      47      8 14254   9  4.4  78.1   11
c R    2.6   20493   170961       167     128     16 14262  11  5.3  82.7   11
c i    2.6   20492   170961       216     167     20 14266  10  5.2  78.6   11
c i    2.6   20491   170961       217     167     20 14266  11  5.2  78.0   11
c i    2.6   20490   170961       219     167     20 14267  11  5.1  77.4   11
c i    2.6   20489   170961       222     168     20 14268  11  5.1  76.8   11
c i    2.6   20482   170961       224     168     21 14268  11  5.0  76.7   11
c i    2.6   20474   170961       414     296     55 14282  10  4.8  70.0   11
c R    2.6   20466   170961       416     297     55 14283  10  4.7  69.8   11
c i    2.7   20465   170961       511     356     77 14292   8  4.6  66.5   11
c i    2.7   20464   170961       512     356     77 14292   7  4.6  66.2   11
c i    2.7   20463   170961       514     357     77 14292   7  4.6  65.8   11
c i    2.7   20462   170961       623     446     88 14297   7  4.7  74.6   11
c i    2.7   20461   170961       628     450     88 14297   7  4.6  74.2   11
c i    2.7   20460   170961       875     650    103 14306   9  5.1  70.6   11
c i    2.7   20459   170961       876     650    103 14306   9  5.1  70.6   11
c i    2.7   20458   170961       877     650    103 14306   9  5.1  70.6   11
c R    2.7   20458   170961       991     749    110 14313   9  5.0  69.0   11
c i    2.7   20457   170961      1072     817    117 14315   8  5.0  67.4   11
c i    2.7   20456   170961      1073     817    117 14315   8  5.0  67.3   11
c i    2.7   20455   170961      1074     817    117 14315   8  5.0  67.3   11
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i    2.7   20454   170961      1075     817    117 14315   8  5.0  67.2   11
c i    2.7   20453   170961      1081     817    121 14315   8  5.0  67.1   11
c i    2.7   20452   170961      1082     817    120 14316   8  5.0  67.1   11
c 
c [simplification-2] limit of 1573 conflicts hit after 1573 conflicts
c [decomp-3] removed 152 variables
c [simpleprobe-2] 5004 schedulable variables 25%
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [decomp-4] removed 107 variables
c [simpleprobe-2] 4872 variables remain 24% (15362 retained)
c [simpleprobe-2] removed 107 variables, found 2175 hbrs, 4 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 28323 literals 70%
c [treelook-1] scheduling used 300036 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 354611 steps
c [treelook-1] 28190 literals remain 70%
c [treelook-1] 19142 variables remain to probed next time 95%
c [treelook-1] removed 0 variables, found 889 hbrs
c [basicprobe-1] limit 1000000 penalty 0 = 0 + 0
c [basicprobe-1-0] 12711 probes remain 63% after last round
c [basicprobe-1-0] 12 units = 12 failed (100%) + 0 lifted (0%)
c [basicprobe-1-0] removed 61 variables, found 1859 hbrs
c [unhide-2] limit 100000 with penalty 0 = 0 + 0
c [unhide-2-2] 11 units, 75 failed, 2240 tauts, 0 hbrs, 3409 literals
c [block-1] scheduling all variables this time
c [block-1] scheduled 20136 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 799 blocked clauses
c [cce-1] boosting limit by 10
c [cce-1] limit of 300000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 208 clauses out of 1073 (19%) of length 19
c [cce-1-1] eliminated 7 clauses out of 855 (1%) of length 18
c [cce-1-1] eliminated 16 clauses out of 847 (2%) of length 17
c [cce-1-1] eliminated 23 clauses out of 123 (19%) of length 13
c [cce-1-1] eliminated 12 clauses out of 218 (6%) of length 12
c [cce-1-1] eliminated 138 clauses out of 2552 (5%) of length 11
c [cce-1-1] eliminated 27 clauses out of 659 (4%) of length 10
c [cce-1-1] eliminated 121 clauses out of 1019 (12%) of length 9
c [cce-1-1] eliminated 136 clauses out of 2663 (5%) of length 8
c [cce-1-1] eliminated 287 clauses out of 2714 (11%) of length 7
c [cce-1-1] eliminated 361 clauses out of 4529 (8%) of length 6
c [cce-1-1] eliminated 328 clauses out of 5670 (6%) of length 5
c [cce-1-1] eliminated 2079 clauses out of 13504 (15%) of length 4
c [cce-1-1] completed large round (ATE)
c [cce-1-1] eliminated 3743 large clauses in 193850967 steps
c [cce-1-1] allowing another 96925483 steps for small clauses
c [cce-1] scheduling 112335 clauses = 102768 binary + 9567 ternary
c [cce-1] tried to eliminate 41232 small clauses 37%
c [cce-1] eliminated 5604 small clauses 5%
c [cce-1] eliminated 5092 binary clauses 5%
c [cce-1] eliminated 512 ternary clauses 5%
c [cce-1-1] eliminated 5604 small clauses in 300000001 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 9347 covered clauses in round 1
c [cce-1] eliminated 9347 covered clauses in TOTAL during 1 rounds
c [elim-2] scheduling all variables this time
c [elim-2] scheduled 20123 variables 100%
c [elim-2] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-2] incomplete 243 not tried 1% in round 1
c [elim-2] transition to [ all 1 rem 1 ] state
c [elim-2] eliminated 678 = 3% variables out of 20123
c [bca-1] limit of 10000000 steps
c [bca-1] 35194 out of 38892 literals actually usable 90%
c [bca-1] added 305 blocked clauses in 111330 steps
c [phase-2] phase bias: 72 positive 49%, 74 negative 51%
c [simplification-2] removed 1007 variables 4.9% (19445 remain 31%)
c [simplification-2] removed 15242 irredundant clauses 8.9% (155719 remain 50%)
c [simplification-2] maximum reduction of 9% = max (5%, 9%)
c [simplification-2] large reduction 9% >= 5% limit
c [simplification-2] new conflict interval 2000 = 2000/1
c [simplification-2] penalized conflict interval 2000 = 1 * 2000
c [simplification-2] new conflict limit 3573
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i   14.1   19444   155719      1973    1405    722 19864   8  5.0  58.3   11
c R   14.2   19444   155719      2311    1691    744 19875  10  5.1  58.6   11
c i   14.2   19443   155719      2373    1740    750 19880   9  5.1  57.9   11
c 
c [simplification-3] limit of 3787 conflicts hit after 3788 conflicts
c [ternres-1] boosting ternary resolution limit by 5
c [ternres-1] limit 20000000 with penalty 0 = 0 + 0
c [ternres-1] all 19443 free variables schedulable
c [ternres-1] 11576 ternary resolvents (1129 bin, 10447 trn)
c [ternres-1] fully completed ternary resolution
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 3158 at-most-one constraints of average size 3.0
c [card-2] found 43 at-most-two constraints of average size 4.0
c [card-2] using previous limit 1000000 for elimination
c [card-2] 3201 out of 3201 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 10959 xors of average arity 2.9
c [gauss-1] connected 31695 occurrences of 3103 variables (average 10.2)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] exported 0 unary, 0 binary and 8 ternary equations
c [decomp-6] removed 403 variables
c [cgrclsr-1] limit 200000 penalty 0 = 0 + 0
c [cgrclsr-1] all 19040 free variables schedulable
c [cgrclsr-1] fully completed congruence closure
c [cgrclsr-1] removed 2 variables
c [lift-1] limit 500000 with penalty 0 = 0 + 0
c [lift-1] using 13384 probes 70%
c [lift-1] 12 units, 5 impls, 2 eqs in 1 rounds
c [lift-1] 18820 variables remain 99% (133 retained)
c [lift-1] removed 85 variables
c [cliff-1] limit of 10000000 steps penalty 0 = 0 + 0
c [cliff-1] failed 33, lifted 63
c [unhide-3] limit 100000 with penalty 0 = 0 + 0
c [unhide-3-3] 8 units, 1 failed, 751 tauts, 0 hbrs, 1706 literals
c [transred-1] limit 152591 based on 152591 irredundant clauses
c [transred-1] removed 20 transitive binary clauses
c [block-2] scheduling all variables this time
c [block-2] scheduled 18820 variables 100%
c [block-2] limit of 50000000 steps penalty 0 = 0 + 0
c [block-2] fully completed
c [block-2] transition to [ all 0 rem 0 ] state
c [block-2] eliminated 226 blocked clauses
c [cce-2] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-2-1] eliminated 14 clauses out of 848 (2%) of length 19
c [cce-2-1] eliminated 2 clauses out of 817 (0%) of length 18
c [cce-2-1] eliminated 4 clauses out of 844 (0%) of length 17
c [cce-2-1] eliminated 45 clauses out of 167 (27%) of length 13
c [cce-2-1] eliminated 6 clauses out of 212 (3%) of length 12
c [cce-2-1] eliminated 33 clauses out of 2356 (1%) of length 11
c [cce-2-1] eliminated 9 clauses out of 680 (1%) of length 10
c [cce-2-1] incomplete large round (ABCE)
c [cce-2-1] eliminated 113 large clauses in 30000001 steps
c [cce-2-1] allowing another 15000000 steps for small clauses
c [cce-2] scheduling 110763 clauses = 93360 binary + 17403 ternary
c [cce-2] tried to eliminate 3148 small clauses 3%
c [cce-2] eliminated 388 small clauses 0%
c [cce-2] eliminated 317 binary clauses 0%
c [cce-2] eliminated 71 ternary clauses 0%
c [cce-2-1] eliminated 388 small clauses in 30000001 steps
c [cce-2-1] incomplete small round (ABCE)
c [cce-2-1] eliminated 501 covered clauses in round 1
c [cce-2] eliminated 501 covered clauses in TOTAL during 1 rounds
c [elim-3] 243 variables 1% will be scheduled this time
c [elim-3] scheduled 243 variables 1%
c [elim-3] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-3-1] eliminated 28 variables 0% in round 1 in 10290217 steps
c [elim-3-1] backward subsumption/strengthening limit 9709783
c [elim-3-1] subsumed 1239 and strengthened 11 clauses in 8252384 steps
c [elim-3-1] rescheduled 637 variables 3% by backward subsumption
c [elim-3-2] eliminated 47 variables 0% in round 2 in 1335652 steps
c [elim-3-2] backward subsumption/strengthening limit 121747
c [elim-3-2] subsumed 0 and strengthened 0 clauses in 121796 steps
c [elim-3] fully completed in 2 rounds
c [elim-3] transition to [ all 0 rem 0 ] state
c [elim-3] eliminated 81 = 0% variables out of 18790
c [bca-2] limit of 10000000 steps
c [bca-2] 30599 out of 37420 literals actually usable 82%
c [bca-2] added 21 blocked clauses in 97402 steps
c [phase-3] phase bias: 5 positive 16%, 27 negative 84%
c [simplification-3] removed 734 variables 3.8% (18709 remain 30%)
c [simplification-3] removed 5824 irredundant clauses 3.7% (149895 remain 48%)
c [simplification-3] maximum reduction of 4% = max (4%, 4%)
c [simplification-3] geometric conflict interval increment 4000 = 20000 / 5
c [simplification-3] new conflict interval 4000
c [simplification-3] penalized conflict interval 4000 = 1 * 4000
c [simplification-3] new conflict limit 7788
c [tabula-rasa-1] number clauses 149895 drops below limit 154944
c [flush-cache] 0 binary, 0 ternary, 2793 large
c [flushphases] 18709 phases reset fully
c [phase-4] phase bias: 407 positive 47%, 463 negative 53%
c [tabula-rasa-1] new conflict interval 20000
c [tabula-rasa-1] conflict limit 20000 does not change
c [tabula-rasa-1] new variable limit 4677 and clause limit 74947
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c R   17.3   18709   149895      5254    1288   6421 19853  11  5.4  58.0   11
c i   17.4   18708   149895      6581    2403   6508 19905   6  5.7  56.1   11
c i   17.6   18707   149895      7873    3515   6583 19938   8  5.6  55.8   12
c i   17.6   18706   149895      7874    3515   6583 19938   8  5.6  55.8   12
c 
c [simplification-4] limit of 8074 conflicts hit after 8074 conflicts
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] all 18706 free variables schedulable
c [ternres-2] 1214 ternary resolvents (112 bin, 1102 trn)
c [ternres-2] fully completed ternary resolution
c [gauss-2] limit 2000000 penalty 0 = 0 + 0
c [gauss-2] extracted 8721 xors of average arity 3.0
c [gauss-2] connected 25928 occurrences of 2818 variables (average 9.2)
c [gauss-2] limit 2000000 penalty 0 = 0 + 0
c [gauss-2] connected 5901 occurrences of 2818 variables (average 2.1)
c [gauss-2] fully completed
c [decomp-7] removed 95 variables
c [gauss-2] exported 0 unary, 7 binary and 9 ternary equations
c [treelook-2] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-2] scheduled 17535 literals 47%
c [treelook-2] scheduling used 150030 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-2] used 170142 steps
c [treelook-2] 17512 literals remain 47%
c [treelook-2] 14404 variables remain to probed next time 77%
c [treelook-2] removed 0 variables, found 34 hbrs
c [cgrclsr-2] limit 200000 penalty 0 = 0 + 0
c [cgrclsr-2] all 18611 free variables schedulable
c [cgrclsr-2] 1868 variables remain 10% (16740 retained)
c [cgrclsr-2] removed 3 variables
c [lift-2] limit 500000 with penalty 0 = 0 + 0
c [lift-2] using 12968 probes 70%
c [lift-2] 8 units, 8 impls, 6 eqs in 1 rounds
c [lift-2] 18357 variables remain 99% (237 retained)
c [lift-2] removed 14 variables
c [cliff-2] limit of 10000000 steps penalty 0 = 0 + 0
c [cliff-2] failed 59, lifted 45
c [unhide-4] limit 100000 with penalty 0 = 0 + 0
c [unhide-4-4] 0 units, 8 failed, 2115 tauts, 0 hbrs, 5402 literals
c [transred-2] limit 237910 with penalty 0 = 0 + 0
c [transred-2] removed 24 transitive binary clauses
c [block-3] scheduling all variables this time
c [block-3] scheduled 18444 variables 100%
c [block-3] limit of 50000000 steps penalty 0 = 0 + 0
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 220 blocked clauses
c [cce-3] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-3-1] eliminated 4 clauses out of 5 (80%) of length 16
c [cce-3-1] eliminated 14 clauses out of 31 (45%) of length 15
c [cce-3-1] eliminated 9 clauses out of 34 (26%) of length 14
c [cce-3-1] eliminated 14 clauses out of 161 (9%) of length 13
c [cce-3-1] eliminated 6 clauses out of 192 (3%) of length 12
c [cce-3-1] eliminated 23 clauses out of 2290 (1%) of length 11
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 70 large clauses in 30000001 steps
c [cce-3-1] allowing another 15000000 steps for small clauses
c [cce-3] scheduling 99230 clauses = 91095 binary + 8135 ternary
c [cce-3] tried to eliminate 3009 small clauses 3%
c [cce-3] eliminated 418 small clauses 0%
c [cce-3] eliminated 383 binary clauses 0%
c [cce-3] eliminated 35 ternary clauses 0%
c [cce-3-1] eliminated 418 small clauses in 30000001 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 488 covered clauses in round 1
c [cce-3] eliminated 488 covered clauses in TOTAL during 1 rounds
c [elim-4] scheduling all variables this time
c [elim-4] scheduled 18433 variables 100%
c [elim-4] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-4] incomplete 560 not tried 3% in round 1
c [elim-4] transition to [ all 1 rem 1 ] state
c [elim-4] eliminated 258 = 1% variables out of 18433
c [bca-3] limit of 10000000 steps
c [bca-3] 29823 out of 36352 literals actually usable 82%
c [bca-3] added 104 blocked clauses in 93147 steps
c [phase-5] phase bias: 1 positive 33%, 2 negative 67%
c [simplification-4] removed 531 variables 2.8% (18175 remain 29%)
c [simplification-4] removed 4034 irredundant clauses 2.7% (145861 remain 47%)
c [simplification-4] maximum reduction of 3% = max (3%, 3%)
c [simplification-4] geometric conflict interval increment 5000 = 20000 / 4
c [simplification-4] new conflict interval 25000
c [simplification-4] penalized conflict interval 25000 = 1 * 25000
c [simplification-4] new conflict limit 33074
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i   20.5   18174   145861      8611    3864   6746 18916   7  5.6  54.8   11
c i   20.5   18142   145861      8612    3864   6746 18916   7  5.6  54.8   11
c -   20.8   18142   145861     10709    3635   6882 18984   7  5.6  54.2   11
c i   20.8   18141   145861     11171    4045   6903 18992   8  5.6  54.5   12
c R   20.8   18140   145861     11781    4593   6928 19000  10  5.7  54.6   12
c i   21.2   18139   145861     15075    7450   7127 19084   8  5.6  54.5   12
c -   21.3   18139   145861     15589    5394   7167 19097   7  5.6  54.1   11
c i   21.7   18138   145861     19115    8499   7343 19177   7  5.7  55.3   12
c i   21.8   18137   145861     19861    9167   7382 19189   8  5.8  55.0   12
c -   22.0   18136   145861     20998    7163   7442 19217   7  5.8  54.2   12
c R   22.5   18136   145861     26149   11864   7608 19279  11  6.2  57.6   13
c -   22.6   18136   145861     26645    8784   7630 19298   7  6.2  57.0   12
c i   22.8   18135   145861     28197   10159   7698 19336   8  6.1  56.7   12
c i   22.8   18134   145861     28209   10162   7704 19338   8  6.1  56.7   12
c i   23.0   18082   145861     29791   11589   7763 19378   7  6.1  56.3   12
c i   23.1   18081   145861     30364   12103   7790 19382   8  6.1  56.1   12
c i   23.3   18080   145861     32438   13961   7881 19413   6  6.2  55.9   12
c -   23.5   18079   145861     33468   10927   7935 19431  10  6.2  55.4   12
c 
c [simplification-5] limit of 34222 conflicts hit after 34223 conflicts
c [ternres-3] limit 4000000 with penalty 0 = 0 + 0
c [ternres-3] all 18079 free variables schedulable
c [ternres-3] 1733 ternary resolvents (28 bin, 1705 trn)
c [ternres-3] fully completed ternary resolution
c [gauss-3] limit 2000000 penalty 0 = 0 + 0
c [gauss-3] extracted 8130 xors of average arity 3.0
c [gauss-3] connected 24016 occurrences of 2708 variables (average 8.9)
c [gauss-3] limit 2000000 penalty 0 = 0 + 0
c [gauss-3] connected 4786 occurrences of 2708 variables (average 1.8)
c [gauss-3] fully completed
c [decomp-10] removed 158 variables
c [gauss-3] exported 0 unary, 11 binary and 43 ternary equations
c [basicprobe-2] limit 1092872 penalty 0 = 0 + 0
c [basicprobe-2-0] 10485 probes remain 59% after last round
c [basicprobe-2-0] 10 units = 10 failed (100%) + 0 lifted (0%)
c [basicprobe-2-0] removed 18 variables, found 1380 hbrs
c [bate-1] eliminated 2 asymmetric tautologies during probing
c [cgrclsr-3] limit 200000 penalty 0 = 0 + 0
c [cgrclsr-3] 1798 schedulable variables 10%
c [cgrclsr-3] fully completed congruence closure
c [cgrclsr-3] removed 3 variables
c [lift-3] limit 655723 with penalty 0 = 0 + 0
c [lift-3] using 12502 probes 70%
c [lift-3] 3 units, 11 impls, 6 eqs in 1 rounds
c [lift-3] 17516 variables remain 98% (375 retained)
c [lift-3] removed 9 variables
c [cliff-3] limit of 10000000 steps penalty 0 = 0 + 0
c [cliff-3] failed 47, lifted 44
c [unhide-5] limit 218574 with penalty 0 = 0 + 0
c [unhide-5-5] 1 units, 5 failed, 482 tauts, 0 hbrs, 8763 literals
c [transred-3] limit 1092872 with penalty 0 = 0 + 0
c [transred-3] removed 138 transitive binary clauses
c [block-4] scheduling all variables this time
c [block-4] scheduled 17780 variables 100%
c [block-4] limit of 50000000 steps penalty 0 = 0 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 430 blocked clauses
c [cce-4] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-4-1] eliminated 6 clauses out of 774 (1%) of length 18
c [cce-4-1] eliminated 22 clauses out of 797 (3%) of length 17
c [cce-4-1] eliminated 2 clauses out of 118 (2%) of length 13
c [cce-4-1] eliminated 12 clauses out of 193 (6%) of length 12
c [cce-4-1] eliminated 16 clauses out of 2179 (1%) of length 11
c [cce-4-1] incomplete large round (ACCE)
c [cce-4-1] eliminated 58 large clauses in 30000001 steps
c [cce-4-1] allowing another 15000000 steps for small clauses
c [cce-4] scheduling 95310 clauses = 87336 binary + 7974 ternary
c [cce-4] tried to eliminate 2547 small clauses 3%
c [cce-4] eliminated 250 small clauses 0%
c [cce-4] eliminated 238 binary clauses 0%
c [cce-4] eliminated 12 ternary clauses 0%
c [cce-4-1] eliminated 250 small clauses in 30000001 steps
c [cce-4-1] incomplete small round (ACCE)
c [cce-4-1] eliminated 308 covered clauses in round 1
c [cce-4] eliminated 308 covered clauses in TOTAL during 1 rounds
c [elim-5] 560 variables 3% will be scheduled this time
c [elim-5] scheduled 560 variables 3%
c [elim-5] limit of 21857450 steps penalty 0 = 0 + 0
c [elim-5-1] eliminated 39 variables 0% in round 1 in 11017381 steps
c [elim-5-1] backward subsumption/strengthening limit 10840069
c [elim-5-1] subsumed 72 and strengthened 24 clauses in 7640069 steps
c [elim-5-1] rescheduled 284 variables 2% by backward subsumption
c [elim-5-2] eliminated 65 variables 0% in round 2 in 1854677 steps
c [elim-5-2] backward subsumption/strengthening limit 1345323
c [elim-5-2] subsumed 0 and strengthened 0 clauses in 1345340 steps
c [elim-5] fully completed in 2 rounds
c [elim-5] transition to [ all 0 rem 0 ] state
c [elim-5] eliminated 105 = 1% variables out of 17747
c [bca-4] limit of 10000000 steps
c [bca-4] 23548 out of 35286 literals actually usable 67%
c [bca-4] added 60 blocked clauses in 80117 steps
c [rephase-1] after 34223 conflicts (new increment 20000, next 54223)
c [flushphases] 409 phases reset
c [phase-6] phase bias: 0 positive 0%, 0 negative 0%
c [simplification-5] removed 437 variables 2.4% (17642 remain 28%)
c [simplification-5] removed 4821 irredundant clauses 3.3% (141040 remain 46%)
c [simplification-5] maximum reduction of 3% = max (2%, 3%)
c [simplification-5] geometric conflict interval increment 6250 = 25000 / 4
c [simplification-5] new conflict interval 31250
c [simplification-5] penalized conflict interval 31250 = 1 * 31250
c [simplification-5] new conflict limit 65473
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i   26.6   17641   141040     34836   11847   8937 20728   7  6.2  55.2   13
c i   27.3   17636   141040     40227   16713   9123 20794   5  6.5  55.3   13
c i   27.3   17630   141040     40232   16716   9123 20795   5  6.5  55.3   13
c i   27.3   17629   141040     40235   16716   9123 20796   5  6.5  55.3   13
c -   27.4   17629   141040     40447   12389   9137 20802   5  6.5  55.2   12
c i   28.4   17628   141040     47035   18222   9424 20918   7  6.6  53.9   13
c i   28.4   17625   141040     47545   18668   9448 20922   6  6.6  53.9   13
c -   28.6   17623   141040     48525   14559   9476 20936   9  6.6  54.0   12
c -   29.3   17623   141040     56144   16084   9597 20989   6  6.9  56.1   12
c R   29.5   17623   141040     57366   17200   9609 20998   8  6.9  56.2   13
c i   29.5   17622   141040     57637   17434   9625 21008   8  6.9  56.1   13
c i   30.7   17621   141040     64918   24041   9875 21099  11  6.9  55.2   13
c -   30.8   17621   141040     65033   18143   9881 21100   9  6.9  55.2   13
c 
c [simplification-6] limit of 66255 conflicts hit after 66256 conflicts
c [ternres-4] limit 4000000 with penalty 0 = 0 + 0
c [ternres-4] all 17621 free variables schedulable
c [ternres-4] 2082 ternary resolvents (54 bin, 2028 trn)
c [ternres-4] 1 variables remain 0% (17620 retained)
c [card-3] limit 500000 penalty 2 = 2 + 0
c [card-3] found 3148 at-most-one constraints of average size 3.1
c [card-3] found 67 at-most-two constraints of average size 4.0
c [card-3] using previous limit 500000 for elimination
c [card-3] 3215 out of 3215 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [gauss-4] limit 2000000 penalty 0 = 0 + 0
c [gauss-4] extracted 7545 xors of average arity 3.0
c [gauss-4] connected 22336 occurrences of 2747 variables (average 8.1)
c [gauss-4] limit 2000000 penalty 0 = 0 + 0
c [gauss-4] connected 4161 occurrences of 2747 variables (average 1.5)
c [gauss-4] fully completed
c [decomp-12] removed 139 variables
c [gauss-4] exported 0 unary, 5 binary and 22 ternary equations
c [simpleprobe-3] 4200 schedulable variables 24%
c [simpleprobe-3] limit 9412156 penalty 0 = 0 + 0
c [decomp-14] removed 359 variables
c [simpleprobe-3] 2336 variables remain 14% (14787 retained)
c [simpleprobe-3] removed 359 variables, found 9460 hbrs, 17 units
c [cgrclsr-4] limit 235303 penalty 0 = 0 + 0
c [cgrclsr-4] all 17123 free variables schedulable
c [cgrclsr-4] fully completed congruence closure
c [lift-4] limit 1411823 with penalty 0 = 0 + 0
c [lift-4] using 12237 probes 71%
c [lift-4] 3 units, 13 impls, 7 eqs in 1 rounds
c [lift-4] 16489 variables remain 96% (622 retained)
c [lift-4] removed 12 variables
c [cliff-4] limit of 10000000 steps penalty 0 = 0 + 0
c [cliff-4] failed 8, lifted 27
c [unhide-6] limit 470607 with penalty 0 = 0 + 0
c [unhide-6-6] 0 units, 1 failed, 4418 tauts, 0 hbrs, 19646 literals
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 379 transitive binary clauses
c [block-5] scheduling all variables this time
c [block-5] scheduled 17072 variables 100%
c [block-5] limit of 50000000 steps penalty 0 = 0 + 0
c [block-5] fully completed
c [block-5] transition to [ all 0 rem 0 ] state
c [block-5] eliminated 359 blocked clauses
c [cce-5] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-5-1] eliminated 2 clauses out of 769 (0%) of length 19
c [cce-5-1] eliminated 6 clauses out of 774 (1%) of length 18
c [cce-5-1] eliminated 18 clauses out of 767 (2%) of length 17
c [cce-5-1] eliminated 2 clauses out of 119 (2%) of length 13
c [cce-5-1] eliminated 2 clauses out of 1998 (0%) of length 11
c [cce-5-1] incomplete large round (ACCE)
c [cce-5-1] eliminated 30 large clauses in 30000001 steps
c [cce-5-1] allowing another 15000000 steps for small clauses
c [cce-5] scheduling 99883 clauses = 84553 binary + 15330 ternary
c [cce-5] tried to eliminate 2749 small clauses 3%
c [cce-5] eliminated 247 small clauses 0%
c [cce-5] eliminated 196 binary clauses 0%
c [cce-5] eliminated 51 ternary clauses 0%
c [cce-5-1] eliminated 247 small clauses in 30000001 steps
c [cce-5-1] incomplete small round (ACCE)
c [cce-5-1] eliminated 277 covered clauses in round 1
c [cce-5] eliminated 277 covered clauses in TOTAL during 1 rounds
c [elim-6] scheduling all variables this time
c [elim-6] scheduled 17057 variables 100%
c [elim-6] limit of 47060781 steps penalty 0 = 0 + 0
c [elim-6-1] eliminated 286 variables 2% in round 1 in 28968765 steps
c [elim-6-1] backward subsumption/strengthening limit 18092016
c [elim-6-1] subsumed 0 and strengthened 0 clauses in 7523298 steps
c [elim-6] fully completed in 1 rounds
c [elim-6] transition to [ all 0 rem 0 ] state
c [elim-6] eliminated 287 = 2% variables out of 17057
c [bca-5] limit of 10000000 steps
c [bca-5] 20227 out of 33542 literals actually usable 60%
c [bca-5] added 75 blocked clauses in 73786 steps
c [rephase-2] after 66256 conflicts (new increment 40000, next 106256)
c [flushphases] 317 phases reset
c [phase-7] phase bias: 0 positive 0%, 0 negative 0%
c [simplification-6] removed 851 variables 4.8% (16770 remain 27%)
c [simplification-6] removed 4470 irredundant clauses 3.2% (136570 remain 44%)
c [simplification-6] maximum reduction of 5% = max (5%, 3%)
c [simplification-6] large reduction 5% >= 5% limit
c [simplification-6] new conflict interval 2000 = 2000/1
c [simplification-6] penalized conflict interval 2000 = 1 * 2000
c [simplification-6] new conflict limit 68256
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i   34.7   16769   136570     66965   17879  10581 24655   5  6.9  54.9   14
c 
c [simplification-7] limit of 68284 conflicts hit after 68286 conflicts
c [ternres-5] limit 4000000 with penalty 0 = 0 + 0
c [ternres-5] 1 schedulable variables 0%
c [ternres-5] 737 ternary resolvents (15 bin, 722 trn)
c [ternres-5] fully completed ternary resolution
c [gauss-5] limit 2000000 penalty 0 = 0 + 0
c [gauss-5] extracted 6491 xors of average arity 3.0
c [gauss-5] connected 19439 occurrences of 2451 variables (average 7.9)
c [gauss-5] limit 2000000 penalty 0 = 0 + 0
c [gauss-5] fully completed
c [gauss-5] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-15] removed 18 variables
c [lift-5] limit 1460614 with penalty 0 = 0 + 0
c [lift-5] using 11712 probes 70%
c [lift-5] 4 units, 20 impls, 5 eqs in 1 rounds
c [lift-5] 15845 variables remain 95% (897 retained)
c [lift-5] removed 9 variables
c [cliff-5] limit of 10000000 steps penalty 0 = 0 + 0
c [cliff-5] failed 2, lifted 10
c [unhide-7] limit 486871 with penalty 0 = 0 + 0
c [unhide-7-7] 0 units, 1 failed, 285 tauts, 0 hbrs, 8038 literals
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 341 transitive binary clauses
c [block-6] scheduling all variables this time
c [block-6] scheduled 16729 variables 100%
c [block-6] limit of 50000000 steps penalty 0 = 0 + 0
c [block-6] fully completed
c [block-6] transition to [ all 0 rem 0 ] state
c [block-6] eliminated 20 blocked clauses
c [block-6] 20 < 1/1000 * 136058 = 136 considered unsuccessful
c [cce-6] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-6-1] eliminated 1 clauses out of 3 (33%) of length 21
c [cce-6-1] eliminated 14 clauses out of 779 (2%) of length 19
c [cce-6-1] eliminated 100 clauses out of 863 (12%) of length 18
c [cce-6-1] eliminated 16 clauses out of 762 (2%) of length 17
c [cce-6-1] eliminated 1 clauses out of 13 (8%) of length 14
c [cce-6-1] eliminated 1 clauses out of 118 (1%) of length 13
c [cce-6-1] eliminated 1 clauses out of 181 (1%) of length 12
c [cce-6-1] incomplete large round (ACCE)
c [cce-6-1] eliminated 134 large clauses in 30000001 steps
c [cce-6-1] allowing another 15000000 steps for small clauses
c [cce-6] scheduling 97851 clauses = 82816 binary + 15035 ternary
c [cce-6] tried to eliminate 2942 small clauses 3%
c [cce-6] eliminated 317 small clauses 0%
c [cce-6] eliminated 252 binary clauses 0%
c [cce-6] eliminated 65 ternary clauses 0%
c [cce-6-1] eliminated 317 small clauses in 30000001 steps
c [cce-6-1] incomplete small round (ACCE)
c [cce-6-1] eliminated 451 covered clauses in round 1
c [cce-6] eliminated 451 covered clauses in TOTAL during 1 rounds
c [elim-7] scheduling all variables this time
c [elim-7] scheduled 16729 variables 100%
c [elim-7] limit of 48687140 steps penalty 0 = 0 + 0
c [elim-7-1] eliminated 46 variables 0% in round 1 in 26315532 steps
c [elim-7-1] backward subsumption/strengthening limit 22371608
c [elim-7-1] subsumed 0 and strengthened 0 clauses in 7403907 steps
c [elim-7] fully completed in 1 rounds
c [elim-7] transition to [ all 0 rem 0 ] state
c [elim-7] eliminated 46 = 0% variables out of 16729
c [bca-6] limit of 10000000 steps
c [bca-6] 19867 out of 33368 literals actually usable 60%
c [bca-6] added 27 blocked clauses in 73682 steps
c [phase-8] phase bias: 0 positive 0%, 0 negative 0%
c [simplification-7] removed 86 variables 0.5% (16683 remain 26%)
c [simplification-7] removed 1135 irredundant clauses 0.8% (135435 remain 44%)
c [simplification-7] maximum reduction of 1% = max (1%, 1%)
c [simplification-7] geometric conflict interval increment 15625 = 31250 / 2
c [simplification-7] new conflict interval 46875
c [simplification-7] penalized conflict interval 46875 = 1 * 46875
c [simplification-7] new conflict limit 115161
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -   39.3   16683   135435     76425   19507  11483 25216   8  7.1  53.9   13
c -   40.7   16683   135435     85917   21236  11690 25271   9  7.5  54.1   13
c -   42.5   16683   135435     96388   23340  11942 25353   9  7.6  53.4   13
c i   42.6   16682   135435     96600   23533  11949 25355   8  7.6  53.3   13
c -   44.5   16682   135435    107448   25576  12198 25429   8  7.7  53.0   13
c 
c [simplification-8] limit of 115635 conflicts hit after 115635 conflicts
c [ternres-6] limit 4768755 with penalty 0 = 0 + 0
c [ternres-6] all 16682 free variables schedulable
c [ternres-6] 2587 ternary resolvents (103 bin, 2484 trn)
c [ternres-6] 20 variables remain 0% (16662 retained)
c [decomp-16] removed 59 variables
c [cgrclsr-5] limit 238437 penalty 1 = 1 + 0
c [cgrclsr-5] all 16624 free variables schedulable
c [cgrclsr-5] fully completed congruence closure
c [lift-6] limit 2861253 with penalty 0 = 0 + 0
c [lift-6] using 11437 probes 69%
c [lift-6] 7 units, 28 impls, 14 eqs in 1 rounds
c [lift-6] 15216 variables remain 92% (1387 retained)
c [lift-6] removed 21 variables
c [cliff-6] limit of 10000000 steps penalty 0 = 0 + 0
c [cliff-6] failed 9, lifted 63
c [unhide-8] limit 953751 with penalty 0 = 0 + 0
c [unhide-8-8] 0 units, 0 failed, 2169 tauts, 0 hbrs, 59082 literals
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 270 transitive binary clauses
c [cce-7] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 21
c [cce-7-1] eliminated 1 clauses out of 740 (0%) of length 19
c [cce-7-1] eliminated 7 clauses out of 761 (1%) of length 18
c [cce-7-1] eliminated 15 clauses out of 770 (2%) of length 17
c [cce-7-1] eliminated 2 clauses out of 175 (1%) of length 12
c [cce-7-1] eliminated 3 clauses out of 1929 (0%) of length 11
c [cce-7-1] incomplete large round (ACCE)
c [cce-7-1] eliminated 29 large clauses in 30000001 steps
c [cce-7-1] allowing another 15000000 steps for small clauses
c [cce-7] scheduling 89086 clauses = 81406 binary + 7680 ternary
c [cce-7] tried to eliminate 2623 small clauses 3%
c [cce-7] eliminated 278 small clauses 0%
c [cce-7] eliminated 252 binary clauses 0%
c [cce-7] eliminated 26 ternary clauses 0%
c [cce-7-1] eliminated 278 small clauses in 30000001 steps
c [cce-7-1] incomplete small round (ACCE)
c [cce-7-1] eliminated 307 covered clauses in round 1
c [cce-7] eliminated 307 covered clauses in TOTAL during 1 rounds
c [elim-8] scheduling all variables this time
c [elim-8] scheduled 16528 variables 100%
c [elim-8] limit of 95375108 steps penalty 0 = 0 + 0
c [elim-8-1] eliminated 123 variables 1% in round 1 in 26589310 steps
c [elim-8-1] backward subsumption/strengthening limit 53178620
c [elim-8-1] subsumed 0 and strengthened 0 clauses in 7255448 steps
c [elim-8] fully completed in 1 rounds
c [elim-8] transition to [ all 0 rem 0 ] state
c [elim-8] eliminated 123 = 1% variables out of 16528
c [bca-7] limit of 10000000 steps
c [bca-7] 16120 out of 32812 literals actually usable 49%
c [bca-7] added 100 blocked clauses in 74922 steps
c [rephase-3] after 115635 conflicts (new increment 80000, next 195635)
c [flushphases] 186 phases reset
c [phase-9] phase bias: 0 positive 0%, 0 negative 0%
c [simplification-8] removed 277 variables 1.7% (16405 remain 26%)
c [simplification-8] removed 2432 irredundant clauses 1.8% (133003 remain 43%)
c [simplification-8] maximum reduction of 2% = max (2%, 2%)
c [simplification-8] geometric conflict interval increment 15625 = 46875 / 3
c [simplification-8] new conflict interval 62500
c [simplification-8] penalized conflict interval 62500 = 1 * 62500
c [simplification-8] new conflict limit 178135
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -   49.4   16405   133003    118888   26254  13521 24681  10  8.2  53.8   14
c R   50.7   16405   133003    125161   31670  13553 24684  12  8.8  54.0   19
c -   51.9   16405   133003    130655   27678  13692 24724   7  8.9  53.7   14
c -   54.5   16405   133003    143438   29984  13966 24828   7  8.9  53.6   14
c i   55.1   16404   133003    146196   32549  14021 24853   8  8.9  53.3   15
c -   57.2   16404   133003    156598   32067  14200 24920   6  9.1  53.5   14
c i   58.8   16403   133003    164236   39074  14369 24972   5  9.1  53.1   16
c i   59.2   16400   133003    166041   40762  14396 24988   8  9.1  53.0   16
c i   59.6   16399   133003    167582   42212  14420 24993   6  9.1  52.8   16
c -   60.2   16399   133003    170340   34245  14468 25021   7  9.1  52.7   14
c i   60.3   16398   133003    170860   34737  14473 25024   8  9.1  52.7   15
c 
c [simplification-9] limit of 178805 conflicts hit after 178807 conflicts
c [ternres-7] limit 8671261 with penalty 0 = 0 + 0
c [ternres-7] 19 schedulable variables 0%
c [ternres-7] 2792 ternary resolvents (33 bin, 2759 trn)
c [ternres-7] fully completed ternary resolution
c [gauss-6] limit 1000000 penalty 1 = 1 + 0
c [gauss-6] extracted 2777 xors of average arity 3.0
c [gauss-6] connected 8264 occurrences of 1615 variables (average 5.1)
c [gauss-6] limit 1000000 penalty 1 = 1 + 0
c [gauss-6] fully completed
c [decomp-17] removed 63 variables
c [gauss-6] exported 0 unary, 1 binary and 2 ternary equations
c [treelook-3] limit 108390 penalty 2 = 2 + 0 boost 1
c [treelook-3] scheduled 11113 literals 34%
c [treelook-3] scheduling used 108550 steps
c [treelook-3] not fully scheduled
c [treelook-3] limit 108390 penalty 2 = 2 + 0 boost 1
c [treelook-3] used 125637 steps
c [treelook-3] 11092 literals remain 34%
c [treelook-3] 9595 variables remain to probed next time 59%
c [treelook-3] removed 0 variables, found 27 hbrs
c [lift-7] limit 5202756 with penalty 0 = 0 + 0
c [lift-7] using 10827 probes 66%
c [lift-7] 13 units, 64 impls, 24 eqs in 1 rounds
c [lift-7] 14092 variables remain 86% (2206 retained)
c [lift-7] removed 37 variables
c [cliff-7] limit of 10000000 steps penalty 0 = 0 + 0
c [cliff-7] failed 9, lifted 17
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 370 transitive binary clauses
c [block-7] scheduling all variables this time
c [block-7] scheduled 16270 variables 100%
c [block-7] limit of 43356305 steps penalty 1 = 1 + 0
c [block-7] fully completed
c [block-7] transition to [ all 0 rem 0 ] state
c [block-7] eliminated 27 blocked clauses
c [block-7] 27 < 1/1000 * 132646 = 132 considered unsuccessful
c [cce-8] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-8-1] eliminated 1 clauses out of 731 (0%) of length 19
c [cce-8-1] eliminated 68 clauses out of 813 (8%) of length 18
c [cce-8-1] eliminated 8 clauses out of 764 (1%) of length 17
c [cce-8-1] eliminated 2 clauses out of 118 (2%) of length 13
c [cce-8-1] eliminated 2 clauses out of 175 (1%) of length 12
c [cce-8-1] eliminated 1 clauses out of 1903 (0%) of length 11
c [cce-8-1] incomplete large round (ACCE)
c [cce-8-1] eliminated 82 large clauses in 30000001 steps
c [cce-8-1] allowing another 15000000 steps for small clauses
c [cce-8] scheduling 87580 clauses = 80033 binary + 7547 ternary
c [cce-8] tried to eliminate 2670 small clauses 3%
c [cce-8] eliminated 349 small clauses 0%
c [cce-8] eliminated 320 binary clauses 0%
c [cce-8] eliminated 29 ternary clauses 0%
c [cce-8-1] eliminated 349 small clauses in 30000001 steps
c [cce-8-1] incomplete small round (ACCE)
c [cce-8-1] eliminated 431 covered clauses in round 1
c [cce-8] eliminated 431 covered clauses in TOTAL during 1 rounds
c [elim-9] scheduling all variables this time
c [elim-9] scheduled 16270 variables 100%
c [elim-9] limit of 173425221 steps penalty 0 = 0 + 0
c [elim-9-1] eliminated 77 variables 0% in round 1 in 26382006 steps
c [elim-9-1] backward subsumption/strengthening limit 52764012
c [elim-9-1] subsumed 0 and strengthened 0 clauses in 7170251 steps
c [elim-9] fully completed in 1 rounds
c [elim-9] transition to [ all 0 rem 0 ] state
c [elim-9] eliminated 77 = 0% variables out of 16270
c [bca-8] limit of 10000000 steps
c [bca-8] 14012 out of 32388 literals actually usable 43%
c [bca-8] added 65 blocked clauses in 77994 steps
c [phase-10] phase bias: 0 positive 0%, 0 negative 0%
c [simplification-9] removed 205 variables 1.3% (16193 remain 26%)
c [simplification-9] removed 1734 irredundant clauses 1.3% (131269 remain 42%)
c [simplification-9] maximum reduction of 1% = max (1%, 1%)
c [simplification-9] geometric conflict interval increment 31250 = 62500 / 2
c [simplification-9] new conflict interval 93750
c [simplification-9] penalized conflict interval 93750 = 1 * 93750
c [simplification-9] new conflict limit 272557
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -   66.2   16193   131269    184945   35629  16430 27566   8  9.5  53.0   16
c -   69.6   16193   131269    199265   37546  16694 27645   6  9.5  52.6   15
c i   70.7   16192   131269    204084   42058  16779 27677   7  9.5  52.3   16
c i   71.2   16191   131269    206725   44501  16818 27692   5  9.5  52.4   17
c i   72.3   16190   131269    211881   49294  16884 27723   6  9.5  52.3   18
c -   73.0   16190   131269    214519   39699  16938 27743   8  9.5  52.3   15
c i   73.6   16189   131269    216951   42003  16973 27760   8  9.5  52.2   16
c i   73.6   16186   131269    216961   42010  16974 27760   8  9.5  52.2   16
c i   73.7   16183   131269    217314   42339  16984 27764   5  9.5  52.2   16
c i   74.0   16178   131269    218311   43286  16997 27769   7  9.5  52.1   16
c i   76.6   16176   131269    228825   53195  17162 27826   9  9.5  51.9   19
c -   77.0   16176   131269    230006   41817  17177 27833   8  9.5  51.8   16
c -   79.8   16176   131269    246206   43738  17338 27877  12  9.7  52.4   16
c -   84.0   16176   131269    265148   45147  17440 27907   6 10.6  52.6   16
c R   85.4   16176   131269    271070   50020  17467 27918  11 10.9  52.6   18
c i   85.8   16175   131269    272461   51312  17485 27936   7 10.9  52.6   18
c 
c [simplification-10] limit of 273391 conflicts hit after 273395 conflicts
c [ternres-8] limit 15485095 with penalty 0 = 0 + 0
c [ternres-8] all 16175 free variables schedulable
c [ternres-8] 3092 ternary resolvents (58 bin, 3034 trn)
c [ternres-8] fully completed ternary resolution
c [card-4] limit 967818 penalty 3 = 3 + 0
c [card-4] found 3307 at-most-one constraints of average size 3.2
c [card-4] found 109 at-most-two constraints of average size 4.0
c [card-4] using previous limit 967818 for elimination
c [card-4] 3416 out of 3416 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [gauss-7] limit 3097019 penalty 0 = 0 + 0
c [gauss-7] extracted 7653 xors of average arity 3.0
c [gauss-7] connected 22704 occurrences of 2473 variables (average 9.2)
c [gauss-7] limit 3097019 penalty 0 = 0 + 0
c [gauss-7] connected 4067 occurrences of 2473 variables (average 1.6)
c [gauss-7] fully completed
c [gauss-7] exported 0 unary, 0 binary and 10 ternary equations
c [decomp-20] removed 92 variables
c [basicprobe-3] limit 15485095 penalty 0 = 0 + 0
c [basicprobe-3-0] 3474 probes remain 22% after last round
c [basicprobe-3-0] 63 units = 59 failed (94%) + 4 lifted (6%)
c [basicprobe-3-0] removed 75 variables, found 9010 hbrs
c [bate-2] eliminated 40 asymmetric tautologies during probing
c [lift-8] limit 9291057 with penalty 0 = 0 + 0
c [lift-8] using 9863 probes 62%
c [lift-8] 25 units, 96 impls, 47 eqs in 1 rounds
c [lift-8] 12400 variables remain 78% (3529 retained)
c [lift-8] removed 79 variables
c [cliff-8] limit of 12388076 steps penalty 0 = 0 + 0
c [cliff-8] failed 5, lifted 20
c [unhide-9] limit 1548509 with penalty 1 = 1 + 0
c [unhide-9-10] 0 units, 0 failed, 4125 tauts, 0 hbrs, 62023 literals
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 295 transitive binary clauses
c [cce-9] limit of 30970191 steps penalty 0 = 0 + 0
c [cce-9-1] eliminated 3 clauses out of 697 (0%) of length 19
c [cce-9-1] eliminated 27 clauses out of 757 (4%) of length 18
c [cce-9-1] eliminated 39 clauses out of 788 (5%) of length 17
c [cce-9-1] eliminated 1 clauses out of 106 (1%) of length 13
c [cce-9-1] eliminated 2 clauses out of 175 (1%) of length 12
c [cce-9-1] eliminated 7 clauses out of 1778 (0%) of length 11
c [cce-9-1] incomplete large round (ACCE)
c [cce-9-1] eliminated 79 large clauses in 30970192 steps
c [cce-9-1] allowing another 15485096 steps for small clauses
c [cce-9] scheduling 85225 clauses = 77804 binary + 7421 ternary
c [cce-9] tried to eliminate 2934 small clauses 3%
c [cce-9] eliminated 432 small clauses 1%
c [cce-9] eliminated 400 binary clauses 1%
c [cce-9] eliminated 32 ternary clauses 0%
c [cce-9-1] eliminated 432 small clauses in 30970192 steps
c [cce-9-1] incomplete small round (ACCE)
c [cce-9-1] eliminated 511 covered clauses in round 1
c [cce-9] eliminated 511 covered clauses in TOTAL during 1 rounds
c [elim-10] scheduling all variables this time
c [elim-10] scheduled 15903 variables 100%
c [elim-10] limit of 309701913 steps penalty 0 = 0 + 0
c [elim-10-1] eliminated 198 variables 1% in round 1 in 26953175 steps
c [elim-10-1] backward subsumption/strengthening limit 53906350
c [elim-10-1] subsumed 0 and strengthened 0 clauses in 6979698 steps
c [elim-10] fully completed in 1 rounds
c [elim-10] transition to [ all 0 rem 0 ] state
c [elim-10] eliminated 198 = 1% variables out of 15903
c [bca-9] limit of 10000000 steps
c [bca-9] 12192 out of 31412 literals actually usable 39%
c [bca-9] added 62 blocked clauses in 80342 steps
c [rephase-4] after 273395 conflicts (new increment 160000, next 433395)
c [flushphases] 17 phases reset
c [phase-11] phase bias: 0 positive 0%, 0 negative 0%
c [simplification-10] removed 470 variables 2.9% (15705 remain 25%)
c [simplification-10] removed 4039 irredundant clauses 3.1% (127230 remain 41%)
c [simplification-10] maximum reduction of 3% = max (3%, 3%)
c [simplification-10] geometric conflict interval increment 23437 = 93750 / 4
c [simplification-10] new conflict interval 117187
c [simplification-10] penalized conflict interval 117187 = 1 * 117187
c [simplification-10] new conflict limit 390582
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -   93.7   15705   127230    284477   44632  18251 34439   6 10.9  52.2   16
c i   95.7   15704   127230    291753   51445  18362 34474   7 10.9  51.9   18
c i   97.3   15702   127230    299104   58250  18429 34490   8 11.0  52.0   21
c -   98.2   15702   127230    302385   46868  18488 34496  11 11.0  51.9   16
c -  103.2   15702   127230    320244   48779  18704 34551   9 10.9  51.5   17
c -  108.0   15702   127230    338922   50574  18867 34591   5 11.0  51.1   17
c i  109.2   15701   127230    343315   54751  18913 34601   7 11.0  51.1   19
c i  113.3   15699   127230    357575   67927  19030 34630   8 11.1  50.8   22
c -  113.6   15699   127230    358263   52546  19041 34638   6 11.1  50.8   17
c i  115.9   15698   127230    366457   60324  19128 34659   6 11.1  50.8   20
c -  119.6   15698   127230    377942   54763  19232 34679   7 11.0  50.5   17
c 
c [simplification-11] limit of 391108 conflicts hit after 391109 conflicts
c [ternres-9] limit 25502515 with penalty 0 = 0 + 0
c [ternres-9] all 15698 free variables schedulable
c [ternres-9] 5746 ternary resolvents (121 bin, 5625 trn)
c [ternres-9] fully completed ternary resolution
c [gauss-8] limit 5100503 penalty 0 = 0 + 0
c [gauss-8] extracted 10476 xors of average arity 3.0
c [gauss-8] connected 31015 occurrences of 2463 variables (average 12.6)
c [gauss-8] limit 5100503 penalty 0 = 0 + 0
c [gauss-8] connected 8069 occurrences of 2463 variables (average 3.3)
c [gauss-8] fully completed
c [gauss-8] exported 0 unary, 0 binary and 2 ternary equations
c [decomp-21] removed 115 variables
c [simpleprobe-4] 2027 schedulable variables 13%
c [simpleprobe-4] limit 102010062 penalty 0 = 0 + 0
c [decomp-22] removed 119 variables
c [simpleprobe-4] fully completed simple probing
c [simpleprobe-4] removed 119 variables, found 15420 hbrs, 8 units
c [cgrclsr-6] limit 637562 penalty 2 = 2 + 0
c [cgrclsr-6] all 15464 free variables schedulable
c [cgrclsr-6] 3629 variables remain 23% (11834 retained)
c [cgrclsr-6] removed 1 variables
c [lift-9] limit 15301509 with penalty 0 = 0 + 0
c [lift-9] using 8447 probes 55%
c [lift-9] 22 units, 152 impls, 54 eqs in 1 rounds
c [lift-9] 10084 variables remain 66% (5299 retained)
c [lift-9] removed 80 variables
c [cliff-9] limit of 20402012 steps penalty 0 = 0 + 0
c [cliff-9] failed 6, lifted 14
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 822 transitive binary clauses
c [cce-10] limit of 51005031 steps penalty 0 = 0 + 0
c [cce-10-1] eliminated 2 clauses out of 681 (0%) of length 19
c [cce-10-1] eliminated 96 clauses out of 816 (12%) of length 18
c [cce-10-1] eliminated 41 clauses out of 758 (5%) of length 17
c [cce-10-1] eliminated 4 clauses out of 111 (4%) of length 13
c [cce-10-1] eliminated 2 clauses out of 175 (1%) of length 12
c [cce-10-1] eliminated 15 clauses out of 1714 (1%) of length 11
c [cce-10-1] eliminated 37 clauses out of 557 (7%) of length 10
c [cce-10-1] eliminated 148 clauses out of 859 (17%) of length 9
c [cce-10-1] eliminated 21 clauses out of 2154 (1%) of length 8
c [cce-10-1] incomplete large round (ACCE)
c [cce-10-1] eliminated 366 large clauses in 51005032 steps
c [cce-10-1] allowing another 25502516 steps for small clauses
c [cce-10] scheduling 82595 clauses = 75230 binary + 7365 ternary
c [cce-10] tried to eliminate 4155 small clauses 5%
c [cce-10] eliminated 517 small clauses 1%
c [cce-10] eliminated 475 binary clauses 1%
c [cce-10] eliminated 42 ternary clauses 1%
c [cce-10-1] eliminated 846 small clauses in 51005032 steps
c [cce-10-1] incomplete small round (ACCE)
c [cce-10-1] eliminated 1212 covered clauses in round 1
c [cce-10] eliminated 1212 covered clauses in TOTAL during 1 rounds
c [elim-11] scheduling all variables this time
c [elim-11] scheduled 15363 variables 100%
c [elim-11] limit of 510050312 steps penalty 0 = 0 + 0
c [elim-11-1] eliminated 149 variables 1% in round 1 in 28160491 steps
c [elim-11-1] backward subsumption/strengthening limit 56320982
c [elim-11-1] subsumed 0 and strengthened 0 clauses in 6842024 steps
c [elim-11] fully completed in 1 rounds
c [elim-11] transition to [ all 0 rem 0 ] state
c [elim-11] eliminated 149 = 1% variables out of 15363
c [bca-10] limit of 10000000 steps
c [bca-10] 10474 out of 30430 literals actually usable 34%
c [bca-10] added 55 blocked clauses in 90014 steps
c [simplification-11] removed 484 variables 3.1% (15214 remain 24%)
c [simplification-11] removed 3734 irredundant clauses 2.9% (123496 remain 40%)
c [simplification-11] maximum reduction of 3% = max (3%, 3%)
c [simplification-11] geometric conflict interval increment 29296 = 117187 / 4
c [simplification-11] new conflict interval 146483
c [simplification-11] penalized conflict interval 146483 = 1 * 146483
c [simplification-11] new conflict limit 537592
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  130.6   15214   123496    401404   55209  23411 51142   9 11.3  50.4   19
c i  131.7   15213   123496    404935   58595  23447 51151   9 11.3  50.3   20
c i  134.9   15212   123496    415267   68248  23544 51174   8 11.2  50.1   22
c -  136.8   15212   123496    422353   57361  23589 51184   8 11.3  50.1   18
c -  144.1   15212   123496    443598   59464  23787 51211   6 11.3  49.7   18
c -  150.6   15212   123496    465871   61664  23946 51241  11 11.3  49.4   19
c i  150.7   15211   123496    466406   62178  23950 51243   7 11.3  49.4   20
c i  153.1   15209   123496    473135   68557  24007 51258   9 11.3  49.3   21
c -  158.0   15209   123496    488083   63448  24136 51280   5 11.4  49.1   19
c -  165.2   15209   123496    512424   65663  24294 51319  15 11.7  49.1   19
c -  170.4   15209   123496    536206   66549  24353 51329  14 12.1  49.3   19
c 
c [simplification-12] limit of 538014 conflicts hit after 538015 conflicts
c [ternres-10] limit 40413567 with penalty 0 = 0 + 0
c [ternres-10] all 15209 free variables schedulable
c [ternres-10] 3479 ternary resolvents (61 bin, 3418 trn)
c [ternres-10] fully completed ternary resolution
c [gauss-9] limit 8082713 penalty 0 = 0 + 0
c [gauss-9] extracted 11738 xors of average arity 3.0
c [gauss-9] connected 34932 occurrences of 2338 variables (average 14.9)
c [gauss-9] limit 8082713 penalty 0 = 0 + 0
c [gauss-9] connected 9971 occurrences of 2338 variables (average 4.3)
c [gauss-9] fully completed
c [gauss-9] exported 0 unary, 0 binary and 2 ternary equations
c [decomp-23] removed 67 variables
c [lift-10] limit 20000000 with penalty 0 = 0 + 0
c [lift-10] using 6428 probes 42%
c [lift-10] 24 units, 169 impls, 61 eqs in 1 rounds
c [lift-10] 7613 variables remain 51% (7440 retained)
c [lift-10] removed 89 variables
c [cliff-10] limit of 32330853 steps penalty 0 = 0 + 0
c [cliff-10] failed 6, lifted 6
c [transred-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 935 transitive binary clauses
c [block-8] scheduling all variables this time
c [block-8] scheduled 15041 variables 100%
c [block-8] limit of 101033917 steps penalty 2 = 2 + 0
c [block-8] fully completed
c [block-8] transition to [ all 0 rem 0 ] state
c [block-8] eliminated 46 blocked clauses
c [block-8] 46 < 1/1000 * 122874 = 122 considered unsuccessful
c [cce-11] limit of 80827134 steps penalty 0 = 0 + 0
c [cce-11-1] eliminated 1 clauses out of 669 (0%) of length 19
c [cce-11-1] eliminated 100 clauses out of 814 (12%) of length 18
c [cce-11-1] eliminated 28 clauses out of 723 (4%) of length 17
c [cce-11-1] eliminated 2 clauses out of 183 (1%) of length 12
c [cce-11-1] eliminated 2 clauses out of 1656 (0%) of length 11
c [cce-11-1] eliminated 7 clauses out of 547 (1%) of length 10
c [cce-11-1] eliminated 10 clauses out of 706 (1%) of length 9
c [cce-11-1] eliminated 91 clauses out of 2130 (4%) of length 8
c [cce-11-1] eliminated 127 clauses out of 1926 (7%) of length 7
c [cce-11-1] eliminated 56 clauses out of 4141 (1%) of length 6
c [cce-11-1] incomplete large round (ACCE)
c [cce-11-1] eliminated 424 large clauses in 80827135 steps
c [cce-11-1] allowing another 40413567 steps for small clauses
c [cce-11] scheduling 80527 clauses = 73451 binary + 7076 ternary
c [cce-11] tried to eliminate 7365 small clauses 9%
c [cce-11] eliminated 1030 small clauses 1%
c [cce-11] eliminated 937 binary clauses 1%
c [cce-11] eliminated 93 ternary clauses 1%
c [cce-11-1] eliminated 1030 small clauses in 80827135 steps
c [cce-11-1] incomplete small round (ACCE)
c [cce-11-1] eliminated 1454 covered clauses in round 1
c [cce-11] eliminated 1454 covered clauses in TOTAL during 1 rounds
c [elim-12] scheduling all variables this time
c [elim-12] scheduled 15040 variables 100%
c [elim-12] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-12-1] eliminated 123 variables 1% in round 1 in 26318302 steps
c [elim-12-1] backward subsumption/strengthening limit 52636604
c [elim-12-1] subsumed 0 and strengthened 0 clauses in 6689694 steps
c [elim-12] fully completed in 1 rounds
c [elim-12] transition to [ all 0 rem 0 ] state
c [elim-12] eliminated 123 = 1% variables out of 15040
c [bca-11] limit of 10000000 steps
c [bca-11] 9421 out of 29836 literals actually usable 32%
c [bca-11] added 44 blocked clauses in 91078 steps
c [rephase-5] after 538015 conflicts (new increment 320000, next 858015)
c [flushphases] 0 phases reset
c [simplification-12] removed 292 variables 1.9% (14917 remain 24%)
c [simplification-12] removed 2870 irredundant clauses 2.3% (120626 remain 39%)
c [simplification-12] maximum reduction of 2% = max (2%, 2%)
c [simplification-12] geometric conflict interval increment 48827 = 146483 / 3
c [simplification-12] new conflict interval 195310
c [simplification-12] penalized conflict interval 195310 = 1 * 195310
c [simplification-12] new conflict limit 733325
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  186.4   14917   120626    570476   67024  26569 53467  11 14.0  50.3   20
c R  190.6   14917   120626    583776   76339  26614 53469   9 14.7  50.8   25
c i  190.8   14916   120626    584430   76949  26622 53473   7 14.7  50.8   25
c -  196.0   14916   120626    598050   68919  26720 53498  13 14.6  50.5   20
c -  205.0   14916   120626    623516   70975  26899 53536   7 14.5  50.2   21
c -  213.6   14916   120626    649396   72932  27053 53560   7 14.5  49.9   21
c i  215.8   14915   120626    655977   79047  27087 53564   8 14.5  49.8   24
c -  223.2   14915   120626    675745   74799  27209 53581   7 14.4  49.5   21
c i  224.5   14914   120626    679882   78524  27228 53585   8 14.5  49.5   23
c -  231.7   14914   120626    702797   76666  27350 53597   8 14.5  49.3   20
c i  241.4   14913   120626    729307  101356  27492 53618   6 14.4  49.1   30
c -  241.8   14913   120626    730187   78670  27502 53619   7 14.4  49.1   22
c 
c [simplification-13] limit of 733689 conflicts hit after 733690 conflicts
c [ternres-11] limit 63387512 with penalty 0 = 0 + 0
c [ternres-11] all 14913 free variables schedulable
c [ternres-11] 1617 ternary resolvents (35 bin, 1582 trn)
c [ternres-11] fully completed ternary resolution
c [gauss-10] limit 12677502 penalty 0 = 0 + 0
c [gauss-10] extracted 11366 xors of average arity 3.0
c [gauss-10] connected 33880 occurrences of 2236 variables (average 15.2)
c [gauss-10] limit 12677502 penalty 0 = 0 + 0
c [gauss-10] connected 9424 occurrences of 2236 variables (average 4.2)
c [gauss-10] fully completed
c [gauss-10] exported 0 unary, 0 binary and 2 ternary equations
c [decomp-24] removed 49 variables
c [cgrclsr-7] limit 3169375 penalty 1 = 1 + 0
c [cgrclsr-7] 3481 schedulable variables 23%
c [cgrclsr-7] fully completed congruence closure
c [cgrclsr-7] removed 7 variables
c [lift-11] limit 20000000 with penalty 0 = 0 + 0
c [lift-11] using 4136 probes 28%
c [lift-11] 14 units, 193 impls, 52 eqs in 1 rounds
c [lift-11] 5262 variables remain 36% (9529 retained)
c [lift-11] removed 66 variables
c [cliff-11] limit of 50710010 steps penalty 0 = 0 + 0
c [cliff-11] failed 6, lifted 2
c [unhide-10] limit 3169375 with penalty 2 = 2 + 0
c [unhide-10-12] 1 units, 0 failed, 10726 tauts, 0 hbrs, 64573 literals
c [transred-11] limit 2000000 with penalty 0 = 0 + 0
c [transred-11] removed 673 transitive binary clauses
c [cce-12] limit of 126775025 steps penalty 0 = 0 + 0
c [cce-12-1] eliminated 1 clauses out of 619 (0%) of length 19
c [cce-12-1] eliminated 24 clauses out of 766 (3%) of length 18
c [cce-12-1] eliminated 35 clauses out of 714 (5%) of length 17
c [cce-12-1] eliminated 3 clauses out of 222 (1%) of length 12
c [cce-12-1] eliminated 8 clauses out of 1463 (1%) of length 11
c [cce-12-1] eliminated 9 clauses out of 635 (1%) of length 10
c [cce-12-1] eliminated 11 clauses out of 762 (1%) of length 9
c [cce-12-1] eliminated 10 clauses out of 2057 (0%) of length 8
c [cce-12-1] eliminated 27 clauses out of 1774 (2%) of length 7
c [cce-12-1] eliminated 228 clauses out of 4107 (6%) of length 6
c [cce-12-1] eliminated 216 clauses out of 5112 (4%) of length 5
c [cce-12-1] incomplete large round (ACCE)
c [cce-12-1] eliminated 572 large clauses in 126775026 steps
c [cce-12-1] allowing another 63387513 steps for small clauses
c [cce-12] scheduling 84231 clauses = 71198 binary + 13033 ternary
c [cce-12] tried to eliminate 11972 small clauses 14%
c [cce-12] eliminated 1550 small clauses 2%
c [cce-12] eliminated 1289 binary clauses 2%
c [cce-12] eliminated 261 ternary clauses 2%
c [cce-12-1] eliminated 1554 small clauses in 126775026 steps
c [cce-12-1] incomplete small round (ACCE)
c [cce-12-1] eliminated 2126 covered clauses in round 1
c [cce-12] eliminated 2126 covered clauses in TOTAL during 1 rounds
c [elim-13] scheduling all variables this time
c [elim-13] scheduled 14781 variables 100%
c [elim-13] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-13-1] eliminated 224 variables 2% in round 1 in 24744184 steps
c [elim-13-1] backward subsumption/strengthening limit 49488368
c [elim-13-1] subsumed 0 and strengthened 0 clauses in 6460460 steps
c [elim-13] fully completed in 1 rounds
c [elim-13] transition to [ all 0 rem 0 ] state
c [elim-13] eliminated 224 = 2% variables out of 14781
c [bca-12] limit of 10000000 steps
c [bca-12] 8097 out of 29116 literals actually usable 28%
c [bca-12] added 37 blocked clauses in 98162 steps
c [simplification-13] removed 356 variables 2.4% (14557 remain 23%)
c [simplification-13] removed 3903 irredundant clauses 3.2% (116723 remain 38%)
c [simplification-13] maximum reduction of 3% = max (2%, 3%)
c [simplification-13] geometric conflict interval increment 48827 = 195310 / 4
c [simplification-13] new conflict interval 244137
c [simplification-13] penalized conflict interval 244137 = 1 * 244137
c [simplification-13] new conflict limit 977827
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  261.8   14557   116723    759969   77594  27331 45826   9 14.4  48.8   22
c i  270.4   14556   116723    784614  100369  27434 45848  13 14.4  48.6   31
c -  272.1   14556   116723    788201   79251  27462 45849   8 14.4  48.5   21
c i  275.9   14555   116723    799542   89909  27520 45853   8 14.3  48.4   26
c i  279.6   14554   116723    808572   98155  27560 45859   7 14.3  48.3   30
c -  283.3   14554   116723    817256   81279  27606 45862   5 14.3  48.2   21
c -  291.4   14554   116723    848179   83102  27692 45884   9 14.5  48.2   22
c -  302.1   14554   116723    877939   84702  27820 45909   9 14.5  48.0   22
c i  303.7   14553   116723    883142   88657  27838 45912   8 14.6  48.0   25
c -  314.0   14549   116723    909593   86753  27972 45940  13 14.6  47.8   22
c i  319.2   14548   116723    923266   99000  28027 45957   6 14.6  47.6   27
c i  323.9   14547   116723    934418  109349  28090 45965  10 14.6  47.6   31
c -  326.7   14547   116723    941224   88521  28107 45967   8 14.6  47.5   22
c -  339.2   14547   116723    973420   90526  28240 45992  11 14.6  47.3   22
c 
c [simplification-14] limit of 978281 conflicts hit after 978283 conflicts
c [ternres-12] limit 92836560 with penalty 0 = 0 + 0
c [ternres-12] all 14547 free variables schedulable
c [ternres-12] 4203 ternary resolvents (60 bin, 4143 trn)
c [ternres-12] fully completed ternary resolution
c [gauss-11] limit 18567312 penalty 0 = 0 + 0
c [gauss-11] extracted 10833 xors of average arity 3.0
c [gauss-11] connected 32145 occurrences of 2172 variables (average 14.8)
c [gauss-11] limit 18567312 penalty 0 = 0 + 0
c [gauss-11] connected 8580 occurrences of 2172 variables (average 4.0)
c [gauss-11] fully completed
c [gauss-11] exported 0 unary, 0 binary and 3 ternary equations
c [decomp-25] removed 84 variables
c [cgrclsr-8] limit 8000000 penalty 0 = 0 + 0
c [cgrclsr-8] all 14463 free variables schedulable
c [cgrclsr-8] 5140 variables remain 36% (9274 retained)
c [cgrclsr-8] removed 49 variables
c [lift-12] limit 20000000 with penalty 0 = 0 + 0
c [lift-12] using 1927 probes 13%
c [lift-12-1] found 22 units 168 impls in round 1
c [lift-12] 22 units, 180 impls, 39 eqs in 2 rounds
c [lift-12] 3209 variables remain 22% (11144 retained)
c [lift-12] removed 61 variables
c [cliff-12] limit of 74269248 steps penalty 0 = 0 + 0
c [cliff-12] failed 5, lifted 4
c [transred-12] limit 2000000 with penalty 0 = 0 + 0
c [transred-12] removed 733 transitive binary clauses
c [cce-13] limit of 185673120 steps penalty 0 = 0 + 0
c [cce-13-1] eliminated 1 clauses out of 613 (0%) of length 19
c [cce-13-1] eliminated 19 clauses out of 755 (3%) of length 18
c [cce-13-1] eliminated 26 clauses out of 689 (4%) of length 17
c [cce-13-1] eliminated 4 clauses out of 233 (2%) of length 12
c [cce-13-1] eliminated 3 clauses out of 1432 (0%) of length 11
c [cce-13-1] eliminated 15 clauses out of 650 (2%) of length 10
c [cce-13-1] eliminated 30 clauses out of 830 (4%) of length 9
c [cce-13-1] eliminated 26 clauses out of 2051 (1%) of length 8
c [cce-13-1] eliminated 29 clauses out of 1768 (2%) of length 7
c [cce-13-1] eliminated 76 clauses out of 3942 (2%) of length 6
c [cce-13-1] eliminated 318 clauses out of 4916 (6%) of length 5
c [cce-13-1] eliminated 1126 clauses out of 9982 (11%) of length 4
c [cce-13-1] completed large round (ACCE)
c [cce-13-1] eliminated 1673 large clauses in 177271087 steps
c [cce-13-1] allowing another 88635543 steps for small clauses
c [cce-13] scheduling 75626 clauses = 68835 binary + 6791 ternary
c [cce-13] tried to eliminate 18694 small clauses 25%
c [cce-13] eliminated 2185 small clauses 3%
c [cce-13] eliminated 1992 binary clauses 3%
c [cce-13] eliminated 193 ternary clauses 3%
c [cce-13-1] eliminated 2311 small clauses in 185673121 steps
c [cce-13-1] incomplete small round (ACCE)
c [cce-13-1] eliminated 3984 covered clauses in round 1
c [cce-13] eliminated 3984 covered clauses in TOTAL during 1 rounds
c [elim-14] scheduling all variables this time
c [elim-14] scheduled 14344 variables 100%
c [elim-14] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-14-1] eliminated 348 variables 2% in round 1 in 26416373 steps
c [elim-14-1] backward subsumption/strengthening limit 52832746
c [elim-14-1] subsumed 0 and strengthened 0 clauses in 6109809 steps
c [elim-14] fully completed in 1 rounds
c [elim-14] transition to [ all 0 rem 0 ] state
c [elim-14] eliminated 348 = 2% variables out of 14344
c [bca-13] limit of 10000000 steps
c [bca-13] 7175 out of 27994 literals actually usable 26%
c [bca-13] added 34 blocked clauses in 107403 steps
c [rephase-6] after 978283 conflicts (new increment 640000, next 1618283)
c [flushphases] 0 phases reset
c [simplification-14] removed 551 variables 3.8% (13996 remain 22%)
c [simplification-14] removed 5830 irredundant clauses 5.0% (110893 remain 36%)
c [simplification-14] maximum reduction of 5% = max (4%, 5%)
c [simplification-14] large reduction 5% >= 5% limit
c [simplification-14] new conflict interval 9782 = min (978283/100, 244137)
c [simplification-14] penalized conflict interval 9782 = 1 * 9782
c [simplification-14] new conflict limit 988065
c 
c [simplification-15] limit of 988077 conflicts hit after 988078 conflicts
c [ternres-13] limit 94112058 with penalty 0 = 0 + 0
c [ternres-13] all 13996 free variables schedulable
c [ternres-13] 709 ternary resolvents (27 bin, 682 trn)
c [ternres-13] fully completed ternary resolution
c [card-5] limit 2941001 penalty 4 = 4 + 0
c [card-5] found 3941 at-most-one constraints of average size 4.1
c [card-5] found 204 at-most-two constraints of average size 4.1
c [card-5] using previous limit 2941001 for elimination
c [card-5] 4145 out of 4145 constraints (100%) meet size limits
c [card-5] no units found
c [card-5] no at-most-one constraints generated
c [gauss-12] limit 18822411 penalty 0 = 0 + 0
c [gauss-12] extracted 10027 xors of average arity 3.0
c [gauss-12] connected 29993 occurrences of 1942 variables (average 15.4)
c [gauss-12] limit 18822411 penalty 0 = 0 + 0
c [gauss-12] connected 7490 occurrences of 1942 variables (average 3.9)
c [gauss-12] fully completed
c [gauss-12] exported 0 unary, 0 binary and 1 ternary equations
c [decomp-26] removed 20 variables
c [treelook-4] limit 588200 penalty 3 = 3 + 0 boost 1
c [treelook-4] scheduled 22015 literals 79%
c [treelook-4] scheduling used 588258 steps
c [treelook-4] not fully scheduled
c [treelook-4] limit 588200 penalty 3 = 3 + 0 boost 1
c [treelook-4] used 602875 steps
c [treelook-4] 21878 literals remain 78%
c [treelook-4] 8212 variables remain to probed next time 59%
c [decomp-27] removed 2 variables
c [treelook-4] removed 2 variables, found 587 hbrs
c [cgrclsr-9] limit 8000000 penalty 0 = 0 + 0
c [cgrclsr-9] 4969 schedulable variables 36%
c [cgrclsr-9] fully completed congruence closure
c [cgrclsr-9] removed 2 variables
c [lift-13] limit 20000000 with penalty 0 = 0 + 0
c [lift-13] using 19 probes 0%
c [lift-13-1] found 1 units 1 impls in round 1
c [lift-13-2] found 0 units 2 impls in round 2
c [lift-13-3] found 0 units 1 impls in round 3
c [lift-13-4] found 0 units 0 impls in round 4
c [lift-13-5] found 0 units 2 impls in round 5
c [lift-13] 1 units, 6 impls, 0 eqs in 6 rounds
c [lift-13] 3098 variables remain 22% (10873 retained)
c [lift-13] removed 1 variables
c [cliff-13] limit of 75289647 steps penalty 0 = 0 + 0
c [cliff-13] failed 2, lifted 4
c [unhide-11] limit 9411205 with penalty 1 = 1 + 0
c [unhide-11-17] 0 units, 0 failed, 10077 tauts, 0 hbrs, 182262 literals
c [transred-13] limit 2000000 with penalty 0 = 0 + 0
c [transred-13] removed 439 transitive binary clauses
c [cce-14] limit of 188224117 steps penalty 0 = 0 + 0
c [cce-14-1] eliminated 1 clauses out of 661 (0%) of length 17
c [cce-14-1] eliminated 1 clauses out of 29 (3%) of length 13
c [cce-14-1] eliminated 26 clauses out of 253 (10%) of length 12
c [cce-14-1] eliminated 28 clauses out of 1375 (2%) of length 11
c [cce-14-1] eliminated 5 clauses out of 631 (1%) of length 10
c [cce-14-1] eliminated 13 clauses out of 892 (1%) of length 9
c [cce-14-1] eliminated 16 clauses out of 2043 (1%) of length 8
c [cce-14-1] eliminated 20 clauses out of 1688 (1%) of length 7
c [cce-14-1] eliminated 41 clauses out of 3895 (1%) of length 6
c [cce-14-1] eliminated 65 clauses out of 4672 (1%) of length 5
c [cce-14-1] eliminated 148 clauses out of 9085 (2%) of length 4
c [cce-14-1] completed large round (ACCE)
c [cce-14-1] eliminated 364 large clauses in 168465054 steps
c [cce-14-1] allowing another 84232527 steps for small clauses
c [cce-14] scheduling 71359 clauses = 64870 binary + 6489 ternary
c [cce-14] tried to eliminate 20323 small clauses 28%
c [cce-14] eliminated 1597 small clauses 2%
c [cce-14] eliminated 1444 binary clauses 2%
c [cce-14] eliminated 153 ternary clauses 2%
c [cce-14-1] eliminated 1597 small clauses in 188224118 steps
c [cce-14-1] incomplete small round (ACCE)
c [cce-14-1] eliminated 1961 covered clauses in round 1
c [cce-14] eliminated 1961 covered clauses in TOTAL during 1 rounds
c [elim-15] scheduling all variables this time
c [elim-15] scheduled 13965 variables 100%
c [elim-15] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-15-1] eliminated 166 variables 1% in round 1 in 22442777 steps
c [elim-15-1] backward subsumption/strengthening limit 44885554
c [elim-15-1] subsumed 0 and strengthened 0 clauses in 5839126 steps
c [elim-15] fully completed in 1 rounds
c [elim-15] transition to [ all 0 rem 0 ] state
c [elim-15] eliminated 166 = 1% variables out of 13965
c [bca-14] limit of 10000000 steps
c [bca-14] 6941 out of 27600 literals actually usable 25%
c [bca-14] added 33 blocked clauses in 111051 steps
c [simplification-15] removed 197 variables 1.4% (13799 remain 22%)
c [simplification-15] removed 3130 irredundant clauses 2.8% (107763 remain 35%)
c [simplification-15] maximum reduction of 3% = max (1%, 3%)
c [simplification-15] geometric conflict interval increment 61034 = 244137 / 4
c [simplification-15] new conflict interval 305171
c [simplification-15] penalized conflict interval 305171 = 1 * 305171
c [simplification-15] new conflict limit 1293249
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  378.2   13799   107763   1011711   86545  29459 42444   8 14.6  47.0   23
c -  390.3   13799   107763   1044703   88460  29559 42470   9 14.6  46.8   23
c -  403.9   13799   107763   1078314   90621  29697 42494  12 14.6  46.6   22
c i  407.5   13798   107763   1086702   98569  29754 42501   7 14.6  46.5   26
c -  415.4   13796   107763   1112576   92518  29808 42512  14 14.6  46.5   23
c -  426.5   13796   107763   1149587   93551  29865 42524   7 14.8  46.3   22
c -  437.9   13796   107763   1189872   94867  29922 42531  16 15.1  46.3   23
c -  450.1   13796   107763   1238090   95851  29988 42538  17 15.9  46.7   23
c R  453.6   13796   107763   1251501  105698  30003 42538  16 16.1  46.7   30
c -  464.9   13796   107763   1276334   97514  30089 42554  12 16.1  46.6   23
c 
c [simplification-16] limit of 1293505 conflicts hit after 1293505 conflicts
c [ternres-14] limit 131611561 with penalty 0 = 0 + 0
c [ternres-14] all 13796 free variables schedulable
c [ternres-14] 8634 ternary resolvents (59 bin, 8575 trn)
c [ternres-14] fully completed ternary resolution
c [gauss-13] limit 26322312 penalty 0 = 0 + 0
c [gauss-13] extracted 9755 xors of average arity 3.0
c [gauss-13] connected 29228 occurrences of 1876 variables (average 15.6)
c [gauss-13] limit 26322312 penalty 0 = 0 + 0
c [gauss-13] connected 7113 occurrences of 1876 variables (average 3.8)
c [gauss-13] fully completed
c [gauss-13] exported 0 unary, 0 binary and 1 ternary equations
c [decomp-28] removed 18 variables
c [basicprobe-4] limit 100000000 penalty 0 = 0 + 0
c [basicprobe-4-0] 2972 sched 22%, 4 failed, 0 lifted, 3150 hbrs
c [decomp-29] removed 11 variables
c [basicprobe-4-1] 7579 sched 55%, 13 failed, 0 lifted, 3210 hbrs
c [decomp-30] removed 16 variables
c [basicprobe-4-2] 7512 sched 55%, 3 failed, 0 lifted, 497 hbrs
c [decomp-31] removed 3 variables
c [basicprobe-4-3] 1504 probes remain 11% after last round
c [basicprobe-4-3] 21 units = 21 failed (100%) + 0 lifted (0%)
c [basicprobe-4-3] removed 31 variables, found 7000 hbrs
c [bate-3] eliminated 30 asymmetric tautologies during probing
c [cgrclsr-10] limit 8000000 penalty 0 = 0 + 0
c [cgrclsr-10] all 13747 free variables schedulable
c [cgrclsr-10] 3662 variables remain 27% (10078 retained)
c [cgrclsr-10] removed 7 variables
c [lift-14] limit 20000000 with penalty 0 = 0 + 0
c [lift-14] using 119 probes 1%
c [lift-14-1] found 0 units 16 impls in round 1
c [lift-14-2] found 0 units 4 impls in round 2
c [lift-14-3] found 0 units 8 impls in round 3
c [lift-14-4] found 0 units 6 impls in round 4
c [lift-14-5] found 0 units 4 impls in round 5
c [lift-14] 0 units, 38 impls, 15 eqs in 6 rounds
c [lift-14] 2916 variables remain 21% (10809 retained)
c [lift-14] removed 15 variables
c [cliff-14] limit of 100000000 steps penalty 0 = 0 + 0
c [cliff-14] failed 0, lifted 0
c [transred-14] limit 2000000 with penalty 0 = 0 + 0
c [transred-14] removed 524 transitive binary clauses
c [block-9] scheduling all variables this time
c [block-9] scheduled 13725 variables 100%
c [block-9] limit of 100000000 steps penalty 3 = 3 + 0
c [block-9] fully completed
c [block-9] transition to [ all 0 rem 0 ] state
c [block-9] eliminated 17 blocked clauses
c [block-9] 17 < 1/1000 * 107399 = 107 considered unsuccessful
c [cce-15] limit of 263223122 steps penalty 0 = 0 + 0
c [cce-15-1] eliminated 15 clauses out of 667 (2%) of length 17
c [cce-15-1] eliminated 2 clauses out of 9 (22%) of length 14
c [cce-15-1] eliminated 2 clauses out of 239 (1%) of length 12
c [cce-15-1] eliminated 17 clauses out of 1365 (1%) of length 11
c [cce-15-1] eliminated 1 clauses out of 637 (0%) of length 10
c [cce-15-1] eliminated 10 clauses out of 886 (1%) of length 9
c [cce-15-1] eliminated 13 clauses out of 2039 (1%) of length 8
c [cce-15-1] eliminated 14 clauses out of 1660 (1%) of length 7
c [cce-15-1] eliminated 23 clauses out of 3891 (1%) of length 6
c [cce-15-1] eliminated 39 clauses out of 4612 (1%) of length 5
c [cce-15-1] eliminated 103 clauses out of 8977 (1%) of length 4
c [cce-15-1] completed large round (ACCE)
c [cce-15-1] eliminated 239 large clauses in 169184171 steps
c [cce-15-1] allowing another 84592085 steps for small clauses
c [cce-15] scheduling 69121 clauses = 62836 binary + 6285 ternary
c [cce-15] tried to eliminate 35373 small clauses 51%
c [cce-15] eliminated 2313 small clauses 3%
c [cce-15] eliminated 2118 binary clauses 3%
c [cce-15] eliminated 195 ternary clauses 3%
c [cce-15-1] eliminated 2313 small clauses in 263223123 steps
c [cce-15-1] incomplete small round (ACCE)
c [cce-15-1] eliminated 2552 covered clauses in round 1
c [cce-15] eliminated 2552 covered clauses in TOTAL during 1 rounds
c [elim-16] scheduling all variables this time
c [elim-16] scheduled 13725 variables 100%
c [elim-16] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-16-1] eliminated 209 variables 2% in round 1 in 23141042 steps
c [elim-16-1] backward subsumption/strengthening limit 46282084
c [elim-16-1] subsumed 0 and strengthened 0 clauses in 5619024 steps
c [elim-16] fully completed in 1 rounds
c [elim-16] transition to [ all 0 rem 0 ] state
c [elim-16] eliminated 209 = 2% variables out of 13725
c [bca-15] limit of 10000000 steps
c [bca-15] 6082 out of 27034 literals actually usable 22%
c [bca-15] added 65 blocked clauses in 127227 steps
c [simplification-16] removed 280 variables 2.0% (13516 remain 21%)
c [simplification-16] removed 3795 irredundant clauses 3.5% (103968 remain 34%)
c [simplification-16] maximum reduction of 4% = max (2%, 4%)
c [simplification-16] geometric conflict interval increment 61034 = 305171 / 5
c [simplification-16] new conflict interval 366205
c [simplification-16] penalized conflict interval 366205 = 1 * 366205
c [simplification-16] new conflict limit 1659710
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  501.4   13516   103968   1315756   98057  38010 49736   6 16.1  46.4   24
c i  509.7   13515   103968   1336313  117085  38077 49740   7 16.1  46.3   33
c -  517.6   13515   103968   1352980  100236  38143 49751  11 16.1  46.1   25
c -  532.7   13515   103968   1392899  101594  38241 49762   9 16.1  46.0   25
c -  549.3   13515   103968   1431517  103945  38360 49770  10 16.1  45.8   25
c -  566.3   13515   103968   1469641  105613  38511 49785  10 16.1  45.5   26
c -  582.2   13515   103968   1510864  107498  38587 49794  15 16.1  45.4   26
c -  601.0   13515   103968   1552654  109206  38674 49800  10 16.1  45.2   26
c -  619.7   13515   103968   1593125  111256  38795 49807  12 16.1  45.0   26
c -  638.8   13515   103968   1633668  113015  38907 49818  14 16.1  44.8   25
c 
c [simplification-17] limit of 1659888 conflicts hit after 1659888 conflicts
c [ternres-15] limit 185330948 with penalty 0 = 0 + 0
c [ternres-15] all 13515 free variables schedulable
c [ternres-15] 5006 ternary resolvents (14 bin, 4992 trn)
c [ternres-15] fully completed ternary resolution
c [gauss-14] limit 37066189 penalty 0 = 0 + 0
c [gauss-14] extracted 9585 xors of average arity 3.0
c [gauss-14] connected 28751 occurrences of 1852 variables (average 15.5)
c [gauss-14] limit 37066189 penalty 0 = 0 + 0
c [gauss-14] connected 6877 occurrences of 1852 variables (average 3.7)
c [gauss-14] fully completed
c [gauss-14] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-32] removed 18 variables
c [simpleprobe-5] all 13497 free variables schedulable
c [simpleprobe-5] limit 200000000 penalty 0 = 0 + 0
c [decomp-33] removed 37 variables
c [simpleprobe-5] fully completed simple probing
c [simpleprobe-5] removed 37 variables, found 17537 hbrs, 0 units
c [cgrclsr-11] limit 8000000 penalty 0 = 0 + 0
c [cgrclsr-11] 3588 schedulable variables 27%
c [cgrclsr-11] fully completed congruence closure
c [lift-15] limit 20000000 with penalty 0 = 0 + 0
c [lift-15] using 117 probes 1%
c [lift-15-1] found 0 units 9 impls in round 1
c [lift-15-2] found 0 units 5 impls in round 2
c [lift-15-3] found 0 units 7 impls in round 3
c [lift-15-4] found 0 units 6 impls in round 4
c [lift-15-5] found 0 units 3 impls in round 5
c [lift-15] 0 units, 30 impls, 32 eqs in 6 rounds
c [lift-15] 2724 variables remain 20% (10704 retained)
c [lift-15] removed 32 variables
c [transred-15] limit 2000000 with penalty 0 = 0 + 0
c [transred-15] removed 923 transitive binary clauses
c [cce-16] limit of 370661897 steps penalty 0 = 0 + 0
c [cce-16-1] eliminated 3 clauses out of 3 (100%) of length 26
c [cce-16-1] eliminated 1 clauses out of 1 (100%) of length 25
c [cce-16-1] eliminated 2 clauses out of 2 (100%) of length 24
c [cce-16-1] eliminated 4 clauses out of 4 (100%) of length 21
c [cce-16-1] eliminated 1 clauses out of 19 (5%) of length 20
c [cce-16-1] eliminated 2 clauses out of 559 (0%) of length 19
c [cce-16-1] eliminated 2 clauses out of 746 (0%) of length 18
c [cce-16-1] eliminated 4 clauses out of 628 (1%) of length 17
c [cce-16-1] eliminated 1 clauses out of 10 (10%) of length 15
c [cce-16-1] eliminated 2 clauses out of 248 (1%) of length 12
c [cce-16-1] eliminated 21 clauses out of 1302 (2%) of length 11
c [cce-16-1] eliminated 4 clauses out of 657 (1%) of length 10
c [cce-16-1] eliminated 21 clauses out of 904 (2%) of length 9
c [cce-16-1] eliminated 40 clauses out of 2042 (2%) of length 8
c [cce-16-1] eliminated 14 clauses out of 1633 (1%) of length 7
c [cce-16-1] eliminated 19 clauses out of 3877 (0%) of length 6
c [cce-16-1] eliminated 42 clauses out of 4801 (1%) of length 5
c [cce-16-1] eliminated 162 clauses out of 9089 (2%) of length 4
c [cce-16-1] completed large round (ACCE)
c [cce-16-1] eliminated 345 large clauses in 177815518 steps
c [cce-16-1] allowing another 88907759 steps for small clauses
c [cce-16] scheduling 65484 clauses = 59400 binary + 6084 ternary
c [cce-16] tried to eliminate 53131 small clauses 81%
c [cce-16] eliminated 1927 small clauses 3%
c [cce-16] eliminated 1726 binary clauses 3%
c [cce-16] eliminated 201 ternary clauses 3%
c [cce-16-1] eliminated 1927 small clauses in 370661898 steps
c [cce-16-1] incomplete small round (ACCE)
c [cce-16-1] eliminated 2272 covered clauses in round 1
c [cce-16] eliminated 2272 covered clauses in TOTAL during 1 rounds
c [elim-17] scheduling all variables this time
c [elim-17] scheduled 13428 variables 100%
c [elim-17] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-17-1] eliminated 157 variables 1% in round 1 in 22470698 steps
c [elim-17-1] backward subsumption/strengthening limit 44941396
c [elim-17-1] subsumed 0 and strengthened 0 clauses in 5444619 steps
c [elim-17] fully completed in 1 rounds
c [elim-17] transition to [ all 0 rem 0 ] state
c [elim-17] eliminated 157 = 1% variables out of 13428
c [bca-16] limit of 10000000 steps
c [bca-16] 5470 out of 26544 literals actually usable 21%
c [bca-16] added 19 blocked clauses in 146759 steps
c [rephase-7] after 1659888 conflicts (new increment 1280000, next 2939888)
c [flushphases] 0 phases reset
c [simplification-17] removed 244 variables 1.8% (13271 remain 21%)
c [simplification-17] removed 2816 irredundant clauses 2.7% (101152 remain 33%)
c [simplification-17] maximum reduction of 3% = max (2%, 3%)
c [simplification-17] geometric conflict interval increment 91551 = 366205 / 4
c [simplification-17] new conflict interval 457756
c [simplification-17] penalized conflict interval 457756 = 1 * 457756
c [simplification-17] new conflict limit 2117644
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  676.2   13271   101152   1680122  113566  43643 66931   9 16.1  44.6   27
c -  695.8   13271   101152   1722250  115539  43754 66938  10 16.1  44.5   28
c -  716.0   13271   101152   1764386  117396  43871 66944  13 16.0  44.3   28
c -  732.5   13271   101152   1810370  118577  43933 66957  12 16.1  44.2   28
c -  754.5   13271   101152   1856143  119895  44006 66964   8 16.2  44.1   29
c -  776.1   13271   101152   1901666  121737  44132 66979   9 16.2  44.0   29
c -  798.8   13271   101152   1946257  123610  44242 66988   8 16.2  43.8   28
c -  821.0   13271   101152   1993355  125083  44326 66997   6 16.3  43.7   28
c -  844.5   13271   101152   2040214  126744  44427 67013   9 16.3  43.5   28
c -  866.1   13271   101152   2088572  128632  44501 67031  13 16.4  43.4   28
c 
c [simplification-18] limit of 2117838 conflicts hit after 2117838 conflicts
c [ternres-16] limit 200000000 with penalty 0 = 0 + 0
c [ternres-16] all 13271 free variables schedulable
c [ternres-16] 4155 ternary resolvents (32 bin, 4123 trn)
c [ternres-16] fully completed ternary resolution
c [decomp-34] removed 12 variables
c [lift-16] limit 20000000 with penalty 0 = 0 + 0
c [lift-16] using 43 probes 0%
c [lift-16-1] found 0 units 5 impls in round 1
c [lift-16-2] found 0 units 5 impls in round 2
c [lift-16-3] found 0 units 3 impls in round 3
c [lift-16-4] found 0 units 4 impls in round 4
c [lift-16-5] found 0 units 1 impls in round 5
c [lift-16] 0 units, 18 impls, 4 eqs in 6 rounds
c [lift-16] 2637 variables remain 20% (10618 retained)
c [lift-16] removed 4 variables
c [cliff-15] limit of 50000000 steps penalty 1 = 1 + 0
c [cliff-15] failed 3, lifted 7
c [unhide-12] limit 5000000 with penalty 2 = 2 + 0
c [unhide-12-19] 0 units, 0 failed, 14262 tauts, 0 hbrs, 596584 literals
c [transred-16] limit 2000000 with penalty 0 = 0 + 0
c [transred-16] removed 740 transitive binary clauses
c [cce-17] limit of 524784737 steps penalty 0 = 0 + 0
c [cce-17-1] eliminated 1 clauses out of 1 (100%) of length 22
c [cce-17-1] eliminated 1 clauses out of 525 (0%) of length 19
c [cce-17-1] eliminated 1 clauses out of 755 (0%) of length 18
c [cce-17-1] eliminated 6 clauses out of 631 (1%) of length 17
c [cce-17-1] eliminated 1 clauses out of 19 (5%) of length 16
c [cce-17-1] eliminated 1 clauses out of 11 (9%) of length 15
c [cce-17-1] eliminated 3 clauses out of 13 (23%) of length 14
c [cce-17-1] eliminated 1 clauses out of 20 (5%) of length 13
c [cce-17-1] eliminated 4 clauses out of 219 (2%) of length 12
c [cce-17-1] eliminated 21 clauses out of 1003 (2%) of length 11
c [cce-17-1] eliminated 6 clauses out of 600 (1%) of length 10
c [cce-17-1] eliminated 5 clauses out of 1000 (0%) of length 9
c [cce-17-1] eliminated 7 clauses out of 2072 (0%) of length 8
c [cce-17-1] eliminated 16 clauses out of 1630 (1%) of length 7
c [cce-17-1] eliminated 15 clauses out of 3847 (0%) of length 6
c [cce-17-1] eliminated 18 clauses out of 4947 (0%) of length 5
c [cce-17-1] eliminated 73 clauses out of 8958 (1%) of length 4
c [cce-17-1] completed large round (ACCE)
c [cce-17-1] eliminated 180 large clauses in 172091011 steps
c [cce-17-1] allowing another 86045505 steps for small clauses
c [cce-17] scheduling 63124 clauses = 57254 binary + 5870 ternary
c [cce-17] tried to eliminate 63124 small clauses 100%
c [cce-17] eliminated 673 small clauses 1%
c [cce-17] eliminated 605 binary clauses 1%
c [cce-17] eliminated 68 ternary clauses 1%
c [cce-17-1] eliminated 673 small clauses in 419075235 steps
c [cce-17-1] completed small round (ACCE)
c [cce-17-1] completed small and large (ACCE)
c [cce-17-1] eliminated 853 covered clauses in round 1
c [cce-17-2] completed large round (ACCE)
c [cce-17-2] allowing another 0 steps for small clauses
c [cce-17] scheduling 62451 clauses = 56649 binary + 5802 ternary
c [cce-17] tried to eliminate 20195 small clauses 32%
c [cce-17-2] incomplete small round (ACCE)
c [cce-17-2] eliminated 0 covered clauses in round 2
c [cce-17] eliminated 853 covered clauses in TOTAL during 2 rounds
c [elim-18] scheduling all variables this time
c [elim-18] scheduled 13245 variables 100%
c [elim-18] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-18-1] eliminated 139 variables 1% in round 1 in 21082052 steps
c [elim-18-1] backward subsumption/strengthening limit 42164104
c [elim-18-1] subsumed 0 and strengthened 0 clauses in 5358087 steps
c [elim-18] fully completed in 1 rounds
c [elim-18] transition to [ all 0 rem 0 ] state
c [elim-18] eliminated 139 = 1% variables out of 13245
c [bca-17] limit of 10000000 steps
c [bca-17] 5217 out of 26214 literals actually usable 20%
c [bca-17] added 12 blocked clauses in 165044 steps
c [simplification-18] removed 165 variables 1.2% (13106 remain 21%)
c [simplification-18] removed 1332 irredundant clauses 1.3% (99820 remain 32%)
c [simplification-18] maximum reduction of 1% = max (1%, 1%)
c [simplification-18] geometric conflict interval increment 228878 = 457756 / 2
c [simplification-18] new conflict interval 686634
c [simplification-18] penalized conflict interval 686634 = 1 * 686634
c [simplification-18] new conflict limit 2804472
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  913.7   13106    99820   2138760  128063  46184 54746  11 16.4  43.3   29
c i  920.7   13105    99820   2152439  140988  46216 54750   9 16.4  43.2   36
c -  938.4   13105    99820   2186119  129761  46275 54757   8 16.4  43.1   29
c -  961.8   13105    99820   2235836  131641  46358 54767  13 16.4  43.0   30
c -  987.8   13105    99820   2283426  133360  46449 54775   8 16.4  42.9   30
c
c CAUGHT SIGNAL 15 SIGTERM
c
c s UNKNOWN
c bate: 72 basic ate = 50 trn 69% + 22 lrg 31% in 3 updates
c bcas: 17 count, 1118 added (106 skipped), 1699460 steps
c bkwd: tried 2166423 clauses, 4329835 lits, 2.00 lits/clause
c bkwd: checked 90816985 occs, 41.92 occs/clause, 20.97 occs/lit
c bkwd: subsumed 4 binary, 1280 ternary, 292 large
c bkwd: strengthened 2 binary, 23 ternary (100% self), 2041 large (0% self)
c blkd: 9 bces, 2144 removed, 6115071 resolutions, 15685015 steps
c blkd: 4745 blocking literals 4%, 103 pure
c bvas: 0 bvas, 0 added, 0 removed
c card: 5 count, 0 units, 87 am1, 10343847 steps
c card: 171 rescheduled, 1347 eliminated, 18956 resolved, 23343 subsumed
c card: 14363 at-most-one constraints found, average size 3.36
c card: 14363 at-most-one constraints used 100%, average size 3.36
c card: 423 at-most-two constraints found, average size 4.05
c card: 423 at-most-two constraints used 100%, average size 4.05
c cces: 17 cces, 28576 eliminated, 24416 ate 85%, 4160 abce 15%
c cces: 0 probed, 0 lifted, 0 failed
c cces: 0 cached, 0 rsz, 0 cols 0%, 0 srch, 0 hits 0%
c cgrs: 11 count, 13251572 esteps, 38434067 csteps
c cgrs: 15 eqs, 1 units
c cgrs: 54 matched (38 ands 70%, 4 xors 7%, 12 ites 22%)
c cgrs: 4 simplified (4 ands 100%, 0 xors 0%, 0 ites 0%)
c cgrs: 45962 extracted (33452 ands 73%, 8469 xors 18%, 4041 ites 9%)
c clff: 15 cliffs, 326 lifted, 200 failed
c clff: 133361 decisions, 485941891 steps
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: 162 gcs, 0 rescored clauses, 1209 rescored vars
c dcps: 34 decompositions, 14527 equivalent 23%
c deco: 199193 decision-only clauses 9%, 80% reduction
c decs: 7163721 decision, 0 random 0.000%, 0 flipped 0.000%
c decs: 252685 flipped 3.527% (in 4265 phases)
c elms: 18 elims, 26716 eliminated 42%
c elms: 37 rounds, 2.1 rounds/bve
c elms: 20818 small 78%, 5795 large 22%
c elms: 41264 tried small, 20818 succeeded 50%, 20446 failed 50%
c elms: 9544 subsumed, 21698 strengthened, 2301 blocked
c elms: 9552766 copies, 13386186 resolutions, 1264925 ipos
c elms: 8378182 subchks, 21282048 strchks
c frcs: 0 computed, 0 - 0 average min-cut range
c gaus: 14 extractions, 126056 extracted, 3.0 size, 4 max
c gaus: exported 0 units, 24 binary and 105 ternary equations
c gaus: 11 gc, 277698112 steps, 138849056 extr 50%, 18155492 elim 7%
c glue: 16.4 orig avg, 15.8 real avg, 3.5 scaled avg
c glue: 0 maxscaledglue=15 (0%)
c hbrs: 161193 = 104846 simple + 55805 trn 65% + 542 lrg 35%, 2642 sub 0%
c hght: 43 average, 2.61 height/glue
c ints: 64184 luby (18114864 steps), 0 inout (0 steps)
c lift: 16 phases, 81529 probed (27397 level1 34%, 54132 level2 66%)
c lift: 158 units, 368 equivalences, 1031 implications
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 2298746 clauses, 61.3 length
c lrnd: 690169 uips 30%, 1341661 flips 58%
c mega: 0 count, 0 failed, 0 rounds
c mins: 140998890 learned lits, 41% minimized
c mins: 2065030 mins 90%, 2473 bin 0%, 32050 size 1%, 199193 deco 9%
c move: moved 2298746, 19151 bin 1%, 2909 trn 0%, 0 lrg 0%
c otfs: str 38198 dyn (37681 red, 517 irr) 10798 drv 28%, 27400 rst 72%
c otfs: sub 309 dyn (309 red, 0 irr)
c phas: 11 computed, 21544 set, 11066 pos (51%), 10478 neg (49%)
c prbs: 4 basic, 60810 probed, 102 failed, 4 lifted
c prbs: 5 simple, 221022 probed, 156 failed, 15195 eqs
c prbs: 4 treelook, 314 probed, 0 failed, 0 lifted
c prps: 2013033828 props, 270 props/dec
c prps: 96% srch, 4% simp, 0% lkhd
c psns: 290606316 searches, 52771387 hits, 18% hit rate
c rdps: 0 count, 0 units, 0 bin, 0 trn, 0 steps
c rdps: 0 partial eliminations, 0 bounded 0%
c rdps: 0 resolutions, 0 size 0%, 0 model 0%
c reds: 83 count, 0 reset, 4 acts 5%
c reds: 0 geom 0%, 0 glue useless 0%
c reds: 0 memlim 0%, 83 arith 100%, 0 double 0%
c rmbd: 22504 removed, 18007 red 80%
c rphs: 7 recomputed phases
c rsts: 63308 restarts 99%, 876 skipped 1%
c rsts: 0 saturating 0%, 0 agile 0%, 876 reuse 100%
c rsts: 35.7 avg interval, 35.7 scaled, 1.0 factor
c rsts: 17357 kept 27.4% average 21.5%
c simp: 18 count (18 confs 100%, 0 irr 0%, 0 vars 0%)
c subl: 2298746 count (3390179 tried 1.5), 211233 sub out of 2282581 (9.3%)
c sync: 0 produced units, 0 successful consumptions 0%
c sync: 0 consume units calls, 0 tried 0%, 0 success 0%
c sync: 0 produced clauses, 0 successful consumptions 0%
c sync: 0 consume clause calls, 0 tried 0%, 0 success 0%
c tabr: 1 count
c tops: 9106 fixed 14%, 82 its, 28165.17 confs/it
c trvs: 46971516617 traversals, 98% srch, 2% simp, 0% lkhd
c trvs: 24.0 search traversals per propagation, 20026.4 per conflict
c trvs: 1.6 search traversals per search visit
c trds: 16 transitive reductions, 7626 removed, 0 failed
c trds: 58356 nodes, 198403 edges, 27490042 steps
c trim: 5092077 words, 19.4 MB
c trnr: 16 count, 1941 bin, 57421 trn, 666285123 steps
c unhd: 12 count, 19 rounds, 29947546 steps
c unhd: 524 non-trivial sccs of average size 2.1
c unhd: 21 units, 21 bin, 0 trn, 0 lrg
c unhd: 94 failed, 87 stamp, 0 lits, 3 bin, 1 trn, 0 lrg
c unhd: 52233 tauts, 863 bin 2%, 8137 trn 16%, 3456 lrg 7%
c unhd: 52233 tauts, 39777 stamp 76%, 49343 red 94%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 1012147 str, 21 bin 0%, 1623 trn 0%, 1010503 lrg 100%, 1002857 red 99%
c vars: 13105 remaining 21% and 50349 removed 79% out of 63454
c vars: 9106 fixed 14%, 26716 eliminated 42%, 14527 equivalent 23%
c vsts: 30262794152 visits, 98% srch, 2% simp, 0% lkhd
c vsts: 15.3 search visits per propagation, 12791.8 per conflict
c wchs: 6361398411 pushed, 77991315 enlarged, 275 defrags
c 
c scaledglue  added       reduced       forcing      resolved     conflicts
c 
c all   2282581 100   1866689 100 245707465 100  39848428 100   1398573 100
c 
c  0     115718   5         0   0 190714007  78< 23581312  59    587848  42 
c  1     103765   5     50033   3  43434677  18   8992175  23<   325652  23<
c  2     396341  17    384707  21   5201936   2   2136626   5    119724   9 
c  3     611502  27    587629  31<  3711417   2   2340701   6    159076  11 
c  4     506835  22<   478761  26   1574895   1   1467359   4    110625   8 
c  5     286116  13    269036  14    641280   0    747566   2     60531   4 
c  6     114577   5     55991   3    208393   0    270724   1     18495   1 
c  7      68607   3     18905   1    105417   0    147628   0      7946   1 
c  8      43005   2     11818   1     63381   0     89411   0      4812   0 
c  9      19081   1      5270   0     28184   0     39730   0      2070   0 
c 10      16228   1      4234   0     22566   0     33468   0      1685   0 
c 11        800   0       301   0      1306   0      1718   0       109   0 
c 12          6   0         4   0         6   0        10   0         0   0 
c 13          0   0         0   0         0   0         0   0         0   0 
c 14          0   0         0   0         0   0         0   0         0   0 
c 15          0   0         0   0         0   0         0   0         0   0 
c 
c avg             3.5           3.5           0.3           0.9           1.5
c std             1.8           1.3           0.7           1.4           1.8
c 
c   80.927   8% analysis
c   72.228   7% cce
c   27.130   3% mincls
c   12.855   1% cliff
c   12.638   1% elim
c   12.626   1% bump
c   11.591   1% ternres
c   10.149   1% decide
c    8.344   1% restart
c    8.340   1% gauss
c    7.822   1% probe
c    6.647   1% gc
c    6.098   1% lift
c    5.618   1% unhide
c    3.098   0% decomp
c    2.760   0% backward
c    2.287   0% defrag
c    2.271   0% cgrclsr
c    1.690   0% transred
c    1.508   0% block
c    1.191   0% reduce
c    1.103   0% bca
c    0.411   0% card
c    0.239   0% phase
c    0.020   0% tabularasa
c    0.006   0% cutwidth
c    0.000   0% bva
c    0.000   0% force
c    0.000   0% locs
c    0.000   0% mega
c    0.000   0% rdp
c ----------------------------------
c    2.548   0% probe simple     33%
c    4.749   0% probe basic      61%
c    0.525   0% probe tree-look   7%
c ==================================
c    2.598   0% preprocessing     2%
c  144.149  14% inprocessing     98%
c ==================================
c  146.747  15% simplifying
c  853.131  85% search
c ==================================
c  999.879 100% all
c 
c 7163721 decisions, 7164.6 decisions/sec
c 2309544 conflicts, 2309.8 conflicts/sec
c 2013033828 propagations, 2.0 megaprops/sec
c 999.9 seconds, 60.7 MB
c
c CAUGHT SIGNAL 15 SIGTERM
c
c launch: done
