c launch: /data/cnf/sc2014/app/UTI-20-5p1.cnf.bz2
c host: atom30
c Lingeling SAT Solver
c 
c Version b7ztzvv 37b745a123cb37a24a48e992b1e2073d5d4068bb
c 
c Copyright (C) 2010-2014 Armin Biere JKU Linz Austria.
c All rights reserved.
c 
c released Sat May  2 12:17:55 CEST 2015
c compiled Sat May  2 12:17:55 CEST 2015
c 
c gcc (Ubuntu 4.8.2-19ubuntu1) 4.8.2
c -Wall -O3 -I../yalsat -I../druplig -DNLGLOG -DNDEBUG -DNCHKSOL
c Linux fmvx1 3.13.0-51-generic x86_64
c 
c piping '/data/cnf/sc2014/app/UTI-20-5p1.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/UTI-20-5p1.cnf.bz2
c no embedded options
c found 'p cnf 225926 1207249' header
c read 225926 variables, 1207249 clauses, 2914329 literals in 0.00 seconds
c
c --abstime=0
c --bate=1
c --batewait=2
c --bca=1
c --bcaddlimldscale=2
c --bcamaxeff=10000000
c --bcaminuse=100
c --bcawait=2
c --bkwdscale=100
c --bkwdroundlim=7
c --bkwdresched=1
c --blkboost=10
c --blkboostvlim=10000000
c --blkclslim=1000000
c --blklarge=1
c --blkmaxeff=800000000
c --blkmineff=50000000
c --blkocclim1=100000
c --blkocclim=1000000
c --blkocclim2=10000
c --blkreleff=100
c --blkresched=1
c --blkrtc=0
c --blksmall=1
c --blksuccessmaxwortc=6
c --blksuccessrat=100
c --block=1
c --blockwait=1
c --boost=1
c --bumpsimp=1
c --card=1
c --cardcut=2
c --cardexpam1=3
c --cardglue=0
c --cardignused=0
c --cardmaxeff=300000000
c --cardmaxlen=1000
c --cardmineff=2000000
c --cardminlen=3
c --cardocclim1=300
c --cardocclim2=15
c --cardreleff=5
c --cardreschedint=10
c --carduse=2
c --cardwait=0
c --cce2wait=1
c --cce=3
c --cceateint=2
c --cceboost=10
c --cceboostdel=3
c --cceboostint=5
c --cceboostvlim=10000000
c --cce3wait=2
c --ccemaxround=3
c --ccemaxeff=2147483647
c --ccemineff=30000000
c --ccereleff=50
c --ccertc=0
c --ccertcint=15
c --ccertcintvlim=2000000
c --ccesuccessrat=100
c --ccewait=2
c --clim=-1
c --compact=0
c --deco=1
c --decolim=100
c --deco1opt=1
c --decompose=1
c --defragfree=50
c --defragint=10000000
c --delmax=10
c --dlim=-1
c --druplig=0
c --drupligcheck=0
c --drupligtrace=0
c --drupligtraceorig=0
c --elim=1
c --elmaxeff=800000000
c --elmblk=1
c --elmblkwait=1
c --elmboost=20
c --elmboostdel=3
c --elmboostint=5
c --elmboostvlim=4000000
c --elmclslim=1000000
c --elmfull=0
c --elmineff=20000000
c --elmlitslim=200
c --elmocclim1=1000
c --elmocclim=1000000
c --elmocclim2=100
c --elmoccsumforced=0
c --elmreleff=200
c --elmresched=0
c --elmroundlim=3
c --elmrtc=0
c --elmrtcint=10
c --elmrtcintvlim=500000
c --elmsuccessmaxwortc=4
c --elmsuccessrat=100
c --exitonabort=0
c --factmax=100000
c --factor=3
c --gauss=1
c --gaussexptrn=1
c --gaussextrall=1
c --gaussmaxeff=50000000
c --gaussmaxor=20
c --gaussmineff=2000000
c --gaussreleff=2
c --gausswait=2
c --gluekeep=4
c --gluekeepsize=15
c --gluescale=4
c --hbrdom=2
c --import=1
c --incredcint=1
c --incredconfslim=0
c --incsavevisits=0
c --inprocessing=1
c --irrlim=1
c --jwhred=1
c --keepmaxglue=1
c --keepmaxglueint=100
c --lhbr=1
c --lkhd=2
c --locs=0
c --locsbanner=0
c --locsclim=1000000
c --locsboost=2
c --locscint=10000
c --locset=2
c --locsexport=1
c --locsmaxeff=100000
c --locsmineff=1000
c --locsred=0
c --locsreleff=5
c --locsrtc=0
c --locsvared=100
c --locswait=2
c --maxscaledglue=15
c --memlim=-1
c --minimize=2
c --minlocalgluelim=200
c --minlocalsizelim=3000
c --minrecgluelim=100
c --minrecsizelim=1000
c --norestartsatlimlo=85
c --move=2
c --otfs=1
c --penmax=4
c --phase=0
c --phaseluckfactor=200
c --phaselucklim=100
c --phaseluckmaxround=10
c --phasesave=1
c --plain=0
c --plim=-1
c --poison=1
c --prbasic=1
c --prbasicmaxeff=400000000
c --prbasicmineff=1000000
c --prbasicreleff=50
c --prbasicroundlim=8
c --prbasicrtc=0
c --prbrtc=0
c --prbsimple=2
c --prbsimpleboost=10
c --prbsimpleliftdepth=2
c --prbsimplemaxeff=200000000
c --prbsimplemineff=2000000
c --prbsimplereleff=40
c --prbsimplertc=0
c --probe=1
c --promote=1
c --promotegluelim=8
c --pure=1
c --quatres=1
c --quatreswait=2
c --queuesort=1
c --queuesortjwh=0
c --randec=0
c --randecint=1000
c --redcls=1
c --redclsglue=6
c --redclsmaxdec=5
c --redclsmaxdepth=10
c --redclsmaxlrg=10
c --redclsmaxprops=100
c --redclsatlimlo=0
c --redclsatlimhi=100
c --redclsize=30
c --redclstype=4
c --reducefixed=0
c --reduceinc=1000
c --reduceinit=50000
c --reduce=1
c --restart=4
c --restartglcint=10
c --restartglclim=115
c --restartinit=0
c --restartint=5
c --restartpen=1
c --retirenb=1
c --retireint=4
c --retiremin=1
c --reusetrail=0
c --rmincpen=4
c --rstinoutinc=110
c --satlimdelay=10000
c --scincinc=200
c --scincincsatlimhi=100
c --scincincdelta=10
c --scincincincint=100000
c --scincincmin=200
c --scincincmode=1
c --scoreshift=0
c --scoreresetint=2147483647
c --seed=0
c --simpbintinc=100
c --simpbintinclim=10000
c --simpcintdelay=2000
c --simpcintinc=20000
c --simpcintincdiv=1
c --simpcintmaxhard=10000000
c --simpcintmaxsoft=1000000
c --simpincdelmaxfact=50
c --simpincdelmaxmin=10000
c --simpinitdelay=0
c --simpintsizepen=0
c --simpen=0
c --simpidiv=3
c --simpiscale=100
c --simpitdelay=10
c --simpitintinc=10
c --simpitintinclim=1000
c --simplify=2
c --simprtc=5
c --simptintinc=1000
c --simptintinclim=10000
c --simpvarchg=100
c --simpvarlim=100
c --sizemaxpen=5
c --sizepen=1000000
c --sleeponabort=0
c --smallirr=90
c --smallve=1
c --smallvevars=10
c --smallvewait=0
c --sortlits=0
c --subl=9
c --sweep=1
c --sweepboost=10
c --sweepboostdel=4
c --sweepboostint=7
c --sweepboostvlim=1000000
c --sweepfacdec=10
c --sweepforgive=2
c --sweepirr=3
c --sweepmaxeff=200000000
c --sweepmaxdec=10000
c --sweepmaxround=3
c --sweepmindec=100
c --sweepmineff=1000000
c --sweepred=3
c --sweepreleff=3
c --sweeprtc=0
c --sweeprtcint=14
c --sweeprtcintvlim=100000
c --sweepsuccessmaxwortc=6
c --sweepsuccessrat=1000
c --sweepwait=2
c --synclsall=1
c --synclsglue=8
c --synclsint=100
c --synclslen=40
c --syncunint=111111
c --termint=122222
c --ternres=1
c --ternresboost=5
c --ternresrtc=0
c --ternreswait=2
c --transred=1
c --transredwait=2
c --trapiflush=0
c --trdmaxeff=2000000
c --trdmineff=100000
c --trdreleff=10
c --treelook=1
c --treelookboost=10
c --treelookfull=0
c --treelookmaxeff=50000000
c --treelookmineff=300000
c --treelookreleff=2
c --treelookrtc=0
c --trep=1
c --trepint=55555
c --trnreleff=10
c --trnrmaxeff=200000000
c --trnrmineff=4000000
c --unhdatrn=2
c --unhdextstamp=1
c --unhdhbr=0
c --unhdlnpr=3
c --unhdmaxeff=20000000
c --unhdmineff=100000
c --unhdreleff=2
c --unhdroundlim=20
c --unhide=1
c --unhidewait=0
c --usedtwice=1
c --vsidsdint=256
c --wait=1
c --waitmax=4
c --witness=0
c --check=0
c --log=-1
c --profile=1
c --profilelong=1
c --verbose=1
c [freezer] frozen 0 variables out of 214523 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 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c *    0.0  214523  1195096         0       0      0     0    0     0   53   0%      0    0    0    0    0%
c 
c [simplification-1] limit 0 conflicts (hard 0) hit after 0 conflicts
c [card-1] limit 2000000 penalty 0 = 0 + 0
c [card-1] found 6247 at-most-one constraints of average size 5.8
c [card-1] no at-most-two constraint found
c [card-1] using previous limit 2000000 for elimination
c [card-1] 6247 out of 6247 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 51720 variables
c [simpleprobe-1] all 174206 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 1287 variables
c [simpleprobe-1] 15114 variables remain 9% (157805 retained 91%)
c [simpleprobe-1] removed 1287 variables, found 20918 hbrs, 291 units
c [unhide-1] limit 57511 based on 920186 irredundant clauses
c [unhide-1-1] 0 units, 2275 failed, 9927 tauts, 0 hbrs, 9683 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 171886 variables 100%
c [elim-1] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-1] rescheduling of touched variables disabled
c [elim-1] incomplete 47285 not tried 28% in round 1
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 66343 = 39% variables out of 171886 scheduled
c [elim-1] considered successful since not run to completion yet
c [phase-count-1] 762627 negative 99.2% of 768449 except 5822 0.8%
c [phase-count-1] 617596 positive 80.4% of 768449 except 150853 19.6%
c [phase-count-1] less non-negative clauses 5822 than limit 76800 (10.0%)
c [phase-count-1] non-pos/non-neg = 150853/5822 = 25.91 >= 2.00 = 200/100
c [lucky-phase-1] forcing lucky phase -1
c [phase-1] phase bias: 0 positive 0%, 105543 negative 100%
c [sort-queue-1] sorted 105543 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 105543 (100%)
c [score-dist-1] max exp 0, different 1 (100%)
c [score-dist-1] median active exp 0, avg 0.0
c [simplification-1] removed 73539 variables 41.1% (105543 remain 49%)
c [simplification-1] removed 426647 irredundant clauses 35.7% (768449 remain 64%)
c [simplification-1] maximum reduction of 41% = max (41%, 36%)
c [simplification-1] large reduction 41% >= 5% limit
c [simplification-1] next conflict interval 1000 = 2000/2
c [simplification-1] penalized conflict interval 1000 = 1 * 1000
c [simplification-1] hard conflict limit 11000 (soft 1000 + delta 10000)
c [simplification-1] new conflict limit 1000 (hard 11000)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i    4.6  105542   768449         2       1      0 14308    0     0   49   0%      0    0    0    0 25500%
c i    4.6  105539   768449        12       5      2 14311    0     1   50   1%      0    1    0    0 25090%
c i    4.6  105475   768449        13       5      2 14311    0     1   50   1%      0    1    0    0 24993%
c i    4.6  105315   768449        18       8      2 14312    0     1   50   1%      0    1    0    0 24766%
c i    4.7  104993   768449        21       8      2 14314    0     1   50   1%      0    1    0    0 24537%
c i    4.7  104981   768449        27      10      3 14316    0     2   50   1%      0    2    0    0 24460%
c i    4.7  104144   768449        59      25     13 14322    0     4   50   1%      0    4    0    0 22910%
c i    4.8  103667   768449        79      42     13 14323    0     6   50   1%      0    6    1    0 23307%
c i    4.8  103655   768449        87      47     13 14325    0     7   50   1%      0    7    1    0 22821%
c i    4.8  102261   768449        88      47     13 14325    0     7   50   1%      0    7    1    0 22732%
c 
c [simplification-2] limit of 10 iterations hit after 10 iterations
c [decomp-3] removed 3406 variables
c [simpleprobe-2] 14151 schedulable variables 14%
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [simpleprobe-2] 17134 variables remain 17% (85003 retained 83%)
c [simpleprobe-2] removed 0 variables, found 3731 hbrs, 0 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 66547 literals 33%
c [treelook-1] scheduling used 484575 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 305583 steps
c [treelook-1] 66541 literals remain 33%
c [treelook-1] 65464 variables remain to probed next time 64%
c [treelook-1] removed 2 variables, found 2063 hbrs
c [basicprobe-1] limit 5956880 based on 744610 irredundant clauses
c [basicprobe-1-0] 29484 probes remain 35% after last round
c [basicprobe-1-0] 60 units = 60 failed (100%) + 0 lifted (0%)
c [basicprobe-1-0] removed 16757 variables, found 17299 hbrs
c [unhide-2] limit 50000 with penalty 1 = 0 + 1
c [unhide-2-2] 2 units, 4490 failed, 5872 tauts, 0 hbrs, 1057 literals
c [elim-2] 41884 variables 50% will be scheduled this time
c [elim-2] scheduled 41884 variables 50%
c [elim-2] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-2] rescheduling of touched variables disabled
c [elim-2] incomplete 12083 not tried 14% in round 1
c [elim-2] transition to [ all 0 rem 1 ] state
c [elim-2] eliminated 306 = 1% variables out of 41884 scheduled
c [elim-2] considered successful since not run to completion yet
c [phase-count-2] 576922 negative 99.0% of 582757 except 5835 1.0%
c [phase-count-2] 466461 positive 80.0% of 582757 except 116296 20.0%
c [phase-count-2] less non-negative clauses 5835 than limit 58200 (10.0%)
c [phase-count-2] non-pos/non-neg = 116296/5835 = 19.93 >= 2.00 = 200/100
c [lucky-phase-2] forcing lucky phase -1
c [phase-2] phase bias: 0 positive 0%, 8125 negative 100%
c [sort-queue-2] sorted 83485 enqueued variables after 88 conflicts
c [score-dist-2] active 0 (0%), one 3221 (4%), zero 80264 (96%)
c [score-dist-2] max exp 1, different 2 (100%)
c [score-dist-2] median active exp 0, avg 0.0
c [simplification-2] removed 18757 variables 18.3% (83485 remain 39%)
c [simplification-2] removed 185692 irredundant clauses 24.2% (582757 remain 49%)
c [simplification-2] maximum reduction of 24% = max (18%, 24%)
c [simplification-2] forced so keeping old conflict interval 0
c [simplification-2] conflict limit remains at 1033 (hard 11000)
c [simplification-2] new iteration interval 100
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i    7.6   83484   582757       102      46     16 21971    0     8   40   1%      0    8    1    0 22079%
c i    7.6   83478   582757       125      60     19 21976    0     9   40   1%      0    9    2    0 21105%
c i    7.6   83464   582757       143      72     21 21979    0     9   40   1%      0    9    2    0 20060%
c i    7.7   83457   582757       199     111     26 21988    0    10   40   2%      0   10    3    0 19138%
c i    7.7   83439   582757       233     137     30 21990    0    12   40   3%      0   12    5    0 20488%
c i    7.8   82663   582757       335     218     36 22004    1    14   40   4%      0   14    6    0 16118%
c i    7.8   82004   582757       362     242     36 22006    1    15   40   4%      0   15    7    0 15450%
c i    7.8   81943   582757       364     243     36 22006    1    15   40   4%      0   15    7    0 15359%
c i    7.8   81796   582757       381     256     37 22008    1    16   40   4%      0   16    6    0 14650%
c i    7.8   81652   582757       402     267     38 22016    1    16   40   4%      0   16    6    0 13634%
c i    7.9   81645   582757       426     281     44 22019    1    16   40   4%      0   16    6    0 12712%
c i    7.9   81596   582757       458     298     50 22027    1    16   40   4%      0   16    5    0 11633%
c i    7.9   81546   582757       538     362     54 22038    1    17   40   5%      0   17    7    0 11907%
c i    8.0   81538   582757       654     451     65 22051    1    20   40   6%      0   20    8    0 10370%
c i    8.0   81530   582757       684     474     69 22053    1    20   40   6%      0   20    9    0 10453%
c i    8.0   81521   582757       712     496     70 22055    1    21   40   7%      0   21   11    0 11381%
c i    8.0   81511   582757       739     515     71 22061    1    22   40   7%      0   22   11    0 10564%
c 
c [simplification-3] limit of 117 binary hit after 117 binaries
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 3293 at-most-one constraints of average size 4.5
c [card-2] no at-most-two constraint found
c [card-2] using previous limit 1000000 for elimination
c [card-2] 3293 out of 3293 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [decomp-6] removed 2812 variables
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] scheduled 49731 literals 31%
c [treelook-2] scheduling used 307467 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] used 311241 steps
c [treelook-2] 49700 literals remain 31%
c [treelook-2] 35673 variables remain to probed next time 44%
c [decomp-7] removed 16 variables
c [treelook-2] removed 17 variables, found 2060 hbrs
c [unhide-3] limit 100000 with penalty 0 = 0 + 0
c [unhide-3-3] 0 units, 1432 failed, 12966 tauts, 0 hbrs, 542 literals
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 79676 variables 100%
c [elim-3] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-3] rescheduling of touched variables disabled
c [elim-3] incomplete 15118 not tried 19% in round 1
c [elim-3] transition to [ all 1 rem 1 ] state
c [elim-3] eliminated 3238 = 4% variables out of 79676 scheduled
c [elim-3] considered successful since not run to completion yet
c [phase-count-3] 532732 negative 99.0% of 538327 except 5595 1.0%
c [phase-count-3] 432015 positive 80.3% of 538327 except 106312 19.7%
c [phase-count-3] less non-negative clauses 5595 than limit 53800 (10.0%)
c [phase-count-3] non-pos/non-neg = 106312/5595 = 19.00 >= 2.00 = 200/100
c [lucky-phase-3] forcing lucky phase -1
c [phase-3] phase bias: 0 positive 0%, 1299 negative 100%
c [sort-queue-3] sorted 76438 enqueued variables after 858 conflicts
c [score-dist-3] active 0 (0%), one 17323 (23%), zero 59115 (77%)
c [score-dist-3] max exp 1, different 2 (100%)
c [score-dist-3] median active exp 0, avg 0.0
c [simplification-3] removed 5032 variables 6.2% (76438 remain 36%)
c [simplification-3] removed 44430 irredundant clauses 7.6% (538327 remain 45%)
c [simplification-3] maximum reduction of 8% = max (6%, 8%)
c [simplification-3] forced so keeping old conflict interval 0
c [simplification-3] conflict limit remains at 1038 (hard 11000)
c [simplification-3] new binary interval 1000
c 
c [simplification-4] limit 1038 conflicts (hard 11000) hit after 1038 conflicts
c [decomp-8] removed 1 variables
c [basicprobe-2] limit 4306584 based on 538323 irredundant clauses
c [basicprobe-2-0] 27940 probes remain 37% after last round
c [basicprobe-2-0] 63 units = 63 failed (100%) + 0 lifted (0%)
c [basicprobe-2-0] removed 336 variables, found 12189 hbrs
c [unhide-4] limit 100000 with penalty 0 = 0 + 0
c [unhide-4-4] 18 units, 997 failed, 2099 tauts, 0 hbrs, 1341 literals
c [elim-4] 11916 variables 16% will be scheduled this time
c [elim-4] scheduled 11916 variables 16%
c [elim-4] boosting limit by 20
c [elim-4] limit of 400000000 steps penalty 0 = 0 + 0
c [elim-4] rescheduling of touched variables disabled
c [elim-4-1] no variable eliminated in round 1 in 25916033 steps
c [elim-4] fully completed in 1 rounds
c [elim-4] transition to [ all 0 rem 0 ] state
c [elim-4] eliminated 0 = 0% variables out of 11916 scheduled
c [phase-count-4] 523286 negative 98.9% of 528881 except 5595 1.1%
c [phase-count-4] 423762 positive 80.1% of 528881 except 105119 19.9%
c [phase-count-4] less non-negative clauses 5595 than limit 52800 (10.0%)
c [phase-count-4] non-pos/non-neg = 105119/5595 = 18.79 >= 2.00 = 200/100
c [lucky-phase-4] forcing lucky phase -1
c [phase-4] phase bias: 0 positive 0%, 1279 negative 100%
c [sort-queue-4] sorted 75626 enqueued variables after 1038 conflicts
c [score-dist-4] active 0 (0%), one 18797 (25%), zero 56829 (75%)
c [score-dist-4] max exp 1, different 2 (100%)
c [score-dist-4] median active exp 0, avg 0.0
c [simplification-4] removed 812 variables 1.1% (75626 remain 35%)
c [simplification-4] removed 9446 irredundant clauses 1.8% (528881 remain 44%)
c [simplification-4] maximum reduction of 2% = max (1%, 2%)
c [simplification-4] geometric conflict interval increment 6666 = 20000 / 3
c [simplification-4] new conflict interval 6666
c [simplification-4] penalized conflict interval 6666 = 1 * 6666
c [simplification-4] hard conflict limit 17704 (soft 7704 + delta 10000)
c [simplification-4] new conflict limit 7704 (hard 17704)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   11.9   75625   528881      1083     714     86 24796    2    33   38   7%      1   32   11    0 6902%
c i   11.9   75622   528881      1100     724     88 24799    2    33   38   7%      1   33   11    0 6565%
c i   12.0   75611   528881      1238     827     97 24823    2    36   38   7%      1   36    8    0 4793%
c i   12.0   75563   528881      1246     831     97 24825    2    36   38   7%      1   35    8    0 4688%
c i   12.1   75556   528881      1272     846    101 24830    2    37   38   6%      1   37    8    0 4406%
c i   12.1   75545   528881      1299     859    109 24835    2    37   38   6%      1   37    7    0 4067%
c i   12.1   75535   528881      1374     914    115 24842    2    38   38   6%      1   38    7    0 3910%
c i   12.1   75485   528881      1397     933    116 24844    3    39   38   7%      1   38    9    0 4517%
c i   12.1   75476   528881      1398     933    116 24844    3    39   38   7%      1   38    9    0 4500%
c i   12.1   75472   528881      1440     968    117 24848    3    40   38   7%      1   39    9    0 4585%
c i   12.2   75467   528881      1446     972    117 24849    3    40   38   7%      1   39    9    0 4555%
c i   12.2   75461   528881      1449     973    117 24850    3    40   38   7%      1   39    9    0 4505%
c i   12.2   75452   528881      1584    1076    130 24866    3    43   38   7%      1   42   12    0 5135%
c i   12.3   75345   528881      1662    1139    134 24875    3    45   38   7%      1   44   11    0 4756%
c i   12.4   75190   528881      1816    1265    151 24885    3    46   38   7%      1   45    9    0 3617%
c i   12.4   75167   528881      1963    1388    157 24899    4    48   38   8%      1   47   11    0 3892%
c i   12.5   75116   528881      2156    1539    167 24923    4    49   38   8%      1   48   10    0 3230%
c i   12.5   74921   528881      2157    1539    167 24923    4    49   38   8%      1   48   10    0 3217%
c i   12.6   74891   528881      2278    1631    180 24934    4    53   38   9%      1   52   14    0 4046%
c i   12.6   74887   528881      2279    1631    180 24934    4    53   38   9%      1   52   14    0 4031%
c i   12.6   74884   528881      2327    1668    187 24935    5    53   38   9%      1   52   14    0 3930%
c i   12.6   74883   528881      2328    1668    187 24935    5    53   38   9%      1   52   14    0 3914%
c i   12.7   74881   528881      2384    1717    189 24937    5    55   38  10%      1   54   24    0 5858%
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   12.7   74690   528881      2387    1718    189 24938    5    55   38  10%      1   54   24    0 5792%
c i   12.7   74683   528881      2402    1731    189 24939    5    55   38  10%      1   54   23    0 5515%
c i   12.9   74675   528881      3124    2344    224 24983    7    61   38  12%      4   59   18    1 2942%
c i   13.0   74674   528881      3203    2407    232 24989    7    61   38  12%      3   59   15    1 2487%
c i   13.0   74669   528881      3245    2439    236 24992    7    62   38  12%      3   60   14    1 2254%
c i   13.0   74666   528881      3277    2456    242 24998    7    62   38  12%      3   60   13    1 2073%
c i   13.0   74657   528881      3328    2497    244 25004    7    62   38  12%      3   60   11    1 1852%
c i   13.3   74655   528881      3761    2854    276 25037    8    69   38  12%      3   66   14    1 1930%
c i   13.3   74653   528881      3763    2854    276 25038    8    69   38  12%      3   66   14    1 1915%
c i   13.4   74197   528881      3997    3045    298 25056    9    71   38  12%      3   69   16    1 2049%
c i   13.5   74165   528881      4271    3265    312 25076    9    73   39  12%      3   70   14    1 1716%
c i   13.7   74161   528881      4496    3438    326 25106    9    76   39  12%      3   73   12    1 1386%
c i   13.9   74157   528881      4710    3607    341 25132    9    80   39  12%      2   77   15    1 1663%
c i   13.9   74148   528881      4791    3665    346 25142    9    81   39  12%      2   78   14    1 1494%
c i   13.9   74147   528881      4808    3678    347 25143    9    81   39  12%      2   78   13    1 1452%
c i   14.2   74035   528881      5120    3939    367 25162   10    85   39  11%      2   81   12    1 1218%
c i   14.2   74029   528881      5183    3996    368 25165   10    85   39  12%      2   81   16    1 1582%
c i   14.3   74022   528881      5327    4114    378 25176   10    87   39  12%      2   83   14    1 1379%
c i   14.5   74017   528881      5636    4374    395 25200   11    90   39  12%      2   86   18    1 1591%
c i   14.6   74016   528881      5756    4479    398 25204   11    90   39  12%      2   86   22    1 1882%
c i   14.6   74015   528881      5757    4479    398 25204   11    90   39  12%      2   86   22    1 1875%
c i   14.6   74010   528881      5856    4567    403 25207   12    90   39  13%      2   85   24    1 1970%
c i   14.7   74008   528881      5963    4662    403 25217   12    91   39  13%      2   86   22    1 1751%
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   14.8   74000   528881      6111    4772    417 25237   12    94   39  12%      2   89   15    1 1215%
c i   14.8   73865   528881      6113    4773    417 25237   12    94   39  12%      2   89   15    1 1206%
c i   14.9   73792   528881      6293    4934    424 25245   12    96   39  13%      2   91   18    1 1377%
c i   15.2   73585   528881      6477    5080    444 25257   12   103   40  12%      1   97   14    1 1045%
c i   15.2   73435   528881      6487    5087    445 25258   12   103   40  12%      1   97   14    1 1015%
c i   15.2   73427   528881      6539    5127    446 25267   12   103   40  12%      1   98   12    1  922%
c i   15.3   73426   528881      6688    5248    453 25275   13   104   40  12%      1   98   24    1 1723%
c i   15.4   73418   528881      6810    5353    461 25281   13   106   40  12%      1  100   22    1 1526%
c i   15.4   73405   528881      6811    5353    461 25281   13   106   40  12%      1  100   22    1 1520%
c i   15.5   73403   528881      6821    5362    461 25281   13   106   40  12%      1  100   22    1 1488%
c i   15.5   73398   528881      6887    5419    465 25282   13   108   40  12%      1  102   25    1 1664%
c i   15.5   73344   528881      6905    5428    468 25286   13   108   40  12%      1  101   23    1 1565%
c i   15.5   73335   528881      6922    5442    470 25286   13   108   40  12%      1  102   24    1 1610%
c i   15.5   73332   528881      6927    5445    471 25286   13   108   40  12%      1  102   24    1 1602%
c i   15.6   73322   528881      6999    5502    476 25294   13   108   40  12%      1  102   20    2 1318%
c i   15.6   73318   528881      7052    5550    477 25297   13   108   40  12%      1  102   19    2 1232%
c i   15.6   73316   528881      7059    5556    477 25297   13   108   40  12%      1  101   18    2 1203%
c i   15.6   73314   528881      7060    5556    477 25297   13   108   40  12%      1  101   18    2 1199%
c i   15.7   73307   528881      7103    5583    484 25304   13   108   40  12%      1  101   17    2 1110%
c i   15.7   73100   528881      7130    5600    484 25309   13   108   40  12%      1  101   16    2 1032%
c i   15.9   73096   528881      7355    5777    500 25331   14   109   40  12%      1  102   18    2 1158%
c i   16.0   73089   528881      7519    5910    517 25342   14   112   40  12%      1  104   19    2 1150%
c i   16.1   73074   528881      7620    6002    522 25344   14   113   40  13%      1  106   23    2 1399%
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   16.1   73071   528881      7653    6032    522 25345   14   113   40  13%      1  105   22    2 1326%
c 
c [simplification-5] limit 7797 conflicts (hard 17704) hit after 7799 conflicts
c [quatres-1] found 30344 quaternary clauses 43% in total
c [ternres-1] boosting ternary resolution limit by 5
c [ternres-1] limit 20000000 with penalty 0 = 0 + 0
c [ternres-1] all 73071 free variables schedulable
c [ternres-1] 118 ternary resolvents (1 bin, 117 trn)
c [ternres-1] fully completed ternary resolution
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 219 xors of average arity 2.4
c [gauss-1] connected 515 occurrences of 364 variables (average 1.4)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] fully completed
c [gauss-1] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-9] removed 151 variables
c [unhide-5] limit 319583 with penalty 0 = 0 + 0
c [unhide-5-5] 1 units, 854 failed, 11209 tauts, 0 hbrs, 14142 literals
c [transred-1] limit 1597918 with penalty 0 = 0 + 0
c [transred-1] removed 194 transitive binary clauses
c [transred-1] found 3 units
c [block-1] scheduling all variables this time
c [block-1] scheduled 72390 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 6663 blocked clauses
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 3 clauses out of 143 (2%) of length 10
c [cce-1-1] eliminated 6 clauses out of 520 (1%) of length 9
c [cce-1-1] eliminated 37 clauses out of 566 (7%) of length 8
c [cce-1-1] eliminated 59 clauses out of 754 (8%) of length 7
c [cce-1-1] eliminated 3038 clauses out of 4199 (72%) of length 6
c [cce-1-1] eliminated 1538 clauses out of 33497 (5%) of length 5
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 4681 large clauses in 30000002 steps
c [cce-1-1] allowing another 15000001 steps for small clauses
c [cce-1-1] scheduling 251242 clauses = 234751 binary + 16491 ternary
c [cce-1-1] tried to eliminate 846 small clauses 0%
c [cce-1-1] eliminated 332 binary clauses 0%
c [cce-1-1] eliminated 16 ternary clauses 0%
c [cce-1-1] eliminated 348 small clauses 0%
c [cce-1-1] eliminated 348 small clauses in 30000009 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 5029 covered clauses in round 1
c [cce-1] eliminated 5029 covered clauses in TOTAL during 1 rounds
c [bca-1] limit of 10000000 steps and 968732 added (scaled 2)
c [bca-1] 127419 out of 144782 literals actually usable 88%
c [bca-1] added 143 blocked clauses in 370892 steps
c [sweep-1] limit 1000000 penalty 0 = 0 + 0
c [sweep-1-1] 9498 pos 13.1% + 62892 neg 86.9% = 72390 sched 100.0% ret 0
c [sweep-1-1] 1015363 steps 29 queries 17452.86 avg class size
c [sweep-1-1] 171 decisions 24 SAT calls 31.50 avg env size
c [sweep-1-1] 72278 variables remain 100% (104 retained 0%)
c [decomp-10] removed 15 variables
c [sweep-1-1] removed 15 vars (0 failed, 4 eqs, 15 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 15 vars in TOTAL (1 rounds, 28 queries)
c [phase-count-5] 482336 negative 99.7% of 484018 except 1682 0.3%
c [phase-count-5] 394287 positive 81.5% of 484018 except 89731 18.5%
c [phase-count-5] less non-negative clauses 1682 than limit 48400 (10.0%)
c [phase-count-5] non-pos/non-neg = 89731/1682 = 53.35 >= 2.00 = 200/100
c [lucky-phase-5] forcing lucky phase -1
c [phase-5] phase bias: 0 positive 0%, 262 negative 100%
c [sort-queue-5] sorted 72375 enqueued variables after 7799 conflicts
c [score-dist-5] active 0 (0%), one 31720 (44%), zero 40655 (56%)
c [score-dist-5] max exp 1, different 2 (100%)
c [score-dist-5] median active exp 0, avg 0.0
c [simplification-5] removed 696 variables 1.0% (72375 remain 34%)
c [simplification-5] removed 44863 irredundant clauses 8.5% (484018 remain 41%)
c [simplification-5] maximum reduction of 8% = max (1%, 8%)
c [simplification-5] large reduction 8% >= 5% limit
c [simplification-5] next conflict interval 2000 = 2000/1
c [simplification-5] penalized conflict interval 2000 = 1 * 2000
c [simplification-5] hard conflict limit 19799 (soft 9799 + delta 10000)
c [simplification-5] new conflict limit 9799 (hard 19799)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   19.2   72374   484018      7812    6051    650 32068   14   116   38  13%      1  108   21    2 1194%
c i   19.2   72298   484018      7821    6056    651 32070   14   116   38  13%      1  108   20    2 1160%
c i   19.4   72290   484018      8025    6202    674 32096   14   116   39  12%      1  108   14    2  822%
c i   19.4   72202   484018      8052    6221    677 32099   14   116   39  12%      1  108   14    2  817%
c i   19.4   72193   484018      8077    6234    679 32107   14   116   39  12%      1  108   13    2  758%
c i   19.4   72096   484018      8083    6238    679 32108   14   116   39  12%      1  107   13    2  744%
c i   19.5   71947   484018      8106    6250    681 32116   14   115   39  12%      1  107   12    2  712%
c i   19.5   71938   484018      8144    6276    686 32122   14   115   39  12%      1  106   11    2  651%
c i   19.5   71912   484018      8209    6319    692 32137   14   114   39  12%      1  106   10    2  555%
c i   19.5   71906   484018      8238    6344    693 32138   14   114   39  12%      1  106    9    2  529%
c i   19.6   71899   484018      8288    6381    701 32142   14   114   39  12%      1  105    8    2  476%
c i   19.6   71891   484018      8313    6397    704 32147   14   113   39  12%      1  105    8    2  452%
c i   19.7   71666   484018      8427    6482    713 32164   13   113   39  12%      1  104    8    2  467%
c i   19.7   71660   484018      8448    6498    714 32167   13   113   39  12%      1  104    8    2  459%
c i   19.7   71654   484018      8468    6516    714 32167   13   113   39  12%      1  104   10    2  545%
c i   19.8   71652   484018      8513    6545    716 32179   13   114   39  12%      1  105    9    2  522%
c i   19.8   71509   484018      8516    6547    716 32179   13   114   39  12%      1  105    9    2  517%
c i   19.8   71500   484018      8536    6560    718 32183   13   114   39  12%      1  105    9    2  496%
c i   19.8   71493   484018      8539    6562    718 32183   13   114   39  12%      1  105    9    2  495%
c i   19.8   71169   484018      8562    6578    720 32187   13   114   39  12%      1  105    8    2  470%
c i   19.8   70672   484018      8581    6589    723 32191   13   113   39  12%      1  104    8    2  458%
c i   19.8   70667   484018      8599    6600    724 32195   13   113   39  12%      1  104    9    2  524%
c i   19.8   70547   484018      8617    6609    727 32200   13   113   39  12%      1  104    9    2  504%
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   19.9   70457   484018      8621    6612    727 32200   13   113   39  12%      1  104    9    2  500%
c i   19.9   70447   484018      8639    6624    729 32203   13   113   39  12%      1  104    9    2  484%
c i   19.9   70399   484018      8641    6623    729 32204   13   113   39  12%      1  104    9    2  480%
c i   19.9   70352   484018      8649    6630    729 32204   13   112   39  12%      1  103    8    2  471%
c i   19.9   70343   484018      8679    6655    729 32208   13   112   39  12%      1  103    8    2  451%
c i   19.9   70300   484018      8683    6657    729 32209   13   112   39  12%      1  103    8    2  450%
c i   19.9   70282   484018      8695    6662    731 32213   13   112   39  12%      1  103    8    2  437%
c i   20.0   70277   484018      8842    6763    749 32239   13   114   39  11%      1  105    7    2  395%
c i   20.1   70268   484018      8854    6773    750 32239   13   114   39  11%      1  105    7    2  390%
c i   20.1   70241   484018      8899    6807    757 32241   13   114   39  11%      1  105    7    2  366%
c i   20.1   70240   484018      8900    6807    757 32241   13   114   39  11%      1  105    7    2  365%
c i   20.1   70239   484018      8939    6833    759 32250   13   114   39  11%      1  105    7    2  383%
c i   20.2   70233   484018      8967    6855    759 32255   13   115   39  11%      1  105    7    2  371%
c i   20.2   70225   484018      8998    6878    761 32259   13   117   39  11%      1  107    7    2  359%
c i   20.4   70199   484018      9172    6998    779 32292   12   118   39  11%      1  108    7    2  373%
c i   20.5   70193   484018      9290    7079    789 32313   12   117   39  10%      1  107    7    2  367%
c i   20.5   70186   484018      9304    7089    790 32315   12   117   39  10%      1  107    7    2  358%
c i   20.5   70179   484018      9308    7091    791 32315   12   117   39  10%      1  107    7    2  355%
c i   20.5   70173   484018      9321    7101    791 32317   12   117   39  10%      1  107    6    2  348%
c i   20.6   70164   484018      9396    7152    801 32329   12   116   39  10%      1  106    6    2  318%
c i   20.7   70156   484018      9457    7192    807 32342   12   116   39  10%      1  106    6    2  318%
c i   20.7   70134   484018      9483    7212    807 32346   12   117   39  10%      1  106    6    2  314%
c i   20.7   70055   484018      9512    7233    809 32349   12   117   39  10%      1  107    6    2  332%
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   20.8   70049   484018      9590    7285    819 32361   12   117   39  10%      1  107    6    2  312%
c i   20.8   70018   484018      9604    7298    819 32361   12   117   39  10%      1  106    6    2  306%
c i   21.0   70010   484018      9743    7400    834 32378   12   117   39  10%      1  106    6    2  329%
c 
c [simplification-6] limit 9829 conflicts (hard 19799) hit after 9829 conflicts
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] all 70008 free variables schedulable
c [ternres-2] 2 ternary resolvents (0 bin, 2 trn)
c [ternres-2] 43452 variables remain 62% (26556 retained 38%)
c [card-3] limit 500000 penalty 2 = 2 + 0
c [card-3] found 2241 at-most-one constraints of average size 4.2
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 500000 for elimination
c [card-3] 2241 out of 2241 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [decomp-11] removed 2718 variables
c [simpleprobe-3] 11236 schedulable variables 16%
c [simpleprobe-3] limit 4303775 penalty 1 = 1 + 0
c [decomp-12] removed 105 variables
c [simpleprobe-3] 16113 variables remain 23% (53439 retained 77%)
c [simpleprobe-3] removed 105 variables, found 8184 hbrs, 33 units
c [unhide-6] limit 430377 with penalty 0 = 0 + 0
c [unhide-6-6] 6 units, 908 failed, 3253 tauts, 0 hbrs, 8685 literals
c [transred-2] limit 2000000 with penalty 0 = 0 + 0
c [transred-2] removed 318 transitive binary clauses
c [transred-2] found 2 units
c [block-2] scheduling all variables this time
c [block-2] scheduled 68347 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 1221 blocked clauses
c [block-2] 1221 < 1/100 * 467683 = 4676 considered unsuccessful
c [cce-2] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-2-1] eliminated 1607 clauses out of 25729 (6%) of length 5
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] eliminated 1607 large clauses in 30000001 steps
c [cce-2-1] allowing another 15000000 steps for small clauses
c [cce-2-1] scheduling 380382 clauses = 223673 binary + 156709 ternary
c [cce-2-1] tried to eliminate 439 small clauses 0%
c [cce-2-1] eliminated 100 binary clauses 0%
c [cce-2-1] eliminated 32 ternary clauses 0%
c [cce-2-1] eliminated 132 small clauses 0%
c [cce-2-1] eliminated 132 small clauses in 30000021 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 1739 covered clauses in round 1
c [cce-2] eliminated 1739 covered clauses in TOTAL during 1 rounds
c [cce-2] 1739 < 1/100 * 458439 = 4584 considered unsuccessful
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 68296 variables 100%
c [elim-5] limit of 21518876 steps penalty 1 = 1 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5] incomplete 9562 not tried 14% in round 1
c [gc-35] reconnected 35166 binary clauses (produced 0 empty 2 units)
c [elim-5] transition to [ all 1 rem 1 ] state
c [elim-5] eliminated 4116 = 6% variables out of 68296 scheduled
c [bca-2] limit of 10000000 steps and 892949 added (scaled 2)
c [bca-2] 112502 out of 128362 literals actually usable 88%
c [bca-2] added 126 blocked clauses in 316611 steps
c [sweep-2] limit 1000000 penalty 0 = 0 + 0
c [sweep-2-1] 8597 pos 13.4% + 55506 neg 86.6% = 64103 sched 99.9% ret 77
c [sweep-2-1] 1056745 steps 23 queries 15528.65 avg class size
c [sweep-2-1] 189 decisions 19 SAT calls 50.37 avg env size
c [sweep-2-1] 64010 variables remain 100% (166 retained 0%)
c [decomp-13] removed 73 variables
c [sweep-2-1] removed 73 vars (0 failed, 3 eqs, 6 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 73 vars in TOTAL (1 rounds, 22 queries)
c [sort-queue-6] sorted 64107 enqueued variables after 9829 conflicts
c [score-dist-6] active 0 (0%), one 39569 (62%), zero 24538 (38%)
c [score-dist-6] max exp 1, different 2 (100%)
c [score-dist-6] median active exp 0, avg 0.0
c [simplification-6] removed 5901 variables 8.4% (64107 remain 30%)
c [simplification-6] removed 37955 irredundant clauses 7.8% (446063 remain 37%)
c [simplification-6] maximum reduction of 8% = max (8%, 8%)
c [simplification-6] large reduction 8% >= 5% limit
c [simplification-6] next conflict interval 2000 = 2000/1
c [simplification-6] penalized conflict interval 2000 = 1 * 2000
c [simplification-6] hard conflict limit 21829 (soft 11829 + delta 10000)
c [simplification-6] new conflict limit 11829 (hard 21829)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   25.1   64106   446063      9911    4034    769 34923   11   120   35  10%      1  109    7    2  386%
c i   25.3   64096   446063     10169    4235    786 34957   11   118   35   9%      1  106    7    2  342%
c i   25.6   64088   446063     10574    4558    814 35001   11   121   35   9%      2  109    9    2  473%
c i   25.6   64080   446063     10632    4601    821 35008   11   120   35   9%      2  108    9    2  437%
c i   25.7   64074   446063     10691    4643    824 35020   11   120   35   9%      2  107    8    2  394%
c i   25.7   64069   446063     10766    4703    833 35024   11   119   35   9%      1  106    7    2  364%
c i   25.7   64025   446063     10770    4706    833 35024   11   119   35   9%      1  106    7    2  365%
c i   25.7   63995   446063     10774    4707    835 35024   11   119   35   9%      1  106    7    2  360%
c i   25.7   63989   446063     10784    4715    835 35025   11   119   35   9%      1  106    7    2  357%
c i   25.8   63983   446063     10858    4771    843 35031   11   118   35   9%      1  106    6    2  326%
c i   25.8   63981   446063     10899    4801    846 35036   11   119   35   9%      1  106    6    2  317%
c i   25.9   63879   446063     11038    4901    863 35055   10   118   35   9%      1  105    6    2  320%
c i   25.9   63870   446063     11039    4901    863 35055   10   118   35   9%      1  105    6    2  319%
c i   25.9   63864   446063     11052    4909    865 35057   10   117   35   9%      1  105    6    2  313%
c i   26.1   63857   446063     11353    5149    885 35087   10   118   35   9%      1  104    7    2  342%
c i   26.2   63854   446063     11597    5335    907 35118   11   119   35   9%      2  105   14    2  669%
c i   26.3   63853   446063     11627    5357    908 35124   11   119   35   9%      1  105   13    2  616%
c i   26.3   63843   446063     11633    5361    908 35125   11   119   35   9%      1  105   12    2  605%
c i   26.3   63833   446063     11652    5377    908 35127   10   118   35   9%      1  105   12    2  576%
c i   26.4   63826   446063     11804    5486    928 35146   10   118   35   9%      1  104   10    2  479%
c 
c [simplification-7] limit 11845 conflicts (hard 21829) hit after 11845 conflicts
c [quatres-2] found 34646 quaternary clauses 54% in total
c [quatres-2-1] removed 1 duplicate quaternary clauses
c [quatres-2-2] added 9 single-self-subsuming ternary resolvents
c [quatres-2-2] added 31 quaternary resolvents
c [ternres-3] limit 4000000 with penalty 0 = 0 + 0
c [ternres-3] 39599 schedulable variables 62%
c [ternres-3] 120 ternary resolvents (0 bin, 120 trn)
c [ternres-3] 14141 variables remain 22% (49661 retained 78%)
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] extracted 24 xors of average arity 2.8
c [gauss-2] connected 68 occurrences of 44 variables (average 1.5)
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] fully completed
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-14] removed 13 variables
c [treelook-3] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-3] scheduled 47740 literals 37%
c [treelook-3] scheduling used 304441 steps
c [treelook-3] not fully scheduled
c [treelook-3] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-3] used 324740 steps
c [treelook-3] 47725 literals remain 37%
c [treelook-3] 23163 variables remain to probed next time 36%
c [treelook-3] removed 9 variables, found 1622 hbrs
c [unhide-7] limit 511170 with penalty 0 = 0 + 0
c [unhide-7-7] 3 units, 207 failed, 8184 tauts, 0 hbrs, 3563 literals
c [transred-3] limit 2000000 with penalty 0 = 0 + 0
c [transred-3] removed 282 transitive binary clauses
c [transred-3] found 7 units
c [elim-6] 9531 variables 15% will be scheduled this time
c [elim-6] scheduled 9531 variables 15%
c [elim-6] limit of 51117025 steps penalty 0 = 0 + 0
c [elim-6] rescheduling of touched variables disabled
c [elim-6-1] eliminated 4 variables 0% in round 1 in 19802245 steps
c [elim-6-1] backward subsumption/strengthening limit 19802200
c [elim-6-1-1] backward checking 307 touched variables 0%
c [elim-6-1-1] fully completed backward checking in 1 rounds
c [elim-6-1] subsumed 0 and strengthened 1 clauses in 189088 steps
c [elim-6-1] rescheduled 6 variables 0% by backward subsumption
c [elim-6-2] no variable eliminated in round 2 in 5296 steps
c [elim-6] fully completed in 2 rounds
c [elim-6] transition to [ all 0 rem 0 ] state
c [elim-6] eliminated 4 = 0% variables out of 9531 scheduled
c [elim-6] 4 < 1/100 * 9531 = 95 considered unsuccessful
c [bca-3] limit of 10000000 steps and 866646 added (scaled 2)
c [bca-3] 107311 out of 127162 literals actually usable 84%
c [bca-3] added 55 blocked clauses in 292738 steps
c [sweep-3] limit 1000000 penalty 0 = 0 + 0
c [sweep-3-1] 8151 pos 12.9% + 55272 neg 87.1% = 63423 sched 99.8% ret 157
c [sweep-3-1] 1135413 steps 15 queries 18208.20 avg class size
c [sweep-3-1] 79 decisions 12 SAT calls 52.42 avg env size
c [sweep-3-1] 63379 variables remain 100% (201 retained 0%)
c [decomp-16] removed 50 variables
c [sweep-3-1] removed 50 vars (0 failed, 2 eqs, 7 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 50 vars in TOTAL (1 rounds, 14 queries)
c [sort-queue-7] sorted 63530 enqueued variables after 11845 conflicts
c [score-dist-7] active 0 (0%), one 40876 (64%), zero 22654 (36%)
c [score-dist-7] max exp 1, different 2 (100%)
c [score-dist-7] median active exp 0, avg 0.0
c [simplification-7] removed 272 variables 0.4% (63530 remain 30%)
c [simplification-7] removed 13137 irredundant clauses 2.9% (432926 remain 36%)
c [simplification-7] maximum reduction of 3% = max (0%, 3%)
c [simplification-7] geometric conflict interval increment 5000 = 20000 / 4
c [simplification-7] new conflict interval 11666
c [simplification-7] penalized conflict interval 11666 = 1 * 11666
c [simplification-7] hard conflict limit 33511 (soft 23511 + delta 10000)
c [simplification-7] new conflict limit 23511 (hard 33511)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   28.5   63529   432926     11929    5565   1007 36979   10   119   35   9%      1  104    9    2  451%
c i   28.5   63524   432926     11963    5589   1011 36983   10   118   35   9%      1  104    9    2  438%
c i   28.5   63522   432926     11964    5589   1011 36983   10   118   35   9%      1  104    9    2  436%
c i   28.5   63521   432926     11965    5589   1011 36983   10   118   35   9%      1  104    9    2  435%
c i   28.5   63519   432926     11966    5589   1011 36983   10   118   35   9%      1  104    9    2  433%
c i   28.7   63518   432926     12195    5770   1035 37005   10   118   35   9%      1  104    9    2  414%
c i   28.8   63515   432926     12237    5797   1041 37011   10   120   35   8%      1  105    8    2  390%
c i   28.8   63511   432926     12249    5804   1043 37013   10   120   35   8%      1  105    8    2  378%
c i   28.8   63486   432926     12282    5826   1047 37018   10   119   35   8%      1  104    8    2  355%
c i   28.8   63483   432926     12283    5826   1047 37018   10   119   35   8%      1  104    7    2  354%
c i   28.8   63478   432926     12315    5850   1050 37021   10   119   35   8%      1  104    7    2  342%
c i   28.8   63259   432926     12334    5862   1054 37022   10   119   35   8%      1  104    7    2  338%
c i   28.9   63223   432926     12351    5871   1058 37023   10   119   35   8%      1  104    7    2  327%
c i   29.0   63137   432926     12496    5986   1071 37037   10   121   35   8%      1  106    6    2  305%
c i   29.0   63134   432926     12497    5986   1071 37037   10   121   35   8%      1  106    6    2  304%
c i   29.1   63132   432926     12541    6018   1075 37043   10   121   35   8%      1  106    6    2  297%
c i   29.3   63086   432926     12780    6187   1100 37083   10   123   35   8%      1  107    6    2  294%
c i   29.3   63082   432926     12849    6237   1106 37094   10   123   35   8%      1  107    7    2  321%
c i   29.5   63075   432926     13014    6364   1119 37117   10   124   35   8%      1  108    8    2  391%
c i   29.5   63065   432926     13046    6387   1123 37121   10   124   35   8%      1  108    8    2  377%
c i   29.5   63048   432926     13059    6395   1124 37122   10   124   35   8%      1  108    8    2  371%
c i   29.5   63015   432926     13060    6395   1124 37122   10   124   35   8%      1  108    8    2  370%
c i   29.5   63008   432926     13087    6419   1125 37122   10   125   35   8%      1  108    8    2  383%
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   29.7   63000   432926     13214    6515   1131 37140    9   126   35   8%      1  110    8    2  383%
c i   29.7   62994   432926     13264    6550   1135 37148    9   126   35   7%      1  110    8    2  377%
c i   29.8   62986   432926     13335    6606   1138 37157    9   126   35   8%      1  109    8    2  374%
c i   30.0   62985   432926     13592    6810   1159 37182    9   129   35   7%      1  112    8    2  371%
c i   30.0   62981   432926     13699    6908   1160 37187    9   128   35   7%      1  111    9    2  408%
c i   30.0   62980   432926     13700    6908   1160 37187    9   128   35   7%      1  111    9    2  407%
c i   30.1   62977   432926     13881    7074   1166 37192   10   127   35   8%      1  110   12    2  536%
c i   30.1   62974   432926     13971    7152   1170 37197   10   127   35   8%      1  109   11    2  482%
c i   30.2   62968   432926     14053    7226   1172 37198   10   128   35   8%      1  110   11    2  467%
c i   30.3   62962   432926     14390    7530   1183 37208   10   128   35   8%      1  109   15    2  634%
c i   30.3   62961   432926     14426    7556   1189 37211   10   127   35   8%      1  109   14    2  577%
c i   30.4   62833   432926     14434    7563   1189 37211   10   127   35   8%      1  108   13    2  564%
c i   30.4   62829   432926     14449    7569   1196 37212   10   127   35   8%      1  108   13    2  538%
c i   30.5   62822   432926     14669    7752   1215 37228   10   128   35   8%      1  109   12    2  493%
c i   30.6   62821   432926     14794    7852   1226 37240   10   128   35   8%      1  109   10    2  423%
c i   30.6   62818   432926     14795    7852   1226 37240   10   128   35   8%      1  109   10    2  421%
c i   30.6   62815   432926     14817    7868   1228 37242   10   128   35   8%      1  109   10    2  406%
c i   30.6   62812   432926     14818    7868   1228 37242   10   128   35   8%      1  109   10    2  404%
c i   30.7   62808   432926     14882    7919   1231 37251   10   128   35   8%      1  109   10    2  399%
c i   30.8   62804   432926     14968    7984   1241 37258   10   130   35   8%      1  111   10    2  423%
c i   30.8   62803   432926     15053    8041   1254 37270   10   130   35   8%      1  110   10    2  394%
c i   31.0   62801   432926     15205    8149   1273 37292   10   131   35   8%      1  111    9    2  359%
c i   31.2   62794   432926     15484    8372   1292 37320   10   132   36   8%      1  112   10    2  401%
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   31.3   62791   432926     15629    8486   1311 37330   10   130   36   8%      1  110   11    2  437%
c i   31.3   62789   432926     15652    8504   1311 37334   10   130   36   8%      1  110   11    3  435%
c i   31.3   62788   432926     15722    8561   1315 37341   10   131   36   8%      1  111   12    3  467%
c i   31.5   62787   432926     15972    8768   1333 37362   10   132   36   8%      1  111   11    3  430%
c i   31.5   62782   432926     16042    8813   1342 37370   10   132   36   8%      1  111   10    3  403%
c i   31.6   62754   432926     16087    8848   1344 37376   10   132   36   8%      1  111   10    3  390%
c i   31.6   62747   432926     16105    8863   1345 37377   10   132   36   8%      1  111   11    3  418%
c i   31.8   62739   432926     16286    9015   1358 37385   11   135   36   8%      1  113   14    3  536%
c i   31.8   62737   432926     16287    9015   1358 37385   11   135   36   8%      1  113   14    3  534%
c i   32.0   62733   432926     16574    9241   1381 37416   11   138   36   8%      1  116   12    3  463%
c i   32.0   62717   432926     16591    9250   1382 37422   11   138   36   8%      1  116   12    3  441%
c i   32.1   62708   432926     16636    9282   1385 37429   11   137   36   8%      1  115   11    3  432%
c i   32.4   62701   432926     17008    9592   1411 37462   11   145   36   8%      2  123   14    3  527%
c i   32.4   62696   432926     17013    9595   1412 37462   11   145   36   8%      2  122   14    3  518%
c i   32.6   62533   432926     17261    9802   1426 37483   11   148   37   8%      2  125   13    3  477%
c i   32.8   62530   432926     17476    9985   1433 37497   12   148   37   8%      2  124   23    3  796%
c i   32.9   62526   432926     17612   10105   1442 37502   12   149   37   8%      2  125   22    3  763%
c i   32.9   62524   432926     17669   10155   1442 37505   12   149   37   8%      1  125   24    3  825%
c i   33.1   62514   432926     18081   10529   1456 37521   13   144   37   9%      2  119   16    3  529%
c i   33.1   62508   432926     18082   10529   1456 37521   13   144   37   9%      2  119   16    3  527%
c i   33.2   62498   432926     18203   10637   1461 37526   13   147   37   9%      2  122   15    3  516%
c i   33.3   62491   432926     18242   10667   1464 37531   13   147   37   9%      2  122   14    3  478%
c i   33.4   62451   432926     18390   10778   1474 37555   13   145   37   9%      2  120   12    3  402%
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   33.5   62443   432926     18481   10851   1483 37561   12   145   37   9%      1  119   11    3  354%
c i   33.5   62442   432926     18499   10862   1483 37566   12   144   37   9%      1  119   10    3  339%
c i   33.8   62441   432926     18796   11090   1508 37599   12   148   37   8%      2  122   10    3  320%
c i   33.9   62432   432926     18910   11187   1514 37606   12   150   37   8%      1  124    9    3  308%
c i   34.1   62425   432926     19154   11384   1535 37626   12   151   37   8%      2  124   11    3  348%
c i   34.3   62422   432926     19271   11479   1547 37631   12   152   37   8%      1  125   10    3  338%
c i   34.3   62242   432926     19313   11509   1553 37636   12   152   37   8%      1  125   10    3  324%
c i   34.3   62236   432926     19317   11512   1553 37636   12   152   37   8%      1  124   10    3  321%
c i   34.3   62232   432926     19368   11553   1556 37641   12   151   37   8%      1  123   10    3  308%
c i   34.4   62201   432926     19419   11590   1559 37650   12   150   37   8%      1  123    9    3  284%
c i   34.5   62193   432926     19484   11645   1562 37656   12   150   37   8%      1  122    9    3  279%
c i   34.7   62186   432926     19697   11821   1573 37678   12   151   37   8%      1  124   12    3  376%
c i   34.7   62180   432926     19745   11863   1574 37680   12   153   37   8%      1  125   13    3  412%
c i   34.8   62175   432926     19819   11926   1576 37686   12   154   37   8%      1  126   13    3  421%
c i   34.8   62163   432926     19829   11935   1576 37686   12   154   37   8%      1  126   14    3  426%
c i   35.1   62157   432926     20263   12316   1587 37706   13   155   37   8%      2  126   19    3  584%
c i   35.1   62156   432926     20264   12316   1587 37706   13   155   37   8%      2  126   19    3  581%
c i   35.1   62155   432926     20269   12319   1588 37706   13   155   37   8%      2  126   19    3  576%
c i   35.1   62151   432926     20284   12333   1588 37706   13   155   37   8%      2  126   19    3  567%
c i   35.2   62144   432926     20463   12490   1593 37719   13   156   37   8%      2  126   18    3  530%
c i   35.3   62141   432926     20505   12519   1596 37728   13   155   37   8%      2  126   16    3  474%
c i   35.4   62133   432926     20602   12592   1601 37741   13   155   37   8%      1  125   14    3  408%
c i   35.4   62126   432926     20656   12641   1602 37743   13   154   37   8%      1  124   14    3  408%
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   35.4   62122   432926     20708   12681   1608 37748   13   154   37   8%      1  124   12    3  373%
c i   35.5   62121   432926     20722   12693   1609 37748   13   154   37   8%      1  124   12    3  366%
c i   35.5   62120   432926     20755   12718   1612 37751   13   153   37   8%      1  123   11    3  337%
c i   35.5   62116   432926     20850   12791   1618 37761   13   153   37   8%      1  123   10    3  296%
c i   35.7   62110   432926     21027   12929   1637 37777   12   152   37   8%      1  122    9    3  266%
c i   35.8   62106   432926     21169   13043   1647 37789   12   151   37   8%      1  120   10    3  302%
c i   35.9   62102   432926     21300   13144   1661 37803   12   150   37   8%      1  119   10    3  290%
c i   35.9   62095   432926     21301   13144   1661 37803   12   150   37   8%      1  119   10    3  289%
c 
c [simplification-8] limit of 266 iterations hit after 266 iterations
c [quatres-3] found 31121 quaternary clauses 52% in total
c [quatres-3-2] added 2 single-self-subsuming ternary resolvents
c [quatres-3-2] added 2 quaternary resolvents
c [ternres-4] limit 4725971 with penalty 0 = 0 + 0
c [ternres-4] 13794 schedulable variables 22%
c [ternres-4] 194 ternary resolvents (0 bin, 194 trn)
c [ternres-4] fully completed ternary resolution
c [decomp-17] removed 1844 variables
c [basicprobe-3] limit 23629859 penalty 0 = 0 + 0
c [basicprobe-3-0] 18572 probes remain 31% after last round
c [basicprobe-3-0] 369 units = 339 failed (92%) + 30 lifted (8%)
c [basicprobe-3-0] removed 1151 variables, found 92532 hbrs
c [bate-1] eliminated 102 asymmetric tautologies during probing
c [unhide-8] limit 945194 with penalty 0 = 0 + 0
c [unhide-8-8] 160 units, 1100 failed, 10086 tauts, 0 hbrs, 20065 literals
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 263 transitive binary clauses
c [transred-4] found 2 units
c [block-3] scheduling all variables this time
c [block-3] scheduled 59280 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 394 blocked clauses
c [block-3] 394 < 1/100 * 411798 = 4117 considered unsuccessful
c [cce-3] limit of 15000000 steps penalty 1 = 1 + 0
c [cce-3-1] eliminated 2 clauses out of 2 (100%) of length 47
c [cce-3-1] eliminated 1 clauses out of 2 (50%) of length 46
c [cce-3-1] eliminated 2 clauses out of 2 (100%) of length 45
c [cce-3-1] eliminated 1 clauses out of 2 (50%) of length 44
c [cce-3-1] eliminated 2 clauses out of 2 (100%) of length 43
c [cce-3-1] eliminated 1 clauses out of 2 (50%) of length 42
c [cce-3-1] eliminated 2 clauses out of 2 (100%) of length 41
c [cce-3-1] eliminated 1 clauses out of 2 (50%) of length 40
c [cce-3-1] eliminated 2 clauses out of 2 (100%) of length 39
c [cce-3-1] eliminated 1 clauses out of 2 (50%) of length 38
c [cce-3-1] eliminated 2 clauses out of 2 (100%) of length 37
c [cce-3-1] eliminated 1 clauses out of 2 (50%) of length 36
c [cce-3-1] eliminated 2 clauses out of 2 (100%) of length 35
c [cce-3-1] eliminated 1 clauses out of 2 (50%) of length 34
c [cce-3-1] eliminated 2 clauses out of 2 (100%) of length 33
c [cce-3-1] eliminated 1 clauses out of 2 (50%) of length 32
c [cce-3-1] eliminated 2 clauses out of 2 (100%) of length 31
c [cce-3-1] eliminated 1 clauses out of 2 (50%) of length 30
c [cce-3-1] eliminated 2 clauses out of 2 (100%) of length 29
c [cce-3-1] eliminated 1 clauses out of 2 (50%) of length 28
c [cce-3-1] eliminated 2 clauses out of 3 (67%) of length 27
c [cce-3-1] eliminated 3 clauses out of 4 (75%) of length 26
c [cce-3-1] eliminated 3 clauses out of 4 (75%) of length 25
c [cce-3-1] eliminated 3 clauses out of 4 (75%) of length 24
c [cce-3-1] eliminated 3 clauses out of 4 (75%) of length 23
c [cce-3-1] eliminated 2 clauses out of 4 (50%) of length 22
c [cce-3-1] eliminated 4 clauses out of 4 (100%) of length 21
c [cce-3-1] eliminated 2 clauses out of 4 (50%) of length 20
c [cce-3-1] eliminated 4 clauses out of 5 (80%) of length 19
c [cce-3-1] eliminated 5 clauses out of 6 (83%) of length 18
c [cce-3-1] eliminated 3 clauses out of 6 (50%) of length 17
c [cce-3-1] eliminated 6 clauses out of 6 (100%) of length 16
c [cce-3-1] eliminated 3 clauses out of 6 (50%) of length 15
c [cce-3-1] eliminated 6 clauses out of 6 (100%) of length 14
c [cce-3-1] eliminated 3 clauses out of 6 (50%) of length 13
c [cce-3-1] eliminated 4 clauses out of 6 (67%) of length 12
c [cce-3-1] eliminated 6 clauses out of 7 (86%) of length 11
c [cce-3-1] eliminated 4 clauses out of 59 (7%) of length 10
c [cce-3-1] eliminated 7 clauses out of 191 (4%) of length 9
c [cce-3-1] eliminated 6 clauses out of 306 (2%) of length 8
c [cce-3-1] eliminated 28 clauses out of 465 (6%) of length 7
c [cce-3-1] eliminated 21 clauses out of 1261 (2%) of length 6
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 158 large clauses in 15000002 steps
c [cce-3-1] allowing another 7500001 steps for small clauses
c [cce-3-1] scheduling 211863 clauses = 195060 binary + 16803 ternary
c [cce-3-1] tried to eliminate 450 small clauses 0%
c [cce-3-1] eliminated 151 binary clauses 0%
c [cce-3-1] eliminated 12 ternary clauses 0%
c [cce-3-1] eliminated 163 small clauses 0%
c [cce-3-1] eliminated 163 small clauses in 15000004 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 321 covered clauses in round 1
c [cce-3] eliminated 321 covered clauses in TOTAL during 1 rounds
c [cce-3] 321 < 1/100 * 402979 = 4029 considered unsuccessful
c [bca-4] limit of 10000000 steps and 805978 added (scaled 2)
c [bca-4] 90723 out of 118532 literals actually usable 77%
c [bca-4] added 56 blocked clauses in 232037 steps
c [sweep-4] limit 1417791 penalty 0 = 0 + 0
c [sweep-4-1] 8210 pos 13.9% + 50889 neg 86.1% = 59099 sched 99.7% ret 166
c [sweep-4-1] 1560694 steps 26 queries 11306.96 avg class size
c [sweep-4-1] 401 decisions 23 SAT calls 88.00 avg env size
c [sweep-4-1] 58928 variables remain 99% (331 retained 1%)
c [decomp-18] removed 467 variables
c [sweep-4-1] removed 467 vars (0 failed, 2 eqs, 4 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 467 vars in TOTAL (1 rounds, 25 queries)
c [sort-queue-8] sorted 58798 enqueued variables after 21301 conflicts
c [score-dist-8] active 0 (0%), one 41783 (71%), zero 17015 (29%)
c [score-dist-8] max exp 1, different 2 (100%)
c [score-dist-8] median active exp 0, avg 0.0
c [simplification-8] removed 3295 variables 5.3% (58798 remain 27%)
c [simplification-8] removed 31522 irredundant clauses 7.3% (401404 remain 34%)
c [simplification-8] maximum reduction of 7% = max (5%, 7%)
c [simplification-8] forced so keeping old conflict interval 11666
c [simplification-8] conflict limit remains at 23649 (hard 33511)
c [simplification-8] new iteration interval 1000
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   39.6   58797   401404     21642   13198   1744 111251   13   151   39   8%      1  119   15    3  445%
c i   39.6   58793   401404     21662   13214   1746 111251   13   150   39   9%      1  119   19    3  531%
c i   39.6   58790   401404     21729   13274   1748 111252   13   151   39   9%      1  120   19    4  528%
c i   39.7   58784   401404     21733   13277   1748 111252   13   151   39   9%      1  120   19    4  551%
c i   39.9   58779   401404     21972   13486   1759 111264   13   152   39   9%      1  120   18    4  507%
c i   40.0   58770   401404     22190   13656   1776 111285   13   152   39   9%      1  120   13    4  375%
c i   40.1   58762   401404     22210   13675   1776 111285   13   152   39   9%      1  120   13    4  374%
c i   40.1   58759   401404     22262   13720   1778 111289   13   153   39   9%      1  120   13    4  361%
c i   40.1   58729   401404     22366   13794   1792 111303   13   151   39   9%      1  118   11    4  303%
c i   40.2   58725   401404     22457   13864   1798 111316   13   151   39   9%      1  118   10    4  279%
c i   40.4   58659   401404     22738   14076   1834 111346   13   152   39   8%      1  119   12    4  333%
c i   40.5   58630   401404     22818   14143   1839 111353   13   152   39   8%      1  118   11    4  302%
c i   40.5   58622   401404     22900   14207   1847 111362   13   150   39   8%      1  117   11    4  301%
c i   40.6   58621   401404     22917   14220   1847 111363   13   150   39   8%      1  116   11    4  290%
c i   40.7   58615   401404     23067   14333   1866 111377   13   150   39   8%      1  116   10    4  281%
c i   40.7   58609   401404     23069   14334   1866 111377   13   150   39   8%      1  116   10    4  279%
c i   40.7   58608   401404     23086   14345   1867 111379   13   149   39   8%      1  115   11    4  290%
c i   40.9   58605   401404     23339   14553   1885 111392   13   153   39   9%      1  118   21    4  554%
c i   41.0   58563   401404     23430   14621   1896 111403   13   153   39   9%      1  118   17    4  445%
c i   41.1   58562   401404     23467   14650   1902 111404   13   153   39   9%      1  118   16    4  431%
c 
c [simplification-9] limit 23656 conflicts (hard 33511) hit after 23656 conflicts
c [quatres-4] found 29633 quaternary clauses 54% in total
c [quatres-4-1] removed 5 duplicate quaternary clauses
c [quatres-4-1] added 1 double-self-subsuming ternary resolvents
c [quatres-4-2] added 6 single-self-subsuming ternary resolvents
c [quatres-4-2] added 4 quaternary resolvents
c [ternres-5] limit 5313620 with penalty 0 = 0 + 0
c [ternres-5] all 58562 free variables schedulable
c [ternres-5] 144 ternary resolvents (2 bin, 142 trn)
c [ternres-5] 26874 variables remain 46% (31688 retained 54%)
c [decomp-19] removed 264 variables
c [simpleprobe-4] 14424 schedulable variables 25%
c [simpleprobe-4] limit 21254483 penalty 0 = 0 + 0
c [decomp-20] removed 1179 variables
c [simpleprobe-4] 14135 variables remain 25% (43220 retained 75%)
c [simpleprobe-4] removed 1179 variables, found 45921 hbrs, 523 units
c [unhide-9] limit 1062724 with penalty 0 = 0 + 0
c [unhide-9-9] 21 units, 92 failed, 8763 tauts, 0 hbrs, 13664 literals
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 331 transitive binary clauses
c [transred-5] found 2 units
c [elim-7] scheduling all variables this time
c [elim-7] scheduled 57107 variables 100%
c [elim-7] limit of 53136208 steps penalty 1 = 1 + 0
c [elim-7] rescheduling of touched variables disabled
c [elim-7-1] eliminated 3439 variables 6% in round 1 in 35018176 steps
c [elim-7-1] backward subsumption/strengthening limit 18118032
c [elim-7-1-1] backward checking 10831 touched variables 19%
c [elim-7-1-1] fully completed backward checking in 1 rounds
c [elim-7-1] subsumed 101 and strengthened 492 clauses in 2786228 steps
c [elim-7-1] rescheduled 1327 variables 2% by backward subsumption
c [elim-7-2] eliminated 174 variables 0% in round 2 in 1471605 steps
c [elim-7-2] backward subsumption/strengthening limit 1471600
c [elim-7-2-1] backward checking 1233 touched variables 2%
c [elim-7-2-1] fully completed backward checking in 1 rounds
c [elim-7-2] subsumed 39 and strengthened 39 clauses in 505564 steps
c [elim-7-2] rescheduled 138 variables 0% by backward subsumption
c [elim-7-3] eliminated 19 variables 0% in round 3 in 140154 steps
c [elim-7-3] backward subsumption/strengthening limit 140100
c [elim-7-3-1] backward checking 117 touched variables 0%
c [elim-7-3-1] incomplete backward checking 0 remain 0%
c [elim-7-3] subsumed 10 and strengthened 6 clauses in 140101 steps
c [elim-7] incomplete 33 not tried 0% in round 3
c [elim-7] transition to [ all 1 rem 1 ] state
c [elim-7] eliminated 3668 = 6% variables out of 57107 scheduled
c [bca-5] limit of 10000000 steps and 739856 added (scaled 2)
c [bca-5] 81777 out of 106880 literals actually usable 77%
c [bca-5] added 95 blocked clauses in 208707 steps
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 15940860 penalty 0 = 0 + 0
c [sweep-5-1] 7243 pos 13.6% + 45929 neg 86.4% = 53172 sched 99.5% ret 267
c [sweep-5-1] 16072734 steps 288 queries 1604.74 avg class size
c [sweep-5-1] 3080 decisions 237 SAT calls 92.65 avg env size
c [sweep-5-1] 44788 variables remain 84% (8332 retained 16%)
c [decomp-21] removed 419 variables
c [sweep-5-1] removed 419 vars (0 failed, 55 eqs, 103 impls)
c [sweep-5] considered successful since not run to completion yet
c [sweep-5] removed 419 vars in TOTAL (1 rounds, 287 queries)
c [sort-queue-9] sorted 53020 enqueued variables after 23656 conflicts
c [score-dist-9] active 0 (0%), one 39331 (74%), zero 13689 (26%)
c [score-dist-9] max exp 1, different 2 (100%)
c [score-dist-9] median active exp 0, avg 0.0
c [simplification-9] removed 5542 variables 9.5% (53020 remain 25%)
c [simplification-9] removed 37690 irredundant clauses 9.4% (363714 remain 30%)
c [simplification-9] maximum reduction of 9% = max (9%, 9%)
c [simplification-9] large reduction 9% >= 5% limit
c [simplification-9] next conflict interval 2000 = 2000/1
c [simplification-9] penalized conflict interval 2000 = 1 * 2000
c [simplification-9] hard conflict limit 35656 (soft 25656 + delta 10000)
c [simplification-9] new conflict limit 25656 (hard 35656)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   45.5   53019   363714     23692   11387   1634 154415   13   155   36   8%      1  120   11    4  304%
c i   45.6   52962   363714     23896   11560   1649 154427   13   155   36   8%      1  119   13    4  335%
c i   45.7   52955   363714     24072   11713   1657 154434   13   155   36   8%      1  119   11    4  297%
c i   46.0   52933   363714     24435   12026   1677 154452   13   156   36   8%      1  120    9    4  240%
c i   46.4   52931   363714     24942   12437   1718 154488   12   159   36   8%      2  122    9    4  242%
c i   46.5   52928   363714     25039   12520   1724 154494   12   159   36   8%      2  121    9    4  222%
c i   46.5   52854   363714     25069   12547   1725 154494   12   158   36   8%      2  121   10    4  253%
c i   46.5   52853   363714     25096   12570   1727 154495   12   159   36   8%      2  121   10    4  245%
c i   46.8   52848   363714     25425   12844   1754 154517   12   158   36   8%      2  119   12    4  310%
c i   46.8   52847   363714     25489   12897   1758 154523   12   156   36   8%      2  118   13    4  315%
c 
c [simplification-10] limit 25656 conflicts (hard 35656) hit after 25656 conflicts
c [quatres-5] found 28551 quaternary clauses 54% in total
c [quatres-5-1] removed 1 duplicate quaternary clauses
c [quatres-5-2] added 8 single-self-subsuming ternary resolvents
c [quatres-5-2] added 19 quaternary resolvents
c [ternres-6] limit 5771998 with penalty 0 = 0 + 0
c [ternres-6] 24244 schedulable variables 46%
c [ternres-6] 715 ternary resolvents (1 bin, 714 trn)
c [ternres-6] fully completed ternary resolution
c [card-4] limit 360749 penalty 3 = 3 + 0
c [card-4] found 1041 at-most-one constraints of average size 4.0
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 360749 for elimination
c [card-4] 1041 out of 1041 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [gauss-3] limit 500000 penalty 2 = 2 + 0
c [gauss-3] extracted 9 xors of average arity 2.7
c [gauss-3] connected 24 occurrences of 24 variables (average 1.0)
c [gauss-3] limit 500000 penalty 2 = 2 + 0
c [gauss-3] fully completed
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-22] removed 5 variables
c [treelook-4] limit 577199 penalty 0 = 0 + 0 boost 1
c [treelook-4] scheduled 62935 literals 60%
c [treelook-4] scheduling used 583841 steps
c [treelook-4] not fully scheduled
c [treelook-4] limit 577199 penalty 0 = 0 + 0 boost 1
c [treelook-4] used 579360 steps
c [treelook-4] 62922 literals remain 60%
c [treelook-4] 17758 variables remain to probed next time 34%
c [treelook-4] removed 3 variables, found 2148 hbrs
c [unhide-10] limit 1154399 with penalty 0 = 0 + 0
c [unhide-10-10] 17 units, 343 failed, 13905 tauts, 0 hbrs, 8061 literals
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 348 transitive binary clauses
c [transred-6] found 1 units
c [elim-8] no untried remaining variables left
c [elim-8] scheduled 52457 variables 100%
c [elim-8] boosting limit by 20
c [elim-8] limit of 2308799260 steps penalty 0 = 0 + 0
c [elim-8] rescheduling of touched variables disabled
c [elim-8-1] eliminated 617 variables 1% in round 1 in 33314381 steps
c [elim-8-1] backward subsumption/strengthening limit 33314300
c [elim-8-1-1] backward checking 3042 touched variables 6%
c [elim-8-1-1] fully completed backward checking in 1 rounds
c [elim-8-1] subsumed 124 and strengthened 64 clauses in 902955 steps
c [elim-8-1] rescheduled 391 variables 1% by backward subsumption
c [elim-8-2] eliminated 31 variables 0% in round 2 in 431284 steps
c [elim-8-2] backward subsumption/strengthening limit 431200
c [elim-8-2-1] backward checking 247 touched variables 0%
c [elim-8-2-1] fully completed backward checking in 1 rounds
c [elim-8-2] subsumed 21 and strengthened 11 clauses in 138438 steps
c [elim-8-2] rescheduled 57 variables 0% by backward subsumption
c [elim-8-3] eliminated 3 variables 0% in round 3 in 76796 steps
c [elim-8-3] backward subsumption/strengthening limit 76700
c [elim-8-3-1] backward checking 34 touched variables 0%
c [elim-8-3-1] incomplete backward checking 0 remain 0%
c [elim-8-3] subsumed 2 and strengthened 4 clauses in 76701 steps
c [elim-8] incomplete 19 not tried 0% in round 3
c [elim-8] transition to [ all 1 rem 1 ] state
c [elim-8] eliminated 665 = 1% variables out of 52457 scheduled
c [bca-6] limit of 10000000 steps and 712765 added (scaled 2)
c [bca-6] 77706 out of 103586 literals actually usable 75%
c [bca-6] added 42 blocked clauses in 197965 steps
c [sweep-6] limit 1731599 penalty 0 = 0 + 0
c [sweep-6-1] 7049 pos 16.1% + 36796 neg 83.9% = 43845 sched 84.7% ret 7947
c [sweep-6-1] 1736349 steps 35 queries 6636.91 avg class size
c [sweep-6-1] 454 decisions 29 SAT calls 104.66 avg env size
c [sweep-6-1] 43557 variables remain 84% (8230 retained 16%)
c [decomp-24] removed 46 variables
c [sweep-6-1] removed 46 vars (0 failed, 6 eqs, 8 impls)
c [sweep-6] considered successful since not run to completion yet
c [sweep-6] removed 46 vars in TOTAL (1 rounds, 34 queries)
c [sort-queue-10] sorted 51746 enqueued variables after 25656 conflicts
c [score-dist-10] active 0 (0%), one 38989 (75%), zero 12757 (25%)
c [score-dist-10] max exp 1, different 2 (100%)
c [score-dist-10] median active exp 0, avg 0.0
c [simplification-10] removed 1099 variables 2.1% (51746 remain 24%)
c [simplification-10] removed 7839 irredundant clauses 2.2% (355875 remain 30%)
c [simplification-10] maximum reduction of 2% = max (2%, 2%)
c [simplification-10] geometric conflict interval increment 6666 = 20000 / 3
c [simplification-10] new conflict interval 18332
c [simplification-10] penalized conflict interval 18332 = 1 * 18332
c [simplification-10] hard conflict limit 53988 (soft 43988 + delta 10000)
c [simplification-10] new conflict limit 43988 (hard 53988)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   49.9   51745   355875     25805   12319   2370 137727   13   161   36   8%      2  122   14    4  356%
c i   50.2   51740   355875     26187   12635   2397 137754   12   165   36   7%      2  125   11    4  264%
c i   50.2   51738   355875     26210   12654   2399 137755   12   165   36   7%      2  125   10    4  257%
c i   50.3   51734   355875     26233   12675   2399 137755   12   165   36   7%      2  126   11    4  259%
c i   50.4   51729   355875     26387   12808   2409 137761   12   167   36   7%      2  127   10    4  242%
c i   50.4   51726   355875     26420   12838   2410 137762   12   166   36   7%      2  126   10    4  240%
c i   50.5   51725   355875     26544   12956   2412 137765   12   167   36   7%      2  127    9    4  228%
c i   50.6   51722   355875     26601   13005   2416 137768   12   168   36   7%      2  127    9    4  215%
c i   50.7   51718   355875     26748   13121   2426 137782   12   171   36   7%      1  130    9    4  219%
c i   50.7   51702   355875     26749   13121   2426 137782   12   171   36   7%      1  130    9    4  218%
c i   50.7   51700   355875     26769   13135   2427 137784   12   171   36   7%      1  130   10    4  248%
c i   50.8   51699   355875     26790   13152   2430 137784   12   170   36   7%      1  130   10    4  248%
c i   50.9   51698   355875     26996   13326   2443 137796   12   168   36   7%      1  127   11    4  258%
c i   51.2   51697   355875     27631   13899   2466 137823   13   164   36   8%      3  122   16    4  367%
c i   51.3   51685   355875     27755   14011   2469 137827   13   167   36   8%      3  125   18    4  410%
c i   51.3   51682   355875     27756   14011   2469 137827   13   167   36   8%      3  125   18    4  408%
c i   51.4   51681   355875     27860   14104   2475 137831   13   168   36   8%      2  125   16    4  374%
c i   51.5   51679   355875     27924   14159   2478 137835   13   167   36   8%      2  124   15    4  345%
c i   51.5   51676   355875     27925   14159   2478 137835   13   167   36   8%      2  124   15    4  343%
c i   51.5   51637   355875     28009   14228   2484 137842   13   167   36   8%      2  124   14    4  321%
c i   51.5   51522   355875     28016   14234   2484 137842   13   167   36   8%      2  124   14    4  316%
c i   51.6   51521   355875     28031   14245   2487 137842   13   167   36   8%      2  124   13    4  308%
c i   51.7   51520   355875     28224   14409   2499 137855   13   168   36   8%      2  124   15    4  341%
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   51.9   51519   355875     28502   14645   2517 137869   13   169   36   8%      2  125   15    4  330%
c i   51.9   51516   355875     28549   14678   2525 137873   13   169   36   8%      2  124   14    4  323%
c i   52.0   51514   355875     28576   14699   2526 137877   13   169   36   8%      2  125   15    4  334%
c i   52.0   51513   355875     28585   14705   2527 137877   13   169   36   8%      2  125   15    4  327%
c i   52.1   51511   355875     28694   14794   2531 137886   13   169   36   8%      1  124   14    4  322%
c i   52.2   51508   355875     28807   14883   2541 137899   13   170   36   8%      1  125   12    4  264%
c i   52.2   51497   355875     28916   14976   2553 137902   13   169   36   8%      1  124   13    4  285%
c i   52.5   51495   355875     29273   15285   2566 137922   13   169   36   8%      2  123   14    5  303%
c i   52.8   51493   355875     29657   15615   2595 137943   13   172   36   8%      2  125   14    5  307%
c i   53.0   51490   355875     29891   15808   2612 137964   13   172   36   7%      2  125   10    5  216%
c i   53.1   51487   355875     29981   15890   2615 137968   13   172   36   8%      2  125   11    5  235%
c i   53.3   51485   355875     30231   16115   2625 137981   13   171   36   8%      2  124   12    5  261%
c i   53.3   51480   355875     30232   16115   2625 137981   13   171   36   8%      2  124   12    5  260%
c i   53.3   51476   355875     30236   16116   2625 137983   13   171   36   8%      2  124   12    5  257%
c i   53.3   51475   355875     30237   16116   2625 137983   13   171   36   8%      2  123   12    5  256%
c i   53.5   51469   355875     30498   16350   2636 137991   13   172   36   8%      2  124   13    5  286%
c i   53.7   51249   355875     30726   16544   2650 138005   13   172   36   8%      1  124   12    5  257%
c i   53.9   51247   355875     30920   16701   2666 138020   13   171   36   8%      1  122   12    5  265%
c i   54.0   51246   355875     31111   16866   2678 138030   13   172   36   7%      1  123   13    5  281%
c i   54.5   51243   355875     31673   17334   2719 138068   13   176   36   8%      2  126   16    5  340%
c i   54.6   51239   355875     31719   17369   2721 138074   13   176   36   8%      2  126   17    5  359%
c i   54.6   51231   355875     31720   17369   2721 138074   13   176   36   8%      2  126   17    5  358%
c i   54.6   51230   355875     31763   17402   2726 138078   13   177   36   7%      2  127   16    5  327%
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   54.8   51229   355875     31890   17507   2733 138086   13   176   36   8%      2  126   15    5  309%
c i   54.9   51226   355875     32068   17660   2742 138093   14   177   36   8%      2  126   17    5  355%
c i   55.1   51225   355875     32272   17825   2757 138110   14   176   36   8%      2  125   20    5  406%
c i   55.2   51224   355875     32485   18009   2761 138124   15   174   36   9%      2  122   25    5  488%
c i   55.2   51222   355875     32617   18130   2765 138129   16   173   37   9%      1  122   32    5  628%
c i   55.3   51221   355875     32689   18194   2768 138132   15   175   37   9%      1  123   27    5  525%
c i   55.6   50951   355875     33011   18479   2784 138144   15   177   37   9%      1  125   18    5  356%
c i   55.8   50949   355875     33255   18688   2791 138159   16   179   37   9%      1  126   18    5  342%
c i   56.6   50947   355875     34323   19612   2840 138229   16   178   38   9%      6  123   15    5  275%
c i   56.7   50942   355875     34405   19684   2844 138233   15   177   38   9%      6  122   13    5  244%
c i   57.0   50941   355875     34737   19968   2860 138253   15   176   38   9%      5  120   15    5  285%
c i   57.1   50889   355875     34867   20083   2866 138260   16   177   38   9%      4  121   19    5  342%
c i   57.2   50886   355875     34998   20199   2874 138264   16   176   38   9%      4  120   18    5  331%
c i   57.5   50885   355875     35391   20539   2898 138282   16   175   38   9%      3  118   19    6  345%
c i   58.0   50881   355875     35984   21065   2920 138317   16   175   38   9%      4  117   14    6  251%
c i   58.2   50674   355875     36216   21268   2925 138335   16   177   38   9%      3  118   19    6  332%
c i   58.2   50661   355875     36305   21340   2930 138346   16   177   38   9%      3  118   17    6  299%
c i   58.8   50657   355875     36901   21848   2963 138381   16   180   38   9%      3  121   15    6  256%
c i   58.9   50655   355875     37012   21945   2967 138388   16   182   38   9%      3  122   14    6  238%
c i   59.1   50654   355875     37191   22100   2979 138395   16   181   38   9%      3  120   15    6  260%
c i   59.8   50653   355875     38067   22868   3015 138437   16   179   39   9%      5  117   19    6  324%
c i   59.9   50644   355875     38288   23050   3024 138453   17   178   39   9%      4  116   21    6  343%
c i   60.0   50643   355875     38409   23158   3028 138461   17   177   39   9%      4  115   18    6  301%
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   60.2   50639   355875     38633   23349   3041 138476   16   177   39   9%      3  114   16    6  260%
c i   60.2   50633   355875     38642   23357   3041 138476   16   177   39   9%      3  114   16    6  259%
c i   60.5   50632   355875     38913   23595   3060 138487   17   181   39   9%      3  117   18    6  288%
c i   60.7   50630   355875     39301   23938   3067 138517   17   181   40   9%      3  117   20    6  326%
c i   60.8   50629   355875     39406   24032   3068 138519   17   182   40   9%      2  117   24    6  381%
c i   61.7   50624   355875     40477   24972   3121 138577   18   185   40  10%      6  119   18    7  269%
c i   61.8   50620   355875     40515   25002   3123 138581   18   185   40  10%      6  118   17    7  254%
c i   61.9   50619   355875     40621   25087   3131 138585   18   185   40  10%      6  119   16    7  251%
c i   61.9   50614   355875     40676   25136   3132 138589   18   185   40  10%      5  119   17    7  266%
c i   62.0   50611   355875     40782   25232   3135 138595   18   186   40  10%      5  119   17    7  253%
c i   62.2   50395   355875     40984   25410   3148 138600   18   187   40  10%      4  120   17    7  254%
c i   62.2   50394   355875     40996   25420   3148 138601   18   187   40  10%      4  120   17    7  252%
c i   63.4   50391   355875     42330   26605   3197 138659   18   187   41  10%      9  117   18    7  263%
c i   63.4   50390   355875     42340   26611   3199 138660   18   187   41  10%      9  117   18    7  256%
c i   63.4   50389   355875     42366   26634   3200 138660   18   186   41  10%      9  117   19    7  272%
c i   63.5   50384   355875     42407   26672   3200 138661   18   187   41  10%      9  117   18    7  257%
c i   63.6   50343   355875     42536   26787   3205 138665   19   186   41  10%      8  117   23    7  335%
c i   64.1   50341   355875     43134   27307   3239 138694   18   189   41  10%      6  118   17    7  236%
c i   64.6   50340   355875     43636   27738   3258 138726   18   190   41  10%      5  119   16    7  229%
c i   64.6   50339   355875     43666   27767   3258 138726   18   191   42  10%      5  119   16    7  228%
c 
c [simplification-11] limit of 3384 binary hit after 3384 binaries
c [quatres-6] found 26548 quaternary clauses 50% in total
c [quatres-6-2] added 11 quaternary resolvents
c [ternres-7] limit 9918564 with penalty 0 = 0 + 0
c [ternres-7] all 50339 free variables schedulable
c [ternres-7] 444 ternary resolvents (0 bin, 444 trn)
c [ternres-7] fully completed ternary resolution
c [decomp-25] removed 1519 variables
c [basicprobe-4] limit 49592820 penalty 0 = 0 + 0
c [basicprobe-4-0] 12822 probes remain 26% after last round
c [basicprobe-4-0] 668 units = 667 failed (100%) + 1 lifted (0%)
c [basicprobe-4-0] removed 1022 variables, found 164835 hbrs
c [bate-2] eliminated 192 asymmetric tautologies during probing
c [unhide-11] limit 1983712 with penalty 0 = 0 + 0
c [unhide-11-11] 14 units, 100 failed, 10096 tauts, 0 hbrs, 44459 literals
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 320 transitive binary clauses
c [transred-7] found 2 units
c [block-4] scheduling all variables this time
c [block-4] scheduled 49053 variables 100%
c [block-4] limit of 24796410 steps penalty 2 = 2 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 195 blocked clauses
c [block-4] 195 < 1/100 * 320050 = 3200 considered unsuccessful
c [cce-4] boosting limit by 10
c [cce-4] limit of 123982050 steps penalty 2 = 2 + 0
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 72
c [cce-4-1] eliminated 1 clauses out of 2 (50%) of length 71
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 70
c [cce-4-1] eliminated 1 clauses out of 2 (50%) of length 69
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 68
c [cce-4-1] eliminated 1 clauses out of 2 (50%) of length 67
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 66
c [cce-4-1] eliminated 1 clauses out of 2 (50%) of length 65
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 64
c [cce-4-1] eliminated 1 clauses out of 2 (50%) of length 63
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 62
c [cce-4-1] eliminated 1 clauses out of 2 (50%) of length 61
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 60
c [cce-4-1] eliminated 1 clauses out of 2 (50%) of length 59
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 58
c [cce-4-1] eliminated 1 clauses out of 2 (50%) of length 57
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 56
c [cce-4-1] eliminated 1 clauses out of 2 (50%) of length 55
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 54
c [cce-4-1] eliminated 1 clauses out of 2 (50%) of length 53
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 52
c [cce-4-1] eliminated 1 clauses out of 2 (50%) of length 51
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 50
c [cce-4-1] eliminated 1 clauses out of 2 (50%) of length 49
c [cce-4-1] eliminated 2 clauses out of 3 (67%) of length 48
c [cce-4-1] eliminated 1 clauses out of 2 (50%) of length 47
c [cce-4-1] eliminated 2 clauses out of 3 (67%) of length 46
c [cce-4-1] eliminated 1 clauses out of 3 (33%) of length 45
c [cce-4-1] eliminated 3 clauses out of 4 (75%) of length 44
c [cce-4-1] eliminated 3 clauses out of 4 (75%) of length 43
c [cce-4-1] eliminated 3 clauses out of 6 (50%) of length 42
c [cce-4-1] eliminated 5 clauses out of 6 (83%) of length 41
c [cce-4-1] eliminated 3 clauses out of 6 (50%) of length 40
c [cce-4-1] eliminated 6 clauses out of 6 (100%) of length 39
c [cce-4-1] eliminated 3 clauses out of 7 (43%) of length 38
c [cce-4-1] eliminated 6 clauses out of 6 (100%) of length 37
c [cce-4-1] eliminated 3 clauses out of 7 (43%) of length 36
c [cce-4-1] eliminated 6 clauses out of 6 (100%) of length 35
c [cce-4-1] eliminated 3 clauses out of 6 (50%) of length 34
c [cce-4-1] eliminated 6 clauses out of 6 (100%) of length 33
c [cce-4-1] eliminated 3 clauses out of 7 (43%) of length 32
c [cce-4-1] eliminated 6 clauses out of 6 (100%) of length 31
c [cce-4-1] eliminated 3 clauses out of 8 (38%) of length 30
c [cce-4-1] eliminated 8 clauses out of 9 (89%) of length 29
c [cce-4-1] eliminated 5 clauses out of 11 (45%) of length 28
c [cce-4-1] eliminated 10 clauses out of 10 (100%) of length 27
c [cce-4-1] eliminated 5 clauses out of 12 (42%) of length 26
c [cce-4-1] eliminated 12 clauses out of 12 (100%) of length 25
c [cce-4-1] eliminated 6 clauses out of 13 (46%) of length 24
c [cce-4-1] eliminated 12 clauses out of 12 (100%) of length 23
c [cce-4-1] eliminated 6 clauses out of 13 (46%) of length 22
c [cce-4-1] eliminated 12 clauses out of 13 (92%) of length 21
c [cce-4-1] eliminated 7 clauses out of 15 (47%) of length 20
c [cce-4-1] eliminated 15 clauses out of 15 (100%) of length 19
c [cce-4-1] eliminated 6 clauses out of 14 (43%) of length 18
c [cce-4-1] eliminated 15 clauses out of 18 (83%) of length 17
c [cce-4-1] eliminated 9 clauses out of 17 (53%) of length 16
c [cce-4-1] eliminated 14 clauses out of 18 (78%) of length 15
c [cce-4-1] eliminated 10 clauses out of 18 (56%) of length 14
c [cce-4-1] eliminated 15 clauses out of 20 (75%) of length 13
c [cce-4-1] eliminated 12 clauses out of 22 (55%) of length 12
c [cce-4-1] eliminated 17 clauses out of 21 (81%) of length 11
c [cce-4-1] eliminated 13 clauses out of 52 (25%) of length 10
c [cce-4-1] eliminated 17 clauses out of 140 (12%) of length 9
c [cce-4-1] eliminated 15 clauses out of 245 (6%) of length 8
c [cce-4-1] eliminated 20 clauses out of 341 (6%) of length 7
c [cce-4-1] eliminated 21 clauses out of 1171 (2%) of length 6
c [cce-4-1] eliminated 9792 clauses out of 15484 (63%) of length 5
c [cce-4-1] eliminated 7336 clauses out of 24649 (30%) of length 4
c [cce-4-1] incomplete large round (ATE)
c [cce-4-1] eliminated 17514 large clauses in 123982050 steps
c [cce-4-1] allowing another 61991025 steps for small clauses
c [cce-4-1] scheduling 177446 clauses = 160747 binary + 16699 ternary
c [cce-4-1] tried to eliminate 5939 small clauses 3%
c [cce-4-1] eliminated 1631 binary clauses 1%
c [cce-4-1] eliminated 246 ternary clauses 1%
c [cce-4-1] eliminated 1877 small clauses 1%
c [cce-4-1] eliminated 1877 small clauses in 123982056 steps
c [cce-4-1] incomplete small round (ATE)
c [cce-4-1] eliminated 19391 covered clauses in round 1
c [cce-4] eliminated 19391 covered clauses in TOTAL during 1 rounds
c [elim-9] no untried remaining variables left
c [elim-9] scheduled 49052 variables 100%
c [elim-9] limit of 198371282 steps penalty 0 = 0 + 0
c [elim-9] rescheduling of touched variables disabled
c [elim-9-1] eliminated 9399 variables 19% in round 1 in 24561144 steps
c [elim-9-1] backward subsumption/strengthening limit 24561100
c [elim-9-1-1] backward checking 23128 touched variables 47%
c [elim-9-1-1] fully completed backward checking in 1 rounds
c [elim-9-1] subsumed 67 and strengthened 239 clauses in 3118008 steps
c [elim-9-1] rescheduled 690 variables 1% by backward subsumption
c [elim-9-2] eliminated 38 variables 0% in round 2 in 586133 steps
c [elim-9-2] backward subsumption/strengthening limit 586100
c [elim-9-2-1] backward checking 407 touched variables 1%
c [elim-9-2-1] fully completed backward checking in 1 rounds
c [elim-9-2] subsumed 19 and strengthened 19 clauses in 350380 steps
c [elim-9-2] rescheduled 78 variables 0% by backward subsumption
c [elim-9-3] eliminated 4 variables 0% in round 3 in 122352 steps
c [elim-9-3] backward subsumption/strengthening limit 122300
c [elim-9-3-1] backward checking 45 touched variables 0%
c [elim-9-3-1] incomplete backward checking 0 remain 0%
c [elim-9-3] subsumed 2 and strengthened 4 clauses in 122301 steps
c [elim-9] incomplete 17 not tried 0% in round 3
c [gc-74] reconnected 284190 binary clauses (produced 0 empty 1 units)
c [elim-9] transition to [ all 1 rem 1 ] state
c [elim-9] eliminated 9456 = 19% variables out of 49052 scheduled
c [bca-7] limit of 10000000 steps and 554006 added (scaled 2)
c [bca-7] 62851 out of 79194 literals actually usable 79%
c [bca-7] added 160 blocked clauses in 146414 steps
c [sweep-7] limit 2975569 penalty 0 = 0 + 0
c [sweep-7-1] 6098 pos 17.9% + 27991 neg 82.1% = 34089 sched 86.1% ret 5507
c [sweep-7-1] 2982207 steps 81 queries 2677.32 avg class size
c [sweep-7-1] 878 decisions 64 SAT calls 116.41 avg env size
c [sweep-7-1] 33325 variables remain 84% (6256 retained 16%)
c [decomp-26] removed 192 variables
c [sweep-7-1] removed 192 vars (0 failed, 17 eqs, 24 impls)
c [sweep-7] removed 192 vars in TOTAL (1 rounds, 80 queries)
c [sort-queue-11] sorted 39404 enqueued variables after 43678 conflicts
c [score-dist-11] active 0 (0%), one 30616 (78%), zero 8788 (22%)
c [score-dist-11] max exp 1, different 2 (100%)
c [score-dist-11] median active exp 0, avg 0.0
c [simplification-11] removed 10935 variables 21.7% (39404 remain 18%)
c [simplification-11] removed 79683 irredundant clauses 22.4% (276192 remain 23%)
c [simplification-11] maximum reduction of 22% = max (22%, 22%)
c [simplification-11] forced so keeping old conflict interval 18332
c [simplification-11] conflict limit remains at 44054 (hard 53988)
c [simplification-11] new binary interval 10000
c 
c [simplification-12] limit 44054 conflicts (hard 53988) hit after 44055 conflicts
c [quatres-7] found 23086 quaternary clauses 68% in total
c [quatres-7-1] removed 11 duplicate quaternary clauses
c [quatres-7-2] added 3 single-self-subsuming ternary resolvents
c [quatres-7-2] added 29 quaternary resolvents
c [ternres-8] limit 9977451 with penalty 0 = 0 + 0
c [ternres-8] all 39404 free variables schedulable
c [ternres-8] 649 ternary resolvents (1 bin, 648 trn)
c [ternres-8] fully completed ternary resolution
c [simpleprobe-5] 12297 schedulable variables 31%
c [simpleprobe-5] limit 39909804 penalty 0 = 0 + 0
c [decomp-28] removed 1176 variables
c [simpleprobe-5] 418 variables remain 1% (37810 retained 99%)
c [simpleprobe-5] removed 1176 variables, found 53417 hbrs, 864 units
c [unhide-12] limit 1995490 with penalty 0 = 0 + 0
c [unhide-12-13] 9 units, 43 failed, 33554 tauts, 0 hbrs, 3715 literals
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 470 transitive binary clauses
c [transred-8] found 2 units
c [elim-10] no untried remaining variables left
c [elim-10] scheduled 38142 variables 100%
c [elim-10] limit of 199549020 steps penalty 0 = 0 + 0
c [elim-10] rescheduling of touched variables disabled
c [elim-10-1] eliminated 713 variables 2% in round 1 in 22315020 steps
c [elim-10-1] backward subsumption/strengthening limit 22315000
c [elim-10-1-1] backward checking 4210 touched variables 11%
c [elim-10-1-1] fully completed backward checking in 1 rounds
c [elim-10-1] subsumed 28 and strengthened 86 clauses in 1082731 steps
c [elim-10-1] rescheduled 270 variables 1% by backward subsumption
c [elim-10-2] eliminated 19 variables 0% in round 2 in 1438999 steps
c [elim-10-2] backward subsumption/strengthening limit 1438900
c [elim-10-2-1] backward checking 171 touched variables 0%
c [elim-10-2-1] fully completed backward checking in 1 rounds
c [elim-10-2] subsumed 13 and strengthened 8 clauses in 150749 steps
c [elim-10-2] rescheduled 46 variables 0% by backward subsumption
c [elim-10-3] eliminated 6 variables 0% in round 3 in 95509 steps
c [elim-10-3] backward subsumption/strengthening limit 95500
c [elim-10-3-1] backward checking 58 touched variables 0%
c [elim-10-3-1] incomplete backward checking 0 remain 0%
c [elim-10-3] subsumed 6 and strengthened 2 clauses in 95501 steps
c [elim-10] incomplete 18 not tried 0% in round 3
c [elim-10] transition to [ all 1 rem 1 ] state
c [elim-10] eliminated 741 = 2% variables out of 38142 scheduled
c [bca-8] limit of 10000000 steps and 514706 added (scaled 2)
c [bca-8] 58459 out of 74804 literals actually usable 78%
c [bca-8] added 63 blocked clauses in 136674 steps
c [sweep-8] limit 2993235 penalty 0 = 0 + 0
c [sweep-8-1] 6077 pos 18.9% + 26062 neg 81.1% = 32139 sched 85.9% ret 5262
c [sweep-8-1] 3086512 steps 93 queries 3471.16 avg class size
c [sweep-8-1] 991 decisions 83 SAT calls 82.10 avg env size
c [sweep-8-1] 31241 variables remain 84% (6155 retained 16%)
c [decomp-29] removed 19 variables
c [sweep-8-1] removed 19 vars (0 failed, 9 eqs, 17 impls)
c [sweep-8] 19 < 1/1000 * 37401 = 37 considered unsuccessful
c [sweep-8] removed 19 vars in TOTAL (1 rounds, 92 queries)
c [sort-queue-12] sorted 37382 enqueued variables after 44055 conflicts
c [score-dist-12] active 0 (0%), one 29945 (80%), zero 7437 (20%)
c [score-dist-12] max exp 1, different 2 (100%)
c [score-dist-12] median active exp 0, avg 0.0
c [simplification-12] removed 2022 variables 5.1% (37382 remain 17%)
c [simplification-12] removed 19348 irredundant clauses 7.0% (256844 remain 21%)
c [simplification-12] maximum reduction of 7% = max (5%, 7%)
c [simplification-12] large reduction 7% >= 5% limit
c [simplification-12] next conflict interval 2000 = 2000/1
c [simplification-12] penalized conflict interval 2000 = 1 * 2000
c [simplification-12] hard conflict limit 56055 (soft 46055 + delta 10000)
c [simplification-12] new conflict limit 46055 (hard 56055)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   77.1   37381   256844     44348    7444   3406 226884   17   184   29   9%      5  111   10    7  136%
c i   77.4   37380   256844     45317    8319   3451 226910   15   199   29   8%      6  124   11    7  147%
c i   77.4   37379   256844     45327    8328   3451 226910   15   199   29   8%      6  124   10    7  144%
c i   77.5   37377   256844     45413    8406   3454 226910   15   197   29   8%      6  122   11    7  151%
c i   77.5   37375   256844     45467    8454   3457 226911   15   196   29   8%      5  121   10    7  138%
c i   77.6   37373   256844     45651    8623   3466 226912   15   195   29   8%      4  119   10    7  134%
c 
c [simplification-13] limit 46056 conflicts (hard 56055) hit after 46057 conflicts
c [quatres-8] found 22287 quaternary clauses 66% in total
c [quatres-8-1] removed 1 duplicate quaternary clauses
c [quatres-8-2] added 3 single-self-subsuming ternary resolvents
c [quatres-8-2] added 9 quaternary resolvents
c [ternres-9] limit 10222819 with penalty 0 = 0 + 0
c [ternres-9] all 37371 free variables schedulable
c [ternres-9] 468 ternary resolvents (0 bin, 468 trn)
c [ternres-9] fully completed ternary resolution
c [decomp-30] removed 14 variables
c [treelook-5] limit 1022281 penalty 0 = 0 + 0 boost 1
c [treelook-5] scheduled 52372 literals 70%
c [treelook-5] scheduling used 875904 steps
c [treelook-5] scheduled completely
c [treelook-5] limit 1022281 penalty 0 = 0 + 0 boost 1
c [treelook-5] used 1036554 steps
c [treelook-5] 52322 literals remain 70%
c [treelook-5] 9811 variables remain to probed next time 26%
c [treelook-5] removed 2 variables, found 5513 hbrs
c [unhide-13] limit 2044563 with penalty 0 = 0 + 0
c [unhide-13-15] 3 units, 40 failed, 11317 tauts, 0 hbrs, 5522 literals
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 377 transitive binary clauses
c [cce-5] limit of 25557049 steps penalty 1 = 1 + 0
c [cce-5-1] eliminated 1 clauses out of 3 (33%) of length 29
c [cce-5-1] eliminated 1 clauses out of 5 (20%) of length 24
c [cce-5-1] eliminated 1 clauses out of 4 (25%) of length 23
c [cce-5-1] eliminated 2 clauses out of 6 (33%) of length 22
c [cce-5-1] eliminated 3 clauses out of 9 (33%) of length 21
c [cce-5-1] eliminated 2 clauses out of 6 (33%) of length 20
c [cce-5-1] eliminated 4 clauses out of 9 (44%) of length 19
c [cce-5-1] eliminated 2 clauses out of 9 (22%) of length 18
c [cce-5-1] eliminated 6 clauses out of 12 (50%) of length 17
c [cce-5-1] eliminated 3 clauses out of 12 (25%) of length 16
c [cce-5-1] eliminated 6 clauses out of 10 (60%) of length 15
c [cce-5-1] eliminated 3 clauses out of 14 (21%) of length 14
c [cce-5-1] eliminated 6 clauses out of 13 (46%) of length 13
c [cce-5-1] eliminated 5 clauses out of 17 (29%) of length 12
c [cce-5-1] eliminated 7 clauses out of 11 (64%) of length 11
c [cce-5-1] eliminated 5 clauses out of 21 (24%) of length 10
c [cce-5-1] eliminated 7 clauses out of 11 (64%) of length 9
c [cce-5-1] eliminated 5 clauses out of 22 (23%) of length 8
c [cce-5-1] eliminated 11 clauses out of 28 (39%) of length 7
c [cce-5-1] eliminated 78 clauses out of 1048 (7%) of length 6
c [cce-5-1] eliminated 167 clauses out of 6334 (3%) of length 5
c [cce-5-1] incomplete large round (ACCE)
c [cce-5-1] eliminated 325 large clauses in 25557053 steps
c [cce-5-1] allowing another 12778526 steps for small clauses
c [cce-5-1] scheduling 142579 clauses = 126960 binary + 15619 ternary
c [cce-5-1] tried to eliminate 1679 small clauses 1%
c [cce-5-1] eliminated 504 binary clauses 0%
c [cce-5-1] eliminated 78 ternary clauses 0%
c [cce-5-1] eliminated 582 small clauses 0%
c [cce-5-1] eliminated 788 small clauses in 25557051 steps
c [cce-5-1] incomplete small round (ACCE)
c [cce-5-1] eliminated 1113 covered clauses in round 1
c [cce-5] eliminated 1113 covered clauses in TOTAL during 1 rounds
c [cce-5] 1113 < 1/100 * 254488 = 2544 considered unsuccessful
c [elim-11] no untried remaining variables left
c [elim-11] scheduled 37321 variables 100%
c [elim-11] limit of 204456394 steps penalty 0 = 0 + 0
c [elim-11] rescheduling of touched variables disabled
c [elim-11-1] eliminated 223 variables 1% in round 1 in 21333145 steps
c [elim-11-1] backward subsumption/strengthening limit 21333100
c [elim-11-1-1] backward checking 1782 touched variables 5%
c [elim-11-1-1] fully completed backward checking in 1 rounds
c [elim-11-1] subsumed 7 and strengthened 40 clauses in 496335 steps
c [elim-11-1] rescheduled 107 variables 0% by backward subsumption
c [elim-11-2] eliminated 8 variables 0% in round 2 in 114139 steps
c [elim-11-2] backward subsumption/strengthening limit 114100
c [elim-11-2-1] backward checking 75 touched variables 0%
c [elim-11-2-1] fully completed backward checking in 1 rounds
c [elim-11-2] subsumed 7 and strengthened 7 clauses in 61718 steps
c [elim-11-2] rescheduled 20 variables 0% by backward subsumption
c [elim-11-3] eliminated 2 variables 0% in round 3 in 15222 steps
c [elim-11-3] backward subsumption/strengthening limit 15200
c [elim-11-3-1] backward checking 11 touched variables 0%
c [elim-11-3-1] incomplete backward checking 0 remain 0%
c [elim-11-3] subsumed 0 and strengthened 0 clauses in 15201 steps
c [elim-11] fully completed in 3 rounds
c [elim-11] transition to [ all 0 rem 0 ] state
c [elim-11] eliminated 234 = 1% variables out of 37321 scheduled
c [elim-11] 234 < 1/100 * 37321 = 373 considered unsuccessful
c [bca-9] limit of 10000000 steps and 506372 added (scaled 2)
c [bca-9] 56222 out of 74176 literals actually usable 76%
c [bca-9] added 44 blocked clauses in 132786 steps
c [sort-queue-13] sorted 37087 enqueued variables after 46057 conflicts
c [score-dist-13] active 0 (0%), one 29794 (80%), zero 7293 (20%)
c [score-dist-13] max exp 1, different 2 (100%)
c [score-dist-13] median active exp 0, avg 0.0
c [simplification-13] removed 284 variables 0.8% (37087 remain 17%)
c [simplification-13] removed 4093 irredundant clauses 1.6% (252751 remain 21%)
c [simplification-13] maximum reduction of 2% = max (1%, 2%)
c [simplification-13] geometric conflict interval increment 6666 = 20000 / 3
c [simplification-13] new conflict interval 24998
c [simplification-13] penalized conflict interval 24998 = 1 * 24998
c [simplification-13] hard conflict limit 83554 (soft 71055 + delta 12499)
c [simplification-13] new conflict limit 71055 (hard 83554)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   80.9   37086   252751     46835    9435   3794 220739   14   190   30   7%      8  112   10    7  139%
c i   81.0   37085   252751     46940    9525   3804 220743   14   188   30   7%      7  110   10    7  141%
c i   81.2   37084   252751     47256    9785   3826 220765   13   184   30   7%      5  106   10    7  132%
c i   81.3   37083   252751     47407    9921   3831 220768   14   184   30   7%      5  106   14    7  192%
c i   81.8   37082   252751     48479   10865   3880 220813   13   177   30   7%      7   97   11    7  155%
c i   81.8   37081   252751     48556   10927   3886 220815   13   178   30   7%      6   98   11    7  154%
c i   81.8   37080   252751     48558   10928   3886 220815   13   178   30   7%      6   98   11    7  153%
c i   81.8   37062   252751     48559   10928   3886 220815   13   178   30   7%      6   98   11    7  152%
c i   81.8   37058   252751     48561   10929   3886 220815   13   178   30   7%      6   98   11    7  151%
c i   82.0   37057   252751     48796   11133   3902 220824   13   176   30   7%      5   95    9    7  126%
c i   82.9   37054   252751     50568   12697   4011 220881   13   174   30   7%     14   91   11    7  145%
c i   83.1   37050   252751     50874   12962   4031 220895   13   171   30   7%     10   87   12    7  158%
c i   83.1   37049   252751     50878   12964   4031 220895   13   171   30   7%     10   87   12    7  158%
c i   83.4   37048   252751     51522   13513   4069 220933   13   169   30   8%      7   84   14    8  179%
c i   83.5   37044   252751     51615   13593   4074 220939   13   171   30   8%      6   86   15    8  194%
c i   83.5   37043   252751     51616   13593   4074 220939   13   171   30   8%      6   86   15    8  194%
c i   83.5   37042   252751     51675   13644   4078 220941   13   170   30   7%      6   86   13    8  172%
c i   84.2   37036   252751     53079   14895   4139 220990   13   166   31   8%     10   80   15    8  198%
c i   84.3   37033   252751     53366   15160   4148 220999   13   161   31   8%      7   74   12    8  157%
c i   84.4   37032   252751     53523   15304   4153 221002   13   158   31   8%      6   71   12    8  149%
c i   84.6   37018   252751     53883   15621   4164 221022   13   158   31   8%      5   70   14    8  182%
c i   85.0   37009   252751     54739   16395   4192 221051   14   160   31   9%      5   72   17    8  221%
c i   85.9   37008   252751     56428   17935   4248 221089   15   157   32   9%     12   67   15    8  188%
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   85.9   37006   252751     56429   17935   4248 221089   15   157   32   9%     12   67   15    8  188%
c i   86.0   36998   252751     56586   18083   4249 221090   15   162   32   9%     10   72   20    8  243%
c i   86.0   36997   252751     56619   18114   4249 221091   15   162   32   9%     10   72   25    8  312%
c i   86.3   36996   252751     57103   18562   4262 221100   15   161   32  10%      7   71   18    8  214%
c i   86.7   36995   252751     57742   19117   4306 221124   15   161   32   9%      5   70   13    8  157%
c i   86.8   36994   252751     57832   19198   4310 221128   15   161   32   9%      4   70   15    8  176%
c i   87.6   36993   252751     59239   20472   4363 221173   15   161   33   9%      9   68   14    8  161%
c i   87.7   36991   252751     59370   20586   4373 221176   15   159   33  10%      8   66   14    8  164%
c i   87.8   36988   252751     59781   20957   4391 221185   15   157   33  10%      5   63   14    8  160%
c i   87.9   36985   252751     59947   21111   4397 221187   15   156   33  10%      4   62   15    8  179%
c i   88.6   36983   252751     61038   22078   4452 221218   15   158   34  10%      6   64   19    9  220%
c i   89.0   36982   252751     62017   22976   4476 221241   16   150   34  11%      6   54   21    9  238%
c i   89.3   36981   252751     62435   23347   4493 221257   16   148   34  11%      4   52   16    9  186%
c i   89.4   36969   252751     62634   23521   4499 221263   17   149   34  11%      3   53   19    9  210%
c i   89.8   36968   252751     63425   24227   4529 221288   17   147   34  11%      4   51   17    9  190%
c i   90.2   36967   252751     64134   24867   4545 221304   17   144   34  12%      3   47   23    9  248%
c i   91.5   36965   252751     66317   26832   4629 221374   18   151   35  12%     18   53   20    9  215%
c i   91.6   36963   252751     66446   26951   4636 221375   18   150   36  12%     15   51   19    9  200%
c i   92.0   36951   252751     66986   27443   4662 221383   18   153   36  12%      9   54   21   10  221%
c i   92.0   36950   252751     67107   27555   4663 221384   19   154   36  12%      8   54   27   10  287%
c i   92.0   36948   252751     67124   27570   4663 221384   19   153   36  12%      8   54   27   10  278%
c i   92.1   36947   252751     67154   27596   4666 221384   19   153   36  12%      8   53   27   10  277%
c i   92.1   36944   252751     67304   27741   4667 221384   19   152   36  13%      6   52   28   10  289%
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   92.3   36943   252751     67623   28019   4678 221393   19   149   36  13%      4   50   20   10  211%
c i   92.3   36942   252751     67682   28075   4678 221395   19   150   36  13%      4   50   23   10  238%
c i   92.3   36929   252751     67683   28075   4678 221395   19   150   36  13%      4   50   23   10  237%
c i   92.9   36928   252751     68534   28862   4697 221413   19   152   36  13%      4   52   19   10  190%
c i   92.9   36927   252751     68574   28899   4697 221415   19   152   36  13%      4   51   18   10  180%
c i   93.4   36895   252751     69325   29590   4719 221445   19   155   36  12%      3   54   18   10  184%
c i   93.8   36894   252751     69952   30164   4733 221469   19   157   36  12%      3   55   22   10  215%
c i   93.9   36893   252751     70097   30302   4737 221471   19   158   36  12%      2   56   20   10  200%
c i   94.2   36892   252751     70627   30792   4746 221487   20   160   36  12%      2   57   21   10  206%
c 
c [simplification-14] limit of 3913 ternary hit after 3913 ternaries
c [quatres-9] found 22308 quaternary clauses 60% in total
c [quatres-9-1] removed 1 duplicate quaternary clauses
c [quatres-9-2] added 4 single-self-subsuming ternary resolvents
c [quatres-9-2] added 12 quaternary resolvents
c [ternres-10] limit 14317763 with penalty 0 = 0 + 0
c [ternres-10] all 36707 free variables schedulable
c [ternres-10] 280 ternary resolvents (2 bin, 278 trn)
c [ternres-10] fully completed ternary resolution
c [gauss-4] limit 357944 penalty 3 = 3 + 0
c [gauss-4] extracted 13 xors of average arity 2.7
c [gauss-4] connected 35 occurrences of 31 variables (average 1.1)
c [gauss-4] limit 357944 penalty 3 = 3 + 0
c [gauss-4] fully completed
c [gauss-4] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-32] removed 39 variables
c [basicprobe-5] limit 71588819 penalty 0 = 0 + 0
c [basicprobe-5-0] 4439 probes remain 12% after last round
c [basicprobe-5-0] 695 units = 673 failed (97%) + 22 lifted (3%)
c [basicprobe-5-0] removed 882 variables, found 220198 hbrs
c [bate-3] eliminated 565 asymmetric tautologies during probing
c [unhide-14] limit 2863552 with penalty 0 = 0 + 0
c [unhide-14-17] 2 units, 59 failed, 27088 tauts, 0 hbrs, 71916 literals
c [transred-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 305 transitive binary clauses
c [bca-10] limit of 10000000 steps and 471804 added (scaled 2)
c [bca-10] 42795 out of 71490 literals actually usable 60%
c [bca-10] added 19 blocked clauses in 122301 steps
c [sweep-9] limit 2147664 penalty 1 = 1 + 0
c [sweep-9-1] 5590 pos 18.6% + 24538 neg 81.4% = 30128 sched 84.3% ret 5616
c [sweep-9-1] 2150718 steps 63 queries 3638.97 avg class size
c [sweep-9-1] 1357 decisions 55 SAT calls 105.07 avg env size
c [sweep-9-1] 29451 variables remain 82% (6285 retained 18%)
c [decomp-33] removed 150 variables
c [sweep-9-1] removed 150 vars (0 failed, 9 eqs, 15 impls)
c [sweep-9] removed 150 vars in TOTAL (1 rounds, 62 queries)
c [sort-queue-14] sorted 35594 enqueued variables after 70690 conflicts
c [score-dist-14] active 0 (0%), one 29773 (84%), zero 5821 (16%)
c [score-dist-14] max exp 1, different 2 (100%)
c [score-dist-14] median active exp 0, avg 0.0
c [simplification-14] removed 1113 variables 3.0% (35594 remain 17%)
c [simplification-14] removed 17595 irredundant clauses 7.0% (235156 remain 20%)
c [simplification-14] maximum reduction of 7% = max (3%, 7%)
c [simplification-14] forced so keeping old conflict interval 24998
c [simplification-14] conflict limit remains at 71107 (hard 83554)
c [simplification-14] new ternary interval 10000
c 
c [simplification-15] limit 71107 conflicts (hard 83554) hit after 71109 conflicts
c [quatres-10] found 20794 quaternary clauses 59% in total
c [quatres-10-1] removed 3 duplicate quaternary clauses
c [quatres-10-2] added 6 single-self-subsuming ternary resolvents
c [ternres-11] limit 14391905 with penalty 0 = 0 + 0
c [ternres-11] all 35594 free variables schedulable
c [ternres-11] 503 ternary resolvents (1 bin, 502 trn)
c [ternres-11] fully completed ternary resolution
c [card-5] limit 449747 penalty 4 = 4 + 0
c [card-5] found 662 at-most-one constraints of average size 4.0
c [card-5] no at-most-two constraint found
c [card-5] using previous limit 449747 for elimination
c [card-5] 662 out of 662 constraints (100%) meet size limits
c [card-5] no units found
c [card-5] no at-most-one constraints generated
c [simpleprobe-6] 371 schedulable variables 1%
c [simpleprobe-6] limit 57567621 penalty 0 = 0 + 0
c [decomp-35] removed 114 variables
c [simpleprobe-6] fully completed simple probing
c [simpleprobe-6] removed 114 variables, found 34073 hbrs, 98 units
c [unhide-15] limit 2878381 with penalty 0 = 0 + 0
c [unhide-15-19] 2 units, 24 failed, 26296 tauts, 0 hbrs, 32450 literals
c [transred-11] limit 2000000 with penalty 0 = 0 + 0
c [transred-11] removed 285 transitive binary clauses
c [block-5] scheduling all variables this time
c [block-5] scheduled 35466 variables 100%
c [block-5] limit of 17989881 steps penalty 3 = 3 + 0
c [block-5] fully completed
c [block-5] transition to [ all 0 rem 0 ] state
c [block-5] eliminated 74 blocked clauses
c [block-5] 74 < 1/100 * 232814 = 2328 considered unsuccessful
c [elim-12] scheduling all variables this time
c [elim-12] scheduled 35462 variables 100%
c [elim-12] limit of 143919053 steps penalty 1 = 1 + 0
c [elim-12] rescheduling of touched variables disabled
c [elim-12-1] eliminated 728 variables 2% in round 1 in 19344470 steps
c [elim-12-1] backward subsumption/strengthening limit 19344400
c [elim-12-1-1] backward checking 4273 touched variables 12%
c [elim-12-1-1] fully completed backward checking in 1 rounds
c [elim-12-1] subsumed 16 and strengthened 98 clauses in 940344 steps
c [elim-12-1] rescheduled 295 variables 1% by backward subsumption
c [elim-12-2] eliminated 13 variables 0% in round 2 in 348528 steps
c [elim-12-2] backward subsumption/strengthening limit 348500
c [elim-12-2-1] backward checking 159 touched variables 0%
c [elim-12-2-1] fully completed backward checking in 1 rounds
c [elim-12-2] subsumed 4 and strengthened 9 clauses in 147973 steps
c [elim-12-2] rescheduled 32 variables 0% by backward subsumption
c [elim-12-3] eliminated 2 variables 0% in round 3 in 82470 steps
c [elim-12-3] backward subsumption/strengthening limit 82400
c [elim-12-3-1] backward checking 18 touched variables 0%
c [elim-12-3-1] fully completed backward checking in 1 rounds
c [elim-12-3] subsumed 1 and strengthened 0 clauses in 39493 steps
c [elim-12] incomplete 2 not tried 0% in round 3
c [elim-12] transition to [ all 1 rem 1 ] state
c [elim-12] eliminated 743 = 2% variables out of 35462 scheduled
c [bca-11] limit of 10000000 steps and 462865 added (scaled 2)
c [bca-11] 41689 out of 69440 literals actually usable 60%
c [bca-11] added 28 blocked clauses in 118537 steps
c [sweep-10] limit 4317571 penalty 0 = 0 + 0
c [sweep-10-1] 5153 pos 17.9% + 23558 neg 82.1% = 28711 sched 82.7% ret 6008
c [sweep-10-1] 4380196 steps 98 queries 2331.00 avg class size
c [sweep-10-1] 2033 decisions 88 SAT calls 133.08 avg env size
c [sweep-10-1] 27397 variables remain 79% (7320 retained 21%)
c [decomp-36] removed 18 variables
c [sweep-10-1] removed 18 vars (0 failed, 9 eqs, 13 impls)
c [sweep-10] 18 < 1/1000 * 34719 = 34 considered unsuccessful
c [sweep-10] removed 18 vars in TOTAL (1 rounds, 97 queries)
c [sort-queue-15] sorted 34701 enqueued variables after 71109 conflicts
c [score-dist-15] active 0 (0%), one 29136 (84%), zero 5565 (16%)
c [score-dist-15] max exp 1, different 2 (100%)
c [score-dist-15] median active exp 0, avg 0.0
c [simplification-15] removed 893 variables 2.5% (34701 remain 16%)
c [simplification-15] removed 4262 irredundant clauses 1.8% (230894 remain 19%)
c [simplification-15] maximum reduction of 3% = max (3%, 2%)
c [simplification-15] geometric conflict interval increment 6249 = 24998 / 4
c [simplification-15] new conflict interval 31247
c [simplification-15] penalized conflict interval 31247 = 1 * 31247
c [simplification-15] hard conflict limit 117979 (soft 102356 + delta 15623)
c [simplification-15] new conflict limit 102356 (hard 117979)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i  105.5   34700   230894     73779   30925   5001 350005   20   162   40  12%     30   57   25   11  234%
c i  105.9   34699   230894     74521   31600   5025 350025   19   159   40  12%     16   54   15   11  137%
c i  106.0   34697   230894     74704   31770   5031 350030   19   159   40  12%     13   53   14   11  133%
c i  106.3   34668   230894     75304   32320   5055 350041   19   157   40  12%      7   51   18   11  172%
c i  106.8   34465   230894     76128   33090   5074 350049   19   158   40  12%      5   52   19   11  175%
c i  107.5   34285   230894     77278   34145   5119 350079   20   158   40  12%      6   50   19   11  176%
c i  107.8   34269   230894     77786   34607   5136 350096   20   156   40  13%      3   48   20   11  181%
c i  108.2   34268   230894     78544   35309   5160 350111   20   157   40  13%      3   49   25   11  218%
c i  109.3   34262   230894     80759   37346   5220 350149   21   159   41  13%     16   49   24   12  210%
c i  110.6   34101   230894     83610   40000   5277 350199   23   155   42  15%     25   43   31   12  259%
c i  110.6   34079   230894     83653   40034   5277 350199   23   154   42  15%     24   42   34   12  276%
c i  110.9   34077   230894     84346   40672   5284 350204   24   148   43  16%     12   35   27   12  220%
c i  112.9   34070   230894     88818   44807   5377 350263   25   167   45  15%     47   51   21   13  162%
c i  113.1   34068   230894     89340   45292   5388 350268   24   167   45  15%     27   50   21   13  158%
c i  113.1   34066   230894     89352   45301   5389 350269   24   167   45  15%     27   50   20   13  154%
c i  113.4   34064   230894     89984   45877   5406 350285   24   166   46  15%     13   48   23   13  170%
c i  114.3   34063   230894     91958   47696   5456 350321   24   159   46  15%     12   40   24   14  177%
c i  115.2   34053   230894     93964   49539   5487 350347   25   164   48  15%     12   44   23   14  162%
c i  115.5   34017   230894     94492   50037   5494 350350   24   166   48  15%      6   46   21   14  151%
c i  115.5   34016   230894     94532   50076   5494 350350   24   167   48  15%      5   47   22   14  156%
c i  115.5   34015   230894     94593   50132   5495 350350   24   165   48  15%      5   45   20   14  145%
c i  118.9   33995   230894    101856   56877   5637 350454   26   171   53  15%     85   46   25   15  163%
c i  119.1   33797   230894    102197   57183   5641 350458   27   173   53  16%     58   47   35   16  225%
c 
c [simplification-16] limit 102356 conflicts (hard 117979) hit after 102356 conflicts
c [quatres-11] found 21018 quaternary clauses 54% in total
c [quatres-11-1] removed 3 duplicate quaternary clauses
c [quatres-11-1] added 1 double-self-subsuming ternary resolvents
c [quatres-11-2] added 9 single-self-subsuming ternary resolvents
c [quatres-11-2] added 10 quaternary resolvents
c [ternres-12] limit 18423588 with penalty 0 = 0 + 0
c [ternres-12] all 33797 free variables schedulable
c [ternres-12] 354 ternary resolvents (2 bin, 352 trn)
c [ternres-12] fully completed ternary resolution
c [decomp-37] removed 934 variables
c [treelook-6] limit 1842358 penalty 0 = 0 + 0 boost 1
c [treelook-6] scheduled 47336 literals 70%
c [treelook-6] scheduling used 970616 steps
c [treelook-6] scheduled completely
c [treelook-6] limit 1842358 penalty 0 = 0 + 0 boost 1
c [treelook-6] used 1917967 steps
c [treelook-6] 47234 literals remain 70%
c [treelook-6] 8553 variables remain to probed next time 25%
c [decomp-38] removed 3 variables
c [treelook-6] removed 3 variables, found 6156 hbrs
c [unhide-16] limit 3684717 with penalty 0 = 0 + 0
c [unhide-16-21] 0 units, 11 failed, 12932 tauts, 0 hbrs, 240657 literals
c [transred-12] limit 2000000 with penalty 0 = 0 + 0
c [transred-12] removed 266 transitive binary clauses
c [cce-6] limit of 23029485 steps penalty 2 = 2 + 0
c [cce-6-1] eliminated 2 clauses out of 4 (50%) of length 49
c [cce-6-1] eliminated 3 clauses out of 4 (75%) of length 48
c [cce-6-1] eliminated 1 clauses out of 3 (33%) of length 47
c [cce-6-1] eliminated 2 clauses out of 3 (67%) of length 46
c [cce-6-1] eliminated 2 clauses out of 4 (50%) of length 45
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 44
c [cce-6-1] eliminated 1 clauses out of 3 (33%) of length 43
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 42
c [cce-6-1] eliminated 2 clauses out of 4 (50%) of length 41
c [cce-6-1] eliminated 1 clauses out of 3 (33%) of length 40
c [cce-6-1] eliminated 2 clauses out of 4 (50%) of length 39
c [cce-6-1] eliminated 1 clauses out of 4 (25%) of length 38
c [cce-6-1] eliminated 2 clauses out of 4 (50%) of length 37
c [cce-6-1] eliminated 1 clauses out of 4 (25%) of length 36
c [cce-6-1] eliminated 2 clauses out of 4 (50%) of length 35
c [cce-6-1] eliminated 1 clauses out of 4 (25%) of length 34
c [cce-6-1] eliminated 2 clauses out of 4 (50%) of length 33
c [cce-6-1] eliminated 1 clauses out of 4 (25%) of length 32
c [cce-6-1] eliminated 2 clauses out of 4 (50%) of length 31
c [cce-6-1] eliminated 1 clauses out of 5 (20%) of length 30
c [cce-6-1] eliminated 2 clauses out of 4 (50%) of length 29
c [cce-6-1] eliminated 1 clauses out of 3 (33%) of length 28
c [cce-6-1] eliminated 2 clauses out of 3 (67%) of length 27
c [cce-6-1] eliminated 1 clauses out of 7 (14%) of length 26
c [cce-6-1] eliminated 2 clauses out of 5 (40%) of length 25
c [cce-6-1] eliminated 1 clauses out of 6 (17%) of length 24
c [cce-6-1] eliminated 2 clauses out of 6 (33%) of length 23
c [cce-6-1] eliminated 1 clauses out of 6 (17%) of length 22
c [cce-6-1] eliminated 2 clauses out of 6 (33%) of length 21
c [cce-6-1] eliminated 1 clauses out of 8 (12%) of length 20
c [cce-6-1] eliminated 2 clauses out of 7 (29%) of length 19
c [cce-6-1] eliminated 3 clauses out of 10 (30%) of length 18
c [cce-6-1] eliminated 1 clauses out of 6 (17%) of length 17
c [cce-6-1] eliminated 4 clauses out of 10 (40%) of length 16
c [cce-6-1] eliminated 2 clauses out of 10 (20%) of length 15
c [cce-6-1] eliminated 6 clauses out of 15 (40%) of length 14
c [cce-6-1] eliminated 5 clauses out of 17 (29%) of length 13
c [cce-6-1] eliminated 7 clauses out of 13 (54%) of length 12
c [cce-6-1] eliminated 5 clauses out of 16 (31%) of length 11
c [cce-6-1] eliminated 10 clauses out of 22 (45%) of length 10
c [cce-6-1] eliminated 8 clauses out of 18 (44%) of length 9
c [cce-6-1] eliminated 9 clauses out of 28 (32%) of length 8
c [cce-6-1] eliminated 10 clauses out of 35 (29%) of length 7
c [cce-6-1] eliminated 9 clauses out of 880 (1%) of length 6
c [cce-6-1] eliminated 65 clauses out of 5811 (1%) of length 5
c [cce-6-1] incomplete large round (ATE)
c [cce-6-1] eliminated 193 large clauses in 23029489 steps
c [cce-6-1] allowing another 11514744 steps for small clauses
c [cce-6-1] scheduling 174170 clauses = 112659 binary + 61511 ternary
c [cce-6-1] tried to eliminate 1241 small clauses 1%
c [cce-6-1] eliminated 204 binary clauses 0%
c [cce-6-1] eliminated 69 ternary clauses 0%
c [cce-6-1] eliminated 273 small clauses 0%
c [cce-6-1] eliminated 283 small clauses in 23029485 steps
c [cce-6-1] incomplete small round (ATE)
c [cce-6-1] eliminated 476 covered clauses in round 1
c [cce-6] eliminated 476 covered clauses in TOTAL during 1 rounds
c [cce-6] 476 < 1/100 * 214673 = 2146 considered unsuccessful
c [elim-13] no untried remaining variables left
c [elim-13] scheduled 33755 variables 100%
c [elim-13] almost no limit of 100000000000 steps
c [elim-13] rescheduling of touched variables disabled
c [elim-13-1] eliminated 189 variables 1% in round 1 in 17196281 steps
c [elim-13-1] backward subsumption/strengthening limit 17196200
c [elim-13-1-1] backward checking 1365 touched variables 4%
c [elim-13-1-1] fully completed backward checking in 1 rounds
c [elim-13-1] subsumed 4 and strengthened 31 clauses in 360172 steps
c [elim-13-1] rescheduled 77 variables 0% by backward subsumption
c [elim-13-2] eliminated 6 variables 0% in round 2 in 116108 steps
c [elim-13-2] backward subsumption/strengthening limit 116100
c [elim-13-2-1] backward checking 89 touched variables 0%
c [elim-13-2-1] fully completed backward checking in 1 rounds
c [elim-13-2] subsumed 6 and strengthened 6 clauses in 55604 steps
c [elim-13-2] rescheduled 25 variables 0% by backward subsumption
c [elim-13-3] eliminated 2 variables 0% in round 3 in 17791 steps
c [elim-13-3] backward subsumption/strengthening limit 17700
c [elim-13-3-1] backward checking 19 touched variables 0%
c [elim-13-3-1] incomplete backward checking 0 remain 0%
c [elim-13-3] subsumed 2 and strengthened 5 clauses in 17701 steps
c [elim-13] incomplete 15 not tried 0% in round 3
c [elim-13] transition to [ all 1 rem 1 ] state
c [elim-13] eliminated 197 = 1% variables out of 33755 scheduled
c [elim-13] 197 < 1/100 * 33755 = 337 considered unsuccessful
c [bca-12] limit of 10000000 steps and 428631 added (scaled 2)
c [bca-12] 34087 out of 67118 literals actually usable 51%
c [bca-12] added 24 blocked clauses in 127192 steps
c [sort-queue-16] sorted 33558 enqueued variables after 102356 conflicts
c [score-dist-16] active 0 (0%), one 28947 (86%), zero 4611 (14%)
c [score-dist-16] max exp 1, different 2 (100%)
c [score-dist-16] median active exp 0, avg 0.0
c [simplification-16] removed 239 variables 0.7% (33558 remain 16%)
c [simplification-16] removed 17036 irredundant clauses 7.4% (213858 remain 18%)
c [simplification-16] maximum reduction of 7% = max (1%, 7%)
c [simplification-16] large reduction 7% >= 5% limit
c [simplification-16] next conflict interval 2000 = 2000/1
c [simplification-16] penalized conflict interval 2000 = 1 * 2000
c [simplification-16] hard conflict limit 114356 (soft 104356 + delta 10000)
c [simplification-16] new conflict limit 104356 (hard 114356)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i  124.1   33557   213858    103476   54686   5864 338686   28   167   55  17%     16   41   32   16  200%
c i  124.3   33556   213858    103752   54936   5867 338694   28   167   55  17%     10   40   31   16  198%
c i  124.4   33544   213858    103973   55137   5872 338702   27   164   55  17%      5   37   25   16  157%
c i  124.5   33543   213858    104170   55330   5873 338703   27   162   55  17%      2   36   25   16  155%
c 
c [simplification-17] limit 104356 conflicts (hard 114356) hit after 104356 conflicts
c [quatres-12] found 20954 quaternary clauses 54% in total
c [quatres-12-1] removed 1 duplicate quaternary clauses
c [quatres-12-2] added 3 single-self-subsuming ternary resolvents
c [quatres-12-2] added 5 quaternary resolvents
c [ternres-13] limit 18644438 with penalty 0 = 0 + 0
c [ternres-13] all 33531 free variables schedulable
c [ternres-13] 196 ternary resolvents (0 bin, 196 trn)
c [ternres-13] fully completed ternary resolution
c [decomp-39] removed 28 variables
c [basicprobe-6] limit 93222192 penalty 0 = 0 + 0
c [basicprobe-6-0] 5099 sched 16%, 570 failed, 22 lifted, 112849 hbrs
c [decomp-40] removed 759 variables
c [basicprobe-6-1] 6608 probes remain 20% after last round
c [basicprobe-6-1] 668 units = 646 failed (97%) + 22 lifted (3%)
c [basicprobe-6-1] removed 857 variables, found 148981 hbrs
c [bate-4] eliminated 366 asymmetric tautologies during probing
c [unhide-17] limit 3728887 with penalty 0 = 0 + 0
c [unhide-17-23] 0 units, 17 failed, 27712 tauts, 0 hbrs, 104435 literals
c [transred-13] limit 2000000 with penalty 0 = 0 + 0
c [transred-13] removed 223 transitive binary clauses
c [bca-13] limit of 10000000 steps and 405851 added (scaled 2)
c [bca-13] 32446 out of 65324 literals actually usable 50%
c [bca-13] added 5 blocked clauses in 124176 steps
c [sweep-11] boosting sweeping limit by 10
c [sweep-11] limit 27966655 penalty 1 = 1 + 0
c [sweep-11-1] 5055 pos 19.5% + 20929 neg 80.5% = 25984 sched 79.6% ret 6677
c [sweep-11-1] 27977863 steps 790 queries 211.32 avg class size
c [sweep-11-1] 21204 decisions 739 SAT calls 135.50 avg env size
c [sweep-11-1] 14192 variables remain 44% (18360 retained 56%)
c [decomp-41] removed 209 variables
c [sweep-11-1] removed 209 vars (0 failed, 54 eqs, 112 impls)
c [sweep-11] removed 209 vars in TOTAL (1 rounds, 789 queries)
c [sort-queue-17] sorted 32452 enqueued variables after 104356 conflicts
c [score-dist-17] active 0 (0%), one 28669 (88%), zero 3783 (12%)
c [score-dist-17] max exp 1, different 2 (100%)
c [score-dist-17] median active exp 0, avg 0.0
c [simplification-17] removed 1079 variables 3.2% (32452 remain 15%)
c [simplification-17] removed 12989 irredundant clauses 6.1% (200869 remain 17%)
c [simplification-17] maximum reduction of 6% = max (3%, 6%)
c [simplification-17] large reduction 6% >= 5% limit
c [simplification-17] next conflict interval 2000 = 2000/1
c [simplification-17] penalized conflict interval 2000 = 1 * 2000
c [simplification-17] hard conflict limit 116356 (soft 106356 + delta 10000)
c [simplification-17] new conflict limit 106356 (hard 116356)
c 
c [simplification-18] limit 106356 conflicts (hard 116356) hit after 106356 conflicts
c [quatres-13] found 20113 quaternary clauses 53% in total
c [quatres-13-1] removed 7 duplicate quaternary clauses
c [quatres-13-2] added 18 single-self-subsuming ternary resolvents
c [ternres-14] limit 18861223 with penalty 0 = 0 + 0
c [ternres-14] all 32452 free variables schedulable
c [ternres-14] 197 ternary resolvents (0 bin, 197 trn)
c [ternres-14] fully completed ternary resolution
c [decomp-42] removed 1 variables
c [simpleprobe-7] all 32451 free variables schedulable
c [simpleprobe-7] limit 75444892 penalty 0 = 0 + 0
c [decomp-43] removed 51 variables
c [simpleprobe-7] fully completed simple probing
c [simpleprobe-7] removed 51 variables, found 42110 hbrs, 18 units
c [unhide-18] limit 3772244 with penalty 0 = 0 + 0
c [unhide-18-25] 2 units, 5 failed, 35821 tauts, 0 hbrs, 98563 literals
c [transred-14] limit 2000000 with penalty 0 = 0 + 0
c [transred-14] removed 274 transitive binary clauses
c [elim-14] no untried remaining variables left
c [elim-14] scheduled 32395 variables 100%
c [elim-14] limit of 188612230 steps penalty 1 = 1 + 0
c [elim-14] rescheduling of touched variables disabled
c [elim-14-1] eliminated 533 variables 2% in round 1 in 15993458 steps
c [elim-14-1] backward subsumption/strengthening limit 15993400
c [elim-14-1-1] backward checking 3409 touched variables 11%
c [elim-14-1-1] fully completed backward checking in 1 rounds
c [elim-14-1] subsumed 6 and strengthened 48 clauses in 713790 steps
c [elim-14-1] rescheduled 152 variables 0% by backward subsumption
c [elim-14-2] eliminated 7 variables 0% in round 2 in 138814 steps
c [elim-14-2] backward subsumption/strengthening limit 138800
c [elim-14-2-1] backward checking 64 touched variables 0%
c [elim-14-2-1] fully completed backward checking in 1 rounds
c [elim-14-2] subsumed 2 and strengthened 3 clauses in 49282 steps
c [elim-14-2] rescheduled 15 variables 0% by backward subsumption
c [elim-14-3] eliminated 1 variables 0% in round 3 in 10401 steps
c [elim-14-3] backward subsumption/strengthening limit 10400
c [elim-14-3-1] backward checking 11 touched variables 0%
c [elim-14-3-1] incomplete backward checking 0 remain 0%
c [elim-14-3] subsumed 1 and strengthened 0 clauses in 10401 steps
c [elim-14] incomplete 3 not tried 0% in round 3
c [elim-14] transition to [ all 1 rem 1 ] state
c [elim-14] eliminated 541 = 2% variables out of 32395 scheduled
c [bca-14] limit of 10000000 steps and 396736 added (scaled 2)
c [bca-14] 31368 out of 63710 literals actually usable 49%
c [bca-14] added 8 blocked clauses in 119732 steps
c [sweep-12] limit 5658366 penalty 0 = 0 + 0
c [sweep-12-1] 3043 pos 21.9% + 10870 neg 78.1% = 13913 sched 43.7% ret 17941
c [sweep-12-1] 5873030 steps 189 queries 530.81 avg class size
c [sweep-12-1] 5127 decisions 172 SAT calls 116.73 avg env size
c [sweep-12-1] 12684 variables remain 40% (19166 retained 60%)
c [decomp-44] removed 25 variables
c [sweep-12-1] removed 25 vars (0 failed, 17 eqs, 30 impls)
c [sweep-12] 25 < 1/1000 * 31854 = 31 considered unsuccessful
c [sweep-12] removed 25 vars in TOTAL (1 rounds, 188 queries)
c [sort-queue-18] sorted 31829 enqueued variables after 106356 conflicts
c [score-dist-18] active 0 (0%), one 28297 (89%), zero 3532 (11%)
c [score-dist-18] max exp 1, different 2 (100%)
c [score-dist-18] median active exp 0, avg 0.0
c [simplification-18] removed 623 variables 1.9% (31829 remain 15%)
c [simplification-18] removed 3011 irredundant clauses 1.5% (197858 remain 17%)
c [simplification-18] maximum reduction of 2% = max (2%, 1%)
c [simplification-18] geometric conflict interval increment 10415 = 31247 / 3
c [simplification-18] new conflict interval 41662
c [simplification-18] penalized conflict interval 41662 = 1 * 41662
c [simplification-18] hard conflict limit 168849 (soft 148018 + delta 20831)
c [simplification-18] new conflict limit 148018 (hard 168849)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i  139.2   31828   197858    106427   52725   5819 379329   27   169   52  16%     10   41   27   16  164%
c i  139.2   31827   197858    106474   52771   5819 379329   27   169   52  16%      9   41   25   16  151%
c i  143.7   31826   197858    116000   61673   5997 379416   27   175   54  15%    113   41   35   18  201%
c -  145.1   31748   197858    119086   25356   6039 379441   28   161   34  17%     18   26   28   18  157%
c i  150.3   31747   197858    133375   38651   6248 379555   26   156   45  17%    209   16   26   19  134%
c i  150.8   31734   197858    134479   39698   6262 379566   27   159   45  17%     45   18   31   20  160%
c i  150.8   31733   197858    134546   39761   6264 379566   27   157   45  17%     39   16   29   20  147%
c i  154.7   31723   197858    145335   49799   6369 379619   26   167   55  16%     99   23   33   21  158%
c 
c [simplification-19] limit 148018 conflicts (hard 168849) hit after 149919 conflicts
c [quatres-14] found 20729 quaternary clauses 51% in total
c [quatres-14-2] added 3 single-self-subsuming ternary resolvents
c [quatres-14-2] added 7 quaternary resolvents
c [ternres-15] limit 22786338 with penalty 0 = 0 + 0
c [ternres-15] all 31723 free variables schedulable
c [ternres-15] 262 ternary resolvents (0 bin, 262 trn)
c [ternres-15] fully completed ternary resolution
c [gauss-5] limit 284829 penalty 4 = 4 + 0
c [gauss-5] extracted 8 xors of average arity 3.0
c [gauss-5] connected 24 occurrences of 24 variables (average 1.0)
c [gauss-5] limit 284829 penalty 4 = 4 + 0
c [gauss-5] fully completed
c [gauss-5] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-45] removed 3 variables
c [treelook-7] limit 2278633 penalty 0 = 0 + 0 boost 1
c [treelook-7] scheduled 44539 literals 70%
c [treelook-7] scheduling used 931050 steps
c [treelook-7] scheduled completely
c [treelook-7] limit 2278633 penalty 0 = 0 + 0 boost 1
c [treelook-7] used 2292241 steps
c [treelook-7] 44460 literals remain 70%
c [treelook-7] 7985 variables remain to probed next time 25%
c [treelook-7] removed 0 variables, found 7763 hbrs
c [unhide-19] limit 4557267 with penalty 0 = 0 + 0
c [unhide-19-28] 1 units, 7 failed, 14814 tauts, 0 hbrs, 501720 literals
c [transred-15] limit 2000000 with penalty 0 = 0 + 0
c [transred-15] removed 248 transitive binary clauses
c [elim-15] no untried remaining variables left
c [elim-15] scheduled 31716 variables 100%
c [elim-15] limit of 455726761 steps penalty 0 = 0 + 0
c [elim-15] rescheduling of touched variables disabled
c [elim-15-1] eliminated 113 variables 0% in round 1 in 15568044 steps
c [elim-15-1] backward subsumption/strengthening limit 15568000
c [elim-15-1-1] backward checking 822 touched variables 3%
c [elim-15-1-1] fully completed backward checking in 1 rounds
c [elim-15-1] subsumed 8 and strengthened 31 clauses in 269347 steps
c [elim-15-1] rescheduled 75 variables 0% by backward subsumption
c [elim-15-2] eliminated 3 variables 0% in round 2 in 713748 steps
c [elim-15-2] backward subsumption/strengthening limit 713700
c [elim-15-2-1] backward checking 77 touched variables 0%
c [elim-15-2-1] fully completed backward checking in 1 rounds
c [elim-15-2] subsumed 1 and strengthened 2 clauses in 46241 steps
c [elim-15-2] rescheduled 6 variables 0% by backward subsumption
c [elim-15-3] eliminated 1 variables 0% in round 3 in 16987 steps
c [elim-15-3] backward subsumption/strengthening limit 16900
c [elim-15-3-1] backward checking 7 touched variables 0%
c [elim-15-3-1] incomplete backward checking 0 remain 0%
c [elim-15-3] subsumed 2 and strengthened 0 clauses in 16901 steps
c [elim-15] incomplete 4 not tried 0% in round 3
c [elim-15] transition to [ all 1 rem 1 ] state
c [elim-15] eliminated 117 = 0% variables out of 31716 scheduled
c [elim-15] 117 < 1/100 * 31716 = 317 considered unsuccessful
c [bca-15] limit of 10000000 steps and 390842 added (scaled 2)
c [bca-15] 31905 out of 63200 literals actually usable 50%
c [bca-15] added 11 blocked clauses in 120770 steps
c [sort-queue-19] sorted 31599 enqueued variables after 149919 conflicts
c [score-dist-19] active 0 (0%), one 28299 (90%), zero 3300 (10%)
c [score-dist-19] max exp 1, different 2 (100%)
c [score-dist-19] median active exp 0, avg 0.0
c [simplification-19] removed 124 variables 0.4% (31599 remain 15%)
c [simplification-19] removed 2904 irredundant clauses 1.5% (194954 remain 16%)
c [simplification-19] maximum reduction of 1% = max (0%, 1%)
c [simplification-19] geometric conflict interval increment 20831 = 41662 / 2
c [simplification-19] new conflict interval 62493
c [simplification-19] penalized conflict interval 62493 = 1 * 62493
c [simplification-19] hard conflict limit 243658 (soft 212412 + delta 31246)
c [simplification-19] new conflict limit 212412 (hard 243658)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i  162.1   31598   194954    152371   54764   6550 369855   27   145   57  18%     40    1   31   21  148%
c -  167.7   31583   194954    166882   33612   6722 369963   26   157   35  17%    146    9   26   22  117%
c i  176.2   31582   194954    191027   56217   6987 370101   30   157   54  19%    416    8   31   23  132%
c -  183.2   31582   194954    207868   38162   7155 370199   31   150   36  21%     80   -0   29   25  117%
c i  184.1   31581   194954    211436   41488   7199 370216   27   138   43  19%    130  -13   18   25   71%
c i  188.7   31571   194954    224543   53762   7305 370269   28   144   50  20%     26   -4   29   25  113%
c i  188.9   31562   194954    225362   54525   7313 370274   28   140   52  20%    -73   -8   26   25  101%
c i  191.6   31549   194954    234246   62769   7376 370311   29   119   59  24%    -27  -26   36   26  140%
c 
c [simplification-20] limit 212412 conflicts (hard 243658) hit after 243658 conflicts
c [quatres-15] found 21587 quaternary clauses 47% in total
c [quatres-15-1] removed 4 duplicate quaternary clauses
c [quatres-15-2] added 3 single-self-subsuming ternary resolvents
c [quatres-15-2] added 19 quaternary resolvents
c [ternres-16] limit 30280687 with penalty 0 = 0 + 0
c [ternres-16] all 31549 free variables schedulable
c [ternres-16] 294 ternary resolvents (0 bin, 294 trn)
c [ternres-16] fully completed ternary resolution
c [decomp-47] removed 56 variables
c [basicprobe-7] limit 151403438 penalty 0 = 0 + 0
c [basicprobe-7-0] 6762 sched 22%, 157 failed, 2 lifted, 54678 hbrs
c [decomp-48] removed 358 variables
c [basicprobe-7-1] 2637 probes remain 9% after last round
c [basicprobe-7-1] 226 units = 223 failed (99%) + 3 lifted (1%)
c [basicprobe-7-1] removed 558 variables, found 76891 hbrs
c [bate-5] eliminated 185 asymmetric tautologies during probing
c [unhide-20] limit 3028068 with penalty 1 = 0 + 1
c [unhide-20-30] 0 units, 2 failed, 28128 tauts, 0 hbrs, 743519 literals
c [transred-16] limit 2000000 with penalty 0 = 0 + 0
c [transred-16] removed 206 transitive binary clauses
c [block-6] scheduling all variables this time
c [block-6] scheduled 30984 variables 100%
c [block-6] limit of 18925429 steps penalty 4 = 4 + 0
c [block-6] fully completed
c [block-6] transition to [ all 0 rem 0 ] state
c [block-6] eliminated 19 blocked clauses
c [block-6] 19 < 1/100 * 187074 = 1870 considered unsuccessful
c [cce-7] limit of 18925429 steps penalty 3 = 3 + 0
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 46
c [cce-7-1] eliminated 1 clauses out of 1 (100%) of length 44
c [cce-7-1] eliminated 2 clauses out of 5 (40%) of length 31
c [cce-7-1] eliminated 2 clauses out of 5 (40%) of length 30
c [cce-7-1] eliminated 2 clauses out of 5 (40%) of length 29
c [cce-7-1] eliminated 3 clauses out of 4 (75%) of length 28
c [cce-7-1] eliminated 1 clauses out of 7 (14%) of length 27
c [cce-7-1] eliminated 4 clauses out of 5 (80%) of length 26
c [cce-7-1] eliminated 4 clauses out of 7 (57%) of length 25
c [cce-7-1] eliminated 3 clauses out of 5 (60%) of length 24
c [cce-7-1] eliminated 3 clauses out of 8 (38%) of length 23
c [cce-7-1] eliminated 5 clauses out of 11 (45%) of length 22
c [cce-7-1] eliminated 3 clauses out of 8 (38%) of length 21
c [cce-7-1] eliminated 4 clauses out of 9 (44%) of length 20
c [cce-7-1] eliminated 5 clauses out of 11 (45%) of length 19
c [cce-7-1] eliminated 6 clauses out of 14 (43%) of length 18
c [cce-7-1] eliminated 6 clauses out of 12 (50%) of length 17
c [cce-7-1] eliminated 6 clauses out of 14 (43%) of length 16
c [cce-7-1] eliminated 6 clauses out of 14 (43%) of length 15
c [cce-7-1] eliminated 3 clauses out of 14 (21%) of length 14
c [cce-7-1] eliminated 7 clauses out of 13 (54%) of length 13
c [cce-7-1] eliminated 5 clauses out of 22 (23%) of length 12
c [cce-7-1] eliminated 5 clauses out of 11 (45%) of length 11
c [cce-7-1] eliminated 7 clauses out of 17 (41%) of length 10
c [cce-7-1] eliminated 5 clauses out of 17 (29%) of length 9
c [cce-7-1] eliminated 11 clauses out of 24 (46%) of length 8
c [cce-7-1] eliminated 4 clauses out of 36 (11%) of length 7
c [cce-7-1] eliminated 12 clauses out of 798 (2%) of length 6
c [cce-7-1] eliminated 22 clauses out of 5513 (0%) of length 5
c [cce-7-1] incomplete large round (ACCE)
c [cce-7-1] eliminated 148 large clauses in 18925430 steps
c [cce-7-1] allowing another 9462715 steps for small clauses
c [cce-7-1] scheduling 149525 clauses = 102327 binary + 47198 ternary
c [cce-7-1] tried to eliminate 1480 small clauses 1%
c [cce-7-1] eliminated 252 binary clauses 0%
c [cce-7-1] eliminated 61 ternary clauses 0%
c [cce-7-1] eliminated 313 small clauses 0%
c [cce-7-1] eliminated 313 small clauses in 18925429 steps
c [cce-7-1] incomplete small round (ACCE)
c [cce-7-1] eliminated 461 covered clauses in round 1
c [cce-7] eliminated 461 covered clauses in TOTAL during 1 rounds
c [cce-7] 461 < 1/100 * 187055 = 1870 considered unsuccessful
c [bca-16] limit of 10000000 steps and 374127 added (scaled 2)
c [bca-16] 29014 out of 61968 literals actually usable 47%
c [bca-16] added 12 blocked clauses in 132769 steps
c [sweep-13] limit 4542103 penalty 1 = 1 + 0
c [sweep-13-1] 2618 pos 21.2% + 9717 neg 78.8% = 12335 sched 39.8% ret 18648
c [sweep-13-1] 4626166 steps 91 queries 718.49 avg class size
c [sweep-13-1] 2690 decisions 84 SAT calls 177.30 avg env size
c [sweep-13-1] 11914 variables remain 38% (19069 retained 62%)
c [decomp-49] removed 19 variables
c [sweep-13-1] removed 19 vars (0 failed, 7 eqs, 9 impls)
c [sweep-13] 19 < 1/1000 * 30983 = 30 considered unsuccessful
c [sweep-13] removed 19 vars in TOTAL (1 rounds, 90 queries)
c [sort-queue-20] sorted 30964 enqueued variables after 243658 conflicts
c [score-dist-20] active 0 (0%), one 28279 (91%), zero 2685 (9%)
c [score-dist-20] max exp 1, different 2 (100%)
c [score-dist-20] median active exp 0, avg 0.0
c [simplification-20] removed 585 variables 1.9% (30964 remain 14%)
c [simplification-20] removed 8385 irredundant clauses 4.3% (186569 remain 16%)
c [simplification-20] maximum reduction of 4% = max (2%, 4%)
c [simplification-20] geometric conflict interval increment 12498 = 62493 / 5
c [simplification-20] new conflict interval 74991
c [simplification-20] penalized conflict interval 74991 = 1 * 74991
c [simplification-20] hard conflict limit 356144 (soft 318649 + delta 37495)
c [simplification-20] new conflict limit 318649 (hard 356144)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c -  207.7   30964   186569    247222   41599   7541 397269   23   106   37  22%     46  -36   19   26   74%
c i  212.9   30963   186569    263772   56957   7664 397324   28   146   52  19%    264    2   42   26  166%
c i  220.8   30960   186569    285629   77234   7837 397397   26   175   74  15%    144   30   21   26   81%
c -  220.9   30834   186569    285674   43980   7837 397397   27   174   38  15%    130   29   25   26   93%
c i  230.5   30833   186569    315321   71426   8059 397494   27   143   65  19%    244   -6   31   26  116%
c i  234.1   30752   186569    323923   79345   8124 397510   30   134   71  23%    -73  -14   34   27  128%
c i  234.1   30749   186569    323929   79347   8124 397513   30   134   71  23%    -74  -14   34   27  125%
c -  234.5   30737   186569    324774   46676   8134 397516   29   123   38  23%   -135  -24   23   27   87%
c i  236.8   30736   186569    331875   53279   8183 397542   31   123   48  25%    -69  -20   39   27  144%
c 
c [simplification-21] limit 318650 conflicts (hard 356144) hit after 345017 conflicts
c [quatres-16] found 21754 quaternary clauses 45% in total
c [quatres-16-1] removed 1 duplicate quaternary clauses
c [quatres-16-2] added 10 single-self-subsuming ternary resolvents
c [quatres-16-2] added 5 quaternary resolvents
c [ternres-17] limit 37758156 with penalty 0 = 0 + 0
c [ternres-17] all 30735 free variables schedulable
c [ternres-17] 227 ternary resolvents (0 bin, 227 trn)
c [ternres-17] fully completed ternary resolution
c [card-6] limit 1179942 penalty 4 = 4 + 0
c [card-6] found 1384 at-most-one constraints of average size 3.9
c [card-6] no at-most-two constraint found
c [card-6] using previous limit 1179942 for elimination
c [card-6] 1384 out of 1384 constraints (100%) meet size limits
c [card-6] no units found
c [card-6] no at-most-one constraints generated
c [decomp-50] removed 232 variables
c [simpleprobe-8] all 30732 free variables schedulable
c [simpleprobe-8] limit 151032624 penalty 0 = 0 + 0
c [decomp-51] removed 12 variables
c [simpleprobe-8] fully completed simple probing
c [simpleprobe-8] removed 12 variables, found 31145 hbrs, 2 units
c [unhide-21] limit 7551631 with penalty 0 = 0 + 0
c [unhide-21-34] 2 units, 5 failed, 42988 tauts, 0 hbrs, 715861 literals
c [transred-17] limit 2000000 with penalty 0 = 0 + 0
c [transred-17] removed 192 transitive binary clauses
c [elim-16] no untried remaining variables left
c [elim-16] scheduled 30576 variables 100%
c [elim-16] limit of 377581562 steps penalty 1 = 1 + 0
c [elim-16] rescheduling of touched variables disabled
c [elim-16-1] eliminated 321 variables 1% in round 1 in 13969183 steps
c [elim-16-1] backward subsumption/strengthening limit 13969100
c [elim-16-1-1] backward checking 2038 touched variables 7%
c [elim-16-1-1] fully completed backward checking in 1 rounds
c [elim-16-1] subsumed 2 and strengthened 41 clauses in 419241 steps
c [elim-16-1] rescheduled 110 variables 0% by backward subsumption
c [elim-16-2] eliminated 2 variables 0% in round 2 in 68902 steps
c [elim-16-2] backward subsumption/strengthening limit 68900
c [elim-16-2-1] backward checking 44 touched variables 0%
c [elim-16-2-1] fully completed backward checking in 1 rounds
c [elim-16-2] subsumed 2 and strengthened 2 clauses in 46717 steps
c [elim-16-2] rescheduled 8 variables 0% by backward subsumption
c [elim-16-3] eliminated 1 variables 0% in round 3 in 31139 steps
c [elim-16-3] backward subsumption/strengthening limit 31100
c [elim-16-3-1] backward checking 7 touched variables 0%
c [elim-16-3-1] incomplete backward checking 0 remain 0%
c [elim-16-3] subsumed 1 and strengthened 0 clauses in 31101 steps
c [elim-16] incomplete 3 not tried 0% in round 3
c [elim-16] transition to [ all 1 rem 1 ] state
c [elim-16] eliminated 324 = 1% variables out of 30576 scheduled
c [bca-17] limit of 10000000 steps and 360785 added (scaled 2)
c [bca-17] 28850 out of 60506 literals actually usable 48%
c [bca-17] added 11 blocked clauses in 121700 steps
c [sort-queue-21] sorted 30252 enqueued variables after 345017 conflicts
c [score-dist-21] active 0 (0%), one 27823 (92%), zero 2429 (8%)
c [score-dist-21] max exp 1, different 2 (100%)
c [score-dist-21] median active exp 0, avg 0.0
c [simplification-21] removed 483 variables 1.6% (30252 remain 14%)
c [simplification-21] removed 6649 irredundant clauses 3.6% (179920 remain 15%)
c [simplification-21] maximum reduction of 4% = max (2%, 4%)
c [simplification-21] geometric conflict interval increment 14998 = 74991 / 5
c [simplification-21] new conflict interval 89989
c [simplification-21] penalized conflict interval 89989 = 1 * 89989
c [simplification-21] hard conflict limit 480000 (soft 435006 + delta 44994)
c [simplification-21] new conflict limit 435006 (hard 480000)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i  249.0   30251   179920    348484   63214   8229 366263   30   143   54  21%     78    1   32   28  116%
c i  253.1   30245   179920    359718   73624   8283 366298   30   117   64  26%      5  -23   15   28   54%
c -  256.1   30240   179920    367984   47007   8338 366325   28   154   37  18%    -32   14   22   28   81%
c i  265.9   30239   179920    399232   76009   8500 366395   26   120   65  21%    369  -22   33   27  119%
c -  268.7   30230   179920    407425   49965   8524 366407   21   164   37  13%   -108   20   26   27   99%
c i  275.2   30229   179920    426545   67756   8633 366480   32   130   56  24%    179   -9   18   27   69%
c -  282.6   30028   179920    446277   51159   8750 366543   31   111   56  27%     78  -24   41   27  151%
c 
c [simplification-22] limit 435006 conflicts (hard 480000) hit after 453605 conflicts
c [quatres-17] found 21698 quaternary clauses 44% in total
c [quatres-17-1] removed 7 duplicate quaternary clauses
c [quatres-17-2] added 6 single-self-subsuming ternary resolvents
c [quatres-17-2] added 15 quaternary resolvents
c [ternres-18] limit 45492841 with penalty 0 = 0 + 0
c [ternres-18] all 30028 free variables schedulable
c [ternres-18] 345 ternary resolvents (1 bin, 344 trn)
c [ternres-18] fully completed ternary resolution
c [decomp-52] removed 233 variables
c [unhide-22] limit 9098568 with penalty 0 = 0 + 0
c [unhide-22-39] 0 units, 2 failed, 14829 tauts, 0 hbrs, 399721 literals
c [transred-18] limit 2000000 with penalty 0 = 0 + 0
c [transred-18] removed 100 transitive binary clauses
c [elim-17] no untried remaining variables left
c [elim-17] scheduled 29892 variables 100%
c [elim-17] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-17] rescheduling of touched variables disabled
c [elim-17-1] eliminated 99 variables 0% in round 1 in 13585079 steps
c [elim-17-1] backward subsumption/strengthening limit 13585000
c [elim-17-1-1] backward checking 655 touched variables 2%
c [elim-17-1-1] fully completed backward checking in 1 rounds
c [elim-17-1] subsumed 6 and strengthened 27 clauses in 158225 steps
c [elim-17-1] rescheduled 76 variables 0% by backward subsumption
c [elim-17-2] eliminated 5 variables 0% in round 2 in 74940 steps
c [elim-17-2] backward subsumption/strengthening limit 74900
c [elim-17-2-1] backward checking 73 touched variables 0%
c [elim-17-2-1] fully completed backward checking in 1 rounds
c [elim-17-2] subsumed 5 and strengthened 1 clauses in 38041 steps
c [elim-17-2] rescheduled 11 variables 0% by backward subsumption
c [elim-17-3] eliminated 2 variables 0% in round 3 in 10659 steps
c [elim-17-3] backward subsumption/strengthening limit 10600
c [elim-17-3-1] backward checking 50 touched variables 0%
c [elim-17-3-1] incomplete backward checking 6 remain 12%
c [elim-17-3] subsumed 3 and strengthened 0 clauses in 10609 steps
c [elim-17] incomplete 5 not tried 0% in round 3
c [elim-17] transition to [ all 1 rem 1 ] state
c [elim-17] eliminated 106 = 0% variables out of 29892 scheduled
c [elim-17] 106 < 1/100 * 29892 = 298 considered unsuccessful
c [bca-18] limit of 10000000 steps and 353447 added (scaled 2)
c [bca-18] 28396 out of 59574 literals actually usable 48%
c [bca-18] added 13 blocked clauses in 117455 steps
c [sort-queue-22] sorted 29786 enqueued variables after 453605 conflicts
c [score-dist-22] active 0 (0%), one 27438 (92%), zero 2348 (8%)
c [score-dist-22] max exp 1, different 2 (100%)
c [score-dist-22] median active exp 0, avg 0.0
c [simplification-22] removed 242 variables 0.8% (29786 remain 14%)
c [simplification-22] removed 3672 irredundant clauses 2.0% (176248 remain 15%)
c [simplification-22] maximum reduction of 2% = max (1%, 2%)
c [simplification-22] geometric conflict interval increment 29996 = 89989 / 3
c [simplification-22] new conflict interval 119985
c [simplification-22] penalized conflict interval 119985 = 1 * 119985
c [simplification-22] hard conflict limit 633582 (soft 573590 + delta 59992)
c [simplification-22] new conflict limit 573590 (hard 633582)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i  296.5   29785   176248    473715   75307   9040 347879   31   121   59  25%    401   -9   38   27  140%
c -  301.1   29774   176248    486457   51990   9098 347903   27   158   36  17%   -105   24   32   27  116%
c -  316.3   29774   176248    526737   53380   9294 347981   29   117   54  25%    413  -16   25   28   89%
c i  324.7   29773   176248    550427   75443   9364 348036   25    97   82  26%    599  -32   39   27  141%
c -  331.4   29768   176248    568001   55452   9443 348083   24    92   55  26%   -233  -30   33   28  118%
c 
c [simplification-23] limit 573590 conflicts (hard 633582) hit after 593085 conflicts
c [quatres-18] found 22305 quaternary clauses 41% in total
c [quatres-18-1] removed 8 duplicate quaternary clauses
c [quatres-18-2] added 8 single-self-subsuming ternary resolvents
c [quatres-18-2] added 11 quaternary resolvents
c [ternres-19] limit 56106988 with penalty 0 = 0 + 0
c [ternres-19] all 29768 free variables schedulable
c [ternres-19] 369 ternary resolvents (1 bin, 368 trn)
c [ternres-19] fully completed ternary resolution
c [decomp-53] removed 38 variables
c [treelook-8] limit 2805349 penalty 1 = 1 + 0 boost 1
c [treelook-8] scheduled 41639 literals 70%
c [treelook-8] scheduling used 911271 steps
c [treelook-8] scheduled completely
c [treelook-8] limit 2805349 penalty 1 = 1 + 0 boost 1
c [treelook-8] used 2810557 steps
c [treelook-8] 41475 literals remain 70%
c [treelook-8] 7018 variables remain to probed next time 24%
c [treelook-8] removed 0 variables, found 12912 hbrs
c [unhide-23] limit 11221397 with penalty 0 = 0 + 0
c [unhide-23-44] 0 units, 18 failed, 11927 tauts, 0 hbrs, 1059486 literals
c [transred-19] limit 2000000 with penalty 0 = 0 + 0
c [transred-19] removed 113 transitive binary clauses
c [bca-19] limit of 10000000 steps and 348933 added (scaled 2)
c [bca-19] 26468 out of 59282 literals actually usable 45%
c [bca-19] added 8 blocked clauses in 135271 steps
c [sweep-14] limit 4208024 penalty 2 = 2 + 0
c [sweep-14-1] 2468 pos 22.1% + 8699 neg 77.9% = 11167 sched 37.7% ret 18473
c [sweep-14-1] 4219092 steps 60 queries 750.50 avg class size
c [sweep-14-1] 2200 decisions 58 SAT calls 142.72 avg env size
c [sweep-14-1] 10831 variables remain 37% (18809 retained 63%)
c [decomp-55] removed 9 variables
c [sweep-14-1] removed 9 vars (0 failed, 1 eqs, 4 impls)
c [sweep-14] 9 < 1/1000 * 29640 = 29 considered unsuccessful
c [sweep-14] removed 9 vars in TOTAL (1 rounds, 59 queries)
c [sort-queue-23] sorted 29631 enqueued variables after 593085 conflicts
c [score-dist-23] active 0 (0%), one 27403 (92%), zero 2228 (8%)
c [score-dist-23] max exp 1, different 2 (100%)
c [score-dist-23] median active exp 0, avg 0.0
c [simplification-23] removed 137 variables 0.5% (29631 remain 14%)
c [simplification-23] removed 2274 irredundant clauses 1.3% (173974 remain 15%)
c [simplification-23] maximum reduction of 1% = max (0%, 1%)
c [simplification-23] geometric conflict interval increment 59992 = 119985 / 2
c [simplification-23] new conflict interval 179977
c [simplification-23] penalized conflict interval 179977 = 1 * 179977
c [simplification-23] hard conflict limit 863050 (soft 773062 + delta 89988)
c [simplification-23] new conflict limit 773062 (hard 863050)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c -  353.3   29631   173974    608974   57098   9881 350718   30    90   37  33%    352  -22   33   27  121%
c i  363.6   29630   173974    638007   84105   9992 350773   30   118   68  26%    592    5   47   27  175%
c i  363.6   29626   173974    638008   84105   9992 350773   30   118   68  26%    591    5   47   27  175%
c -  369.1   29625   173974    650728   58333  10050 350788   32   110   38  29%   -476   -3   31   28  112%
c 1  384.3   29625   173974    693058   97560  10223 350862   28   116   93  24%    237    0   30   28  109%
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
s SATISFIABLE
c
c bate: 1410 basic ate = 1242 trn 88% + 168 lrg 12% in 5 updates
c bcas: 19 count, 923 added (1555 skipped), 3274727 steps
c bkwd: tried 325894 clauses, 650765 lits, 2.00 lits/clause
c bkwd: checked 8591690 occs, 26.36 occs/clause, 13.20 occs/lit
c bkwd: subsumed 41 binary, 352 ternary, 125 large
c bkwd: strengthened 13 binary, 0 ternary (0% self), 1313 large (0% self)
c blkd: 6 bces, 8566 removed, 6698424 resolutions, 18794218 steps
c blkd: 9072 blocking literals 2%, 72 pure
c bump: 691887 bumped seen, 191969159 lits 277.5 on average
c card: 6 count, 0 units, 0 am1, 101718051 steps
c card: 0 rescheduled, 0 eliminated, 0 resolved, 66862 subsumed
c card: 14868 at-most-one constraints found, average size 4.89
c card: 14868 at-most-one constraints used 100%, average size 4.89
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, 28314 eliminated, 28231 ate 100%, 83 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 clls: 1 sat, 0 simp, 0 freeze, 0 melt
c clls: 4121578 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 165 gcs, 0 rescored clauses, 0 rescored vars
c dcps: 55 decompositions, 8747 equivalent 4%
c deco: 7665 decision-only clauses 1%, 58% reduction
c decs: 6099662 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 17 elims, 90789 eliminated 40%, 79 pure 0%
c elms: 51 rounds, 3.0 rounds/bve
c elms: 77053 small 85%, 13585 large 15%
c elms: 204592 tried small, 77055 succeeded 38%, 127537 failed 62%
c elms: 36253 subsumed, 57130 strengthened, 924 blocked
c elms: 16234643 copies, 15413338 resolutions, 5570505 ipos
c elms: 3835980 subchks, 2782633 strchks
c gaus: 5 extractions, 273 extracted, 2.4 size, 3 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 8286398 steps, 4143199 extr 50%, 2692 elim 0%
c glue: 25.8 orig avg, 25.8 real avg, 4.2 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 1060961 = 239499 simple 23% + 804502 trn 76% + 16960 lrg 2%, 4932 sub 0%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 691887 clauses, 137.6 length
c lrnd: 95171942 lits = 143094090 orig - 47922148 removed 33%
c lrnd: 289961 uips 42%, 340873 flips 49%
c mins: 666835 mins 96%, 4940 bin 1%, 11585 size 2%
c mins: 409579390 poisoned searches, 65052112 hits, 16% hit rate
c mins: 481634253 used twice searches, 10935606 hits, 2% hit rate
c move: moved 16911, 10841 bin 64%, 6070 trn 36%
c otfs: 2354 driving 22%, 8581 restarting 78%
c otfs: str 10935, 10733 red 98%, 202 irr 2%
c otfs: str 10935, 0 bin 0%, 187 trn 2%, 10748 lrg 98%
c otfs: sub 20, 20 red 100%, 0 irr 0%
c otfs: sub 20, 0 bin 0%, 0 trn 0%, 20 lrg 100%
c phas: 5 computed, 116508 set, 0 pos (0%), 116508 neg (100%)
c prbs: 7 basic, 67744 probed, 2671 failed, 78 lifted
c prbs: 8 simple, 715715 probed, 1829 failed, 780 eqs
c prbs: 8 treelook, 429 probed, 8 failed, 0 lifted
c prom: 194980 locked 10% out of 1889288 tried
c prps: 807575394 props, 125 props/dec
c prps: 95% srch, 5% simp, 0% lkhd
c quat: 18 count, 189 quat, 101 self1, 2 self2, 1137 dup
c queu: 23 sorted, 6099662 next (21 steps 0.00)
c queu: 193333992 enq (0 steps 0.00), 191969159 deq 99%
c redc: 20730 clauses 33%, 62406 tried 9%, 318 sat 1%
c redc: 57304 lits 8%, 748527 tried 1%, 318 sat 0%
c redc: 2748 times jump level reduced, 16.5 levels on average
c reds: 14 count, 49504.1 conflicts per reduce
c reds: 0 memlim 0%, 14 arith 100%
c reds: 395675 collected 80%, 96288 retired 20%
c rmbd: 44970 removed, 8084 red 18%
c rsts: 18488 restarts 100%, 0 skipped 0%
c rsts: 0 saturating 0%, 0 reuse 0%
c rsts: 0 kept 0.0% average 0.0%
c simp: 23 count, 18 confs 78%, 0 vars 0%
c simp: 2 its 9%, 2 bin 9%, 1 trns 4%
c subl: 691887 count (622564 tried 0.9), 35636 sub out of 675773 (5.3%)
c swps: 14 count, 14 rounds, 1867 queries (133.4/round)
c swps: 1687 sat calls, 26 unsat (0.7% success rate)
c swps: 40854 decisions 24.2, 1183 conflicts 0.7
c swps; 1874.6 avg class size, 121.2 avg environment size
c swps: 0 failed, 367 impls, 195 equivs
c swp0: 616 type 0 queries, 197 unsat (32.0%), 587 sat (95.3%)
c swp1: 1251 type 1 queries, 711 unsat (56.8%), 1085 sat (86.7%)
c sync: 0 produced units, 0 successful consumptions 0%
c sync: 0 consume units calls, 0 tried 0%, 0 success 0%
c sync: 0 produced clauses, 0 successful consumptions 0%
c sync: 0 consume clause calls, 0 tried 0%, 0 success 0%
c time: 13584035 calls to obtain time
c tops: 96765 fixed 43%, 500 its, 1386.12 confs/it
c trds: 19 transitive reductions, 5115 removed, 21 failed
c trds: 28248 nodes, 81838 edges, 37613877 steps
c trim: 1649580 words, 6.3 MB
c trnr: 19 count, 12 bin, 5869 trn, 126254438 steps
c unhd: 23 count, 44 rounds, 101840936 steps
c unhd: 2362 non-trivial sccs of average size 2.2
c unhd: 263 units, 261 bin, 1 trn, 1 lrg
c unhd: 13031 failed, 12837 stamp, 0 lits, 163 bin, 23 trn, 1 lrg
c unhd: 383766 tauts, 10894 bin 3%, 10149 trn 3%, 1356 lrg 0%
c unhd: 383766 tauts, 361367 stamp 94%, 310959 red 81%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 4102827 str, 261 bin 0%, 5049 trn 0%, 4097517 lrg 100%, 4081271 red 99%
c vars: 29625 remaining 13% and 196301 removed 87% out of 225926
c vars: 96765 fixed 43%, 90789 eliminated 40%, 8747 equivalent 4%
c vsts: 6763118192 visits, 95% srch, 5% simp, 0% lkhd
c vsts: 8.4 search visits per propagation, 9249.3 per conflict
c wchs: 1242398183 pushed, 40673820 enlarged, 244 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all         675962        395675         96288      45871699       6604920        332634
c 
c  0 0         62288   9     15261   4         0   0  26633409  58   2795589  42     76752  23     2.1
c  1 5         25203   4     11571   3      4187   4   3647312   8<   559816   8     22425   7     0.9
c  2 6         72561  11     41265  10     10566  11   6087580  13   1037341  16<    51765  16     3.1
c  3 9        102880  15     66502  17     13857  14   4034721   9    798499  12     53136  16<    4.6
c  4 14       108775  16<    72287  18     15255  16   2531872   6    558697   8     43238  13     5.2
c  5 21        98231  15     65083  16<    14385  15<  1374487   3    354484   5     31538   9     5.4
c  6 30        78611  12     50853  13     12157  13    806215   2    232698   4     23001   7     4.5
c  7 41        55325   8     34749   9      9306  10    401432   1    132917   2     14718   4     3.5
c  8 54        32865   5     20211   5      6395   7    175383   0     69664   1      8223   2     2.3
c  9 69        17376   3      9874   2      4172   4     92712   0     32172   0      3874   1     1.0
c 10 86        11702   2      5935   1      3085   3     64990   0     22792   0      2665   1     0.7
c 11 126        8224   1      1816   0      2312   2     19055   0      8853   0      1143   0     0.5
c 12 230        1919   0       268   0       610   1      2525   0      1398   0       156   0     0.2
c 13 534           2   0         0   0         1   0         6   0         0   0         0   0     0.0
c 
c avg                  4.3           4.5           5.1           1.2           1.9           3.0
c std                  2.5           2.2           2.5           1.8           2.2           2.5
c 
c   27.994   7% unhide
c   27.570   7% probe
c   15.227   4% elim
c   14.782   4% bump
c    8.609   2% cce
c    7.580   2% sweep
c    3.876   1% decide
c    2.578   1% bca
c    2.258   1% transred
c 
c    5.209 < 1% rest (below)
c 
c    2.010   1% block
c    1.061   0% gauss
c    0.921   0% ternres
c    0.893   0% quatres
c    0.324   0% card
c    0.000   0% locs
c    0.000   0% queuesort
c    0.000   0% rescore
c ==================================
c    4.575   1% preprocessing     4%
c  101.334  26% inprocessing     96%
c ==================================
c  105.909  28% simplifying
c  278.423  72% search
c ==================================
c  384.347 100% all
c 
c        693058 conflicts,        1803.2 confs/sec
c          8639 ternaries,          80.2 confs/ternary
c          6757 binaries,          102.6 confs/binary
c           500 iterations,       1386.1 confs/iteration
c 
c            14 reductions,          0.0 redus/sec,  49504.1 confs/reduction
c         18488 restarts,           48.1 rests/sec,     37.5 confs/restart
c       6099662 decisions,       15870.2 decis/sec,      8.8 decis/conflict
c     807575394 propagations,  2101163.1 props/sec,    132.4 props/decision
c 
c 384.3 seconds, 100.5 MB
c launch: done
