c launch: /data/cnf/sc2014/app/UCG-20-10p0.cnf.bz2
c host: atom28
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-10p0.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/UCG-20-10p0.cnf.bz2
c no embedded options
c found 'p cnf 258799 1372149' header
c read 258799 variables, 1372149 clauses, 3305872 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=6
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 245650 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] AVG (--score=6)
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  245650  1358130         0       0      0     0    0     0   58   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 6235 at-most-one constraints of average size 5.8
c [card-1] no at-most-two constraint found
c [card-1] using previous limit 2000000 for elimination
c [card-1] 6235 out of 6235 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 62743 variables
c [simpleprobe-1] all 196056 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 256 variables
c [simpleprobe-1] 14990 variables remain 8% (180810 retained 92%)
c [simpleprobe-1] removed 256 variables, found 15144 hbrs, 20 units
c [unhide-1] limit 65074 based on 1041195 irredundant clauses
c [unhide-1-1] 14 units, 1356 failed, 8994 tauts, 0 hbrs, 8360 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 193678 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 60734 not tried 31% in round 1
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 74453 = 38% variables out of 193678 scheduled
c [elim-1] considered successful since not run to completion yet
c [phase-count-1] 858937 negative 99.2% of 865538 except 6601 0.8%
c [phase-count-1] 693844 positive 80.2% of 865538 except 171694 19.8%
c [phase-count-1] less non-negative clauses 6601 than limit 86500 (10.0%)
c [phase-count-1] non-pos/non-neg = 171694/6601 = 26.01 >= 2.00 = 200/100
c [lucky-phase-1] forcing lucky phase -1
c [phase-1] phase bias: 0 positive 0%, 119225 negative 100%
c [sort-queue-1] sorted 119225 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 119225 (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 82997 variables 41.0% (119225 remain 49%)
c [simplification-1] removed 492592 irredundant clauses 36.3% (865538 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    5.2  119224   865538       170     130     14 10753    0     8   58   6%      0    8    6    0 18896%
c i    5.2  118389   865538       179     135     16 10753    1     8   58   7%      0    8    7    0 18884%
c i    5.3  118377   865538       194     146     18 10754    1     9   58   7%      0    9    7    0 18187%
c i    5.3  118376   865538       219     165     20 10757    1    10   58   6%      0   10    6    0 16868%
c i    5.3  118366   865538       220     165     20 10757    1    10   58   6%      0   10    6    0 16803%
c i    5.5  117065   865538       271     209     23 10760    1    13   58   5%      0   13    6    0 14773%
c i    5.5  116834   865538       273     210     23 10760    1    13   58   5%      0   13    6    0 14728%
c i    5.6  116193   865538       355     272     37 10763    1    17   58   5%      0   17    7    0 13436%
c i    5.7  115430   865538       419     329     39 10766    1    18   58   6%      0   18    8    0 12297%
c i    6.0  115412   865538       858     705     66 10789    2    22   58   8%      1   22    9    0 7093%
c 
c [simplification-2] limit of 10 iterations hit after 10 iterations
c [decomp-3] removed 3952 variables
c [simpleprobe-2] 13745 schedulable variables 12%
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [decomp-4] removed 9 variables
c [simpleprobe-2] 14832 variables remain 13% (100432 retained 87%)
c [simpleprobe-2] removed 9 variables, found 1662 hbrs, 2 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 44139 literals 19%
c [treelook-1] scheduling used 391301 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 531650 steps
c [treelook-1] 44048 literals remain 19%
c [treelook-1] 43830 variables remain to probed next time 38%
c [decomp-5] removed 133 variables
c [treelook-1] removed 220 variables, found 3941 hbrs
c [basicprobe-1] limit 6684464 based on 835558 irredundant clauses
c [basicprobe-1-0] 41932 probes remain 38% after last round
c [basicprobe-1-0] 24 units = 24 failed (100%) + 0 lifted (0%)
c [basicprobe-1-0] removed 4490 variables, found 18261 hbrs
c [unhide-2] limit 52222 based on 835558 irredundant clauses
c [unhide-2-2] 17 units, 2324 failed, 8420 tauts, 0 hbrs, 1940 literals
c [elim-2] 56554 variables 53% will be scheduled this time
c [elim-2] scheduled 56554 variables 53%
c [elim-2] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-2] rescheduling of touched variables disabled
c [elim-2] incomplete 22110 not tried 21% in round 1
c [elim-2] transition to [ all 0 rem 1 ] state
c [elim-2] eliminated 57 = 0% variables out of 56554 scheduled
c [elim-2] considered successful since not run to completion yet
c [phase-count-2] 755791 negative 99.1% of 762392 except 6601 0.9%
c [phase-count-2] 608166 positive 79.8% of 762392 except 154226 20.2%
c [phase-count-2] less non-negative clauses 6601 than limit 76200 (10.0%)
c [phase-count-2] non-pos/non-neg = 154226/6601 = 23.36 >= 2.00 = 200/100
c [lucky-phase-2] forcing lucky phase -1
c [phase-2] phase bias: 0 positive 0%, 15252 negative 100%
c [sort-queue-2] sorted 93400 enqueued variables after 858 conflicts
c [score-dist-2] active 13750 (13%), one 0 (0%), zero 93400 (87%)
c [score-dist-2] max exp 511, different 12 (2%)
c [score-dist-2] median active exp 509, avg 509.2
c [simplification-2] removed 8229 variables 7.1% (107150 remain 44%)
c [simplification-2] removed 103146 irredundant clauses 11.9% (762392 remain 56%)
c [simplification-2] maximum reduction of 12% = max (7%, 12%)
c [simplification-2] forced so keeping old conflict interval 0
c [simplification-2] conflict limit remains at 1016 (hard 11000)
c [simplification-2] new iteration interval 100
c 
c [simplification-3] limit 1016 conflicts (hard 11000) hit after 1017 conflicts
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 4126 at-most-one constraints of average size 4.6
c [card-2] no at-most-two constraint found
c [card-2] using previous limit 1000000 for elimination
c [card-2] 4126 out of 4126 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [decomp-6] removed 58 variables
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] scheduled 36320 literals 17%
c [treelook-2] scheduling used 304458 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] used 1948891 steps
c [treelook-2] 36311 literals remain 17%
c [treelook-2] 25960 variables remain to probed next time 24%
c [treelook-2] removed 1 variables, found 1129 hbrs
c [unhide-3] limit 50000 with penalty 1 = 0 + 1
c [unhide-3-3] 17 units, 1082 failed, 17064 tauts, 0 hbrs, 503 literals
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 105704 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 29406 not tried 28% in round 1
c [elim-3] transition to [ all 1 rem 1 ] state
c [elim-3] eliminated 2052 = 2% variables out of 105704 scheduled
c [elim-3] considered successful since not run to completion yet
c [phase-count-3] 724019 negative 99.1% of 730485 except 6466 0.9%
c [phase-count-3] 580776 positive 79.5% of 730485 except 149709 20.5%
c [phase-count-3] less non-negative clauses 6466 than limit 73000 (10.0%)
c [phase-count-3] non-pos/non-neg = 149709/6466 = 23.15 >= 2.00 = 200/100
c [lucky-phase-3] forcing lucky phase -1
c [phase-3] phase bias: 0 positive 0%, 13946 negative 100%
c [sort-queue-3] sorted 88210 enqueued variables after 1017 conflicts
c [score-dist-3] active 15442 (15%), one 0 (0%), zero 88210 (85%)
c [score-dist-3] max exp 511, different 12 (2%)
c [score-dist-3] median active exp 510, avg 509.6
c [simplification-3] removed 3498 variables 3.3% (103652 remain 42%)
c [simplification-3] removed 31907 irredundant clauses 4.2% (730485 remain 54%)
c [simplification-3] maximum reduction of 4% = max (3%, 4%)
c [simplification-3] geometric conflict interval increment 4000 = 20000 / 5
c [simplification-3] new conflict interval 4000
c [simplification-3] penalized conflict interval 4000 = 1 * 4000
c [simplification-3] hard conflict limit 15017 (soft 5017 + delta 10000)
c [simplification-3] new conflict limit 5017 (hard 15017)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   11.9  103651   730485      1023     756     78 20018    2    27   50   7%      1   26    8    0 5554%
c i   12.1  103642   730485      1123     832     86 20025    2    30   51   7%      1   29    8    0 5401%
c i   12.2  103608   730485      1322     996    101 20040    3    33   51   9%      1   33   15    0 7130%
c i   12.2  103597   730485      1323     996    101 20040    3    33   51   9%      1   33   15    0 7102%
c i   12.2  103587   730485      1334    1004    101 20042    3    34   51   9%      1   33   15    0 6873%
c i   12.2  103577   730485      1348    1014    103 20043    3    34   51   9%      1   34   14    0 6766%
c i   12.3  103570   730485      1391    1050    108 20044    3    36   51   8%      1   36   14    0 6184%
c i   12.3  103566   730485      1393    1051    108 20044    3    36   51   8%      1   36   14    0 6155%
c i   12.3  103508   730485      1422    1074    110 20047    3    37   51   8%      1   37   14    0 6249%
c i   12.4  103497   730485      1536    1170    115 20053    3    39   51   9%      1   39   13    0 5321%
c i   12.4  103484   730485      1537    1170    115 20053    3    39   51   9%      1   39   13    0 5300%
c i   12.5  103196   730485      1591    1217    120 20053    3    41   51   8%      1   40   12    0 4792%
c i   12.7  103186   730485      1668    1275    130 20058    4    44   51   8%      1   43   11    0 4077%
c i   12.7  103176   730485      1693    1296    130 20059    4    44   51   8%      1   43   11    0 4099%
c i   12.7  103166   730485      1694    1296    130 20059    4    44   51   8%      1   43   11    0 4083%
c i   12.7  103153   730485      1702    1301    130 20061    4    44   51   8%      1   43   11    0 3999%
c i   12.7  103145   730485      1704    1302    130 20061    4    44   51   8%      1   43   11    0 3995%
c i   13.0  103131   730485      1973    1514    158 20082    4    49   51   9%      1   48   12    0 3692%
c i   13.1  103129   730485      2018    1549    164 20083    4    51   51   8%      1   50   11    0 3397%
c i   13.2  103116   730485      2124    1647    166 20085    5    53   51   9%      1   52   15    0 4085%
c 
c [simplification-4] limit of 154 binary hit after 154 binaries
c [decomp-8] removed 583 variables
c [basicprobe-2] limit 5806896 based on 725862 irredundant clauses
c [basicprobe-2-0] 38660 probes remain 38% after last round
c [basicprobe-2-0] 18 units = 18 failed (100%) + 0 lifted (0%)
c [basicprobe-2-0] removed 1547 variables, found 10843 hbrs
c [unhide-4] limit 94701 with penalty 1 = 0 + 1
c [unhide-4-4] 4 units, 1776 failed, 4649 tauts, 0 hbrs, 1289 literals
c [elim-4] 21770 variables 22% will be scheduled this time
c [elim-4] scheduled 21770 variables 22%
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 41631589 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 21770 scheduled
c [phase-count-4] 690746 negative 99.1% of 697211 except 6465 0.9%
c [phase-count-4] 551026 positive 79.0% of 697211 except 146185 21.0%
c [phase-count-4] less non-negative clauses 6465 than limit 69700 (10.0%)
c [phase-count-4] non-pos/non-neg = 146185/6465 = 22.61 >= 2.00 = 200/100
c [lucky-phase-4] forcing lucky phase -1
c [phase-4] phase bias: 0 positive 0%, 9860 negative 100%
c [sort-queue-4] sorted 75160 enqueued variables after 2546 conflicts
c [score-dist-4] active 24647 (25%), one 0 (0%), zero 75160 (75%)
c [score-dist-4] max exp 513, different 14 (3%)
c [score-dist-4] median active exp 512, avg 511.6
c [simplification-4] removed 3296 variables 3.2% (99807 remain 41%)
c [simplification-4] removed 33274 irredundant clauses 4.6% (697211 remain 51%)
c [simplification-4] maximum reduction of 5% = max (3%, 5%)
c [simplification-4] forced so keeping old conflict interval 4000
c [simplification-4] conflict limit remains at 5058 (hard 15017)
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   15.8   99806   697211      2550    1988    172 24481    6    61   49   9%      2   60   14    0 3202%
c i   16.1   99730   697211      2734    2142    181 24496    6    66   50   9%      2   65   13    0 2774%
c i   16.1   99384   697211      2744    2149    181 24497    6    66   50   9%      2   65   13    0 2709%
c i   16.2   99371   697211      2920    2306    190 24505    6    69   50   9%      2   68   15    1 2926%
c i   16.2   99370   697211      2922    2307    190 24505    6    69   50   9%      2   68   15    1 2909%
c i   16.2   99367   697211      2923    2307    190 24505    6    69   50   9%      2   68   15    1 2898%
c i   16.3   99360   697211      2947    2328    192 24505    6    70   50   9%      2   68   15    1 2794%
c i   16.5   99350   697211      3082    2427    203 24517    7    73   50   9%      2   71   13    1 2365%
c i   16.7   99337   697211      3220    2526    218 24533    7    79   50   9%      2   77   13    1 2285%
c i   16.9   99262   697211      3296    2590    225 24537    7    84   50   8%      2   82   12    1 2053%
c i   17.0   98847   697211      3355    2639    229 24541    7    89   50   8%      1   87   19    1 3078%
c i   17.0   98839   697211      3398    2675    234 24542    7    92   50   8%      1   89   19    1 2971%
c i   17.5   98712   697211      3901    3108    255 24568    9   101   50   9%      2   98   23    1 2818%
c i   17.7   98704   697211      3976    3161    264 24577    9   102   50   9%      2   99   19    1 2306%
c i   17.8   98694   697211      4064    3228    270 24587    9   104   50   9%      2  101   16    1 1979%
c i   17.9   98686   697211      4155    3303    275 24595    9   105   50   9%      2  102   16    1 1910%
c i   18.0   98569   697211      4194    3334    275 24602    9   107   50   9%      2  103   17    1 2001%
c i   18.1   98551   697211      4265    3382    283 24613   10   110   50   9%      2  106   18    1 2023%
c i   18.3   98540   697211      4362    3457    289 24623   10   116   50   8%      2  112   16    1 1744%
c i   18.7   98470   697211      4691    3730    303 24640   11   126   51   9%      2  121   21    1 2081%
c i   18.8   98334   697211      4776    3810    304 24643   11   128   51   9%      2  124   21    1 2022%
c i   19.0   98328   697211      4968    3983    313 24649   12   132   51   9%      2  127   24    1 2116%
c i   19.1   98245   697211      5035    4028    317 24655   12   132   51   9%      2  127   21    1 1842%
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.1   98238   697211      5041    4032    318 24655   12   132   51   9%      2  127   21    1 1819%
c 
c [simplification-5] limit 5075 conflicts (hard 15017) hit after 5075 conflicts
c [quatres-1] found 33232 quaternary clauses 32% in total
c [quatres-1-2] added 1 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 97960 free variables schedulable
c [ternres-1] 276 ternary resolvents (0 bin, 276 trn)
c [ternres-1] fully completed ternary resolution
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 384 xors of average arity 2.2
c [gauss-1] connected 830 occurrences of 405 variables (average 2.0)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] fully completed
c [gauss-1] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-9] removed 256 variables
c [simpleprobe-3] 12226 schedulable variables 13%
c [simpleprobe-3] limit 7947128 penalty 0 = 0 + 0
c [decomp-10] removed 135 variables
c [simpleprobe-3] 11196 variables remain 11% (86373 retained 89%)
c [simpleprobe-3] removed 135 variables, found 14033 hbrs, 60 units
c [unhide-5] limit 397356 with penalty 0 = 0 + 0
c [unhide-5-5] 3 units, 560 failed, 18373 tauts, 0 hbrs, 5930 literals
c [transred-1] limit 1986782 with penalty 0 = 0 + 0
c [transred-1] removed 266 transitive binary clauses
c [transred-1] found 9 units
c [block-1] scheduling all variables this time
c [block-1] scheduled 96909 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 11997 blocked clauses
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 57 clauses out of 408 (14%) of length 10
c [cce-1-1] eliminated 119 clauses out of 2668 (4%) of length 9
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 176 large clauses in 30000005 steps
c [cce-1-1] allowing another 15000002 steps for small clauses
c [cce-1-1] scheduling 525207 clauses = 324659 binary + 200548 ternary
c [cce-1-1] tried to eliminate 334 small clauses 0%
c [cce-1-1] eliminated 84 binary clauses 0%
c [cce-1-1] eliminated 24 ternary clauses 0%
c [cce-1-1] eliminated 108 small clauses 0%
c [cce-1-1] eliminated 108 small clauses in 30000002 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 284 covered clauses in round 1
c [cce-1] eliminated 284 covered clauses in TOTAL during 1 rounds
c [cce-1] 284 < 1/100 * 650215 = 6502 considered unsuccessful
c [bca-1] limit of 10000000 steps and 1300362 added (scaled 2)
c [bca-1] 176975 out of 193820 literals actually usable 91%
c [bca-1] added 271 blocked clauses in 566193 steps
c [sweep-1] limit 1299862 based on 649931 irredundant clauses
c [sweep-1-1] 4413 pos 4.6% + 92496 neg 95.4% = 96909 sched 100.0% ret 0
c [sweep-1-1] 2930011 steps 14 queries 26228.57 avg class size
c [sweep-1-1] 247 decisions 11 SAT calls 180.55 avg env size
c [sweep-1-1] 96834 variables remain 100% (20 retained 0%)
c [decomp-11] removed 62 variables
c [sweep-1-1] removed 62 vars (0 failed, 3 eqs, 5 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 62 vars in TOTAL (1 rounds, 13 queries)
c [phase-count-5] 642924 negative 99.0% of 649360 except 6436 1.0%
c [phase-count-5] 522433 positive 80.5% of 649360 except 126927 19.5%
c [phase-count-5] less non-negative clauses 6436 than limit 64900 (10.0%)
c [phase-count-5] non-pos/non-neg = 126927/6436 = 19.72 >= 2.00 = 200/100
c [lucky-phase-5] forcing lucky phase -1
c [phase-5] phase bias: 0 positive 0%, 5526 negative 100%
c [sort-queue-5] sorted 64982 enqueued variables after 5075 conflicts
c [score-dist-5] active 31865 (33%), one 0 (0%), zero 64982 (67%)
c [score-dist-5] max exp 514, different 12 (2%)
c [score-dist-5] median active exp 513, avg 513.0
c [simplification-5] removed 1113 variables 1.1% (96847 remain 39%)
c [simplification-5] removed 47851 irredundant clauses 6.9% (649360 remain 48%)
c [simplification-5] maximum reduction of 7% = max (1%, 7%)
c [simplification-5] large reduction 7% >= 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 17075 (soft 7075 + delta 10000)
c [simplification-5] new conflict limit 7075 (hard 17075)
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   23.5   96846   649360      5102    4041    621 48094   12   131   49   9%      2  126   18    1 1621%
c i   23.5   96845   649360      5120    4053    623 48096   12   131   49   9%      2  126   18    1 1553%
c i   23.5   96843   649360      5178    4093    625 48102   12   130   49   9%      2  125   18    1 1561%
c i   23.5   96838   649360      5183    4096    625 48103   12   130   49   9%      2  125   18    1 1544%
c i   23.6   96821   649360      5273    4170    630 48112   12   134   50   9%      1  128   18    1 1550%
c i   23.9   96813   649360      5457    4327    640 48124   13   145   50   9%      1  140   26    1 2048%
c i   24.2   96798   649360      5593    4442    643 48129   13   151   50   9%      1  145   21    1 1611%
c i   24.2   96786   649360      5594    4442    643 48129   13   151   50   9%      1  145   21    1 1605%
c i   24.5   96776   649360      5719    4551    652 48132   13   162   50   8%      1  156   23    1 1730%
c i   24.5   96766   649360      5776    4599    658 48133   14   168   50   8%      1  161   25    1 1807%
c i   24.6   96746   649360      5839    4653    662 48133   14   168   50   8%      1  161   24    1 1713%
c i   25.5   96736   649360      6402    5104    707 48178   14   181   50   8%      3  173   16    1 1058%
c i   25.5   96686   649360      6403    5104    707 48178   14   181   50   8%      3  173   16    1 1054%
c i   25.6   96667   649360      6469    5156    711 48185   14   181   50   8%      2  172   15    2  967%
c i   26.6   96162   649360      6970    5552    753 48228   15   204   50   8%      3  194   24    2 1400%
c i   26.8   96075   649360      7061    5631    757 48232   16   209   50   7%      3  199   23    2 1297%
c i   26.8   96070   649360      7063    5632    757 48232   16   209   50   7%      3  199   22    2 1292%
c i   26.8   96069   649360      7082    5644    759 48235   16   208   50   8%      3  198   23    2 1333%
c i   26.8   96068   649360      7085    5644    759 48237   16   208   50   8%      3  198   23    2 1318%
c 
c [simplification-6] limit 7105 conflicts (hard 17075) hit after 7106 conflicts
c [quatres-2] found 34659 quaternary clauses 34% in total
c [quatres-2-1] removed 1 duplicate quaternary clauses
c [quatres-2-2] added 1 single-self-subsuming ternary resolvents
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] all 96067 free variables schedulable
c [ternres-2] 2 ternary resolvents (0 bin, 2 trn)
c [ternres-2] 66351 variables remain 69% (29716 retained 31%)
c [card-3] limit 500000 penalty 2 = 2 + 0
c [card-3] found 1917 at-most-one constraints of average size 4.1
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 500000 for elimination
c [card-3] 1917 out of 1917 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [decomp-12] removed 936 variables
c [treelook-3] limit 303047 penalty 0 = 0 + 0 boost 1
c [treelook-3] scheduled 72205 literals 38%
c [treelook-3] scheduling used 518088 steps
c [treelook-3] not fully scheduled
c [treelook-3] limit 303047 penalty 0 = 0 + 0 boost 1
c [treelook-3] used 361394 steps
c [treelook-3] 72199 literals remain 38%
c [treelook-3] 20439 variables remain to probed next time 21%
c [treelook-3] removed 0 variables, found 3224 hbrs
c [unhide-6] limit 606095 with penalty 0 = 0 + 0
c [unhide-6-6] 17 units, 799 failed, 9104 tauts, 0 hbrs, 10501 literals
c [transred-2] limit 2000000 with penalty 0 = 0 + 0
c [transred-2] removed 266 transitive binary clauses
c [transred-2] found 12 units
c [block-2] scheduling all variables this time
c [block-2] scheduled 94440 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 1222 blocked clauses
c [block-2] 1222 < 1/100 * 644495 = 6444 considered unsuccessful
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 94440 variables 100%
c [elim-5] limit of 30304763 steps penalty 1 = 1 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5] incomplete 13092 not tried 14% in round 1
c [elim-5] transition to [ all 1 rem 1 ] state
c [elim-5] eliminated 1862 = 2% variables out of 94440 scheduled
c [bca-2] limit of 10000000 steps and 1252063 added (scaled 2)
c [bca-2] 164989 out of 185158 literals actually usable 89%
c [bca-2] added 139 blocked clauses in 512788 steps
c [sweep-2] limit 1251428 based on 625714 irredundant clauses
c [sweep-2-1] 4439 pos 4.8% + 88124 neg 95.2% = 92563 sched 100.0% ret 15
c [sweep-2-1] 1412942 steps 11 queries 27994.36 avg class size
c [sweep-2-1] 176 decisions 9 SAT calls 204.22 avg env size
c [sweep-2-1] 92540 variables remain 100% (38 retained 0%)
c [decomp-14] removed 2 variables
c [sweep-2-1] removed 2 vars (0 failed, 1 eqs, 1 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 2 vars in TOTAL (1 rounds, 10 queries)
c [phase-count-6] 619602 negative 99.0% of 625710 except 6108 1.0%
c [phase-count-6] 500828 positive 80.0% of 625710 except 124882 20.0%
c [phase-count-6] less non-negative clauses 6108 than limit 62500 (10.0%)
c [phase-count-6] non-pos/non-neg = 124882/6108 = 20.45 >= 2.00 = 200/100
c [lucky-phase-6] forcing lucky phase -1
c [phase-6] phase bias: 0 positive 0%, 3671 negative 100%
c [sort-queue-6] sorted 54358 enqueued variables after 7106 conflicts
c [score-dist-6] active 38218 (41%), one 0 (0%), zero 54358 (59%)
c [score-dist-6] max exp 514, different 12 (2%)
c [score-dist-6] median active exp 514, avg 513.5
c [simplification-6] removed 3491 variables 3.6% (92576 remain 38%)
c [simplification-6] removed 23650 irredundant clauses 3.6% (625710 remain 46%)
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 8000
c [simplification-6] penalized conflict interval 8000 = 1 * 8000
c [simplification-6] hard conflict limit 25106 (soft 15106 + delta 10000)
c [simplification-6] new conflict limit 15106 (hard 25106)
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.9   92575   625710      7177    5384    546 42255   15   210   49   7%      3  200   19    2 1070%
c i   31.5   92574   625710      7623    5770    567 42275   16   217   49   7%      3  205   24    2 1270%
c i   31.5   92573   625710      7625    5770    567 42276   16   217   49   7%      3  205   24    2 1260%
c i   32.0   92572   625710      7998    6088    583 42298   16   218   49   8%      3  205   18    2  914%
c i   32.2   92571   625710      8131    6211    585 42300   17   216   49   8%      3  203   24    2 1166%
c i   33.1   92562   625710      8717    6725    617 42322   18   218   49   8%      4  203   24    2 1067%
c i   33.3   92558   625710      8845    6835    626 42329   18   220   49   8%      3  205   22    2  961%
c i   33.4   92547   625710      8869    6854    628 42330   18   220   49   8%      3  205   22    2  958%
c i   33.4   92394   625710      8886    6866    628 42333   18   220   49   8%      3  204   21    2  913%
c i   33.4   92344   625710      8934    6897    633 42335   18   218   49   8%      3  202   20    2  857%
c i   33.4   92338   625710      8935    6897    633 42335   18   218   49   8%      3  202   20    2  853%
c i   34.0   92336   625710      9333    7228    657 42362   19   220   50   9%      3  204   27    2 1100%
c i   34.1   92335   625710      9349    7237    659 42365   19   221   50   9%      3  204   26    2 1058%
c i   34.4   91591   625710      9538    7391    664 42381   19   221   50   9%      3  203   24    3  935%
c i   34.5   91587   625710      9636    7474    666 42385   20   217   50   9%      2  200   28    3 1084%
c i   35.0   91583   625710      9882    7689    675 42398   20   215   50   9%      2  197   21    3  808%
c i   35.0   91582   625710      9889    7694    675 42398   20   215   50   9%      2  197   21    3  796%
c i   35.2   91581   625710     10005    7796    679 42405   20   219   50   9%      2  201   22    3  837%
c i   35.2   91449   625710     10008    7798    679 42405   20   219   50   9%      2  201   23    3  869%
c i   35.3   91448   625710     10057    7833    682 42415   20   220   50   9%      2  201   23    3  853%
c i   35.3   91447   625710     10058    7833    682 42415   20   220   50   9%      2  201   23    3  850%
c i   35.3   91446   625710     10059    7833    682 42415   20   220   50   9%      2  201   23    3  846%
c i   35.3   91445   625710     10060    7833    682 42415   20   220   50   9%      2  201   23    3  843%
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   35.7   91444   625710     10226    7978    692 42421   20   225   50   9%      2  206   27    3  987%
c i   36.1   91443   625710     10414    8137    699 42436   21   237   51   9%      2  217   32    3 1117%
c i   36.1   91442   625710     10416    8137    699 42437   21   237   51   9%      2  217   32    3 1108%
c i   36.6   91441   625710     10643    8336    708 42450   23   265   51   9%      2  244   49    3 1583%
c i   37.1   91440   625710     10913    8578    718 42460   23   267   51   9%      2  245   30    3  964%
c i   37.2   91439   625710     10942    8600    719 42464   23   267   51   9%      2  245   28    3  894%
c i   37.3   91312   625710     10998    8650    722 42466   23   269   51   9%      2  247   28    3  895%
c i   37.7   91309   625710     11167    8801    732 42471   24   282   51   9%      1  259   41    3 1246%
c i   38.1   91299   625710     11357    8959    743 42485   25   297   51   8%      1  273   42    3 1222%
c i   38.1   91286   625710     11360    8960    743 42486   25   296   51   8%      1  273   41    3 1208%
c i   38.1   91227   625710     11361    8960    743 42486   25   296   51   8%      1  273   41    3 1203%
c i   38.1   91222   625710     11392    8984    745 42489   25   296   51   8%      1  272   38    3 1109%
c i   38.7   91208   625710     11675    9231    752 42505   26   296   51   9%      2  271   39    4 1089%
c i   38.7   91204   625710     11696    9247    751 42509   26   295   51   9%      1  270   37    4 1021%
c i   38.7   91201   625710     11698    9248    751 42509   26   295   51   9%      1  270   36    4 1014%
c i   38.9   90563   625710     11813    9339    760 42512   26   294   51   9%      1  268   32    4  877%
c i   39.1   90562   625710     11888    9399    767 42516   26   293   51   9%      1  267   29    4  804%
c i   39.3   90510   625710     12066    9559    773 42525   26   292   51   9%      1  265   29    4  788%
c i   39.8   90509   625710     12312    9779    781 42537   27   296   51   9%      1  268   41    4 1058%
c i   39.8   90505   625710     12332    9797    781 42538   27   296   51   9%      1  269   39    4 1021%
c i   39.9   90502   625710     12367    9828    783 42538   28   302   51   9%      1  274   47    4 1199%
c i   39.9   90501   625710     12368    9828    783 42538   27   301   51   9%      1  274   47    4 1194%
c i   40.0   90500   625710     12377    9836    783 42538   28   303   51   9%      1  275   48    4 1217%
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   40.0   90499   625710     12386    9844    783 42538   28   304   51   9%      1  276   48    4 1230%
c i   40.3   90497   625710     12538    9970    789 42547   28   305   52   9%      1  276   38    4  952%
c i   40.7   90360   625710     12788   10188    798 42555   28   306   52   9%      1  276   35    4  862%
c i   41.1   90359   625710     13040   10404    803 42562   33   306   53  11%      1  275   91    4 2044%
c i   41.5   90358   625710     13264   10603    810 42571   32   308   53  10%      1  277   53    5 1162%
c i   41.8   90351   625710     13516   10824    815 42580   32   310   53  10%      1  277   44    5  938%
c i   42.3   90350   625710     13717   11009    819 42588   33   323   53  10%      1  290   49    5 1025%
c i   42.5   90349   625710     13824   11099    821 42598   33   323   54  10%      1  289   45    5  922%
c i   42.7   90342   625710     13879   11144    824 42600   34   324   54  10%      1  290   50    5 1013%
c i   42.9   90341   625710     13988   11238    827 42604   34   325   54  11%      1  290   52    5 1038%
c i   44.0   90340   625710     14500   11671    861 42628   37   327   54  11%      2  290   48    5  890%
c i   44.0   90339   625710     14515   11682    862 42629   36   327   54  11%      2  290   46    5  859%
c i   44.3   90338   625710     14608   11769    865 42630   37   332   54  11%      2  294   46    5  854%
c i   44.3   90337   625710     14611   11771    865 42630   37   331   54  11%      2  294   47    5  863%
c i   44.3   90326   625710     14614   11773    865 42630   37   331   54  11%      2  294   47    5  856%
c i   44.4   90323   625710     14672   11819    869 42632   37   332   54  11%      2  294   47    5  857%
c i   44.7   90321   625710     14827   11954    874 42636   37   331   54  11%      2  293   48    6  857%
c i   45.0   90318   625710     14986   12086    882 42640   38   329   54  12%      2  290   54    6  942%
c i   45.4   90317   625710     15134   12206    888 42657   39   337   54  12%      2  297   56    6  962%
c 
c [simplification-7] limit 15196 conflicts (hard 25106) hit after 15196 conflicts
c [quatres-3] found 33825 quaternary clauses 36% in total
c [quatres-3-2] added 3 single-self-subsuming ternary resolvents
c [quatres-3-2] added 2 quaternary resolvents
c [ternres-3] limit 7179782 with penalty 0 = 0 + 0
c [ternres-3] 62377 schedulable variables 67%
c [ternres-3] 16 ternary resolvents (0 bin, 16 trn)
c [ternres-3] 8754 variables remain 10% (81560 retained 90%)
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] extracted 254 xors of average arity 2.1
c [gauss-2] connected 542 occurrences of 266 variables (average 2.0)
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] fully completed
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-15] removed 305 variables
c [basicprobe-3] limit 35898911 penalty 0 = 0 + 0
c [basicprobe-3-0] 32040 probes remain 36% after last round
c [basicprobe-3-0] 149 units = 149 failed (100%) + 0 lifted (0%)
c [basicprobe-3-0] removed 1829 variables, found 64481 hbrs
c [bate-1] eliminated 91 asymmetric tautologies during probing
c [unhide-7] limit 717978 with penalty 1 = 0 + 1
c [unhide-7-7] 6 units, 283 failed, 13522 tauts, 0 hbrs, 38642 literals
c [transred-3] limit 2000000 with penalty 0 = 0 + 0
c [transred-3] removed 195 transitive binary clauses
c [transred-3] found 8 units
c [cce-2] limit of 17949455 steps penalty 1 = 1 + 0
c [cce-2-1] eliminated 12 clauses out of 1674 (1%) of length 9
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] eliminated 12 large clauses in 17949458 steps
c [cce-2-1] allowing another 8974729 steps for small clauses
c [cce-2-1] scheduling 307963 clauses = 289540 binary + 18423 ternary
c [cce-2-1] tried to eliminate 285 small clauses 0%
c [cce-2-1] eliminated 95 binary clauses 0%
c [cce-2-1] eliminated 8 ternary clauses 0%
c [cce-2-1] eliminated 103 small clauses 0%
c [cce-2-1] eliminated 5138 small clauses in 17949456 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 5150 covered clauses in round 1
c [cce-2] eliminated 5150 covered clauses in TOTAL during 1 rounds
c [cce-2] 5150 < 1/100 * 589359 = 5893 considered unsuccessful
c [elim-6] 12853 variables 15% will be scheduled this time
c [elim-6] scheduled 12853 variables 15%
c [elim-6] limit of 143595647 steps penalty 0 = 0 + 0
c [elim-6] rescheduling of touched variables disabled
c [elim-6-1] no variable eliminated in round 1 in 26800208 steps
c [elim-6] fully completed in 1 rounds
c [elim-6] transition to [ all 0 rem 0 ] state
c [elim-6] eliminated 0 = 0% variables out of 12853 scheduled
c [bca-3] limit of 10000000 steps and 1165125 added (scaled 2)
c [bca-3] 147121 out of 175354 literals actually usable 84%
c [bca-3] added 40 blocked clauses in 433957 steps
c [sweep-3] limit 2153934 penalty 0 = 0 + 0
c [sweep-3-1] 3694 pos 4.2% + 83950 neg 95.8% = 87644 sched 100.0% ret 32
c [sweep-3-1] 3248887 steps 17 queries 23749.18 avg class size
c [sweep-3-1] 221 decisions 13 SAT calls 97.15 avg env size
c [sweep-3-1] 87246 variables remain 100% (63 retained 0%)
c [decomp-16] removed 423 variables
c [sweep-3-1] removed 423 vars (0 failed, 3 eqs, 6 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 423 vars in TOTAL (1 rounds, 16 queries)
c [phase-count-7] 573100 negative 98.9% of 579207 except 6107 1.1%
c [phase-count-7] 463092 positive 80.0% of 579207 except 116115 20.0%
c [phase-count-7] less non-negative clauses 6107 than limit 57900 (10.0%)
c [phase-count-7] non-pos/non-neg = 116115/6107 = 19.01 >= 2.00 = 200/100
c [lucky-phase-7] forcing lucky phase -1
c [phase-7] phase bias: 0 positive 0%, 1563 negative 100%
c [sort-queue-7] sorted 42159 enqueued variables after 15196 conflicts
c [score-dist-7] active 45094 (52%), one 0 (0%), zero 42159 (48%)
c [score-dist-7] max exp 515, different 10 (2%)
c [score-dist-7] median active exp 515, avg 514.8
c [simplification-7] removed 3061 variables 3.4% (87253 remain 36%)
c [simplification-7] removed 46503 irredundant clauses 7.4% (579207 remain 43%)
c [simplification-7] maximum reduction of 7% = max (3%, 7%)
c [simplification-7] large reduction 7% >= 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 27196 (soft 17196 + delta 10000)
c [simplification-7] new conflict limit 17196 (hard 27196)
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   50.6   87252   579207     15285   12216    891 99810   39   337   55  12%      1  296   52    6  882%
c i   51.2   87250   579207     15674   12558    896 99830   39   330   56  12%      2  288   40    6  663%
c i   51.5   87249   579207     15822   12696    897 99833   39   325   56  12%      2  283   35    6  572%
c i   51.7   87244   579207     15956   12816    899 99842   39   323   56  12%      2  279   36    6  579%
c i   51.8   87243   579207     15996   12849    901 99845   39   324   56  12%      2  281   38    6  615%
c i   52.0   87241   579207     16156   12976    908 99851   41   329   56  12%      1  285   58    6  902%
c i   52.1   87239   579207     16238   13053    909 99851   41   326   56  13%      1  281   53    6  812%
c i   52.5   87236   579207     16492   13274    912 99860   41   325   56  13%      1  280   52    7  773%
c i   52.9   87235   579207     16752   13508    920 99864   41   322   56  13%      1  276   43    7  630%
c i   52.9   87234   579207     16800   13552    922 99864   41   321   56  13%      1  274   44    7  643%
c 
c [simplification-8] limit 17196 conflicts (hard 27196) hit after 17198 conflicts
c [quatres-4] found 38743 quaternary clauses 41% in total
c [quatres-4-1] removed 2 duplicate quaternary clauses
c [ternres-4] limit 7976064 with penalty 0 = 0 + 0
c [ternres-4] 8449 schedulable variables 10%
c [ternres-4] 7 ternary resolvents (0 bin, 7 trn)
c [ternres-4] fully completed ternary resolution
c [decomp-17] removed 32 variables
c [simpleprobe-4] 10063 schedulable variables 12%
c [simpleprobe-4] limit 31904256 penalty 0 = 0 + 0
c [decomp-18] removed 1464 variables
c [simpleprobe-4] 1768 variables remain 2% (83989 retained 98%)
c [simpleprobe-4] removed 1464 variables, found 45495 hbrs, 510 units
c [unhide-8] limit 1595212 with penalty 0 = 0 + 0
c [unhide-8-8] 4 units, 786 failed, 22773 tauts, 0 hbrs, 41622 literals
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 282 transitive binary clauses
c [transred-4] found 4 units
c [block-3] scheduling all variables this time
c [block-3] scheduled 84755 variables 100%
c [block-3] limit of 39880320 steps penalty 1 = 1 + 0
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 97 blocked clauses
c [block-3] 97 < 1/100 * 564840 = 5648 considered unsuccessful
c [bca-4] limit of 10000000 steps and 1110297 added (scaled 2)
c [bca-4] 140939 out of 169510 literals actually usable 83%
c [bca-4] added 96 blocked clauses in 419716 steps
c [sweep-4] limit 2392819 penalty 0 = 0 + 0
c [sweep-4-1] 4285 pos 5.1% + 80413 neg 94.9% = 84698 sched 99.9% ret 56
c [sweep-4-1] 2863053 steps 24 queries 14057.88 avg class size
c [sweep-4-1] 413 decisions 21 SAT calls 143.71 avg env size
c [sweep-4-1] 84533 variables remain 100% (201 retained 0%)
c [decomp-19] removed 53 variables
c [sweep-4-1] removed 53 vars (0 failed, 2 eqs, 5 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 53 vars in TOTAL (1 rounds, 23 queries)
c [phase-count-8] 548445 negative 98.9% of 554547 except 6102 1.1%
c [phase-count-8] 439404 positive 79.2% of 554547 except 115143 20.8%
c [phase-count-8] less non-negative clauses 6102 than limit 55400 (10.0%)
c [phase-count-8] non-pos/non-neg = 115143/6102 = 18.87 >= 2.00 = 200/100
c [lucky-phase-8] forcing lucky phase -1
c [phase-8] phase bias: 0 positive 0%, 1506 negative 100%
c [sort-queue-8] sorted 39781 enqueued variables after 17198 conflicts
c [score-dist-8] active 44920 (53%), one 0 (0%), zero 39781 (47%)
c [score-dist-8] max exp 516, different 11 (2%)
c [score-dist-8] median active exp 515, avg 515.2
c [simplification-8] removed 2533 variables 2.9% (84701 remain 34%)
c [simplification-8] removed 24660 irredundant clauses 4.3% (554547 remain 41%)
c [simplification-8] maximum reduction of 4% = max (3%, 4%)
c [simplification-8] geometric conflict interval increment 4000 = 20000 / 5
c [simplification-8] new conflict interval 12000
c [simplification-8] penalized conflict interval 12000 = 1 * 12000
c [simplification-8] hard conflict limit 39198 (soft 29198 + delta 10000)
c [simplification-8] new conflict limit 29198 (hard 39198)
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.3   84700   554547     17383   13987    906 119217   43   319   56  13%      3  270   48    7  669%
c i   57.3   84698   554547     17391   13994    906 119217   43   319   56  13%      3  269   48    7  663%
c i   58.6   84697   554547     18231   14745    938 119235   44   312   56  14%      5  259   44    8  563%
c i   58.7   84694   554547     18280   14787    938 119237   44   314   56  14%      5  262   54    8  697%
c i   59.4   84600   554547     18610   15091    946 119244   45   320   56  14%      4  266   54    8  669%
c i   59.4   84566   554547     18624   15103    946 119245   45   319   56  14%      4  265   52    8  645%
c i   59.4   84565   554547     18640   15117    946 119245   45   320   56  14%      4  265   54    8  664%
c i   60.3   84564   554547     19206   15619    963 119262   47   319   56  15%      4  262   54    8  634%
c i   61.0   84562   554547     19835   16162    978 119271   45   304   56  15%      4  245   44    9  499%
c i   61.0   84558   554547     19838   16163    978 119272   45   304   56  15%      4  245   44    9  497%
c i   61.0   84549   554547     19840   16164    978 119272   45   304   56  15%      4  245   44    9  498%
c i   61.1   84535   554547     19868   16187    980 119274   45   304   56  15%      4  244   41    9  468%
c i   61.3   84534   554547     20021   16317    984 119283   46   305   56  15%      4  245   45    9  506%
c i   61.3   84529   554547     20049   16343    984 119283   45   304   56  15%      4  244   44    9  497%
c i   61.5   84528   554547     20127   16409    989 119286   47   307   56  15%      3  247   63    9  697%
c i   61.6   84524   554547     20147   16425    989 119286   47   309   56  15%      3  248   69    9  767%
c i   61.6   84521   554547     20159   16436    989 119286   47   310   56  15%      3  249   67    9  740%
c i   61.6   84520   554547     20171   16446    990 119286   47   310   56  15%      3  249   64    9  710%
c i   61.8   84516   554547     20267   16532    991 119289   48   315   56  15%      3  254   76    9  824%
c i   61.9   84514   554547     20331   16589    994 119291   48   314   56  15%      3  253   67    9  729%
c i   62.1   84513   554547     20407   16661    994 119291   48   315   56  15%      3  254   58    9  629%
c i   62.1   84510   554547     20409   16662    994 119291   48   315   56  15%      3  254   58    9  626%
c i   62.1   84504   554547     20423   16670    996 119293   48   316   56  15%      2  254   63    9  678%
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   63.3   84498   554547     21113   17290   1019 119310   51   330   56  15%      4  266   75   10  763%
c i   63.7   84497   554547     21309   17467   1024 119314   52   337   57  15%      3  273   69   10  687%
c i   63.7   84493   554547     21325   17481   1024 119314   51   336   57  15%      3  271   65   10  652%
c i   63.8   84492   554547     21388   17538   1024 119314   52   335   57  15%      3  270   67   10  661%
c i   63.8   84491   554547     21393   17542   1024 119314   52   335   57  15%      3  270   67   10  661%
c i   63.8   84490   554547     21409   17557   1024 119314   52   336   57  15%      3  270   64   10  636%
c i   64.1   84489   554547     21553   17674   1027 119324   52   336   57  15%      3  271   63   10  618%
c i   64.2   84488   554547     21574   17685   1031 119329   52   336   57  15%      3  271   62   10  608%
c i   64.4   84479   554547     21711   17804   1037 119333   51   334   57  15%      2  267   51   10  500%
c i   65.1   84478   554547     21981   18041   1043 119344   54   350   58  15%      2  283   84   11  794%
c i   66.0   84477   554547     22427   18437   1053 119364   55   362   59  15%      2  293   68   11  623%
c i   66.2   84476   554547     22547   18545   1055 119367   55   362   59  15%      2  292   57   11  519%
c i   66.2   84475   554547     22548   18545   1055 119367   55   362   59  15%      2  291   57   11  517%
c i   66.7   84474   554547     22815   18792   1056 119373   55   358   59  15%      2  287   60   11  537%
c i   67.2   84473   554547     23106   19057   1060 119380   56   359   59  16%      2  287   67   12  579%
c i   67.2   84472   554547     23122   19072   1060 119380   56   359   59  16%      2  287   65   12  567%
c i   68.0   84466   554547     23547   19442   1074 119395   57   356   59  16%      2  281   66   12  553%
c i   68.1   84465   554547     23611   19498   1076 119398   58   361   59  16%      2  286   74   12  620%
c i   68.2   84459   554547     23670   19546   1078 119400   58   359   59  16%      2  284   68   12  565%
c i   68.9   84453   554547     24038   19872   1090 119407   60   367   59  16%      2  290   80   12  645%
c i   69.0   84447   554547     24142   19964   1094 119408   59   362   59  16%      2  285   62   12  503%
c i   69.1   84444   554547     24168   19988   1095 119408   58   362   59  16%      2  285   58   12  468%
c i   69.2   84443   554547     24224   20035   1098 119411   59   363   60  16%      2  285   60   12  485%
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   69.3   84442   554547     24256   20064   1098 119411   59   363   60  16%      2  286   63   12  509%
c i   70.2   84435   554547     24729   20486   1110 119428   58   358   60  16%      2  279   48   13  374%
c i   70.3   84431   554547     24791   20543   1111 119430   57   357   60  16%      2  277   46   13  359%
c i   70.9   84394   554547     25114   20836   1116 119439   57   350   60  16%      2  268   54   13  417%
c i   71.0   84393   554547     25159   20871   1117 119444   57   350   60  16%      2  268   54   13  419%
c i   71.6   83746   554547     25436   21105   1124 119453   59   354   60  17%      2  272   80   13  600%
c i   71.6   83745   554547     25470   21133   1126 119455   59   354   60  17%      2  271   75   13  562%
c i   71.7   83736   554547     25495   21154   1128 119455   59   355   60  17%      2  272   72   13  540%
c i   71.9   83730   554547     25609   21258   1131 119457   60   359   60  17%      1  276   78   13  580%
c i   73.1   83729   554547     26166   21768   1139 119468   63   367   60  17%      3  282   84   14  601%
c i   73.4   83728   554547     26280   21876   1141 119470   62   365   60  17%      2  279   70   14  493%
c i   73.4   83727   554547     26284   21879   1141 119470   62   365   60  17%      2  279   70   14  494%
c i   73.4   83726   554547     26304   21895   1141 119471   63   364   60  17%      2  278   77   14  541%
c i   73.4   83723   554547     26320   21906   1141 119473   63   364   60  17%      2  278   78   14  549%
c i   73.5   83720   554547     26350   21935   1141 119473   63   364   60  17%      2  277   73   14  517%
c i   73.5   83719   554547     26354   21938   1141 119473   63   363   60  17%      2  277   72   14  511%
c i   74.1   83718   554547     26646   22194   1146 119477   65   362   62  18%      2  275   97   15  666%
c i   75.1   83717   554547     27161   22637   1164 119502   66   369   64  18%      3  280   96   15  640%
c i   75.3   83716   554547     27232   22697   1168 119504   67   369   64  18%      2  279   96   15  637%
c i   75.7   83715   554547     27415   22863   1177 119507   66   367   64  18%      2  276   73   15  480%
c i   76.2   83710   554547     27632   23063   1180 119512   67   372   64  18%      2  280   77   15  499%
c i   76.4   83707   554547     27742   23161   1182 119514   68   370   65  18%      2  278   88   16  566%
c i   77.5   83706   554547     28331   23686   1195 119529   68   378   66  18%      3  283   76   16  477%
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.7   83701   554547     28406   23750   1199 119530   69   378   66  18%      3  283   81   16  502%
c i   77.9   83700   554547     28527   23860   1200 119532   69   379   66  18%      2  284   77   16  474%
c i   78.5   83697   554547     28842   24140   1208 119545   69   380   66  18%      2  283   78   17  474%
c i   79.1   83684   554547     29135   24395   1221 119557   69   382   68  18%      2  284   70   17  416%
c i   79.1   83681   554547     29151   24409   1222 119557   69   382   68  18%      2  284   68   17  406%
c 
c [simplification-9] limit 29228 conflicts (hard 39198) hit after 29229 conflicts
c [ternres-5] limit 13791957 with penalty 0 = 0 + 0
c [ternres-5] all 83676 free variables schedulable
c [ternres-5] 15 ternary resolvents (0 bin, 15 trn)
c [ternres-5] fully completed ternary resolution
c [decomp-20] removed 1156 variables
c [unhide-9] limit 1379195 with penalty 1 = 0 + 1
c [unhide-9-9] 4 units, 93 failed, 11712 tauts, 0 hbrs, 100887 literals
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 225 transitive binary clauses
c [transred-5] found 3 units
c [elim-7] scheduling all variables this time
c [elim-7] scheduled 83373 variables 100%
c [elim-7] limit of 137919575 steps penalty 1 = 1 + 0
c [elim-7] rescheduling of touched variables disabled
c [elim-7-1] eliminated 2660 variables 3% in round 1 in 48600175 steps
c [elim-7-1] backward subsumption/strengthening limit 48600100
c [elim-7-1-1] backward checking 8721 touched variables 10%
c [elim-7-1-1] fully completed backward checking in 1 rounds
c [elim-7-1] subsumed 2 and strengthened 344 clauses in 2891187 steps
c [elim-7-1] rescheduled 750 variables 1% by backward subsumption
c [elim-7-2] eliminated 106 variables 0% in round 2 in 853054 steps
c [elim-7-2] backward subsumption/strengthening limit 853000
c [elim-7-2-1] backward checking 782 touched variables 1%
c [elim-7-2-1] fully completed backward checking in 1 rounds
c [elim-7-2] subsumed 0 and strengthened 0 clauses in 439709 steps
c [elim-7] fully completed in 2 rounds
c [elim-7] transition to [ all 0 rem 0 ] state
c [elim-7] eliminated 2766 = 3% variables out of 83373 scheduled
c [bca-5] limit of 10000000 steps and 1055255 added (scaled 2)
c [bca-5] 135080 out of 161216 literals actually usable 84%
c [bca-5] added 102 blocked clauses in 413705 steps
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 41375870 penalty 0 = 0 + 0
c [sweep-5-1] 3907 pos 4.9% + 76524 neg 95.1% = 80431 sched 99.8% ret 176
c [sweep-5-1] 41449553 steps 481 queries 1299.45 avg class size
c [sweep-5-1] 5563 decisions 401 SAT calls 103.60 avg env size
c [sweep-5-1] 66767 variables remain 84% (13014 retained 16%)
c [decomp-21] removed 1121 variables
c [sweep-5-1] removed 1121 vars (0 failed, 106 eqs, 163 impls)
c [sweep-5] considered successful since not run to completion yet
c [sweep-5] removed 1121 vars in TOTAL (1 rounds, 480 queries)
c [phase-count-9] 514772 negative 98.9% of 520536 except 5764 1.1%
c [phase-count-9] 409657 positive 78.7% of 520536 except 110879 21.3%
c [phase-count-9] less non-negative clauses 5764 than limit 52000 (10.0%)
c [phase-count-9] non-pos/non-neg = 110879/5764 = 19.24 >= 2.00 = 200/100
c [lucky-phase-9] forcing lucky phase -1
c [phase-9] phase bias: 0 positive 0%, 901 negative 100%
c [sort-queue-9] sorted 32247 enqueued variables after 29229 conflicts
c [score-dist-9] active 47239 (59%), one 0 (0%), zero 32247 (41%)
c [score-dist-9] max exp 516, different 10 (2%)
c [score-dist-9] median active exp 516, avg 515.8
c [simplification-9] removed 4190 variables 5.0% (79486 remain 32%)
c [simplification-9] removed 34011 irredundant clauses 6.1% (520536 remain 38%)
c [simplification-9] maximum reduction of 6% = max (5%, 6%)
c [simplification-9] large reduction 6% >= 5% limit
c [simplification-9] next conflict interval 2000 = 2000/1
c [simplification-9] penalized conflict interval 2000 = 1 * 2000
c [simplification-9] hard conflict limit 41229 (soft 31229 + delta 10000)
c [simplification-9] new conflict limit 31229 (hard 41229)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   85.9   79485   520536     29415   14550   1019 134049   69   382   55  18%      2  282   65   17  385%
c i   86.0   79484   520536     29464   14585   1025 134053   68   378   55  18%      2  279   58   17  343%
c i   86.4   79476   520536     29696   14797   1036 134057   67   379   55  18%      2  278   54   17  318%
c i   87.1   79474   520536     30104   15165   1045 134065   68   384   55  18%      2  281   80   17  461%
c i   87.2   79473   520536     30174   15230   1045 134065   68   385   55  18%      2  282   82   18  471%
c i   87.6   79469   520536     30363   15409   1047 134067   68   380   55  18%      1  277   65   18  368%
c i   87.7   79468   520536     30429   15468   1047 134070   67   381   55  18%      1  277   61   18  346%
c i   88.1   79466   520536     30666   15688   1050 134075   69   384   55  18%      1  279   81   18  455%
c i   88.4   79465   520536     30889   15867   1063 134086   68   381   55  18%      1  275   59   18  330%
c i   89.0   79460   520536     31232   16155   1079 134108   68   376   55  18%      1  269   67   18  365%
c 
c [simplification-10] limit 31229 conflicts (hard 41229) hit after 31232 conflicts
c [quatres-5] found 35220 quaternary clauses 40% in total
c [quatres-5-1] removed 1 duplicate quaternary clauses
c [quatres-5-2] added 1 quaternary resolvents
c [ternres-6] limit 14693128 with penalty 0 = 0 + 0
c [ternres-6] all 79455 free variables schedulable
c [ternres-6] 241 ternary resolvents (0 bin, 241 trn)
c [ternres-6] fully completed ternary resolution
c [card-4] limit 918320 penalty 3 = 3 + 0
c [card-4] found 3158 at-most-one constraints of average size 4.0
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 918320 for elimination
c [card-4] 3158 out of 3158 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [gauss-3] limit 734656 penalty 2 = 2 + 0
c [gauss-3] extracted 15 xors of average arity 2.7
c [gauss-3] connected 41 occurrences of 35 variables (average 1.2)
c [gauss-3] limit 734656 penalty 2 = 2 + 0
c [gauss-3] fully completed
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-22] removed 31 variables
c [treelook-4] limit 734656 penalty 1 = 1 + 0 boost 1
c [treelook-4] scheduled 83959 literals 53%
c [treelook-4] scheduling used 734658 steps
c [treelook-4] not fully scheduled
c [treelook-4] limit 734656 penalty 1 = 1 + 0 boost 1
c [treelook-4] used 796406 steps
c [treelook-4] 83936 literals remain 53%
c [treelook-4] 13581 variables remain to probed next time 17%
c [decomp-23] removed 1 variables
c [treelook-4] removed 4 variables, found 4940 hbrs
c [unhide-10] limit 2938625 with penalty 0 = 0 + 0
c [unhide-10-10] 13 units, 611 failed, 15008 tauts, 0 hbrs, 32193 literals
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 201 transitive binary clauses
c [transred-6] found 3 units
c [cce-3] limit of 18366410 steps penalty 2 = 2 + 0
c [cce-3-1] eliminated 1 clauses out of 234 (0%) of length 10
c [cce-3-1] eliminated 21 clauses out of 1364 (2%) of length 9
c [cce-3-1] eliminated 21 clauses out of 462 (5%) of length 8
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 43 large clauses in 18366411 steps
c [cce-3-1] allowing another 9183205 steps for small clauses
c [cce-3-1] scheduling 285961 clauses = 263055 binary + 22906 ternary
c [cce-3-1] tried to eliminate 363 small clauses 0%
c [cce-3-1] eliminated 107 binary clauses 0%
c [cce-3-1] eliminated 16 ternary clauses 0%
c [cce-3-1] eliminated 123 small clauses 0%
c [cce-3-1] eliminated 6276 small clauses in 18366410 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 6319 covered clauses in round 1
c [cce-3] eliminated 6319 covered clauses in TOTAL during 1 rounds
c [elim-8] scheduling all variables this time
c [elim-8] scheduled 78838 variables 100%
c [elim-8] boosting limit by 20
c [elim-8] limit of 5877251200 steps penalty 0 = 0 + 0
c [elim-8] rescheduling of touched variables disabled
c [elim-8-1] eliminated 1403 variables 2% in round 1 in 49391241 steps
c [elim-8-1] backward subsumption/strengthening limit 49391200
c [elim-8-1-1] backward checking 4732 touched variables 6%
c [elim-8-1-1] fully completed backward checking in 1 rounds
c [elim-8-1] subsumed 13 and strengthened 40 clauses in 1873994 steps
c [elim-8-1] rescheduled 130 variables 0% by backward subsumption
c [elim-8-2] eliminated 17 variables 0% in round 2 in 142956 steps
c [elim-8-2] backward subsumption/strengthening limit 142900
c [elim-8-2-1] backward checking 137 touched variables 0%
c [elim-8-2-1] incomplete backward checking 0 remain 0%
c [elim-8-2] subsumed 0 and strengthened 8 clauses in 142901 steps
c [elim-8-2] rescheduled 23 variables 0% by backward subsumption
c [elim-8-3] eliminated 2 variables 0% in round 3 in 22553 steps
c [elim-8-3] backward subsumption/strengthening limit 22500
c [elim-8-3-1] backward checking 25 touched variables 0%
c [elim-8-3-1] incomplete backward checking 0 remain 0%
c [elim-8-3] subsumed 0 and strengthened 4 clauses in 22501 steps
c [elim-8] incomplete 16 not tried 0% in round 3
c [elim-8] transition to [ all 1 rem 1 ] state
c [elim-8] eliminated 1431 = 2% variables out of 78838 scheduled
c [bca-6] limit of 10000000 steps and 1018990 added (scaled 2)
c [bca-6] 129101 out of 154816 literals actually usable 83%
c [bca-6] added 336 blocked clauses in 393551 steps
c [sweep-6] limit 4407938 penalty 0 = 0 + 0
c [sweep-6-1] 3832 pos 5.9% + 61320 neg 94.1% = 65152 sched 84.2% ret 12255
c [sweep-6-1] 4458006 steps 51 queries 7920.80 avg class size
c [sweep-6-1] 528 decisions 41 SAT calls 84.95 avg env size
c [sweep-6-1] 64897 variables remain 84% (12473 retained 16%)
c [decomp-24] removed 51 variables
c [sweep-6-1] removed 51 vars (0 failed, 11 eqs, 25 impls)
c [sweep-6] considered successful since not run to completion yet
c [sweep-6] removed 51 vars in TOTAL (1 rounds, 50 queries)
c [phase-count-10] 502955 negative 98.9% of 508649 except 5694 1.1%
c [phase-count-10] 397972 positive 78.2% of 508649 except 110677 21.8%
c [phase-count-10] less non-negative clauses 5694 than limit 50800 (10.0%)
c [phase-count-10] non-pos/non-neg = 110677/5694 = 19.44 >= 2.00 = 200/100
c [lucky-phase-10] forcing lucky phase -1
c [phase-10] phase bias: 0 positive 0%, 863 negative 100%
c [sort-queue-10] sorted 30057 enqueued variables after 31232 conflicts
c [score-dist-10] active 47299 (61%), one 0 (0%), zero 30057 (39%)
c [score-dist-10] max exp 516, different 10 (2%)
c [score-dist-10] median active exp 516, avg 515.8
c [simplification-10] removed 2099 variables 2.6% (77356 remain 31%)
c [simplification-10] removed 11887 irredundant clauses 2.3% (508649 remain 37%)
c [simplification-10] maximum reduction of 3% = max (3%, 2%)
c [simplification-10] geometric conflict interval increment 5000 = 20000 / 4
c [simplification-10] new conflict interval 17000
c [simplification-10] penalized conflict interval 17000 = 1 * 17000
c [simplification-10] hard conflict limit 58232 (soft 48232 + delta 10000)
c [simplification-10] new conflict limit 48232 (hard 58232)
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   94.6   77355   508649     31540   14434   1166 124844   67   371   53  18%      1  263   54   18  293%
c i   95.1   77354   508649     31795   14655   1176 124858   66   369   53  18%      1  260   56   19  300%
c i   95.7   77169   508649     32230   15033   1191 124874   67   360   53  19%      2  249   62   19  326%
c i   96.4   77168   508649     32628   15392   1198 124883   65   356   53  18%      2  243   47   19  245%
c i   96.5   77167   508649     32648   15411   1198 124883   65   356   53  18%      2  243   49   19  254%
c i   96.8   77154   508649     32823   15565   1199 124885   66   354   53  19%      2  241   72   19  372%
c i   96.8   77146   508649     32860   15596   1199 124889   66   355   53  19%      2  242   71   19  365%
c i   97.0   77145   508649     32952   15673   1202 124896   66   354   53  19%      1  240   61   19  315%
c i   97.1   77138   508649     33063   15764   1209 124899   65   351   53  19%      1  237   54   19  278%
c i   97.5   77137   508649     33244   15922   1214 124908   65   353   53  18%      1  238   60   20  305%
c i   97.8   77131   508649     33398   16062   1216 124913   66   354   53  19%      1  238   70   20  353%
c i   97.8   77130   508649     33424   16082   1217 124914   66   352   53  19%      1  237   65   20  330%
c i   97.8   77128   508649     33443   16098   1217 124914   66   352   53  19%      1  237   71   20  362%
c i   98.9   77125   508649     34028   16630   1229 124928   66   361   53  18%      2  243   75   20  373%
c i   99.3   77124   508649     34236   16823   1230 124929   67   359   53  19%      2  241   78   20  382%
c i   99.6   77121   508649     34439   17001   1238 124939   65   351   53  19%      2  232   50   20  246%
c i   99.6   77120   508649     34452   17011   1239 124940   65   350   53  19%      2  231   50   20  245%
c i  100.1   77114   508649     34709   17241   1251 124949   65   352   53  18%      2  232   54   21  263%
c i  100.7   77113   508649     35071   17559   1263 124960   65   356   54  18%      2  235   63   21  303%
c i  100.8   77112   508649     35135   17619   1263 124962   66   356   54  18%      2  235   67   21  322%
c i  100.9   77111   508649     35180   17660   1264 124963   65   355   54  18%      1  233   65   21  310%
c i  102.2   77110   508649     35789   18215   1281 124977   64   353   54  18%      3  229   57   21  267%
c i  102.4   77054   508649     35968   18377   1282 124980   66   351   54  19%      2  226   73   21  340%
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  102.7   77053   508649     36136   18532   1285 124983   65   351   55  19%      2  226   66   22  308%
c i  103.0   77052   508649     36353   18718   1290 124988   64   343   55  19%      2  217   50   22  229%
c i  103.5   77051   508649     36608   18952   1290 124992   64   340   55  19%      2  213   57   22  262%
c i  103.5   77046   508649     36618   18958   1290 124995   64   339   55  19%      2  212   55   22  255%
c i  103.9   76959   508649     36861   19165   1294 125001   63   335   56  19%      1  207   54   22  246%
c i  104.1   76951   508649     36953   19250   1296 125003   63   334   56  19%      1  206   51   22  235%
c i  104.2   76950   508649     37012   19297   1301 125005   63   335   56  19%      1  207   52   22  237%
c i  104.5   76947   508649     37170   19437   1302 125010   63   333   56  19%      1  204   62   22  280%
c i  105.1   76946   508649     37458   19689   1308 125012   65   334   56  19%      1  205   86   22  384%
c i  105.2   76896   508649     37593   19797   1308 125012   64   326   56  20%      1  197   70   22  312%
c i  106.1   76889   508649     38171   20306   1319 125027   64   321   58  20%      2  189   57   23  250%
c i  106.1   76832   508649     38172   20306   1319 125027   64   321   58  20%      2  189   57   23  249%
c i  106.6   76825   508649     38428   20525   1328 125033   67   322   58  21%      2  190   91   23  395%
c i  106.6   76823   508649     38429   20525   1328 125033   67   322   58  21%      2  190   91   23  394%
c i  106.6   76820   508649     38430   20525   1328 125033   66   322   58  21%      2  190   91   23  392%
c i  107.1   76814   508649     38708   20785   1332 125035   66   321   59  20%      2  188   68   23  293%
c i  107.1   76726   508649     38729   20804   1332 125036   66   321   59  20%      2  188   66   23  284%
c i  107.2   76725   508649     38777   20845   1333 125040   65   321   59  20%      2  188   59   23  252%
c i  107.5   76724   508649     38914   20969   1335 125042   65   326   60  20%      1  192   63   23  272%
c i  107.7   76723   508649     39018   21065   1335 125044   65   325   60  20%      1  192   64   23  276%
c i  108.3   76722   508649     39387   21397   1339 125053   66   323   60  20%      1  188   63   24  265%
c i  108.5   76719   508649     39472   21467   1344 125055   66   324   60  20%      1  189   67   24  281%
c i  108.6   76717   508649     39549   21538   1345 125055   67   324   60  21%      1  188   78   24  326%
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  108.9   76716   508649     39683   21665   1346 125057   67   323   60  21%      1  187   77   24  323%
c i  108.9   76715   508649     39684   21665   1346 125057   67   323   60  21%      1  187   77   24  322%
c i  109.8   76714   508649     40242   22151   1362 125076   67   320   61  21%      2  182   70   24  290%
c i  110.2   76711   508649     40444   22342   1366 125078   67   322   61  21%      2  185   71   24  291%
c i  110.3   76705   508649     40487   22380   1366 125078   67   325   61  21%      2  187   79   24  322%
c i  110.3   76704   508649     40488   22380   1366 125078   67   325   61  21%      2  187   79   24  321%
c i  111.7   76703   508649     41200   23020   1379 125092   70   327   62  22%      3  187   80   25  317%
c i  111.8   76702   508649     41236   23055   1379 125092   70   328   62  21%      3  188   78   25  312%
c i  111.9   76701   508649     41294   23109   1381 125092   70   330   62  21%      3  190   75   25  298%
c i  112.7   76697   508649     41677   23445   1393 125107   71   333   64  21%      3  192   73   25  288%
c i  113.4   76692   508649     42093   23807   1406 125116   73   333   64  22%      3  190  104   26  402%
c i  113.9   76691   508649     42378   24075   1409 125119   74   333   64  22%      2  190   91   26  349%
c i  114.6   76690   508649     42746   24411   1418 125127   73   328   64  22%      2  184   75   26  282%
c i  115.0   76496   508649     42970   24624   1421 125128   72   323   64  22%      2  178   64   27  242%
c i  115.5   76495   508649     43224   24849   1427 125132   73   325   64  23%      2  179   77   27  287%
c i  115.7   76491   508649     43326   24940   1428 125135   74   326   64  23%      1  180   81   27  303%
c i  115.8   76490   508649     43395   25005   1428 125135   73   324   64  23%      1  178   70   27  260%
c i  116.4   76487   508649     43730   25305   1431 125137   73   322   64  23%      1  175   78   27  287%
c i  116.5   76486   508649     43735   25309   1431 125137   73   322   64  23%      1  174   77   27  282%
c i  117.3   76474   508649     44264   25776   1444 125148   69   309   64  23%      2  160   50   27  185%
c i  118.3   76469   508649     44813   26257   1454 125155   72   307   65  23%      3  158   75   28  271%
c i  118.7   76468   508649     44997   26427   1454 125159   73   311   65  23%      2  161   89   28  319%
c i  118.7   76467   508649     45015   26442   1454 125159   73   310   65  23%      2  160   85   28  306%
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  119.3   76466   508649     45292   26684   1458 125172   73   307   66  24%      2  156   72   28  257%
c i  119.4   76465   508649     45323   26713   1458 125172   73   308   66  24%      2  157   72   28  256%
c i  119.9   76464   508649     45646   26999   1466 125177   73   312   66  23%      2  160   79   28  279%
c i  120.9   76348   508649     46125   27427   1471 125185   75   316   69  24%      2  163   82   29  286%
c i  121.0   76347   508649     46157   27456   1471 125185   75   315   69  24%      2  162   83   29  287%
c i  122.2   76346   508649     46704   27936   1477 125195   79   322   70  25%      3  168   99   30  337%
c i  122.3   76306   508649     46754   27979   1477 125195   80   322   70  25%      2  168  104   30  353%
c i  122.3   76305   508649     46755   27979   1477 125195   80   322   70  25%      2  168  104   30  351%
c i  122.5   76296   508649     46855   28070   1477 125195   80   321   70  25%      2  166   99   30  334%
c i  123.2   76287   508649     47196   28356   1482 125200   81   320   70  25%      2  164  100   30  334%
c i  123.2   76286   508649     47249   28400   1484 125202   81   319   70  25%      2  163   86   30  286%
c i  123.7   76280   508649     47485   28601   1489 125208   81   324   70  25%      2  167   88   30  291%
c 
c [simplification-11] limit 48295 conflicts (hard 58232) hit after 48296 conflicts
c [quatres-6] found 31359 quaternary clauses 38% in total
c [quatres-6-2] added 1 single-self-subsuming ternary resolvents
c [ternres-7] limit 22192469 with penalty 0 = 0 + 0
c [ternres-7] all 76276 free variables schedulable
c [ternres-7] 89 ternary resolvents (0 bin, 89 trn)
c [ternres-7] fully completed ternary resolution
c [decomp-25] removed 1345 variables
c [basicprobe-4] limit 110962347 penalty 0 = 0 + 0
c [basicprobe-4-0] 25438 probes remain 34% after last round
c [basicprobe-4-0] 565 units = 565 failed (100%) + 0 lifted (0%)
c [basicprobe-4-0] removed 1821 variables, found 127652 hbrs
c [bate-2] eliminated 234 asymmetric tautologies during probing
c [unhide-11] limit 2219246 with penalty 1 = 0 + 1
c [unhide-11-11] 9 units, 96 failed, 9258 tauts, 0 hbrs, 140529 literals
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 312 transitive binary clauses
c [transred-7] found 1 units
c [block-4] scheduling all variables this time
c [block-4] scheduled 74028 variables 100%
c [block-4] limit of 55481173 steps penalty 2 = 2 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 48 blocked clauses
c [block-4] 48 < 1/100 * 475142 = 4751 considered unsuccessful
c [elim-9] no untried remaining variables left
c [elim-9] scheduled 74018 variables 100%
c [elim-9] limit of 443849389 steps penalty 0 = 0 + 0
c [elim-9] rescheduling of touched variables disabled
c [elim-9-1] eliminated 1960 variables 3% in round 1 in 43279415 steps
c [elim-9-1] backward subsumption/strengthening limit 43279400
c [elim-9-1-1] backward checking 7040 touched variables 10%
c [elim-9-1-1] fully completed backward checking in 1 rounds
c [elim-9-1] subsumed 12 and strengthened 246 clauses in 2301870 steps
c [elim-9-1] rescheduled 576 variables 1% by backward subsumption
c [elim-9-2] eliminated 78 variables 0% in round 2 in 742665 steps
c [elim-9-2] backward subsumption/strengthening limit 742600
c [elim-9-2-1] backward checking 594 touched variables 1%
c [elim-9-2-1] fully completed backward checking in 1 rounds
c [elim-9-2] subsumed 6 and strengthened 13 clauses in 348136 steps
c [elim-9-2] rescheduled 55 variables 0% by backward subsumption
c [elim-9-3] eliminated 6 variables 0% in round 3 in 229721 steps
c [elim-9-3] backward subsumption/strengthening limit 229700
c [elim-9-3-1] backward checking 50 touched variables 0%
c [elim-9-3-1] fully completed backward checking in 1 rounds
c [elim-9-3] subsumed 0 and strengthened 8 clauses in 168338 steps
c [elim-9] incomplete 29 not tried 0% in round 3
c [gc-73] reconnected 240079 binary clauses (produced 0 empty 1 units)
c [elim-9] transition to [ all 1 rem 1 ] state
c [elim-9] eliminated 2061 = 3% variables out of 74018 scheduled
c [bca-7] limit of 10000000 steps and 937482 added (scaled 2)
c [bca-7] 117065 out of 143916 literals actually usable 81%
c [bca-7] added 107 blocked clauses in 351386 steps
c [sweep-7] limit 6657740 penalty 0 = 0 + 0
c [sweep-7-1] 3650 pos 6.0% + 57040 neg 94.0% = 60690 sched 84.3% ret 11267
c [sweep-7-1] 6690177 steps 79 queries 5293.13 avg class size
c [sweep-7-1] 1131 decisions 59 SAT calls 174.34 avg env size
c [sweep-7-1] 60078 variables remain 84% (11821 retained 16%)
c [decomp-26] removed 132 variables
c [sweep-7-1] removed 132 vars (0 failed, 26 eqs, 32 impls)
c [sweep-7] removed 132 vars in TOTAL (1 rounds, 78 queries)
c [phase-count-11] 462084 negative 98.9% of 467458 except 5374 1.1%
c [phase-count-11] 362326 positive 77.5% of 467458 except 105132 22.5%
c [phase-count-11] skipping relative phase luck test
c [phase-11] phase bias: 329 positive 100%, 0 negative 0%
c [sort-queue-11] sorted 25510 enqueued variables after 48296 conflicts
c [score-dist-11] active 46315 (64%), one 0 (0%), zero 25510 (36%)
c [score-dist-11] max exp 517, different 11 (2%)
c [score-dist-11] median active exp 517, avg 516.6
c [simplification-11] removed 4451 variables 5.8% (71825 remain 29%)
c [simplification-11] removed 41191 irredundant clauses 8.1% (467458 remain 34%)
c [simplification-11] maximum reduction of 8% = max (6%, 8%)
c [simplification-11] large reduction 8% >= 5% limit
c [simplification-11] next conflict interval 2000 = 2000/1
c [simplification-11] penalized conflict interval 2000 = 1 * 2000
c [simplification-11] hard conflict limit 60296 (soft 50296 + delta 10000)
c [simplification-11] new conflict limit 50296 (hard 60296)
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  134.1   71824   467458     48319   18603   1460 230970   81   324   54  25%      4  166   63   31  203%
c i  134.1   71770   467458     48338   18620   1460 230970   81   324   57  25%      4  166   67   31  216%
c i  134.7   71765   467458     48667   18905   1472 230978   80   321   59  25%      3  162   67   31  216%
c i  135.7   71762   467458     49221   19392   1481 230984   81   324   59  25%      3  163   84   32  267%
c i  137.2   71755   467458     50114   20162   1509 231017   79   325   59  24%      5  162   61   32  190%
c 
c [simplification-12] limit 50296 conflicts (hard 60296) hit after 50298 conflicts
c [quatres-7] found 31355 quaternary clauses 39% in total
c [quatres-7-1] removed 2 duplicate quaternary clauses
c [quatres-7-2] added 2 single-self-subsuming ternary resolvents
c [quatres-7-2] added 5 quaternary resolvents
c [ternres-8] limit 23000297 with penalty 0 = 0 + 0
c [ternres-8] all 71755 free variables schedulable
c [ternres-8] 386 ternary resolvents (0 bin, 386 trn)
c [ternres-8] fully completed ternary resolution
c [decomp-27] removed 75 variables
c [simpleprobe-5] 1581 schedulable variables 2%
c [simpleprobe-5] limit 92001189 penalty 0 = 0 + 0
c [decomp-28] removed 1501 variables
c [simpleprobe-5] fully completed simple probing
c [simpleprobe-5] removed 1501 variables, found 81409 hbrs, 754 units
c [unhide-12] limit 4600059 with penalty 0 = 0 + 0
c [unhide-12-13] 19 units, 322 failed, 61359 tauts, 0 hbrs, 58151 literals
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 252 transitive binary clauses
c [transred-8] found 1 units
c [cce-4] boosting limit by 10
c [cce-4] limit of 575007435 steps penalty 1 = 1 + 0
c [cce-4-1] eliminated 27 clauses out of 796 (3%) of length 7
c [cce-4-1] eliminated 2891 clauses out of 5223 (55%) of length 6
c [cce-4-1] eliminated 25449 clauses out of 36714 (69%) of length 5
c [cce-4-1] eliminated 14710 clauses out of 29471 (50%) of length 4
c [cce-4-1] incomplete large round (ATE)
c [cce-4-1] eliminated 43077 large clauses in 575007443 steps
c [cce-4-1] allowing another 287503721 steps for small clauses
c [cce-4-1] scheduling 348380 clauses = 232482 binary + 115898 ternary
c [cce-4-1] tried to eliminate 12732 small clauses 4%
c [cce-4-1] eliminated 2071 binary clauses 1%
c [cce-4-1] eliminated 790 ternary clauses 1%
c [cce-4-1] eliminated 2861 small clauses 1%
c [cce-4-1] eliminated 3311 small clauses in 575007439 steps
c [cce-4-1] incomplete small round (ATE)
c [cce-4-1] eliminated 46388 covered clauses in round 1
c [cce-4] eliminated 46388 covered clauses in TOTAL during 1 rounds
c [elim-10] no untried remaining variables left
c [elim-10] scheduled 69896 variables 100%
c [elim-10] limit of 460005948 steps penalty 0 = 0 + 0
c [elim-10] rescheduling of touched variables disabled
c [elim-10-1] eliminated 18394 variables 26% in round 1 in 33729082 steps
c [elim-10-1] backward subsumption/strengthening limit 33729000
c [elim-10-1-1] backward checking 38830 touched variables 56%
c [elim-10-1-1] fully completed backward checking in 1 rounds
c [elim-10-1] subsumed 28 and strengthened 62 clauses in 5550987 steps
c [elim-10-1] rescheduled 221 variables 0% by backward subsumption
c [elim-10-2] eliminated 13 variables 0% in round 2 in 212604 steps
c [elim-10-2] backward subsumption/strengthening limit 212600
c [elim-10-2-1] backward checking 168 touched variables 0%
c [elim-10-2-1] incomplete backward checking 0 remain 0%
c [elim-10-2] subsumed 12 and strengthened 5 clauses in 212601 steps
c [elim-10-2] rescheduled 34 variables 0% by backward subsumption
c [elim-10-3] eliminated 1 variables 0% in round 3 in 124604 steps
c [elim-10-3] backward subsumption/strengthening limit 124600
c [elim-10-3-1] backward checking 9 touched variables 0%
c [elim-10-3-1] incomplete backward checking 0 remain 0%
c [elim-10-3] subsumed 3 and strengthened 0 clauses in 124601 steps
c [elim-10] incomplete 7 not tried 0% in round 3
c [elim-10] transition to [ all 1 rem 1 ] state
c [elim-10] eliminated 18409 = 26% variables out of 69896 scheduled
c [bca-8] limit of 10000000 steps and 712693 added (scaled 2)
c [bca-8] 92060 out of 102976 literals actually usable 89%
c [bca-8] added 309 blocked clauses in 221963 steps
c [sweep-8] limit 6900089 penalty 0 = 0 + 0
c [sweep-8-1] 3854 pos 8.8% + 40102 neg 91.2% = 43956 sched 85.4% ret 7531
c [sweep-8-1] 6946266 steps 149 queries 3889.21 avg class size
c [sweep-8-1] 1337 decisions 130 SAT calls 81.12 avg env size
c [sweep-8-1] 42619 variables remain 83% (8779 retained 17%)
c [decomp-29] removed 165 variables
c [sweep-8-1] removed 165 vars (0 failed, 28 eqs, 36 impls)
c [sweep-8] removed 165 vars in TOTAL (1 rounds, 148 queries)
c [phase-count-12] 353944 negative 99.7% of 354883 except 939 0.3%
c [phase-count-12] 254985 positive 71.9% of 354883 except 99898 28.1%
c [phase-count-12] skipping relative phase luck test
c [phase-12] phase bias: 1 positive 1%, 152 negative 99%
c [sort-queue-12] sorted 14967 enqueued variables after 50298 conflicts
c [score-dist-12] active 36355 (71%), one 0 (0%), zero 14967 (29%)
c [score-dist-12] max exp 517, different 11 (2%)
c [score-dist-12] median active exp 517, avg 516.7
c [simplification-12] removed 20433 variables 28.5% (51322 remain 21%)
c [simplification-12] removed 112575 irredundant clauses 24.1% (354883 remain 26%)
c [simplification-12] maximum reduction of 28% = max (28%, 24%)
c [simplification-12] large reduction 28% >= 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 62298 (soft 52298 + delta 10000)
c [simplification-12] new conflict limit 52298 (hard 62298)
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  160.2   51321   354883     50375    4712   2221 223147   77   324   38  24%      4  160   50   32  154%
c i  160.3   51318   354883     50557    4875   2223 223153   75   321   38  23%      3  157   41   32  128%
c 
c [simplification-13] limit 52298 conflicts (hard 62298) hit after 52299 conflicts
c [quatres-8] found 25132 quaternary clauses 55% in total
c [quatres-8-1] removed 1 duplicate quaternary clauses
c [quatres-8-2] added 1 single-self-subsuming ternary resolvents
c [quatres-8-2] added 7 quaternary resolvents
c [ternres-9] limit 23338413 with penalty 0 = 0 + 0
c [ternres-9] all 51317 free variables schedulable
c [ternres-9] 857 ternary resolvents (0 bin, 857 trn)
c [ternres-9] fully completed ternary resolution
c [decomp-30] removed 5 variables
c [treelook-5] limit 2333841 penalty 0 = 0 + 0 boost 1
c [treelook-5] scheduled 66490 literals 65%
c [treelook-5] scheduling used 1007573 steps
c [treelook-5] scheduled completely
c [treelook-5] limit 2333841 penalty 0 = 0 + 0 boost 1
c [treelook-5] used 2420958 steps
c [treelook-5] 66438 literals remain 65%
c [treelook-5] 7247 variables remain to probed next time 14%
c [treelook-5] removed 12 variables, found 16232 hbrs
c [unhide-13] limit 4667682 with penalty 0 = 0 + 0
c [unhide-13-16] 8 units, 238 failed, 31890 tauts, 0 hbrs, 22683 literals
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 323 transitive binary clauses
c [transred-9] found 2 units
c [cce-5] limit of 116692066 steps penalty 0 = 0 + 0
c [cce-5-1] eliminated 5 clauses out of 35 (14%) of length 7
c [cce-5-1] eliminated 435 clauses out of 3580 (12%) of length 6
c [cce-5-1] eliminated 381 clauses out of 14846 (3%) of length 5
c [cce-5-1] incomplete large round (ACCE)
c [cce-5-1] eliminated 821 large clauses in 116692068 steps
c [cce-5-1] allowing another 58346034 steps for small clauses
c [cce-5-1] scheduling 194817 clauses = 173774 binary + 21043 ternary
c [cce-5-1] tried to eliminate 4393 small clauses 2%
c [cce-5-1] eliminated 1248 binary clauses 1%
c [cce-5-1] eliminated 248 ternary clauses 1%
c [cce-5-1] eliminated 1496 small clauses 1%
c [cce-5-1] eliminated 1551 small clauses in 116692073 steps
c [cce-5-1] incomplete small round (ACCE)
c [cce-5-1] eliminated 2372 covered clauses in round 1
c [cce-5] eliminated 2372 covered clauses in TOTAL during 1 rounds
c [cce-5] 2372 < 1/100 * 347909 = 3479 considered unsuccessful
c [elim-11] no untried remaining variables left
c [elim-11] scheduled 51096 variables 100%
c [elim-11] limit of 466768265 steps penalty 0 = 0 + 0
c [elim-11] rescheduling of touched variables disabled
c [elim-11-1] eliminated 665 variables 1% in round 1 in 29472045 steps
c [elim-11-1] backward subsumption/strengthening limit 29472000
c [elim-11-1-1] backward checking 4196 touched variables 8%
c [elim-11-1-1] fully completed backward checking in 1 rounds
c [elim-11-1] subsumed 5 and strengthened 21 clauses in 1014837 steps
c [elim-11-1] rescheduled 70 variables 0% by backward subsumption
c [elim-11-2] eliminated 1 variables 0% in round 2 in 35473 steps
c [elim-11-2] backward subsumption/strengthening limit 35400
c [elim-11-2-1] backward checking 22 touched variables 0%
c [elim-11-2-1] incomplete backward checking 0 remain 0%
c [elim-11-2] subsumed 0 and strengthened 2 clauses in 35401 steps
c [elim-11-2] rescheduled 8 variables 0% by backward subsumption
c [elim-11-3] eliminated 1 variables 0% in round 3 in 8293 steps
c [elim-11-3] backward subsumption/strengthening limit 8200
c [elim-11-3-1] backward checking 10 touched variables 0%
c [elim-11-3-1] incomplete backward checking 0 remain 0%
c [elim-11-3] subsumed 0 and strengthened 2 clauses in 8222 steps
c [elim-11] incomplete 8 not tried 0% in round 3
c [elim-11] transition to [ all 1 rem 1 ] state
c [elim-11] eliminated 667 = 1% variables out of 51096 scheduled
c [bca-9] limit of 10000000 steps and 689514 added (scaled 2)
c [bca-9] 87956 out of 100860 literals actually usable 87%
c [bca-9] added 76 blocked clauses in 213543 steps
c [sweep-9] limit 7001523 penalty 0 = 0 + 0
c [sweep-9-1] 3757 pos 9.0% + 38149 neg 91.0% = 41906 sched 83.1% ret 8523
c [sweep-9-1] 7137158 steps 126 queries 2520.40 avg class size
c [sweep-9-1] 1576 decisions 119 SAT calls 131.16 avg env size
c [sweep-9-1] 40915 variables remain 81% (9442 retained 19%)
c [decomp-32] removed 104 variables
c [sweep-9-1] removed 104 vars (0 failed, 16 eqs, 21 impls)
c [sweep-9] removed 104 vars in TOTAL (1 rounds, 125 queries)
c [phase-count-13] 342758 negative 99.7% of 343666 except 908 0.3%
c [phase-count-13] 247069 positive 71.9% of 343666 except 96597 28.1%
c [phase-count-13] skipping relative phase luck test
c [phase-13] phase bias: 9 positive 100%, 0 negative 0%
c [sort-queue-13] sorted 14112 enqueued variables after 52299 conflicts
c [score-dist-13] active 36213 (72%), one 0 (0%), zero 14112 (28%)
c [score-dist-13] max exp 517, different 11 (2%)
c [score-dist-13] median active exp 517, avg 516.7
c [simplification-13] removed 992 variables 1.9% (50325 remain 20%)
c [simplification-13] removed 11217 irredundant clauses 3.2% (343666 remain 25%)
c [simplification-13] maximum reduction of 3% = max (2%, 3%)
c [simplification-13] geometric conflict interval increment 5000 = 20000 / 4
c [simplification-13] new conflict interval 22000
c [simplification-13] penalized conflict interval 22000 = 1 * 22000
c [simplification-13] hard conflict limit 85299 (soft 74299 + delta 11000)
c [simplification-13] new conflict limit 74299 (hard 85299)
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  168.2   50324   343666     52468    6439   2899 212631   57   292   46  19%     15  123   18   32   58%
c i  168.3   50323   343666     52896    6837   2913 212635   55   301   46  18%     11  132   31   32   97%
c i  168.7   50310   343666     53732    7566   2943 212663   50   285   47  18%      8  114   28   32   87%
c i  169.1   50309   343666     54604    8362   2955 212675   47   285   47  17%      7  113   40   32  126%
c i  169.2   50307   343666     54645    8398   2955 212675   47   285   47  17%      6  112   37   32  116%
c i  169.3   50304   343666     54805    8528   2960 212687   47   282   47  17%      5  110   39   32  122%
c i  169.3   50303   343666     54898    8608   2969 212689   47   284   47  16%      5  111   37   32  116%
c i  169.6   50302   343666     55405    9042   2979 212705   43   263   48  16%      4   90   17   32   52%
c i  170.1   50301   343666     56024    9606   2992 212717   46   281   49  16%      4  107   53   32  165%
c i  170.3   50300   343666     56271    9826   2994 212720   46   281   49  16%      3  106   52   32  162%
c i  170.6   50299   343666     56676   10196   2994 212724   48   284   49  17%      2  108   67   33  206%
c i  170.7   50137   343666     56775   10287   2994 212725   48   285   50  17%      2  109   65   33  201%
c i  171.3   50064   343666     57456   10894   3015 212744   51   292   50  18%      3  116   67   33  205%
c i  171.7   50063   343666     57921   11301   3020 212754   56   293   51  19%      2  116   72   33  217%
c i  172.5   50051   343666     58823   12121   3025 212776   58   301   51  19%      4  122   69   34  205%
c i  172.8   50050   343666     59182   12448   3027 212783   58   293   51  20%      3  113   67   34  196%
c i  173.6   50049   343666     60143   13320   3044 212798   54   270   53  20%      5   88   41   34  122%
c i  175.1   50048   343666     61812   14767   3078 212836   52   244   55  21%     12   61   36   34  105%
c i  175.4   50047   343666     62166   15083   3084 212838   52   241   55  22%      9   57   44   34  129%
c i  175.4   50046   343666     62167   15083   3084 212838   52   241   55  22%      9   57   44   34  128%
c i  175.7   50043   343666     62608   15455   3099 212846   50   232   56  21%      6   48   29   34   84%
c i  176.1   50042   343666     63143   15940   3103 212849   47   218   56  22%      4   33   22   34   64%
c i  176.1   50040   343666     63214   16002   3104 212849   46   215   56  22%      4   30   20   34   59%
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  176.2   50039   343666     63281   16059   3104 212849   47   214   56  22%      4   30   31   34   90%
c i  176.9   50038   343666     64033   16698   3119 212860   51   225   56  23%      4   40   73   35  210%
c i  178.8   50035   343666     66160   18592   3149 212892   53   228   57  23%     17   42   56   35  158%
c i  178.9   50032   343666     66304   18725   3149 212894   54   235   57  23%     15   49   73   36  205%
c i  179.0   50011   343666     66396   18806   3150 212896   55   237   58  23%     13   51   76   36  213%
c i  179.3   50008   343666     66669   19048   3150 212897   58   247   58  24%     10   61   94   36  262%
c i  179.3   50007   343666     66673   19050   3150 212897   58   247   58  24%     10   61   95   36  263%
c i  179.5   49998   343666     66833   19185   3152 212899   61   253   59  24%      8   67  112   36  310%
c i  179.8   49997   343666     67078   19398   3154 212900   63   254   59  25%      6   67   92   36  253%
c i  180.1   49996   343666     67389   19669   3157 212907   63   251   60  25%      4   64   75   37  205%
c i  180.6   49995   343666     67905   20111   3163 212914   64   250   60  26%      3   62   85   37  230%
c i  181.0   49992   343666     68371   20496   3169 212914   68   253   64  27%      2   65  112   37  300%
c i  181.1   49983   343666     68457   20578   3170 212914   68   252   64  27%      2   64   91   37  245%
c i  181.1   49966   343666     68488   20606   3171 212914   67   251   64  27%      2   63   85   37  229%
c i  181.3   49965   343666     68701   20795   3175 212916   67   249   64  27%      1   60   68   37  184%
c i  181.7   49964   343666     69047   21111   3178 212920   65   246   64  26%      1   57   53   37  141%
c i  181.7   49962   343666     69048   21111   3178 212920   65   246   64  26%      1   57   52   37  140%
c i  182.8   49937   343666     70199   22127   3192 212935   67   247   64  27%      5   57   95   38  249%
c i  183.2   49936   343666     70535   22434   3196 212938   68   248   65  28%      4   58   94   38  245%
c i  183.8   49933   343666     71125   22958   3202 212943   67   239   66  28%      3   49   60   38  155%
c i  184.8   49932   343666     72029   23783   3213 212957   67   244   66  28%      4   53   68   39  175%
c i  184.8   49931   343666     72096   23836   3214 212958   68   244   66  28%      4   53   78   39  201%
c i  184.8   49930   343666     72097   23836   3214 212958   68   244   66  28%      4   53   78   39  200%
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  185.1   49929   343666     72358   24072   3217 212962   67   241   66  28%      3   49   64   39  164%
c i  186.0   49927   343666     73315   24926   3225 212975   68   243   66  28%      4   51   84   39  214%
c i  187.0   49926   343666     74211   25726   3242 212991   67   242   67  28%      5   50   64   40  161%
c i  187.0   49894   343666     74285   25796   3243 212992   66   240   67  28%      4   47   55   40  139%
c 
c [simplification-14] limit 74331 conflicts (hard 85299) hit after 74331 conflicts
c [quatres-9] found 23987 quaternary clauses 54% in total
c [quatres-9-2] added 2 single-self-subsuming ternary resolvents
c [quatres-9-2] added 17 quaternary resolvents
c [ternres-10] limit 28236782 with penalty 0 = 0 + 0
c [ternres-10] all 49894 free variables schedulable
c [ternres-10] 383 ternary resolvents (0 bin, 383 trn)
c [ternres-10] fully completed ternary resolution
c [gauss-4] limit 705919 penalty 3 = 3 + 0
c [gauss-4] extracted 21 xors of average arity 2.5
c [gauss-4] connected 53 occurrences of 30 variables (average 1.8)
c [gauss-4] limit 705919 penalty 3 = 3 + 0
c [gauss-4] fully completed
c [gauss-4] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-33] removed 35 variables
c [basicprobe-5] limit 141183914 penalty 0 = 0 + 0
c [basicprobe-5-0] 10647 probes remain 22% after last round
c [basicprobe-5-0] 792 units = 768 failed (97%) + 24 lifted (3%)
c [basicprobe-5-0] removed 1307 variables, found 222055 hbrs
c [bate-3] eliminated 1120 asymmetric tautologies during probing
c [unhide-14] limit 2823678 with penalty 1 = 0 + 1
c [unhide-14-18] 14 units, 291 failed, 51597 tauts, 0 hbrs, 330927 literals
c [transred-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 243 transitive binary clauses
c [transred-10] found 1 units
c [elim-12] no untried remaining variables left
c [elim-12] scheduled 48296 variables 100%
c [elim-12] limit of 564735657 steps penalty 0 = 0 + 0
c [elim-12] rescheduling of touched variables disabled
c [elim-12-1] eliminated 1155 variables 2% in round 1 in 26763427 steps
c [elim-12-1] backward subsumption/strengthening limit 26763400
c [elim-12-1-1] backward checking 6086 touched variables 13%
c [elim-12-1-1] fully completed backward checking in 1 rounds
c [elim-12-1] subsumed 15 and strengthened 35 clauses in 1551621 steps
c [elim-12-1] rescheduled 138 variables 0% by backward subsumption
c [elim-12-2] eliminated 12 variables 0% in round 2 in 68027 steps
c [elim-12-2] backward subsumption/strengthening limit 68000
c [elim-12-2-1] backward checking 132 touched variables 0%
c [elim-12-2-1] incomplete backward checking 0 remain 0%
c [elim-12-2] subsumed 6 and strengthened 12 clauses in 68001 steps
c [elim-12-2] rescheduled 57 variables 0% by backward subsumption
c [elim-12-3] eliminated 5 variables 0% in round 3 in 44278 steps
c [elim-12-3] backward subsumption/strengthening limit 44200
c [elim-12-3-1] backward checking 55 touched variables 0%
c [elim-12-3-1] incomplete backward checking 0 remain 0%
c [elim-12-3] subsumed 0 and strengthened 10 clauses in 44201 steps
c [elim-12] incomplete 39 not tried 0% in round 3
c [elim-12] transition to [ all 1 rem 1 ] state
c [elim-12] eliminated 1173 = 2% variables out of 48296 scheduled
c [bca-10] limit of 10000000 steps and 637644 added (scaled 2)
c [bca-10] 75621 out of 94248 literals actually usable 80%
c [bca-10] added 91 blocked clauses in 199926 steps
c [sweep-10] limit 8471034 penalty 0 = 0 + 0
c [sweep-10-1] 3483 pos 9.0% + 35082 neg 91.0% = 38565 sched 81.8% ret 8558
c [sweep-10-1] 8596360 steps 147 queries 1588.73 avg class size
c [sweep-10-1] 3512 decisions 132 SAT calls 234.46 avg env size
c [sweep-10-1] 36966 variables remain 79% (10045 retained 21%)
c [decomp-34] removed 159 variables
c [sweep-10-1] removed 159 vars (0 failed, 22 eqs, 26 impls)
c [sweep-10] removed 159 vars in TOTAL (1 rounds, 146 queries)
c [phase-count-14] 316597 negative 99.7% of 317494 except 897 0.3%
c [phase-count-14] 225429 positive 71.0% of 317494 except 92065 29.0%
c [phase-count-14] skipping relative phase luck test
c [phase-14] phase bias: 2 positive 10%, 19 negative 90%
c [sort-queue-14] sorted 11453 enqueued variables after 74331 conflicts
c [score-dist-14] active 35511 (76%), one 0 (0%), zero 11453 (24%)
c [score-dist-14] max exp 518, different 11 (2%)
c [score-dist-14] median active exp 518, avg 517.4
c [simplification-14] removed 2930 variables 5.9% (46964 remain 19%)
c [simplification-14] removed 26172 irredundant clauses 7.6% (317494 remain 23%)
c [simplification-14] maximum reduction of 8% = max (6%, 8%)
c [simplification-14] large reduction 8% >= 5% limit
c [simplification-14] next conflict interval 2000 = 2000/1
c [simplification-14] penalized conflict interval 2000 = 1 * 2000
c [simplification-14] hard conflict limit 86331 (soft 76331 + delta 10000)
c [simplification-14] new conflict limit 76331 (hard 86331)
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  197.0   46963   317494     74728   24166   3590 345688   69   242   70  28%      3   49   82   40  204%
c i  197.3   46962   317494     75044   24440   3596 345693   70   249   70  28%      2   56   89   40  220%
c i  197.3   46961   317494     75045   24440   3596 345693   70   249   70  28%      2   56   88   40  220%
c i  197.3   46960   317494     75046   24440   3596 345693   70   249   70  28%      2   56   88   40  219%
c i  197.3   46956   317494     75047   24440   3596 345693   70   249   70  28%      2   56   88   40  218%
c i  197.6   46953   317494     75329   24677   3602 345700   68   245   70  28%      1   52   54   40  135%
c i  197.9   46952   317494     75630   24943   3608 345703   68   243   70  28%      1   49   59   40  146%
c i  198.0   46947   317494     75742   25025   3608 345705   69   243   70  28%      0   49   80   40  197%
c i  198.1   46946   317494     75800   25071   3608 345706   70   242   70  29%      0   48   88   41  217%
c 
c [simplification-15] limit 76361 conflicts (hard 86331) hit after 76361 conflicts
c [quatres-10] found 22658 quaternary clauses 53% in total
c [quatres-10-1] removed 6 duplicate quaternary clauses
c [quatres-10-2] added 2 single-self-subsuming ternary resolvents
c [quatres-10-2] added 3 quaternary resolvents
c [ternres-11] limit 28723739 with penalty 0 = 0 + 0
c [ternres-11] all 46946 free variables schedulable
c [ternres-11] 1265 ternary resolvents (0 bin, 1265 trn)
c [ternres-11] fully completed ternary resolution
c [card-5] limit 897616 penalty 4 = 4 + 0
c [card-5] found 1934 at-most-one constraints of average size 4.1
c [card-5] no at-most-two constraint found
c [card-5] using previous limit 897616 for elimination
c [card-5] 1934 out of 1934 constraints (100%) meet size limits
c [card-5] no units found
c [card-5] no at-most-one constraints generated
c [decomp-35] removed 26 variables
c [simpleprobe-6] all 46938 free variables schedulable
c [simpleprobe-6] limit 114894956 penalty 0 = 0 + 0
c [decomp-36] removed 856 variables
c [simpleprobe-6] fully completed simple probing
c [simpleprobe-6] removed 856 variables, found 108521 hbrs, 382 units
c [unhide-15] limit 5744747 with penalty 0 = 0 + 0
c [unhide-15-21] 4 units, 86 failed, 58321 tauts, 0 hbrs, 93693 literals
c [transred-11] limit 2000000 with penalty 0 = 0 + 0
c [transred-11] removed 419 transitive binary clauses
c [block-5] scheduling all variables this time
c [block-5] scheduled 45898 variables 100%
c [block-5] limit of 35904673 steps penalty 3 = 3 + 0
c [block-5] fully completed
c [block-5] transition to [ all 0 rem 0 ] state
c [block-5] eliminated 433 blocked clauses
c [block-5] 433 < 1/100 * 303370 = 3033 considered unsuccessful
c [cce-6] limit of 71809347 steps penalty 1 = 1 + 0
c [cce-6-1] eliminated 2 clauses out of 4 (50%) of length 22
c [cce-6-1] eliminated 4 clauses out of 4 (100%) of length 18
c [cce-6-1] eliminated 4 clauses out of 5 (80%) of length 14
c [cce-6-1] eliminated 5 clauses out of 8 (62%) of length 10
c [cce-6-1] eliminated 2 clauses out of 5 (40%) of length 8
c [cce-6-1] eliminated 16 clauses out of 55 (29%) of length 7
c [cce-6-1] eliminated 15 clauses out of 2836 (1%) of length 6
c [cce-6-1] eliminated 3 clauses out of 14028 (0%) of length 5
c [cce-6-1] incomplete large round (ATE)
c [cce-6-1] eliminated 51 large clauses in 71809355 steps
c [cce-6-1] allowing another 35904677 steps for small clauses
c [cce-6-1] scheduling 246031 clauses = 159362 binary + 86669 ternary
c [cce-6-1] tried to eliminate 2411 small clauses 1%
c [cce-6-1] eliminated 374 binary clauses 0%
c [cce-6-1] eliminated 162 ternary clauses 0%
c [cce-6-1] eliminated 536 small clauses 0%
c [cce-6-1] eliminated 536 small clauses in 71809361 steps
c [cce-6-1] incomplete small round (ATE)
c [cce-6-1] eliminated 587 covered clauses in round 1
c [cce-6] eliminated 587 covered clauses in TOTAL during 1 rounds
c [cce-6] 587 < 1/100 * 302898 = 3028 considered unsuccessful
c [elim-13] no untried remaining variables left
c [elim-13] scheduled 45898 variables 100%
c [elim-13] almost no limit of 100000000000 steps
c [elim-13] rescheduling of touched variables disabled
c [elim-13-1] eliminated 872 variables 2% in round 1 in 25082588 steps
c [elim-13-1] backward subsumption/strengthening limit 25082500
c [elim-13-1-1] backward checking 5170 touched variables 11%
c [elim-13-1-1] fully completed backward checking in 1 rounds
c [elim-13-1] subsumed 1 and strengthened 17 clauses in 1211578 steps
c [elim-13-1] rescheduled 53 variables 0% by backward subsumption
c [elim-13-2] eliminated 4 variables 0% in round 2 in 85133 steps
c [elim-13-2] backward subsumption/strengthening limit 85100
c [elim-13-2-1] backward checking 48 touched variables 0%
c [elim-13-2-1] fully completed backward checking in 1 rounds
c [elim-13-2] subsumed 0 and strengthened 6 clauses in 63741 steps
c [elim-13-2] rescheduled 24 variables 0% by backward subsumption
c [elim-13-3] eliminated 1 variables 0% in round 3 in 19717 steps
c [elim-13-3] backward subsumption/strengthening limit 19700
c [elim-13-3-1] backward checking 14 touched variables 0%
c [elim-13-3-1] incomplete backward checking 0 remain 0%
c [elim-13-3] subsumed 0 and strengthened 2 clauses in 19701 steps
c [elim-13] incomplete 8 not tried 0% in round 3
c [elim-13] transition to [ all 1 rem 1 ] state
c [elim-13] eliminated 877 = 2% variables out of 45898 scheduled
c [bca-11] limit of 10000000 steps and 603715 added (scaled 2)
c [bca-11] 71573 out of 90044 literals actually usable 79%
c [bca-11] added 63 blocked clauses in 191253 steps
c [sweep-11] boosting sweeping limit by 10
c [sweep-11] limit 86171210 penalty 0 = 0 + 0
c [sweep-11-1] 3444 pos 9.7% + 32232 neg 90.3% = 35676 sched 79.2% ret 9345
c [sweep-11-1] 86204355 steps 2009 queries 214.83 avg class size
c [sweep-11-1] 22574 decisions 1840 SAT calls 98.55 avg env size
c [sweep-11-1] 16432 variables remain 37% (28167 retained 63%)
c [decomp-37] removed 871 variables
c [sweep-11-1] removed 871 vars (0 failed, 215 eqs, 361 impls)
c [sweep-11] removed 871 vars in TOTAL (1 rounds, 2008 queries)
c [phase-count-15] 296864 negative 99.7% of 297742 except 878 0.3%
c [phase-count-15] 208072 positive 69.9% of 297742 except 89670 30.1%
c [phase-count-15] skipping relative phase luck test
c [phase-15] phase bias: 1 positive 100%, 0 negative 0%
c [sort-queue-15] sorted 7921 enqueued variables after 76361 conflicts
c [score-dist-15] active 36229 (82%), one 0 (0%), zero 7921 (18%)
c [score-dist-15] max exp 518, different 10 (2%)
c [score-dist-15] median active exp 518, avg 517.7
c [simplification-15] removed 2796 variables 6.0% (44150 remain 18%)
c [simplification-15] removed 19752 irredundant clauses 6.2% (297742 remain 22%)
c [simplification-15] maximum reduction of 6% = max (6%, 6%)
c [simplification-15] large reduction 6% >= 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 88361 (soft 78361 + delta 10000)
c [simplification-15] new conflict limit 78361 (hard 88361)
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  212.5   44149   297742     76980   25360   4461 395473   68   236   69  29%      5   42   62   41  152%
c i  213.1   44148   297742     77620   25930   4463 395478   70   241   69  29%      4   46   71   41  173%
c i  213.4   44145   297742     77841   26140   4463 395480   69   241   69  29%      3   46   67   41  161%
c 
c [simplification-16] limit 78361 conflicts (hard 88361) hit after 78362 conflicts
c [quatres-11] found 20520 quaternary clauses 50% in total
c [quatres-11-2] added 3 single-self-subsuming ternary resolvents
c [quatres-11-2] added 7 quaternary resolvents
c [ternres-12] limit 29171905 with penalty 0 = 0 + 0
c [ternres-12] all 44145 free variables schedulable
c [ternres-12] 1530 ternary resolvents (1 bin, 1529 trn)
c [ternres-12] fully completed ternary resolution
c [decomp-38] removed 8 variables
c [treelook-6] limit 2917190 penalty 0 = 0 + 0 boost 1
c [treelook-6] scheduled 56416 literals 64%
c [treelook-6] scheduling used 975570 steps
c [treelook-6] scheduled completely
c [treelook-6] limit 2917190 penalty 0 = 0 + 0 boost 1
c [treelook-6] used 2957060 steps
c [treelook-6] 56361 literals remain 64%
c [treelook-6] 5771 variables remain to probed next time 13%
c [treelook-6] removed 3 variables, found 21098 hbrs
c [unhide-16] limit 5834381 with penalty 0 = 0 + 0
c [unhide-16-24] 15 units, 260 failed, 69050 tauts, 0 hbrs, 92474 literals
c [transred-12] limit 2000000 with penalty 0 = 0 + 0
c [transred-12] removed 360 transitive binary clauses
c [transred-12] found 1 units
c [elim-14] no untried remaining variables left
c [elim-14] scheduled 43923 variables 100%
c [elim-14] limit of 583438112 steps penalty 0 = 0 + 0
c [elim-14] rescheduling of touched variables disabled
c [elim-14-1] eliminated 307 variables 1% in round 1 in 23989165 steps
c [elim-14-1] backward subsumption/strengthening limit 23989100
c [elim-14-1-1] backward checking 2133 touched variables 5%
c [elim-14-1-1] fully completed backward checking in 1 rounds
c [elim-14-1] subsumed 3 and strengthened 15 clauses in 677267 steps
c [elim-14-1] rescheduled 57 variables 0% by backward subsumption
c [elim-14-2] eliminated 3 variables 0% in round 2 in 66475 steps
c [elim-14-2] backward subsumption/strengthening limit 66400
c [elim-14-2-1] backward checking 29 touched variables 0%
c [elim-14-2-1] fully completed backward checking in 1 rounds
c [elim-14-2] subsumed 3 and strengthened 2 clauses in 49731 steps
c [elim-14-2] rescheduled 13 variables 0% by backward subsumption
c [elim-14-3] no variable eliminated in round 3 in 9784 steps
c [elim-14] fully completed in 3 rounds
c [elim-14] transition to [ all 0 rem 0 ] state
c [elim-14] eliminated 311 = 1% variables out of 43923 scheduled
c [elim-14] 311 < 1/100 * 43923 = 439 considered unsuccessful
c [bca-12] limit of 10000000 steps and 584039 added (scaled 2)
c [bca-12] 66411 out of 87226 literals actually usable 76%
c [bca-12] added 64 blocked clauses in 178993 steps
c [sweep-12] limit 8751571 penalty 0 = 0 + 0
c [sweep-12-1] 1956 pos 12.2% + 14077 neg 87.8% = 16033 sched 36.8% ret 27579
c [sweep-12-1] 8767574 steps 224 queries 691.81 avg class size
c [sweep-12-1] 2663 decisions 210 SAT calls 89.71 avg env size
c [sweep-12-1] 15218 variables remain 35% (28385 retained 65%)
c [decomp-40] removed 35 variables
c [sweep-12-1] removed 35 vars (0 failed, 20 eqs, 35 impls)
c [sweep-12] 35 < 1/1000 * 43612 = 43 considered unsuccessful
c [sweep-12] removed 35 vars in TOTAL (1 rounds, 223 queries)
c [phase-count-16] 290393 negative 99.7% of 291210 except 817 0.3%
c [phase-count-16] 202395 positive 69.5% of 291210 except 88815 30.5%
c [phase-count-16] skipping relative phase luck test
c [phase-16] phase bias: 1 positive 100%, 0 negative 0%
c [sort-queue-16] sorted 7591 enqueued variables after 78362 conflicts
c [score-dist-16] active 35986 (83%), one 0 (0%), zero 7591 (17%)
c [score-dist-16] max exp 518, different 10 (2%)
c [score-dist-16] median active exp 518, avg 517.7
c [simplification-16] removed 568 variables 1.3% (43577 remain 18%)
c [simplification-16] removed 6532 irredundant clauses 2.2% (291210 remain 21%)
c [simplification-16] maximum reduction of 2% = max (1%, 2%)
c [simplification-16] geometric conflict interval increment 7333 = 22000 / 3
c [simplification-16] new conflict interval 29333
c [simplification-16] penalized conflict interval 29333 = 1 * 29333
c [simplification-16] hard conflict limit 122361 (soft 107695 + delta 14666)
c [simplification-16] new conflict limit 107695 (hard 122361)
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  220.1   43576   291210     79003   26918   5271 345310   64   224   69  29%      6   28   62   42  150%
c i  220.1   43575   291210     79005   26919   5271 345310   64   224   69  29%      6   28   62   42  148%
c i  221.1   43574   291210     80032   27833   5289 345322   68   232   70  29%      6   36   81   42  193%
c i  221.7   43573   291210     80565   28326   5294 345323   68   231   70  29%      4   35   59   42  139%
c i  221.9   43572   291210     80964   28693   5299 345325   63   220   70  29%      3   23   28   42   68%
c i  222.3   43571   291210     81386   29092   5300 345325   60   206   70  29%      2    9   29   42   70%
c i  222.6   43570   291210     81726   29394   5307 345333   61   212   70  29%      1   15   61   42  145%
c i  226.4   43569   291210     86939   34164   5330 345363   36    96   70  37%     60  -97   29   41   71%
c i  228.6   43566   291210     90262   37252   5357 345394   38   180   80  21%     32  -10   41   41  101%
c i  229.0   43565   291210     90818   37781   5360 345395   37   171   83  22%     18  -19   30   41   73%
c i  230.3   43562   291210     92187   38985   5378 345412   40   162   87  25%      9  -28   34   41   83%
c i  232.0   43559   291210     94068   40676   5390 345437   42   151   87  28%     11  -38   28   41   67%
c i  232.1   43558   291210     94136   40732   5391 345438   42   150   87  28%     10  -39   30   41   72%
c i  236.1   43429   291210     98719   44902   5423 345479   49   161   87  31%     47  -25   51   42  121%
c i  239.4   43428   291210    103108   49056   5438 345491   39   112   93  35%     43  -71   40   41   97%
c i  241.2   43427   291210    105023   50782   5457 345502   46   129   96  36%     14  -52   57   42  137%
c i  241.9   43426   291210    105646   51360   5459 345506   44   121   96  37%      5  -60   40   42   97%
c i  241.9   43425   291210    105653   51365   5459 345507   44   121   96  37%      5  -60   40   42   96%
c i  244.4   43423   291210    108618   54148   5468 345511   37   100  110  37%     21  -78   16   41   38%
c -  247.8   43423   291210    111735   23175   5492 345534   49   139   53  35%     23  -36   47   42  113%
c 
c [simplification-17] limit 107701 conflicts (hard 122361) hit after 122362 conflicts
c [quatres-12] found 20253 quaternary clauses 48% in total
c [quatres-12-2] added 4 single-self-subsuming ternary resolvents
c [quatres-12-2] added 2 quaternary resolvents
c [ternres-13] limit 37267992 with penalty 0 = 0 + 0
c [ternres-13] all 43423 free variables schedulable
c [ternres-13] 315 ternary resolvents (4 bin, 311 trn)
c [ternres-13] fully completed ternary resolution
c [decomp-41] removed 174 variables
c [basicprobe-6] limit 186339963 penalty 0 = 0 + 0
c [basicprobe-6-0] 253 probes remain 1% after last round
c [basicprobe-6-0] 1094 units = 1064 failed (97%) + 30 lifted (3%)
c [basicprobe-6-0] removed 1534 variables, found 299164 hbrs
c [bate-4] eliminated 886 asymmetric tautologies during probing
c [unhide-17] limit 7453598 with penalty 0 = 0 + 0
c [unhide-17-28] 4 units, 55 failed, 81469 tauts, 0 hbrs, 236995 literals
c [transred-13] limit 2000000 with penalty 0 = 0 + 0
c [transred-13] removed 296 transitive binary clauses
c [transred-13] found 2 units
c [bca-13] limit of 10000000 steps and 539337 added (scaled 2)
c [bca-13] 62909 out of 83592 literals actually usable 75%
c [bca-13] added 18 blocked clauses in 176565 steps
c [phase-count-17] 268177 negative 99.7% of 268995 except 818 0.3%
c [phase-count-17] 184029 positive 68.4% of 268995 except 84966 31.6%
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 6342 enqueued variables after 122362 conflicts
c [score-dist-17] active 35453 (85%), one 0 (0%), zero 6342 (15%)
c [score-dist-17] max exp 518, different 9 (2%)
c [score-dist-17] median active exp 518, avg 517.8
c [simplification-17] removed 1628 variables 3.7% (41795 remain 17%)
c [simplification-17] removed 22215 irredundant clauses 7.6% (268995 remain 20%)
c [simplification-17] maximum reduction of 8% = max (4%, 8%)
c [simplification-17] large reduction 8% >= 5% limit
c [simplification-17] next conflict interval 2000 = 2000/1
c [simplification-17] penalized conflict interval 2000 = 1 * 2000
c [simplification-17] hard conflict limit 134362 (soft 124362 + delta 10000)
c [simplification-17] new conflict limit 124362 (hard 134362)
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  266.9   41794   268995    124172   34576   5639 534018   30    66   72  45%    194  -93   32   40   80%
c 
c [simplification-18] limit 124362 conflicts (hard 134362) hit after 134364 conflicts
c [quatres-13] found 18677 quaternary clauses 46% in total
c [quatres-13-1] removed 2 duplicate quaternary clauses
c [quatres-13-2] added 1 quaternary resolvents
c [ternres-14] limit 39411775 with penalty 0 = 0 + 0
c [ternres-14] all 41768 free variables schedulable
c [ternres-14] 269 ternary resolvents (0 bin, 269 trn)
c [ternres-14] fully completed ternary resolution
c [decomp-42] removed 92 variables
c [simpleprobe-7] all 41703 free variables schedulable
c [simpleprobe-7] limit 157647102 penalty 0 = 0 + 0
c [decomp-43] removed 417 variables
c [simpleprobe-7] fully completed simple probing
c [simpleprobe-7] removed 417 variables, found 146528 hbrs, 165 units
c [unhide-18] limit 3941177 with penalty 1 = 0 + 1
c [unhide-18-30] 1 units, 18 failed, 90557 tauts, 0 hbrs, 290937 literals
c [transred-14] limit 2000000 with penalty 0 = 0 + 0
c [transred-14] removed 502 transitive binary clauses
c [transred-14] found 1 units
c [cce-7] limit of 49264719 steps penalty 2 = 2 + 0
c [cce-7-1] eliminated 1 clauses out of 3 (33%) of length 26
c [cce-7-1] eliminated 1 clauses out of 3 (33%) of length 22
c [cce-7-1] eliminated 3 clauses out of 3 (100%) of length 18
c [cce-7-1] eliminated 2 clauses out of 3 (67%) of length 14
c [cce-7-1] eliminated 4 clauses out of 10 (40%) of length 10
c [cce-7-1] eliminated 1 clauses out of 6 (17%) of length 8
c [cce-7-1] eliminated 2 clauses out of 38 (5%) of length 7
c [cce-7-1] eliminated 13 clauses out of 2608 (0%) of length 6
c [cce-7-1] eliminated 4 clauses out of 12381 (0%) of length 5
c [cce-7-1] incomplete large round (ACCE)
c [cce-7-1] eliminated 31 large clauses in 49264727 steps
c [cce-7-1] allowing another 24632363 steps for small clauses
c [cce-7-1] scheduling 164475 clauses = 147490 binary + 16985 ternary
c [cce-7-1] tried to eliminate 2455 small clauses 1%
c [cce-7-1] eliminated 575 binary clauses 0%
c [cce-7-1] eliminated 119 ternary clauses 1%
c [cce-7-1] eliminated 694 small clauses 0%
c [cce-7-1] eliminated 1218 small clauses in 49264720 steps
c [cce-7-1] incomplete small round (ACCE)
c [cce-7-1] eliminated 1249 covered clauses in round 1
c [cce-7] eliminated 1249 covered clauses in TOTAL during 1 rounds
c [cce-7] 1249 < 1/100 * 263314 = 2633 considered unsuccessful
c [elim-15] scheduling all variables this time
c [elim-15] scheduled 40991 variables 100%
c [elim-15] limit of 394117757 steps penalty 1 = 1 + 0
c [elim-15] rescheduling of touched variables disabled
c [elim-15-1] eliminated 995 variables 2% in round 1 in 20531417 steps
c [elim-15-1] backward subsumption/strengthening limit 20531400
c [elim-15-1-1] backward checking 5618 touched variables 14%
c [elim-15-1-1] fully completed backward checking in 1 rounds
c [elim-15-1] subsumed 4 and strengthened 42 clauses in 1314025 steps
c [elim-15-1] rescheduled 135 variables 0% by backward subsumption
c [elim-15-2] eliminated 10 variables 0% in round 2 in 165789 steps
c [elim-15-2] backward subsumption/strengthening limit 165700
c [elim-15-2-1] backward checking 128 touched variables 0%
c [elim-15-2-1] fully completed backward checking in 1 rounds
c [elim-15-2] subsumed 0 and strengthened 11 clauses in 107376 steps
c [elim-15-2] rescheduled 43 variables 0% by backward subsumption
c [elim-15-3] eliminated 3 variables 0% in round 3 in 35814 steps
c [elim-15-3] backward subsumption/strengthening limit 35800
c [elim-15-3-1] backward checking 36 touched variables 0%
c [elim-15-3-1] incomplete backward checking 0 remain 0%
c [elim-15-3] subsumed 0 and strengthened 6 clauses in 35801 steps
c [elim-15] incomplete 24 not tried 0% in round 3
c [elim-15] transition to [ all 1 rem 1 ] state
c [elim-15] eliminated 1008 = 2% variables out of 40991 scheduled
c [bca-14] limit of 10000000 steps and 522310 added (scaled 2)
c [bca-14] 59957 out of 79968 literals actually usable 75%
c [bca-14] added 60 blocked clauses in 172864 steps
c [sweep-13] limit 5911766 penalty 1 = 1 + 0
c [sweep-13-1] 1684 pos 12.1% + 12273 neg 87.9% = 13957 sched 34.9% ret 26026
c [sweep-13-1] 6140757 steps 116 queries 1215.39 avg class size
c [sweep-13-1] 1674 decisions 108 SAT calls 143.57 avg env size
c [sweep-13-1] 13488 variables remain 34% (26395 retained 66%)
c [decomp-44] removed 121 variables
c [sweep-13-1] removed 121 vars (0 failed, 8 eqs, 17 impls)
c [sweep-13] removed 121 vars in TOTAL (1 rounds, 115 queries)
c [phase-count-18] 259201 negative 99.7% of 259995 except 794 0.3%
c [phase-count-18] 177257 positive 68.2% of 259995 except 82738 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 5717 enqueued variables after 134364 conflicts
c [score-dist-18] active 34145 (86%), one 0 (0%), zero 5717 (14%)
c [score-dist-18] max exp 519, different 10 (2%)
c [score-dist-18] median active exp 518, avg 518.2
c [simplification-18] removed 1906 variables 4.6% (39862 remain 16%)
c [simplification-18] removed 9000 irredundant clauses 3.3% (259995 remain 19%)
c [simplification-18] maximum reduction of 5% = max (5%, 3%)
c [simplification-18] large reduction 5% >= 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 146364 (soft 136364 + delta 10000)
c [simplification-18] new conflict limit 136364 (hard 146364)
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  284.1   39861   259995    135091   37246   5292 546523   30    76   77  40%    112  -71   47   38  123%
c 
c [simplification-19] limit 136364 conflicts (hard 146364) hit after 146366 conflicts
c [quatres-14] found 18536 quaternary clauses 46% in total
c [quatres-14-1] removed 2 duplicate quaternary clauses
c [quatres-14-2] added 1 single-self-subsuming ternary resolvents
c [quatres-14-2] added 5 quaternary resolvents
c [ternres-15] limit 41285799 with penalty 0 = 0 + 0
c [ternres-15] all 39859 free variables schedulable
c [ternres-15] 430 ternary resolvents (0 bin, 430 trn)
c [ternres-15] fully completed ternary resolution
c [gauss-5] limit 516072 penalty 4 = 4 + 0
c [gauss-5] extracted 12 xors of average arity 3.0
c [gauss-5] connected 36 occurrences of 36 variables (average 1.0)
c [gauss-5] limit 516072 penalty 4 = 4 + 0
c [gauss-5] fully completed
c [gauss-5] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-45] removed 2 variables
c [treelook-7] limit 4128579 penalty 0 = 0 + 0 boost 1
c [treelook-7] scheduled 49119 literals 62%
c [treelook-7] scheduling used 953873 steps
c [treelook-7] scheduled completely
c [treelook-7] limit 4128579 penalty 0 = 0 + 0 boost 1
c [treelook-7] used 4201688 steps
c [treelook-7] 48992 literals remain 61%
c [treelook-7] 4882 variables remain to probed next time 12%
c [treelook-7] removed 6 variables, found 26547 hbrs
c [unhide-19] limit 4128579 with penalty 1 = 0 + 1
c [unhide-19-32] 0 units, 48 failed, 59111 tauts, 0 hbrs, 533999 literals
c [transred-15] limit 2000000 with penalty 0 = 0 + 0
c [transred-15] removed 449 transitive binary clauses
c [elim-16] no untried remaining variables left
c [elim-16] scheduled 39819 variables 100%
c [elim-16] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-16] rescheduling of touched variables disabled
c [elim-16-1] eliminated 89 variables 0% in round 1 in 20025015 steps
c [elim-16-1] backward subsumption/strengthening limit 20025000
c [elim-16-1-1] backward checking 903 touched variables 2%
c [elim-16-1-1] fully completed backward checking in 1 rounds
c [elim-16-1] subsumed 1 and strengthened 10 clauses in 286928 steps
c [elim-16-1] rescheduled 33 variables 0% by backward subsumption
c [elim-16-2] eliminated 5 variables 0% in round 2 in 24311 steps
c [elim-16-2] backward subsumption/strengthening limit 24300
c [elim-16-2-1] backward checking 74 touched variables 0%
c [elim-16-2-1] incomplete backward checking 39 remain 53%
c [elim-16-2] subsumed 3 and strengthened 0 clauses in 24303 steps
c [elim-16-2] rescheduled 5 variables 0% by backward subsumption
c [elim-16-3] no variable eliminated in round 3 in 23450 steps
c [elim-16] fully completed in 3 rounds
c [elim-16] transition to [ all 0 rem 0 ] state
c [elim-16] eliminated 94 = 0% variables out of 39819 scheduled
c [elim-16] 94 < 1/100 * 39819 = 398 considered unsuccessful
c [bca-15] limit of 10000000 steps and 517858 added (scaled 2)
c [bca-15] 59014 out of 79452 literals actually usable 74%
c [bca-15] added 22 blocked clauses in 181565 steps
c [sweep-14] limit 12385739 penalty 0 = 0 + 0
c [sweep-14-1] 1684 pos 12.6% + 11719 neg 87.4% = 13403 sched 33.7% ret 26322
c [sweep-14-1] 12395189 steps 312 queries 622.53 avg class size
c [sweep-14-1] 3752 decisions 282 SAT calls 104.53 avg env size
c [sweep-14-1] 12121 variables remain 31% (27453 retained 69%)
c [decomp-47] removed 200 variables
c [sweep-14-1] removed 200 vars (0 failed, 34 eqs, 49 impls)
c [sweep-14] removed 200 vars in TOTAL (1 rounds, 311 queries)
c [phase-count-19] 256878 negative 99.7% of 257674 except 796 0.3%
c [phase-count-19] 175968 positive 68.3% of 257674 except 81706 31.7%
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 5535 enqueued variables after 146366 conflicts
c [score-dist-19] active 33990 (86%), one 0 (0%), zero 5535 (14%)
c [score-dist-19] max exp 519, different 10 (2%)
c [score-dist-19] median active exp 519, avg 518.4
c [simplification-19] removed 334 variables 0.8% (39525 remain 16%)
c [simplification-19] removed 2320 irredundant clauses 0.9% (257674 remain 19%)
c [simplification-19] maximum reduction of 1% = max (1%, 1%)
c [simplification-19] geometric conflict interval increment 14666 = 29333 / 2
c [simplification-19] new conflict interval 43999
c [simplification-19] penalized conflict interval 43999 = 1 * 43999
c [simplification-19] hard conflict limit 212364 (soft 190365 + delta 21999)
c [simplification-19] new conflict limit 190365 (hard 212364)
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  299.4   39524   257674    147289   48857   5502 518883   25    58   92  44%    123  -75   15   36   42%
c i  302.4   39523   257674    151557   52976   5508 518892   21    43   92  50%      2  -85   13   35   36%
c i  305.3   39521   257674    155666   56881   5515 518897   24    53   92  46%     -1  -70   20   35   59%
c -  306.6   39521   257674    157622   30674   5527 518902   21    45   57  47%    -26  -76   18   34   54%
c i  309.5   39520   257674    161672   34515   5532 518909   27    58   67  47%     28  -58   39   34  116%
c i  317.8   39483   257674    172406   44539   5562 518934   32    66   81  48%     97  -43   14   34   41%
c i  323.8   39448   257674    181577   53160   5573 518938   20    44   85  46%     70  -57   12   32   38%
c -  329.7   39432   257674    189951   32738   5581 518947   15    25   57  59%     57  -68   16   30   54%
c i  332.4   39431   257674    193697   36144   5597 518970   19    34   67  56%    110  -56   20   29   68%
c i  332.4   39414   257674    193698   36144   5597 518970   19    34   67  56%    110  -56   20   29   67%
c i  334.1   39385   257674    195909   38207   5612 518979   22    49   69  45%    -23  -39   13   29   46%
c i  338.8   39367   257674    203440   45410   5623 518989   21    44   76  48%     39  -39   26   28   92%
c i  342.4   39284   257674    208393   50067   5631 519000   22    48   82  47%      1  -33   17   28   61%
c i  344.4   39283   257674    211040   52536   5637 519002   20    44   82  46%    -29  -36   18   27   65%
c i  344.6   39281   257674    211292   52769   5637 519007   20    43   82  46%    -35  -36   16   27   60%
c 
c [simplification-20] limit 190375 conflicts (hard 212364) hit after 212365 conflicts
c [quatres-15] found 18455 quaternary clauses 44% in total
c [quatres-15-2] added 3 single-self-subsuming ternary resolvents
c [quatres-15-2] added 7 quaternary resolvents
c [ternres-16] limit 52567517 with penalty 0 = 0 + 0
c [ternres-16] all 39281 free variables schedulable
c [ternres-16] 184 ternary resolvents (0 bin, 184 trn)
c [ternres-16] fully completed ternary resolution
c [decomp-48] removed 247 variables
c [basicprobe-7] limit 262837586 penalty 0 = 0 + 0
c [basicprobe-7-0] 973 sched 3%, 392 failed, 8 lifted, 12145 hbrs
c [decomp-49] removed 533 variables
c [basicprobe-7-1] 1080 probes remain 3% after last round
c [basicprobe-7-1] 848 units = 814 failed (96%) + 34 lifted (4%)
c [basicprobe-7-1] removed 1296 variables, found 124731 hbrs
c [bate-5] eliminated 142 asymmetric tautologies during probing
c [unhide-20] limit 5256751 with penalty 1 = 0 + 1
c [unhide-20-34] 1 units, 0 failed, 65895 tauts, 0 hbrs, 205066 literals
c [transred-16] limit 2000000 with penalty 0 = 0 + 0
c [transred-16] removed 403 transitive binary clauses
c [transred-16] found 1 units
c [block-6] scheduling all variables this time
c [block-6] scheduled 37978 variables 100%
c [block-6] limit of 32854698 steps penalty 4 = 4 + 0
c [block-6] fully completed
c [block-6] transition to [ all 0 rem 0 ] state
c [block-6] eliminated 38 blocked clauses
c [block-6] 38 < 1/100 * 241285 = 2412 considered unsuccessful
c [bca-16] limit of 10000000 steps and 483831 added (scaled 2)
c [bca-16] 55105 out of 75956 literals actually usable 73%
c [bca-16] added 18 blocked clauses in 177054 steps
c [sweep-15] limit 15770255 penalty 0 = 0 + 0
c [sweep-15-1] 1559 pos 13.4% + 10058 neg 86.6% = 11617 sched 30.6% ret 26360
c [sweep-15-1] 15880769 steps 437 queries 163.77 avg class size
c [sweep-15-1] 5430 decisions 400 SAT calls 98.93 avg env size
c [sweep-15-1] 10050 variables remain 26% (27927 retained 74%)
c [decomp-50] removed 159 variables
c [sweep-15-1] removed 159 vars (0 failed, 39 eqs, 71 impls)
c [sweep-15] removed 159 vars in TOTAL (1 rounds, 436 queries)
c [phase-count-20] 240232 negative 99.7% of 241032 except 800 0.3%
c [phase-count-20] 161656 positive 67.1% of 241032 except 79376 32.9%
c [phase-count-20] skipping relative phase luck test
c [phase-20] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-20] sorted 4351 enqueued variables after 212365 conflicts
c [score-dist-20] active 33467 (88%), one 0 (0%), zero 4351 (12%)
c [score-dist-20] max exp 519, different 10 (2%)
c [score-dist-20] median active exp 519, avg 518.6
c [simplification-20] removed 1463 variables 3.7% (37818 remain 15%)
c [simplification-20] removed 16642 irredundant clauses 6.5% (241032 remain 18%)
c [simplification-20] maximum reduction of 6% = max (4%, 6%)
c [simplification-20] large reduction 6% >= 5% limit
c [simplification-20] next conflict interval 2123 = min (212365/100, 43999)
c [simplification-20] penalized conflict interval 2123 = 1 * 2123
c [simplification-20] hard conflict limit 224488 (soft 214488 + delta 10000)
c [simplification-20] new conflict limit 214488 (hard 224488)
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  362.6   37817   241032    217375   58356   5071 555829   18    33   92  54%     21  -42   15   27   58%
c -  365.9   37815   241032    222419   32392   5076 555839   14    27   56  53%      7  -46   14   26   56%
c 
c [simplification-21] limit 214488 conflicts (hard 224488) hit after 224490 conflicts
c [quatres-16] found 17356 quaternary clauses 43% in total
c [quatres-16-1] removed 2 duplicate quaternary clauses
c [quatres-16-2] added 2 single-self-subsuming ternary resolvents
c [quatres-16-2] added 1 quaternary resolvents
c [ternres-17] limit 54462949 with penalty 0 = 0 + 0
c [ternres-17] all 37815 free variables schedulable
c [ternres-17] 172 ternary resolvents (0 bin, 172 trn)
c [ternres-17] fully completed ternary resolution
c [card-6] limit 1701967 penalty 4 = 4 + 0
c [card-6] found 2394 at-most-one constraints of average size 4.0
c [card-6] no at-most-two constraint found
c [card-6] using previous limit 1701967 for elimination
c [card-6] 2394 out of 2394 constraints (100%) meet size limits
c [card-6] no units found
c [card-6] no at-most-one constraints generated
c [decomp-51] removed 12 variables
c [simpleprobe-8] all 37806 free variables schedulable
c [simpleprobe-8] limit 200000000 penalty 0 = 0 + 0
c [decomp-52] removed 80 variables
c [simpleprobe-8] fully completed simple probing
c [simpleprobe-8] removed 80 variables, found 88575 hbrs, 44 units
c [unhide-21] limit 10892589 with penalty 0 = 0 + 0
c [unhide-21-39] 1 units, 11 failed, 137874 tauts, 0 hbrs, 72534 literals
c [transred-17] limit 2000000 with penalty 0 = 0 + 0
c [transred-17] removed 453 transitive binary clauses
c [elim-17] scheduling all variables this time
c [elim-17] scheduled 37645 variables 100%
c [elim-17] limit of 400000000 steps penalty 1 = 1 + 0
c [elim-17] rescheduling of touched variables disabled
c [elim-17-1] eliminated 556 variables 1% in round 1 in 18788364 steps
c [elim-17-1] backward subsumption/strengthening limit 18788300
c [elim-17-1-1] backward checking 3412 touched variables 9%
c [elim-17-1-1] fully completed backward checking in 1 rounds
c [elim-17-1] subsumed 6 and strengthened 16 clauses in 756020 steps
c [elim-17-1] rescheduled 66 variables 0% by backward subsumption
c [elim-17-2] eliminated 6 variables 0% in round 2 in 39391 steps
c [elim-17-2] backward subsumption/strengthening limit 39300
c [elim-17-2-1] backward checking 71 touched variables 0%
c [elim-17-2-1] incomplete backward checking 22 remain 31%
c [elim-17-2] subsumed 3 and strengthened 5 clauses in 39348 steps
c [elim-17-2] rescheduled 26 variables 0% by backward subsumption
c [elim-17-3] eliminated 2 variables 0% in round 3 in 52426 steps
c [elim-17-3] backward subsumption/strengthening limit 52400
c [elim-17-3-1] backward checking 46 touched variables 0%
c [elim-17-3-1] incomplete backward checking 0 remain 0%
c [elim-17-3] subsumed 5 and strengthened 6 clauses in 52401 steps
c [elim-17] incomplete 34 not tried 0% in round 3
c [elim-17] transition to [ all 1 rem 1 ] state
c [elim-17] eliminated 564 = 1% variables out of 37645 scheduled
c [bca-17] limit of 10000000 steps and 473782 added (scaled 2)
c [bca-17] 54310 out of 74164 literals actually usable 73%
c [bca-17] added 33 blocked clauses in 153986 steps
c [sweep-16] limit 16338884 penalty 0 = 0 + 0
c [sweep-16-1] 1183 pos 12.2% + 8517 neg 87.8% = 9700 sched 26.2% ret 27381
c [sweep-16-1] 16364268 steps 567 queries 227.96 avg class size
c [sweep-16-1] 5355 decisions 511 SAT calls 90.43 avg env size
c [sweep-16-1] 7835 variables remain 21% (29176 retained 79%)
c [decomp-53] removed 137 variables
c [sweep-16-1] removed 137 vars (0 failed, 56 eqs, 104 impls)
c [sweep-16] removed 137 vars in TOTAL (1 rounds, 566 queries)
c [phase-count-21] 235019 negative 99.7% of 235815 except 796 0.3%
c [phase-count-21] 158521 positive 67.2% of 235815 except 77294 32.8%
c [phase-count-21] skipping relative phase luck test
c [phase-21] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-21] sorted 4086 enqueued variables after 224490 conflicts
c [score-dist-21] active 32858 (89%), one 0 (0%), zero 4086 (11%)
c [score-dist-21] max exp 519, different 10 (2%)
c [score-dist-21] median active exp 519, avg 518.7
c [simplification-21] removed 871 variables 2.3% (36944 remain 15%)
c [simplification-21] removed 5217 irredundant clauses 2.2% (235815 remain 17%)
c [simplification-21] maximum reduction of 2% = max (2%, 2%)
c [simplification-21] geometric conflict interval increment 14666 = 43999 / 3
c [simplification-21] new conflict interval 58665
c [simplification-21] penalized conflict interval 58665 = 1 * 58665
c [simplification-21] hard conflict limit 312487 (soft 283155 + delta 29332)
c [simplification-21] new conflict limit 283155 (hard 312487)
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  393.3   36943   235815    254164   60973   4975 476158   19    41   80  46%    397  -21   13   24   55%
c -  396.4   36940   235815    258482   33901   4988 476170   18    41   53  45%   -101  -20   16   23   68%
c i  400.4   36939   235815    266127   41193   5001 476186   15    28   64  54%     15  -30   19   22   86%
c i  410.8   36868   235815    281927   55937   5037 476214   19    39   72  48%     82  -13   22   21  104%
c -  419.0   36862   235815    293663   35907   5056 476226   16    34   53  48%     27  -17   15   21   74%
c 
c [simplification-22] limit 283155 conflicts (hard 312487) hit after 301500 conflicts
c [quatres-17] found 17480 quaternary clauses 41% in total
c [quatres-17-2] added 6 quaternary resolvents
c [ternres-18] limit 66363461 with penalty 0 = 0 + 0
c [ternres-18] all 36862 free variables schedulable
c [ternres-18] 118 ternary resolvents (0 bin, 118 trn)
c [ternres-18] fully completed ternary resolution
c [decomp-54] removed 95 variables
c [treelook-8] limit 6636346 penalty 0 = 0 + 0 boost 1
c [treelook-8] scheduled 42629 literals 58%
c [treelook-8] scheduling used 816713 steps
c [treelook-8] scheduled completely
c [treelook-8] limit 6636346 penalty 0 = 0 + 0 boost 1
c [treelook-8] used 6656454 steps
c [treelook-8] 42504 literals remain 58%
c [treelook-8] 4223 variables remain to probed next time 11%
c [decomp-55] removed 5 variables
c [treelook-8] removed 6 variables, found 39885 hbrs
c [unhide-22] limit 13272692 with penalty 0 = 0 + 0
c [unhide-22-45] 0 units, 6 failed, 93414 tauts, 0 hbrs, 98947 literals
c [transred-18] limit 2000000 with penalty 0 = 0 + 0
c [transred-18] removed 315 transitive binary clauses
c [cce-8] boosting limit by 10
c [cce-8] limit of 414771631 steps penalty 3 = 3 + 0
c [cce-8-1] eliminated 1 clauses out of 1 (100%) of length 118
c [cce-8-1] eliminated 1 clauses out of 1 (100%) of length 114
c [cce-8-1] eliminated 1 clauses out of 1 (100%) of length 90
c [cce-8-1] eliminated 1 clauses out of 1 (100%) of length 86
c [cce-8-1] eliminated 1 clauses out of 1 (100%) of length 82
c [cce-8-1] eliminated 1 clauses out of 1 (100%) of length 78
c [cce-8-1] eliminated 2 clauses out of 2 (100%) of length 70
c [cce-8-1] eliminated 2 clauses out of 2 (100%) of length 66
c [cce-8-1] eliminated 2 clauses out of 2 (100%) of length 58
c [cce-8-1] eliminated 1 clauses out of 1 (100%) of length 56
c [cce-8-1] eliminated 1 clauses out of 1 (100%) of length 55
c [cce-8-1] eliminated 2 clauses out of 2 (100%) of length 54
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 53
c [cce-8-1] eliminated 3 clauses out of 3 (100%) of length 52
c [cce-8-1] eliminated 2 clauses out of 3 (67%) of length 51
c [cce-8-1] eliminated 3 clauses out of 4 (75%) of length 50
c [cce-8-1] eliminated 2 clauses out of 4 (50%) of length 49
c [cce-8-1] eliminated 3 clauses out of 4 (75%) of length 48
c [cce-8-1] eliminated 2 clauses out of 4 (50%) of length 47
c [cce-8-1] eliminated 4 clauses out of 5 (80%) of length 46
c [cce-8-1] eliminated 3 clauses out of 5 (60%) of length 45
c [cce-8-1] eliminated 6 clauses out of 6 (100%) of length 44
c [cce-8-1] eliminated 3 clauses out of 6 (50%) of length 43
c [cce-8-1] eliminated 4 clauses out of 6 (67%) of length 42
c [cce-8-1] eliminated 5 clauses out of 6 (83%) of length 41
c [cce-8-1] eliminated 4 clauses out of 6 (67%) of length 40
c [cce-8-1] eliminated 6 clauses out of 7 (86%) of length 39
c [cce-8-1] eliminated 6 clauses out of 9 (67%) of length 38
c [cce-8-1] eliminated 5 clauses out of 6 (83%) of length 37
c [cce-8-1] eliminated 4 clauses out of 6 (67%) of length 36
c [cce-8-1] eliminated 5 clauses out of 6 (83%) of length 35
c [cce-8-1] eliminated 5 clauses out of 8 (62%) of length 34
c [cce-8-1] eliminated 4 clauses out of 5 (80%) of length 33
c [cce-8-1] eliminated 3 clauses out of 7 (43%) of length 32
c [cce-8-1] eliminated 5 clauses out of 6 (83%) of length 31
c [cce-8-1] eliminated 6 clauses out of 10 (60%) of length 30
c [cce-8-1] eliminated 6 clauses out of 7 (86%) of length 29
c [cce-8-1] eliminated 5 clauses out of 7 (71%) of length 28
c [cce-8-1] eliminated 6 clauses out of 7 (86%) of length 27
c [cce-8-1] eliminated 6 clauses out of 8 (75%) of length 26
c [cce-8-1] eliminated 5 clauses out of 8 (62%) of length 25
c [cce-8-1] eliminated 9 clauses out of 10 (90%) of length 24
c [cce-8-1] eliminated 6 clauses out of 9 (67%) of length 23
c [cce-8-1] eliminated 11 clauses out of 14 (79%) of length 22
c [cce-8-1] eliminated 7 clauses out of 10 (70%) of length 21
c [cce-8-1] eliminated 9 clauses out of 11 (82%) of length 20
c [cce-8-1] eliminated 8 clauses out of 11 (73%) of length 19
c [cce-8-1] eliminated 15 clauses out of 17 (88%) of length 18
c [cce-8-1] eliminated 8 clauses out of 15 (53%) of length 17
c [cce-8-1] eliminated 11 clauses out of 14 (79%) of length 16
c [cce-8-1] eliminated 8 clauses out of 11 (73%) of length 15
c [cce-8-1] eliminated 13 clauses out of 21 (62%) of length 14
c [cce-8-1] eliminated 14 clauses out of 18 (78%) of length 13
c [cce-8-1] eliminated 16 clauses out of 21 (76%) of length 12
c [cce-8-1] eliminated 18 clauses out of 22 (82%) of length 11
c [cce-8-1] eliminated 24 clauses out of 36 (67%) of length 10
c [cce-8-1] eliminated 20 clauses out of 26 (77%) of length 9
c [cce-8-1] eliminated 21 clauses out of 39 (54%) of length 8
c [cce-8-1] eliminated 23 clauses out of 67 (34%) of length 7
c [cce-8-1] eliminated 32 clauses out of 2563 (1%) of length 6
c [cce-8-1] eliminated 1534 clauses out of 11888 (13%) of length 5
c [cce-8-1] eliminated 2037 clauses out of 16060 (13%) of length 4
c [cce-8-1] completed large round (ATE)
c [cce-8-1] eliminated 3982 large clauses in 300327216 steps
c [cce-8-1] allowing another 150163608 steps for small clauses
c [cce-8-1] scheduling 153682 clauses = 140215 binary + 13467 ternary
c [cce-8-1] tried to eliminate 26281 small clauses 17%
c [cce-8-1] eliminated 4465 binary clauses 3%
c [cce-8-1] eliminated 886 ternary clauses 7%
c [cce-8-1] eliminated 5351 small clauses 3%
c [cce-8-1] eliminated 5351 small clauses in 414771647 steps
c [cce-8-1] incomplete small round (ATE)
c [cce-8-1] eliminated 9333 covered clauses in round 1
c [cce-8] eliminated 9333 covered clauses in TOTAL during 1 rounds
c [elim-18] no untried remaining variables left
c [elim-18] scheduled 36826 variables 100%
c [elim-18] boosting limit by 20
c [elim-18] limit of 16000000000 steps penalty 0 = 0 + 0
c [elim-18] rescheduling of touched variables disabled
c [elim-18-1] eliminated 525 variables 1% in round 1 in 16178758 steps
c [elim-18-1] backward subsumption/strengthening limit 16178700
c [elim-18-1-1] backward checking 3792 touched variables 10%
c [elim-18-1-1] fully completed backward checking in 1 rounds
c [elim-18-1] subsumed 3 and strengthened 38 clauses in 784445 steps
c [elim-18-1] rescheduled 87 variables 0% by backward subsumption
c [elim-18-2] eliminated 9 variables 0% in round 2 in 57252 steps
c [elim-18-2] backward subsumption/strengthening limit 57200
c [elim-18-2-1] backward checking 85 touched variables 0%
c [elim-18-2-1] incomplete backward checking 0 remain 0%
c [elim-18-2] subsumed 2 and strengthened 4 clauses in 57201 steps
c [elim-18-2] rescheduled 20 variables 0% by backward subsumption
c [elim-18-3] eliminated 2 variables 0% in round 3 in 20041 steps
c [elim-18-3] backward subsumption/strengthening limit 20000
c [elim-18-3-1] backward checking 20 touched variables 0%
c [elim-18-3-1] incomplete backward checking 6 remain 30%
c [elim-18-3] subsumed 0 and strengthened 4 clauses in 20002 steps
c [elim-18] incomplete 16 not tried 0% in round 3
c [elim-18] transition to [ all 1 rem 1 ] state
c [elim-18] eliminated 536 = 1% variables out of 36826 scheduled
c [bca-18] limit of 10000000 steps and 447586 added (scaled 2)
c [bca-18] 52946 out of 72582 literals actually usable 73%
c [bca-18] added 32 blocked clauses in 159487 steps
c [sweep-17] limit 19909038 penalty 0 = 0 + 0
c [sweep-17-1] 1005 pos 13.4% + 6494 neg 86.6% = 7499 sched 20.7% ret 28791
c [sweep-17-1] 19962737 steps 691 queries 153.49 avg class size
c [sweep-17-1] 5148 decisions 625 SAT calls 64.19 avg env size
c [sweep-17-1] 5583 variables remain 15% (30707 retained 85%)
c [decomp-56] removed 104 variables
c [sweep-17-1] removed 104 vars (0 failed, 69 eqs, 127 impls)
c [sweep-17] removed 104 vars in TOTAL (1 rounds, 690 queries)
c [phase-count-22] 222230 negative 99.7% of 222972 except 742 0.3%
c [phase-count-22] 150464 positive 67.5% of 222972 except 72508 32.5%
c [phase-count-22] skipping relative phase luck test
c [phase-22] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-22] sorted 3923 enqueued variables after 301500 conflicts
c [score-dist-22] active 32263 (89%), one 0 (0%), zero 3923 (11%)
c [score-dist-22] max exp 520, different 11 (2%)
c [score-dist-22] median active exp 520, avg 519.4
c [simplification-22] removed 676 variables 1.8% (36186 remain 15%)
c [simplification-22] removed 12843 irredundant clauses 5.4% (222972 remain 16%)
c [simplification-22] maximum reduction of 5% = max (2%, 5%)
c [simplification-22] large reduction 5% >= 5% limit
c [simplification-22] next conflict interval 3015 = min (301500/100, 58665)
c [simplification-22] penalized conflict interval 3015 = 1 * 3015
c [simplification-22] hard conflict limit 314515 (soft 304515 + delta 10000)
c [simplification-22] new conflict limit 304515 (hard 314515)
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  442.6   36185   222972    302311   42839   5661 415723   22    50   65  44%    150    2   20   21   99%
c 
c [simplification-23] limit 304515 conflicts (hard 314515) hit after 314518 conflicts
c [quatres-18] found 15471 quaternary clauses 39% in total
c [quatres-18-1] removed 1 duplicate quaternary clauses
c [quatres-18-2] added 2 quaternary resolvents
c [ternres-19] limit 68499268 with penalty 0 = 0 + 0
c [ternres-19] all 36183 free variables schedulable
c [ternres-19] 210 ternary resolvents (2 bin, 208 trn)
c [ternres-19] fully completed ternary resolution
c [decomp-57] removed 3 variables
c [basicprobe-8] limit 342496344 penalty 0 = 0 + 0
c [basicprobe-8-0] 1566 sched 4%, 225 failed, 12 lifted, 10273 hbrs
c [decomp-58] removed 288 variables
c [basicprobe-8-1] 13314 sched 37%, 209 failed, 7 lifted, 45900 hbrs
c [decomp-59] removed 298 variables
c [basicprobe-8-2] 6974 probes remain 20% after last round
c [basicprobe-8-2] 549 units = 530 failed (97%) + 19 lifted (3%)
c [basicprobe-8-2] removed 760 variables, found 61402 hbrs
c [bate-6] eliminated 167 asymmetric tautologies during probing
c [unhide-23] limit 6849926 with penalty 1 = 0 + 1
c [unhide-23-48] 0 units, 2 failed, 40571 tauts, 0 hbrs, 227728 literals
c [transred-19] limit 2000000 with penalty 0 = 0 + 0
c [transred-19] removed 363 transitive binary clauses
c [elim-19] no untried remaining variables left
c [elim-19] scheduled 35422 variables 100%
c [elim-19] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-19] rescheduling of touched variables disabled
c [elim-19-1] eliminated 227 variables 1% in round 1 in 15660010 steps
c [elim-19-1] backward subsumption/strengthening limit 15660000
c [elim-19-1-1] backward checking 1540 touched variables 4%
c [elim-19-1-1] fully completed backward checking in 1 rounds
c [elim-19-1] subsumed 0 and strengthened 6 clauses in 324058 steps
c [elim-19-1] rescheduled 18 variables 0% by backward subsumption
c [elim-19-2] eliminated 1 variables 0% in round 2 in 12003 steps
c [elim-19-2] backward subsumption/strengthening limit 12000
c [elim-19-2-1] backward checking 12 touched variables 0%
c [elim-19-2-1] incomplete backward checking 8 remain 67%
c [elim-19-2] subsumed 0 and strengthened 2 clauses in 12035 steps
c [elim-19-2] rescheduled 8 variables 0% by backward subsumption
c [elim-19-3] no variable eliminated in round 3 in 10826 steps
c [elim-19] fully completed in 3 rounds
c [elim-19] transition to [ all 0 rem 0 ] state
c [elim-19] eliminated 228 = 1% variables out of 35422 scheduled
c [elim-19] 228 < 1/100 * 35422 = 354 considered unsuccessful
c [bca-19] limit of 10000000 steps and 428312 added (scaled 2)
c [bca-19] 50207 out of 70390 literals actually usable 71%
c [bca-19] added 25 blocked clauses in 164574 steps
c [sweep-18] almost no limit of 4000000000 steps
c [sweep-18-1] 781 pos 14.5% + 4610 neg 85.5% = 5391 sched 15.3% ret 29803
c [sweep-18-1] 47471492 steps 2772 queries 31.17 avg class size
c [sweep-18-1] 14271 decisions 2420 SAT calls 52.50 avg env size
c [sweep-18-1] fully completed sweeping round
c [decomp-60] removed 485 variables
c [sweep-18-1] removed 485 vars (0 failed, 359 eqs, 485 impls)
c [sweep-18-2] 3821 pos 11.0% + 30888 neg 89.0% = 34709 sched 100.0% ret 0
c [sweep-18-2] 152987249 steps 5277 queries 52.18 avg class size
c [sweep-18-2] 43903 decisions 5076 SAT calls 90.98 avg env size
c [sweep-18-2] fully completed sweeping round
c [decomp-61] removed 247 variables
c [sweep-18-2] removed 247 vars (0 failed, 233 eqs, 656 impls)
c [sweep-18-3] 3819 pos 11.1% + 30643 neg 88.9% = 34462 sched 100.0% ret 0
c [sweep-18-3] 147435991 steps 5096 queries 47.75 avg class size
c [sweep-18-3] 42114 decisions 4997 SAT calls 96.57 avg env size
c [sweep-18-3] fully completed sweeping round
c [decomp-62] removed 208 variables
c [sweep-18-3] removed 208 vars (0 failed, 116 eqs, 460 impls)
c [sweep-18] removed 940 vars in TOTAL (3 rounds, 13142 queries)
c [sort-queue-23] sorted 2750 enqueued variables after 314518 conflicts
c [score-dist-23] active 31504 (92%), one 0 (0%), zero 2750 (8%)
c [score-dist-23] max exp 520, different 10 (2%)
c [score-dist-23] median active exp 520, avg 519.7
c [simplification-23] removed 1929 variables 5.3% (34254 remain 14%)
c [simplification-23] removed 11577 irredundant clauses 5.2% (211395 remain 16%)
c [simplification-23] maximum reduction of 5% = max (5%, 5%)
c [simplification-23] large reduction 5% >= 5% limit
c [simplification-23] next conflict interval 3145 = min (314518/100, 58665)
c [simplification-23] penalized conflict interval 3145 = 1 * 3145
c [simplification-23] hard conflict limit 327663 (soft 317663 + delta 10000)
c [simplification-23] new conflict limit 317663 (hard 327663)
c 
c [simplification-24] limit 317663 conflicts (hard 327663) hit after 322196 conflicts
c [quatres-19] found 14853 quaternary clauses 36% in total
c [quatres-19-1] removed 1 duplicate quaternary clauses
c [quatres-19-2] added 5 single-self-subsuming ternary resolvents
c [ternres-20] limit 69774932 with penalty 0 = 0 + 0
c [ternres-20] all 34254 free variables schedulable
c [ternres-20] 285 ternary resolvents (6 bin, 279 trn)
c [ternres-20] fully completed ternary resolution
c [simpleprobe-9] all 34254 free variables schedulable
c [simpleprobe-9] limit 200000000 penalty 0 = 0 + 0
c [decomp-64] removed 47 variables
c [simpleprobe-9] fully completed simple probing
c [simpleprobe-9] removed 47 variables, found 72407 hbrs, 26 units
c [unhide-24] limit 6977493 with penalty 1 = 0 + 1
c [unhide-24-51] 0 units, 10 failed, 128345 tauts, 0 hbrs, 180726 literals
c [transred-20] limit 2000000 with penalty 0 = 0 + 0
c [transred-20] removed 393 transitive binary clauses
c [cce-9] limit of 87218665 steps penalty 2 = 2 + 0
c [cce-9-1] eliminated 1 clauses out of 1 (100%) of length 138
c [cce-9-1] eliminated 1 clauses out of 1 (100%) of length 110
c [cce-9-1] eliminated 2 clauses out of 2 (100%) of length 71
c [cce-9-1] eliminated 1 clauses out of 2 (50%) of length 70
c [cce-9-1] eliminated 1 clauses out of 2 (50%) of length 69
c [cce-9-1] eliminated 1 clauses out of 2 (50%) of length 68
c [cce-9-1] eliminated 1 clauses out of 2 (50%) of length 67
c [cce-9-1] eliminated 2 clauses out of 2 (100%) of length 66
c [cce-9-1] eliminated 1 clauses out of 2 (50%) of length 65
c [cce-9-1] eliminated 1 clauses out of 2 (50%) of length 64
c [cce-9-1] eliminated 1 clauses out of 2 (50%) of length 63
c [cce-9-1] eliminated 1 clauses out of 2 (50%) of length 62
c [cce-9-1] eliminated 1 clauses out of 2 (50%) of length 61
c [cce-9-1] eliminated 1 clauses out of 2 (50%) of length 60
c [cce-9-1] eliminated 1 clauses out of 2 (50%) of length 59
c [cce-9-1] eliminated 1 clauses out of 2 (50%) of length 58
c [cce-9-1] eliminated 1 clauses out of 3 (33%) of length 57
c [cce-9-1] eliminated 1 clauses out of 2 (50%) of length 56
c [cce-9-1] eliminated 1 clauses out of 2 (50%) of length 55
c [cce-9-1] eliminated 1 clauses out of 2 (50%) of length 54
c [cce-9-1] eliminated 1 clauses out of 3 (33%) of length 53
c [cce-9-1] eliminated 1 clauses out of 2 (50%) of length 52
c [cce-9-1] eliminated 1 clauses out of 2 (50%) of length 51
c [cce-9-1] eliminated 1 clauses out of 3 (33%) of length 50
c [cce-9-1] eliminated 2 clauses out of 4 (50%) of length 49
c [cce-9-1] eliminated 2 clauses out of 5 (40%) of length 48
c [cce-9-1] eliminated 3 clauses out of 5 (60%) of length 47
c [cce-9-1] eliminated 2 clauses out of 6 (33%) of length 46
c [cce-9-1] eliminated 1 clauses out of 2 (50%) of length 45
c [cce-9-1] eliminated 1 clauses out of 4 (25%) of length 44
c [cce-9-1] eliminated 2 clauses out of 3 (67%) of length 43
c [cce-9-1] eliminated 2 clauses out of 5 (40%) of length 42
c [cce-9-1] eliminated 1 clauses out of 4 (25%) of length 41
c [cce-9-1] eliminated 1 clauses out of 2 (50%) of length 40
c [cce-9-1] eliminated 1 clauses out of 5 (20%) of length 39
c [cce-9-1] eliminated 2 clauses out of 3 (67%) of length 38
c [cce-9-1] eliminated 1 clauses out of 5 (20%) of length 37
c [cce-9-1] eliminated 1 clauses out of 1 (100%) of length 36
c [cce-9-1] eliminated 3 clauses out of 6 (50%) of length 35
c [cce-9-1] eliminated 1 clauses out of 3 (33%) of length 34
c [cce-9-1] eliminated 1 clauses out of 4 (25%) of length 33
c [cce-9-1] eliminated 2 clauses out of 4 (50%) of length 32
c [cce-9-1] eliminated 1 clauses out of 5 (20%) of length 31
c [cce-9-1] eliminated 2 clauses out of 4 (50%) of length 30
c [cce-9-1] eliminated 1 clauses out of 5 (20%) of length 29
c [cce-9-1] eliminated 2 clauses out of 3 (67%) of length 28
c [cce-9-1] eliminated 1 clauses out of 5 (20%) of length 27
c [cce-9-1] eliminated 1 clauses out of 2 (50%) of length 26
c [cce-9-1] eliminated 1 clauses out of 5 (20%) of length 25
c [cce-9-1] eliminated 1 clauses out of 3 (33%) of length 24
c [cce-9-1] eliminated 1 clauses out of 5 (20%) of length 23
c [cce-9-1] eliminated 1 clauses out of 6 (17%) of length 22
c [cce-9-1] eliminated 1 clauses out of 6 (17%) of length 21
c [cce-9-1] eliminated 2 clauses out of 2 (100%) of length 20
c [cce-9-1] eliminated 1 clauses out of 7 (14%) of length 19
c [cce-9-1] eliminated 2 clauses out of 5 (40%) of length 18
c [cce-9-1] eliminated 1 clauses out of 6 (17%) of length 17
c [cce-9-1] eliminated 2 clauses out of 7 (29%) of length 16
c [cce-9-1] eliminated 2 clauses out of 8 (25%) of length 15
c [cce-9-1] eliminated 5 clauses out of 10 (50%) of length 14
c [cce-9-1] eliminated 2 clauses out of 9 (22%) of length 13
c [cce-9-1] eliminated 4 clauses out of 11 (36%) of length 12
c [cce-9-1] eliminated 3 clauses out of 11 (27%) of length 11
c [cce-9-1] eliminated 8 clauses out of 19 (42%) of length 10
c [cce-9-1] eliminated 7 clauses out of 17 (41%) of length 9
c [cce-9-1] eliminated 9 clauses out of 33 (27%) of length 8
c [cce-9-1] eliminated 10 clauses out of 66 (15%) of length 7
c [cce-9-1] eliminated 26 clauses out of 2676 (1%) of length 6
c [cce-9-1] eliminated 229 clauses out of 9992 (2%) of length 5
c [cce-9-1] incomplete large round (ACCE)
c [cce-9-1] eliminated 381 large clauses in 87218687 steps
c [cce-9-1] allowing another 43609343 steps for small clauses
c [cce-9-1] scheduling 171460 clauses = 132562 binary + 38898 ternary
c [cce-9-1] tried to eliminate 4533 small clauses 3%
c [cce-9-1] eliminated 654 binary clauses 0%
c [cce-9-1] eliminated 145 ternary clauses 0%
c [cce-9-1] eliminated 799 small clauses 0%
c [cce-9-1] eliminated 855 small clauses in 87218666 steps
c [cce-9-1] incomplete small round (ACCE)
c [cce-9-1] eliminated 1236 covered clauses in round 1
c [cce-9] eliminated 1236 covered clauses in TOTAL during 1 rounds
c [cce-9] 1236 < 1/100 * 209975 = 2099 considered unsuccessful
c [bca-20] limit of 10000000 steps and 418929 added (scaled 2)
c [bca-20] 45035 out of 68400 literals actually usable 66%
c [bca-20] added 38 blocked clauses in 160057 steps
c [sweep-19] limit 20932479 penalty 0 = 0 + 0
c [sweep-19-1] 3924 pos 11.5% + 30275 neg 88.5% = 34199 sched 100.0% ret 0
c [sweep-19-1] 20935409 steps 268 queries 710.82 avg class size
c [sweep-19-1] 7760 decisions 261 SAT calls 210.51 avg env size
c [sweep-19-1] 28270 variables remain 83% (5920 retained 17%)
c [decomp-65] removed 18 variables
c [sweep-19-1] removed 18 vars (0 failed, 8 eqs, 16 impls)
c [sweep-19] 18 < 1/1000 * 34199 = 34 considered unsuccessful
c [sweep-19] removed 18 vars in TOTAL (1 rounds, 267 queries)
c [sort-queue-24] sorted 2682 enqueued variables after 322196 conflicts
c [score-dist-24] active 31499 (92%), one 0 (0%), zero 2682 (8%)
c [score-dist-24] max exp 520, different 10 (2%)
c [score-dist-24] median active exp 520, avg 519.8
c [simplification-24] removed 73 variables 0.2% (34181 remain 14%)
c [simplification-24] removed 2772 irredundant clauses 1.3% (208623 remain 15%)
c [simplification-24] maximum reduction of 1% = max (0%, 1%)
c [simplification-24] geometric conflict interval increment 29332 = 58665 / 2
c [simplification-24] new conflict interval 87997
c [simplification-24] penalized conflict interval 87997 = 1 * 87997
c [simplification-24] hard conflict limit 454191 (soft 410193 + delta 43998)
c [simplification-24] new conflict limit 410193 (hard 454191)
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 -  502.4   34181   208623    329634   38235   6004 387325   16    33   51  50%    235  -14   11   20   56%
c i  502.8   34180   208623    330271   38811   6004 387331   18    37   61  48%    242   -9   43   20  214%
c -  525.3   34179   208623    365998   40812   6041 387350   15    24   52  60%    314  -14   19   18  105%
c -  549.4   34179   208623    401791   41675   6081 387370   11    19   53  59%    613  -16   10   17   58%
c i  557.1   34178   208623    415441   54603   6093 387377   13    24   68  56%    690   -8   19   16  121%
c -  571.8   34178   208623    439517   43582   6109 387395   10    14   53  66%   -144  -14    8   14   57%
c 
c [simplification-25] limit 410193 conflicts (hard 454191) hit after 449574 conflicts
c [quatres-20] found 14985 quaternary clauses 34% in total
c [quatres-20-1] removed 1 duplicate quaternary clauses
c [quatres-20-2] added 6 single-self-subsuming ternary resolvents
c [quatres-20-2] added 5 quaternary resolvents
c [ternres-21] limit 89321402 with penalty 0 = 0 + 0
c [ternres-21] all 34178 free variables schedulable
c [ternres-21] 68 ternary resolvents (0 bin, 68 trn)
c [ternres-21] fully completed ternary resolution
c [gauss-6] limit 1116517 penalty 4 = 4 + 0
c [gauss-6] extracted 38 xors of average arity 3.0
c [gauss-6] connected 114 occurrences of 114 variables (average 1.0)
c [gauss-6] limit 1116517 penalty 4 = 4 + 0
c [gauss-6] fully completed
c [gauss-6] exported 0 unary, 0 binary and 0 ternary equations
c [treelook-9] limit 8932140 penalty 0 = 0 + 0 boost 1
c [treelook-9] scheduled 39747 literals 58%
c [treelook-9] scheduling used 745808 steps
c [treelook-9] scheduled completely
c [treelook-9] limit 8932140 penalty 0 = 0 + 0 boost 1
c [treelook-9] used 8959837 steps
c [treelook-9] 39425 literals remain 58%
c [treelook-9] 3765 variables remain to probed next time 11%
c [treelook-9] removed 3 variables, found 44309 hbrs
c [unhide-25] limit 17864280 with penalty 0 = 0 + 0
c [unhide-25-59] 0 units, 17 failed, 92009 tauts, 0 hbrs, 206456 literals
c [transred-21] limit 2000000 with penalty 0 = 0 + 0
c [transred-21] removed 313 transitive binary clauses
c [elim-20] scheduling all variables this time
c [elim-20] scheduled 34169 variables 100%
c [elim-20] limit of 400000000 steps penalty 1 = 1 + 0
c [elim-20] rescheduling of touched variables disabled
c [elim-20-1] eliminated 249 variables 1% in round 1 in 15078107 steps
c [elim-20-1] backward subsumption/strengthening limit 15078100
c [elim-20-1-1] backward checking 1690 touched variables 5%
c [elim-20-1-1] fully completed backward checking in 1 rounds
c [elim-20-1] subsumed 5 and strengthened 2 clauses in 347683 steps
c [elim-20-1] rescheduled 18 variables 0% by backward subsumption
c [elim-20-2] no variable eliminated in round 2 in 6164 steps
c [elim-20] fully completed in 2 rounds
c [elim-20] transition to [ all 0 rem 0 ] state
c [elim-20] eliminated 249 = 1% variables out of 34169 scheduled
c [elim-20] 249 < 1/100 * 34169 = 341 considered unsuccessful
c [bca-21] limit of 10000000 steps and 414640 added (scaled 2)
c [bca-21] 45644 out of 67842 literals actually usable 67%
c [bca-21] added 157 blocked clauses in 150002 steps
c [sort-queue-25] sorted 2581 enqueued variables after 449574 conflicts
c [score-dist-25] active 31339 (92%), one 0 (0%), zero 2581 (8%)
c [score-dist-25] max exp 520, different 10 (2%)
c [score-dist-25] median active exp 520, avg 519.8
c [simplification-25] removed 258 variables 0.8% (33920 remain 14%)
c [simplification-25] removed 2038 irredundant clauses 1.0% (206585 remain 15%)
c [simplification-25] maximum reduction of 1% = max (1%, 1%)
c [simplification-25] geometric conflict interval increment 43998 = 87997 / 2
c [simplification-25] new conflict interval 131995
c [simplification-25] penalized conflict interval 131995 = 1 * 131995
c [simplification-25] hard conflict limit 647566 (soft 581569 + delta 65997)
c [simplification-25] new conflict limit 581569 (hard 647566)
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 -  604.8   33920   206585    478123   44491   5948 333585   11    17   50  65%    376   -9    9   14   67%
c -  632.2   33920   206585    517591   45630   6011 333605   14    25   50  55%    669   -0   13   14   95%
c -  659.5   33920   206585    557779   47602   6036 333631   12    21   50  57%    832   -3   21   13  152%
c i  663.5   33919   206585    563444   53023   6052 333636   14    27   60  52%    848    1   10   14   70%
c -  685.9   33919   206585    596909   48958   6071 333647   13    22   51  59%   -492   -3   23   13  170%
c 
c [simplification-26] limit 581569 conflicts (hard 647566) hit after 622604 conflicts
c [quatres-21] found 15228 quaternary clauses 32% in total
c [quatres-21-1] removed 4 duplicate quaternary clauses
c [quatres-21-2] added 3 single-self-subsuming ternary resolvents
c [quatres-21-2] added 13 quaternary resolvents
c [ternres-22] limit 118611643 with penalty 0 = 0 + 0
c [ternres-22] all 33919 free variables schedulable
c [ternres-22] 157 ternary resolvents (0 bin, 157 trn)
c [ternres-22] fully completed ternary resolution
c [decomp-68] removed 3 variables
c [basicprobe-9] limit 400000000 penalty 0 = 0 + 0
c [basicprobe-9-0] 6696 sched 20%, 159 failed, 2 lifted, 22123 hbrs
c [decomp-69] removed 237 variables
c [basicprobe-9-1] 12187 sched 36%, 156 failed, 3 lifted, 21278 hbrs
c [decomp-70] removed 192 variables
c [basicprobe-9-2] 5234 probes remain 16% after last round
c [basicprobe-9-2] 381 units = 376 failed (99%) + 5 lifted (1%)
c [basicprobe-9-2] removed 500 variables, found 46457 hbrs
c [bate-7] eliminated 107 asymmetric tautologies during probing
c [unhide-26] limit 20000000 with penalty 0 = 0 + 0
c [unhide-26-67] 0 units, 3 failed, 47720 tauts, 0 hbrs, 244851 literals
c [transred-22] limit 2000000 with penalty 0 = 0 + 0
c [transred-22] removed 250 transitive binary clauses
c [block-7] scheduling all variables this time
c [block-7] scheduled 33413 variables 100%
c [block-7] limit of 50000000 steps penalty 4 = 4 + 0
c [block-7] fully completed
c [block-7] transition to [ all 0 rem 0 ] state
c [block-7] eliminated 23 blocked clauses
c [block-7] 23 < 1/100 * 199826 = 1998 considered unsuccessful
c [bca-22] limit of 10000000 steps and 401154 added (scaled 2)
c [bca-22] 44709 out of 66828 literals actually usable 67%
c [bca-22] added 29 blocked clauses in 168466 steps
c [sweep-20] limit 17791746 penalty 1 = 1 + 0
c [sweep-20-1] 3512 pos 12.6% + 24436 neg 87.4% = 27948 sched 83.6% ret 5465
c [sweep-20-1] 17792423 steps 405 queries 564.63 avg class size
c [sweep-20-1] 7097 decisions 394 SAT calls 149.19 avg env size
c [sweep-20-1] 22970 variables remain 69% (10439 retained 31%)
c [decomp-71] removed 18 variables
c [sweep-20-1] removed 18 vars (0 failed, 13 eqs, 17 impls)
c [sweep-20] 18 < 1/1000 * 33413 = 33 considered unsuccessful
c [sweep-20] removed 18 vars in TOTAL (1 rounds, 404 queries)
c [sort-queue-26] sorted 2101 enqueued variables after 622604 conflicts
c [score-dist-26] active 31294 (94%), one 0 (0%), zero 2101 (6%)
c [score-dist-26] max exp 521, different 11 (2%)
c [score-dist-26] median active exp 521, avg 520.5
c [simplification-26] removed 524 variables 1.5% (33395 remain 14%)
c [simplification-26] removed 6852 irredundant clauses 3.3% (199733 remain 15%)
c [simplification-26] maximum reduction of 3% = max (2%, 3%)
c [simplification-26] geometric conflict interval increment 32998 = 131995 / 4
c [simplification-26] new conflict interval 164993
c [simplification-26] penalized conflict interval 164993 = 1 * 164993
c [simplification-26] hard conflict limit 870093 (soft 787597 + delta 82496)
c [simplification-26] new conflict limit 787597 (hard 870093)
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 -  738.7   33395   199733    638179   49753   5944 323809   15    29   51  53%    217    4   18   14  132%
c -  767.5   33395   199733    681133   51802   5992 323822   13    21   52  61%    605   -3   10   13   74%
c -  797.4   33395   199733    723276   53880   6020 323834   14    22   52  63%    804   -1   16   13  124%
c -  829.7   33395   199733    765250   54740   6047 323860   14    24   52  61%    908    1   11   14   79%
c i  836.0   33394   199733    774589   63239   6072 323868   12    19   64  64%    923   -4    5   13   40%
c -  862.5   33391   199733    811042   57577   6127 323878   13    20   53  64%   -955    1   23   12  182%
c i  867.1   33390   199733    817017   62963   6139 323886   15    26   65  56%   -783    6    6   13   51%
c i  885.7   33378   199733    844739   87290   6221 323908    9    13   88  69%   -601   -6    6   12   49%
c i  892.8   32844   199733    854758   95690   6247 323915    9    12   97  74%   -748   -7    6   12   52%
c -  895.0   32311   199733    857554   60671   6250 323916   10    14   71  69%   -816   -5    9   11   81%
c i  897.8   32310   199733    862255   64548   6276 323921   10    15   82  63%   -698   -2    7   11   60%
c i  897.9   31858   199733    862294   64585   6276 323921   10    15   82  63%   -702   -2    7   11   64%
c i  899.9   31798   199733    865435   67134   6318 323934   10    17   82  59%   -725   -1    7   11   60%
c i  900.0   31625   199733    865641   67271   6324 323941   10    17   82  60%   -730   -1    8   11   73%
c i  900.1   30854   199733    865825   67403   6331 323944   10    17   82  60%   -733   -1    6   11   55%
c i  900.1   30009   199733    865832   67405   6332 323945   10    17   82  60%   -733   -1    6   11   54%
c i  900.1   27275   199733    865833   67405   6332 323945   10    17   82  60%   -733   -1    6   11   54%
c i  900.1   26957   199733    865836   67405   6332 323947   10    17   82  60%   -733   -1    6   11   53%
c i  900.1   26913   199733    865837   67405   6332 323947   10    17   82  60%   -733   -1    6   11   53%
c i  900.1   26536   199733    865838   67405   6332 323947   10    17   82  60%   -733   -1    6   11   53%
c 0  900.1   25736   199733    865838   67405   6332 323947   10    17   82  60%   -733   -1    6   11   53%
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: 2747 basic ate = 2526 trn 92% + 221 lrg 8% in 7 updates
c bcas: 22 count, 2126 added (503 skipped), 5761594 steps
c bkwd: tried 520350 clauses, 1040315 lits, 2.00 lits/clause
c bkwd: checked 15451856 occs, 29.70 occs/clause, 14.85 occs/lit
c bkwd: subsumed 16 binary, 88 ternary, 37 large
c bkwd: strengthened 4 binary, 1 ternary (100% self), 1001 large (0% self)
c blkd: 7 bces, 13858 removed, 10232431 resolutions, 28283155 steps
c blkd: 18988 blocking literals 4%, 12 pure
c bump: 872123 bumped seen, 329207045 lits 377.5 on average
c card: 6 count, 0 units, 0 am1, 176098500 steps
c card: 0 rescheduled, 0 eliminated, 0 resolved, 74302 subsumed
c card: 19764 at-most-one constraints found, average size 4.72
c card: 19764 at-most-one constraints used 100%, average size 4.72
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: 9 cces, 60645 eliminated, 59733 ate 98%, 912 abce 2%
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: 4678021 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 214 gcs, 0 rescored clauses, 0 rescored vars
c dcps: 71 decompositions, 10662 equivalent 4%
c deco: 11819 decision-only clauses 1%, 66% reduction
c decs: 5330061 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 20 elims, 108773 eliminated 42%, 160 pure 0%
c elms: 56 rounds, 2.8 rounds/bve
c elms: 86389 small 79%, 22212 large 20%
c elms: 254924 tried small, 86389 succeeded 34%, 168535 failed 66%
c elms: 49301 subsumed, 73070 strengthened, 1571 blocked
c elms: 24154049 copies, 23873275 resolutions, 7154870 ipos
c elms: 5831413 subchks, 3514460 strchks
c gaus: 6 extractions, 724 extracted, 2.2 size, 3 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 12148010 steps, 6074005 extr 50%, 8874 elim 0%
c glue: 20.1 orig avg, 20.1 real avg, 3.4 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 1880540 = 573774 simple 31% + 1230232 trn 65% + 76534 lrg 4%, 6586 sub 0%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 872123 clauses, 125.7 length
c lrnd: 109588188 lits = 215161630 orig - 105573442 removed 49%
c lrnd: 287720 uips 33%, 525294 flips 60%
c mins: 847700 mins 98%, 3028 bin 0%, 6731 size 1%
c mins: 348826278 poisoned searches, 70386275 hits, 20% hit rate
c mins: 469388612 used twice searches, 8404818 hits, 2% hit rate
c move: moved 35013, 22947 bin 66%, 12066 trn 34%
c otfs: 1197 driving 26%, 3462 restarting 74%
c otfs: str 4659, 4458 red 96%, 201 irr 4%
c otfs: str 4659, 0 bin 0%, 180 trn 4%, 4479 lrg 96%
c otfs: sub 16, 15 red 94%, 1 irr 6%
c otfs: sub 16, 0 bin 0%, 2 trn 12%, 14 lrg 88%
c phas: 22 computed, 172827 set, 343 pos (0%), 172484 neg (100%)
c prbs: 9 basic, 158844 probed, 4308 failed, 112 lifted
c prbs: 9 simple, 1028584 probed, 1963 failed, 1624 eqs
c prbs: 9 treelook, 699 probed, 25 failed, 0 lifted
c prom: 229545 locked 11% out of 2142493 tried
c prps: 2037101382 props, 349 props/dec
c prps: 91% srch, 9% simp, 0% lkhd
c quat: 21 count, 85 quat, 39 self1, 0 self2, 1273 dup
c queu: 26 sorted, 5330061 next (2258 steps 0.00)
c queu: 330227045 enq (4183121534 steps 12.67), 329207045 deq 100%
c redc: 8018 clauses 10%, 77727 tried 9%, 94 sat 0%
c redc: 14797 lits 2%, 837760 tried 0%, 94 sat 0%
c redc: 821 times jump level reduced, 38.2 levels on average
c reds: 20 count, 43291.9 conflicts per reduce
c reds: 0 memlim 0%, 20 arith 100%
c reds: 595038 collected 88%, 81284 retired 12%
c rmbd: 58800 removed, 14352 red 24%
c rsts: 18112 restarts 100%, 0 skipped 0%
c rsts: 0 saturating 0%, 0 reuse 0%
c rsts: 0 kept 0.0% average 0.0%
c scnc: 0 count, 1.000 min (0/1000), 1.000 max (0/1000)
c simp: 26 count, 24 confs 92%, 0 vars 0%
c simp: 1 its 4%, 1 bin 4%, 0 trns 0%
c subl: 872123 count (621004 tried 0.7), 61844 sub out of 863181 (7.2%)
c swps: 20 count, 22 rounds, 19251 queries (875.0/round)
c swps: 18060 sat calls, 252 unsat (0.4% success rate)
c swps: 176445 decisions 9.8, 7482 conflicts 0.4
c swps; 324.5 avg class size, 92.8 avg environment size
c swps: 0 failed, 2718 impls, 1388 equivs
c swp0: 6408 type 0 queries, 2857 unsat (44.6%), 6056 sat (94.5%)
c swp1: 12843 type 1 queries, 6851 unsat (53.3%), 11807 sat (91.9%)
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: 12405323 calls to obtain time
c tops: 113628 fixed 44%, 438 its, 1976.80 confs/it
c trds: 22 transitive reductions, 7081 removed, 49 failed
c trds: 36465 nodes, 111550 edges, 44007197 steps
c trim: 1429697 words, 5.5 MB
c trnr: 22 count, 13 bin, 7262 trn, 175364299 steps
c unhd: 26 count, 67 rounds, 175841184 steps
c unhd: 1539 non-trivial sccs of average size 2.2
c unhd: 175 units, 173 bin, 2 trn, 0 lrg
c unhd: 11133 failed, 11042 stamp, 0 lits, 50 bin, 25 trn, 0 lrg
c unhd: 1248059 tauts, 28659 bin 2%, 16185 trn 1%, 1391 lrg 0%
c unhd: 1248059 tauts, 1201824 stamp 96%, 1144811 red 92%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 3278563 str, 173 bin 0%, 4523 trn 0%, 3273867 lrg 100%, 3259667 red 99%
c vars: 25736 remaining 10% and 233063 removed 90% out of 258799
c vars: 113628 fixed 44%, 108773 eliminated 42%, 10662 equivalent 4%
c vsts: 17678525356 visits, 91% srch, 9% simp, 0% lkhd
c vsts: 8.7 search visits per propagation, 18596.6 per conflict
c wchs: 2979467592 pushed, 86088731 enlarged, 311 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all         863266        595038         81284      44912706       7220108        426101
c 
c  0 0         45973   5      6819   1         0   0  26498929  59   2974902  41    119551  28     3.9
c  1 5         38451   4     18448   3      5847   7   4591532  10<  1040583  14     64324  15     2.3
c  2 6        185656  22    135179  23     16472  20   6026985  13   1523949  21<   118197  28<    7.8
c  3 9        299737  35<   242900  41<    21164  26   2603761   6    708267  10     48501  11    10.1
c  4 14       136979  16    107000  18     13290  16<  1764337   4    349464   5     22133   5     6.6
c  5 21        48834   6     33516   6      6311   8   1172680   3    210783   3     16096   4     5.3
c  6 30        30549   4     19170   3      4449   5    641149   1    124007   2     10674   3     4.7
c  7 41        21363   2     11799   2      3427   4    564915   1     95883   1      7562   2     5.0
c  8 54        15077   2      7728   1      2541   3    279110   1     54705   1      5580   1     5.2
c  9 69        11657   1      5524   1      2135   3    317046   1     51448   1      4825   1     3.9
c 10 86        11872   1      4667   1      2209   3    307166   1     54042   1      4800   1     3.9
c 11 126       10117   1      1580   0      2160   3    130362   0     25820   0      2955   1     2.3
c 12 230        6384   1       690   0      1217   1     13867   0      5889   0       834   0     2.4
c 13 534         617   0        18   0        62   0       867   0       366   0        69   0     0.6
c 
c avg                  3.4           3.4           4.2           1.2           1.6           2.1
c std                  2.2           1.6           2.6           2.0           2.1           2.3
c 
c  118.512  13% bump
c   61.219   7% probe
c   58.138   6% unhide
c   39.022   4% cce
c   35.108   4% sweep
c   22.259   2% elim
c    4.185   0% bca
c    3.275   0% decide
c 
c   10.066 < 1% rest (below)
c 
c    3.178   0% block
c    2.515   0% transred
c    1.762   0% gauss
c    1.369   0% ternres
c    0.850   0% quatres
c    0.393   0% card
c    0.000   0% locs
c    0.000   0% queuesort
c    0.000   0% rescore
c ==================================
c    5.039   1% preprocessing     2%
c  239.176  27% inprocessing     98%
c ==================================
c  244.215  27% simplifying
c  655.924  73% search
c ==================================
c  900.144 100% all
c 
c        865838 conflicts,         961.9 confs/sec
c          3504 ternaries,         247.1 confs/ternary
c          3234 binaries,          267.7 confs/binary
c           438 iterations,       1976.8 confs/iteration
c 
c            20 reductions,          0.0 redus/sec,  43291.9 confs/reduction
c         18112 restarts,           20.1 rests/sec,     47.8 confs/restart
c       5330061 decisions,        5921.3 decis/sec,      6.2 decis/conflict
c    2037101382 propagations,  2263084.3 props/sec,    382.2 props/decision
c 
c 900.1 seconds, 117.7 MB
c launch: done
