c launch: /data/cnf/sc2014/app/ACG-15-10p0.cnf.bz2
c host: atom28
c Lingeling SAT Solver
c 
c Version b7ztzu 7b29300825af9bcc1c8b2c5ebcf65fa1cb101cad
c 
c Copyright (C) 2010-2014 Armin Biere JKU Linz Austria.
c All rights reserved.
c 
c released Sun Apr 26 19:26:13 CEST 2015
c compiled Sun Apr 26 19:26:13 CEST 2015
c 
c gcc (Ubuntu 4.8.2-19ubuntu1) 4.8.2
c -Wall -O3 -I../yalsat -I../druplig -DNLGLOG -DNDEBUG -DNCHKSOL
c Linux cluster2 3.13.0-45-generic x86_64
c 
c piping '/data/cnf/sc2014/app/ACG-15-10p0.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/ACG-15-10p0.cnf.bz2
c no embedded options
c found 'p cnf 262253 1131732' header
c read 262253 variables, 1131732 clauses, 2644763 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 252004 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  252004  1120813         0       0      0     0    0     0   61   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 5064 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] 5064 out of 5064 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 54025 variables
c [simpleprobe-1] all 208228 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 417 variables
c [simpleprobe-1] fully completed simple probing
c [simpleprobe-1] removed 417 variables, found 11185 hbrs, 20 units
c [unhide-1] limit 53492 based on 855883 irredundant clauses
c [unhide-1-1] 6 units, 1919 failed, 14578 tauts, 0 hbrs, 5999 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 200713 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 59076 not tried 29% in round 1
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 85192 = 42% variables out of 200713 scheduled
c [elim-1] considered successful since not run to completion yet
c [phase-count-1] 676017 negative 99.3% of 680813 except 4796 0.7%
c [phase-count-1] 547738 positive 80.5% of 680813 except 133075 19.5%
c [phase-count-1] less non-negative clauses 4796 than limit 68000 (10.0%)
c [phase-count-1] non-pos/non-neg = 133075/4796 = 27.75 >= 2.00 = 200/100
c [lucky-phase-1] forcing lucky phase -1
c [phase-1] phase bias: 0 positive 0%, 115521 negative 100%
c [sort-queue-1] sorted 115521 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 115521 (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 98588 variables 46.0% (115521 remain 46%)
c [simplification-1] removed 440000 irredundant clauses 39.3% (680813 remain 61%)
c [simplification-1] maximum reduction of 46% = max (46%, 39%)
c [simplification-1] large reduction 46% >= 5% limit
c [simplification-1] next conflict interval 1000 = 2000/2
c [simplification-1] penalized conflict interval 1000 = 1 * 1000
c [simplification-1] hard conflict limit 11000 (soft 1000 + delta 10000)
c [simplification-1] new conflict limit 1000 (hard 11000)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i    5.5  115520   680813        77      66      3  5529    0     8   51   3%      0    8    4    0 22444%
c i    5.5  115087   680813       100      84      6  5530    0    10   51   3%      0   10    4    0 20872%
c i    6.2  115075   680813       516     422     22  5539    4    31   51  12%      1   31   27    0 10819%
c i    6.2  115061   680813       538     433     24  5547    4    34   51  11%      1   33   25    0 10018%
c i    6.4  114949   680813       584     471     28  5549    4    40   51  10%      1   40   27    0 9923%
c i    7.0  114916   680813       753     625     31  5553    7    78   51   9%      1   78   56    0 11871%
c i    7.4  114883   680813       867     726     36  5557   10   108   52   9%      1  107   78    1 11767%
c 
c [simplification-2] limit 1000 conflicts (hard 11000) hit after 1000 conflicts
c [decomp-3] removed 736 variables
c [simpleprobe-2] all 114785 free variables schedulable
c [simpleprobe-2] limit 2132271 penalty 0 = 0 + 0
c [decomp-4] removed 645 variables
c [simpleprobe-2] 85186 variables remain 75% (28954 retained 25%)
c [simpleprobe-2] removed 645 variables, found 2992 hbrs, 102 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 83428 literals 37%
c [treelook-1] scheduling used 413898 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 576820 steps
c [treelook-1] 83424 literals remain 37%
c [treelook-1] 82262 variables remain to probed next time 72%
c [decomp-5] removed 2 variables
c [treelook-1] removed 2 variables, found 4703 hbrs
c [basicprobe-1] limit 5376672 based on 672084 irredundant clauses
c [basicprobe-1-0] 33504 probes remain 30% after last round
c [basicprobe-1-0] 22 units = 22 failed (100%) + 0 lifted (0%)
c [basicprobe-1-0] removed 3155 variables, found 16679 hbrs
c [unhide-2] limit 106613 with penalty 0 = 0 + 0
c [unhide-2-2] 0 units, 2055 failed, 2697 tauts, 0 hbrs, 24400 literals
c [elim-2] 55095 variables 52% will be scheduled this time
c [elim-2] scheduled 55095 variables 52%
c [elim-2] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-2] rescheduling of touched variables disabled
c [elim-2] incomplete 11044 not tried 10% in round 1
c [elim-2] transition to [ all 0 rem 1 ] state
c [elim-2] eliminated 1520 = 3% variables out of 55095 scheduled
c [elim-2] considered successful since not run to completion yet
c [phase-count-2] 600429 negative 99.2% of 605225 except 4796 0.8%
c [phase-count-2] 479874 positive 79.3% of 605225 except 125351 20.7%
c [phase-count-2] less non-negative clauses 4796 than limit 60500 (10.0%)
c [phase-count-2] non-pos/non-neg = 125351/4796 = 26.14 >= 2.00 = 200/100
c [lucky-phase-2] forcing lucky phase -1
c [phase-2] phase bias: 0 positive 0%, 2446 negative 100%
c [sort-queue-2] sorted 79704 enqueued variables after 1000 conflicts
c [score-dist-2] active 25380 (24%), one 0 (0%), zero 79704 (76%)
c [score-dist-2] max exp 508, different 11 (2%)
c [score-dist-2] median active exp 503, avg 503.3
c [simplification-2] removed 9791 variables 8.5% (105084 remain 42%)
c [simplification-2] removed 75588 irredundant clauses 11.1% (605225 remain 54%)
c [simplification-2] maximum reduction of 11% = max (9%, 11%)
c [simplification-2] large reduction 11% >= 5% limit
c [simplification-2] next conflict interval 2000 = 2000/1
c [simplification-2] penalized conflict interval 2000 = 1 * 2000
c [simplification-2] hard conflict limit 13000 (soft 3000 + delta 10000)
c [simplification-2] new conflict limit 3000 (hard 13000)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   11.9  105083   605225      1189     901     47 23049   22   201   47  11%      2  200  126    1 8413%
c i   12.0  104935   605225      1228     928     51 23049   23   210   47  11%      1  209  130    2 8174%
c i   13.3  104118   605225      1639    1200     82 23109   40   272   48  15%      2  269  171    3 6112%
c 
c [simplification-3] limit of 131 binary hit after 131 binaries
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 3603 at-most-one constraints of average size 4.2
c [card-2] no at-most-two constraint found
c [card-2] using previous limit 1000000 for elimination
c [card-2] 3603 out of 3603 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [decomp-6] removed 2139 variables
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] scheduled 78492 literals 38%
c [treelook-2] scheduling used 400218 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] used 539402 steps
c [treelook-2] 78283 literals remain 38%
c [treelook-2] 64093 variables remain to probed next time 62%
c [decomp-7] removed 31 variables
c [treelook-2] removed 208 variables, found 2609 hbrs
c [unhide-3] limit 255396 with penalty 0 = 0 + 0
c [unhide-3-3] 12 units, 824 failed, 8299 tauts, 0 hbrs, 16155 literals
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 101277 variables 100%
c [elim-3] limit of 25539623 steps penalty 0 = 0 + 0
c [elim-3] rescheduling of touched variables disabled
c [elim-3] incomplete 12041 not tried 12% in round 1
c [elim-3] transition to [ all 1 rem 1 ] state
c [elim-3] eliminated 3308 = 3% variables out of 101277 scheduled
c [elim-3] considered successful since not run to completion yet
c [phase-count-3] 564043 negative 99.2% of 568799 except 4756 0.8%
c [phase-count-3] 449318 positive 79.0% of 568799 except 119481 21.0%
c [phase-count-3] less non-negative clauses 4756 than limit 56800 (10.0%)
c [phase-count-3] non-pos/non-neg = 119481/4756 = 25.12 >= 2.00 = 200/100
c [lucky-phase-3] forcing lucky phase -1
c [phase-3] phase bias: 0 positive 0%, 1968 negative 100%
c [sort-queue-3] sorted 65527 enqueued variables after 2335 conflicts
c [score-dist-3] active 32442 (33%), one 0 (0%), zero 65527 (67%)
c [score-dist-3] max exp 509, different 18 (4%)
c [score-dist-3] median active exp 500, avg 500.2
c [simplification-3] removed 5894 variables 5.7% (97969 remain 39%)
c [simplification-3] removed 36426 irredundant clauses 6.0% (568799 remain 51%)
c [simplification-3] maximum reduction of 6% = max (6%, 6%)
c [simplification-3] forced so keeping old conflict interval 0
c [simplification-3] conflict limit remains at 3000 (hard 13000)
c [simplification-3] 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   18.3   97968   568799      2555    1884     93 20268   50   269   47  19%      6  262   61    4 1493%
c i   18.5   97928   568799      2584    1907     95 20270   50   269   47  18%      5  262   57    4 1395%
c i   18.7   97927   568799      2684    1977     96 20270   51   269   47  19%      5  262   78    4 1829%
c i   18.8   97926   568799      2686    1977     96 20270   51   269   47  19%      5  262   77    4 1822%
c i   18.8   97925   568799      2687    1977     96 20270   51   269   47  19%      5  262   77    4 1815%
c i   19.1   97924   568799      2824    2059     97 20270   54   269   47  20%      5  262  101    5 2226%
c i   19.2   97830   568799      2859    2075     97 20270   55   269   47  21%      4  261  114    5 2455%
c 
c [simplification-4] limit 3015 conflicts (hard 13000) hit after 3015 conflicts
c [decomp-8] removed 184 variables
c [basicprobe-2] limit 8346070 penalty 0 = 0 + 0
c [basicprobe-2-0] 30458 probes remain 32% after last round
c [basicprobe-2-0] 30 units = 30 failed (100%) + 0 lifted (0%)
c [basicprobe-2-0] removed 2224 variables, found 16690 hbrs
c [unhide-4] limit 333842 with penalty 0 = 0 + 0
c [unhide-4-4] 7 units, 1052 failed, 4764 tauts, 0 hbrs, 9922 literals
c [elim-4] 10501 variables 11% will be scheduled this time
c [elim-4] scheduled 10501 variables 11%
c [elim-4] boosting limit by 20
c [elim-4] limit of 667685620 steps penalty 0 = 0 + 0
c [elim-4] rescheduling of touched variables disabled
c [elim-4-1] eliminated 3 variables 0% in round 1 in 19317977 steps
c [elim-4-1] backward subsumption/strengthening limit 19317900
c [elim-4-1-1] backward checking 4061 touched variables 4%
c [elim-4-1-1] fully completed backward checking in 1 rounds
c [elim-4-1] subsumed 138 and strengthened 24 clauses in 669664 steps
c [elim-4-1] rescheduled 436 variables 0% by backward subsumption
c [elim-4-2] eliminated 63 variables 0% in round 2 in 242184 steps
c [elim-4-2] backward subsumption/strengthening limit 242100
c [elim-4-2-1] backward checking 467 touched variables 0%
c [elim-4-2-1] fully completed backward checking in 1 rounds
c [elim-4-2] subsumed 37 and strengthened 46 clauses in 222738 steps
c [elim-4-2] rescheduled 219 variables 0% by backward subsumption
c [elim-4-3] eliminated 7 variables 0% in round 3 in 159358 steps
c [elim-4-3] backward subsumption/strengthening limit 159300
c [elim-4-3-1] backward checking 58 touched variables 0%
c [elim-4-3-1] fully completed backward checking in 1 rounds
c [elim-4-3] subsumed 1 and strengthened 0 clauses in 113206 steps
c [elim-4] incomplete 2 not tried 0% in round 3
c [elim-4] transition to [ all 0 rem 1 ] state
c [elim-4] eliminated 73 = 1% variables out of 10501 scheduled
c [elim-4] considered successful since not run to completion yet
c [phase-count-4] 535318 negative 99.1% of 540074 except 4756 0.9%
c [phase-count-4] 424507 positive 78.6% of 540074 except 115567 21.4%
c [phase-count-4] less non-negative clauses 4756 than limit 54000 (10.0%)
c [phase-count-4] non-pos/non-neg = 115567/4756 = 24.30 >= 2.00 = 200/100
c [lucky-phase-4] forcing lucky phase -1
c [phase-4] phase bias: 0 positive 0%, 1408 negative 100%
c [sort-queue-4] sorted 60032 enqueued variables after 3015 conflicts
c [score-dist-4] active 34056 (36%), one 0 (0%), zero 60032 (64%)
c [score-dist-4] max exp 509, different 20 (4%)
c [score-dist-4] median active exp 501, avg 500.8
c [simplification-4] removed 3736 variables 3.8% (94088 remain 37%)
c [simplification-4] removed 28725 irredundant clauses 5.1% (540074 remain 48%)
c [simplification-4] maximum reduction of 5% = max (4%, 5%)
c [simplification-4] large reduction 5% >= 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 15015 (soft 5015 + delta 10000)
c [simplification-4] new conflict limit 5015 (hard 15015)
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.1   94087   540074      3732    2132     96 29641   72   263   46  27%      6  252  134    6 2092%
c i   23.1   94073   540074      3733    2132     96 29641   72   263   46  27%      6  252  134    6 2084%
c i   23.1   94063   540074      3734    2132     96 29641   72   263   46  27%      6  252  133    6 2076%
c i   23.1   94049   540074      3735    2132     96 29641   72   263   46  27%      6  252  133    6 2068%
c i   23.2   94039   540074      3736    2132     96 29641   72   263   46  27%      6  252  132    6 2060%
c i   23.2   94021   540074      3737    2132     96 29641   72   263   46  27%      6  251  132    6 2052%
c i   23.2   94002   540074      3738    2132     96 29641   72   263   46  27%      6  251  131    6 2044%
c i   23.2   93992   540074      3739    2132     96 29641   72   263   46  27%      6  251  131    6 2036%
c i   23.2   93979   540074      3740    2132     96 29641   72   263   46  27%      6  251  130    6 2028%
c i   23.2   93971   540074      3741    2132     96 29641   72   262   46  27%      6  251  130    6 2020%
c 
c [simplification-5] limit of 27 iterations hit after 27 iterations
c [quatres-1] found 33731 quaternary clauses 37% in total
c [quatres-1-2] added 1 single-self-subsuming ternary resolvents
c [quatres-1-2] added 6 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 93957 free variables schedulable
c [ternres-1] 1429 ternary resolvents (8 bin, 1421 trn)
c [ternres-1] fully completed ternary resolution
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 846 xors of average arity 2.1
c [gauss-1] connected 1745 occurrences of 1271 variables (average 1.4)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] fully completed
c [decomp-9] removed 843 variables
c [gauss-1] exported 0 unary, 20 binary and 0 ternary equations
c [decomp-10] removed 2 variables
c [simpleprobe-3] 69280 schedulable variables 74%
c [simpleprobe-3] limit 8359462 penalty 0 = 0 + 0
c [decomp-11] removed 1997 variables
c [simpleprobe-3] 30183 variables remain 33% (60932 retained 67%)
c [simpleprobe-3] removed 1997 variables, found 27822 hbrs, 343 units
c [unhide-5] limit 417973 with penalty 0 = 0 + 0
c [unhide-5-5] 7 units, 270 failed, 8273 tauts, 0 hbrs, 2220 literals
c [transred-1] limit 2000000 with penalty 0 = 0 + 0
c [transred-1] removed 184 transitive binary clauses
c [transred-1] found 4 units
c [block-1] scheduling all variables this time
c [block-1] scheduled 90492 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 9912 blocked clauses
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 12 clauses out of 398 (3%) of length 10
c [cce-1-1] eliminated 89 clauses out of 2137 (4%) of length 9
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 101 large clauses in 30000006 steps
c [cce-1-1] allowing another 15000003 steps for small clauses
c [cce-1-1] scheduling 323391 clauses = 276039 binary + 47352 ternary
c [cce-1-1] tried to eliminate 341 small clauses 0%
c [cce-1-1] eliminated 75 binary clauses 0%
c [cce-1-1] eliminated 11 ternary clauses 0%
c [cce-1-1] eliminated 86 small clauses 0%
c [cce-1-1] eliminated 86 small clauses in 30000003 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 187 covered clauses in round 1
c [cce-1] eliminated 187 covered clauses in TOTAL during 1 rounds
c [cce-1] 187 < 1/100 * 503336 = 5033 considered unsuccessful
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 90492 variables 100%
c [elim-5] limit of 41797312 steps penalty 0 = 0 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5-1] eliminated 2094 variables 2% in round 1 in 41420513 steps
c [elim-5-1] backward subsumption/strengthening limit 376799
c [elim-5-1-1] backward checking 9245 touched variables 10%
c [elim-5-1-1] incomplete backward checking 7520 remain 81%
c [elim-5-1] subsumed 32 and strengthened 5 clauses in 376807 steps
c [elim-5] incomplete 105 not tried 0% in round 1
c [elim-5] transition to [ all 1 rem 1 ] state
c [elim-5] eliminated 2097 = 2% variables out of 90492 scheduled
c [bca-1] limit of 10000000 steps and 999702 added (scaled 2)
c [bca-1] 162166 out of 176792 literals actually usable 92%
c [bca-1] added 224 blocked clauses in 477851 steps
c [sweep-1] limit 1000000 penalty 0 = 0 + 0
c [sweep-1-1] 3517 pos 4.0% + 84878 neg 96.0% = 88395 sched 100.0% ret 0
c [sweep-1-1] 1077431 steps 14 queries 17511.14 avg class size
c [sweep-1-1] 334 decisions 10 SAT calls 119.70 avg env size
c [sweep-1-1] 88179 variables remain 100% (29 retained 0%)
c [decomp-12] removed 229 variables
c [sweep-1-1] removed 229 vars (2 failed, 1 eqs, 3 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 229 vars in TOTAL (1 rounds, 13 queries)
c [phase-count-5] 493514 negative 99.1% of 498247 except 4733 0.9%
c [phase-count-5] 395806 positive 79.4% of 498247 except 102441 20.6%
c [phase-count-5] less non-negative clauses 4733 than limit 49800 (10.0%)
c [phase-count-5] non-pos/non-neg = 102441/4733 = 21.64 >= 2.00 = 200/100
c [lucky-phase-5] forcing lucky phase -1
c [phase-5] phase bias: 0 positive 0%, 1277 negative 100%
c [sort-queue-5] sorted 53248 enqueued variables after 3741 conflicts
c [score-dist-5] active 34918 (40%), one 0 (0%), zero 53248 (60%)
c [score-dist-5] max exp 510, different 24 (5%)
c [score-dist-5] median active exp 500, avg 499.3
c [simplification-5] removed 5791 variables 6.2% (88166 remain 35%)
c [simplification-5] removed 41827 irredundant clauses 7.7% (498247 remain 44%)
c [simplification-5] maximum reduction of 8% = max (6%, 8%)
c [simplification-5] forced so keeping old conflict interval 0
c [simplification-5] conflict limit remains at 5105 (hard 15015)
c [simplification-5] 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   30.4   88165   498247      4209    2281    919 63021   82   260   45  31%      5  247  169    8 2240%
c i   30.7   88155   498247      4314    2319    919 63021   84   259   46  32%      5  246  172    8 2191%
c i   30.7   88147   498247      4315    2319    919 63021   84   259   46  32%      5  246  171    8 2182%
c i   30.7   88138   498247      4316    2319    919 63021   84   259   46  32%      5  246  170    8 2174%
c i   30.7   88125   498247      4317    2319    919 63021   84   259   46  32%      5  246  170    8 2166%
c i   30.7   88115   498247      4319    2319    919 63022   84   259   46  32%      5  246  168    8 2149%
c i   31.5   88103   498247      4691    2513    921 63023   90   256   46  35%      4  241  149    9 1732%
c i   31.5   88086   498247      4693    2513    921 63023   90   256   46  35%      4  241  149    9 1729%
c i   31.5   88085   498247      4694    2513    921 63023   90   256   46  35%      4  241  149    9 1722%
c i   32.1   88084   498247      4976    2669    928 63060   89   249   46  36%      4  234  102    9 1137%
c i   32.1   88072   498247      4977    2669    928 63060   89   249   46  36%      4  234  101    9 1132%
c i   32.1   88065   498247      4978    2669    928 63060   89   249   46  36%      4  233  101    9 1128%
c i   32.1   88050   498247      4987    2673    928 63060   89   249   46  36%      4  233  101    9 1132%
c 
c [simplification-6] limit 5176 conflicts (hard 15015) hit after 5180 conflicts
c [quatres-2] found 33566 quaternary clauses 37% in total
c [quatres-2-2] added 9 quaternary resolvents
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] all 88033 free variables schedulable
c [ternres-2] 317 ternary resolvents (0 bin, 317 trn)
c [ternres-2] 29418 variables remain 33% (58615 retained 67%)
c [card-3] limit 500000 penalty 2 = 2 + 0
c [card-3] found 1859 at-most-one constraints of average size 3.9
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 500000 for elimination
c [card-3] 1859 out of 1859 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [gauss-2] limit 2000000 penalty 0 = 0 + 0
c [gauss-2] extracted 49 xors of average arity 2.7
c [gauss-2] connected 131 occurrences of 106 variables (average 1.2)
c [gauss-2] limit 2000000 penalty 0 = 0 + 0
c [gauss-2] fully completed
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-13] removed 16 variables
c [treelook-3] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-3] scheduled 55185 literals 31%
c [treelook-3] scheduling used 300153 steps
c [treelook-3] not fully scheduled
c [treelook-3] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-3] used 759106 steps
c [treelook-3] 55177 literals remain 31%
c [treelook-3] 42852 variables remain to probed next time 49%
c [treelook-3] removed 0 variables, found 1062 hbrs
c [unhide-6] limit 567321 with penalty 0 = 0 + 0
c [unhide-6-6] 5 units, 381 failed, 3754 tauts, 0 hbrs, 16487 literals
c [transred-2] limit 2000000 with penalty 0 = 0 + 0
c [transred-2] removed 167 transitive binary clauses
c [transred-2] found 7 units
c [block-2] scheduling all variables this time
c [block-2] scheduled 87487 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 612 blocked clauses
c [block-2] 612 < 1/100 * 496681 = 4966 considered unsuccessful
c [elim-6] no untried remaining variables left
c [elim-6] scheduled 87487 variables 100%
c [elim-6] limit of 56732106 steps penalty 0 = 0 + 0
c [elim-6] rescheduling of touched variables disabled
c [elim-6-1] eliminated 840 variables 1% in round 1 in 40263319 steps
c [elim-6-1] backward subsumption/strengthening limit 16468787
c [elim-6-1-1] backward checking 4205 touched variables 5%
c [elim-6-1-1] fully completed backward checking in 1 rounds
c [elim-6-1] subsumed 17 and strengthened 3 clauses in 897810 steps
c [elim-6-1] rescheduled 66 variables 0% by backward subsumption
c [elim-6-2] eliminated 3 variables 0% in round 2 in 34074 steps
c [elim-6-2] backward subsumption/strengthening limit 34000
c [elim-6-2-1] backward checking 26 touched variables 0%
c [elim-6-2-1] incomplete backward checking 0 remain 0%
c [elim-6-2] subsumed 4 and strengthened 2 clauses in 34001 steps
c [elim-6-2] rescheduled 15 variables 0% by backward subsumption
c [elim-6-3] no variable eliminated in round 3 in 11370 steps
c [elim-6] fully completed in 3 rounds
c [elim-6] transition to [ all 0 rem 0 ] state
c [elim-6] eliminated 843 = 1% variables out of 87487 scheduled
c [elim-6] 843 < 1/100 * 87487 = 874 considered unsuccessful
c [bca-2] limit of 10000000 steps and 979444 added (scaled 2)
c [bca-2] 158611 out of 173290 literals actually usable 92%
c [bca-2] added 101 blocked clauses in 470026 steps
c [sweep-2] limit 1000000 penalty 0 = 0 + 0
c [sweep-2-1] 3404 pos 3.9% + 83214 neg 96.1% = 86618 sched 100.0% ret 26
c [sweep-2-1] 1297437 steps 8 queries 30882.50 avg class size
c [sweep-2-1] 22 decisions 4 SAT calls 39.50 avg env size
c [sweep-2-1] 86614 variables remain 100% (30 retained 0%)
c [decomp-15] removed 18 variables
c [sweep-2-1] removed 18 vars (0 failed, 3 eqs, 5 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 18 vars in TOTAL (1 rounds, 7 queries)
c [phase-count-6] 484665 negative 99.0% of 489384 except 4719 1.0%
c [phase-count-6] 387179 positive 79.1% of 489384 except 102205 20.9%
c [phase-count-6] less non-negative clauses 4719 than limit 48900 (10.0%)
c [phase-count-6] non-pos/non-neg = 102205/4719 = 21.66 >= 2.00 = 200/100
c [lucky-phase-6] forcing lucky phase -1
c [phase-6] phase bias: 0 positive 0%, 1015 negative 100%
c [sort-queue-6] sorted 51160 enqueued variables after 5180 conflicts
c [score-dist-6] active 35466 (41%), one 0 (0%), zero 51160 (59%)
c [score-dist-6] max exp 509, different 29 (6%)
c [score-dist-6] median active exp 495, avg 495.3
c [simplification-6] removed 1407 variables 1.6% (86626 remain 34%)
c [simplification-6] removed 8863 irredundant clauses 1.8% (489384 remain 44%)
c [simplification-6] maximum reduction of 2% = max (2%, 2%)
c [simplification-6] geometric conflict interval increment 6666 = 20000 / 3
c [simplification-6] new conflict interval 6666
c [simplification-6] penalized conflict interval 6666 = 1 * 6666
c [simplification-6] hard conflict limit 21846 (soft 11846 + delta 10000)
c [simplification-6] new conflict limit 11846 (hard 21846)
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   37.0   86625   489384      5183    2720   1024 60290   89   245   44  36%      3  229   95    9 1031%
c i   37.0   86605   489384      5188    2724   1024 60290   89   245   45  36%      3  228   94    9 1022%
c i   37.6   86593   489384      5478    2964   1026 60292   87   236   46  37%      3  218   72    9  766%
c i   37.8   86579   489384      5542    3025   1027 60292   87   233   46  37%      3  216   63    9  668%
c i   37.8   86578   489384      5543    3025   1027 60292   87   233   46  37%      3  216   63    9  665%
c i   37.8   86577   489384      5544    3025   1027 60292   86   233   46  37%      3  215   63    9  663%
c i   37.8   86576   489384      5545    3025   1027 60292   86   233   46  37%      3  215   62    9  660%
c i   40.6   86575   489384      6820    4221   1037 60296   72   186   50  39%      9  164   34   10  347%
c i   43.1   86574   489384      7866    5123   1042 60303   71   165   54  43%      9  141   72   11  671%
c i   44.3   86567   489384      8384    5524   1050 60310   75   166   56  45%      7  141  134   12 1167%
c i   44.4   86555   489384      8444    5547   1050 60310   77   168   56  46%      7  143  159   12 1359%
c i   44.5   86554   489384      8476    5563   1050 60311   79   169   56  47%      6  144  166   12 1407%
c i   44.7   86384   489384      8545    5579   1050 60311   81   171   56  48%      6  145  187   12 1551%
c i   44.7   86383   489384      8548    5581   1050 60311   81   171   56  48%      6  145  186   12 1542%
c i   44.7   86367   489384      8559    5586   1050 60311   82   171   56  48%      6  146  187   12 1545%
c i   46.3   86353   489384      9236    5996   1080 60335   98   200   56  49%      6  173  191   14 1371%
c i   46.3   86300   489384      9258    6015   1080 60335   98   200   56  49%      5  173  192   14 1371%
c i   46.9   86209   489384      9615    6274   1082 60338   99   204   58  49%      4  176  130   14  898%
c i   47.0   86200   489384      9633    6287   1082 60338   99   204   58  49%      4  176  130   14  894%
c i   47.5   86199   489384      9905    6513   1083 60340   98   213   58  46%      4  184  104   15  706%
c i   48.2   86198   489384     10187    6705   1083 60340  110   227   58  48%      3  198  237   16 1495%
c i   48.2   86197   489384     10188    6705   1083 60340  110   227   58  48%      3  198  236   16 1489%
c 
c [simplification-7] limit 11891 conflicts (hard 21846) hit after 11893 conflicts
c [quatres-3] found 32553 quaternary clauses 37% in total
c [quatres-3-2] added 1 single-self-subsuming ternary resolvents
c [quatres-3-2] added 6 quaternary resolvents
c [ternres-3] limit 6307929 with penalty 0 = 0 + 0
c [ternres-3] 28796 schedulable variables 33%
c [ternres-3] 1140 ternary resolvents (2 bin, 1138 trn)
c [ternres-3] fully completed ternary resolution
c [decomp-16] removed 495 variables
c [basicprobe-3] limit 31539649 penalty 0 = 0 + 0
c [basicprobe-3-0] 28215 probes remain 33% after last round
c [basicprobe-3-0] 100 units = 100 failed (100%) + 0 lifted (0%)
c [basicprobe-3-0] removed 1725 variables, found 38977 hbrs
c [bate-1] eliminated 59 asymmetric tautologies during probing
c [unhide-7] limit 630792 with penalty 1 = 0 + 1
c [unhide-7-7] 7 units, 108 failed, 5636 tauts, 0 hbrs, 229216 literals
c [transred-3] limit 2000000 with penalty 0 = 0 + 0
c [transred-3] removed 157 transitive binary clauses
c [cce-2] limit of 15769824 steps penalty 1 = 1 + 0
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] allowing another 7884914 steps for small clauses
c [cce-2-1] scheduling 338158 clauses = 255277 binary + 82881 ternary
c [cce-2-1] tried to eliminate 216 small clauses 0%
c [cce-2-1] eliminated 43 binary clauses 0%
c [cce-2-1] eliminated 43 ternary clauses 0%
c [cce-2-1] eliminated 86 small clauses 0%
c [cce-2-1] eliminated 1894 small clauses in 15769826 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 1894 covered clauses in round 1
c [cce-2] eliminated 1894 covered clauses in TOTAL during 1 rounds
c [cce-2] 1894 < 1/100 * 472004 = 4720 considered unsuccessful
c [bca-3] limit of 10000000 steps and 940882 added (scaled 2)
c [bca-3] 150442 out of 168370 literals actually usable 89%
c [bca-3] added 45 blocked clauses in 434283 steps
c [sweep-3] limit 1892378 penalty 0 = 0 + 0
c [sweep-3-1] 3282 pos 3.9% + 80875 neg 96.1% = 84157 sched 100.0% ret 27
c [sweep-3-1] 2330720 steps 17 queries 11899.35 avg class size
c [sweep-3-1] 77 decisions 14 SAT calls 72.07 avg env size
c [sweep-3-1] 84049 variables remain 100% (126 retained 0%)
c [decomp-17] removed 255 variables
c [sweep-3-1] removed 255 vars (0 failed, 2 eqs, 3 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 255 vars in TOTAL (1 rounds, 16 queries)
c [phase-count-7] 464821 negative 99.0% of 469540 except 4719 1.0%
c [phase-count-7] 371988 positive 79.2% of 469540 except 97552 20.8%
c [phase-count-7] less non-negative clauses 4719 than limit 46900 (10.0%)
c [phase-count-7] non-pos/non-neg = 97552/4719 = 20.67 >= 2.00 = 200/100
c [lucky-phase-7] forcing lucky phase -1
c [phase-7] phase bias: 0 positive 0%, 705 negative 100%
c [sort-queue-7] sorted 46402 enqueued variables after 11893 conflicts
c [score-dist-7] active 37527 (45%), one 0 (0%), zero 46402 (55%)
c [score-dist-7] max exp 510, different 56 (11%)
c [score-dist-7] median active exp 492, avg 487.7
c [simplification-7] removed 2268 variables 2.6% (83929 remain 33%)
c [simplification-7] removed 19844 irredundant clauses 4.1% (469540 remain 42%)
c [simplification-7] maximum reduction of 4% = max (3%, 4%)
c [simplification-7] geometric conflict interval increment 4000 = 20000 / 5
c [simplification-7] new conflict interval 10666
c [simplification-7] penalized conflict interval 10666 = 1 * 10666
c [simplification-7] hard conflict limit 32559 (soft 22559 + delta 10000)
c [simplification-7] new conflict limit 22559 (hard 32559)
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   56.7   83928   469540     12062    7999   1760 96915  139   253   64  55%     16  217  159   21  761%
c i   56.7   83927   469540     12063    7999   1760 96915  139   253   64  55%     16  217  158   21  758%
c i   56.7   83926   469540     12064    7999   1760 96915  139   253   64  55%     16  217  158   21  755%
c i   60.9   83925   469540     13870    9099   1761 96919  146   236   65  62%     17  195  116   25  470%
c i   60.9   83924   469540     13874    9102   1761 96919  146   236   65  62%     16  195  114   25  464%
c i   60.9   83921   469540     13875    9102   1761 96919  146   236   65  62%     16  195  114   25  462%
c i   62.9   83920   469540     15032    9930   1770 96972  147   270   65  55%     12  224  173   27  647%
c i   62.9   83919   469540     15033    9930   1770 96972  147   269   65  55%     12  224  173   27  644%
c i   62.9   83913   469540     15036    9932   1770 96972  147   269   65  55%     11  224  173   27  644%
c i   62.9   83906   469540     15037    9932   1770 96972  147   269   65  55%     11  224  172   27  641%
c i   63.0   83905   469540     15121    9982   1771 96975  148   270   65  55%     10  224  174   27  646%
c i   63.5   83897   469540     15331   10065   1773 96983  154   274   67  56%      9  228  232   28  835%
c i   63.5   83896   469540     15332   10065   1773 96983  154   274   67  56%      9  228  231   28  832%
c i   63.5   83895   469540     15333   10065   1773 96983  154   274   67  56%      9  228  230   28  829%
c i   63.5   83890   469540     15334   10065   1773 96983  154   274   67  56%      9  228  229   28  826%
c i   63.5   83885   469540     15335   10065   1773 96983  154   274   67  56%      9  228  228   28  822%
c i   63.5   83884   469540     15336   10065   1773 96983  154   274   67  56%      9  228  228   28  819%
c i   63.5   83883   469540     15337   10065   1773 96983  154   274   67  56%      9  227  227   28  816%
c i   63.5   83882   469540     15338   10065   1773 96983  154   274   67  56%      8  227  226   28  813%
c i   63.5   83881   469540     15357   10080   1773 96984  153   274   67  56%      8  228  217   28  782%
c i   63.7   83865   469540     15403   10105   1773 96984  154   276   67  56%      8  229  216   28  774%
c i   63.7   83864   469540     15406   10105   1773 96984  154   276   67  56%      8  229  217   28  776%
c i   63.7   83863   469540     15407   10105   1773 96984  154   275   67  56%      8  229  216   28  773%
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.7   83862   469540     15412   10105   1773 96984  154   275   67  56%      8  229  218   28  779%
c i   66.8   83861   469540     16650   10926   1781 97016  158   278   68  57%      9  228  168   31  549%
c i   66.9   83860   469540     16658   10932   1781 97016  158   279   68  57%      9  228  165   31  539%
c i   66.9   83859   469540     16659   10932   1781 97016  158   278   68  57%      9  228  164   31  537%
c i   66.9   83858   469540     16660   10932   1781 97016  158   278   68  57%      9  228  164   31  535%
c i   66.9   83857   469540     16661   10932   1781 97016  158   278   68  57%      9  227  163   31  533%
c i   66.9   83856   469540     16662   10932   1781 97016  157   278   68  57%      9  227  162   31  531%
c i   66.9   83855   469540     16663   10932   1781 97016  157   278   68  57%      9  227  162   31  529%
c i   66.9   83854   469540     16664   10932   1781 97016  157   278   68  57%      9  227  161   31  527%
c i   66.9   83853   469540     16665   10932   1781 97016  157   278   68  57%      9  227  160   31  524%
c i   66.9   83852   469540     16666   10932   1781 97016  157   278   68  57%      9  227  160   31  522%
c i   66.9   83851   469540     16667   10932   1781 97016  157   278   68  57%      9  227  159   31  520%
c i   66.9   83850   469540     16668   10932   1781 97016  157   278   68  57%      9  227  159   31  518%
c i   66.9   83849   469540     16669   10932   1781 97016  157   278   68  57%      9  227  158   31  516%
c i   66.9   83833   469540     16670   10932   1781 97016  157   278   68  57%      9  227  157   31  514%
c i   67.0   83832   469540     16687   10946   1781 97016  157   278   68  57%      9  227  157   31  513%
c i   67.9   83831   469540     17081   11223   1785 97018  158   278   68  57%      7  225  145   31  460%
c i   68.8   83817   469540     17502   11591   1786 97020  154   272   68  56%      5  219  149   32  465%
c i   69.3   83816   469540     17764   11743   1787 97020  161   279   68  58%      4  225  226   33  687%
c i   69.4   83815   469540     17806   11761   1788 97022  161   281   68  57%      4  226  224   33  680%
c i   69.4   83814   469540     17807   11761   1788 97022  161   281   68  57%      4  226  224   33  677%
c i   69.5   83813   469540     17808   11761   1788 97022  161   281   68  57%      4  226  223   33  675%
c i   69.5   83812   469540     17809   11761   1788 97022  161   281   68  57%      4  226  222   33  672%
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   69.5   83811   469540     17810   11761   1788 97022  161   281   68  57%      4  226  221   33  670%
c i   69.5   83810   469540     17811   11761   1788 97022  161   280   68  57%      4  226  220   33  667%
c i   69.5   83809   469540     17812   11761   1788 97022  161   280   68  57%      4  226  219   33  664%
c i   69.5   83808   469540     17813   11761   1788 97022  161   280   68  57%      4  226  218   33  662%
c i   69.5   83807   469540     17814   11761   1788 97022  161   280   68  57%      4  226  218   33  659%
c i   69.5   83806   469540     17815   11761   1788 97022  161   280   68  57%      4  225  217   33  657%
c i   69.5   83805   469540     17816   11761   1788 97022  161   280   68  57%      4  225  216   33  654%
c i   69.6   83804   469540     17842   11780   1789 97022  161   281   68  57%      3  226  215   33  649%
c i   69.6   83803   469540     17843   11780   1789 97022  161   281   68  57%      3  226  214   33  647%
c i   69.7   83766   469540     17880   11801   1789 97023  162   283   68  57%      3  228  218   33  658%
c i   70.9   83759   469540     18327   12139   1790 97023  170   299   68  57%      3  243  250   35  722%
c i   70.9   83758   469540     18330   12141   1790 97023  170   299   68  57%      3  243  247   35  714%
c i   70.9   83757   469540     18331   12141   1790 97023  170   299   68  57%      3  243  246   35  711%
c i   72.1   83756   469540     18890   12514   1790 97024  173   305   68  57%      3  246  194   36  540%
c i   72.1   83755   469540     18892   12515   1790 97024  173   305   68  57%      3  246  193   36  536%
c i   73.1   83754   469540     19331   12825   1795 97033  177   316   73  56%      3  256  220   37  594%
c i   73.1   83753   469540     19334   12827   1795 97033  177   316   73  56%      3  256  220   37  592%
c i   77.9   83752   469540     21067   13886   1796 97087  167   285   73  58%     13  219  133   40  334%
c i   78.7   83751   469540     21339   14009   1804 97093  170   286   73  59%     10  219  197   41  483%
c i   79.1   83745   469540     21470   14073   1806 97093  171   288   73  59%      9  220  203   41  495%
c i   79.1   83741   469540     21490   14073   1806 97094  171   287   73  60%      8  219  205   41  500%
c i   79.9   83740   469540     21744   14208   1806 97094  172   285   73  61%      7  216  187   42  450%
c i   80.1   83739   469540     21864   14291   1806 97094  171   283   73  61%      6  214  171   42  409%
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   81.0   83738   469540     22200   14432   1806 97094  172   278   73  62%      4  208  175   43  412%
c i   82.9   83698   469540     22894   14797   1808 97096  170   269   73  63%      4  197  178   44  407%
c 
c [simplification-8] limit 22951 conflicts (hard 32559) hit after 22951 conflicts
c [quatres-4] found 34436 quaternary clauses 40% in total
c [quatres-4-2] added 1 single-self-subsuming ternary resolvents
c [ternres-4] limit 12566894 with penalty 0 = 0 + 0
c [ternres-4] all 83690 free variables schedulable
c [ternres-4] 261 ternary resolvents (0 bin, 261 trn)
c [ternres-4] fully completed ternary resolution
c [gauss-3] limit 1256689 penalty 1 = 1 + 0
c [gauss-3] extracted 36 xors of average arity 2.9
c [gauss-3] connected 103 occurrences of 72 variables (average 1.4)
c [gauss-3] limit 1256689 penalty 1 = 1 + 0
c [gauss-3] fully completed
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-18] removed 11 variables
c [simpleprobe-4] 27353 schedulable variables 33%
c [simpleprobe-4] limit 50267577 penalty 0 = 0 + 0
c [decomp-19] removed 1185 variables
c [simpleprobe-4] fully completed simple probing
c [simpleprobe-4] removed 1185 variables, found 35135 hbrs, 231 units
c [unhide-8] limit 1256689 with penalty 1 = 0 + 1
c [unhide-8-8] 1 units, 250 failed, 10301 tauts, 0 hbrs, 266867 literals
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 129 transitive binary clauses
c [transred-4] found 1 units
c [block-3] scheduling all variables this time
c [block-3] scheduled 82052 variables 100%
c [block-3] limit of 62834471 steps penalty 1 = 1 + 0
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 36 blocked clauses
c [block-3] 36 < 1/100 * 460401 = 4604 considered unsuccessful
c [elim-7] scheduling all variables this time
c [elim-7] scheduled 82052 variables 100%
c [elim-7] limit of 125668942 steps penalty 1 = 1 + 0
c [elim-7] rescheduling of touched variables disabled
c [elim-7-1] eliminated 1434 variables 2% in round 1 in 37156645 steps
c [elim-7-1] backward subsumption/strengthening limit 37156600
c [elim-7-1-1] backward checking 6422 touched variables 8%
c [elim-7-1-1] fully completed backward checking in 1 rounds
c [elim-7-1] subsumed 42 and strengthened 67 clauses in 1485321 steps
c [elim-7-1] rescheduled 279 variables 0% by backward subsumption
c [elim-7-2] eliminated 24 variables 0% in round 2 in 215687 steps
c [elim-7-2] backward subsumption/strengthening limit 215600
c [elim-7-2-1] backward checking 197 touched variables 0%
c [elim-7-2-1] fully completed backward checking in 1 rounds
c [elim-7-2] subsumed 5 and strengthened 4 clauses in 163584 steps
c [elim-7-2] rescheduled 27 variables 0% by backward subsumption
c [elim-7-3] no variable eliminated in round 3 in 19958 steps
c [elim-7] fully completed in 3 rounds
c [elim-7] transition to [ all 0 rem 0 ] state
c [elim-7] eliminated 1458 = 2% variables out of 82052 scheduled
c [bca-4] limit of 10000000 steps and 906881 added (scaled 2)
c [bca-4] 142708 out of 161190 literals actually usable 89%
c [bca-4] added 88 blocked clauses in 423984 steps
c [sweep-4] limit 3770068 penalty 0 = 0 + 0
c [sweep-4-1] 2866 pos 3.6% + 77620 neg 96.4% = 80486 sched 99.9% ret 108
c [sweep-4-1] 3977525 steps 42 queries 10256.31 avg class size
c [sweep-4-1] 437 decisions 28 SAT calls 228.50 avg env size
c [sweep-4-1] 80287 variables remain 100% (296 retained 0%)
c [decomp-20] removed 31 variables
c [sweep-4-1] removed 31 vars (0 failed, 14 eqs, 27 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 31 vars in TOTAL (1 rounds, 41 queries)
c [phase-count-8] 448301 negative 99.0% of 453034 except 4733 1.0%
c [phase-count-8] 355964 positive 78.6% of 453034 except 97070 21.4%
c [phase-count-8] less non-negative clauses 4733 than limit 45300 (10.0%)
c [phase-count-8] non-pos/non-neg = 97070/4733 = 20.51 >= 2.00 = 200/100
c [lucky-phase-8] forcing lucky phase -1
c [phase-8] phase bias: 0 positive 0%, 369 negative 100%
c [sort-queue-8] sorted 38870 enqueued variables after 22951 conflicts
c [score-dist-8] active 41693 (52%), one 0 (0%), zero 38870 (48%)
c [score-dist-8] max exp 510, different 98 (19%)
c [score-dist-8] median active exp 497, avg 481.7
c [simplification-8] removed 3127 variables 3.7% (80563 remain 32%)
c [simplification-8] removed 16506 irredundant clauses 3.5% (453034 remain 40%)
c [simplification-8] maximum reduction of 4% = max (4%, 4%)
c [simplification-8] geometric conflict interval increment 4000 = 20000 / 5
c [simplification-8] new conflict interval 14666
c [simplification-8] penalized conflict interval 14666 = 1 * 14666
c [simplification-8] hard conflict limit 47617 (soft 37617 + delta 10000)
c [simplification-8] new conflict limit 37617 (hard 47617)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   90.9   80562   453034     23602   11346   1417 118845  172   274   58  63%      4  200  182   45  401%
c i   91.0   80561   453034     23642   11375   1417 118845  173   274   58  63%      4  200  183   45  403%
c i   91.1   80560   453034     23652   11378   1417 118845  173   274   58  63%      4  200  185   45  407%
c i   91.1   80559   453034     23653   11378   1417 118845  173   274   58  63%      4  199  184   45  406%
c i   91.1   80558   453034     23654   11378   1417 118845  173   274   58  63%      4  199  183   45  404%
c i   91.3   80557   453034     23764   11411   1418 118845  175   274   58  64%      3  199  210   46  459%
c i   91.8   80556   453034     23954   11505   1418 118845  176   273   58  64%      3  198  205   46  444%
c i   92.2   80543   453034     24064   11553   1418 118846  177   272   58  65%      2  196  200   46  430%
c i   92.2   80542   453034     24065   11553   1418 118846  177   272   58  65%      2  196  199   46  428%
c i   92.2   80541   453034     24068   11553   1418 118848  176   272   58  65%      2  196  196   46  423%
c i   92.2   80540   453034     24069   11553   1418 118848  176   272   58  65%      2  196  196   46  422%
c i   92.2   80539   453034     24070   11553   1418 118848  176   272   58  65%      2  196  195   46  420%
c i   92.2   80538   453034     24071   11553   1418 118848  176   272   58  65%      2  196  194   46  419%
c i   92.3   80537   453034     24134   11592   1421 118856  175   272   58  64%      2  196  176   46  378%
c i   93.7   80536   453034     24781   11994   1434 118879  187   292   59  64%      3  214  312   48  644%
c i   93.8   80535   453034     24782   11994   1434 118879  187   292   59  64%      3  214  311   48  642%
c i   93.8   80534   453034     24786   11997   1434 118879  187   292   59  64%      3  214  307   48  633%
c i   93.8   80533   453034     24806   12008   1434 118879  188   293   59  64%      3  215  312   49  644%
c i   93.8   80532   453034     24807   12008   1434 118879  188   293   59  64%      2  215  311   49  641%
c i   93.8   80531   453034     24808   12008   1434 118879  188   293   59  64%      2  215  310   49  639%
c i   93.8   80530   453034     24809   12008   1434 118879  188   293   59  64%      2  215  309   49  636%
c i   93.9   80529   453034     24820   12012   1434 118879  188   293   59  64%      2  215  311   49  640%
c i   93.9   80528   453034     24821   12012   1434 118879  188   293   59  64%      2  215  310   49  638%
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   94.6   80527   453034     25054   12076   1435 118879  203   304   59  67%      2  225  395   50  789%
c i   94.6   80526   453034     25082   12078   1435 118879  204   305   59  67%      2  226  398   50  794%
c i   95.1   80525   453034     25280   12186   1435 118879  210   313   59  67%      1  233  346   51  679%
c i   95.1   80524   453034     25284   12188   1435 118880  210   313   59  67%      1  233  344   51  675%
c i   95.2   80523   453034     25301   12200   1435 118881  210   314   59  67%      1  234  340   51  667%
c i   96.1   80518   453034     25699   12369   1436 118882  219   324   63  68%      1  243  293   53  557%
c i   96.1   80517   453034     25700   12369   1436 118882  219   324   63  68%      1  242  292   53  555%
c i   96.2   80516   453034     25701   12369   1436 118882  219   324   63  68%      1  242  291   53  553%
c i   96.3   80515   453034     25786   12439   1436 118882  218   325   63  67%      1  244  255   53  483%
c i   96.5   80382   453034     25882   12502   1436 118882  217   327   63  66%      1  245  235   53  444%
c i   96.8   80381   453034     25997   12561   1436 118882  218   327   63  67%      1  245  248   53  465%
c i   96.8   80380   453034     25998   12561   1436 118882  218   327   63  67%      1  245  247   53  463%
c i   97.0   80379   453034     26072   12614   1437 118882  219   328   63  67%      0  245  246   54  459%
c i   97.0   80378   453034     26073   12614   1437 118882  219   327   63  67%      0  245  245   54  457%
c i   97.6   80377   453034     26378   12804   1438 118882  218   333   63  66%      0  249  220   54  405%
c i   99.3   80370   453034     27170   13309   1443 118886  228   356   63  64%      3  269  263   57  462%
c i   99.5   80369   453034     27239   13365   1443 118887  227   358   63  64%      2  271  246   57  432%
c i  101.4   80368   453034     28211   14023   1449 118890  220   354   63  62%      5  263  189   59  320%
c i  101.5   80367   453034     28213   14023   1449 118891  220   354   63  62%      5  263  187   59  317%
c i  101.5   80366   453034     28215   14023   1449 118892  220   354   63  62%      5  263  186   59  315%
c i  102.1   80365   453034     28491   14185   1453 118901  218   351   63  62%      4  259  192   60  323%
c i  102.1   80364   453034     28492   14185   1453 118901  218   351   63  62%      4  259  191   60  321%
c i  102.1   80354   453034     28493   14185   1453 118901  218   351   63  62%      4  259  191   60  320%
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i  102.1   80348   453034     28494   14185   1453 118901  218   351   63  62%      4  258  190   60  319%
c i  102.1   80342   453034     28495   14185   1453 118901  218   351   63  62%      4  258  189   60  318%
c i  102.1   80336   453034     28496   14185   1453 118901  218   351   63  62%      4  258  188   60  316%
c i  102.1   80332   453034     28497   14185   1453 118901  218   350   63  62%      4  258  188   60  315%
c i  102.1   80323   453034     28498   14185   1453 118901  218   350   63  62%      4  258  187   60  314%
c i  102.4   80314   453034     28600   14246   1453 118901  219   350   63  62%      3  258  211   60  352%
c i  102.4   80300   453034     28606   14247   1453 118901  219   350   63  63%      3  257  211   60  352%
c i  102.4   80291   453034     28607   14247   1453 118901  219   350   63  63%      3  257  210   60  351%
c i  102.4   80277   453034     28608   14247   1453 118901  219   350   63  63%      3  257  209   60  349%
c i  102.4   80264   453034     28609   14247   1453 118901  219   350   63  63%      3  257  208   60  348%
c i  102.4   80255   453034     28610   14247   1453 118901  219   350   63  63%      3  257  207   60  346%
c i  102.4   80254   453034     28611   14247   1453 118901  219   350   63  63%      3  257  207   60  345%
c i  102.4   80238   453034     28612   14247   1453 118901  219   350   63  63%      3  257  206   60  344%
c i  102.4   80224   453034     28613   14247   1453 118901  219   350   63  63%      3  257  205   60  342%
c i  102.4   80207   453034     28614   14247   1453 118901  218   349   63  63%      3  257  204   60  341%
c i  102.4   80191   453034     28615   14247   1453 118901  218   349   63  63%      3  257  203   60  340%
c i  104.4   80176   453034     29566   14826   1456 118911  212   344   63  62%      5  248  188   62  304%
c i  106.0   80175   453034     30334   15433   1459 118914  192   319   63  60%      5  220   58   62   94%
c i  106.0   80174   453034     30335   15433   1459 118914  192   319   63  60%      5  220   58   62   93%
c i  106.7   80173   453034     30766   15785   1459 118920  175   293   63  60%      3  192   34   62   55%
c i  108.3   80172   453034     31667   16463   1461 118920  156   258   65  60%      5  156   98   62  158%
c i  108.3   80171   453034     31668   16463   1461 118920  156   258   65  60%      5  156   97   62  157%
c i  108.4   80170   453034     31740   16518   1461 118920  155   257   65  60%      4  154   96   62  155%
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i  108.9   80159   453034     31936   16655   1464 118920  151   252   65  60%      3  149   85   62  137%
c i  108.9   80158   453034     31937   16655   1464 118920  151   252   65  60%      3  148   85   62  137%
c i  108.9   80157   453034     31938   16655   1464 118920  151   252   65  60%      3  148   85   62  136%
c i  110.1   80156   453034     32668   17263   1466 118921  135   225   65  60%      4  120   66   62  106%
c i  110.3   80155   453034     32772   17343   1466 118921  134   224   65  60%      3  119   75   62  121%
c i  111.2   80147   453034     33320   17822   1469 118921  124   209   65  59%      3  103   57   62   92%
c i  120.2   80146   453034     37980   21212   1474 118938  118   191   70  62%     53   79  173   65  265%
c 
c [simplification-9] limit 37986 conflicts (hard 47617) hit after 37989 conflicts
c [quatres-5] found 32357 quaternary clauses 39% in total
c [quatres-5-2] added 5 quaternary resolvents
c [ternres-5] limit 20030775 with penalty 0 = 0 + 0
c [ternres-5] all 80146 free variables schedulable
c [ternres-5] 751 ternary resolvents (0 bin, 751 trn)
c [ternres-5] fully completed ternary resolution
c [decomp-21] removed 438 variables
c [unhide-9] limit 2003077 with penalty 1 = 0 + 1
c [unhide-9-9] 5 units, 47 failed, 3615 tauts, 0 hbrs, 90701 literals
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 157 transitive binary clauses
c [transred-5] found 3 units
c [elim-8] scheduling all variables this time
c [elim-8] scheduled 79995 variables 100%
c [elim-8] boosting limit by 20
c [elim-8] limit of 8012310100 steps penalty 0 = 0 + 0
c [elim-8] rescheduling of touched variables disabled
c [elim-8-1] eliminated 888 variables 1% in round 1 in 36302788 steps
c [elim-8-1] backward subsumption/strengthening limit 36302700
c [elim-8-1-1] backward checking 3832 touched variables 5%
c [elim-8-1-1] fully completed backward checking in 1 rounds
c [elim-8-1] subsumed 8 and strengthened 2 clauses in 1159319 steps
c [elim-8-1] rescheduled 32 variables 0% by backward subsumption
c [elim-8-2] eliminated 1 variables 0% in round 2 in 21097 steps
c [elim-8-2] backward subsumption/strengthening limit 21000
c [elim-8-2-1] backward checking 11 touched variables 0%
c [elim-8-2-1] incomplete backward checking 0 remain 0%
c [elim-8-2] subsumed 0 and strengthened 0 clauses in 21001 steps
c [elim-8-2] fully rescheduled 79106 variables 99%
c [elim-8-3] eliminated 17 variables 0% in round 3 in 36173374 steps
c [elim-8-3] backward subsumption/strengthening limit 36173300
c [elim-8-3-1] backward checking 145 touched variables 0%
c [elim-8-3-1] fully completed backward checking in 1 rounds
c [elim-8-3] subsumed 1 and strengthened 0 clauses in 122661 steps
c [elim-8] incomplete 3 not tried 0% in round 3
c [elim-8] transition to [ all 1 rem 1 ] state
c [elim-8] eliminated 906 = 1% variables out of 79995 scheduled
c [bca-5] limit of 10000000 steps and 889939 added (scaled 2)
c [bca-5] 138832 out of 158180 literals actually usable 88%
c [bca-5] added 52 blocked clauses in 418611 steps
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 60092320 penalty 0 = 0 + 0
c [sweep-5-1] 2736 pos 3.5% + 76083 neg 96.5% = 78819 sched 99.7% ret 270
c [sweep-5-1] 60142547 steps 613 queries 798.29 avg class size
c [sweep-5-1] 5492 decisions 504 SAT calls 87.57 avg env size
c [sweep-5-1] 60128 variables remain 77% (18440 retained 23%)
c [decomp-22] removed 1037 variables
c [sweep-5-1] removed 1037 vars (0 failed, 128 eqs, 193 impls)
c [sweep-5] considered successful since not run to completion yet
c [sweep-5] removed 1037 vars in TOTAL (1 rounds, 612 queries)
c [phase-count-9] 435792 negative 98.9% of 440500 except 4708 1.1%
c [phase-count-9] 346459 positive 78.7% of 440500 except 94041 21.3%
c [phase-count-9] less non-negative clauses 4708 than limit 44000 (10.0%)
c [phase-count-9] non-pos/non-neg = 94041/4708 = 19.97 >= 2.00 = 200/100
c [lucky-phase-9] forcing lucky phase -1
c [phase-9] phase bias: 0 positive 0%, 182 negative 100%
c [sort-queue-9] sorted 34532 enqueued variables after 37989 conflicts
c [score-dist-9] active 43520 (56%), one 0 (0%), zero 34532 (44%)
c [score-dist-9] max exp 510, different 155 (30%)
c [score-dist-9] median active exp 494, avg 468.4
c [simplification-9] removed 2094 variables 2.6% (78052 remain 31%)
c [simplification-9] removed 12534 irredundant clauses 2.8% (440500 remain 39%)
c [simplification-9] maximum reduction of 3% = max (3%, 3%)
c [simplification-9] geometric conflict interval increment 5000 = 20000 / 4
c [simplification-9] new conflict interval 19666
c [simplification-9] penalized conflict interval 19666 = 1 * 19666
c [simplification-9] hard conflict limit 67655 (soft 57655 + delta 10000)
c [simplification-9] new conflict limit 57655 (hard 67655)
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  129.7   78051   440500     38091   16712   1704 145278  120   194   64  62%     47   83  175   65  268%
c i  129.7   78045   440500     38110   16724   1704 145282  120   195   64  61%     46   83  169   65  259%
c i  129.7   78044   440500     38111   16724   1704 145282  120   195   64  61%     46   83  168   65  258%
c i  129.9   78043   440500     38209   16797   1704 145282  119   195   64  61%     42   84  147   65  225%
c i  130.1   78042   440500     38269   16831   1704 145282  120   197   64  61%     39   86  159   65  244%
c i  130.1   78041   440500     38274   16835   1704 145282  120   198   64  61%     39   86  157   65  239%
c i  130.2   78040   440500     38315   16873   1705 145282  120   199   64  60%     37   87  148   65  226%
c i  130.2   78039   440500     38332   16887   1706 145283  120   199   64  60%     36   88  139   65  212%
c i  131.8   78038   440500     38941   17174   1707 145285  133   214   64  62%     20  102  199   67  298%
c i  131.9   78037   440500     38965   17196   1707 145286  133   214   64  62%     20  102  191   67  285%
c i  131.9   78036   440500     38971   17200   1708 145286  133   214   64  62%     19  102  190   67  284%
c i  132.8   78035   440500     39326   17388   1709 145288  135   216   64  63%     13  103  166   67  246%
c i  133.5   78034   440500     39642   17565   1711 145288  136   217   64  63%      9  103  152   68  224%
c i  138.3   78033   440500     41681   18903   1723 145299  120   192   64  62%     15   76   88   69  128%
c i  138.3   78032   440500     41682   18903   1723 145299  119   192   64  62%     15   76   87   69  127%
c i  145.0   78031   440500     45453   21709   1729 145327   91   136   74  67%     38   16   43   69   62%
c i  145.1   78030   440500     45543   21787   1729 145327   90   135   74  67%     34   15   54   69   77%
c i  145.1   78029   440500     45545   21788   1729 145327   90   135   74  67%     34   15   53   69   77%
c i  145.1   78028   440500     45547   21789   1729 145327   90   135   74  67%     34   15   53   69   77%
c i  146.1   78027   440500     46176   22382   1729 145329   86   127   74  68%     18    8   62   69   89%
c i  148.7   78026   440500     47895   23646   1735 145341   79   117   83  67%     12   -2   48   69   69%
c i  150.5   78023   440500     48800   24296   1736 145355   86   134   86  64%      6   14  116   70  167%
c i  151.6   78022   440500     49287   24587   1739 145370   98   152   89  64%      3   32  192   71  271%
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  152.0   78020   440500     49483   24762   1739 145370  101   166   89  61%      1   45  181   71  256%
c i  152.0   78019   440500     49494   24767   1739 145370  101   166   89  61%      1   46  185   71  261%
c i  153.4   78018   440500     50033   25077   1739 145373  114   183   89  63%     -0   62  187   72  260%
c i  153.7   78007   440500     50141   25118   1739 145373  117   185   89  63%     -1   65  203   72  280%
c i  153.7   78000   440500     50142   25118   1739 145373  117   185   89  63%     -1   65  202   72  279%
c i  154.4   77999   440500     50590   25430   1739 145378  120   193   89  62%     -2   72  147   73  202%
c i  157.0   77998   440500     52166   26410   1741 145380  144   235   95  61%      6  112  203   76  268%
c i  157.0   77995   440500     52167   26410   1741 145380  144   235   95  61%      6  112  202   76  267%
c i  158.5   77994   440500     53008   26805   1743 145381  167   259   95  64%      3  134  270   78  345%
c i  158.5   77993   440500     53010   26805   1743 145382  167   259   95  64%      3  134  268   78  343%
c i  160.2   77992   440500     54062   27316   1743 145388  189   285   95  66%      3  158  267   81  330%
c i  161.0   77991   440500     54570   27642   1743 145388  195   301   95  65%      1  173  216   82  262%
c i  161.1   77990   440500     54594   27664   1743 145388  195   302   95  64%      1  174  221   82  268%
c i  161.1   77989   440500     54599   27668   1743 145388  195   302   95  64%      1  174  220   82  268%
c i  161.1   77988   440500     54601   27669   1743 145388  195   302   95  64%      1  174  219   82  266%
c i  161.1   77987   440500     54606   27673   1743 145388  195   302   95  64%      1  174  216   82  262%
c i  161.1   77986   440500     54610   27675   1743 145388  195   302   95  64%      1  174  214   82  260%
c i  161.7   77985   440500     55027   28005   1748 145398  188   308   95  61%     -1  178  127   83  154%
c i  161.7   77984   440500     55037   28011   1748 145398  188   307   95  61%     -1  177  123   83  149%
c i  164.4   77983   440500     56401   28825   1767 145424  224   357   95  63%      4  223  366   87  419%
c i  164.4   77982   440500     56404   28827   1767 145424  224   357   95  63%      4  223  365   87  418%
c i  164.4   77981   440500     56405   28827   1767 145424  224   357   95  63%      4  223  364   87  417%
c i  166.5   77980   440500     57369   29326   1769 145425  241   369   95  65%      3  232  276   91  305%
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  166.5   77979   440500     57372   29327   1769 145425  241   369   95  65%      3  232  276   91  304%
c i  166.5   77978   440500     57375   29327   1769 145425  241   369   95  65%      3  232  275   91  304%
c i  166.5   77977   440500     57378   29327   1769 145425  241   369   95  65%      3  232  275   91  304%
c i  166.5   77976   440500     57383   29327   1769 145425  241   369   95  65%      3  232  276   91  305%
c i  166.6   77975   440500     57392   29327   1769 145425  241   369  106  65%      3  232  278   91  307%
c i  166.6   77974   440500     57409   29328   1769 145425  242   369  106  66%      2  232  283   91  312%
c 
c [simplification-10] limit 57750 conflicts (hard 67655) hit after 57750 conflicts
c [quatres-6] found 34139 quaternary clauses 41% in total
c [quatres-6-2] added 5 single-self-subsuming ternary resolvents
c [quatres-6-2] added 6 quaternary resolvents
c [ternres-6] limit 28838282 with penalty 0 = 0 + 0
c [ternres-6] all 77974 free variables schedulable
c [ternres-6] 505 ternary resolvents (2 bin, 503 trn)
c [ternres-6] fully completed ternary resolution
c [card-4] limit 1802392 penalty 3 = 3 + 0
c [card-4] found 6361 at-most-one constraints of average size 4.0
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 1802392 for elimination
c [card-4] 6361 out of 6361 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [decomp-23] removed 82 variables
c [treelook-4] limit 1441914 penalty 1 = 1 + 0 boost 1
c [treelook-4] scheduled 134004 literals 86%
c [treelook-4] scheduling used 1441916 steps
c [treelook-4] not fully scheduled
c [treelook-4] limit 1441914 penalty 1 = 1 + 0 boost 1
c [treelook-4] used 1538779 steps
c [treelook-4] 133987 literals remain 86%
c [treelook-4] 35880 variables remain to probed next time 46%
c [treelook-4] removed 1 variables, found 9268 hbrs
c [unhide-10] limit 1441914 with penalty 2 = 0 + 2
c [unhide-10-10] 6 units, 214 failed, 9559 tauts, 0 hbrs, 611646 literals
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 178 transitive binary clauses
c [transred-6] found 1 units
c [cce-3] limit of 36047852 steps penalty 2 = 2 + 0
c [cce-3-1] eliminated 16 clauses out of 1473 (1%) of length 9
c [cce-3-1] eliminated 27 clauses out of 423 (6%) of length 8
c [cce-3-1] eliminated 37 clauses out of 767 (5%) of length 7
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 80 large clauses in 36047852 steps
c [cce-3-1] allowing another 18023926 steps for small clauses
c [cce-3-1] scheduling 311978 clauses = 237104 binary + 74874 ternary
c [cce-3-1] tried to eliminate 515 small clauses 0%
c [cce-3-1] eliminated 90 binary clauses 0%
c [cce-3-1] eliminated 31 ternary clauses 0%
c [cce-3-1] eliminated 121 small clauses 0%
c [cce-3-1] eliminated 3906 small clauses in 36047856 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 3986 covered clauses in round 1
c [cce-3] eliminated 3986 covered clauses in TOTAL during 1 rounds
c [cce-3] 3986 < 1/100 * 438416 = 4384 considered unsuccessful
c [elim-9] no untried remaining variables left
c [elim-9] scheduled 77445 variables 100%
c [elim-9] limit of 576765642 steps penalty 0 = 0 + 0
c [elim-9] rescheduling of touched variables disabled
c [elim-9-1] eliminated 2056 variables 3% in round 1 in 39788738 steps
c [elim-9-1] backward subsumption/strengthening limit 39788700
c [elim-9-1-1] backward checking 6456 touched variables 8%
c [elim-9-1-1] fully completed backward checking in 1 rounds
c [elim-9-1] subsumed 24 and strengthened 666 clauses in 3205090 steps
c [elim-9-1] rescheduled 1305 variables 2% by backward subsumption
c [elim-9-2] eliminated 217 variables 0% in round 2 in 2824458 steps
c [elim-9-2] backward subsumption/strengthening limit 2824400
c [elim-9-2-1] backward checking 1380 touched variables 2%
c [elim-9-2-1] fully completed backward checking in 1 rounds
c [elim-9-2] subsumed 0 and strengthened 0 clauses in 792458 steps
c [elim-9] fully completed in 2 rounds
c [elim-9] transition to [ all 0 rem 0 ] state
c [elim-9] eliminated 2273 = 3% variables out of 77445 scheduled
c [bca-6] limit of 10000000 steps and 855911 added (scaled 2)
c [bca-6] 131365 out of 150346 literals actually usable 87%
c [bca-6] added 376 blocked clauses in 400042 steps
c [sweep-6] limit 8651484 penalty 0 = 0 + 0
c [sweep-6-1] 2720 pos 4.7% + 55081 neg 95.3% = 57801 sched 76.9% ret 17371
c [sweep-6-1] 8874392 steps 97 queries 3395.98 avg class size
c [sweep-6-1] 863 decisions 81 SAT calls 85.23 avg env size
c [sweep-6-1] 56643 variables remain 76% (18189 retained 24%)
c [decomp-25] removed 391 variables
c [sweep-6-1] removed 391 vars (0 failed, 20 eqs, 30 impls)
c [sweep-6] considered successful since not run to completion yet
c [sweep-6] removed 391 vars in TOTAL (1 rounds, 96 queries)
c [phase-count-10] 420678 negative 98.9% of 425277 except 4599 1.1%
c [phase-count-10] 332161 positive 78.1% of 425277 except 93116 21.9%
c [phase-count-10] less non-negative clauses 4599 than limit 42500 (10.0%)
c [phase-count-10] non-pos/non-neg = 93116/4599 = 20.25 >= 2.00 = 200/100
c [lucky-phase-10] forcing lucky phase -1
c [phase-10] phase bias: 0 positive 0%, 154 negative 100%
c [sort-queue-10] sorted 30620 enqueued variables after 57750 conflicts
c [score-dist-10] active 44161 (59%), one 0 (0%), zero 30620 (41%)
c [score-dist-10] max exp 510, different 231 (45%)
c [score-dist-10] median active exp 494, avg 461.2
c [simplification-10] removed 3193 variables 4.1% (74781 remain 30%)
c [simplification-10] removed 15223 irredundant clauses 3.5% (425277 remain 38%)
c [simplification-10] maximum reduction of 4% = max (4%, 3%)
c [simplification-10] geometric conflict interval increment 4000 = 20000 / 5
c [simplification-10] new conflict interval 23666
c [simplification-10] penalized conflict interval 23666 = 1 * 23666
c [simplification-10] hard conflict limit 93249 (soft 81416 + delta 11833)
c [simplification-10] new conflict limit 81416 (hard 93249)
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  180.3   74780   425277     60619   23558   1927 144867  183   278   73  66%     28  132  133   93  143%
c i  181.9   74779   425277     61556   24024   1928 144877  181   275   73  66%     12  127  182   94  194%
c i  182.0   74778   425277     61557   24024   1928 144877  181   275   73  66%     12  127  182   94  193%
c i  182.0   74776   425277     61558   24024   1928 144877  181   274   73  66%     12  127  181   94  192%
c i  191.1   74775   425277     67942   29089   1943 144895   83   129   82  64%     73  -24   34   92   37%
c i  191.1   74774   425277     67943   29089   1943 144895   83   129   82  64%     73  -24   33   92   36%
c i  191.3   74773   425277     68087   29173   1943 144895   84   132   82  64%     62  -21   72   92   78%
c i  195.6   74772   425277     71240   31815   1950 144895   66   129   88  51%     25  -23   56   90   63%
c i  197.6   74745   425277     72418   32735   1955 144903   64   121   88  53%      7  -31   71   89   79%
c i  199.1   74744   425277     73292   33241   1957 144908   71   126   88  56%      1  -25   98   90  110%
c i  207.4   74743   425277     77726   35784   1964 144943   83   130   98  64%     41  -20   79   90   88%
c i  207.8   74735   425277     77936   35923   1964 144943   83   130   98  64%     31  -20   77   90   86%
c i  207.8   74734   425277     77938   35924   1964 144943   83   130   98  64%     31  -21   77   90   86%
c i  207.8   74733   425277     77940   35925   1964 144943   83   130   98  64%     31  -21   77   90   86%
c i  207.8   74732   425277     77943   35927   1964 144943   83   130   98  64%     31  -21   77   90   86%
c i  207.8   74731   425277     77946   35929   1964 144943   83   130   98  64%     30  -21   77   90   85%
c i  207.8   74730   425277     77947   35929   1964 144943   83   130   98  64%     30  -21   76   90   85%
c i  219.8   74729   425277     84356   41689   2000 144978   53    81  115  66%     68  -65   40   86   47%
c i  219.8   74728   425277     84360   41690   2000 144980   53    81  115  66%     68  -65   41   86   48%
c i  219.9   74727   425277     84361   41690   2000 144980   53    81  115  66%     68  -65   41   86   48%
c i  223.4   74726   425277     86186   42783   2007 144999   69   104  115  67%     12  -41   50   86   58%
c i  223.4   74725   425277     86189   42784   2007 144999   69   104  115  67%     12  -41   50   86   58%
c i  225.3   74724   425277     87280   43794   2009 145004   62    93  115  67%     -0  -51   41   85   48%
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  230.8   74723   425277     90334   46736   2009 145006   57    84  122  68%     16  -57   47   84   57%
c i  230.8   74722   425277     90335   46736   2009 145006   57    84  122  68%     16  -57   47   84   56%
c i  230.8   74721   425277     90336   46736   2009 145006   57    84  122  68%     16  -57   47   84   56%
c i  231.4   74720   425277     90732   47042   2012 145018   59    90  122  66%      7  -51   74   84   88%
c i  231.8   74719   425277     90929   47161   2013 145020   61    93  122  65%      3  -47   85   84  102%
c i  231.8   74718   425277     90931   47162   2013 145020   61    93  122  65%      3  -47   85   84  101%
c i  231.8   74717   425277     90933   47163   2013 145020   61    93  122  65%      3  -47   85   84  101%
c i  231.8   74716   425277     90936   47165   2013 145020   61    93  122  65%      3  -47   84   84  100%
c i  232.2   74715   425277     91144   47306   2013 145021   62    95  122  65%     -1  -45   87   84  103%
c i  233.1   74714   425277     91603   47756   2013 145021   63    95  122  66%     -5  -46   68   84   81%
c i  233.1   74713   425277     91605   47757   2013 145021   63    95  122  66%     -5  -46   68   84   81%
c i  234.4   74712   425277     92371   48441   2015 145021   63    96  122  66%     -8  -44   70   84   84%
c 
c [simplification-11] limit 81525 conflicts (hard 93249) hit after 93249 conflicts
c [quatres-7] found 34179 quaternary clauses 42% in total
c [quatres-7-1] removed 1 duplicate quaternary clauses
c [quatres-7-2] added 10 quaternary resolvents
c [ternres-7] limit 42219817 with penalty 0 = 0 + 0
c [ternres-7] all 74712 free variables schedulable
c [ternres-7] 561 ternary resolvents (0 bin, 561 trn)
c [ternres-7] fully completed ternary resolution
c [gauss-4] limit 2110990 penalty 2 = 2 + 0
c [gauss-4] extracted 48 xors of average arity 3.0
c [gauss-4] connected 142 occurrences of 128 variables (average 1.1)
c [gauss-4] limit 2110990 penalty 2 = 2 + 0
c [gauss-4] fully completed
c [gauss-4] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-26] removed 2 variables
c [basicprobe-4] limit 211099089 penalty 0 = 0 + 0
c [basicprobe-4-0] 20273 probes remain 28% after last round
c [basicprobe-4-0] 784 units = 777 failed (99%) + 7 lifted (1%)
c [basicprobe-4-0] removed 2405 variables, found 147675 hbrs
c [bate-2] eliminated 436 asymmetric tautologies during probing
c [unhide-11] limit 2110990 with penalty 2 = 0 + 2
c [unhide-11-11] 3 units, 70 failed, 5040 tauts, 0 hbrs, 542596 literals
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 183 transitive binary clauses
c [block-4] scheduling all variables this time
c [block-4] scheduled 72137 variables 100%
c [block-4] limit of 105549544 steps penalty 2 = 2 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 19 blocked clauses
c [block-4] 19 < 1/100 * 407564 = 4075 considered unsuccessful
c [elim-10] scheduling all variables this time
c [elim-10] scheduled 72137 variables 100%
c [elim-10] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-10] rescheduling of touched variables disabled
c [elim-10-1] eliminated 2104 variables 3% in round 1 in 34909393 steps
c [elim-10-1] backward subsumption/strengthening limit 34909300
c [elim-10-1-1] backward checking 8136 touched variables 11%
c [elim-10-1-1] fully completed backward checking in 1 rounds
c [elim-10-1] subsumed 50 and strengthened 204 clauses in 2137517 steps
c [elim-10-1] rescheduled 616 variables 1% by backward subsumption
c [elim-10-2] eliminated 66 variables 0% in round 2 in 567417 steps
c [elim-10-2] backward subsumption/strengthening limit 567400
c [elim-10-2-1] backward checking 500 touched variables 1%
c [elim-10-2-1] fully completed backward checking in 1 rounds
c [elim-10-2] subsumed 2 and strengthened 3 clauses in 286906 steps
c [elim-10-2] rescheduled 17 variables 0% by backward subsumption
c [elim-10-3] no variable eliminated in round 3 in 20861 steps
c [elim-10] fully completed in 3 rounds
c [elim-10] transition to [ all 0 rem 0 ] state
c [elim-10] eliminated 2182 = 3% variables out of 72137 scheduled
c [bca-7] limit of 10000000 steps and 802471 added (scaled 2)
c [bca-7] 121748 out of 139912 literals actually usable 87%
c [bca-7] added 71 blocked clauses in 372332 steps
c [sweep-7] limit 12665945 penalty 0 = 0 + 0
c [sweep-7-1] 2309 pos 4.3% + 50945 neg 95.7% = 53254 sched 76.1% ret 16701
c [sweep-7-1] 12729607 steps 132 queries 2832.62 avg class size
c [sweep-7-1] 1187 decisions 106 SAT calls 63.34 avg env size
c [sweep-7-1] 51483 variables remain 74% (18409 retained 26%)
c [decomp-27] removed 205 variables
c [sweep-7-1] removed 205 vars (0 failed, 26 eqs, 44 impls)
c [sweep-7] removed 205 vars in TOTAL (1 rounds, 131 queries)
c [phase-count-11] 395513 negative 98.9% of 400047 except 4534 1.1%
c [phase-count-11] 311017 positive 77.7% of 400047 except 89030 22.3%
c [phase-count-11] skipping relative phase luck test
c [phase-11] phase bias: 31 positive 100%, 0 negative 0%
c [sort-queue-11] sorted 27073 enqueued variables after 93249 conflicts
c [score-dist-11] active 42677 (61%), one 0 (0%), zero 27073 (39%)
c [score-dist-11] max exp 510, different 356 (70%)
c [score-dist-11] median active exp 491, avg 433.0
c [simplification-11] removed 4962 variables 6.6% (69750 remain 28%)
c [simplification-11] removed 25230 irredundant clauses 5.9% (400047 remain 36%)
c [simplification-11] maximum reduction of 7% = max (7%, 6%)
c [simplification-11] large reduction 7% >= 5% limit
c [simplification-11] next conflict interval 2000 = 2000/1
c [simplification-11] penalized conflict interval 2000 = 1 * 2000
c [simplification-11] hard conflict limit 105249 (soft 95249 + delta 10000)
c [simplification-11] new conflict limit 95249 (hard 105249)
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  252.1   69749   400047     93483   28328   2258 274351   63    95   75  66%     -7  -44   52   83   62%
c i  261.5   69748   400047     99268   33114   2284 274360   67    99   78  68%     56  -38   57   82   69%
c i  261.9   69745   400047     99481   33316   2284 274360   66    97   78  68%     42  -39   53   82   64%
c i  270.9   69741   400047    104998   38439   2304 274363   48    65   86  74%     50  -67   41   79   52%
c 
c [simplification-12] limit 95249 conflicts (hard 105249) hit after 105249 conflicts
c [quatres-8] found 32981 quaternary clauses 44% in total
c [quatres-8-1] removed 1 duplicate quaternary clauses
c [quatres-8-2] added 2 single-self-subsuming ternary resolvents
c [quatres-8-2] added 29 quaternary resolvents
c [ternres-8] limit 46629934 with penalty 0 = 0 + 0
c [ternres-8] all 69741 free variables schedulable
c [ternres-8] 783 ternary resolvents (3 bin, 780 trn)
c [ternres-8] fully completed ternary resolution
c [decomp-28] removed 10 variables
c [simpleprobe-5] all 69740 free variables schedulable
c [simpleprobe-5] limit 186519739 penalty 0 = 0 + 0
c [decomp-29] removed 3114 variables
c [simpleprobe-5] fully completed simple probing
c [simpleprobe-5] removed 3114 variables, found 65380 hbrs, 763 units
c [unhide-12] limit 2331496 with penalty 2 = 0 + 2
c [unhide-12-12] 2 units, 133 failed, 42096 tauts, 0 hbrs, 395605 literals
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 217 transitive binary clauses
c [elim-11] scheduling all variables this time
c [elim-11] scheduled 66425 variables 100%
c [elim-11] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-11] rescheduling of touched variables disabled
c [elim-11-1] eliminated 1476 variables 2% in round 1 in 33027525 steps
c [elim-11-1] backward subsumption/strengthening limit 33027500
c [elim-11-1-1] backward checking 6838 touched variables 10%
c [elim-11-1-1] fully completed backward checking in 1 rounds
c [elim-11-1] subsumed 70 and strengthened 11 clauses in 1856995 steps
c [elim-11-1] rescheduled 224 variables 0% by backward subsumption
c [elim-11-2] eliminated 14 variables 0% in round 2 in 134774 steps
c [elim-11-2] backward subsumption/strengthening limit 134700
c [elim-11-2-1] backward checking 120 touched variables 0%
c [elim-11-2-1] incomplete backward checking 0 remain 0%
c [elim-11-2] subsumed 10 and strengthened 17 clauses in 134701 steps
c [elim-11-2] rescheduled 52 variables 0% by backward subsumption
c [elim-11-3] no variable eliminated in round 3 in 177381 steps
c [elim-11] fully completed in 3 rounds
c [elim-11] transition to [ all 0 rem 0 ] state
c [elim-11] eliminated 1490 = 2% variables out of 66425 scheduled
c [bca-8] limit of 10000000 steps and 749292 added (scaled 2)
c [bca-8] 111325 out of 129872 literals actually usable 86%
c [bca-8] added 72 blocked clauses in 346898 steps
c [sweep-8] limit 13988980 penalty 0 = 0 + 0
c [sweep-8-1] 2266 pos 4.7% + 46441 neg 95.3% = 48707 sched 75.0% ret 16228
c [sweep-8-1] 14014745 steps 144 queries 2275.19 avg class size
c [sweep-8-1] 1721 decisions 121 SAT calls 126.11 avg env size
c [sweep-8-1] 46357 variables remain 72% (18306 retained 28%)
c [decomp-30] removed 480 variables
c [sweep-8-1] removed 480 vars (0 failed, 25 eqs, 39 impls)
c [sweep-8] removed 480 vars in TOTAL (1 rounds, 143 queries)
c [phase-count-12] 367719 negative 98.8% of 372193 except 4474 1.2%
c [phase-count-12] 283602 positive 76.2% of 372193 except 88591 23.8%
c [phase-count-12] skipping relative phase luck test
c [phase-12] phase bias: 2 positive 50%, 2 negative 50%
c [sort-queue-12] sorted 21977 enqueued variables after 105249 conflicts
c [score-dist-12] active 42478 (66%), one 0 (0%), zero 21977 (34%)
c [score-dist-12] max exp 510, different 391 (77%)
c [score-dist-12] median active exp 489, avg 428.6
c [simplification-12] removed 5286 variables 7.6% (64455 remain 26%)
c [simplification-12] removed 27854 irredundant clauses 7.0% (372193 remain 33%)
c [simplification-12] maximum reduction of 8% = max (8%, 7%)
c [simplification-12] large reduction 8% >= 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 117249 (soft 107249 + delta 10000)
c [simplification-12] new conflict limit 107249 (hard 117249)
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  278.4   64454   372193    105266   31692   1829 271347   47    64   72  73%     34  -67   39   79   50%
c i  280.5   64453   372193    106773   33104   1831 271347   44    60   80  73%      3  -70   41   78   52%
c i  284.9   64452   372193    109645   35735   1835 271348   38    51   80  75%     11  -75   24   76   32%
c i  285.3   64451   372193    109966   35991   1836 271349   38    51   80  75%      3  -75   28   76   37%
c i  286.0   64450   372193    110406   36327   1838 271350   37    50   80  75%     -4  -76   34   76   45%
c i  291.2   64449   372193    113920   39635   1846 271350   35    46   93  77%     19  -76   33   73   45%
c i  295.9   64448   372193    117123   42475   1861 271350   46    62   93  73%     16  -56   53   72   73%
c 
c [simplification-13] limit 107249 conflicts (hard 117249) hit after 117250 conflicts
c [quatres-9] found 28658 quaternary clauses 41% in total
c [quatres-9-2] added 3 single-self-subsuming ternary resolvents
c [quatres-9-2] added 7 quaternary resolvents
c [ternres-9] limit 50533214 with penalty 0 = 0 + 0
c [ternres-9] all 64448 free variables schedulable
c [ternres-9] 653 ternary resolvents (2 bin, 651 trn)
c [ternres-9] fully completed ternary resolution
c [decomp-31] removed 12 variables
c [treelook-5] limit 5053321 penalty 0 = 0 + 0 boost 1
c [treelook-5] scheduled 108139 literals 84%
c [treelook-5] scheduling used 1506633 steps
c [treelook-5] scheduled completely
c [treelook-5] limit 5053321 penalty 0 = 0 + 0 boost 1
c [treelook-5] used 5125525 steps
c [treelook-5] 108038 literals remain 84%
c [treelook-5] 27164 variables remain to probed next time 42%
c [decomp-32] removed 3 variables
c [treelook-5] removed 8 variables, found 24346 hbrs
c [unhide-13] limit 2526660 with penalty 2 = 0 + 2
c [unhide-13-13] 2 units, 11 failed, 3465 tauts, 0 hbrs, 225052 literals
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 201 transitive binary clauses
c [elim-12] scheduling all variables this time
c [elim-12] scheduled 64318 variables 100%
c [elim-12] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-12] rescheduling of touched variables disabled
c [elim-12-1] eliminated 1244 variables 2% in round 1 in 33655380 steps
c [elim-12-1] backward subsumption/strengthening limit 33655300
c [elim-12-1-1] backward checking 5018 touched variables 8%
c [elim-12-1-1] fully completed backward checking in 1 rounds
c [elim-12-1] subsumed 31 and strengthened 15 clauses in 1621107 steps
c [elim-12-1] rescheduled 125 variables 0% by backward subsumption
c [elim-12-2] eliminated 10 variables 0% in round 2 in 97458 steps
c [elim-12-2] backward subsumption/strengthening limit 97400
c [elim-12-2-1] backward checking 86 touched variables 0%
c [elim-12-2-1] incomplete backward checking 0 remain 0%
c [elim-12-2] subsumed 2 and strengthened 1 clauses in 97401 steps
c [elim-12-2] rescheduled 8 variables 0% by backward subsumption
c [elim-12-3] no variable eliminated in round 3 in 4058 steps
c [elim-12] fully completed in 3 rounds
c [elim-12] transition to [ all 0 rem 0 ] state
c [elim-12] eliminated 1261 = 2% variables out of 64318 scheduled
c [bca-9] limit of 10000000 steps and 730792 added (scaled 2)
c [bca-9] 107888 out of 126116 literals actually usable 86%
c [bca-9] added 50 blocked clauses in 343486 steps
c [sweep-9] limit 15159964 penalty 0 = 0 + 0
c [sweep-9-1] 2454 pos 5.4% + 42834 neg 94.6% = 45288 sched 71.8% ret 17769
c [sweep-9-1] 15217251 steps 173 queries 1830.65 avg class size
c [sweep-9-1] 2352 decisions 149 SAT calls 162.60 avg env size
c [sweep-9-1] 42800 variables remain 68% (20223 retained 32%)
c [decomp-33] removed 89 variables
c [sweep-9-1] removed 89 vars (0 failed, 25 eqs, 45 impls)
c [sweep-9] removed 89 vars in TOTAL (1 rounds, 172 queries)
c [phase-count-13] 360087 negative 98.8% of 364482 except 4395 1.2%
c [phase-count-13] 277093 positive 76.0% of 364482 except 87389 24.0%
c [phase-count-13] skipping relative phase luck test
c [phase-13] phase bias: 2 positive 100%, 0 negative 0%
c [sort-queue-13] sorted 20697 enqueued variables after 117250 conflicts
c [score-dist-13] active 42271 (67%), one 0 (0%), zero 20697 (33%)
c [score-dist-13] max exp 509, different 430 (84%)
c [score-dist-13] median active exp 479, avg 413.1
c [simplification-13] removed 1480 variables 2.3% (62968 remain 25%)
c [simplification-13] removed 7711 irredundant clauses 2.1% (364482 remain 33%)
c [simplification-13] maximum reduction of 2% = max (2%, 2%)
c [simplification-13] geometric conflict interval increment 7888 = 23666 / 3
c [simplification-13] new conflict interval 31554
c [simplification-13] penalized conflict interval 31554 = 1 * 31554
c [simplification-13] hard conflict limit 164581 (soft 148804 + delta 15777)
c [simplification-13] new conflict limit 148804 (hard 164581)
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  303.6   62967   364482    117849   39456   2148 290663   48    66   92  73%      0  -52   61   72   85%
c i  306.1   62966   364482    119523   41054   2150 290664   47    63   93  75%     -3  -53   49   72   69%
c i  306.1   62965   364482    119546   41075   2150 290664   47    63   93  75%     -4  -53   50   72   70%
c i  309.5   62964   364482    121874   43254   2161 290678   48    65   93  74%      3  -50   49   71   70%
c i  313.2   62963   364482    125076   46377   2169 290685   47    67  104  70%     15  -45   50   70   72%
c i  319.1   62962   364482    129432   50666   2170 290685   43    57  116  76%     31  -52   33   68   49%
c -  321.1   62962   364482    131124   25140   2172 290685   33    44   57  74%      2  -63   13   66   19%
c i  328.7   62961   364482    137014   30727   2179 290687   35    47   81  75%     78  -55   41   64   65%
c i  328.8   62960   364482    137074   30777   2180 290688   36    49   81  73%     72  -53   49   64   77%
c i  328.8   62959   364482    137124   30814   2181 290688   36    50   81  73%     67  -52   55   64   86%
c i  328.8   62958   364482    137126   30815   2181 290688   36    50   81  73%     67  -52   54   64   86%
c i  328.8   62957   364482    137127   30815   2181 290688   36    50   81  73%     67  -52   54   64   85%
c i  347.7   62956   364482    150226   43511   2202 290693   46    58  109  80%    151  -35   60   60  100%
c i  357.6   62955   364482    157574   50761   2216 290697   40    51  126  78%     58  -38   48   58   83%
c i  357.6   62954   364482    157575   50761   2216 290697   40    51  126  78%     57  -38   48   58   83%
c -  362.0   62954   364482    160386   27261   2221 290706   44    58   58  76%     -6  -30   48   58   83%
c 
c [simplification-14] limit 148829 conflicts (hard 164581) hit after 164581 conflicts
c [quatres-10] found 28752 quaternary clauses 41% in total
c [quatres-10-2] added 7 single-self-subsuming ternary resolvents
c [quatres-10-2] added 6 quaternary resolvents
c [ternres-10] limit 64264559 with penalty 0 = 0 + 0
c [ternres-10] all 62954 free variables schedulable
c [ternres-10] 393 ternary resolvents (0 bin, 393 trn)
c [ternres-10] fully completed ternary resolution
c [decomp-34] removed 14 variables
c [basicprobe-5] limit 321322798 penalty 0 = 0 + 0
c [basicprobe-5-0] 11049 probes remain 18% after last round
c [basicprobe-5-0] 1216 units = 1202 failed (99%) + 14 lifted (1%)
c [basicprobe-5-0] removed 2694 variables, found 189016 hbrs
c [bate-3] eliminated 993 asymmetric tautologies during probing
c [unhide-14] limit 6426455 with penalty 1 = 0 + 1
c [unhide-14-16] 20 units, 188 failed, 79011 tauts, 0 hbrs, 420514 literals
c [transred-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 179 transitive binary clauses
c [cce-4] boosting limit by 10
c [cce-4] limit of 401653497 steps penalty 3 = 3 + 0
c [cce-4-1] eliminated 9 clauses out of 670 (1%) of length 7
c [cce-4-1] eliminated 2244 clauses out of 4325 (52%) of length 6
c [cce-4-1] eliminated 17455 clauses out of 26307 (66%) of length 5
c [cce-4-1] eliminated 9232 clauses out of 28019 (33%) of length 4
c [cce-4-1] incomplete large round (ATE)
c [cce-4-1] eliminated 28940 large clauses in 401653504 steps
c [cce-4-1] allowing another 200826752 steps for small clauses
c [cce-4-1] scheduling 242732 clauses = 190221 binary + 52511 ternary
c [cce-4-1] tried to eliminate 11102 small clauses 5%
c [cce-4-1] eliminated 1830 binary clauses 1%
c [cce-4-1] eliminated 797 ternary clauses 2%
c [cce-4-1] eliminated 2627 small clauses 1%
c [cce-4-1] eliminated 3258 small clauses in 401653502 steps
c [cce-4-1] incomplete small round (ATE)
c [cce-4-1] eliminated 32198 covered clauses in round 1
c [cce-4] eliminated 32198 covered clauses in TOTAL during 1 rounds
c [elim-13] scheduling all variables this time
c [elim-13] scheduled 59969 variables 100%
c [elim-13] almost no limit of 100000000000 steps
c [elim-13] rescheduling of touched variables disabled
c [elim-13-1] eliminated 14801 variables 25% in round 1 in 25138163 steps
c [elim-13-1] backward subsumption/strengthening limit 25138100
c [elim-13-1-1] backward checking 33667 touched variables 56%
c [elim-13-1-1] fully completed backward checking in 1 rounds
c [elim-13-1] subsumed 77 and strengthened 34 clauses in 5068414 steps
c [elim-13-1] rescheduled 268 variables 0% by backward subsumption
c [elim-13-2] eliminated 14 variables 0% in round 2 in 279008 steps
c [elim-13-2] backward subsumption/strengthening limit 279000
c [elim-13-2-1] backward checking 97 touched variables 0%
c [elim-13-2-1] incomplete backward checking 0 remain 0%
c [elim-13-2] subsumed 9 and strengthened 7 clauses in 279001 steps
c [elim-13-2] rescheduled 43 variables 0% by backward subsumption
c [elim-13-3] no variable eliminated in round 3 in 31215 steps
c [elim-13] fully completed in 3 rounds
c [elim-13] transition to [ all 0 rem 0 ] state
c [elim-13] eliminated 14815 = 25% variables out of 59969 scheduled
c [bca-10] limit of 10000000 steps and 553939 added (scaled 2)
c [bca-10] 84442 out of 90310 literals actually usable 94%
c [bca-10] added 135 blocked clauses in 196775 steps
c [sweep-10] limit 19279367 penalty 0 = 0 + 0
c [sweep-10-1] 2272 pos 6.9% + 30702 neg 93.1% = 32974 sched 73.0% ret 12180
c [sweep-10-1] 19293001 steps 353 queries 667.08 avg class size
c [sweep-10-1] 3923 decisions 306 SAT calls 84.41 avg env size
c [sweep-10-1] 28738 variables remain 64% (16203 retained 36%)
c [decomp-35] removed 510 variables
c [sweep-10-1] removed 510 vars (0 failed, 54 eqs, 77 impls)
c [sweep-10] removed 510 vars in TOTAL (1 rounds, 352 queries)
c [phase-count-14] 274417 negative 99.8% of 275083 except 666 0.2%
c [phase-count-14] 194446 positive 70.7% of 275083 except 80637 29.3%
c [phase-count-14] skipping relative phase luck test
c [phase-14] phase bias: 1 positive 6%, 17 negative 94%
c [sort-queue-14] sorted 14749 enqueued variables after 164581 conflicts
c [score-dist-14] active 29895 (67%), one 1227 (3%), zero 13522 (30%)
c [score-dist-14] max exp 510, different 438 (86%)
c [score-dist-14] median active exp 502, avg 434.8
c [simplification-14] removed 18310 variables 29.1% (44644 remain 18%)
c [simplification-14] removed 89399 irredundant clauses 24.5% (275083 remain 25%)
c [simplification-14] maximum reduction of 29% = max (29%, 25%)
c [simplification-14] large reduction 29% >= 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 176581 (soft 166581 + delta 10000)
c [simplification-14] new conflict limit 166581 (hard 176581)
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  400.0   44643   275083    164703    3002   2883 359444   41    56   39  73%     52  -30   43   56   76%
c 
c [simplification-15] limit 166581 conflicts (hard 176581) hit after 168256 conflicts
c [quatres-11] found 26212 quaternary clauses 64% in total
c [quatres-11-2] added 2 single-self-subsuming ternary resolvents
c [quatres-11-2] added 20 quaternary resolvents
c [ternres-11] limit 65103580 with penalty 0 = 0 + 0
c [ternres-11] all 44631 free variables schedulable
c [ternres-11] 1145 ternary resolvents (3 bin, 1142 trn)
c [ternres-11] fully completed ternary resolution
c [card-5] limit 2034486 penalty 4 = 4 + 0
c [card-5] found 2538 at-most-one constraints of average size 4.1
c [card-5] no at-most-two constraint found
c [card-5] using previous limit 2034486 for elimination
c [card-5] 2538 out of 2538 constraints (100%) meet size limits
c [card-5] no units found
c [card-5] no at-most-one constraints generated
c [gauss-5] limit 1627589 penalty 3 = 3 + 0
c [gauss-5] extracted 37 xors of average arity 2.8
c [gauss-5] connected 105 occurrences of 86 variables (average 1.2)
c [gauss-5] limit 1627589 penalty 3 = 3 + 0
c [gauss-5] fully completed
c [gauss-5] exported 0 unary, 0 binary and 0 ternary equations
c [simpleprobe-6] all 44631 free variables schedulable
c [simpleprobe-6] limit 200000000 penalty 0 = 0 + 0
c [decomp-37] removed 739 variables
c [simpleprobe-6] fully completed simple probing
c [simpleprobe-6] removed 739 variables, found 101670 hbrs, 247 units
c [unhide-15] limit 13020716 with penalty 0 = 0 + 0
c [unhide-15-23] 12 units, 95 failed, 85732 tauts, 0 hbrs, 37146 literals
c [transred-11] limit 2000000 with penalty 0 = 0 + 0
c [transred-11] removed 217 transitive binary clauses
c [transred-11] found 1 units
c [block-5] scheduling all variables this time
c [block-5] scheduled 43716 variables 100%
c [block-5] limit of 81379475 steps penalty 3 = 3 + 0
c [block-5] fully completed
c [block-5] transition to [ all 0 rem 0 ] state
c [block-5] eliminated 160 blocked clauses
c [block-5] 160 < 1/100 * 263218 = 2632 considered unsuccessful
c [elim-14] scheduling all variables this time
c [elim-14] scheduled 43711 variables 100%
c [elim-14] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-14] rescheduling of touched variables disabled
c [elim-14-1] eliminated 855 variables 2% in round 1 in 21969644 steps
c [elim-14-1] backward subsumption/strengthening limit 21969600
c [elim-14-1-1] backward checking 4408 touched variables 10%
c [elim-14-1-1] fully completed backward checking in 1 rounds
c [elim-14-1] subsumed 24 and strengthened 10 clauses in 1028591 steps
c [elim-14-1] rescheduled 87 variables 0% by backward subsumption
c [elim-14-2] eliminated 8 variables 0% in round 2 in 51856 steps
c [elim-14-2] backward subsumption/strengthening limit 51800
c [elim-14-2-1] backward checking 92 touched variables 0%
c [elim-14-2-1] incomplete backward checking 0 remain 0%
c [elim-14-2] subsumed 8 and strengthened 1 clauses in 51801 steps
c [elim-14-2] rescheduled 21 variables 0% by backward subsumption
c [elim-14-3] eliminated 2 variables 0% in round 3 in 27093 steps
c [elim-14-3] backward subsumption/strengthening limit 27000
c [elim-14-3-1] backward checking 34 touched variables 0%
c [elim-14-3-1] incomplete backward checking 0 remain 0%
c [elim-14-3] subsumed 6 and strengthened 0 clauses in 27001 steps
c [elim-14] incomplete 5 not tried 0% in round 3
c [elim-14] transition to [ all 1 rem 1 ] state
c [elim-14] eliminated 867 = 2% variables out of 43711 scheduled
c [bca-11] limit of 10000000 steps and 522733 added (scaled 2)
c [bca-11] 76919 out of 85690 literals actually usable 90%
c [bca-11] added 54 blocked clauses in 180492 steps
c [sweep-11] boosting sweeping limit by 10
c [sweep-11] limit 195310740 penalty 0 = 0 + 0
c [sweep-11-1] 2213 pos 8.0% + 25495 neg 92.0% = 27708 sched 64.7% ret 15136
c [sweep-11-1] 195325800 steps 4521 queries 66.34 avg class size
c [sweep-11-1] 18629 decisions 3738 SAT calls 64.03 avg env size
c [sweep-11-1] 4419 variables remain 10% (37872 retained 90%)
c [decomp-38] removed 2249 variables
c [sweep-11-1] removed 2249 vars (0 failed, 821 eqs, 1334 impls)
c [sweep-11] removed 2249 vars in TOTAL (1 rounds, 4520 queries)
c [phase-count-15] 254916 negative 99.8% of 255520 except 604 0.2%
c [phase-count-15] 178836 positive 70.0% of 255520 except 76684 30.0%
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 11017 enqueued variables after 168256 conflicts
c [score-dist-15] active 29578 (73%), one 652 (2%), zero 10365 (26%)
c [score-dist-15] max exp 510, different 359 (70%)
c [score-dist-15] median active exp 503, avg 480.0
c [simplification-15] removed 4036 variables 9.0% (40595 remain 16%)
c [simplification-15] removed 19563 irredundant clauses 7.1% (255520 remain 23%)
c [simplification-15] maximum reduction of 9% = max (9%, 7%)
c [simplification-15] large reduction 9% >= 5% limit
c [simplification-15] next conflict interval 2000 = 2000/1
c [simplification-15] penalized conflict interval 2000 = 1 * 2000
c [simplification-15] hard conflict limit 180256 (soft 170256 + delta 10000)
c [simplification-15] new conflict limit 170256 (hard 180256)
c 
c [simplification-16] limit 170256 conflicts (hard 180256) hit after 170256 conflicts
c [quatres-12] found 23807 quaternary clauses 62% in total
c [quatres-12-1] removed 2 duplicate quaternary clauses
c [quatres-12-2] added 6 single-self-subsuming ternary resolvents
c [quatres-12-2] added 7 quaternary resolvents
c [ternres-12] limit 65469777 with penalty 0 = 0 + 0
c [ternres-12] all 40595 free variables schedulable
c [ternres-12] 1008 ternary resolvents (15 bin, 993 trn)
c [ternres-12] fully completed ternary resolution
c [decomp-39] removed 4 variables
c [treelook-6] limit 6546977 penalty 0 = 0 + 0 boost 1
c [treelook-6] scheduled 62423 literals 77%
c [treelook-6] scheduling used 1235804 steps
c [treelook-6] scheduled completely
c [treelook-6] limit 6546977 penalty 0 = 0 + 0 boost 1
c [treelook-6] used 6557360 steps
c [treelook-6] 61782 literals remain 76%
c [treelook-6] 14235 variables remain to probed next time 35%
c [decomp-40] removed 2 variables
c [treelook-6] removed 109 variables, found 7234 hbrs
c [unhide-16] limit 13093955 with penalty 0 = 0 + 0
c [unhide-16-30] 14 units, 133 failed, 90180 tauts, 0 hbrs, 56039 literals
c [transred-12] limit 2000000 with penalty 0 = 0 + 0
c [transred-12] removed 215 transitive binary clauses
c [transred-12] found 1 units
c [cce-5] limit of 81837222 steps penalty 2 = 2 + 0
c [cce-5-1] eliminated 1 clauses out of 1 (100%) of length 47
c [cce-5-1] eliminated 1 clauses out of 1 (100%) of length 46
c [cce-5-1] eliminated 1 clauses out of 1 (100%) of length 45
c [cce-5-1] eliminated 2 clauses out of 2 (100%) of length 44
c [cce-5-1] eliminated 3 clauses out of 4 (75%) of length 43
c [cce-5-1] eliminated 1 clauses out of 2 (50%) of length 42
c [cce-5-1] eliminated 2 clauses out of 2 (100%) of length 41
c [cce-5-1] eliminated 1 clauses out of 2 (50%) of length 40
c [cce-5-1] eliminated 2 clauses out of 2 (100%) of length 39
c [cce-5-1] eliminated 1 clauses out of 2 (50%) of length 38
c [cce-5-1] eliminated 2 clauses out of 2 (100%) of length 37
c [cce-5-1] eliminated 1 clauses out of 2 (50%) of length 36
c [cce-5-1] eliminated 2 clauses out of 2 (100%) 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 2 clauses out of 2 (100%) of length 31
c [cce-5-1] eliminated 1 clauses out of 2 (50%) of length 30
c [cce-5-1] eliminated 2 clauses out of 2 (100%) of length 29
c [cce-5-1] eliminated 1 clauses out of 2 (50%) of length 28
c [cce-5-1] eliminated 2 clauses out of 2 (100%) of length 27
c [cce-5-1] eliminated 1 clauses out of 2 (50%) of length 26
c [cce-5-1] eliminated 2 clauses out of 2 (100%) of length 25
c [cce-5-1] eliminated 1 clauses out of 2 (50%) of length 24
c [cce-5-1] eliminated 2 clauses out of 2 (100%) of length 23
c [cce-5-1] eliminated 1 clauses out of 2 (50%) of length 22
c [cce-5-1] eliminated 3 clauses out of 3 (100%) of length 21
c [cce-5-1] eliminated 1 clauses out of 2 (50%) of length 20
c [cce-5-1] eliminated 2 clauses out of 2 (100%) of length 19
c [cce-5-1] eliminated 1 clauses out of 2 (50%) of length 18
c [cce-5-1] eliminated 2 clauses out of 2 (100%) of length 17
c [cce-5-1] eliminated 1 clauses out of 2 (50%) of length 16
c [cce-5-1] eliminated 2 clauses out of 2 (100%) of length 15
c [cce-5-1] eliminated 1 clauses out of 2 (50%) of length 14
c [cce-5-1] eliminated 2 clauses out of 2 (100%) of length 13
c [cce-5-1] eliminated 1 clauses out of 2 (50%) of length 12
c [cce-5-1] eliminated 2 clauses out of 2 (100%) of length 11
c [cce-5-1] eliminated 1 clauses out of 2 (50%) of length 10
c [cce-5-1] eliminated 2 clauses out of 3 (67%) of length 9
c [cce-5-1] eliminated 1 clauses out of 6 (17%) of length 8
c [cce-5-1] eliminated 4 clauses out of 20 (20%) of length 7
c [cce-5-1] eliminated 157 clauses out of 3054 (5%) of length 6
c [cce-5-1] eliminated 20 clauses out of 9704 (0%) of length 5
c [cce-5-1] incomplete large round (ACCE)
c [cce-5-1] eliminated 242 large clauses in 81837222 steps
c [cce-5-1] allowing another 40918611 steps for small clauses
c [cce-5-1] scheduling 181269 clauses = 135946 binary + 45323 ternary
c [cce-5-1] tried to eliminate 2766 small clauses 2%
c [cce-5-1] eliminated 487 binary clauses 0%
c [cce-5-1] eliminated 222 ternary clauses 0%
c [cce-5-1] eliminated 709 small clauses 0%
c [cce-5-1] eliminated 874 small clauses in 81837225 steps
c [cce-5-1] incomplete small round (ACCE)
c [cce-5-1] eliminated 1116 covered clauses in round 1
c [cce-5] eliminated 1116 covered clauses in TOTAL during 1 rounds
c [cce-5] 1116 < 1/100 * 248295 = 2482 considered unsuccessful
c [elim-15] no untried remaining variables left
c [elim-15] scheduled 40312 variables 100%
c [elim-15] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-15] rescheduling of touched variables disabled
c [elim-15-1] eliminated 729 variables 2% in round 1 in 28238328 steps
c [elim-15-1] backward subsumption/strengthening limit 28238300
c [elim-15-1-1] backward checking 3956 touched variables 10%
c [elim-15-1-1] fully completed backward checking in 1 rounds
c [elim-15-1] subsumed 25 and strengthened 7 clauses in 988675 steps
c [elim-15-1] rescheduled 88 variables 0% by backward subsumption
c [elim-15-2] eliminated 3 variables 0% in round 2 in 40962 steps
c [elim-15-2] backward subsumption/strengthening limit 40900
c [elim-15-2-1] backward checking 28 touched variables 0%
c [elim-15-2-1] incomplete backward checking 0 remain 0%
c [elim-15-2] subsumed 0 and strengthened 3 clauses in 40901 steps
c [elim-15-2] rescheduled 9 variables 0% by backward subsumption
c [elim-15-3] no variable eliminated in round 3 in 5173 steps
c [elim-15] fully completed in 3 rounds
c [elim-15] transition to [ all 0 rem 0 ] state
c [elim-15] eliminated 732 = 2% variables out of 40312 scheduled
c [bca-12] limit of 10000000 steps and 490164 added (scaled 2)
c [bca-12] 67101 out of 79162 literals actually usable 85%
c [bca-12] added 37 blocked clauses in 156451 steps
c [sweep-12] limit 19640933 penalty 0 = 0 + 0
c [sweep-12-1] 220 pos 6.4% + 3192 neg 93.6% = 3412 sched 8.6% ret 36168
c [sweep-12-1] 19684474 steps 494 queries 84.41 avg class size
c [sweep-12-1] 2385 decisions 416 SAT calls 68.99 avg env size
c [sweep-12-1] 2493 variables remain 6% (37083 retained 94%)
c [decomp-41] removed 206 variables
c [sweep-12-1] removed 206 vars (0 failed, 81 eqs, 134 impls)
c [sweep-12] removed 206 vars in TOTAL (1 rounds, 493 queries)
c [phase-count-16] 243688 negative 99.8% of 244220 except 532 0.2%
c [phase-count-16] 169888 positive 69.6% of 244220 except 74332 30.4%
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 10172 enqueued variables after 170256 conflicts
c [score-dist-16] active 29202 (74%), one 562 (1%), zero 9610 (24%)
c [score-dist-16] max exp 509, different 346 (68%)
c [score-dist-16] median active exp 497, avg 479.4
c [simplification-16] removed 1221 variables 3.0% (39374 remain 16%)
c [simplification-16] removed 11300 irredundant clauses 4.4% (244220 remain 22%)
c [simplification-16] maximum reduction of 4% = max (3%, 4%)
c [simplification-16] geometric conflict interval increment 6310 = 31554 / 5
c [simplification-16] new conflict interval 37864
c [simplification-16] penalized conflict interval 37864 = 1 * 37864
c [simplification-16] hard conflict limit 227052 (soft 208120 + delta 18932)
c [simplification-16] new conflict limit 208120 (hard 227052)
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  426.7   39373   244220    171793    8285   3339 391888   70   113   43  62%     51   25   57   59   96%
c i  437.7   39372   244220    186028   20178   3406 391965   61    88   61  69%    150   -1   70   59  119%
c i  441.7   39348   244220    190963   24599   3429 391973   50    74   64  68%      6  -14   57   58   99%
c i  442.9   39326   244220    192396   25821   3438 391984   47    67   64  70%    -31  -20   33   57   57%
c i  454.5   39324   244220    205361   36864   3559 392006   75   124   91  60%    123   39   93   58  162%
c i  454.5   39323   244220    205377   36870   3559 392009   75   125   91  60%    121   40   97   58  168%
c i  454.6   39320   244220    205454   36920   3559 392010   77   128   91  61%    107   43  120   58  207%
c i  455.4   39249   244220    206313   37399   3559 392018   86   140   91  61%     14   55  107   59  183%
c 
c [simplification-17] limit 208120 conflicts (hard 227052) hit after 211281 conflicts
c [quatres-13] found 23050 quaternary clauses 60% in total
c [quatres-13-2] added 10 single-self-subsuming ternary resolvents
c [quatres-13-2] added 5 quaternary resolvents
c [ternres-13] limit 74291455 with penalty 0 = 0 + 0
c [ternres-13] all 39248 free variables schedulable
c [ternres-13] 589 ternary resolvents (0 bin, 589 trn)
c [ternres-13] fully completed ternary resolution
c [decomp-42] removed 135 variables
c [basicprobe-6] limit 371457277 penalty 0 = 0 + 0
c [basicprobe-6-0] 10497 sched 28%, 758 failed, 19 lifted, 302191 hbrs
c [decomp-43] removed 1534 variables
c [basicprobe-6-1] 9723 probes remain 26% after last round
c [basicprobe-6-1] 833 units = 814 failed (98%) + 19 lifted (2%)
c [basicprobe-6-1] removed 1683 variables, found 318442 hbrs
c [bate-4] eliminated 818 asymmetric tautologies during probing
c [unhide-17] limit 3714572 with penalty 2 = 0 + 2
c [unhide-17-32] 0 units, 12 failed, 54480 tauts, 0 hbrs, 681302 literals
c [transred-13] limit 2000000 with penalty 0 = 0 + 0
c [transred-13] removed 294 transitive binary clauses
c [elim-16] scheduling all variables this time
c [elim-16] scheduled 37538 variables 100%
c [elim-16] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-16] rescheduling of touched variables disabled
c [elim-16-1] eliminated 1175 variables 3% in round 1 in 27909317 steps
c [elim-16-1] backward subsumption/strengthening limit 27909300
c [elim-16-1-1] backward checking 5646 touched variables 15%
c [elim-16-1-1] fully completed backward checking in 1 rounds
c [elim-16-1] subsumed 44 and strengthened 10 clauses in 1269731 steps
c [elim-16-1] rescheduled 165 variables 0% by backward subsumption
c [elim-16-2] eliminated 9 variables 0% in round 2 in 74475 steps
c [elim-16-2] backward subsumption/strengthening limit 74400
c [elim-16-2-1] backward checking 91 touched variables 0%
c [elim-16-2-1] incomplete backward checking 0 remain 0%
c [elim-16-2] subsumed 6 and strengthened 10 clauses in 74401 steps
c [elim-16-2] rescheduled 44 variables 0% by backward subsumption
c [elim-16-3] eliminated 1 variables 0% in round 3 in 25731 steps
c [elim-16-3] backward subsumption/strengthening limit 25700
c [elim-16-3-1] backward checking 14 touched variables 0%
c [elim-16-3-1] incomplete backward checking 0 remain 0%
c [elim-16-3] subsumed 0 and strengthened 2 clauses in 25701 steps
c [elim-16] incomplete 8 not tried 0% in round 3
c [elim-16] transition to [ all 1 rem 1 ] state
c [elim-16] eliminated 1185 = 3% variables out of 37538 scheduled
c [bca-13] limit of 10000000 steps and 451702 added (scaled 2)
c [bca-13] 58562 out of 72708 literals actually usable 81%
c [bca-13] added 24 blocked clauses in 169243 steps
c [sweep-13] limit 22287436 penalty 0 = 0 + 0
c [sweep-13-1] 148 pos 7.1% + 1941 neg 92.9% = 2089 sched 5.7% ret 34264
c [sweep-13-1] 22340531 steps 759 queries 40.62 avg class size
c [sweep-13-1] 3916 decisions 643 SAT calls 68.65 avg env size
c [sweep-13-1] 900 variables remain 2% (35262 retained 98%)
c [decomp-44] removed 466 variables
c [sweep-13-1] removed 466 vars (0 failed, 116 eqs, 245 impls)
c [sweep-13] removed 466 vars in TOTAL (1 rounds, 758 queries)
c [phase-count-17] 223114 negative 99.8% of 223628 except 514 0.2%
c [phase-count-17] 152775 positive 68.3% of 223628 except 70853 31.7%
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 8147 enqueued variables after 211281 conflicts
c [score-dist-17] active 27740 (77%), one 658 (2%), zero 7489 (21%)
c [score-dist-17] max exp 510, different 332 (65%)
c [score-dist-17] median active exp 491, avg 447.0
c [simplification-17] removed 3361 variables 8.6% (35887 remain 14%)
c [simplification-17] removed 20592 irredundant clauses 8.4% (223628 remain 20%)
c [simplification-17] maximum reduction of 9% = max (9%, 8%)
c [simplification-17] large reduction 9% >= 5% limit
c [simplification-17] next conflict interval 2112 = min (211281/100, 37864)
c [simplification-17] penalized conflict interval 2112 = 1 * 2112
c [simplification-17] hard conflict limit 223393 (soft 213393 + delta 10000)
c [simplification-17] new conflict limit 213393 (hard 223393)
c 
c [simplification-18] limit 213393 conflicts (hard 223393) hit after 223396 conflicts
c [quatres-14] found 21934 quaternary clauses 58% in total
c [quatres-14-1] removed 3 duplicate quaternary clauses
c [quatres-14-2] added 3 quaternary resolvents
c [ternres-14] limit 76822162 with penalty 0 = 0 + 0
c [ternres-14] all 35887 free variables schedulable
c [ternres-14] 559 ternary resolvents (1 bin, 558 trn)
c [ternres-14] fully completed ternary resolution
c [simpleprobe-7] all 35887 free variables schedulable
c [simpleprobe-7] limit 200000000 penalty 0 = 0 + 0
c [decomp-46] removed 108 variables
c [simpleprobe-7] 394 variables remain 1% (35385 retained 99%)
c [simpleprobe-7] removed 108 variables, found 292560 hbrs, 40 units
c [unhide-18] limit 3841108 with penalty 2 = 0 + 2
c [unhide-18-33] 0 units, 6 failed, 138592 tauts, 0 hbrs, 157660 literals
c [transred-14] limit 2000000 with penalty 0 = 0 + 0
c [transred-14] removed 455 transitive binary clauses
c [elim-17] no untried remaining variables left
c [elim-17] scheduled 35775 variables 100%
c [elim-17] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-17] rescheduling of touched variables disabled
c [elim-17-1] eliminated 192 variables 1% in round 1 in 30530837 steps
c [elim-17-1] backward subsumption/strengthening limit 30530800
c [elim-17-1-1] backward checking 1259 touched variables 4%
c [elim-17-1-1] fully completed backward checking in 1 rounds
c [elim-17-1] subsumed 6 and strengthened 5 clauses in 344257 steps
c [elim-17-1] rescheduled 38 variables 0% by backward subsumption
c [elim-17-2] eliminated 3 variables 0% in round 2 in 19669 steps
c [elim-17-2] backward subsumption/strengthening limit 19600
c [elim-17-2-1] backward checking 32 touched variables 0%
c [elim-17-2-1] incomplete backward checking 0 remain 0%
c [elim-17-2] subsumed 2 and strengthened 3 clauses in 19601 steps
c [elim-17-2] rescheduled 17 variables 0% by backward subsumption
c [elim-17-3] eliminated 1 variables 0% in round 3 in 17104 steps
c [elim-17-3] backward subsumption/strengthening limit 17100
c [elim-17-3-1] backward checking 12 touched variables 0%
c [elim-17-3-1] incomplete backward checking 0 remain 0%
c [elim-17-3] subsumed 0 and strengthened 2 clauses in 17101 steps
c [elim-17] incomplete 8 not tried 0% in round 3
c [elim-17] transition to [ all 1 rem 1 ] state
c [elim-17] eliminated 196 = 1% variables out of 35775 scheduled
c [elim-17] 196 < 1/100 * 35775 = 357 considered unsuccessful
c [bca-14] limit of 10000000 steps and 445228 added (scaled 2)
c [bca-14] 56570 out of 71160 literals actually usable 79%
c [bca-14] added 11 blocked clauses in 173452 steps
c [sweep-14] limit 23046648 penalty 0 = 0 + 0
c [sweep-14-1] 58 pos 7.3% + 740 neg 92.7% = 798 sched 2.2% ret 34781
c [sweep-14-1] 23130984 steps 616 queries 14.12 avg class size
c [sweep-14-1] 3201 decisions 516 SAT calls 102.25 avg env size
c [sweep-14-1] 17 variables remain 0% (35562 retained 100%)
c [decomp-47] removed 122 variables
c [sweep-14-1] removed 122 vars (0 failed, 99 eqs, 203 impls)
c [sweep-14] removed 122 vars in TOTAL (1 rounds, 615 queries)
c [phase-count-18] 221383 negative 99.8% of 221889 except 506 0.2%
c [phase-count-18] 151213 positive 68.1% of 221889 except 70676 31.9%
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 7971 enqueued variables after 223396 conflicts
c [score-dist-18] active 27486 (78%), one 730 (2%), zero 7241 (20%)
c [score-dist-18] max exp 510, different 339 (66%)
c [score-dist-18] median active exp 483, avg 436.6
c [simplification-18] removed 430 variables 1.2% (35457 remain 14%)
c [simplification-18] removed 1739 irredundant clauses 0.8% (221889 remain 20%)
c [simplification-18] maximum reduction of 1% = max (1%, 1%)
c [simplification-18] geometric conflict interval increment 18932 = 37864 / 2
c [simplification-18] new conflict interval 56796
c [simplification-18] penalized conflict interval 56796 = 1 * 56796
c [simplification-18] hard conflict limit 308590 (soft 280192 + delta 28398)
c [simplification-18] new conflict limit 280192 (hard 308590)
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  497.5   35456   221889    224640   51583   3733 696802   32    53  128  60%    188  -31   33   55   61%
c -  502.6   35456   221889    229848   27192   3769 696851   57    87   58  66%    -15    4  105   55  190%
c -  527.9   35456   221889    263837   29412   3823 696924   26    39   57  66%    405  -26   26   43   61%
c i  545.4   35455   221889    289881   52452   3845 696955   17    24   79  71%    608  -28   19   34   56%
c -  550.9   35454   221889    297371   30810   3861 696958   23    34   57  69%   -270  -16   20   33   60%
c 
c [simplification-19] limit 280192 conflicts (hard 308590) hit after 308591 conflicts
c [quatres-15] found 21847 quaternary clauses 56% in total
c [quatres-15-1] removed 2 duplicate quaternary clauses
c [quatres-15-2] added 3 single-self-subsuming ternary resolvents
c [quatres-15-2] added 1 quaternary resolvents
c [ternres-15] limit 92755536 with penalty 0 = 0 + 0
c [ternres-15] all 35454 free variables schedulable
c [ternres-15] 165 ternary resolvents (2 bin, 163 trn)
c [ternres-15] fully completed ternary resolution
c [decomp-48] removed 4 variables
c [treelook-7] limit 9275553 penalty 0 = 0 + 0 boost 1
c [treelook-7] scheduled 54053 literals 76%
c [treelook-7] scheduling used 1521057 steps
c [treelook-7] scheduled completely
c [treelook-7] limit 9275553 penalty 0 = 0 + 0 boost 1
c [treelook-7] used 9343572 steps
c [treelook-7] 53247 literals remain 75%
c [treelook-7] 11794 variables remain to probed next time 33%
c [treelook-7] removed 137 variables, found 13018 hbrs
c [unhide-19] limit 9275553 with penalty 1 = 0 + 1
c [unhide-19-37] 0 units, 3 failed, 114339 tauts, 0 hbrs, 284866 literals
c [transred-15] limit 2000000 with penalty 0 = 0 + 0
c [transred-15] removed 335 transitive binary clauses
c [transred-15] found 1 units
c [cce-6] limit of 57972210 steps penalty 3 = 3 + 0
c [cce-6-1] eliminated 1 clauses out of 1 (100%) of length 99
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 98
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 97
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 96
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 95
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 94
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 93
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 92
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 91
c [cce-6-1] eliminated 3 clauses out of 3 (100%) of length 90
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 89
c [cce-6-1] eliminated 1 clauses out of 1 (100%) of length 88
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 87
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 86
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 85
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 84
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 83
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 82
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 81
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 80
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 79
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 78
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 77
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 76
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 75
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 74
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 73
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 72
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 71
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 70
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 69
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 68
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 67
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 66
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 65
c [cce-6-1] eliminated 1 clauses out of 3 (33%) of length 64
c [cce-6-1] eliminated 3 clauses out of 3 (100%) of length 63
c [cce-6-1] eliminated 3 clauses out of 4 (75%) of length 62
c [cce-6-1] eliminated 3 clauses out of 3 (100%) of length 61
c [cce-6-1] eliminated 3 clauses out of 4 (75%) of length 60
c [cce-6-1] eliminated 3 clauses out of 4 (75%) of length 59
c [cce-6-1] eliminated 3 clauses out of 4 (75%) of length 58
c [cce-6-1] eliminated 3 clauses out of 4 (75%) of length 57
c [cce-6-1] eliminated 2 clauses out of 4 (50%) of length 56
c [cce-6-1] eliminated 4 clauses out of 4 (100%) of length 55
c [cce-6-1] eliminated 2 clauses out of 4 (50%) of length 54
c [cce-6-1] eliminated 4 clauses out of 4 (100%) of length 53
c [cce-6-1] eliminated 2 clauses out of 3 (67%) of length 52
c [cce-6-1] eliminated 4 clauses out of 4 (100%) of length 51
c [cce-6-1] eliminated 2 clauses out of 4 (50%) of length 50
c [cce-6-1] eliminated 4 clauses out of 4 (100%) of length 49
c [cce-6-1] eliminated 2 clauses out of 5 (40%) of length 48
c [cce-6-1] eliminated 4 clauses out of 4 (100%) of length 47
c [cce-6-1] eliminated 2 clauses out of 3 (67%) of length 46
c [cce-6-1] eliminated 4 clauses out of 4 (100%) of length 45
c [cce-6-1] eliminated 2 clauses out of 4 (50%) of length 44
c [cce-6-1] eliminated 4 clauses out of 5 (80%) of length 43
c [cce-6-1] eliminated 4 clauses out of 7 (57%) of length 42
c [cce-6-1] eliminated 5 clauses out of 7 (71%) of length 41
c [cce-6-1] eliminated 4 clauses out of 8 (50%) of length 40
c [cce-6-1] eliminated 7 clauses out of 9 (78%) of length 39
c [cce-6-1] eliminated 7 clauses out of 12 (58%) of length 38
c [cce-6-1] eliminated 10 clauses out of 11 (91%) of length 37
c [cce-6-1] eliminated 8 clauses out of 13 (62%) of length 36
c [cce-6-1] eliminated 9 clauses out of 12 (75%) of length 35
c [cce-6-1] eliminated 8 clauses out of 13 (62%) of length 34
c [cce-6-1] eliminated 15 clauses out of 17 (88%) of length 33
c [cce-6-1] eliminated 10 clauses out of 19 (53%) of length 32
c [cce-6-1] eliminated 19 clauses out of 20 (95%) of length 31
c [cce-6-1] eliminated 10 clauses out of 20 (50%) of length 30
c [cce-6-1] eliminated 20 clauses out of 20 (100%) of length 29
c [cce-6-1] eliminated 10 clauses out of 21 (48%) of length 28
c [cce-6-1] eliminated 20 clauses out of 20 (100%) of length 27
c [cce-6-1] eliminated 10 clauses out of 22 (45%) of length 26
c [cce-6-1] eliminated 20 clauses out of 20 (100%) of length 25
c [cce-6-1] eliminated 9 clauses out of 19 (47%) of length 24
c [cce-6-1] eliminated 19 clauses out of 20 (95%) of length 23
c [cce-6-1] eliminated 12 clauses out of 22 (55%) of length 22
c [cce-6-1] eliminated 19 clauses out of 22 (86%) of length 21
c [cce-6-1] eliminated 16 clauses out of 24 (67%) of length 20
c [cce-6-1] eliminated 20 clauses out of 27 (74%) of length 19
c [cce-6-1] eliminated 17 clauses out of 25 (68%) of length 18
c [cce-6-1] eliminated 24 clauses out of 28 (86%) of length 17
c [cce-6-1] eliminated 15 clauses out of 25 (60%) of length 16
c [cce-6-1] eliminated 24 clauses out of 26 (92%) of length 15
c [cce-6-1] eliminated 18 clauses out of 29 (62%) of length 14
c [cce-6-1] eliminated 24 clauses out of 27 (89%) of length 13
c [cce-6-1] eliminated 18 clauses out of 30 (60%) of length 12
c [cce-6-1] eliminated 27 clauses out of 31 (87%) of length 11
c [cce-6-1] eliminated 21 clauses out of 35 (60%) of length 10
c [cce-6-1] eliminated 29 clauses out of 37 (78%) of length 9
c [cce-6-1] eliminated 26 clauses out of 43 (60%) of length 8
c [cce-6-1] eliminated 36 clauses out of 63 (57%) of length 7
c [cce-6-1] eliminated 38 clauses out of 2933 (1%) of length 6
c [cce-6-1] eliminated 27 clauses out of 8827 (0%) of length 5
c [cce-6-1] incomplete large round (ATE)
c [cce-6-1] eliminated 752 large clauses in 57972217 steps
c [cce-6-1] allowing another 28986108 steps for small clauses
c [cce-6-1] scheduling 150323 clauses = 127397 binary + 22926 ternary
c [cce-6-1] tried to eliminate 2351 small clauses 2%
c [cce-6-1] eliminated 385 binary clauses 0%
c [cce-6-1] eliminated 154 ternary clauses 1%
c [cce-6-1] eliminated 539 small clauses 0%
c [cce-6-1] eliminated 557 small clauses in 57972211 steps
c [cce-6-1] incomplete small round (ATE)
c [cce-6-1] eliminated 1309 covered clauses in round 1
c [cce-6] eliminated 1309 covered clauses in TOTAL during 1 rounds
c [cce-6] 1309 < 1/100 * 218087 = 2180 considered unsuccessful
c [bca-15] limit of 10000000 steps and 434726 added (scaled 2)
c [bca-15] 56004 out of 70624 literals actually usable 79%
c [bca-15] added 10 blocked clauses in 162681 steps
c [sweep-15] limit 27826660 penalty 0 = 0 + 0
c [sweep-15-1] 0 pos 0.0% + 12 neg 100.0% = 12 sched 0.0% ret 35299
c [sweep-15-1] 755752 steps 9 queries 3.89 avg class size
c [sweep-15-1] 67 decisions 8 SAT calls 169.50 avg env size
c [sweep-15-1] fully completed sweeping round
c [decomp-50] removed 1 variables
c [sweep-15-1] removed 1 vars (0 failed, 0 eqs, 3 impls)
c [sweep-15-2] 2853 pos 8.1% + 32457 neg 91.9% = 35310 sched 100.0% ret 0
c [sweep-15-2] 27110921 steps 403 queries 521.69 avg class size
c [sweep-15-2] 7785 decisions 394 SAT calls 166.28 avg env size
c [sweep-15-2] 24876 variables remain 71% (10395 retained 29%)
c [decomp-51] removed 58 variables
c [sweep-15-2] removed 58 vars (0 failed, 13 eqs, 42 impls)
c [sweep-15] removed 59 vars in TOTAL (2 rounds, 410 queries)
c [sort-queue-19] sorted 11061 enqueued variables after 308591 conflicts
c [score-dist-19] active 24191 (69%), one 4182 (12%), zero 6879 (20%)
c [score-dist-19] max exp 510, different 413 (81%)
c [score-dist-19] median active exp 502, avg 428.6
c [simplification-19] removed 202 variables 0.6% (35252 remain 14%)
c [simplification-19] removed 6332 irredundant clauses 2.9% (215557 remain 19%)
c [simplification-19] maximum reduction of 3% = max (1%, 3%)
c [simplification-19] geometric conflict interval increment 14199 = 56796 / 4
c [simplification-19] new conflict interval 70995
c [simplification-19] penalized conflict interval 70995 = 1 * 70995
c [simplification-19] hard conflict limit 415083 (soft 379586 + delta 35497)
c [simplification-19] new conflict limit 379586 (hard 415083)
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 -  586.3   35252   215557    331227   31031   3947 599515   14    19   54  72%    251  -20   13   26   51%
c -  613.9   35252   215557    367037   31952   3994 599572   17    22   54  79%    577  -15   16   25   66%
c -  637.6   35252   215557    401970   33265   4020 599588   15    18   54  83%    761  -11   16   21   76%
c 
c [simplification-20] limit 379586 conflicts (hard 415083) hit after 415085 conflicts
c [quatres-16] found 18850 quaternary clauses 52% in total
c [quatres-16-1] removed 1 duplicate quaternary clauses
c [quatres-16-2] added 5 single-self-subsuming ternary resolvents
c [quatres-16-2] added 11 quaternary resolvents
c [ternres-16] limit 113248041 with penalty 0 = 0 + 0
c [ternres-16] all 35252 free variables schedulable
c [ternres-16] 171 ternary resolvents (0 bin, 171 trn)
c [ternres-16] fully completed ternary resolution
c [gauss-6] limit 1415600 penalty 4 = 4 + 0
c [gauss-6] extracted 47 xors of average arity 3.0
c [gauss-6] connected 140 occurrences of 136 variables (average 1.0)
c [gauss-6] limit 1415600 penalty 4 = 4 + 0
c [gauss-6] fully completed
c [gauss-6] exported 0 unary, 0 binary and 0 ternary equations
c [basicprobe-7] limit 400000000 penalty 0 = 0 + 0
c [basicprobe-7-0] 9478 sched 27%, 363 failed, 12 lifted, 126475 hbrs
c [decomp-53] removed 783 variables
c [basicprobe-7-1] 8224 probes remain 24% after last round
c [basicprobe-7-1] 463 units = 446 failed (96%) + 17 lifted (4%)
c [basicprobe-7-1] removed 930 variables, found 143070 hbrs
c [bate-5] eliminated 207 asymmetric tautologies during probing
c [unhide-20] limit 10000000 with penalty 1 = 0 + 1
c [unhide-20-41] 0 units, 19 failed, 109000 tauts, 0 hbrs, 102269 literals
c [transred-16] limit 2000000 with penalty 0 = 0 + 0
c [transred-16] removed 248 transitive binary clauses
c [block-6] scheduling all variables this time
c [block-6] scheduled 34314 variables 100%
c [block-6] limit of 50000000 steps penalty 4 = 4 + 0
c [block-6] fully completed
c [block-6] transition to [ all 0 rem 0 ] state
c [block-6] eliminated 133 blocked clauses
c [block-6] 133 < 1/100 * 206604 = 2066 considered unsuccessful
c [elim-18] no untried remaining variables left
c [elim-18] scheduled 34314 variables 100%
c [elim-18] boosting limit by 20
c [elim-18] limit of 8000000000 steps penalty 1 = 1 + 0
c [elim-18] rescheduling of touched variables disabled
c [elim-18-1] eliminated 1293 variables 4% in round 1 in 22874501 steps
c [elim-18-1] backward subsumption/strengthening limit 22874500
c [elim-18-1-1] backward checking 5778 touched variables 17%
c [elim-18-1-1] fully completed backward checking in 1 rounds
c [elim-18-1] subsumed 29 and strengthened 10 clauses in 1369101 steps
c [elim-18-1] rescheduled 120 variables 0% by backward subsumption
c [elim-18-2] eliminated 9 variables 0% in round 2 in 57543 steps
c [elim-18-2] backward subsumption/strengthening limit 57500
c [elim-18-2-1] backward checking 89 touched variables 0%
c [elim-18-2-1] incomplete backward checking 12 remain 13%
c [elim-18-2] subsumed 12 and strengthened 11 clauses in 57508 steps
c [elim-18-2] rescheduled 39 variables 0% by backward subsumption
c [elim-18-3] eliminated 1 variables 0% in round 3 in 165423 steps
c [elim-18-3] backward subsumption/strengthening limit 165400
c [elim-18-3-1] backward checking 25 touched variables 0%
c [elim-18-3-1] fully completed backward checking in 1 rounds
c [elim-18-3] subsumed 0 and strengthened 4 clauses in 103529 steps
c [elim-18] incomplete 16 not tried 0% in round 3
c [elim-18] transition to [ all 1 rem 1 ] state
c [elim-18] eliminated 1303 = 4% variables out of 34314 scheduled
c [bca-16] limit of 10000000 steps and 411867 added (scaled 2)
c [bca-16] 51558 out of 66024 literals actually usable 78%
c [bca-16] added 12 blocked clauses in 155465 steps
c [sweep-16] limit 33974412 penalty 0 = 0 + 0
c [sweep-16-1] 2322 pos 9.8% + 21280 neg 90.2% = 23602 sched 71.5% ret 9409
c [sweep-16-1] 33994323 steps 821 queries 173.02 avg class size
c [sweep-16-1] 9882 decisions 782 SAT calls 102.93 avg env size
c [sweep-16-1] 14800 variables remain 45% (18178 retained 55%)
c [decomp-54] removed 85 variables
c [sweep-16-1] removed 85 vars (0 failed, 44 eqs, 107 impls)
c [sweep-16] removed 85 vars in TOTAL (1 rounds, 820 queries)
c [sort-queue-20] sorted 10036 enqueued variables after 415085 conflicts
c [score-dist-20] active 22890 (70%), one 4493 (14%), zero 5543 (17%)
c [score-dist-20] max exp 510, different 374 (73%)
c [score-dist-20] median active exp 502, avg 439.5
c [simplification-20] removed 2326 variables 6.6% (32926 remain 13%)
c [simplification-20] removed 10531 irredundant clauses 4.9% (205026 remain 18%)
c [simplification-20] maximum reduction of 7% = max (7%, 5%)
c [simplification-20] large reduction 7% >= 5% limit
c [simplification-20] next conflict interval 4150 = min (415085/100, 70995)
c [simplification-20] penalized conflict interval 4150 = 1 * 4150
c [simplification-20] hard conflict limit 429235 (soft 419235 + delta 10000)
c [simplification-20] new conflict limit 419235 (hard 429235)
c 
c [simplification-21] limit 419235 conflicts (hard 429235) hit after 429237 conflicts
c [quatres-17] found 17876 quaternary clauses 49% in total
c [quatres-17-1] removed 1 duplicate quaternary clauses
c [quatres-17-2] added 6 quaternary resolvents
c [ternres-17] limit 115672129 with penalty 0 = 0 + 0
c [ternres-17] all 32926 free variables schedulable
c [ternres-17] 304 ternary resolvents (2 bin, 302 trn)
c [ternres-17] fully completed ternary resolution
c [card-6] limit 3614754 penalty 4 = 4 + 0
c [card-6] found 4510 at-most-one constraints of average size 3.8
c [card-6] no at-most-two constraint found
c [card-6] using previous limit 3614754 for elimination
c [card-6] 4510 out of 4510 constraints (100%) meet size limits
c [card-6] no units found
c [card-6] no at-most-one constraints generated
c [simpleprobe-8] 174 schedulable variables 1%
c [simpleprobe-8] limit 200000000 penalty 0 = 0 + 0
c [decomp-56] removed 15 variables
c [simpleprobe-8] fully completed simple probing
c [simpleprobe-8] removed 15 variables, found 39357 hbrs, 7 units
c [unhide-21] limit 10000000 with penalty 1 = 0 + 1
c [unhide-21-46] 0 units, 17 failed, 64254 tauts, 0 hbrs, 154705 literals
c [transred-17] limit 2000000 with penalty 0 = 0 + 0
c [transred-17] removed 314 transitive binary clauses
c [elim-19] no untried remaining variables left
c [elim-19] scheduled 32898 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 119 variables 0% in round 1 in 35340866 steps
c [elim-19-1] backward subsumption/strengthening limit 35340800
c [elim-19-1-1] backward checking 896 touched variables 3%
c [elim-19-1-1] fully completed backward checking in 1 rounds
c [elim-19-1] subsumed 4 and strengthened 1 clauses in 240820 steps
c [elim-19-1] rescheduled 16 variables 0% by backward subsumption
c [elim-19-2] no variable eliminated in round 2 in 9433 steps
c [elim-19] fully completed in 2 rounds
c [elim-19] transition to [ all 0 rem 0 ] state
c [elim-19] eliminated 119 = 0% variables out of 32898 scheduled
c [elim-19] 119 < 1/100 * 32898 = 328 considered unsuccessful
c [bca-17] limit of 10000000 steps and 406231 added (scaled 2)
c [bca-17] 50481 out of 65560 literals actually usable 77%
c [bca-17] added 9 blocked clauses in 166060 steps
c [sweep-17] limit 34701638 penalty 0 = 0 + 0
c [sweep-17-1] 1665 pos 11.3% + 13101 neg 88.7% = 14766 sched 45.0% ret 18013
c [sweep-17-1] 34712703 steps 888 queries 141.29 avg class size
c [sweep-17-1] 8411 decisions 858 SAT calls 77.42 avg env size
c [sweep-17-1] 9639 variables remain 29% (23137 retained 71%)
c [decomp-57] removed 35 variables
c [sweep-17-1] removed 35 vars (0 failed, 31 eqs, 98 impls)
c [sweep-17] removed 35 vars in TOTAL (1 rounds, 887 queries)
c [sort-queue-21] sorted 9279 enqueued variables after 429237 conflicts
c [score-dist-21] active 23465 (72%), one 3887 (12%), zero 5392 (16%)
c [score-dist-21] max exp 510, different 366 (72%)
c [score-dist-21] median active exp 501, avg 450.6
c [simplification-21] removed 182 variables 0.6% (32744 remain 13%)
c [simplification-21] removed 2569 irredundant clauses 1.3% (202457 remain 18%)
c [simplification-21] maximum reduction of 1% = max (1%, 1%)
c [simplification-21] geometric conflict interval increment 35497 = 70995 / 2
c [simplification-21] new conflict interval 106492
c [simplification-21] penalized conflict interval 106492 = 1 * 106492
c [simplification-21] hard conflict limit 588975 (soft 535729 + delta 53246)
c [simplification-21] new conflict limit 535729 (hard 588975)
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 -  689.3   32744   202457    437285   33911   3621 374662   16    20   49  80%    871   -5   15   19   77%
c -  714.1   32744   202457    473561   34539   3653 374686   21    29   51  74%    936    3   16   19   81%
c -  738.9   32744   202457    510012   35772   3665 374693   14    17   52  82%    974   -5   14   17   77%
c -  767.0   32744   202457    548192   37018   3684 374710   11    13   52  85%    996   -8   10   15   66%
c 
c [simplification-22] limit 535729 conflicts (hard 588975) hit after 575419 conflicts
c [quatres-18] found 17961 quaternary clauses 46% in total
c [quatres-18-1] removed 1 duplicate quaternary clauses
c [quatres-18-2] added 5 quaternary resolvents
c [ternres-18] limit 143448475 with penalty 0 = 0 + 0
c [ternres-18] all 32744 free variables schedulable
c [ternres-18] 114 ternary resolvents (0 bin, 114 trn)
c [ternres-18] fully completed ternary resolution
c [treelook-8] limit 14344847 penalty 0 = 0 + 0 boost 1
c [treelook-8] scheduled 49217 literals 75%
c [treelook-8] scheduling used 1010499 steps
c [treelook-8] scheduled completely
c [treelook-8] limit 14344847 penalty 0 = 0 + 0 boost 1
c [treelook-8] used 14355136 steps
c [treelook-8] 48858 literals remain 75%
c [treelook-8] 10254 variables remain to probed next time 31%
c [treelook-8] removed 4 variables, found 110486 hbrs
c [unhide-22] limit 10000000 with penalty 1 = 0 + 1
c [unhide-22-50] 0 units, 4 failed, 75264 tauts, 0 hbrs, 246295 literals
c [transred-18] limit 2000000 with penalty 0 = 0 + 0
c [transred-18] removed 263 transitive binary clauses
c [bca-18] limit of 10000000 steps and 404123 added (scaled 2)
c [bca-18] 49842 out of 65474 literals actually usable 76%
c [bca-18] added 6 blocked clauses in 167362 steps
c [sweep-18] almost no limit of 4000000000 steps
c [sweep-18-1] 1250 pos 13.0% + 8386 neg 87.0% = 9636 sched 29.4% ret 23100
c [sweep-18-1] 102533910 steps 3265 queries 20.86 avg class size
c [sweep-18-1] 18909 decisions 3107 SAT calls 65.92 avg env size
c [sweep-18-1] fully completed sweeping round
c [decomp-60] removed 172 variables
c [sweep-18-1] removed 172 vars (0 failed, 161 eqs, 471 impls)
c [sweep-18-2] 2927 pos 9.0% + 29637 neg 91.0% = 32564 sched 100.0% ret 0
c [sweep-18-2] 175567890 steps 4517 queries 53.07 avg class size
c [sweep-18-2] 40310 decisions 4392 SAT calls 86.21 avg env size
c [sweep-18-2] fully completed sweeping round
c [decomp-61] removed 179 variables
c [sweep-18-2] removed 179 vars (0 failed, 135 eqs, 450 impls)
c [sweep-18-3] 2925 pos 9.0% + 29460 neg 91.0% = 32385 sched 100.0% ret 0
c [sweep-18-3] 177038458 steps 4496 queries 47.52 avg class size
c [sweep-18-3] 39750 decisions 4409 SAT calls 83.14 avg env size
c [sweep-18-3] fully completed sweeping round
c [decomp-62] removed 109 variables
c [sweep-18-3] removed 109 vars (0 failed, 96 eqs, 361 impls)
c [sweep-18] removed 460 vars in TOTAL (3 rounds, 12275 queries)
c [sort-queue-22] sorted 7751 enqueued variables after 575419 conflicts
c [score-dist-22] active 24525 (76%), one 2844 (9%), zero 4907 (15%)
c [score-dist-22] max exp 511, different 336 (66%)
c [score-dist-22] median active exp 503, avg 486.1
c [simplification-22] removed 468 variables 1.4% (32276 remain 13%)
c [simplification-22] removed 2222 irredundant clauses 1.1% (200235 remain 18%)
c [simplification-22] maximum reduction of 1% = max (1%, 1%)
c [simplification-22] geometric conflict interval increment 53246 = 106492 / 2
c [simplification-22] new conflict interval 159738
c [simplification-22] penalized conflict interval 159738 = 1 * 159738
c [simplification-22] hard conflict limit 815026 (soft 735157 + delta 79869)
c [simplification-22] new conflict limit 735157 (hard 815026)
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 -  824.3   32276   200235    587498   39270   3791 454376   12    15   53  81%   1009   -3   18   14  125%
c -  852.9   32276   200235    628378   40345   3799 454378   13    15   53  88%   1016   -2   13   14   92%
c i  874.1   32275   200235    658846   64878   3804 454386   12    15   82  83%   1019   -1   11   13   86%
c i  875.2   32274   200235    660370   66212   3804 454387   12    15   82  83%  -3382   -1   12   13   90%
c -  883.2   32274   200235    671136   41003   3819 454387   11    14   53  81%  -3856   -2   11   13   87%
c -  914.8   32274   200235    714210   41736   3828 454389   11    14   53  78%  -1505   -1   11   12   88%
c i  934.4   32273   200235    740991   62770   3892 454407    8     9   85  86%   -657   -5    6   11   57%
c i  938.7   31893   200235    745957   66709   3931 454412    8    10   85  85%  -1710   -4    6   11   51%
c i  938.7   31473   200235    745987   66733   3932 454416    8    10   85  85%  -1712   -4    5   11   49%
c -  950.5   31456   200235    761294   44417   3961 454422   10    11   54  88%  -1210   -2    9   11   86%
c i  953.7   31455   200235    766004   48255   3976 454432    9    10   68  88%  -1056   -3    7   11   69%
c i  958.1   30968   200235    772114   53131   4000 454443    8     9   68  87%  -1159   -3    5   10   52%
c i  960.0   29363   200235    775156   55370   4026 454453    8     9   68  88%  -1148   -4    5   10   51%
c i  960.0   29320   200235    775189   55394   4026 454453    8     9   68  88%  -1149   -4    5   10   49%
c i  960.0   26856   200235    775196   55391   4028 454454    8     9   68  88%  -1149   -4    5   10   48%
c i  960.1   26340   200235    775410   55524   4036 454456    8     9   68  88%  -1152   -4    5   10   44%
c i  960.2   26326   200235    775547   55576   4050 454464    7     8   68  88%  -1153   -4    4   10   40%
c i  960.2   26055   200235    775578   55587   4054 454466    7     8   68  88%  -1153   -4    4   10   39%
c i  960.2   25733   200235    775580   55587   4054 454467    7     8   68  88%  -1153   -4    4   10   39%
c i  960.2   25391   200235    775595   55596   4054 454469    7     8   68  89%  -1153   -4    4   10   38%
c i  960.2   25180   200235    775599   55596   4054 454470    7     8   68  89%  -1153   -4    4   10   38%
c i  960.3   24813   200235    775606   55598   4056 454471    7     8   68  89%  -1153   -4    4   10   37%
c i  960.3   24659   200235    775607   55598   4056 454471    7     8   68  89%  -1153   -4    4   10   37%
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  960.3   21157   200235    775607   55598   4056 454471    7     8   68  89%  -1153   -4    4   10   37%
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
s UNSATISFIABLE
c
c bate: 2513 basic ate = 2437 trn 97% + 76 lrg 3% in 5 updates
c bcas: 18 count, 1377 added (132 skipped), 5215494 steps
c bkwd: tried 694035 clauses, 1387211 lits, 2.00 lits/clause
c bkwd: checked 17521377 occs, 25.25 occs/clause, 12.63 occs/lit
c bkwd: subsumed 18 binary, 634 ternary, 74 large
c bkwd: strengthened 1 binary, 1 ternary (100% self), 1188 large (0% self)
c blkd: 6 bces, 10872 removed, 8009940 resolutions, 21899618 steps
c blkd: 12116 blocking literals 2%, 5 pure
c bump: 780245 bumped seen, 476276368 lits 610.4 on average
c card: 6 count, 0 units, 0 am1, 245724557 steps
c card: 0 rescheduled, 0 eliminated, 0 resolved, 103292 subsumed
c card: 23935 at-most-one constraints found, average size 4.38
c card: 23935 at-most-one constraints used 100%, average size 4.38
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: 6 cces, 34283 eliminated, 34215 ate 100%, 68 abce 0%
c cces: 0 probed, 0 lifted, 0 failed
c cces: 0 cached, 0 rsz, 0 cols 0%, 0 srch, 0 hits 0%
c clls: 1 sat, 0 simp, 0 freeze, 0 melt
c clls: 3776495 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 177 gcs, 0 rescored clauses, 3021 rescored vars
c dcps: 62 decompositions, 15363 equivalent 6%
c deco: 35368 decision-only clauses 5%, 69% reduction
c decs: 3734400 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 19 elims, 121794 eliminated 46%, 27 pure 0%
c elms: 55 rounds, 2.9 rounds/bve
c elms: 104583 small 86%, 17179 large 14%
c elms: 460814 tried small, 104583 succeeded 23%, 356231 failed 77%
c elms: 55454 subsumed, 75487 strengthened, 1100 blocked
c elms: 27566593 copies, 26535427 resolutions, 19576634 ipos
c elms: 6912487 subchks, 5249196 strchks
c gaus: 6 extractions, 1063 extracted, 2.2 size, 3 max
c gaus: exported 0 units, 20 binary and 0 ternary equations
c gaus: 0 gc, 20822576 steps, 10411288 extr 50%, 42666 elim 0%
c glue: 34.0 orig avg, 34.0 real avg, 4.5 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 1927937 = 576101 simple 30% + 1262610 trn 65% + 89226 lrg 5%, 4661 sub 0%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 780245 clauses, 196.6 length
c lrnd: 153427258 lits = 295095509 orig - 141668251 removed 48%
c lrnd: 308527 uips 40%, 427399 flips 55%
c mins: 734426 mins 95%, 1679 bin 0%, 3536 size 0%
c mins: 395144746 poisoned searches, 87611944 hits, 22% hit rate
c mins: 544949656 used twice searches, 10280580 hits, 2% hit rate
c move: moved 24512, 13446 bin 55%, 11066 trn 45%
c otfs: 1252 driving 28%, 3148 restarting 72%
c otfs: str 4400, 4304 red 98%, 96 irr 2%
c otfs: str 4400, 0 bin 0%, 80 trn 2%, 4320 lrg 98%
c otfs: sub 31, 31 red 100%, 0 irr 0%
c otfs: sub 31, 0 bin 0%, 1 trn 3%, 30 lrg 97%
c phas: 18 computed, 125100 set, 36 pos (0%), 125064 neg (100%)
c prbs: 7 basic, 70520 probed, 3391 failed, 57 lifted
c prbs: 8 simple, 1186400 probed, 1753 failed, 4597 eqs
c prbs: 8 treelook, 1565 probed, 104 failed, 0 lifted
c prom: 105200 locked 6% out of 1673259 tried
c prps: 2990220000 props, 751 props/dec
c prps: 94% srch, 6% simp, 0% lkhd
c quat: 18 count, 142 quat, 46 self1, 0 self2, 2939 dup
c queu: 22 sorted, 3734400 next (69362 steps 0.02)
c queu: 560783450 enq (876945528 steps 1.56), 476276368 deq 85%
c redc: 3486 clauses 16%, 21914 tried 3%, 15 sat 0%
c redc: 6513 lits 3%, 224038 tried 0%, 15 sat 0%
c redc: 299 times jump level reduced, 44.3 levels on average
c reds: 17 count, 45623.9 conflicts per reduce
c reds: 0 memlim 0%, 17 arith 100%
c reds: 493045 collected 93%, 34613 retired 7%
c rmbd: 63637 removed, 28028 red 44%
c rsts: 7249 restarts 97%, 224 skipped 3%
c rsts: 224 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: 22 count, 20 confs 91%, 0 vars 0%
c simp: 1 its 5%, 1 bin 5%, 0 trns 0%
c subl: 780245 count (796189 tried 1.0), 109266 sub out of 775407 (14.1%)
c swps: 18 count, 21 rounds, 22361 queries (1064.8/round)
c swps: 20586 sat calls, 163 unsat (0.3% success rate)
c swps: 169653 decisions 8.2, 5890 conflicts 0.3
c swps; 204.7 avg class size, 80.7 avg environment size
c swps: 2 failed, 3914 impls, 1895 equivs
c swp0: 7446 type 0 queries, 3905 unsat (52.4%), 6859 sat (92.1%)
c swp1: 14915 type 1 queries, 8404 unsat (56.3%), 13607 sat (91.2%)
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: 9036122 calls to obtain time
c tops: 103939 fixed 40%, 350 its, 2216.02 confs/it
c trds: 18 transitive reductions, 4093 removed, 19 failed
c trds: 23541 nodes, 67698 edges, 36048485 steps
c trim: 2378288 words, 9.1 MB
c trnr: 18 count, 40 bin, 10808 trn, 116463234 steps
c unhd: 22 count, 50 rounds, 135413954 steps
c unhd: 3586 non-trivial sccs of average size 2.2
c unhd: 109 units, 108 bin, 1 trn, 0 lrg
c unhd: 7811 failed, 7750 stamp, 0 lits, 33 bin, 9 trn, 0 lrg
c unhd: 932929 tauts, 10505 bin 1%, 18387 trn 2%, 410 lrg 0%
c unhd: 932929 tauts, 903627 stamp 97%, 871386 red 93%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 4577662 str, 108 bin 0%, 9020 trn 0%, 4568534 lrg 100%, 4533665 red 99%
c vars: 21157 remaining 8% and 241096 removed 92% out of 262253
c vars: 103939 fixed 40%, 121794 eliminated 46%, 15363 equivalent 6%
c vsts: 20054102963 visits, 92% srch, 8% simp, 0% lkhd
c vsts: 6.6 search visits per propagation, 23703.6 per conflict
c wchs: 1946367343 pushed, 71489895 enlarged, 261 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all         775549        493045         34613      39159053       7911825        323989
c 
c  0 0         19521   3      1695   0         0   0  20721474  53   2790064  35     70222  22     3.2
c  1 5         12878   2      3455   1      1737   5   3245436   8    660204   8     29483   9     2.5
c  2 6         68741   9     33926   7      5887  17   4808503  12<  1326925  17<    69413  21    11.2
c  3 9        212587  27    153340  31      9089  26   3821034  10   1192524  15     57328  18<   17.5
c  4 14       205721  27    165835  34<     7449  22<  2564563   7    787392  10     31953  10    15.0
c  5 21        57767   7<    39969   8      3206   9   1529059   4    397429   5     17236   5     6.0
c  6 30        40674   5     24255   5      2298   7   1122516   3    287989   4     13002   4    10.4
c  7 41        50755   7     32153   7      1981   6    484259   1    174864   2     10725   3    28.0
c  8 54        31732   4     20065   4      1161   3    248759   1     95388   1      7447   2    11.5
c  9 69        19124   2     10322   2       662   2    281475   1     74715   1      5778   2     7.6
c 10 86        16863   2      5867   1       571   2    149785   0     52035   1      4731   1     6.1
c 11 126       20418   3      1706   0       450   1    124588   0     45824   1      3456   1     5.6
c 12 230       18301   2       457   0       120   0     55813   0     25826   0      3039   1    11.2
c 13 534         465   0         0   0         2   0      1787   0       645   0       176   0     0.5
c 14 1526          2   0         0   0         0   0         2   0         1   0         0   0     0.0
c 15 5046          0   0         0   0         0   0         0   0         0   0         0   0     0.0
c 
c avg                  4.6           4.3           4.1           1.5           2.2           2.9
c std                  2.6           1.8           2.2           2.2           2.4           2.7
c 
c   94.659  10% bump
c   52.941   6% unhide
c   52.413   5% probe
c   43.153   4% sweep
c   31.894   3% elim
c   20.933   2% cce
c   10.878   1% rescore
c    3.679   0% bca
c 
c   10.989 < 1% rest (below)
c 
c    2.625   0% block
c    2.128   0% decide
c    2.045   0% gauss
c    1.931   0% transred
c    0.907   0% ternres
c    0.885   0% quatres
c    0.468   0% card
c    0.000   0% locs
c    0.000   0% queuesort
c ==================================
c    5.346   1% preprocessing     2%
c  220.781  23% inprocessing     98%
c ==================================
c  226.127  24% simplifying
c  734.120  76% search
c ==================================
c  960.252 100% all
c 
c        775607 conflicts,         807.7 confs/sec
c          1492 ternaries,         519.8 confs/ternary
c          1585 binaries,          489.3 confs/binary
c           350 iterations,       2216.0 confs/iteration
c 
c            17 reductions,          0.0 redus/sec,  45623.9 confs/reduction
c          7249 restarts,            7.5 rests/sec,    107.0 confs/restart
c       3734400 decisions,        3889.0 decis/sec,      4.8 decis/conflict
c    2990220000 propagations,  3113996.1 props/sec,    800.7 props/decision
c 
c 960.3 seconds, 135.2 MB
c launch: done
