c launch: /data/cnf/sc2014/app/UCG-20-5p1.cnf.bz2
c host: atom19
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-5p1.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/UCG-20-5p1.cnf.bz2
c no embedded options
c found 'p cnf 224986 1204430' header
c read 224986 variables, 1204430 clauses, 2908691 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=4
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 213583 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] VSIDS (--score=4) decay interval 256 (--vsidsdint=256)
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  213583  1192277         0       0      0     0    0     0   55   0%      0    0    0    0    0%
c 
c [simplification-1] limit 0 conflicts (hard 0) hit after 0 conflicts
c [card-1] limit 2000000 penalty 0 = 0 + 0
c [card-1] found 6240 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] 6240 out of 6240 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 51700 variables
c [simpleprobe-1] all 173286 free variables schedulable
c [simpleprobe-1] boosting simple probing limit by 10
c [simpleprobe-1] limit 20000000 penalty 0 = 0 + 0
c [decomp-2] removed 203 variables
c [simpleprobe-1] 9287 variables remain 5% (163796 retained 95%)
c [simpleprobe-1] removed 203 variables, found 14830 hbrs, 20 units
c [unhide-1] limit 57932 based on 926913 irredundant clauses
c [unhide-1-1] 17 units, 836 failed, 10768 tauts, 0 hbrs, 8216 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 171574 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 47540 not tried 28% in round 1
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 65901 = 38% variables out of 171574 scheduled
c [elim-1] considered successful since not run to completion yet
c [phase-count-1] 769054 negative 99.2% of 774975 except 5921 0.8%
c [phase-count-1] 623698 positive 80.5% of 774975 except 151277 19.5%
c [phase-count-1] less non-negative clauses 5921 than limit 77400 (10.0%)
c [phase-count-1] non-pos/non-neg = 151277/5921 = 25.55 >= 2.00 = 200/100
c [lucky-phase-1] forcing lucky phase -1
c [phase-1] phase bias: 0 positive 0%, 105673 negative 100%
c [sort-queue-1] sorted 105673 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 105673 (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 72469 variables 40.7% (105673 remain 49%)
c [simplification-1] removed 417302 irredundant clauses 35.0% (774975 remain 65%)
c [simplification-1] maximum reduction of 41% = max (41%, 35%)
c [simplification-1] large reduction 41% >= 5% limit
c [simplification-1] next conflict interval 1000 = 2000/2
c [simplification-1] penalized conflict interval 1000 = 1 * 1000
c [simplification-1] hard conflict limit 11000 (soft 1000 + delta 10000)
c [simplification-1] new conflict limit 1000 (hard 11000)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i    4.5  105672   774975         4       2      1  8106    0     1   51   0%      0    1    0    0 25376%
c i    4.5  104996   774975         5       2      1  8106    0     1   51   0%      0    1    0    0 25278%
c i    4.5  104977   774975        12       7      2  8106    0     1   51   1%      0    1    0    0 25048%
c i    4.6  104974   774975       108      79      8  8115    0     2   51   7%      0    2    2    0 21662%
c i    4.8  104958   774975       228     177     19  8125    0     6   52   5%      0    6    3    0 17527%
c i    4.8  104907   774975       264     201     26  8129    0     7   52   5%      0    7    4    0 16153%
c i    4.9  104897   774975       323     244     35  8133    0     8   52   5%      0    8    4    0 14361%
c i    5.1  103950   774975       397     300     43  8140    1    11   52   5%      0   11    5    0 13478%
c i    5.2  103893   774975       469     362     49  8140    1    15   52   4%      0   15    5    0 12745%
c i    5.4  102989   774975       528     415     50  8142    1    18   52   4%      0   18    6    0 12091%
c 
c [simplification-2] limit of 10 iterations hit after 10 iterations
c [decomp-3] removed 4392 variables
c [simpleprobe-2] 8614 schedulable variables 9%
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [simpleprobe-2] 9520 variables remain 9% (91761 retained 91%)
c [simpleprobe-2] removed 0 variables, found 1597 hbrs, 0 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 51894 literals 26%
c [treelook-1] scheduling used 311635 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 312711 steps
c [treelook-1] 51889 literals remain 26%
c [treelook-1] 51442 variables remain to probed next time 51%
c [treelook-1] removed 2 variables, found 1867 hbrs
c [basicprobe-1] limit 5911744 based on 738968 irredundant clauses
c [basicprobe-1-0] 34046 probes remain 37% after last round
c [basicprobe-1-0] 43 units = 43 failed (100%) + 0 lifted (0%)
c [basicprobe-1-0] removed 9973 variables, found 16953 hbrs
c [unhide-2] limit 50000 with penalty 1 = 0 + 1
c [unhide-2-2] 13 units, 2044 failed, 6435 tauts, 0 hbrs, 1134 literals
c [elim-2] 42331 variables 47% will be scheduled this time
c [elim-2] scheduled 42331 variables 47%
c [elim-2] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-2] rescheduling of touched variables disabled
c [elim-2] incomplete 13833 not tried 16% in round 1
c [elim-2] transition to [ all 0 rem 1 ] state
c [elim-2] eliminated 77 = 0% variables out of 42331 scheduled
c [elim-2] considered successful since not run to completion yet
c [phase-count-2] 622059 negative 99.1% of 627980 except 5921 0.9%
c [phase-count-2] 500314 positive 79.7% of 627980 except 127666 20.3%
c [phase-count-2] less non-negative clauses 5921 than limit 62700 (10.0%)
c [phase-count-2] non-pos/non-neg = 127666/5921 = 21.56 >= 2.00 = 200/100
c [lucky-phase-2] forcing lucky phase -1
c [phase-2] phase bias: 0 positive 0%, 815 negative 100%
c [sort-queue-2] sorted 73850 enqueued variables after 528 conflicts
c [score-dist-2] active 15196 (17%), one 0 (0%), zero 73850 (83%)
c [score-dist-2] max exp 505, different 7 (1%)
c [score-dist-2] median active exp 502, avg 501.8
c [simplification-2] removed 12342 variables 12.2% (89046 remain 42%)
c [simplification-2] removed 146995 irredundant clauses 19.0% (627980 remain 53%)
c [simplification-2] maximum reduction of 19% = max (12%, 19%)
c [simplification-2] forced so keeping old conflict interval 0
c [simplification-2] conflict limit remains at 1013 (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    8.2   89045   627980       578     439     55 16088    1    23   44   5%      0   23   11    0 14413%
c i    8.3   88203   627980       616     465     56 16093    1    25   44   5%      0   25   13    0 14208%
c i    8.3   88198   627980       617     465     56 16093    1    25   44   5%      0   25   12    0 14153%
c i    8.3   87673   627980       642     482     60 16095    1    27   44   5%      0   27   12    0 13410%
c i    8.4   87672   627980       644     483     60 16095    1    27   44   5%      0   27   12    0 13320%
c i    8.4   86396   627980       656     491     62 16096    1    28   44   5%      0   27   12    0 12794%
c i    8.4   84204   627980       670     497     63 16102    1    29   44   5%      0   29   12    0 12210%
c i    8.8   84195   627980       870     665     73 16110    2    45   44   5%      0   45   18    0 11239%
c i    8.8   84022   627980       873     666     73 16111    2    45   44   5%      0   45   18    0 11142%
c i    8.8   83823   627980       877     669     73 16111    2    45   44   5%      0   45   18    0 11062%
c i    8.9   83046   627980       893     684     73 16111    2    47   44   5%      0   47   17    0 10526%
c i    8.9   82652   627980       947     727     75 16111    3    51   44   6%      0   51   23    0 11347%
c 
c [simplification-3] limit 1033 conflicts (hard 11000) hit after 1033 conflicts
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 4207 at-most-one constraints of average size 4.7
c [card-2] no at-most-two constraint found
c [card-2] using previous limit 1000000 for elimination
c [card-2] 4207 out of 4207 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [decomp-6] removed 6806 variables
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] scheduled 57049 literals 35%
c [treelook-2] scheduling used 300803 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] used 311240 steps
c [treelook-2] 57026 literals remain 35%
c [treelook-2] 31675 variables remain to probed next time 39%
c [treelook-2] removed 8 variables, found 2509 hbrs
c [unhide-3] limit 121033 with penalty 0 = 0 + 0
c [unhide-3-3] 4 units, 750 failed, 14993 tauts, 0 hbrs, 1183 literals
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 81087 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 15698 not tried 19% in round 1
c [elim-3] transition to [ all 1 rem 1 ] state
c [elim-3] eliminated 1634 = 2% variables out of 81087 scheduled
c [elim-3] considered successful since not run to completion yet
c [phase-count-3] 541446 negative 98.9% of 547205 except 5759 1.1%
c [phase-count-3] 434644 positive 79.4% of 547205 except 112561 20.6%
c [phase-count-3] less non-negative clauses 5759 than limit 54700 (10.0%)
c [phase-count-3] non-pos/non-neg = 112561/5759 = 19.55 >= 2.00 = 200/100
c [lucky-phase-3] forcing lucky phase -1
c [phase-3] phase bias: 0 positive 0%, 687 negative 100%
c [sort-queue-3] sorted 59525 enqueued variables after 1033 conflicts
c [score-dist-3] active 19928 (25%), one 0 (0%), zero 59525 (75%)
c [score-dist-3] max exp 506, different 10 (2%)
c [score-dist-3] median active exp 501, avg 501.2
c [simplification-3] removed 3199 variables 3.9% (79453 remain 37%)
c [simplification-3] removed 80775 irredundant clauses 12.9% (547205 remain 46%)
c [simplification-3] maximum reduction of 13% = max (4%, 13%)
c [simplification-3] large reduction 13% >= 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 13033 (soft 3033 + delta 10000)
c [simplification-3] new conflict limit 3033 (hard 13033)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   11.2   79452   547205      1042     722     71 15440    3    57   39   6%      0   57   23    0 9851%
c i   11.6   79445   547205      1340     960     85 15464    6    84   40   7%      1   83   28    0 7007%
c i   11.6   79438   547205      1369     975     91 15465    6    88   40   7%      1   87   26    0 6391%
c i   11.6   79432   547205      1370     975     91 15465    6    88   40   7%      1   87   26    0 6366%
c i   12.0   79423   547205      1652    1189    106 15487   10   114   40   9%      1  113   65    1 9153%
c 
c [simplification-4] limit 3043 conflicts (hard 13033) hit after 3044 conflicts
c [decomp-8] removed 50 variables
c [basicprobe-2] limit 6499027 penalty 0 = 0 + 0
c [basicprobe-2-0] 28638 probes remain 37% after last round
c [basicprobe-2-0] 40 units = 40 failed (100%) + 0 lifted (0%)
c [basicprobe-2-0] removed 1966 variables, found 12307 hbrs
c [unhide-4] limit 259961 with penalty 0 = 0 + 0
c [unhide-4-4] 16 units, 1043 failed, 4219 tauts, 0 hbrs, 5875 literals
c [elim-4] 12236 variables 16% will be scheduled this time
c [elim-4] scheduled 12236 variables 16%
c [elim-4] boosting limit by 20
c [elim-4] limit of 519922160 steps penalty 0 = 0 + 0
c [elim-4] rescheduling of touched variables disabled
c [elim-4-1] eliminated 4 variables 0% in round 1 in 25610387 steps
c [elim-4-1] backward subsumption/strengthening limit 25610300
c [elim-4-1-1] backward checking 74 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 103316 steps
c [elim-4-1] fully rescheduled 76168 variables 100%
c [elim-4-2] eliminated 294 variables 0% in round 2 in 47683139 steps
c [elim-4-2] backward subsumption/strengthening limit 47683100
c [elim-4-2-1] backward checking 1557 touched variables 2%
c [elim-4-2-1] fully completed backward checking in 1 rounds
c [elim-4-2] subsumed 5 and strengthened 7 clauses in 553802 steps
c [elim-4-2] rescheduled 34 variables 0% by backward subsumption
c [elim-4-3] eliminated 6 variables 0% in round 3 in 13894 steps
c [elim-4-3] backward subsumption/strengthening limit 13800
c [elim-4-3-1] backward checking 39 touched variables 0%
c [elim-4-3-1] incomplete backward checking 0 remain 0%
c [elim-4-3] subsumed 1 and strengthened 3 clauses in 13801 steps
c [elim-4] incomplete 14 not tried 0% in round 3
c [elim-4] transition to [ all 1 rem 1 ] state
c [elim-4] eliminated 304 = 2% variables out of 12236 scheduled
c [elim-4] considered successful since not run to completion yet
c [phase-count-4] 510425 negative 98.9% of 516165 except 5740 1.1%
c [phase-count-4] 407093 positive 78.9% of 516165 except 109072 21.1%
c [phase-count-4] less non-negative clauses 5740 than limit 51600 (10.0%)
c [phase-count-4] non-pos/non-neg = 109072/5740 = 19.00 >= 2.00 = 200/100
c [lucky-phase-4] forcing lucky phase -1
c [phase-4] phase bias: 0 positive 0%, 499 negative 100%
c [sort-queue-4] sorted 49942 enqueued variables after 3044 conflicts
c [score-dist-4] active 25926 (34%), one 0 (0%), zero 49942 (66%)
c [score-dist-4] max exp 508, different 19 (4%)
c [score-dist-4] median active exp 502, avg 499.5
c [simplification-4] removed 3544 variables 4.5% (75868 remain 36%)
c [simplification-4] removed 31040 irredundant clauses 5.7% (516165 remain 43%)
c [simplification-4] maximum reduction of 6% = max (4%, 6%)
c [simplification-4] large reduction 6% >= 5% limit
c [simplification-4] next conflict interval 2000 = 2000/1
c [simplification-4] penalized conflict interval 2000 = 1 * 2000
c [simplification-4] hard conflict limit 15044 (soft 5044 + delta 10000)
c [simplification-4] new conflict limit 5044 (hard 15044)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   15.9   75867   516165      3061    2268    131 21313   21   130   39  17%     10  127   23    2 1312%
c i   16.2   75858   516165      3222    2382    148 21335   22   138   39  16%      9  134   24    2 1316%
c i   16.2   75846   516165      3226    2385    148 21335   22   138   39  16%      9  134   25    2 1323%
c i   16.2   75842   516165      3230    2387    148 21335   22   138   39  16%      9  134   24    2 1318%
c i   16.3   75834   516165      3301    2444    152 21340   23   144   39  16%      8  140   40    2 2064%
c i   16.4   75825   516165      3347    2484    152 21340   24   147   39  16%      8  143   46    2 2287%
c i   16.6   75782   516165      3440    2562    155 21346   24   152   39  16%      7  148   44    2 2153%
c i   16.6   75771   516165      3457    2574    155 21346   24   153   39  16%      7  149   43    2 2083%
c i   17.0   75736   516165      3730    2795    166 21362   27   182   39  15%      6  177   67    2 2833%
c i   17.0   75725   516165      3731    2795    166 21362   27   182   39  15%      6  176   67    2 2822%
c i   17.0   75718   516165      3732    2795    166 21362   27   182   39  15%      6  176   67    2 2811%
c i   17.0   75712   516165      3733    2795    166 21362   27   182   39  15%      6  176   66    2 2800%
c i   17.0   75701   516165      3734    2795    166 21362   27   182   39  15%      6  176   66    2 2789%
c i   17.2   75688   516165      3876    2913    168 21366   28   184   39  15%      5  179   61    2 2443%
c i   18.2   75610   516165      4692    3580    179 21382   38   186   40  20%      6  178   78    3 2255%
c i   18.5   75603   516165      5024    3819    181 21387   40   182   40  22%      5  173   81    4 2123%
c 
c [simplification-5] limit 5088 conflicts (hard 15044) hit after 5088 conflicts
c [quatres-1] found 38035 quaternary clauses 45% in total
c [quatres-1-2] added 3 quaternary resolvents
c [ternres-1] boosting ternary resolution limit by 5
c [ternres-1] limit 20000000 with penalty 0 = 0 + 0
c [ternres-1] all 75599 free variables schedulable
c [ternres-1] 40 ternary resolvents (0 bin, 40 trn)
c [ternres-1] fully completed ternary resolution
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 39 xors of average arity 2.5
c [gauss-1] connected 96 occurrences of 70 variables (average 1.4)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] fully completed
c [gauss-1] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-9] removed 42 variables
c [unhide-5] limit 446851 with penalty 0 = 0 + 0
c [unhide-5-5] 7 units, 436 failed, 8527 tauts, 0 hbrs, 6682 literals
c [transred-1] limit 2000000 with penalty 0 = 0 + 0
c [transred-1] removed 333 transitive binary clauses
c [transred-1] found 13 units
c [block-1] scheduling all variables this time
c [block-1] scheduled 74894 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 7427 blocked clauses
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 3 clauses out of 144 (2%) of length 10
c [cce-1-1] eliminated 26 clauses out of 705 (4%) of length 9
c [cce-1-1] eliminated 50 clauses out of 599 (8%) of length 8
c [cce-1-1] eliminated 107 clauses out of 858 (12%) of length 7
c [cce-1-1] eliminated 3223 clauses out of 4795 (67%) of length 6
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 3409 large clauses in 30000007 steps
c [cce-1-1] allowing another 15000003 steps for small clauses
c [cce-1-1] scheduling 259044 clauses = 242946 binary + 16098 ternary
c [cce-1-1] tried to eliminate 703 small clauses 0%
c [cce-1-1] eliminated 265 binary clauses 0%
c [cce-1-1] eliminated 18 ternary clauses 0%
c [cce-1-1] eliminated 283 small clauses 0%
c [cce-1-1] eliminated 283 small clauses in 30000003 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 3692 covered clauses in round 1
c [cce-1] eliminated 3692 covered clauses in TOTAL during 1 rounds
c [cce-1] 3692 < 1/100 * 492113 = 4921 considered unsuccessful
c [elim-5] no untried remaining variables left
c [elim-5] scheduled 74894 variables 100%
c [elim-5] limit of 44685161 steps penalty 0 = 0 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5-1] eliminated 296 variables 0% in round 1 in 44497222 steps
c [elim-5-1] backward subsumption/strengthening limit 187939
c [elim-5-1-1] backward checking 1899 touched variables 3%
c [elim-5-1-1] incomplete backward checking 1350 remain 71%
c [elim-5-1] subsumed 0 and strengthened 1 clauses in 188028 steps
c [elim-5] incomplete 6 not tried 0% in round 1
c [elim-5] transition to [ all 1 rem 1 ] state
c [elim-5] eliminated 297 = 0% variables out of 74894 scheduled
c [elim-5] 297 < 1/100 * 74894 = 748 considered unsuccessful
c [bca-1] limit of 10000000 steps and 975690 added (scaled 2)
c [bca-1] 135543 out of 149196 literals actually usable 91%
c [bca-1] added 206 blocked clauses in 415159 steps
c [sweep-1] limit 1000000 penalty 0 = 0 + 0
c [sweep-1-1] 3994 pos 5.4% + 70603 neg 94.6% = 74597 sched 100.0% ret 0
c [sweep-1-1] 1068280 steps 15 queries 19893.27 avg class size
c [sweep-1-1] 185 decisions 13 SAT calls 77.69 avg env size
c [sweep-1-1] 74549 variables remain 100% (48 retained 0%)
c [decomp-10] removed 6 variables
c [sweep-1-1] removed 6 vars (0 failed, 1 eqs, 4 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 6 vars in TOTAL (1 rounds, 14 queries)
c [phase-count-5] 485027 negative 99.5% of 487586 except 2559 0.5%
c [phase-count-5] 389876 positive 80.0% of 487586 except 97710 20.0%
c [phase-count-5] less non-negative clauses 2559 than limit 48700 (10.0%)
c [phase-count-5] non-pos/non-neg = 97710/2559 = 38.18 >= 2.00 = 200/100
c [lucky-phase-5] forcing lucky phase -1
c [phase-5] phase bias: 0 positive 0%, 387 negative 100%
c [sort-queue-5] sorted 43370 enqueued variables after 5088 conflicts
c [score-dist-5] active 31221 (42%), one 0 (0%), zero 43370 (58%)
c [score-dist-5] max exp 510, different 29 (6%)
c [score-dist-5] median active exp 497, avg 495.9
c [simplification-5] removed 1008 variables 1.3% (74591 remain 35%)
c [simplification-5] removed 28579 irredundant clauses 5.5% (487586 remain 41%)
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 17088 (soft 7088 + delta 10000)
c [simplification-5] new conflict limit 7088 (hard 17088)
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.0   74590   487586      5110    3760    252 29527   40   185   38  22%      5  176   61    4 1605%
c i   23.2   74586   487586      5232    3866    258 29531   40   193   40  21%      4  184   52    4 1339%
c i   23.2   74061   487586      5235    3868    258 29531   40   194   40  21%      4  184   51    4 1325%
c i   24.1   74054   487586      5905    4347    260 29538   72   241   41  30%      5  230  289    6 4556%
c i   24.1   74046   487586      5906    4347    260 29538   72   241   41  30%      5  230  288    6 4539%
c i   24.1   74040   487586      5907    4347    260 29538   72   241   41  30%      5  230  287    6 4521%
c i   24.1   74032   487586      5908    4347    260 29538   72   241   41  30%      5  230  285    6 4503%
c i   24.1   74027   487586      5909    4347    260 29538   72   241   41  30%      5  230  284    6 4486%
c i   24.1   74018   487586      5910    4347    260 29538   72   241   41  30%      5  229  283    6 4468%
c i   24.1   74011   487586      5911    4347    260 29538   72   241   41  30%      5  229  282    6 4451%
c i   24.1   74000   487586      5915    4350    260 29538   71   241   41  30%      5  230  278    6 4383%
c i   24.1   73991   487586      5916    4350    260 29538   71   241   41  30%      5  229  277    6 4365%
c i   24.9   73981   487586      6439    4638    262 29539  100   264   42  38%      4  251  278    9 3181%
c i   25.1   73972   487586      6606    4728    262 29539  104   269   42  39%      4  255  235    9 2536%
c i   25.1   73964   487586      6608    4729    262 29539  104   269   42  39%      4  255  233    9 2517%
c i   25.1   73952   487586      6613    4732    262 29539  104   269   42  39%      4  255  229    9 2471%
c i   25.4   73944   487586      6796    4867    263 29539  106   276   42  38%      3  262  198   10 2057%
c i   25.4   73931   487586      6797    4867    263 29539  106   276   42  38%      3  262  197   10 2049%
c i   25.6   73922   487586      6986    5016    267 29541  103   276   42  38%      3  260  118   10 1214%
c 
c [simplification-6] limit 7180 conflicts (hard 17088) hit after 7180 conflicts
c [quatres-2] found 37919 quaternary clauses 48% in total
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] all 73875 free variables schedulable
c [ternres-2] 2 ternary resolvents (0 bin, 2 trn)
c [ternres-2] 43474 variables remain 59% (30401 retained 41%)
c [card-3] limit 500000 penalty 2 = 2 + 0
c [card-3] found 2538 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] 2538 out of 2538 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [decomp-11] removed 755 variables
c [simpleprobe-3] 6066 schedulable variables 8%
c [simpleprobe-3] limit 6349645 penalty 1 = 1 + 0
c [decomp-12] removed 24 variables
c [simpleprobe-3] 4941 variables remain 7% (68871 retained 93%)
c [simpleprobe-3] removed 24 variables, found 8399 hbrs, 9 units
c [unhide-6] limit 634964 with penalty 0 = 0 + 0
c [unhide-6-6] 1 units, 541 failed, 5340 tauts, 0 hbrs, 32882 literals
c [transred-2] limit 2000000 with penalty 0 = 0 + 0
c [transred-2] removed 402 transitive binary clauses
c [transred-2] found 14 units
c [block-2] scheduling all variables this time
c [block-2] scheduled 72969 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 1067 blocked clauses
c [block-2] 1067 < 1/100 * 481100 = 4811 considered unsuccessful
c [bca-2] limit of 10000000 steps and 941977 added (scaled 2)
c [bca-2] 131275 out of 145940 literals actually usable 90%
c [bca-2] added 138 blocked clauses in 400350 steps
c [sweep-2] limit 1000000 penalty 0 = 0 + 0
c [sweep-2-1] 3720 pos 5.1% + 69203 neg 94.9% = 72923 sched 99.9% ret 46
c [sweep-2-1] 1021256 steps 21 queries 18824.48 avg class size
c [sweep-2-1] 117 decisions 11 SAT calls 43.18 avg env size
c [sweep-2-1] 72892 variables remain 100% (74 retained 0%)
c [decomp-13] removed 16 variables
c [sweep-2-1] removed 16 vars (1 failed, 9 eqs, 5 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 16 vars in TOTAL (1 rounds, 20 queries)
c [phase-count-6] 468086 negative 99.5% of 470636 except 2550 0.5%
c [phase-count-6] 374235 positive 79.5% of 470636 except 96401 20.5%
c [phase-count-6] less non-negative clauses 2550 than limit 47000 (10.0%)
c [phase-count-6] non-pos/non-neg = 96401/2550 = 37.80 >= 2.00 = 200/100
c [lucky-phase-6] forcing lucky phase -1
c [phase-6] phase bias: 0 positive 0%, 296 negative 100%
c [sort-queue-6] sorted 40682 enqueued variables after 7180 conflicts
c [score-dist-6] active 32271 (44%), one 0 (0%), zero 40682 (56%)
c [score-dist-6] max exp 508, different 36 (7%)
c [score-dist-6] median active exp 492, avg 491.6
c [simplification-6] removed 922 variables 1.2% (72953 remain 34%)
c [simplification-6] removed 16950 irredundant clauses 3.5% (470636 remain 39%)
c [simplification-6] maximum reduction of 3% = max (1%, 3%)
c [simplification-6] geometric conflict interval increment 5000 = 20000 / 4
c [simplification-6] new conflict interval 5000
c [simplification-6] penalized conflict interval 5000 = 1 * 5000
c [simplification-6] hard conflict limit 22180 (soft 12180 + delta 10000)
c [simplification-6] new conflict limit 12180 (hard 22180)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   28.4   72952   470636      7327    5306    308 33450   99   275   41  36%      3  259   73   10  737%
c i   28.5   72947   470636      7432    5379    309 33453   98   271   41  36%      3  254   58   10  586%
c i   28.5   72941   470636      7439    5382    310 33455   97   271   41  36%      3  254   57   10  571%
c i   28.5   72928   470636      7440    5382    310 33455   97   271   41  36%      3  254   57   10  569%
c i   28.5   72919   470636      7442    5383    310 33455   97   271   41  36%      3  254   56   10  565%
c i   28.5   72906   470636      7443    5383    310 33455   97   271   41  36%      3  254   56   10  563%
c i   28.6   72894   470636      7494    5424    312 33458   96   272   41  35%      2  255   48   10  477%
c i   28.6   72889   470636      7516    5440    313 33458   96   272   41  35%      2  254   44   10  444%
c i   28.6   72863   470636      7538    5452    315 33463   95   271   41  35%      2  254   41   10  410%
c i   28.7   72839   470636      7585    5489    318 33463   94   274   41  34%      2  256   36   10  363%
c i   28.8   72831   470636      7644    5540    321 33465   93   274   41  34%      2  256   34   10  340%
c i   28.8   72818   470636      7647    5541    321 33466   93   274   41  34%      2  256   34   10  337%
c i   28.8   72805   470636      7651    5543    321 33467   93   274   41  34%      2  256   34   10  336%
c i   28.8   72791   470636      7652    5543    321 33467   93   274   41  34%      2  256   33   10  335%
c i   29.3   72777   470636      7954    5796    332 33480   91   286   41  32%      2  267   59   10  577%
c i   29.3   72764   470636      7960    5801    332 33480   91   287   41  32%      2  268   61   10  598%
c i   29.4   72753   470636      8038    5869    335 33480   91   294   41  31%      2  274   67   10  644%
c i   30.3   72748   470636      8546    6300    339 33493  109   346   41  32%      3  324  243   12 2004%
c i   30.9   72747   470636      8897    6589    341 33499  122   361   42  34%      3  338  236   13 1749%
c i   30.9   72740   470636      8898    6589    341 33499  122   361   42  34%      3  338  235   13 1742%
c i   30.9   72729   470636      8899    6589    341 33499  121   361   42  34%      3  337  234   13 1735%
c i   30.9   72722   470636      8900    6589    341 33499  121   361   42  34%      3  337  233   13 1729%
c i   30.9   72715   470636      8901    6589    341 33499  121   361   42  34%      3  337  232   13 1722%
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   30.9   72708   470636      8902    6589    341 33499  121   361   42  34%      3  337  231   13 1715%
c i   31.0   72698   470636      8903    6589    341 33499  121   361   42  34%      3  337  230   13 1708%
c i   31.0   72691   470636      8904    6589    341 33499  121   361   42  34%      3  337  229   13 1702%
c i   31.0   72680   470636      8909    6589    341 33503  121   361   42  34%      3  337  225   13 1669%
c i   31.0   72670   470636      8910    6589    341 33503  121   361   42  34%      3  337  224   13 1663%
c i   31.0   72661   470636      8911    6589    341 33503  121   360   42  34%      3  337  223   13 1656%
c i   31.3   72651   470636      9128    6741    345 33534  122   369   42  33%      2  344  175   14 1264%
c i   31.3   72650   470636      9145    6742    345 33539  122   369   42  33%      2  344  182   14 1310%
c 
c [simplification-7] limit of 364 binary hit after 364 binaries
c [ternres-3] limit 4129666 with penalty 0 = 0 + 0
c [ternres-3] 42761 schedulable variables 59%
c [ternres-3] 8 ternary resolvents (0 bin, 8 trn)
c [ternres-3] 10131 variables remain 14% (62519 retained 86%)
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] extracted 32 xors of average arity 2.7
c [gauss-2] connected 86 occurrences of 86 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-14] removed 25 variables
c [treelook-3] limit 412966 penalty 0 = 0 + 0 boost 1
c [treelook-3] scheduled 61900 literals 43%
c [treelook-3] scheduling used 423969 steps
c [treelook-3] not fully scheduled
c [treelook-3] limit 412966 penalty 0 = 0 + 0 boost 1
c [treelook-3] used 566188 steps
c [treelook-3] 61890 literals remain 43%
c [treelook-3] 25883 variables remain to probed next time 36%
c [treelook-3] removed 3 variables, found 5140 hbrs
c [unhide-7] limit 825933 with penalty 0 = 0 + 0
c [unhide-7-7] 15 units, 262 failed, 11102 tauts, 0 hbrs, 27437 literals
c [transred-3] limit 2000000 with penalty 0 = 0 + 0
c [transred-3] removed 370 transitive binary clauses
c [transred-3] found 11 units
c [cce-2] limit of 15000000 steps penalty 1 = 1 + 0
c [cce-2-1] eliminated 1 clauses out of 792 (0%) of length 7
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] eliminated 1 large clauses in 15000004 steps
c [cce-2-1] allowing another 7500002 steps for small clauses
c [cce-2-1] scheduling 241868 clauses = 225870 binary + 15998 ternary
c [cce-2-1] tried to eliminate 344 small clauses 0%
c [cce-2-1] eliminated 109 binary clauses 0%
c [cce-2-1] eliminated 8 ternary clauses 0%
c [cce-2-1] eliminated 117 small clauses 0%
c [cce-2-1] eliminated 5248 small clauses in 15000004 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 5249 covered clauses in round 1
c [cce-2] eliminated 5249 covered clauses in TOTAL during 1 rounds
c [elim-6] no untried remaining variables left
c [elim-6] scheduled 72056 variables 100%
c [elim-6] limit of 41296664 steps penalty 1 = 1 + 0
c [elim-6] rescheduling of touched variables disabled
c [elim-6-1] eliminated 545 variables 1% in round 1 in 40438787 steps
c [elim-6-1] backward subsumption/strengthening limit 857877
c [elim-6-1-1] backward checking 2454 touched variables 3%
c [elim-6-1-1] fully completed backward checking in 1 rounds
c [elim-6-1] subsumed 14 and strengthened 65 clauses in 836296 steps
c [elim-6-1] rescheduled 212 variables 0% by backward subsumption
c [elim-6] incomplete 105 not tried 0% in round 2
c [elim-6] transition to [ all 1 rem 1 ] state
c [elim-6] eliminated 579 = 1% variables out of 72056 scheduled
c [elim-6] 579 < 1/100 * 72056 = 720 considered unsuccessful
c [bca-3] limit of 10000000 steps and 903780 added (scaled 2)
c [bca-3] 126684 out of 142956 literals actually usable 89%
c [bca-3] added 111 blocked clauses in 381888 steps
c [sweep-3] limit 1238899 penalty 0 = 0 + 0
c [sweep-3-1] 3695 pos 5.2% + 67720 neg 94.8% = 71415 sched 99.9% ret 62
c [sweep-3-1] 1371685 steps 22 queries 14472.45 avg class size
c [sweep-3-1] 219 decisions 11 SAT calls 94.55 avg env size
c [sweep-3-1] 71361 variables remain 100% (97 retained 0%)
c [decomp-16] removed 61 variables
c [sweep-3-1] removed 61 vars (0 failed, 10 eqs, 15 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 61 vars in TOTAL (1 rounds, 21 queries)
c [phase-count-7] 448684 negative 99.4% of 451197 except 2513 0.6%
c [phase-count-7] 357720 positive 79.3% of 451197 except 93477 20.7%
c [phase-count-7] less non-negative clauses 2513 than limit 45100 (10.0%)
c [phase-count-7] non-pos/non-neg = 93477/2513 = 37.20 >= 2.00 = 200/100
c [lucky-phase-7] forcing lucky phase -1
c [phase-7] phase bias: 0 positive 0%, 181 negative 100%
c [sort-queue-7] sorted 36229 enqueued variables after 9209 conflicts
c [score-dist-7] active 35187 (49%), one 0 (0%), zero 36229 (51%)
c [score-dist-7] max exp 509, different 44 (9%)
c [score-dist-7] median active exp 499, avg 494.6
c [simplification-7] removed 1234 variables 1.7% (71416 remain 33%)
c [simplification-7] removed 19439 irredundant clauses 4.1% (451197 remain 38%)
c [simplification-7] maximum reduction of 4% = max (2%, 4%)
c [simplification-7] forced so keeping old conflict interval 5000
c [simplification-7] conflict limit remains at 12314 (hard 22180)
c [simplification-7] 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   35.9   71415   451197      9542    6221    313 37494  133   388   41  34%      2  361  221   15 1449%
c i   35.9   71403   451197      9548    6223    313 37496  133   388   41  34%      2  361  220   15 1445%
c i   36.0   71399   451197      9578    6241    314 37498  134   390   41  34%      2  363  231   15 1504%
c i   36.0   71383   451197      9596    6250    314 37498  135   391   41  35%      2  363  236   15 1529%
c i   36.0   71378   451197      9597    6250    314 37498  135   390   41  35%      2  363  236   15 1523%
c i   36.0   71374   451197      9598    6250    314 37498  135   390   41  35%      2  363  235   15 1517%
c i   36.0   71369   451197      9599    6250    314 37498  135   390   41  35%      2  363  234   15 1511%
c i   36.0   71360   451197      9600    6250    314 37498  135   390   41  35%      2  363  233   15 1505%
c i   36.1   71355   451197      9602    6251    314 37498  135   390   41  35%      2  363  231   15 1494%
c i   36.1   71351   451197      9603    6251    314 37498  135   390   41  35%      2  363  230   15 1488%
c i   36.1   71346   451197      9614    6259    314 37498  135   390   41  35%      2  363  229   15 1480%
c i   36.1   71343   451197      9616    6260    314 37498  135   390   41  35%      2  363  228   15 1469%
c i   36.1   71340   451197      9617    6260    314 37498  135   390   41  35%      2  363  227   15 1463%
c i   36.1   71333   451197      9618    6260    314 37498  135   390   41  35%      2  363  226   15 1457%
c i   36.1   71326   451197      9619    6260    314 37498  135   390   41  35%      2  363  225   15 1451%
c i   36.1   71318   451197      9620    6260    314 37498  135   390   41  35%      2  363  224   15 1446%
c i   36.1   71314   451197      9621    6260    314 37498  135   390   41  35%      2  362  223   15 1440%
c i   36.2   71306   451197      9677    6302    314 37498  137   392   41  35%      2  364  234   16 1490%
c i   36.7   71295   451197     10035    6597    316 37507  137   405   41  34%      2  375  167   16 1020%
c i   37.1   71294   451197     10358    6836    317 37515  144   412   41  35%      2  381  189   17 1084%
c i   37.4   71292   451197     10556    6996    325 37518  140   421   41  33%      2  389  122   18  694%
c i   39.1   71284   451197     11683    7689    332 37543  175   441   43  40%      7  401  256   22 1159%
c i   39.2   71283   451197     11707    7706    332 37544  175   440   43  40%      7  401  249   22 1125%
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.4   71280   451197     11865    7827    332 37545  176   440   43  40%      6  400  222   23  984%
c i   40.3   71279   451197     12341    8203    332 37548  191   469   44  41%      5  425  342   25 1386%
c i   40.4   71278   451197     12373    8227    332 37548  193   471   44  41%      5  427  358   25 1438%
c 
c [simplification-8] limit 12425 conflicts (hard 22180) hit after 12425 conflicts
c [quatres-3] found 37761 quaternary clauses 48% in total
c [quatres-3-2] added 24 quaternary resolvents
c [ternres-4] limit 5552967 with penalty 0 = 0 + 0
c [ternres-4] 9945 schedulable variables 14%
c [ternres-4] 17 ternary resolvents (0 bin, 17 trn)
c [ternres-4] fully completed ternary resolution
c [decomp-17] removed 150 variables
c [basicprobe-3] limit 27764838 penalty 0 = 0 + 0
c [basicprobe-3-0] 24364 probes remain 36% after last round
c [basicprobe-3-0] 249 units = 249 failed (100%) + 0 lifted (0%)
c [basicprobe-3-0] removed 3255 variables, found 48669 hbrs
c [bate-1] eliminated 82 asymmetric tautologies during probing
c [unhide-8] limit 1110593 with penalty 0 = 0 + 0
c [unhide-8-8] 16 units, 794 failed, 8591 tauts, 0 hbrs, 68673 literals
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 340 transitive binary clauses
c [transred-4] found 10 units
c [block-3] scheduling all variables this time
c [block-3] scheduled 67092 variables 100%
c [block-3] limit of 27764838 steps penalty 1 = 1 + 0
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 292 blocked clauses
c [block-3] 292 < 1/100 * 429068 = 4290 considered unsuccessful
c [cce-3] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-3-1] eliminated 2 clauses out of 709 (0%) of length 7
c [cce-3-1] eliminated 117 clauses out of 1464 (8%) of length 6
c [cce-3-1] eliminated 1198 clauses out of 29833 (4%) of length 5
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 1317 large clauses in 30000001 steps
c [cce-3-1] allowing another 15000000 steps for small clauses
c [cce-3-1] scheduling 228806 clauses = 212634 binary + 16172 ternary
c [cce-3-1] tried to eliminate 734 small clauses 0%
c [cce-3-1] eliminated 246 binary clauses 0%
c [cce-3-1] eliminated 17 ternary clauses 0%
c [cce-3-1] eliminated 263 small clauses 0%
c [cce-3-1] eliminated 263 small clauses in 30000021 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 1580 covered clauses in round 1
c [cce-3] eliminated 1580 covered clauses in TOTAL during 1 rounds
c [cce-3] 1580 < 1/100 * 419514 = 4195 considered unsuccessful
c [bca-4] limit of 10000000 steps and 836595 added (scaled 2)
c [bca-4] 116877 out of 134096 literals actually usable 87%
c [bca-4] added 105 blocked clauses in 341219 steps
c [sweep-4] limit 1665890 penalty 0 = 0 + 0
c [sweep-4-1] 3781 pos 5.6% + 63182 neg 94.4% = 66963 sched 99.9% ret 84
c [sweep-4-1] 1693387 steps 27 queries 9207.11 avg class size
c [sweep-4-1] 261 decisions 22 SAT calls 70.09 avg env size
c [sweep-4-1] 66819 variables remain 100% (208 retained 0%)
c [decomp-18] removed 268 variables
c [sweep-4-1] removed 268 vars (0 failed, 4 eqs, 10 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 268 vars in TOTAL (1 rounds, 26 queries)
c [phase-count-8] 415685 negative 99.7% of 416985 except 1300 0.3%
c [phase-count-8] 328981 positive 78.9% of 416985 except 88004 21.1%
c [phase-count-8] less non-negative clauses 1300 than limit 41600 (10.0%)
c [phase-count-8] non-pos/non-neg = 88004/1300 = 67.70 >= 2.00 = 200/100
c [lucky-phase-8] forcing lucky phase -1
c [phase-8] phase bias: 0 positive 0%, 160 negative 100%
c [sort-queue-8] sorted 31477 enqueued variables after 12425 conflicts
c [score-dist-8] active 35302 (53%), one 0 (0%), zero 31477 (47%)
c [score-dist-8] max exp 509, different 57 (11%)
c [score-dist-8] median active exp 496, avg 490.7
c [simplification-8] removed 4499 variables 6.3% (66779 remain 31%)
c [simplification-8] removed 34212 irredundant clauses 7.6% (416985 remain 35%)
c [simplification-8] maximum reduction of 8% = max (6%, 8%)
c [simplification-8] large reduction 8% >= 5% limit
c [simplification-8] next conflict interval 2000 = 2000/1
c [simplification-8] penalized conflict interval 2000 = 1 * 2000
c [simplification-8] hard conflict limit 24425 (soft 14425 + delta 10000)
c [simplification-8] new conflict limit 14425 (hard 24425)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   44.7   66778   416985     12476    8244    428 68925  200   475   41  42%      4  431  398   26 1557%
c i   44.8   66777   416985     12542    8276    428 68926  207   480   43  43%      4  435  450   26 1720%
c i   45.7   66776   416985     13167    8742    436 68939  217   499   46  44%      4  450  272   29  955%
c i   46.1   66770   416985     13430    8948    442 68944  213   499   46  43%      4  448  187   29  646%
c i   46.2   66769   416985     13466    8971    442 68956  211   499   46  42%      4  448  167   29  577%
c i   46.2   66768   416985     13467    8971    442 68956  211   499   46  42%      4  448  167   29  574%
c i   46.2   66767   416985     13468    8971    442 68956  211   499   46  42%      4  448  166   29  572%
c i   46.2   66766   416985     13469    8971    442 68956  211   499   46  42%      4  448  165   29  570%
c i   46.2   66765   416985     13470    8971    442 68956  211   499   46  42%      4  448  165   29  568%
c i   46.2   66764   416985     13476    8971    442 68961  211   498   46  42%      3  447  161   29  555%
c i   46.2   66763   416985     13477    8971    442 68961  211   498   46  42%      3  447  160   29  552%
c i   46.2   66762   416985     13478    8971    442 68961  211   498   46  42%      3  447  160   29  550%
c i   46.2   66761   416985     13479    8971    442 68961  211   498   46  42%      3  447  159   29  548%
c i   46.2   66760   416985     13480    8971    442 68961  211   498   46  42%      3  447  158   29  546%
c i   46.3   66759   416985     13494    8968    442 68971  210   498   46  42%      3  447  151   29  520%
c i   46.3   66758   416985     13526    8986    442 68979  210   498   46  42%      3  446  159   29  546%
c i   46.5   66757   416985     13624    9044    450 68992  209   498   46  42%      3  446  158   29  541%
c i   46.5   66756   416985     13625    9044    450 68992  209   498   46  42%      3  446  158   29  539%
c i   46.5   66755   416985     13630    9048    450 68992  208   498   46  42%      3  446  155   29  529%
c i   46.5   66754   416985     13631    9048    450 68992  208   498   46  42%      3  446  154   29  527%
c i   46.5   66753   416985     13632    9048    450 68992  208   498   46  42%      3  446  153   29  525%
c i   46.6   66752   416985     13655    9067    450 68992  209   498   46  42%      3  446  164   29  560%
c i   46.6   66751   416985     13656    9067    450 68992  209   498   46  42%      3  445  164   29  558%
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   46.6   66750   416985     13657    9067    450 68992  209   497   46  42%      3  445  163   29  556%
c i   46.9   66749   416985     13879    9218    452 69005  203   498   46  41%      3  445  128   30  433%
c i   47.0   66748   416985     14001    9299    452 69016  199   490   46  41%      2  435  103   30  348%
c i   47.0   66742   416985     14002    9299    452 69016  199   489   46  41%      2  435  103   30  346%
c i   47.0   66736   416985     14006    9299    452 69018  198   489   46  41%      2  434  101   30  341%
c i   47.0   66400   416985     14007    9299    452 69018  198   489   46  41%      2  434  101   30  340%
c 
c [simplification-9] limit 14580 conflicts (hard 24425) hit after 14581 conflicts
c [quatres-4] found 36641 quaternary clauses 53% in total
c [quatres-4-1] removed 1 duplicate quaternary clauses
c [ternres-5] limit 6531341 with penalty 0 = 0 + 0
c [ternres-5] all 66398 free variables schedulable
c [ternres-5] 27 ternary resolvents (1 bin, 26 trn)
c [ternres-5] 12793 variables remain 19% (53605 retained 81%)
c [decomp-19] removed 404 variables
c [simpleprobe-4] 3990 schedulable variables 6%
c [simpleprobe-4] limit 26125366 penalty 0 = 0 + 0
c [decomp-20] removed 769 variables
c [simpleprobe-4] fully completed simple probing
c [simpleprobe-4] removed 769 variables, found 37242 hbrs, 311 units
c [unhide-9] limit 1306268 with penalty 0 = 0 + 0
c [unhide-9-9] 5 units, 52 failed, 9717 tauts, 0 hbrs, 31825 literals
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 399 transitive binary clauses
c [transred-5] found 5 units
c [bca-5] limit of 10000000 steps and 794980 added (scaled 2)
c [bca-5] 112784 out of 130876 literals actually usable 86%
c [bca-5] added 67 blocked clauses in 325718 steps
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 19594020 penalty 0 = 0 + 0
c [sweep-5-1] 3646 pos 5.6% + 61604 neg 94.4% = 65250 sched 99.7% ret 187
c [sweep-5-1] 19630199 steps 343 queries 1803.36 avg class size
c [sweep-5-1] 3887 decisions 276 SAT calls 87.89 avg env size
c [sweep-5-1] 56807 variables remain 87% (8297 retained 13%)
c [decomp-21] removed 808 variables
c [sweep-5-1] removed 808 vars (0 failed, 80 eqs, 127 impls)
c [sweep-5] considered successful since not run to completion yet
c [sweep-5] removed 808 vars in TOTAL (1 rounds, 342 queries)
c [phase-count-9] 391657 negative 99.7% of 392948 except 1291 0.3%
c [phase-count-9] 307194 positive 78.2% of 392948 except 85754 21.8%
c [phase-count-9] less non-negative clauses 1291 than limit 39200 (10.0%)
c [phase-count-9] non-pos/non-neg = 85754/1291 = 66.42 >= 2.00 = 200/100
c [lucky-phase-9] forcing lucky phase -1
c [phase-9] phase bias: 0 positive 0%, 83 negative 100%
c [sort-queue-9] sorted 26841 enqueued variables after 14581 conflicts
c [score-dist-9] active 37788 (58%), one 0 (0%), zero 26841 (42%)
c [score-dist-9] max exp 510, different 66 (13%)
c [score-dist-9] median active exp 500, avg 491.7
c [simplification-9] removed 1769 variables 2.7% (64629 remain 30%)
c [simplification-9] removed 24037 irredundant clauses 5.8% (392948 remain 33%)
c [simplification-9] maximum reduction of 6% = max (3%, 6%)
c [simplification-9] large reduction 6% >= 5% limit
c [simplification-9] next conflict interval 2000 = 2000/1
c [simplification-9] penalized conflict interval 2000 = 1 * 2000
c [simplification-9] hard conflict limit 26581 (soft 16581 + delta 10000)
c [simplification-9] new conflict limit 16581 (hard 26581)
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.5   64628   392948     14615    9159    453 118852  213   489   42  44%      3  430  287   32  893%
c i   51.5   64627   392948     14620    9160    453 118852  213   488   42  44%      3  430  287   32  893%
c i   51.7   64626   392948     14689    9187    453 118852  216   488   43  44%      3  429  308   33  946%
c i   52.4   64625   392948     15142    9468    456 118856  214   486   45  44%      3  424  207   34  615%
c i   53.6   64624   392948     15902   10052    463 118857  206   479   45  43%      4  413  160   35  455%
c i   53.8   64618   392948     16038   10170    464 118857  204   477   45  43%      4  409  156   35  439%
c i   54.1   64615   392948     16295   10386    465 118858  200   470   45  42%      3  401  142   36  396%
c 
c [simplification-10] limit 16583 conflicts (hard 26581) hit after 16586 conflicts
c [ternres-6] limit 7321351 with penalty 0 = 0 + 0
c [ternres-6] 12465 schedulable variables 19%
c [ternres-6] 29 ternary resolvents (2 bin, 27 trn)
c [ternres-6] fully completed ternary resolution
c [card-4] limit 457584 penalty 3 = 3 + 0
c [card-4] found 1818 at-most-one constraints of average size 4.1
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 457584 for elimination
c [card-4] 1818 out of 1818 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 26 xors of average arity 2.7
c [gauss-3] connected 71 occurrences of 62 variables (average 1.1)
c [gauss-3] limit 500000 penalty 2 = 2 + 0
c [gauss-3] fully completed
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-22] removed 3 variables
c [treelook-4] limit 732135 penalty 0 = 0 + 0 boost 1
c [treelook-4] scheduled 85629 literals 66%
c [treelook-4] scheduling used 732138 steps
c [treelook-4] not fully scheduled
c [treelook-4] limit 732135 penalty 0 = 0 + 0 boost 1
c [treelook-4] used 837816 steps
c [treelook-4] 85612 literals remain 66%
c [treelook-4] 21822 variables remain to probed next time 34%
c [treelook-4] removed 2 variables, found 4902 hbrs
c [unhide-10] limit 1464270 with penalty 0 = 0 + 0
c [unhide-10-10] 12 units, 333 failed, 13264 tauts, 0 hbrs, 77020 literals
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 342 transitive binary clauses
c [transred-6] found 6 units
c [cce-4] boosting limit by 10
c [cce-4] limit of 183033780 steps penalty 1 = 1 + 0
c [cce-4-1] eliminated 17901 clauses out of 27591 (65%) of length 5
c [cce-4-1] incomplete large round (ATE)
c [cce-4-1] eliminated 17901 large clauses in 183033791 steps
c [cce-4-1] allowing another 91516895 steps for small clauses
c [cce-4-1] scheduling 217288 clauses = 200841 binary + 16447 ternary
c [cce-4-1] tried to eliminate 6884 small clauses 3%
c [cce-4-1] eliminated 1857 binary clauses 1%
c [cce-4-1] eliminated 277 ternary clauses 2%
c [cce-4-1] eliminated 2134 small clauses 1%
c [cce-4-1] eliminated 5832 small clauses in 183033781 steps
c [cce-4-1] incomplete small round (ATE)
c [cce-4-1] eliminated 23733 covered clauses in round 1
c [cce-4] eliminated 23733 covered clauses in TOTAL during 1 rounds
c [elim-7] no untried remaining variables left
c [elim-7] scheduled 64245 variables 100%
c [elim-7] limit of 36606756 steps penalty 2 = 2 + 0
c [elim-7] rescheduling of touched variables disabled
c [elim-7-1] eliminated 13826 variables 22% in round 1 in 34619173 steps
c [elim-7-1] backward subsumption/strengthening limit 1987583
c [elim-7-1-1] backward checking 32008 touched variables 50%
c [elim-7-1-1] incomplete backward checking 23900 remain 75%
c [elim-7-1] subsumed 97 and strengthened 165 clauses in 1987596 steps
c [elim-7] incomplete 579 not tried 1% in round 1
c [gc-66] reconnected 110945 binary clauses (produced 0 empty 1 units)
c [elim-7] transition to [ all 1 rem 1 ] state
c [elim-7] eliminated 13858 = 22% variables out of 64245 scheduled
c [bca-6] limit of 10000000 steps and 670141 added (scaled 2)
c [bca-6] 95996 out of 100776 literals actually usable 95%
c [bca-6] added 66 blocked clauses in 247928 steps
c [sweep-6] limit 2196405 penalty 0 = 0 + 0
c [sweep-6-1] 3322 pos 7.5% + 41045 neg 92.5% = 44367 sched 88.1% ret 6020
c [sweep-6-1] 2234991 steps 52 queries 6418.35 avg class size
c [sweep-6-1] 578 decisions 45 SAT calls 42.18 avg env size
c [sweep-6-1] 44043 variables remain 87% (6318 retained 13%)
c [decomp-24] removed 42 variables
c [sweep-6-1] removed 42 vars (0 failed, 8 eqs, 12 impls)
c [sweep-6] considered successful since not run to completion yet
c [sweep-6] removed 42 vars in TOTAL (1 rounds, 51 queries)
c [phase-count-10] 333301 negative 99.7% of 334323 except 1022 0.3%
c [phase-count-10] 252107 positive 75.4% of 334323 except 82216 24.6%
c [phase-count-10] less non-negative clauses 1022 than limit 33400 (10.0%)
c [phase-count-10] non-pos/non-neg = 82216/1022 = 80.45 >= 2.00 = 200/100
c [lucky-phase-10] forcing lucky phase -1
c [phase-10] phase bias: 0 positive 0%, 75 negative 100%
c [sort-queue-10] sorted 20181 enqueued variables after 16586 conflicts
c [score-dist-10] active 30164 (60%), one 0 (0%), zero 20181 (40%)
c [score-dist-10] max exp 510, different 74 (14%)
c [score-dist-10] median active exp 496, avg 489.6
c [simplification-10] removed 14267 variables 22.1% (50345 remain 24%)
c [simplification-10] removed 58625 irredundant clauses 14.9% (334323 remain 28%)
c [simplification-10] maximum reduction of 22% = max (22%, 15%)
c [simplification-10] large reduction 22% >= 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 28586 (soft 18586 + delta 10000)
c [simplification-10] new conflict limit 18586 (hard 28586)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   63.2   50344   334323     16928    1654    585 97470  182   453   31  40%      4  380   48   36  131%
c i   63.2   50343   334323     16929    1654    585 97470  182   453   31  40%      4  380   47   36  131%
c i   63.2   50342   334323     16930    1654    585 97470  182   453   31  40%      4  380   47   36  130%
c i   63.2   50340   334323     16931    1654    585 97470  182   453   31  40%      4  380   47   36  130%
c i   63.5   50333   334323     17184    1882    590 97471  177   460   31  38%      3  386   81   36  222%
c i   63.5   50321   334323     17194    1886    590 97471  177   460   31  39%      3  386   94   36  257%
c i   63.7   50310   334323     17355    2018    592 97471  180   467   32  39%      3  392  173   37  467%
c i   64.0   50301   334323     17665    2284    594 97473  178   482   32  37%      2  404  162   38  433%
c i   64.0   50300   334323     17667    2284    594 97473  178   481   32  37%      2  404  164   38  436%
c i   64.0   50299   334323     17672    2285    594 97473  179   482   32  37%      2  404  170   38  454%
c i   64.0   50295   334323     17695    2299    596 97474  180   482   32  37%      2  405  188   38  498%
c i   64.1   50290   334323     17716    2315    596 97475  180   483   32  37%      2  405  191   38  507%
c i   64.3   50284   334323     18172    2701    600 97493  171   458   33  37%      3  378  103   38  271%
c i   64.3   50280   334323     18175    2703    600 97493  171   458   33  37%      3  378  104   38  272%
c i   64.3   50275   334323     18176    2703    600 97493  171   458   33  37%      3  378  103   38  271%
c i   64.3   50269   334323     18177    2703    600 97493  171   458   33  37%      3  377  103   38  270%
c i   64.5   50264   334323     18347    2842    601 97495  171   455   33  37%      2  374  131   38  340%
c i   64.5   50261   334323     18359    2853    601 97495  170   455   33  37%      2  374  131   38  340%
c i   64.6   50259   334323     18446    2917    602 97495  171   453   33  38%      2  371  151   39  391%
c i   64.7   50255   334323     18484    2941    602 97496  171   452   33  38%      2  370  154   39  397%
c 
c [simplification-11] limit 18647 conflicts (hard 28586) hit after 18647 conflicts
c [quatres-5] found 41105 quaternary clauses 75% in total
c [quatres-5-2] added 3 single-self-subsuming ternary resolvents
c [quatres-5-2] added 14 quaternary resolvents
c [ternres-7] limit 7934887 with penalty 0 = 0 + 0
c [ternres-7] all 50248 free variables schedulable
c [ternres-7] 1013 ternary resolvents (0 bin, 1013 trn)
c [ternres-7] fully completed ternary resolution
c [decomp-25] removed 124 variables
c [basicprobe-4] limit 39674437 penalty 0 = 0 + 0
c [basicprobe-4-0] 13371 probes remain 27% after last round
c [basicprobe-4-0] 502 units = 502 failed (100%) + 0 lifted (0%)
c [basicprobe-4-0] removed 958 variables, found 83409 hbrs
c [bate-2] eliminated 459 asymmetric tautologies during probing
c [unhide-11] limit 1586977 with penalty 0 = 0 + 0
c [unhide-11-11] 31 units, 135 failed, 5801 tauts, 0 hbrs, 36610 literals
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 402 transitive binary clauses
c [block-4] scheduling all variables this time
c [block-4] scheduled 48995 variables 100%
c [block-4] limit of 19837218 steps penalty 2 = 2 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 674 blocked clauses
c [block-4] 674 < 1/100 * 320891 = 3208 considered unsuccessful
c [cce-5] limit of 39674437 steps penalty 0 = 0 + 0
c [cce-5-1] eliminated 1 clauses out of 1 (100%) of length 37
c [cce-5-1] eliminated 2 clauses out of 2 (100%) of length 36
c [cce-5-1] eliminated 1 clauses out of 2 (50%) of length 35
c [cce-5-1] eliminated 1 clauses out of 2 (50%) of length 34
c [cce-5-1] eliminated 2 clauses out of 2 (100%) of length 33
c [cce-5-1] eliminated 1 clauses out of 2 (50%) of length 32
c [cce-5-1] eliminated 1 clauses out of 3 (33%) of length 31
c [cce-5-1] eliminated 4 clauses out of 4 (100%) of length 30
c [cce-5-1] eliminated 2 clauses out of 4 (50%) of length 29
c [cce-5-1] eliminated 4 clauses out of 5 (80%) of length 28
c [cce-5-1] eliminated 3 clauses out of 5 (60%) of length 27
c [cce-5-1] eliminated 6 clauses out of 6 (100%) of length 26
c [cce-5-1] eliminated 3 clauses out of 6 (50%) of length 25
c [cce-5-1] eliminated 6 clauses out of 6 (100%) of length 24
c [cce-5-1] eliminated 3 clauses out of 6 (50%) of length 23
c [cce-5-1] eliminated 6 clauses out of 6 (100%) of length 22
c [cce-5-1] eliminated 3 clauses out of 6 (50%) of length 21
c [cce-5-1] eliminated 5 clauses out of 6 (83%) of length 20
c [cce-5-1] eliminated 4 clauses out of 6 (67%) of length 19
c [cce-5-1] eliminated 5 clauses out of 7 (71%) of length 18
c [cce-5-1] eliminated 5 clauses out of 7 (71%) of length 17
c [cce-5-1] eliminated 7 clauses out of 8 (88%) of length 16
c [cce-5-1] eliminated 6 clauses out of 8 (75%) of length 15
c [cce-5-1] eliminated 6 clauses out of 8 (75%) of length 14
c [cce-5-1] eliminated 6 clauses out of 8 (75%) of length 13
c [cce-5-1] eliminated 6 clauses out of 8 (75%) of length 12
c [cce-5-1] eliminated 6 clauses out of 8 (75%) of length 11
c [cce-5-1] eliminated 6 clauses out of 8 (75%) of length 10
c [cce-5-1] eliminated 7 clauses out of 10 (70%) of length 9
c [cce-5-1] eliminated 5 clauses out of 8 (62%) of length 8
c [cce-5-1] eliminated 18 clauses out of 34 (53%) of length 7
c [cce-5-1] eliminated 52 clauses out of 1265 (4%) of length 6
c [cce-5-1] eliminated 208 clauses out of 10104 (2%) of length 5
c [cce-5-1] incomplete large round (ACCE)
c [cce-5-1] eliminated 401 large clauses in 39674442 steps
c [cce-5-1] allowing another 19837221 steps for small clauses
c [cce-5-1] scheduling 165927 clauses = 151391 binary + 14536 ternary
c [cce-5-1] tried to eliminate 1993 small clauses 1%
c [cce-5-1] eliminated 599 binary clauses 0%
c [cce-5-1] eliminated 97 ternary clauses 1%
c [cce-5-1] eliminated 696 small clauses 0%
c [cce-5-1] eliminated 696 small clauses in 39674438 steps
c [cce-5-1] incomplete small round (ACCE)
c [cce-5-1] eliminated 1097 covered clauses in round 1
c [cce-5] eliminated 1097 covered clauses in TOTAL during 1 rounds
c [cce-5] 1097 < 1/100 * 318426 = 3184 considered unsuccessful
c [bca-7] limit of 10000000 steps and 635504 added (scaled 2)
c [bca-7] 89668 out of 97982 literals actually usable 92%
c [bca-7] added 26 blocked clauses in 225935 steps
c [sweep-7] limit 2380466 penalty 0 = 0 + 0
c [sweep-7-1] 3373 pos 7.8% + 39607 neg 92.2% = 42980 sched 87.7% ret 6010
c [sweep-7-1] 2397626 steps 55 queries 6614.45 avg class size
c [sweep-7-1] 546 decisions 50 SAT calls 65.38 avg env size
c [sweep-7-1] 42541 variables remain 87% (6448 retained 13%)
c [decomp-26] removed 150 variables
c [sweep-7-1] removed 150 vars (0 failed, 4 eqs, 8 impls)
c [sweep-7] removed 150 vars in TOTAL (1 rounds, 54 queries)
c [phase-count-11] 315821 negative 99.7% of 316807 except 986 0.3%
c [phase-count-11] 238684 positive 75.3% of 316807 except 78123 24.7%
c [phase-count-11] skipping relative phase luck test
c [phase-11] phase bias: 11 positive 100%, 0 negative 0%
c [sort-queue-11] sorted 17834 enqueued variables after 18647 conflicts
c [score-dist-11] active 31006 (63%), one 0 (0%), zero 17834 (37%)
c [score-dist-11] max exp 509, different 81 (16%)
c [score-dist-11] median active exp 496, avg 489.7
c [simplification-11] removed 1408 variables 2.8% (48840 remain 23%)
c [simplification-11] removed 17516 irredundant clauses 5.2% (316807 remain 27%)
c [simplification-11] maximum reduction of 5% = max (3%, 5%)
c [simplification-11] large reduction 5% >= 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 30647 (soft 20647 + delta 10000)
c [simplification-11] new conflict limit 20647 (hard 30647)
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   70.6   48839   316807     20290    4262   1887 170502  174   449   36  39%     14  357  170   43  401%
c i   70.8   48837   316807     20581    4492   1902 170513  178   469   36  38%     11  376  201   43  463%
c i   70.8   48836   316807     20583    4493   1902 170513  178   469   36  38%     11  376  202   43  465%
c i   70.8   48834   316807     20584    4493   1902 170513  178   468   36  38%     11  375  201   43  463%
c i   70.8   48828   316807     20585    4493   1902 170513  178   468   36  38%     11  375  200   43  461%
c i   70.8   48822   316807     20586    4493   1902 170513  178   468   36  38%     11  375  199   43  459%
c i   70.8   48815   316807     20589    4495   1902 170513  178   468   36  38%     11  375  200   43  460%
c 
c [simplification-12] limit 20685 conflicts (hard 30647) hit after 20685 conflicts
c [quatres-6] found 38345 quaternary clauses 76% in total
c [quatres-6-2] added 3 single-self-subsuming ternary resolvents
c [quatres-6-2] added 1 quaternary resolvents
c [ternres-8] limit 8503957 with penalty 0 = 0 + 0
c [ternres-8] all 48815 free variables schedulable
c [ternres-8] 62 ternary resolvents (0 bin, 62 trn)
c [ternres-8] fully completed ternary resolution
c [decomp-27] removed 28 variables
c [simpleprobe-5] all 48812 free variables schedulable
c [simpleprobe-5] limit 34015829 penalty 0 = 0 + 0
c [decomp-28] removed 1313 variables
c [simpleprobe-5] 65 variables remain 0% (47434 retained 100%)
c [simpleprobe-5] removed 1313 variables, found 63359 hbrs, 668 units
c [unhide-12] limit 1700791 with penalty 0 = 0 + 0
c [unhide-12-12] 3 units, 198 failed, 29827 tauts, 0 hbrs, 18195 literals
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 355 transitive binary clauses
c [transred-8] found 1 units
c [elim-8] no untried remaining variables left
c [elim-8] scheduled 47198 variables 100%
c [elim-8] boosting limit by 20
c [elim-8] limit of 1700791490 steps penalty 1 = 1 + 0
c [elim-8] rescheduling of touched variables disabled
c [elim-8-1] eliminated 1868 variables 4% in round 1 in 26240836 steps
c [elim-8-1] backward subsumption/strengthening limit 26240800
c [elim-8-1-1] backward checking 7908 touched variables 17%
c [elim-8-1-1] fully completed backward checking in 1 rounds
c [elim-8-1] subsumed 64 and strengthened 113 clauses in 1955468 steps
c [elim-8-1] rescheduled 409 variables 1% by backward subsumption
c [elim-8-2] eliminated 37 variables 0% in round 2 in 1124374 steps
c [elim-8-2] backward subsumption/strengthening limit 1124300
c [elim-8-2-1] backward checking 287 touched variables 1%
c [elim-8-2-1] fully completed backward checking in 1 rounds
c [elim-8-2] subsumed 19 and strengthened 22 clauses in 218876 steps
c [elim-8-2] rescheduled 69 variables 0% by backward subsumption
c [elim-8-3] eliminated 6 variables 0% in round 3 in 520987 steps
c [elim-8-3] backward subsumption/strengthening limit 520900
c [elim-8-3-1] backward checking 52 touched variables 0%
c [elim-8-3-1] fully completed backward checking in 1 rounds
c [elim-8-3] subsumed 8 and strengthened 3 clauses in 91650 steps
c [elim-8] incomplete 19 not tried 0% in round 3
c [elim-8] transition to [ all 1 rem 1 ] state
c [elim-8] eliminated 1918 = 4% variables out of 47198 scheduled
c [bca-8] limit of 10000000 steps and 593401 added (scaled 2)
c [bca-8] 82039 out of 90562 literals actually usable 91%
c [bca-8] added 60 blocked clauses in 206080 steps
c [sweep-8] limit 2551187 penalty 0 = 0 + 0
c [sweep-8-1] 3034 pos 7.6% + 36723 neg 92.4% = 39757 sched 87.8% ret 5523
c [sweep-8-1] 2552988 steps 64 queries 4844.67 avg class size
c [sweep-8-1] 627 decisions 55 SAT calls 90.18 avg env size
c [sweep-8-1] 39388 variables remain 87% (5859 retained 13%)
c [decomp-29] removed 107 variables
c [sweep-8-1] removed 107 vars (0 failed, 9 eqs, 15 impls)
c [sweep-8] removed 107 vars in TOTAL (1 rounds, 63 queries)
c [phase-count-12] 294935 negative 99.7% of 295905 except 970 0.3%
c [phase-count-12] 218959 positive 74.0% of 295905 except 76946 26.0%
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 14776 enqueued variables after 20685 conflicts
c [score-dist-12] active 30397 (67%), one 0 (0%), zero 14776 (33%)
c [score-dist-12] max exp 509, different 89 (17%)
c [score-dist-12] median active exp 494, avg 488.4
c [simplification-12] removed 3642 variables 7.5% (45173 remain 21%)
c [simplification-12] removed 20902 irredundant clauses 6.6% (295905 remain 25%)
c [simplification-12] maximum reduction of 7% = max (7%, 7%)
c [simplification-12] large reduction 7% >= 5% limit
c [simplification-12] next conflict interval 2000 = 2000/1
c [simplification-12] penalized conflict interval 2000 = 1 * 2000
c [simplification-12] hard conflict limit 32685 (soft 22685 + delta 10000)
c [simplification-12] new conflict limit 22685 (hard 32685)
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   74.8   45172   295905     21259    3624   1468 189631  185   479   33  39%      8  382  234   45  517%
c i   74.8   45170   295905     21276    3638   1468 189631  185   479   33  39%      8  382  224   45  496%
c i   74.8   45144   295905     21291    3651   1468 189631  184   479   33  38%      8  382  217   45  479%
c i   74.8   45142   295905     21293    3652   1468 189631  184   479   33  38%      8  382  215   45  476%
c i   74.8   45140   295905     21294    3652   1468 189631  184   479   33  38%      8  382  214   45  474%
c i   74.8   45137   295905     21323    3677   1470 189631  183   479   33  38%      7  382  199   45  440%
c i   75.1   45135   295905     21677    3977   1479 189645  178   480   34  37%      6  381  135   46  295%
c i   75.1   45133   295905     21706    4000   1479 189645  178   480   34  37%      5  381  138   46  302%
c i   75.2   45126   295905     21729    4019   1478 189646  178   481   34  37%      5  381  138   46  303%
c i   75.2   45121   295905     21791    4062   1478 189651  177   480   34  37%      5  380  141   46  308%
c i   75.2   45118   295905     21794    4063   1478 189651  177   480   34  37%      5  380  141   46  307%
c i   75.2   45115   295905     21795    4063   1478 189651  177   480   34  37%      5  380  140   46  306%
c i   75.2   45113   295905     21796    4063   1478 189651  177   480   34  37%      5  380  139   46  305%
c i   75.2   45109   295905     21797    4063   1478 189651  177   479   34  37%      5  380  139   46  304%
c i   75.2   45106   295905     21798    4063   1478 189651  177   479   34  37%      5  379  138   46  302%
c i   75.6   45102   295905     22368    4485   1486 189675  166   449   34  37%      4  346   81   46  177%
c 
c [simplification-13] limit 22743 conflicts (hard 32685) hit after 22743 conflicts
c [quatres-7] found 33514 quaternary clauses 74% in total
c [quatres-7-2] added 25 quaternary resolvents
c [ternres-9] limit 9032601 with penalty 0 = 0 + 0
c [ternres-9] all 45101 free variables schedulable
c [ternres-9] 625 ternary resolvents (1 bin, 624 trn)
c [ternres-9] fully completed ternary resolution
c [decomp-30] removed 81 variables
c [treelook-5] limit 903260 penalty 0 = 0 + 0 boost 1
c [treelook-5] scheduled 67528 literals 75%
c [treelook-5] scheduling used 903262 steps
c [treelook-5] not fully scheduled
c [treelook-5] limit 903260 penalty 0 = 0 + 0 boost 1
c [treelook-5] used 978352 steps
c [treelook-5] 67482 literals remain 75%
c [treelook-5] 10787 variables remain to probed next time 24%
c [treelook-5] removed 8 variables, found 7906 hbrs
c [unhide-13] limit 1806520 with penalty 0 = 0 + 0
c [unhide-13-14] 24 units, 171 failed, 18608 tauts, 0 hbrs, 24905 literals
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 352 transitive binary clauses
c [transred-9] found 1 units
c [cce-6] limit of 22581503 steps penalty 1 = 1 + 0
c [cce-6-1] eliminated 2 clauses out of 3 (67%) of length 24
c [cce-6-1] eliminated 1 clauses out of 3 (33%) of length 23
c [cce-6-1] eliminated 2 clauses out of 3 (67%) of length 22
c [cce-6-1] eliminated 1 clauses out of 5 (20%) of length 21
c [cce-6-1] eliminated 1 clauses out of 3 (33%) of length 20
c [cce-6-1] eliminated 2 clauses out of 5 (40%) of length 19
c [cce-6-1] eliminated 1 clauses out of 4 (25%) of length 18
c [cce-6-1] eliminated 2 clauses out of 5 (40%) of length 17
c [cce-6-1] eliminated 1 clauses out of 3 (33%) of length 16
c [cce-6-1] eliminated 2 clauses out of 4 (50%) of length 15
c [cce-6-1] eliminated 1 clauses out of 5 (20%) of length 14
c [cce-6-1] eliminated 2 clauses out of 3 (67%) of length 13
c [cce-6-1] eliminated 1 clauses out of 5 (20%) of length 12
c [cce-6-1] eliminated 2 clauses out of 4 (50%) of length 11
c [cce-6-1] eliminated 3 clauses out of 6 (50%) of length 10
c [cce-6-1] eliminated 3 clauses out of 8 (38%) of length 9
c [cce-6-1] eliminated 3 clauses out of 5 (60%) of length 8
c [cce-6-1] eliminated 3 clauses out of 21 (14%) of length 7
c [cce-6-1] eliminated 16 clauses out of 1222 (1%) of length 6
c [cce-6-1] incomplete large round (ATE)
c [cce-6-1] eliminated 49 large clauses in 22581503 steps
c [cce-6-1] allowing another 11290751 steps for small clauses
c [cce-6-1] scheduling 155992 clauses = 139995 binary + 15997 ternary
c [cce-6-1] tried to eliminate 1241 small clauses 1%
c [cce-6-1] eliminated 319 binary clauses 0%
c [cce-6-1] eliminated 70 ternary clauses 0%
c [cce-6-1] eliminated 389 small clauses 0%
c [cce-6-1] eliminated 1686 small clauses in 22581505 steps
c [cce-6-1] incomplete small round (ATE)
c [cce-6-1] eliminated 1735 covered clauses in round 1
c [cce-6] eliminated 1735 covered clauses in TOTAL during 1 rounds
c [cce-6] 1735 < 1/100 * 289754 = 2897 considered unsuccessful
c [elim-9] no untried remaining variables left
c [elim-9] scheduled 44875 variables 100%
c [elim-9] limit of 180652026 steps penalty 0 = 0 + 0
c [elim-9] rescheduling of touched variables disabled
c [elim-9-1] eliminated 678 variables 2% in round 1 in 24624159 steps
c [elim-9-1] backward subsumption/strengthening limit 24624100
c [elim-9-1-1] backward checking 3562 touched variables 8%
c [elim-9-1-1] fully completed backward checking in 1 rounds
c [elim-9-1] subsumed 34 and strengthened 75 clauses in 942765 steps
c [elim-9-1] rescheduled 217 variables 0% by backward subsumption
c [elim-9-2] eliminated 18 variables 0% in round 2 in 855203 steps
c [elim-9-2] backward subsumption/strengthening limit 855200
c [elim-9-2-1] backward checking 179 touched variables 0%
c [elim-9-2-1] fully completed backward checking in 1 rounds
c [elim-9-2] subsumed 18 and strengthened 17 clauses in 161825 steps
c [elim-9-2] rescheduled 59 variables 0% by backward subsumption
c [elim-9-3] eliminated 4 variables 0% in round 3 in 454615 steps
c [elim-9-3] backward subsumption/strengthening limit 454600
c [elim-9-3-1] backward checking 44 touched variables 0%
c [elim-9-3-1] fully completed backward checking in 1 rounds
c [elim-9-3] subsumed 4 and strengthened 1 clauses in 82914 steps
c [elim-9] incomplete 12 not tried 0% in round 3
c [gc-90] reconnected 182076 binary clauses (produced 0 empty 1 units)
c [elim-9] transition to [ all 1 rem 1 ] state
c [elim-9] eliminated 711 = 2% variables out of 44875 scheduled
c [bca-9] limit of 10000000 steps and 573079 added (scaled 2)
c [bca-9] 78899 out of 88330 literals actually usable 89%
c [bca-9] added 35 blocked clauses in 198852 steps
c [sweep-9] limit 2709780 penalty 0 = 0 + 0
c [sweep-9-1] 3230 pos 8.4% + 35267 neg 91.6% = 38497 sched 87.2% ret 5667
c [sweep-9-1] 2751294 steps 94 queries 5313.30 avg class size
c [sweep-9-1] 850 decisions 86 SAT calls 63.00 avg env size
c [sweep-9-1] 37829 variables remain 86% (6292 retained 14%)
c [decomp-32] removed 75 variables
c [sweep-9-1] removed 75 vars (0 failed, 15 eqs, 24 impls)
c [sweep-9] removed 75 vars in TOTAL (1 rounds, 93 queries)
c [phase-count-13] 284596 negative 99.7% of 285545 except 949 0.3%
c [phase-count-13] 210647 positive 73.8% of 285545 except 74898 26.2%
c [phase-count-13] skipping relative phase luck test
c [phase-13] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-13] sorted 13633 enqueued variables after 22743 conflicts
c [score-dist-13] active 30456 (69%), one 0 (0%), zero 13633 (31%)
c [score-dist-13] max exp 509, different 96 (19%)
c [score-dist-13] median active exp 494, avg 486.9
c [simplification-13] removed 1012 variables 2.2% (44089 remain 21%)
c [simplification-13] removed 10360 irredundant clauses 3.5% (285545 remain 24%)
c [simplification-13] maximum reduction of 4% = max (2%, 4%)
c [simplification-13] geometric conflict interval increment 4000 = 20000 / 5
c [simplification-13] new conflict interval 9000
c [simplification-13] penalized conflict interval 9000 = 1 * 9000
c [simplification-13] hard conflict limit 41743 (soft 31743 + delta 10000)
c [simplification-13] new conflict limit 31743 (hard 41743)
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.1   44088   285545     23295    4972   1869 180703  169   441   34  38%      6  334  194   48  403%
c i   80.3   44074   285545     23472    5114   1870 180704  173   441   35  39%      5  332  233   49  479%
c i   81.1   44072   285545     24299    5800   1891 180712  165   459   36  36%      5  346  191   50  384%
c i   81.1   44071   285545     24302    5801   1891 180712  165   459   36  36%      5  346  191   50  385%
c i   81.7   44070   285545     24964    6365   1899 180720  171   481   36  36%      5  364  205   51  402%
c i   81.8   44068   285545     25091    6471   1904 180720  173   487   36  36%      4  370  222   51  432%
c i   85.6   44027   285545     29286    9177   1933 180781  194   421   45  46%     47  284  235   61  388%
c i   86.6   44026   285545     30266    9754   1948 180787  192   399   45  48%     21  258  127   62  204%
c i   86.9   43866   285545     30506    9927   1950 180788  192   398   45  48%     17  255  172   63  275%
c i   87.1   43864   285545     30709   10058   1951 180793  195   398   45  49%     13  255  221   63  348%
c i   87.5   43840   285545     31128   10261   1953 180793  200   392   45  51%      9  248  231   65  358%
c i   87.6   43837   285545     31158   10281   1953 180794  199   392   45  51%      8  247  221   65  342%
c i   88.1   43835   285545     31654   10507   1953 180806  202   383   45  53%      5  237  222   66  337%
c 
c [simplification-14] limit 31746 conflicts (hard 41743) hit after 31749 conflicts
c [quatres-8] found 31044 quaternary clauses 73% in total
c [quatres-8-1] added 1 double-self-subsuming ternary resolvents
c [quatres-8-2] added 1 single-self-subsuming ternary resolvents
c [quatres-8-2] added 6 quaternary resolvents
c [ternres-10] limit 11517954 with penalty 0 = 0 + 0
c [ternres-10] all 43829 free variables schedulable
c [ternres-10] 495 ternary resolvents (0 bin, 495 trn)
c [ternres-10] fully completed ternary resolution
c [gauss-4] limit 287948 penalty 3 = 3 + 0
c [gauss-4] extracted 10 xors of average arity 3.0
c [gauss-4] connected 30 occurrences of 30 variables (average 1.0)
c [gauss-4] limit 287948 penalty 3 = 3 + 0
c [gauss-4] fully completed
c [gauss-4] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-33] removed 3 variables
c [basicprobe-5] limit 57589770 penalty 0 = 0 + 0
c [basicprobe-5-0] 9043 probes remain 21% after last round
c [basicprobe-5-0] 604 units = 599 failed (99%) + 5 lifted (1%)
c [basicprobe-5-0] removed 1019 variables, found 122647 hbrs
c [bate-3] eliminated 550 asymmetric tautologies during probing
c [unhide-14] limit 2303590 with penalty 0 = 0 + 0
c [unhide-14-16] 7 units, 154 failed, 26241 tauts, 0 hbrs, 95018 literals
c [transred-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 368 transitive binary clauses
c [transred-10] found 3 units
c [elim-10] no untried remaining variables left
c [elim-10] scheduled 42636 variables 100%
c [elim-10] limit of 230359082 steps penalty 0 = 0 + 0
c [elim-10] rescheduling of touched variables disabled
c [elim-10-1] eliminated 1434 variables 3% in round 1 in 22531274 steps
c [elim-10-1] backward subsumption/strengthening limit 22531200
c [elim-10-1-1] backward checking 6655 touched variables 16%
c [elim-10-1-1] fully completed backward checking in 1 rounds
c [elim-10-1] subsumed 58 and strengthened 95 clauses in 1494872 steps
c [elim-10-1] rescheduled 355 variables 1% by backward subsumption
c [elim-10-2] eliminated 26 variables 0% in round 2 in 190534 steps
c [elim-10-2] backward subsumption/strengthening limit 190500
c [elim-10-2-1] backward checking 265 touched variables 1%
c [elim-10-2-1] fully completed backward checking in 1 rounds
c [elim-10-2] subsumed 25 and strengthened 20 clauses in 141893 steps
c [elim-10-2] rescheduled 80 variables 0% by backward subsumption
c [elim-10-3] eliminated 4 variables 0% in round 3 in 77125 steps
c [elim-10-3] backward subsumption/strengthening limit 77100
c [elim-10-3-1] backward checking 39 touched variables 0%
c [elim-10-3-1] fully completed backward checking in 1 rounds
c [elim-10-3] subsumed 7 and strengthened 2 clauses in 75320 steps
c [elim-10] incomplete 17 not tried 0% in round 3
c [elim-10] transition to [ all 1 rem 1 ] state
c [elim-10] eliminated 1467 = 3% variables out of 42636 scheduled
c [bca-10] limit of 10000000 steps and 532687 added (scaled 2)
c [bca-10] 71027 out of 82340 literals actually usable 86%
c [bca-10] added 48 blocked clauses in 179444 steps
c [sweep-10] limit 3455386 penalty 0 = 0 + 0
c [sweep-10-1] 2984 pos 8.4% + 32419 neg 91.6% = 35403 sched 86.0% ret 5766
c [sweep-10-1] 3477862 steps 82 queries 4808.52 avg class size
c [sweep-10-1] 1160 decisions 71 SAT calls 96.56 avg env size
c [sweep-10-1] 34677 variables remain 84% (6391 retained 16%)
c [decomp-34] removed 184 variables
c [sweep-10-1] removed 184 vars (0 failed, 10 eqs, 19 impls)
c [sweep-10] removed 184 vars in TOTAL (1 rounds, 81 queries)
c [phase-count-14] 263698 negative 99.6% of 264636 except 938 0.4%
c [phase-count-14] 194343 positive 73.4% of 264636 except 70293 26.6%
c [phase-count-14] skipping relative phase luck test
c [phase-14] phase bias: 1 positive 100%, 0 negative 0%
c [sort-queue-14] sorted 11195 enqueued variables after 31749 conflicts
c [score-dist-14] active 29790 (73%), one 0 (0%), zero 11195 (27%)
c [score-dist-14] max exp 509, different 130 (25%)
c [score-dist-14] median active exp 490, avg 477.7
c [simplification-14] removed 2844 variables 6.5% (40985 remain 19%)
c [simplification-14] removed 20909 irredundant clauses 7.3% (264636 remain 22%)
c [simplification-14] maximum reduction of 7% = max (6%, 7%)
c [simplification-14] large reduction 7% >= 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 43749 (soft 33749 + delta 10000)
c [simplification-14] new conflict limit 33749 (hard 43749)
c 
c [simplification-15] limit 33749 conflicts (hard 43749) hit after 33750 conflicts
c [quatres-9] found 27836 quaternary clauses 72% in total
c [quatres-9-2] added 2 single-self-subsuming ternary resolvents
c [quatres-9-2] added 16 quaternary resolvents
c [ternres-11] limit 12091565 with penalty 0 = 0 + 0
c [ternres-11] all 40985 free variables schedulable
c [ternres-11] 936 ternary resolvents (0 bin, 936 trn)
c [ternres-11] fully completed ternary resolution
c [card-5] limit 377861 penalty 4 = 4 + 0
c [card-5] found 873 at-most-one constraints of average size 4.1
c [card-5] no at-most-two constraint found
c [card-5] using previous limit 377861 for elimination
c [card-5] 873 out of 873 constraints (100%) meet size limits
c [card-5] no units found
c [card-5] no at-most-one constraints generated
c [simpleprobe-6] 59 schedulable variables 0%
c [simpleprobe-6] limit 48366260 penalty 0 = 0 + 0
c [decomp-36] removed 154 variables
c [simpleprobe-6] fully completed simple probing
c [simpleprobe-6] removed 154 variables, found 24742 hbrs, 59 units
c [unhide-15] limit 2418313 with penalty 0 = 0 + 0
c [unhide-15-18] 7 units, 215 failed, 25016 tauts, 0 hbrs, 40487 literals
c [transred-11] limit 2000000 with penalty 0 = 0 + 0
c [transred-11] removed 340 transitive binary clauses
c [transred-11] found 1 units
c [block-5] scheduling all variables this time
c [block-5] scheduled 40727 variables 100%
c [block-5] limit of 15114456 steps penalty 3 = 3 + 0
c [block-5] fully completed
c [block-5] transition to [ all 0 rem 0 ] state
c [block-5] eliminated 234 blocked clauses
c [block-5] 234 < 1/100 * 261062 = 2610 considered unsuccessful
c [elim-11] no untried remaining variables left
c [elim-11] scheduled 40724 variables 100%
c [elim-11] limit of 241831300 steps penalty 0 = 0 + 0
c [elim-11] rescheduling of touched variables disabled
c [elim-11-1] eliminated 437 variables 1% in round 1 in 21729068 steps
c [elim-11-1] backward subsumption/strengthening limit 21729000
c [elim-11-1-1] backward checking 2399 touched variables 6%
c [elim-11-1-1] fully completed backward checking in 1 rounds
c [elim-11-1] subsumed 26 and strengthened 42 clauses in 643091 steps
c [elim-11-1] rescheduled 139 variables 0% by backward subsumption
c [elim-11-2] eliminated 8 variables 0% in round 2 in 457360 steps
c [elim-11-2] backward subsumption/strengthening limit 457300
c [elim-11-2-1] backward checking 74 touched variables 0%
c [elim-11-2-1] fully completed backward checking in 1 rounds
c [elim-11-2] subsumed 3 and strengthened 4 clauses in 84405 steps
c [elim-11-2] rescheduled 12 variables 0% by backward subsumption
c [elim-11-3] no variable eliminated in round 3 in 6047 steps
c [elim-11] fully completed in 3 rounds
c [elim-11] transition to [ all 0 rem 0 ] state
c [elim-11] eliminated 446 = 1% variables out of 40724 scheduled
c [bca-11] limit of 10000000 steps and 518457 added (scaled 2)
c [bca-11] 69145 out of 80558 literals actually usable 86%
c [bca-11] added 39 blocked clauses in 176237 steps
c [sweep-11] boosting sweeping limit by 10
c [sweep-11] limit 36274690 penalty 0 = 0 + 0
c [sweep-11-1] 2806 pos 8.2% + 31277 neg 91.8% = 34083 sched 84.6% ret 6195
c [sweep-11-1] 36277965 steps 989 queries 319.18 avg class size
c [sweep-11-1] 10506 decisions 874 SAT calls 85.97 avg env size
c [sweep-11-1] 21627 variables remain 54% (18388 retained 46%)
c [decomp-37] removed 749 variables
c [sweep-11-1] removed 749 vars (0 failed, 147 eqs, 220 impls)
c [sweep-11] removed 749 vars in TOTAL (1 rounds, 988 queries)
c [phase-count-15] 255101 negative 99.6% of 256023 except 922 0.4%
c [phase-count-15] 187040 positive 73.1% of 256023 except 68983 26.9%
c [phase-count-15] skipping relative phase luck test
c [phase-15] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-15] sorted 9092 enqueued variables after 33750 conflicts
c [score-dist-15] active 30437 (77%), one 0 (0%), zero 9092 (23%)
c [score-dist-15] max exp 510, different 138 (27%)
c [score-dist-15] median active exp 502, avg 486.7
c [simplification-15] removed 1456 variables 3.6% (39529 remain 19%)
c [simplification-15] removed 8613 irredundant clauses 3.3% (256023 remain 21%)
c [simplification-15] maximum reduction of 4% = max (4%, 3%)
c [simplification-15] geometric conflict interval increment 4000 = 20000 / 5
c [simplification-15] new conflict interval 13000
c [simplification-15] penalized conflict interval 13000 = 1 * 13000
c [simplification-15] hard conflict limit 56750 (soft 46750 + delta 10000)
c [simplification-15] new conflict limit 46750 (hard 56750)
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  101.3   39528   256023     34375   10521   2838 269795  194   319   41  61%     24  164  157   71  223%
c i  101.3   39527   256023     34377   10520   2838 269795  194   319   41  61%     24  164  157   71  222%
c i  101.3   39526   256023     34379   10521   2838 269795  194   319   41  61%     24  164  156   71  220%
c i  101.3   39525   256023     34380   10521   2838 269795  194   319   41  61%     24  164  155   71  219%
c i  101.3   39521   256023     34381   10521   2838 269795  194   319   41  61%     24  164  154   71  218%
c i  102.2   39520   256023     35352   10971   2840 269798  180   291   43  62%     12  134  134   72  188%
c i  102.6   39517   256023     35747   11070   2840 269800  178   279   43  64%      8  122  149   72  207%
c i  102.6   39516   256023     35758   11075   2840 269800  178   279   43  64%      8  121  148   72  205%
c i  102.7   39513   256023     35860   11121   2840 269800  176   276   43  64%      7  118  133   72  185%
c i  102.7   39512   256023     35861   11121   2840 269800  176   276   43  64%      7  118  133   72  184%
c i  102.7   39511   256023     35862   11121   2840 269800  176   276   43  64%      7  118  132   72  183%
c i  102.8   39504   256023     35936   11157   2840 269800  175   273   43  64%      6  115  128   72  177%
c i  102.8   39503   256023     35952   11163   2840 269800  175   273   43  64%      6  115  126   72  175%
c i  103.5   39501   256023     36836   11677   2842 269801  157   245   43  64%      4   85   90   72  125%
c i  103.6   39496   256023     37011   11732   2842 269802  155   240   43  65%      3   80   99   72  136%
c i  104.2   39495   256023     37708   12114   2842 269806  143   219   43  65%      3   59   70   72   97%
c i  104.3   39494   256023     37961   12227   2843 269806  140   215   43  65%      1   54   94   73  130%
c i  105.3   39493   256023     39343   13288   2869 269831  127   227   46  56%      7   66  118   73  161%
c i  105.9   39447   256023     39882   13650   2875 269843  134   236   48  56%      4   74  171   74  231%
c i  106.6   39445   256023     40607   14161   2881 269852  145   255   48  57%      3   92  215   75  285%
c i  106.6   39440   256023     40691   14207   2882 269853  148   258   48  57%      2   95  232   76  307%
c i  107.1   39439   256023     41109   14476   2883 269855  166   280   48  59%      1  116  316   77  409%
c i  107.2   39435   256023     41257   14608   2883 269855  170   290   48  59%      1  126  303   78  390%
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  107.9   39434   256023     41877   14998   2885 269856  197   323   53  61%      1  157  343   80  428%
c i  108.3   39418   256023     42311   15331   2886 269856  207   341   53  61%      0  174  313   82  383%
c i  108.3   39417   256023     42312   15331   2886 269856  207   341   53  61%      0  174  311   82  381%
c i  108.3   39416   256023     42313   15331   2886 269856  207   341   53  61%      0  174  310   82  380%
c i  108.3   39415   256023     42314   15331   2886 269856  207   341   53  61%      0  174  309   82  378%
c i  108.3   39413   256023     42315   15331   2886 269856  207   341   53  61%      0  174  308   82  377%
c i  108.3   39411   256023     42316   15331   2886 269856  206   341   53  61%      0  174  307   82  375%
c i  108.3   39400   256023     42317   15331   2886 269856  206   341   53  61%      0  174  305   82  374%
c i  108.3   39399   256023     42318   15331   2886 269856  206   341   53  61%      0  174  304   82  373%
c i  108.4   39394   256023     42319   15331   2886 269856  206   340   53  61%      0  174  303   82  371%
c i  108.4   39389   256023     42321   15332   2886 269856  206   340   53  61%      0  174  302   82  370%
c i  108.4   39388   256023     42322   15332   2886 269856  206   340   53  61%      0  174  301   82  369%
c i  108.4   39387   256023     42323   15332   2886 269856  206   340   53  61%      0  173  300   82  367%
c i  108.4   39386   256023     42324   15332   2886 269856  206   340   53  61%      0  173  299   82  366%
c i  108.4   39385   256023     42325   15332   2886 269856  206   340   53  61%      0  173  298   82  365%
c i  108.4   39380   256023     42328   15333   2886 269856  206   340   53  61%      0  173  295   82  362%
c i  108.4   39375   256023     42329   15333   2886 269856  206   340   53  61%      0  173  294   82  360%
c i  108.5   39368   256023     42456   15427   2888 269856  207   343   53  60%     -0  176  275   82  336%
c i  109.9   39365   256023     43854   16509   2906 269863  226   387   53  58%      6  216  235   86  274%
c i  112.1   39364   256023     46150   18360   2923 269906  249   431   64  58%     18  251  291   92  314%
c i  112.2   39362   256023     46263   18419   2925 269906  251   431   64  58%     16  251  303   93  326%
c i  112.2   39361   256023     46264   18419   2925 269906  251   431   64  58%     16  251  302   93  325%
c i  112.2   39357   256023     46265   18419   2925 269906  251   430   64  58%     16  251  301   93  324%
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.2   39355   256023     46266   18419   2925 269906  251   430   64  58%     16  251  299   93  322%
c i  112.2   39347   256023     46267   18419   2925 269906  251   430   64  58%     16  250  298   93  321%
c i  112.2   39346   256023     46268   18419   2925 269906  251   430   64  58%     16  250  297   93  320%
c i  112.2   39345   256023     46269   18419   2925 269906  251   430   64  58%     16  250  296   93  319%
c i  112.4   39344   256023     46494   18585   2925 269906  249   426   64  59%     12  246  252   93  270%
c 
c [simplification-16] limit 46998 conflicts (hard 56750) hit after 47000 conflicts
c [quatres-10] found 26021 quaternary clauses 70% in total
c [quatres-10-2] added 5 single-self-subsuming ternary resolvents
c [quatres-10-2] added 8 quaternary resolvents
c [ternres-12] limit 15690239 with penalty 0 = 0 + 0
c [ternres-12] all 39334 free variables schedulable
c [ternres-12] 680 ternary resolvents (0 bin, 680 trn)
c [ternres-12] fully completed ternary resolution
c [decomp-38] removed 243 variables
c [treelook-6] limit 1569023 penalty 0 = 0 + 0 boost 1
c [treelook-6] scheduled 57599 literals 73%
c [treelook-6] scheduling used 992419 steps
c [treelook-6] scheduled completely
c [treelook-6] limit 1569023 penalty 0 = 0 + 0 boost 1
c [treelook-6] used 1644010 steps
c [treelook-6] 57398 literals remain 73%
c [treelook-6] 8786 variables remain to probed next time 22%
c [decomp-39] removed 50 variables
c [treelook-6] removed 98 variables, found 16439 hbrs
c [unhide-16] limit 3138047 with penalty 0 = 0 + 0
c [unhide-16-20] 8 units, 99 failed, 24894 tauts, 0 hbrs, 160189 literals
c [transred-12] limit 2000000 with penalty 0 = 0 + 0
c [transred-12] removed 299 transitive binary clauses
c [transred-12] found 2 units
c [cce-7] limit of 19612799 steps penalty 2 = 2 + 0
c [cce-7-1] eliminated 1 clauses out of 3 (33%) of length 22
c [cce-7-1] eliminated 3 clauses out of 4 (75%) of length 21
c [cce-7-1] eliminated 3 clauses out of 5 (60%) of length 20
c [cce-7-1] eliminated 4 clauses out of 9 (44%) of length 19
c [cce-7-1] eliminated 6 clauses out of 7 (86%) of length 18
c [cce-7-1] eliminated 2 clauses out of 7 (29%) of length 17
c [cce-7-1] eliminated 4 clauses out of 5 (80%) of length 16
c [cce-7-1] eliminated 3 clauses out of 9 (33%) of length 15
c [cce-7-1] eliminated 3 clauses out of 5 (60%) of length 14
c [cce-7-1] eliminated 2 clauses out of 9 (22%) of length 13
c [cce-7-1] eliminated 4 clauses out of 5 (80%) of length 12
c [cce-7-1] eliminated 3 clauses out of 7 (43%) of length 11
c [cce-7-1] eliminated 3 clauses out of 6 (50%) of length 10
c [cce-7-1] eliminated 2 clauses out of 7 (29%) of length 9
c [cce-7-1] eliminated 4 clauses out of 7 (57%) of length 8
c [cce-7-1] eliminated 6 clauses out of 21 (29%) of length 7
c [cce-7-1] eliminated 17 clauses out of 1128 (2%) of length 6
c [cce-7-1] eliminated 18 clauses out of 8285 (0%) of length 5
c [cce-7-1] incomplete large round (ACCE)
c [cce-7-1] eliminated 88 large clauses in 19612813 steps
c [cce-7-1] allowing another 9806406 steps for small clauses
c [cce-7-1] scheduling 138489 clauses = 122846 binary + 15643 ternary
c [cce-7-1] tried to eliminate 1221 small clauses 1%
c [cce-7-1] eliminated 297 binary clauses 0%
c [cce-7-1] eliminated 120 ternary clauses 1%
c [cce-7-1] eliminated 417 small clauses 0%
c [cce-7-1] eliminated 623 small clauses in 19612801 steps
c [cce-7-1] incomplete small round (ACCE)
c [cce-7-1] eliminated 711 covered clauses in round 1
c [cce-7] eliminated 711 covered clauses in TOTAL during 1 rounds
c [cce-7] 711 < 1/100 * 247903 = 2479 considered unsuccessful
c [elim-12] scheduling all variables this time
c [elim-12] scheduled 38971 variables 100%
c [elim-12] limit of 313804785 steps penalty 0 = 0 + 0
c [elim-12] rescheduling of touched variables disabled
c [elim-12-1] eliminated 1162 variables 3% in round 1 in 22451555 steps
c [elim-12-1] backward subsumption/strengthening limit 22451500
c [elim-12-1-1] backward checking 4668 touched variables 12%
c [elim-12-1-1] fully completed backward checking in 1 rounds
c [elim-12-1] subsumed 33 and strengthened 63 clauses in 1254930 steps
c [elim-12-1] rescheduled 213 variables 1% by backward subsumption
c [elim-12-2] eliminated 17 variables 0% in round 2 in 733747 steps
c [elim-12-2] backward subsumption/strengthening limit 733700
c [elim-12-2-1] backward checking 172 touched variables 0%
c [elim-12-2-1] fully completed backward checking in 1 rounds
c [elim-12-2] subsumed 15 and strengthened 4 clauses in 119698 steps
c [elim-12-2] rescheduled 40 variables 0% by backward subsumption
c [elim-12-3] eliminated 6 variables 0% in round 3 in 127019 steps
c [elim-12-3] backward subsumption/strengthening limit 127000
c [elim-12-3-1] backward checking 69 touched variables 0%
c [elim-12-3-1] fully completed backward checking in 1 rounds
c [elim-12-3] subsumed 2 and strengthened 0 clauses in 89786 steps
c [elim-12] incomplete 3 not tried 0% in round 3
c [elim-12] transition to [ all 1 rem 1 ] state
c [elim-12] eliminated 1187 = 3% variables out of 38971 scheduled
c [bca-12] limit of 10000000 steps and 490008 added (scaled 2)
c [bca-12] 62836 out of 75570 literals actually usable 83%
c [bca-12] added 105 blocked clauses in 161453 steps
c [sweep-12] limit 4707071 penalty 0 = 0 + 0
c [sweep-12-1] 1907 pos 9.3% + 18490 neg 90.7% = 20397 sched 54.0% ret 17387
c [sweep-12-1] 4789919 steps 172 queries 1658.42 avg class size
c [sweep-12-1] 1953 decisions 156 SAT calls 76.54 avg env size
c [sweep-12-1] 19565 variables remain 52% (18182 retained 48%)
c [decomp-40] removed 114 variables
c [sweep-12-1] removed 114 vars (0 failed, 22 eqs, 31 impls)
c [sweep-12] removed 114 vars in TOTAL (1 rounds, 171 queries)
c [phase-count-16] 243304 negative 99.6% of 244179 except 875 0.4%
c [phase-count-16] 177899 positive 72.9% of 244179 except 66280 27.1%
c [phase-count-16] skipping relative phase luck test
c [phase-16] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-16] sorted 7877 enqueued variables after 47000 conflicts
c [score-dist-16] active 29793 (79%), one 0 (0%), zero 7877 (21%)
c [score-dist-16] max exp 510, different 188 (37%)
c [score-dist-16] median active exp 490, avg 470.7
c [simplification-16] removed 1664 variables 4.2% (37670 remain 18%)
c [simplification-16] removed 11844 irredundant clauses 4.6% (244179 remain 20%)
c [simplification-16] maximum reduction of 5% = max (4%, 5%)
c [simplification-16] large reduction 5% >= 5% limit
c [simplification-16] next conflict interval 2000 = 2000/1
c [simplification-16] penalized conflict interval 2000 = 1 * 2000
c [simplification-16] hard conflict limit 59000 (soft 49000 + delta 10000)
c [simplification-16] new conflict limit 49000 (hard 59000)
c 
c [simplification-17] limit 49000 conflicts (hard 59000) hit after 49000 conflicts
c [quatres-11] found 24985 quaternary clauses 69% in total
c [quatres-11-2] added 15 quaternary resolvents
c [ternres-13] limit 16154339 with penalty 0 = 0 + 0
c [ternres-13] all 37670 free variables schedulable
c [ternres-13] 508 ternary resolvents (1 bin, 507 trn)
c [ternres-13] fully completed ternary resolution
c [basicprobe-6] limit 80771695 penalty 0 = 0 + 0
c [basicprobe-6-0] 3146 probes remain 9% after last round
c [basicprobe-6-0] 784 units = 764 failed (97%) + 20 lifted (3%)
c [basicprobe-6-0] removed 1263 variables, found 122206 hbrs
c [bate-4] eliminated 788 asymmetric tautologies during probing
c [unhide-17] limit 3230867 with penalty 0 = 0 + 0
c [unhide-17-22] 10 units, 78 failed, 32299 tauts, 0 hbrs, 87486 literals
c [transred-13] limit 2000000 with penalty 0 = 0 + 0
c [transred-13] removed 444 transitive binary clauses
c [elim-13] no untried remaining variables left
c [elim-13] scheduled 36264 variables 100%
c [elim-13] almost no limit of 100000000000 steps
c [elim-13] rescheduling of touched variables disabled
c [elim-13-1] eliminated 1006 variables 3% in round 1 in 20625305 steps
c [elim-13-1] backward subsumption/strengthening limit 20625300
c [elim-13-1-1] backward checking 4986 touched variables 14%
c [elim-13-1-1] fully completed backward checking in 1 rounds
c [elim-13-1] subsumed 43 and strengthened 94 clauses in 1248571 steps
c [elim-13-1] rescheduled 300 variables 1% by backward subsumption
c [elim-13-2] eliminated 24 variables 0% in round 2 in 614623 steps
c [elim-13-2] backward subsumption/strengthening limit 614600
c [elim-13-2-1] backward checking 345 touched variables 1%
c [elim-13-2-1] fully completed backward checking in 1 rounds
c [elim-13-2] subsumed 27 and strengthened 16 clauses in 264872 steps
c [elim-13-2] rescheduled 57 variables 0% by backward subsumption
c [elim-13-3] eliminated 5 variables 0% in round 3 in 120019 steps
c [elim-13-3] backward subsumption/strengthening limit 120000
c [elim-13-3-1] backward checking 37 touched variables 0%
c [elim-13-3-1] fully completed backward checking in 1 rounds
c [elim-13-3] subsumed 7 and strengthened 0 clauses in 53350 steps
c [elim-13] incomplete 14 not tried 0% in round 3
c [elim-13] transition to [ all 1 rem 1 ] state
c [elim-13] eliminated 1035 = 3% variables out of 36264 scheduled
c [bca-13] limit of 10000000 steps and 450081 added (scaled 2)
c [bca-13] 58233 out of 70460 literals actually usable 83%
c [bca-13] added 70 blocked clauses in 147358 steps
c [sweep-13] limit 4846301 penalty 0 = 0 + 0
c [sweep-13-1] 1779 pos 9.6% + 16679 neg 90.4% = 18458 sched 52.4% ret 16771
c [sweep-13-1] 4866888 steps 147 queries 1259.71 avg class size
c [sweep-13-1] 1750 decisions 135 SAT calls 87.37 avg env size
c [sweep-13-1] 17601 variables remain 50% (17471 retained 50%)
c [decomp-42] removed 215 variables
c [sweep-13-1] removed 215 vars (0 failed, 14 eqs, 20 impls)
c [sweep-13] removed 215 vars in TOTAL (1 rounds, 146 queries)
c [phase-count-17] 222890 negative 99.6% of 223739 except 849 0.4%
c [phase-count-17] 161604 positive 72.2% of 223739 except 62135 27.8%
c [phase-count-17] skipping relative phase luck test
c [phase-17] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-17] sorted 6626 enqueued variables after 49000 conflicts
c [score-dist-17] active 28388 (81%), one 0 (0%), zero 6626 (19%)
c [score-dist-17] max exp 509, different 193 (38%)
c [score-dist-17] median active exp 490, avg 469.4
c [simplification-17] removed 2656 variables 7.1% (35014 remain 16%)
c [simplification-17] removed 20440 irredundant clauses 8.4% (223739 remain 19%)
c [simplification-17] maximum reduction of 8% = max (7%, 8%)
c [simplification-17] large reduction 8% >= 5% limit
c [simplification-17] next conflict interval 2000 = 2000/1
c [simplification-17] penalized conflict interval 2000 = 1 * 2000
c [simplification-17] hard conflict limit 61000 (soft 51000 + delta 10000)
c [simplification-17] new conflict limit 51000 (hard 61000)
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  125.4   35013   223739     49421   12203   3576 303717  243   442   43  55%     26  251  229   99  230%
c i  125.4   35012   223739     49422   12203   3576 303717  242   442   43  55%     26  251  228   99  230%
c i  125.8   34995   223739     49857   12560   3579 303724  247   450   43  55%     16  257  288  100  287%
c i  126.7   34991   223739     50858   13254   3606 303737  259   460   44  56%      8  264  337  103  326%
c 
c [simplification-18] limit 51010 conflicts (hard 61000) hit after 51012 conflicts
c [quatres-12] found 22320 quaternary clauses 69% in total
c [quatres-12-2] added 3 single-self-subsuming ternary resolvents
c [quatres-12-2] added 7 quaternary resolvents
c [ternres-14] limit 16649366 with penalty 0 = 0 + 0
c [ternres-14] all 34940 free variables schedulable
c [ternres-14] 543 ternary resolvents (0 bin, 543 trn)
c [ternres-14] fully completed ternary resolution
c [decomp-43] removed 78 variables
c [simpleprobe-7] all 34936 free variables schedulable
c [simpleprobe-7] limit 66597464 penalty 0 = 0 + 0
c [decomp-44] removed 344 variables
c [simpleprobe-7] fully completed simple probing
c [simpleprobe-7] removed 344 variables, found 58996 hbrs, 150 units
c [unhide-18] limit 3329873 with penalty 0 = 0 + 0
c [unhide-18-24] 1 units, 39 failed, 47403 tauts, 0 hbrs, 165136 literals
c [transred-14] limit 2000000 with penalty 0 = 0 + 0
c [transred-14] removed 606 transitive binary clauses
c [transred-14] found 1 units
c [elim-14] no untried remaining variables left
c [elim-14] scheduled 34557 variables 100%
c [elim-14] limit of 332987320 steps penalty 0 = 0 + 0
c [elim-14] rescheduling of touched variables disabled
c [elim-14-1] eliminated 405 variables 1% in round 1 in 20036712 steps
c [elim-14-1] backward subsumption/strengthening limit 20036700
c [elim-14-1-1] backward checking 2361 touched variables 7%
c [elim-14-1-1] fully completed backward checking in 1 rounds
c [elim-14-1] subsumed 15 and strengthened 41 clauses in 696548 steps
c [elim-14-1] rescheduled 144 variables 0% by backward subsumption
c [elim-14-2] eliminated 10 variables 0% in round 2 in 741574 steps
c [elim-14-2] backward subsumption/strengthening limit 741500
c [elim-14-2-1] backward checking 119 touched variables 0%
c [elim-14-2-1] fully completed backward checking in 1 rounds
c [elim-14-2] subsumed 0 and strengthened 3 clauses in 85474 steps
c [elim-14-2] rescheduled 10 variables 0% by backward subsumption
c [elim-14-3] no variable eliminated in round 3 in 5482 steps
c [elim-14] fully completed in 3 rounds
c [elim-14] transition to [ all 0 rem 0 ] state
c [elim-14] eliminated 416 = 1% variables out of 34557 scheduled
c [bca-14] limit of 10000000 steps and 433372 added (scaled 2)
c [bca-14] 55977 out of 68284 literals actually usable 82%
c [bca-14] added 37 blocked clauses in 141577 steps
c [sweep-14] limit 4994809 penalty 0 = 0 + 0
c [sweep-14-1] 1902 pos 11.0% + 15332 neg 89.0% = 17234 sched 50.5% ret 16907
c [sweep-14-1] 5015472 steps 186 queries 1242.83 avg class size
c [sweep-14-1] 1856 decisions 165 SAT calls 79.97 avg env size
c [sweep-14-1] 16428 variables remain 48% (17677 retained 52%)
c [decomp-45] removed 96 variables
c [sweep-14-1] removed 96 vars (0 failed, 23 eqs, 36 impls)
c [sweep-14] removed 96 vars in TOTAL (1 rounds, 185 queries)
c [phase-count-18] 215091 negative 99.6% of 215906 except 815 0.4%
c [phase-count-18] 154668 positive 71.6% of 215906 except 61238 28.4%
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 6094 enqueued variables after 51012 conflicts
c [score-dist-18] active 27951 (82%), one 0 (0%), zero 6094 (18%)
c [score-dist-18] max exp 509, different 200 (39%)
c [score-dist-18] median active exp 494, avg 470.3
c [simplification-18] removed 895 variables 2.6% (34045 remain 16%)
c [simplification-18] removed 7833 irredundant clauses 3.5% (215906 remain 18%)
c [simplification-18] maximum reduction of 4% = max (3%, 4%)
c [simplification-18] geometric conflict interval increment 4000 = 20000 / 5
c [simplification-18] new conflict interval 17000
c [simplification-18] penalized conflict interval 17000 = 1 * 17000
c [simplification-18] hard conflict limit 78012 (soft 68012 + delta 10000)
c [simplification-18] new conflict limit 68012 (hard 78012)
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  131.2   34044   215906     51433   12474   3814 308233  269   477   43  56%      4  279  318  105  301%
c i  131.9   34041   215906     52372   13197   3819 308262  259   484   43  54%      3  281  194  107  181%
c i  132.3   34029   215906     52934   13570   3823 308269  271   493   44  55%      1  288  378  109  347%
c i  135.2   34028   215906     56633   15909   3859 308289  224   388   49  58%     36  170  153  114  134%
c i  137.1   34027   215906     59019   17268   3863 308300  243   383   52  63%     20  158  294  119  246%
c i  138.2   34023   215906     60249   17935   3910 308320  251   388   52  65%      9  161  234  122  192%
c i  140.6   34020   215906     63495   19715   3941 308327  219   335   62  65%     28  102  172  126  136%
c i  141.1   34019   215906     64218   20235   3945 308328  207   329   63  63%     13   95  126  126  100%
c 
c [simplification-19] limit 68012 conflicts (hard 78012) hit after 68012 conflicts
c [quatres-13] found 21419 quaternary clauses 67% in total
c [quatres-13-2] added 1 single-self-subsuming ternary resolvents
c [quatres-13-2] added 13 quaternary resolvents
c [ternres-15] limit 20240628 with penalty 0 = 0 + 0
c [ternres-15] all 33969 free variables schedulable
c [ternres-15] 300 ternary resolvents (1 bin, 299 trn)
c [ternres-15] fully completed ternary resolution
c [gauss-5] limit 253007 penalty 4 = 4 + 0
c [gauss-5] extracted 12 xors of average arity 2.6
c [gauss-5] connected 31 occurrences of 31 variables (average 1.0)
c [gauss-5] limit 253007 penalty 4 = 4 + 0
c [gauss-5] fully completed
c [gauss-5] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-46] removed 35 variables
c [treelook-7] limit 2024062 penalty 0 = 0 + 0 boost 1
c [treelook-7] scheduled 48249 literals 71%
c [treelook-7] scheduling used 909897 steps
c [treelook-7] scheduled completely
c [treelook-7] limit 2024062 penalty 0 = 0 + 0 boost 1
c [treelook-7] used 2032562 steps
c [treelook-7] 48188 literals remain 71%
c [treelook-7] 7229 variables remain to probed next time 21%
c [treelook-7] removed 1 variables, found 19842 hbrs
c [unhide-19] limit 4048125 with penalty 0 = 0 + 0
c [unhide-19-27] 3 units, 46 failed, 29548 tauts, 0 hbrs, 226807 literals
c [transred-15] limit 2000000 with penalty 0 = 0 + 0
c [transred-15] removed 475 transitive binary clauses
c [elim-15] scheduling all variables this time
c [elim-15] scheduled 33890 variables 100%
c [elim-15] limit of 404812574 steps penalty 0 = 0 + 0
c [elim-15] rescheduling of touched variables disabled
c [elim-15-1] eliminated 330 variables 1% in round 1 in 19826836 steps
c [elim-15-1] backward subsumption/strengthening limit 19826800
c [elim-15-1-1] backward checking 1588 touched variables 5%
c [elim-15-1-1] fully completed backward checking in 1 rounds
c [elim-15-1] subsumed 4 and strengthened 19 clauses in 424341 steps
c [elim-15-1] rescheduled 58 variables 0% by backward subsumption
c [elim-15-2] eliminated 3 variables 0% in round 2 in 44020 steps
c [elim-15-2] backward subsumption/strengthening limit 44000
c [elim-15-2-1] backward checking 33 touched variables 0%
c [elim-15-2-1] incomplete backward checking 0 remain 0%
c [elim-15-2] subsumed 6 and strengthened 0 clauses in 44001 steps
c [elim-15-2] rescheduled 12 variables 0% by backward subsumption
c [elim-15-3] no variable eliminated in round 3 in 627800 steps
c [elim-15] fully completed in 3 rounds
c [elim-15] transition to [ all 0 rem 0 ] state
c [elim-15] eliminated 333 = 1% variables out of 33890 scheduled
c [elim-15] 333 < 1/100 * 33890 = 338 considered unsuccessful
c [bca-15] limit of 10000000 steps and 425590 added (scaled 2)
c [bca-15] 53528 out of 67116 literals actually usable 80%
c [bca-15] added 34 blocked clauses in 143234 steps
c [sweep-15] limit 6072188 penalty 0 = 0 + 0
c [sweep-15-1] 1905 pos 11.8% + 14263 neg 88.2% = 16168 sched 48.2% ret 17389
c [sweep-15-1] 6081851 steps 154 queries 1061.84 avg class size
c [sweep-15-1] 2485 decisions 142 SAT calls 109.64 avg env size
c [sweep-15-1] 15471 variables remain 46% (18086 retained 54%)
c [decomp-48] removed 40 variables
c [sweep-15-1] removed 40 vars (0 failed, 13 eqs, 21 impls)
c [sweep-15] removed 40 vars in TOTAL (1 rounds, 153 queries)
c [phase-count-19] 211405 negative 99.6% of 212214 except 809 0.4%
c [phase-count-19] 152104 positive 71.7% of 212214 except 60110 28.3%
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 5808 enqueued variables after 68012 conflicts
c [score-dist-19] active 27709 (83%), one 0 (0%), zero 5808 (17%)
c [score-dist-19] max exp 510, different 266 (52%)
c [score-dist-19] median active exp 473, avg 446.1
c [simplification-19] removed 452 variables 1.3% (33517 remain 16%)
c [simplification-19] removed 3692 irredundant clauses 1.7% (212214 remain 18%)
c [simplification-19] maximum reduction of 2% = max (1%, 2%)
c [simplification-19] geometric conflict interval increment 6666 = 20000 / 3
c [simplification-19] new conflict interval 23666
c [simplification-19] penalized conflict interval 23666 = 1 * 23666
c [simplification-19] hard conflict limit 103511 (soft 91678 + delta 11833)
c [simplification-19] new conflict limit 91678 (hard 103511)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i  155.0   33516   212214     75976   26069   4071 294698   92   142   58  65%    147  -90   59  122   48%
c i  155.3   33514   212214     76405   26443   4074 294700  105   168   58  63%     90  -63  198  123  161%
c i  163.9   33509   212214     89737   35178   4114 294763   92   147   71  63%    157  -75   36  121   30%
c i  163.9   33508   212214     89779   35217   4114 294763   92   148   71  62%    149  -74   35  121   29%
c i  163.9   33507   212214     89799   35233   4114 294763   92   148   71  62%    145  -74   36  121   30%
c i  163.9   33506   212214     89808   35237   4114 294763   92   148   71  62%    144  -74   38  121   31%
c i  163.9   33505   212214     89825   35252   4114 294764   91   149   71  61%    141  -73   38  121   32%
c i  164.0   33504   212214     89957   35369   4117 294769   89   154   71  58%    119  -68   33  120   28%
c i  164.1   33500   212214     90231   35560   4122 294769   91   160   71  57%     83  -62   82  120   68%
c i  164.2   33499   212214     90233   35561   4122 294769   91   160   71  57%     83  -62   82  120   69%
c i  164.7   33490   212214     91111   36225   4139 294788   98   180   71  55%     18  -41  125  120  104%
c i  164.8   33489   212214     91209   36284   4139 294788   99   180   71  55%     13  -41  128  120  106%
c i  164.8   33484   212214     91210   36284   4139 294788   99   179   71  55%     13  -41  127  120  106%
c i  165.1   33479   212214     91825   36704   4139 294790  100   176   71  57%     -7  -44  100  120   83%
c 
c [simplification-20] limit 91694 conflicts (hard 103511) hit after 103511 conflicts
c [quatres-14] found 21533 quaternary clauses 65% in total
c [quatres-14-2] added 5 single-self-subsuming ternary resolvents
c [quatres-14-2] added 6 quaternary resolvents
c [ternres-16] limit 27270215 with penalty 0 = 0 + 0
c [ternres-16] all 33468 free variables schedulable
c [ternres-16] 163 ternary resolvents (1 bin, 162 trn)
c [ternres-16] fully completed ternary resolution
c [decomp-49] removed 55 variables
c [basicprobe-7] limit 136351077 penalty 0 = 0 + 0
c [basicprobe-7-0] 3457 sched 11%, 497 failed, 16 lifted, 64250 hbrs
c [decomp-50] removed 915 variables
c [basicprobe-7-1] 4709 probes remain 15% after last round
c [basicprobe-7-1] 726 units = 705 failed (97%) + 21 lifted (3%)
c [basicprobe-7-1] removed 1359 variables, found 113239 hbrs
c [bate-5] eliminated 313 asymmetric tautologies during probing
c [unhide-20] limit 2727021 with penalty 1 = 0 + 1
c [unhide-20-29] 1 units, 53 failed, 33251 tauts, 0 hbrs, 311944 literals
c [transred-16] limit 2000000 with penalty 0 = 0 + 0
c [transred-16] removed 512 transitive binary clauses
c [transred-16] found 2 units
c [block-6] scheduling all variables this time
c [block-6] scheduled 32075 variables 100%
c [block-6] limit of 17043884 steps penalty 4 = 4 + 0
c [block-6] fully completed
c [block-6] transition to [ all 0 rem 0 ] state
c [block-6] eliminated 112 blocked clauses
c [block-6] 112 < 1/100 * 197696 = 1976 considered unsuccessful
c [cce-8] boosting limit by 10
c [cce-8] limit of 170438846 steps penalty 3 = 3 + 0
c [cce-8-1] eliminated 1 clauses out of 1 (100%) of length 70
c [cce-8-1] eliminated 2 clauses out of 2 (100%) of length 69
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 68
c [cce-8-1] eliminated 2 clauses out of 2 (100%) of length 67
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 66
c [cce-8-1] eliminated 2 clauses out of 2 (100%) of length 65
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 64
c [cce-8-1] eliminated 2 clauses out of 2 (100%) of length 63
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 62
c [cce-8-1] eliminated 2 clauses out of 2 (100%) of length 61
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 60
c [cce-8-1] eliminated 2 clauses out of 2 (100%) of length 59
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 58
c [cce-8-1] eliminated 2 clauses out of 2 (100%) of length 57
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 56
c [cce-8-1] eliminated 2 clauses out of 2 (100%) of length 55
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 54
c [cce-8-1] eliminated 2 clauses out of 2 (100%) of length 53
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 52
c [cce-8-1] eliminated 2 clauses out of 2 (100%) of length 51
c [cce-8-1] eliminated 1 clauses out of 3 (33%) of length 50
c [cce-8-1] eliminated 3 clauses out of 3 (100%) of length 49
c [cce-8-1] eliminated 3 clauses out of 4 (75%) of length 48
c [cce-8-1] eliminated 3 clauses out of 4 (75%) of length 47
c [cce-8-1] eliminated 3 clauses out of 4 (75%) of length 46
c [cce-8-1] eliminated 3 clauses out of 3 (100%) of length 45
c [cce-8-1] eliminated 2 clauses out of 4 (50%) of length 44
c [cce-8-1] eliminated 4 clauses out of 4 (100%) of length 43
c [cce-8-1] eliminated 2 clauses out of 4 (50%) of length 42
c [cce-8-1] eliminated 4 clauses out of 4 (100%) of length 41
c [cce-8-1] eliminated 3 clauses out of 5 (60%) of length 40
c [cce-8-1] eliminated 3 clauses out of 4 (75%) of length 39
c [cce-8-1] eliminated 3 clauses out of 5 (60%) of length 38
c [cce-8-1] eliminated 4 clauses out of 4 (100%) of length 37
c [cce-8-1] eliminated 3 clauses out of 5 (60%) of length 36
c [cce-8-1] eliminated 4 clauses out of 5 (80%) of length 35
c [cce-8-1] eliminated 4 clauses out of 5 (80%) of length 34
c [cce-8-1] eliminated 3 clauses out of 4 (75%) of length 33
c [cce-8-1] eliminated 3 clauses out of 4 (75%) of length 32
c [cce-8-1] eliminated 3 clauses out of 4 (75%) of length 31
c [cce-8-1] eliminated 3 clauses out of 4 (75%) of length 30
c [cce-8-1] eliminated 3 clauses out of 5 (60%) of length 29
c [cce-8-1] eliminated 3 clauses out of 5 (60%) of length 28
c [cce-8-1] eliminated 3 clauses out of 5 (60%) of length 27
c [cce-8-1] eliminated 3 clauses out of 5 (60%) of length 26
c [cce-8-1] eliminated 6 clauses out of 8 (75%) of length 25
c [cce-8-1] eliminated 4 clauses out of 8 (50%) of length 24
c [cce-8-1] eliminated 5 clauses out of 6 (83%) of length 23
c [cce-8-1] eliminated 4 clauses out of 7 (57%) of length 22
c [cce-8-1] eliminated 2 clauses out of 3 (67%) of length 21
c [cce-8-1] eliminated 3 clauses out of 5 (60%) of length 20
c [cce-8-1] eliminated 3 clauses out of 7 (43%) of length 19
c [cce-8-1] eliminated 4 clauses out of 4 (100%) of length 18
c [cce-8-1] eliminated 3 clauses out of 7 (43%) of length 17
c [cce-8-1] eliminated 3 clauses out of 6 (50%) of length 16
c [cce-8-1] eliminated 3 clauses out of 10 (30%) of length 15
c [cce-8-1] eliminated 4 clauses out of 10 (40%) of length 14
c [cce-8-1] eliminated 6 clauses out of 11 (55%) of length 13
c [cce-8-1] eliminated 8 clauses out of 16 (50%) of length 12
c [cce-8-1] eliminated 8 clauses out of 18 (44%) of length 11
c [cce-8-1] eliminated 7 clauses out of 13 (54%) of length 10
c [cce-8-1] eliminated 10 clauses out of 18 (56%) of length 9
c [cce-8-1] eliminated 9 clauses out of 21 (43%) of length 8
c [cce-8-1] eliminated 13 clauses out of 30 (43%) of length 7
c [cce-8-1] eliminated 17 clauses out of 944 (2%) of length 6
c [cce-8-1] eliminated 711 clauses out of 7168 (10%) of length 5
c [cce-8-1] eliminated 6519 clauses out of 17775 (37%) of length 4
c [cce-8-1] completed large round (ATE)
c [cce-8-1] eliminated 7458 large clauses in 147922970 steps
c [cce-8-1] allowing another 73961485 steps for small clauses
c [cce-8-1] scheduling 157892 clauses = 103650 binary + 54242 ternary
c [cce-8-1] tried to eliminate 11674 small clauses 7%
c [cce-8-1] eliminated 1812 binary clauses 2%
c [cce-8-1] eliminated 680 ternary clauses 1%
c [cce-8-1] eliminated 2492 small clauses 2%
c [cce-8-1] eliminated 2492 small clauses in 170438846 steps
c [cce-8-1] incomplete small round (ATE)
c [cce-8-1] eliminated 9950 covered clauses in round 1
c [cce-8] eliminated 9950 covered clauses in TOTAL during 1 rounds
c [bca-16] limit of 10000000 steps and 376209 added (scaled 2)
c [bca-16] 49174 out of 64148 literals actually usable 77%
c [bca-16] added 34 blocked clauses in 150949 steps
c [sweep-16] limit 8181064 penalty 0 = 0 + 0
c [sweep-16-1] 1730 pos 11.6% + 13126 neg 88.4% = 14856 sched 46.3% ret 17217
c [sweep-16-1] 8234959 steps 257 queries 686.30 avg class size
c [sweep-16-1] 4574 decisions 230 SAT calls 95.62 avg env size
c [sweep-16-1] 13632 variables remain 43% (18358 retained 57%)
c [decomp-51] removed 246 variables
c [sweep-16-1] removed 246 vars (0 failed, 31 eqs, 48 impls)
c [sweep-16] removed 246 vars in TOTAL (1 rounds, 256 queries)
c [sort-queue-20] sorted 4830 enqueued variables after 103511 conflicts
c [score-dist-20] active 26997 (85%), one 0 (0%), zero 4830 (15%)
c [score-dist-20] max exp 510, different 384 (75%)
c [score-dist-20] median active exp 487, avg 415.5
c [simplification-20] removed 1641 variables 4.9% (31827 remain 15%)
c [simplification-20] removed 25240 irredundant clauses 11.9% (186974 remain 16%)
c [simplification-20] maximum reduction of 12% = max (5%, 12%)
c [simplification-20] large reduction 12% >= 5% limit
c [simplification-20] next conflict interval 2000 = 2000/1
c [simplification-20] penalized conflict interval 2000 = 1 * 2000
c [simplification-20] hard conflict limit 115511 (soft 105511 + delta 10000)
c [simplification-20] new conflict limit 105511 (hard 115511)
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  188.0   31826   186974    103769   43258   4791 362581  114   171   84  67%    126  -46  123  122  101%
c i  192.7   31825   186974    109612   47002   4803 362625  124   179   84  69%     30  -35   42  123   35%
c i  193.8   31823   186974    111514   48567   4807 362632   91   135   84  68%    -18  -77   47  120   40%
c i  195.1   31801   186974    113684   50250   4864 362633   73   118   84  62%    -22  -91   33  118   28%
c 
c [simplification-21] limit 105511 conflicts (hard 115511) hit after 115512 conflicts
c [quatres-15] found 11889 quaternary clauses 53% in total
c [quatres-15-1] removed 2 duplicate quaternary clauses
c [quatres-15-2] added 3 quaternary resolvents
c [ternres-17] limit 29574854 with penalty 0 = 0 + 0
c [ternres-17] all 31798 free variables schedulable
c [ternres-17] 216 ternary resolvents (1 bin, 215 trn)
c [ternres-17] fully completed ternary resolution
c [card-6] limit 924214 penalty 4 = 4 + 0
c [card-6] found 1165 at-most-one constraints of average size 3.8
c [card-6] no at-most-two constraint found
c [card-6] using previous limit 924214 for elimination
c [card-6] 1165 out of 1165 constraints (100%) meet size limits
c [card-6] no units found
c [card-6] no at-most-one constraints generated
c [decomp-52] removed 36 variables
c [simpleprobe-8] all 31791 free variables schedulable
c [simpleprobe-8] limit 118299417 penalty 0 = 0 + 0
c [decomp-53] removed 120 variables
c [simpleprobe-8] fully completed simple probing
c [simpleprobe-8] removed 120 variables, found 65043 hbrs, 47 units
c [unhide-21] limit 2957485 with penalty 1 = 0 + 1
c [unhide-21-31] 1 units, 47 failed, 52395 tauts, 0 hbrs, 511920 literals
c [transred-17] limit 2000000 with penalty 0 = 0 + 0
c [transred-17] removed 636 transitive binary clauses
c [elim-16] scheduling all variables this time
c [elim-16] scheduled 31586 variables 100%
c [elim-16] limit of 295748543 steps penalty 1 = 1 + 0
c [elim-16] rescheduling of touched variables disabled
c [elim-16-1] eliminated 1997 variables 6% in round 1 in 15284346 steps
c [elim-16-1] backward subsumption/strengthening limit 15284300
c [elim-16-1-1] backward checking 8364 touched variables 26%
c [elim-16-1-1] fully completed backward checking in 1 rounds
c [elim-16-1] subsumed 38 and strengthened 180 clauses in 1422686 steps
c [elim-16-1] rescheduled 559 variables 2% by backward subsumption
c [elim-16-2] eliminated 34 variables 0% in round 2 in 612702 steps
c [elim-16-2] backward subsumption/strengthening limit 612700
c [elim-16-2-1] backward checking 328 touched variables 1%
c [elim-16-2-1] fully completed backward checking in 1 rounds
c [elim-16-2] subsumed 19 and strengthened 11 clauses in 139551 steps
c [elim-16-2] rescheduled 52 variables 0% by backward subsumption
c [elim-16-3] eliminated 2 variables 0% in round 3 in 90523 steps
c [elim-16-3] backward subsumption/strengthening limit 90500
c [elim-16-3-1] backward checking 39 touched variables 0%
c [elim-16-3-1] fully completed backward checking in 1 rounds
c [elim-16-3] subsumed 5 and strengthened 1 clauses in 54015 steps
c [elim-16] incomplete 12 not tried 0% in round 3
c [elim-16] transition to [ all 1 rem 1 ] state
c [elim-16] eliminated 2033 = 6% variables out of 31586 scheduled
c [bca-17] limit of 10000000 steps and 361016 added (scaled 2)
c [bca-17] 45584 out of 59108 literals actually usable 77%
c [bca-17] added 43 blocked clauses in 132768 steps
c [sweep-17] limit 8872456 penalty 0 = 0 + 0
c [sweep-17-1] 1422 pos 11.3% + 11166 neg 88.7% = 12588 sched 42.6% ret 16965
c [sweep-17-1] 8885668 steps 279 queries 490.62 avg class size
c [sweep-17-1] 3710 decisions 270 SAT calls 92.82 avg env size
c [sweep-17-1] 11356 variables remain 38% (18173 retained 62%)
c [decomp-54] removed 44 variables
c [sweep-17-1] removed 44 vars (0 failed, 15 eqs, 44 impls)
c [sweep-17] removed 44 vars in TOTAL (1 rounds, 278 queries)
c [sort-queue-21] sorted 4044 enqueued variables after 115512 conflicts
c [score-dist-21] active 25465 (86%), one 0 (0%), zero 4044 (14%)
c [score-dist-21] max exp 510, different 410 (80%)
c [score-dist-21] median active exp 490, avg 413.6
c [simplification-21] removed 2289 variables 7.2% (29509 remain 14%)
c [simplification-21] removed 7203 irredundant clauses 3.9% (179771 remain 15%)
c [simplification-21] maximum reduction of 7% = max (7%, 4%)
c [simplification-21] large reduction 7% >= 5% limit
c [simplification-21] next conflict interval 2000 = 2000/1
c [simplification-21] penalized conflict interval 2000 = 1 * 2000
c [simplification-21] hard conflict limit 127512 (soft 117512 + delta 10000)
c [simplification-21] new conflict limit 117512 (hard 127512)
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  204.6   29508   179770    118049   33564   4373 335636   75   129   58  58%      9  -75   41  115   36%
c i  204.6   29507   179770    118172   33656   4374 335638   73   130   58  56%      3  -74   38  115   33%
c 
c [simplification-22] limit 117512 conflicts (hard 127512) hit after 127512 conflicts
c [quatres-16] found 12569 quaternary clauses 53% in total
c [quatres-16-1] removed 1 duplicate quaternary clauses
c [quatres-16-2] added 57 quaternary resolvents
c [ternres-18] limit 31520149 with penalty 0 = 0 + 0
c [ternres-18] all 29507 free variables schedulable
c [ternres-18] 953 ternary resolvents (0 bin, 953 trn)
c [ternres-18] fully completed ternary resolution
c [decomp-55] removed 8 variables
c [treelook-8] limit 3152014 penalty 0 = 0 + 0 boost 1
c [treelook-8] scheduled 39578 literals 67%
c [treelook-8] scheduling used 847181 steps
c [treelook-8] scheduled completely
c [treelook-8] limit 3152014 penalty 0 = 0 + 0 boost 1
c [treelook-8] used 3198847 steps
c [treelook-8] 39501 literals remain 67%
c [treelook-8] 6120 variables remain to probed next time 21%
c [decomp-56] removed 1 variables
c [treelook-8] removed 1 variables, found 20754 hbrs
c [unhide-22] limit 6304029 with penalty 0 = 0 + 0
c [unhide-22-35] 2 units, 8 failed, 53511 tauts, 0 hbrs, 169312 literals
c [transred-18] limit 2000000 with penalty 0 = 0 + 0
c [transred-18] removed 620 transitive binary clauses
c [cce-9] limit of 39400187 steps penalty 2 = 2 + 0
c [cce-9-1] eliminated 1 clauses out of 1 (100%) of length 58
c [cce-9-1] eliminated 1 clauses out of 2 (50%) of length 57
c [cce-9-1] eliminated 2 clauses out of 2 (100%) of length 56
c [cce-9-1] eliminated 1 clauses out of 3 (33%) of length 55
c [cce-9-1] eliminated 2 clauses out of 3 (67%) of length 54
c [cce-9-1] eliminated 1 clauses out of 2 (50%) of length 53
c [cce-9-1] eliminated 2 clauses out of 3 (67%) of length 52
c [cce-9-1] eliminated 1 clauses out of 3 (33%) of length 51
c [cce-9-1] eliminated 4 clauses out of 5 (80%) of length 50
c [cce-9-1] eliminated 1 clauses out of 2 (50%) of length 49
c [cce-9-1] eliminated 1 clauses out of 3 (33%) of length 48
c [cce-9-1] eliminated 2 clauses out of 3 (67%) of length 47
c [cce-9-1] eliminated 2 clauses out of 3 (67%) of length 46
c [cce-9-1] eliminated 2 clauses out of 2 (100%) of length 45
c [cce-9-1] eliminated 1 clauses out of 3 (33%) of length 44
c [cce-9-1] eliminated 2 clauses out of 3 (67%) of length 43
c [cce-9-1] eliminated 1 clauses out of 3 (33%) of length 42
c [cce-9-1] eliminated 2 clauses out of 3 (67%) of length 41
c [cce-9-1] eliminated 1 clauses out of 4 (25%) of length 40
c [cce-9-1] eliminated 2 clauses out of 3 (67%) of length 39
c [cce-9-1] eliminated 1 clauses out of 4 (25%) of length 38
c [cce-9-1] eliminated 3 clauses out of 3 (100%) of length 37
c [cce-9-1] eliminated 1 clauses out of 5 (20%) of length 36
c [cce-9-1] eliminated 2 clauses out of 3 (67%) of length 35
c [cce-9-1] eliminated 1 clauses out of 3 (33%) of length 34
c [cce-9-1] eliminated 2 clauses out of 3 (67%) of length 33
c [cce-9-1] eliminated 1 clauses out of 3 (33%) of length 32
c [cce-9-1] eliminated 2 clauses out of 3 (67%) of length 31
c [cce-9-1] eliminated 1 clauses out of 3 (33%) of length 30
c [cce-9-1] eliminated 2 clauses out of 4 (50%) of length 29
c [cce-9-1] eliminated 2 clauses out of 6 (33%) of length 28
c [cce-9-1] eliminated 4 clauses out of 6 (67%) of length 27
c [cce-9-1] eliminated 1 clauses out of 4 (25%) of length 26
c [cce-9-1] eliminated 2 clauses out of 4 (50%) of length 25
c [cce-9-1] eliminated 1 clauses out of 5 (20%) of length 24
c [cce-9-1] eliminated 2 clauses out of 5 (40%) of length 23
c [cce-9-1] eliminated 1 clauses out of 4 (25%) of length 22
c [cce-9-1] eliminated 2 clauses out of 4 (50%) of length 21
c [cce-9-1] eliminated 1 clauses out of 3 (33%) of length 20
c [cce-9-1] eliminated 2 clauses out of 7 (29%) of length 19
c [cce-9-1] eliminated 1 clauses out of 3 (33%) of length 18
c [cce-9-1] eliminated 3 clauses out of 6 (50%) of length 17
c [cce-9-1] eliminated 4 clauses out of 10 (40%) of length 16
c [cce-9-1] eliminated 7 clauses out of 15 (47%) of length 15
c [cce-9-1] eliminated 9 clauses out of 16 (56%) of length 14
c [cce-9-1] eliminated 7 clauses out of 16 (44%) of length 13
c [cce-9-1] eliminated 6 clauses out of 13 (46%) of length 12
c [cce-9-1] eliminated 8 clauses out of 19 (42%) of length 11
c [cce-9-1] eliminated 8 clauses out of 19 (42%) of length 10
c [cce-9-1] eliminated 9 clauses out of 21 (43%) of length 9
c [cce-9-1] eliminated 10 clauses out of 28 (36%) of length 8
c [cce-9-1] eliminated 14 clauses out of 41 (34%) of length 7
c [cce-9-1] eliminated 26 clauses out of 998 (3%) of length 6
c [cce-9-1] eliminated 51 clauses out of 6540 (1%) of length 5
c [cce-9-1] incomplete large round (ACCE)
c [cce-9-1] eliminated 229 large clauses in 39400197 steps
c [cce-9-1] allowing another 19700098 steps for small clauses
c [cce-9-1] scheduling 145855 clauses = 95462 binary + 50393 ternary
c [cce-9-1] tried to eliminate 2610 small clauses 2%
c [cce-9-1] eliminated 408 binary clauses 0%
c [cce-9-1] eliminated 162 ternary clauses 0%
c [cce-9-1] eliminated 570 small clauses 0%
c [cce-9-1] eliminated 570 small clauses in 39400199 steps
c [cce-9-1] incomplete small round (ACCE)
c [cce-9-1] eliminated 799 covered clauses in round 1
c [cce-9] eliminated 799 covered clauses in TOTAL during 1 rounds
c [cce-9] 799 < 1/100 * 178065 = 1780 considered unsuccessful
c [elim-17] no untried remaining variables left
c [elim-17] scheduled 29486 variables 100%
c [elim-17] limit of 630402996 steps penalty 0 = 0 + 0
c [elim-17] rescheduling of touched variables disabled
c [elim-17-1] eliminated 242 variables 1% in round 1 in 14380978 steps
c [elim-17-1] backward subsumption/strengthening limit 14380900
c [elim-17-1-1] backward checking 1795 touched variables 6%
c [elim-17-1-1] fully completed backward checking in 1 rounds
c [elim-17-1] subsumed 13 and strengthened 16 clauses in 427121 steps
c [elim-17-1] rescheduled 65 variables 0% by backward subsumption
c [elim-17-2] eliminated 3 variables 0% in round 2 in 41552 steps
c [elim-17-2] backward subsumption/strengthening limit 41500
c [elim-17-2-1] backward checking 39 touched variables 0%
c [elim-17-2-1] fully completed backward checking in 1 rounds
c [elim-17-2] subsumed 6 and strengthened 1 clauses in 33265 steps
c [elim-17-2] rescheduled 12 variables 0% by backward subsumption
c [elim-17-3] eliminated 4 variables 0% in round 3 in 6633 steps
c [elim-17-3] backward subsumption/strengthening limit 6600
c [elim-17-3-1] backward checking 25 touched variables 0%
c [elim-17-3-1] incomplete backward checking 5 remain 20%
c [elim-17-3] subsumed 1 and strengthened 0 clauses in 6622 steps
c [elim-17] incomplete 3 not tried 0% in round 3
c [elim-17] transition to [ all 1 rem 1 ] state
c [elim-17] eliminated 249 = 1% variables out of 29486 scheduled
c [elim-17] 249 < 1/100 * 29486 = 294 considered unsuccessful
c [bca-18] limit of 10000000 steps and 354692 added (scaled 2)
c [bca-18] 44292 out of 58476 literals actually usable 76%
c [bca-18] added 33 blocked clauses in 136723 steps
c [sweep-18] almost no limit of 4000000000 steps
c [sweep-18-1] 1408 pos 12.6% + 9777 neg 87.4% = 11185 sched 38.3% ret 18052
c [sweep-18-1] 79423628 steps 4192 queries 35.66 avg class size
c [sweep-18-1] 22938 decisions 3354 SAT calls 56.09 avg env size
c [sweep-18-1] fully completed sweeping round
c [decomp-57] removed 899 variables
c [sweep-18-1] removed 899 vars (0 failed, 855 eqs, 901 impls)
c [sweep-18-2] 2996 pos 10.6% + 25342 neg 89.4% = 28338 sched 100.0% ret 0
c [sweep-18-2] 123631530 steps 4472 queries 58.65 avg class size
c [sweep-18-2] 44267 decisions 4292 SAT calls 73.63 avg env size
c [sweep-18-2] fully completed sweeping round
c [decomp-58] removed 329 variables
c [sweep-18-2] removed 329 vars (0 failed, 223 eqs, 631 impls)
c [sweep-18-3] 2989 pos 10.7% + 25020 neg 89.3% = 28009 sched 100.0% ret 0
c [sweep-18-3] 125922992 steps 4327 queries 48.36 avg class size
c [sweep-18-3] 39383 decisions 4251 SAT calls 70.48 avg env size
c [sweep-18-3] fully completed sweeping round
c [decomp-59] removed 131 variables
c [sweep-18-3] removed 131 vars (0 failed, 97 eqs, 448 impls)
c [sweep-18] removed 1359 vars in TOTAL (3 rounds, 12988 queries)
c [sort-queue-22] sorted 3129 enqueued variables after 127512 conflicts
c [score-dist-22] active 24749 (89%), one 0 (0%), zero 3129 (11%)
c [score-dist-22] max exp 511, different 370 (72%)
c [score-dist-22] median active exp 504, avg 479.7
c [simplification-22] removed 1629 variables 5.5% (27878 remain 13%)
c [simplification-22] removed 6877 irredundant clauses 3.8% (172893 remain 15%)
c [simplification-22] maximum reduction of 6% = max (6%, 4%)
c [simplification-22] large reduction 6% >= 5% limit
c [simplification-22] next conflict interval 2000 = 2000/1
c [simplification-22] penalized conflict interval 2000 = 1 * 2000
c [simplification-22] hard conflict limit 139512 (soft 129512 + delta 10000)
c [simplification-22] new conflict limit 129512 (hard 139512)
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  233.1   27877   172893    133821   45689   4625 358682  101   141   67  72%    169  -53  104  114   91%
c 
c [simplification-23] limit 129512 conflicts (hard 139512) hit after 139512 conflicts
c [quatres-17] found 12875 quaternary clauses 50% in total
c [quatres-17-1] removed 1 duplicate quaternary clauses
c [quatres-17-2] added 17 single-self-subsuming ternary resolvents
c [quatres-17-2] added 8 quaternary resolvents
c [ternres-19] limit 33484057 with penalty 0 = 0 + 0
c [ternres-19] all 27877 free variables schedulable
c [ternres-19] 380 ternary resolvents (1 bin, 379 trn)
c [ternres-19] fully completed ternary resolution
c [decomp-60] removed 2 variables
c [basicprobe-8] limit 167420287 penalty 0 = 0 + 0
c [basicprobe-8-0] 5004 sched 18%, 250 failed, 5 lifted, 18098 hbrs
c [decomp-61] removed 410 variables
c [basicprobe-8-1] 2709 probes remain 10% after last round
c [basicprobe-8-1] 409 units = 398 failed (97%) + 11 lifted (3%)
c [basicprobe-8-1] removed 623 variables, found 31167 hbrs
c [bate-6] eliminated 153 asymmetric tautologies during probing
c [unhide-23] limit 3348405 with penalty 1 = 0 + 1
c [unhide-23-37] 0 units, 14 failed, 86843 tauts, 0 hbrs, 122875 literals
c [transred-19] limit 2000000 with penalty 0 = 0 + 0
c [transred-19] removed 835 transitive binary clauses
c [transred-19] found 2 units
c [bca-19] limit of 10000000 steps and 325650 added (scaled 2)
c [bca-19] 36323 out of 54438 literals actually usable 67%
c [bca-19] added 11 blocked clauses in 125613 steps
c [sweep-19] limit 10045217 penalty 0 = 0 + 0
c [sweep-19-1] 3101 pos 11.4% + 24117 neg 88.6% = 27218 sched 100.0% ret 0
c [sweep-19-1] 10906881 steps 187 queries 856.09 avg class size
c [sweep-19-1] 6844 decisions 182 SAT calls 224.27 avg env size
c [sweep-19-1] 22890 variables remain 84% (4315 retained 16%)
c [decomp-62] removed 26 variables
c [sweep-19-1] removed 26 vars (0 failed, 5 eqs, 13 impls)
c [sweep-19] 26 < 1/1000 * 27218 = 27 considered unsuccessful
c [sweep-19] removed 26 vars in TOTAL (1 rounds, 186 queries)
c [sort-queue-23] sorted 2761 enqueued variables after 139512 conflicts
c [score-dist-23] active 24431 (90%), one 93 (0%), zero 2668 (10%)
c [score-dist-23] max exp 510, different 369 (72%)
c [score-dist-23] median active exp 460, avg 457.3
c [simplification-23] removed 685 variables 2.5% (27192 remain 13%)
c [simplification-23] removed 10798 irredundant clauses 6.2% (162095 remain 14%)
c [simplification-23] maximum reduction of 6% = max (2%, 6%)
c [simplification-23] large reduction 6% >= 5% limit
c [simplification-23] next conflict interval 2000 = 2000/1
c [simplification-23] penalized conflict interval 2000 = 1 * 2000
c [simplification-23] hard conflict limit 151512 (soft 141512 + delta 10000)
c [simplification-23] new conflict limit 141512 (hard 151512)
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  246.8   27191   162095    142673   51283   4676 286376   66    94   69  70%     60  -92   32  110   29%
c i  251.8   27188   162095    149887   56177   4685 286389   75    99   73  76%     35  -78   76  106   71%
c -  252.3   27186   162095    150434   27386   4687 286389   84   113   37  75%     -3  -63  135  107  126%
c 
c [simplification-24] limit 141512 conflicts (hard 151512) hit after 151512 conflicts
c [quatres-18] found 12436 quaternary clauses 50% in total
c [quatres-18-1] removed 1 duplicate quaternary clauses
c [quatres-18-2] added 1 single-self-subsuming ternary resolvents
c [quatres-18-2] added 2 quaternary resolvents
c [ternres-20] limit 35520588 with penalty 0 = 0 + 0
c [ternres-20] all 27186 free variables schedulable
c [ternres-20] 90 ternary resolvents (1 bin, 89 trn)
c [ternres-20] fully completed ternary resolution
c [decomp-63] removed 7 variables
c [simpleprobe-9] all 27185 free variables schedulable
c [simpleprobe-9] limit 142082352 penalty 0 = 0 + 0
c [decomp-64] removed 55 variables
c [simpleprobe-9] fully completed simple probing
c [simpleprobe-9] removed 55 variables, found 45522 hbrs, 19 units
c [unhide-24] limit 7104117 with penalty 0 = 0 + 0
c [unhide-24-42] 1 units, 5 failed, 92053 tauts, 0 hbrs, 121919 literals
c [transred-20] limit 2000000 with penalty 0 = 0 + 0
c [transred-20] removed 697 transitive binary clauses
c [elim-18] no untried remaining variables left
c [elim-18] scheduled 27124 variables 100%
c [elim-18] boosting limit by 20
c [elim-18] limit of 7104117630 steps penalty 1 = 1 + 0
c [elim-18] rescheduling of touched variables disabled
c [elim-18-1] eliminated 729 variables 3% in round 1 in 13843830 steps
c [elim-18-1] backward subsumption/strengthening limit 13843800
c [elim-18-1-1] backward checking 3861 touched variables 14%
c [elim-18-1-1] fully completed backward checking in 1 rounds
c [elim-18-1] subsumed 15 and strengthened 40 clauses in 737398 steps
c [elim-18-1] rescheduled 135 variables 0% by backward subsumption
c [elim-18-2] eliminated 10 variables 0% in round 2 in 237076 steps
c [elim-18-2] backward subsumption/strengthening limit 237000
c [elim-18-2-1] backward checking 110 touched variables 0%
c [elim-18-2-1] fully completed backward checking in 1 rounds
c [elim-18-2] subsumed 6 and strengthened 0 clauses in 108880 steps
c [elim-18-2] rescheduled 14 variables 0% by backward subsumption
c [elim-18-3] no variable eliminated in round 3 in 524434 steps
c [elim-18] fully completed in 3 rounds
c [elim-18] transition to [ all 0 rem 0 ] state
c [elim-18] eliminated 739 = 3% variables out of 27124 scheduled
c [bca-20] limit of 10000000 steps and 319578 added (scaled 2)
c [bca-20] 35868 out of 52772 literals actually usable 68%
c [bca-20] added 21 blocked clauses in 103141 steps
c [sort-queue-24] sorted 2980 enqueued variables after 151512 conflicts
c [score-dist-24] active 23405 (89%), one 426 (2%), zero 2554 (10%)
c [score-dist-24] max exp 510, different 353 (69%)
c [score-dist-24] median active exp 455, avg 441.0
c [simplification-24] removed 801 variables 2.9% (26385 remain 12%)
c [simplification-24] removed 2873 irredundant clauses 1.8% (159222 remain 13%)
c [simplification-24] maximum reduction of 3% = max (3%, 2%)
c [simplification-24] geometric conflict interval increment 5916 = 23666 / 4
c [simplification-24] new conflict interval 29582
c [simplification-24] penalized conflict interval 29582 = 1 * 29582
c [simplification-24] hard conflict limit 195885 (soft 181094 + delta 14791)
c [simplification-24] new conflict limit 181094 (hard 195885)
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  268.3   26384   159222    170749   42871   4493 210303   44    74   49  60%    221  -75   57   89   64%
c 
c [simplification-25] limit 181094 conflicts (hard 195885) hit after 189170 conflicts
c [quatres-19] found 12595 quaternary clauses 47% in total
c [quatres-19-1] removed 2 duplicate quaternary clauses
c [quatres-19-2] added 2 single-self-subsuming ternary resolvents
c [quatres-19-2] added 9 quaternary resolvents
c [ternres-21] limit 40805509 with penalty 0 = 0 + 0
c [ternres-21] all 26383 free variables schedulable
c [ternres-21] 250 ternary resolvents (1 bin, 249 trn)
c [ternres-21] fully completed ternary resolution
c [gauss-6] limit 510068 penalty 4 = 4 + 0
c [gauss-6] extracted 22 xors of average arity 3.0
c [gauss-6] connected 66 occurrences of 42 variables (average 1.6)
c [gauss-6] limit 510068 penalty 4 = 4 + 0
c [gauss-6] fully completed
c [gauss-6] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-65] removed 1 variables
c [treelook-9] limit 4080550 penalty 0 = 0 + 0 boost 1
c [treelook-9] scheduled 36276 literals 69%
c [treelook-9] scheduling used 704341 steps
c [treelook-9] scheduled completely
c [treelook-9] limit 4080550 penalty 0 = 0 + 0 boost 1
c [treelook-9] used 4124786 steps
c [treelook-9] 36131 literals remain 68%
c [treelook-9] 5524 variables remain to probed next time 21%
c [treelook-9] removed 7 variables, found 12004 hbrs
c [unhide-25] limit 4080550 with penalty 1 = 0 + 1
c [unhide-25-45] 0 units, 16 failed, 13690 tauts, 0 hbrs, 689215 literals
c [transred-21] limit 2000000 with penalty 0 = 0 + 0
c [transred-21] removed 495 transitive binary clauses
c [transred-21] found 1 units
c [cce-10] limit of 25503443 steps penalty 3 = 3 + 0
c [cce-10-1] eliminated 2 clauses out of 2 (100%) of length 81
c [cce-10-1] eliminated 1 clauses out of 2 (50%) of length 80
c [cce-10-1] eliminated 2 clauses out of 2 (100%) of length 79
c [cce-10-1] eliminated 1 clauses out of 2 (50%) of length 78
c [cce-10-1] eliminated 2 clauses out of 2 (100%) of length 77
c [cce-10-1] eliminated 1 clauses out of 2 (50%) of length 76
c [cce-10-1] eliminated 1 clauses out of 2 (50%) of length 75
c [cce-10-1] eliminated 2 clauses out of 2 (100%) 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 2 (100%) of length 72
c [cce-10-1] eliminated 1 clauses out of 3 (33%) of length 71
c [cce-10-1] eliminated 1 clauses out of 1 (100%) of length 70
c [cce-10-1] eliminated 2 clauses out of 2 (100%) of length 69
c [cce-10-1] eliminated 1 clauses out of 2 (50%) of length 68
c [cce-10-1] eliminated 2 clauses out of 2 (100%) of length 67
c [cce-10-1] eliminated 1 clauses out of 2 (50%) of length 66
c [cce-10-1] eliminated 2 clauses out of 3 (67%) of length 65
c [cce-10-1] eliminated 1 clauses out of 3 (33%) of length 64
c [cce-10-1] eliminated 2 clauses out of 2 (100%) of length 63
c [cce-10-1] eliminated 1 clauses out of 3 (33%) of length 62
c [cce-10-1] eliminated 2 clauses out of 2 (100%) of length 61
c [cce-10-1] eliminated 1 clauses out of 3 (33%) of length 60
c [cce-10-1] eliminated 2 clauses out of 2 (100%) of length 59
c [cce-10-1] eliminated 1 clauses out of 2 (50%) of length 48
c [cce-10-1] eliminated 2 clauses out of 3 (67%) of length 33
c [cce-10-1] eliminated 3 clauses out of 7 (43%) of length 32
c [cce-10-1] eliminated 4 clauses out of 6 (67%) of length 31
c [cce-10-1] eliminated 6 clauses out of 9 (67%) of length 30
c [cce-10-1] eliminated 6 clauses out of 9 (67%) of length 29
c [cce-10-1] eliminated 6 clauses out of 10 (60%) of length 28
c [cce-10-1] eliminated 6 clauses out of 13 (46%) of length 27
c [cce-10-1] eliminated 7 clauses out of 13 (54%) of length 26
c [cce-10-1] eliminated 9 clauses out of 14 (64%) of length 25
c [cce-10-1] eliminated 8 clauses out of 17 (47%) of length 24
c [cce-10-1] eliminated 11 clauses out of 18 (61%) of length 23
c [cce-10-1] eliminated 14 clauses out of 21 (67%) of length 22
c [cce-10-1] eliminated 15 clauses out of 22 (68%) of length 21
c [cce-10-1] eliminated 14 clauses out of 23 (61%) of length 20
c [cce-10-1] eliminated 14 clauses out of 20 (70%) of length 19
c [cce-10-1] eliminated 14 clauses out of 24 (58%) of length 18
c [cce-10-1] eliminated 17 clauses out of 25 (68%) of length 17
c [cce-10-1] eliminated 15 clauses out of 27 (56%) of length 16
c [cce-10-1] eliminated 16 clauses out of 29 (55%) of length 15
c [cce-10-1] eliminated 18 clauses out of 33 (55%) of length 14
c [cce-10-1] eliminated 16 clauses out of 33 (48%) of length 13
c [cce-10-1] eliminated 24 clauses out of 35 (69%) of length 12
c [cce-10-1] eliminated 22 clauses out of 44 (50%) of length 11
c [cce-10-1] eliminated 33 clauses out of 60 (55%) of length 10
c [cce-10-1] eliminated 37 clauses out of 62 (60%) of length 9
c [cce-10-1] eliminated 42 clauses out of 79 (53%) of length 8
c [cce-10-1] eliminated 40 clauses out of 98 (41%) of length 7
c [cce-10-1] eliminated 54 clauses out of 1019 (5%) of length 6
c [cce-10-1] eliminated 18 clauses out of 6385 (0%) of length 5
c [cce-10-1] incomplete large round (ATE)
c [cce-10-1] eliminated 526 large clauses in 25503447 steps
c [cce-10-1] allowing another 12751723 steps for small clauses
c [cce-10-1] scheduling 128480 clauses = 90293 binary + 38187 ternary
c [cce-10-1] tried to eliminate 1928 small clauses 2%
c [cce-10-1] eliminated 276 binary clauses 0%
c [cce-10-1] eliminated 62 ternary clauses 0%
c [cce-10-1] eliminated 338 small clauses 0%
c [cce-10-1] eliminated 360 small clauses in 25503445 steps
c [cce-10-1] incomplete small round (ATE)
c [cce-10-1] eliminated 886 covered clauses in round 1
c [cce-10] eliminated 886 covered clauses in TOTAL during 1 rounds
c [cce-10] 886 < 1/100 * 158131 = 1581 considered unsuccessful
c [elim-19] scheduling all variables this time
c [elim-19] scheduled 26366 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 68 variables 0% in round 1 in 12695638 steps
c [elim-19-1] backward subsumption/strengthening limit 12695600
c [elim-19-1-1] backward checking 574 touched variables 2%
c [elim-19-1-1] fully completed backward checking in 1 rounds
c [elim-19-1] subsumed 5 and strengthened 9 clauses in 181776 steps
c [elim-19-1] rescheduled 36 variables 0% by backward subsumption
c [elim-19-2] no variable eliminated in round 2 in 413814 steps
c [elim-19] fully completed in 2 rounds
c [elim-19] transition to [ all 0 rem 0 ] state
c [elim-19] eliminated 68 = 0% variables out of 26366 scheduled
c [elim-19] 68 < 1/100 * 26366 = 263 considered unsuccessful
c [bca-21] limit of 10000000 steps and 315388 added (scaled 2)
c [bca-21] 34766 out of 52598 literals actually usable 66%
c [bca-21] added 9 blocked clauses in 130236 steps
c [sweep-20] limit 6120826 penalty 1 = 1 + 0
c [sweep-20-1] 2970 pos 13.4% + 19162 neg 86.6% = 22132 sched 84.2% ret 4166
c [sweep-20-1] 7003310 steps 180 queries 941.21 avg class size
c [sweep-20-1] 4380 decisions 176 SAT calls 142.59 avg env size
c [sweep-20-1] 19737 variables remain 75% (6547 retained 25%)
c [decomp-67] removed 18 variables
c [sweep-20-1] removed 18 vars (0 failed, 3 eqs, 9 impls)
c [sweep-20] 18 < 1/1000 * 26298 = 26 considered unsuccessful
c [sweep-20] removed 18 vars in TOTAL (1 rounds, 179 queries)
c [sort-queue-25] sorted 3311 enqueued variables after 189170 conflicts
c [score-dist-25] active 22969 (87%), one 893 (3%), zero 2418 (9%)
c [score-dist-25] max exp 510, different 347 (68%)
c [score-dist-25] median active exp 495, avg 413.9
c [simplification-25] removed 103 variables 0.4% (26280 remain 12%)
c [simplification-25] removed 2285 irredundant clauses 1.4% (156937 remain 13%)
c [simplification-25] maximum reduction of 1% = max (0%, 1%)
c [simplification-25] geometric conflict interval increment 14791 = 29582 / 2
c [simplification-25] new conflict interval 44373
c [simplification-25] penalized conflict interval 44373 = 1 * 44373
c [simplification-25] hard conflict limit 255729 (soft 233543 + delta 22186)
c [simplification-25] new conflict limit 233543 (hard 255729)
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 -  287.6   26280   156937    193860   31340   4648 208723  109   162   36  68%    227   20   87   89   98%
c i  310.5   26279   156937    234329   57519   4801 208910   72   110   67  66%    594  -38   60   95   63%
c -  312.5   26279   156937    238337   32818   4810 208942   71   111   37  64%   -310  -36   45   94   48%
c 
c [simplification-26] limit 233543 conflicts (hard 255729) hit after 255730 conflicts
c [quatres-20] found 12881 quaternary clauses 46% in total
c [quatres-20-1] removed 1 duplicate quaternary clauses
c [quatres-20-2] added 2 single-self-subsuming ternary resolvents
c [quatres-20-2] added 5 quaternary resolvents
c [ternres-22] limit 50518399 with penalty 0 = 0 + 0
c [ternres-22] all 26279 free variables schedulable
c [ternres-22] 113 ternary resolvents (0 bin, 113 trn)
c [ternres-22] fully completed ternary resolution
c [decomp-68] removed 1 variables
c [basicprobe-9] limit 252591999 penalty 0 = 0 + 0
c [basicprobe-9-0] 2919 sched 11%, 155 failed, 6 lifted, 10342 hbrs
c [decomp-69] removed 212 variables
c [basicprobe-9-1] 9123 sched 35%, 128 failed, 6 lifted, 18760 hbrs
c [decomp-70] removed 155 variables
c [basicprobe-9-2] 9095 sched 35%, 89 failed, 5 lifted, 4529 hbrs
c [decomp-71] removed 100 variables
c [basicprobe-9-3] 5838 probes remain 23% after last round
c [basicprobe-9-3] 416 units = 399 failed (96%) + 17 lifted (4%)
c [basicprobe-9-3] removed 497 variables, found 34369 hbrs
c [bate-7] eliminated 91 asymmetric tautologies during probing
c [unhide-26] limit 10103679 with penalty 0 = 0 + 0
c [unhide-26-52] 0 units, 0 failed, 44300 tauts, 0 hbrs, 293744 literals
c [transred-22] limit 2000000 with penalty 0 = 0 + 0
c [transred-22] removed 354 transitive binary clauses
c [block-7] scheduling all variables this time
c [block-7] scheduled 25782 variables 100%
c [block-7] limit of 31573999 steps penalty 4 = 4 + 0
c [block-7] fully completed
c [block-7] transition to [ all 0 rem 0 ] state
c [block-7] eliminated 25 blocked clauses
c [block-7] 25 < 1/100 * 149325 = 1493 considered unsuccessful
c [bca-22] limit of 10000000 steps and 299749 added (scaled 2)
c [bca-22] 33500 out of 51566 literals actually usable 65%
c [bca-22] added 14 blocked clauses in 111758 steps
c [sort-queue-26] sorted 3207 enqueued variables after 255730 conflicts
c [score-dist-26] active 22575 (88%), one 1253 (5%), zero 1954 (8%)
c [score-dist-26] max exp 510, different 393 (77%)
c [score-dist-26] median active exp 472, avg 346.8
c [simplification-26] removed 497 variables 1.9% (25782 remain 12%)
c [simplification-26] removed 7637 irredundant clauses 4.9% (149300 remain 13%)
c [simplification-26] maximum reduction of 5% = max (2%, 5%)
c [simplification-26] large reduction 5% >= 5% limit
c [simplification-26] next conflict interval 2557 = min (255730/100, 44373)
c [simplification-26] penalized conflict interval 2557 = 1 * 2557
c [simplification-26] hard conflict limit 268287 (soft 258287 + delta 10000)
c [simplification-26] new conflict limit 258287 (hard 268287)
c 
c [simplification-27] limit 258287 conflicts (hard 268287) hit after 268287 conflicts
c [quatres-21] found 12572 quaternary clauses 45% in total
c [quatres-21-1] removed 2 duplicate quaternary clauses
c [ternres-23] limit 52125176 with penalty 0 = 0 + 0
c [ternres-23] all 25782 free variables schedulable
c [ternres-23] 146 ternary resolvents (1 bin, 145 trn)
c [ternres-23] fully completed ternary resolution
c [decomp-72] removed 1 variables
c [simpleprobe-10] all 25781 free variables schedulable
c [simpleprobe-10] limit 200000000 penalty 0 = 0 + 0
c [decomp-73] removed 2 variables
c [simpleprobe-10] fully completed simple probing
c [simpleprobe-10] removed 2 variables, found 27077 hbrs, 0 units
c [transred-23] limit 2000000 with penalty 0 = 0 + 0
c [transred-23] removed 692 transitive binary clauses
c [elim-20] scheduling all variables this time
c [elim-20] scheduled 25779 variables 100%
c [elim-20] limit of 400000000 steps penalty 1 = 1 + 0
c [elim-20] rescheduling of touched variables disabled
c [elim-20-1] eliminated 130 variables 1% in round 1 in 11686386 steps
c [elim-20-1] backward subsumption/strengthening limit 11686300
c [elim-20-1-1] backward checking 872 touched variables 3%
c [elim-20-1-1] fully completed backward checking in 1 rounds
c [elim-20-1] subsumed 3 and strengthened 7 clauses in 176714 steps
c [elim-20-1] rescheduled 22 variables 0% by backward subsumption
c [elim-20-2] no variable eliminated in round 2 in 399597 steps
c [elim-20] fully completed in 2 rounds
c [elim-20] transition to [ all 0 rem 0 ] state
c [elim-20] eliminated 130 = 1% variables out of 25779 scheduled
c [elim-20] 130 < 1/100 * 25779 = 257 considered unsuccessful
c [bca-23] limit of 10000000 steps and 299226 added (scaled 2)
c [bca-23] 33025 out of 51300 literals actually usable 64%
c [bca-23] added 4 blocked clauses in 116155 steps
c [sort-queue-27] sorted 7376 enqueued variables after 268287 conflicts
c [score-dist-27] active 18273 (71%), one 5488 (21%), zero 1888 (7%)
c [score-dist-27] max exp 510, different 375 (73%)
c [score-dist-27] median active exp 496, avg 451.7
c [simplification-27] removed 133 variables 0.5% (25649 remain 12%)
c [simplification-27] removed 265 irredundant clauses 0.2% (149035 remain 13%)
c [simplification-27] maximum reduction of 1% = max (1%, 0%)
c [simplification-27] geometric conflict interval increment 22186 = 44373 / 2
c [simplification-27] new conflict interval 66559
c [simplification-27] penalized conflict interval 66559 = 1 * 66559
c [simplification-27] hard conflict limit 368125 (soft 334846 + delta 33279)
c [simplification-27] new conflict limit 334846 (hard 368125)
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  347.3   25648   149035    278316   54506   4839 224852   49    77   56  64%    289  -42   46   75   61%
c -  352.2   25648   149035    287401   33087   4843 224853   56    79   36  70%   -224  -34   60   72   84%
c -  371.6   25648   149035    322168   34698   4892 224874   51    66   36  78%    290  -31   53   64   83%
c -  388.6   25648   149035    355367   35505   4924 224902   57    73   37  78%    582  -13   56   59   95%
c 
c [simplification-28] limit 334846 conflicts (hard 368125) hit after 368125 conflicts
c [ternres-24] limit 66440661 with penalty 0 = 0 + 0
c [ternres-24] all 25648 free variables schedulable
c [ternres-24] 41 ternary resolvents (0 bin, 41 trn)
c [ternres-24] fully completed ternary resolution
c [card-7] limit 2076270 penalty 4 = 4 + 0
c [card-7] found 4200 at-most-one constraints of average size 3.9
c [card-7] no at-most-two constraint found
c [card-7] using previous limit 2076270 for elimination
c [card-7] 4200 out of 4200 constraints (100%) meet size limits
c [card-7] no units found
c [card-7] no at-most-one constraints generated
c [decomp-74] removed 1 variables
c [treelook-10] limit 6644066 penalty 0 = 0 + 0 boost 1
c [treelook-10] scheduled 34844 literals 68%
c [treelook-10] scheduling used 664708 steps
c [treelook-10] scheduled completely
c [treelook-10] limit 6644066 penalty 0 = 0 + 0 boost 1
c [treelook-10] used 6663068 steps
c [treelook-10] 34299 literals remain 67%
c [treelook-10] 5427 variables remain to probed next time 21%
c [decomp-75] removed 2 variables
c [treelook-10] removed 11 variables, found 41115 hbrs
c [unhide-27] limit 6644066 with penalty 1 = 1 + 0
c [unhide-27-56] 0 units, 1 failed, 49476 tauts, 0 hbrs, 442215 literals
c [transred-24] limit 2000000 with penalty 0 = 0 + 0
c [transred-24] removed 499 transitive binary clauses
c [bca-24] limit of 10000000 steps and 298208 added (scaled 2)
c [bca-24] 33259 out of 51274 literals actually usable 65%
c [bca-24] added 9 blocked clauses in 118043 steps
c [sweep-21] limit 4983049 penalty 2 = 2 + 0
c [sweep-21-1] 2503 pos 12.8% + 17079 neg 87.2% = 19582 sched 76.4% ret 6054
c [sweep-21-1] 4997491 steps 94 queries 1340.17 avg class size
c [sweep-21-1] 3167 decisions 92 SAT calls 175.20 avg env size
c [sweep-21-1] 18724 variables remain 73% (6912 retained 27%)
c [decomp-76] removed 2 variables
c [sweep-21-1] removed 2 vars (0 failed, 1 eqs, 13 impls)
c [sweep-21] 2 < 1/1000 * 25636 = 25 considered unsuccessful
c [sweep-21] removed 2 vars in TOTAL (1 rounds, 93 queries)
c [sort-queue-28] sorted 7555 enqueued variables after 368125 conflicts
c [score-dist-28] active 18079 (71%), one 5722 (22%), zero 1833 (7%)
c [score-dist-28] max exp 510, different 411 (80%)
c [score-dist-28] median active exp 494, avg 421.8
c [simplification-28] removed 14 variables 0.1% (25634 remain 12%)
c [simplification-28] removed 513 irredundant clauses 0.3% (148522 remain 12%)
c [simplification-28] maximum reduction of 0% = max (0%, 0%)
c [simplification-28] full geometric conflict interval increment 66559
c [simplification-28] new conflict interval 133118
c [simplification-28] penalized conflict interval 133118 = 1 * 133118
c [simplification-28] hard conflict limit 567802 (soft 501243 + delta 66559)
c [simplification-28] new conflict limit 501243 (hard 567802)
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  401.2   25633   148522    371620   50245   4907 216537   46    56   51  82%    679  -25   41   57   73%
c -  410.5   25622   148522    389476   36429   4915 216543   42    51   36  82%   -367  -23   42   53   80%
c -  427.9   25622   148522    423952   37581   4934 216554   41    47   36  88%    202  -17   41   49   83%
c i  439.0   25621   148522    447616   58878   4983 216564   10    17   57  57%    451  -39    5   39   13%
c -  445.9   25506   148522    461268   39207   5007 216584   12    15   37  76%   -420  -34    9   35   25%
c i  449.5   25505   148522    468431   45436   5018 216597   33    41   48  81%   -271   -7   44   34  129%
c i  453.7   25504   148522    476022   51930   5021 216603   49    62   62  79%   -423   14   56   36  156%
c i  453.7   25503   148522    476048   51948   5021 216603   49    62   62  79%   -426   14   55   36  152%
c -  465.9   25503   148522    498798   39829   5024 216606   23    26   49  89%    -84  -18   23   33   69%
c 
c [simplification-29] limit 501243 conflicts (hard 567802) hit after 507317 conflicts
c [quatres-22] found 12637 quaternary clauses 41% in total
c [quatres-22-1] removed 2 duplicate quaternary clauses
c [quatres-22-2] added 4 single-self-subsuming ternary resolvents
c [quatres-22-2] added 5 quaternary resolvents
c [ternres-25] limit 86465158 with penalty 0 = 0 + 0
c [ternres-25] all 25503 free variables schedulable
c [ternres-25] 50 ternary resolvents (1 bin, 49 trn)
c [ternres-25] fully completed ternary resolution
c [decomp-77] removed 131 variables
c [basicprobe-10] limit 400000000 penalty 0 = 0 + 0
c [basicprobe-10-0] 5829 sched 24%, 567 failed, 2 lifted, 5060 hbrs
c [decomp-78] removed 995 variables
c [basicprobe-10-1] 8447 sched 36%, 371 failed, 17 lifted, 9241 hbrs
c [decomp-79] removed 1100 variables
c [basicprobe-10-2] 8053 sched 35%, 142 failed, 3 lifted, 10521 hbrs
c [decomp-80] removed 380 variables
c [basicprobe-10-3] 7880 sched 34%, 76 failed, 4 lifted, 5596 hbrs
c [decomp-81] removed 236 variables
c [basicprobe-10-4] 7836 sched 35%, 69 failed, 0 lifted, 4797 hbrs
c [decomp-82] removed 162 variables
c [basicprobe-10-5] 7797 sched 35%, 46 failed, 0 lifted, 3816 hbrs
c [decomp-83] removed 193 variables
c [basicprobe-10-6] 7752 sched 35%, 38 failed, 0 lifted, 1888 hbrs
c [decomp-84] removed 69 variables
c [basicprobe-10-7] 755 probes remain 3% after last round
c [basicprobe-10-7] 1367 units = 1339 failed (98%) + 28 lifted (2%)
c [basicprobe-10-7] removed 3203 variables, found 41843 hbrs
c [bate-8] eliminated 121 asymmetric tautologies during probing
c [unhide-28] limit 17293031 with penalty 0 = 0 + 0
c [unhide-28-70] 2 units, 0 failed, 46173 tauts, 0 hbrs, 197118 literals
c [transred-25] limit 2000000 with penalty 0 = 0 + 0
c [transred-25] removed 447 transitive binary clauses
c [cce-11] limit of 27020361 steps penalty 4 = 4 + 0
c [cce-11-1] eliminated 1 clauses out of 1 (100%) of length 46
c [cce-11-1] eliminated 1 clauses out of 1 (100%) of length 43
c [cce-11-1] eliminated 1 clauses out of 1 (100%) of length 41
c [cce-11-1] eliminated 1 clauses out of 2 (50%) of length 39
c [cce-11-1] eliminated 1 clauses out of 6 (17%) of length 26
c [cce-11-1] eliminated 1 clauses out of 4 (25%) of length 25
c [cce-11-1] eliminated 1 clauses out of 7 (14%) of length 22
c [cce-11-1] eliminated 2 clauses out of 7 (29%) of length 19
c [cce-11-1] eliminated 1 clauses out of 9 (11%) of length 18
c [cce-11-1] eliminated 2 clauses out of 9 (22%) of length 17
c [cce-11-1] eliminated 2 clauses out of 13 (15%) of length 16
c [cce-11-1] eliminated 1 clauses out of 7 (14%) of length 15
c [cce-11-1] eliminated 1 clauses out of 11 (9%) of length 14
c [cce-11-1] eliminated 1 clauses out of 11 (9%) of length 13
c [cce-11-1] eliminated 2 clauses out of 26 (8%) of length 10
c [cce-11-1] eliminated 2 clauses out of 19 (11%) of length 9
c [cce-11-1] eliminated 4 clauses out of 34 (12%) of length 8
c [cce-11-1] eliminated 6 clauses out of 46 (13%) of length 7
c [cce-11-1] eliminated 15 clauses out of 507 (3%) of length 6
c [cce-11-1] eliminated 192 clauses out of 4323 (4%) of length 5
c [cce-11-1] eliminated 78 clauses out of 8394 (1%) of length 4
c [cce-11-1] incomplete large round (ACCE)
c [cce-11-1] eliminated 316 large clauses in 27020370 steps
c [cce-11-1] allowing another 13510185 steps for small clauses
c [cce-11-1] scheduling 90823 clauses = 69361 binary + 21462 ternary
c [cce-11-1] tried to eliminate 5048 small clauses 6%
c [cce-11-1] eliminated 954 binary clauses 1%
c [cce-11-1] eliminated 225 ternary clauses 1%
c [cce-11-1] eliminated 1179 small clauses 1%
c [cce-11-1] eliminated 1179 small clauses in 27020362 steps
c [cce-11-1] incomplete small round (ACCE)
c [cce-11-1] eliminated 1495 covered clauses in round 1
c [cce-11] eliminated 1495 covered clauses in TOTAL during 1 rounds
c [bca-25] limit of 10000000 steps and 225878 added (scaled 2)
c [bca-25] 30220 out of 44564 literals actually usable 68%
c [bca-25] added 20 blocked clauses in 91904 steps
c [sort-queue-29] sorted 9502 enqueued variables after 507317 conflicts
c [score-dist-29] active 12779 (57%), one 8319 (37%), zero 1183 (5%)
c [score-dist-29] max exp 509, different 317 (62%)
c [score-dist-29] median active exp 500, avg 451.1
c [simplification-29] removed 3222 variables 12.6% (22281 remain 10%)
c [simplification-29] removed 36164 irredundant clauses 24.3% (112358 remain 9%)
c [simplification-29] maximum reduction of 24% = max (13%, 24%)
c [simplification-29] large reduction 24% >= 5% limit
c [simplification-29] next conflict interval 5073 = min (507317/100, 133118)
c [simplification-29] penalized conflict interval 5073 = 1 * 5073
c [simplification-29] hard conflict limit 522390 (soft 512390 + delta 10000)
c [simplification-29] new conflict limit 512390 (hard 522390)
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 1  486.2   22281   112358    507398   29520   4229 138756   25    48   31  51%     52    6   14   32   45%
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
s SATISFIABLE
c
c bate: 2557 basic ate = 2126 trn 83% + 431 lrg 17% in 8 updates
c bcas: 25 count, 1345 added (3743 skipped), 4909722 steps
c bkwd: tried 403203 clauses, 805377 lits, 2.00 lits/clause
c bkwd: checked 11571265 occs, 28.70 occs/clause, 14.37 occs/lit
c bkwd: subsumed 70 binary, 422 ternary, 154 large
c bkwd: strengthened 4 binary, 1 ternary (100% self), 1135 large (0% self)
c blkd: 7 bces, 9831 removed, 7500911 resolutions, 21118415 steps
c blkd: 11269 blocking literals 3%, 55 pure
c bump: 512158 bumped seen, 213981859 lits 417.8 on average
c card: 7 count, 0 units, 0 am1, 97193421 steps
c card: 0 rescheduled, 0 eliminated, 0 resolved, 76041 subsumed
c card: 21041 at-most-one constraints found, average size 4.68
c card: 21041 at-most-one constraints used 100%, average size 4.68
c card: 0 at-most-two constraints found, average size 0.00
c card: 0 at-most-two constraints used 0%, average size 0.00
c cces: 11 cces, 40573 eliminated, 40176 ate 99%, 397 abce 1%
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: 4113121 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 232 gcs, 0 rescored clauses, 1972 rescored vars
c dcps: 84 decompositions, 10198 equivalent 5%
c deco: 68104 decision-only clauses 13%, 58% reduction
c decs: 4491883 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 20 elims, 93372 eliminated 42%, 81 pure 0%
c elms: 57 rounds, 2.9 rounds/bve
c elms: 77940 small 83%, 15296 large 16%
c elms: 260836 tried small, 77945 succeeded 30%, 182891 failed 70%
c elms: 36075 subsumed, 59785 strengthened, 496 blocked
c elms: 21898917 copies, 21078626 resolutions, 7183578 ipos
c elms: 5444755 subchks, 3275298 strchks
c gaus: 6 extractions, 141 extracted, 2.7 size, 3 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 9102630 steps, 4551315 extr 50%, 695 elim 0%
c glue: 77.3 orig avg, 77.3 real avg, 7.0 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 1257230 = 346807 simple 28% + 853203 trn 68% + 57220 lrg 5%, 5472 sub 0%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 512158 clauses, 142.8 length
c lrnd: 73139971 lits = 131462766 orig - 58322795 removed 44%
c lrnd: 219001 uips 43%, 254855 flips 50%
c mins: 420526 mins 85%, 2224 bin 0%, 5794 size 1%
c mins: 138506000 poisoned searches, 24848840 hits, 18% hit rate
c mins: 199754951 used twice searches, 16679821 hits, 8% hit rate
c move: moved 24383, 16104 bin 66%, 8279 trn 34%
c otfs: 2545 driving 35%, 4793 restarting 65%
c otfs: str 7338, 7199 red 98%, 139 irr 2%
c otfs: str 7338, 0 bin 0%, 114 trn 2%, 7224 lrg 98%
c otfs: sub 53, 51 red 96%, 2 irr 4%
c otfs: sub 53, 0 bin 0%, 3 trn 6%, 50 lrg 94%
c phas: 19 computed, 108868 set, 12 pos (0%), 108856 neg (100%)
c prbs: 10 basic, 234160 probed, 5038 failed, 102 lifted
c prbs: 10 simple, 900871 probed, 1283 failed, 927 eqs
c prbs: 10 treelook, 1004 probed, 28 failed, 0 lifted
c prom: 55195 locked 3% out of 1602236 tried
c prps: 1205605871 props, 240 props/dec
c prps: 90% srch, 10% simp, 0% lkhd
c quat: 22 count, 227 quat, 49 self1, 1 self2, 1763 dup
c queu: 29 sorted, 4491883 next (80054 steps 0.02)
c queu: 257403316 enq (387038282 steps 1.50), 213981859 deq 83%
c redc: 3226 clauses 17%, 18702 tried 4%, 57 sat 0%
c redc: 7794 lits 4%, 196600 tried 0%, 57 sat 0%
c redc: 316 times jump level reduced, 30.8 levels on average
c reds: 10 count, 50739.8 conflicts per reduce
c reds: 0 memlim 0%, 10 arith 100%
c reds: 272528 collected 92%, 24434 retired 8%
c rmbd: 50044 removed, 13367 red 27%
c rsts: 7627 restarts 99%, 51 skipped 1%
c rsts: 51 saturating 100%, 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: 29 count, 27 confs 93%, 0 vars 0%
c simp: 1 its 3%, 1 bin 3%, 0 trns 0%
c subl: 512158 count (615377 tried 1.2), 99097 sub out of 506145 (19.6%)
c swps: 21 count, 23 rounds, 16388 queries (712.5/round)
c swps: 14959 sat calls, 200 unsat (0.5% success rate)
c swps: 156243 decisions 10.4, 7305 conflicts 0.5
c swps; 387.5 avg class size, 74.3 avg environment size
c swps: 1 failed, 2674 impls, 1599 equivs
c swp0: 5457 type 0 queries, 2881 unsat (52.8%), 4938 sat (90.5%)
c swp1: 10931 type 1 queries, 6300 unsat (57.6%), 9851 sat (90.1%)
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: 10012891 calls to obtain time
c tops: 99135 fixed 44%, 305 its, 1663.60 confs/it
c trds: 25 transitive reductions, 11614 removed, 73 failed
c trds: 67063 nodes, 197889 edges, 50017405 steps
c trim: 1862668 words, 7.1 MB
c trnr: 25 count, 13 bin, 7674 trn, 145700594 steps
c unhd: 28 count, 70 rounds, 130336391 steps
c unhd: 3315 non-trivial sccs of average size 2.3
c unhd: 207 units, 201 bin, 2 trn, 4 lrg
c unhd: 8370 failed, 8307 stamp, 0 lits, 36 bin, 13 trn, 4 lrg
c unhd: 804285 tauts, 23917 bin 3%, 10420 trn 1%, 11304 lrg 1%
c unhd: 804285 tauts, 758644 stamp 94%, 723553 red 90%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 3976022 str, 201 bin 0%, 5372 trn 0%, 3970449 lrg 100%, 3954298 red 99%
c vars: 22281 remaining 10% and 202705 removed 90% out of 224986
c vars: 99135 fixed 44%, 93372 eliminated 42%, 10198 equivalent 5%
c vsts: 9877528221 visits, 88% srch, 12% simp, 0% lkhd
c vsts: 8.0 search visits per propagation, 17042.2 per conflict
c wchs: 1246815526 pushed, 57393657 enlarged, 345 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all         506372        272528         24434      35643279       6466676        234542
c 
c  0 0         19131   4      1473   1         0   0  16045147  45   2041985  32     51199  22     1.7
c  1 5          8345   2      2547   1       985   4   2073239   6    397130   6     14378   6     1.0
c  2 6         27173   5     14769   5      2228   9   3524926  10<   705377  11     25522  11     3.9
c  3 9         28624   6     17242   6      2448  10   3345183   9    582437   9<    19150   8     3.7
c  4 14        28790   6     16887   6      2124   9   2096442   6    457677   7     16657   7<    3.4
c  5 21        39189   8     21419   8      2186   9   2418605   7    503448   8     17488   7     4.9
c  6 30        19576   4     11215   4      1795   7<  1598038   4    352241   5     14622   6     2.2
c  7 41       109740  22<    86728  32<     4063  17   2111388   6    656603  10     27214  12    12.8
c  8 54        62374  12     45188  17      2590  11    713825   2    243406   4     13016   6     7.4
c  9 69        37527   7     25109   9      1796   7    649092   2    173721   3      9191   4     3.8
c 10 86        38959   8     18294   7      1804   7    568009   2    164048   3     10068   4     5.0
c 11 126       52200  10      8437   3      1778   7    342262   1    118847   2      8403   4    10.4
c 12 230       32100   6      3198   1       634   3    150093   0     66235   1      6969   3    12.1
c 13 534        2644   1        22   0         3   0      7030   0      3521   0       665   0     1.5
c 
c avg                  7.0           6.7           6.3           2.4           3.4           4.4
c std                  3.2           2.4           3.0           2.9           3.3           3.6
c 
c   45.660   9% probe
c   45.141   9% unhide
c   38.681   8% bump
c   24.399   5% sweep
c   19.548   4% elim
c   17.861   4% cce
c    5.499   1% rescore
c    3.439   1% bca
c    2.803   1% transred
c    2.787   1% decide
c 
c    5.957 < 1% rest (below)
c 
c    2.292   0% block
c    1.358   0% gauss
c    1.134   0% ternres
c    0.790   0% quatres
c    0.382   0% card
c    0.000   0% locs
c    0.000   0% queuesort
c ==================================
c    4.488   1% preprocessing     3%
c  171.716  35% inprocessing     97%
c ==================================
c  176.204  36% simplifying
c  310.024  64% search
c ==================================
c  486.245 100% all
c 
c        507398 conflicts,        1043.5 confs/sec
c          1970 ternaries,         257.6 confs/ternary
c          2177 binaries,          233.1 confs/binary
c           305 iterations,       1663.6 confs/iteration
c 
c            10 reductions,          0.0 redus/sec,  50739.8 confs/reduction
c          7627 restarts,           15.7 rests/sec,     66.5 confs/restart
c       4491883 decisions,        9237.9 decis/sec,      8.9 decis/conflict
c    1205605871 propagations,  2479421.8 props/sec,    268.4 props/decision
c 
c 486.2 seconds, 97.4 MB
c launch: done
