c launch: /data/cnf/sc2014/app/010-80-12.cnf.bz2
c host: atom20
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/010-80-12.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/010-80-12.cnf.bz2
c no embedded options
c found 'p cnf 13408 478488' header
c read 13408 variables, 478488 clauses, 3138520 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 13017 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   13017   308391         0       0      0     0   0  0.0   0.0   17
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 3 at-most-one constraints of average size 3.0
c [card-1] found 6 at-most-two constraints of average size 4.0
c [card-1] using previous limit 2000000 for elimination
c [card-1] 9 out of 9 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 429 variables
c [simpleprobe-1] all 12979 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 11 variables
c [simpleprobe-1] 5228 variables remain 40% (7740 retained)
c [simpleprobe-1] removed 11 variables, found 2 hbrs, 4 units
c [unhide-1] limit 154093 based on 308186 irredundant clauses
c [unhide-1-1] 0 units, 9 failed, 801 tauts, 0 hbrs, 17 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 12965 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 447 variables 3% in round 1 in 3951699 steps
c [elim-1-1] backward subsumption/strengthening limit 7903398
c [elim-1-1] subsumed 967 and strengthened 80 clauses in 7903482 steps
c [elim-1-1] rescheduled 3669 variables 28% by backward subsumption
c [elim-1-2] no variable eliminated in round 2 in 32171 steps
c [elim-1] fully completed in 2 rounds
c [elim-1] transition to [ all 0 rem 0 ] state
c [elim-1] eliminated 447 = 3% variables out of 12965
c [phase-1] phase bias: 4970 positive 40%, 7548 negative 60%
c [simplification-1] removed 499 variables 3.8% (12518 remain 96%)
c [simplification-1] removed 6050 irredundant clauses 2.0% (302341 remain 98%)
c [simplification-1] maximum reduction of 4% = max (4%, 2%)
c [simplification-1] geometric conflict interval increment 4000 = 20000 / 5
c [simplification-1] new conflict interval 4000
c [simplification-1] penalized conflict interval 4000 = 1 * 4000
c [simplification-1] new conflict limit 4000
c [cut-width] 16120, max 27063, min4 13659 at 75%, min10 8175 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    1.5   12518   302341         5       4      0     2   0  3.0  25.5   23
c R    1.5   12518   302341        20      13      1     2   1  2.9  37.8   23
c R    1.5   12518   302341        64      41      7     2   1  3.4  67.4   23
c R    1.5   12518   302341       166     126     10     3   1  4.2 101.5   23
c R    1.5   12518   302341       414     319     16     5   2  4.6 169.3   23
c R    1.5   12518   302341       981     802     32     8   5  4.8 220.8   23
c R    1.6   12518   302341      2284    1879     60    10   6  5.3 284.3   23
c 
c [simplification-2] limit of 4024 conflicts hit after 4024 conflicts
c [decomp-3] removed 1 variables
c [simpleprobe-2] 5045 schedulable variables 40%
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [simpleprobe-2] 5045 variables remain 40% (7472 retained)
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 5995 literals 24%
c [treelook-1] scheduling used 300073 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 300034 steps
c [treelook-1] 5001 literals remain 20%
c [treelook-1] 2819 variables remain to probed next time 23%
c [treelook-1] removed 0 variables, found 2 hbrs
c [basicprobe-1] limit 1000000 penalty 0 = 0 + 0
c [basicprobe-1-0] 534 sched 4%, 3 failed, 0 lifted, 22 hbrs
c [decomp-6] removed 3 variables
c [basicprobe-1-1] 541 sched 4%, 0 failed, 0 lifted, 2 hbrs
c [basicprobe-1-2] 540 sched 4%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-1-2] fully completed probing
c [basicprobe-1-2] 3 units = 3 failed (100%) + 0 lifted (0%)
c [basicprobe-1-2] removed 3 variables, found 24 hbrs
c [unhide-2] limit 151152 based on 302304 irredundant clauses
c [unhide-2-2] 0 units, 0 failed, 2 tauts, 0 hbrs, 25 literals
c [block-1] scheduling all variables this time
c [block-1] scheduled 12514 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 650 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 17604 clauses out of 103993 (17%) of length 7
c [cce-1-1] eliminated 432 clauses out of 85619 (1%) of length 6
c [cce-1-1] eliminated 11868 clauses out of 66777 (18%) of length 5
c [cce-1-1] eliminated 154 clauses out of 34007 (0%) of length 4
c [cce-1-1] completed large round (ATE)
c [cce-1-1] eliminated 30058 large clauses in 184595551 steps
c [cce-1-1] allowing another 92297775 steps for small clauses
c [cce-1] scheduling 10805 clauses = 321 binary + 10484 ternary
c [cce-1] tried to eliminate 10805 small clauses 100%
c [cce-1] eliminated 1048 small clauses 10%
c [cce-1] eliminated 6 binary clauses 2%
c [cce-1] eliminated 1042 ternary clauses 10%
c [cce-1-1] eliminated 1048 small clauses in 95893079 steps
c [cce-1-1] completed small round (ATE)
c [cce-1-1] completed small and large (ATE)
c [cce-1-1] eliminated 31106 covered clauses in round 1
c [cce-1-2] completed large round (ABCE)
c [cce-1-2] allowing another 0 steps for small clauses
c [cce-1] scheduling 9757 clauses = 315 binary + 9442 ternary
c [cce-1] tried to eliminate 9757 small clauses 100%
c [cce-1-2] completed small round (ABCE)
c [cce-1-2] completed small and large (ABCE)
c [cce-1-2] eliminated 0 covered clauses in round 2
c [cce-1] eliminated 31106 covered clauses in TOTAL during 2 rounds
c [elim-2] scheduling all variables this time
c [elim-2] scheduled 12514 variables 100%
c [elim-2] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-2] incomplete 9873 not tried 79% in round 1
c [elim-2] transition to [ all 1 rem 1 ] state
c [elim-2] eliminated 103 = 1% variables out of 12514
c [bca-1] limit of 10000000 steps
c [bca-1] 21141 out of 24824 literals actually usable 85%
c [bca-1] added 0 blocked clauses in 177129 steps
c [phase-2] phase bias: 28 positive 9%, 276 negative 91%
c [simplification-2] removed 107 variables 0.9% (12411 remain 95%)
c [simplification-2] removed 34091 irredundant clauses 11.3% (268250 remain 87%)
c [simplification-2] maximum reduction of 11% = max (1%, 11%)
c [simplification-2] large reduction 11% >= 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 6024
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c R    8.2   12411   268250      5201    4326   1135    35   9  5.7 333.4   22
c -    8.3   12411   268250      5612    2691   1138    36   7  5.7 348.9   22
c 
c [simplification-3] limit of 6028 conflicts hit after 6029 conflicts
c [ternres-1] boosting ternary resolution limit by 5
c [ternres-1] limit 20000000 with penalty 0 = 0 + 0
c [ternres-1] all 12411 free variables schedulable
c [ternres-1] 165 ternary resolvents (17 bin, 148 trn)
c [ternres-1] fully completed ternary resolution
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 2 at-most-one constraints of average size 3.0
c [card-2] found 6 at-most-two constraints of average size 4.2
c [card-2] using previous limit 1000000 for elimination
c [card-2] 8 out of 8 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 1809 xors of average arity 5.0
c [gauss-1] connected 9009 occurrences of 503 variables (average 17.9)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] fully completed
c [gauss-1] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-8] removed 1 variables
c [cgrclsr-1] limit 200000 penalty 0 = 0 + 0
c [cgrclsr-1] all 12410 free variables schedulable
c [cgrclsr-1] fully completed congruence closure
c [lift-1] limit 500000 with penalty 0 = 0 + 0
c [lift-1] using 2784 probes 22%
c [lift-1-1] found 0 units 18 impls in round 1
c [lift-1] 1 units, 30 impls, 2 eqs in 2 rounds
c [lift-1] 9626 variables remain 78% (2781 retained)
c [lift-1] removed 3 variables
c [cliff-1] limit of 10000000 steps penalty 0 = 0 + 0
c [cliff-1] failed 1, lifted 0
c [transred-1] limit 268235 based on 268235 irredundant clauses
c [transred-1] removed 10 transitive binary clauses
c [block-2] scheduling all variables this time
c [block-2] scheduled 12406 variables 100%
c [block-2] limit of 50000000 steps penalty 0 = 0 + 0
c [block-2] fully completed
c [block-2] transition to [ all 0 rem 0 ] state
c [block-2] eliminated 0 blocked clauses
c [cce-2] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-2-1] incomplete large round (ACCE)
c [cce-2-1] allowing another 15000000 steps for small clauses
c [cce-2] scheduling 714 clauses = 317 binary + 397 ternary
c [cce-2] tried to eliminate 714 small clauses 100%
c [cce-2] eliminated 34 small clauses 5%
c [cce-2] eliminated 2 binary clauses 1%
c [cce-2] eliminated 32 ternary clauses 8%
c [cce-2-1] eliminated 34 small clauses in 15199752 steps
c [cce-2-1] completed small round (ACCE)
c [cce-2-1] eliminated 34 covered clauses in round 1
c [cce-2-2] incomplete large round (ACCE)
c [cce-2-2] allowing another 7400124 steps for small clauses
c [cce-2] scheduling 680 clauses = 315 binary + 365 ternary
c [cce-2] tried to eliminate 680 small clauses 100%
c [cce-2-2] completed small round (ACCE)
c [cce-2-2] eliminated 0 covered clauses in round 2
c [cce-2] eliminated 34 covered clauses in TOTAL during 2 rounds
c [cce-2] 34 < 1/1000 * 268227 = 268 considered unsuccessful
c [elim-3] 9873 variables 80% will be scheduled this time
c [elim-3] scheduled 9873 variables 80%
c [elim-3] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-3] incomplete 7867 not tried 63% in round 1
c [elim-3] transition to [ all 0 rem 1 ] state
c [elim-3] eliminated 3 = 0% variables out of 12406
c [elim-3] 3 < 1/1000 * 12406 = 12 considered unsuccessful
c [phase-3] phase bias: 14 positive 67%, 7 negative 33%
c [simplification-3] removed 8 variables 0.1% (12403 remain 95%)
c [simplification-3] removed 71 irredundant clauses 0.0% (268179 remain 87%)
c [simplification-3] maximum reduction of 0% = max (0%, 0%)
c [simplification-3] full geometric conflict interval increment 20000
c [simplification-3] new conflict interval 24000
c [simplification-3] penalized conflict interval 24000 = 1 * 24000
c [simplification-3] new conflict limit 30029
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -   12.2   12403   268179      9658    3750   1321    78   7  5.8 366.8   21
c R   12.3   12403   268179     11667    5512   1339    81   9  6.0 391.4   21
c -   12.6   12403   268179     14020    4536   1376    83   8  6.0 387.1   21
c -   13.1   12403   268179     19231    5604   1452    89   7  6.2 381.5   21
c -   13.6   12403   268179     24957    6780   1510    92   9  6.5 396.0   21
c R   13.7   12403   268179     25924    7662   1524    92  12  6.5 399.2   21
c 
c [simplification-4] limit of 30059 conflicts hit after 30059 conflicts
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] all 12403 free variables schedulable
c [ternres-2] 21 ternary resolvents (4 bin, 17 trn)
c [ternres-2] fully completed ternary resolution
c [decomp-9] removed 1 variables
c [treelook-2] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-2] scheduled 1185 literals 5%
c [treelook-2] scheduling used 150022 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-2] used 150000 steps
c [treelook-2] 639 literals remain 3%
c [treelook-2] 630 variables remain to probed next time 5%
c [treelook-2] removed 0 variables, found 5 hbrs
c [lift-2] limit 500000 with penalty 0 = 0 + 0
c [lift-2] using 162 probes 1%
c [lift-2-1] found 0 units 0 impls in round 1
c [lift-2-2] found 0 units 1 impls in round 2
c [lift-2-3] found 0 units 1 impls in round 3
c [lift-2-4] found 0 units 0 impls in round 4
c [lift-2-5] found 0 units 0 impls in round 5
c [lift-2] 0 units, 2 impls, 0 eqs in 6 rounds
c [lift-2] 9463 variables remain 76% (2939 retained)
c [cliff-2] limit of 10000000 steps penalty 0 = 0 + 0
c [cliff-2] failed 0, lifted 0
c [unhide-3] limit 134088 based on 268177 irredundant clauses
c [unhide-3-3] 0 units, 0 failed, 8 tauts, 0 hbrs, 29 literals
c [transred-2] limit 445574 with penalty 0 = 0 + 0
c [transred-2] removed 4 transitive binary clauses
c [bca-2] limit of 10000000 steps
c [bca-2] 19017 out of 24806 literals actually usable 77%
c [bca-2] added 0 blocked clauses in 166341 steps
c [rephase-1] after 30059 conflicts (new increment 20000, next 50059)
c [flushphases] 6872 phases reset
c [phase-4] phase bias: 0 positive 0%, 0 negative 0%
c [simplification-4] removed 1 variables 0.0% (12402 remain 95%)
c [simplification-4] removed 4 irredundant clauses 0.0% (268175 remain 87%)
c [simplification-4] maximum reduction of 0% = max (0%, 0%)
c [simplification-4] full geometric conflict interval increment 24000
c [simplification-4] new conflict interval 48000
c [simplification-4] penalized conflict interval 48000 = 1 * 48000
c [simplification-4] new conflict limit 78059
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -   15.4   12402   268175     31131    7718   1588   115   8  6.6 391.3   22
c -   16.1   12402   268175     38035    8818   1681   115   9  6.7 388.7   22
c -   16.9   12402   268175     45506   10061   1750   116   9  6.9 383.2   22
c -   17.6   12402   268175     53508   11348   1817   119  13  7.3 393.4   22
c R   17.9   12402   268175     56984   14540   1836   119  13  7.4 399.3   22
c -   18.5   12402   268175     61784   12395   1900   121   9  7.5 398.3   22
c -   19.5   12402   268175     70944   13729   1977   124  10  7.6 395.6   22
c 
c [simplification-5] limit of 78075 conflicts hit after 78075 conflicts
c [ternres-3] limit 4000000 with penalty 0 = 0 + 0
c [ternres-3] all 12402 free variables schedulable
c [ternres-3] 2 ternary resolvents (0 bin, 2 trn)
c [ternres-3] fully completed ternary resolution
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] extracted 8 xors of average arity 3.0
c [gauss-2] connected 24 occurrences of 3 variables (average 8.0)
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] fully completed
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [basicprobe-2] limit 1395370 penalty 0 = 0 + 0
c [basicprobe-2-0] 597 sched 5%, 0 failed, 0 lifted, 2 hbrs
c [basicprobe-2-1] 599 sched 5%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-2-1] fully completed probing
c [basicprobe-2-1] removed 0 variables, found 2 hbrs
c [cgrclsr-2] limit 134087 based on 268175 irredundant clauses
c [cgrclsr-2] all 12402 free variables schedulable
c [cgrclsr-2] fully completed congruence closure
c [transred-3] limit 1395370 with penalty 0 = 0 + 0
c [transred-3] removed 0 transitive binary clauses
c [block-3] scheduling all variables this time
c [block-3] scheduled 12402 variables 100%
c [block-3] limit of 25000000 steps penalty 1 = 1 + 0
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 0 blocked clauses
c [cce-3] limit of 15000000 steps penalty 1 = 1 + 0
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] allowing another 7500000 steps for small clauses
c [cce-3] scheduling 724 clauses = 312 binary + 412 ternary
c [cce-3] tried to eliminate 724 small clauses 100%
c [cce-3] eliminated 4 small clauses 1%
c [cce-3] eliminated 1 binary clauses 0%
c [cce-3] eliminated 3 ternary clauses 1%
c [cce-3-1] eliminated 4 small clauses in 7703317 steps
c [cce-3-1] completed small round (ACCE)
c [cce-3-1] eliminated 4 covered clauses in round 1
c [cce-3-2] incomplete large round (ACCE)
c [cce-3-2] allowing another 3648342 steps for small clauses
c [cce-3] scheduling 720 clauses = 311 binary + 409 ternary
c [cce-3] tried to eliminate 720 small clauses 100%
c [cce-3-2] completed small round (ACCE)
c [cce-3-2] eliminated 0 covered clauses in round 2
c [cce-3] eliminated 4 covered clauses in TOTAL during 2 rounds
c [cce-3] 4 < 1/1000 * 268175 = 268 considered unsuccessful
c [elim-4] scheduling all variables this time
c [elim-4] scheduled 12402 variables 100%
c [elim-4] limit of 13953705 steps penalty 1 = 1 + 0
c [elim-4] incomplete 9775 not tried 79% in round 1
c [elim-4] transition to [ all 1 rem 1 ] state
c [elim-4] eliminated 1 = 0% variables out of 12402
c [elim-4] 1 < 1/1000 * 12402 = 12 considered unsuccessful
c [rephase-2] after 78075 conflicts (new increment 40000, next 118075)
c [flushphases] 6704 phases reset
c [phase-5] phase bias: 0 positive 0%, 0 negative 0%
c [simplification-5] removed 1 variables 0.0% (12401 remain 95%)
c [simplification-5] removed 23 irredundant clauses 0.0% (268152 remain 87%)
c [simplification-5] maximum reduction of 0% = max (0%, 0%)
c [simplification-5] full geometric conflict interval increment 48000
c [simplification-5] new conflict interval 96000
c [simplification-5] penalized conflict interval 96000 = 1 * 96000
c [simplification-5] new conflict limit 174075
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -   23.0   12401   268152     80482   14925   2062   125  18  8.0 395.3   22
c -   24.2   12401   268152     90404   16040   2147   126  11  8.2 396.7   22
c -   25.4   12401   268152    101051   17272   2228   126  11  8.3 392.1   22
c -   26.5   12401   268152    112100   18547   2299   131  14  8.7 396.7   22
c -   27.5   12401   268152    123857   20110   2349   133  20  9.2 405.2   23
c R   27.5   12401   268152    124226   20459   2352   133  17  9.2 405.4   23
c -   29.1   12401   268152    135731   21051   2419   135  13  9.3 405.0   23
c -   30.8   12401   268152    148723   22626   2508   138  17  9.6 403.4   23
c -   32.5   12401   268152    161835   23635   2599   140  15  9.9 403.2   23
c 
c [simplification-6] limit of 174099 conflicts hit after 174099 conflicts
c [ternres-4] limit 4000000 with penalty 0 = 0 + 0
c [ternres-4] all 12401 free variables schedulable
c [ternres-4] 16 ternary resolvents (5 bin, 11 trn)
c [ternres-4] fully completed ternary resolution
c [card-3] limit 500000 penalty 2 = 2 + 0
c [card-3] found 2 at-most-one constraints of average size 3.0
c [card-3] found 6 at-most-two constraints of average size 4.2
c [card-3] using previous limit 500000 for elimination
c [card-3] 8 out of 8 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [lift-3] limit 1154335 with penalty 1 = 1 + 0
c [lift-3] using 418 probes 3%
c [lift-3-1] found 0 units 0 impls in round 1
c [lift-3-2] found 0 units 0 impls in round 2
c [lift-3-3] found 0 units 0 impls in round 3
c [lift-3-4] found 0 units 0 impls in round 4
c [lift-3-5] found 0 units 0 impls in round 5
c [lift-3] 0 units, 0 impls, 0 eqs in 6 rounds
c [lift-3] 9045 variables remain 73% (3356 retained)
c [cliff-3] limit of 5000000 steps penalty 1 = 1 + 0
c [cliff-3] failed 0, lifted 0
c [rephase-3] after 174099 conflicts (new increment 80000, next 254099)
c [flushphases] 6462 phases reset
c [phase-6] phase bias: 0 positive 0%, 0 negative 0%
c [simplification-6] removed 0 variables 0.0% (12401 remain 95%)
c [simplification-6] removed 0 irredundant clauses 0.0% (268152 remain 87%)
c [simplification-6] maximum reduction of 0% = max (0%, 0%)
c [simplification-6] full geometric conflict interval increment 96000
c [simplification-6] new conflict interval 192000
c [simplification-6] penalized conflict interval 192000 = 1 * 192000
c [simplification-6] new conflict limit 366099
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -   34.9   12401   268152    175887   25334   2713   150  15 10.1 404.3   24
c -   36.7   12401   268152    189929   26240   2800   153  10 10.3 405.0   23
c -   38.9   12401   268152    205160   27920   2921   156  17 10.4 406.4   23
c -   40.6   12401   268152    223026   30549   3167   162   6 10.0 407.3   23
c -   42.3   12401   268152    240322   32504   3342   169  11  9.9 412.4   24
c -   43.7   12401   268152    257786   34352   3471   177  12  9.9 420.5   24
c R   44.6   12401   268152    268910   44626   3521   180  13  9.9 425.1   25
c -   45.5   12401   268152    275499   35921   3625   181   7  9.9 423.5   24
c -   48.0   12401   268152    294629   38205   3845   190  12  9.8 425.2   24
c -   50.5   12401   268152    313977   39936   4141   192  10  9.7 423.1   24
c -   53.0   12401   268152    333473   41731   4325   194  10  9.7 425.8   25
c -   55.7   12401   268152    353326   43486   4499   194   8  9.7 426.2   25
c 
c [simplification-7] limit of 366137 conflicts hit after 366137 conflicts
c [ternres-5] limit 8768314 with penalty 0 = 0 + 0
c [ternres-5] all 12401 free variables schedulable
c [ternres-5] 7 ternary resolvents (4 bin, 3 trn)
c [ternres-5] fully completed ternary resolution
c [simpleprobe-3] 4996 schedulable variables 40%
c [simpleprobe-3] limit 17536628 penalty 1 = 1 + 0
c [simpleprobe-3] 3669 variables remain 30% (8732 retained)
c [simpleprobe-3] removed 0 variables, found 17 hbrs, 0 units
c [unhide-4] limit 438415 with penalty 2 = 2 + 0
c [unhide-4-4] 0 units, 0 failed, 73 tauts, 0 hbrs, 221 literals
c [transred-4] limit 1000000 with penalty 1 = 1 + 0
c [transred-4] removed 6 transitive binary clauses
c [bca-3] limit of 10000000 steps
c [bca-3] 8835 out of 24804 literals actually usable 36%
c [bca-3] added 0 blocked clauses in 122261 steps
c [rephase-4] after 366137 conflicts (new increment 160000, next 526137)
c [flushphases] 2699 phases reset
c [phase-7] phase bias: 0 positive 0%, 0 negative 0%
c [simplification-7] removed 0 variables 0.0% (12401 remain 95%)
c [simplification-7] removed 0 irredundant clauses 0.0% (268152 remain 87%)
c [simplification-7] maximum reduction of 0% = max (0%, 0%)
c [simplification-7] full geometric conflict interval increment 192000
c [simplification-7] new conflict interval 384000
c [simplification-7] penalized conflict interval 384000 = 1 * 384000
c [simplification-7] new conflict limit 750137
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -   59.6   12401   268152    374318   45595   4655   215  13  9.7 426.9   25
c -   61.6   12401   268152    395510   47468   4830   221   8  9.8 430.4   25
c -   64.7   12401   268152    417704   49698   5062   225  12  9.8 429.0   25
c -   67.7   12401   268152    440571   51710   5262   225  10  9.8 428.3   25
c -   70.3   12401   268152    463991   53346   5435   227  10  9.9 431.8   25
c -   73.7   12401   268152    488218   55071   5586   229  10 10.0 436.2   26
c -   75.3   12401   268152    512513   56469   5658   229  39 10.3 437.6   25
c -   77.2   12401   268152    536354   58207   5724   230  22 10.7 441.6   26
c -   78.6   12401   268152    560014   59240   5764   230  19 11.0 444.0   26
c R   79.5   12401   268152    578685   76075   5791   231  22 11.3 445.1   30
c -   80.6   12401   268152    584869   60266   5817   231  12 11.3 444.6   26
c -   84.3   12401   268152    610475   62050   5925   231  12 11.4 442.8   27
c -   87.7   12401   268152    636934   63830   6054   231  11 11.5 442.9   26
c -   91.8   12401   268152    663595   65891   6166   231   9 11.5 440.4   27
c -   95.9   12401   268152    690954   68010   6315   231  14 11.6 440.3   27
c -   99.9   12401   268152    719136   69994   6514   231  12 11.6 440.7   27
c -  104.8   12401   268152    747912   72127   6697   231  12 11.6 439.9   27
c 
c [simplification-8] limit of 750147 conflicts hit after 750149 conflicts
c [ternres-6] limit 19306041 with penalty 0 = 0 + 0
c [ternres-6] all 12401 free variables schedulable
c [ternres-6] 17 ternary resolvents (1 bin, 16 trn)
c [ternres-6] fully completed ternary resolution
c [gauss-3] limit 965302 penalty 2 = 2 + 0
c [gauss-3] extracted 4 xors of average arity 3.0
c [gauss-3] connected 12 occurrences of 3 variables (average 4.0)
c [gauss-3] limit 965302 penalty 2 = 2 + 0
c [gauss-3] fully completed
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [cgrclsr-3] limit 482651 penalty 2 = 2 + 0
c [cgrclsr-3] all 12401 free variables schedulable
c [cgrclsr-3] fully completed congruence closure
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 2 transitive binary clauses
c [block-4] scheduling all variables this time
c [block-4] scheduled 12401 variables 100%
c [block-4] limit of 48265104 steps penalty 2 = 2 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 0 blocked clauses
c [cce-4] limit of 9653020 steps penalty 2 = 2 + 0
c [cce-4-1] incomplete large round (ACCE)
c [cce-4-1] allowing another 4826510 steps for small clauses
c [cce-4] scheduling 929 clauses = 327 binary + 602 ternary
c [cce-4] tried to eliminate 929 small clauses 100%
c [cce-4] eliminated 14 small clauses 2%
c [cce-4] eliminated 2 binary clauses 1%
c [cce-4] eliminated 12 ternary clauses 2%
c [cce-4-1] eliminated 14 small clauses in 5189175 steps
c [cce-4-1] completed small round (ACCE)
c [cce-4-1] eliminated 14 covered clauses in round 1
c [cce-4-2] incomplete large round (ACCE)
c [cce-4-2] allowing another 2231923 steps for small clauses
c [cce-4] scheduling 915 clauses = 325 binary + 590 ternary
c [cce-4] tried to eliminate 915 small clauses 100%
c [cce-4-2] completed small round (ACCE)
c [cce-4-2] eliminated 0 covered clauses in round 2
c [cce-4] eliminated 14 covered clauses in TOTAL during 2 rounds
c [cce-4] 14 < 1/1000 * 268152 = 268 considered unsuccessful
c [elim-5] 7864 variables 63% will be scheduled this time
c [elim-5] scheduled 7864 variables 63%
c [elim-5] limit of 96530209 steps penalty 2 = 2 + 0
c [elim-5] incomplete 3933 not tried 32% in round 1
c [elim-5] transition to [ all 0 rem 1 ] state
c [elim-5] eliminated 0 = 0% variables out of 12401
c [rephase-5] after 750149 conflicts (new increment 320000, next 1070149)
c [flushphases] 2630 phases reset
c [phase-8] phase bias: 27 positive 59%, 19 negative 41%
c [simplification-8] removed 0 variables 0.0% (12401 remain 95%)
c [simplification-8] removed 252 irredundant clauses 0.1% (267900 remain 87%)
c [simplification-8] maximum reduction of 0% = max (0%, 0%)
c [simplification-8] full geometric conflict interval increment 384000
c [simplification-8] new conflict interval 768000
c [simplification-8] penalized conflict interval 768000 = 1 * 768000
c [simplification-8] new conflict limit 1518149
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  112.4   12401   267900    777054   74317   6879   232  13 11.6 439.3   28
c -  117.3   12401   267900    807153   76481   7001   232  13 11.6 438.9   28
c -  119.7   12401   267900    837376   77874   7056   232  38 11.9 442.5   28
c -  124.0   12401   267900    868495   79269   7147   232  13 12.0 443.1   29
c -  127.9   12401   267900    901333   81355   7224   232  25 12.0 443.5   28
c -  131.8   12401   267900    933724   82281   7291   232  11 12.2 442.5   29
c -  135.0   12401   267900    967221   83877   7342   232  27 12.3 443.1   29
c -  138.8   12401   267900   1000283   84877   7376   232  13 12.4 441.8   29
c -  142.6   12401   267900   1034386   85986   7414   233  19 12.6 440.7   29
c -  146.9   12401   267900   1068837   87286   7462   233  11 12.7 439.3   29
c -  149.2   12401   267900   1103171   88486   7479   233  29 12.9 439.8   29
c -  150.8   12401   267900   1137689   89232   7479   233  43 13.2 440.4   30
c -  152.3   12401   267900   1172127   89958   7490   233  32 13.6 441.3   30
c -  154.1   12401   267900   1207316   90849   7501   233  37 13.7 442.9   30
c -  156.1   12401   267900   1243323   91335   7522   233   9 13.9 443.9   30
c -  161.5   12401   267900   1281162   92611   7575   233  10 14.0 443.3   30
c -  166.8   12401   267900   1319225   93910   7617   233  19 14.0 442.9   30
c -  171.3   12401   267900   1357718   95269   7649   233  32 14.1 443.3   30
c -  175.7   12401   267900   1396567   96264   7672   233  34 14.4 442.8   30
c -  180.2   12401   267900   1435623   97228   7700   233  15 14.5 442.7   30
c -  185.7   12401   267900   1476045   98428   7726   233  21 14.6 441.9   30
c -  189.1   12401   267900   1514449   99888   7734   233  36 15.1 442.7   30
c 
c [simplification-9] limit of 1518149 conflicts hit after 1518150 conflicts
c [ternres-7] limit 38202284 with penalty 0 = 0 + 0
c [ternres-7] all 12401 free variables schedulable
c [ternres-7] 9 ternary resolvents (0 bin, 9 trn)
c [ternres-7] fully completed ternary resolution
c [lift-4] limit 5000000 with penalty 2 = 2 + 0
c [lift-4] using 1124 probes 9%
c [lift-4-1] found 0 units 1 impls in round 1
c [lift-4-2] found 0 units 0 impls in round 2
c [lift-4-3] found 0 units 0 impls in round 3
c [lift-4-4] found 0 units 0 impls in round 4
c [lift-4-5] found 0 units 0 impls in round 5
c [lift-4] 0 units, 1 impls, 0 eqs in 6 rounds
c [lift-4] 7921 variables remain 64% (4480 retained)
c [cliff-4] limit of 7640456 steps penalty 2 = 2 + 0
c [cliff-4] failed 0, lifted 0
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 0 transitive binary clauses
c [rephase-6] after 1518150 conflicts (new increment 640000, next 2158150)
c [flushphases] 2627 phases reset
c [phase-9] phase bias: 2 positive 100%, 0 negative 0%
c [simplification-9] removed 0 variables 0.0% (12401 remain 95%)
c [simplification-9] removed 0 irredundant clauses 0.0% (267900 remain 87%)
c [simplification-9] maximum reduction of 0% = max (0%, 0%)
c [simplification-9] full geometric conflict interval increment 768000
c [simplification-9] new conflict interval 1536000
c [simplification-9] penalized conflict interval 1536000 = 1 * 1536000
c [simplification-9] new conflict limit 3054150
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  196.9   12401   267900   1554301  101630   7851   236  11 15.1 441.2   31
c -  204.2   12401   267900   1595793  104195   7979   236  12 15.1 440.3   32
c -  210.4   12401   267900   1638068  106316   8028   236  14 15.2 440.6   32
c -  217.0   12401   267900   1683929  110481   8515   238  12 15.1 439.3   32
c -  222.2   12401   267900   1733220  115886   9589   288  13 14.9 435.9   32
c -  226.6   12401   267900   1775744  118061   9761   291  30 16.0 435.8   31
c -  230.4   12401   267900   1818091  120385   9802   291  18 16.9 436.4   32
c -  239.2   12401   267900   1861664  122422   9888   291  17 16.9 434.9   32
c -  246.4   12401   267900   1907876  124877  10088   291  13 16.9 435.1   33
c -  252.6   12401   267900   1955718  127171  10282   291  26 16.8 436.5   33
c -  260.7   12401   267900   2002219  129762  10373   291  13 16.9 435.6   33
c -  268.1   12401   267900   2049539  132882  10556   292  18 17.0 434.3   33
c -  273.2   12401   267900   2096403  135178  10669   292  16 17.3 435.1   33
c -  277.5   12401   267900   2145482  136333  10698   292  33 17.5 434.9   33
c -  284.6   12401   267900   2194293  138300  10776   292  19 17.5 433.9   33
c -  293.2   12401   267900   2242780  141204  10819   292  13 17.6 433.6   33
c -  301.2   12401   267900   2293611  145480  11108   301  17 17.5 431.7   34
c -  306.9   12401   267900   2344940  148954  11390   308  26 17.5 431.4   34
c -  311.8   12401   267900   2393302  151040  11402   308  29 18.1 432.3   33
c -  318.0   12401   267900   2444504  154864  11488   308  30 18.6 433.5   34
c -  322.5   12401   267900   2497252  159563  11598   308  34 18.8 434.9   35
c -  328.4   12401   267900   2546578  160343  11611   308  32 19.5 435.4   35
c -  337.2   12401   267900   2596023  160998  11613   308  35 20.2 435.9   35
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  345.9   12401   267900   2646284  161581  11614   308  39 21.0 436.4   36
c -  355.6   12401   267900   2696528  162208  11614   308  38 21.6 436.9   36
c -  365.6   12401   267900   2747235  162736  11614   308  38 22.1 437.3   36
c -  374.7   12401   267900   2798242  163280  11614   308  37 22.6 437.8   36
c -  384.3   12401   267900   2849986  163829  11614   308  37 23.1 438.2   36
c -  394.7   12401   267900   2902504  164397  11614   308  39 23.6 438.7   36
c -  405.0   12401   267900   2955521  164962  11615   308  38 24.1 439.2   36
c -  415.8   12401   267900   3008920  165553  11615   308  39 24.5 439.7   36
c 
c [simplification-10] limit of 3054234 conflicts hit after 3054235 conflicts
c [ternres-8] limit 109846154 with penalty 0 = 0 + 0
c [ternres-8] all 12401 free variables schedulable
c [ternres-8] 126 ternary resolvents (5 bin, 121 trn)
c [ternres-8] fully completed ternary resolution
c [card-4] limit 6865384 penalty 3 = 3 + 0
c [card-4] found 2 at-most-one constraints of average size 3.0
c [card-4] found 4 at-most-two constraints of average size 4.0
c [card-4] using previous limit 6865384 for elimination
c [card-4] 6 out of 6 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [decomp-18] removed 3 variables
c [treelook-3] limit 1373076 penalty 2 = 2 + 0 boost 1
c [treelook-3] scheduled 1327 literals 5%
c [treelook-3] scheduling used 1075270 steps
c [treelook-3] scheduled completely
c [treelook-3] limit 1373076 penalty 2 = 2 + 0 boost 1
c [treelook-3] used 369445 steps
c [treelook-3] fully completed tree based probing
c [treelook-3] removed 0 variables, found 10 hbrs
c [rephase-7] after 3054235 conflicts (new increment 1280000, next 4334235)
c [flushphases] 0 phases reset
c [simplification-10] removed 3 variables 0.0% (12398 remain 95%)
c [simplification-10] removed 6 irredundant clauses 0.0% (267894 remain 87%)
c [simplification-10] maximum reduction of 0% = max (0%, 0%)
c [simplification-10] full geometric conflict interval increment 1536000
c [simplification-10] conflict interval soft limit 1000000 reached
c [simplification-10] new conflict interval 1000000
c [simplification-10] penalized conflict interval 1000000 = 1 * 1000000
c [simplification-10] new conflict limit 4054235
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  426.2   12398   267894   3063029  165521  11692   320  15 24.8 439.8   40
c -  431.1   12398   267894   3120628  166345  11694   320  45 24.9 440.0   40
c -  436.6   12398   267894   3178574  166981  11695   320  49 24.9 440.4   39
c -  443.0   12398   267894   3238180  167512  11695   320  43 25.0 440.8   39
c -  446.6   12398   267894   3297388  168068  11695   320  47 25.0 441.1   39
c -  449.2   12398   267894   3357155  168581  11699   320  23 25.0 441.5   60
c -  453.8   12398   267894   3419287  170145  11736   320  51 24.9 441.6   40
c -  459.6   12398   267894   3479194  170689  11736   320  48 24.7 442.0   40
c -  467.9   12398   267894   3542670  172703  11836   321  17 24.6 440.7   38
c -  475.8   12398   267894   3608134  174779  11977   322  27 24.4 439.0   39
c -  483.3   12398   267894   3673173  176268  12091   322  20 24.3 437.4   39
c -  490.7   12398   267894   3739108  178018  12177   322  35 24.2 435.9   39
c -  499.2   12398   267894   3800073  179553  12179   322  30 24.7 436.6   37
c -  508.1   12398   267894   3860207  180200  12179   322  34 25.1 437.1   39
c -  519.1   12398   267894   3920549  180760  12179   322  32 25.7 437.7   39
c -  530.5   12398   267894   3981859  181399  12179   322  36 26.1 438.2   39
c -  541.4   12398   267894   4043400  181967  12179   322  36 26.5 438.7   39
c 
c [simplification-11] limit of 4054239 conflicts hit after 4054239 conflicts
c [ternres-9] limit 157798317 with penalty 0 = 0 + 0
c [ternres-9] all 12398 free variables schedulable
c [ternres-9] 28 ternary resolvents (1 bin, 27 trn)
c [ternres-9] fully completed ternary resolution
c [unhide-5] limit 2500000 with penalty 3 = 3 + 0
c [unhide-5-8] 0 units, 0 failed, 177 tauts, 0 hbrs, 1362 literals
c [transred-7] limit 1000000 with penalty 1 = 1 + 0
c [transred-7] removed 2 transitive binary clauses
c [bca-4] limit of 10000000 steps
c [bca-4] 57 out of 24798 literals actually usable 0%
c [bca-4] not enough literals usable
c [bca-4] added 0 blocked clauses in 192518 steps
c [simplification-11] removed 0 variables 0.0% (12398 remain 95%)
c [simplification-11] removed 29 irredundant clauses 0.0% (267865 remain 87%)
c [simplification-11] maximum reduction of 0% = max (0%, 0%)
c [simplification-11] full geometric conflict interval increment 1000000
c [simplification-11] conflict interval soft limit 1000000 reached
c [simplification-11] new conflict interval 1000000
c [simplification-11] penalized conflict interval 1000000 = 1 * 1000000
c [simplification-11] new conflict limit 5054239
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  548.6   12398   267865   4110482  182580  12167   320  46 26.4 438.3   39
c -  554.6   12398   267865   4178191  183618  12167   320  41 26.2 438.5   39
c -  563.3   12398   267865   4246908  184791  12167   320  43 26.1 438.8   39
c -  574.0   12398   267865   4316156  186001  12167   320  44 25.9 439.1   39
c -  583.3   12398   267865   4384936  187131  12167   320  43 25.8 439.3   62
c -  593.5   12398   267865   4453641  188098  12167   320  43 25.6 439.6   62
c -  602.9   12398   267865   4522303  188923  12167   320  44 25.5 439.9   62
c -  614.1   12398   267865   4590770  189545  12167   320  45 25.4 440.1   62
c -  626.5   12398   267865   4660004  190526  12167   320  38 25.3 440.4   40
c -  642.4   12398   267865   4729406  191222  12169   320  34 26.5 440.7   40
c -  650.3   12398   267865   4802142  193562  12375   320  20 26.4 439.7   41
c -  659.5   12398   267865   4877023  195757  12548   320  11 26.2 437.9   41
c -  671.1   12398   267865   4954329  198281  12681   320  30 26.1 435.9   42
c -  680.4   12398   267865   5028577  202344  12788   320  20 26.1 435.7   42
c 
c [simplification-12] limit of 5054239 conflicts hit after 5054242 conflicts
c [ternres-10] limit 200000000 with penalty 0 = 0 + 0
c [ternres-10] all 12398 free variables schedulable
c [ternres-10] 32 ternary resolvents (0 bin, 32 trn)
c [ternres-10] fully completed ternary resolution
c [gauss-4] limit 5194260 penalty 3 = 3 + 0
c [gauss-4] extracted 5232 xors of average arity 5.0
c [gauss-4] connected 26088 occurrences of 843 variables (average 30.9)
c [gauss-4] limit 5194260 penalty 3 = 3 + 0
c [gauss-4] connected 5153 occurrences of 843 variables (average 6.1)
c [gauss-4] fully completed
c [gauss-4] exported 0 unary, 0 binary and 0 ternary equations
c [basicprobe-3] limit 50000000 penalty 1 = 1 + 0
c [basicprobe-3-0] 793 sched 6%, 0 failed, 0 lifted, 6 hbrs
c [basicprobe-3-1] 795 sched 6%, 0 failed, 0 lifted, 1 hbrs
c [basicprobe-3-2] 795 sched 6%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-3-2] fully completed probing
c [basicprobe-3-2] removed 0 variables, found 7 hbrs
c [cgrclsr-4] limit 1000000 penalty 3 = 3 + 0
c [cgrclsr-4] all 12398 free variables schedulable
c [cgrclsr-4] fully completed congruence closure
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 2 transitive binary clauses
c [block-5] scheduling all variables this time
c [block-5] scheduled 12398 variables 100%
c [block-5] limit of 100000000 steps penalty 3 = 3 + 0
c [block-5] fully completed
c [block-5] transition to [ all 0 rem 0 ] state
c [block-5] eliminated 2 blocked clauses
c [block-5] 2 < 1/1000 * 267865 = 267 considered unsuccessful
c [cce-5] limit of 51942604 steps penalty 3 = 3 + 0
c [cce-5-1] incomplete large round (ACCE)
c [cce-5-1] allowing another 25971302 steps for small clauses
c [cce-5] scheduling 10076 clauses = 353 binary + 9723 ternary
c [cce-5] tried to eliminate 10076 small clauses 100%
c [cce-5] eliminated 9 small clauses 0%
c [cce-5] eliminated 9 ternary clauses 0%
c [cce-5-1] eliminated 9 small clauses in 30588549 steps
c [cce-5-1] completed small round (ACCE)
c [cce-5-1] eliminated 9 covered clauses in round 1
c [cce-5-2] eliminated 275 clauses out of 92504 (0%) of length 6
c [cce-5-2] incomplete large round (ACCE)
c [cce-5-2] eliminated 275 large clauses in 21354056 steps
c [cce-5-2] allowing another 10677028 steps for small clauses
c [cce-5] scheduling 10067 clauses = 353 binary + 9714 ternary
c [cce-5] tried to eliminate 10067 small clauses 100%
c [cce-5-2] completed small round (ACCE)
c [cce-5-2] eliminated 275 covered clauses in round 2
c [cce-5-3] incomplete large round (ACCE)
c [cce-5-3] allowing another 3033186 steps for small clauses
c [cce-5] scheduling 10067 clauses = 353 binary + 9714 ternary
c [cce-5] tried to eliminate 6622 small clauses 66%
c [cce-5-3] incomplete small round (ACCE)
c [cce-5-3] eliminated 0 covered clauses in round 3
c [cce-5] eliminated 284 covered clauses in TOTAL during 3 rounds
c [elim-6] scheduling all variables this time
c [elim-6] scheduled 12398 variables 100%
c [elim-6] limit of 100000000 steps penalty 3 = 3 + 0
c [elim-6] incomplete 3683 not tried 30% in round 1
c [elim-6] transition to [ all 1 rem 1 ] state
c [elim-6] eliminated 3 = 0% variables out of 12398
c [elim-6] 3 < 1/1000 * 12398 = 12 considered unsuccessful
c [rephase-8] after 5054242 conflicts (new increment 2560000, next 7614242)
c [flushphases] 0 phases reset
c [simplification-12] removed 3 variables 0.0% (12395 remain 95%)
c [simplification-12] removed 486 irredundant clauses 0.2% (267379 remain 87%)
c [simplification-12] maximum reduction of 0% = max (0%, 0%)
c [simplification-12] full geometric conflict interval increment 1000000
c [simplification-12] conflict interval soft limit 1000000 reached
c [simplification-12] new conflict interval 1000000
c [simplification-12] penalized conflict interval 1000000 = 1 * 1000000
c [simplification-12] new conflict limit 6054242
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  693.5   12395   267379   5102721  204516  12838   321  42 26.2 436.5   42
c -  698.3   12395   267379   5177737  205722  12855   321  43 26.3 437.1   42
c -  702.8   12395   267379   5252954  207223  12871   321  39 26.2 437.7   43
c -  709.0   12395   267379   5327460  209594  12892   321  27 26.4 438.1   43
c -  717.0   12395   267379   5401108  212502  12913   321  31 26.6 438.6   42
c -  728.9   12395   267379   5472724  213131  12913   321  33 26.8 438.9   42
c -  741.9   12395   267379   5544776  213773  12914   321  34 27.1 439.3   44
c -  754.2   12395   267379   5620852  217038  12945   321  37 27.5 439.8   42
c R  755.4   12395   267379   5632454  228279  12945   321  28 27.6 439.9   55
c -  763.0   12395   267379   5699722  218651  13061   322  38 27.5 439.0   43
c -  773.1   12395   267379   5777201  219161  13062   322  38 27.6 439.1   41
c -  778.2   12395   267379   5860294  220225  13066   322  39 27.6 439.4   41
c -  783.5   12395   267379   5939938  220891  13069   322  41 27.6 439.8   64
c -  793.9   12395   267379   6023704  223543  13197   322  41 27.4 438.3   44
c 
c [simplification-13] limit of 6054242 conflicts hit after 6054243 conflicts
c [ternres-11] limit 200000000 with penalty 0 = 0 + 0
c [ternres-11] all 12395 free variables schedulable
c [ternres-11] 38 ternary resolvents (2 bin, 36 trn)
c [ternres-11] fully completed ternary resolution
c [lift-5] limit 2500000 with penalty 3 = 3 + 0
c [lift-5] using 1007 probes 8%
c [lift-5-1] found 0 units 0 impls in round 1
c [lift-5-2] found 0 units 0 impls in round 2
c [lift-5-3] found 0 units 0 impls in round 3
c [lift-5-4] found 0 units 0 impls in round 4
c [lift-5-5] found 0 units 0 impls in round 5
c [lift-5] 0 units, 0 impls, 0 eqs in 6 rounds
c [lift-5] 6914 variables remain 56% (5481 retained)
c [cliff-5] limit of 12500000 steps penalty 3 = 3 + 0
c [cliff-5] failed 0, lifted 0
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 1 transitive binary clauses
c [simplification-13] removed 0 variables 0.0% (12395 remain 95%)
c [simplification-13] removed 0 irredundant clauses 0.0% (267379 remain 87%)
c [simplification-13] maximum reduction of 0% = max (0%, 0%)
c [simplification-13] full geometric conflict interval increment 1000000
c [simplification-13] new conflict interval 2000000
c [simplification-13] penalized conflict interval 2000000 = 1 * 2000000
c [simplification-13] new conflict limit 8054243
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  808.2   12395   267379   6105208  225921  13304   323  15 27.3 437.1   45
c -  835.4   12395   267379   6186317  229982  13330   323  28 27.7 437.0   46
c -  863.5   12395   267379   6268855  233017  13363   323  18 27.8 436.6   46
c -  872.1   12395   267379   6352954  235103  13435   323  16 27.8 436.2   46
c -  886.4   12395   267379   6439291  237913  13550   323  16 27.6 434.0   46
c -  912.7   12395   267379   6524375  241990  13577   323  36 27.9 434.1   46
c -  917.1   12395   267379   6609730  242883  13581   323  41 27.9 434.7   45
c -  922.7   12395   267379   6694779  243776  13584   323  40 27.9 435.2   45
c -  930.8   12395   267379   6777964  244630  13590   323  39 28.0 435.7   45
c -  943.2   12395   267379   6858914  245351  13591   323  36 28.6 436.3   45
c -  953.2   12395   267379   6941966  246310  13593   323  33 28.8 436.8   46
c -  966.2   12395   267379   7028166  248503  13639   323  24 28.8 436.0   47
c -  984.3   12395   267379   7114091  250706  13672   323  34 28.9 434.8   47
c
c CAUGHT SIGNAL 15 SIGTERM
c
c s UNKNOWN
c bate: 0 basic ate = 0 trn 0% + 0 lrg 0% in 0 updates
c bcas: 4 count, 0 added (0 skipped), 658249 steps
c bkwd: tried 24771 clauses, 48550 lits, 1.96 lits/clause
c bkwd: checked 3067331 occs, 123.83 occs/clause, 63.18 occs/lit
c bkwd: subsumed 0 binary, 0 ternary, 967 large
c bkwd: strengthened 0 binary, 2 ternary (100% self), 78 large (0% self)
c blkd: 5 bces, 652 removed, 24639579 resolutions, 43203410 steps
c blkd: 90 blocking literals 0%, 0 pure
c bvas: 0 bvas, 0 added, 0 removed
c card: 4 count, 0 units, 0 am1, 10919032 steps
c card: 0 rescheduled, 0 eliminated, 0 resolved, 675 subsumed
c card: 9 at-most-one constraints found, average size 3.00
c card: 9 at-most-one constraints used 100%, average size 3.00
c card: 22 at-most-two constraints found, average size 4.09
c card: 22 at-most-two constraints used 100%, average size 4.09
c cces: 5 cces, 31442 eliminated, 31442 ate 100%, 0 abce 0%
c cces: 0 probed, 0 lifted, 0 failed
c cces: 0 cached, 0 rsz, 0 cols 0%, 0 srch, 0 hits 0%
c cgrs: 4 count, 1816742 esteps, 38917 csteps
c cgrs: 0 eqs, 0 units
c cgrs: 0 matched (0 ands 0%, 0 xors 0%, 0 ites 0%)
c cgrs: 0 simplified (0 ands 0%, 0 xors 0%, 0 ites 0%)
c cgrs: 1189 extracted (23 ands 2%, 1133 xors 95%, 33 ites 3%)
c clff: 5 cliffs, 0 lifted, 1 failed
c clff: 2475716 decisions, 43535821 steps
c clls: 1 sat, 0 simp, 0 freeze, 0 melt
c clls: 3617008 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 53 gcs, 0 rescored clauses, 3562 rescored vars
c dcps: 24 decompositions, 53 equivalent 0%
c deco: 5689 decision-only clauses 0%, 46% reduction
c decs: 96034098 decision, 0 random 0.000%, 0 flipped 0.000%
c decs: 3930582 flipped 4.093% (in 6981 phases)
c elms: 6 elims, 557 eliminated 4%
c elms: 7 rounds, 1.2 rounds/bve
c elms: 545 small 98%, 12 large 2%
c elms: 2947 tried small, 545 succeeded 18%, 2402 failed 82%
c elms: 2187 subsumed, 4866 strengthened, 3 blocked
c elms: 2913559 copies, 8476942 resolutions, 856005 ipos
c elms: 526254 subchks, 250945 strchks
c frcs: 0 computed, 0 - 0 average min-cut range
c gaus: 4 extractions, 7053 extracted, 5.0 size, 5 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 1 gc, 18320020 steps, 9160010 extr 50%, 263635 elim 1%
c glue: 29.2 orig avg, 29.1 real avg, 4.5 scaled avg
c glue: 0 maxscaledglue=15 (0%)
c hbrs: 105 = 19 simple + 75 trn 18% + 11 lrg 71%, 49 sub 10%
c hght: 435 average, 14.90 height/glue
c ints: 173307 luby (53606086 steps), 0 inout (0 steps)
c lift: 5 phases, 107419 probed (35813 level1 33%, 71606 level2 67%)
c lift: 1 units, 2 equivalences, 33 implications
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 6771284 clauses, 75.0 length
c lrnd: 2052690 uips 30%, 3998093 flips 59%
c mega: 0 count, 0 failed, 0 rounds
c mins: 508180527 learned lits, 1% minimized
c mins: 6062853 mins 90%, 88 bin 0%, 702654 size 10%, 5689 deco 0%
c move: moved 6771284, 11 bin 0%, 1407 trn 0%, 0 lrg 0%
c otfs: str 1255103 dyn (1244616 red, 10487 irr) 408266 drv 33%, 846837 rst 67%
c otfs: sub 16050 dyn (16050 red, 0 irr)
c phas: 9 computed, 12891 set, 5041 pos (39%), 7850 neg (61%)
c prbs: 3 basic, 10387 probed, 3 failed, 0 lifted
c prbs: 3 simple, 28206 probed, 4 failed, 1 eqs
c prbs: 3 treelook, 2867 probed, 0 failed, 0 lifted
c prps: 821130312 props, 9 props/dec
c prps: 100% srch, 0% simp, 0% lkhd
c psns: 114466763 searches, 11019794 hits, 10% 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: 156 count, 0 reset, 5 acts 3%
c reds: 0 geom 0%, 0 glue useless 0%
c reds: 0 memlim 0%, 156 arith 100%, 0 double 0%
c rmbd: 12 removed, 2 red 17%
c rphs: 8 recomputed phases
c rsts: 88952 restarts 51%, 84355 skipped 49%
c rsts: 0 saturating 0%, 74129 agile 88%, 10226 reuse 12%
c rsts: 79.8 avg interval, 79.8 scaled, 1.0 factor
c rsts: 22397 kept 25.2% average 50.4%
c simp: 13 count (13 confs 100%, 0 irr 0%, 0 vars 0%)
c subl: 6771284 count (12780487 tried 1.9), 84220 sub out of 6766687 (1.2%)
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: 0 count
c tops: 403 fixed 3%, 0 its, 0.00 confs/it
c trvs: 53528767453 traversals, 100% srch, 0% simp, 0% lkhd
c trvs: 65.3 search traversals per propagation, 7449.3 per conflict
c trvs: 1.8 search traversals per search visit
c trds: 9 transitive reductions, 27 removed, 0 failed
c trds: 221023 nodes, 4949 edges, 6128 steps
c trim: 2117785 words, 8.1 MB
c trnr: 11 count, 39 bin, 422 trn, 21524932 steps
c unhd: 5 count, 8 rounds, 5148182 steps
c unhd: 0 non-trivial sccs of average size 0.0
c unhd: 0 units, 0 bin, 0 trn, 0 lrg
c unhd: 9 failed, 9 stamp, 0 lits, 0 bin, 0 trn, 0 lrg
c unhd: 1061 tauts, 0 bin 0%, 769 trn 72%, 288 lrg 27%
c unhd: 1061 tauts, 4 stamp 0%, 507 red 48%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 1654 str, 0 bin 0%, 24 trn 1%, 1630 lrg 99%, 1592 red 96%
c vars: 12395 remaining 92% and 1013 removed 8% out of 13408
c vars: 403 fixed 3%, 557 eliminated 4%, 53 equivalent 0%
c vsts: 30542381719 visits, 100% srch, 0% simp, 0% lkhd
c vsts: 37.3 search visits per propagation, 4247.7 per conflict
c wchs: 11225626663 pushed, 34433042 enlarged, 453 defrags
c 
c scaledglue  added       reduced       forcing      resolved     conflicts
c 
c all   6766687 100   6343882 100 195970878 100  57680675 100   3530564 100
c 
c  0     181030   3         0   0 113770070  58  19831976  34    745087  21 
c  1     378615   6    289795   5  44632847  23< 10334529  18    544372  15 
c  2    1080064  16   1065915  17  15661660   8   7275787  13<   542415  15 
c  3    1155642  17   1136747  18   9199578   5   6344181  11    486676  14<
c  4    1151028  17<  1127868  18   4951723   3   4484597   8    327848   9 
c  5     868731  13    842387  13<  2882388   1   2924289   5    166394   5 
c  6     578612   9    563450   9   1689776   1   1946870   3    162404   5 
c  7     382542   6    373101   6    996854   1   1252999   2    123395   3 
c  8     307427   5    299469   5    983517   1   1156589   2     99698   3 
c  9     242857   4    233805   4    420016   0    708753   1     93338   3 
c 10     260213   4    247315   4    424742   0    802427   1    131552   4 
c 11     149102   2    137277   2    292876   0    517553   1     90713   3 
c 12      13343   0     12133   0     24213   0     49007   0     10670   0 
c 13      17481   0     14620   0     40618   0     51118   0      6002   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             4.5           4.6           0.9           2.2           3.2
c std             2.6           2.5           1.6           2.6           3.1
c 
c  117.218  12% analysis
c   89.273   9% decide
c   19.874   2% bump
c   14.191   1% mincls
c    9.772   1% defrag
c    8.635   1% cce
c    8.447   1% restart
c    5.237   1% elim
c    4.670   0% gc
c    3.360   0% reduce
c    3.186   0% decomp
c    3.164   0% block
c    2.705   0% probe
c    2.473   0% cliff
c    0.897   0% lift
c    0.730   0% gauss
c    0.636   0% cgrclsr
c    0.616   0% unhide
c    0.461   0% bca
c    0.414   0% phase
c    0.225   0% card
c    0.214   0% backward
c    0.149   0% ternres
c    0.044   0% transred
c    0.017   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    0.000   0% tabularasa
c ----------------------------------
c    0.893   0% probe simple     33%
c    0.819   0% probe basic      30%
c    0.993   0% probe tree-look  37%
c ==================================
c    1.489   0% preprocessing     5%
c   27.855   3% inprocessing     95%
c ==================================
c   29.344   3% simplifying
c  970.302  97% search
c ==================================
c  999.646 100% all
c 
c 96034098 decisions, 96068.1 decisions/sec
c 7179550 conflicts, 7182.1 conflicts/sec
c 821130312 propagations, 0.8 megaprops/sec
c 999.6 seconds, 128.2 MB
c
c CAUGHT SIGNAL 15 SIGTERM
c
c launch: done
