c launch: /data/cnf/sc2014/app/UCG-20-5p0.cnf.bz2
c host: atom32
c Lingeling SAT Solver
c 
c Version b7ztzu 7b29300825af9bcc1c8b2c5ebcf65fa1cb101cad
c 
c Copyright (C) 2010-2014 Armin Biere JKU Linz Austria.
c All rights reserved.
c 
c released Sun Apr 26 19:26:13 CEST 2015
c compiled Sun Apr 26 19:26:13 CEST 2015
c 
c gcc (Ubuntu 4.8.2-19ubuntu1) 4.8.2
c -Wall -O3 -I../yalsat -I../druplig -DNLGLOG -DNDEBUG -DNCHKSOL
c Linux cluster2 3.13.0-45-generic x86_64
c 
c piping '/data/cnf/sc2014/app/UCG-20-5p0.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/UCG-20-5p0.cnf.bz2
c no embedded options
c found 'p cnf 224587 1190673' header
c read 224587 variables, 1190673 clauses, 2868616 literals in 0.00 seconds
c
c --abstime=0
c --bate=1
c --batewait=2
c --bca=1
c --bcaddlimldscale=2
c --bcamaxeff=10000000
c --bcaminuse=100
c --bcawait=2
c --bkwdscale=100
c --bkwdroundlim=7
c --bkwdresched=1
c --blkboost=10
c --blkboostvlim=10000000
c --blkclslim=1000000
c --blklarge=1
c --blkmaxeff=800000000
c --blkmineff=50000000
c --blkocclim1=100000
c --blkocclim=1000000
c --blkocclim2=10000
c --blkreleff=100
c --blkresched=1
c --blkrtc=0
c --blksmall=1
c --blksuccessmaxwortc=6
c --blksuccessrat=100
c --block=1
c --blockwait=1
c --boost=1
c --bumpsimp=1
c --card=1
c --cardcut=2
c --cardexpam1=3
c --cardglue=0
c --cardignused=0
c --cardmaxeff=300000000
c --cardmaxlen=1000
c --cardmineff=2000000
c --cardminlen=3
c --cardocclim1=300
c --cardocclim2=15
c --cardreleff=5
c --cardreschedint=10
c --carduse=2
c --cardwait=0
c --cce2wait=1
c --cce=3
c --cceateint=2
c --cceboost=10
c --cceboostdel=3
c --cceboostint=5
c --cceboostvlim=10000000
c --cce3wait=2
c --ccemaxround=3
c --ccemaxeff=2147483647
c --ccemineff=30000000
c --ccereleff=50
c --ccertc=0
c --ccertcint=15
c --ccertcintvlim=2000000
c --ccesuccessrat=100
c --ccewait=2
c --clim=-1
c --compact=0
c --deco=1
c --decolim=100
c --deco1opt=1
c --decompose=1
c --defragfree=50
c --defragint=10000000
c --delmax=10
c --dlim=-1
c --druplig=0
c --drupligcheck=0
c --drupligtrace=0
c --drupligtraceorig=0
c --elim=1
c --elmaxeff=800000000
c --elmblk=1
c --elmblkwait=1
c --elmboost=20
c --elmboostdel=3
c --elmboostint=5
c --elmboostvlim=4000000
c --elmclslim=1000000
c --elmfull=0
c --elmineff=20000000
c --elmlitslim=200
c --elmocclim1=1000
c --elmocclim=1000000
c --elmocclim2=100
c --elmoccsumforced=0
c --elmreleff=200
c --elmresched=0
c --elmroundlim=3
c --elmrtc=0
c --elmrtcint=10
c --elmrtcintvlim=500000
c --elmsuccessmaxwortc=4
c --elmsuccessrat=100
c --exitonabort=0
c --factmax=100000
c --factor=3
c --gauss=1
c --gaussexptrn=1
c --gaussextrall=1
c --gaussmaxeff=50000000
c --gaussmaxor=20
c --gaussmineff=2000000
c --gaussreleff=2
c --gausswait=2
c --gluekeep=4
c --gluekeepsize=15
c --gluescale=4
c --hbrdom=2
c --import=1
c --incredcint=1
c --incredconfslim=0
c --incsavevisits=0
c --inprocessing=1
c --irrlim=1
c --jwhred=1
c --keepmaxglue=1
c --keepmaxglueint=100
c --lhbr=1
c --lkhd=2
c --locs=0
c --locsbanner=0
c --locsclim=1000000
c --locsboost=2
c --locscint=10000
c --locset=2
c --locsexport=1
c --locsmaxeff=100000
c --locsmineff=1000
c --locsred=0
c --locsreleff=5
c --locsrtc=0
c --locsvared=100
c --locswait=2
c --maxscaledglue=15
c --memlim=-1
c --minimize=2
c --minlocalgluelim=200
c --minlocalsizelim=3000
c --minrecgluelim=100
c --minrecsizelim=1000
c --norestartsatlimlo=85
c --move=2
c --otfs=1
c --penmax=4
c --phase=0
c --phaseluckfactor=200
c --phaselucklim=100
c --phaseluckmaxround=10
c --phasesave=1
c --plain=0
c --plim=-1
c --poison=1
c --prbasic=1
c --prbasicmaxeff=400000000
c --prbasicmineff=1000000
c --prbasicreleff=50
c --prbasicroundlim=8
c --prbasicrtc=0
c --prbrtc=0
c --prbsimple=2
c --prbsimpleboost=10
c --prbsimpleliftdepth=2
c --prbsimplemaxeff=200000000
c --prbsimplemineff=2000000
c --prbsimplereleff=40
c --prbsimplertc=0
c --probe=1
c --promote=1
c --promotegluelim=8
c --pure=1
c --quatres=1
c --quatreswait=2
c --queuesort=1
c --queuesortjwh=0
c --randec=0
c --randecint=1000
c --redcls=1
c --redclsglue=6
c --redclsmaxdec=5
c --redclsmaxdepth=10
c --redclsmaxlrg=10
c --redclsmaxprops=100
c --redclsatlimlo=0
c --redclsatlimhi=100
c --redclsize=30
c --redclstype=4
c --reducefixed=0
c --reduceinc=1000
c --reduceinit=50000
c --reduce=1
c --restart=4
c --restartglcint=10
c --restartglclim=115
c --restartinit=0
c --restartint=5
c --restartpen=1
c --retirenb=1
c --retireint=4
c --retiremin=1
c --reusetrail=0
c --rmincpen=4
c --rstinoutinc=110
c --satlimdelay=10000
c --scincinc=200
c --scincincsatlimhi=100
c --scincincdelta=10
c --scincincincint=100000
c --scincincmin=200
c --scincincmode=1
c --score=5
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 213184 free variables 0%
c [limits] no decision limit
c [limits] no conflict limit
c [limits] no propagation limit
c [limits] simplification not delayed since 'simpdelay' zero
c [set-maximum-score] maximum score limit 1.000000d+500
c [set-minimum-score] minimum score limit 1.000000d-500
c [score-type] EVSIDS (--score=5)
c [set-score-increment-1] factor 1.200000d+00 (200/1000) after 0 conflicts
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  213184  1178520         0       0      0     0    0     0   55   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 3890 at-most-one constraints of average size 5.6
c [card-1] no at-most-two constraint found
c [card-1] using previous limit 2000000 for elimination
c [card-1] 3890 out of 3890 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 51698 variables
c [simpleprobe-1] all 172889 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 203 variables
c [simpleprobe-1] 9771 variables remain 6% (162915 retained 94%)
c [simpleprobe-1] removed 203 variables, found 14534 hbrs, 20 units
c [unhide-1] limit 57075 based on 913200 irredundant clauses
c [unhide-1-1] 48 units, 1097 failed, 7918 tauts, 0 hbrs, 11588 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 170685 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 46391 not tried 27% in round 1
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 65787 = 39% variables out of 170685 scheduled
c [elim-1] considered successful since not run to completion yet
c [phase-count-1] 751369 negative 99.2% of 757269 except 5900 0.8%
c [phase-count-1] 606227 positive 80.1% of 757269 except 151042 19.9%
c [phase-count-1] less non-negative clauses 5900 than limit 75700 (10.0%)
c [phase-count-1] non-pos/non-neg = 151042/5900 = 25.60 >= 2.00 = 200/100
c [lucky-phase-1] forcing lucky phase -1
c [phase-1] phase bias: 0 positive 0%, 104898 negative 100%
c [sort-queue-1] sorted 104898 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 104898 (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 72846 variables 41.0% (104898 remain 49%)
c [simplification-1] removed 421251 irredundant clauses 35.7% (757269 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.5  104897   757269        13      12      0  9783    0     5   51   2%      0    5    2    0 24899%
c i    4.5  103888   757269        47      33      5  9788    0     7   52   3%      0    7    2    0 22838%
c i    4.6  101250   757269        67      46      7  9792    0     8   52   3%      0    8    3    0 22188%
c i    4.6  101238   757269       122      74     19  9804    0     8   52   3%      0    8    3    0 18647%
c i    4.6  100535   757269       154     100     20  9806    0     9   52   4%      0    9    4    0 17749%
c i    4.6   99642   757269       168     109     21  9808    0     9   52   4%      0    9    4    0 17127%
c i    4.7   99171   757269       239     169     24  9814    1    11   52   5%      0   11    6    0 16233%
c i    4.7   98780   757269       243     171     24  9815    1    11   52   5%      0   11    6    0 16057%
c i    4.7   98570   757269       256     181     25  9816    1    11   52   5%      0   11    6    0 15551%
c i    4.8   98559   757269       380     287     33  9824    1    15   52   5%      0   15    6    0 12079%
c 
c [simplification-2] limit of 10 iterations hit after 10 iterations
c [decomp-3] removed 7788 variables
c [simpleprobe-2] 8700 schedulable variables 9%
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [simpleprobe-2] 9297 variables remain 10% (87813 retained 90%)
c [simpleprobe-2] removed 0 variables, found 1753 hbrs, 0 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 65033 literals 33%
c [treelook-1] scheduling used 491904 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 406617 steps
c [treelook-1] 65027 literals remain 33%
c [treelook-1] 64682 variables remain to probed next time 67%
c [treelook-1] removed 0 variables, found 3579 hbrs
c [basicprobe-1] limit 5563096 based on 695387 irredundant clauses
c [basicprobe-1-0] 31019 probes remain 36% after last round
c [basicprobe-1-0] 45 units = 45 failed (100%) + 0 lifted (0%)
c [basicprobe-1-0] removed 11951 variables, found 16627 hbrs
c [unhide-2] limit 100000 with penalty 0 = 0 + 0
c [unhide-2-2] 19 units, 2865 failed, 8050 tauts, 0 hbrs, 1176 literals
c [elim-2] 39578 variables 48% will be scheduled this time
c [elim-2] scheduled 39578 variables 48%
c [elim-2] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-2] rescheduling of touched variables disabled
c [elim-2] incomplete 11002 not tried 13% in round 1
c [elim-2] transition to [ all 0 rem 1 ] state
c [elim-2] eliminated 105 = 0% variables out of 39578 scheduled
c [elim-2] considered successful since not run to completion yet
c [phase-count-2] 560741 negative 99.0% of 566647 except 5906 1.0%
c [phase-count-2] 446675 positive 78.8% of 566647 except 119972 21.2%
c [phase-count-2] less non-negative clauses 5906 than limit 56600 (10.0%)
c [phase-count-2] non-pos/non-neg = 119972/5906 = 20.31 >= 2.00 = 200/100
c [lucky-phase-2] forcing lucky phase -1
c [phase-2] phase bias: 0 positive 0%, 11190 negative 100%
c [sort-queue-2] sorted 73160 enqueued variables after 380 conflicts
c [score-dist-2] active 9582 (12%), one 0 (0%), zero 73160 (88%)
c [score-dist-2] max exp 601, different 100 (17%)
c [score-dist-2] median active exp 564, avg 557.5
c [simplification-2] removed 14586 variables 15.0% (82742 remain 39%)
c [simplification-2] removed 190622 irredundant clauses 25.2% (566647 remain 48%)
c [simplification-2] maximum reduction of 25% = max (15%, 25%)
c [simplification-2] forced so keeping old conflict interval 0
c [simplification-2] conflict limit remains at 1002 (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.4   82741   566647       386     277     34 17869    1    15   41   5%      0   15    6    0 11897%
c i    7.4   82660   566647       459     326     45 17881    1    17   41   5%      0   17    6    0 10571%
c i    7.4   82586   566647       460     326     45 17881    1    17   41   5%      0   17    6    0 10530%
c i    7.5   82578   566647       533     381     51 17891    1    19   41   5%      0   19    6    0 9496%
c i    7.5   82490   566647       536     382     51 17892    1    19   41   5%      0   19    6    0 9402%
c i    7.6   82482   566647       606     442     55 17897    1    19   41   5%      0   19    6    0 8657%
c i    7.6   82475   566647       704     525     64 17901    1    21   41   6%      0   21    7    0 8510%
c i    7.7   82463   566647       802     605     72 17908    1    23   41   6%      0   23    7    0 7864%
c i    7.7   82217   566647       852     642     79 17912    1    24   41   6%      0   24    7    0 7138%
c i    7.7   82208   566647       853     642     79 17912    1    24   41   6%      0   24    7    0 7110%
c 
c [simplification-3] limit 1026 conflicts (hard 11000) hit after 1026 conflicts
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 3558 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] 3558 out of 3558 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [decomp-6] removed 791 variables
c [unhide-3] limit 100000 with penalty 0 = 0 + 0
c [unhide-3-3] 12 units, 663 failed, 15153 tauts, 0 hbrs, 784 literals
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 81088 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 15308 not tried 19% in round 1
c [elim-3] transition to [ all 1 rem 1 ] state
c [elim-3] eliminated 1452 = 2% variables out of 81088 scheduled
c [elim-3] considered successful since not run to completion yet
c [phase-count-3] 531218 negative 98.9% of 537012 except 5794 1.1%
c [phase-count-3] 422679 positive 78.7% of 537012 except 114333 21.3%
c [phase-count-3] less non-negative clauses 5794 than limit 53700 (10.0%)
c [phase-count-3] non-pos/non-neg = 114333/5794 = 19.73 >= 2.00 = 200/100
c [lucky-phase-3] forcing lucky phase -1
c [phase-3] phase bias: 0 positive 0%, 7559 negative 100%
c [sort-queue-3] sorted 65393 enqueued variables after 1026 conflicts
c [score-dist-3] active 14243 (18%), one 0 (0%), zero 65393 (82%)
c [score-dist-3] max exp 770, different 246 (32%)
c [score-dist-3] median active exp 671, avg 653.2
c [simplification-3] removed 2569 variables 3.1% (79636 remain 37%)
c [simplification-3] removed 29635 irredundant clauses 5.2% (537012 remain 46%)
c [simplification-3] maximum reduction of 5% = max (3%, 5%)
c [simplification-3] large reduction 5% >= 5% limit
c [simplification-3] next conflict interval 2000 = 2000/1
c [simplification-3] penalized conflict interval 2000 = 1 * 2000
c [simplification-3] hard conflict limit 13026 (soft 3026 + delta 10000)
c [simplification-3] new conflict limit 3026 (hard 13026)
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    9.7   79635   537012      1070     756     78 16032    2    29   40   7%      1   28   11    0 7768%
c i    9.7   79619   537012      1098     780     78 16034    2    29   40   8%      1   29   12    0 7898%
c i    9.7   79615   537012      1123     800     80 16035    2    29   40   8%      1   29   12    0 7661%
c i    9.7   79606   537012      1228     881     86 16050    2    31   40   8%      1   31   10    0 6070%
c i    9.9   79602   537012      1481    1091    102 16070    3    36   40   9%      1   35   14    0 5985%
c i   10.0   79596   537012      1625    1205    113 16084    4    39   40  10%      1   38   16    0 5727%
c i   10.0   79588   537012      1680    1248    118 16087    4    41   40   9%      1   40   14    0 5121%
c i   10.0   79578   537012      1688    1254    118 16088    4    41   40   9%      1   41   14    0 5068%
c i   10.0   79571   537012      1689    1254    118 16088    4    41   40   9%      1   40   14    0 5049%
c i   10.1   79369   537012      1766    1317    125 16094    4    42   40   9%      1   41   12    0 4161%
c i   10.2   79361   537012      1905    1421    139 16112    4    43   40   9%      1   42   10    0 3281%
c i   10.2   79341   537012      2031    1532    144 16118    4    46   40   9%      1   45   12    0 3696%
c i   10.2   79188   537012      2032    1532    144 16118    4    46   40   9%      1   45   12    0 3682%
c i   10.3   79138   537012      2114    1606    148 16120    4    46   40  10%      1   45   12    0 3467%
c i   10.3   79129   537012      2115    1606    148 16120    4    46   40  10%      1   45   12    0 3454%
c i   10.4   79115   537012      2258    1726    155 16127    5    49   40  11%      1   48   20    0 4919%
c 
c [simplification-4] limit of 190 binary hit after 190 binaries
c [decomp-7] removed 551 variables
c [treelook-2] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-2] scheduled 50152 literals 32%
c [treelook-2] scheduling used 356922 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-2] used 243698 steps
c [treelook-2] 50130 literals remain 32%
c [treelook-2] 44957 variables remain to probed next time 57%
c [decomp-8] removed 1 variables
c [treelook-2] removed 9 variables, found 1937 hbrs
c [unhide-4] limit 108212 with penalty 0 = 0 + 0
c [unhide-4-4] 8 units, 866 failed, 2891 tauts, 0 hbrs, 3096 literals
c [elim-4] 10846 variables 14% will be scheduled this time
c [elim-4] scheduled 10846 variables 14%
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 22831267 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 10846 scheduled
c [phase-count-4] 515028 negative 98.9% of 520824 except 5796 1.1%
c [phase-count-4] 407730 positive 78.3% of 520824 except 113094 21.7%
c [phase-count-4] less non-negative clauses 5796 than limit 52000 (10.0%)
c [phase-count-4] non-pos/non-neg = 113094/5796 = 19.51 >= 2.00 = 200/100
c [lucky-phase-4] forcing lucky phase -1
c [phase-4] phase bias: 0 positive 0%, 6786 negative 100%
c [sort-queue-4] sorted 61279 enqueued variables after 2345 conflicts
c [score-dist-4] active 16624 (21%), one 30 (0%), zero 61249 (79%)
c [score-dist-4] max exp 615, different 403 (65%)
c [score-dist-4] median active exp 527, avg 423.9
c [simplification-4] removed 1204 variables 1.5% (77903 remain 37%)
c [simplification-4] removed 16188 irredundant clauses 3.0% (520824 remain 44%)
c [simplification-4] maximum reduction of 3% = max (2%, 3%)
c [simplification-4] forced so keeping old conflict interval 0
c [simplification-4] conflict limit remains at 3057 (hard 13026)
c [simplification-4] new binary 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   12.1   77902   520824      2477    1870    165 13722    6    54   39  10%      1   53   15    0 3391%
c i   12.1   77897   520824      2478    1870    165 13722    6    54   39  10%      1   53   15    0 3378%
c i   12.1   77883   520824      2510    1900    165 13722    6    54   39  10%      1   53   16    0 3470%
c i   12.2   77875   520824      2721    2047    190 13751    6    58   39  10%      1   57   13    0 2728%
c i   12.3   77870   520824      2819    2132    194 13757    6    59   39  10%      1   58   13    0 2566%
c i   12.3   77856   520824      2841    2150    195 13759    6    59   39  10%      1   58   12    1 2441%
c i   12.3   77699   520824      2846    2153    195 13760    6    59   39  10%      1   58   12    1 2408%
c i   12.4   77606   520824      2852    2156    196 13761    6    60   39  10%      1   58   12    1 2374%
c i   12.4   77596   520824      2853    2156    196 13761    6    60   39  10%      1   58   12    1 2365%
c i   12.4   77591   520824      2879    2173    200 13765    6    60   39  10%      1   58   11    1 2208%
c i   12.4   77586   520824      2970    2245    205 13777    6    61   39  10%      1   60   12    1 2349%
c i   12.4   77578   520824      2995    2266    208 13777    6    62   39  10%      1   60   12    1 2295%
c i   12.4   77572   520824      2998    2267    208 13777    6    62   39  10%      1   60   12    1 2281%
c i   12.5   77562   520824      3038    2299    211 13780    6    62   39  10%      1   61   12    1 2317%
c 
c [simplification-5] limit 3083 conflicts (hard 13026) hit after 3083 conflicts
c [quatres-1] found 33811 quaternary clauses 40% in total
c [quatres-1-2] added 1 single-self-subsuming ternary resolvents
c [quatres-1-2] added 3 quaternary resolvents
c [ternres-1] boosting ternary resolution limit by 5
c [ternres-1] limit 20000000 with penalty 0 = 0 + 0
c [ternres-1] all 77557 free variables schedulable
c [ternres-1] 46 ternary resolvents (0 bin, 46 trn)
c [ternres-1] fully completed ternary resolution
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 43 xors of average arity 2.8
c [gauss-1] connected 119 occurrences of 108 variables (average 1.1)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] fully completed
c [decomp-9] removed 12 variables
c [gauss-1] exported 1 unary, 0 binary and 0 ternary equations
c [basicprobe-2] limit 4150032 based on 518754 irredundant clauses
c [basicprobe-2-0] 28438 probes remain 38% after last round
c [basicprobe-2-0] 39 units = 39 failed (100%) + 0 lifted (0%)
c [basicprobe-2-0] removed 2473 variables, found 9424 hbrs
c [bate-1] eliminated 7 asymmetric tautologies during probing
c [unhide-5] limit 139807 with penalty 0 = 0 + 0
c [unhide-5-5] 4 units, 303 failed, 13314 tauts, 0 hbrs, 2728 literals
c [transred-1] limit 699036 with penalty 0 = 0 + 0
c [transred-1] removed 133 transitive binary clauses
c [transred-1] found 5 units
c [block-1] scheduling all variables this time
c [block-1] scheduled 74605 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 7601 blocked clauses
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 3 clauses out of 158 (2%) of length 10
c [cce-1-1] eliminated 35 clauses out of 743 (5%) of length 9
c [cce-1-1] eliminated 37 clauses out of 636 (6%) of length 8
c [cce-1-1] eliminated 73 clauses out of 841 (9%) of length 7
c [cce-1-1] eliminated 3288 clauses out of 4599 (71%) of length 6
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 3436 large clauses in 30000005 steps
c [cce-1-1] allowing another 15000002 steps for small clauses
c [cce-1-1] scheduling 378700 clauses = 239226 binary + 139474 ternary
c [cce-1-1] tried to eliminate 407 small clauses 0%
c [cce-1-1] eliminated 92 binary clauses 0%
c [cce-1-1] eliminated 41 ternary clauses 0%
c [cce-1-1] eliminated 133 small clauses 0%
c [cce-1-1] eliminated 133 small clauses in 30000016 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 3569 covered clauses in round 1
c [cce-1] eliminated 3569 covered clauses in TOTAL during 1 rounds
c [cce-1] 3569 < 1/100 * 477443 = 4774 considered unsuccessful
c [bca-1] limit of 10000000 steps and 948248 added (scaled 2)
c [bca-1] 139535 out of 149212 literals actually usable 94%
c [bca-1] added 193 blocked clauses in 445086 steps
c [sweep-1] limit 1000000 penalty 0 = 0 + 0
c [sweep-1-1] 3945 pos 5.3% + 70660 neg 94.7% = 74605 sched 100.0% ret 0
c [sweep-1-1] 1250357 steps 15 queries 21457.27 avg class size
c [sweep-1-1] 115 decisions 12 SAT calls 42.42 avg env size
c [sweep-1-1] 74580 variables remain 100% (25 retained 0%)
c [decomp-11] removed 75 variables
c [sweep-1-1] removed 75 vars (0 failed, 2 eqs, 8 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 75 vars in TOTAL (1 rounds, 14 queries)
c [phase-count-5] 471086 negative 99.4% of 473727 except 2641 0.6%
c [phase-count-5] 376052 positive 79.4% of 473727 except 97675 20.6%
c [phase-count-5] less non-negative clauses 2641 than limit 47300 (10.0%)
c [phase-count-5] non-pos/non-neg = 97675/2641 = 36.98 >= 2.00 = 200/100
c [lucky-phase-5] forcing lucky phase -1
c [phase-5] phase bias: 0 positive 0%, 6570 negative 100%
c [sort-queue-5] sorted 57182 enqueued variables after 3083 conflicts
c [score-dist-5] active 17348 (23%), one 26 (0%), zero 57156 (77%)
c [score-dist-5] max exp 809, different 460 (57%)
c [score-dist-5] median active exp 708, avg 588.2
c [simplification-5] removed 3027 variables 3.9% (74530 remain 35%)
c [simplification-5] removed 47097 irredundant clauses 9.0% (473727 remain 40%)
c [simplification-5] maximum reduction of 9% = max (4%, 9%)
c [simplification-5] large reduction 9% >= 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 15083 (soft 5083 + delta 10000)
c [simplification-5] new conflict limit 5083 (hard 15083)
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   15.8   74529   473727      3171    2386    347 29515    7    66   38  10%      1   64   14    1 2445%
c i   16.0   74518   473727      3487    2638    379 29540    7    71   38  10%      1   69   13    1 2110%
c i   16.0   74508   473727      3518    2661    380 29546    7    72   38  10%      1   70   12    1 1943%
c i   16.0   74498   473727      3588    2716    387 29552    7    74   38  10%      1   72   11    1 1793%
c i   16.1   74493   473727      3743    2833    407 29563    7    75   38   9%      1   72    9    1 1326%
c i   16.4   74442   473727      4298    3299    438 29596    8    80   38  10%      3   77   16    1 2042%
c i   16.4   74440   473727      4300    3298    439 29596    8    80   38  10%      3   77   16    1 2027%
c i   16.5   74437   473727      4410    3392    442 29604    8    81   38  10%      2   77   14    1 1758%
c i   16.6   74436   473727      4589    3547    452 29614    9    83   38  11%      2   80   17    1 2002%
c i   16.6   74427   473727      4606    3563    452 29614    9    83   38  11%      2   79   17    1 2023%
c i   16.6   74426   473727      4683    3630    457 29617    9    83   38  11%      2   79   16    1 1901%
c i   16.6   74425   473727      4694    3637    457 29618    9    83   38  11%      2   79   16    1 1883%
c i   16.8   74414   473727      5016    3911    472 29642   11    86   38  12%      2   83   31    1 3033%
c 
c [simplification-6] limit 5088 conflicts (hard 15083) hit after 5088 conflicts
c [quatres-2] found 36363 quaternary clauses 46% in total
c [quatres-2-1] removed 1 duplicate quaternary clauses
c [quatres-2-2] added 1 single-self-subsuming ternary resolvents
c [quatres-2-2] added 2 quaternary resolvents
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] all 74406 free variables schedulable
c [ternres-2] 3 ternary resolvents (0 bin, 3 trn)
c [ternres-2] 40878 variables remain 55% (33528 retained 45%)
c [card-3] limit 500000 penalty 2 = 2 + 0
c [card-3] found 2590 at-most-one constraints of average size 4.3
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 500000 for elimination
c [card-3] 2590 out of 2590 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [gauss-2] limit 2000000 penalty 0 = 0 + 0
c [gauss-2] extracted 209 xors of average arity 2.3
c [gauss-2] connected 473 occurrences of 310 variables (average 1.5)
c [gauss-2] limit 2000000 penalty 0 = 0 + 0
c [gauss-2] fully completed
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-12] removed 104 variables
c [unhide-6] limit 208288 with penalty 0 = 0 + 0
c [unhide-6-6] 10 units, 804 failed, 3622 tauts, 0 hbrs, 4871 literals
c [transred-2] limit 1041441 with penalty 0 = 0 + 0
c [transred-2] removed 180 transitive binary clauses
c [transred-2] found 4 units
c [block-2] scheduling all variables this time
c [block-2] scheduled 73073 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 1291 blocked clauses
c [block-2] 1291 < 1/100 * 472062 = 4720 considered unsuccessful
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 73066 variables 100%
c [elim-5] limit of 10414414 steps penalty 1 = 1 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5] incomplete 22366 not tried 31% in round 1
c [elim-5] transition to [ all 1 rem 1 ] state
c [elim-5] eliminated 1112 = 2% variables out of 73066 scheduled
c [bca-2] limit of 10000000 steps and 914292 added (scaled 2)
c [bca-2] 133906 out of 143910 literals actually usable 93%
c [bca-2] added 141 blocked clauses in 432148 steps
c [sweep-2] limit 1000000 penalty 0 = 0 + 0
c [sweep-2-1] 3715 pos 5.2% + 68218 neg 94.8% = 71933 sched 100.0% ret 21
c [sweep-2-1] 1022732 steps 20 queries 19281.40 avg class size
c [sweep-2-1] 106 decisions 14 SAT calls 57.14 avg env size
c [sweep-2-1] 71706 variables remain 100% (90 retained 0%)
c [decomp-13] removed 169 variables
c [sweep-2-1] removed 169 vars (0 failed, 5 eqs, 12 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 169 vars in TOTAL (1 rounds, 19 queries)
c [phase-count-6] 453495 negative 99.4% of 456041 except 2546 0.6%
c [phase-count-6] 360049 positive 79.0% of 456041 except 95992 21.0%
c [phase-count-6] less non-negative clauses 2546 than limit 45600 (10.0%)
c [phase-count-6] non-pos/non-neg = 95992/2546 = 37.70 >= 2.00 = 200/100
c [lucky-phase-6] forcing lucky phase -1
c [phase-6] phase bias: 0 positive 0%, 6477 negative 100%
c [sort-queue-6] sorted 55529 enqueued variables after 5088 conflicts
c [score-dist-6] active 16256 (23%), one 2611 (4%), zero 52918 (74%)
c [score-dist-6] max exp 832, different 493 (59%)
c [score-dist-6] median active exp 734, avg 625.3
c [simplification-6] removed 2621 variables 3.5% (71785 remain 34%)
c [simplification-6] removed 17686 irredundant clauses 3.7% (456041 remain 39%)
c [simplification-6] maximum reduction of 4% = max (4%, 4%)
c [simplification-6] geometric conflict interval increment 4000 = 20000 / 5
c [simplification-6] new conflict interval 4000
c [simplification-6] penalized conflict interval 4000 = 1 * 4000
c [simplification-6] hard conflict limit 19088 (soft 9088 + delta 10000)
c [simplification-6] new conflict limit 9088 (hard 19088)
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.6   71784   456041      5226    3120    436 27321   11    90   37  12%      2   85   19    1 1794%
c i   19.6   71783   456041      5249    3141    437 27321   11    89   37  12%      2   85   18    1 1740%
c i   19.6   71777   456041      5270    3159    439 27321   11    91   37  12%      2   86   17    1 1635%
c i   19.7   71773   456041      5490    3341    454 27339   10    90   37  12%      2   86   11    1 1056%
c i   19.8   71765   456041      5695    3503    481 27348   10    91   37  11%      2   86   10    1  909%
c i   19.8   71760   456041      5711    3513    483 27350   10    91   37  11%      2   86   10    1  870%
c i   19.8   71757   456041      5729    3524    487 27351   10    91   37  11%      2   86    9    1  838%
c i   19.8   71746   456041      5731    3524    487 27352   10    91   37  11%      2   86    9    1  832%
c i   19.9   71741   456041      5766    3555    490 27352   10    91   37  11%      2   86    9    1  837%
c i   19.9   71738   456041      5769    3556    491 27352   10    91   37  11%      2   86    9    1  829%
c i   19.9   71736   456041      5786    3571    492 27352   10    91   37  11%      2   86    9    1  849%
c i   19.9   71735   456041      5812    3590    494 27356   10    91   37  11%      2   86   10    1  870%
c i   20.1   71728   456041      6157    3897    503 27375   11    95   37  12%      2   90   17    1 1445%
c i   20.1   71727   456041      6214    3944    507 27380   11    95   37  12%      2   90   16    1 1287%
c i   20.1   71726   456041      6215    3944    507 27380   11    95   37  12%      2   90   16    1 1282%
c i   20.2   71724   456041      6425    4129    520 27386   11    99   37  11%      2   93   16    1 1242%
c i   20.3   71721   456041      6556    4241    525 27394   11    98   37  11%      2   92   13    1 1016%
c i   20.3   71720   456041      6616    4296    525 27396   12    98   37  12%      2   93   17    1 1281%
c i   20.4   71717   456041      6790    4448    531 27401   12    97   37  12%      2   91   19    1 1387%
c i   20.4   71703   456041      6858    4501    532 27409   12    98   37  12%      1   91   19    1 1371%
c i   20.5   71696   456041      7080    4684    550 27426   12   100   37  12%      2   93   16    1 1103%
c i   20.7   71689   456041      7271    4834    567 27444   12   103   37  12%      1   97   13    1  927%
c i   20.7   71640   456041      7353    4895    572 27456   12   104   37  12%      1   97   14    1  926%
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.7   71639   456041      7354    4895    572 27456   12   104   37  12%      1   97   13    1  922%
c i   20.8   71636   456041      7506    5005    589 27474   12   104   37  12%      1   97   13    1  880%
c i   20.8   71628   456041      7541    5036    590 27475   12   104   37  12%      1   97   13    1  851%
c i   20.9   71627   456041      7619    5102    595 27481   12   104   37  12%      1   97   12    2  788%
c i   21.0   71609   456041      7720    5174    605 27498   12   109   37  11%      1  102   10    2  666%
c i   21.0   71601   456041      7745    5193    606 27502   12   109   37  11%      1  102   10    2  629%
c i   21.1   71410   456041      7876    5290    625 27512   12   112   38  11%      1  104   10    2  660%
c i   21.2   71401   456041      7942    5349    627 27516   12   114   38  10%      1  106   11    2  740%
c i   21.3   71039   456041      8016    5411    631 27522   12   116   38  10%      1  108   15    2  931%
c i   21.4   71015   456041      8095    5472    640 27529   12   116   38  10%      1  108   12    2  752%
c i   21.4   71006   456041      8096    5472    640 27529   12   116   38  10%      1  108   12    2  749%
c i   21.4   71001   456041      8161    5520    646 27539   12   117   38  10%      1  108   11    2  683%
c i   21.4   70995   456041      8163    5521    646 27539   12   116   38  10%      1  108   11    2  680%
c i   21.4   70982   456041      8172    5526    646 27542   12   116   38  10%      1  108   11    2  668%
c i   21.4   70976   456041      8181    5530    648 27544   12   116   38  10%      1  108   11    2  677%
c i   21.4   70900   456041      8203    5545    649 27545   12   116   38  10%      1  108   11    2  720%
c i   21.5   70891   456041      8231    5568    650 27548   12   116   38  10%      1  107   11    2  700%
c i   21.5   70882   456041      8238    5573    651 27548   12   116   38  10%      1  107   11    2  685%
c i   21.5   70799   456041      8283    5607    655 27554   12   115   38  10%      1  107   11    2  669%
c i   21.5   70792   456041      8286    5607    657 27554   12   115   38  10%      1  107   11    2  662%
c i   21.8   70746   456041      8521    5806    672 27569   12   123   38  10%      1  115   15    2  912%
c i   21.9   70739   456041      8631    5900    680 27576   12   124   38  10%      1  115   16    2  971%
c i   21.9   70736   456041      8663    5931    680 27576   12   124   38  10%      1  114   18    2 1087%
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   22.0   70732   456041      8810    6048    686 27588   13   125   38  10%      1  116   17    2  970%
c i   22.0   70348   456041      8831    6064    687 27590   12   125   38  10%      1  116   16    2  909%
c i   22.1   70338   456041      8841    6072    687 27591   12   125   38  10%      1  116   15    2  889%
c i   22.1   70337   456041      8850    6077    689 27592   12   125   38  10%      1  116   15    2  861%
c i   22.3   70314   456041      9049    6245    697 27610   13   126   38  10%      1  117   14    2  825%
c i   22.3   70307   456041      9077    6266    697 27615   12   127   38  10%      1  117   14    2  778%
c 
c [simplification-7] limit 9139 conflicts (hard 19088) hit after 9139 conflicts
c [quatres-3] found 34477 quaternary clauses 47% in total
c [quatres-3-2] added 3 single-self-subsuming ternary resolvents
c [quatres-3-2] added 12 quaternary resolvents
c [ternres-3] limit 4000000 with penalty 0 = 0 + 0
c [ternres-3] 38657 schedulable variables 54%
c [ternres-3] 81 ternary resolvents (1 bin, 80 trn)
c [ternres-3] 4489 variables remain 6% (65814 retained 94%)
c [decomp-14] removed 1576 variables
c [simpleprobe-3] 5965 schedulable variables 8%
c [simpleprobe-3] limit 3773197 penalty 1 = 1 + 0
c [decomp-15] removed 9 variables
c [simpleprobe-3] 5454 variables remain 8% (64746 retained 92%)
c [simpleprobe-3] removed 9 variables, found 5882 hbrs, 4 units
c [unhide-7] limit 377319 with penalty 0 = 0 + 0
c [unhide-7-7] 4 units, 155 failed, 8271 tauts, 0 hbrs, 5342 literals
c [transred-3] limit 1886598 with penalty 0 = 0 + 0
c [transred-3] removed 416 transitive binary clauses
c [transred-3] found 16 units
c [cce-2] limit of 15000000 steps penalty 1 = 1 + 0
c [cce-2-1] eliminated 1 clauses out of 676 (0%) of length 7
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] eliminated 1 large clauses in 15000000 steps
c [cce-2-1] allowing another 7500000 steps for small clauses
c [cce-2-1] scheduling 237256 clauses = 219706 binary + 17550 ternary
c [cce-2-1] tried to eliminate 456 small clauses 0%
c [cce-2-1] eliminated 145 binary clauses 0%
c [cce-2-1] eliminated 18 ternary clauses 0%
c [cce-2-1] eliminated 163 small clauses 0%
c [cce-2-1] eliminated 3523 small clauses in 15000005 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 3524 covered clauses in round 1
c [cce-2] eliminated 3524 covered clauses in TOTAL during 1 rounds
c [cce-2] 3524 < 1/100 * 439037 = 4390 considered unsuccessful
c [elim-6] 21923 variables 31% will be scheduled this time
c [elim-6] scheduled 21923 variables 31%
c [elim-6] limit of 37731973 steps penalty 0 = 0 + 0
c [elim-6] rescheduling of touched variables disabled
c [elim-6-1] eliminated 11 variables 0% in round 1 in 28116932 steps
c [elim-6-1] backward subsumption/strengthening limit 9615041
c [elim-6-1-1] backward checking 157 touched variables 0%
c [elim-6-1-1] fully completed backward checking in 1 rounds
c [elim-6-1] subsumed 2 and strengthened 11 clauses in 128133 steps
c [elim-6-1] rescheduled 30 variables 0% by backward subsumption
c [elim-6-2] no variable eliminated in round 2 in 20053 steps
c [elim-6] fully completed in 2 rounds
c [elim-6] transition to [ all 0 rem 0 ] state
c [elim-6] eliminated 15 = 0% variables out of 21923 scheduled
c [elim-6] 15 < 1/100 * 21923 = 219 considered unsuccessful
c [bca-3] limit of 10000000 steps and 869495 added (scaled 2)
c [bca-3] 123161 out of 139606 literals actually usable 88%
c [bca-3] added 117 blocked clauses in 378414 steps
c [sweep-3] limit 1000000 penalty 0 = 0 + 0
c [sweep-3-1] 4251 pos 6.1% + 65472 neg 93.9% = 69723 sched 99.9% ret 79
c [sweep-3-1] 1050022 steps 14 queries 16014.14 avg class size
c [sweep-3-1] 240 decisions 10 SAT calls 226.00 avg env size
c [sweep-3-1] 69688 variables remain 100% (107 retained 0%)
c [decomp-16] removed 11 variables
c [sweep-3-1] removed 11 vars (0 failed, 3 eqs, 9 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 11 vars in TOTAL (1 rounds, 13 queries)
c [phase-count-7] 431780 negative 99.4% of 434327 except 2547 0.6%
c [phase-count-7] 342791 positive 78.9% of 434327 except 91536 21.1%
c [phase-count-7] less non-negative clauses 2547 than limit 43400 (10.0%)
c [phase-count-7] non-pos/non-neg = 91536/2547 = 35.94 >= 2.00 = 200/100
c [lucky-phase-7] forcing lucky phase -1
c [phase-7] phase bias: 0 positive 0%, 1958 negative 100%
c [sort-queue-7] sorted 44889 enqueued variables after 9139 conflicts
c [score-dist-7] active 24902 (36%), one 3628 (5%), zero 41261 (59%)
c [score-dist-7] max exp 894, different 608 (68%)
c [score-dist-7] median active exp 744, avg 727.7
c [simplification-7] removed 512 variables 0.7% (69791 remain 33%)
c [simplification-7] removed 21714 irredundant clauses 4.8% (434327 remain 37%)
c [simplification-7] maximum reduction of 5% = max (1%, 5%)
c [simplification-7] large reduction 5% >= 5% limit
c [simplification-7] next conflict interval 2000 = 2000/1
c [simplification-7] penalized conflict interval 2000 = 1 * 2000
c [simplification-7] hard conflict limit 21139 (soft 11139 + delta 10000)
c [simplification-7] new conflict limit 11139 (hard 21139)
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.2   69790   434327      9144    6241    752 32432   12   127   37  10%      1  117   13    2  761%
c i   25.5   69779   434327      9562    6572    790 32472   12   130   38  10%      2  119   11    2  586%
c i   25.6   69770   434327      9661    6661    793 32478   13   130   38  10%      2  119   13    2  701%
c i   25.7   69762   434327      9846    6832    797 32481   13   131   38  10%      2  120   23    2 1186%
c i   25.7   69761   434327      9900    6880    799 32483   14   132   38  10%      1  120   26    2 1320%
c i   25.8   69733   434327     10078    7022    814 32499   14   132   38  10%      1  121   20    2 1000%
c i   25.9   69725   434327     10234    7154    826 32509   14   135   38  10%      1  123   16    2  795%
c i   26.0   69643   434327     10267    7179    831 32511   14   136   38  10%      1  124   15    2  750%
c i   26.0   69553   434327     10285    7189    834 32514   13   135   38  10%      1  123   14    2  711%
c i   26.0   69552   434327     10310    7203    841 32517   13   135   38  10%      1  123   13    2  656%
c i   26.0   69544   434327     10313    7203    841 32519   13   135   38  10%      1  123   13    2  649%
c i   26.0   69273   434327     10331    7210    845 32525   13   134   38  10%      1  122   12    2  612%
c i   26.0   69229   434327     10341    7212    847 32530   13   134   38  10%      1  122   12    2  591%
c i   26.0   69224   434327     10342    7212    847 32530   13   134   38  10%      1  122   12    2  588%
c i   26.0   68876   434327     10352    7216    850 32532   13   134   38  10%      1  122   12    2  570%
c i   26.1   68670   434327     10370    7227    852 32536   13   133   38  10%      1  121   11    2  548%
c i   26.1   68662   434327     10404    7251    853 32543   13   134   38  10%      1  121   10    2  510%
c i   26.1   68652   434327     10413    7257    855 32543   13   133   38  10%      1  121   10    2  502%
c i   26.1   68564   434327     10422    7265    855 32543   13   133   38  10%      1  121   10    2  510%
c i   26.2   68552   434327     10497    7313    865 32558   13   134   38  10%      1  121    9    2  424%
c i   26.2   68448   434327     10522    7334    867 32559   13   134   38  10%      1  121    9    2  448%
c i   26.3   68440   434327     10587    7382    871 32571   13   135   38  10%      1  122   10    2  485%
c i   26.3   68432   434327     10629    7416    876 32572   13   135   38  10%      1  122    9    2  457%
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   26.4   68341   434327     10653    7433    880 32574   13   134   38  10%      1  122    9    2  427%
c i   26.5   68314   434327     10698    7449    892 32590   13   134   38   9%      1  122    8    2  376%
c i   26.5   68030   434327     10720    7461    895 32595   13   134   38   9%      1  121    7    2  355%
c i   26.7   68020   434327     10858    7556    908 32623   13   134   38   9%      1  121    7    2  359%
c i   26.8   68012   434327     11114    7773    916 32647   13   133   38  10%      1  119   13    2  630%
c 
c [simplification-8] limit 11156 conflicts (hard 21139) hit after 11156 conflicts
c [quatres-4] found 32825 quaternary clauses 48% in total
c [quatres-4-2] added 1 single-self-subsuming ternary resolvents
c [quatres-4-2] added 4 quaternary resolvents
c [ternres-4] limit 4000000 with penalty 0 = 0 + 0
c [ternres-4] 4357 schedulable variables 6%
c [ternres-4] 74 ternary resolvents (0 bin, 74 trn)
c [ternres-4] fully completed ternary resolution
c [gauss-3] limit 1000000 penalty 1 = 1 + 0
c [gauss-3] extracted 113 xors of average arity 2.5
c [gauss-3] connected 283 occurrences of 244 variables (average 1.2)
c [gauss-3] limit 1000000 penalty 1 = 1 + 0
c [gauss-3] fully completed
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-17] removed 130 variables
c [treelook-3] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-3] scheduled 59511 literals 44%
c [treelook-3] scheduling used 386598 steps
c [treelook-3] not fully scheduled
c [treelook-3] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-3] used 398631 steps
c [treelook-3] 59502 literals remain 44%
c [treelook-3] 36218 variables remain to probed next time 53%
c [treelook-3] removed 1 variables, found 3333 hbrs
c [unhide-8] limit 473628 with penalty 0 = 0 + 0
c [unhide-8-8] 4 units, 578 failed, 4993 tauts, 0 hbrs, 8167 literals
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 371 transitive binary clauses
c [transred-4] found 8 units
c [block-3] scheduling all variables this time
c [block-3] scheduled 67282 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 141 blocked clauses
c [block-3] 141 < 1/100 * 423481 = 4234 considered unsuccessful
c [bca-4] limit of 10000000 steps and 835623 added (scaled 2)
c [bca-4] 115069 out of 134536 literals actually usable 86%
c [bca-4] added 130 blocked clauses in 341639 steps
c [sweep-4] limit 1000000 penalty 0 = 0 + 0
c [sweep-4-1] 5384 pos 8.0% + 61780 neg 92.0% = 67164 sched 99.8% ret 103
c [sweep-4-1] 1346589 steps 12 queries 19825.25 avg class size
c [sweep-4-1] 87 decisions 9 SAT calls 65.00 avg env size
c [sweep-4-1] 67129 variables remain 100% (124 retained 0%)
c [decomp-19] removed 23 variables
c [sweep-4-1] removed 23 vars (0 failed, 3 eqs, 3 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 23 vars in TOTAL (1 rounds, 11 queries)
c [phase-count-8] 414685 negative 99.4% of 417234 except 2549 0.6%
c [phase-count-8] 329158 positive 78.9% of 417234 except 88076 21.1%
c [phase-count-8] less non-negative clauses 2549 than limit 41700 (10.0%)
c [phase-count-8] non-pos/non-neg = 88076/2549 = 34.55 >= 2.00 = 200/100
c [lucky-phase-8] forcing lucky phase -1
c [phase-8] phase bias: 0 positive 0%, 978 negative 100%
c [sort-queue-8] sorted 36444 enqueued variables after 11156 conflicts
c [score-dist-8] active 30800 (46%), one 3468 (5%), zero 32976 (49%)
c [score-dist-8] max exp 925, different 736 (79%)
c [score-dist-8] median active exp 757, avg 647.5
c [simplification-8] removed 752 variables 1.1% (67244 remain 32%)
c [simplification-8] removed 17093 irredundant clauses 3.9% (417234 remain 35%)
c [simplification-8] maximum reduction of 4% = max (1%, 4%)
c [simplification-8] geometric conflict interval increment 4000 = 20000 / 5
c [simplification-8] new conflict interval 8000
c [simplification-8] penalized conflict interval 8000 = 1 * 8000
c [simplification-8] hard conflict limit 29156 (soft 19156 + delta 10000)
c [simplification-8] new conflict limit 19156 (hard 29156)
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.4   67243   417234     11773    8262    994 30702   13   140   37  10%      3  125   15    2  666%
c i   29.4   67234   417234     11784    8269    996 30703   13   140   37  10%      3  125   15    2  649%
c i   29.5   67117   417234     11866    8340    999 30705   14   139   37  10%      3  125   17    2  755%
c i   29.5   67041   417234     11878    8350    999 30706   14   140   37  10%      3  125   17    2  744%
c i   29.5   67031   417234     11903    8374    999 30706   14   140   37  10%      3  125   17    2  732%
c i   29.6   67025   417234     11979    8438   1002 30710   14   140   37  10%      3  125   21    2  914%
c i   29.7   67023   417234     12083    8525   1006 30721   14   141   37  10%      2  126   16    2  699%
c i   29.7   67012   417234     12096    8530   1009 30725   14   141   37  10%      2  126   16    2  674%
c i   29.8   67003   417234     12182    8603   1012 30734   14   143   37  10%      2  127   15    2  617%
c i   29.9   66880   417234     12287    8687   1021 30742   14   145   37   9%      2  130   15    2  632%
c i   29.9   66653   417234     12290    8689   1021 30742   14   145   37   9%      2  130   15    2  629%
c i   29.9   66502   417234     12294    8688   1022 30742   14   145   37   9%      2  130   15    2  623%
c i   29.9   66492   417234     12366    8745   1028 30747   14   146   37  10%      2  130   16    2  686%
c i   30.0   66484   417234     12388    8760   1030 30751   14   146   37   9%      2  130   15    2  645%
c i   30.1   66345   417234     12536    8877   1040 30759   15   146   37  10%      2  129   28    2 1103%
c i   30.1   66292   417234     12554    8893   1040 30759   15   146   37  10%      2  129   27    3 1080%
c i   30.1   66291   417234     12584    8917   1044 30760   15   146   37  10%      2  130   25    3  984%
c i   30.2   66279   417234     12596    8928   1044 30760   15   147   37  10%      2  131   24    3  957%
c i   30.2   66007   417234     12678    8991   1048 30766   15   151   37  10%      2  134   29    3 1116%
c i   30.2   66002   417234     12681    8992   1048 30767   15   151   37  10%      2  134   28    3 1103%
c i   30.2   65993   417234     12682    8992   1048 30767   15   151   37  10%      2  134   28    3 1099%
c i   30.3   65985   417234     12709    9013   1051 30769   15   151   37  10%      2  135   26    3 1013%
c i   30.3   65866   417234     12739    9032   1056 30774   15   151   37  10%      1  134   24    3  926%
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   30.3   65865   417234     12773    9061   1057 30777   15   150   37  10%      1  133   22    3  842%
c i   30.3   65848   417234     12774    9061   1057 30777   15   150   37  10%      1  133   21    3  838%
c i   30.4   65793   417234     12843    9110   1067 30786   15   149   37  10%      1  133   18    3  694%
c i   30.4   65786   417234     12867    9131   1069 30786   15   149   37  10%      1  132   17    3  646%
c i   30.4   65780   417234     12907    9161   1074 30790   15   148   37  10%      1  131   15    3  593%
c i   30.4   65775   417234     12909    9162   1074 30790   15   148   37  10%      1  131   15    3  589%
c i   30.5   65767   417234     12988    9227   1079 30796   15   148   37  10%      1  131   13    3  519%
c i   30.5   65748   417234     13065    9271   1085 30808   15   146   37  10%      1  129   13    3  509%
c i   30.5   65741   417234     13099    9290   1090 30817   15   145   37  10%      1  128   12    3  463%
c i   30.5   65724   417234     13112    9299   1091 30818   15   145   37  10%      1  128   12    3  458%
c i   30.5   65717   417234     13113    9299   1091 30818   15   145   37  10%      1  128   12    3  457%
c i   30.5   65704   417234     13122    9306   1092 30818   15   145   37  10%      1  128   12    3  468%
c i   30.6   65700   417234     13173    9343   1095 30826   15   145   37  10%      1  127   12    3  471%
c i   30.6   65680   417234     13203    9366   1095 30831   15   144   37  10%      1  127   12    3  454%
c i   30.6   65669   417234     13223    9379   1097 30832   15   144   37  10%      1  126   12    3  453%
c i   30.6   65661   417234     13226    9380   1098 30832   15   144   37  10%      1  126   12    3  449%
c i   30.6   65651   417234     13227    9380   1098 30832   15   144   37  10%      1  126   12    3  447%
c i   30.7   65646   417234     13315    9441   1110 30846   14   144   37  10%      1  126   10    3  370%
c i   30.7   65556   417234     13331    9455   1110 30847   14   143   37  10%      1  126    9    3  358%
c i   30.7   65555   417234     13332    9455   1110 30847   14   143   37  10%      1  125    9    3  357%
c i   30.8   65546   417234     13380    9494   1116 30849   14   144   37  10%      1  126   10    3  369%
c i   30.8   65541   417234     13422    9524   1118 30857   14   144   37  10%      1  126   10    3  391%
c i   31.1   64982   417234     13810    9869   1132 30876   15   147   37  10%      1  128   16    3  580%
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.6   64980   417234     14745   10700   1163 30903   16   144   38  11%      5  124   21    3  694%
c i   31.6   64975   417234     14778   10727   1164 30907   16   144   38  11%      5  123   19    3  631%
c i   31.7   64969   417234     14857   10778   1177 30921   16   143   38  11%      5  122   16    3  523%
c i   31.8   64966   417234     14899   10814   1178 30925   16   143   38  11%      5  122   14    3  476%
c i   31.8   64956   417234     14942   10850   1179 30930   16   143   38  11%      4  122   13    3  431%
c i   31.8   64945   417234     14943   10850   1179 30930   16   143   38  11%      4  122   13    3  430%
c i   31.8   64897   417234     14966   10869   1179 30933   16   143   38  11%      4  122   13    3  429%
c i   31.9   64882   417234     15019   10913   1180 30939   16   142   38  11%      4  121   13    3  440%
c i   31.9   64876   417234     15053   10939   1181 30942   16   142   38  11%      4  121   13    3  422%
c i   32.1   64873   417234     15262   11117   1189 30959   16   144   38  11%      4  123   19    3  610%
c i   32.3   64872   417234     15550   11375   1195 30972   16   145   38  11%      3  123   17    3  537%
c i   32.3   64867   417234     15560   11379   1196 30976   16   145   38  11%      3  123   16    3  520%
c i   32.3   64853   417234     15577   11392   1197 30978   16   145   38  11%      3  123   16    3  499%
c i   32.3   64761   417234     15604   11410   1203 30979   16   146   38  11%      3  124   15    3  480%
c i   32.4   64734   417234     15612   11415   1204 30980   16   146   38  11%      3  123   15    3  468%
c i   32.4   64730   417234     15624   11421   1206 30983   16   145   38  11%      3  123   14    3  451%
c i   32.5   64705   417234     15819   11586   1213 30993   17   147   38  11%      3  124   21    3  648%
c i   32.5   64654   417234     15830   11596   1213 30993   17   147   38  11%      3  124   21    3  640%
c i   32.6   64648   417234     15909   11654   1223 30999   16   147   38  11%      2  124   17    3  535%
c i   32.6   64594   417234     15910   11654   1223 30999   16   147   38  11%      2  124   17    3  533%
c i   32.6   64560   417234     15953   11682   1228 31008   16   146   38  11%      2  123   15    3  474%
c i   32.6   64548   417234     15954   11682   1228 31008   16   146   38  11%      2  123   15    3  472%
c i   32.6   64544   417234     15961   11684   1230 31010   16   146   38  11%      2  123   15    3  461%
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   32.7   64515   417234     16035   11734   1240 31021   16   145   38  11%      2  122   13    3  393%
c i   32.7   64508   417234     16072   11765   1242 31024   16   145   38  11%      2  122   12    3  370%
c i   32.7   64501   417234     16079   11771   1242 31024   16   146   38  11%      2  123   13    3  415%
c i   32.8   64500   417234     16107   11796   1243 31024   16   146   38  11%      2  123   14    3  431%
c i   32.8   64479   417234     16193   11876   1244 31027   16   145   38  11%      2  122   17    3  510%
c i   32.8   64478   417234     16194   11876   1244 31027   16   145   38  11%      2  122   17    3  508%
c i   32.8   64477   417234     16195   11876   1244 31027   16   145   38  11%      2  122   17    3  506%
c i   32.8   64476   417234     16196   11876   1244 31027   16   145   38  11%      2  122   17    3  504%
c i   32.8   64475   417234     16197   11876   1244 31027   16   145   38  11%      2  121   16    3  502%
c i   32.8   64474   417234     16198   11876   1244 31027   16   145   38  11%      2  121   16    3  500%
c i   33.2   64473   417234     16681   12295   1269 31051   16   152   38  11%      2  128   14    3  412%
c i   33.4   64470   417234     16973   12537   1284 31072   16   151   38  11%      2  126   18    3  519%
c i   33.5   64467   417234     17053   12612   1285 31075   17   150   38  11%      2  125   20    3  583%
c i   33.7   64463   417234     17345   12865   1291 31085   17   151   38  11%      2  126   26    4  732%
c i   33.7   64452   417234     17383   12902   1291 31085   17   151   39  12%      2  126   26    4  730%
c i   33.7   64443   417234     17465   12979   1292 31085   19   151   39  12%      2  126   45    4 1204%
c i   34.0   64436   417234     17771   13229   1314 31108   19   153   39  13%      2  127   29    4  773%
c i   34.0   64431   417234     17772   13229   1314 31108   19   153   39  13%      2  127   29    4  770%
c i   34.0   64426   417234     17773   13229   1314 31108   19   153   39  13%      2  127   29    4  767%
c i   34.0   64414   417234     17774   13229   1314 31108   19   153   39  13%      2  127   29    4  764%
c i   34.0   64406   417234     17783   13234   1315 31110   19   153   39  13%      2  127   28    4  740%
c i   34.2   64405   417234     17962   13381   1328 31126   19   155   39  12%      2  128   20    4  516%
c i   34.2   64400   417234     17967   13383   1330 31126   19   155   39  12%      2  128   19    4  509%
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   34.2   64397   417234     17968   13383   1330 31126   19   155   39  12%      2  128   19    4  507%
c i   34.2   64393   417234     17969   13383   1330 31126   19   155   39  12%      2  128   19    4  505%
c i   34.2   64384   417234     17974   13386   1331 31126   19   155   39  12%      2  128   19    4  497%
c i   34.3   64375   417234     18030   13436   1331 31130   19   155   39  12%      2  129   19    4  491%
c i   34.3   64367   417234     18071   13472   1331 31134   19   155   39  12%      2  128   17    4  454%
c i   34.4   64363   417234     18124   13514   1334 31137   19   155   39  12%      1  128   19    4  484%
c i   34.4   64355   417234     18134   13521   1335 31138   19   155   39  12%      1  128   18    4  469%
c i   34.4   64348   417234     18136   13522   1335 31138   19   155   39  12%      1  128   18    4  467%
c 
c [simplification-9] limit of 243 iterations hit after 243 iterations
c [quatres-5] found 29727 quaternary clauses 48% in total
c [quatres-5-2] added 4 single-self-subsuming ternary resolvents
c [quatres-5-2] added 3 quaternary resolvents
c [ternres-5] limit 4000000 with penalty 0 = 0 + 0
c [ternres-5] all 64341 free variables schedulable
c [ternres-5] 56 ternary resolvents (0 bin, 56 trn)
c [ternres-5] 29391 variables remain 46% (34950 retained 54%)
c [decomp-20] removed 3529 variables
c [basicprobe-3] limit 19610478 penalty 0 = 0 + 0
c [basicprobe-3-0] 21911 probes remain 35% after last round
c [basicprobe-3-0] 184 units = 184 failed (100%) + 0 lifted (0%)
c [basicprobe-3-0] removed 1276 variables, found 42127 hbrs
c [bate-2] eliminated 70 asymmetric tautologies during probing
c [unhide-9] limit 784419 with penalty 0 = 0 + 0
c [unhide-9-9] 52 units, 213 failed, 9299 tauts, 0 hbrs, 23766 literals
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 352 transitive binary clauses
c [transred-5] found 8 units
c [elim-7] scheduling all variables this time
c [elim-7] scheduled 61471 variables 100%
c [elim-7] limit of 39220956 steps penalty 1 = 1 + 0
c [elim-7] rescheduling of touched variables disabled
c [elim-7-1] eliminated 3582 variables 6% in round 1 in 31925679 steps
c [elim-7-1] backward subsumption/strengthening limit 7295277
c [elim-7-1-1] backward checking 10787 touched variables 18%
c [elim-7-1-1] fully completed backward checking in 1 rounds
c [elim-7-1] subsumed 47 and strengthened 255 clauses in 2641790 steps
c [elim-7-1] rescheduled 786 variables 1% by backward subsumption
c [elim-7-2] eliminated 77 variables 0% in round 2 in 530836 steps
c [elim-7-2] backward subsumption/strengthening limit 530800
c [elim-7-2-1] backward checking 584 touched variables 1%
c [elim-7-2-1] fully completed backward checking in 1 rounds
c [elim-7-2] subsumed 49 and strengthened 24 clauses in 296742 steps
c [elim-7-2] rescheduled 232 variables 0% by backward subsumption
c [elim-7-3] eliminated 24 variables 0% in round 3 in 178624 steps
c [elim-7-3] backward subsumption/strengthening limit 178600
c [elim-7-3-1] backward checking 119 touched variables 0%
c [elim-7-3-1] fully completed backward checking in 1 rounds
c [elim-7-3] subsumed 13 and strengthened 8 clauses in 167116 steps
c [elim-7] incomplete 198 not tried 0% in round 3
c [gc-58] reconnected 65506 binary clauses (produced 0 empty 1 units)
c [elim-7] transition to [ all 1 rem 1 ] state
c [elim-7] eliminated 3764 = 6% variables out of 61471 scheduled
c [bca-5] limit of 10000000 steps and 727584 added (scaled 2)
c [bca-5] 94444 out of 115416 literals actually usable 82%
c [bca-5] added 152 blocked clauses in 266218 steps
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 11766280 penalty 0 = 0 + 0
c [sweep-5-1] 4747 pos 8.2% + 52848 neg 91.8% = 57595 sched 99.8% ret 112
c [sweep-5-1] 11797465 steps 211 queries 3115.27 avg class size
c [sweep-5-1] 2168 decisions 167 SAT calls 72.77 avg env size
c [sweep-5-1] 53173 variables remain 93% (4265 retained 7%)
c [decomp-21] removed 437 variables
c [sweep-5-1] removed 437 vars (0 failed, 53 eqs, 81 impls)
c [sweep-5] considered successful since not run to completion yet
c [sweep-5] removed 437 vars in TOTAL (1 rounds, 210 queries)
c [phase-count-9] 357699 negative 99.4% of 359841 except 2142 0.6%
c [phase-count-9] 281752 positive 78.3% of 359841 except 78089 21.7%
c [phase-count-9] less non-negative clauses 2142 than limit 35900 (10.0%)
c [phase-count-9] non-pos/non-neg = 78089/2142 = 36.46 >= 2.00 = 200/100
c [lucky-phase-9] forcing lucky phase -1
c [phase-9] phase bias: 0 positive 0%, 223 negative 100%
c [sort-queue-9] sorted 31031 enqueued variables after 18136 conflicts
c [score-dist-9] active 26239 (46%), one 10692 (19%), zero 20339 (36%)
c [score-dist-9] max exp 784, different 594 (76%)
c [score-dist-9] median active exp 679, avg 572.4
c [simplification-9] removed 7071 variables 11.0% (57270 remain 27%)
c [simplification-9] removed 57393 irredundant clauses 13.8% (359841 remain 31%)
c [simplification-9] maximum reduction of 14% = max (11%, 14%)
c [simplification-9] forced so keeping old conflict interval 8000
c [simplification-9] conflict limit remains at 19368 (hard 29156)
c [simplification-9] 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   38.4   57269   359841     18209   10296   1133 68487   18   155   36  12%      1  128   15    4  378%
c i   38.4   57262   359841     18211   10296   1134 68487   18   155   36  12%      1  128   14    4  376%
c i   38.5   57257   359841     18365   10426   1146 68495   18   156   37  12%      1  129   15    4  379%
c i   38.7   57254   359841     18500   10548   1151 68502   18   157   37  11%      1  130   12    4  314%
c i   38.7   57249   359841     18544   10583   1155 68506   18   158   37  11%      1  131   12    4  307%
c i   38.8   57246   359841     18705   10710   1169 68522   18   156   37  11%      1  128   10    4  250%
c i   38.8   57240   359841     18712   10714   1170 68523   17   156   37  11%      1  128   10    4  244%
c i   38.8   57118   359841     18748   10742   1174 68524   17   155   37  11%      1  127    9    4  228%
c i   38.8   57117   359841     18749   10742   1174 68524   17   155   37  11%      1  127    9    4  227%
c i   38.9   57116   359841     18800   10777   1180 68533   17   155   37  11%      1  127    8    4  214%
c i   38.9   57115   359841     18868   10825   1185 68545   17   155   37  11%      1  127    8    4  210%
c i   39.0   57000   359841     18943   10887   1189 68551   17   155   37  11%      1  127    8    4  211%
c i   39.0   56998   359841     18946   10889   1189 68551   17   155   37  11%      1  127    8    4  209%
c i   39.0   56997   359841     18968   10907   1190 68553   17   155   37  11%      1  126    8    4  206%
c i   39.1   56995   359841     19069   10990   1198 68561   17   154   37  11%      1  125    8    4  197%
c i   39.1   56986   359841     19070   10990   1198 68561   17   154   37  11%      1  125    8    4  196%
c i   39.1   56968   359841     19118   11031   1201 68563   17   154   37  11%      1  125    8    4  193%
c i   39.2   56965   359841     19203   11089   1208 68580   16   152   37  11%      1  123    7    4  179%
c 
c [simplification-10] limit 19397 conflicts (hard 29156) hit after 19397 conflicts
c [quatres-6] found 29970 quaternary clauses 50% in total
c [quatres-6-1] removed 1 duplicate quaternary clauses
c [quatres-6-2] added 2 single-self-subsuming ternary resolvents
c [quatres-6-2] added 28 quaternary resolvents
c [ternres-6] limit 4224677 with penalty 0 = 0 + 0
c [ternres-6] 26003 schedulable variables 45%
c [ternres-6] 318 ternary resolvents (3 bin, 315 trn)
c [ternres-6] fully completed ternary resolution
c [card-4] limit 264042 penalty 3 = 3 + 0
c [card-4] found 1306 at-most-one constraints of average size 4.0
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 264042 for elimination
c [card-4] 1306 out of 1306 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [decomp-22] removed 342 variables
c [simpleprobe-4] 4579 schedulable variables 8%
c [simpleprobe-4] limit 16898711 penalty 0 = 0 + 0
c [decomp-23] removed 710 variables
c [simpleprobe-4] 939 variables remain 2% (55279 retained 98%)
c [simpleprobe-4] removed 710 variables, found 24830 hbrs, 267 units
c [unhide-10] limit 844935 with penalty 0 = 0 + 0
c [unhide-10-10] 11 units, 442 failed, 14013 tauts, 0 hbrs, 10920 literals
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 491 transitive binary clauses
c [transred-6] found 4 units
c [cce-3] limit of 7500000 steps penalty 2 = 2 + 0
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 3 (33%) of length 30
c [cce-3-1] eliminated 3 clauses out of 3 (100%) of length 29
c [cce-3-1] eliminated 3 clauses out of 5 (60%) of length 28
c [cce-3-1] eliminated 5 clauses out of 6 (83%) of length 27
c [cce-3-1] eliminated 5 clauses out of 7 (71%) of length 26
c [cce-3-1] eliminated 5 clauses out of 5 (100%) of length 25
c [cce-3-1] eliminated 3 clauses out of 6 (50%) of length 24
c [cce-3-1] eliminated 6 clauses out of 6 (100%) of length 23
c [cce-3-1] eliminated 3 clauses out of 6 (50%) of length 22
c [cce-3-1] eliminated 6 clauses out of 6 (100%) of length 21
c [cce-3-1] eliminated 3 clauses out of 6 (50%) of length 20
c [cce-3-1] eliminated 6 clauses out of 6 (100%) of length 19
c [cce-3-1] eliminated 3 clauses out of 7 (43%) of length 18
c [cce-3-1] eliminated 8 clauses out of 8 (100%) of length 17
c [cce-3-1] eliminated 4 clauses out of 8 (50%) of length 16
c [cce-3-1] eliminated 8 clauses out of 8 (100%) of length 15
c [cce-3-1] eliminated 4 clauses out of 8 (50%) of length 14
c [cce-3-1] eliminated 8 clauses out of 9 (89%) of length 13
c [cce-3-1] eliminated 6 clauses out of 10 (60%) of length 12
c [cce-3-1] eliminated 9 clauses out of 10 (90%) of length 11
c [cce-3-1] eliminated 6 clauses out of 82 (7%) of length 10
c [cce-3-1] eliminated 10 clauses out of 238 (4%) of length 9
c [cce-3-1] eliminated 7 clauses out of 365 (2%) of length 8
c [cce-3-1] eliminated 16 clauses out of 508 (3%) of length 7
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 147 large clauses in 7500004 steps
c [cce-3-1] allowing another 3750002 steps for small clauses
c [cce-3-1] scheduling 197350 clauses = 178292 binary + 19058 ternary
c [cce-3-1] tried to eliminate 297 small clauses 0%
c [cce-3-1] eliminated 86 binary clauses 0%
c [cce-3-1] eliminated 15 ternary clauses 0%
c [cce-3-1] eliminated 101 small clauses 0%
c [cce-3-1] eliminated 5388 small clauses in 7500004 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 5535 covered clauses in round 1
c [cce-3] eliminated 5535 covered clauses in TOTAL during 1 rounds
c [elim-8] no untried remaining variables left
c [elim-8] scheduled 55668 variables 100%
c [elim-8] boosting limit by 20
c [elim-8] limit of 1689871140 steps penalty 0 = 0 + 0
c [elim-8] rescheduling of touched variables disabled
c [elim-8-1] eliminated 811 variables 1% in round 1 in 29542619 steps
c [elim-8-1] backward subsumption/strengthening limit 29542600
c [elim-8-1-1] backward checking 3554 touched variables 6%
c [elim-8-1-1] fully completed backward checking in 1 rounds
c [elim-8-1] subsumed 36 and strengthened 86 clauses in 980160 steps
c [elim-8-1] rescheduled 333 variables 1% by backward subsumption
c [elim-8-2] eliminated 33 variables 0% in round 2 in 560026 steps
c [elim-8-2] backward subsumption/strengthening limit 560000
c [elim-8-2-1] backward checking 274 touched variables 0%
c [elim-8-2-1] fully completed backward checking in 1 rounds
c [elim-8-2] subsumed 17 and strengthened 20 clauses in 166399 steps
c [elim-8-2] rescheduled 76 variables 0% by backward subsumption
c [elim-8-3] eliminated 9 variables 0% in round 3 in 236175 steps
c [elim-8-3] backward subsumption/strengthening limit 236100
c [elim-8-3-1] backward checking 85 touched variables 0%
c [elim-8-3-1] fully completed backward checking in 1 rounds
c [elim-8-3] subsumed 10 and strengthened 5 clauses in 107263 steps
c [elim-8] incomplete 34 not tried 0% in round 3
c [gc-66] reconnected 75399 binary clauses (produced 0 empty 1 units)
c [elim-8] transition to [ all 1 rem 1 ] state
c [elim-8] eliminated 877 = 2% variables out of 55668 scheduled
c [bca-6] limit of 10000000 steps and 684100 added (scaled 2)
c [bca-6] 86548 out of 109584 literals actually usable 79%
c [bca-6] added 74 blocked clauses in 237939 steps
c [sweep-6] limit 1267403 penalty 0 = 0 + 0
c [sweep-6-1] 5296 pos 10.4% + 45748 neg 89.6% = 51044 sched 93.2% ret 3747
c [sweep-6-1] 1277148 steps 21 queries 10070.24 avg class size
c [sweep-6-1] 307 decisions 16 SAT calls 47.69 avg env size
c [sweep-6-1] 50989 variables remain 93% (3796 retained 7%)
c [decomp-24] removed 23 variables
c [sweep-6-1] removed 23 vars (0 failed, 5 eqs, 8 impls)
c [sweep-6] considered successful since not run to completion yet
c [sweep-6] removed 23 vars in TOTAL (1 rounds, 20 queries)
c [phase-count-10] 339455 negative 99.4% of 341505 except 2050 0.6%
c [phase-count-10] 265053 positive 77.6% of 341505 except 76452 22.4%
c [phase-count-10] less non-negative clauses 2050 than limit 34100 (10.0%)
c [phase-count-10] non-pos/non-neg = 76452/2050 = 37.29 >= 2.00 = 200/100
c [lucky-phase-10] forcing lucky phase -1
c [phase-10] phase bias: 0 positive 0%, 90 negative 100%
c [sort-queue-10] sorted 24255 enqueued variables after 19397 conflicts
c [score-dist-10] active 30513 (56%), one 8327 (15%), zero 15928 (29%)
c [score-dist-10] max exp 617, different 563 (91%)
c [score-dist-10] median active exp 389, avg 405.9
c [simplification-10] removed 2180 variables 3.8% (54768 remain 26%)
c [simplification-10] removed 18336 irredundant clauses 5.1% (341505 remain 29%)
c [simplification-10] maximum reduction of 5% = max (4%, 5%)
c [simplification-10] large reduction 5% >= 5% limit
c [simplification-10] next conflict interval 2000 = 2000/1
c [simplification-10] penalized conflict interval 2000 = 1 * 2000
c [simplification-10] hard conflict limit 31397 (soft 21397 + delta 10000)
c [simplification-10] new conflict limit 21397 (hard 31397)
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   42.5   54767   341505     19419   10379   1326 75075   16   150   35  10%      1  121    6    4  162%
c i   42.6   54711   341505     19524   10464   1334 75085   16   149   35  10%      1  119    6    4  164%
c i   42.6   54709   341505     19556   10487   1340 75087   15   149   35  10%      1  119    7    4  170%
c i   42.8   54703   341505     19742   10635   1356 75104   15   151   35  10%      1  121   12    4  292%
c i   42.8   54702   341505     19761   10653   1356 75104   15   152   35  10%      1  122   12    4  293%
c i   43.1   54697   341505     20003   10856   1371 75121   16   155   35  10%      1  124   19    4  470%
c i   43.2   54630   341505     20111   10951   1377 75123   16   156   35  10%      1  125   20    4  501%
c i   43.2   54629   341505     20173   11001   1378 75129   16   156   35  10%      1  125   19    4  456%
c i   43.2   54621   341505     20174   11001   1378 75129   16   156   35  10%      1  125   18    4  454%
c i   43.3   54606   341505     20303   11106   1387 75138   16   157   35  10%      1  126   19    4  459%
c i   43.3   54605   341505     20304   11106   1387 75138   16   157   35  10%      1  126   19    4  457%
c i   43.3   54603   341505     20305   11106   1387 75138   16   157   35  10%      1  126   19    4  455%
c i   43.3   54602   341505     20306   11106   1387 75138   16   157   35  10%      1  126   19    4  454%
c i   43.3   54601   341505     20307   11106   1387 75138   16   157   35  10%      1  126   19    4  452%
c i   43.4   54600   341505     20418   11196   1397 75147   16   157   35  10%      1  126   16    4  385%
c i   43.5   54575   341505     20478   11247   1399 75153   16   158   35  10%      1  127   15    4  362%
c i   43.7   54558   341505     20656   11395   1408 75168   16   159   35  10%      1  127   16    4  377%
c i   43.8   54557   341505     20866   11577   1418 75182   16   158   35  10%      1  126   12    4  293%
c i   43.8   54550   341505     20876   11580   1418 75185   15   158   35  10%      1  126   12    4  286%
c i   43.9   54541   341505     21042   11727   1424 75191   16   158   35  10%      1  126   16    4  371%
c i   44.0   54480   341505     21055   11737   1424 75193   16   159   35  10%      1  127   15    4  365%
c i   44.0   54479   341505     21109   11779   1429 75197   16   161   35  10%      1  128   15    4  356%
c i   44.0   54475   341505     21113   11781   1429 75198   16   161   35  10%      1  128   15    4  352%
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   44.1   54470   341505     21187   11843   1434 75203   16   161   35  10%      1  128   15    4  351%
c i   44.2   54469   341505     21344   11982   1437 75209   16   160   35  10%      1  127   19    4  438%
c i   44.2   54466   341505     21364   12000   1437 75210   16   160   35  10%      1  127   18    4  429%
c 
c [simplification-11] limit 21450 conflicts (hard 31397) hit after 21451 conflicts
c [quatres-7] found 28620 quaternary clauses 50% in total
c [quatres-7-1] removed 1 duplicate quaternary clauses
c [quatres-7-2] added 2 single-self-subsuming ternary resolvents
c [quatres-7-2] added 7 quaternary resolvents
c [ternres-7] limit 4717273 with penalty 0 = 0 + 0
c [ternres-7] all 54466 free variables schedulable
c [ternres-7] 187 ternary resolvents (0 bin, 187 trn)
c [ternres-7] 14358 variables remain 26% (40108 retained 74%)
c [gauss-4] limit 500000 penalty 2 = 2 + 0
c [gauss-4] extracted 17 xors of average arity 2.8
c [gauss-4] connected 48 occurrences of 45 variables (average 1.1)
c [gauss-4] limit 500000 penalty 2 = 2 + 0
c [gauss-4] fully completed
c [gauss-4] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-25] removed 15 variables
c [treelook-4] limit 471727 penalty 0 = 0 + 0 boost 1
c [treelook-4] scheduled 64117 literals 59%
c [treelook-4] scheduling used 471744 steps
c [treelook-4] not fully scheduled
c [treelook-4] limit 471727 penalty 0 = 0 + 0 boost 1
c [treelook-4] used 531110 steps
c [treelook-4] 64104 literals remain 59%
c [treelook-4] 27181 variables remain to probed next time 50%
c [treelook-4] removed 1 variables, found 4041 hbrs
c [unhide-11] limit 943454 with penalty 0 = 0 + 0
c [unhide-11-11] 12 units, 30 failed, 7050 tauts, 0 hbrs, 9176 literals
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 364 transitive binary clauses
c [transred-7] found 7 units
c [block-4] scheduling all variables this time
c [block-4] scheduled 54302 variables 100%
c [block-4] limit of 12500000 steps penalty 2 = 2 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 107 blocked clauses
c [block-4] 107 < 1/100 * 333277 = 3332 considered unsuccessful
c [elim-9] no untried remaining variables left
c [elim-9] scheduled 54298 variables 100%
c [elim-9] limit of 94345469 steps penalty 0 = 0 + 0
c [elim-9] rescheduling of touched variables disabled
c [elim-9-1] eliminated 770 variables 1% in round 1 in 28085295 steps
c [elim-9-1] backward subsumption/strengthening limit 28085200
c [elim-9-1-1] backward checking 3316 touched variables 6%
c [elim-9-1-1] fully completed backward checking in 1 rounds
c [elim-9-1] subsumed 19 and strengthened 62 clauses in 913865 steps
c [elim-9-1] rescheduled 203 variables 0% by backward subsumption
c [elim-9-2] eliminated 24 variables 0% in round 2 in 158771 steps
c [elim-9-2] backward subsumption/strengthening limit 158700
c [elim-9-2-1] backward checking 267 touched variables 0%
c [elim-9-2-1] incomplete backward checking 0 remain 0%
c [elim-9-2] subsumed 12 and strengthened 5 clauses in 158701 steps
c [elim-9-2] rescheduled 33 variables 0% by backward subsumption
c [elim-9-3] eliminated 3 variables 0% in round 3 in 30080 steps
c [elim-9-3] backward subsumption/strengthening limit 30000
c [elim-9-3-1] backward checking 60 touched variables 0%
c [elim-9-3-1] incomplete backward checking 2 remain 3%
c [elim-9-3] subsumed 3 and strengthened 0 clauses in 30013 steps
c [elim-9] incomplete 8 not tried 0% in round 3
c [elim-9] transition to [ all 1 rem 1 ] state
c [elim-9] eliminated 836 = 2% variables out of 54298 scheduled
c [bca-7] limit of 10000000 steps and 660181 added (scaled 2)
c [bca-7] 82446 out of 106926 literals actually usable 77%
c [bca-7] added 48 blocked clauses in 223256 steps
c [sweep-7] limit 1415182 penalty 0 = 0 + 0
c [sweep-7-1] 3824 pos 7.7% + 45970 neg 92.3% = 49794 sched 93.1% ret 3668
c [sweep-7-1] 1477024 steps 37 queries 9107.16 avg class size
c [sweep-7-1] 256 decisions 32 SAT calls 60.78 avg env size
c [sweep-7-1] 49576 variables remain 93% (3886 retained 7%)
c [decomp-27] removed 157 variables
c [sweep-7-1] removed 157 vars (0 failed, 5 eqs, 7 impls)
c [sweep-7] removed 157 vars in TOTAL (1 rounds, 36 queries)
c [phase-count-11] 327471 negative 99.4% of 329447 except 1976 0.6%
c [phase-count-11] 256227 positive 77.8% of 329447 except 73220 22.2%
c [phase-count-11] skipping relative phase luck test
c [phase-11] phase bias: 2 positive 100%, 0 negative 0%
c [sort-queue-11] sorted 24106 enqueued variables after 21451 conflicts
c [score-dist-11] active 29199 (55%), one 9620 (18%), zero 14486 (27%)
c [score-dist-11] max exp 658, different 597 (91%)
c [score-dist-11] median active exp 504, avg 455.3
c [simplification-11] removed 1161 variables 2.1% (53305 remain 25%)
c [simplification-11] removed 12058 irredundant clauses 3.5% (329447 remain 28%)
c [simplification-11] maximum reduction of 4% = max (2%, 4%)
c [simplification-11] geometric conflict interval increment 4000 = 20000 / 5
c [simplification-11] new conflict interval 12000
c [simplification-11] penalized conflict interval 12000 = 1 * 12000
c [simplification-11] hard conflict limit 43451 (soft 33451 + delta 10000)
c [simplification-11] new conflict limit 33451 (hard 43451)
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   47.2   53304   329447     21543   11579   1509 77373   16   160   35  10%      1  126   16    4  374%
c i   47.4   53303   329447     21785   11793   1521 77387   15   160   36  10%      1  126   13    4  291%
c i   47.5   53302   329447     21808   11815   1521 77387   16   162   36  10%      1  128   13    4  302%
c i   47.5   53296   329447     21826   11829   1522 77389   16   162   36  10%      1  128   14    4  326%
c i   47.7   53295   329447     22136   12093   1539 77402   15   162   36  10%      1  127   15    4  338%
c i   47.8   53294   329447     22231   12178   1542 77408   16   164   36   9%      1  129   16    4  359%
c i   47.9   53290   329447     22320   12248   1548 77419   15   166   36   9%      1  131   14    4  318%
c i   48.1   53283   329447     22507   12421   1551 77424   16   171   36   9%      1  136   25    4  559%
c i   48.4   53280   329447     22837   12718   1561 77441   17   172   36  10%      1  136   21    5  461%
c i   48.4   53279   329447     22846   12722   1563 77443   17   172   36  10%      1  136   21    5  453%
c i   48.4   53278   329447     22874   12742   1566 77445   17   171   36  10%      1  135   21    5  457%
c i   48.5   53275   329447     22917   12775   1568 77451   17   171   36  10%      1  135   20    5  438%
c i   48.5   53149   329447     22985   12835   1567 77457   17   172   36  10%      1  136   18    5  392%
c i   48.6   53141   329447     23082   12912   1579 77463   16   172   36  10%      1  136   15    5  335%
c i   48.6   53140   329447     23094   12920   1579 77466   16   172   36  10%      1  136   15    5  329%
c i   48.7   53138   329447     23169   12988   1582 77467   16   172   36  10%      1  136   16    5  355%
c i   48.7   53134   329447     23172   12990   1582 77467   16   172   36  10%      1  136   17    5  359%
c i   48.7   53131   329447     23176   12992   1583 77467   16   172   36  10%      1  136   17    5  359%
c i   48.9   53130   329447     23419   13218   1592 77472   17   173   36  10%      1  136   19    5  412%
c i   49.0   53128   329447     23553   13337   1594 77475   17   173   36  10%      1  136   21    5  436%
c i   49.0   53122   329447     23558   13341   1594 77475   17   174   36  10%      1  136   21    5  447%
c i   49.1   53116   329447     23598   13377   1595 77476   17   173   36  10%      1  136   23    5  478%
c i   49.1   53115   329447     23621   13399   1595 77476   17   174   36  10%      1  136   25    5  528%
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.2   53114   329447     23754   13527   1596 77478   18   176   36  10%      1  138   26    5  541%
c i   49.3   53111   329447     23924   13683   1601 77482   18   175   36  10%      1  137   22    5  462%
c i   49.3   53106   329447     23925   13683   1601 77482   18   175   36  10%      1  137   22    5  460%
c i   49.3   53105   329447     23930   13686   1601 77483   18   175   36  10%      1  137   22    5  454%
c i   49.5   53104   329447     24140   13869   1608 77495   18   177   36  10%      1  139   22    5  445%
c i   49.6   53090   329447     24238   13951   1612 77502   18   178   36  10%      1  139   21    5  436%
c i   49.6   53084   329447     24239   13951   1612 77502   18   178   36  10%      1  139   21    5  434%
c i   50.0   53076   329447     24715   14369   1624 77525   19   179   36  10%      2  140   26    5  504%
c i   50.1   53075   329447     24904   14534   1635 77534   19   178   36  11%      2  138   27    5  518%
c i   50.3   53072   329447     25084   14702   1638 77538   20   181   36  11%      2  140   28    5  545%
c i   50.3   53064   329447     25096   14711   1638 77540   20   181   36  11%      2  140   29    5  549%
c i   50.3   53063   329447     25101   14712   1638 77543   20   180   36  11%      2  140   28    5  538%
c i   50.3   53057   329447     25141   14746   1639 77545   20   182   36  11%      1  141   27    5  518%
c i   50.3   53049   329447     25143   14747   1639 77545   20   182   36  11%      1  141   27    5  518%
c i   50.3   53048   329447     25144   14747   1639 77545   20   182   36  11%      1  141   27    5  516%
c i   50.3   53046   329447     25146   14748   1639 77545   20   181   36  11%      1  141   27    5  515%
c i   50.3   53038   329447     25147   14748   1639 77545   20   181   36  11%      1  141   27    5  513%
c i   50.6   53032   329447     25434   14989   1661 77561   20   182   36  11%      2  140   20    5  375%
c i   50.9   53028   329447     25948   15424   1678 77594   21   180   36  11%      2  138   25    5  463%
c i   51.0   53021   329447     25986   15455   1677 77597   21   180   36  11%      2  138   26    5  467%
c i   51.3   53020   329447     26342   15762   1690 77613   21   184   36  11%      2  141   25    6  455%
c i   51.4   53015   329447     26416   15822   1693 77620   21   185   36  11%      2  142   24    6  434%
c i   51.6   53014   329447     26627   16013   1703 77624   21   187   36  11%      2  143   22    6  393%
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.8   53007   329447     26795   16155   1710 77638   21   187   36  11%      2  143   20    6  346%
c i   52.2   53004   329447     27177   16487   1729 77659   22   192   38  11%      2  147   28    6  482%
c i   52.3   52994   329447     27289   16574   1738 77667   21   190   38  11%      2  144   23    6  398%
c i   52.4   52992   329447     27383   16665   1738 77668   21   189   38  11%      2  143   23    6  389%
c i   52.4   52989   329447     27446   16717   1741 77671   21   190   38  11%      2  144   22    6  383%
c i   52.5   52982   329447     27579   16836   1745 77677   22   190   38  11%      1  143   25    6  422%
c i   52.6   52981   329447     27622   16876   1746 77677   22   190   38  12%      1  143   26    6  446%
c i   52.7   52975   329447     27800   17037   1750 77682   22   192   38  12%      1  146   29    6  479%
c i   53.1   52971   329447     28122   17315   1760 77692   23   192   38  12%      1  144   28    6  460%
c i   53.2   52970   329447     28284   17466   1763 77694   23   192   38  12%      1  144   26    6  430%
c i   53.2   52963   329447     28302   17480   1763 77695   23   192   38  12%      1  144   26    6  417%
c i   53.3   52956   329447     28344   17513   1764 77701   23   191   38  12%      1  143   24    6  396%
c i   53.4   52952   329447     28626   17764   1777 77712   23   188   39  12%      1  140   23    6  371%
c i   53.4   52949   329447     28627   17764   1777 77712   23   188   39  12%      1  140   23    6  370%
c i   53.7   52914   329447     28908   18023   1785 77721   23   191   39  12%      1  142   29    6  452%
c i   53.8   52910   329447     28964   18056   1788 77738   23   192   39  12%      1  143   26    6  408%
c i   54.0   52909   329447     29264   18318   1802 77750   24   196   39  12%      1  146   28    6  434%
c i   54.1   52903   329447     29336   18378   1805 77755   23   196   39  12%      1  146   24    6  368%
c i   54.1   52897   329447     29337   18378   1805 77755   23   196   39  12%      1  146   24    6  367%
c i   54.1   52892   329447     29338   18378   1805 77755   23   196   39  12%      1  146   24    6  365%
c i   54.1   52885   329447     29340   18378   1806 77755   23   196   39  12%      1  146   23    6  363%
c i   54.2   52881   329447     29409   18439   1808 77758   23   195   39  12%      1  145   22    6  338%
c i   54.4   52878   329447     29600   18618   1813 77760   24   197   39  12%      1  147   26    7  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   54.4   52871   329447     29614   18630   1814 77760   24   197   39  12%      1  147   26    7  395%
c i   54.4   52865   329447     29700   18701   1818 77765   23   198   39  12%      1  147   23    7  348%
c i   54.6   52862   329447     29796   18783   1822 77771   24   197   39  12%      1  146   24    7  364%
c i   54.6   52858   329447     29797   18783   1822 77771   24   197   39  12%      1  146   24    7  362%
c i   54.6   52853   329447     29798   18783   1822 77771   24   197   39  12%      1  146   24    7  361%
c i   54.6   52847   329447     29824   18802   1823 77776   23   196   39  12%      1  145   23    7  345%
c i   54.8   52839   329447     30060   19022   1827 77784   24   197   39  12%      1  145   31    7  461%
c i   54.8   52837   329447     30061   19022   1827 77784   24   197   39  12%      1  145   31    7  460%
c i   54.9   52833   329447     30211   19153   1834 77789   24   196   39  12%      1  144   33    7  496%
c i   55.0   52830   329447     30277   19208   1836 77791   25   196   39  13%      1  144   37    7  541%
c i   55.2   52829   329447     30439   19352   1843 77800   25   196   39  13%      1  143   36    7  524%
c i   55.8   52823   329447     30932   19799   1855 77821   26   198   40  13%      2  144   38    7  534%
c i   56.0   52822   329447     31128   19968   1866 77830   27   197   40  13%      2  143   33    7  467%
c i   56.0   52816   329447     31129   19968   1866 77830   27   197   40  13%      2  143   33    7  466%
c i   56.0   52806   329447     31130   19968   1866 77830   27   197   40  13%      2  143   33    7  464%
c i   56.0   52797   329447     31131   19968   1866 77830   27   197   40  13%      2  143   33    7  462%
c i   56.1   52785   329447     31193   20024   1867 77833   27   197   40  13%      2  143   32    7  453%
c i   56.3   52775   329447     31445   20253   1877 77841   27   196   40  14%      2  142   29    7  404%
c i   56.3   52774   329447     31474   20276   1881 77842   27   196   40  14%      1  142   30    7  415%
c i   56.5   52773   329447     31732   20500   1890 77851   27   196   41  14%      1  141   32    7  440%
c i   56.8   52772   329447     32042   20787   1901 77857   28   195   41  14%      2  139   28    7  375%
c i   56.8   52771   329447     32045   20789   1901 77857   28   195   41  14%      2  139   28    7  372%
c i   56.8   52770   329447     32056   20799   1901 77857   28   194   41  14%      2  138   28    7  376%
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   57.1   52759   329447     32263   20980   1905 77865   28   193   41  15%      1  137   36    8  477%
c i   57.1   52751   329447     32336   21041   1912 77869   28   193   41  15%      1  136   34    8  449%
c i   57.3   52749   329447     32489   21186   1915 77871   29   194   41  15%      1  138   45    8  586%
c i   57.5   52743   329447     32688   21365   1922 77877   30   195   41  15%      1  138   40    8  507%
c i   57.6   52740   329447     32780   21448   1928 77879   30   197   41  15%      1  139   37    8  466%
c i   57.9   52737   329447     33081   21725   1935 77889   30   197   42  15%      1  139   37    8  464%
c i   57.9   52730   329447     33082   21725   1935 77889   30   197   42  15%      1  139   37    8  463%
c i   58.0   52704   329447     33208   21842   1938 77893   30   196   42  15%      1  138   33    8  409%
c i   58.0   52703   329447     33209   21842   1938 77893   30   196   42  15%      1  138   33    8  407%
c i   58.1   52699   329447     33329   21941   1942 77903   30   195   42  15%      1  136   33    8  413%
c i   58.1   52691   329447     33358   21968   1943 77903   30   195   42  15%      1  137   32    8  392%
c i   58.3   52690   329447     33435   22039   1944 77904   31   195   42  16%      1  136   38    8  462%
c i   58.3   52684   329447     33437   22040   1944 77904   31   195   42  16%      1  136   37    8  459%
c 
c [simplification-12] limit 33636 conflicts (hard 43451) hit after 33637 conflicts
c [quatres-8] found 27262 quaternary clauses 49% in total
c [quatres-8-1] added 1 double-self-subsuming ternary resolvents
c [quatres-8-2] added 8 quaternary resolvents
c [ternres-8] limit 7769484 with penalty 0 = 0 + 0
c [ternres-8] 13898 schedulable variables 26%
c [ternres-8] 250 ternary resolvents (1 bin, 249 trn)
c [ternres-8] fully completed ternary resolution
c [decomp-28] removed 691 variables
c [basicprobe-4] limit 38847420 penalty 0 = 0 + 0
c [basicprobe-4-0] 16541 probes remain 32% after last round
c [basicprobe-4-0] 431 units = 431 failed (100%) + 0 lifted (0%)
c [basicprobe-4-0] removed 1022 variables, found 66864 hbrs
c [bate-3] eliminated 106 asymmetric tautologies during probing
c [unhide-12] limit 1553896 with penalty 0 = 0 + 0
c [unhide-12-12] 20 units, 471 failed, 14794 tauts, 0 hbrs, 44885 literals
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 381 transitive binary clauses
c [transred-8] found 2 units
c [cce-4] boosting limit by 10
c [cce-4] limit of 194237100 steps penalty 1 = 1 + 0
c [cce-4-1] eliminated 1 clauses out of 1 (100%) of length 33
c [cce-4-1] eliminated 2 clauses out of 3 (67%) of length 32
c [cce-4-1] eliminated 2 clauses out of 3 (67%) of length 31
c [cce-4-1] eliminated 1 clauses out of 3 (33%) of length 30
c [cce-4-1] eliminated 1 clauses out of 59 (2%) of length 10
c [cce-4-1] eliminated 1 clauses out of 314 (0%) of length 8
c [cce-4-1] eliminated 4 clauses out of 430 (1%) of length 7
c [cce-4-1] eliminated 52 clauses out of 1235 (4%) of length 6
c [cce-4-1] eliminated 13729 clauses out of 20255 (68%) of length 5
c [cce-4-1] eliminated 8270 clauses out of 25238 (33%) of length 4
c [cce-4-1] incomplete large round (ATE)
c [cce-4-1] eliminated 22063 large clauses in 194237104 steps
c [cce-4-1] allowing another 97118552 steps for small clauses
c [cce-4-1] scheduling 245303 clauses = 162467 binary + 82836 ternary
c [cce-4-1] tried to eliminate 5752 small clauses 2%
c [cce-4-1] eliminated 1123 binary clauses 1%
c [cce-4-1] eliminated 285 ternary clauses 0%
c [cce-4-1] eliminated 1408 small clauses 1%
c [cce-4-1] eliminated 5672 small clauses in 194237113 steps
c [cce-4-1] incomplete small round (ATE)
c [cce-4-1] eliminated 27735 covered clauses in round 1
c [cce-4] eliminated 27735 covered clauses in TOTAL during 1 rounds
c [elim-10] no untried remaining variables left
c [elim-10] scheduled 51118 variables 100%
c [elim-10] limit of 155389683 steps penalty 0 = 0 + 0
c [elim-10] rescheduling of touched variables disabled
c [elim-10-1] eliminated 12493 variables 24% in round 1 in 23980531 steps
c [elim-10-1] backward subsumption/strengthening limit 23980500
c [elim-10-1-1] backward checking 27777 touched variables 54%
c [elim-10-1-1] fully completed backward checking in 1 rounds
c [elim-10-1] subsumed 83 and strengthened 475 clauses in 3621365 steps
c [elim-10-1] rescheduled 1191 variables 2% by backward subsumption
c [elim-10-2] eliminated 58 variables 0% in round 2 in 1609208 steps
c [elim-10-2] backward subsumption/strengthening limit 1609200
c [elim-10-2-1] backward checking 664 touched variables 1%
c [elim-10-2-1] fully completed backward checking in 1 rounds
c [elim-10-2] subsumed 22 and strengthened 29 clauses in 466827 steps
c [elim-10-2] rescheduled 106 variables 0% by backward subsumption
c [elim-10-3] eliminated 8 variables 0% in round 3 in 67774 steps
c [elim-10-3] backward subsumption/strengthening limit 67700
c [elim-10-3-1] backward checking 60 touched variables 0%
c [elim-10-3-1] incomplete backward checking 0 remain 0%
c [elim-10-3] subsumed 9 and strengthened 5 clauses in 67701 steps
c [elim-10] incomplete 22 not tried 0% in round 3
c [elim-10] transition to [ all 1 rem 1 ] state
c [elim-10] eliminated 12583 = 25% variables out of 51118 scheduled
c [bca-8] limit of 10000000 steps and 517889 added (scaled 2)
c [bca-8] 65765 out of 77072 literals actually usable 85%
c [bca-8] added 196 blocked clauses in 156711 steps
c [sweep-8] limit 2330845 penalty 0 = 0 + 0
c [sweep-8-1] 3369 pos 9.3% + 32696 neg 90.7% = 36065 sched 93.6% ret 2470
c [sweep-8-1] 2362875 steps 44 queries 5235.52 avg class size
c [sweep-8-1] 566 decisions 37 SAT calls 88.27 avg env size
c [sweep-8-1] 35811 variables remain 93% (2694 retained 7%)
c [decomp-29] removed 119 variables
c [sweep-8-1] removed 119 vars (0 failed, 10 eqs, 11 impls)
c [sweep-8] removed 119 vars in TOTAL (1 rounds, 43 queries)
c [phase-count-12] 257075 negative 99.7% of 257898 except 823 0.3%
c [phase-count-12] 189924 positive 73.6% of 257898 except 67974 26.4%
c [phase-count-12] skipping relative phase luck test
c [phase-12] phase bias: 0 positive 0%, 1 negative 100%
c [sort-queue-12] sorted 19591 enqueued variables after 33637 conflicts
c [score-dist-12] active 18825 (49%), one 10212 (27%), zero 9379 (24%)
c [score-dist-12] max exp 864, different 658 (76%)
c [score-dist-12] median active exp 786, avg 689.2
c [simplification-12] removed 14262 variables 27.1% (38416 remain 18%)
c [simplification-12] removed 71549 irredundant clauses 21.7% (257898 remain 22%)
c [simplification-12] maximum reduction of 27% = max (27%, 22%)
c [simplification-12] large reduction 27% >= 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 45637 (soft 35637 + delta 10000)
c [simplification-12] new conflict limit 35637 (hard 45637)
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   67.9   38415   257898     33745    4791   2013 103362   30   192   29  16%      1  133   27    8  329%
c i   68.1   38411   257898     34163    5152   2033 103394   28   185   29  15%      2  125   12    8  148%
c i   68.2   38410   257898     34313    5286   2035 103405   28   186   29  15%      1  125   14    8  165%
c i   68.5   38409   257898     34853    5760   2057 103434   26   185   29  14%      2  123   17    8  206%
c i   68.9   38408   257898     35615    6444   2089 103456   24   180   29  13%      4  117   15    8  176%
c i   68.9   38407   257898     35618    6446   2089 103456   24   180   29  13%      4  117   15    8  175%
c 
c [simplification-13] limit 35640 conflicts (hard 45637) hit after 35640 conflicts
c [quatres-9] found 23509 quaternary clauses 68% in total
c [quatres-9-1] removed 4 duplicate quaternary clauses
c [quatres-9-2] added 2 single-self-subsuming ternary resolvents
c [quatres-9-2] added 21 quaternary resolvents
c [ternres-9] limit 8145791 with penalty 0 = 0 + 0
c [ternres-9] all 38404 free variables schedulable
c [ternres-9] 1107 ternary resolvents (3 bin, 1104 trn)
c [ternres-9] fully completed ternary resolution
c [decomp-30] removed 16 variables
c [simpleprobe-5] 819 schedulable variables 2%
c [simpleprobe-5] limit 32583165 penalty 0 = 0 + 0
c [decomp-31] removed 925 variables
c [simpleprobe-5] fully completed simple probing
c [simpleprobe-5] removed 925 variables, found 50409 hbrs, 425 units
c [unhide-13] limit 1629158 with penalty 0 = 0 + 0
c [unhide-13-14] 16 units, 299 failed, 23151 tauts, 0 hbrs, 6714 literals
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 535 transitive binary clauses
c [transred-9] found 1 units
c [cce-5] limit of 40728957 steps penalty 0 = 0 + 0
c [cce-5-1] eliminated 5 clauses out of 15 (33%) of length 7
c [cce-5-1] eliminated 67 clauses out of 1022 (7%) of length 6
c [cce-5-1] eliminated 132 clauses out of 7065 (2%) of length 5
c [cce-5-1] incomplete large round (ACCE)
c [cce-5-1] eliminated 204 large clauses in 40728961 steps
c [cce-5-1] allowing another 20364480 steps for small clauses
c [cce-5-1] scheduling 138938 clauses = 119940 binary + 18998 ternary
c [cce-5-1] tried to eliminate 2330 small clauses 2%
c [cce-5-1] eliminated 629 binary clauses 1%
c [cce-5-1] eliminated 191 ternary clauses 1%
c [cce-5-1] eliminated 820 small clauses 1%
c [cce-5-1] eliminated 2309 small clauses in 40728959 steps
c [cce-5-1] incomplete small round (ACCE)
c [cce-5-1] eliminated 2513 covered clauses in round 1
c [cce-5] eliminated 2513 covered clauses in TOTAL during 1 rounds
c [elim-11] no untried remaining variables left
c [elim-11] scheduled 37272 variables 100%
c [elim-11] limit of 162915828 steps penalty 0 = 0 + 0
c [elim-11] rescheduling of touched variables disabled
c [elim-11-1] eliminated 829 variables 2% in round 1 in 19995745 steps
c [elim-11-1] backward subsumption/strengthening limit 19995700
c [elim-11-1-1] backward checking 4448 touched variables 12%
c [elim-11-1-1] fully completed backward checking in 1 rounds
c [elim-11-1] subsumed 49 and strengthened 117 clauses in 1215314 steps
c [elim-11-1] rescheduled 359 variables 1% by backward subsumption
c [elim-11-2] eliminated 40 variables 0% in round 2 in 1112816 steps
c [elim-11-2] backward subsumption/strengthening limit 1112800
c [elim-11-2-1] backward checking 250 touched variables 1%
c [elim-11-2-1] fully completed backward checking in 1 rounds
c [elim-11-2] subsumed 17 and strengthened 12 clauses in 146035 steps
c [elim-11-2] rescheduled 50 variables 0% by backward subsumption
c [elim-11-3] eliminated 5 variables 0% in round 3 in 32414 steps
c [elim-11-3] backward subsumption/strengthening limit 32400
c [elim-11-3-1] backward checking 53 touched variables 0%
c [elim-11-3-1] incomplete backward checking 0 remain 0%
c [elim-11-3] subsumed 11 and strengthened 3 clauses in 32401 steps
c [elim-11] incomplete 25 not tried 0% in round 3
c [gc-91] reconnected 129465 binary clauses (produced 0 empty 1 units)
c [elim-11] transition to [ all 1 rem 1 ] state
c [elim-11] eliminated 882 = 2% variables out of 37272 scheduled
c [bca-9] limit of 10000000 steps and 477819 added (scaled 2)
c [bca-9] 59383 out of 72782 literals actually usable 82%
c [bca-9] added 71 blocked clauses in 142314 steps
c [sweep-9] limit 2443737 penalty 0 = 0 + 0
c [sweep-9-1] 3557 pos 10.5% + 30444 neg 89.5% = 34001 sched 93.4% ret 2389
c [sweep-9-1] 2462692 steps 66 queries 4154.83 avg class size
c [sweep-9-1] 712 decisions 59 SAT calls 68.53 avg env size
c [sweep-9-1] 33194 variables remain 91% (3174 retained 9%)
c [decomp-32] removed 67 variables
c [sweep-9-1] removed 67 vars (0 failed, 8 eqs, 15 impls)
c [sweep-9] removed 67 vars in TOTAL (1 rounds, 65 queries)
c [phase-count-13] 237320 negative 99.7% of 238077 except 757 0.3%
c [phase-count-13] 172915 positive 72.6% of 238077 except 65162 27.4%
c [phase-count-13] skipping relative phase luck test
c [phase-13] phase bias: 1 positive 100%, 0 negative 0%
c [sort-queue-13] sorted 15877 enqueued variables after 35640 conflicts
c [score-dist-13] active 20446 (56%), one 7836 (22%), zero 8041 (22%)
c [score-dist-13] max exp 898, different 665 (74%)
c [score-dist-13] median active exp 757, avg 657.4
c [simplification-13] removed 2081 variables 5.4% (36323 remain 17%)
c [simplification-13] removed 19821 irredundant clauses 7.7% (238077 remain 20%)
c [simplification-13] maximum reduction of 8% = max (5%, 8%)
c [simplification-13] large reduction 8% >= 5% limit
c [simplification-13] next conflict interval 2000 = 2000/1
c [simplification-13] penalized conflict interval 2000 = 1 * 2000
c [simplification-13] hard conflict limit 47640 (soft 37640 + delta 10000)
c [simplification-13] new conflict limit 37640 (hard 47640)
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   72.8   36322   238077     35885    6325   2865 127393   24   175   29  14%      4  111   15    8  176%
c i   73.0   36321   238077     36317    6711   2877 127415   23   174   29  13%      3  110   14    8  172%
c i   73.0   36320   238077     36367    6756   2879 127416   22   173   29  13%      3  109   14    8  164%
c i   73.2   36319   238077     36725    7065   2890 127442   22   171   29  13%      3  107   16    8  189%
c i   73.2   36318   238077     36755    7087   2895 127444   22   171   29  13%      3  106   15    8  174%
c i   73.5   36317   238077     37178    7458   2915 127460   22   170   29  13%      3  105   19    9  220%
c i   73.6   36315   238077     37479    7721   2932 127472   21   167   29  13%      2  101   15    9  173%
c i   73.7   36313   238077     37608    7835   2938 127478   21   166   29  13%      2  100   15    9  175%
c i   73.7   36311   238077     37609    7835   2938 127478   21   166   29  13%      2  100   15    9  174%
c i   73.7   36308   238077     37610    7835   2938 127478   21   166   29  13%      2  100   15    9  174%
c i   73.7   36305   238077     37611    7835   2938 127478   21   166   29  13%      2  100   15    9  173%
c 
c [simplification-14] limit 37670 conflicts (hard 47640) hit after 37670 conflicts
c [quatres-10] found 22014 quaternary clauses 67% in total
c [quatres-10-1] removed 1 duplicate quaternary clauses
c [quatres-10-2] added 2 single-self-subsuming ternary resolvents
c [quatres-10-2] added 17 quaternary resolvents
c [ternres-10] limit 8502180 with penalty 0 = 0 + 0
c [ternres-10] all 36303 free variables schedulable
c [ternres-10] 919 ternary resolvents (0 bin, 919 trn)
c [ternres-10] fully completed ternary resolution
c [decomp-33] removed 28 variables
c [treelook-5] limit 850218 penalty 0 = 0 + 0 boost 1
c [treelook-5] scheduled 56760 literals 78%
c [treelook-5] scheduling used 850220 steps
c [treelook-5] not fully scheduled
c [treelook-5] limit 850218 penalty 0 = 0 + 0 boost 1
c [treelook-5] used 893532 steps
c [treelook-5] 56657 literals remain 78%
c [treelook-5] 13040 variables remain to probed next time 36%
c [decomp-34] removed 2 variables
c [treelook-5] removed 23 variables, found 6423 hbrs
c [unhide-14] limit 1700436 with penalty 0 = 0 + 0
c [unhide-14-16] 8 units, 230 failed, 10648 tauts, 0 hbrs, 7078 literals
c [transred-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 413 transitive binary clauses
c [cce-6] limit of 42510900 steps penalty 0 = 0 + 0
c [cce-6-1] eliminated 2 clauses out of 4 (50%) of length 15
c [cce-6-1] eliminated 1 clauses out of 5 (20%) of length 14
c [cce-6-1] eliminated 2 clauses out of 6 (33%) of length 13
c [cce-6-1] eliminated 1 clauses out of 3 (33%) of length 12
c [cce-6-1] eliminated 2 clauses out of 5 (40%) of length 11
c [cce-6-1] eliminated 1 clauses out of 5 (20%) of length 10
c [cce-6-1] eliminated 2 clauses out of 7 (29%) of length 9
c [cce-6-1] eliminated 1 clauses out of 6 (17%) of length 8
c [cce-6-1] eliminated 2 clauses out of 16 (12%) of length 7
c [cce-6-1] eliminated 10 clauses out of 974 (1%) of length 6
c [cce-6-1] eliminated 46 clauses out of 7043 (1%) of length 5
c [cce-6-1] incomplete large round (ATE)
c [cce-6-1] eliminated 70 large clauses in 42510900 steps
c [cce-6-1] allowing another 21255450 steps for small clauses
c [cce-6-1] scheduling 186448 clauses = 115794 binary + 70654 ternary
c [cce-6-1] tried to eliminate 1602 small clauses 1%
c [cce-6-1] eliminated 298 binary clauses 0%
c [cce-6-1] eliminated 90 ternary clauses 0%
c [cce-6-1] eliminated 388 small clauses 0%
c [cce-6-1] eliminated 516 small clauses in 42510908 steps
c [cce-6-1] incomplete small round (ATE)
c [cce-6-1] eliminated 586 covered clauses in round 1
c [cce-6] eliminated 586 covered clauses in TOTAL during 1 rounds
c [cce-6] 586 < 1/100 * 234014 = 2340 considered unsuccessful
c [elim-12] no untried remaining variables left
c [elim-12] scheduled 36164 variables 100%
c [elim-12] limit of 170043601 steps penalty 0 = 0 + 0
c [elim-12] rescheduling of touched variables disabled
c [elim-12-1] eliminated 373 variables 1% in round 1 in 19589770 steps
c [elim-12-1] backward subsumption/strengthening limit 19589700
c [elim-12-1-1] backward checking 2483 touched variables 7%
c [elim-12-1-1] fully completed backward checking in 1 rounds
c [elim-12-1] subsumed 13 and strengthened 52 clauses in 650561 steps
c [elim-12-1] rescheduled 156 variables 0% by backward subsumption
c [elim-12-2] eliminated 9 variables 0% in round 2 in 1249469 steps
c [elim-12-2] backward subsumption/strengthening limit 1249400
c [elim-12-2-1] backward checking 102 touched variables 0%
c [elim-12-2-1] fully completed backward checking in 1 rounds
c [elim-12-2] subsumed 4 and strengthened 3 clauses in 104708 steps
c [elim-12-2] rescheduled 17 variables 0% by backward subsumption
c [elim-12-3] no variable eliminated in round 3 in 10117 steps
c [elim-12] fully completed in 3 rounds
c [elim-12] transition to [ all 0 rem 0 ] state
c [elim-12] eliminated 387 = 1% variables out of 36164 scheduled
c [bca-10] limit of 10000000 steps and 465963 added (scaled 2)
c [bca-10] 56991 out of 71556 literals actually usable 80%
c [bca-10] added 47 blocked clauses in 138446 steps
c [sweep-10] limit 2550654 penalty 0 = 0 + 0
c [sweep-10-1] 3255 pos 9.9% + 29465 neg 90.1% = 32720 sched 91.5% ret 3057
c [sweep-10-1] 2783355 steps 64 queries 2954.19 avg class size
c [sweep-10-1] 1165 decisions 56 SAT calls 134.48 avg env size
c [sweep-10-1] 32157 variables remain 90% (3606 retained 10%)
c [decomp-35] removed 52 variables
c [sweep-10-1] removed 52 vars (0 failed, 10 eqs, 13 impls)
c [sweep-10] removed 52 vars in TOTAL (1 rounds, 63 queries)
c [phase-count-14] 231504 negative 99.7% of 232256 except 752 0.3%
c [phase-count-14] 168430 positive 72.5% of 232256 except 63826 27.5%
c [phase-count-14] skipping relative phase luck test
c [phase-14] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-14] sorted 15433 enqueued variables after 37670 conflicts
c [score-dist-14] active 20292 (57%), one 7912 (22%), zero 7521 (21%)
c [score-dist-14] max exp 941, different 719 (76%)
c [score-dist-14] median active exp 812, avg 709.1
c [simplification-14] removed 578 variables 1.6% (35725 remain 17%)
c [simplification-14] removed 5821 irredundant clauses 2.4% (232256 remain 20%)
c [simplification-14] maximum reduction of 2% = max (2%, 2%)
c [simplification-14] geometric conflict interval increment 6666 = 20000 / 3
c [simplification-14] new conflict interval 18666
c [simplification-14] penalized conflict interval 18666 = 1 * 18666
c [simplification-14] hard conflict limit 66336 (soft 56336 + delta 10000)
c [simplification-14] new conflict limit 56336 (hard 66336)
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.2   35724   232256     37764    7834   3623 125008   21   167   30  13%      2  101   21    9  241%
c i   77.3   35723   232256     37998    8042   3633 125013   21   168   30  13%      2  101   21    9  247%
c i   77.6   35721   232256     38472    8447   3654 125040   21   168   30  12%      2  100   18    9  204%
c i   77.8   35719   232256     38829    8753   3675 125055   21   163   30  13%      2   95   24    9  268%
c i   78.4   35717   232256     39817    9613   3724 125087   21   165   30  13%      6   95   20    9  223%
c i   78.5   35716   232256     40139    9891   3742 125107   21   164   30  13%      5   94   21    9  236%
c i   78.6   35715   232256     40277   10010   3748 125111   21   165   30  13%      4   95   24    9  266%
c i   78.8   35713   232256     40607   10301   3763 125126   21   161   30  13%      3   90   17    9  187%
c i   78.8   35712   232256     40672   10355   3770 125129   20   159   30  13%      3   89   16    9  172%
c i   78.8   35710   232256     40682   10363   3771 125129   20   159   30  13%      3   89   15    9  167%
c i   78.9   35707   232256     40889   10549   3775 125140   20   160   30  13%      3   89   17    9  183%
c i   79.4   35676   232256     41727   11283   3807 125171   21   156   31  14%      5   84   28    9  296%
c i   80.0   35674   232256     42622   12090   3833 125197   23   153   31  15%      6   80   32   10  330%
c i   80.1   35670   232256     42874   12310   3841 125212   24   154   31  15%      5   81   29   10  301%
c i   80.2   35623   232256     42928   12356   3843 125217   23   153   31  15%      5   80   26   10  268%
c i   80.4   35622   232256     43320   12715   3852 125227   23   150   32  16%      4   76   22   10  221%
c i   80.4   35621   232256     43323   12716   3852 125228   23   150   32  16%      4   76   21   10  219%
c i   80.4   35620   232256     43329   12717   3853 125231   23   150   32  16%      4   76   21   10  214%
c i   81.4   35618   232256     44745   13974   3895 125277   23   145   32  16%     10   69   25   10  251%
c i   81.4   35617   232256     44749   13976   3896 125277   23   145   32  16%     10   69   25   10  250%
c i   81.7   35616   232256     45227   14409   3910 125290   25   145   32  17%      7   69   34   10  327%
c i   81.8   35615   232256     45276   14445   3913 125299   25   145   32  17%      7   69   29   10  287%
c i   81.8   35608   232256     45279   14445   3914 125299   25   145   32  17%      7   68   29   10  286%
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   81.9   35606   232256     45425   14576   3918 125303   24   143   32  17%      6   67   23   10  225%
c i   82.2   35605   232256     45976   15060   3940 125323   24   140   32  17%      5   63   19   10  186%
c i   82.8   35603   232256     46877   15878   3964 125356   24   137   33  18%      6   59   23   11  215%
c i   83.1   35600   232256     47299   16255   3977 125369   25   136   33  18%      5   58   27   11  254%
c i   83.4   35598   232256     47647   16575   3981 125382   26   138   33  19%      4   60   29   11  265%
c i   83.8   35597   232256     48198   17081   3988 125394   26   140   34  19%      3   61   33   11  297%
c i   84.1   35594   232256     48600   17435   3996 125405   26   138   35  19%      3   58   26   11  235%
c i   84.1   35593   232256     48607   17438   3999 125405   26   137   35  19%      3   58   25   11  230%
c i   84.5   35590   232256     49089   17884   4005 125413   29   142   35  20%      3   63   56   11  494%
c i   84.9   35589   232256     49611   18366   4012 125416   29   141   36  20%      3   61   28   12  248%
c i   85.3   35588   232256     50139   18854   4020 125432   29   142   36  21%      3   61   31   12  264%
c i   85.7   35587   232256     50735   19405   4026 125448   29   138   37  21%      3   56   22   12  191%
c i   88.7   35586   232256     55308   23637   4095 125503   28   116   38  24%     53   32   26   13  202%
c i   88.9   35579   232256     55574   23891   4095 125505   29   115   38  25%     40   31   39   13  296%
c i   89.1   35577   232256     55765   24068   4102 125507   29   113   38  25%     33   28   25   13  193%
c i   89.4   35575   232256     56164   24436   4108 125511   29   112   39  26%     22   28   33   13  251%
c 
c [simplification-15] limit 56347 conflicts (hard 66336) hit after 56348 conflicts
c [quatres-11] found 21771 quaternary clauses 63% in total
c [quatres-11-2] added 3 single-self-subsuming ternary resolvents
c [quatres-11-2] added 10 quaternary resolvents
c [ternres-11] limit 12193912 with penalty 0 = 0 + 0
c [ternres-11] all 35574 free variables schedulable
c [ternres-11] 361 ternary resolvents (1 bin, 360 trn)
c [ternres-11] fully completed ternary resolution
c [card-5] limit 381059 penalty 4 = 4 + 0
c [card-5] found 1287 at-most-one constraints of average size 4.1
c [card-5] no at-most-two constraint found
c [card-5] using previous limit 381059 for elimination
c [card-5] 1287 out of 1287 constraints (100%) meet size limits
c [card-5] no units found
c [card-5] no at-most-one constraints generated
c [gauss-5] limit 304847 penalty 3 = 3 + 0
c [gauss-5] extracted 31 xors of average arity 2.5
c [gauss-5] connected 78 occurrences of 69 variables (average 1.1)
c [gauss-5] limit 304847 penalty 3 = 3 + 0
c [gauss-5] fully completed
c [gauss-5] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-36] removed 56 variables
c [basicprobe-5] limit 60969561 penalty 0 = 0 + 0
c [basicprobe-5-0] 7954 probes remain 23% after last round
c [basicprobe-5-0] 534 units = 528 failed (99%) + 6 lifted (1%)
c [basicprobe-5-0] removed 722 variables, found 110615 hbrs
c [bate-4] eliminated 886 asymmetric tautologies during probing
c [unhide-15] limit 2438782 with penalty 0 = 0 + 0
c [unhide-15-18] 6 units, 214 failed, 25807 tauts, 0 hbrs, 75579 literals
c [transred-11] limit 2000000 with penalty 0 = 0 + 0
c [transred-11] removed 400 transitive binary clauses
c [transred-11] found 2 units
c [block-5] scheduling all variables this time
c [block-5] scheduled 34523 variables 100%
c [block-5] limit of 15242390 steps penalty 3 = 3 + 0
c [block-5] fully completed
c [block-5] transition to [ all 0 rem 0 ] state
c [block-5] eliminated 229 blocked clauses
c [block-5] 229 < 1/100 * 219363 = 2193 considered unsuccessful
c [elim-13] scheduling all variables this time
c [elim-13] scheduled 34518 variables 100%
c [elim-13] almost no limit of 100000000000 steps
c [elim-13] rescheduling of touched variables disabled
c [elim-13-1] eliminated 891 variables 3% in round 1 in 17747548 steps
c [elim-13-1] backward subsumption/strengthening limit 17747500
c [elim-13-1-1] backward checking 5187 touched variables 15%
c [elim-13-1-1] fully completed backward checking in 1 rounds
c [elim-13-1] subsumed 25 and strengthened 84 clauses in 1187736 steps
c [elim-13-1] rescheduled 304 variables 1% by backward subsumption
c [elim-13-2] eliminated 18 variables 0% in round 2 in 1061911 steps
c [elim-13-2] backward subsumption/strengthening limit 1061900
c [elim-13-2-1] backward checking 388 touched variables 1%
c [elim-13-2-1] fully completed backward checking in 1 rounds
c [elim-13-2] subsumed 2 and strengthened 10 clauses in 204584 steps
c [elim-13-2] rescheduled 38 variables 0% by backward subsumption
c [elim-13-3] no variable eliminated in round 3 in 14998 steps
c [elim-13] fully completed in 3 rounds
c [elim-13] transition to [ all 0 rem 0 ] state
c [elim-13] eliminated 909 = 3% variables out of 34518 scheduled
c [bca-11] limit of 10000000 steps and 432348 added (scaled 2)
c [bca-11] 48681 out of 67220 literals actually usable 72%
c [bca-11] added 56 blocked clauses in 133088 steps
c [sweep-11] boosting sweeping limit by 10
c [sweep-11] limit 36581730 penalty 0 = 0 + 0
c [sweep-11-1] 2916 pos 9.6% + 27465 neg 90.4% = 30381 sched 90.4% ret 3228
c [sweep-11-1] 36582551 steps 980 queries 247.94 avg class size
c [sweep-11-1] 11212 decisions 885 SAT calls 85.97 avg env size
c [sweep-11-1] 17305 variables remain 52% (16012 retained 48%)
c [decomp-37] removed 518 variables
c [sweep-11-1] removed 518 vars (0 failed, 127 eqs, 203 impls)
c [sweep-11] removed 518 vars in TOTAL (1 rounds, 979 queries)
c [phase-count-15] 211419 negative 99.6% of 212179 except 760 0.4%
c [phase-count-15] 150875 positive 71.1% of 212179 except 61304 28.9%
c [phase-count-15] skipping relative phase luck test
c [phase-15] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-15] sorted 14764 enqueued variables after 56348 conflicts
c [score-dist-15] active 18327 (55%), one 9594 (29%), zero 5170 (16%)
c [score-dist-15] max exp 509, different 410 (80%)
c [score-dist-15] median active exp 393, avg 374.7
c [simplification-15] removed 2483 variables 7.0% (33091 remain 16%)
c [simplification-15] removed 20077 irredundant clauses 8.6% (212179 remain 18%)
c [simplification-15] maximum reduction of 9% = max (7%, 9%)
c [simplification-15] large reduction 9% >= 5% limit
c [simplification-15] next conflict interval 2000 = 2000/1
c [simplification-15] penalized conflict interval 2000 = 1 * 2000
c [simplification-15] hard conflict limit 68348 (soft 58348 + delta 10000)
c [simplification-15] new conflict limit 58348 (hard 68348)
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   96.9   33090   212179     57193   24272   4109 204632   28   114   43  25%     11   29   26   13  197%
c 
c [simplification-16] limit 58348 conflicts (hard 68348) hit after 58348 conflicts
c [quatres-12] found 19966 quaternary clauses 60% in total
c [quatres-12-1] removed 2 duplicate quaternary clauses
c [quatres-12-2] added 5 single-self-subsuming ternary resolvents
c [quatres-12-2] added 15 quaternary resolvents
c [ternres-12] limit 12541304 with penalty 0 = 0 + 0
c [ternres-12] all 33090 free variables schedulable
c [ternres-12] 757 ternary resolvents (1 bin, 756 trn)
c [ternres-12] fully completed ternary resolution
c [decomp-38] removed 5 variables
c [simpleprobe-6] all 33086 free variables schedulable
c [simpleprobe-6] limit 50165216 penalty 0 = 0 + 0
c [decomp-39] removed 523 variables
c [simpleprobe-6] fully completed simple probing
c [simpleprobe-6] removed 523 variables, found 37123 hbrs, 262 units
c [unhide-16] limit 2508260 with penalty 0 = 0 + 0
c [unhide-16-20] 5 units, 167 failed, 31038 tauts, 0 hbrs, 37499 literals
c [transred-12] limit 2000000 with penalty 0 = 0 + 0
c [transred-12] removed 636 transitive binary clauses
c [transred-12] found 5 units
c [cce-7] limit of 31353260 steps penalty 1 = 1 + 0
c [cce-7-1] eliminated 2 clauses out of 5 (40%) of length 10
c [cce-7-1] eliminated 4 clauses out of 8 (50%) of length 8
c [cce-7-1] eliminated 1 clauses out of 15 (7%) of length 7
c [cce-7-1] eliminated 3 clauses out of 905 (0%) of length 6
c [cce-7-1] eliminated 5 clauses out of 6811 (0%) of length 5
c [cce-7-1] incomplete large round (ACCE)
c [cce-7-1] eliminated 15 large clauses in 31353281 steps
c [cce-7-1] allowing another 15676640 steps for small clauses
c [cce-7-1] scheduling 123587 clauses = 106844 binary + 16743 ternary
c [cce-7-1] tried to eliminate 2330 small clauses 2%
c [cce-7-1] eliminated 576 binary clauses 1%
c [cce-7-1] eliminated 151 ternary clauses 1%
c [cce-7-1] eliminated 727 small clauses 1%
c [cce-7-1] eliminated 787 small clauses in 31353261 steps
c [cce-7-1] incomplete small round (ACCE)
c [cce-7-1] eliminated 802 covered clauses in round 1
c [cce-7] eliminated 802 covered clauses in TOTAL during 1 rounds
c [cce-7] 802 < 1/100 * 203361 = 2033 considered unsuccessful
c [elim-14] scheduling all variables this time
c [elim-14] scheduled 32483 variables 100%
c [elim-14] limit of 250826081 steps penalty 0 = 0 + 0
c [elim-14] rescheduling of touched variables disabled
c [elim-14-1] eliminated 470 variables 1% in round 1 in 16290755 steps
c [elim-14-1] backward subsumption/strengthening limit 16290700
c [elim-14-1-1] backward checking 2979 touched variables 9%
c [elim-14-1-1] fully completed backward checking in 1 rounds
c [elim-14-1] subsumed 15 and strengthened 53 clauses in 625422 steps
c [elim-14-1] rescheduled 175 variables 1% by backward subsumption
c [elim-14-2] eliminated 9 variables 0% in round 2 in 118195 steps
c [elim-14-2] backward subsumption/strengthening limit 118100
c [elim-14-2-1] backward checking 116 touched variables 0%
c [elim-14-2-1] fully completed backward checking in 1 rounds
c [elim-14-2] subsumed 1 and strengthened 2 clauses in 62576 steps
c [elim-14-2] rescheduled 12 variables 0% by backward subsumption
c [elim-14-3] no variable eliminated in round 3 in 5696 steps
c [elim-14] fully completed in 3 rounds
c [elim-14] transition to [ all 0 rem 0 ] state
c [elim-14] eliminated 480 = 1% variables out of 32483 scheduled
c [bca-12] limit of 10000000 steps and 404466 added (scaled 2)
c [bca-12] 45036 out of 64008 literals actually usable 70%
c [bca-12] added 44 blocked clauses in 125754 steps
c [sweep-12] limit 3762391 penalty 0 = 0 + 0
c [sweep-12-1] 1760 pos 10.5% + 15041 neg 89.5% = 16801 sched 52.5% ret 15202
c [sweep-12-1] 3781303 steps 96 queries 1243.36 avg class size
c [sweep-12-1] 1477 decisions 88 SAT calls 133.41 avg env size
c [sweep-12-1] 16349 variables remain 51% (15620 retained 49%)
c [decomp-40] removed 50 variables
c [sweep-12-1] removed 50 vars (0 failed, 11 eqs, 10 impls)
c [sweep-12] removed 50 vars in TOTAL (1 rounds, 95 queries)
c [phase-count-16] 200544 negative 99.6% of 201296 except 752 0.4%
c [phase-count-16] 141399 positive 70.2% of 201296 except 59897 29.8%
c [phase-count-16] skipping relative phase luck test
c [phase-16] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-16] sorted 17527 enqueued variables after 58348 conflicts
c [score-dist-16] active 14426 (45%), one 13006 (41%), zero 4521 (14%)
c [score-dist-16] max exp 553, different 416 (75%)
c [score-dist-16] median active exp 504, avg 416.2
c [simplification-16] removed 1137 variables 3.4% (31953 remain 15%)
c [simplification-16] removed 10883 irredundant clauses 5.1% (201296 remain 17%)
c [simplification-16] maximum reduction of 5% = max (3%, 5%)
c [simplification-16] large reduction 5% >= 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 70348 (soft 60348 + delta 10000)
c [simplification-16] new conflict limit 60348 (hard 70348)
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  103.3   31952   201296     60823   26720   4561 201206   22    79   42  28%     37   -7   13   14   96%
c i  106.1   31951   201296     66476   31853   4586 201219   13    32   43  41%     65  -51    7   13   54%
c i  107.4   31950   201296     69114   34127   4602 201224   11    27   44  42%     23  -54    7   13   51%
c i  108.2   31840   201296     70106   35060   4606 201229   15    41   44  38%      9  -40   30   14  222%
c 
c [simplification-17] limit 60348 conflicts (hard 70348) hit after 70349 conflicts
c [quatres-13] found 19233 quaternary clauses 59% in total
c [quatres-13-2] added 3 single-self-subsuming ternary resolvents
c [quatres-13-2] added 10 quaternary resolvents
c [ternres-13] limit 14301056 with penalty 0 = 0 + 0
c [ternres-13] all 31838 free variables schedulable
c [ternres-13] 342 ternary resolvents (0 bin, 342 trn)
c [ternres-13] fully completed ternary resolution
c [decomp-41] removed 124 variables
c [treelook-6] limit 1430105 penalty 0 = 0 + 0 boost 1
c [treelook-6] scheduled 50258 literals 79%
c [treelook-6] scheduling used 910765 steps
c [treelook-6] scheduled completely
c [treelook-6] limit 1430105 penalty 0 = 0 + 0 boost 1
c [treelook-6] used 1486716 steps
c [treelook-6] 50208 literals remain 79%
c [treelook-6] 10400 variables remain to probed next time 33%
c [treelook-6] removed 1 variables, found 11423 hbrs
c [unhide-17] limit 2860211 with penalty 0 = 0 + 0
c [unhide-17-22] 6 units, 87 failed, 15721 tauts, 0 hbrs, 43224 literals
c [transred-13] limit 2000000 with penalty 0 = 0 + 0
c [transred-13] removed 575 transitive binary clauses
c [transred-13] found 4 units
c [elim-15] scheduling all variables this time
c [elim-15] scheduled 31716 variables 100%
c [elim-15] limit of 286021131 steps penalty 0 = 0 + 0
c [elim-15] rescheduling of touched variables disabled
c [elim-15-1] eliminated 201 variables 1% in round 1 in 15710181 steps
c [elim-15-1] backward subsumption/strengthening limit 15710100
c [elim-15-1-1] backward checking 1412 touched variables 4%
c [elim-15-1-1] fully completed backward checking in 1 rounds
c [elim-15-1] subsumed 9 and strengthened 23 clauses in 339606 steps
c [elim-15-1] rescheduled 84 variables 0% by backward subsumption
c [elim-15-2] eliminated 2 variables 0% in round 2 in 38437 steps
c [elim-15-2] backward subsumption/strengthening limit 38400
c [elim-15-2-1] backward checking 47 touched variables 0%
c [elim-15-2-1] incomplete backward checking 0 remain 0%
c [elim-15-2] subsumed 4 and strengthened 2 clauses in 38401 steps
c [elim-15-2] rescheduled 8 variables 0% by backward subsumption
c [elim-15-3] eliminated 1 variables 0% in round 3 in 7276 steps
c [elim-15-3] backward subsumption/strengthening limit 7200
c [elim-15-3-1] backward checking 9 touched variables 0%
c [elim-15-3-1] incomplete backward checking 0 remain 0%
c [elim-15-3] subsumed 4 and strengthened 1 clauses in 7201 steps
c [elim-15] incomplete 8 not tried 0% in round 3
c [elim-15] transition to [ all 1 rem 1 ] state
c [elim-15] eliminated 206 = 1% variables out of 31716 scheduled
c [elim-15] 206 < 1/100 * 31716 = 317 considered unsuccessful
c [bca-13] limit of 10000000 steps and 395404 added (scaled 2)
c [bca-13] 43926 out of 63022 literals actually usable 70%
c [bca-13] added 28 blocked clauses in 125854 steps
c [sweep-13] limit 4290316 penalty 0 = 0 + 0
c [sweep-13-1] 1890 pos 11.7% + 14211 neg 88.3% = 16101 sched 51.1% ret 15409
c [sweep-13-1] 4329388 steps 143 queries 1005.11 avg class size
c [sweep-13-1] 2234 decisions 122 SAT calls 106.59 avg env size
c [sweep-13-1] 15459 variables remain 49% (16051 retained 51%)
c [decomp-43] removed 99 variables
c [sweep-13-1] removed 99 vars (0 failed, 23 eqs, 30 impls)
c [sweep-13] removed 99 vars in TOTAL (1 rounds, 142 queries)
c [phase-count-17] 196287 negative 99.6% of 197026 except 739 0.4%
c [phase-count-17] 137650 positive 69.9% of 197026 except 59376 30.1%
c [phase-count-17] skipping relative phase luck test
c [phase-17] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-17] sorted 17972 enqueued variables after 70349 conflicts
c [score-dist-17] active 13439 (43%), one 13679 (44%), zero 4293 (14%)
c [score-dist-17] max exp 727, different 348 (48%)
c [score-dist-17] median active exp 687, avg 632.2
c [simplification-17] removed 427 variables 1.3% (31411 remain 15%)
c [simplification-17] removed 4270 irredundant clauses 2.1% (197026 remain 17%)
c [simplification-17] maximum reduction of 2% = max (1%, 2%)
c [simplification-17] geometric conflict interval increment 6666 = 20000 / 3
c [simplification-17] new conflict interval 25332
c [simplification-17] penalized conflict interval 25332 = 1 * 25332
c [simplification-17] hard conflict limit 108347 (soft 95681 + delta 12666)
c [simplification-17] new conflict limit 95681 (hard 108347)
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  112.0   31410   197026     71105   27821   4676 195845   18    52   44  35%      3  -28   30   14  215%
c i  112.2   31407   197026     71348   28050   4681 195845   19    54   44  34%      1  -26   24   14  173%
c i  112.7   31405   197026     71954   28630   4690 195850   19    59   44  33%     -1  -21   25   14  177%
c i  112.7   31404   197026     71955   28630   4690 195850   19    59   44  33%     -1  -21   25   14  176%
c i  115.3   31310   197026     75823   32236   4720 195869   19    55   44  34%     35  -24   10   14   73%
c i  115.6   31273   197026     76441   32834   4721 195869   18    52   44  35%     17  -26   13   14   88%
c i  116.5   31271   197026     78268   34515   4738 195881   18    50   44  36%     10  -28   27   14  185%
c i  117.4   31270   197026     79405   35577   4753 195887   19    53   44  35%      3  -24   18   14  124%
c i  119.3   31269   197026     82085   38136   4764 195901   18    51   44  36%     18  -25   21   15  146%
c i  119.9   31268   197026     83006   38955   4770 195906   17    46   44  37%      6  -30   11   15   73%
c i  120.9   31266   197026     84746   40633   4778 195917   16    46   44  35%      6  -29   18   15  126%
c i  121.9   31265   197026     86726   42525   4785 195923   15    40   47  38%      9  -34   12   15   83%
c i  122.3   31262   197026     87379   43124   4785 195924   15    37   47  40%      2  -37   13   15   92%
c i  125.3   31259   197026     93832   48906   4828 195944    9    19   52  48%     71  -50    5   14   36%
c i  125.9   31238   197026     94571   49588   4829 195946   10    20   52  50%     31  -49   12   14   85%
c i  126.4   31237   197026     95532   50432   4833 195947   11    22   52  49%      8  -47   15   14  108%
c i  128.4   31234   197026     98397   53093   4860 195971   13    30   52  43%     17  -37   12   14   88%
c -  133.8   31234   197026    107627   27821   4883 195987   11    21   34  53%    107  -40    9   14   64%
c 
c [simplification-18] limit 95691 conflicts (hard 108347) hit after 108347 conflicts
c [quatres-14] found 18903 quaternary clauses 54% in total
c [quatres-14-1] removed 1 duplicate quaternary clauses
c [quatres-14-2] added 1 single-self-subsuming ternary resolvents
c [quatres-14-2] added 5 quaternary resolvents
c [ternres-14] limit 20718517 with penalty 0 = 0 + 0
c [ternres-14] all 31234 free variables schedulable
c [ternres-14] 270 ternary resolvents (1 bin, 269 trn)
c [ternres-14] fully completed ternary resolution
c [decomp-44] removed 224 variables
c [basicprobe-6] limit 103592585 penalty 0 = 0 + 0
c [basicprobe-6-0] 7258 sched 24%, 738 failed, 26 lifted, 130519 hbrs
c [decomp-45] removed 1253 variables
c [basicprobe-6-1] 8915 probes remain 30% after last round
c [basicprobe-6-1] 822 units = 795 failed (97%) + 27 lifted (3%)
c [basicprobe-6-1] removed 1367 variables, found 141312 hbrs
c [bate-5] eliminated 697 asymmetric tautologies during probing
c [unhide-18] limit 4143703 with penalty 0 = 0 + 0
c [unhide-18-25] 1 units, 69 failed, 44762 tauts, 0 hbrs, 33525 literals
c [transred-14] limit 2000000 with penalty 0 = 0 + 0
c [transred-14] removed 457 transitive binary clauses
c [bca-14] limit of 10000000 steps and 356656 added (scaled 2)
c [bca-14] 41590 out of 59476 literals actually usable 70%
c [bca-14] added 22 blocked clauses in 118570 steps
c [sweep-14] limit 6215555 penalty 0 = 0 + 0
c [sweep-14-1] 1572 pos 10.6% + 13219 neg 89.4% = 14791 sched 49.7% ret 14946
c [sweep-14-1] 6369259 steps 166 queries 550.14 avg class size
c [sweep-14-1] 2104 decisions 153 SAT calls 96.39 avg env size
c [sweep-14-1] 13864 variables remain 47% (15821 retained 53%)
c [decomp-46] removed 81 variables
c [sweep-14-1] removed 81 vars (0 failed, 13 eqs, 24 impls)
c [sweep-14] removed 81 vars in TOTAL (1 rounds, 165 queries)
c [phase-count-18] 176701 negative 99.6% of 177391 except 690 0.4%
c [phase-count-18] 120908 positive 68.2% of 177391 except 56483 31.8%
c [phase-count-18] skipping relative phase luck test
c [phase-18] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-18] sorted 18986 enqueued variables after 108347 conflicts
c [score-dist-18] active 10670 (36%), one 15679 (53%), zero 3307 (11%)
c [score-dist-18] max exp 761, different 298 (39%)
c [score-dist-18] median active exp 711, avg 648.6
c [simplification-18] removed 1578 variables 5.1% (29656 remain 14%)
c [simplification-18] removed 19635 irredundant clauses 10.0% (177391 remain 15%)
c [simplification-18] maximum reduction of 10% = max (5%, 10%)
c [simplification-18] large reduction 10% >= 5% limit
c [simplification-18] next conflict interval 2000 = 2000/1
c [simplification-18] penalized conflict interval 2000 = 1 * 2000
c [simplification-18] hard conflict limit 120347 (soft 110347 + delta 10000)
c [simplification-18] new conflict limit 110347 (hard 120347)
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  142.7   29655   177391    114938   32955   5051 271512   12    23   39  54%    204  -34   15   14  107%
c 
c [simplification-19] limit 110347 conflicts (hard 120347) hit after 120348 conflicts
c [quatres-15] found 17080 quaternary clauses 50% in total
c [quatres-15-1] removed 6 duplicate quaternary clauses
c [quatres-15-2] added 1 quaternary resolvents
c [ternres-15] limit 22302253 with penalty 0 = 0 + 0
c [ternres-15] all 29630 free variables schedulable
c [ternres-15] 335 ternary resolvents (0 bin, 335 trn)
c [ternres-15] fully completed ternary resolution
c [decomp-47] removed 26 variables
c [simpleprobe-7] all 29630 free variables schedulable
c [simpleprobe-7] limit 89209012 penalty 0 = 0 + 0
c [decomp-48] removed 186 variables
c [simpleprobe-7] fully completed simple probing
c [simpleprobe-7] removed 186 variables, found 54243 hbrs, 86 units
c [unhide-19] limit 4460450 with penalty 0 = 0 + 0
c [unhide-19-28] 1 units, 253 failed, 44138 tauts, 0 hbrs, 29940 literals
c [transred-15] limit 2000000 with penalty 0 = 0 + 0
c [transred-15] removed 741 transitive binary clauses
c [transred-15] found 3 units
c [cce-8] boosting limit by 10
c [cce-8] limit of 278778162 steps penalty 2 = 2 + 0
c [cce-8-1] eliminated 1 clauses out of 4 (25%) of length 16
c [cce-8-1] eliminated 1 clauses out of 1 (100%) of length 12
c [cce-8-1] eliminated 1 clauses out of 4 (25%) of length 9
c [cce-8-1] eliminated 2 clauses out of 9 (22%) of length 8
c [cce-8-1] eliminated 1 clauses out of 20 (5%) of length 7
c [cce-8-1] eliminated 6 clauses out of 865 (1%) of length 6
c [cce-8-1] eliminated 257 clauses out of 6340 (4%) of length 5
c [cce-8-1] eliminated 4475 clauses out of 15191 (29%) of length 4
c [cce-8-1] completed large round (ATE)
c [cce-8-1] eliminated 4744 large clauses in 123837809 steps
c [cce-8-1] allowing another 61918904 steps for small clauses
c [cce-8-1] scheduling 135181 clauses = 97221 binary + 37960 ternary
c [cce-8-1] tried to eliminate 34772 small clauses 26%
c [cce-8-1] eliminated 5513 binary clauses 6%
c [cce-8-1] eliminated 1138 ternary clauses 3%
c [cce-8-1] eliminated 6651 small clauses 5%
c [cce-8-1] eliminated 6793 small clauses in 278778166 steps
c [cce-8-1] incomplete small round (ATE)
c [cce-8-1] eliminated 11537 covered clauses in round 1
c [cce-8] eliminated 11537 covered clauses in TOTAL during 1 rounds
c [elim-16] no untried remaining variables left
c [elim-16] scheduled 29364 variables 100%
c [elim-16] limit of 223022530 steps penalty 1 = 1 + 0
c [elim-16] rescheduling of touched variables disabled
c [elim-16-1] eliminated 1662 variables 6% in round 1 in 11599414 steps
c [elim-16-1] backward subsumption/strengthening limit 11599400
c [elim-16-1-1] backward checking 8294 touched variables 28%
c [elim-16-1-1] fully completed backward checking in 1 rounds
c [elim-16-1] subsumed 25 and strengthened 192 clauses in 1294084 steps
c [elim-16-1] rescheduled 508 variables 2% by backward subsumption
c [elim-16-2] eliminated 48 variables 0% in round 2 in 217751 steps
c [elim-16-2] backward subsumption/strengthening limit 217700
c [elim-16-2-1] backward checking 428 touched variables 1%
c [elim-16-2-1] fully completed backward checking in 1 rounds
c [elim-16-2] subsumed 18 and strengthened 15 clauses in 138553 steps
c [elim-16-2] rescheduled 73 variables 0% by backward subsumption
c [elim-16-3] eliminated 11 variables 0% in round 3 in 71586 steps
c [elim-16-3] backward subsumption/strengthening limit 71500
c [elim-16-3-1] backward checking 107 touched variables 0%
c [elim-16-3-1] fully completed backward checking in 1 rounds
c [elim-16-3] subsumed 9 and strengthened 3 clauses in 61443 steps
c [elim-16] incomplete 28 not tried 0% in round 3
c [elim-16] transition to [ all 1 rem 1 ] state
c [elim-16] eliminated 1721 = 6% variables out of 29364 scheduled
c [bca-15] limit of 10000000 steps and 318765 added (scaled 2)
c [bca-15] 38579 out of 55288 literals actually usable 70%
c [bca-15] added 37 blocked clauses in 118433 steps
c [sweep-15] limit 6690675 penalty 0 = 0 + 0
c [sweep-15-1] 1492 pos 11.8% + 11177 neg 88.2% = 12669 sched 45.8% ret 14974
c [sweep-15-1] 6697304 steps 227 queries 719.91 avg class size
c [sweep-15-1] 3507 decisions 210 SAT calls 95.75 avg env size
c [sweep-15-1] 11545 variables remain 42% (16091 retained 58%)
c [decomp-49] removed 65 variables
c [sweep-15-1] removed 65 vars (0 failed, 23 eqs, 35 impls)
c [sweep-15] removed 65 vars in TOTAL (1 rounds, 226 queries)
c [phase-count-19] 158021 negative 99.6% of 158654 except 633 0.4%
c [phase-count-19] 108185 positive 68.2% of 158654 except 50469 31.8%
c [phase-count-19] skipping relative phase luck test
c [phase-19] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-19] sorted 15641 enqueued variables after 120348 conflicts
c [score-dist-19] active 11937 (43%), one 12860 (47%), zero 2781 (10%)
c [score-dist-19] max exp 975, different 349 (36%)
c [score-dist-19] median active exp 923, avg 815.4
c [simplification-19] removed 2052 variables 6.9% (27578 remain 13%)
c [simplification-19] removed 18737 irredundant clauses 10.6% (158654 remain 13%)
c [simplification-19] maximum reduction of 11% = max (7%, 11%)
c [simplification-19] large reduction 11% >= 5% limit
c [simplification-19] next conflict interval 2000 = 2000/1
c [simplification-19] penalized conflict interval 2000 = 1 * 2000
c [simplification-19] hard conflict limit 132348 (soft 122348 + delta 10000)
c [simplification-19] new conflict limit 122348 (hard 132348)
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  155.6   27577   158654    120364   33409   5520 244154   10    17   38  59%     29  -37   11   13   85%
c 
c [simplification-20] limit 122348 conflicts (hard 132348) hit after 132348 conflicts
c [quatres-16] found 12764 quaternary clauses 42% in total
c [quatres-16-1] removed 2 duplicate quaternary clauses
c [quatres-16-2] added 1 single-self-subsuming ternary resolvents
c [quatres-16-2] added 13 quaternary resolvents
c [ternres-16] limit 23857842 with penalty 0 = 0 + 0
c [ternres-16] all 27554 free variables schedulable
c [ternres-16] 648 ternary resolvents (0 bin, 648 trn)
c [ternres-16] fully completed ternary resolution
c [gauss-6] limit 298223 penalty 4 = 4 + 0
c [gauss-6] extracted 9 xors of average arity 3.0
c [gauss-6] connected 27 occurrences of 27 variables (average 1.0)
c [gauss-6] limit 298223 penalty 4 = 4 + 0
c [gauss-6] fully completed
c [gauss-6] exported 0 unary, 0 binary and 0 ternary equations
c [treelook-7] limit 2385784 penalty 0 = 0 + 0 boost 1
c [treelook-7] scheduled 43631 literals 79%
c [treelook-7] scheduling used 901381 steps
c [treelook-7] scheduled completely
c [treelook-7] limit 2385784 penalty 0 = 0 + 0 boost 1
c [treelook-7] used 2386386 steps
c [treelook-7] 43517 literals remain 79%
c [treelook-7] 8533 variables remain to probed next time 31%
c [treelook-7] removed 6 variables, found 13666 hbrs
c [unhide-20] limit 4771568 with penalty 0 = 0 + 0
c [unhide-20-31] 1 units, 31 failed, 32673 tauts, 0 hbrs, 28530 literals
c [transred-16] limit 2000000 with penalty 0 = 0 + 0
c [transred-16] removed 537 transitive binary clauses
c [transred-16] found 1 units
c [block-6] scheduling all variables this time
c [block-6] scheduled 27520 variables 100%
c [block-6] limit of 14911151 steps penalty 4 = 4 + 0
c [block-6] fully completed
c [block-6] transition to [ all 0 rem 0 ] state
c [block-6] eliminated 49 blocked clauses
c [block-6] 49 < 1/100 * 157581 = 1575 considered unsuccessful
c [elim-17] no untried remaining variables left
c [elim-17] scheduled 27520 variables 100%
c [elim-17] limit of 477156851 steps penalty 0 = 0 + 0
c [elim-17] rescheduling of touched variables disabled
c [elim-17-1] eliminated 175 variables 1% in round 1 in 11409829 steps
c [elim-17-1] backward subsumption/strengthening limit 11409800
c [elim-17-1-1] backward checking 1340 touched variables 5%
c [elim-17-1-1] fully completed backward checking in 1 rounds
c [elim-17-1] subsumed 9 and strengthened 25 clauses in 330043 steps
c [elim-17-1] rescheduled 87 variables 0% by backward subsumption
c [elim-17-2] eliminated 9 variables 0% in round 2 in 60218 steps
c [elim-17-2] backward subsumption/strengthening limit 60200
c [elim-17-2-1] backward checking 100 touched variables 0%
c [elim-17-2-1] fully completed backward checking in 1 rounds
c [elim-17-2] subsumed 5 and strengthened 3 clauses in 52518 steps
c [elim-17-2] rescheduled 18 variables 0% by backward subsumption
c [elim-17-3] no variable eliminated in round 3 in 20449 steps
c [elim-17] fully completed in 3 rounds
c [elim-17] transition to [ all 0 rem 0 ] state
c [elim-17] eliminated 184 = 1% variables out of 27520 scheduled
c [elim-17] 184 < 1/100 * 27520 = 275 considered unsuccessful
c [bca-16] limit of 10000000 steps and 315348 added (scaled 2)
c [bca-16] 37660 out of 54674 literals actually usable 69%
c [bca-16] added 17 blocked clauses in 127348 steps
c [sweep-16] limit 7157352 penalty 0 = 0 + 0
c [sweep-16-1] 1387 pos 12.2% + 9978 neg 87.8% = 11365 sched 41.6% ret 15971
c [sweep-16-1] 7911019 steps 202 queries 538.47 avg class size
c [sweep-16-1] 2489 decisions 188 SAT calls 94.54 avg env size
c [sweep-16-1] 10483 variables remain 38% (16853 retained 62%)
c [decomp-52] removed 14 variables
c [sweep-16-1] removed 14 vars (0 failed, 13 eqs, 30 impls)
c [sweep-16] 14 < 1/1000 * 27336 = 27 considered unsuccessful
c [sweep-16] removed 14 vars in TOTAL (1 rounds, 201 queries)
c [sort-queue-20] sorted 17382 enqueued variables after 132348 conflicts
c [score-dist-20] active 9940 (36%), one 14696 (54%), zero 2686 (10%)
c [score-dist-20] max exp 698, different 286 (41%)
c [score-dist-20] median active exp 658, avg 603.4
c [simplification-20] removed 232 variables 0.8% (27322 remain 13%)
c [simplification-20] removed 1585 irredundant clauses 1.0% (157069 remain 13%)
c [simplification-20] maximum reduction of 1% = max (1%, 1%)
c [simplification-20] geometric conflict interval increment 12666 = 25332 / 2
c [simplification-20] new conflict interval 37998
c [simplification-20] penalized conflict interval 37998 = 1 * 37998
c [simplification-20] hard conflict limit 189345 (soft 170346 + delta 18999)
c [simplification-20] new conflict limit 170346 (hard 189345)
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 -  176.2   27322   157069    154935   37024   5915 223077    9    14   33  62%    385  -24    7   12   61%
c i  176.5   27321   157069    155478   37430   5934 223085    9    15   39  60%    391  -24    6   12   53%
c i  176.8   27170   157069    156083   37848   5954 223092    8    13   39  62%    153  -25    5   12   42%
c i  177.1   26763   157069    156910   38531   5973 223102    8    13   39  62%     -9  -25    5   12   46%
c i  177.7   26756   157069    158164   39489   5986 223108    8    12   39  65%    -96  -25    6   12   52%
c i  177.7   25167   157069    158180   39494   5990 223110    8    12   39  65%    -96  -25    6   12   50%
c i  177.9   25107   157069    158558   39755   5999 223114    8    12   39  66%   -110  -26    6   12   48%
c i  178.0   25012   157069    158913   40012   6015 223120    7    11   39  66%   -118  -26    5   12   42%
c i  178.1   24934   157069    159180   40173   6027 223126    7    11   39  66%   -123  -26    7   12   57%
c i  178.2   24932   157069    159190   40181   6027 223127    7    11   39  66%   -123  -26    6   12   56%
c i  178.2   24833   157069    159225   40190   6033 223131    7    11   39  66%   -124  -26    6   12   54%
c i  178.2   24547   157069    159257   40207   6036 223132    7    11   39  66%   -124  -26    6   12   51%
c i  178.2   24374   157069    159258   40207   6036 223132    7    11   39  66%   -124  -26    6   12   51%
c i  178.2   24229   157069    159294   40220   6043 223136    7    11   39  66%   -125  -26    5   12   47%
c i  178.2   24089   157069    159295   40220   6043 223136    7    11   39  66%   -125  -26    5   12   47%
c i  178.2   23977   157069    159299   40220   6043 223138    7    11   39  66%   -125  -26    5   12   47%
c i  178.2   23583   157069    159301   40220   6043 223139    7    11   39  66%   -125  -26    5   12   46%
c i  178.2   23358   157069    159304   40220   6043 223141    7    11   39  66%   -125  -26    5   12   46%
c i  178.2   22333   157069    159307   40220   6043 223143    7    11   39  66%   -125  -26    5   12   45%
c 0  178.2   21926   157069    159307   40220   6043 223143    7    11   39  66%   -125  -26    5   12   45%
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 UNSATISFIABLE
c
c bate: 1766 basic ate = 1436 trn 81% + 330 lrg 19% in 5 updates
c bcas: 16 count, 1373 added (735 skipped), 3511218 steps
c bkwd: tried 398397 clauses, 795663 lits, 2.00 lits/clause
c bkwd: checked 10499904 occs, 26.36 occs/clause, 13.20 occs/lit
c bkwd: subsumed 70 binary, 309 ternary, 163 large
c bkwd: strengthened 19 binary, 6 ternary (100% self), 1560 large (0% self)
c blkd: 6 bces, 9418 removed, 6761618 resolutions, 18935380 steps
c blkd: 10878 blocking literals 2%, 31 pure
c bump: 160716 bumped seen, 34447862 lits 214.3 on average
c card: 5 count, 0 units, 0 am1, 40091632 steps
c card: 0 rescheduled, 0 eliminated, 0 resolved, 77670 subsumed
c card: 12631 at-most-one constraints found, average size 4.68
c card: 12631 at-most-one constraints used 100%, average size 4.68
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: 8 cces, 41071 eliminated, 40974 ate 100%, 97 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: 4059289 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 158 gcs, 0 rescored clauses, 84 rescored vars
c dcps: 52 decompositions, 8022 equivalent 4%
c deco: 961 decision-only clauses 1%, 55% reduction
c decs: 1808164 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 17 elims, 91142 eliminated 41%, 233 pure 0%
c elms: 47 rounds, 2.8 rounds/bve
c elms: 77316 small 85%, 13562 large 15%
c elms: 214458 tried small, 77326 succeeded 36%, 137132 failed 64%
c elms: 32189 subsumed, 58429 strengthened, 988 blocked
c elms: 16294482 copies, 15746417 resolutions, 5742842 ipos
c elms: 3580314 subchks, 2063501 strchks
c gaus: 6 extractions, 422 extracted, 2.4 size, 3 max
c gaus: exported 1 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 12207076 steps, 6103538 extr 50%, 4654 elim 0%
c glue: 15.5 orig avg, 15.5 real avg, 2.8 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 674683 = 188774 simple 28% + 469648 trn 70% + 16261 lrg 2%, 3481 sub 1%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 160716 clauses, 65.6 length
c lrnd: 10548802 lits = 18482576 orig - 7933774 removed 43%
c lrnd: 66083 uips 41%, 81086 flips 50%
c mins: 152406 mins 95%, 2579 bin 2%, 4534 size 3%
c mins: 40499776 poisoned searches, 6968909 hits, 17% hit rate
c mins: 51237612 used twice searches, 1510851 hits, 3% hit rate
c move: moved 26402, 17345 bin 66%, 9057 trn 34%
c otfs: 417 driving 30%, 955 restarting 70%
c otfs: str 1372, 1228 red 90%, 144 irr 10%
c otfs: str 1372, 0 bin 0%, 173 trn 13%, 1199 lrg 87%
c otfs: sub 2, 2 red 100%, 0 irr 0%
c otfs: sub 2, 0 bin 0%, 1 trn 50%, 1 lrg 50%
c phas: 19 computed, 146733 set, 3 pos (0%), 146730 neg (100%)
c prbs: 6 basic, 30494 probed, 2022 failed, 33 lifted
c prbs: 7 simple, 627420 probed, 1064 failed, 713 eqs
c prbs: 7 treelook, 264 probed, 18 failed, 0 lifted
c prom: 14814 locked 7% out of 223397 tried
c prps: 379996222 props, 196 props/dec
c prps: 93% srch, 7% simp, 0% lkhd
c quat: 16 count, 159 quat, 31 self1, 1 self2, 768 dup
c queu: 20 sorted, 1808164 next (165910 steps 0.09)
c queu: 36719006 enq (37888099 steps 1.03), 34447862 deq 94%
c redc: 5001 clauses 16%, 31098 tried 20%, 194 sat 1%
c redc: 10493 lits 3%, 330634 tried 2%, 194 sat 0%
c redc: 670 times jump level reduced, 21.7 levels on average
c reds: 2 count, 79653.5 conflicts per reduce
c reds: 0 memlim 0%, 2 arith 100%
c reds: 50502 collected 83%, 10496 retired 17%
c rmbd: 41541 removed, 5977 red 14%
c rsts: 6432 restarts 100%, 0 skipped 0%
c rsts: 0 saturating 0%, 0 reuse 0%
c rsts: 0 kept 0.0% average 0.0%
c scnc: 1 count, 1.200 min (200/1000), 1.200 max (200/1000)
c simp: 20 count, 17 confs 85%, 0 vars 0%
c simp: 2 its 10%, 1 bin 5%, 0 trns 0%
c subl: 160716 count (128093 tried 0.8), 10772 sub out of 153306 (7.0%)
c swps: 16 count, 16 rounds, 2302 queries (143.9/round)
c swps: 2058 sat calls, 89 unsat (0.9% success rate)
c swps: 28745 decisions 14.0, 1826 conflicts 0.9
c swps; 1710.9 avg class size, 91.0 avg environment size
c swps: 0 failed, 499 impls, 314 equivs
c swp0: 762 type 0 queries, 243 unsat (31.9%), 717 sat (94.1%)
c swp1: 1540 type 1 queries, 1014 unsat (65.8%), 1271 sat (82.5%)
c sync: 0 produced units, 0 successful consumptions 0%
c sync: 0 consume units calls, 0 tried 0%, 0 success 0%
c sync: 0 produced clauses, 0 successful consumptions 0%
c sync: 0 consume clause calls, 0 tried 0%, 0 success 0%
c time: 3938806 calls to obtain time
c tops: 103497 fixed 46%, 490 its, 325.12 confs/it
c trds: 16 transitive reductions, 6982 removed, 70 failed
c trds: 40953 nodes, 106511 edges, 29640618 steps
c trim: 400054 words, 1.5 MB
c trnr: 16 count, 11 bin, 5743 trn, 76900816 steps
c unhd: 20 count, 31 rounds, 63504252 steps
c unhd: 1395 non-trivial sccs of average size 2.4
c unhd: 248 units, 247 bin, 1 trn, 0 lrg
c unhd: 9837 failed, 9762 stamp, 0 lits, 36 bin, 25 trn, 0 lrg
c unhd: 337306 tauts, 13979 bin 4%, 12338 trn 4%, 600 lrg 0%
c unhd: 337306 tauts, 310389 stamp 92%, 267967 red 79%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 388588 str, 247 bin 0%, 4591 trn 1%, 383750 lrg 99%, 368127 red 95%
c vars: 21926 remaining 10% and 202661 removed 90% out of 224587
c vars: 103497 fixed 46%, 91142 eliminated 41%, 8022 equivalent 4%
c vsts: 3046985237 visits, 92% srch, 8% simp, 0% lkhd
c vsts: 7.9 search visits per propagation, 17594.0 per conflict
c wchs: 485662285 pushed, 38927861 enlarged, 230 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all         153465         50502         10496       6603237        922450         64852
c 
c  0 0         24327  16       993   2         0   0   4326352  66    485592  53     27830  43     1.5
c  1 5         11994   8      2117   4       620   6    483349   7<    97185  11<     7773  12     1.0
c  2 6         39228  26     15743  31      2080  20    645827  10    133625  14     10413  16<    3.4
c  3 9         37940  25<    19555  39<     2437  23    431757   7     82254   9      6080   9     3.7
c  4 14        13251   9      5270  10      1291  12<   260693   4     41472   4      3626   6     2.1
c  5 21         7830   5      2278   5      1001  10    182970   3     28453   3      2785   4     1.4
c  6 30         5959   4      1655   3       861   8    129699   2     23962   3      2541   4     1.3
c  7 41         4706   3      1339   3       720   7     69952   1     12782   1      1543   2     1.2
c  8 54         2740   2       640   1       474   5     26962   0      6836   1       815   1     0.7
c  9 69         1854   1       416   1       337   3     24275   0      4461   0       581   1     0.6
c 10 86         1852   1       316   1       332   3     15781   0      3771   0       510   1     0.6
c 11 126        1424   1       138   0       261   2      4964   0      1760   0       302   0     0.4
c 12 230         358   0        42   0        82   1       651   0       296   0        53   0     0.2
c 13 534           2   0         0   0         0   0         5   0         1   0         0   0     0.0
c 
c avg                  2.9           3.1           4.4           1.1           1.4           1.9
c std                  2.3           1.7           2.6           1.8           2.0           2.4
c 
c   17.270  10% cce
c   14.750   8% elim
c   14.047   8% probe
c   11.707   7% unhide
c    7.560   4% sweep
c    5.137   3% bump
c    2.046   1% bca
c    1.947   1% block
c    1.664   1% transred
c    1.476   1% gauss
c 
c    2.843 < 1% rest (below)
c 
c    1.121   1% decide
c    0.664   0% ternres
c    0.582   0% quatres
c    0.282   0% card
c    0.195   0% rescore
c    0.000   0% locs
c    0.000   0% queuesort
c ==================================
c    4.462   3% preprocessing     5%
c   76.988  43% inprocessing     95%
c ==================================
c   81.450  46% simplifying
c   96.756  54% search
c ==================================
c  178.209 100% all
c 
c        159307 conflicts,         893.9 confs/sec
c          3111 ternaries,          51.2 confs/ternary
c          3247 binaries,           49.1 confs/binary
c           490 iterations,        325.1 confs/iteration
c 
c             2 reductions,          0.0 redus/sec,  79653.5 confs/reduction
c          6432 restarts,           36.1 rests/sec,     24.8 confs/restart
c       1808164 decisions,       10146.3 decis/sec,     11.4 decis/conflict
c     379996222 propagations,  2132300.9 props/sec,    210.2 props/decision
c 
c 178.2 seconds, 77.3 MB
c launch: done
