c launch: /data/cnf/sc2014/app/9dlx_vliw_at_b_iq9.cnf.bz2
c host: atom04
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/9dlx_vliw_at_b_iq9.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/9dlx_vliw_at_b_iq9.cnf.bz2
c no embedded options
c found 'p cnf 482093 9676386' header
c read 482093 variables, 9676386 clauses, 28195028 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 482092 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  482092  9676385         0       0      0     0   0  0.0   0.0  209
c 
c [simplification-1] limit of 0 conflicts hit after 0 conflicts
c [card-1] limit 2419096 based on 9676385 irredundant clauses
c [card-1] found 12620 at-most-one constraints of average size 3.0
c [card-1] no at-most-two constraint found
c [card-1] using previous limit 2419096 for elimination
c [card-1] 12620 out of 12620 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 12 variables
c [simpleprobe-1] all 482081 free variables schedulable
c [simpleprobe-1] boosting simple probing limit by 10
c [simpleprobe-1] limit 2419084 based on 9676339 irredundant clauses
c [simpleprobe-1] 482081 variables remain 100% (0 retained)
c [simpleprobe-1] removed 0 variables, found 12 hbrs, 0 units
c [unhide-1] limit 4838169 based on 9676339 irredundant clauses
c [unhide-1-1] 1120 units, 0 failed, 47904 tauts, 0 hbrs, 181888 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 480961 variables 100%
c [elim-1] boosting limit by 40
c [elim-1] limit of 50000000 steps penalty 4 = 0 + 4
c [elim-1] incomplete 477989 not tried 99% in round 1
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 2973 = 1% variables out of 480961
c [phase-1] phase bias: 87538 positive 18%, 390450 negative 82%
c [simplification-1] removed 4093 variables 0.8% (477988 remain 99%)
c [simplification-1] removed 84578 irredundant clauses 0.9% (9591807 remain 99%)
c [simplification-1] maximum reduction of 1% = max (1%, 1%)
c [simplification-1] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-1] new conflict interval 10000
c [simplification-1] penalized conflict interval 20000 = 2 * 10000
c [simplification-1] new conflict limit 20000
c [cut-width] 6597549, max 10918140, min4 4309376 at 75%, min10 2075917 at 90%
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   32.5  477988  9591807        60      27     33    12   0  3.6 1412.0  307
c R   35.2  477988  9591807       160      66     94    12   0  8.3 1762.0  307
c i   37.0  477987  9591807       285     153    116    17   0 11.1 4510.1  308
c R   37.7  477974  9591807       422     280    124    18   2 15.8 5611.5  308
c R   41.8  477974  9591807      1072     858    136    65   0 23.1 9323.3  308
c R   48.4  477974  9591807      2470    2110    211    94   1 22.0 9892.5  310
c -   56.3  477974  9591807      4838    2302    255   111   1 23.7 9094.6  310
c R   56.7  477974  9591807      5547    2979    263   112   1 24.5 8984.1  310
c i   59.8  477973  9591807      6649    3977    288   129   0 25.1 8727.5  311
c -   64.5  471585  9591807      8161    2833    318   153   1 25.2 8402.5  310
c -   70.4  471585  9591807     12269    3456    367   232   1 26.0 7953.5  310
c R   70.4  471585  9591807     12321    3507    367   232   1 25.9 7952.4  310
c i   83.6  471584  9591807     16229    7090    455   302   0 26.0 7037.5  312
c -   86.0  471584  9591807     16805    4115    461   308   0 25.8 6891.8  310
c 
c [simplification-2] limit of 20678 conflicts hit after 20680 conflicts
c [decomp-3] removed 6993 variables
c [treelook-1] limit 2362651 based on 9450606 irredundant clauses
c [treelook-1] scheduled 354301 literals 38%
c [treelook-1] scheduling used 2362752 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 2362651 based on 9450606 irredundant clauses
c [treelook-1] used 2456665 steps
c [treelook-1] 354292 literals remain 38%
c [treelook-1] 342855 variables remain to probed next time 73%
c [treelook-1] removed 0 variables, found 71 hbrs
c [basicprobe-1] limit 18901212 based on 9450606 irredundant clauses
c [basicprobe-1-0] 467284 probes remain 99% after last round
c [basicprobe-1-0] 29 units = 29 failed (100%) + 0 lifted (0%)
c [basicprobe-1-0] removed 30 variables, found 13381 hbrs
c [unhide-2] limit 4725303 based on 9450606 irredundant clauses
c [unhide-2-2] 21490 units, 30 failed, 103 tauts, 0 hbrs, 265231 literals
c [elim-2] 448813 variables 100% will be scheduled this time
c [elim-2] scheduled 448813 variables 100%
c [elim-2] limit of 33402903 steps penalty 3 = 0 + 3
c [elim-2] incomplete 442490 not tried 99% in round 1
c [elim-2] transition to [ all 0 rem 1 ] state
c [elim-2] eliminated 6324 = 1% variables out of 448813
c [rephase-1] after 20680 conflicts (new increment 20000, next 40680)
c [flushphases] 3730 phases reset
c [phase-2] phase bias: 0 positive 0%, 0 negative 0%
c [simplification-2] removed 29095 variables 6.2% (442489 remain 92%)
c [simplification-2] removed 684981 irredundant clauses 7.1% (8906826 remain 92%)
c [simplification-2] maximum reduction of 7% = max (6%, 7%)
c [simplification-2] large reduction 7% >= 5% limit
c [simplification-2] new conflict interval 2000 = 2000/1
c [simplification-2] penalized conflict interval 4000 = 2 * 2000
c [simplification-2] new conflict limit 24680
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  117.0  442489  8906826     22013    4574    554 13668   0 28.2 6394.2  290
c 
c [simplification-3] limit of 24802 conflicts hit after 24802 conflicts
c [card-2] limit 2226706 based on 8906826 irredundant clauses
c [card-2] found 11262 at-most-one constraints of average size 3.0
c [card-2] no at-most-two constraint found
c [card-2] using previous limit 2226706 for elimination
c [card-2] 11262 out of 11262 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [decomp-5] removed 105 variables
c [simpleprobe-2] all 442384 free variables schedulable
c [simpleprobe-2] limit 3664262 penalty 4 = 1 + 3
c [simpleprobe-2] 422914 variables remain 96% (19470 retained)
c [simpleprobe-2] removed 0 variables, found 1426 hbrs, 0 units
c [unhide-3] limit 4453321 based on 8906642 irredundant clauses
c [unhide-3-3] 560 units, 12 failed, 20003 tauts, 0 hbrs, 31294 literals
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 441703 variables 100%
c [elim-3] limit of 36642621 steps penalty 3 = 0 + 3
c [elim-3] incomplete 437613 not tried 99% in round 1
c [elim-3] transition to [ all 1 rem 1 ] state
c [elim-3] eliminated 4091 = 1% variables out of 441703
c [phase-3] phase bias: 0 positive 0%, 0 negative 0%
c [simplification-3] removed 4877 variables 1.1% (437612 remain 91%)
c [simplification-3] removed 47474 irredundant clauses 0.5% (8859352 remain 92%)
c [simplification-3] maximum reduction of 1% = max (1%, 1%)
c [simplification-3] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-3] new conflict interval 20000
c [simplification-3] penalized conflict interval 40000 = 2 * 20000
c [simplification-3] new conflict limit 64802
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c R  145.5  437612  8859352     27162    9229    612 15072   1 30.0 6123.7  292
c -  147.3  437612  8859352     27675    5198    616 15078   0 29.9 6066.5  288
c i  152.7  437611  8859352     29877    7154    635 15122   0 29.5 5915.2  290
c -  160.2  437611  8859352     34163    5829    652 15161   1 30.8 5618.7  288
c -  170.8  437611  8859352     41322    6448    680 15202   1 31.7 5282.6  288
c -  184.3  437611  8859352     48859    7024    720 15237   0 31.2 4919.7  289
c -  186.1  437611  8859352     56907    7781    736 15244   0 33.0 4820.6  289
c R  186.4  437611  8859352     58946    9452    740 15244   0 33.6 4806.2  289
c 
c [simplification-4] limit of 65294 conflicts hit after 65294 conflicts
c [decomp-7] removed 48 variables
c [unhide-4] limit 4429638 based on 8859277 irredundant clauses
c [unhide-4-4] 10027 units, 37 failed, 149 tauts, 0 hbrs, 171491 literals
c [elim-4] 404430 variables 100% will be scheduled this time
c [elim-4] scheduled 404430 variables 100%
c [elim-4] limit of 70134795 steps penalty 3 = 0 + 3
c [elim-4] incomplete 397122 not tried 98% in round 1
c [elim-4] transition to [ all 0 rem 1 ] state
c [elim-4] eliminated 7309 = 2% variables out of 404430
c [rephase-2] after 65294 conflicts (new increment 40000, next 105294)
c [flushphases] 1244 phases reset
c [phase-4] phase bias: 0 positive 0%, 0 negative 0%
c [simplification-4] removed 40490 variables 9.3% (397121 remain 82%)
c [simplification-4] removed 755565 irredundant clauses 8.5% (8103787 remain 84%)
c [simplification-4] maximum reduction of 9% = max (9%, 9%)
c [simplification-4] large reduction 9% >= 5% limit
c [simplification-4] new conflict interval 2000 = 2000/1
c [simplification-4] penalized conflict interval 4000 = 2 * 2000
c [simplification-4] new conflict limit 69294
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  218.6  397121  8103787     68532    8133    839 15121   0 32.3 4818.4  265
c 
c [simplification-5] limit of 69314 conflicts hit after 69316 conflicts
c [ternres-1] boosting ternary resolution limit by 5
c [ternres-1] limit 32415148 based on 8103787 irredundant clauses
c [ternres-1] all 397121 free variables schedulable
c [ternres-1] 16513 ternary resolvents (0 bin, 16513 trn)
c [ternres-1] 265380 variables remain 67% (131741 retained)
c [gauss-1] limit 4051893 based on 8103787 irredundant clauses
c [gauss-1] extracted 28 xors of average arity 2.0
c [gauss-1] connected 56 occurrences of 51 variables (average 1.1)
c [gauss-1] limit 4051893 based on 8103787 irredundant clauses
c [gauss-1] fully completed
c [gauss-1] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-8] removed 141 variables
c [treelook-2] limit 2025879 based on 8103517 irredundant clauses
c [treelook-2] scheduled 290951 literals 37%
c [treelook-2] scheduling used 2025881 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 2025879 based on 8103517 irredundant clauses
c [treelook-2] used 5853402 steps
c [treelook-2] 290948 literals remain 37%
c [treelook-2] 249783 variables remain to probed next time 63%
c [treelook-2] removed 0 variables, found 436 hbrs
c [cgrclsr-1] limit 4051758 based on 8103517 irredundant clauses
c [cgrclsr-1] all 396980 free variables schedulable
c [cgrclsr-1] 325185 variables remain 82% (71795 retained)
c [lift-1] limit 2155241 with penalty 3 = 0 + 3
c [lift-1] using 86739 probes 22%
c [lift-1] 2 units, 4 impls, 0 eqs in 1 rounds
c [lift-1] 396972 variables remain 100% (6 retained)
c [lift-1] removed 2 variables
c [cliff-1] limit of 16206692 steps based on 8103346 irredundant clauses
c [cliff-1] failed 0, lifted 921
c [unhide-5] limit 4051673 based on 8103346 irredundant clauses
c [unhide-5-5] 857 units, 16 failed, 13434 tauts, 0 hbrs, 22145 literals
c [transred-1] limit 8075540 based on 8075540 irredundant clauses
c [transred-1] removed 5 transitive binary clauses
c [block-1] scheduling all variables this time
c [block-1] scheduled 391803 variables 100%
c [block-1] boosting limit by 10
c [block-1] limit of 359206850 steps penalty 3 = 0 + 3
c [block-1] fully completed
c [block-1] transition to [ all 0 rem 0 ] state
c [block-1] eliminated 1155823 blocked clauses
c [cce-1] boosting limit by 10
c [cce-1] limit of 71841370 steps penalty 3 = 0 + 3
c [cce-1-1] eliminated 1 clauses out of 1 (100%) of length 211
c [cce-1-1] eliminated 1 clauses out of 1 (100%) of length 194
c [cce-1-1] eliminated 1 clauses out of 1 (100%) of length 190
c [cce-1-1] eliminated 3 clauses out of 3 (100%) of length 185
c [cce-1-1] eliminated 2 clauses out of 3 (67%) of length 184
c [cce-1-1] eliminated 2 clauses out of 2 (100%) of length 183
c [cce-1-1] eliminated 4 clauses out of 5 (80%) of length 182
c [cce-1-1] eliminated 2 clauses out of 2 (100%) of length 181
c [cce-1-1] eliminated 1 clauses out of 5 (20%) of length 178
c [cce-1-1] eliminated 2 clauses out of 8 (25%) of length 176
c [cce-1-1] eliminated 2 clauses out of 3 (67%) of length 174
c [cce-1-1] eliminated 3 clauses out of 3 (100%) of length 173
c [cce-1-1] eliminated 4 clauses out of 4 (100%) of length 172
c [cce-1-1] eliminated 2 clauses out of 4 (50%) of length 171
c [cce-1-1] eliminated 8 clauses out of 10 (80%) of length 170
c [cce-1-1] eliminated 4 clauses out of 11 (36%) of length 169
c [cce-1-1] eliminated 6 clauses out of 8 (75%) of length 168
c [cce-1-1] eliminated 3 clauses out of 16 (19%) of length 167
c [cce-1-1] eliminated 8 clauses out of 9 (89%) of length 166
c [cce-1-1] eliminated 1 clauses out of 3 (33%) of length 163
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 60 large clauses in 71841371 steps
c [cce-1-1] allowing another 35920685 steps for small clauses
c [cce-1] scheduling 6381727 clauses = 6380449 binary + 1278 ternary
c [cce-1] tried to eliminate 41 small clauses 0%
c [cce-1] eliminated 3 small clauses 0%
c [cce-1] eliminated 3 binary clauses 0%
c [cce-1-1] eliminated 3 small clauses in 71841371 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 63 covered clauses in round 1
c [cce-1] eliminated 63 covered clauses in TOTAL during 1 rounds
c [cce-1] 63 < 1/1000 * 6839468 = 6839 considered unsuccessful
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 389690 variables 100%
c [elim-5] limit of 71841370 steps penalty 3 = 0 + 3
c [elim-5] incomplete 370291 not tried 95% in round 1
c [elim-5] transition to [ all 1 rem 1 ] state
c [elim-5] eliminated 19400 = 5% variables out of 389690
c [bca-1] limit of 10000000 steps
c [bca-1] 722631 out of 740582 literals actually usable 98%
c [bca-1] added 12527 blocked clauses in 2099996 steps
c [phase-5] phase bias: 0 positive 0%, 0 negative 0%
c [simplification-5] removed 26831 variables 6.8% (370290 remain 77%)
c [simplification-5] removed 1283865 irredundant clauses 15.8% (6819922 remain 70%)
c [simplification-5] maximum reduction of 16% = max (7%, 16%)
c [simplification-5] large reduction 16% >= 5% limit
c [simplification-5] new conflict interval 2000 = 2000/1
c [simplification-5] penalized conflict interval 4000 = 2 * 2000
c [simplification-5] new conflict limit 73316
c 
c [simplification-6] limit of 73340 conflicts hit after 73340 conflicts
c [ternres-2] limit 27279684 based on 6819921 irredundant clauses
c [ternres-2] 247622 schedulable variables 67%
c [ternres-2] 20299 ternary resolvents (0 bin, 20299 trn)
c [ternres-2] 90683 variables remain 24% (279607 retained)
c [card-3] limit 1704980 based on 6819921 irredundant clauses
c [card-3] found 8852 at-most-one constraints of average size 3.0
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 1704980 for elimination
c [card-3] 8852 out of 8852 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [decomp-10] removed 161 variables
c [basicprobe-2] limit 13638698 based on 6819349 irredundant clauses
c [basicprobe-2-0] 342400 probes remain 93% after last round
c [basicprobe-2-0] 13 units = 13 failed (100%) + 0 lifted (0%)
c [basicprobe-2-0] removed 13 variables, found 6465 hbrs
c [lift-2] limit 2225857 with penalty 3 = 0 + 3
c [lift-2] using 84646 probes 23%
c [lift-2] 1 units, 4 impls, 0 eqs in 1 rounds
c [lift-2] 370103 variables remain 100% (12 retained)
c [lift-2] removed 1 variables
c [cliff-2] limit of 13638100 steps based on 6819050 irredundant clauses
c [cliff-2] failed 0, lifted 78
c [unhide-6] limit 3409525 based on 6819050 irredundant clauses
c [unhide-6-6] 1705 units, 120 failed, 3393 tauts, 0 hbrs, 85422 literals
c [transred-2] limit 6814822 based on 6814822 irredundant clauses
c [transred-2] removed 3 transitive binary clauses
c [block-2] scheduling all variables this time
c [block-2] scheduled 367376 variables 100%
c [block-2] limit of 37097627 steps penalty 3 = 0 + 3
c [block-2] incomplete 13879 not tried 4%
c [block-2] transition to [ all 1 rem 1 ] state
c [block-2] eliminated 1442 blocked clauses
c [block-2] 1442 < 1/1000 * 6814822 = 6814 considered unsuccessful
c [elim-6] 367290 variables 100% will be scheduled this time
c [elim-6] scheduled 367290 variables 100%
c [elim-6] limit of 74195254 steps penalty 3 = 0 + 3
c [elim-6] incomplete 359586 not tried 98% in round 1
c [elim-6] transition to [ all 0 rem 1 ] state
c [elim-6] eliminated 7705 = 2% variables out of 367290
c [bca-2] limit of 10000000 steps
c [bca-2] 696663 out of 719172 literals actually usable 97%
c [bca-2] added 1196 blocked clauses in 2077948 steps
c [phase-6] phase bias: 0 positive 0%, 0 negative 0%
c [simplification-6] removed 10705 variables 2.9% (359585 remain 75%)
c [simplification-6] removed 48967 irredundant clauses 0.7% (6770954 remain 70%)
c [simplification-6] maximum reduction of 3% = max (3%, 1%)
c [simplification-6] geometric conflict interval increment 5000 = 20000 / 4
c [simplification-6] new conflict interval 25000
c [simplification-6] penalized conflict interval 50000 = 2 * 25000
c [simplification-6] new conflict limit 123340
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i  316.7  359584  6770936     77897   15637  36810 134749   0 31.3 4452.4  256
c i  317.1  359583  6770932     78334   15997  36810 134750   0 31.2 4447.6  256
c i  317.1  359582  6770932     78354   16008  36810 134750   0 31.2 4447.6  256
c -  317.9  359582  6770932     78553    8667  36818 134773   0 31.1 4438.1  253
c i  326.0  359581  6770928     87939   16921  36868 134834   0 30.3 4264.6  257
c -  327.1  359581  6770928     88634    9496  36870 134845   1 30.2 4242.6  253
c -  343.4  359581  6770927     99235   10221  36954 135027   0 29.8 3960.4  252
c -  362.6  359581  6770927    110091   10946  37014 135126   2 30.4 3718.3  252
c -  365.5  359581  6770927    121992   11763  37033 135148   1 32.0 3656.4  253
c 
c [simplification-7] limit of 124178 conflicts hit after 124178 conflicts
c [ternres-3] limit 27083708 based on 6770927 irredundant clauses
c [ternres-3] 88107 schedulable variables 25%
c [ternres-3] 11686 ternary resolvents (0 bin, 11686 trn)
c [ternres-3] 453 variables remain 0% (359128 retained)
c [gauss-2] limit 3385463 based on 6770927 irredundant clauses
c [gauss-2] extracted 37 xors of average arity 2.0
c [gauss-2] connected 75 occurrences of 73 variables (average 1.0)
c [gauss-2] limit 3385065 based on 6770131 irredundant clauses
c [gauss-2] fully completed
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-11] removed 167 variables
c [cgrclsr-2] limit 3384966 based on 6769933 irredundant clauses
c [cgrclsr-2] 294415 schedulable variables 82%
c [cgrclsr-2] 225525 variables remain 63% (133889 retained)
c [lift-3] limit 2500000 with penalty 3 = 0 + 3
c [lift-3] using 83340 probes 23%
c [lift-3] 19 units, 0 impls, 0 eqs in 1 rounds
c [lift-3] 359382 variables remain 100% (13 retained)
c [lift-3] removed 19 variables
c [cliff-3] limit of 13539516 steps based on 6769758 irredundant clauses
c [cliff-3] failed 5, lifted 774
c [unhide-7] limit 3384879 based on 6769758 irredundant clauses
c [unhide-7-7] 7 units, 20 failed, 40987 tauts, 0 hbrs, 23815 literals
c [transred-3] limit 6671254 based on 6671254 irredundant clauses
c [transred-3] removed 0 transitive binary clauses
c [cce-2] limit of 5309149 steps penalty 4 = 1 + 3
c [cce-2-1] incomplete large round (ABCE)
c [cce-2-1] allowing another 2654575 steps for small clauses
c [cce-2] scheduling 6326211 clauses = 6217957 binary + 108254 ternary
c [cce-2] tried to eliminate 18 small clauses 0%
c [cce-2] eliminated 5 small clauses 0%
c [cce-2] eliminated 5 binary clauses 0%
c [cce-2-1] eliminated 318 small clauses in 5309150 steps
c [cce-2-1] incomplete small round (ABCE)
c [cce-2-1] eliminated 318 covered clauses in round 1
c [cce-2] eliminated 318 covered clauses in TOTAL during 1 rounds
c [cce-2] 318 < 1/1000 * 6671254 = 6671 considered unsuccessful
c [elim-7] scheduling all variables this time
c [elim-7] scheduled 358003 variables 100%
c [elim-7] limit of 100000000 steps penalty 3 = 0 + 3
c [elim-7] incomplete 342635 not tried 96% in round 1
c [elim-7] transition to [ all 1 rem 1 ] state
c [elim-7] eliminated 15338 = 4% variables out of 358003
c [bca-3] limit of 10000000 steps
c [bca-3] 664321 out of 685332 literals actually usable 97%
c [bca-3] added 12108 blocked clauses in 2192989 steps
c [rephase-3] after 124178 conflicts (new increment 80000, next 204178)
c [flushphases] 465 phases reset
c [phase-7] phase bias: 0 positive 0%, 0 negative 0%
c [simplification-7] removed 16916 variables 4.7% (342665 remain 71%)
c [simplification-7] removed 123548 irredundant clauses 1.8% (6647379 remain 69%)
c [simplification-7] maximum reduction of 5% = max (5%, 2%)
c [simplification-7] large reduction 5% >= 5% limit
c [simplification-7] new conflict interval 2000 = 2000/1
c [simplification-7] penalized conflict interval 4000 = 2 * 2000
c [simplification-7] new conflict limit 128178
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c R  389.1  342665  6647379    128057   15842  38729 99649   1 33.7 3625.2  256
c 
c [simplification-8] limit of 128182 conflicts hit after 128182 conflicts
c [ternres-4] limit 26589508 based on 6647377 irredundant clauses
c [ternres-4] 450 schedulable variables 0%
c [ternres-4] 681 ternary resolvents (0 bin, 681 trn)
c [ternres-4] 1 variables remain 0% (342664 retained)
c [decomp-12] removed 22 variables
c [lift-4] limit 2500000 with penalty 3 = 0 + 3
c [lift-4] using 75758 probes 22%
c [lift-4] 848 units, 3 impls, 0 eqs in 1 rounds
c [lift-4] 341777 variables remain 100% (18 retained)
c [lift-4] removed 848 variables
c [cliff-4] limit of 13276274 steps based on 6638137 irredundant clauses
c [cliff-4] failed 0, lifted 41
c [unhide-8] limit 3319068 based on 6638137 irredundant clauses
c [unhide-8-8] 13126 units, 46 failed, 1120 tauts, 0 hbrs, 213876 literals
c [block-3] 13747 variables 4% will be scheduled this time
c [block-3] scheduled 13747 variables 4%
c [block-3] limit of 26713558 steps penalty 4 = 1 + 3
c [block-3] incomplete 142 not tried 0%
c [block-3] transition to [ all 0 rem 1 ] state
c [block-3] eliminated 855 blocked clauses
c [block-3] 855 < 1/1000 * 6607451 = 6607 considered unsuccessful
c [elim-8] 328521 variables 100% will be scheduled this time
c [elim-8] scheduled 328521 variables 100%
c [elim-8] limit of 100000000 steps penalty 3 = 0 + 3
c [elim-8] incomplete 312552 not tried 95% in round 1
c [elim-8] transition to [ all 0 rem 1 ] state
c [elim-8] eliminated 14834 = 5% variables out of 328552
c [bca-4] limit of 10000000 steps
c [bca-4] 605665 out of 627438 literals actually usable 97%
c [bca-4] added 779 blocked clauses in 2040950 steps
c [phase-8] phase bias: 0 positive 0%, 0 negative 0%
c [simplification-8] removed 28947 variables 8.4% (313718 remain 65%)
c [simplification-8] removed 383144 irredundant clauses 5.8% (6264233 remain 65%)
c [simplification-8] maximum reduction of 8% = max (8%, 6%)
c [simplification-8] large reduction 8% >= 5% limit
c [simplification-8] new conflict interval 2000 = 2000/1
c [simplification-8] penalized conflict interval 4000 = 2 * 2000
c [simplification-8] new conflict limit 132182
c 
c [simplification-9] limit of 132258 conflicts hit after 132259 conflicts
c [ternres-5] limit 25056932 based on 6264233 irredundant clauses
c [ternres-5] 1 schedulable variables 0%
c [ternres-5] 76 ternary resolvents (0 bin, 76 trn)
c [ternres-5] fully completed ternary resolution
c [decomp-13] removed 56 variables
c [simpleprobe-3] 299911 schedulable variables 96%
c [simpleprobe-3] limit 5572021 penalty 5 = 2 + 3
c [decomp-14] removed 2 variables
c [simpleprobe-3] 300018 variables remain 96% (13642 retained)
c [simpleprobe-3] removed 2 variables, found 2288 hbrs, 2 units
c [lift-5] limit 2500000 with penalty 3 = 0 + 3
c [lift-5] using 65797 probes 21%
c [lift-5] 0 units, 0 impls, 0 eqs in 1 rounds
c [lift-5] 313644 variables remain 100% (16 retained)
c [cliff-5] limit of 12528152 steps based on 6264076 irredundant clauses
c [cliff-5] failed 0, lifted 0
c [unhide-9] limit 3132038 based on 6264076 irredundant clauses
c [unhide-9-9] 7 units, 9 failed, 19603 tauts, 0 hbrs, 37702 literals
c [transred-4] limit 6244450 based on 6244450 irredundant clauses
c [transred-4] removed 1 transitive binary clauses
c [transred-4] found 1 units
c [elim-9] scheduling all variables this time
c [elim-9] scheduled 313639 variables 100%
c [elim-9] limit of 100000000 steps penalty 3 = 0 + 3
c [elim-9] incomplete 287952 not tried 92% in round 1
c [elim-9] transition to [ all 1 rem 1 ] state
c [elim-9] eliminated 15291 = 5% variables out of 313639
c [bca-5] limit of 10000000 steps
c [bca-5] 574028 out of 596698 literals actually usable 96%
c [bca-5] added 2182 blocked clauses in 1975239 steps
c [phase-9] phase bias: 0 positive 0%, 0 negative 0%
c [simplification-9] removed 15370 variables 4.9% (298348 remain 62%)
c [simplification-9] removed 50506 irredundant clauses 0.8% (6213727 remain 64%)
c [simplification-9] maximum reduction of 5% = max (5%, 1%)
c [simplification-9] large reduction 5% >= 5% limit
c [simplification-9] new conflict interval 2000 = 2000/1
c [simplification-9] penalized conflict interval 4000 = 2 * 2000
c [simplification-9] new conflict limit 136259
c 
c [simplification-10] limit of 136277 conflicts hit after 136278 conflicts
c [ternres-6] limit 24854908 based on 6213727 irredundant clauses
c [ternres-6] all 298348 free variables schedulable
c [ternres-6] 4617 ternary resolvents (0 bin, 4617 trn)
c [ternres-6] 195791 variables remain 66% (102557 retained)
c [card-4] limit 1553431 based on 6213727 irredundant clauses
c [card-4] found 7025 at-most-one constraints of average size 3.0
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 1553431 for elimination
c [card-4] 7025 out of 7025 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [gauss-3] limit 3106863 based on 6213727 irredundant clauses
c [gauss-3] extracted 2 xors of average arity 2.0
c [gauss-3] connected 4 occurrences of 2 variables (average 2.0)
c [gauss-3] limit 3106863 based on 6213727 irredundant clauses
c [gauss-3] fully completed
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-15] removed 15 variables
c [cgrclsr-3] limit 3106850 based on 6213701 irredundant clauses
c [cgrclsr-3] 187117 schedulable variables 63%
c [cgrclsr-3] 99250 variables remain 33% (199081 retained)
c [cgrclsr-3] removed 2 variables
c [unhide-10] limit 3106847 based on 6213695 irredundant clauses
c [unhide-10-10] 1257 units, 6 failed, 1061 tauts, 0 hbrs, 94388 literals
c [transred-5] limit 6210950 based on 6210950 irredundant clauses
c [transred-5] removed 2 transitive binary clauses
c [transred-5] found 1 units
c [cce-3] limit of 3105475 steps based on 6210950 irredundant clauses
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 181
c [cce-3-1] eliminated 1 clauses out of 2 (50%) of length 179
c [cce-3-1] eliminated 2 clauses out of 6 (33%) of length 178
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 4 large clauses in 3105476 steps
c [cce-3-1] allowing another 1552738 steps for small clauses
c [cce-3] scheduling 5711167 clauses = 5692120 binary + 19047 ternary
c [cce-3] tried to eliminate 3 small clauses 0%
c [cce-3-1] eliminated 17225 small clauses in 3105476 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 17229 covered clauses in round 1
c [cce-3] eliminated 17229 covered clauses in TOTAL during 1 rounds
c [elim-10] 285603 variables 96% will be scheduled this time
c [elim-10] scheduled 285603 variables 96%
c [elim-10] limit of 100000000 steps penalty 3 = 0 + 3
c [elim-10] incomplete 254545 not tried 86% in round 1
c [elim-10] transition to [ all 0 rem 1 ] state
c [elim-10] eliminated 11849 = 4% variables out of 297069
c [bca-6] limit of 10000000 steps
c [bca-6] 547374 out of 570442 literals actually usable 96%
c [bca-6] added 37731 blocked clauses in 2027848 steps
c [phase-10] phase bias: 0 positive 0%, 0 negative 0%
c [simplification-10] removed 13128 variables 4.4% (285220 remain 59%)
c [simplification-10] removed 42303 irredundant clauses 0.7% (6171424 remain 64%)
c [simplification-10] maximum reduction of 4% = max (4%, 1%)
c [simplification-10] geometric conflict interval increment 5000 = 25000 / 5
c [simplification-10] new conflict interval 30000
c [simplification-10] penalized conflict interval 60000 = 2 * 30000
c [simplification-10] new conflict limit 196278
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  473.0  285220  6171424    144429   11683  17944 111532   0 34.0 3336.6  243
c i  475.3  285219  6171424    146281   13207  17954 111552   0 34.1 3318.5  244
c -  487.7  285219  6171424    157352   12710  18017 111601   1 33.7 3205.8  244
c -  507.3  285219  6171424    170724   13533  18104 111679   0 34.0 3028.5  243
c i  508.3  285218  6171424    171217   13993  18106 111679   0 34.0 3023.2  245
c -  517.9  285218  6171424    186197   14458  18164 111756   1 35.0 2936.8  243
c 
c [simplification-11] limit of 197020 conflicts hit after 197021 conflicts
c [ternres-7] limit 24685696 based on 6171424 irredundant clauses
c [ternres-7] 186839 schedulable variables 66%
c [ternres-7] 13401 ternary resolvents (1 bin, 13400 trn)
c [ternres-7] 4318 variables remain 2% (280900 retained)
c [decomp-16] removed 86 variables
c [lift-6] limit 1542771 based on 6171087 irredundant clauses
c [lift-6] using 55812 probes 20%
c [lift-6] 0 units, 2 impls, 0 eqs in 1 rounds
c [lift-6] 285115 variables remain 100% (19 retained)
c [cliff-6] limit of 12342174 steps based on 6171087 irredundant clauses
c [cliff-6] failed 1, lifted 26
c [unhide-11] limit 3085543 based on 6171087 irredundant clauses
c [unhide-11-11] 8301 units, 13 failed, 48539 tauts, 0 hbrs, 199699 literals
c [transred-6] limit 6076688 based on 6076688 irredundant clauses
c [transred-6] removed 4 transitive binary clauses
c [transred-6] found 3 units
c [block-4] scheduling all variables this time
c [block-4] scheduled 269256 variables 100%
c [block-4] limit of 19530783 steps penalty 5 = 2 + 3
c [block-4] incomplete 77948 not tried 29%
c [block-4] transition to [ all 1 rem 1 ] state
c [block-4] eliminated 19650 blocked clauses
c [elim-11] scheduling all variables this time
c [elim-11] scheduled 268782 variables 100%
c [elim-11] limit of 100000000 steps penalty 3 = 0 + 3
c [elim-11] incomplete 205261 not tried 76% in round 1
c [elim-11] transition to [ all 1 rem 1 ] state
c [elim-11] eliminated 9151 = 3% variables out of 268782
c [bca-7] limit of 10000000 steps
c [bca-7] 486982 out of 519264 literals actually usable 94%
c [bca-7] added 191415 blocked clauses in 2193505 steps
c [phase-11] phase bias: 0 positive 0%, 1 negative 100%
c [simplification-11] removed 25587 variables 9.0% (259631 remain 54%)
c [simplification-11] removed 364316 irredundant clauses 5.9% (5807108 remain 60%)
c [simplification-11] maximum reduction of 9% = max (9%, 6%)
c [simplification-11] large reduction 9% >= 5% limit
c [simplification-11] new conflict interval 2000 = 2000/1
c [simplification-11] penalized conflict interval 4000 = 2 * 2000
c [simplification-11] new conflict limit 201021
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  559.6  259631  5807108    201060   14863  23675 311787   0 34.7 2791.0  238
c 
c [simplification-12] limit of 201075 conflicts hit after 201076 conflicts
c [ternres-8] limit 23228432 based on 5807108 irredundant clauses
c [ternres-8] 4119 schedulable variables 2%
c [ternres-8] 13365 ternary resolvents (0 bin, 13365 trn)
c [ternres-8] 577 variables remain 0% (259054 retained)
c [decomp-17] removed 348 variables
c [treelook-3] limit 1451510 based on 5806043 irredundant clauses
c [treelook-3] scheduled 218455 literals 42%
c [treelook-3] scheduling used 1451528 steps
c [treelook-3] not fully scheduled
c [treelook-3] limit 1451510 based on 5806043 irredundant clauses
c [treelook-3] used 7254319 steps
c [treelook-3] 218452 literals remain 42%
c [treelook-3] 160511 variables remain to probed next time 62%
c [treelook-3] removed 2 variables, found 218 hbrs
c [cgrclsr-4] limit 2899995 based on 5799991 irredundant clauses
c [cgrclsr-4] 86242 schedulable variables 33%
c [cgrclsr-4] fully completed congruence closure
c [cgrclsr-4] removed 1 variables
c [cliff-7] limit of 11599934 steps based on 5799967 irredundant clauses
c [cliff-7] failed 0, lifted 0
c [unhide-12] limit 2899983 based on 5799967 irredundant clauses
c [unhide-12-12] 5923 units, 34 failed, 1757 tauts, 0 hbrs, 49717 literals
c [transred-7] limit 5785451 based on 5785451 irredundant clauses
c [transred-7] removed 5 transitive binary clauses
c [transred-7] found 5 units
c [cce-4] limit of 7926820 steps penalty 4 = 1 + 3
c [cce-4-1] eliminated 1 clauses out of 1 (100%) of length 182
c [cce-4-1] eliminated 4 clauses out of 4 (100%) of length 178
c [cce-4-1] eliminated 18 clauses out of 19 (95%) of length 177
c [cce-4-1] eliminated 6 clauses out of 9 (67%) of length 176
c [cce-4-1] eliminated 16 clauses out of 37 (43%) of length 175
c [cce-4-1] incomplete large round (ACCE)
c [cce-4-1] eliminated 45 large clauses in 7926821 steps
c [cce-4-1] allowing another 3963410 steps for small clauses
c [cce-4] scheduling 5174480 clauses = 5062533 binary + 111947 ternary
c [cce-4] tried to eliminate 4 small clauses 0%
c [cce-4] eliminated 1 small clauses 0%
c [cce-4] eliminated 1 binary clauses 0%
c [cce-4-1] eliminated 192417 small clauses in 7926821 steps
c [cce-4-1] incomplete small round (ACCE)
c [cce-4-1] eliminated 192462 covered clauses in round 1
c [cce-4] eliminated 192462 covered clauses in TOTAL during 1 rounds
c [elim-12] 193690 variables 78% will be scheduled this time
c [elim-12] scheduled 193690 variables 78%
c [elim-12] limit of 100000000 steps penalty 3 = 0 + 3
c [elim-12] incomplete 159112 not tried 64% in round 1
c [elim-12] transition to [ all 0 rem 1 ] state
c [elim-12] eliminated 6174 = 2% variables out of 247865
c [bca-8] limit of 10000000 steps
c [bca-8] 462368 out of 483384 literals actually usable 96%
c [bca-8] added 5506 blocked clauses in 2053007 steps
c [phase-12] phase bias: 0 positive 0%, 0 negative 0%
c [simplification-12] removed 17940 variables 6.9% (241691 remain 50%)
c [simplification-12] removed 230287 irredundant clauses 4.0% (5576821 remain 58%)
c [simplification-12] maximum reduction of 7% = max (7%, 4%)
c [simplification-12] large reduction 7% >= 5% limit
c [simplification-12] new conflict interval 2010 = min (201076/100, 30000)
c [simplification-12] penalized conflict interval 4020 = 2 * 2010
c [simplification-12] new conflict limit 205096
c 
c [simplification-13] limit of 205140 conflicts hit after 205141 conflicts
c [ternres-9] limit 22307284 based on 5576821 irredundant clauses
c [ternres-9] 543 schedulable variables 0%
c [ternres-9] 4780 ternary resolvents (0 bin, 4780 trn)
c [ternres-9] 118 variables remain 0% (241573 retained)
c [decomp-19] removed 26 variables
c [basicprobe-3] limit 11153522 based on 5576761 irredundant clauses
c [basicprobe-3-0] 226234 probes remain 94% after last round
c [basicprobe-3-0] 23 units = 23 failed (100%) + 0 lifted (0%)
c [basicprobe-3-0] removed 1808 variables, found 4070 hbrs
c [cgrclsr-5] limit 2776441 based on 5552882 irredundant clauses
c [cgrclsr-5] all 239857 free variables schedulable
c [cgrclsr-5] 151440 variables remain 63% (88416 retained)
c [cgrclsr-5] removed 1 variables
c [unhide-13] limit 2776441 based on 5552882 irredundant clauses
c [unhide-13-13] 5537 units, 12 failed, 33272 tauts, 0 hbrs, 70754 literals
c [transred-8] limit 5505402 based on 5505402 irredundant clauses
c [transred-8] removed 13 transitive binary clauses
c [transred-8] found 2 units
c [block-5] 127 variables 0% will be scheduled this time
c [block-5] scheduled 127 variables 0%
c [block-5] limit of 40290813 steps penalty 4 = 1 + 3
c [block-5] fully completed
c [block-5] transition to [ all 0 rem 0 ] state
c [block-5] eliminated 1 blocked clauses
c [block-5] 1 < 1/1000 * 5505401 = 5505 considered unsuccessful
c [cce-5] limit of 16116325 steps penalty 3 = 0 + 3
c [cce-5-1] eliminated 20 clauses out of 21 (95%) of length 174
c [cce-5-1] eliminated 1 clauses out of 1 (100%) of length 172
c [cce-5-1] eliminated 1 clauses out of 1 (100%) of length 170
c [cce-5-1] incomplete large round (ACCE)
c [cce-5-1] eliminated 22 large clauses in 16116326 steps
c [cce-5-1] allowing another 8058163 steps for small clauses
c [cce-5] scheduling 4907033 clauses = 4809620 binary + 97413 ternary
c [cce-5] tried to eliminate 28 small clauses 0%
c [cce-5] eliminated 4 small clauses 0%
c [cce-5] eliminated 4 binary clauses 0%
c [cce-5-1] eliminated 4 small clauses in 16116326 steps
c [cce-5-1] incomplete small round (ACCE)
c [cce-5-1] eliminated 26 covered clauses in round 1
c [cce-5] eliminated 26 covered clauses in TOTAL during 1 rounds
c [cce-5] 26 < 1/1000 * 5352963 = 5352 considered unsuccessful
c [elim-13] scheduling all variables this time
c [elim-13] scheduled 229925 variables 100%
c [elim-13] limit of 100000000 steps penalty 3 = 0 + 3
c [elim-13] incomplete 135383 not tried 59% in round 1
c [elim-13] transition to [ all 1 rem 1 ] state
c [elim-13] eliminated 5142 = 2% variables out of 229925
c [bca-9] limit of 10000000 steps
c [bca-9] 420356 out of 449568 literals actually usable 94%
c [bca-9] added 6757 blocked clauses in 1833535 steps
c [rephase-4] after 205141 conflicts (new increment 160000, next 365141)
c [flushphases] 116 phases reset
c [phase-13] phase bias: 0 positive 0%, 0 negative 0%
c [simplification-13] removed 16908 variables 7.0% (224783 remain 47%)
c [simplification-13] removed 241014 irredundant clauses 4.3% (5335807 remain 55%)
c [simplification-13] maximum reduction of 7% = max (7%, 4%)
c [simplification-13] large reduction 7% >= 5% limit
c [simplification-13] new conflict interval 2051 = min (205141/100, 30000)
c [simplification-13] penalized conflict interval 4102 = 2 * 2051
c [simplification-13] new conflict limit 209243
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i  608.7  224782  5335807    207861   20655  24924 230040   0 34.5 2785.8  227
c 
c [simplification-14] limit of 209337 conflicts hit after 209337 conflicts
c [ternres-10] limit 21343228 based on 5335807 irredundant clauses
c [ternres-10] 111 schedulable variables 0%
c [ternres-10] 1669 ternary resolvents (0 bin, 1669 trn)
c [ternres-10] 13 variables remain 0% (224769 retained)
c [gauss-4] limit 2667903 based on 5335807 irredundant clauses
c [gauss-4] extracted 5 xors of average arity 2.0
c [gauss-4] connected 10 occurrences of 8 variables (average 1.2)
c [gauss-4] limit 2667882 based on 5335765 irredundant clauses
c [gauss-4] fully completed
c [gauss-4] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-20] removed 69 variables
c [cgrclsr-6] limit 2667471 based on 5334942 irredundant clauses
c [cgrclsr-6] 141850 schedulable variables 63%
c [cgrclsr-6] 47541 variables remain 21% (177154 retained)
c [cgrclsr-6] removed 18 variables
c [lift-7] limit 1333679 based on 5334716 irredundant clauses
c [lift-7] using 51704 probes 23%
c [lift-7] 0 units, 0 impls, 0 eqs in 1 rounds
c [lift-7] 224675 variables remain 100% (20 retained)
c [cliff-8] limit of 10669432 steps based on 5334716 irredundant clauses
c [cliff-8] failed 5, lifted 0
c [unhide-14] limit 2667358 based on 5334716 irredundant clauses
c [unhide-14-14] 3071 units, 26 failed, 2498 tauts, 0 hbrs, 94019 literals
c [transred-9] limit 5285521 based on 5285521 irredundant clauses
c [transred-9] removed 9 transitive binary clauses
c [transred-9] found 1 units
c [elim-14] 128909 variables 61% will be scheduled this time
c [elim-14] scheduled 128909 variables 61%
c [elim-14] limit of 100000000 steps penalty 3 = 0 + 3
c [elim-14] incomplete 105326 not tried 49% in round 1
c [elim-14] transition to [ all 0 rem 1 ] state
c [elim-14] eliminated 4320 = 2% variables out of 212850
c [bca-10] limit of 10000000 steps
c [bca-10] 389457 out of 417062 literals actually usable 93%
c [bca-10] added 3485 blocked clauses in 1754846 steps
c [phase-14] phase bias: 0 positive 0%, 0 negative 0%
c [simplification-14] removed 16252 variables 7.2% (208530 remain 43%)
c [simplification-14] removed 262730 irredundant clauses 4.9% (5073077 remain 52%)
c [simplification-14] maximum reduction of 7% = max (7%, 5%)
c [simplification-14] large reduction 7% >= 5% limit
c [simplification-14] new conflict interval 2093 = min (209337/100, 30000)
c [simplification-14] penalized conflict interval 4186 = 2 * 2093
c [simplification-14] new conflict limit 213523
c 
c [simplification-15] limit of 213535 conflicts hit after 213535 conflicts
c [ternres-11] limit 20292308 based on 5073077 irredundant clauses
c [ternres-11] 10 schedulable variables 0%
c [ternres-11] 308 ternary resolvents (0 bin, 308 trn)
c [ternres-11] fully completed ternary resolution
c [card-5] limit 1268269 based on 5073077 irredundant clauses
c [card-5] found 3483 at-most-one constraints of average size 3.5
c [card-5] no at-most-two constraint found
c [card-5] using previous limit 1268269 for elimination
c [card-5] 3483 out of 3483 constraints (100%) meet size limits
c [card-5] no units found
c [card-5] no at-most-one constraints generated
c [decomp-21] removed 139 variables
c [simpleprobe-4] 199382 schedulable variables 96%
c [simpleprobe-4] limit 12500000 penalty 4 = 1 + 3
c [decomp-22] removed 2 variables
c [simpleprobe-4] 199473 variables remain 96% (8916 retained)
c [simpleprobe-4] removed 2 variables, found 1687 hbrs, 0 units
c [cgrclsr-7] limit 2535461 based on 5070923 irredundant clauses
c [cgrclsr-7] 44206 schedulable variables 21%
c [cgrclsr-7] fully completed congruence closure
c [cliff-9] limit of 10141846 steps based on 5070923 irredundant clauses
c [cliff-9] failed 0, lifted 0
c [unhide-15] limit 2535461 based on 5070923 irredundant clauses
c [unhide-15-15] 9 units, 3 failed, 19004 tauts, 0 hbrs, 56210 literals
c [transred-10] limit 5052252 based on 5052252 irredundant clauses
c [transred-10] removed 10 transitive binary clauses
c [transred-10] found 1 units
c [cce-6] limit of 8276183 steps penalty 4 = 1 + 3
c [cce-6-1] eliminated 1 clauses out of 1 (100%) of length 162
c [cce-6-1] incomplete large round (ACCE)
c [cce-6-1] eliminated 1 large clauses in 8276184 steps
c [cce-6-1] allowing another 4138092 steps for small clauses
c [cce-6] scheduling 4602199 clauses = 4514211 binary + 87988 ternary
c [cce-6] tried to eliminate 43 small clauses 0%
c [cce-6] eliminated 19 small clauses 0%
c [cce-6] eliminated 19 binary clauses 0%
c [cce-6-1] eliminated 204 small clauses in 8276184 steps
c [cce-6-1] incomplete small round (ACCE)
c [cce-6-1] eliminated 205 covered clauses in round 1
c [cce-6] eliminated 205 covered clauses in TOTAL during 1 rounds
c [cce-6] 205 < 1/1000 * 5052251 = 5052 considered unsuccessful
c [elim-15] scheduling all variables this time
c [elim-15] scheduled 208377 variables 100%
c [elim-15] limit of 100000000 steps penalty 3 = 0 + 3
c [elim-15] incomplete 100113 not tried 48% in round 1
c [elim-15] transition to [ all 1 rem 1 ] state
c [elim-15] eliminated 5983 = 3% variables out of 208377
c [bca-11] limit of 10000000 steps
c [bca-11] 377589 out of 404790 literals actually usable 93%
c [bca-11] added 816 blocked clauses in 1725946 steps
c [phase-15] phase bias: 0 positive 0%, 0 negative 0%
c [simplification-15] removed 6136 variables 2.9% (202394 remain 42%)
c [simplification-15] removed 43802 irredundant clauses 0.9% (5029275 remain 52%)
c [simplification-15] maximum reduction of 3% = max (3%, 1%)
c [simplification-15] geometric conflict interval increment 7500 = 30000 / 4
c [simplification-15] new conflict interval 37500
c [simplification-15] penalized conflict interval 75000 = 2 * 37500
c [simplification-15] new conflict limit 288535
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  654.2  202394  5029275    220128   14925  21368 174459   0 34.6 2706.9  214
c -  670.3  202394  5029275    236184   15870  21497 174604   0 34.3 2596.4  214
c -  677.3  202394  5029275    251579   16887  21556 174645   0 35.0 2621.0  212
c -  687.7  202394  5029275    267292   17599  21685 174677   1 35.9 2615.4  213
c R  694.5  202394  5029275    277024   26790  21756 174698   1 36.7 2626.4  225
c -  703.9  202394  5029275    283627   18178  21835 174770   0 36.5 2596.2  213
c 
c [simplification-16] limit of 289235 conflicts hit after 289241 conflicts
c [ternres-12] limit 20117100 based on 5029275 irredundant clauses
c [ternres-12] all 202394 free variables schedulable
c [ternres-12] 21736 ternary resolvents (0 bin, 21736 trn)
c [ternres-12] 158948 variables remain 79% (43446 retained)
c [decomp-23] removed 26 variables
c [unhide-16] limit 2514034 based on 5028068 irredundant clauses
c [unhide-16-16] 177 units, 24 failed, 1343 tauts, 0 hbrs, 73326 literals
c [transred-11] limit 5019396 based on 5019396 irredundant clauses
c [transred-11] removed 13 transitive binary clauses
c [transred-11] found 2 units
c [block-6] scheduling all variables this time
c [block-6] scheduled 200820 variables 100%
c [block-6] limit of 25000000 steps penalty 5 = 2 + 3
c [block-6] incomplete 59459 not tried 30%
c [block-6] transition to [ all 1 rem 1 ] state
c [block-6] eliminated 105498 blocked clauses
c [elim-16] 97420 variables 49% will be scheduled this time
c [elim-16] scheduled 97420 variables 49%
c [elim-16] limit of 200000000 steps penalty 2 = 0 + 2
c [elim-16] incomplete 76579 not tried 39% in round 1
c [elim-16] transition to [ all 0 rem 1 ] state
c [elim-16] eliminated 2434 = 1% variables out of 198214
c [bca-12] limit of 10000000 steps
c [bca-12] 354101 out of 391562 literals actually usable 90%
c [bca-12] added 18331 blocked clauses in 1521441 steps
c [phase-16] phase bias: 0 positive 0%, 0 negative 0%
c [simplification-16] removed 6614 variables 3.3% (195780 remain 41%)
c [simplification-16] removed 153910 irredundant clauses 3.1% (4875365 remain 50%)
c [simplification-16] maximum reduction of 3% = max (3%, 3%)
c [simplification-16] geometric conflict interval increment 9375 = 37500 / 4
c [simplification-16] new conflict interval 46875
c [simplification-16] penalized conflict interval 93750 = 2 * 46875
c [simplification-16] new conflict limit 382991
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  740.1  195780  4875365    302474   18705  42415 182928   1 36.0 2557.3  213
c -  758.2  195780  4875365    320952   19518  42519 183081   1 35.7 2485.7  213
c i  760.1  195779  4875365    322689   21106  42552 183099   0 35.7 2476.1  214
c -  771.9  194316  4875365    339498   20348  42633 183210   1 35.3 2431.8  213
c -  788.3  194316  4875365    359988   21298  42737 183390   1 34.7 2376.5  213
c -  807.6  194316  4875365    379514   22065  42867 183475   1 34.8 2341.7  213
c 
c [simplification-17] limit of 384225 conflicts hit after 384225 conflicts
c [ternres-13] limit 25201234 with penalty 2 = 0 + 2
c [ternres-13] 152633 schedulable variables 78%
c [ternres-13] 34607 ternary resolvents (0 bin, 34607 trn)
c [ternres-13] 43600 variables remain 22% (150716 retained)
c [decomp-24] removed 2222 variables
c [treelook-4] limit 1207797 based on 4831188 irredundant clauses
c [treelook-4] scheduled 156535 literals 40%
c [treelook-4] scheduling used 1207974 steps
c [treelook-4] not fully scheduled
c [treelook-4] limit 1207797 based on 4831188 irredundant clauses
c [treelook-4] used 2322684 steps
c [treelook-4] 156215 literals remain 40%
c [treelook-4] 106373 variables remain to probed next time 55%
c [decomp-25] removed 459 variables
c [treelook-4] removed 769 variables, found 36 hbrs
c [cgrclsr-8] limit 2408924 based on 4817849 irredundant clauses
c [cgrclsr-8] all 192789 free variables schedulable
c [cgrclsr-8] 117852 variables remain 61% (74937 retained)
c [cliff-10] limit of 10080493 steps penalty 3 = 1 + 2
c [cliff-10] failed 0, lifted 0
c [unhide-17] limit 5000000 with penalty 2 = 0 + 2
c [unhide-17-17] 241 units, 1 failed, 17884 tauts, 0 hbrs, 45092 literals
c [transred-12] limit 4800656 based on 4800656 irredundant clauses
c [transred-12] removed 0 transitive binary clauses
c [elim-17] scheduling all variables this time
c [elim-17] scheduled 192535 variables 100%
c [elim-17] limit of 200000000 steps penalty 2 = 0 + 2
c [elim-17] incomplete 75462 not tried 39% in round 1
c [elim-17] transition to [ all 1 rem 1 ] state
c [elim-17] eliminated 3289 = 2% variables out of 192535
c [bca-13] limit of 10000000 steps
c [bca-13] 342336 out of 378494 literals actually usable 90%
c [bca-13] added 4712 blocked clauses in 1455975 steps
c [rephase-5] after 384225 conflicts (new increment 320000, next 704225)
c [flushphases] 61 phases reset
c [phase-17] phase bias: 0 positive 0%, 0 negative 0%
c [simplification-17] removed 5070 variables 2.6% (189246 remain 39%)
c [simplification-17] removed 96677 irredundant clauses 2.0% (4778688 remain 49%)
c [simplification-17] maximum reduction of 3% = max (3%, 2%)
c [simplification-17] geometric conflict interval increment 11718 = 46875 / 4
c [simplification-17] new conflict interval 58593
c [simplification-17] penalized conflict interval 117186 = 2 * 58593
c [simplification-17] new conflict limit 501411
c [tabula-rasa-1] number clauses 4778688 drops below limit 4838192
c [flush-cache] 0 binary, 0 ternary, 25305 large
c [flushphases] 189246 phases reset fully
c [phase-18] phase bias: 1876 positive 12%, 13386 negative 88%
c [tabula-rasa-1] new conflict interval 20000
c [tabula-rasa-1] new conflict limit 404225
c [tabula-rasa-1] new variable limit 47311 and clause limit 2389344
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  834.7  189246  4778688    389137    2526  72711 169679   2 34.7 2324.1  210
c -  835.4  189246  4778688    392792    3297  72719 169683   1 34.7 2320.7  210
c -  836.1  189246  4778688    396858    3869  72721 169684   1 35.0 2316.6  210
c -  836.8  189246  4778688    402229    5005  72728 169691   1 35.1 2312.6  210
c 
c [simplification-18] limit of 404271 conflicts hit after 404273 conflicts
c [ternres-14] limit 25459106 with penalty 2 = 0 + 2
c [ternres-14] 42578 schedulable variables 22%
c [ternres-14] 19389 ternary resolvents (1 bin, 19388 trn)
c [ternres-14] 21929 variables remain 12% (167317 retained)
c [decomp-26] removed 20 variables
c [basicprobe-4] limit 25000000 penalty 2 = 0 + 2
c [basicprobe-4-0] 175483 probes remain 93% after last round
c [basicprobe-4-0] 31 units = 31 failed (100%) + 0 lifted (0%)
c [basicprobe-4-0] removed 537 variables, found 8197 hbrs
c [bate-1] eliminated 2 asymmetric tautologies during probing
c [lift-8] limit 1188649 based on 4754599 irredundant clauses
c [lift-8] using 52059 probes 28%
c [lift-8] 360 units, 4 impls, 0 eqs in 1 rounds
c [lift-8] 188301 variables remain 100% (28 retained)
c [lift-8] removed 360 variables
c [unhide-18] limit 5000000 with penalty 2 = 0 + 2
c [unhide-18-18] 590 units, 24 failed, 3772 tauts, 0 hbrs, 49836 literals
c [block-7] 58748 variables 31% will be scheduled this time
c [block-7] scheduled 58748 variables 31%
c [block-7] limit of 100000000 steps penalty 3 = 1 + 2
c [block-7] fully completed
c [block-7] transition to [ all 0 rem 0 ] state
c [block-7] eliminated 604284 blocked clauses
c [cce-7] limit of 12729553 steps penalty 4 = 2 + 2
c [cce-7-1] incomplete large round (ACCE)
c [cce-7-1] allowing another 6364777 steps for small clauses
c [cce-7] scheduling 3727367 clauses = 3646792 binary + 80575 ternary
c [cce-7] tried to eliminate 12 small clauses 0%
c [cce-7-1] incomplete small round (ACCE)
c [cce-7-1] eliminated 0 covered clauses in round 1
c [cce-7] eliminated 0 covered clauses in TOTAL during 1 rounds
c [elim-18] 67304 variables 37% will be scheduled this time
c [elim-18] scheduled 67304 variables 37%
c [elim-18] limit of 200000000 steps penalty 2 = 0 + 2
c [elim-18] incomplete 57198 not tried 32% in round 1
c [elim-18] transition to [ all 0 rem 1 ] state
c [elim-18] eliminated 3497 = 2% variables out of 179716
c [bca-14] limit of 10000000 steps
c [bca-14] 343207 out of 352440 literals actually usable 97%
c [bca-14] added 34254 blocked clauses in 1519948 steps
c [rephase-6] after 404273 conflicts (new increment 20000, next 424273)
c [flushphases] 17262 phases reset
c [phase-19] phase bias: 300 positive 78%, 83 negative 22%
c [simplification-18] removed 13027 variables 6.9% (176219 remain 37%)
c [simplification-18] removed 699499 irredundant clauses 14.6% (4079189 remain 42%)
c [simplification-18] maximum reduction of 15% = max (7%, 15%)
c [simplification-18] large reduction 15% >= 5% limit
c [simplification-18] new conflict interval 4042 = min (404273/100, 20000)
c [simplification-18] penalized conflict interval 8084 = 2 * 4042
c [simplification-18] new conflict limit 412357
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c i  868.3  176218  4079189    405454    7519  90045 220130   0 35.1 2309.7  202
c -  872.5  176218  4079189    408157    6061  90063 220148   0 35.1 2307.8  201
c 
c [simplification-19] limit of 412509 conflicts hit after 412519 conflicts
c [ternres-15] limit 26032549 with penalty 2 = 0 + 2
c [ternres-15] 20626 schedulable variables 12%
c [ternres-15] 24305 ternary resolvents (4 bin, 24301 trn)
c [ternres-15] 1622 variables remain 1% (174596 retained)
c [gauss-5] limit 2039593 based on 4079187 irredundant clauses
c [gauss-5] extracted 82 xors of average arity 2.0
c [gauss-5] connected 165 occurrences of 163 variables (average 1.0)
c [gauss-5] limit 2039573 based on 4079147 irredundant clauses
c [gauss-5] fully completed
c [gauss-5] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-27] removed 1383 variables
c [simpleprobe-5] 167397 schedulable variables 96%
c [simpleprobe-5] limit 50000000 penalty 2 = 0 + 2
c [decomp-28] removed 224 variables
c [simpleprobe-5] 160660 variables remain 92% (13951 retained)
c [simpleprobe-5] removed 224 variables, found 25054 hbrs, 221 units
c [unhide-19] limit 5000000 with penalty 2 = 0 + 2
c [unhide-19-19] 33 units, 4 failed, 15004 tauts, 0 hbrs, 35863 literals
c [transred-13] limit 4053014 based on 4053014 irredundant clauses
c [transred-13] removed 19 transitive binary clauses
c [transred-13] found 1 units
c [block-8] scheduling all variables this time
c [block-8] scheduled 174575 variables 100%
c [block-8] limit of 200000000 steps penalty 2 = 0 + 2
c [block-8] fully completed
c [block-8] transition to [ all 0 rem 0 ] state
c [block-8] eliminated 46132 blocked clauses
c [elim-19] scheduling all variables this time
c [elim-19] scheduled 173529 variables 100%
c [elim-19] limit of 200000000 steps penalty 2 = 0 + 2
c [elim-19] incomplete 55163 not tried 32% in round 1
c [elim-19] transition to [ all 1 rem 1 ] state
c [elim-19] eliminated 4650 = 3% variables out of 173529
c [bca-15] limit of 10000000 steps
c [bca-15] 318601 out of 337760 literals actually usable 94%
c [bca-15] added 14338 blocked clauses in 1408084 steps
c [phase-20] phase bias: 23 positive 74%, 8 negative 26%
c [simplification-19] removed 7339 variables 4.2% (168879 remain 35%)
c [simplification-19] removed 105477 irredundant clauses 2.6% (3973710 remain 41%)
c [simplification-19] maximum reduction of 4% = max (4%, 3%)
c [simplification-19] geometric conflict interval increment 4000 = 20000 / 5
c [simplification-19] new conflict interval 24000
c [simplification-19] penalized conflict interval 48000 = 2 * 24000
c [simplification-19] new conflict limit 460519
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  907.8  168879  3973710    413890    6691 108555 221679   0 35.0 2300.6  199
c -  913.5  168879  3973710    420072    7538 108606 221710   1 34.9 2292.6  200
c -  919.4  168879  3973710    426615    8115 108633 221727   0 34.8 2274.9  200
c -  923.3  168879  3973708    434251    8844 108686 221747   0 34.9 2261.5  200
c -  931.1  168879  3973708    441953    9548 108742 221765   0 34.8 2238.0  200
c -  938.4  168879  3973707    450761   10401 108833 221833   1 34.6 2215.7  200
c -  943.9  168879  3973707    460130   10972 108897 221879   1 34.7 2198.2  200
c 
c [simplification-20] limit of 460885 conflicts hit after 460888 conflicts
c [ternres-16] limit 28577250 with penalty 2 = 0 + 2
c [ternres-16] 1577 schedulable variables 1%
c [ternres-16] 10572 ternary resolvents (6 bin, 10566 trn)
c [ternres-16] 475 variables remain 0% (168404 retained)
c [decomp-29] removed 5 variables
c [treelook-5] limit 1428862 penalty 2 = 0 + 2 boost 1
c [treelook-5] scheduled 142943 literals 42%
c [treelook-5] scheduling used 1444336 steps
c [treelook-5] not fully scheduled
c [treelook-5] limit 1428862 penalty 2 = 0 + 2 boost 1
c [treelook-5] used 1474427 steps
c [treelook-5] 142935 literals remain 42%
c [treelook-5] 92135 variables remain to probed next time 55%
c [treelook-5] removed 0 variables, found 19 hbrs
c [cgrclsr-9] limit 1986850 based on 3973701 irredundant clauses
c [cgrclsr-9] 103231 schedulable variables 61%
c [cgrclsr-9] 34882 variables remain 21% (133983 retained)
c [cgrclsr-9] removed 9 variables
c [lift-9] limit 1250000 with penalty 4 = 2 + 2
c [lift-9] using 48680 probes 29%
c [lift-9] 78 units, 2 impls, 5 eqs in 1 rounds
c [lift-9] 168743 variables remain 100% (39 retained)
c [lift-9] removed 83 variables
c [cliff-11] limit of 7943560 steps based on 3971780 irredundant clauses
c [cliff-11] failed 0, lifted 0
c [unhide-20] limit 5000000 with penalty 2 = 0 + 2
c [unhide-20-20] 519 units, 41 failed, 2097 tauts, 0 hbrs, 21883 literals
c [transred-14] limit 3971517 based on 3971517 irredundant clauses
c [transred-14] removed 9 transitive binary clauses
c [block-9] scheduling all variables this time
c [block-9] scheduled 168233 variables 100%
c [block-9] limit of 200000000 steps penalty 2 = 0 + 2
c [block-9] fully completed
c [block-9] transition to [ all 0 rem 0 ] state
c [block-9] eliminated 61293 blocked clauses
c [elim-20] 54044 variables 32% will be scheduled this time
c [elim-20] scheduled 54044 variables 32%
c [elim-20] limit of 200000000 steps penalty 2 = 0 + 2
c [elim-20] incomplete 48221 not tried 29% in round 1
c [elim-20] transition to [ all 0 rem 1 ] state
c [elim-20] eliminated 345 = 0% variables out of 167697
c [bca-16] limit of 10000000 steps
c [bca-16] 317373 out of 334706 literals actually usable 95%
c [bca-16] added 4917 blocked clauses in 1361594 steps
c [rephase-7] after 460888 conflicts (new increment 40000, next 500888)
c [flushphases] 5718 phases reset
c [phase-21] phase bias: 5 positive 23%, 17 negative 77%
c [simplification-20] removed 1527 variables 0.9% (167352 remain 35%)
c [simplification-20] removed 90911 irredundant clauses 2.3% (3882796 remain 40%)
c [simplification-20] maximum reduction of 2% = max (1%, 2%)
c [simplification-20] geometric conflict interval increment 8000 = 24000 / 3
c [simplification-20] new conflict interval 32000
c [simplification-20] penalized conflict interval 64000 = 2 * 32000
c [simplification-20] new conflict limit 524888
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  978.2  167352  3882796    471282   11581 119357 212464   0 34.8 2183.6  198
c -  987.4  167352  3882796    481484   12338 119413 212507   1 34.8 2163.1  198
c i  993.8  167351  3882796    487755   18064 119458 212524   0 34.7 2150.5  201
c
c CAUGHT SIGNAL 15 SIGTERM
c
c s UNKNOWN
c bate: 2 basic ate = 1 trn 50% + 1 lrg 50% in 1 updates
c bcas: 16 count, 351054 added (172471 skipped), 29242851 steps
c bkwd: tried 0 clauses, 0 lits, 0.00 lits/clause
c bkwd: checked 0 occs, 0.00 occs/clause, 0.00 occs/lit
c bkwd: subsumed 0 binary, 0 ternary, 0 large
c bkwd: strengthened 0 binary, 0 ternary (0% self), 0 large (0% self)
c blkd: 9 bces, 1994978 removed, 136477708 resolutions, 504138294 steps
c blkd: 90910 blocking literals 9%, 14744 pure
c bvas: 0 bvas, 0 added, 0 removed
c card: 5 count, 0 units, 0 am1, 18905921 steps
c card: 0 rescheduled, 0 eliminated, 0 resolved, 40081 subsumed
c card: 43242 at-most-one constraints found, average size 3.05
c card: 43242 at-most-one constraints used 100%, average size 3.05
c card: 0 at-most-two constraints found, average size 0.00
c card: 0 at-most-two constraints used 0%, average size 0.00
c cces: 7 cces, 164 eliminated, 144 ate 88%, 20 abce 12%
c cces: 0 probed, 0 lifted, 0 failed
c cces: 0 cached, 0 rsz, 0 cols 0%, 0 srch, 0 hits 0%
c cgrs: 9 count, 25819625 esteps, 48268690 csteps
c cgrs: 0 eqs, 11 units
c cgrs: 2 matched (2 ands 100%, 0 xors 0%, 0 ites 0%)
c cgrs: 0 simplified (0 ands 0%, 0 xors 0%, 0 ites 0%)
c cgrs: 46004 extracted (44033 ands 96%, 10 xors 0%, 1961 ites 4%)
c clff: 11 cliffs, 1840 lifted, 11 failed
c clff: 6376 decisions, 138470133 steps
c clls: 1 sat, 0 simp, 0 freeze, 0 melt
c clls: 37871414 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 134 gcs, 0 rescored clauses, 248 rescored vars
c dcps: 30 decompositions, 4633 equivalent 1%
c deco: 17520 decision-only clauses 4%, 59% reduction
c decs: 32054139 decision, 0 random 0.000%, 0 flipped 0.000%
c decs: 0 flipped 0.000% (in 0 phases)
c elms: 20 elims, 164840 eliminated 34%
c elms: 20 rounds, 1.0 rounds/bve
c elms: 62442 small 38%, 87654 large 53%
c elms: 78493 tried small, 62442 succeeded 80%, 16051 failed 20%
c elms: 48748 subsumed, 516215 strengthened, 0 blocked
c elms: 23322628 copies, 38735219 resolutions, 1575865 ipos
c elms: 16589815 subchks, 19955310 strchks
c frcs: 0 computed, 0 - 0 average min-cut range
c gaus: 5 extractions, 154 extracted, 2.0 size, 3 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 30594788 steps, 15297394 extr 50%, 477 elim 0%
c glue: 34.7 orig avg, 32.1 real avg, 5.0 scaled avg
c glue: 0 maxscaledglue=15 (0%)
c hbrs: 162025 = 30467 simple + 131142 trn 19% + 416 lrg 81%, 2832 sub 0%
c hght: 2148 average, 61.97 height/glue
c ints: 15355 luby (3573988 steps), 0 inout (0 steps)
c lift: 9 phases, 318 probed (112 level1 35%, 206 level2 65%)
c lift: 1308 units, 5 equivalences, 19 implications
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 471460 clauses, 98.6 length
c lrnd: 187859 uips 40%, 201076 flips 43%
c mega: 0 count, 0 failed, 0 rounds
c mins: 46471702 learned lits, 14% minimized
c mins: 438807 mins 93%, 2782 bin 1%, 12352 size 3%, 17520 deco 4%
c move: moved 471461, 1923013 bin 408%, 16614 trn 4%, 0 lrg 0%
c otfs: str 63796 dyn (61694 red, 2102 irr) 18091 drv 28%, 45705 rst 72%
c otfs: sub 270 dyn (235 red, 35 irr)
c phas: 21 computed, 493687 set, 89742 pos (18%), 403945 neg (82%)
c prbs: 4 basic, 1157 probed, 96 failed, 0 lifted
c prbs: 5 simple, 522118 probed, 223 failed, 4 eqs
c prbs: 5 treelook, 25 probed, 3 failed, 0 lifted
c prps: 2894111866 props, 89 props/dec
c prps: 98% srch, 2% simp, 0% lkhd
c psns: 19632670 searches, 7179547 hits, 37% 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: 45 count, 0 reset, 0 acts 0%
c reds: 0 geom 0%, 0 glue useless 0%
c reds: 0 memlim 0%, 45 arith 100%, 0 double 0%
c rmbd: 44848 removed, 8797 red 20%
c rphs: 7 recomputed phases
c rsts: 14345 restarts 93%, 1010 skipped 7%
c rsts: 0 saturating 0%, 11 agile 1%, 999 reuse 99%
c rsts: 32.7 avg interval, 32.7 scaled, 1.0 factor
c rsts: 9551 kept 66.6% average 19.7%
c simp: 20 count (20 confs 100%, 0 irr 0%, 0 vars 0%)
c subl: 471460 count (775041 tried 1.6), 30275 sub out of 465073 (6.5%)
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: 145269 fixed 30%, 14 its, 34968.00 confs/it
c trvs: 15425250677 traversals, 98% srch, 2% simp, 0% lkhd
c trvs: 5.3 search traversals per propagation, 31019.3 per conflict
c trvs: 1.3 search traversals per search visit
c trds: 14 transitive reductions, 93 removed, 17 failed
c trds: 1637 nodes, 13044 edges, 79825573 steps
c trim: 1632925 words, 6.2 MB
c trnr: 16 count, 12 bin, 197992 trn, 376236695 steps
c unhd: 20 count, 20 rounds, 268166727 steps
c unhd: 3326 non-trivial sccs of average size 2.1
c unhd: 74557 units, 74557 bin, 0 trn, 0 lrg
c unhd: 478 failed, 467 stamp, 0 lits, 9 bin, 2 trn, 0 lrg
c unhd: 292927 tauts, 1458 bin 0%, 16855 trn 6%, 66423 lrg 23%
c unhd: 292927 tauts, 208191 stamp 71%, 26689 red 9%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 1823651 str, 74557 bin 4%, 24420 trn 1%, 1724674 lrg 95%, 592055 red 32%
c vars: 167351 remaining 35% and 314742 removed 65% out of 482093
c vars: 145269 fixed 30%, 164840 eliminated 34%, 4633 equivalent 1%
c vsts: 12254462986 visits, 98% srch, 2% simp, 0% lkhd
c vsts: 4.2 search visits per propagation, 24542.4 per conflict
c wchs: 1841395577 pushed, 242247901 enlarged, 202 defrags
c 
c scaledglue  added       reduced       forcing      resolved     conflicts
c 
c all    465073 100    367956 100   9510134 100   2741350 100    240503 100
c 
c  0      12435   3         0   0   1830307  19    200715   7     14288   6 
c  1      10695   2         0   0   1610826  17    211116   8     14003   6 
c  2      37869   8     11999   3   3784906  40<   836216  31     50246  21 
c  3      69565  15     64421  18    942189  10    435956  16<    42043  17 
c  4      74564  16     67472  18    566803   6    323387  12     31865  13<
c  5      75013  16<    67293  18<   323666   3    242057   9     25453  11 
c  6      64055  14     56039  15    192473   2    183313   7     23391  10 
c  7      48196  10     41483  11    112222   1    127685   5     17240   7 
c  8      31049   7     26554   7     65918   1     78527   3      9095   4 
c  9      16267   3     13921   4     33279   0     40692   1      4930   2 
c 10      13523   3     11386   3     28150   0     34243   1      4541   2 
c 11       8480   2      5995   2     15220   0     21196   1      3115   1 
c 12       3330   1      1370   0      4140   0      6197   0       293   0 
c 13         32   0        23   0        35   0        50   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             5.1           5.4           2.0           3.4           4.0
c std             2.4           2.1           1.7           2.3           2.5
c 
c  108.314  11% elim
c   84.072   8% block
c   78.693   8% gc
c   58.973   6% decide
c   56.975   6% unhide
c   49.247   5% restart
c   48.761   5% analysis
c   47.802   5% decomp
c   38.009   4% probe
c   26.617   3% defrag
c   26.261   3% card
c   23.151   2% bca
c   21.500   2% cgrclsr
c   18.817   2% cce
c   16.776   2% lift
c   11.964   1% cliff
c   11.210   1% phase
c    6.775   1% gauss
c    5.642   1% bump
c    3.006   0% transred
c    2.042   0% ternres
c    2.018   0% reduce
c    1.465   0% mincls
c    0.482   0% tabularasa
c    0.183   0% cutwidth
c    0.000   0% backward
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   18.872   2% probe simple     50%
c    5.591   1% probe basic      15%
c   13.546   1% probe tree-look  36%
c ==================================
c   31.822   3% preprocessing     7%
c  441.037  44% inprocessing     93%
c ==================================
c  472.860  48% simplifying
c  521.652  52% search
c ==================================
c  994.520 100% all
c 
c 32054139 decisions, 32230.8 decisions/sec
c 489552 conflicts, 492.2 conflicts/sec
c 2894111866 propagations, 2.9 megaprops/sec
c 994.5 seconds, 464.2 MB
c
c CAUGHT SIGNAL 15 SIGTERM
c
c launch: done
