c launch: /data/cnf/sc2014/app/UCG-20-10p1.cnf.bz2
c host: atom18
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-10p1.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/UCG-20-10p1.cnf.bz2
c no embedded options
c found 'p cnf 259258 1388006' header
c read 259258 variables, 1388006 clauses, 3352067 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=2
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 246109 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] VMTF (--score=2)
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  246109  1373987         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 6014 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] 6014 out of 6014 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 62780 variables
c [simpleprobe-1] all 196478 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 221 variables
c [simpleprobe-1] 15148 variables remain 8% (181109 retained 92%)
c [simpleprobe-1] removed 221 variables, found 15749 hbrs, 20 units
c [unhide-1] limit 66079 based on 1057273 irredundant clauses
c [unhide-1-1] 25 units, 1431 failed, 8310 tauts, 0 hbrs, 12876 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 194130 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 60833 not tried 31% in round 1
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 74191 = 38% variables out of 194130 scheduled
c [elim-1] considered successful since not run to completion yet
c [phase-count-1] 874938 negative 99.2% of 881558 except 6620 0.8%
c [phase-count-1] 709837 positive 80.5% of 881558 except 171721 19.5%
c [phase-count-1] less non-negative clauses 6620 than limit 88100 (10.0%)
c [phase-count-1] non-pos/non-neg = 171721/6620 = 25.94 >= 2.00 = 200/100
c [lucky-phase-1] forcing lucky phase -1
c [phase-1] phase bias: 0 positive 0%, 119939 negative 100%
c [sort-queue-1] sorted 119939 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 119939 (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 82741 variables 40.8% (119939 remain 49%)
c [simplification-1] removed 492429 irredundant clauses 35.8% (881558 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  119938   881558        37      22      7 11269    0     7   57   1%      0    7    1    0 23247%
c i    5.3  119934   881558        72      49     11 11272    0     9   57   2%      0    9    2    0 22084%
c i    5.4  119170   881558       135     102     15 11277    0    12   58   2%      0   12    3    0 19125%
c i    5.4  119135   881558       185     140     19 11284    0    12   58   3%      0   12    3    0 17218%
c i    5.5  119132   881558       308     240     29 11291    1    14   58   5%      0   14    8    0 17619%
c i    5.6  119131   881558       366     287     36 11294    1    15   58   5%      0   15    7    0 14880%
c i    5.6  118791   881558       369     288     36 11295    1    15   58   5%      0   15    7    0 14723%
c i    5.7  118781   881558       414     317     42 11304    1    16   58   5%      0   16    7    0 13025%
c i    5.8  118716   881558       492     367     49 11321    1    18   58   5%      0   18    6    0 10577%
c i    5.8  118705   881558       514     384     51 11323    1    19   58   5%      0   19    6    0 10201%
c 
c [simplification-2] limit of 10 iterations hit after 10 iterations
c [decomp-3] removed 1290 variables
c [simpleprobe-2] 14414 schedulable variables 12%
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [decomp-4] removed 3 variables
c [simpleprobe-2] 12257 variables remain 10% (106389 retained 90%)
c [simpleprobe-2] removed 3 variables, found 1418 hbrs, 1 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 79959 literals 34%
c [treelook-1] scheduling used 514920 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 528271 steps
c [treelook-1] 79946 literals remain 34%
c [treelook-1] 77739 variables remain to probed next time 66%
c [treelook-1] removed 4 variables, found 3584 hbrs
c [basicprobe-1] limit 6972208 based on 871526 irredundant clauses
c [basicprobe-1-0] 43519 probes remain 39% after last round
c [basicprobe-1-0] 25 units = 25 failed (100%) + 0 lifted (0%)
c [basicprobe-1-0] removed 5793 variables, found 17340 hbrs
c [unhide-2] limit 54470 based on 871526 irredundant clauses
c [unhide-2-2] 10 units, 2280 failed, 8534 tauts, 0 hbrs, 1500 literals
c [elim-2] 57019 variables 52% will be scheduled this time
c [elim-2] scheduled 57019 variables 52%
c [elim-2] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-2] rescheduling of touched variables disabled
c [elim-2] incomplete 22747 not tried 21% in round 1
c [elim-2] transition to [ all 0 rem 1 ] state
c [elim-2] eliminated 83 = 0% variables out of 57019 scheduled
c [elim-2] considered successful since not run to completion yet
c [phase-count-2] 778361 negative 99.2% of 784981 except 6620 0.8%
c [phase-count-2] 626615 positive 79.8% of 784981 except 158366 20.2%
c [phase-count-2] less non-negative clauses 6620 than limit 78400 (10.0%)
c [phase-count-2] non-pos/non-neg = 158366/6620 = 23.92 >= 2.00 = 200/100
c [lucky-phase-2] forcing lucky phase -1
c [phase-2] phase bias: 0 positive 0%, 11568 negative 100%
c [sort-queue-2] sorted 109568 enqueued variables after 514 conflicts
c [score-dist-2] active 0 (0%), one 11844 (11%), zero 97724 (89%)
c [score-dist-2] max exp 1, different 2 (100%)
c [score-dist-2] median active exp 0, avg 0.0
c [simplification-2] removed 9127 variables 7.7% (109568 remain 45%)
c [simplification-2] removed 96577 irredundant clauses 11.0% (784981 remain 57%)
c [simplification-2] maximum reduction of 11% = max (8%, 11%)
c [simplification-2] forced so keeping old conflict interval 0
c [simplification-2] conflict limit remains at 1003 (hard 11000)
c [simplification-2] new iteration interval 100
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i    9.1  109567   784981       518     379     49 21819    1    19   51   5%      0   19    6    0 10210%
c i    9.2  108900   784981       593     436     51 21829    1    23   51   5%      0   23    7    0 9837%
c i    9.3  108566   784981       730     542     66 21843    1    25   51   5%      0   25    6    0 7411%
c i    9.3  108557   784981       731     542     66 21843    1    25   51   5%      0   25    6    0 7382%
c i    9.4  108545   784981       756     560     70 21845    1    26   51   5%      0   26    6    0 7101%
c i    9.4  108538   784981       762     562     72 21846    1    26   51   5%      0   26    6    0 6977%
c i    9.4  108537   784981       779     574     75 21847    1    26   51   5%      0   26    6    0 6904%
c i    9.4  108532   784981       800     586     79 21851    1    26   51   5%      0   26    6    0 6618%
c i    9.5  108049   784981       815     596     79 21855    1    27   51   5%      0   26    6    0 6430%
c i    9.5  107877   784981       816     596     79 21855    1    27   51   5%      0   26    6    0 6405%
c i    9.5  107784   784981       825     604     79 21855    1    27   51   5%      0   27    6    0 6500%
c i    9.5  107574   784981       865     630     86 21860    1    28   51   5%      0   27    5    0 5986%
c i    9.5  107480   784981       868     632     86 21860    1    28   51   5%      0   27    5    0 5943%
c i    9.6  107473   784981       937     683     91 21870    2    29   51   5%      0   29    7    0 7180%
c 
c [simplification-3] limit 1030 conflicts (hard 11000) hit after 1030 conflicts
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 3868 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] 3868 out of 3868 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [decomp-6] removed 2507 variables
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] scheduled 64273 literals 30%
c [treelook-2] scheduling used 431833 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] used 340654 steps
c [treelook-2] 64251 literals remain 30%
c [treelook-2] 53839 variables remain to probed next time 50%
c [treelook-2] removed 17 variables, found 2429 hbrs
c [unhide-3] limit 50000 with penalty 1 = 0 + 1
c [unhide-3-3] 9 units, 1033 failed, 20908 tauts, 0 hbrs, 494 literals
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 105055 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 29235 not tried 28% in round 1
c [elim-3] transition to [ all 1 rem 1 ] state
c [elim-3] eliminated 2871 = 3% variables out of 105055 scheduled
c [elim-3] considered successful since not run to completion yet
c [phase-count-3] 724240 negative 99.1% of 730691 except 6451 0.9%
c [phase-count-3] 583150 positive 79.8% of 730691 except 147541 20.2%
c [phase-count-3] less non-negative clauses 6451 than limit 73000 (10.0%)
c [phase-count-3] non-pos/non-neg = 147541/6451 = 22.87 >= 2.00 = 200/100
c [lucky-phase-3] forcing lucky phase -1
c [phase-3] phase bias: 0 positive 0%, 9559 negative 100%
c [sort-queue-3] sorted 102184 enqueued variables after 1030 conflicts
c [score-dist-3] active 0 (0%), one 20120 (20%), zero 82064 (80%)
c [score-dist-3] max exp 1, different 2 (100%)
c [score-dist-3] median active exp 0, avg 0.0
c [simplification-3] removed 5282 variables 4.9% (102184 remain 42%)
c [simplification-3] removed 54290 irredundant clauses 6.9% (730691 remain 53%)
c [simplification-3] maximum reduction of 7% = max (5%, 7%)
c [simplification-3] large reduction 7% >= 5% limit
c [simplification-3] next conflict interval 2000 = 2000/1
c [simplification-3] penalized conflict interval 2000 = 1 * 2000
c [simplification-3] hard conflict limit 13030 (soft 3030 + delta 10000)
c [simplification-3] new conflict limit 3030 (hard 13030)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   12.4  102183   730691      1050     729    104 20496    2    30   49   6%      0   30    8    0 6555%
c i   12.4  101529   730691      1063     739    104 20498    2    30   49   6%      0   30    7    0 6333%
c i   12.5  101518   730691      1137     804    107 20501    2    31   49   6%      0   30    8    0 5980%
c i   12.5  101206   730691      1138     804    107 20501    2    31   49   6%      0   30    8    0 5957%
c i   12.5  101202   730691      1154     816    107 20504    2    31   49   6%      0   30    7    0 5806%
c i   12.5  101197   730691      1170     830    107 20505    2    31   49   6%      0   30    7    0 5644%
c i   12.6  101163   730691      1287     930    115 20512    2    32   49   6%      0   32    8    0 5293%
c i   12.6  101154   730691      1295     935    115 20513    2    32   49   6%      0   32    7    0 5194%
c i   12.7  101019   730691      1323     953    119 20517    2    33   49   6%      0   32    7    0 4965%
c i   12.8  101018   730691      1395    1005    128 20526    2    35   49   6%      0   34    8    0 4985%
c i   12.8  101014   730691      1396    1005    128 20526    2    35   49   6%      0   34    8    0 4965%
c i   12.8  100806   730691      1441    1031    137 20533    2    36   49   6%      0   35    7    0 4487%
c i   12.8  100740   730691      1442    1031    137 20533    2    36   49   6%      0   35    7    0 4470%
c i   13.1  100733   730691      1824    1334    166 20566    3    41   49   7%      1   40   10    0 4426%
c i   13.2  100730   730691      1945    1437    177 20572    3    43   49   7%      1   42    9    0 3981%
c i   13.3  100616   730691      2007    1479    183 20583    3    43   49   7%      1   42    8    0 3421%
c 
c [simplification-4] limit of 224 binary hit after 224 binaries
c [decomp-8] removed 1620 variables
c [basicprobe-2] limit 5766728 based on 720841 irredundant clauses
c [basicprobe-2-0] 36719 probes remain 37% after last round
c [basicprobe-2-0] 30 units = 30 failed (100%) + 0 lifted (0%)
c [basicprobe-2-0] removed 2253 variables, found 15129 hbrs
c [unhide-4] limit 155526 with penalty 0 = 0 + 0
c [unhide-4-4] 10 units, 1737 failed, 7084 tauts, 0 hbrs, 1354 literals
c [elim-4] 21776 variables 23% will be scheduled this time
c [elim-4] scheduled 21776 variables 23%
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] eliminated 1 variables 0% in round 1 in 42323336 steps
c [elim-4-1] backward subsumption/strengthening limit 42323300
c [elim-4-1-1] backward checking 53 touched variables 0%
c [elim-4-1-1] fully completed backward checking in 1 rounds
c [elim-4-1] subsumed 0 and strengthened 0 clauses in 126584 steps
c [elim-4-1] fully rescheduled 96574 variables 100%
c [elim-4-2] eliminated 925 variables 1% in round 2 in 65840591 steps
c [elim-4-2] backward subsumption/strengthening limit 65840500
c [elim-4-2-1] backward checking 3122 touched variables 3%
c [elim-4-2-1] fully completed backward checking in 1 rounds
c [elim-4-2] subsumed 0 and strengthened 0 clauses in 1237068 steps
c [elim-4] fully completed in 2 rounds
c [elim-4] transition to [ all 0 rem 0 ] state
c [elim-4] eliminated 928 = 4% variables out of 21776 scheduled
c [elim-4] 928 < 1/100 * 21776 = 217 considered unsuccessful
c [phase-count-4] 675763 negative 99.1% of 682104 except 6341 0.9%
c [phase-count-4] 542513 positive 79.5% of 682104 except 139591 20.5%
c [phase-count-4] less non-negative clauses 6341 than limit 68200 (10.0%)
c [phase-count-4] non-pos/non-neg = 139591/6341 = 22.01 >= 2.00 = 200/100
c [lucky-phase-4] forcing lucky phase -1
c [phase-4] phase bias: 0 positive 0%, 8713 negative 100%
c [sort-queue-4] sorted 95647 enqueued variables after 2085 conflicts
c [score-dist-4] active 0 (0%), one 25312 (26%), zero 70335 (74%)
c [score-dist-4] max exp 1, different 2 (100%)
c [score-dist-4] median active exp 0, avg 0.0
c [simplification-4] removed 4959 variables 4.9% (95647 remain 39%)
c [simplification-4] removed 48587 irredundant clauses 6.6% (682104 remain 50%)
c [simplification-4] maximum reduction of 7% = max (5%, 7%)
c [simplification-4] forced so keeping old conflict interval 0
c [simplification-4] conflict limit remains at 3061 (hard 13030)
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   17.1   95646   682104      2260    1615    182 26887    3    46   47   7%      1   45    8    0 3129%
c i   17.1   95547   682104      2283    1632    183 26890    3    47   47   7%      1   46    9    0 3200%
c i   17.2   95514   682104      2350    1681    189 26899    3    49   47   7%      1   48    8    0 2991%
c i   17.2   95497   682104      2361    1688    191 26900    3    49   47   7%      1   48    8    0 2922%
c i   17.3   95496   682104      2508    1809    200 26913    4    51   47   8%      1   49   13    0 4274%
c i   17.3   95482   682104      2525    1819    201 26917    4    52   47   8%      1   50   13    0 4179%
c i   17.4   95368   682104      2631    1905    211 26926    4    54   47   8%      1   52   12    0 3647%
c i   17.4   95365   682104      2632    1905    211 26926    4    54   47   8%      1   52   12    0 3633%
c i   17.4   95362   682104      2633    1905    211 26926    4    54   47   8%      1   52   12    0 3618%
c i   17.4   95356   682104      2669    1936    213 26927    4    53   47   8%      1   52   12    0 3420%
c i   17.4   95355   682104      2706    1967    213 26932    4    53   47   8%      1   52   10    0 3092%
c i   17.4   95348   682104      2716    1973    213 26935    4    53   47   8%      1   52   10    0 2986%
c i   17.5   95341   682104      2839    2070    223 26947    4    55   47   8%      1   53    9    0 2444%
c i   17.6   95333   682104      2848    2077    223 26948    4    55   47   8%      1   53    8    0 2387%
c 
c [simplification-5] limit 3083 conflicts (hard 13030) hit after 3084 conflicts
c [quatres-1] found 40952 quaternary clauses 39% in total
c [quatres-1-2] added 1 single-self-subsuming ternary resolvents
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 95098 free variables schedulable
c [ternres-1] 71 ternary resolvents (0 bin, 71 trn)
c [ternres-1] fully completed ternary resolution
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 43 xors of average arity 2.7
c [gauss-1] connected 118 occurrences of 101 variables (average 1.2)
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 35 variables
c [simpleprobe-3] 9692 schedulable variables 10%
c [simpleprobe-3] limit 4253323 penalty 0 = 0 + 0
c [decomp-10] removed 48 variables
c [simpleprobe-3] 12101 variables remain 13% (82914 retained 87%)
c [simpleprobe-3] removed 48 variables, found 7860 hbrs, 18 units
c [unhide-5] limit 212666 with penalty 0 = 0 + 0
c [unhide-5-5] 13 units, 553 failed, 16782 tauts, 0 hbrs, 2328 literals
c [transred-1] limit 1063330 with penalty 0 = 0 + 0
c [transred-1] removed 129 transitive binary clauses
c [transred-1] found 6 units
c [block-1] scheduling all variables this time
c [block-1] scheduled 93901 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 10723 blocked clauses
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 29 clauses out of 420 (7%) of length 10
c [cce-1-1] eliminated 149 clauses out of 2290 (7%) of length 9
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 178 large clauses in 30000004 steps
c [cce-1-1] allowing another 15000002 steps for small clauses
c [cce-1-1] scheduling 518044 clauses = 314339 binary + 203705 ternary
c [cce-1-1] tried to eliminate 199 small clauses 0%
c [cce-1-1] eliminated 32 binary clauses 0%
c [cce-1-1] eliminated 19 ternary clauses 0%
c [cce-1-1] eliminated 51 small clauses 0%
c [cce-1-1] eliminated 51 small clauses in 30000006 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 229 covered clauses in round 1
c [cce-1] eliminated 229 covered clauses in TOTAL during 1 rounds
c [cce-1] 229 < 1/100 * 641836 = 6418 considered unsuccessful
c [bca-1] limit of 10000000 steps and 1283714 added (scaled 2)
c [bca-1] 175202 out of 187804 literals actually usable 93%
c [bca-1] added 274 blocked clauses in 563125 steps
c [sweep-1] limit 1283214 based on 641607 irredundant clauses
c [sweep-1-1] 4139 pos 4.4% + 89762 neg 95.6% = 93901 sched 100.0% ret 0
c [sweep-1-1] 1343498 steps 10 queries 33714.50 avg class size
c [sweep-1-1] 62 decisions 8 SAT calls 41.88 avg env size
c [sweep-1-1] 93882 variables remain 100% (19 retained 0%)
c [decomp-11] removed 41 variables
c [sweep-1-1] removed 41 vars (0 failed, 1 eqs, 4 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 41 vars in TOTAL (1 rounds, 9 queries)
c [phase-count-5] 635128 negative 99.0% of 641450 except 6322 1.0%
c [phase-count-5] 517590 positive 80.7% of 641450 except 123860 19.3%
c [phase-count-5] less non-negative clauses 6322 than limit 64100 (10.0%)
c [phase-count-5] non-pos/non-neg = 123860/6322 = 19.59 >= 2.00 = 200/100
c [lucky-phase-5] forcing lucky phase -1
c [phase-5] phase bias: 0 positive 0%, 8654 negative 100%
c [sort-queue-5] sorted 93860 enqueued variables after 3084 conflicts
c [score-dist-5] active 0 (0%), one 26739 (28%), zero 67121 (72%)
c [score-dist-5] max exp 1, different 2 (100%)
c [score-dist-5] median active exp 0, avg 0.0
c [simplification-5] removed 1238 variables 1.3% (93860 remain 38%)
c [simplification-5] removed 40654 irredundant clauses 6.0% (641450 remain 47%)
c [simplification-5] maximum reduction of 6% = max (1%, 6%)
c [simplification-5] large reduction 6% >= 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 15084 (soft 5084 + delta 10000)
c [simplification-5] new conflict limit 5084 (hard 15084)
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   21.8   93859   641450      3233    2360    333 43267    5    65   46   7%      2   64   10    0 2364%
c i   21.9   93856   641450      3370    2467    345 43281    5    67   46   7%      2   65    9    0 2062%
c i   22.0   93692   641450      3383    2474    346 43285    5    67   46   7%      2   65    8    0 1989%
c i   22.0   93690   641450      3403    2484    347 43293    5    67   46   7%      2   65    8    0 1875%
c i   22.0   93685   641450      3454    2518    356 43299    5    66   46   7%      2   64    7    0 1692%
c i   22.3   93591   641450      3809    2813    383 43320    5    71   46   7%      2   68    9    0 1776%
c i   22.4   93556   641450      3861    2855    386 43326    5    71   46   8%      2   69    9    0 1770%
c i   22.5   93553   641450      4018    2979    395 43341    5    72   46   8%      2   69    9    1 1744%
c i   22.6   93548   641450      4119    3068    399 43348    6    72   46   8%      2   70   11    1 2073%
c i   22.8   93043   641450      4324    3231    413 43367    6    75   46   8%      2   72   13    1 2235%
c i   22.8   93042   641450      4325    3231    413 43367    6    75   46   8%      2   72   13    1 2226%
c i   22.8   93025   641450      4368    3265    416 43372    6    76   46   8%      2   73   13    1 2186%
c i   22.9   93017   641450      4382    3272    419 43375    6    75   46   8%      2   72   12    1 2089%
c i   22.9   92889   641450      4427    3309    420 43381    6    76   46   8%      1   73   11    1 1951%
c i   23.2   92883   641450      4664    3500    443 43398    7    82   46   8%      2   79   11    1 1783%
c i   23.4   92873   641450      4744    3560    451 43409    7    85   46   8%      1   81   10    1 1642%
c i   23.4   92872   641450      4779    3585    453 43416    7    85   46   8%      1   82   10    1 1538%
c i   23.5   92862   641450      4817    3603    458 43430    7    85   46   8%      1   82    9    1 1402%
c i   23.5   92852   641450      4826    3609    459 43431    7    85   46   8%      1   82    9    1 1372%
c i   23.5   92850   641450      4833    3613    459 43433    7    85   46   8%      1   82    9    1 1344%
c i   23.5   92697   641450      4837    3615    459 43434    7    85   46   8%      1   82    9    1 1340%
c i   23.6   92696   641450      4934    3693    471 43440    7    87   46   8%      1   83    9    1 1329%
c i   23.7   92687   641450      4990    3738    473 43446    7    87   46   8%      1   83   11    1 1615%
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.7   92686   641450      5035    3769    478 43452    7    88   46   8%      1   84   11    1 1578%
c 
c [simplification-6] limit 5098 conflicts (hard 15084) hit after 5098 conflicts
c [quatres-2] found 36937 quaternary clauses 38% 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 92682 free variables schedulable
c [ternres-2] 15 ternary resolvents (0 bin, 15 trn)
c [ternres-2] 65018 variables remain 70% (27664 retained 30%)
c [card-3] limit 500000 penalty 2 = 2 + 0
c [card-3] found 2248 at-most-one constraints of average size 4.3
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 500000 for elimination
c [card-3] 2248 out of 2248 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [decomp-12] removed 1204 variables
c [treelook-3] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-3] scheduled 58536 literals 32%
c [treelook-3] scheduling used 300153 steps
c [treelook-3] not fully scheduled
c [treelook-3] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-3] used 436071 steps
c [treelook-3] 58469 literals remain 32%
c [treelook-3] 36133 variables remain to probed next time 39%
c [decomp-13] removed 7 variables
c [treelook-3] removed 51 variables, found 4407 hbrs
c [unhide-6] limit 347813 with penalty 0 = 0 + 0
c [unhide-6-6] 11 units, 841 failed, 6950 tauts, 0 hbrs, 3602 literals
c [transred-2] limit 1739067 with penalty 0 = 0 + 0
c [transred-2] removed 200 transitive binary clauses
c [transred-2] found 5 units
c [block-2] scheduling all variables this time
c [block-2] scheduled 91354 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 1142 blocked clauses
c [block-2] 1142 < 1/100 * 635087 = 6350 considered unsuccessful
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 91354 variables 100%
c [elim-5] limit of 17390677 steps penalty 1 = 1 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5] incomplete 23606 not tried 26% in round 1
c [elim-5] transition to [ all 1 rem 1 ] state
c [elim-5] eliminated 1944 = 2% variables out of 91354 scheduled
c [bca-2] limit of 10000000 steps and 1233251 added (scaled 2)
c [bca-2] 164709 out of 178822 literals actually usable 92%
c [bca-2] added 175 blocked clauses in 524064 steps
c [sweep-2] limit 1232614 based on 616307 irredundant clauses
c [sweep-2-1] 4829 pos 5.4% + 84566 neg 94.6% = 89395 sched 100.0% ret 15
c [sweep-2-1] 1612663 steps 20 queries 25744.45 avg class size
c [sweep-2-1] 207 decisions 19 SAT calls 41.42 avg env size
c [sweep-2-1] 89180 variables remain 100% (58 retained 0%)
c [decomp-14] removed 181 variables
c [sweep-2-1] removed 181 vars (0 failed, 0 eqs, 2 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 181 vars in TOTAL (1 rounds, 19 queries)
c [phase-count-6] 609246 negative 99.0% of 615445 except 6199 1.0%
c [phase-count-6] 494684 positive 80.4% of 615445 except 120761 19.6%
c [phase-count-6] less non-negative clauses 6199 than limit 61500 (10.0%)
c [phase-count-6] non-pos/non-neg = 120761/6199 = 19.48 >= 2.00 = 200/100
c [lucky-phase-6] forcing lucky phase -1
c [phase-6] phase bias: 0 positive 0%, 6186 negative 100%
c [sort-queue-6] sorted 89229 enqueued variables after 5098 conflicts
c [score-dist-6] active 0 (0%), one 27684 (31%), zero 61545 (69%)
c [score-dist-6] max exp 1, different 2 (100%)
c [score-dist-6] median active exp 0, avg 0.0
c [simplification-6] removed 3453 variables 3.7% (89229 remain 36%)
c [simplification-6] removed 26005 irredundant clauses 4.1% (615445 remain 45%)
c [simplification-6] maximum reduction of 4% = max (4%, 4%)
c [simplification-6] geometric conflict interval increment 4000 = 20000 / 5
c [simplification-6] new conflict interval 4000
c [simplification-6] penalized conflict interval 4000 = 1 * 4000
c [simplification-6] hard conflict limit 19098 (soft 9098 + delta 10000)
c [simplification-6] new conflict limit 9098 (hard 19098)
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   27.4   89228   615445      5108    3220    447 39477    7    89   44   8%      1   85    9    1 1334%
c i   27.4   89145   615445      5129    3236    449 39478    7    89   44   8%      1   85    9    1 1381%
c i   27.6   89136   615445      5286    3365    461 39486    7    89   45   8%      1   85   11    1 1544%
c i   27.6   89135   615445      5344    3416    463 39489    7    89   45   8%      1   85   10    1 1447%
c i   27.7   89132   615445      5491    3540    473 39499    7    90   45   8%      1   85    9    1 1231%
c i   28.0   89128   615445      5688    3680    485 39533    7    93   45   7%      1   89    8    1 1068%
c i   28.1   89127   615445      5758    3728    493 39541    7    94   45   7%      1   89    8    1 1012%
c i   28.1   89125   615445      5763    3728    494 39543    7    94   45   7%      1   89    8    1  997%
c i   28.2   89117   615445      5813    3763    498 39553    7    96   45   7%      1   91    8    1  987%
c i   28.2   89002   615445      5817    3765    498 39554    7    96   45   7%      1   91    7    1  975%
c i   28.2   88948   615445      5827    3772    499 39555    7    96   45   7%      1   91    7    1  953%
c i   28.6   88940   615445      6179    4060    523 39591    7   101   45   7%      2   96   10    1 1193%
c i   28.7   88889   615445      6325    4181    529 39607    8   101   45   8%      1   96   13    1 1513%
c i   28.8   88888   615445      6345    4196    531 39609    8   102   45   8%      1   96   13    1 1482%
c i   28.9   88879   615445      6496    4331    535 39616    8   102   45   8%      1   96   14    1 1603%
c i   28.9   88878   615445      6509    4343    535 39616    8   101   45   8%      1   96   14    1 1565%
c i   29.0   88875   615445      6694    4495    546 39625    8   101   45   8%      1   95   13    1 1446%
c i   29.2   88748   615445      6848    4621    559 39636    8   105   45   8%      1   98   13    1 1357%
c i   29.2   88743   615445      6915    4673    567 39641    8   106   45   8%      1   99   12    1 1217%
c i   29.3   88742   615445      6979    4720    573 39651    8   106   45   8%      1  100   12    1 1199%
c i   29.6   88738   615445      7230    4916    598 39673    8   108   45   8%      1  101   11    1 1109%
c i   29.6   88731   615445      7231    4916    597 39674    8   108   45   8%      1  101   11    1 1104%
c i   29.7   88726   615445      7294    4959    602 39686    8   109   45   8%      1  102   10    1 1007%
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   29.7   88703   615445      7295    4959    602 39686    8   109   45   8%      1  102   10    1 1003%
c i   29.7   88702   615445      7296    4959    602 39686    8   109   45   8%      1  102   10    1  999%
c i   29.8   88700   615445      7440    5074    607 39705    8   109   45   8%      1  102   10    1  964%
c i   30.0   88692   615445      7561    5166    618 39719    9   112   45   8%      1  104   13    1 1184%
c i   30.0   88685   615445      7577    5179    620 39719    9   112   45   8%      1  105   13    1 1203%
c i   30.1   88682   615445      7671    5255    626 39725    9   113   45   8%      1  106   12    1 1144%
c i   30.1   88675   615445      7705    5278    630 39731    9   113   45   8%      1  105   12    1 1068%
c i   30.2   88668   615445      7783    5346    634 39736    9   114   46   8%      1  106   12    1 1075%
c i   30.4   88663   615445      7914    5450    648 39747    9   116   46   8%      1  108   16    1 1408%
c i   30.8   88660   615445      8336    5799    680 39776   10   121   46   8%      2  113   16    1 1306%
c i   30.9   88657   615445      8364    5815    686 39781   10   123   46   8%      2  114   15    1 1218%
c i   31.0   88462   615445      8466    5894    695 39793   10   123   46   8%      2  114   12    1  948%
c i   31.1   88455   615445      8478    5903    695 39795   10   123   46   8%      2  114   12    1  950%
c i   31.1   88452   615445      8571    5978    699 39802   10   122   46   8%      2  113   14    1 1126%
c i   31.3   88442   615445      8741    6106    715 39826   10   125   46   8%      1  115   11    1  887%
c i   31.4   88438   615445      8795    6135    726 39838   10   125   46   8%      1  115   11    1  821%
c i   31.5   88432   615445      8824    6157    728 39842   10   124   46   8%      1  115   10    1  771%
c i   31.5   88426   615445      8830    6161    729 39842   10   124   46   8%      1  115   10    1  760%
c i   31.5   88425   615445      8858    6181    731 39844   10   124   46   8%      1  114   10    1  747%
c i   31.5   88288   615445      8868    6190    731 39844   10   124   46   8%      1  114   10    1  749%
c i   31.5   88280   615445      8869    6190    731 39844   10   124   46   8%      1  114   10    1  746%
c i   31.6   88274   615445      8924    6230    739 39847   10   125   46   8%      1  115    9    1  725%
c i   31.7   88263   615445      8981    6265    745 39862   10   124   46   8%      1  115    9    1  660%
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   31.7   88255   615445      8985    6265    747 39863   10   124   46   8%      1  114    9    1  651%
c i   31.7   88251   615445      9019    6283    756 39869   10   123   46   8%      1  114    8    1  600%
c i   31.7   88250   615445      9059    6313    759 39874   10   123   46   8%      1  113    9    1  672%
c i   31.8   88249   615445      9134    6377    764 39877   10   124   46   8%      1  114    9    1  692%
c 
c [simplification-7] limit 9147 conflicts (hard 19098) hit after 9147 conflicts
c [quatres-3] found 35036 quaternary clauses 37% in total
c [quatres-3-1] added 1 double-self-subsuming ternary resolvents
c [quatres-3-2] added 3 single-self-subsuming ternary resolvents
c [ternres-3] limit 4000000 with penalty 0 = 0 + 0
c [ternres-3] 61916 schedulable variables 69%
c [ternres-3] 28 ternary resolvents (0 bin, 28 trn)
c [ternres-3] 34076 variables remain 39% (54167 retained 61%)
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] extracted 47 xors of average arity 2.8
c [gauss-2] connected 131 occurrences of 131 variables (average 1.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 35 variables
c [basicprobe-3] limit 15620702 penalty 0 = 0 + 0
c [basicprobe-3-0] 32002 probes remain 37% after last round
c [basicprobe-3-0] 75 units = 75 failed (100%) + 0 lifted (0%)
c [basicprobe-3-0] removed 923 variables, found 30780 hbrs
c [bate-1] eliminated 43 asymmetric tautologies during probing
c [unhide-7] limit 624828 with penalty 0 = 0 + 0
c [unhide-7-7] 39 units, 359 failed, 12779 tauts, 0 hbrs, 5770 literals
c [transred-3] limit 2000000 with penalty 0 = 0 + 0
c [transred-3] removed 219 transitive binary clauses
c [transred-3] found 9 units
c [cce-2] limit of 15000000 steps penalty 1 = 1 + 0
c [cce-2-1] eliminated 1 clauses out of 347 (0%) of length 10
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] eliminated 1 large clauses in 15000000 steps
c [cce-2-1] allowing another 7500000 steps for small clauses
c [cce-2-1] scheduling 307156 clauses = 287491 binary + 19665 ternary
c [cce-2-1] tried to eliminate 257 small clauses 0%
c [cce-2-1] eliminated 94 binary clauses 0%
c [cce-2-1] eliminated 6 ternary clauses 0%
c [cce-2-1] eliminated 100 small clauses 0%
c [cce-2-1] eliminated 6799 small clauses in 15000019 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 6800 covered clauses in round 1
c [cce-2] eliminated 6800 covered clauses in TOTAL during 1 rounds
c [elim-6] 23205 variables 27% will be scheduled this time
c [elim-6] scheduled 23205 variables 27%
c [elim-6] limit of 62482809 steps penalty 0 = 0 + 0
c [elim-6] rescheduling of touched variables disabled
c [elim-6-1] eliminated 2 variables 0% in round 1 in 38770179 steps
c [elim-6-1] backward subsumption/strengthening limit 23712630
c [elim-6-1-1] backward checking 158 touched variables 0%
c [elim-6-1-1] fully completed backward checking in 1 rounds
c [elim-6-1] subsumed 0 and strengthened 0 clauses in 130821 steps
c [elim-6-1] fully rescheduled 86562 variables 100%
c [elim-6] incomplete 14912 not tried 17% in round 2
c [elim-6] transition to [ all 1 rem 1 ] state
c [elim-6] eliminated 1701 = 7% variables out of 23205 scheduled
c [bca-3] limit of 10000000 steps and 1156624 added (scaled 2)
c [bca-3] 150573 out of 169728 literals actually usable 89%
c [bca-3] added 66 blocked clauses in 461539 steps
c [sweep-3] limit 1155900 based on 577950 irredundant clauses
c [sweep-3-1] 4819 pos 5.7% + 79990 neg 94.3% = 84809 sched 99.9% ret 54
c [sweep-3-1] 1538797 steps 25 queries 24154.72 avg class size
c [sweep-3-1] 259 decisions 22 SAT calls 43.05 avg env size
c [sweep-3-1] 84665 variables remain 100% (198 retained 0%)
c [decomp-16] removed 68 variables
c [sweep-3-1] removed 68 vars (0 failed, 2 eqs, 4 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 68 vars in TOTAL (1 rounds, 24 queries)
c [phase-count-7] 571927 negative 99.0% of 577854 except 5927 1.0%
c [phase-count-7] 463590 positive 80.2% of 577854 except 114264 19.8%
c [phase-count-7] less non-negative clauses 5927 than limit 57700 (10.0%)
c [phase-count-7] non-pos/non-neg = 114264/5927 = 19.28 >= 2.00 = 200/100
c [lucky-phase-7] forcing lucky phase -1
c [phase-7] phase bias: 0 positive 0%, 2384 negative 100%
c [sort-queue-7] sorted 84795 enqueued variables after 9147 conflicts
c [score-dist-7] active 0 (0%), one 33518 (40%), zero 51277 (60%)
c [score-dist-7] max exp 1, different 2 (100%)
c [score-dist-7] median active exp 0, avg 0.0
c [simplification-7] removed 3448 variables 3.9% (84795 remain 34%)
c [simplification-7] removed 37591 irredundant clauses 6.1% (577854 remain 42%)
c [simplification-7] maximum reduction of 6% = max (4%, 6%)
c [simplification-7] large reduction 6% >= 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 21147 (soft 11147 + delta 10000)
c [simplification-7] new conflict limit 11147 (hard 21147)
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   36.7   84794   577854      9181    5232    763 64404   10   123   44   8%      1  113    9    1  663%
c i   36.8   84747   577854      9207    5251    766 64407   10   124   44   8%      1  114    8    1  629%
c i   36.8   84737   577854      9208    5251    766 64407   10   124   44   8%      1  114    8    1  626%
c i   36.8   84728   577854      9220    5256    771 64408   10   124   44   8%      1  114    8    1  623%
c i   36.8   84724   577854      9232    5264    772 64410   10   124   44   8%      1  114    8    1  617%
c i   37.0   84716   577854      9334    5347    779 64421   10   124   44   8%      1  114    9    1  633%
c i   37.1   84665   577854      9371    5372    785 64425   10   125   44   8%      1  115    8    1  600%
c i   37.1   84662   577854      9409    5402    788 64429   10   127   44   8%      1  116    9    1  645%
c i   37.1   84657   577854      9410    5402    788 64429   10   127   44   8%      1  116    9    1  643%
c i   37.6   84612   577854      9798    5709    807 64482   10   131   44   8%      2  120   11    1  782%
c i   37.8   84399   577854      9968    5832    831 64494   10   132   44   8%      2  120   13    1  923%
c i   37.9   84395   577854     10050    5897    838 64501   10   132   44   8%      1  120   16    1 1058%
c i   38.2   84394   577854     10388    6184    866 64516   11   136   44   8%      2  123   15    2  992%
c i   38.3   84390   577854     10438    6224    869 64522   11   135   44   8%      2  123   15    2  978%
c i   38.4   84389   577854     10472    6253    872 64522   11   136   44   8%      2  124   15    2  972%
c i   38.4   84384   577854     10478    6257    872 64523   11   136   44   8%      2  123   15    2  958%
c i   38.4   84379   577854     10529    6299    876 64526   11   136   44   8%      2  123   16    2 1021%
c i   38.4   84376   577854     10541    6310    876 64526   11   136   44   8%      2  124   16    2 1022%
c i   38.7   84371   577854     10841    6564    893 64551   11   136   44   8%      2  123   17    2 1018%
c i   38.7   84367   577854     10855    6574    895 64552   11   138   44   8%      2  125   16    2  978%
c i   38.8   84256   577854     10880    6597    896 64552   11   139   44   8%      2  126   15    2  932%
c i   38.9   84251   577854     11011    6707    904 64560   11   141   45   8%      2  128   14    2  830%
c i   39.0   84216   577854     11070    6748    912 64569   11   141   45   8%      1  128   14    2  808%
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   39.1   84215   577854     11154    6822    916 64574   12   140   45   8%      1  127   16    2  921%
c 
c [simplification-8] limit 11168 conflicts (hard 21147) hit after 11168 conflicts
c [quatres-4] found 35873 quaternary clauses 39% in total
c [quatres-4-1] removed 1 duplicate quaternary clauses
c [quatres-4-2] added 3 single-self-subsuming ternary resolvents
c [quatres-4-2] added 1 quaternary resolvents
c [ternres-4] limit 4000000 with penalty 0 = 0 + 0
c [ternres-4] 32490 schedulable variables 38%
c [ternres-4] 11 ternary resolvents (0 bin, 11 trn)
c [ternres-4] 4378 variables remain 5% (79834 retained 95%)
c [decomp-17] removed 627 variables
c [simpleprobe-4] 10616 schedulable variables 13%
c [simpleprobe-4] limit 15590629 penalty 0 = 0 + 0
c [decomp-18] removed 337 variables
c [simpleprobe-4] 4218 variables remain 5% (79613 retained 95%)
c [simpleprobe-4] removed 337 variables, found 16274 hbrs, 110 units
c [unhide-8] limit 779531 with penalty 0 = 0 + 0
c [unhide-8-8] 3 units, 840 failed, 11151 tauts, 0 hbrs, 3341 literals
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 227 transitive binary clauses
c [transred-4] found 7 units
c [block-3] scheduling all variables this time
c [block-3] scheduled 82446 variables 100%
c [block-3] limit of 25000000 steps penalty 1 = 1 + 0
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 27 blocked clauses
c [block-3] 27 < 1/100 * 569584 = 5695 considered unsuccessful
c [cce-3] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-3-1] eliminated 13 clauses out of 317 (4%) of length 10
c [cce-3-1] eliminated 36 clauses out of 1505 (2%) of length 9
c [cce-3-1] eliminated 19 clauses out of 432 (4%) of length 8
c [cce-3-1] eliminated 61 clauses out of 647 (9%) of length 7
c [cce-3-1] eliminated 2100 clauses out of 5480 (38%) of length 6
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 2229 large clauses in 30000006 steps
c [cce-3-1] allowing another 15000003 steps for small clauses
c [cce-3-1] scheduling 450348 clauses = 278528 binary + 171820 ternary
c [cce-3-1] tried to eliminate 350 small clauses 0%
c [cce-3-1] eliminated 83 binary clauses 0%
c [cce-3-1] eliminated 33 ternary clauses 0%
c [cce-3-1] eliminated 116 small clauses 0%
c [cce-3-1] eliminated 116 small clauses in 30000020 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 2345 covered clauses in round 1
c [cce-3] eliminated 2345 covered clauses in TOTAL during 1 rounds
c [cce-3] 2345 < 1/100 * 556855 = 5568 considered unsuccessful
c [elim-7] 14719 variables 18% will be scheduled this time
c [elim-7] scheduled 14719 variables 18%
c [elim-7] limit of 77953148 steps penalty 0 = 0 + 0
c [elim-7] rescheduling of touched variables disabled
c [elim-7-1] no variable eliminated in round 1 in 29677777 steps
c [elim-7] fully completed in 1 rounds
c [elim-7] transition to [ all 0 rem 0 ] state
c [elim-7] eliminated 0 = 0% variables out of 14719 scheduled
c [bca-4] limit of 10000000 steps and 1105349 added (scaled 2)
c [bca-4] 141804 out of 164894 literals actually usable 86%
c [bca-4] added 145 blocked clauses in 421511 steps
c [sweep-4] limit 1169297 penalty 0 = 0 + 0
c [sweep-4-1] 4929 pos 6.0% + 77329 neg 94.0% = 82258 sched 99.8% ret 188
c [sweep-4-1] 1283454 steps 17 queries 19952.65 avg class size
c [sweep-4-1] 99 decisions 15 SAT calls 41.47 avg env size
c [sweep-4-1] 82215 variables remain 100% (231 retained 0%)
c [decomp-19] removed 123 variables
c [sweep-4-1] removed 123 vars (0 failed, 1 eqs, 4 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 123 vars in TOTAL (1 rounds, 16 queries)
c [phase-count-8] 548230 negative 99.3% of 552047 except 3817 0.7%
c [phase-count-8] 440028 positive 79.7% of 552047 except 112019 20.3%
c [phase-count-8] less non-negative clauses 3817 than limit 55200 (10.0%)
c [phase-count-8] non-pos/non-neg = 112019/3817 = 29.35 >= 2.00 = 200/100
c [lucky-phase-8] forcing lucky phase -1
c [phase-8] phase bias: 0 positive 0%, 1224 negative 100%
c [sort-queue-8] sorted 82323 enqueued variables after 11168 conflicts
c [score-dist-8] active 0 (0%), one 36743 (45%), zero 45580 (55%)
c [score-dist-8] max exp 1, different 2 (100%)
c [score-dist-8] median active exp 0, avg 0.0
c [simplification-8] removed 1889 variables 2.2% (82323 remain 33%)
c [simplification-8] removed 25807 irredundant clauses 4.5% (552047 remain 40%)
c [simplification-8] maximum reduction of 4% = max (2%, 4%)
c [simplification-8] geometric conflict interval increment 4000 = 20000 / 5
c [simplification-8] new conflict interval 8000
c [simplification-8] penalized conflict interval 8000 = 1 * 8000
c [simplification-8] hard conflict limit 29168 (soft 19168 + delta 10000)
c [simplification-8] new conflict limit 19168 (hard 29168)
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   43.4   82322   552047     11295    6886    919 68796   12   141   44   8%      1  127   17    2 1000%
c i   43.5   82319   552047     11402    6971    932 68802   12   142   44   8%      1  127   15    2  856%
c i   43.7   82311   552047     11547    7093    942 68806   13   143   44   9%      1  129   30    2 1627%
c i   43.8   82301   552047     11681    7211    944 68812   13   145   44   9%      1  131   28    2 1477%
c i   43.8   82300   552047     11723    7250    944 68814   13   145   44   9%      1  130   26    2 1343%
c i   43.8   82294   552047     11736    7259    945 68816   14   145   44   9%      1  130   26    2 1338%
c i   43.9   82284   552047     11774    7288    946 68823   14   145   44   9%      1  130   26    2 1320%
c i   44.0   82282   552047     11935    7425    954 68834   14   147   44   9%      1  131   23    2 1179%
c i   44.1   82269   552047     12014    7497    956 68837   14   146   44   9%      1  131   19    2  975%
c i   44.2   82268   552047     12088    7563    959 68839   14   146   44   9%      1  131   19    2  940%
c i   44.2   82143   552047     12090    7563    960 68839   14   146   44   9%      1  130   19    2  933%
c i   44.6   82142   552047     12540    7933    994 68873   14   147   44   9%      2  131   15    2  720%
c i   45.1   82137   552047     12879    8220   1018 68898   14   151   44   9%      2  134   15    2  714%
c i   45.1   82132   552047     12920    8248   1023 68904   14   152   44   9%      2  134   14    2  655%
c i   45.2   82128   552047     12945    8270   1025 68904   14   153   44   9%      2  135   14    2  651%
c i   45.2   82123   552047     12969    8287   1026 68909   14   153   44   9%      2  136   15    2  687%
c i   45.3   82083   552047     13028    8341   1028 68911   14   153   44   9%      2  135   15    2  700%
c i   45.3   82074   552047     13029    8341   1028 68911   14   153   44   9%      2  135   15    2  697%
c i   45.4   82026   552047     13138    8431   1033 68920   14   156   44   9%      2  138   16    2  745%
c i   45.6   82025   552047     13462    8713   1050 68939   14   155   44   9%      2  136   14    2  629%
c i   45.7   82022   552047     13590    8834   1053 68941   14   154   44   9%      2  136   18    2  761%
c i   45.9   82020   552047     13664    8887   1067 68947   14   162   44   9%      2  143   17    2  712%
c i   45.9   82015   552047     13678    8899   1067 68948   14   161   44   9%      2  142   16    2  709%
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   45.9   82014   552047     13717    8931   1072 68949   14   161   44   9%      2  142   16    2  682%
c i   46.1   82007   552047     13875    9064   1075 68959   15   159   44   9%      1  140   23    2  965%
c i   46.2   82002   552047     13985    9159   1082 68965   15   162   44   9%      1  143   20    2  810%
c i   46.2   81996   552047     13986    9159   1082 68965   15   162   44   9%      1  142   19    2  807%
c i   46.4   81989   552047     14062    9216   1089 68976   15   165   44   9%      1  145   17    2  693%
c i   46.5   81988   552047     14174    9311   1093 68986   15   166   44   9%      1  147   23    2  915%
c i   46.6   81987   552047     14198    9332   1094 68987   15   167   44   9%      1  147   22    2  880%
c i   46.7   81984   552047     14356    9465   1109 68993   15   168   44   9%      1  148   18    2  717%
c i   46.7   81983   552047     14360    9468   1109 68993   15   168   44   9%      1  148   18    2  711%
c i   47.2   81976   552047     14747    9810   1120 69014   16   170   44  10%      2  149   29    3 1110%
c i   47.2   81975   552047     14806    9859   1120 69019   17   170   44  10%      2  148   31    3 1137%
c i   47.3   81972   552047     14915    9947   1130 69025   17   172   45  10%      2  150   25    3  934%
c i   47.4   81969   552047     14964    9990   1132 69026   17   171   45  10%      1  150   26    3  946%
c i   47.5   81968   552047     15040   10059   1133 69027   17   170   45  10%      1  148   26    3  947%
c i   47.5   81961   552047     15103   10115   1136 69029   17   170   45  10%      1  148   25    3  893%
c i   47.7   81955   552047     15208   10209   1142 69033   17   170   45  10%      1  148   21    3  755%
c i   47.8   81952   552047     15283   10269   1149 69040   17   174   45  10%      1  152   20    3  697%
c i   47.9   81949   552047     15347   10319   1152 69049   17   175   45  10%      1  153   19    3  685%
c i   48.1   81890   552047     15549   10499   1161 69059   18   175   45  10%      1  152   28    3  962%
c i   48.1   81885   552047     15636   10575   1166 69061   18   175   45  10%      1  152   27    3  923%
c i   48.1   81879   552047     15637   10575   1166 69061   18   175   45  10%      1  151   27    3  919%
c i   48.3   81876   552047     15923   10836   1174 69070   18   171   45  10%      1  147   18    3  593%
c i   48.4   81873   552047     16018   10914   1179 69074   18   172   45  10%      1  148   21    3  693%
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   48.5   81870   552047     16146   11031   1180 69083   18   174   46  10%      1  150   22    3  708%
c i   48.7   81869   552047     16285   11153   1188 69089   18   173   46  10%      1  149   21    3  673%
c i   48.7   81865   552047     16351   11210   1193 69091   18   173   46  10%      1  148   20    3  647%
c i   48.7   81852   552047     16355   11212   1193 69092   18   173   46  10%      1  148   20    3  638%
c i   48.9   81829   552047     16504   11340   1200 69100   19   174   46  11%      1  148   29    3  913%
c i   49.0   81827   552047     16539   11369   1202 69103   19   174   46  11%      1  149   27    3  850%
c i   49.2   81826   552047     16696   11495   1216 69112   19   174   46  11%      1  149   20    3  629%
c i   49.2   81822   552047     16712   11509   1216 69113   18   174   46  11%      1  148   20    3  615%
c i   49.2   81821   552047     16713   11509   1216 69113   18   174   46  11%      1  148   20    3  613%
c i   49.3   81820   552047     16785   11572   1221 69116   19   177   46  11%      1  151   21    3  634%
c i   49.4   81819   552047     16839   11616   1226 69118   19   176   46  11%      1  151   20    3  605%
c i   49.5   81814   552047     16873   11646   1228 69119   18   177   46  10%      1  151   19    3  573%
c i   49.5   81813   552047     16911   11675   1233 69121   18   178   46  10%      1  152   18    3  561%
c i   49.6   81804   552047     16966   11725   1233 69123   19   178   46  10%      1  152   19    3  585%
c i   49.7   81803   552047     17084   11823   1241 69130   18   177   46  10%      1  151   18    3  556%
c i   50.0   81795   552047     17292   12003   1253 69140   19   179   46  11%      1  152   23    3  688%
c i   50.0   81794   552047     17304   12013   1254 69140   19   179   46  11%      1  152   22    3  665%
c i   50.1   81790   552047     17432   12130   1257 69147   19   180   47  10%      1  153   21    3  616%
c i   50.3   81783   552047     17508   12200   1259 69150   19   181   47  10%      1  154   21    3  608%
c i   50.3   81778   552047     17568   12256   1261 69151   19   185   47  10%      1  158   24    3  689%
c i   50.4   81777   552047     17604   12289   1262 69151   19   184   47  10%      1  157   22    3  643%
c i   50.7   81774   552047     17846   12496   1276 69165   19   189   47  10%      1  161   25    4  708%
c i   50.7   81773   552047     17847   12496   1276 69165   19   189   47  10%      1  161   25    4  706%
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   51.3   81770   552047     18436   12998   1299 69219   19   189   47  10%      3  159   21    4  566%
c i   51.3   81764   552047     18437   12998   1299 69219   19   189   47  10%      3  159   21    4  564%
c i   51.5   81762   552047     18521   13076   1301 69222   20   193   47  10%      2  163   22    4  591%
c i   51.5   81670   552047     18542   13093   1302 69224   19   192   47  10%      2  162   21    4  563%
c i   51.5   81665   552047     18543   13093   1302 69224   19   192   47  10%      2  162   21    4  561%
c i   51.5   81662   552047     18564   13107   1303 69228   19   192   47  10%      2  162   20    4  531%
c i   51.6   81656   552047     18617   13151   1308 69231   19   191   47  10%      2  161   19    4  510%
c i   51.6   81651   552047     18637   13170   1308 69231   19   191   47  10%      2  161   19    4  519%
c i   51.7   81643   552047     18721   13248   1309 69233   19   191   47  10%      2  161   21    4  547%
c i   51.7   81640   552047     18770   13294   1308 69235   20   191   47  10%      2  161   22    4  590%
c i   51.8   81633   552047     18795   13315   1309 69237   20   192   47  10%      2  162   22    4  570%
c i   51.9   81629   552047     18870   13380   1313 69242   20   199   47  10%      2  168   23    4  605%
c i   51.9   81625   552047     18871   13380   1313 69242   20   199   47  10%      2  168   23    4  602%
c i   52.0   81618   552047     18883   13388   1313 69244   20   199   47  10%      2  168   23    4  614%
c i   52.2   81611   552047     19121   13605   1316 69258   20   195   47  10%      2  164   23    4  604%
c i   52.3   81610   552047     19193   13665   1321 69262   20   194   47  10%      2  163   22    4  566%
c 
c [simplification-9] limit 19257 conflicts (hard 29168) hit after 19257 conflicts
c [quatres-5] found 32459 quaternary clauses 38% in total
c [quatres-5-2] added 1 quaternary resolvents
c [ternres-5] limit 6656872 with penalty 0 = 0 + 0
c [ternres-5] 4245 schedulable variables 5%
c [ternres-5] 2 ternary resolvents (0 bin, 2 trn)
c [ternres-5] fully completed ternary resolution
c [decomp-20] removed 817 variables
c [treelook-4] limit 665687 penalty 0 = 0 + 0 boost 1
c [treelook-4] scheduled 88322 literals 54%
c [treelook-4] scheduling used 666151 steps
c [treelook-4] not fully scheduled
c [treelook-4] limit 665687 penalty 0 = 0 + 0 boost 1
c [treelook-4] used 849487 steps
c [treelook-4] 88290 literals remain 54%
c [treelook-4] 29376 variables remain to probed next time 36%
c [decomp-21] removed 15 variables
c [treelook-4] removed 26 variables, found 5902 hbrs
c [unhide-9] limit 1331374 with penalty 0 = 0 + 0
c [unhide-9-9] 6 units, 171 failed, 10892 tauts, 0 hbrs, 41702 literals
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 244 transitive binary clauses
c [transred-5] found 5 units
c [bca-5] limit of 10000000 steps and 1067112 added (scaled 2)
c [bca-5] 131123 out of 162294 literals actually usable 81%
c [bca-5] added 78 blocked clauses in 380955 steps
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 19970610 penalty 0 = 0 + 0
c [sweep-5-1] 5689 pos 7.0% + 75234 neg 93.0% = 80923 sched 99.7% ret 223
c [sweep-5-1] 20101678 steps 212 queries 3079.58 avg class size
c [sweep-5-1] 2663 decisions 174 SAT calls 95.64 avg env size
c [sweep-5-1] 73728 variables remain 92% (6136 retained 8%)
c [decomp-22] removed 1446 variables
c [sweep-5-1] removed 1446 vars (0 failed, 54 eqs, 74 impls)
c [sweep-5] considered successful since not run to completion yet
c [sweep-5] removed 1446 vars in TOTAL (1 rounds, 211 queries)
c [phase-count-9] 518554 negative 99.3% of 522364 except 3810 0.7%
c [phase-count-9] 415934 positive 79.6% of 522364 except 106430 20.4%
c [phase-count-9] less non-negative clauses 3810 than limit 52200 (10.0%)
c [phase-count-9] non-pos/non-neg = 106430/3810 = 27.93 >= 2.00 = 200/100
c [lucky-phase-9] forcing lucky phase -1
c [phase-9] phase bias: 0 positive 0%, 209 negative 100%
c [sort-queue-9] sorted 79700 enqueued variables after 19257 conflicts
c [score-dist-9] active 0 (0%), one 47447 (60%), zero 32253 (40%)
c [score-dist-9] max exp 1, different 2 (100%)
c [score-dist-9] median active exp 0, avg 0.0
c [simplification-9] removed 1903 variables 2.3% (79700 remain 32%)
c [simplification-9] removed 29683 irredundant clauses 5.4% (522364 remain 38%)
c [simplification-9] maximum reduction of 5% = max (2%, 5%)
c [simplification-9] large reduction 5% >= 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 31257 (soft 21257 + delta 10000)
c [simplification-9] new conflict limit 21257 (hard 31257)
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   55.5   79699   522364     19272   13597   1256 86737   20   194   46  10%      1  162   19    4  479%
c i   55.6   79695   522364     19396   13711   1258 86740   20   191   48  10%      1  159   22    4  553%
c i   55.6   79692   522364     19418   13728   1259 86743   20   190   48  10%      1  158   21    4  527%
c i   55.7   79399   522364     19509   13807   1262 86747   20   190   48  10%      1  158   21    4  525%
c i   55.7   79398   522364     19564   13849   1266 86754   20   189   48  10%      1  157   19    4  470%
c i   55.8   79395   522364     19595   13875   1268 86756   20   190   48  10%      1  157   19    4  479%
c i   55.9   79370   522364     19670   13945   1270 86757   20   193   48  10%      1  160   22    4  557%
c i   56.1   79368   522364     19839   14092   1276 86762   20   195   48  10%      1  162   25    4  615%
c i   56.1   79354   522364     19844   14096   1276 86762   20   195   48  10%      1  161   25    4  610%
c i   56.1   79291   522364     19849   14097   1277 86764   20   195   48  10%      1  161   24    4  600%
c i   56.2   79262   522364     19921   14162   1280 86767   20   195   48  10%      1  161   22    4  544%
c i   56.4   79257   522364     20002   14233   1282 86773   20   196   48  10%      1  162   22    4  527%
c i   56.7   79253   522364     20185   14387   1290 86789   20   197   48  10%      1  163   19    4  452%
c i   56.7   79249   522364     20208   14409   1290 86789   20   199   48  10%      1  165   19    4  449%
c i   57.2   79244   522364     20636   14796   1300 86809   21   199   48  10%      2  164   27    4  630%
c i   57.3   79077   522364     20675   14829   1301 86811   21   199   48  10%      2  164   25    4  572%
c i   57.3   79072   522364     20676   14829   1301 86811   21   199   48  10%      2  163   25    4  570%
c i   57.5   79053   522364     20920   15043   1315 86824   21   200   48  10%      2  164   21    4  479%
c i   57.8   79044   522364     21102   15212   1317 86828   21   203   48  10%      2  167   28    4  620%
c i   57.8   79040   522364     21131   15238   1318 86828   21   204   48  11%      1  167   28    4  636%
c i   57.9   79036   522364     21179   15277   1321 86832   21   203   48  10%      1  167   27    4  595%
c 
c [simplification-10] limit 21271 conflicts (hard 31257) hit after 21271 conflicts
c [quatres-6] found 32122 quaternary clauses 40% in total
c [ternres-6] limit 7408934 with penalty 0 = 0 + 0
c [ternres-6] all 79035 free variables schedulable
c [ternres-6] 35 ternary resolvents (0 bin, 35 trn)
c [ternres-6] 24534 variables remain 31% (54501 retained 69%)
c [card-4] limit 463058 penalty 3 = 3 + 0
c [card-4] found 2113 at-most-one constraints of average size 4.1
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 463058 for elimination
c [card-4] 2113 out of 2113 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [gauss-3] limit 500000 penalty 2 = 2 + 0
c [gauss-3] extracted 92 xors of average arity 2.3
c [gauss-3] connected 216 occurrences of 161 variables (average 1.3)
c [gauss-3] limit 500000 penalty 2 = 2 + 0
c [gauss-3] fully completed
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-23] removed 222 variables
c [basicprobe-4] limit 37044670 penalty 0 = 0 + 0
c [basicprobe-4-0] 27799 probes remain 36% after last round
c [basicprobe-4-0] 185 units = 185 failed (100%) + 0 lifted (0%)
c [basicprobe-4-0] removed 644 variables, found 54320 hbrs
c [bate-2] eliminated 83 asymmetric tautologies during probing
c [unhide-10] limit 1481786 with penalty 0 = 0 + 0
c [unhide-10-10] 14 units, 764 failed, 16038 tauts, 0 hbrs, 36844 literals
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 220 transitive binary clauses
c [transred-6] found 5 units
c [cce-4] boosting limit by 10
c [cce-4] limit of 185223350 steps penalty 1 = 1 + 0
c [cce-4-1] eliminated 903 clauses out of 3011 (30%) of length 6
c [cce-4-1] eliminated 10021 clauses out of 37743 (27%) of length 5
c [cce-4-1] incomplete large round (ATE)
c [cce-4-1] eliminated 10924 large clauses in 185223360 steps
c [cce-4-1] allowing another 92611680 steps for small clauses
c [cce-4-1] scheduling 278942 clauses = 259934 binary + 19008 ternary
c [cce-4-1] tried to eliminate 3430 small clauses 1%
c [cce-4-1] eliminated 915 binary clauses 0%
c [cce-4-1] eliminated 110 ternary clauses 1%
c [cce-4-1] eliminated 1025 small clauses 0%
c [cce-4-1] eliminated 8881 small clauses in 185223352 steps
c [cce-4-1] incomplete small round (ATE)
c [cce-4-1] eliminated 19805 covered clauses in round 1
c [cce-4] eliminated 19805 covered clauses in TOTAL during 1 rounds
c [elim-8] scheduling all variables this time
c [elim-8] scheduled 77399 variables 100%
c [elim-8] boosting limit by 20
c [elim-8] limit of 1481786810 steps penalty 1 = 1 + 0
c [elim-8] rescheduling of touched variables disabled
c [elim-8-1] eliminated 8741 variables 11% in round 1 in 45024654 steps
c [elim-8-1] backward subsumption/strengthening limit 45024600
c [elim-8-1-1] backward checking 23638 touched variables 31%
c [elim-8-1-1] fully completed backward checking in 1 rounds
c [elim-8-1] subsumed 19 and strengthened 376 clauses in 5202638 steps
c [elim-8-1] rescheduled 900 variables 1% by backward subsumption
c [elim-8-2] eliminated 124 variables 0% in round 2 in 1227921 steps
c [elim-8-2] backward subsumption/strengthening limit 1227900
c [elim-8-2-1] backward checking 853 touched variables 1%
c [elim-8-2-1] fully completed backward checking in 1 rounds
c [elim-8-2] subsumed 4 and strengthened 5 clauses in 683647 steps
c [elim-8-2] rescheduled 19 variables 0% by backward subsumption
c [elim-8-3] eliminated 1 variables 0% in round 3 in 157295 steps
c [elim-8-3] backward subsumption/strengthening limit 157200
c [elim-8-3-1] backward checking 10 touched variables 0%
c [elim-8-3-1] incomplete backward checking 0 remain 0%
c [elim-8-3] subsumed 0 and strengthened 2 clauses in 157201 steps
c [elim-8] incomplete 8 not tried 0% in round 3
c [gc-65] reconnected 119969 binary clauses (produced 0 empty 1 units)
c [elim-8] transition to [ all 1 rem 1 ] state
c [elim-8] eliminated 8891 = 11% variables out of 77399 scheduled
c [bca-6] limit of 10000000 steps and 946843 added (scaled 2)
c [bca-6] 120231 out of 137018 literals actually usable 88%
c [bca-6] added 707 blocked clauses in 344767 steps
c [sweep-6] limit 2222680 penalty 0 = 0 + 0
c [sweep-6-1] 5374 pos 8.5% + 57896 neg 91.5% = 63270 sched 92.4% ret 5238
c [sweep-6-1] 2226136 steps 32 queries 12220.28 avg class size
c [sweep-6-1] 309 decisions 29 SAT calls 80.79 avg env size
c [sweep-6-1] 63022 variables remain 92% (5479 retained 8%)
c [decomp-24] removed 48 variables
c [sweep-6-1] removed 48 vars (0 failed, 3 eqs, 6 impls)
c [sweep-6] considered successful since not run to completion yet
c [sweep-6] removed 48 vars in TOTAL (1 rounds, 31 queries)
c [phase-count-10] 471496 negative 99.7% of 472854 except 1358 0.3%
c [phase-count-10] 370085 positive 78.3% of 472854 except 102769 21.7%
c [phase-count-10] less non-negative clauses 1358 than limit 47200 (10.0%)
c [phase-count-10] non-pos/non-neg = 102769/1358 = 75.68 >= 2.00 = 200/100
c [lucky-phase-10] forcing lucky phase -1
c [phase-10] phase bias: 0 positive 0%, 114 negative 100%
c [sort-queue-10] sorted 68460 enqueued variables after 21271 conflicts
c [score-dist-10] active 0 (0%), one 41179 (60%), zero 27281 (40%)
c [score-dist-10] max exp 1, different 2 (100%)
c [score-dist-10] median active exp 0, avg 0.0
c [simplification-10] removed 10575 variables 13.4% (68460 remain 28%)
c [simplification-10] removed 49510 irredundant clauses 9.5% (472854 remain 34%)
c [simplification-10] maximum reduction of 13% = max (13%, 9%)
c [simplification-10] large reduction 13% >= 5% limit
c [simplification-10] next conflict interval 2000 = 2000/1
c [simplification-10] penalized conflict interval 2000 = 1 * 2000
c [simplification-10] hard conflict limit 33271 (soft 23271 + delta 10000)
c [simplification-10] new conflict limit 23271 (hard 33271)
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   68.2   68459   472854     21432    5936   1321 105121   21   201   39  10%      1  164   16    5  353%
c i   68.3   68458   472854     21493    5985   1328 105125   20   201   39  10%      1  163   14    5  307%
c i   68.4   68041   472854     21565    6047   1328 105132   20   200   39  10%      1  162   13    5  296%
c i   68.4   67928   472854     21569    6050   1328 105132   20   200   39  10%      1  162   13    5  292%
c i   68.5   67925   472854     21713    6159   1344 105150   20   198   39  10%      1  160   10    5  231%
c i   68.6   67771   472854     21777    6213   1348 105154   20   197   39  10%      1  159    9    5  206%
c i   68.9   67770   472854     21936    6352   1353 105164   19   197   39  10%      1  159   10    5  228%
c i   69.1   67767   472854     22140    6526   1363 105175   20   196   39  10%      1  157   21    5  456%
c i   69.1   67757   472854     22161    6544   1364 105176   20   196   39  10%      1  157   20    5  430%
c i   69.4   67752   472854     22405    6762   1379 105183   19   194   39  10%      1  155   14    5  310%
c i   69.6   67749   472854     22651    6972   1395 105200   19   193   39  10%      1  153   12    5  247%
c i   69.7   67655   472854     22726    7025   1404 105210   18   191   39  10%      1  151   10    5  208%
c i   69.7   67585   472854     22728    7026   1404 105210   18   191   39  10%      1  151   10    5  206%
c i   69.7   67580   472854     22769    7057   1407 105216   18   190   39  10%      1  150    9    5  189%
c i   69.7   67526   472854     22803    7078   1413 105221   18   189   39  10%      1  149    9    5  184%
c i   69.8   67520   472854     22839    7104   1417 105226   18   188   39  10%      1  148    8    5  169%
c i   69.8   67516   472854     22893    7146   1421 105233   18   187   39  10%      1  146    7    5  153%
c i   69.9   67462   472854     22959    7189   1428 105248   18   186   39  10%      1  145   10    5  215%
c i   69.9   67425   472854     22974    7199   1429 105250   18   186   39  10%      1  145   10    5  212%
c i   69.9   66933   472854     23016    7226   1433 105256   18   185   39  10%      1  144    9    5  194%
c i   70.0   66930   472854     23083    7283   1437 105258   18   184   39  10%      1  143    8    5  179%
c i   70.1   66859   472854     23182    7351   1450 105271   17   183   39   9%      1  142    7    5  158%
c i   70.2   66804   472854     23241    7397   1455 105277   17   182   39   9%      1  141    7    5  155%
c 
c [simplification-11] limit 23278 conflicts (hard 33271) hit after 23278 conflicts
c [ternres-7] limit 8103727 with penalty 0 = 0 + 0
c [ternres-7] 20700 schedulable variables 30%
c [ternres-7] 137 ternary resolvents (0 bin, 137 trn)
c [ternres-7] fully completed ternary resolution
c [decomp-25] removed 1904 variables
c [simpleprobe-5] 3543 schedulable variables 5%
c [simpleprobe-5] limit 32414911 penalty 0 = 0 + 0
c [decomp-26] removed 1208 variables
c [simpleprobe-5] 998 variables remain 2% (64350 retained 98%)
c [simpleprobe-5] removed 1208 variables, found 56907 hbrs, 378 units
c [unhide-11] limit 1620745 with penalty 0 = 0 + 0
c [unhide-11-11] 6 units, 79 failed, 10523 tauts, 0 hbrs, 6125 literals
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 309 transitive binary clauses
c [transred-7] found 5 units
c [block-4] scheduling all variables this time
c [block-4] scheduled 65235 variables 100%
c [block-4] limit of 20259319 steps penalty 2 = 2 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 85 blocked clauses
c [block-4] 85 < 1/100 * 446299 = 4462 considered unsuccessful
c [cce-5] limit of 40518639 steps penalty 0 = 0 + 0
c [cce-5-1] eliminated 1 clauses out of 91 (1%) of length 10
c [cce-5-1] eliminated 1 clauses out of 408 (0%) of length 9
c [cce-5-1] eliminated 2 clauses out of 380 (1%) of length 8
c [cce-5-1] eliminated 5 clauses out of 472 (1%) of length 7
c [cce-5-1] eliminated 2 clauses out of 2635 (0%) of length 6
c [cce-5-1] incomplete large round (ACCE)
c [cce-5-1] eliminated 11 large clauses in 40518640 steps
c [cce-5-1] allowing another 20259320 steps for small clauses
c [cce-5-1] scheduling 365639 clauses = 218010 binary + 147629 ternary
c [cce-5-1] tried to eliminate 555 small clauses 0%
c [cce-5-1] eliminated 78 binary clauses 0%
c [cce-5-1] eliminated 60 ternary clauses 0%
c [cce-5-1] eliminated 138 small clauses 0%
c [cce-5-1] eliminated 138 small clauses in 40518643 steps
c [cce-5-1] incomplete small round (ACCE)
c [cce-5-1] eliminated 149 covered clauses in round 1
c [cce-5] eliminated 149 covered clauses in TOTAL during 1 rounds
c [cce-5] 149 < 1/100 * 445192 = 4451 considered unsuccessful
c [elim-9] no untried remaining variables left
c [elim-9] scheduled 65234 variables 100%
c [elim-9] limit of 162074559 steps penalty 0 = 0 + 0
c [elim-9] rescheduling of touched variables disabled
c [elim-9-1] eliminated 2173 variables 3% in round 1 in 42138349 steps
c [elim-9-1] backward subsumption/strengthening limit 42138300
c [elim-9-1-1] backward checking 6631 touched variables 10%
c [elim-9-1-1] fully completed backward checking in 1 rounds
c [elim-9-1] subsumed 31 and strengthened 39 clauses in 1999855 steps
c [elim-9-1] rescheduled 181 variables 0% by backward subsumption
c [elim-9-2] eliminated 18 variables 0% in round 2 in 236378 steps
c [elim-9-2] backward subsumption/strengthening limit 236300
c [elim-9-2-1] backward checking 150 touched variables 0%
c [elim-9-2-1] fully completed backward checking in 1 rounds
c [elim-9-2] subsumed 0 and strengthened 2 clauses in 156060 steps
c [elim-9-2] rescheduled 8 variables 0% by backward subsumption
c [elim-9-3] no variable eliminated in round 3 in 8849 steps
c [elim-9] fully completed in 3 rounds
c [elim-9] transition to [ all 0 rem 0 ] state
c [elim-9] eliminated 2197 = 3% variables out of 65234 scheduled
c [bca-7] limit of 10000000 steps and 879002 added (scaled 2)
c [bca-7] 105165 out of 126076 literals actually usable 83%
c [bca-7] added 70 blocked clauses in 280469 steps
c [sweep-7] limit 2431118 penalty 0 = 0 + 0
c [sweep-7-1] 5946 pos 10.3% + 52053 neg 89.7% = 57999 sched 92.0% ret 5038
c [sweep-7-1] 2527752 steps 31 queries 12406.23 avg class size
c [sweep-7-1] 325 decisions 23 SAT calls 77.00 avg env size
c [sweep-7-1] 57897 variables remain 92% (5122 retained 8%)
c [decomp-27] removed 29 variables
c [sweep-7-1] removed 29 vars (0 failed, 8 eqs, 12 impls)
c [sweep-7] 29 < 1/1000 * 63037 = 63 considered unsuccessful
c [sweep-7] removed 29 vars in TOTAL (1 rounds, 30 queries)
c [phase-count-11] 437335 negative 99.7% of 438657 except 1322 0.3%
c [phase-count-11] 342311 positive 78.0% of 438657 except 96346 22.0%
c [phase-count-11] skipping relative phase luck test
c [phase-11] phase bias: 27 positive 100%, 0 negative 0%
c [sort-queue-11] sorted 63008 enqueued variables after 23278 conflicts
c [score-dist-11] active 0 (0%), one 43082 (68%), zero 19926 (32%)
c [score-dist-11] max exp 1, different 2 (100%)
c [score-dist-11] median active exp 0, avg 0.0
c [simplification-11] removed 3793 variables 5.7% (63008 remain 26%)
c [simplification-11] removed 34197 irredundant clauses 7.2% (438657 remain 32%)
c [simplification-11] maximum reduction of 7% = max (6%, 7%)
c [simplification-11] large reduction 7% >= 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 35278 (soft 25278 + delta 10000)
c [simplification-11] new conflict limit 25278 (hard 35278)
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   75.6   63007   438657     23480    7160   1540 155540   17   181   39   9%      1  139    8    5  177%
c i   75.7   63003   438657     23565    7227   1549 155546   17   180   39   9%      1  138    9    5  184%
c i   76.1   62909   438657     23945    7555   1572 155564   16   181   39   9%      1  138   11    5  232%
c i   76.6   62906   438657     24372    7916   1596 155600   16   180   39   9%      2  137   13    5  277%
c i   76.7   62905   438657     24395    7936   1597 155601   16   181   39   9%      2  137   13    5  277%
c i   77.0   62881   438657     24718    8213   1613 155622   15   179   39   9%      2  134   14    5  290%
c i   77.0   62880   438657     24732    8223   1614 155624   15   178   39   9%      2  134   13    5  280%
c i   77.3   62879   438657     24964    8425   1628 155635   15   180   39   9%      2  135   13    5  278%
c i   77.4   62878   438657     25043    8501   1629 155636   15   184   39   8%      2  139   15    5  315%
c i   77.4   62840   438657     25049    8504   1630 155637   15   183   39   8%      2  138   15    5  309%
c i   77.6   62837   438657     25188    8628   1633 155647   16   186   39   8%      2  140   18    5  375%
c 
c [simplification-12] limit 25279 conflicts (hard 35278) hit after 25279 conflicts
c [quatres-7] found 29134 quaternary clauses 48% in total
c [quatres-7-1] removed 2 duplicate quaternary clauses
c [quatres-7-2] added 1 single-self-subsuming ternary resolvents
c [quatres-7-2] added 8 quaternary resolvents
c [ternres-8] limit 8852258 with penalty 0 = 0 + 0
c [ternres-8] all 62837 free variables schedulable
c [ternres-8] 238 ternary resolvents (0 bin, 238 trn)
c [ternres-8] 8053 variables remain 13% (54784 retained 87%)
c [decomp-28] removed 175 variables
c [treelook-5] limit 885225 penalty 0 = 0 + 0 boost 1
c [treelook-5] scheduled 85384 literals 68%
c [treelook-5] scheduling used 885227 steps
c [treelook-5] not fully scheduled
c [treelook-5] limit 885225 penalty 0 = 0 + 0 boost 1
c [treelook-5] used 1002605 steps
c [treelook-5] 85349 literals remain 68%
c [treelook-5] 18177 variables remain to probed next time 29%
c [decomp-29] removed 2 variables
c [treelook-5] removed 11 variables, found 7250 hbrs
c [unhide-12] limit 1770451 with penalty 0 = 0 + 0
c [unhide-12-12] 7 units, 522 failed, 19000 tauts, 0 hbrs, 7499 literals
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 274 transitive binary clauses
c [transred-8] found 4 units
c [elim-10] scheduling all variables this time
c [elim-10] scheduled 62299 variables 100%
c [elim-10] limit of 177045160 steps penalty 0 = 0 + 0
c [elim-10] rescheduling of touched variables disabled
c [elim-10-1] eliminated 601 variables 1% in round 1 in 42453317 steps
c [elim-10-1] backward subsumption/strengthening limit 42453300
c [elim-10-1-1] backward checking 2224 touched variables 4%
c [elim-10-1-1] fully completed backward checking in 1 rounds
c [elim-10-1] subsumed 22 and strengthened 10 clauses in 919950 steps
c [elim-10-1] rescheduled 59 variables 0% by backward subsumption
c [elim-10-2] eliminated 10 variables 0% in round 2 in 80635 steps
c [elim-10-2] backward subsumption/strengthening limit 80600
c [elim-10-2-1] backward checking 100 touched variables 0%
c [elim-10-2-1] incomplete backward checking 0 remain 0%
c [elim-10-2] subsumed 39 and strengthened 2 clauses in 80601 steps
c [elim-10-2] rescheduled 48 variables 0% by backward subsumption
c [elim-10-3] eliminated 7 variables 0% in round 3 in 99508 steps
c [elim-10-3] backward subsumption/strengthening limit 99500
c [elim-10-3-1] backward checking 97 touched variables 0%
c [elim-10-3-1] incomplete backward checking 0 remain 0%
c [elim-10-3] subsumed 4 and strengthened 0 clauses in 99501 steps
c [elim-10] incomplete 5 not tried 0% in round 3
c [elim-10] transition to [ all 1 rem 1 ] state
c [elim-10] eliminated 632 = 1% variables out of 62299 scheduled
c [bca-8] limit of 10000000 steps and 861505 added (scaled 2)
c [bca-8] 100047 out of 123336 literals actually usable 81%
c [bca-8] added 58 blocked clauses in 264130 steps
c [phase-count-12] 428929 negative 99.7% of 430124 except 1195 0.3%
c [phase-count-12] 334754 positive 77.8% of 430124 except 95370 22.2%
c [phase-count-12] skipping relative phase luck test
c [phase-12] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-12] sorted 61667 enqueued variables after 25279 conflicts
c [score-dist-12] active 0 (0%), one 43492 (71%), zero 18175 (29%)
c [score-dist-12] max exp 1, different 2 (100%)
c [score-dist-12] median active exp 0, avg 0.0
c [simplification-12] removed 1170 variables 1.9% (61667 remain 25%)
c [simplification-12] removed 8533 irredundant clauses 1.9% (430124 remain 31%)
c [simplification-12] maximum reduction of 2% = max (2%, 2%)
c [simplification-12] geometric conflict interval increment 6666 = 20000 / 3
c [simplification-12] new conflict interval 14666
c [simplification-12] penalized conflict interval 14666 = 1 * 14666
c [simplification-12] hard conflict limit 49945 (soft 39945 + delta 10000)
c [simplification-12] new conflict limit 39945 (hard 49945)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   80.6   61666   430124     25335    8431   1775 134753   16   186   39   8%      1  140   15    5  310%
c i   80.7   61578   430124     25417    8494   1784 134761   15   185   39   8%      1  139   13    5  257%
c i   81.0   61575   430124     25752    8763   1812 134786   15   184   39   8%      2  137   12    5  233%
c i   81.2   61480   430124     25851    8835   1827 134793   15   182   39   8%      1  135   12    5  232%
c i   81.2   61327   430124     25868    8848   1827 134796   15   182   39   8%      1  135   11    5  224%
c i   81.2   61326   430124     25906    8878   1831 134797   15   182   39   8%      1  135   11    5  224%
c i   81.2   61238   430124     25931    8897   1832 134801   15   181   39   8%      1  134   11    5  212%
c i   81.8   60986   430124     26524    9390   1875 134838   15   182   39   8%      3  134   16    5  313%
c i   82.1   60985   430124     26824    9661   1888 134848   15   188   39   8%      3  139   18    5  351%
c i   82.1   60982   430124     26826    9661   1889 134848   15   188   39   8%      3  139   18    5  348%
c i   82.3   60976   430124     26917    9734   1897 134856   15   188   39   8%      2  139   15    5  293%
c i   82.5   60974   430124     27133    9931   1904 134863   16   190   39   8%      2  141   20    5  389%
c i   82.6   60972   430124     27295   10071   1914 134871   16   191   39   8%      2  141   19    5  367%
c i   82.8   60971   430124     27503   10248   1926 134887   16   188   39   8%      2  138   17    5  317%
c i   82.8   60970   430124     27520   10263   1926 134888   16   188   39   8%      2  138   16    5  310%
c i   83.0   60964   430124     27710   10421   1944 134898   16   187   39   8%      2  136   14    5  263%
c i   83.0   60945   430124     27714   10423   1944 134899   16   187   39   8%      2  136   14    5  263%
c i   83.3   60944   430124     28077   10743   1962 134913   16   185   39   9%      2  134   21    5  398%
c i   83.4   60943   430124     28138   10796   1963 134918   16   186   39   9%      2  135   19    5  358%
c i   83.8   60942   430124     28605   11204   1985 134948   16   185   40   9%      2  133   18    5  333%
c i   84.3   60939   430124     29141   11680   1998 134968   18   187   40   9%      3  133   28    6  503%
c i   84.4   60911   430124     29159   11696   1998 134969   18   186   40  10%      3  133   28    6  486%
c i   84.5   60908   430124     29230   11758   2005 134970   18   188   40   9%      3  134   25    6  432%
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   84.5   60903   430124     29233   11759   2005 134971   18   188   40   9%      3  134   24    6  427%
c i   84.6   60858   430124     29341   11849   2010 134981   18   188   40   9%      2  134   22    6  392%
c i   84.6   60854   430124     29345   11851   2010 134982   18   188   40   9%      2  134   22    6  393%
c i   84.6   60850   430124     29367   11872   2010 134982   18   188   40   9%      2  134   24    6  419%
c i   84.7   60849   430124     29406   11905   2011 134986   18   188   40   9%      2  134   22    6  393%
c i   84.8   60846   430124     29485   11973   2015 134989   18   189   40  10%      2  134   25    6  438%
c i   85.1   60845   430124     29857   12308   2030 135006   18   189   41   9%      2  134   19    6  322%
c i   85.2   60841   430124     29923   12362   2034 135010   18   192   41   9%      2  137   20    6  349%
c i   85.3   60829   430124     30004   12436   2036 135013   18   193   41   9%      2  137   20    6  340%
c i   85.7   60784   430124     30331   12724   2053 135027   18   190   41  10%      2  134   22    6  366%
c i   85.9   60783   430124     30517   12900   2055 135033   18   193   41   9%      2  137   19    6  323%
c i   85.9   60782   430124     30545   12927   2055 135033   18   192   41   9%      2  136   20    6  338%
c i   86.4   60781   430124     30937   13283   2068 135051   18   194   41   9%      2  137   21    6  347%
c i   87.2   60780   430124     31644   13893   2105 135093   19   196   42  10%      4  138   24    6  393%
c i   87.2   60777   430124     31697   13942   2107 135093   19   196   42  10%      4  137   22    6  352%
c i   87.3   60773   430124     31709   13950   2107 135093   19   196   42  10%      3  137   22    6  348%
c i   87.6   60770   430124     32103   14298   2124 135110   20   200   42  10%      3  140   30    6  473%
c i   87.6   60763   430124     32105   14299   2124 135110   20   200   42  10%      3  140   30    6  477%
c i   87.9   60762   430124     32340   14509   2132 135116   21   199   42  10%      3  139   29    6  444%
c i   88.7   60711   430124     33041   15143   2157 135139   22   206   43  11%      4  144   26    7  391%
c i   89.0   60706   430124     33278   15352   2170 135147   23   210   43  11%      3  148   33    7  484%
c i   89.0   60703   430124     33284   15356   2170 135148   23   211   43  11%      3  149   33    7  478%
c i   89.9   60699   430124     34109   16093   2203 135181   24   212   43  11%      5  148   31    7  437%
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   90.4   60698   430124     34497   16430   2220 135204   25   223   43  11%      4  158   36    7  490%
c i   90.4   60697   430124     34519   16451   2220 135204   25   223   43  11%      4  158   35    7  482%
c i   90.4   60696   430124     34533   16460   2222 135206   25   223   43  11%      4  158   34    7  473%
c i   90.6   60695   430124     34666   16581   2226 135212   25   227   43  11%      4  162   30    7  416%
c i   90.6   60694   430124     34737   16640   2229 135216   25   229   43  11%      3  164   34    7  468%
c i   90.8   60601   430124     34814   16707   2234 135220   25   230   43  11%      3  164   29    7  398%
c i   90.8   60598   430124     34815   16707   2234 135220   25   230   43  11%      3  164   29    7  396%
c i   90.9   60597   430124     34989   16866   2240 135223   25   228   43  11%      3  161   25    7  338%
c i   91.1   60596   430124     35133   16992   2246 135231   26   228   44  11%      2  162   32    7  425%
c i   91.3   60589   430124     35398   17224   2261 135238   25   222   44  11%      2  155   23    8  310%
c i   91.3   60586   430124     35428   17245   2263 135241   25   223   44  11%      2  156   23    8  310%
c i   91.4   60584   430124     35459   17267   2267 135244   25   223   44  11%      2  155   21    8  284%
c i   92.1   60581   430124     36128   17869   2293 135268   24   220   45  11%      3  151   23    8  305%
c i   92.1   60573   430124     36150   17887   2294 135268   25   220   45  11%      3  151   27    8  358%
c i   92.4   60572   430124     36375   18089   2303 135279   25   218   45  11%      3  149   28    8  366%
c i   92.4   60566   430124     36416   18121   2306 135284   25   218   45  11%      3  149   26    8  339%
c i   92.4   60562   430124     36436   18134   2309 135287   25   217   45  11%      3  148   25    8  317%
c i   92.5   60559   430124     36525   18216   2311 135289   25   218   45  11%      2  148   24    8  314%
c i   92.9   60550   430124     36769   18435   2316 135294   26   222   46  12%      2  152   39    8  490%
c i   93.0   60549   430124     36910   18568   2320 135295   26   221   46  12%      2  150   32    8  400%
c i   93.0   60548   430124     36929   18585   2320 135296   26   221   46  12%      2  150   31    8  384%
c i   93.3   60547   430124     37224   18851   2335 135303   26   218   46  12%      2  147   22    8  269%
c i   93.7   60506   430124     37646   19238   2348 135312   25   215   46  12%      2  143   21    8  258%
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   93.8   60505   430124     37720   19298   2351 135315   25   214   46  12%      2  142   20    8  253%
c i   94.9   60504   430124     38651   20129   2377 135355   26   213   47  12%      5  139   31    8  368%
c i   95.0   60503   430124     38828   20272   2386 135363   26   210   47  12%      4  135   29    8  343%
c i   95.9   60500   430124     39610   21000   2405 135389   28   213   47  13%      5  137   32    9  364%
c i   96.1   60499   430124     39738   21104   2417 135394   28   212   47  13%      5  136   29    9  325%
c 
c [simplification-13] limit 39973 conflicts (hard 49945) hit after 39973 conflicts
c [quatres-8] found 27063 quaternary clauses 46% in total
c [quatres-8-2] added 3 single-self-subsuming ternary resolvents
c [ternres-9] limit 13713612 with penalty 0 = 0 + 0
c [ternres-9] 7773 schedulable variables 13%
c [ternres-9] 119 ternary resolvents (0 bin, 119 trn)
c [ternres-9] fully completed ternary resolution
c [decomp-30] removed 1421 variables
c [basicprobe-5] limit 68568063 penalty 0 = 0 + 0
c [basicprobe-5-0] 17383 probes remain 29% after last round
c [basicprobe-5-0] 409 units = 391 failed (96%) + 18 lifted (4%)
c [basicprobe-5-0] removed 690 variables, found 104892 hbrs
c [bate-3] eliminated 276 asymmetric tautologies during probing
c [unhide-13] limit 2742722 with penalty 0 = 0 + 0
c [unhide-13-14] 22 units, 475 failed, 30371 tauts, 0 hbrs, 112262 literals
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 231 transitive binary clauses
c [transred-9] found 1 units
c [cce-6] limit of 34284031 steps penalty 1 = 1 + 0
c [cce-6-1] eliminated 1 clauses out of 1 (100%) of length 95
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 94
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 93
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 92
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 91
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 90
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 89
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 88
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 87
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 86
c [cce-6-1] eliminated 2 clauses out of 3 (67%) of length 85
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 84
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 83
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 82
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 81
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 80
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 79
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 78
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 77
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 76
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 75
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 74
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 73
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 72
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 71
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 70
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 69
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 68
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 67
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 66
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 65
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 64
c [cce-6-1] eliminated 2 clauses out of 3 (67%) of length 63
c [cce-6-1] eliminated 2 clauses out of 3 (67%) of length 62
c [cce-6-1] eliminated 3 clauses out of 3 (100%) of length 61
c [cce-6-1] eliminated 3 clauses out of 4 (75%) of length 60
c [cce-6-1] eliminated 3 clauses out of 4 (75%) of length 59
c [cce-6-1] eliminated 2 clauses out of 4 (50%) of length 58
c [cce-6-1] eliminated 3 clauses out of 4 (75%) of length 57
c [cce-6-1] eliminated 3 clauses out of 5 (60%) of length 56
c [cce-6-1] eliminated 4 clauses out of 5 (80%) of length 55
c [cce-6-1] eliminated 3 clauses out of 5 (60%) of length 54
c [cce-6-1] eliminated 5 clauses out of 5 (100%) of length 53
c [cce-6-1] eliminated 4 clauses out of 6 (67%) of length 52
c [cce-6-1] eliminated 4 clauses out of 6 (67%) of length 51
c [cce-6-1] eliminated 4 clauses out of 6 (67%) of length 50
c [cce-6-1] eliminated 4 clauses out of 6 (67%) of length 49
c [cce-6-1] eliminated 5 clauses out of 6 (83%) of length 48
c [cce-6-1] eliminated 4 clauses out of 6 (67%) of length 47
c [cce-6-1] eliminated 4 clauses out of 6 (67%) of length 46
c [cce-6-1] eliminated 4 clauses out of 6 (67%) of length 45
c [cce-6-1] eliminated 5 clauses out of 6 (83%) of length 44
c [cce-6-1] eliminated 4 clauses out of 6 (67%) of length 43
c [cce-6-1] eliminated 4 clauses out of 6 (67%) of length 42
c [cce-6-1] eliminated 4 clauses out of 6 (67%) of length 41
c [cce-6-1] eliminated 5 clauses out of 6 (83%) of length 40
c [cce-6-1] eliminated 4 clauses out of 6 (67%) of length 39
c [cce-6-1] eliminated 5 clauses out of 6 (83%) of length 38
c [cce-6-1] eliminated 4 clauses out of 6 (67%) of length 37
c [cce-6-1] eliminated 4 clauses out of 6 (67%) of length 36
c [cce-6-1] eliminated 5 clauses out of 6 (83%) of length 35
c [cce-6-1] eliminated 4 clauses out of 6 (67%) of length 34
c [cce-6-1] eliminated 5 clauses out of 6 (83%) of length 33
c [cce-6-1] eliminated 4 clauses out of 6 (67%) of length 32
c [cce-6-1] eliminated 5 clauses out of 6 (83%) of length 31
c [cce-6-1] eliminated 5 clauses out of 8 (62%) of length 30
c [cce-6-1] eliminated 4 clauses out of 6 (67%) of length 29
c [cce-6-1] eliminated 4 clauses out of 6 (67%) of length 28
c [cce-6-1] eliminated 4 clauses out of 6 (67%) of length 27
c [cce-6-1] eliminated 4 clauses out of 6 (67%) of length 26
c [cce-6-1] eliminated 5 clauses out of 6 (83%) of length 25
c [cce-6-1] eliminated 4 clauses out of 7 (57%) of length 24
c [cce-6-1] eliminated 5 clauses out of 6 (83%) of length 23
c [cce-6-1] eliminated 4 clauses out of 6 (67%) of length 22
c [cce-6-1] eliminated 5 clauses out of 6 (83%) of length 21
c [cce-6-1] eliminated 4 clauses out of 6 (67%) of length 20
c [cce-6-1] eliminated 5 clauses out of 6 (83%) of length 19
c [cce-6-1] eliminated 5 clauses out of 7 (71%) of length 18
c [cce-6-1] eliminated 4 clauses out of 6 (67%) of length 17
c [cce-6-1] eliminated 5 clauses out of 6 (83%) of length 16
c [cce-6-1] eliminated 4 clauses out of 6 (67%) of length 15
c [cce-6-1] eliminated 4 clauses out of 6 (67%) of length 14
c [cce-6-1] eliminated 5 clauses out of 6 (83%) of length 13
c [cce-6-1] eliminated 4 clauses out of 6 (67%) of length 12
c [cce-6-1] eliminated 4 clauses out of 7 (57%) of length 11
c [cce-6-1] eliminated 6 clauses out of 69 (9%) of length 10
c [cce-6-1] eliminated 5 clauses out of 322 (2%) of length 9
c [cce-6-1] eliminated 7 clauses out of 343 (2%) of length 8
c [cce-6-1] eliminated 5 clauses out of 463 (1%) of length 7
c [cce-6-1] eliminated 3 clauses out of 2643 (0%) of length 6
c [cce-6-1] incomplete large round (ATE)
c [cce-6-1] eliminated 290 large clauses in 34284032 steps
c [cce-6-1] allowing another 17142016 steps for small clauses
c [cce-6-1] scheduling 333766 clauses = 203392 binary + 130374 ternary
c [cce-6-1] tried to eliminate 529 small clauses 0%
c [cce-6-1] eliminated 93 binary clauses 0%
c [cce-6-1] eliminated 40 ternary clauses 0%
c [cce-6-1] eliminated 133 small clauses 0%
c [cce-6-1] eliminated 4299 small clauses in 34284031 steps
c [cce-6-1] incomplete small round (ATE)
c [cce-6-1] eliminated 4589 covered clauses in round 1
c [cce-6] eliminated 4589 covered clauses in TOTAL during 1 rounds
c [elim-11] no untried remaining variables left
c [elim-11] scheduled 59053 variables 100%
c [elim-11] limit of 274272254 steps penalty 0 = 0 + 0
c [elim-11] rescheduling of touched variables disabled
c [elim-11-1] eliminated 1344 variables 2% in round 1 in 43432066 steps
c [elim-11-1] backward subsumption/strengthening limit 43432000
c [elim-11-1-1] backward checking 5383 touched variables 9%
c [elim-11-1-1] fully completed backward checking in 1 rounds
c [elim-11-1] subsumed 19 and strengthened 40 clauses in 1734283 steps
c [elim-11-1] rescheduled 149 variables 0% by backward subsumption
c [elim-11-2] eliminated 16 variables 0% in round 2 in 85275 steps
c [elim-11-2] backward subsumption/strengthening limit 85200
c [elim-11-2-1] backward checking 176 touched variables 0%
c [elim-11-2-1] incomplete backward checking 0 remain 0%
c [elim-11-2] subsumed 12 and strengthened 11 clauses in 85201 steps
c [elim-11-2] rescheduled 62 variables 0% by backward subsumption
c [elim-11-3] eliminated 7 variables 0% in round 3 in 42922 steps
c [elim-11-3] backward subsumption/strengthening limit 42900
c [elim-11-3-1] backward checking 53 touched variables 0%
c [elim-11-3-1] incomplete backward checking 0 remain 0%
c [elim-11-3] subsumed 2 and strengthened 6 clauses in 42901 steps
c [elim-11] incomplete 29 not tried 0% in round 3
c [elim-11] transition to [ all 1 rem 1 ] state
c [elim-11] eliminated 1373 = 2% variables out of 59053 scheduled
c [bca-9] limit of 10000000 steps and 804680 added (scaled 2)
c [bca-9] 83890 out of 115362 literals actually usable 73%
c [bca-9] added 58 blocked clauses in 219056 steps
c [sweep-8] limit 2057041 penalty 1 = 1 + 0
c [sweep-8-1] 5231 pos 9.9% + 47874 neg 90.1% = 53105 sched 92.1% ret 4575
c [sweep-8-1] 2203701 steps 23 queries 7524.65 avg class size
c [sweep-8-1] 330 decisions 22 SAT calls 150.00 avg env size
c [sweep-8-1] 52966 variables remain 92% (4710 retained 8%)
c [decomp-31] removed 48 variables
c [sweep-8-1] removed 48 vars (0 failed, 0 eqs, 2 impls)
c [sweep-8] 48 < 1/1000 * 57680 = 57 considered unsuccessful
c [sweep-8] removed 48 vars in TOTAL (1 rounds, 22 queries)
c [phase-count-13] 400422 negative 99.7% of 401580 except 1158 0.3%
c [phase-count-13] 311488 positive 77.6% of 401580 except 90092 22.4%
c [phase-count-13] skipping relative phase luck test
c [phase-13] phase bias: 2 positive 40%, 3 negative 60%
c [sort-queue-13] sorted 57632 enqueued variables after 39973 conflicts
c [score-dist-13] active 0 (0%), one 44254 (77%), zero 13378 (23%)
c [score-dist-13] max exp 1, different 2 (100%)
c [score-dist-13] median active exp 0, avg 0.0
c [simplification-13] removed 2866 variables 4.7% (57632 remain 23%)
c [simplification-13] removed 28544 irredundant clauses 6.6% (401580 remain 29%)
c [simplification-13] maximum reduction of 7% = max (5%, 7%)
c [simplification-13] large reduction 7% >= 5% limit
c [simplification-13] next conflict interval 2000 = 2000/1
c [simplification-13] penalized conflict interval 2000 = 1 * 2000
c [simplification-13] hard conflict limit 51973 (soft 41973 + delta 10000)
c [simplification-13] new conflict limit 41973 (hard 51973)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i  103.8   57631   401580     40024   19334   2425 185994   27   214   47  13%      4  137   22    9  250%
c i  103.9   57629   401580     40172   19464   2435 185999   27   212   48  13%      3  134   21    9  239%
c i  105.3   57628   401580     41358   20533   2482 186045   27   219   48  13%      8  139   32    9  341%
c i  105.4   57618   401580     41473   20636   2486 186050   28   219   48  13%      7  139   31    9  334%
c i  105.8   57617   401580     41861   20992   2501 186056   28   226   48  12%      5  145   34    9  357%
c i  105.9   57616   401580     41954   21065   2512 186064   28   223   48  12%      5  142   26    9  278%
c 
c [simplification-14] limit 41973 conflicts (hard 51973) hit after 41973 conflicts
c [quatres-9] found 26266 quaternary clauses 45% in total
c [quatres-9-1] removed 2 duplicate quaternary clauses
c [quatres-9-2] added 1 single-self-subsuming ternary resolvents
c [quatres-9-2] added 5 quaternary resolvents
c [ternres-10] limit 14353853 with penalty 0 = 0 + 0
c [ternres-10] all 57616 free variables schedulable
c [ternres-10] 184 ternary resolvents (0 bin, 184 trn)
c [ternres-10] fully completed ternary resolution
c [gauss-4] limit 358846 penalty 3 = 3 + 0
c [gauss-4] extracted 18 xors of average arity 2.9
c [gauss-4] connected 52 occurrences of 49 variables (average 1.1)
c [gauss-4] limit 358846 penalty 3 = 3 + 0
c [gauss-4] fully completed
c [gauss-4] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-32] removed 34 variables
c [simpleprobe-6] 883 schedulable variables 2%
c [simpleprobe-6] limit 57415415 penalty 0 = 0 + 0
c [decomp-33] removed 675 variables
c [simpleprobe-6] fully completed simple probing
c [simpleprobe-6] removed 675 variables, found 41487 hbrs, 337 units
c [unhide-14] limit 2870770 with penalty 0 = 0 + 0
c [unhide-14-16] 7 units, 254 failed, 27603 tauts, 0 hbrs, 59839 literals
c [transred-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 272 transitive binary clauses
c [transred-10] found 3 units
c [cce-7] limit of 71769269 steps penalty 0 = 0 + 0
c [cce-7-1] eliminated 1 clauses out of 1 (100%) of length 154
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 153
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 152
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 151
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 150
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 149
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 148
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 147
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 146
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 145
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 144
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 143
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 142
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 141
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 140
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 139
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 138
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 137
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 136
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 135
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 134
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 133
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 132
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 131
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 130
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 129
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 128
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 127
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 126
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 125
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 124
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 123
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 122
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 121
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 120
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 119
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 118
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 117
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 116
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 115
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 114
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 113
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 112
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 111
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 110
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 109
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 108
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 107
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 106
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 105
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 104
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 103
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 102
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 101
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 100
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 99
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 98
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 97
c [cce-7-1] eliminated 1 clauses out of 4 (25%) of length 96
c [cce-7-1] eliminated 3 clauses out of 3 (100%) of length 95
c [cce-7-1] eliminated 3 clauses out of 4 (75%) of length 94
c [cce-7-1] eliminated 3 clauses out of 5 (60%) of length 93
c [cce-7-1] eliminated 3 clauses out of 4 (75%) of length 92
c [cce-7-1] eliminated 3 clauses out of 5 (60%) of length 91
c [cce-7-1] eliminated 3 clauses out of 5 (60%) of length 90
c [cce-7-1] eliminated 5 clauses out of 7 (71%) of length 89
c [cce-7-1] eliminated 4 clauses out of 6 (67%) of length 88
c [cce-7-1] eliminated 5 clauses out of 7 (71%) of length 87
c [cce-7-1] eliminated 4 clauses out of 6 (67%) of length 86
c [cce-7-1] eliminated 5 clauses out of 7 (71%) of length 85
c [cce-7-1] eliminated 5 clauses out of 8 (62%) of length 84
c [cce-7-1] eliminated 5 clauses out of 5 (100%) of length 83
c [cce-7-1] eliminated 3 clauses out of 7 (43%) of length 82
c [cce-7-1] eliminated 6 clauses out of 6 (100%) of length 81
c [cce-7-1] eliminated 3 clauses out of 7 (43%) of length 80
c [cce-7-1] eliminated 6 clauses out of 6 (100%) of length 79
c [cce-7-1] eliminated 3 clauses out of 7 (43%) of length 78
c [cce-7-1] eliminated 6 clauses out of 6 (100%) of length 77
c [cce-7-1] eliminated 3 clauses out of 7 (43%) of length 76
c [cce-7-1] eliminated 6 clauses out of 6 (100%) of length 75
c [cce-7-1] eliminated 3 clauses out of 7 (43%) of length 74
c [cce-7-1] eliminated 6 clauses out of 6 (100%) of length 73
c [cce-7-1] eliminated 3 clauses out of 7 (43%) of length 72
c [cce-7-1] eliminated 6 clauses out of 6 (100%) of length 71
c [cce-7-1] eliminated 3 clauses out of 7 (43%) of length 70
c [cce-7-1] eliminated 6 clauses out of 6 (100%) of length 69
c [cce-7-1] eliminated 3 clauses out of 7 (43%) of length 68
c [cce-7-1] eliminated 6 clauses out of 6 (100%) of length 67
c [cce-7-1] eliminated 3 clauses out of 7 (43%) of length 66
c [cce-7-1] eliminated 6 clauses out of 6 (100%) of length 65
c [cce-7-1] eliminated 3 clauses out of 7 (43%) of length 64
c [cce-7-1] eliminated 6 clauses out of 7 (86%) of length 63
c [cce-7-1] eliminated 3 clauses out of 7 (43%) of length 62
c [cce-7-1] eliminated 6 clauses out of 6 (100%) of length 61
c [cce-7-1] eliminated 3 clauses out of 7 (43%) of length 60
c [cce-7-1] eliminated 6 clauses out of 6 (100%) of length 59
c [cce-7-1] eliminated 3 clauses out of 8 (38%) of length 58
c [cce-7-1] eliminated 6 clauses out of 7 (86%) of length 57
c [cce-7-1] eliminated 3 clauses out of 9 (33%) of length 56
c [cce-7-1] eliminated 6 clauses out of 6 (100%) of length 55
c [cce-7-1] eliminated 3 clauses out of 8 (38%) of length 54
c [cce-7-1] eliminated 6 clauses out of 7 (86%) of length 53
c [cce-7-1] eliminated 3 clauses out of 7 (43%) of length 52
c [cce-7-1] eliminated 6 clauses out of 8 (75%) of length 51
c [cce-7-1] eliminated 3 clauses out of 8 (38%) of length 50
c [cce-7-1] eliminated 6 clauses out of 8 (75%) of length 49
c [cce-7-1] eliminated 3 clauses out of 8 (38%) of length 48
c [cce-7-1] eliminated 6 clauses out of 7 (86%) of length 47
c [cce-7-1] eliminated 3 clauses out of 8 (38%) of length 46
c [cce-7-1] eliminated 6 clauses out of 8 (75%) of length 45
c [cce-7-1] eliminated 3 clauses out of 8 (38%) of length 44
c [cce-7-1] eliminated 6 clauses out of 7 (86%) of length 43
c [cce-7-1] eliminated 3 clauses out of 8 (38%) of length 42
c [cce-7-1] eliminated 5 clauses out of 7 (71%) of length 41
c [cce-7-1] eliminated 4 clauses out of 8 (50%) of length 40
c [cce-7-1] eliminated 5 clauses out of 7 (71%) of length 39
c [cce-7-1] eliminated 4 clauses out of 8 (50%) of length 38
c [cce-7-1] eliminated 5 clauses out of 7 (71%) of length 37
c [cce-7-1] eliminated 4 clauses out of 8 (50%) of length 36
c [cce-7-1] eliminated 5 clauses out of 8 (62%) of length 35
c [cce-7-1] eliminated 4 clauses out of 7 (57%) of length 34
c [cce-7-1] eliminated 5 clauses out of 8 (62%) of length 33
c [cce-7-1] eliminated 4 clauses out of 7 (57%) of length 32
c [cce-7-1] eliminated 5 clauses out of 8 (62%) of length 31
c [cce-7-1] eliminated 4 clauses out of 6 (67%) of length 30
c [cce-7-1] eliminated 5 clauses out of 10 (50%) of length 29
c [cce-7-1] eliminated 5 clauses out of 9 (56%) of length 28
c [cce-7-1] eliminated 5 clauses out of 8 (62%) of length 27
c [cce-7-1] eliminated 3 clauses out of 8 (38%) of length 26
c [cce-7-1] eliminated 6 clauses out of 7 (86%) of length 25
c [cce-7-1] eliminated 3 clauses out of 9 (33%) of length 24
c [cce-7-1] eliminated 6 clauses out of 7 (86%) of length 23
c [cce-7-1] eliminated 3 clauses out of 6 (50%) of length 22
c [cce-7-1] eliminated 6 clauses out of 8 (75%) of length 21
c [cce-7-1] eliminated 3 clauses out of 7 (43%) of length 20
c [cce-7-1] eliminated 6 clauses out of 8 (75%) of length 19
c [cce-7-1] eliminated 3 clauses out of 7 (43%) of length 18
c [cce-7-1] eliminated 6 clauses out of 8 (75%) of length 17
c [cce-7-1] eliminated 4 clauses out of 9 (44%) of length 16
c [cce-7-1] eliminated 5 clauses out of 7 (71%) of length 15
c [cce-7-1] eliminated 4 clauses out of 8 (50%) of length 14
c [cce-7-1] eliminated 6 clauses out of 9 (67%) of length 13
c [cce-7-1] eliminated 3 clauses out of 7 (43%) of length 12
c [cce-7-1] eliminated 5 clauses out of 9 (56%) of length 11
c [cce-7-1] eliminated 4 clauses out of 69 (6%) of length 10
c [cce-7-1] eliminated 5 clauses out of 317 (2%) of length 9
c [cce-7-1] eliminated 4 clauses out of 338 (1%) of length 8
c [cce-7-1] eliminated 7 clauses out of 459 (2%) of length 7
c [cce-7-1] eliminated 28 clauses out of 2622 (1%) of length 6
c [cce-7-1] incomplete large round (ACCE)
c [cce-7-1] eliminated 511 large clauses in 71769271 steps
c [cce-7-1] allowing another 35884635 steps for small clauses
c [cce-7-1] scheduling 215798 clauses = 195124 binary + 20674 ternary
c [cce-7-1] tried to eliminate 1512 small clauses 1%
c [cce-7-1] eliminated 346 binary clauses 0%
c [cce-7-1] eliminated 61 ternary clauses 0%
c [cce-7-1] eliminated 407 small clauses 0%
c [cce-7-1] eliminated 1343 small clauses in 71769272 steps
c [cce-7-1] incomplete small round (ACCE)
c [cce-7-1] eliminated 1854 covered clauses in round 1
c [cce-7] eliminated 1854 covered clauses in TOTAL during 1 rounds
c [cce-7] 1854 < 1/100 * 385316 = 3853 considered unsuccessful
c [elim-12] no untried remaining variables left
c [elim-12] scheduled 56565 variables 100%
c [elim-12] limit of 287077077 steps penalty 0 = 0 + 0
c [elim-12] rescheduling of touched variables disabled
c [elim-12-1] eliminated 553 variables 1% in round 1 in 35542488 steps
c [elim-12-1] backward subsumption/strengthening limit 35542400
c [elim-12-1-1] backward checking 2840 touched variables 5%
c [elim-12-1-1] fully completed backward checking in 1 rounds
c [elim-12-1] subsumed 15 and strengthened 27 clauses in 936115 steps
c [elim-12-1] rescheduled 88 variables 0% by backward subsumption
c [elim-12-2] eliminated 10 variables 0% in round 2 in 68589 steps
c [elim-12-2] backward subsumption/strengthening limit 68500
c [elim-12-2-1] backward checking 83 touched variables 0%
c [elim-12-2-1] incomplete backward checking 0 remain 0%
c [elim-12-2] subsumed 1 and strengthened 4 clauses in 68501 steps
c [elim-12-2] rescheduled 19 variables 0% by backward subsumption
c [elim-12-3] eliminated 2 variables 0% in round 3 in 15136 steps
c [elim-12-3] backward subsumption/strengthening limit 15100
c [elim-12-3-1] backward checking 20 touched variables 0%
c [elim-12-3-1] incomplete backward checking 0 remain 0%
c [elim-12-3] subsumed 0 and strengthened 4 clauses in 15101 steps
c [elim-12] incomplete 16 not tried 0% in round 3
c [elim-12] transition to [ all 1 rem 1 ] state
c [elim-12] eliminated 565 = 1% variables out of 56565 scheduled
c [bca-10] limit of 10000000 steps and 765571 added (scaled 2)
c [bca-10] 81264 out of 112002 literals actually usable 73%
c [bca-10] added 61 blocked clauses in 212528 steps
c [phase-count-14] 381020 negative 99.7% of 382128 except 1108 0.3%
c [phase-count-14] 293232 positive 76.7% of 382128 except 88896 23.3%
c [phase-count-14] skipping relative phase luck test
c [phase-14] phase bias: 1 positive 17%, 5 negative 83%
c [sort-queue-14] sorted 56000 enqueued variables after 41973 conflicts
c [score-dist-14] active 0 (0%), one 43730 (78%), zero 12270 (22%)
c [score-dist-14] max exp 1, different 2 (100%)
c [score-dist-14] median active exp 0, avg 0.0
c [simplification-14] removed 1616 variables 2.8% (56000 remain 23%)
c [simplification-14] removed 19452 irredundant clauses 4.8% (382128 remain 28%)
c [simplification-14] maximum reduction of 5% = max (3%, 5%)
c [simplification-14] large reduction 5% >= 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 53973 (soft 43973 + delta 10000)
c [simplification-14] new conflict limit 43973 (hard 53973)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i  112.4   55999   382128     42151   18191   2523 194925   27   221   44  12%      4  139   25    9  261%
c i  112.4   55998   382128     42207   18238   2526 194929   27   220   44  12%      4  138   23    9  242%
c i  112.6   55997   382128     42468   18480   2532 194934   27   218   44  13%      3  135   27   10  285%
c i  112.9   55996   382128     42760   18744   2540 194947   27   215   44  13%      3  132   26   10  274%
c i  113.2   55995   382128     43051   19002   2549 194951   27   211   44  13%      2  127   29   10  294%
c i  113.3   55992   382128     43149   19091   2553 194952   28   210   44  13%      2  127   29   10  302%
c i  113.3   55989   382128     43169   19110   2553 194952   28   211   44  13%      2  127   29   10  294%
c i  113.3   55982   382128     43180   19118   2554 194953   27   210   44  13%      2  127   28   10  286%
c i  113.5   55979   382128     43305   19232   2558 194958   28   210   44  13%      2  126   34   10  347%
c i  113.5   55970   382128     43384   19308   2558 194959   28   209   44  13%      1  125   31   10  313%
c 
c [simplification-15] limit 43973 conflicts (hard 53973) hit after 43973 conflicts
c [quatres-10] found 25589 quaternary clauses 45% in total
c [quatres-10-2] added 1 single-self-subsuming ternary resolvents
c [ternres-11] limit 14934803 with penalty 0 = 0 + 0
c [ternres-11] all 55970 free variables schedulable
c [ternres-11] 190 ternary resolvents (0 bin, 190 trn)
c [ternres-11] fully completed ternary resolution
c [card-5] limit 466712 penalty 4 = 4 + 0
c [card-5] found 1549 at-most-one constraints of average size 4.0
c [card-5] no at-most-two constraint found
c [card-5] using previous limit 466712 for elimination
c [card-5] 1549 out of 1549 constraints (100%) meet size limits
c [card-5] no units found
c [card-5] no at-most-one constraints generated
c [decomp-34] removed 40 variables
c [treelook-6] limit 1493480 penalty 0 = 0 + 0 boost 1
c [treelook-6] scheduled 88819 literals 79%
c [treelook-6] scheduling used 1275268 steps
c [treelook-6] scheduled completely
c [treelook-6] limit 1493480 penalty 0 = 0 + 0 boost 1
c [treelook-6] used 1626822 steps
c [treelook-6] 88788 literals remain 79%
c [treelook-6] 15676 variables remain to probed next time 28%
c [treelook-6] removed 1 variables, found 13223 hbrs
c [unhide-15] limit 2986960 with penalty 0 = 0 + 0
c [unhide-15-18] 3 units, 118 failed, 16500 tauts, 0 hbrs, 31030 literals
c [transred-11] limit 2000000 with penalty 0 = 0 + 0
c [transred-11] removed 211 transitive binary clauses
c [transred-11] found 2 units
c [block-5] scheduling all variables this time
c [block-5] scheduled 55809 variables 100%
c [block-5] limit of 18668504 steps penalty 3 = 3 + 0
c [block-5] fully completed
c [block-5] transition to [ all 0 rem 0 ] state
c [block-5] eliminated 26 blocked clauses
c [block-5] 26 < 1/100 * 378712 = 3787 considered unsuccessful
c [elim-13] no untried remaining variables left
c [elim-13] scheduled 55806 variables 100%
c [elim-13] almost no limit of 100000000000 steps
c [elim-13] rescheduling of touched variables disabled
c [elim-13-1] eliminated 152 variables 0% in round 1 in 34737749 steps
c [elim-13-1] backward subsumption/strengthening limit 34737700
c [elim-13-1-1] backward checking 1144 touched variables 2%
c [elim-13-1-1] fully completed backward checking in 1 rounds
c [elim-13-1] subsumed 3 and strengthened 7 clauses in 446368 steps
c [elim-13-1] rescheduled 28 variables 0% by backward subsumption
c [elim-13-2] eliminated 4 variables 0% in round 2 in 19629 steps
c [elim-13-2] backward subsumption/strengthening limit 19600
c [elim-13-2-1] backward checking 39 touched variables 0%
c [elim-13-2-1] incomplete backward checking 11 remain 28%
c [elim-13-2] subsumed 0 and strengthened 6 clauses in 19625 steps
c [elim-13-2] rescheduled 18 variables 0% by backward subsumption
c [elim-13-3] eliminated 2 variables 0% in round 3 in 12566 steps
c [elim-13-3] backward subsumption/strengthening limit 12500
c [elim-13-3-1] backward checking 32 touched variables 0%
c [elim-13-3-1] incomplete backward checking 11 remain 34%
c [elim-13-3] subsumed 6 and strengthened 2 clauses in 12548 steps
c [elim-13] incomplete 13 not tried 0% in round 3
c [elim-13] transition to [ all 1 rem 1 ] state
c [elim-13] eliminated 158 = 0% variables out of 55806 scheduled
c [elim-13] 158 < 1/100 * 55806 = 558 considered unsuccessful
c [bca-11] limit of 10000000 steps and 756296 added (scaled 2)
c [bca-11] 79921 out of 111298 literals actually usable 72%
c [bca-11] added 26 blocked clauses in 210664 steps
c [phase-count-15] 376372 negative 99.7% of 377475 except 1103 0.3%
c [phase-count-15] 289409 positive 76.7% of 377475 except 88066 23.3%
c [phase-count-15] skipping relative phase luck test
c [phase-15] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-15] sorted 55648 enqueued variables after 43973 conflicts
c [score-dist-15] active 0 (0%), one 43593 (78%), zero 12055 (22%)
c [score-dist-15] max exp 1, different 2 (100%)
c [score-dist-15] median active exp 0, avg 0.0
c [simplification-15] removed 322 variables 0.6% (55648 remain 23%)
c [simplification-15] removed 4653 irredundant clauses 1.2% (377475 remain 27%)
c [simplification-15] maximum reduction of 1% = max (1%, 1%)
c [simplification-15] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-15] new conflict interval 24666
c [simplification-15] penalized conflict interval 24666 = 1 * 24666
c [simplification-15] hard conflict limit 80972 (soft 68639 + delta 12333)
c [simplification-15] new conflict limit 68639 (hard 80972)
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  118.3   55647   377475     44263   19924   2675 192255   27   210   46  13%      4  124   22   10  223%
c i  118.5   55646   377475     44491   20132   2679 192263   27   206   46  13%      4  120   28   10  273%
c i  118.5   55645   377475     44492   20132   2679 192263   27   206   46  13%      4  120   28   10  272%
c i  118.5   55643   377475     44498   20136   2680 192263   27   206   46  13%      4  120   27   10  267%
c i  118.6   55642   377475     44575   20206   2682 192266   28   206   46  13%      3  120   31   10  302%
c i  118.7   55641   377475     44700   20312   2693 192271   27   205   46  13%      3  119   24   10  234%
c i  118.8   55640   377475     44762   20366   2694 192273   27   203   46  13%      3  116   23   10  225%
c i  118.8   55638   377475     44792   20395   2694 192273   27   203   46  13%      3  116   24   10  238%
c i  118.9   55637   377475     44882   20479   2695 192276   27   201   46  13%      2  114   23   10  230%
c i  119.1   55636   377475     45146   20723   2703 192278   27   199   46  14%      2  112   30   10  291%
c i  120.2   55635   377475     46163   21648   2746 192312   27   201   46  13%      6  112   30   11  287%
c i  120.3   55602   377475     46245   21724   2747 192315   27   200   46  13%      5  111   27   11  254%
c i  120.4   55601   377475     46390   21852   2748 192323   27   197   46  13%      4  108   23   11  220%
c i  121.5   55600   377475     47402   22764   2785 192362   26   194   46  14%      6  103   29   11  274%
c i  121.5   55599   377475     47403   22764   2785 192362   26   194   46  14%      6  103   29   11  273%
c i  121.5   55582   377475     47446   22798   2787 192368   26   194   46  14%      6  103   28   11  264%
c i  121.6   55580   377475     47555   22901   2788 192370   26   193   46  13%      5  102   23   11  215%
c i  121.8   55579   377475     47769   23095   2792 192373   26   190   46  14%      4   98   24   11  218%
c i  122.1   55578   377475     48006   23317   2798 192378   27   195   46  14%      4  103   34   11  310%
c i  122.5   55577   377475     48395   23677   2807 192384   27   194   46  14%      3  101   26   11  233%
c i  122.7   55510   377475     48541   23808   2811 192389   26   195   46  14%      3  102   24   11  216%
c i  123.0   55509   377475     48760   24003   2820 192393   26   195   46  14%      2  101   25   11  227%
c i  123.2   55502   377475     48937   24159   2832 192397   27   197   46  14%      2  103   37   11  332%
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i  123.3   55496   377475     49036   24246   2838 192402   27   195   46  14%      2  102   31   11  275%
c i  123.3   55495   377475     49037   24246   2838 192402   27   195   46  14%      2  102   31   11  274%
c i  123.3   55455   377475     49047   24255   2838 192402   27   196   46  14%      1  102   33   11  297%
c i  124.0   55454   377475     49560   24730   2846 192415   28   199   46  14%      2  105   33   11  292%
c i  124.0   55451   377475     49563   24732   2846 192415   28   199   46  14%      2  105   33   11  289%
c i  124.0   55450   377475     49564   24732   2846 192415   28   199   46  14%      2  105   33   11  288%
c i  124.5   55447   377475     49997   25128   2864 192428   28   201   46  14%      2  106   31   12  271%
c i  124.7   55444   377475     50130   25252   2866 192431   29   201   46  14%      2  105   30   12  263%
c i  125.0   55438   377475     50486   25563   2881 192448   29   199   46  15%      2  103   39   12  330%
c i  125.4   55437   377475     50904   25939   2888 192457   30   199   47  15%      2  102   42   12  354%
c i  125.4   55435   377475     50916   25950   2888 192457   30   198   47  15%      2  102   41   12  342%
c i  125.9   55433   377475     51441   26417   2901 192472   33   202   49  16%      2  105   43   12  352%
c i  126.1   55432   377475     51585   26544   2904 192477   33   205   49  16%      2  107   48   12  389%
c i  126.5   55431   377475     52100   27018   2918 192489   32   206   50  16%      2  108   24   12  195%
c i  126.7   55423   377475     52228   27129   2920 192489   34   209   50  16%      2  110   53   13  419%
c i  126.9   55414   377475     52418   27296   2927 192495   35   211   50  17%      2  112   50   13  396%
c i  127.0   55413   377475     52517   27375   2929 192498   37   213   50  17%      1  114   71   13  552%
c i  127.0   55412   377475     52578   27420   2937 192502   37   214   50  17%      1  114   60   13  472%
c i  127.0   55411   377475     52579   27420   2937 192502   37   214   50  17%      1  114   60   13  470%
c i  127.7   55410   377475     53242   28013   2948 192516   38   213   51  18%      3  112   53   13  405%
c i  127.7   55408   377475     53244   28014   2948 192516   38   213   51  18%      3  112   53   13  402%
c i  127.8   55401   377475     53381   28145   2950 192518   38   211   51  18%      2  110   47   13  359%
c i  128.1   55400   377475     53680   28420   2954 192520   39   213   52  19%      2  111   58   13  431%
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  128.1   55399   377475     53699   28438   2954 192520   39   212   52  19%      2  111   55   13  411%
c i  128.2   55398   377475     53742   28477   2955 192521   39   212   52  19%      2  111   52   13  387%
c i  128.8   55397   377475     54371   29064   2962 192529   38   214   52  18%      3  112   32   14  232%
c i  129.0   55396   377475     54604   29267   2965 192534   41   217   53  19%      2  114   60   14  432%
c i  129.2   55387   377475     54819   29458   2969 192539   42   217   53  20%      2  113   68   14  482%
c i  129.5   55386   377475     55169   29779   2975 192550   43   218   53  20%      2  114   57   14  402%
c i  129.7   55385   377475     55358   29948   2980 192557   43   218   53  20%      1  114   48   14  333%
c i  130.8   55384   377475     56351   30829   3010 192576   45   223   53  20%      5  117   60   15  400%
c i  131.0   55380   377475     56530   30994   3013 192583   45   226   53  20%      4  120   51   15  340%
c i  131.1   55379   377475     56674   31115   3025 192586   44   227   53  20%      3  120   37   15  248%
c i  131.2   55377   377475     56794   31229   3025 192588   44   226   55  20%      3  119   37   15  249%
c i  131.5   55237   377475     57122   31531   3033 192593   44   227   55  19%      2  119   45   15  294%
c i  131.9   55236   377475     57532   31899   3044 192602   44   225   55  19%      2  117   39   15  256%
c i  131.9   55235   377475     57562   31919   3050 192604   43   224   55  19%      2  116   36   15  235%
c i  132.0   55234   377475     57655   32000   3057 192608   43   222   55  19%      2  114   31   15  204%
c i  132.3   55233   377475     57925   32234   3065 192615   44   222   55  20%      1  113   47   15  301%
c i  132.6   55232   377475     58208   32484   3069 192619   45   225   56  20%      1  116   60   16  381%
c i  132.7   55230   377475     58396   32642   3085 192624   45   224   56  20%      1  114   49   16  313%
c i  132.8   55229   377475     58425   32668   3086 192624   45   223   56  20%      1  114   48   16  308%
c i  133.0   55228   377475     58680   32891   3094 192635   45   220   56  20%      1  110   50   16  316%
c i  133.3   55227   377475     59022   33200   3106 192645   46   227   57  20%      1  116   51   16  315%
c i  134.0   55226   377475     59614   33732   3116 192662   46   233   58  20%      2  121   48   16  292%
c i  134.2   55044   377475     59803   33898   3127 192668   46   231   59  20%      2  119   41   16  247%
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.2   55043   377475     59843   33935   3128 192669   45   231   59  20%      1  119   38   16  234%
c i  134.9   55039   377475     60439   34456   3142 192685   46   229   60  20%      2  115   59   17  353%
c i  134.9   54999   377475     60440   34456   3142 192685   46   229   60  20%      2  115   59   17  351%
c i  134.9   54995   377475     60441   34456   3142 192685   46   229   60  20%      2  115   59   17  350%
c i  134.9   54994   377475     60457   34466   3145 192687   46   228   60  20%      2  115   56   17  335%
c i  135.3   54993   377475     60845   34810   3158 192704   47   227   61  21%      2  113   46   17  272%
c i  135.7   54992   377475     61285   35210   3168 192706   49   229   61  21%      2  114   61   17  354%
c i  135.9   54991   377475     61421   35319   3171 192708   50   227   61  22%      2  113   64   17  368%
c i  136.3   54990   377475     61856   35706   3188 192726   47   224   61  21%      2  108   36   17  208%
c i  136.6   54987   377475     62149   35962   3193 192736   49   224   61  22%      1  108   52   18  291%
c i  136.6   54986   377475     62150   35962   3193 192736   49   224   61  22%      1  108   51   18  290%
c i  137.1   54982   377475     62675   36426   3204 192752   48   220   61  22%      2  103   42   18  235%
c i  137.1   54977   377475     62688   36437   3204 192752   48   221   61  22%      2  104   47   18  263%
c i  137.4   54975   377475     62911   36636   3206 192755   48   215   61  22%      1   97   43   18  240%
c i  137.4   54973   377475     62912   36636   3206 192755   48   215   61  22%      1   97   43   18  239%
c i  138.0   54972   377475     63458   37132   3221 192767   51   224   61  23%      2  106   69   18  376%
c i  138.7   54944   377475     64155   37764   3237 192785   51   224   61  23%      3  105   52   19  277%
c i  139.3   54943   377475     64661   38241   3247 192792   50   224   62  22%      3  104   48   19  252%
c i  139.4   54941   377475     64717   38294   3247 192792   50   224   62  22%      3  104   47   19  246%
c i  139.7   54940   377475     65039   38582   3250 192796   51   228   62  22%      2  107   51   19  265%
c i  140.9   54920   377475     66200   39645   3285 192817   51   227   62  22%      7  105   52   20  262%
c i  140.9   54916   377475     66204   39645   3286 192819   51   227   62  22%      7  105   51   20  258%
c i  141.3   54823   377475     66620   40018   3291 192825   51   224   64  23%      5  100   52   20  258%
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  141.3   54822   377475     66621   40018   3291 192825   51   224   64  23%      5  100   51   20  257%
c i  141.4   54814   377475     66725   40111   3292 192829   51   223   64  23%      4  100   53   20  265%
c i  141.5   54813   377475     66854   40235   3292 192832   51   227   64  23%      4  103   53   20  263%
c i  142.2   54725   377475     67528   40835   3305 192846   54   230   66  23%      4  105   53   21  258%
c i  142.2   54724   377475     67531   40836   3306 192846   54   230   66  23%      4  105   52   21  255%
c i  142.3   54722   377475     67630   40917   3310 192854   53   233   66  23%      3  108   46   21  221%
c i  142.3   54690   377475     67671   40951   3314 192856   53   233   66  23%      3  108   43   21  211%
c i  142.6   54689   377475     67861   41118   3315 192856   53   232   66  23%      2  107   54   21  259%
c 
c [simplification-16] limit of 482 iterations hit after 482 iterations
c [quatres-11] found 24010 quaternary clauses 43% in total
c [quatres-11-1] removed 1 duplicate quaternary clauses
c [quatres-11-2] added 2 single-self-subsuming ternary resolvents
c [quatres-11-2] added 1 quaternary resolvents
c [ternres-12] limit 21456794 with penalty 0 = 0 + 0
c [ternres-12] all 54678 free variables schedulable
c [ternres-12] 78 ternary resolvents (0 bin, 78 trn)
c [ternres-12] fully completed ternary resolution
c [decomp-36] removed 1027 variables
c [basicprobe-6] limit 107283973 penalty 0 = 0 + 0
c [basicprobe-6-0] 13397 probes remain 25% after last round
c [basicprobe-6-0] 650 units = 645 failed (99%) + 5 lifted (1%)
c [basicprobe-6-0] removed 1160 variables, found 147116 hbrs
c [bate-4] eliminated 440 asymmetric tautologies during probing
c [unhide-16] limit 2145679 with penalty 1 = 0 + 1
c [unhide-16-19] 8 units, 373 failed, 33435 tauts, 0 hbrs, 157426 literals
c [transred-12] limit 2000000 with penalty 0 = 0 + 0
c [transred-12] removed 301 transitive binary clauses
c [transred-12] found 3 units
c [cce-8] boosting limit by 10
c [cce-8] limit of 536419865 steps penalty 1 = 1 + 0
c [cce-8-1] eliminated 2 clauses out of 434 (0%) of length 7
c [cce-8-1] eliminated 2 clauses out of 2535 (0%) of length 6
c [cce-8-1] eliminated 10161 clauses out of 19303 (53%) of length 5
c [cce-8-1] eliminated 10418 clauses out of 22090 (47%) of length 4
c [cce-8-1] completed large round (ATE)
c [cce-8-1] eliminated 20583 large clauses in 523813130 steps
c [cce-8-1] allowing another 261906565 steps for small clauses
c [cce-8-1] scheduling 287586 clauses = 191287 binary + 96299 ternary
c [cce-8-1] tried to eliminate 13298 small clauses 5%
c [cce-8-1] eliminated 2141 binary clauses 1%
c [cce-8-1] eliminated 751 ternary clauses 1%
c [cce-8-1] eliminated 2892 small clauses 1%
c [cce-8-1] eliminated 5379 small clauses in 536419865 steps
c [cce-8-1] incomplete small round (ATE)
c [cce-8-1] eliminated 25962 covered clauses in round 1
c [cce-8] eliminated 25962 covered clauses in TOTAL during 1 rounds
c [bca-12] limit of 10000000 steps and 660749 added (scaled 2)
c [bca-12] 69629 out of 106420 literals actually usable 65%
c [bca-12] added 49 blocked clauses in 190673 steps
c [sweep-9] limit 1609259 penalty 2 = 2 + 0
c [sweep-9-1] 4785 pos 9.6% + 44895 neg 90.4% = 49680 sched 93.4% ret 3529
c [sweep-9-1] 1728334 steps 21 queries 8680.76 avg class size
c [sweep-9-1] 753 decisions 17 SAT calls 745.41 avg env size
c [sweep-9-1] 49566 variables remain 93% (3620 retained 7%)
c [decomp-37] removed 100 variables
c [sweep-9-1] removed 100 vars (0 failed, 3 eqs, 6 impls)
c [sweep-9] removed 100 vars in TOTAL (1 rounds, 20 queries)
c [phase-count-16] 328354 negative 99.8% of 329153 except 799 0.2%
c [phase-count-16] 240489 positive 73.1% of 329153 except 88664 26.9%
c [phase-count-16] skipping relative phase luck test
c [phase-16] phase bias: 0 positive 0%, 1 negative 100%
c [sort-queue-16] sorted 53109 enqueued variables after 67861 conflicts
c [score-dist-16] active 0 (0%), one 42925 (81%), zero 10184 (19%)
c [score-dist-16] max exp 1, different 2 (100%)
c [score-dist-16] median active exp 0, avg 0.0
c [simplification-16] removed 1569 variables 2.9% (53109 remain 22%)
c [simplification-16] removed 48322 irredundant clauses 12.8% (329153 remain 24%)
c [simplification-16] maximum reduction of 13% = max (3%, 13%)
c [simplification-16] forced so keeping old conflict interval 24666
c [simplification-16] conflict limit remains at 68754 (hard 80972)
c [simplification-16] new iteration interval 1000
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i  164.1   53108   329153     67962   40456   4227 291526   53   233   73  23%      2  107   43   21  209%
c 
c [simplification-17] limit 68754 conflicts (hard 80972) hit after 68754 conflicts
c [quatres-12] found 13285 quaternary clauses 39% in total
c [quatres-12-1] removed 1 duplicate quaternary clauses
c [quatres-12-2] added 1 single-self-subsuming ternary resolvents
c [quatres-12-2] added 3 quaternary resolvents
c [ternres-13] limit 21677516 with penalty 0 = 0 + 0
c [ternres-13] all 53108 free variables schedulable
c [ternres-13] 51 ternary resolvents (0 bin, 51 trn)
c [ternres-13] fully completed ternary resolution
c [decomp-38] removed 1 variables
c [simpleprobe-7] all 53108 free variables schedulable
c [simpleprobe-7] limit 86710065 penalty 0 = 0 + 0
c [decomp-39] removed 915 variables
c [simpleprobe-7] fully completed simple probing
c [simpleprobe-7] removed 915 variables, found 50926 hbrs, 466 units
c [unhide-17] limit 2167751 with penalty 1 = 0 + 1
c [unhide-17-21] 4 units, 111 failed, 43670 tauts, 0 hbrs, 148872 literals
c [transred-13] limit 2000000 with penalty 0 = 0 + 0
c [transred-13] removed 340 transitive binary clauses
c [transred-13] found 2 units
c [cce-9] limit of 108387581 steps penalty 0 = 0 + 0
c [cce-9-1] eliminated 5 clauses out of 9017 (0%) of length 5
c [cce-9-1] incomplete large round (ACCE)
c [cce-9-1] eliminated 5 large clauses in 108387605 steps
c [cce-9-1] allowing another 54193802 steps for small clauses
c [cce-9-1] scheduling 200458 clauses = 180945 binary + 19513 ternary
c [cce-9-1] tried to eliminate 3192 small clauses 2%
c [cce-9-1] eliminated 672 binary clauses 0%
c [cce-9-1] eliminated 172 ternary clauses 1%
c [cce-9-1] eliminated 844 small clauses 0%
c [cce-9-1] eliminated 1903 small clauses in 108387583 steps
c [cce-9-1] incomplete small round (ACCE)
c [cce-9-1] eliminated 1908 covered clauses in round 1
c [cce-9] eliminated 1908 covered clauses in TOTAL during 1 rounds
c [cce-9] 1908 < 1/100 * 314350 = 3143 considered unsuccessful
c [elim-14] no untried remaining variables left
c [elim-14] scheduled 52045 variables 100%
c [elim-14] limit of 216775163 steps penalty 1 = 1 + 0
c [elim-14] rescheduling of touched variables disabled
c [elim-14-1] eliminated 8559 variables 16% in round 1 in 26490908 steps
c [elim-14-1] backward subsumption/strengthening limit 26490900
c [elim-14-1-1] backward checking 22516 touched variables 43%
c [elim-14-1-1] fully completed backward checking in 1 rounds
c [elim-14-1] subsumed 19 and strengthened 79 clauses in 3679300 steps
c [elim-14-1] rescheduled 225 variables 0% by backward subsumption
c [elim-14-2] eliminated 22 variables 0% in round 2 in 174173 steps
c [elim-14-2] backward subsumption/strengthening limit 174100
c [elim-14-2-1] backward checking 235 touched variables 0%
c [elim-14-2-1] incomplete backward checking 0 remain 0%
c [elim-14-2] subsumed 4 and strengthened 21 clauses in 174101 steps
c [elim-14-2] rescheduled 79 variables 0% by backward subsumption
c [elim-14-3] eliminated 6 variables 0% in round 3 in 57170 steps
c [elim-14-3] backward subsumption/strengthening limit 57100
c [elim-14-3-1] backward checking 69 touched variables 0%
c [elim-14-3-1] incomplete backward checking 0 remain 0%
c [elim-14-3] subsumed 1 and strengthened 10 clauses in 57101 steps
c [elim-14] incomplete 42 not tried 0% in round 3
c [elim-14] transition to [ all 1 rem 1 ] state
c [elim-14] eliminated 8587 = 16% variables out of 52045 scheduled
c [bca-13] limit of 10000000 steps and 590923 added (scaled 2)
c [bca-13] 66004 out of 86918 literals actually usable 76%
c [bca-13] added 149 blocked clauses in 159955 steps
c [phase-count-17] 294033 negative 99.7% of 294770 except 737 0.3%
c [phase-count-17] 212200 positive 72.0% of 294770 except 82570 28.0%
c [phase-count-17] skipping relative phase luck test
c [phase-17] phase bias: 0 positive 0%, 1 negative 100%
c [sort-queue-17] sorted 43458 enqueued variables after 68754 conflicts
c [score-dist-17] active 0 (0%), one 35035 (81%), zero 8423 (19%)
c [score-dist-17] max exp 1, different 2 (100%)
c [score-dist-17] median active exp 0, avg 0.0
c [simplification-17] removed 9650 variables 18.2% (43458 remain 18%)
c [simplification-17] removed 34383 irredundant clauses 10.4% (294770 remain 21%)
c [simplification-17] maximum reduction of 18% = max (18%, 10%)
c [simplification-17] large reduction 18% >= 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 80754 (soft 70754 + delta 10000)
c [simplification-17] new conflict limit 70754 (hard 80754)
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  174.1   43457   294770     69204   12593   3822 250361   47   224   36  21%      7   97   30   21  141%
c i  174.1   43456   294770     69215   12599   3825 250362   47   224   36  21%      7   96   29   21  137%
c i  174.1   43455   294770     69216   12599   3825 250362   47   224   36  21%      7   96   29   21  136%
c i  174.4   43451   294770     70197   13478   3860 250384   41   198   37  21%      7   70   27   21  131%
c i  174.6   43450   294770     70431   13686   3869 250394   40   199   37  20%      5   70   27   21  128%
c i  174.7   43449   294770     70558   13793   3875 250399   40   199   37  20%      5   70   34   21  163%
c i  174.8   43402   294770     70742   13958   3883 250408   39   198   37  20%      4   68   24   21  117%
c 
c [simplification-18] limit 70764 conflicts (hard 80754) hit after 70766 conflicts
c [quatres-13] found 17635 quaternary clauses 48% in total
c [quatres-13-1] removed 2 duplicate quaternary clauses
c [quatres-13-2] added 3 single-self-subsuming ternary resolvents
c [quatres-13-2] added 5 quaternary resolvents
c [ternres-14] limit 21927313 with penalty 0 = 0 + 0
c [ternres-14] all 43402 free variables schedulable
c [ternres-14] 688 ternary resolvents (0 bin, 688 trn)
c [ternres-14] fully completed ternary resolution
c [decomp-40] removed 65 variables
c [treelook-7] limit 2192731 penalty 0 = 0 + 0 boost 1
c [treelook-7] scheduled 60040 literals 69%
c [treelook-7] scheduling used 996214 steps
c [treelook-7] scheduled completely
c [treelook-7] limit 2192731 penalty 0 = 0 + 0 boost 1
c [treelook-7] used 2208780 steps
c [treelook-7] 59978 literals remain 69%
c [treelook-7] 9885 variables remain to probed next time 23%
c [treelook-7] removed 4 variables, found 15773 hbrs
c [unhide-18] limit 4385462 with penalty 0 = 0 + 0
c [unhide-18-24] 2 units, 148 failed, 29811 tauts, 0 hbrs, 53010 literals
c [transred-14] limit 2000000 with penalty 0 = 0 + 0
c [transred-14] removed 293 transitive binary clauses
c [transred-14] found 1 units
c [elim-15] no untried remaining variables left
c [elim-15] scheduled 43268 variables 100%
c [elim-15] limit of 438546260 steps penalty 0 = 0 + 0
c [elim-15] rescheduling of touched variables disabled
c [elim-15-1] eliminated 188 variables 0% in round 1 in 25691372 steps
c [elim-15-1] backward subsumption/strengthening limit 25691300
c [elim-15-1-1] backward checking 1376 touched variables 3%
c [elim-15-1-1] fully completed backward checking in 1 rounds
c [elim-15-1] subsumed 2 and strengthened 10 clauses in 348893 steps
c [elim-15-1] rescheduled 38 variables 0% by backward subsumption
c [elim-15-2] eliminated 5 variables 0% in round 2 in 22363 steps
c [elim-15-2] backward subsumption/strengthening limit 22300
c [elim-15-2-1] backward checking 52 touched variables 0%
c [elim-15-2-1] incomplete backward checking 24 remain 46%
c [elim-15-2] subsumed 0 and strengthened 6 clauses in 22301 steps
c [elim-15-2] rescheduled 24 variables 0% by backward subsumption
c [elim-15-3] eliminated 1 variables 0% in round 3 in 20247 steps
c [elim-15-3] backward subsumption/strengthening limit 20200
c [elim-15-3-1] backward checking 37 touched variables 0%
c [elim-15-3-1] incomplete backward checking 2 remain 5%
c [elim-15-3] subsumed 0 and strengthened 4 clauses in 20242 steps
c [elim-15] incomplete 16 not tried 0% in round 3
c [elim-15] transition to [ all 1 rem 1 ] state
c [elim-15] eliminated 194 = 0% variables out of 43268 scheduled
c [elim-15] 194 < 1/100 * 43268 = 432 considered unsuccessful
c [bca-14] limit of 10000000 steps and 582290 added (scaled 2)
c [bca-14] 64285 out of 86150 literals actually usable 75%
c [bca-14] added 46 blocked clauses in 157496 steps
c [sweep-10] limit 3289096 penalty 1 = 1 + 0
c [sweep-10-1] 4853 pos 12.1% + 35367 neg 87.9% = 40220 sched 93.4% ret 2854
c [sweep-10-1] 3317247 steps 58 queries 4059.67 avg class size
c [sweep-10-1] 1023 decisions 52 SAT calls 186.96 avg env size
c [sweep-10-1] 39395 variables remain 92% (3642 retained 8%)
c [decomp-42] removed 73 variables
c [sweep-10-1] removed 73 vars (0 failed, 7 eqs, 10 impls)
c [sweep-10] removed 73 vars in TOTAL (1 rounds, 57 queries)
c [phase-count-18] 289318 negative 99.8% of 290040 except 722 0.2%
c [phase-count-18] 208869 positive 72.0% of 290040 except 81171 28.0%
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 43001 enqueued variables after 70766 conflicts
c [score-dist-18] active 0 (0%), one 34840 (81%), zero 8161 (19%)
c [score-dist-18] max exp 1, different 2 (100%)
c [score-dist-18] median active exp 0, avg 0.0
c [simplification-18] removed 401 variables 0.9% (43001 remain 17%)
c [simplification-18] removed 4730 irredundant clauses 1.6% (290040 remain 21%)
c [simplification-18] maximum reduction of 2% = max (1%, 2%)
c [simplification-18] geometric conflict interval increment 8222 = 24666 / 3
c [simplification-18] new conflict interval 32888
c [simplification-18] penalized conflict interval 32888 = 1 * 32888
c [simplification-18] hard conflict limit 120098 (soft 103654 + delta 16444)
c [simplification-18] new conflict limit 103654 (hard 120098)
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  178.4   43000   290040     71353   14156   4407 237357   35   184   37  19%      3   54   13   21   62%
c i  182.8   42999   290040     79023   21250   4574 237485   33   187   44  17%     97   52   40   22  182%
c i  183.2   42983   290040     79607   21781   4596 237497   34   188   44  18%     53   53   50   22  226%
c i  183.6   42982   290040     80112   22245   4606 237510   33   185   44  18%     31   50   29   22  131%
c i  183.6   42979   290040     80128   22253   4609 237513   33   185   44  18%     30   49   27   22  124%
c i  183.6   42967   290040     80215   22338   4609 237514   33   186   44  18%     27   50   30   22  137%
c i  184.4   42966   290040     81336   23391   4629 237523   35   189   45  19%     10   53   46   22  207%
c i  184.7   42965   290040     81765   23789   4636 237528   36   188   47  19%      5   51   40   23  178%
c i  184.7   42964   290040     81771   23793   4636 237529   36   188   47  19%      5   51   39   23  174%
c i  184.7   42960   290040     81779   23798   4638 237529   36   188   47  19%      5   51   39   23  171%
c i  185.7   42959   290040     83264   25164   4681 237554   34   183   47  19%      5   45   29   23  128%
c i  187.6   42930   290040     86053   27715   4743 237606   33   165   50  20%     21   25   32   23  140%
c i  188.7   42928   290040     87454   29011   4772 237632   34   167   54  20%      8   28   30   23  130%
c i  189.2   42886   290040     88059   29567   4786 237641   35   175   55  20%      3   35   38   24  162%
c i  190.5   42847   290040     89773   31120   4837 237672   38   180   55  21%      7   39   43   24  179%
c i  190.5   42834   290040     89774   31120   4837 237672   38   180   55  21%      7   39   43   24  179%
c i  190.5   42830   290040     89816   31154   4838 237674   37   179   55  21%      6   38   38   24  159%
c i  193.0   42823   290040     93277   34322   4889 237722   37   170   57  22%     29   27   35   25  142%
c i  193.0   42820   290040     93278   34322   4889 237722   37   170   57  22%     29   27   35   25  141%
c i  195.1   42813   290040     96250   37072   4949 237761   35   161   58  22%     23   17   30   25  121%
c i  199.3   42812   290040    101495   41931   5057 237826   39   166   63  23%     54   21   36   26  139%
c 
c [simplification-19] limit 103676 conflicts (hard 120098) hit after 103676 conflicts
c [quatres-14] found 17861 quaternary clauses 44% in total
c [quatres-14-2] added 1 single-self-subsuming ternary resolvents
c [quatres-14-2] added 5 quaternary resolvents
c [ternres-15] limit 28135390 with penalty 0 = 0 + 0
c [ternres-15] all 42812 free variables schedulable
c [ternres-15] 176 ternary resolvents (0 bin, 176 trn)
c [ternres-15] fully completed ternary resolution
c [gauss-5] limit 351692 penalty 4 = 4 + 0
c [gauss-5] extracted 12 xors of average arity 2.5
c [gauss-5] connected 30 occurrences of 30 variables (average 1.0)
c [gauss-5] limit 351692 penalty 4 = 4 + 0
c [gauss-5] fully completed
c [gauss-5] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-43] removed 17 variables
c [basicprobe-7] limit 140676954 penalty 0 = 0 + 0
c [basicprobe-7-0] 6833 probes remain 16% after last round
c [basicprobe-7-0] 637 units = 616 failed (97%) + 21 lifted (3%)
c [basicprobe-7-0] removed 957 variables, found 165337 hbrs
c [bate-5] eliminated 851 asymmetric tautologies during probing
c [unhide-19] limit 2813539 with penalty 1 = 0 + 1
c [unhide-19-26] 3 units, 67 failed, 37938 tauts, 0 hbrs, 510330 literals
c [transred-15] limit 2000000 with penalty 0 = 0 + 0
c [transred-15] removed 313 transitive binary clauses
c [transred-15] found 1 units
c [cce-10] limit of 70338477 steps penalty 1 = 1 + 0
c [cce-10-1] eliminated 1 clauses out of 1 (100%) of length 93
c [cce-10-1] eliminated 2 clauses out of 3 (67%) of length 92
c [cce-10-1] eliminated 1 clauses out of 3 (33%) of length 91
c [cce-10-1] eliminated 2 clauses out of 5 (40%) of length 90
c [cce-10-1] eliminated 1 clauses out of 3 (33%) of length 89
c [cce-10-1] eliminated 2 clauses out of 4 (50%) of length 88
c [cce-10-1] eliminated 1 clauses out of 4 (25%) of length 87
c [cce-10-1] eliminated 2 clauses out of 4 (50%) of length 86
c [cce-10-1] eliminated 1 clauses out of 4 (25%) of length 85
c [cce-10-1] eliminated 2 clauses out of 5 (40%) of length 84
c [cce-10-1] eliminated 1 clauses out of 3 (33%) of length 83
c [cce-10-1] eliminated 2 clauses out of 6 (33%) of length 82
c [cce-10-1] eliminated 1 clauses out of 2 (50%) of length 81
c [cce-10-1] eliminated 2 clauses out of 5 (40%) of length 80
c [cce-10-1] eliminated 1 clauses out of 3 (33%) of length 79
c [cce-10-1] eliminated 2 clauses out of 5 (40%) of length 78
c [cce-10-1] eliminated 1 clauses out of 3 (33%) of length 77
c [cce-10-1] eliminated 2 clauses out of 5 (40%) of length 76
c [cce-10-1] eliminated 1 clauses out of 3 (33%) of length 75
c [cce-10-1] eliminated 2 clauses out of 5 (40%) of length 74
c [cce-10-1] eliminated 1 clauses out of 2 (50%) of length 73
c [cce-10-1] eliminated 2 clauses out of 6 (33%) of length 72
c [cce-10-1] eliminated 1 clauses out of 3 (33%) of length 71
c [cce-10-1] eliminated 2 clauses out of 5 (40%) of length 70
c [cce-10-1] eliminated 1 clauses out of 3 (33%) of length 69
c [cce-10-1] eliminated 2 clauses out of 5 (40%) of length 68
c [cce-10-1] eliminated 1 clauses out of 3 (33%) of length 67
c [cce-10-1] eliminated 2 clauses out of 5 (40%) of length 66
c [cce-10-1] eliminated 1 clauses out of 4 (25%) of length 65
c [cce-10-1] eliminated 2 clauses out of 4 (50%) of length 64
c [cce-10-1] eliminated 1 clauses out of 4 (25%) of length 63
c [cce-10-1] eliminated 2 clauses out of 5 (40%) of length 62
c [cce-10-1] eliminated 1 clauses out of 4 (25%) of length 61
c [cce-10-1] eliminated 2 clauses out of 4 (50%) of length 60
c [cce-10-1] eliminated 1 clauses out of 4 (25%) of length 59
c [cce-10-1] eliminated 2 clauses out of 4 (50%) of length 58
c [cce-10-1] eliminated 1 clauses out of 4 (25%) of length 57
c [cce-10-1] eliminated 2 clauses out of 5 (40%) of length 56
c [cce-10-1] eliminated 1 clauses out of 5 (20%) of length 55
c [cce-10-1] eliminated 2 clauses out of 5 (40%) of length 54
c [cce-10-1] eliminated 1 clauses out of 5 (20%) of length 53
c [cce-10-1] eliminated 2 clauses out of 4 (50%) of length 52
c [cce-10-1] eliminated 1 clauses out of 5 (20%) of length 51
c [cce-10-1] eliminated 2 clauses out of 3 (67%) of length 50
c [cce-10-1] eliminated 1 clauses out of 5 (20%) of length 49
c [cce-10-1] eliminated 3 clauses out of 7 (43%) of length 48
c [cce-10-1] eliminated 1 clauses out of 3 (33%) of length 47
c [cce-10-1] eliminated 2 clauses out of 6 (33%) of length 46
c [cce-10-1] eliminated 1 clauses out of 5 (20%) of length 45
c [cce-10-1] eliminated 2 clauses out of 6 (33%) of length 44
c [cce-10-1] eliminated 1 clauses out of 4 (25%) of length 43
c [cce-10-1] eliminated 2 clauses out of 7 (29%) of length 42
c [cce-10-1] eliminated 1 clauses out of 4 (25%) of length 41
c [cce-10-1] eliminated 2 clauses out of 5 (40%) of length 40
c [cce-10-1] eliminated 1 clauses out of 5 (20%) of length 39
c [cce-10-1] eliminated 2 clauses out of 7 (29%) of length 38
c [cce-10-1] eliminated 1 clauses out of 4 (25%) of length 37
c [cce-10-1] eliminated 2 clauses out of 6 (33%) of length 36
c [cce-10-1] eliminated 1 clauses out of 5 (20%) of length 35
c [cce-10-1] eliminated 2 clauses out of 4 (50%) of length 34
c [cce-10-1] eliminated 1 clauses out of 5 (20%) of length 33
c [cce-10-1] eliminated 2 clauses out of 4 (50%) of length 32
c [cce-10-1] eliminated 1 clauses out of 4 (25%) of length 31
c [cce-10-1] eliminated 2 clauses out of 5 (40%) of length 30
c [cce-10-1] eliminated 1 clauses out of 5 (20%) of length 29
c [cce-10-1] eliminated 2 clauses out of 4 (50%) of length 28
c [cce-10-1] eliminated 1 clauses out of 5 (20%) of length 27
c [cce-10-1] eliminated 2 clauses out of 7 (29%) of length 26
c [cce-10-1] eliminated 2 clauses out of 9 (22%) of length 25
c [cce-10-1] eliminated 4 clauses out of 7 (57%) of length 24
c [cce-10-1] eliminated 2 clauses out of 9 (22%) of length 23
c [cce-10-1] eliminated 4 clauses out of 6 (67%) of length 22
c [cce-10-1] eliminated 2 clauses out of 7 (29%) of length 21
c [cce-10-1] eliminated 4 clauses out of 6 (67%) of length 20
c [cce-10-1] eliminated 2 clauses out of 7 (29%) of length 19
c [cce-10-1] eliminated 4 clauses out of 7 (57%) of length 18
c [cce-10-1] eliminated 2 clauses out of 8 (25%) of length 17
c [cce-10-1] eliminated 4 clauses out of 7 (57%) of length 16
c [cce-10-1] eliminated 2 clauses out of 7 (29%) of length 15
c [cce-10-1] eliminated 4 clauses out of 9 (44%) of length 14
c [cce-10-1] eliminated 4 clauses out of 10 (40%) of length 13
c [cce-10-1] eliminated 3 clauses out of 8 (38%) of length 12
c [cce-10-1] eliminated 6 clauses out of 11 (55%) of length 11
c [cce-10-1] eliminated 4 clauses out of 11 (36%) of length 10
c [cce-10-1] eliminated 6 clauses out of 12 (50%) of length 9
c [cce-10-1] eliminated 3 clauses out of 15 (20%) of length 8
c [cce-10-1] eliminated 33 clauses out of 63 (52%) of length 7
c [cce-10-1] eliminated 251 clauses out of 3107 (8%) of length 6
c [cce-10-1] incomplete large round (ATE)
c [cce-10-1] eliminated 449 large clauses in 70338479 steps
c [cce-10-1] allowing another 35169239 steps for small clauses
c [cce-10-1] scheduling 168749 clauses = 152514 binary + 16235 ternary
c [cce-10-1] tried to eliminate 2445 small clauses 1%
c [cce-10-1] eliminated 493 binary clauses 0%
c [cce-10-1] eliminated 105 ternary clauses 1%
c [cce-10-1] eliminated 598 small clauses 0%
c [cce-10-1] eliminated 1707 small clauses in 70338480 steps
c [cce-10-1] incomplete small round (ATE)
c [cce-10-1] eliminated 2156 covered clauses in round 1
c [cce-10] eliminated 2156 covered clauses in TOTAL during 1 rounds
c [cce-10] 2156 < 1/100 * 273030 = 2730 considered unsuccessful
c [bca-15] limit of 10000000 steps and 543229 added (scaled 2)
c [bca-15] 54079 out of 83394 literals actually usable 65%
c [bca-15] added 34 blocked clauses in 163367 steps
c [sweep-11] boosting sweeping limit by 10
c [sweep-11] limit 84406170 penalty 0 = 0 + 0
c [sweep-11-1] 4509 pos 11.7% + 34011 neg 88.3% = 38520 sched 92.4% ret 3176
c [sweep-11-1] 84456674 steps 1576 queries 149.70 avg class size
c [sweep-11-1] 24242 decisions 1424 SAT calls 138.18 avg env size
c [sweep-11-1] 16908 variables remain 41% (24690 retained 59%)
c [decomp-44] removed 452 variables
c [sweep-11-1] removed 452 vars (0 failed, 179 eqs, 314 impls)
c [sweep-11] removed 452 vars in TOTAL (1 rounds, 1575 queries)
c [phase-count-19] 268807 negative 99.7% of 269498 except 691 0.3%
c [phase-count-19] 190120 positive 70.5% of 269498 except 79378 29.5%
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 41244 enqueued variables after 103676 conflicts
c [score-dist-19] active 0 (0%), one 34991 (85%), zero 6253 (15%)
c [score-dist-19] max exp 1, different 2 (100%)
c [score-dist-19] median active exp 0, avg 0.0
c [simplification-19] removed 1568 variables 3.7% (41244 remain 17%)
c [simplification-19] removed 20542 irredundant clauses 7.1% (269498 remain 20%)
c [simplification-19] maximum reduction of 7% = max (4%, 7%)
c [simplification-19] large reduction 7% >= 5% limit
c [simplification-19] next conflict interval 2000 = 2000/1
c [simplification-19] penalized conflict interval 2000 = 1 * 2000
c [simplification-19] hard conflict limit 115676 (soft 105676 + delta 10000)
c [simplification-19] new conflict limit 105676 (hard 115676)
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  216.4   41243   269498    104091   44605   5702 378287   37   147   80  25%     18    1   35   26  133%
c i  217.3   41241   269498    105222   45659   5716 378307   37   151   80  24%      4    5   41   27  155%
c i  218.0   41240   269498    105959   46334   5725 378316   39   155   80  25%     -2   10   45   27  167%
c i  218.0   41239   269498    106065   46433   5727 378318   39   154   80  25%     -3    8   38   27  142%
c i  218.3   41233   269498    106345   46680   5728 378322   40   155   80  26%     -5    9   58   27  213%
c i  219.2   41232   269498    107440   47694   5747 378331   41   153   80  27%     -4    7   40   27  147%
c i  219.2   41231   269498    107453   47703   5747 378333   40   152   80  27%     -4    6   39   27  143%
c 
c [simplification-20] limit 105676 conflicts (hard 115676) hit after 108942 conflicts
c [quatres-15] found 17346 quaternary clauses 43% in total
c [quatres-15-1] removed 1 duplicate quaternary clauses
c [quatres-15-2] added 2 single-self-subsuming ternary resolvents
c [quatres-15-2] added 1 quaternary resolvents
c [ternres-16] limit 29170215 with penalty 0 = 0 + 0
c [ternres-16] all 41196 free variables schedulable
c [ternres-16] 547 ternary resolvents (1 bin, 546 trn)
c [ternres-16] fully completed ternary resolution
c [decomp-45] removed 53 variables
c [simpleprobe-8] all 41191 free variables schedulable
c [simpleprobe-8] limit 116680862 penalty 0 = 0 + 0
c [decomp-46] removed 615 variables
c [simpleprobe-8] fully completed simple probing
c [simpleprobe-8] removed 615 variables, found 75927 hbrs, 316 units
c [unhide-20] limit 2917021 with penalty 1 = 0 + 1
c [unhide-20-27] 0 units, 21 failed, 50338 tauts, 0 hbrs, 167380 literals
c [transred-16] limit 2000000 with penalty 0 = 0 + 0
c [transred-16] removed 527 transitive binary clauses
c [block-6] scheduling all variables this time
c [block-6] scheduled 40553 variables 100%
c [block-6] limit of 18231384 steps penalty 4 = 4 + 0
c [block-6] fully completed
c [block-6] transition to [ all 0 rem 0 ] state
c [block-6] eliminated 92 blocked clauses
c [block-6] 92 < 1/100 * 263139 = 2631 considered unsuccessful
c [elim-16] no untried remaining variables left
c [elim-16] scheduled 40550 variables 100%
c [elim-16] limit of 291702156 steps penalty 1 = 1 + 0
c [elim-16] rescheduling of touched variables disabled
c [elim-16-1] eliminated 909 variables 2% in round 1 in 21573160 steps
c [elim-16-1] backward subsumption/strengthening limit 21573100
c [elim-16-1-1] backward checking 5153 touched variables 13%
c [elim-16-1-1] fully completed backward checking in 1 rounds
c [elim-16-1] subsumed 10 and strengthened 46 clauses in 1204587 steps
c [elim-16-1] rescheduled 166 variables 0% by backward subsumption
c [elim-16-2] eliminated 18 variables 0% in round 2 in 123453 steps
c [elim-16-2] backward subsumption/strengthening limit 123400
c [elim-16-2-1] backward checking 173 touched variables 0%
c [elim-16-2-1] incomplete backward checking 0 remain 0%
c [elim-16-2] subsumed 1 and strengthened 23 clauses in 123401 steps
c [elim-16-2] rescheduled 74 variables 0% by backward subsumption
c [elim-16-3] eliminated 6 variables 0% in round 3 in 133283 steps
c [elim-16-3] backward subsumption/strengthening limit 133200
c [elim-16-3-1] backward checking 68 touched variables 0%
c [elim-16-3-1] fully completed backward checking in 1 rounds
c [elim-16-3] subsumed 0 and strengthened 10 clauses in 94791 steps
c [elim-16] incomplete 40 not tried 0% in round 3
c [elim-16] transition to [ all 1 rem 1 ] state
c [elim-16] eliminated 933 = 2% variables out of 40550 scheduled
c [bca-16] limit of 10000000 steps and 523660 added (scaled 2)
c [bca-16] 49933 out of 79236 literals actually usable 63%
c [bca-16] added 30 blocked clauses in 153437 steps
c [sweep-12] limit 8751064 penalty 0 = 0 + 0
c [sweep-12-1] 2124 pos 13.1% + 14033 neg 86.9% = 16157 sched 40.8% ret 23460
c [sweep-12-1] 8753870 steps 184 queries 789.72 avg class size
c [sweep-12-1] 4119 decisions 170 SAT calls 162.50 avg env size
c [sweep-12-1] 15159 variables remain 38% (24443 retained 62%)
c [decomp-47] removed 32 variables
c [sweep-12-1] removed 32 vars (0 failed, 17 eqs, 25 impls)
c [sweep-12] 32 < 1/1000 * 39617 = 39 considered unsuccessful
c [sweep-12] removed 32 vars in TOTAL (1 rounds, 183 queries)
c [phase-count-20] 260229 negative 99.7% of 260897 except 668 0.3%
c [phase-count-20] 181505 positive 69.6% of 260897 except 79392 30.4%
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 39585 enqueued variables after 108942 conflicts
c [score-dist-20] active 0 (0%), one 34240 (86%), zero 5345 (14%)
c [score-dist-20] max exp 1, different 2 (100%)
c [score-dist-20] median active exp 0, avg 0.0
c [simplification-20] removed 1611 variables 3.9% (39585 remain 16%)
c [simplification-20] removed 8601 irredundant clauses 3.2% (260897 remain 19%)
c [simplification-20] maximum reduction of 4% = max (4%, 3%)
c [simplification-20] geometric conflict interval increment 6577 = 32888 / 5
c [simplification-20] new conflict interval 39465
c [simplification-20] penalized conflict interval 39465 = 1 * 39465
c [simplification-20] hard conflict limit 168139 (soft 148407 + delta 19732)
c [simplification-20] new conflict limit 148407 (hard 168139)
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  235.0   39584   260897    120944   54328   5919 372532   38   130   77  29%    166  -14   44   29  153%
c i  235.0   39583   260897    120945   54328   5919 372532   37   130   77  29%    166  -14   44   29  152%
c i  235.6   39578   260897    121652   54973   5929 372538   39   131   80  30%     71  -14   40   29  137%
c i  236.4   39577   260897    122775   56021   5939 372545   38   123   80  31%     10  -21   38   29  129%
c -  241.9   39576   260897    129304   25718   6000 372604   37   112   40  33%     55  -29   46   30  155%
c i  242.9   39575   260897    130783   27097   6005 372613   35   111   45  31%     76  -29   16   30   55%
c i  243.5   39574   260897    131908   28133   6020 372624   35   112   46  31%     10  -28   30   30  102%
c i  243.5   39573   260897    131913   28137   6020 372624   35   112   46  31%      9  -28   31   30  105%
c i  243.6   39570   260897    132162   28365   6025 372625   35   114   46  31%      1  -25   34   30  113%
c i  246.2   39538   260897    136480   32404   6071 372662   29    92   50  32%     19  -46   22   30   74%
c i  249.7   39520   260897    141655   37227   6134 372701   37   122   61  30%     32  -14   38   30  125%
c i  253.4   39498   260897    147460   42468   6187 372769   34   109   66  31%     40  -23   45   31  147%
c i  255.1   39497   260897    150555   45410   6202 372787   28    83   74  33%      2  -48   22   30   72%
c i  258.5   39490   260897    155040   49573   6233 372822   25    71   79  36%     20  -57   12   30   41%
c i  258.8   39489   260897    155507   50013   6235 372824   27    75   79  36%      2  -53   47   30  155%
c i  260.3   39482   260897    157395   51761   6250 372834   26    72   80  36%    -12  -54   15   30   49%
c i  260.3   39481   260897    157396   51761   6250 372834   26    72   80  36%    -13  -54   15   30   49%
c i  263.5   39480   260897    161523   55501   6286 372875   28    77   80  36%     15  -47   31   30  103%
c i  263.5   39475   260897    161527   55502   6286 372877   28    77   80  36%     15  -47   31   30  102%
c i  263.5   39473   260897    161530   55503   6286 372878   28    77   80  36%     15  -47   30   30  101%
c 
c [simplification-21] limit 148434 conflicts (hard 168139) hit after 168140 conflicts
c [quatres-16] found 17610 quaternary clauses 41% in total
c [quatres-16-1] removed 1 duplicate quaternary clauses
c [quatres-16-2] added 10 single-self-subsuming ternary resolvents
c [quatres-16-2] added 7 quaternary resolvents
c [ternres-17] limit 39506468 with penalty 0 = 0 + 0
c [ternres-17] all 39359 free variables schedulable
c [ternres-17] 305 ternary resolvents (1 bin, 304 trn)
c [ternres-17] fully completed ternary resolution
c [card-6] limit 1234577 penalty 4 = 4 + 0
c [card-6] found 2317 at-most-one constraints of average size 4.0
c [card-6] no at-most-two constraint found
c [card-6] using previous limit 1234577 for elimination
c [card-6] 2317 out of 2317 constraints (100%) meet size limits
c [card-6] no units found
c [card-6] no at-most-one constraints generated
c [decomp-48] removed 246 variables
c [treelook-8] limit 3950646 penalty 0 = 0 + 0 boost 1
c [treelook-8] scheduled 55079 literals 70%
c [treelook-8] scheduling used 1114231 steps
c [treelook-8] scheduled completely
c [treelook-8] limit 3950646 penalty 0 = 0 + 0 boost 1
c [treelook-8] used 3974368 steps
c [treelook-8] 54973 literals remain 70%
c [treelook-8] 9361 variables remain to probed next time 24%
c [treelook-8] removed 12 variables, found 23320 hbrs
c [unhide-21] limit 1975323 with penalty 2 = 0 + 2
c [unhide-21-28] 1 units, 3 failed, 3715 tauts, 0 hbrs, 820907 literals
c [transred-17] limit 2000000 with penalty 0 = 0 + 0
c [transred-17] removed 445 transitive binary clauses
c [transred-17] found 1 units
c [elim-17] no untried remaining variables left
c [elim-17] scheduled 39283 variables 100%
c [elim-17] limit of 790129374 steps penalty 0 = 0 + 0
c [elim-17] rescheduling of touched variables disabled
c [elim-17-1] eliminated 220 variables 1% in round 1 in 20733791 steps
c [elim-17-1] backward subsumption/strengthening limit 20733700
c [elim-17-1-1] backward checking 1421 touched variables 4%
c [elim-17-1-1] fully completed backward checking in 1 rounds
c [elim-17-1] subsumed 1 and strengthened 12 clauses in 306753 steps
c [elim-17-1] rescheduled 35 variables 0% by backward subsumption
c [elim-17-2] eliminated 4 variables 0% in round 2 in 36284 steps
c [elim-17-2] backward subsumption/strengthening limit 36200
c [elim-17-2-1] backward checking 46 touched variables 0%
c [elim-17-2-1] incomplete backward checking 0 remain 0%
c [elim-17-2] subsumed 2 and strengthened 8 clauses in 36201 steps
c [elim-17-2] rescheduled 26 variables 0% by backward subsumption
c [elim-17-3] eliminated 2 variables 0% in round 3 in 31988 steps
c [elim-17-3] backward subsumption/strengthening limit 31900
c [elim-17-3-1] backward checking 21 touched variables 0%
c [elim-17-3-1] incomplete backward checking 0 remain 0%
c [elim-17-3] subsumed 0 and strengthened 2 clauses in 31901 steps
c [elim-17] incomplete 8 not tried 0% in round 3
c [elim-17] transition to [ all 1 rem 1 ] state
c [elim-17] eliminated 226 = 1% variables out of 39283 scheduled
c [elim-17] 226 < 1/100 * 39283 = 392 considered unsuccessful
c [bca-17] limit of 10000000 steps and 511159 added (scaled 2)
c [bca-17] 49050 out of 78116 literals actually usable 63%
c [bca-17] added 15 blocked clauses in 166040 steps
c [phase-count-21] 254184 negative 99.7% of 254823 except 639 0.3%
c [phase-count-21] 177062 positive 69.5% of 254823 except 77761 30.5%
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 39057 enqueued variables after 168140 conflicts
c [score-dist-21] active 0 (0%), one 33967 (87%), zero 5090 (13%)
c [score-dist-21] max exp 1, different 2 (100%)
c [score-dist-21] median active exp 0, avg 0.0
c [simplification-21] removed 302 variables 0.8% (39057 remain 16%)
c [simplification-21] removed 6074 irredundant clauses 2.3% (254823 remain 19%)
c [simplification-21] maximum reduction of 2% = max (1%, 2%)
c [simplification-21] geometric conflict interval increment 13155 = 39465 / 3
c [simplification-21] new conflict interval 52620
c [simplification-21] penalized conflict interval 52620 = 1 * 52620
c [simplification-21] hard conflict limit 247070 (soft 220760 + delta 26310)
c [simplification-21] new conflict limit 220760 (hard 247070)
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  274.9   39056   254823    170083   59442   6288 388555   25    74   89  34%     81  -45   18   30   61%
c i  275.9   39055   254823    171333   60597   6308 388575   29    91   90  32%      5  -27   30   30  102%
c i  276.5   39052   254823    172176   61392   6321 388585   29    93   90  32%    -14  -25   40   30  133%
c -  279.5   39052   254823    176568   34272   6345 388601   25    77   43  32%     16  -38   32   29  110%
c i  286.1   39051   254823    186394   43450   6419 388658   36   106   61  34%    156   -6   35   30  116%
c i  288.4   39020   254823    190399   47239   6448 388677   31    98   62  31%     -0  -14   27   30   90%
c i  296.4   39019   254823    202175   58311   6524 388731   29    88   78  33%    111  -21   33   30  111%
c -  304.2   39016   254823    213399   37934   6598 388798   25    74   44  34%     98  -30   17   29   57%
c i  309.5   39015   254823    222311   46256   6667 388851   19    55   58  35%    215  -45   11   28   38%
c i  314.0   38978   254823    229776   53290   6737 388893   22    56   63  39%     17  -39   31   28  113%
c i  317.9   38974   254823    236117   59128   6790 388930   25    75   71  34%      3  -18   33   27  120%
c 
c [simplification-22] limit 220760 conflicts (hard 247070) hit after 247070 conflicts
c [quatres-17] found 18294 quaternary clauses 38% in total
c [quatres-17-1] removed 3 duplicate quaternary clauses
c [quatres-17-2] added 1 single-self-subsuming ternary resolvents
c [quatres-17-2] added 5 quaternary resolvents
c [ternres-18] limit 52936736 with penalty 0 = 0 + 0
c [ternres-18] all 38974 free variables schedulable
c [ternres-18] 245 ternary resolvents (0 bin, 245 trn)
c [ternres-18] fully completed ternary resolution
c [decomp-50] removed 90 variables
c [basicprobe-8] limit 264683682 penalty 0 = 0 + 0
c [basicprobe-8-0] 6835 sched 18%, 727 failed, 11 lifted, 168868 hbrs
c [decomp-51] removed 964 variables
c [basicprobe-8-1] 8938 probes remain 24% after last round
c [basicprobe-8-1] 926 units = 908 failed (98%) + 18 lifted (2%)
c [basicprobe-8-1] removed 1204 variables, found 205018 hbrs
c [bate-6] eliminated 468 asymmetric tautologies during probing
c [unhide-22] limit 5293673 with penalty 1 = 0 + 1
c [unhide-22-30] 1 units, 66 failed, 64059 tauts, 0 hbrs, 534730 literals
c [transred-18] limit 2000000 with penalty 0 = 0 + 0
c [transred-18] removed 429 transitive binary clauses
c [transred-18] found 2 units
c [cce-11] limit of 66170920 steps penalty 2 = 2 + 0
c [cce-11-1] eliminated 1 clauses out of 2 (50%) of length 89
c [cce-11-1] eliminated 2 clauses out of 6 (33%) of length 33
c [cce-11-1] eliminated 1 clauses out of 5 (20%) of length 32
c [cce-11-1] eliminated 2 clauses out of 3 (67%) of length 31
c [cce-11-1] eliminated 1 clauses out of 6 (17%) of length 30
c [cce-11-1] eliminated 2 clauses out of 4 (50%) of length 29
c [cce-11-1] eliminated 1 clauses out of 6 (17%) of length 28
c [cce-11-1] eliminated 2 clauses out of 5 (40%) of length 27
c [cce-11-1] eliminated 1 clauses out of 7 (14%) of length 26
c [cce-11-1] eliminated 2 clauses out of 9 (22%) of length 25
c [cce-11-1] eliminated 1 clauses out of 5 (20%) of length 24
c [cce-11-1] eliminated 2 clauses out of 9 (22%) of length 23
c [cce-11-1] eliminated 3 clauses out of 6 (50%) of length 22
c [cce-11-1] eliminated 3 clauses out of 9 (33%) of length 21
c [cce-11-1] eliminated 3 clauses out of 6 (50%) of length 20
c [cce-11-1] eliminated 3 clauses out of 6 (50%) of length 19
c [cce-11-1] eliminated 3 clauses out of 10 (30%) of length 18
c [cce-11-1] eliminated 3 clauses out of 7 (43%) of length 17
c [cce-11-1] eliminated 3 clauses out of 8 (38%) of length 16
c [cce-11-1] eliminated 3 clauses out of 9 (33%) of length 15
c [cce-11-1] eliminated 3 clauses out of 8 (38%) of length 14
c [cce-11-1] eliminated 3 clauses out of 11 (27%) of length 13
c [cce-11-1] eliminated 4 clauses out of 11 (36%) of length 12
c [cce-11-1] eliminated 3 clauses out of 10 (30%) of length 11
c [cce-11-1] eliminated 7 clauses out of 16 (44%) of length 10
c [cce-11-1] eliminated 5 clauses out of 17 (29%) of length 9
c [cce-11-1] eliminated 11 clauses out of 23 (48%) of length 8
c [cce-11-1] eliminated 8 clauses out of 44 (18%) of length 7
c [cce-11-1] eliminated 88 clauses out of 2862 (3%) of length 6
c [cce-11-1] eliminated 4 clauses out of 10634 (0%) of length 5
c [cce-11-1] incomplete large round (ACCE)
c [cce-11-1] eliminated 178 large clauses in 66170922 steps
c [cce-11-1] allowing another 33085461 steps for small clauses
c [cce-11-1] scheduling 158446 clauses = 143845 binary + 14601 ternary
c [cce-11-1] tried to eliminate 2643 small clauses 2%
c [cce-11-1] eliminated 542 binary clauses 0%
c [cce-11-1] eliminated 118 ternary clauses 1%
c [cce-11-1] eliminated 660 small clauses 0%
c [cce-11-1] eliminated 727 small clauses in 66170924 steps
c [cce-11-1] incomplete small round (ACCE)
c [cce-11-1] eliminated 905 covered clauses in round 1
c [cce-11] eliminated 905 covered clauses in TOTAL during 1 rounds
c [cce-11] 905 < 1/100 * 238312 = 2383 considered unsuccessful
c [bca-18] limit of 10000000 steps and 476334 added (scaled 2)
c [bca-18] 44901 out of 75428 literals actually usable 60%
c [bca-18] added 19 blocked clauses in 167214 steps
c [sweep-13] limit 7940510 penalty 1 = 1 + 0
c [sweep-13-1] 2069 pos 14.1% + 12568 neg 85.9% = 14637 sched 38.8% ret 23076
c [sweep-13-1] 7999176 steps 188 queries 633.43 avg class size
c [sweep-13-1] 2782 decisions 167 SAT calls 129.34 avg env size
c [sweep-13-1] 13799 variables remain 37% (23911 retained 63%)
c [decomp-52] removed 33 variables
c [sweep-13-1] removed 33 vars (0 failed, 22 eqs, 39 impls)
c [sweep-13] 33 < 1/1000 * 37713 = 37 considered unsuccessful
c [sweep-13] removed 33 vars in TOTAL (1 rounds, 187 queries)
c [sort-queue-22] sorted 37680 enqueued variables after 247070 conflicts
c [score-dist-22] active 0 (0%), one 33730 (90%), zero 3950 (10%)
c [score-dist-22] max exp 1, different 2 (100%)
c [score-dist-22] median active exp 0, avg 0.0
c [simplification-22] removed 1294 variables 3.3% (37680 remain 15%)
c [simplification-22] removed 17482 irredundant clauses 6.9% (237341 remain 17%)
c [simplification-22] maximum reduction of 7% = max (3%, 7%)
c [simplification-22] large reduction 7% >= 5% limit
c [simplification-22] next conflict interval 2470 = min (247070/100, 52620)
c [simplification-22] penalized conflict interval 2470 = 1 * 2470
c [simplification-22] hard conflict limit 259540 (soft 249540 + delta 10000)
c [simplification-22] new conflict limit 249540 (hard 259540)
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  342.1   37679   237341    247684   69381   6899 504895   25    67   93  37%     83  -20   32   27  119%
c i  342.7   37660   237341    248355   69986   6906 504900   27    78   93  34%      7   -8   35   27  130%
c i  343.0   37656   237341    248768   70366   6911 504906   28    85   93  33%    -22   -1   38   27  143%
c -  343.9   37652   237341    249823   39264   6918 504908   26    78   46  34%    -53   -9   18   27   67%
c i  347.5   37651   237341    256610   45663   6954 504935   19    49   55  38%     28  -35   12   26   47%
c 
c [simplification-23] limit 249540 conflicts (hard 259540) hit after 259540 conflicts
c [quatres-18] found 17308 quaternary clauses 37% in total
c [quatres-18-1] removed 4 duplicate quaternary clauses
c [quatres-18-2] added 2 single-self-subsuming ternary resolvents
c [quatres-18-2] added 9 quaternary resolvents
c [ternres-19] limit 54828082 with penalty 0 = 0 + 0
c [ternres-19] all 37651 free variables schedulable
c [ternres-19] 288 ternary resolvents (2 bin, 286 trn)
c [ternres-19] fully completed ternary resolution
c [decomp-53] removed 33 variables
c [simpleprobe-9] all 37647 free variables schedulable
c [simpleprobe-9] limit 200000000 penalty 0 = 0 + 0
c [decomp-54] removed 350 variables
c [simpleprobe-9] fully completed simple probing
c [simpleprobe-9] removed 350 variables, found 99183 hbrs, 218 units
c [unhide-23] limit 10965616 with penalty 0 = 0 + 0
c [unhide-23-35] 1 units, 44 failed, 124329 tauts, 0 hbrs, 448151 literals
c [transred-19] limit 2000000 with penalty 0 = 0 + 0
c [transred-19] removed 410 transitive binary clauses
c [elim-18] no untried remaining variables left
c [elim-18] scheduled 37198 variables 100%
c [elim-18] boosting limit by 20
c [elim-18] limit of 8000000000 steps penalty 1 = 1 + 0
c [elim-18] rescheduling of touched variables disabled
c [elim-18-1] eliminated 673 variables 2% in round 1 in 18033158 steps
c [elim-18-1] backward subsumption/strengthening limit 18033100
c [elim-18-1-1] backward checking 3895 touched variables 10%
c [elim-18-1-1] fully completed backward checking in 1 rounds
c [elim-18-1] subsumed 11 and strengthened 11 clauses in 730219 steps
c [elim-18-1] rescheduled 57 variables 0% by backward subsumption
c [elim-18-2] eliminated 3 variables 0% in round 2 in 35533 steps
c [elim-18-2] backward subsumption/strengthening limit 35500
c [elim-18-2-1] backward checking 35 touched variables 0%
c [elim-18-2-1] incomplete backward checking 0 remain 0%
c [elim-18-2] subsumed 3 and strengthened 2 clauses in 35501 steps
c [elim-18-2] rescheduled 13 variables 0% by backward subsumption
c [elim-18-3] eliminated 1 variables 0% in round 3 in 16041 steps
c [elim-18-3] backward subsumption/strengthening limit 16000
c [elim-18-3-1] backward checking 10 touched variables 0%
c [elim-18-3-1] incomplete backward checking 0 remain 0%
c [elim-18-3] subsumed 0 and strengthened 2 clauses in 16001 steps
c [elim-18] incomplete 8 not tried 0% in round 3
c [elim-18] transition to [ all 1 rem 1 ] state
c [elim-18] eliminated 677 = 2% variables out of 37198 scheduled
c [bca-19] limit of 10000000 steps and 460666 added (scaled 2)
c [bca-19] 45079 out of 73044 literals actually usable 62%
c [bca-19] added 65 blocked clauses in 142882 steps
c [sort-queue-23] sorted 36521 enqueued variables after 259540 conflicts
c [score-dist-23] active 0 (0%), one 33046 (90%), zero 3475 (10%)
c [score-dist-23] max exp 1, different 2 (100%)
c [score-dist-23] median active exp 0, avg 0.0
c [simplification-23] removed 1130 variables 3.0% (36521 remain 15%)
c [simplification-23] removed 7773 irredundant clauses 3.3% (229568 remain 17%)
c [simplification-23] maximum reduction of 3% = max (3%, 3%)
c [simplification-23] geometric conflict interval increment 13155 = 52620 / 4
c [simplification-23] new conflict interval 65775
c [simplification-23] penalized conflict interval 65775 = 1 * 65775
c [simplification-23] hard conflict limit 358202 (soft 325315 + delta 32887)
c [simplification-23] new conflict limit 325315 (hard 358202)
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 -  376.9   36521   229568    290621   41132   6863 453017   21    53   44  39%    357  -19   23   23  100%
c i  401.0   36520   229568    326959   75245   7057 453204   16    41   80  40%    641  -27   10   22   45%
c -  401.9   36519   229568    328009   43362   7060 453206   16    38   45  41%    -52  -29   14   22   64%
c i  404.1   36518   229568    331502   46623   7078 453222   19    50   54  39%   -362  -16   27   22  123%
c i  412.2   36516   229568    343852   58053   7161 453284   24    65   63  37%   -195    0   36   22  160%
c i  416.9   36514   229568    350706   64417   7190 453308   26    62   65  42%   -250   -2   31   22  137%
c i  416.9   36513   229568    350707   64417   7190 453308   26    62   65  42%   -250   -2   31   22  137%
c i  421.8   36512   229568    357582   70966   7220 453336   21    49   73  43%   -221  -15   35   22  159%
c 
c [simplification-24] limit 325325 conflicts (hard 358202) hit after 358203 conflicts
c [quatres-19] found 17775 quaternary clauses 36% in total
c [quatres-19-1] removed 7 duplicate quaternary clauses
c [quatres-19-2] added 3 single-self-subsuming ternary resolvents
c [quatres-19-2] added 8 quaternary resolvents
c [ternres-20] limit 70707762 with penalty 0 = 0 + 0
c [ternres-20] all 36509 free variables schedulable
c [ternres-20] 229 ternary resolvents (0 bin, 229 trn)
c [ternres-20] fully completed ternary resolution
c [decomp-55] removed 18 variables
c [treelook-9] limit 7070776 penalty 0 = 0 + 0 boost 1
c [treelook-9] scheduled 50511 literals 69%
c [treelook-9] scheduling used 1111889 steps
c [treelook-9] scheduled completely
c [treelook-9] limit 7070776 penalty 0 = 0 + 0 boost 1
c [treelook-9] used 7142981 steps
c [treelook-9] 50349 literals remain 69%
c [treelook-9] 9120 variables remain to probed next time 25%
c [treelook-9] removed 10 variables, found 37262 hbrs
c [unhide-24] limit 7070776 with penalty 1 = 0 + 1
c [unhide-24-38] 1 units, 18 failed, 54339 tauts, 0 hbrs, 696985 literals
c [transred-20] limit 2000000 with penalty 0 = 0 + 0
c [transred-20] removed 314 transitive binary clauses
c [elim-19] no untried remaining variables left
c [elim-19] scheduled 36425 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 92 variables 0% in round 1 in 17856793 steps
c [elim-19-1] backward subsumption/strengthening limit 17856700
c [elim-19-1-1] backward checking 611 touched variables 2%
c [elim-19-1-1] fully completed backward checking in 1 rounds
c [elim-19-1] subsumed 1 and strengthened 2 clauses in 161373 steps
c [elim-19-1] rescheduled 11 variables 0% by backward subsumption
c [elim-19-2] eliminated 1 variables 0% in round 2 in 5386 steps
c [elim-19-2] backward subsumption/strengthening limit 5300
c [elim-19-2-1] backward checking 12 touched variables 0%
c [elim-19-2-1] incomplete backward checking 9 remain 75%
c [elim-19-2] subsumed 0 and strengthened 2 clauses in 5326 steps
c [elim-19-2] rescheduled 8 variables 0% by backward subsumption
c [elim-19-3] no variable eliminated in round 3 in 7517 steps
c [elim-19] fully completed in 3 rounds
c [elim-19] transition to [ all 0 rem 0 ] state
c [elim-19] eliminated 93 = 0% variables out of 36425 scheduled
c [elim-19] 93 < 1/100 * 36425 = 364 considered unsuccessful
c [bca-20] limit of 10000000 steps and 456762 added (scaled 2)
c [bca-20] 43195 out of 72666 literals actually usable 59%
c [bca-20] added 18 blocked clauses in 166159 steps
c [sort-queue-24] sorted 36332 enqueued variables after 358203 conflicts
c [score-dist-24] active 0 (0%), one 33036 (91%), zero 3296 (9%)
c [score-dist-24] max exp 1, different 2 (100%)
c [score-dist-24] median active exp 0, avg 0.0
c [simplification-24] removed 177 variables 0.5% (36332 remain 15%)
c [simplification-24] removed 1968 irredundant clauses 0.9% (227600 remain 17%)
c [simplification-24] maximum reduction of 1% = max (0%, 1%)
c [simplification-24] geometric conflict interval increment 32887 = 65775 / 2
c [simplification-24] new conflict interval 98662
c [simplification-24] penalized conflict interval 98662 = 1 * 98662
c [simplification-24] hard conflict limit 506196 (soft 456865 + delta 49331)
c [simplification-24] new conflict limit 456865 (hard 506196)
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  433.5   36331   227600    362939   75078   7314 427838   27    63   85  42%   -224    0   31   23  138%
c i  433.5   36328   227600    362940   75078   7314 427838   27    63   85  42%   -224    0   31   23  137%
c -  436.4   36323   227600    366390   44151   7326 427849   23    51   45  45%   -238  -11   25   23  111%
c i  450.7   36322   227600    388312   64189   7431 427913   17    34   62  50%    119  -22   22   21  103%
c i  454.3   36318   227600    393544   68985   7474 427932   15    38   63  40%   -181  -18    7   21   35%
c 1  457.4   36069   227600    398874   73954   7490 427939   15    43   68  35%   -165  -11   12   20   61%
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
s SATISFIABLE
c
c bate: 2161 basic ate = 2011 trn 93% + 150 lrg 7% in 6 updates
c bcas: 20 count, 2143 added (1291 skipped), 5350031 steps
c bkwd: tried 467225 clauses, 933964 lits, 2.00 lits/clause
c bkwd: checked 13921671 occs, 29.80 occs/clause, 14.91 occs/lit
c bkwd: subsumed 47 binary, 149 ternary, 36 large
c bkwd: strengthened 7 binary, 2 ternary (100% self), 784 large (0% self)
c blkd: 6 bces, 12095 removed, 9653736 resolutions, 26826613 steps
c blkd: 13597 blocking literals 3%, 7 pure
c bump: 399318 bumped seen, 149917836 lits 375.4 on average
c card: 6 count, 0 units, 0 am1, 84322152 steps
c card: 0 rescheduled, 0 eliminated, 0 resolved, 71509 subsumed
c card: 18109 at-most-one constraints found, average size 4.77
c card: 18109 at-most-one constraints used 100%, average size 4.77
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: 11 cces, 42323 eliminated, 42163 ate 100%, 160 abce 0%
c cces: 0 probed, 0 lifted, 0 failed
c cces: 0 cached, 0 rsz, 0 cols 0%, 0 srch, 0 hits 0%
c clls: 1 sat, 0 simp, 0 freeze, 0 melt
c clls: 4740073 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 182 gcs, 0 rescored clauses, 0 rescored vars
c dcps: 56 decompositions, 9379 equivalent 4%
c deco: 8846 decision-only clauses 2%, 66% reduction
c decs: 4125913 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 19 elims, 105943 eliminated 41%, 110 pure 0%
c elms: 56 rounds, 2.9 rounds/bve
c elms: 85504 small 81%, 20322 large 19%
c elms: 265634 tried small, 85507 succeeded 32%, 180127 failed 68%
c elms: 51208 subsumed, 69021 strengthened, 1505 blocked
c elms: 27009936 copies, 26806887 resolutions, 7612334 ipos
c elms: 7886144 subchks, 5920119 strchks
c gaus: 5 extractions, 212 extracted, 2.6 size, 3 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 8421188 steps, 4210594 extr 50%, 1194 elim 0%
c glue: 26.0 orig avg, 26.0 real avg, 3.7 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 1283569 = 365731 simple 28% + 879163 trn 68% + 38675 lrg 3%, 5165 sub 0%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 399318 clauses, 170.1 length
c lrnd: 67930630 lits = 99294712 orig - 31364082 removed 32%
c lrnd: 163554 uips 41%, 203121 flips 51%
c mins: 376356 mins 95%, 4324 bin 1%, 7855 size 2%
c mins: 185290801 poisoned searches, 43034906 hits, 23% hit rate
c mins: 223919280 used twice searches, 5443502 hits, 2% hit rate
c move: moved 27511, 17390 bin 63%, 10121 trn 37%
c otfs: 938 driving 24%, 2998 restarting 76%
c otfs: str 3936, 3713 red 94%, 223 irr 6%
c otfs: str 3936, 0 bin 0%, 163 trn 4%, 3773 lrg 96%
c otfs: sub 7, 7 red 100%, 0 irr 0%
c otfs: sub 7, 0 bin 0%, 1 trn 14%, 6 lrg 86%
c phas: 21 computed, 168590 set, 30 pos (0%), 168560 neg (100%)
c prbs: 8 basic, 44469 probed, 2875 failed, 62 lifted
c prbs: 9 simple, 910818 probed, 1864 failed, 939 eqs
c prbs: 9 treelook, 416 probed, 33 failed, 0 lifted
c prom: 48987 locked 6% out of 760762 tried
c prps: 1022945374 props, 233 props/dec
c prps: 94% srch, 6% simp, 0% lkhd
c quat: 19 count, 60 quat, 39 self1, 1 self2, 603 dup
c queu: 24 sorted, 4125913 next (11 steps 0.00)
c queu: 151766741 enq (151766692 steps 1.00), 149917836 deq 99%
c redc: 9320 clauses 20%, 46172 tried 12%, 234 sat 1%
c redc: 21077 lits 4%, 495999 tried 0%, 234 sat 0%
c redc: 1224 times jump level reduced, 21.7 levels on average
c reds: 7 count, 56982.0 conflicts per reduce
c reds: 0 memlim 0%, 7 arith 100%
c reds: 185522 collected 81%, 43937 retired 19%
c rmbd: 57663 removed, 9301 red 16%
c rsts: 11146 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: 24 count, 21 confs 88%, 0 vars 0%
c simp: 2 its 8%, 1 bin 4%, 0 trns 0%
c subl: 399318 count (366184 tried 0.9), 18850 sub out of 386715 (4.9%)
c swps: 13 count, 13 rounds, 2384 queries (183.4/round)
c swps: 2142 sat calls, 77 unsat (0.6% success rate)
c swps: 37173 decisions 17.4, 1382 conflicts 0.6
c swps; 1809.9 avg class size, 137.8 avg environment size
c swps: 0 failed, 502 impls, 297 equivs
c swp0: 792 type 0 queries, 369 unsat (46.6%), 722 sat (91.2%)
c swp1: 1592 type 1 queries, 975 unsat (61.2%), 1365 sat (85.7%)
c sync: 0 produced units, 0 successful consumptions 0%
c sync: 0 consume units calls, 0 tried 0%, 0 success 0%
c sync: 0 produced clauses, 0 successful consumptions 0%
c sync: 0 consume clause calls, 0 tried 0%, 0 success 0%
c time: 9051477 calls to obtain time
c tops: 107867 fixed 42%, 560 its, 712.27 confs/it
c trds: 20 transitive reductions, 5908 removed, 62 failed
c trds: 30612 nodes, 84064 edges, 38831945 steps
c trim: 882847 words, 3.4 MB
c trnr: 20 count, 4 bin, 3633 trn, 135040037 steps
c unhd: 24 count, 38 rounds, 106058167 steps
c unhd: 1083 non-trivial sccs of average size 2.2
c unhd: 206 units, 204 bin, 2 trn, 0 lrg
c unhd: 12308 failed, 12220 stamp, 0 lits, 43 bin, 32 trn, 0 lrg
c unhd: 665059 tauts, 23663 bin 4%, 14526 trn 2%, 925 lrg 0%
c unhd: 665059 tauts, 625945 stamp 94%, 566464 red 85%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 3864357 str, 204 bin 0%, 3433 trn 0%, 3860720 lrg 100%, 3841947 red 99%
c vars: 36069 remaining 14% and 223189 removed 86% out of 259258
c vars: 107867 fixed 42%, 105943 eliminated 41%, 9379 equivalent 4%
c vsts: 8340508026 visits, 93% srch, 7% simp, 0% lkhd
c vsts: 8.0 search visits per propagation, 19424.9 per conflict
c wchs: 1250654769 pushed, 65284344 enlarged, 262 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all         386775        185522         43937      22273145       2938147        178356
c 
c  0 0         41914  11      4734   3         0   0  14429752  65   1472823  50     63769  36     2.9
c  1 5         20920   5      7507   4      2483   6   1710987   8<   297405  10     21779  12     1.5
c  2 6         67402  17     34608  19      6978  16   2198728  10    389435  13<    28962  16<    4.4
c  3 9         84434  22     51257  28      8767  20   1247196   6    247082   8     17778  10     7.6
c  4 14        50029  13<    29913  16<     6015  14    993602   4    170619   6     12207   7     6.4
c  5 21        33299   9     18211  10      4456  10<   603581   3    120996   4     10078   6     6.1
c  6 30        24809   6     12817   7      3588   8    373778   2     73740   3      6721   4     4.7
c  7 41        17854   5      9099   5      2841   6    260357   1     56656   2      5453   3     3.6
c  8 54        14294   4      6914   4      2431   6    194839   1     42929   1      4185   2     2.9
c  9 69         9941   3      4621   2      1812   4    118332   1     27735   1      2830   2     2.6
c 10 86         9147   2      3664   2      1779   4     97170   0     22412   1      2530   1     1.8
c 11 126        8310   2      1595   1      1796   4     37039   0     12951   0      1628   1     1.3
c 12 230        4158   1       553   0       944   2      7444   0      3176   0       414   0     1.5
c 13 534         264   0        29   0        47   0       340   0       188   0        22   0     0.2
c 
c avg                  3.9           4.0           4.9           1.1           1.7           2.3
c std                  2.8           2.3           2.9           2.0           2.4           2.7
c 
c   34.045   7% cce
c   33.240   7% probe
c   31.693   7% unhide
c   24.311   5% elim
c   18.951   4% bump
c   10.319   2% sweep
c    3.709   1% bca
c    2.709   1% block
c    2.652   1% decide
c 
c    6.038 < 1% rest (below)
c 
c    2.382   1% transred
c    1.387   0% gauss
c    1.114   0% ternres
c    0.779   0% quatres
c    0.376   0% card
c    0.000   0% locs
c    0.000   0% queuesort
c    0.000   0% rescore
c ==================================
c    5.153   1% preprocessing     3%
c  154.508  34% inprocessing     97%
c ==================================
c  159.661  35% simplifying
c  297.730  65% search
c ==================================
c  457.410 100% all
c 
c        398874 conflicts,         872.0 confs/sec
c          5980 ternaries,          66.7 confs/ternary
c          5580 binaries,           71.5 confs/binary
c           560 iterations,        712.3 confs/iteration
c 
c             7 reductions,          0.0 redus/sec,  56982.0 confs/reduction
c         11146 restarts,           24.4 rests/sec,     35.8 confs/restart
c       4125913 decisions,        9020.2 decis/sec,     10.3 decis/conflict
c    1022945374 propagations,  2236386.9 props/sec,    247.9 props/decision
c 
c 457.4 seconds, 105.3 MB
c launch: done
