c launch: /data/cnf/sc2014/app/ACG-15-10p1.cnf.bz2
c host: atom20
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-10p1.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/ACG-15-10p1.cnf.bz2
c no embedded options
c found 'p cnf 268258 1155731' header
c read 268258 variables, 1155731 clauses, 2704052 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 258009 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  258009  1144812         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 4318 at-most-one constraints of average size 5.5
c [card-1] no at-most-two constraint found
c [card-1] using previous limit 2000000 for elimination
c [card-1] 4318 out of 4318 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 54067 variables
c [simpleprobe-1] all 214191 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 398 variables
c [simpleprobe-1] fully completed simple probing
c [simpleprobe-1] removed 398 variables, found 11562 hbrs, 20 units
c [unhide-1] limit 55007 based on 880119 irredundant clauses
c [unhide-1-1] 20 units, 1691 failed, 14412 tauts, 0 hbrs, 6764 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 206065 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 62549 not tried 30% in round 1
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 87046 = 42% variables out of 206065 scheduled
c [elim-1] considered successful since not run to completion yet
c [phase-count-1] 697187 negative 99.3% of 701983 except 4796 0.7%
c [phase-count-1] 568717 positive 81.0% of 701983 except 133266 19.0%
c [phase-count-1] less non-negative clauses 4796 than limit 70100 (10.0%)
c [phase-count-1] non-pos/non-neg = 133266/4796 = 27.79 >= 2.00 = 200/100
c [lucky-phase-1] forcing lucky phase -1
c [phase-1] phase bias: 0 positive 0%, 119019 negative 100%
c [sort-queue-1] sorted 119019 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 119019 (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 101094 variables 45.9% (119019 remain 46%)
c [simplification-1] removed 442829 irredundant clauses 38.7% (701983 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  119018   701983        34      30      2  5609    0     7   52   1%      0    7    1    0 24029%
c i    5.5  118603   701983        42      36      2  5610    0     8   52   1%      0    8    1    0 24072%
c i    5.7  118589   701983       196     166      6  5617    1    11   52   6%      0   11    8    0 17925%
c i    6.1  117836   701983       362     306     20  5622    1    23   52   4%      0   23    7    0 12253%
c i    6.3  117014   701983       462     390     24  5630    1    26   52   4%      0   26    9    0 11563%
c i    6.3  117013   701983       464     391     24  5630    1    26   52   4%      0   26    9    0 11493%
c i    6.3  117012   701983       465     391     24  5630    1    26   52   4%      0   26    9    0 11449%
c i    6.4  117011   701983       467     392     24  5630    1    26   52   4%      0   26    9    0 11379%
c i    6.9  117004   701983       788     613     53  5663    3    41   52   6%      1   41   18    0 10041%
c 
c [simplification-2] limit 1021 conflicts (hard 11000) hit after 1023 conflicts
c [decomp-3] removed 3644 variables
c [simpleprobe-2] all 115375 free variables schedulable
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [decomp-4] removed 321 variables
c [simpleprobe-2] 102779 variables remain 89% (12275 retained 11%)
c [simpleprobe-2] removed 321 variables, found 2957 hbrs, 49 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 55585 literals 24%
c [treelook-1] scheduling used 302754 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 535087 steps
c [treelook-1] 55583 literals remain 24%
c [treelook-1] 55538 variables remain to probed next time 48%
c [treelook-1] removed 0 variables, found 3831 hbrs
c [basicprobe-1] limit 5416064 based on 677008 irredundant clauses
c [basicprobe-1-0] 32977 probes remain 29% after last round
c [basicprobe-1-0] 19 units = 19 failed (100%) + 0 lifted (0%)
c [basicprobe-1-0] removed 2221 variables, found 13833 hbrs
c [unhide-2] limit 100000 with penalty 0 = 0 + 0
c [unhide-2-2] 11 units, 1654 failed, 3052 tauts, 0 hbrs, 19255 literals
c [elim-2] 58103 variables 53% will be scheduled this time
c [elim-2] scheduled 58103 variables 53%
c [elim-2] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-2] rescheduling of touched variables disabled
c [elim-2] incomplete 11991 not tried 11% in round 1
c [elim-2] transition to [ all 0 rem 1 ] state
c [elim-2] eliminated 1700 = 3% variables out of 58103 scheduled
c [elim-2] considered successful since not run to completion yet
c [phase-count-2] 617937 negative 99.2% of 622735 except 4798 0.8%
c [phase-count-2] 497512 positive 79.9% of 622735 except 125223 20.1%
c [phase-count-2] less non-negative clauses 4798 than limit 62200 (10.0%)
c [phase-count-2] non-pos/non-neg = 125223/4798 = 26.10 >= 2.00 = 200/100
c [lucky-phase-2] forcing lucky phase -1
c [phase-2] phase bias: 0 positive 0%, 1359 negative 100%
c [sort-queue-2] sorted 92416 enqueued variables after 1023 conflicts
c [score-dist-2] active 15460 (14%), one 0 (0%), zero 92416 (86%)
c [score-dist-2] max exp 508, different 11 (2%)
c [score-dist-2] median active exp 502, avg 502.2
c [simplification-2] removed 7675 variables 6.6% (107876 remain 42%)
c [simplification-2] removed 79248 irredundant clauses 11.3% (622735 remain 54%)
c [simplification-2] maximum reduction of 11% = max (7%, 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 13023 (soft 3023 + delta 10000)
c [simplification-2] new conflict limit 3023 (hard 13023)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   11.2  107875   622735      1036     734     71 19400    6    53   47  10%      1   53   44    0 11785%
c i   12.0  107790   622735      1429    1077    100 19408    9   104   48   8%      2  103   43    1 6974%
c i   12.5  107789   622735      1582    1217    102 19413   13   133   48  10%      2  131   76    1 8591%
c i   12.6  107773   622735      1583    1217    102 19413   13   133   48  10%      2  131   76    1 8558%
c i   13.0  107767   622735      1733    1348    105 19416   23   172   49  13%      2  170  187    2 11963%
c i   14.2  107734   622735      2256    1809    113 19436   38   258   49  15%      3  255  185    3 6761%
c i   14.8  107701   622735      2437    1949    114 19441   58   288   50  20%      3  284  342    4 8373%
c i   14.8  107689   622735      2438    1949    114 19441   58   288   50  20%      3  284  341    4 8341%
c i   14.8  107679   622735      2439    1949    114 19441   58   288   50  20%      3  284  339    4 8308%
c i   15.4  107669   622735      2634    2092    115 19441   84   316   51  27%      2  311  489    6 8278%
c 
c [simplification-3] limit of 19 iterations hit after 19 iterations
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 4571 at-most-one constraints of average size 4.5
c [card-2] no at-most-two constraint found
c [card-2] using previous limit 1000000 for elimination
c [card-2] 4571 out of 4571 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [decomp-6] removed 1156 variables
c [unhide-3] limit 280074 with penalty 0 = 0 + 0
c [unhide-3-3] 9 units, 707 failed, 10262 tauts, 0 hbrs, 57806 literals
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 104800 variables 100%
c [elim-3] limit of 28007485 steps penalty 0 = 0 + 0
c [elim-3] rescheduling of touched variables disabled
c [elim-3] incomplete 11033 not tried 11% in round 1
c [elim-3] transition to [ all 1 rem 1 ] state
c [elim-3] eliminated 3351 = 3% variables out of 104800 scheduled
c [elim-3] considered successful since not run to completion yet
c [phase-count-3] 585516 negative 99.2% of 590228 except 4712 0.8%
c [phase-count-3] 470004 positive 79.6% of 590228 except 120224 20.4%
c [phase-count-3] less non-negative clauses 4712 than limit 59000 (10.0%)
c [phase-count-3] non-pos/non-neg = 120224/4712 = 25.51 >= 2.00 = 200/100
c [lucky-phase-3] forcing lucky phase -1
c [phase-3] phase bias: 0 positive 0%, 283 negative 100%
c [sort-queue-3] sorted 72943 enqueued variables after 2634 conflicts
c [score-dist-3] active 28506 (28%), one 0 (0%), zero 72943 (72%)
c [score-dist-3] max exp 509, different 18 (4%)
c [score-dist-3] median active exp 501, avg 500.9
c [simplification-3] removed 6210 variables 5.8% (101449 remain 39%)
c [simplification-3] removed 32507 irredundant clauses 5.2% (590228 remain 52%)
c [simplification-3] maximum reduction of 6% = max (6%, 5%)
c [simplification-3] forced so keeping old conflict interval 0
c [simplification-3] conflict limit remains at 3053 (hard 13023)
c [simplification-3] new iteration interval 100
c 
c [simplification-4] limit 3053 conflicts (hard 13023) hit after 3055 conflicts
c [decomp-7] removed 37 variables
c [treelook-2] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-2] scheduled 37383 literals 18%
c [treelook-2] scheduling used 197099 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-2] used 431405 steps
c [treelook-2] 37381 literals remain 18%
c [treelook-2] 28113 variables remain to probed next time 28%
c [treelook-2] removed 0 variables, found 3366 hbrs
c [unhide-4] limit 323080 with penalty 0 = 0 + 0
c [unhide-4-4] 11 units, 667 failed, 2157 tauts, 0 hbrs, 31989 literals
c [elim-4] 10851 variables 11% will be scheduled this time
c [elim-4] scheduled 10851 variables 11%
c [elim-4] boosting limit by 20
c [elim-4] limit of 646161580 steps penalty 0 = 0 + 0
c [elim-4] rescheduling of touched variables disabled
c [elim-4-1] no variable eliminated in round 1 in 21029214 steps
c [elim-4] fully completed in 1 rounds
c [elim-4] transition to [ all 0 rem 0 ] state
c [elim-4] eliminated 0 = 0% variables out of 10851 scheduled
c [phase-count-4] 572491 negative 99.2% of 577203 except 4712 0.8%
c [phase-count-4] 457501 positive 79.3% of 577203 except 119702 20.7%
c [phase-count-4] less non-negative clauses 4712 than limit 57700 (10.0%)
c [phase-count-4] non-pos/non-neg = 119702/4712 = 25.40 >= 2.00 = 200/100
c [lucky-phase-4] forcing lucky phase -1
c [phase-4] phase bias: 0 positive 0%, 283 negative 100%
c [sort-queue-4] sorted 71130 enqueued variables after 3055 conflicts
c [score-dist-4] active 28814 (29%), one 0 (0%), zero 71130 (71%)
c [score-dist-4] max exp 510, different 20 (4%)
c [score-dist-4] median active exp 500, avg 500.4
c [simplification-4] removed 1505 variables 1.5% (99944 remain 39%)
c [simplification-4] removed 13025 irredundant clauses 2.2% (577203 remain 50%)
c [simplification-4] maximum reduction of 2% = max (1%, 2%)
c [simplification-4] geometric conflict interval increment 6666 = 20000 / 3
c [simplification-4] new conflict interval 6666
c [simplification-4] penalized conflict interval 6666 = 1 * 6666
c [simplification-4] hard conflict limit 19721 (soft 9721 + delta 10000)
c [simplification-4] new conflict limit 9721 (hard 19721)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   21.7   99943   577203      3106    2350    124 16159  118   368   49  32%      3  361  419    9 4831%
c i   21.7   99942   577203      3107    2350    124 16159  118   368   49  32%      3  361  417    9 4813%
c i   21.7   99941   577203      3108    2350    124 16159  118   368   49  32%      3  361  416    9 4794%
c i   21.7   99940   577203      3109    2350    124 16159  118   368   49  32%      3  361  414    9 4775%
c i   21.8   99827   577203      3141    2381    124 16159  119   370   49  32%      3  363  397    9 4508%
c i   21.9   99818   577203      3172    2399    124 16161  121   372   50  33%      3  365  405    9 4495%
c i   21.9   99817   577203      3174    2399    124 16162  121   372   50  33%      3  365  402    9 4460%
c i   21.9   99816   577203      3175    2399    124 16162  121   372   50  33%      3  365  400    9 4443%
c i   21.9   99815   577203      3176    2399    124 16162  121   372   50  33%      3  365  399    9 4425%
c i   21.9   99814   577203      3178    2399    124 16163  121   372   50  33%      3  365  396    9 4391%
c i   21.9   99813   577203      3179    2399    124 16163  121   372   50  33%      3  365  394    9 4374%
c i   21.9   99812   577203      3180    2399    124 16163  121   372   50  33%      3  364  393    9 4357%
c i   22.0   99811   577203      3181    2399    124 16163  121   372   50  33%      3  364  391    9 4340%
c i   22.0   99810   577203      3186    2400    124 16165  121   372   50  33%      3  365  389    9 4307%
c i   22.0   99809   577203      3187    2400    124 16165  121   372   50  33%      3  364  387    9 4291%
c i   23.5   99808   577203      3811    2859    140 16197  133   396   50  34%      4  384  188   11 1731%
c i   23.5   99759   577203      3826    2873    140 16197  132   396   50  33%      4  385  178   11 1641%
c i   23.5   99758   577203      3827    2873    140 16197  132   396   50  33%      4  385  177   11 1635%
c i   23.6   99757   577203      3828    2873    140 16197  132   396   50  33%      4  385  177   11 1629%
c i   23.6   99756   577203      3830    2873    140 16198  132   396   50  33%      4  385  175   11 1616%
c i   23.9   99755   577203      4000    3024    145 16203  130   404   50  32%      3  392  136   11 1234%
c i   24.4   99749   577203      4205    3197    150 16216  129   415   51  31%      3  402  129   11 1135%
c i   24.6   99740   577203      4277    3257    154 16217  130   422   51  31%      3  408  146   12 1261%
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   24.6   99730   577203      4284    3261    154 16217  131   423   51  31%      3  409  156   12 1347%
c i   25.0   99729   577203      4410    3369    158 16220  136   441   51  31%      3  427  213   12 1756%
c i   26.3   99723   577203      4893    3765    172 16231  143   463   52  31%      3  445  183   14 1353%
c i   26.4   99514   577203      4941    3803    174 16233  143   464   52  31%      3  446  178   14 1301%
c i   26.7   99502   577203      5047    3881    174 16233  145   466   52  31%      3  447  180   14 1294%
c i   26.7   99488   577203      5048    3881    174 16233  145   466   52  31%      3  447  179   14 1289%
c 
c [simplification-5] limit of 218 binary hit after 218 binaries
c [quatres-1] found 30211 quaternary clauses 32% in total
c [quatres-1-2] added 3 single-self-subsuming ternary resolvents
c [quatres-1-2] added 12 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 99475 free variables schedulable
c [ternres-1] 2009 ternary resolvents (3 bin, 2006 trn)
c [ternres-1] fully completed ternary resolution
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 571 xors of average arity 2.1
c [gauss-1] connected 1175 occurrences of 884 variables (average 1.3)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] fully completed
c [decomp-9] removed 613 variables
c [gauss-1] exported 0 unary, 2 binary and 0 ternary equations
c [basicprobe-2] limit 17136818 penalty 0 = 0 + 0
c [basicprobe-2-0] 30267 probes remain 31% after last round
c [basicprobe-2-0] 57 units = 57 failed (100%) + 0 lifted (0%)
c [basicprobe-2-0] removed 2287 variables, found 29840 hbrs
c [bate-1] eliminated 24 asymmetric tautologies during probing
c [unhide-5] limit 685472 with penalty 0 = 0 + 0
c [unhide-5-5] 8 units, 345 failed, 10652 tauts, 0 hbrs, 57874 literals
c [transred-1] limit 2000000 with penalty 0 = 0 + 0
c [transred-1] removed 139 transitive binary clauses
c [transred-1] found 7 units
c [block-1] scheduling all variables this time
c [block-1] scheduled 95683 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 9897 blocked clauses
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 24 clauses out of 408 (6%) of length 10
c [cce-1-1] eliminated 101 clauses out of 2098 (5%) of length 9
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 125 large clauses in 30000006 steps
c [cce-1-1] allowing another 15000003 steps for small clauses
c [cce-1-1] scheduling 390033 clauses = 288345 binary + 101688 ternary
c [cce-1-1] tried to eliminate 339 small clauses 0%
c [cce-1-1] eliminated 71 binary clauses 0%
c [cce-1-1] eliminated 50 ternary clauses 0%
c [cce-1-1] eliminated 121 small clauses 0%
c [cce-1-1] eliminated 121 small clauses in 30000001 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 246 covered clauses in round 1
c [cce-1] eliminated 246 covered clauses in TOTAL during 1 rounds
c [cce-1] 246 < 1/100 * 535659 = 5356 considered unsuccessful
c [bca-1] limit of 10000000 steps and 1071326 added (scaled 2)
c [bca-1] 174729 out of 191368 literals actually usable 91%
c [bca-1] added 199 blocked clauses in 504126 steps
c [sweep-1] limit 1070826 based on 535413 irredundant clauses
c [sweep-1-1] 3702 pos 3.9% + 91981 neg 96.1% = 95683 sched 100.0% ret 0
c [sweep-1-1] 1239855 steps 10 queries 26430.00 avg class size
c [sweep-1-1] 107 decisions 9 SAT calls 103.67 avg env size
c [sweep-1-1] 95666 variables remain 100% (17 retained 0%)
c [decomp-11] removed 507 variables
c [sweep-1-1] removed 507 vars (0 failed, 0 eqs, 4 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 507 vars in TOTAL (1 rounds, 9 queries)
c [phase-count-5] 529713 negative 99.1% of 534399 except 4686 0.9%
c [phase-count-5] 432045 positive 80.8% of 534399 except 102354 19.2%
c [phase-count-5] less non-negative clauses 4686 than limit 53400 (10.0%)
c [phase-count-5] non-pos/non-neg = 102354/4686 = 21.84 >= 2.00 = 200/100
c [lucky-phase-5] forcing lucky phase -1
c [phase-5] phase bias: 0 positive 0%, 248 negative 100%
c [sort-queue-5] sorted 61398 enqueued variables after 5974 conflicts
c [score-dist-5] active 33778 (35%), one 0 (0%), zero 61398 (65%)
c [score-dist-5] max exp 509, different 31 (6%)
c [score-dist-5] median active exp 498, avg 496.3
c [simplification-5] removed 4299 variables 4.3% (95176 remain 37%)
c [simplification-5] removed 42804 irredundant clauses 7.4% (534399 remain 47%)
c [simplification-5] maximum reduction of 7% = max (4%, 7%)
c [simplification-5] forced so keeping old conflict interval 6666
c [simplification-5] conflict limit remains at 9859 (hard 19721)
c [simplification-5] 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   34.1   95175   534399      5975    4387   1673 54795  187   501   49  37%      6  475  304   19 1632%
c i   34.1   95174   534399      5985    4395   1673 54796  186   501   51  37%      6  476  296   19 1586%
c i   34.2   95173   534399      6006    4411   1673 54796  187   502   52  37%      6  476  292   19 1556%
c i   34.2   95172   534399      6010    4412   1673 54796  187   502   52  37%      6  476  295   19 1570%
c i   34.2   95171   534399      6013    4413   1673 54796  187   502   52  37%      6  476  296   19 1578%
c i   34.2   95170   534399      6014    4413   1673 54796  187   502   52  37%      6  476  295   19 1572%
c i   34.3   95169   534399      6015    4413   1673 54796  187   501   52  37%      6  476  294   19 1566%
c i   34.3   95168   534399      6016    4413   1673 54796  187   501   52  37%      6  476  293   19 1559%
c i   34.3   95167   534399      6017    4413   1673 54796  187   501   52  37%      6  476  292   19 1553%
c i   34.3   95166   534399      6018    4413   1673 54796  187   501   52  37%      6  475  291   19 1547%
c i   34.8   95165   534399      6196    4509   1675 54803  193   506   54  38%      5  479  301   20 1535%
c i   35.0   95164   534399      6267    4560   1674 54804  196   507   54  39%      5  479  317   20 1587%
c i   35.7   95155   534399      6506    4716   1675 54807  200   507   54  40%      4  478  306   21 1463%
c i   35.7   95154   534399      6507    4716   1675 54807  200   507   54  40%      4  477  305   21 1457%
c i   37.0   95153   534399      7036    5001   1681 54812  213   508   54  42%      4  476  285   23 1231%
c i   39.5   95140   534399      8055    5658   1690 54852  222   510   56  43%      7  470  231   27  868%
c i   39.6   95134   534399      8069    5669   1690 54852  222   510   56  44%      7  470  234   27  880%
c i   39.7   95133   534399      8098    5685   1690 54852  223   510   56  44%      7  470  255   27  950%
c i   40.0   95132   534399      8187    5744   1690 54852  224   510   56  44%      6  469  260   27  959%
c i   40.4   95131   534399      8331    5834   1690 54855  225   507   56  44%      6  465  250   28  904%
c i   41.2   95127   534399      8515    5975   1692 54860  226   501   56  45%      5  457  245   28  868%
c i   41.3   95126   534399      8567    6010   1697 54860  225   499   56  45%      5  455  236   28  832%
c i   41.3   95123   534399      8568    6010   1697 54860  225   499   56  45%      5  455  235   28  829%
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   41.4   95120   534399      8569    6010   1697 54860  225   499   56  45%      5  455  234   28  826%
c i   41.4   95110   534399      8570    6010   1697 54860  225   498   56  45%      5  455  233   28  823%
c i   41.4   95109   534399      8572    6011   1697 54860  225   498   56  45%      5  455  232   28  818%
c i   41.4   95106   534399      8573    6011   1697 54860  225   498   56  45%      5  455  231   28  815%
c i   41.4   95102   534399      8574    6011   1697 54860  225   498   56  45%      5  455  230   28  811%
c i   41.4   95099   534399      8576    6011   1697 54860  225   498   56  45%      4  454  228   28  806%
c i   41.4   95089   534399      8577    6011   1697 54860  225   498   56  45%      4  454  227   28  803%
c i   41.5   95075   534399      8578    6011   1697 54860  225   498   56  45%      4  454  226   28  800%
c i   41.5   95072   534399      8579    6011   1697 54860  225   498   56  45%      4  454  226   28  797%
c i   41.5   95068   534399      8580    6011   1697 54860  225   497   56  45%      4  454  225   28  794%
c i   41.5   95054   534399      8581    6011   1697 54860  225   497   56  45%      4  454  224   28  791%
c i   41.5   95041   534399      8582    6011   1697 54860  225   497   56  45%      4  454  223   28  788%
c i   41.5   95040   534399      8583    6011   1697 54860  225   497   56  45%      4  453  222   28  785%
c i   41.5   95036   534399      8584    6011   1697 54860  225   497   56  45%      4  453  221   28  781%
c i   41.5   95030   534399      8587    6013   1697 54860  224   497   56  45%      4  453  219   28  773%
c i   41.6   95028   534399      8589    6014   1697 54860  224   497   56  45%      4  453  217   28  768%
c i   43.5   95017   534399      9408    6614   1708 54886  226   498   56  45%      6  449  265   31  860%
c i   43.6   95015   534399      9409    6614   1708 54886  226   498   56  45%      6  449  264   31  857%
c i   43.6   95013   534399      9410    6614   1708 54886  226   498   56  45%      6  449  263   31  854%
c i   43.6   95002   534399      9411    6614   1708 54886  226   498   56  45%      6  449  262   31  850%
c i   43.6   94999   534399      9412    6614   1708 54886  226   498   56  45%      6  449  261   31  847%
c i   43.6   94996   534399      9413    6614   1708 54886  226   498   56  45%      6  449  260   31  844%
c i   43.6   94985   534399      9417    6614   1708 54888  226   498   56  45%      6  448  259   31  840%
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   43.6   94983   534399      9418    6614   1708 54888  226   498   56  45%      6  448  258   31  837%
c i   43.7   94972   534399      9419    6614   1708 54888  226   497   56  45%      6  448  257   31  834%
c i   43.7   94970   534399      9420    6614   1708 54888  226   497   56  45%      6  448  256   31  831%
c i   43.7   94959   534399      9421    6614   1708 54888  226   497   56  45%      6  448  255   31  827%
c i   43.7   94957   534399      9422    6614   1708 54888  226   497   56  45%      6  448  254   31  824%
c i   43.7   94944   534399      9423    6614   1708 54888  226   497   56  45%      6  448  253   31  821%
c i   43.7   94932   534399      9424    6614   1708 54888  225   497   56  45%      6  448  252   31  818%
c i   43.7   94929   534399      9425    6614   1708 54888  225   497   56  45%      6  447  251   31  815%
c 
c [simplification-6] limit 10205 conflicts (hard 19721) hit after 10205 conflicts
c [quatres-2] found 34376 quaternary clauses 38% in total
c [quatres-2-2] added 8 single-self-subsuming ternary resolvents
c [ternres-2] limit 6186230 with penalty 0 = 0 + 0
c [ternres-2] all 94920 free variables schedulable
c [ternres-2] 62 ternary resolvents (0 bin, 62 trn)
c [ternres-2] 7019 variables remain 7% (87901 retained 93%)
c [card-3] limit 773278 penalty 2 = 2 + 0
c [card-3] found 3690 at-most-one constraints of average size 4.3
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 773278 for elimination
c [card-3] 3690 out of 3690 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 93 xors of average arity 2.4
c [gauss-2] connected 226 occurrences of 183 variables (average 1.2)
c [gauss-2] limit 2000000 penalty 0 = 0 + 0
c [gauss-2] fully completed
c [decomp-12] removed 41 variables
c [gauss-2] exported 0 unary, 1 binary and 0 ternary equations
c [simpleprobe-3] 84579 schedulable variables 89%
c [simpleprobe-3] limit 24744921 penalty 0 = 0 + 0
c [decomp-14] removed 4386 variables
c [simpleprobe-3] 2626 variables remain 3% (87867 retained 97%)
c [simpleprobe-3] removed 4386 variables, found 57346 hbrs, 588 units
c [unhide-6] limit 1237246 with penalty 0 = 0 + 0
c [unhide-6-6] 1 units, 360 failed, 9336 tauts, 0 hbrs, 92347 literals
c [transred-2] limit 2000000 with penalty 0 = 0 + 0
c [transred-2] removed 158 transitive binary clauses
c [transred-2] found 7 units
c [block-2] scheduling all variables this time
c [block-2] scheduled 89013 variables 100%
c [block-2] limit of 61862304 steps penalty 0 = 0 + 0
c [block-2] fully completed
c [block-2] transition to [ all 0 rem 0 ] state
c [block-2] eliminated 798 blocked clauses
c [block-2] 798 < 1/100 * 505278 = 5052 considered unsuccessful
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 89013 variables 100%
c [elim-5] limit of 61862304 steps penalty 1 = 1 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5-1] eliminated 2905 variables 3% in round 1 in 41635766 steps
c [elim-5-1] backward subsumption/strengthening limit 20226538
c [elim-5-1-1] backward checking 11475 touched variables 13%
c [elim-5-1-1] fully completed backward checking in 1 rounds
c [elim-5-1] subsumed 94 and strengthened 113 clauses in 2711645 steps
c [elim-5-1] rescheduled 553 variables 1% by backward subsumption
c [elim-5-2] eliminated 58 variables 0% in round 2 in 1307208 steps
c [elim-5-2] backward subsumption/strengthening limit 1307200
c [elim-5-2-1] backward checking 383 touched variables 0%
c [elim-5-2-1] fully completed backward checking in 1 rounds
c [elim-5-2] subsumed 11 and strengthened 21 clauses in 286077 steps
c [elim-5-2] rescheduled 82 variables 0% by backward subsumption
c [elim-5-3] no variable eliminated in round 3 in 51231 steps
c [elim-5] fully completed in 3 rounds
c [elim-5] transition to [ all 0 rem 0 ] state
c [elim-5] eliminated 2963 = 3% variables out of 89013 scheduled
c [bca-2] limit of 10000000 steps and 975901 added (scaled 2)
c [bca-2] 156463 out of 172102 literals actually usable 91%
c [bca-2] added 117 blocked clauses in 469768 steps
c [sweep-2] limit 1855869 penalty 0 = 0 + 0
c [sweep-2-1] 3279 pos 3.8% + 82758 neg 96.2% = 86037 sched 100.0% ret 13
c [sweep-2-1] 2150988 steps 15 queries 19385.60 avg class size
c [sweep-2-1] 107 decisions 11 SAT calls 34.82 avg env size
c [sweep-2-1] 85888 variables remain 100% (46 retained 0%)
c [decomp-15] removed 124 variables
c [sweep-2-1] removed 124 vars (0 failed, 3 eqs, 5 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 124 vars in TOTAL (1 rounds, 14 queries)
c [phase-count-6] 482428 negative 99.0% of 487077 except 4649 1.0%
c [phase-count-6] 386716 positive 79.4% of 487077 except 100361 20.6%
c [phase-count-6] less non-negative clauses 4649 than limit 48700 (10.0%)
c [phase-count-6] non-pos/non-neg = 100361/4649 = 21.59 >= 2.00 = 200/100
c [lucky-phase-6] forcing lucky phase -1
c [phase-6] phase bias: 0 positive 0%, 222 negative 100%
c [sort-queue-6] sorted 50670 enqueued variables after 10205 conflicts
c [score-dist-6] active 35256 (41%), one 0 (0%), zero 50670 (59%)
c [score-dist-6] max exp 510, different 47 (9%)
c [score-dist-6] median active exp 497, avg 493.2
c [simplification-6] removed 8994 variables 9.5% (85926 remain 33%)
c [simplification-6] removed 47322 irredundant clauses 8.9% (487077 remain 43%)
c [simplification-6] maximum reduction of 9% = max (9%, 9%)
c [simplification-6] large reduction 9% >= 5% limit
c [simplification-6] next conflict interval 2000 = 2000/1
c [simplification-6] penalized conflict interval 2000 = 1 * 2000
c [simplification-6] hard conflict limit 22205 (soft 12205 + delta 10000)
c [simplification-6] new conflict limit 12205 (hard 22205)
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   52.7   85925   487077     10422    4585   1001 95547  280   542   49  52%      7  486  431   37 1150%
c i   52.9   85921   487077     10499    4635   1001 95547  285   548   49  52%      7  491  475   38 1246%
c i   52.9   85917   487077     10500    4635   1001 95547  285   548   49  52%      7  491  473   38 1241%
c i   52.9   85916   487077     10501    4635   1001 95547  285   548   49  52%      7  491  471   38 1236%
c i   52.9   85911   487077     10504    4636   1001 95548  285   547   49  52%      7  491  468   38 1228%
c i   52.9   85904   487077     10509    4637   1001 95551  285   547   49  52%      7  491  461   38 1210%
c i   53.0   85903   487077     10521    4643   1001 95552  286   548   49  52%      7  491  469   38 1227%
c i   53.0   85897   487077     10522    4643   1001 95552  286   548   49  52%      7  491  467   38 1222%
c i   53.0   85889   487077     10546    4659   1001 95552  288   549   49  52%      7  492  475   38 1236%
c i   53.3   85875   487077     10696    4771   1001 95552  297   561   50  53%      6  502  506   40 1278%
c i   53.8   85873   487077     10881    4911   1001 95556  305   573   50  53%      5  513  482   41 1183%
c i   53.9   85872   487077     10899    4926   1001 95556  305   574   50  53%      5  514  475   41 1162%
c i   53.9   85871   487077     10900    4926   1001 95556  305   574   50  53%      5  514  473   41 1157%
c i   54.3   85870   487077     11073    5050   1004 95557  312   583   50  53%      4  522  470   42 1120%
c i   54.9   85788   487077     11334    5228   1006 95559  324   598   51  54%      4  535  493   44 1125%
c i   54.9   85787   487077     11343    5236   1006 95559  325   599   51  54%      4  536  493   44 1122%
c i   55.1   85786   487077     11413    5275   1016 95565  326   605   51  54%      3  542  474   44 1069%
c i   55.1   85785   487077     11414    5275   1016 95565  326   605   51  54%      3  541  472   44 1065%
c i   55.1   85784   487077     11415    5275   1016 95565  326   605   51  54%      3  541  470   44 1061%
c i   55.1   85783   487077     11416    5275   1016 95565  326   605   51  54%      3  541  468   44 1057%
c i   55.1   85782   487077     11417    5275   1016 95565  326   605   51  54%      3  541  466   44 1053%
c i   55.1   85781   487077     11418    5275   1016 95565  326   605   51  54%      3  541  464   44 1049%
c i   55.1   85780   487077     11419    5275   1016 95565  325   605   51  54%      3  541  463   44 1044%
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   55.1   85779   487077     11420    5275   1016 95565  325   604   51  54%      3  541  461   44 1040%
c i   55.2   85778   487077     11421    5275   1016 95565  325   604   51  54%      3  540  459   44 1036%
c i   55.2   85777   487077     11422    5275   1016 95565  325   604   51  54%      3  540  457   44 1032%
c i   55.2   85776   487077     11423    5275   1016 95565  325   604   51  54%      3  540  455   44 1028%
c i   55.3   85772   487077     11500    5319   1019 95587  325   609   54  53%      3  544  419   45  940%
c i   55.3   85771   487077     11502    5320   1019 95587  325   609   54  53%      3  544  419   45  939%
c i   55.7   85770   487077     11649    5446   1022 95590  328   618   54  53%      3  553  420   45  925%
c i   55.7   85769   487077     11663    5454   1022 95592  328   619   54  53%      3  553  411   45  903%
c i   55.7   85768   487077     11664    5454   1022 95592  328   619   54  53%      3  553  409   45  900%
c i   55.7   85767   487077     11665    5454   1022 95592  328   619   54  53%      3  553  408   45  896%
c i   55.7   85766   487077     11666    5454   1022 95592  328   618   54  53%      3  552  406   45  893%
c i   55.7   85765   487077     11667    5454   1022 95592  328   618   54  53%      3  552  404   45  889%
c i   55.7   85764   487077     11668    5454   1022 95592  327   618   54  53%      3  552  403   45  886%
c i   55.7   85763   487077     11669    5454   1022 95592  327   618   54  53%      3  552  401   45  882%
c i   55.8   85762   487077     11670    5454   1022 95592  327   618   54  53%      3  552  400   45  879%
c i   55.8   85761   487077     11671    5454   1022 95592  327   618   54  53%      3  552  398   45  876%
c i   55.8   85760   487077     11672    5454   1022 95592  327   617   54  53%      3  552  397   45  872%
c i   55.8   85759   487077     11673    5454   1022 95592  327   617   54  53%      3  551  395   45  869%
c i   55.8   85758   487077     11674    5454   1022 95592  327   617   54  53%      3  551  393   45  865%
c i   55.8   85757   487077     11675    5454   1022 95592  327   617   54  53%      3  551  392   45  862%
c i   56.2   85756   487077     11824    5550   1025 95592  333   623   54  53%      2  556  435   46  937%
c i   56.7   85747   487077     12045    5717   1030 95592  336   627   54  54%      2  558  405   48  851%
c i   56.7   85745   487077     12059    5730   1030 95592  336   627   54  54%      2  558  405   48  851%
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.8   85740   487077     12062    5732   1030 95592  336   627   54  54%      2  557  405   48  850%
c i   56.8   85738   487077     12063    5732   1030 95592  336   626   54  54%      2  557  404   48  846%
c i   56.8   85735   487077     12064    5732   1030 95592  336   626   54  54%      2  557  402   48  843%
c i   56.8   85731   487077     12065    5732   1030 95592  336   626   54  54%      2  557  400   48  840%
c i   56.8   85728   487077     12066    5732   1030 95592  336   626   54  54%      2  557  399   48  837%
c i   56.8   85721   487077     12067    5732   1030 95592  336   626   54  54%      2  557  397   48  833%
c i   56.8   85719   487077     12068    5732   1030 95592  335   626   54  54%      2  556  396   48  830%
c i   56.8   85709   487077     12069    5732   1030 95592  335   625   54  54%      2  556  394   48  827%
c i   56.8   85700   487077     12070    5732   1030 95592  335   625   54  54%      2  556  393   48  824%
c i   57.4   85687   487077     12354    5935   1045 95609  324   619   54  52%      2  548  222   48  460%
c 
c [simplification-7] limit 12559 conflicts (hard 22205) hit after 12559 conflicts
c [quatres-3] found 31442 quaternary clauses 37% in total
c [quatres-3-2] added 5 quaternary resolvents
c [ternres-3] limit 7517034 with penalty 0 = 0 + 0
c [ternres-3] 6306 schedulable variables 7%
c [ternres-3] 242 ternary resolvents (3 bin, 239 trn)
c [ternres-3] fully completed ternary resolution
c [gauss-3] limit 2000000 penalty 0 = 0 + 0
c [gauss-3] extracted 58 xors of average arity 2.7
c [gauss-3] connected 154 occurrences of 118 variables (average 1.3)
c [gauss-3] limit 2000000 penalty 0 = 0 + 0
c [gauss-3] fully completed
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-16] removed 28 variables
c [unhide-7] limit 1503406 with penalty 0 = 0 + 0
c [unhide-7-7] 3 units, 113 failed, 5378 tauts, 0 hbrs, 76855 literals
c [transred-3] limit 2000000 with penalty 0 = 0 + 0
c [transred-3] removed 135 transitive binary clauses
c [transred-3] found 2 units
c [cce-2] limit of 18792585 steps penalty 1 = 1 + 0
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] allowing another 9396293 steps for small clauses
c [cce-2-1] scheduling 345444 clauses = 258393 binary + 87051 ternary
c [cce-2-1] tried to eliminate 268 small clauses 0%
c [cce-2-1] eliminated 54 binary clauses 0%
c [cce-2-1] eliminated 37 ternary clauses 0%
c [cce-2-1] eliminated 91 small clauses 0%
c [cce-2-1] eliminated 1568 small clauses in 18792585 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 1568 covered clauses in round 1
c [cce-2] eliminated 1568 covered clauses in TOTAL during 1 rounds
c [cce-2] 1568 < 1/100 * 480262 = 4802 considered unsuccessful
c [elim-6] scheduling all variables this time
c [elim-6] scheduled 85408 variables 100%
c [elim-6] limit of 150340680 steps penalty 0 = 0 + 0
c [elim-6] rescheduling of touched variables disabled
c [elim-6-1] eliminated 1272 variables 1% in round 1 in 40063849 steps
c [elim-6-1] backward subsumption/strengthening limit 40063800
c [elim-6-1-1] backward checking 5047 touched variables 6%
c [elim-6-1-1] fully completed backward checking in 1 rounds
c [elim-6-1] subsumed 15 and strengthened 2 clauses in 1536916 steps
c [elim-6-1] rescheduled 44 variables 0% by backward subsumption
c [elim-6-2] eliminated 3 variables 0% in round 2 in 32445 steps
c [elim-6-2] backward subsumption/strengthening limit 32400
c [elim-6-2-1] backward checking 24 touched variables 0%
c [elim-6-2-1] incomplete backward checking 0 remain 0%
c [elim-6-2] subsumed 3 and strengthened 2 clauses in 32401 steps
c [elim-6-2] rescheduled 14 variables 0% by backward subsumption
c [elim-6-3] no variable eliminated in round 3 in 10161 steps
c [elim-6] fully completed in 3 rounds
c [elim-6] transition to [ all 0 rem 0 ] state
c [elim-6] eliminated 1275 = 1% variables out of 85408 scheduled
c [bca-3] limit of 10000000 steps and 952830 added (scaled 2)
c [bca-3] 150757 out of 168268 literals actually usable 90%
c [bca-3] added 47 blocked clauses in 445568 steps
c [sweep-3] limit 2255110 penalty 0 = 0 + 0
c [sweep-3-1] 3061 pos 3.6% + 81030 neg 96.4% = 84091 sched 100.0% ret 42
c [sweep-3-1] 2592692 steps 17 queries 17676.35 avg class size
c [sweep-3-1] 199 decisions 15 SAT calls 69.80 avg env size
c [sweep-3-1] 83828 variables remain 100% (86 retained 0%)
c [decomp-17] removed 249 variables
c [sweep-3-1] removed 249 vars (0 failed, 2 eqs, 5 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 249 vars in TOTAL (1 rounds, 16 queries)
c [phase-count-7] 469950 negative 99.0% of 474526 except 4576 1.0%
c [phase-count-7] 377119 positive 79.5% of 474526 except 97407 20.5%
c [phase-count-7] less non-negative clauses 4576 than limit 47400 (10.0%)
c [phase-count-7] non-pos/non-neg = 97407/4576 = 21.29 >= 2.00 = 200/100
c [lucky-phase-7] forcing lucky phase -1
c [phase-7] phase bias: 0 positive 0%, 133 negative 100%
c [sort-queue-7] sorted 46011 enqueued variables after 12559 conflicts
c [score-dist-7] active 37873 (45%), one 0 (0%), zero 46011 (55%)
c [score-dist-7] max exp 508, different 54 (11%)
c [score-dist-7] median active exp 500, avg 492.8
c [simplification-7] removed 1728 variables 2.0% (83884 remain 33%)
c [simplification-7] removed 12551 irredundant clauses 2.6% (474526 remain 41%)
c [simplification-7] maximum reduction of 3% = max (2%, 3%)
c [simplification-7] geometric conflict interval increment 5000 = 20000 / 4
c [simplification-7] new conflict interval 11666
c [simplification-7] penalized conflict interval 11666 = 1 * 11666
c [simplification-7] hard conflict limit 34225 (soft 24225 + delta 10000)
c [simplification-7] new conflict limit 24225 (hard 34225)
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.8   83883   474526     12875    6095   1127 94047  315   613   53  51%      3  537  265   50  534%
c i   64.3   83876   474526     13147    6294   1129 94054  309   608   53  51%      2  530  254   50  503%
c i   64.4   83875   474526     13148    6294   1129 94054  309   608   53  51%      2  530  253   50  501%
c i   64.5   83874   474526     13202    6324   1129 94054  309   606   53  51%      2  527  261   51  516%
c i   64.9   83873   474526     13394    6444   1135 94070  307   601   53  51%      2  521  266   51  520%
c i   64.9   83872   474526     13395    6444   1135 94070  307   601   53  51%      2  521  265   51  518%
c i   64.9   83871   474526     13396    6444   1135 94070  307   600   53  51%      2  520  264   51  516%
c i   65.4   83870   474526     13638    6594   1141 94070  302   588   53  51%      2  506  241   52  464%
c i   65.8   83859   474526     13817    6689   1141 94072  298   578   53  52%      2  494  227   52  433%
c i   65.8   83858   474526     13818    6689   1141 94072  298   578   53  52%      2  494  226   52  431%
c i   66.0   83857   474526     13879    6737   1142 94072  295   573   53  52%      2  489  203   52  387%
c i   66.0   83856   474526     13881    6738   1142 94072  295   573   53  52%      2  489  201   52  384%
c i   66.0   83855   474526     13883    6739   1142 94072  295   573   53  52%      2  489  200   52  382%
c i   66.0   83854   474526     13885    6739   1142 94072  295   572   53  52%      2  489  199   52  381%
c i   66.0   83853   474526     13895    6747   1142 94072  295   572   53  52%      2  488  197   52  376%
c i   66.0   83850   474526     13897    6748   1142 94072  295   571   53  52%      2  487  196   52  375%
c i   66.0   83849   474526     13899    6749   1142 94072  295   571   53  52%      2  487  196   52  374%
c i   66.3   83848   474526     14046    6848   1142 94073  289   559   53  52%      1  474  167   53  317%
c i   66.3   83847   474526     14047    6848   1142 94073  289   559   53  52%      1  474  166   53  316%
c i   68.2   83846   474526     14909    7392   1154 94079  261   500   54  52%      5  410  178   54  331%
c i   68.2   83845   474526     14918    7399   1154 94079  261   500   54  52%      4  409  179   54  333%
c i   68.2   83844   474526     14928    7408   1154 94079  260   499   54  52%      4  408  176   54  329%
c i   68.2   83843   474526     14933    7412   1154 94079  260   499   54  52%      4  408  176   54  328%
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   68.2   83842   474526     14934    7412   1154 94079  260   499   54  52%      4  408  175   54  326%
c i   68.2   83841   474526     14935    7412   1154 94079  260   499   54  52%      4  408  175   54  325%
c i   68.3   83840   474526     14936    7412   1154 94079  260   499   54  52%      4  408  174   54  324%
c i   68.3   83839   474526     14937    7412   1154 94079  260   498   54  52%      4  408  173   54  323%
c i   68.3   83838   474526     14938    7412   1154 94079  260   498   54  52%      4  407  172   54  321%
c i   68.3   83837   474526     14939    7412   1154 94079  260   498   54  52%      4  407  172   54  320%
c i   68.3   83836   474526     14940    7412   1154 94079  260   498   54  52%      4  407  171   54  319%
c i   68.3   83835   474526     14941    7412   1154 94079  260   498   54  52%      4  407  170   54  318%
c i   68.3   83834   474526     14942    7412   1154 94079  260   498   54  52%      4  407  170   54  316%
c i   68.3   83833   474526     14943    7412   1154 94079  260   498   54  52%      4  407  169   54  315%
c i   68.3   83830   474526     14956    7424   1154 94079  259   497   54  52%      4  406  167   54  311%
c i   68.3   83829   474526     14958    7425   1154 94079  259   497   54  52%      4  406  166   54  309%
c i   68.3   83828   474526     14959    7425   1154 94079  259   497   54  52%      4  406  165   54  308%
c i   71.5   83827   474526     16394    8313   1176 94108  225   430   58  52%     11  331  160   56  288%
c i   71.8   83826   474526     16553    8450   1178 94109  222   426   58  52%      9  326  149   56  267%
c i   72.3   83823   474526     16759    8579   1178 94109  217   415   58  52%      8  314  134   56  240%
c i   72.4   83821   474526     16794    8596   1178 94109  216   413   58  52%      7  312  134   56  238%
c i   79.4   83820   474526     19996   10698   1228 94124  181   340   62  53%     33  227  182   60  303%
c i   79.4   83819   474526     20006   10707   1228 94124  180   340   62  53%     33  227  178   60  296%
c i   79.5   83818   474526     20007   10707   1228 94124  180   340   62  53%     33  227  178   60  295%
c i   79.5   83817   474526     20016   10713   1228 94124  180   340   62  53%     33  227  177   60  294%
c i   79.5   83816   474526     20018   10714   1228 94124  180   340   62  53%     33  227  176   60  292%
c i   82.0   83815   474526     21106   11392   1230 94128  172   314   64  55%     16  197  120   62  194%
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   83.8   83712   474526     21854   11838   1234 94138  163   293   64  56%     10  174   91   62  146%
c i   83.9   83711   474526     21920   11875   1234 94138  162   291   64  56%      9  172   86   62  138%
c i   85.9   83710   474526     22718   12377   1237 94138  150   267   65  56%      7  146   95   63  151%
c i   85.9   83709   474526     22719   12377   1237 94138  150   267   65  56%      7  146   94   63  150%
c i   86.0   83708   474526     22757   12403   1237 94138  149   266   65  56%      7  145   94   63  150%
c i   86.4   83707   474526     22931   12486   1239 94141  150   264   65  57%      5  142  128   63  203%
c i   86.4   83706   474526     22935   12489   1239 94141  150   264   65  57%      5  142  127   63  202%
c i   87.7   83705   474526     23516   12823   1240 94145  146   253   65  58%      4  130  126   64  198%
c i   87.7   83704   474526     23517   12823   1240 94145  146   252   65  58%      4  130  125   64  197%
c i   87.7   83703   474526     23520   12825   1240 94145  146   252   65  58%      4  130  124   64  195%
c 
c [simplification-8] limit 24462 conflicts (hard 34225) hit after 24462 conflicts
c [quatres-4] found 32014 quaternary clauses 37% in total
c [quatres-4-2] added 3 single-self-subsuming ternary resolvents
c [quatres-4-2] added 5 quaternary resolvents
c [ternres-4] limit 13703765 with penalty 0 = 0 + 0
c [ternres-4] all 83703 free variables schedulable
c [ternres-4] 1197 ternary resolvents (4 bin, 1193 trn)
c [ternres-4] fully completed ternary resolution
c [decomp-18] removed 187 variables
c [unhide-8] limit 1370376 with penalty 1 = 0 + 1
c [unhide-8-8] 2 units, 211 failed, 3495 tauts, 0 hbrs, 232852 literals
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 141 transitive binary clauses
c [transred-4] found 2 units
c [block-3] scheduling all variables this time
c [block-3] scheduled 83302 variables 100%
c [block-3] limit of 68518826 steps penalty 1 = 1 + 0
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 19 blocked clauses
c [block-3] 19 < 1/100 * 473459 = 4734 considered unsuccessful
c [elim-7] scheduling all variables this time
c [elim-7] scheduled 83302 variables 100%
c [elim-7] limit of 274075304 steps penalty 0 = 0 + 0
c [elim-7] rescheduling of touched variables disabled
c [elim-7-1] eliminated 689 variables 1% in round 1 in 39328704 steps
c [elim-7-1] backward subsumption/strengthening limit 39328700
c [elim-7-1-1] backward checking 2902 touched variables 3%
c [elim-7-1-1] fully completed backward checking in 1 rounds
c [elim-7-1] subsumed 18 and strengthened 0 clauses in 832245 steps
c [elim-7-1] rescheduled 52 variables 0% by backward subsumption
c [elim-7-2] eliminated 1 variables 0% in round 2 in 30217 steps
c [elim-7-2] backward subsumption/strengthening limit 30200
c [elim-7-2-1] backward checking 8 touched variables 0%
c [elim-7-2-1] incomplete backward checking 0 remain 0%
c [elim-7-2] subsumed 1 and strengthened 1 clauses in 30201 steps
c [elim-7-2] rescheduled 5 variables 0% by backward subsumption
c [elim-7-3] no variable eliminated in round 3 in 3846 steps
c [elim-7] fully completed in 3 rounds
c [elim-7] transition to [ all 0 rem 0 ] state
c [elim-7] eliminated 690 = 1% variables out of 83302 scheduled
c [elim-7] 690 < 1/100 * 83302 = 833 considered unsuccessful
c [bca-4] limit of 10000000 steps and 937565 added (scaled 2)
c [bca-4] 143143 out of 165226 literals actually usable 87%
c [bca-4] added 78 blocked clauses in 413111 steps
c [sweep-4] limit 4111129 penalty 0 = 0 + 0
c [sweep-4-1] 3333 pos 4.0% + 79197 neg 96.0% = 82530 sched 99.9% ret 82
c [sweep-4-1] 4242792 steps 44 queries 6746.30 avg class size
c [sweep-4-1] 684 decisions 38 SAT calls 174.76 avg env size
c [sweep-4-1] 81948 variables remain 99% (542 retained 1%)
c [decomp-19] removed 140 variables
c [sweep-4-1] removed 140 vars (0 failed, 6 eqs, 9 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 140 vars in TOTAL (1 rounds, 43 queries)
c [phase-count-8] 463401 negative 99.0% of 467948 except 4547 1.0%
c [phase-count-8] 370997 positive 79.3% of 467948 except 96951 20.7%
c [phase-count-8] less non-negative clauses 4547 than limit 46700 (10.0%)
c [phase-count-8] non-pos/non-neg = 96951/4547 = 21.32 >= 2.00 = 200/100
c [lucky-phase-8] forcing lucky phase -1
c [phase-8] phase bias: 0 positive 0%, 70 negative 100%
c [sort-queue-8] sorted 39654 enqueued variables after 24462 conflicts
c [score-dist-8] active 42818 (52%), one 0 (0%), zero 39654 (48%)
c [score-dist-8] max exp 510, different 102 (20%)
c [score-dist-8] median active exp 494, avg 480.1
c [simplification-8] removed 1231 variables 1.5% (82472 remain 32%)
c [simplification-8] removed 6578 irredundant clauses 1.4% (467948 remain 41%)
c [simplification-8] maximum reduction of 1% = max (1%, 1%)
c [simplification-8] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-8] new conflict interval 21666
c [simplification-8] penalized conflict interval 21666 = 1 * 21666
c [simplification-8] hard conflict limit 56961 (soft 46128 + delta 10833)
c [simplification-8] new conflict limit 46128 (hard 56961)
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   95.3   82471   467948     24636   12798   1917 93676  134   225   60  60%      7  100   83   64  129%
c i   99.8   82470   467948     26507   14024   1921 93677  125   198   63  63%     15   71  123   65  188%
c i  100.5   82469   467948     26801   14203   1922 93679  123   195   63  63%     11   67  107   65  163%
c i  100.9   82462   467948     26988   14319   1923 93679  123   193   66  63%      9   66  110   66  168%
c i  103.6   82461   467948     28188   14980   1923 93681  120   185   66  65%      8   57  104   66  156%
c i  103.6   82442   467948     28191   14982   1923 93681  120   185   66  65%      8   57  103   66  155%
c i  103.6   82441   467948     28192   14982   1923 93681  120   185   66  65%      8   57  102   66  154%
c i  111.3   82436   467948     33342   19348   1964 93700   76   142   74  53%     60   11   52   66   78%
c i  111.3   82432   467948     33349   19354   1964 93700   76   142   74  53%     59   11   51   66   77%
c i  111.4   82431   467948     33361   19365   1964 93700   76   143   74  53%     59   12   51   66   77%
c i  111.4   82430   467948     33362   19365   1964 93700   76   143   74  53%     59   12   51   66   77%
c i  111.5   82429   467948     33512   19494   1967 93701   75   150   74  50%     50   19   59   66   90%
c i  111.5   82428   467948     33513   19494   1967 93701   75   150   74  50%     50   19   59   66   89%
c i  111.5   82410   467948     33516   19496   1967 93701   75   150   74  50%     50   19   60   66   91%
c i  111.9   82409   467948     33692   19606   1972 93705   79   157   74  50%     41   26  111   66  168%
c i  112.1   82408   467948     33790   19644   1972 93714   81   159   74  51%     37   27  128   66  192%
c i  112.2   82407   467948     33812   19647   1972 93714   82   159   74  51%     36   28  134   66  202%
c i  112.2   82406   467948     33824   19652   1972 93714   82   159   74  51%     36   28  136   66  205%
c i  114.0   82405   467948     34641   20127   1972 93716   96   175   74  55%     17   44  162   68  240%
c i  114.0   82404   467948     34642   20127   1972 93716   96   175   74  55%     17   44  162   68  239%
c i  114.3   82403   467948     34759   20220   1973 93717   97   178   74  55%     14   46  145   68  215%
c i  116.0   82400   467948     35474   20650   1974 93720   99   176   78  56%      7   43  111   68  164%
c i  133.7   82398   467948     42775   25231   1982 93738  104   151   96  69%     88   14   90   73  123%
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  136.9   82397   467948     44533   26892   1983 93742   91   131  105  70%     21   -6   61   73   84%
c i  141.1   82394   467948     46706   28776   1984 93750   84   120  110  70%     12  -16   88   73  121%
c i  141.2   82393   467948     46709   28778   1984 93750   84   120  110  69%     12  -16   89   73  122%
c i  142.5   82392   467948     47215   29054   1984 93753   91   131  110  69%      5   -5  126   73  171%
c i  142.7   82372   467948     47280   29089   1984 93755   91   131  110  69%      4   -5  119   73  162%
c i  142.7   82371   467948     47283   29091   1984 93755   91   131  110  69%      4   -5  118   73  161%
c i  144.2   82370   467948     47955   29687   1985 93756   88   128  110  69%     -1   -8   73   73   99%
c i  144.9   82369   467948     48266   29826   1986 93756   92   132  110  70%     -3   -4  119   74  162%
c i  145.0   82368   467948     48283   29828   1986 93756   93   132  110  70%     -3   -4  122   74  165%
c 
c [simplification-9] limit 46181 conflicts (hard 56961) hit after 49660 conflicts
c [quatres-5] found 31768 quaternary clauses 37% in total
c [quatres-5-2] added 9 quaternary resolvents
c [ternres-5] limit 25469725 with penalty 0 = 0 + 0
c [ternres-5] all 82368 free variables schedulable
c [ternres-5] 664 ternary resolvents (2 bin, 662 trn)
c [ternres-5] fully completed ternary resolution
c [gauss-4] limit 2546972 penalty 1 = 1 + 0
c [gauss-4] extracted 62 xors of average arity 2.7
c [gauss-4] connected 168 occurrences of 127 variables (average 1.3)
c [gauss-4] limit 2546972 penalty 1 = 1 + 0
c [gauss-4] fully completed
c [gauss-4] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-20] removed 13 variables
c [treelook-3] limit 636743 penalty 2 = 2 + 0 boost 1
c [treelook-3] scheduled 90240 literals 55%
c [treelook-3] scheduling used 636913 steps
c [treelook-3] not fully scheduled
c [treelook-3] limit 636743 penalty 2 = 2 + 0 boost 1
c [treelook-3] used 646356 steps
c [treelook-3] 90235 literals remain 55%
c [treelook-3] 19284 variables remain to probed next time 23%
c [treelook-3] removed 0 variables, found 4749 hbrs
c [unhide-9] limit 1273486 with penalty 2 = 0 + 2
c [unhide-9-9] 2 units, 90 failed, 3407 tauts, 0 hbrs, 2033769 literals
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 113 transitive binary clauses
c [transred-5] found 4 units
c [bca-5] limit of 10000000 steps and 927408 added (scaled 2)
c [bca-5] 139864 out of 164434 literals actually usable 85%
c [bca-5] added 24 blocked clauses in 417098 steps
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 76409170 penalty 0 = 0 + 0
c [sweep-5-1] 3240 pos 4.0% + 78447 neg 96.0% = 81687 sched 99.4% ret 529
c [sweep-5-1] 76495112 steps 660 queries 623.17 avg class size
c [sweep-5-1] 7892 decisions 530 SAT calls 138.19 avg env size
c [sweep-5-1] 61871 variables remain 76% (19848 retained 24%)
c [decomp-22] removed 1158 variables
c [sweep-5-1] removed 1158 vars (1 failed, 153 eqs, 212 impls)
c [sweep-5] considered successful since not run to completion yet
c [sweep-5] removed 1158 vars in TOTAL (1 rounds, 659 queries)
c [phase-count-9] 454283 negative 99.0% of 458836 except 4553 1.0%
c [phase-count-9] 363628 positive 79.3% of 458836 except 95208 20.7%
c [phase-count-9] less non-negative clauses 4553 than limit 45800 (10.0%)
c [phase-count-9] non-pos/non-neg = 95208/4553 = 20.91 >= 2.00 = 200/100
c [lucky-phase-9] forcing lucky phase -1
c [phase-9] phase bias: 0 positive 0%, 23 negative 100%
c [sort-queue-9] sorted 34702 enqueued variables after 49660 conflicts
c [score-dist-9] active 46356 (57%), one 0 (0%), zero 34702 (43%)
c [score-dist-9] max exp 510, different 198 (39%)
c [score-dist-9] median active exp 501, avg 462.7
c [simplification-9] removed 1310 variables 1.6% (81058 remain 31%)
c [simplification-9] removed 9112 irredundant clauses 1.9% (458836 remain 40%)
c [simplification-9] maximum reduction of 2% = max (2%, 2%)
c [simplification-9] geometric conflict interval increment 7222 = 21666 / 3
c [simplification-9] new conflict interval 28888
c [simplification-9] penalized conflict interval 28888 = 1 * 28888
c [simplification-9] hard conflict limit 92992 (soft 78548 + delta 14444)
c [simplification-9] new conflict limit 78548 (hard 92992)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i  160.2   81057   458836     50547   31391   2181 135368  104   143  129  72%     11    7  143   75  190%
c i  160.2   81056   458836     50549   31392   2181 135368  104   143  129  72%     11    7  142   75  189%
c i  162.0   81055   458836     51367   31904   2181 135373  110   156  129  71%      2   20  121   76  160%
c i  162.1   81036   458836     51380   31912   2181 135373  110   156  129  71%      2   19  117   76  154%
c i  164.4   81006   458836     52548   32808   2185 135374  103   148  129  70%      0   11  133   76  174%
c i  164.4   81005   458836     52550   32808   2185 135375  103   148  129  70%      0   11  132   76  173%
c i  164.4   81004   458836     52552   32809   2185 135375  103   148  129  70%      0   11  131   76  172%
c i  164.4   81003   458836     52556   32812   2185 135375  103   148  129  70%      0   11  131   76  172%
c i  164.4   81002   458836     52565   32820   2185 135375  103   148  129  70%      0   11  132   76  173%
c i  169.5   81001   458836     55062   34769   2185 135378   94   131  129  72%     14   -6   66   76   87%
c i  170.3   80961   458836     55505   35207   2186 135379   91   126  129  72%      6  -11   66   76   87%
c i  172.2   80960   458836     56829   36042   2188 135385   88   122  129  72%      2  -14   77   76  101%
c i  172.2   80959   458836     56836   36047   2188 135385   88   122  129  72%      2  -14   76   76  100%
c i  172.2   80958   458836     56840   36049   2188 135385   88   122  129  72%      2  -14   76   76   99%
c i  172.2   80957   458836     56841   36049   2188 135385   88   122  129  72%      2  -14   75   76   99%
c i  172.2   80956   458836     56842   36049   2188 135385   88   122  129  72%      2  -14   75   76   98%
c i  172.2   80955   458836     56843   36049   2188 135385   88   122  129  72%      2  -14   75   76   98%
c i  172.3   80954   458836     56844   36049   2188 135385   88   122  129  72%      2  -14   75   76   97%
c i  172.3   80953   458836     56846   36050   2188 135385   88   122  129  72%      2  -14   74   76   97%
c i  172.3   80952   458836     56847   36050   2188 135385   88   122  129  72%      2  -15   74   76   97%
c i  172.3   80951   458836     56849   36050   2188 135386   88   122  129  72%      2  -15   73   76   96%
c i  172.4   80950   458836     56886   36082   2188 135386   88   122  129  72%      2  -15   74   76   97%
c i  173.4   80949   458836     57638   36714   2192 135394   85   119  129  71%     -2  -17   67   76   87%
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  173.8   80948   458836     57899   36823   2192 135394   88   124  129  71%     -4  -12  119   77  155%
c i  173.8   80947   458836     57900   36823   2192 135394   88   124  129  71%     -4  -12  118   77  154%
c i  173.8   80946   458836     57901   36823   2192 135394   88   124  129  71%     -4  -12  118   77  153%
c i  174.3   80945   458836     58156   36939   2192 135397   92   129  129  71%     -5   -7  143   77  186%
c i  174.3   80944   458836     58157   36939   2192 135397   92   129  129  71%     -5   -7  143   77  185%
c i  174.3   80943   458836     58158   36939   2192 135397   92   129  129  71%     -5   -7  142   77  185%
c i  174.3   80942   458836     58159   36939   2192 135397   92   129  129  71%     -5   -7  141   77  184%
c i  174.4   80941   458836     58179   36942   2192 135397   93   129  129  72%     -5   -7  149   77  193%
c i  174.4   80940   458836     58191   36944   2192 135397   93   129  129  72%     -5   -7  152   77  197%
c i  174.4   80939   458836     58192   36944   2192 135397   93   129  129  72%     -5   -7  151   77  196%
c i  174.4   80938   458836     58193   36944   2192 135397   93   129  129  72%     -5   -7  151   77  196%
c i  174.6   80937   458836     58274   36993   2192 135401   94   132  129  72%     -6   -4  154   77  200%
c i  174.6   80933   458836     58279   36993   2194 135403   94   132  129  72%     -6   -4  151   77  196%
c i  174.6   80929   458836     58280   36993   2194 135403   94   132  129  72%     -6   -5  150   77  195%
c i  178.2   80925   458836     59869   37791   2197 135413  106   148  129  72%      2   12  102   78  130%
c i  191.7   80924   458836     68072   45556   2206 135423   64    85  166  75%     96  -48   51   76   67%
c i  195.1   80916   458836     69802   46838   2209 135427   74   102  166  73%     17  -31   73   77   96%
c i  199.3   80915   458836     72324   49315   2211 135431   69    93  216  74%     10  -38   67   76   88%
c i  201.1   80914   458836     73446   50283   2211 135432   69    96  218  71%     -2  -34   50   76   66%
c i  202.1   80905   458836     73940   50500   2211 135435   83   117  218  71%     -6  -13  179   77  233%
c i  202.1   80904   458836     73941   50500   2211 135435   83   117  218  71%     -6  -13  179   77  232%
c i  202.1   80903   458836     73943   50501   2211 135435   83   117  218  71%     -6  -13  177   77  230%
c i  204.5   80902   458836     74976   50989   2211 135436   95   132  225  72%     -7    2  141   78  181%
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  205.0   80901   458836     75183   51099   2211 135436   95   132  225  72%     -9    2  116   78  149%
c i  205.0   80900   458836     75184   51099   2211 135436   95   132  225  72%     -9    2  116   78  148%
c i  205.0   80899   458836     75185   51099   2211 135436   95   132  225  72%     -9    1  115   78  148%
c i  205.0   80898   458836     75186   51099   2211 135436   95   132  225  72%     -9    1  115   78  147%
c i  205.0   80897   458836     75187   51099   2211 135436   95   132  225  72%     -9    1  114   78  147%
c i  205.0   80896   458836     75188   51099   2211 135436   95   132  225  72%     -9    1  114   78  146%
c i  205.4   80895   458836     75380   51273   2211 135436   95   130  225  73%    -10   -0   96   78  123%
c i  206.3   80823   458836     75797   51547   2212 135436   94   129  245  73%    -11   -1   92   78  118%
c i  206.4   80822   458836     75827   51573   2212 135436   94   129  245  73%    -12   -2   87   78  112%
c -  208.2   80571   458836     76739   24252   2214 135440   89   122   67  73%    -10   -8   75   78   97%
c i  210.5   80570   458836     78362   25318   2216 135440   88   119   89  74%      8  -11   85   78  109%
c i  219.4   80569   458836     84086   30937   2220 135445   64    84  128  76%     55  -43   48   77   63%
c i  220.3   80568   458836     84610   31164   2220 135447   73    96  129  76%     27  -31  121   77  157%
c i  229.3   80567   458836     89576   35193   2225 135461   77   102  143  76%     42  -24   62   78   80%
c i  229.4   80566   458836     89593   35199   2225 135461   78   103  143  76%     41  -23   73   78   94%
c i  229.6   80565   458836     89705   35268   2225 135461   80   107  143  75%     34  -18  105   78  135%
c i  231.9   80564   458836     90869   36327   2229 135462   79   106  143  75%      4  -20   76   78   98%
c i  231.9   80563   458836     90870   36327   2229 135462   79   106  143  75%      4  -20   76   78   97%
c i  231.9   80562   458836     90871   36327   2229 135462   79   106  143  75%      4  -20   75   78   97%
c i  231.9   80561   458836     90872   36327   2229 135462   79   106  143  75%      4  -20   75   78   96%
c i  233.4   80560   458836     91685   37116   2229 135462   77   102  143  76%     -6  -24   68   78   87%
c 
c [simplification-10] limit 78806 conflicts (hard 92992) hit after 92993 conflicts
c [quatres-6] found 30217 quaternary clauses 37% in total
c [quatres-6-2] added 9 single-self-subsuming ternary resolvents
c [ternres-6] limit 41128293 with penalty 0 = 0 + 0
c [ternres-6] all 80366 free variables schedulable
c [ternres-6] 480 ternary resolvents (2 bin, 478 trn)
c [ternres-6] fully completed ternary resolution
c [card-4] limit 2570518 penalty 3 = 3 + 0
c [card-4] found 8193 at-most-one constraints of average size 3.9
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 2570518 for elimination
c [card-4] 8193 out of 8193 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [decomp-23] removed 740 variables
c [basicprobe-3] limit 205641467 penalty 0 = 0 + 0
c [basicprobe-3-0] 22986 probes remain 30% after last round
c [basicprobe-3-0] 641 units = 638 failed (100%) + 3 lifted (0%)
c [basicprobe-3-0] removed 2722 variables, found 165314 hbrs
c [bate-2] eliminated 292 asymmetric tautologies during probing
c [unhide-10] limit 1028207 with penalty 3 = 0 + 3
c [unhide-10-10] 11 units, 579 failed, 22157 tauts, 0 hbrs, 3339546 literals
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 48 transitive binary clauses
c [cce-3] limit of 51410366 steps penalty 2 = 2 + 0
c [cce-3-1] eliminated 2 clauses out of 1232 (0%) of length 9
c [cce-3-1] eliminated 6 clauses out of 500 (1%) of length 8
c [cce-3-1] eliminated 23 clauses out of 768 (3%) of length 7
c [cce-3-1] eliminated 2870 clauses out of 4414 (65%) of length 6
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 2901 large clauses in 51410370 steps
c [cce-3-1] allowing another 25705185 steps for small clauses
c [cce-3-1] scheduling 276992 clauses = 234182 binary + 42810 ternary
c [cce-3-1] tried to eliminate 812 small clauses 0%
c [cce-3-1] eliminated 159 binary clauses 0%
c [cce-3-1] eliminated 25 ternary clauses 0%
c [cce-3-1] eliminated 184 small clauses 0%
c [cce-3-1] eliminated 7659 small clauses in 51410367 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 10560 covered clauses in round 1
c [cce-3] eliminated 10560 covered clauses in TOTAL during 1 rounds
c [elim-8] scheduling all variables this time
c [elim-8] scheduled 76631 variables 100%
c [elim-8] boosting limit by 20
c [elim-8] limit of 8000000000 steps penalty 1 = 1 + 0
c [elim-8] rescheduling of touched variables disabled
c [elim-8-1] eliminated 3449 variables 5% in round 1 in 39415642 steps
c [elim-8-1] backward subsumption/strengthening limit 39415600
c [elim-8-1-1] backward checking 11947 touched variables 16%
c [elim-8-1-1] fully completed backward checking in 1 rounds
c [elim-8-1] subsumed 102 and strengthened 275 clauses in 7018160 steps
c [elim-8-1] rescheduled 904 variables 1% by backward subsumption
c [elim-8-2] eliminated 96 variables 0% in round 2 in 3325783 steps
c [elim-8-2] backward subsumption/strengthening limit 3325700
c [elim-8-2-1] backward checking 734 touched variables 1%
c [elim-8-2-1] fully completed backward checking in 1 rounds
c [elim-8-2] subsumed 7 and strengthened 18 clauses in 527428 steps
c [elim-8-2] rescheduled 57 variables 0% by backward subsumption
c [elim-8-3] eliminated 1 variables 0% in round 3 in 50716 steps
c [elim-8-3] backward subsumption/strengthening limit 50700
c [elim-8-3-1] backward checking 25 touched variables 0%
c [elim-8-3-1] incomplete backward checking 0 remain 0%
c [elim-8-3] subsumed 0 and strengthened 0 clauses in 50701 steps
c [elim-8] fully completed in 3 rounds
c [elim-8] transition to [ all 0 rem 0 ] state
c [elim-8] eliminated 3546 = 5% variables out of 76631 scheduled
c [bca-6] limit of 10000000 steps and 831262 added (scaled 2)
c [bca-6] 127900 out of 146172 literals actually usable 87%
c [bca-6] added 191 blocked clauses in 379265 steps
c [sweep-6] limit 12338488 penalty 0 = 0 + 0
c [sweep-6-1] 2513 pos 4.5% + 53776 neg 95.5% = 56289 sched 77.0% ret 16796
c [sweep-6-1] 12509537 steps 133 queries 2671.62 avg class size
c [sweep-6-1] 1096 decisions 102 SAT calls 60.79 avg env size
c [sweep-6-1] 54699 variables remain 75% (18325 retained 25%)
c [decomp-24] removed 227 variables
c [sweep-6-1] removed 227 vars (0 failed, 33 eqs, 54 impls)
c [sweep-6] considered successful since not run to completion yet
c [sweep-6] removed 227 vars in TOTAL (1 rounds, 132 queries)
c [phase-count-10] 412754 negative 99.6% of 414417 except 1663 0.4%
c [phase-count-10] 323442 positive 78.0% of 414417 except 90975 22.0%
c [phase-count-10] less non-negative clauses 1663 than limit 41400 (10.0%)
c [phase-count-10] non-pos/non-neg = 90975/1663 = 54.71 >= 2.00 = 200/100
c [lucky-phase-10] forcing lucky phase -1
c [phase-10] phase bias: 0 positive 0%, 19 negative 100%
c [sort-queue-10] sorted 28142 enqueued variables after 92993 conflicts
c [score-dist-10] active 44716 (61%), one 0 (0%), zero 28142 (39%)
c [score-dist-10] max exp 510, different 348 (68%)
c [score-dist-10] median active exp 492, avg 418.2
c [simplification-10] removed 7508 variables 9.3% (72858 remain 28%)
c [simplification-10] removed 44419 irredundant clauses 9.7% (414417 remain 36%)
c [simplification-10] maximum reduction of 10% = max (9%, 10%)
c [simplification-10] large reduction 10% >= 5% limit
c [simplification-10] next conflict interval 2000 = 2000/1
c [simplification-10] penalized conflict interval 2000 = 1 * 2000
c [simplification-10] hard conflict limit 104993 (soft 94993 + delta 10000)
c [simplification-10] new conflict limit 94993 (hard 104993)
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  255.0   72857   414417     93091   16748   2004 263714   80   105   61  76%     -7  -20   72   78   93%
c i  263.5   72856   414417     99086   22576   2025 263720   65    86   85  75%     56  -36   60   76   78%
c i  263.5   72855   414417     99087   22576   2025 263720   65    86   85  75%     56  -36   59   76   78%
c i  263.5   72854   414417     99088   22576   2025 263720   65    86   85  75%     56  -36   59   76   77%
c i  263.8   72853   414417     99259   22680   2025 263721   66    88   85  75%     44  -34   72   76   94%
c i  264.6   72852   414417     99762   22974   2025 263722   70    97   85  73%     20  -25   99   77  129%
c i  265.1   72851   414417     99958   23141   2026 263722   71    97   85  73%     13  -24   86   77  112%
c i  266.0   72850   414417    100579   23697   2029 263724   70    96   85  72%     -1  -25   64   77   84%
c i  266.1   72849   414417    100599   23715   2029 263724   70    97   85  72%     -1  -25   65   77   85%
c i  266.5   72848   414417    100859   23879   2030 263725   72   100   85  72%     -6  -21   91   77  119%
c i  266.5   72847   414417    100863   23879   2030 263725   72   100   85  72%     -6  -21   92   77  120%
c i  269.4   72846   414417    102384   24906   2039 263728   82   119   90  69%     -7   -3   87   77  112%
c i  269.5   72829   414417    102483   24968   2042 263736   83   121   91  68%     -8   -1   91   77  117%
c i  269.5   72828   414417    102486   24970   2042 263736   83   121   91  68%     -8   -1   91   77  117%
c i  269.7   72827   414417    102640   25098   2042 263736   83   122   91  68%    -10    1   88   77  113%
c i  269.8   72826   414417    102641   25098   2042 263736   83   122   91  68%    -10    1   87   77  113%
c i  269.8   72825   414417    102654   25103   2042 263736   83   122   91  68%    -10    1   91   77  117%
c i  273.0   72824   414417    104809   27055   2050 263739   68   101   95  67%     -1  -20   32   77   42%
c i  273.1   72817   414417    104849   27072   2050 263739   68   101   95  68%     -1  -20   42   77   55%
c 
c [simplification-11] limit 95028 conflicts (hard 104993) hit after 104994 conflicts
c [quatres-7] found 31593 quaternary clauses 42% in total
c [quatres-7-2] added 6 single-self-subsuming ternary resolvents
c [quatres-7-2] added 30 quaternary resolvents
c [ternres-7] limit 45107270 with penalty 0 = 0 + 0
c [ternres-7] all 72815 free variables schedulable
c [ternres-7] 1356 ternary resolvents (3 bin, 1353 trn)
c [ternres-7] fully completed ternary resolution
c [decomp-25] removed 54 variables
c [simpleprobe-4] 2200 schedulable variables 3%
c [simpleprobe-4] limit 180429080 penalty 0 = 0 + 0
c [decomp-26] removed 2055 variables
c [simpleprobe-4] fully completed simple probing
c [simpleprobe-4] removed 2055 variables, found 59912 hbrs, 495 units
c [unhide-11] limit 2255363 with penalty 2 = 0 + 2
c [unhide-11-11] 3 units, 72 failed, 5201 tauts, 0 hbrs, 717760 literals
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 230 transitive binary clauses
c [transred-7] found 1 units
c [block-4] scheduling all variables this time
c [block-4] scheduled 70623 variables 100%
c [block-4] limit of 112768175 steps penalty 2 = 2 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 168 blocked clauses
c [block-4] 168 < 1/100 * 396305 = 3963 considered unsuccessful
c [elim-9] scheduling all variables this time
c [elim-9] scheduled 70607 variables 100%
c [elim-9] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-9] rescheduling of touched variables disabled
c [elim-9-1] eliminated 1521 variables 2% in round 1 in 36274659 steps
c [elim-9-1] backward subsumption/strengthening limit 36274600
c [elim-9-1-1] backward checking 6774 touched variables 10%
c [elim-9-1-1] fully completed backward checking in 1 rounds
c [elim-9-1] subsumed 33 and strengthened 25 clauses in 1954552 steps
c [elim-9-1] rescheduled 151 variables 0% by backward subsumption
c [elim-9-2] eliminated 10 variables 0% in round 2 in 95958 steps
c [elim-9-2] backward subsumption/strengthening limit 95900
c [elim-9-2-1] backward checking 68 touched variables 0%
c [elim-9-2-1] incomplete backward checking 0 remain 0%
c [elim-9-2] subsumed 4 and strengthened 7 clauses in 95901 steps
c [elim-9-2] rescheduled 19 variables 0% by backward subsumption
c [elim-9-3] eliminated 3 variables 0% in round 3 in 11850 steps
c [elim-9-3] backward subsumption/strengthening limit 11800
c [elim-9-3-1] backward checking 10 touched variables 0%
c [elim-9-3-1] incomplete backward checking 0 remain 0%
c [elim-9-3] subsumed 0 and strengthened 0 clauses in 11801 steps
c [elim-9] fully completed in 3 rounds
c [elim-9] transition to [ all 0 rem 0 ] state
c [elim-9] eliminated 1534 = 2% variables out of 70607 scheduled
c [bca-7] limit of 10000000 steps and 785474 added (scaled 2)
c [bca-7] 118977 out of 138148 literals actually usable 86%
c [bca-7] added 57 blocked clauses in 359966 steps
c [sweep-7] limit 13532181 penalty 0 = 0 + 0
c [sweep-7-1] 2235 pos 4.3% + 50144 neg 95.7% = 52379 sched 75.8% ret 16694
c [sweep-7-1] 13695073 steps 164 queries 2172.22 avg class size
c [sweep-7-1] 1451 decisions 137 SAT calls 71.28 avg env size
c [sweep-7-1] 50022 variables remain 73% (18840 retained 27%)
c [decomp-27] removed 299 variables
c [sweep-7-1] removed 299 vars (0 failed, 36 eqs, 41 impls)
c [sweep-7] removed 299 vars in TOTAL (1 rounds, 163 queries)
c [phase-count-11] 389386 negative 99.6% of 390967 except 1581 0.4%
c [phase-count-11] 301821 positive 77.2% of 390967 except 89146 22.8%
c [phase-count-11] skipping relative phase luck test
c [phase-11] phase bias: 5 positive 100%, 0 negative 0%
c [sort-queue-11] sorted 24308 enqueued variables after 104994 conflicts
c [score-dist-11] active 44466 (65%), one 0 (0%), zero 24308 (35%)
c [score-dist-11] max exp 509, different 383 (75%)
c [score-dist-11] median active exp 491, avg 421.7
c [simplification-11] removed 4041 variables 5.5% (68774 remain 27%)
c [simplification-11] removed 23450 irredundant clauses 5.7% (390967 remain 34%)
c [simplification-11] maximum reduction of 6% = max (6%, 6%)
c [simplification-11] large reduction 6% >= 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 116994 (soft 106994 + delta 10000)
c [simplification-11] new conflict limit 106994 (hard 116994)
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  281.5   68773   390967    105098   23422   2168 301767   70   103   83  68%     -5  -18   73   77   95%
c i  282.1   68766   390967    105521   23678   2169 301768   72   106   84  68%    -10  -14   90   77  117%
c i  282.1   68765   390967    105527   23680   2169 301770   72   106   84  68%    -10  -14   88   77  115%
c i  282.1   68764   390967    105533   23684   2170 301770   72   106   84  67%    -10  -14   87   77  113%
c i  282.2   68763   390967    105619   23736   2170 301773   72   108   84  67%    -11  -13   92   77  120%
c i  283.9   68762   390967    106571   24424   2174 301776   74   109   84  68%    -12  -12   78   77  101%
c i  286.4   68761   390967    108062   25343   2177 301779   83   119   84  70%     -8   -1   87   77  113%
c i  288.6   68760   390967    109463   26505   2179 301786   79   114   84  70%     -8   -6   63   77   82%
c i  292.2   68759   390967    111821   28663   2180 301788   68    98   87  70%      3  -22   61   76   79%
c i  296.5   68758   390967    114536   30782   2180 301790   75   101  106  74%      9  -18   68   77   88%
c 
c [simplification-12] limit 106996 conflicts (hard 116994) hit after 116994 conflicts
c [quatres-8] found 28295 quaternary clauses 40% in total
c [quatres-8-2] added 2 single-self-subsuming ternary resolvents
c [quatres-8-2] added 9 quaternary resolvents
c [ternres-8] limit 48977396 with penalty 0 = 0 + 0
c [ternres-8] all 68727 free variables schedulable
c [ternres-8] 654 ternary resolvents (7 bin, 647 trn)
c [ternres-8] fully completed ternary resolution
c [gauss-5] limit 2448869 penalty 2 = 2 + 0
c [gauss-5] extracted 54 xors of average arity 2.9
c [gauss-5] connected 157 occurrences of 136 variables (average 1.2)
c [gauss-5] limit 2448869 penalty 2 = 2 + 0
c [gauss-5] fully completed
c [gauss-5] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-28] removed 3 variables
c [unhide-12] limit 2448869 with penalty 2 = 0 + 2
c [unhide-12-12] 7 units, 284 failed, 30872 tauts, 0 hbrs, 542220 literals
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 177 transitive binary clauses
c [transred-8] found 1 units
c [cce-4] boosting limit by 10
c [cce-4] limit of 1224434910 steps penalty 1 = 1 + 0
c [cce-4-1] eliminated 5 clauses out of 711 (1%) of length 7
c [cce-4-1] eliminated 100 clauses out of 1731 (6%) of length 6
c [cce-4-1] eliminated 25249 clauses out of 36848 (69%) of length 5
c [cce-4-1] eliminated 15388 clauses out of 27481 (56%) of length 4
c [cce-4-1] completed large round (ATE)
c [cce-4-1] eliminated 40742 large clauses in 784019344 steps
c [cce-4-1] allowing another 392009672 steps for small clauses
c [cce-4-1] scheduling 280136 clauses = 213026 binary + 67110 ternary
c [cce-4-1] tried to eliminate 35714 small clauses 13%
c [cce-4-1] eliminated 5873 binary clauses 3%
c [cce-4-1] eliminated 2647 ternary clauses 4%
c [cce-4-1] eliminated 8520 small clauses 3%
c [cce-4-1] eliminated 11197 small clauses in 1224434910 steps
c [cce-4-1] incomplete small round (ATE)
c [cce-4-1] eliminated 51939 covered clauses in round 1
c [cce-4] eliminated 51939 covered clauses in TOTAL during 1 rounds
c [elim-10] scheduling all variables this time
c [elim-10] scheduled 68394 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 18266 variables 27% in round 1 in 27311573 steps
c [elim-10-1] backward subsumption/strengthening limit 27311500
c [elim-10-1-1] backward checking 38428 touched variables 56%
c [elim-10-1-1] fully completed backward checking in 1 rounds
c [elim-10-1] subsumed 32 and strengthened 18 clauses in 5330529 steps
c [elim-10-1] rescheduled 146 variables 0% by backward subsumption
c [elim-10-2] eliminated 6 variables 0% in round 2 in 102130 steps
c [elim-10-2] backward subsumption/strengthening limit 102100
c [elim-10-2-1] backward checking 72 touched variables 0%
c [elim-10-2-1] incomplete backward checking 0 remain 0%
c [elim-10-2] subsumed 7 and strengthened 3 clauses in 102101 steps
c [elim-10-2] rescheduled 21 variables 0% by backward subsumption
c [elim-10-3] no variable eliminated in round 3 in 35367 steps
c [elim-10] fully completed in 3 rounds
c [elim-10] transition to [ all 0 rem 0 ] state
c [elim-10] eliminated 18273 = 27% variables out of 68394 scheduled
c [bca-8] limit of 10000000 steps and 595810 added (scaled 2)
c [bca-8] 94949 out of 100244 literals actually usable 95%
c [bca-8] added 202 blocked clauses in 226360 steps
c [sweep-8] limit 14693218 penalty 0 = 0 + 0
c [sweep-8-1] 2287 pos 6.0% + 35855 neg 94.0% = 38142 sched 76.1% ret 11979
c [sweep-8-1] 14764751 steps 259 queries 1348.98 avg class size
c [sweep-8-1] 2518 decisions 229 SAT calls 66.21 avg env size
c [sweep-8-1] 34561 variables remain 69% (15399 retained 31%)
c [decomp-29] removed 257 variables
c [sweep-8-1] removed 257 vars (0 failed, 38 eqs, 43 impls)
c [sweep-8] removed 257 vars in TOTAL (1 rounds, 258 queries)
c [phase-count-12] 295961 negative 99.9% of 296388 except 427 0.1%
c [phase-count-12] 213099 positive 71.9% of 296388 except 83289 28.1%
c [phase-count-12] skipping relative phase luck test
c [phase-12] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-12] sorted 17472 enqueued variables after 116994 conflicts
c [score-dist-12] active 32392 (65%), one 0 (0%), zero 17472 (35%)
c [score-dist-12] max exp 509, different 398 (78%)
c [score-dist-12] median active exp 499, avg 435.0
c [simplification-12] removed 18863 variables 27.4% (49864 remain 19%)
c [simplification-12] removed 94579 irredundant clauses 24.2% (296388 remain 26%)
c [simplification-12] maximum reduction of 27% = max (27%, 24%)
c [simplification-12] large reduction 27% >= 5% limit
c [simplification-12] next conflict interval 2000 = 2000/1
c [simplification-12] penalized conflict interval 2000 = 1 * 2000
c [simplification-12] hard conflict limit 128994 (soft 118994 + delta 10000)
c [simplification-12] new conflict limit 118994 (hard 128994)
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  344.8   49863   296388    118344    3747   4372 251294   69   111   39  63%     24   -7   37   76   49%
c i  344.9   49853   296388    118593    3955   4377 251294   69   121   39  58%     14    2   61   76   79%
c 
c [simplification-13] limit 118994 conflicts (hard 128994) hit after 118995 conflicts
c [quatres-9] found 22254 quaternary clauses 54% in total
c [quatres-9-2] added 6 single-self-subsuming ternary resolvents
c [quatres-9-2] added 25 quaternary resolvents
c [ternres-9] limit 49217173 with penalty 0 = 0 + 0
c [ternres-9] all 49853 free variables schedulable
c [ternres-9] 1130 ternary resolvents (1 bin, 1129 trn)
c [ternres-9] fully completed ternary resolution
c [decomp-30] removed 11 variables
c [unhide-13] limit 9843434 with penalty 0 = 0 + 0
c [unhide-13-18] 16 units, 461 failed, 28702 tauts, 0 hbrs, 14698 literals
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 126 transitive binary clauses
c [transred-9] found 2 units
c [cce-5] limit of 246085868 steps penalty 0 = 0 + 0
c [cce-5-1] eliminated 1 clauses out of 1 (100%) of length 60
c [cce-5-1] eliminated 1 clauses out of 1 (100%) of length 59
c [cce-5-1] eliminated 1 clauses out of 1 (100%) of length 58
c [cce-5-1] eliminated 2 clauses out of 2 (100%) of length 57
c [cce-5-1] eliminated 1 clauses out of 2 (50%) of length 56
c [cce-5-1] eliminated 2 clauses out of 2 (100%) of length 55
c [cce-5-1] eliminated 1 clauses out of 2 (50%) of length 54
c [cce-5-1] eliminated 2 clauses out of 2 (100%) of length 53
c [cce-5-1] eliminated 1 clauses out of 2 (50%) of length 52
c [cce-5-1] eliminated 2 clauses out of 2 (100%) of length 51
c [cce-5-1] eliminated 1 clauses out of 2 (50%) of length 50
c [cce-5-1] eliminated 2 clauses out of 2 (100%) of length 49
c [cce-5-1] eliminated 1 clauses out of 2 (50%) of length 48
c [cce-5-1] eliminated 2 clauses out of 2 (100%) of length 47
c [cce-5-1] eliminated 1 clauses out of 2 (50%) of length 46
c [cce-5-1] eliminated 2 clauses out of 2 (100%) of length 45
c [cce-5-1] eliminated 1 clauses out of 2 (50%) of length 44
c [cce-5-1] eliminated 2 clauses out of 2 (100%) 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 3 (33%) 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 3 (67%) of length 29
c [cce-5-1] eliminated 1 clauses out of 1 (100%) 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 1 (100%) 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 2 clauses out of 3 (67%) of length 22
c [cce-5-1] eliminated 1 clauses out of 2 (50%) of length 21
c [cce-5-1] eliminated 2 clauses out of 2 (100%) of length 20
c [cce-5-1] eliminated 1 clauses out of 2 (50%) of length 19
c [cce-5-1] eliminated 2 clauses out of 2 (100%) of length 18
c [cce-5-1] eliminated 1 clauses out of 2 (50%) of length 17
c [cce-5-1] eliminated 3 clauses out of 3 (100%) of length 16
c [cce-5-1] eliminated 1 clauses out of 1 (100%) of length 15
c [cce-5-1] eliminated 1 clauses out of 1 (100%) of length 14
c [cce-5-1] eliminated 2 clauses out of 3 (67%) 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 2 clauses out of 3 (67%) of length 10
c [cce-5-1] eliminated 3 clauses out of 4 (75%) of length 9
c [cce-5-1] eliminated 1 clauses out of 1 (100%) of length 8
c [cce-5-1] eliminated 6 clauses out of 61 (10%) of length 7
c [cce-5-1] eliminated 189 clauses out of 3128 (6%) of length 6
c [cce-5-1] eliminated 1670 clauses out of 14385 (12%) of length 5
c [cce-5-1] incomplete large round (ACCE)
c [cce-5-1] eliminated 1946 large clauses in 246085869 steps
c [cce-5-1] allowing another 123042934 steps for small clauses
c [cce-5-1] scheduling 212198 clauses = 151440 binary + 60758 ternary
c [cce-5-1] tried to eliminate 6197 small clauses 3%
c [cce-5-1] eliminated 1057 binary clauses 1%
c [cce-5-1] eliminated 525 ternary clauses 1%
c [cce-5-1] eliminated 1582 small clauses 1%
c [cce-5-1] eliminated 2018 small clauses in 246085873 steps
c [cce-5-1] incomplete small round (ACCE)
c [cce-5-1] eliminated 3964 covered clauses in round 1
c [cce-5] eliminated 3964 covered clauses in TOTAL during 1 rounds
c [elim-11] scheduling all variables this time
c [elim-11] scheduled 49421 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 1053 variables 2% in round 1 in 22112751 steps
c [elim-11-1] backward subsumption/strengthening limit 22112700
c [elim-11-1-1] backward checking 5600 touched variables 11%
c [elim-11-1-1] fully completed backward checking in 1 rounds
c [elim-11-1] subsumed 16 and strengthened 16 clauses in 1161178 steps
c [elim-11-1] rescheduled 89 variables 0% by backward subsumption
c [elim-11-2] eliminated 6 variables 0% in round 2 in 59871 steps
c [elim-11-2] backward subsumption/strengthening limit 59800
c [elim-11-2-1] backward checking 49 touched variables 0%
c [elim-11-2-1] incomplete backward checking 0 remain 0%
c [elim-11-2] subsumed 1 and strengthened 0 clauses in 59801 steps
c [elim-11-2] rescheduled 3 variables 0% by backward subsumption
c [elim-11-3] no variable eliminated in round 3 in 2101 steps
c [elim-11] fully completed in 3 rounds
c [elim-11] transition to [ all 0 rem 0 ] state
c [elim-11] eliminated 1063 = 2% variables out of 49421 scheduled
c [bca-9] limit of 10000000 steps and 567141 added (scaled 2)
c [bca-9] 88382 out of 96718 literals actually usable 91%
c [bca-9] added 204 blocked clauses in 210624 steps
c [sweep-9] limit 14765152 penalty 0 = 0 + 0
c [sweep-9-1] 2880 pos 8.5% + 30865 neg 91.5% = 33745 sched 69.8% ret 14613
c [sweep-9-1] 14819898 steps 288 queries 1411.84 avg class size
c [sweep-9-1] 3139 decisions 255 SAT calls 67.45 avg env size
c [sweep-9-1] 30693 variables remain 64% (17570 retained 36%)
c [decomp-31] removed 202 variables
c [sweep-9-1] removed 202 vars (0 failed, 39 eqs, 45 impls)
c [sweep-9] removed 202 vars in TOTAL (1 rounds, 287 queries)
c [phase-count-13] 281943 negative 99.9% of 282349 except 406 0.1%
c [phase-count-13] 202068 positive 71.6% of 282349 except 80281 28.4%
c [phase-count-13] skipping relative phase luck test
c [phase-13] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-13] sorted 15637 enqueued variables after 118995 conflicts
c [score-dist-13] active 32519 (68%), one 0 (0%), zero 15637 (32%)
c [score-dist-13] max exp 509, different 379 (74%)
c [score-dist-13] median active exp 500, avg 454.8
c [simplification-13] removed 1697 variables 3.4% (48156 remain 19%)
c [simplification-13] removed 14039 irredundant clauses 4.7% (282349 remain 25%)
c [simplification-13] maximum reduction of 5% = max (3%, 5%)
c [simplification-13] large reduction 5% >= 5% limit
c [simplification-13] next conflict interval 2000 = 2000/1
c [simplification-13] penalized conflict interval 2000 = 1 * 2000
c [simplification-13] hard conflict limit 130995 (soft 120995 + delta 10000)
c [simplification-13] new conflict limit 120995 (hard 130995)
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  357.5   48155   282349    119409    4572   4593 231242   85   157   40  54%     -1   39  177   77  230%
c 
c [simplification-14] limit 120995 conflicts (hard 130995) hit after 121462 conflicts
c [quatres-10] found 22063 quaternary clauses 57% in total
c [quatres-10-2] added 2 single-self-subsuming ternary resolvents
c [quatres-10-2] added 34 quaternary resolvents
c [ternres-10] limit 49881972 with penalty 0 = 0 + 0
c [ternres-10] all 48155 free variables schedulable
c [ternres-10] 887 ternary resolvents (2 bin, 885 trn)
c [ternres-10] fully completed ternary resolution
c [decomp-32] removed 1 variables
c [unhide-14] limit 9976394 with penalty 0 = 0 + 0
c [unhide-14-24] 5 units, 142 failed, 13957 tauts, 0 hbrs, 67748 literals
c [transred-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 145 transitive binary clauses
c [transred-10] found 1 units
c [cce-6] limit of 249409860 steps penalty 0 = 0 + 0
c [cce-6-1] eliminated 2 clauses out of 3 (67%) of length 27
c [cce-6-1] eliminated 1 clauses out of 3 (33%) of length 26
c [cce-6-1] eliminated 3 clauses out of 3 (100%) of length 25
c [cce-6-1] eliminated 3 clauses out of 4 (75%) of length 24
c [cce-6-1] eliminated 3 clauses out of 5 (60%) of length 23
c [cce-6-1] eliminated 3 clauses out of 4 (75%) of length 22
c [cce-6-1] eliminated 3 clauses out of 5 (60%) of length 21
c [cce-6-1] eliminated 3 clauses out of 5 (60%) of length 20
c [cce-6-1] eliminated 2 clauses out of 4 (50%) of length 19
c [cce-6-1] eliminated 4 clauses out of 4 (100%) of length 18
c [cce-6-1] eliminated 2 clauses out of 5 (40%) of length 17
c [cce-6-1] eliminated 3 clauses out of 4 (75%) of length 16
c [cce-6-1] eliminated 3 clauses out of 5 (60%) of length 15
c [cce-6-1] eliminated 3 clauses out of 4 (75%) of length 14
c [cce-6-1] eliminated 2 clauses out of 4 (50%) of length 13
c [cce-6-1] eliminated 4 clauses out of 5 (80%) of length 12
c [cce-6-1] eliminated 2 clauses out of 5 (40%) of length 11
c [cce-6-1] eliminated 3 clauses out of 4 (75%) of length 10
c [cce-6-1] eliminated 3 clauses out of 7 (43%) of length 9
c [cce-6-1] eliminated 3 clauses out of 5 (60%) of length 8
c [cce-6-1] eliminated 4 clauses out of 60 (7%) of length 7
c [cce-6-1] eliminated 5 clauses out of 2944 (0%) of length 6
c [cce-6-1] eliminated 433 clauses out of 12515 (3%) of length 5
c [cce-6-1] incomplete large round (ATE)
c [cce-6-1] eliminated 497 large clauses in 249409864 steps
c [cce-6-1] allowing another 124704932 steps for small clauses
c [cce-6-1] scheduling 204968 clauses = 146334 binary + 58634 ternary
c [cce-6-1] tried to eliminate 6733 small clauses 3%
c [cce-6-1] eliminated 1006 binary clauses 1%
c [cce-6-1] eliminated 451 ternary clauses 1%
c [cce-6-1] eliminated 1457 small clauses 1%
c [cce-6-1] eliminated 1533 small clauses in 249409865 steps
c [cce-6-1] incomplete small round (ATE)
c [cce-6-1] eliminated 2030 covered clauses in round 1
c [cce-6] eliminated 2030 covered clauses in TOTAL during 1 rounds
c [cce-6] 2030 < 1/100 * 278467 = 2784 considered unsuccessful
c [elim-12] scheduling all variables this time
c [elim-12] scheduled 47962 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 553 variables 1% in round 1 in 21332777 steps
c [elim-12-1] backward subsumption/strengthening limit 21332700
c [elim-12-1-1] backward checking 3263 touched variables 7%
c [elim-12-1-1] fully completed backward checking in 1 rounds
c [elim-12-1] subsumed 6 and strengthened 10 clauses in 758658 steps
c [elim-12-1] rescheduled 30 variables 0% by backward subsumption
c [elim-12-2] no variable eliminated in round 2 in 15248 steps
c [elim-12] fully completed in 2 rounds
c [elim-12] transition to [ all 0 rem 0 ] state
c [elim-12] eliminated 553 = 1% variables out of 47962 scheduled
c [bca-10] limit of 10000000 steps and 551999 added (scaled 2)
c [bca-10] 85335 out of 94820 literals actually usable 90%
c [bca-10] added 111 blocked clauses in 204445 steps
c [sweep-10] limit 14964591 penalty 0 = 0 + 0
c [sweep-10-1] 2383 pos 7.9% + 27868 neg 92.1% = 30251 sched 63.8% ret 17158
c [sweep-10-1] 15000863 steps 315 queries 1098.71 avg class size
c [sweep-10-1] 3262 decisions 272 SAT calls 71.24 avg env size
c [sweep-10-1] 27661 variables remain 58% (19682 retained 42%)
c [decomp-33] removed 178 variables
c [sweep-10-1] removed 178 vars (0 failed, 49 eqs, 64 impls)
c [sweep-10] removed 178 vars in TOTAL (1 rounds, 314 queries)
c [phase-count-14] 274327 negative 99.9% of 274724 except 397 0.1%
c [phase-count-14] 196556 positive 71.5% of 274724 except 78168 28.5%
c [phase-count-14] skipping relative phase luck test
c [phase-14] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-14] sorted 14728 enqueued variables after 121462 conflicts
c [score-dist-14] active 32503 (69%), one 0 (0%), zero 14728 (31%)
c [score-dist-14] max exp 510, different 375 (73%)
c [score-dist-14] median active exp 495, avg 461.0
c [simplification-14] removed 924 variables 1.9% (47231 remain 18%)
c [simplification-14] removed 7625 irredundant clauses 2.7% (274724 remain 24%)
c [simplification-14] maximum reduction of 3% = max (2%, 3%)
c [simplification-14] geometric conflict interval increment 7222 = 28888 / 4
c [simplification-14] new conflict interval 36110
c [simplification-14] penalized conflict interval 36110 = 1 * 36110
c [simplification-14] hard conflict limit 175627 (soft 157572 + delta 18055)
c [simplification-14] new conflict limit 157572 (hard 175627)
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  372.9   47230   274724    122485    6773   5069 228005  181   283   45  64%     13  159  291   86  339%
c i  372.9   47228   274724    122486    6773   5069 228005  181   283   45  64%     13  159  289   86  338%
c i  375.5   47224   274724    125284    8613   5079 228010  176   282   46  62%     10  151  132   90  148%
c i  377.2   47222   274724    127110    9543   5107 228043  175   267   46  66%     -1  132  183   92  199%
c i  378.5   47221   274724    128481   10102   5109 228043  171   249   48  69%     -6  112  147   93  158%
c i  395.9   47220   274724    149233   25564   5188 228127  141   224   80  63%    251   83  271   95  286%
c i  396.0   47219   274724    149275   25595   5188 228127  143   226   80  63%    238   84  290   95  305%
c i  396.1   47217   274724    149276   25595   5188 228127  143   226   80  63%    238   84  289   95  304%
c i  396.1   47214   274724    149277   25595   5188 228127  143   226   80  63%    238   84  288   95  303%
c i  396.1   47213   274724    149278   25595   5188 228127  143   226   80  63%    237   84  287   95  302%
c 
c [simplification-15] limit 157612 conflicts (hard 175627) hit after 157613 conflicts
c [quatres-11] found 22172 quaternary clauses 57% in total
c [quatres-11-2] added 3 single-self-subsuming ternary resolvents
c [quatres-11-2] added 20 quaternary resolvents
c [ternres-11] limit 57898097 with penalty 0 = 0 + 0
c [ternres-11] all 47206 free variables schedulable
c [ternres-11] 613 ternary resolvents (6 bin, 607 trn)
c [ternres-11] fully completed ternary resolution
c [card-5] limit 1809315 penalty 4 = 4 + 0
c [card-5] found 4610 at-most-one constraints of average size 4.0
c [card-5] no at-most-two constraint found
c [card-5] using previous limit 1809315 for elimination
c [card-5] 4610 out of 4610 constraints (100%) meet size limits
c [card-5] no units found
c [card-5] no at-most-one constraints generated
c [decomp-34] removed 38 variables
c [treelook-4] limit 723726 penalty 3 = 3 + 0 boost 1
c [treelook-4] scheduled 59676 literals 63%
c [treelook-4] scheduling used 723985 steps
c [treelook-4] not fully scheduled
c [treelook-4] limit 723726 penalty 3 = 3 + 0 boost 1
c [treelook-4] used 762852 steps
c [treelook-4] 59480 literals remain 63%
c [treelook-4] 9820 variables remain to probed next time 21%
c [decomp-35] removed 2 variables
c [treelook-4] removed 2 variables, found 7779 hbrs
c [unhide-15] limit 5789809 with penalty 1 = 0 + 1
c [unhide-15-27] 3 units, 76 failed, 7361 tauts, 0 hbrs, 765905 literals
c [transred-11] limit 2000000 with penalty 0 = 0 + 0
c [transred-11] removed 112 transitive binary clauses
c [block-5] scheduling all variables this time
c [block-5] scheduled 47148 variables 100%
c [block-5] limit of 72372622 steps penalty 3 = 3 + 0
c [block-5] fully completed
c [block-5] transition to [ all 0 rem 0 ] state
c [block-5] eliminated 121 blocked clauses
c [block-5] 121 < 1/100 * 272913 = 2729 considered unsuccessful
c [elim-13] scheduling all variables this time
c [elim-13] scheduled 47144 variables 100%
c [elim-13] almost no limit of 100000000000 steps
c [elim-13] rescheduling of touched variables disabled
c [elim-13-1] eliminated 257 variables 1% in round 1 in 21098479 steps
c [elim-13-1] backward subsumption/strengthening limit 21098400
c [elim-13-1-1] backward checking 1542 touched variables 3%
c [elim-13-1-1] fully completed backward checking in 1 rounds
c [elim-13-1] subsumed 2 and strengthened 16 clauses in 337301 steps
c [elim-13-1] rescheduled 36 variables 0% by backward subsumption
c [elim-13-2] no variable eliminated in round 2 in 19187 steps
c [elim-13] fully completed in 2 rounds
c [elim-13] transition to [ all 0 rem 0 ] state
c [elim-13] eliminated 257 = 1% variables out of 47144 scheduled
c [elim-13] 257 < 1/100 * 47144 = 471 considered unsuccessful
c [bca-11] limit of 10000000 steps and 545665 added (scaled 2)
c [bca-11] 79414 out of 93776 literals actually usable 85%
c [bca-11] added 74 blocked clauses in 214486 steps
c [sweep-11] boosting sweeping limit by 10
c [sweep-11] limit 173694290 penalty 0 = 0 + 0
c [sweep-11-1] 2561 pos 9.3% + 24878 neg 90.7% = 27439 sched 58.5% ret 19448
c [sweep-11-1] 173736699 steps 3747 queries 86.78 avg class size
c [sweep-11-1] 24321 decisions 3197 SAT calls 73.52 avg env size
c [sweep-11-1] 9098 variables remain 20% (37180 retained 80%)
c [decomp-36] removed 1756 variables
c [sweep-11-1] removed 1756 vars (0 failed, 595 eqs, 1001 impls)
c [sweep-11] removed 1756 vars in TOTAL (1 rounds, 3746 queries)
c [phase-count-15] 266673 negative 99.9% of 267072 except 399 0.1%
c [phase-count-15] 190464 positive 71.3% of 267072 except 76608 28.7%
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 12835 enqueued variables after 157613 conflicts
c [score-dist-15] active 32296 (72%), one 351 (1%), zero 12484 (28%)
c [score-dist-15] max exp 510, different 349 (68%)
c [score-dist-15] median active exp 503, avg 479.5
c [simplification-15] removed 2075 variables 4.4% (45131 remain 17%)
c [simplification-15] removed 7652 irredundant clauses 2.8% (267072 remain 23%)
c [simplification-15] maximum reduction of 4% = max (4%, 3%)
c [simplification-15] geometric conflict interval increment 7222 = 36110 / 5
c [simplification-15] new conflict interval 43332
c [simplification-15] penalized conflict interval 43332 = 1 * 43332
c [simplification-15] hard conflict limit 222611 (soft 200945 + delta 21666)
c [simplification-15] new conflict limit 200945 (hard 222611)
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  438.2   45130   267072    175013   39717   5312 332074  206   298  118  69%    279  101  290  133  218%
c i  439.3   45126   267072    176082   40225   5316 332076  208   301  118  69%     33  102  197  134  147%
c -  460.9   45054   267072    199068   25531   5433 332244  132   188   54  71%    213  -17   55  134   41%
c i  470.2   45053   267072    210525   35804   5448 332283   50    72   73  69%    343 -118   38  120   32%
c 
c [simplification-16] limit 200945 conflicts (hard 222611) hit after 222613 conflicts
c [quatres-12] found 21682 quaternary clauses 55% in total
c [quatres-12-2] added 9 single-self-subsuming ternary resolvents
c [quatres-12-2] added 4 quaternary resolvents
c [ternres-12] limit 72913566 with penalty 0 = 0 + 0
c [ternres-12] all 45053 free variables schedulable
c [ternres-12] 721 ternary resolvents (8 bin, 713 trn)
c [ternres-12] fully completed ternary resolution
c [gauss-6] limit 1822839 penalty 3 = 3 + 0
c [gauss-6] extracted 70 xors of average arity 2.6
c [gauss-6] connected 185 occurrences of 139 variables (average 1.3)
c [gauss-6] limit 1822839 penalty 3 = 3 + 0
c [gauss-6] fully completed
c [gauss-6] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-37] removed 2 variables
c [basicprobe-4] limit 364567830 penalty 0 = 0 + 0
c [basicprobe-4-0] 13616 sched 32%, 1454 failed, 105 lifted, 374393 hbrs
c [decomp-38] removed 3300 variables
c [basicprobe-4-1] 12354 probes remain 30% after last round
c [basicprobe-4-1] 1563 units = 1458 failed (93%) + 105 lifted (7%)
c [basicprobe-4-1] removed 3304 variables, found 375902 hbrs
c [bate-3] eliminated 1610 asymmetric tautologies during probing
c [unhide-16] limit 3645678 with penalty 2 = 0 + 2
c [unhide-16-29] 3 units, 111 failed, 93675 tauts, 0 hbrs, 398251 literals
c [transred-12] limit 2000000 with penalty 0 = 0 + 0
c [transred-12] removed 203 transitive binary clauses
c [cce-7] limit of 182283915 steps penalty 1 = 1 + 0
c [cce-7-1] eliminated 1 clauses out of 1 (100%) of length 61
c [cce-7-1] eliminated 1 clauses out of 1 (100%) of length 60
c [cce-7-1] eliminated 1 clauses out of 3 (33%) of length 13
c [cce-7-1] eliminated 3 clauses out of 4 (75%) of length 12
c [cce-7-1] eliminated 1 clauses out of 4 (25%) of length 11
c [cce-7-1] eliminated 1 clauses out of 4 (25%) of length 10
c [cce-7-1] eliminated 2 clauses out of 6 (33%) of length 9
c [cce-7-1] eliminated 2 clauses out of 4 (50%) of length 8
c [cce-7-1] eliminated 3 clauses out of 52 (6%) of length 7
c [cce-7-1] eliminated 2 clauses out of 2822 (0%) of length 6
c [cce-7-1] eliminated 159 clauses out of 9044 (2%) of length 5
c [cce-7-1] eliminated 6 clauses out of 17344 (0%) of length 4
c [cce-7-1] incomplete large round (ACCE)
c [cce-7-1] eliminated 182 large clauses in 182283920 steps
c [cce-7-1] allowing another 91141960 steps for small clauses
c [cce-7-1] scheduling 181523 clauses = 135480 binary + 46043 ternary
c [cce-7-1] tried to eliminate 6024 small clauses 3%
c [cce-7-1] eliminated 917 binary clauses 1%
c [cce-7-1] eliminated 400 ternary clauses 1%
c [cce-7-1] eliminated 1317 small clauses 1%
c [cce-7-1] eliminated 1398 small clauses in 182283915 steps
c [cce-7-1] incomplete small round (ACCE)
c [cce-7-1] eliminated 1580 covered clauses in round 1
c [cce-7] eliminated 1580 covered clauses in TOTAL during 1 rounds
c [cce-7] 1580 < 1/100 * 237304 = 2373 considered unsuccessful
c [bca-12] limit of 10000000 steps and 472600 added (scaled 2)
c [bca-12] 65506 out of 83264 literals actually usable 79%
c [bca-12] added 22 blocked clauses in 190932 steps
c [sweep-12] limit 21874069 penalty 0 = 0 + 0
c [sweep-12-1] 647 pos 8.5% + 6927 neg 91.5% = 7574 sched 18.2% ret 34057
c [sweep-12-1] 22027916 steps 457 queries 206.54 avg class size
c [sweep-12-1] 2966 decisions 387 SAT calls 69.40 avg env size
c [sweep-12-1] 6150 variables remain 15% (34849 retained 85%)
c [decomp-39] removed 796 variables
c [sweep-12-1] removed 796 vars (1 failed, 69 eqs, 122 impls)
c [sweep-12] removed 796 vars in TOTAL (1 rounds, 456 queries)
c [phase-count-16] 232044 negative 99.8% of 232439 except 395 0.2%
c [phase-count-16] 163941 positive 70.5% of 232439 except 68498 29.5%
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 10807 enqueued variables after 222613 conflicts
c [score-dist-16] active 30028 (74%), one 779 (2%), zero 10028 (25%)
c [score-dist-16] max exp 510, different 427 (84%)
c [score-dist-16] median active exp 469, avg 413.8
c [simplification-16] removed 4218 variables 9.4% (40835 remain 16%)
c [simplification-16] removed 34633 irredundant clauses 13.0% (232439 remain 20%)
c [simplification-16] maximum reduction of 13% = max (9%, 13%)
c [simplification-16] large reduction 13% >= 5% limit
c [simplification-16] next conflict interval 2226 = min (222613/100, 43332)
c [simplification-16] penalized conflict interval 2226 = 1 * 2226
c [simplification-16] hard conflict limit 234839 (soft 224839 + delta 10000)
c [simplification-16] new conflict limit 224839 (hard 234839)
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  508.6   40834   232439    225853   50466   5621 533551   44    59  103  74%     53 -104   38  104   37%
c -  514.3   40805   232439    232365   29418   5623 533560   43    70   58  61%    -75  -84   39   98   40%
c 
c [simplification-17] limit 224839 conflicts (hard 234839) hit after 234841 conflicts
c [quatres-13] found 16717 quaternary clauses 52% in total
c [quatres-13-1] removed 2 duplicate quaternary clauses
c [quatres-13-2] added 3 single-self-subsuming ternary resolvents
c [ternres-13] limit 75343373 with penalty 0 = 0 + 0
c [ternres-13] all 40805 free variables schedulable
c [ternres-13] 900 ternary resolvents (0 bin, 900 trn)
c [ternres-13] fully completed ternary resolution
c [decomp-40] removed 30 variables
c [simpleprobe-5] all 40805 free variables schedulable
c [simpleprobe-5] limit 200000000 penalty 0 = 0 + 0
c [decomp-41] removed 774 variables
c [simpleprobe-5] fully completed simple probing
c [simpleprobe-5] removed 774 variables, found 182381 hbrs, 178 units
c [unhide-17] limit 7534337 with penalty 1 = 0 + 1
c [unhide-17-33] 3 units, 440 failed, 164468 tauts, 0 hbrs, 329562 literals
c [transred-13] limit 2000000 with penalty 0 = 0 + 0
c [transred-13] removed 278 transitive binary clauses
c [elim-14] scheduling all variables this time
c [elim-14] scheduled 39859 variables 100%
c [elim-14] limit of 400000000 steps penalty 1 = 1 + 0
c [elim-14] rescheduling of touched variables disabled
c [elim-14-1] eliminated 1957 variables 5% in round 1 in 21272585 steps
c [elim-14-1] backward subsumption/strengthening limit 21272500
c [elim-14-1-1] backward checking 8685 touched variables 22%
c [elim-14-1-1] fully completed backward checking in 1 rounds
c [elim-14-1] subsumed 38 and strengthened 13 clauses in 1864729 steps
c [elim-14-1] rescheduled 130 variables 0% by backward subsumption
c [elim-14-2] eliminated 12 variables 0% in round 2 in 138621 steps
c [elim-14-2] backward subsumption/strengthening limit 138600
c [elim-14-2-1] backward checking 92 touched variables 0%
c [elim-14-2-1] fully completed backward checking in 1 rounds
c [elim-14-2] subsumed 2 and strengthened 10 clauses in 108641 steps
c [elim-14-2] rescheduled 26 variables 0% by backward subsumption
c [elim-14-3] no variable eliminated in round 3 in 25695 steps
c [elim-14] fully completed in 3 rounds
c [elim-14] transition to [ all 0 rem 0 ] state
c [elim-14] eliminated 1969 = 5% variables out of 39859 scheduled
c [bca-13] limit of 10000000 steps and 446477 added (scaled 2)
c [bca-13] 59062 out of 75782 literals actually usable 78%
c [bca-13] added 42 blocked clauses in 158879 steps
c [sweep-13] limit 22603011 penalty 0 = 0 + 0
c [sweep-13-1] 601 pos 10.9% + 4931 neg 89.1% = 5532 sched 14.6% ret 32358
c [sweep-13-1] 22670741 steps 588 queries 123.09 avg class size
c [sweep-13-1] 4477 decisions 515 SAT calls 86.28 avg env size
c [sweep-13-1] 4047 variables remain 11% (33839 retained 89%)
c [decomp-42] removed 220 variables
c [sweep-13-1] removed 220 vars (0 failed, 75 eqs, 153 impls)
c [sweep-13] removed 220 vars in TOTAL (1 rounds, 587 queries)
c [phase-count-17] 222021 negative 99.8% of 222392 except 371 0.2%
c [phase-count-17] 155051 positive 69.7% of 222392 except 67341 30.3%
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 9285 enqueued variables after 234841 conflicts
c [score-dist-17] active 28385 (75%), one 817 (2%), zero 8468 (22%)
c [score-dist-17] max exp 510, different 416 (81%)
c [score-dist-17] median active exp 494, avg 419.4
c [simplification-17] removed 3135 variables 7.7% (37670 remain 15%)
c [simplification-17] removed 10047 irredundant clauses 4.3% (222392 remain 19%)
c [simplification-17] maximum reduction of 8% = max (8%, 4%)
c [simplification-17] large reduction 8% >= 5% limit
c [simplification-17] next conflict interval 2348 = min (234841/100, 43332)
c [simplification-17] penalized conflict interval 2348 = 1 * 2348
c [simplification-17] hard conflict limit 247189 (soft 237189 + delta 10000)
c [simplification-17] new conflict limit 237189 (hard 247189)
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  531.0   37669   222392    240825   34821   5330 449351   29    38   70  75%     57 -104   26   90   29%
c 
c [simplification-18] limit 237189 conflicts (hard 247189) hit after 247190 conflicts
c [quatres-14] found 16165 quaternary clauses 49% in total
c [quatres-14-1] removed 3 duplicate quaternary clauses
c [quatres-14-2] added 3 single-self-subsuming ternary resolvents
c [quatres-14-2] added 8 quaternary resolvents
c [ternres-14] limit 77805705 with penalty 0 = 0 + 0
c [ternres-14] all 37666 free variables schedulable
c [ternres-14] 850 ternary resolvents (5 bin, 845 trn)
c [ternres-14] fully completed ternary resolution
c [decomp-43] removed 4 variables
c [unhide-18] limit 7780570 with penalty 1 = 0 + 1
c [unhide-18-37] 2 units, 41 failed, 49129 tauts, 0 hbrs, 499877 literals
c [transred-14] limit 2000000 with penalty 0 = 0 + 0
c [transred-14] removed 246 transitive binary clauses
c [elim-15] scheduling all variables this time
c [elim-15] scheduled 37596 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 200 variables 1% in round 1 in 34991425 steps
c [elim-15-1] backward subsumption/strengthening limit 34991400
c [elim-15-1-1] backward checking 1334 touched variables 4%
c [elim-15-1-1] fully completed backward checking in 1 rounds
c [elim-15-1] subsumed 4 and strengthened 12 clauses in 303067 steps
c [elim-15-1] rescheduled 32 variables 0% by backward subsumption
c [elim-15-2] eliminated 1 variables 0% in round 2 in 124566 steps
c [elim-15-2] backward subsumption/strengthening limit 124500
c [elim-15-2-1] backward checking 15 touched variables 0%
c [elim-15-2-1] fully completed backward checking in 1 rounds
c [elim-15-2] subsumed 0 and strengthened 0 clauses in 32987 steps
c [elim-15] fully completed in 2 rounds
c [elim-15] transition to [ all 0 rem 0 ] state
c [elim-15] eliminated 201 = 1% variables out of 37596 scheduled
c [elim-15] 201 < 1/100 * 37596 = 375 considered unsuccessful
c [bca-14] limit of 10000000 steps and 440168 added (scaled 2)
c [bca-14] 57515 out of 74792 literals actually usable 77%
c [bca-14] added 22 blocked clauses in 165894 steps
c [sweep-14] limit 23341711 penalty 0 = 0 + 0
c [sweep-14-1] 435 pos 11.2% + 3455 neg 88.8% = 3890 sched 10.4% ret 33505
c [sweep-14-1] 23362275 steps 587 queries 78.32 avg class size
c [sweep-14-1] 4079 decisions 523 SAT calls 87.85 avg env size
c [sweep-14-1] 2676 variables remain 7% (34717 retained 93%)
c [decomp-44] removed 151 variables
c [sweep-14-1] removed 151 vars (0 failed, 64 eqs, 133 impls)
c [sweep-14] removed 151 vars in TOTAL (1 rounds, 586 queries)
c [sort-queue-18] sorted 9161 enqueued variables after 247190 conflicts
c [score-dist-18] active 28083 (75%), one 952 (3%), zero 8209 (22%)
c [score-dist-18] max exp 510, different 423 (83%)
c [score-dist-18] median active exp 493, avg 423.9
c [simplification-18] removed 422 variables 1.1% (37244 remain 14%)
c [simplification-18] removed 3081 irredundant clauses 1.4% (219311 remain 19%)
c [simplification-18] maximum reduction of 1% = max (1%, 1%)
c [simplification-18] geometric conflict interval increment 21666 = 43332 / 2
c [simplification-18] new conflict interval 64998
c [simplification-18] penalized conflict interval 64998 = 1 * 64998
c [simplification-18] hard conflict limit 344687 (soft 312188 + delta 32499)
c [simplification-18] new conflict limit 312188 (hard 344687)
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  555.1   37243   219311    257467   48962   5836 413425   55    84   90  65%     90  -41   41   81   51%
c -  564.7   37097   219311    267805   30617   5856 413464   44    66   57  66%      1  -51   45   75   60%
c i  565.6   37096   219311    268850   31445   5858 413469   72   117   74  61%     17    0  312   77  408%
c i  570.4   37038   219311    274419   34752   5866 413473  138   212   79  65%    -66   89   91   85  108%
c i  583.5   37036   219311    291183   48636   5886 413484   66   106  102  63%    111  -20   63   81   77%
c i  590.0   37017   219311    298972   55067   5905 413513   70   107  115  65%    -23  -17   68   80   84%
c i  592.9   37002   219311    302172   57143   5906 413516   79   112  115  71%    -86  -12   83   81  103%
c -  596.2   36998   219311    305361   29708   5913 413527   65    92   52  71%    -84  -30   58   79   73%
c i  606.4   36997   219311    317870   41019   5939 413551   52    78   82  67%    106  -34   70   73   96%
c 
c [simplification-19] limit 312188 conflicts (hard 344687) hit after 326831 conflicts
c [quatres-15] found 15110 quaternary clauses 46% in total
c [quatres-15-2] added 1 single-self-subsuming ternary resolvents
c [quatres-15-2] added 9 quaternary resolvents
c [ternres-15] limit 94098143 with penalty 0 = 0 + 0
c [ternres-15] all 36970 free variables schedulable
c [ternres-15] 284 ternary resolvents (0 bin, 284 trn)
c [ternres-15] fully completed ternary resolution
c [decomp-45] removed 306 variables
c [treelook-5] limit 2352453 penalty 2 = 2 + 0 boost 1
c [treelook-5] scheduled 43899 literals 59%
c [treelook-5] scheduling used 747371 steps
c [treelook-5] scheduled completely
c [treelook-5] limit 2352453 penalty 2 = 2 + 0 boost 1
c [treelook-5] used 2523964 steps
c [treelook-5] 43874 literals remain 59%
c [treelook-5] 6416 variables remain to probed next time 17%
c [decomp-46] removed 1 variables
c [treelook-5] removed 1 variables, found 10649 hbrs
c [unhide-19] limit 9409814 with penalty 1 = 0 + 1
c [unhide-19-42] 1 units, 8 failed, 46392 tauts, 0 hbrs, 1335017 literals
c [transred-15] limit 2000000 with penalty 0 = 0 + 0
c [transred-15] removed 190 transitive binary clauses
c [cce-8] boosting limit by 10
c [cce-8] limit of 1176226792 steps penalty 2 = 2 + 0
c [cce-8-1] eliminated 1 clauses out of 1 (100%) of length 207
c [cce-8-1] eliminated 1 clauses out of 1 (100%) of length 206
c [cce-8-1] eliminated 2 clauses out of 2 (100%) of length 205
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 204
c [cce-8-1] eliminated 2 clauses out of 2 (100%) of length 203
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 202
c [cce-8-1] eliminated 2 clauses out of 2 (100%) of length 201
c [cce-8-1] eliminated 2 clauses out of 2 (100%) of length 200
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 199
c [cce-8-1] eliminated 2 clauses out of 2 (100%) of length 198
c [cce-8-1] eliminated 1 clauses out of 1 (100%) of length 197
c [cce-8-1] eliminated 2 clauses out of 2 (100%) of length 196
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 195
c [cce-8-1] eliminated 2 clauses out of 2 (100%) of length 194
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 193
c [cce-8-1] eliminated 2 clauses out of 2 (100%) of length 192
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 191
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 190
c [cce-8-1] eliminated 2 clauses out of 2 (100%) of length 189
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 188
c [cce-8-1] eliminated 2 clauses out of 2 (100%) of length 187
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 186
c [cce-8-1] eliminated 2 clauses out of 2 (100%) of length 185
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 184
c [cce-8-1] eliminated 2 clauses out of 2 (100%) of length 183
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 182
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 181
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 180
c [cce-8-1] eliminated 2 clauses out of 2 (100%) of length 179
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 178
c [cce-8-1] eliminated 1 clauses out of 1 (100%) of length 177
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 176
c [cce-8-1] eliminated 2 clauses out of 2 (100%) of length 175
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 174
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 173
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 172
c [cce-8-1] eliminated 2 clauses out of 2 (100%) of length 171
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 170
c [cce-8-1] eliminated 2 clauses out of 2 (100%) of length 169
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 168
c [cce-8-1] eliminated 2 clauses out of 2 (100%) of length 167
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 166
c [cce-8-1] eliminated 2 clauses out of 2 (100%) of length 165
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 164
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 163
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 162
c [cce-8-1] eliminated 2 clauses out of 2 (100%) of length 161
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 160
c [cce-8-1] eliminated 2 clauses out of 2 (100%) of length 159
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 158
c [cce-8-1] eliminated 2 clauses out of 2 (100%) of length 157
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 156
c [cce-8-1] eliminated 1 clauses out of 1 (100%) of length 155
c [cce-8-1] eliminated 3 clauses out of 3 (100%) of length 154
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 153
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 152
c [cce-8-1] eliminated 2 clauses out of 2 (100%) of length 151
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 150
c [cce-8-1] eliminated 2 clauses out of 2 (100%) of length 149
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 148
c [cce-8-1] eliminated 1 clauses out of 1 (100%) of length 147
c [cce-8-1] eliminated 2 clauses out of 3 (67%) of length 146
c [cce-8-1] eliminated 1 clauses out of 1 (100%) of length 145
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 144
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 143
c [cce-8-1] eliminated 2 clauses out of 2 (100%) of length 142
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 141
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 140
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 139
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 138
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 137
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 136
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 135
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 134
c [cce-8-1] eliminated 2 clauses out of 2 (100%) of length 133
c [cce-8-1] eliminated 1 clauses out of 3 (33%) of length 132
c [cce-8-1] eliminated 2 clauses out of 3 (67%) of length 131
c [cce-8-1] eliminated 2 clauses out of 3 (67%) of length 130
c [cce-8-1] eliminated 2 clauses out of 3 (67%) of length 129
c [cce-8-1] eliminated 2 clauses out of 4 (50%) of length 128
c [cce-8-1] eliminated 2 clauses out of 3 (67%) of length 127
c [cce-8-1] eliminated 3 clauses out of 4 (75%) of length 126
c [cce-8-1] eliminated 3 clauses out of 5 (60%) of length 125
c [cce-8-1] eliminated 2 clauses out of 3 (67%) of length 124
c [cce-8-1] eliminated 2 clauses out of 4 (50%) of length 123
c [cce-8-1] eliminated 3 clauses out of 4 (75%) of length 122
c [cce-8-1] eliminated 2 clauses out of 4 (50%) of length 121
c [cce-8-1] eliminated 3 clauses out of 3 (100%) of length 120
c [cce-8-1] eliminated 3 clauses out of 4 (75%) of length 119
c [cce-8-1] eliminated 3 clauses out of 4 (75%) of length 118
c [cce-8-1] eliminated 2 clauses out of 3 (67%) of length 117
c [cce-8-1] eliminated 3 clauses out of 4 (75%) of length 116
c [cce-8-1] eliminated 2 clauses out of 4 (50%) of length 115
c [cce-8-1] eliminated 2 clauses out of 3 (67%) of length 114
c [cce-8-1] eliminated 2 clauses out of 4 (50%) of length 113
c [cce-8-1] eliminated 2 clauses out of 4 (50%) of length 112
c [cce-8-1] eliminated 3 clauses out of 4 (75%) of length 111
c [cce-8-1] eliminated 2 clauses out of 4 (50%) of length 110
c [cce-8-1] eliminated 3 clauses out of 4 (75%) of length 109
c [cce-8-1] eliminated 2 clauses out of 4 (50%) of length 108
c [cce-8-1] eliminated 4 clauses out of 4 (100%) of length 107
c [cce-8-1] eliminated 2 clauses out of 4 (50%) of length 106
c [cce-8-1] eliminated 3 clauses out of 4 (75%) of length 105
c [cce-8-1] eliminated 2 clauses out of 4 (50%) of length 104
c [cce-8-1] eliminated 3 clauses out of 4 (75%) of length 103
c [cce-8-1] eliminated 2 clauses out of 4 (50%) of length 102
c [cce-8-1] eliminated 2 clauses out of 4 (50%) of length 101
c [cce-8-1] eliminated 2 clauses out of 4 (50%) of length 100
c [cce-8-1] eliminated 3 clauses out of 4 (75%) of length 99
c [cce-8-1] eliminated 2 clauses out of 4 (50%) of length 98
c [cce-8-1] eliminated 2 clauses out of 5 (40%) of length 97
c [cce-8-1] eliminated 2 clauses out of 3 (67%) of length 96
c [cce-8-1] eliminated 2 clauses out of 4 (50%) of length 95
c [cce-8-1] eliminated 2 clauses out of 4 (50%) of length 94
c [cce-8-1] eliminated 3 clauses out of 4 (75%) of length 93
c [cce-8-1] eliminated 2 clauses out of 4 (50%) of length 92
c [cce-8-1] eliminated 3 clauses out of 4 (75%) of length 91
c [cce-8-1] eliminated 2 clauses out of 4 (50%) of length 90
c [cce-8-1] eliminated 2 clauses out of 4 (50%) of length 89
c [cce-8-1] eliminated 3 clauses out of 4 (75%) of length 88
c [cce-8-1] eliminated 2 clauses out of 4 (50%) of length 87
c [cce-8-1] eliminated 3 clauses out of 4 (75%) of length 86
c [cce-8-1] eliminated 2 clauses out of 4 (50%) of length 85
c [cce-8-1] eliminated 3 clauses out of 4 (75%) of length 84
c [cce-8-1] eliminated 2 clauses out of 4 (50%) of length 83
c [cce-8-1] eliminated 3 clauses out of 4 (75%) of length 82
c [cce-8-1] eliminated 2 clauses out of 4 (50%) of length 81
c [cce-8-1] eliminated 3 clauses out of 4 (75%) of length 80
c [cce-8-1] eliminated 2 clauses out of 4 (50%) of length 79
c [cce-8-1] eliminated 3 clauses out of 4 (75%) of length 78
c [cce-8-1] eliminated 2 clauses out of 4 (50%) of length 77
c [cce-8-1] eliminated 3 clauses out of 4 (75%) of length 76
c [cce-8-1] eliminated 2 clauses out of 4 (50%) of length 75
c [cce-8-1] eliminated 3 clauses out of 4 (75%) of length 74
c [cce-8-1] eliminated 2 clauses out of 4 (50%) of length 73
c [cce-8-1] eliminated 3 clauses out of 4 (75%) of length 72
c [cce-8-1] eliminated 2 clauses out of 4 (50%) of length 71
c [cce-8-1] eliminated 3 clauses out of 5 (60%) of length 70
c [cce-8-1] eliminated 2 clauses out of 3 (67%) of length 69
c [cce-8-1] eliminated 3 clauses out of 4 (75%) of length 68
c [cce-8-1] eliminated 2 clauses out of 4 (50%) of length 67
c [cce-8-1] eliminated 3 clauses out of 4 (75%) of length 66
c [cce-8-1] eliminated 2 clauses out of 4 (50%) of length 65
c [cce-8-1] eliminated 3 clauses out of 4 (75%) of length 64
c [cce-8-1] eliminated 2 clauses out of 4 (50%) of length 63
c [cce-8-1] eliminated 3 clauses out of 5 (60%) of length 62
c [cce-8-1] eliminated 2 clauses out of 4 (50%) of length 61
c [cce-8-1] eliminated 2 clauses out of 5 (40%) of length 60
c [cce-8-1] eliminated 2 clauses out of 4 (50%) of length 59
c [cce-8-1] eliminated 2 clauses out of 4 (50%) of length 58
c [cce-8-1] eliminated 3 clauses out of 5 (60%) of length 57
c [cce-8-1] eliminated 2 clauses out of 4 (50%) of length 56
c [cce-8-1] eliminated 3 clauses out of 4 (75%) of length 55
c [cce-8-1] eliminated 2 clauses out of 3 (67%) of length 54
c [cce-8-1] eliminated 2 clauses out of 4 (50%) of length 53
c [cce-8-1] eliminated 2 clauses out of 4 (50%) of length 52
c [cce-8-1] eliminated 2 clauses out of 5 (40%) of length 51
c [cce-8-1] eliminated 3 clauses out of 5 (60%) of length 50
c [cce-8-1] eliminated 4 clauses out of 6 (67%) of length 49
c [cce-8-1] eliminated 3 clauses out of 5 (60%) of length 48
c [cce-8-1] eliminated 3 clauses out of 7 (43%) of length 47
c [cce-8-1] eliminated 4 clauses out of 6 (67%) of length 46
c [cce-8-1] eliminated 4 clauses out of 7 (57%) of length 45
c [cce-8-1] eliminated 4 clauses out of 8 (50%) of length 44
c [cce-8-1] eliminated 3 clauses out of 5 (60%) of length 43
c [cce-8-1] eliminated 4 clauses out of 7 (57%) of length 42
c [cce-8-1] eliminated 3 clauses out of 6 (50%) of length 41
c [cce-8-1] eliminated 5 clauses out of 7 (71%) of length 40
c [cce-8-1] eliminated 3 clauses out of 6 (50%) of length 39
c [cce-8-1] eliminated 5 clauses out of 7 (71%) of length 38
c [cce-8-1] eliminated 3 clauses out of 6 (50%) of length 37
c [cce-8-1] eliminated 4 clauses out of 7 (57%) of length 36
c [cce-8-1] eliminated 3 clauses out of 6 (50%) of length 35
c [cce-8-1] eliminated 4 clauses out of 7 (57%) of length 34
c [cce-8-1] eliminated 3 clauses out of 6 (50%) of length 33
c [cce-8-1] eliminated 4 clauses out of 7 (57%) of length 32
c [cce-8-1] eliminated 3 clauses out of 6 (50%) of length 31
c [cce-8-1] eliminated 4 clauses out of 10 (40%) of length 30
c [cce-8-1] eliminated 5 clauses out of 9 (56%) of length 29
c [cce-8-1] eliminated 7 clauses out of 10 (70%) of length 28
c [cce-8-1] eliminated 6 clauses out of 12 (50%) of length 27
c [cce-8-1] eliminated 7 clauses out of 12 (58%) of length 26
c [cce-8-1] eliminated 5 clauses out of 11 (45%) of length 25
c [cce-8-1] eliminated 8 clauses out of 12 (67%) of length 24
c [cce-8-1] eliminated 7 clauses out of 12 (58%) of length 23
c [cce-8-1] eliminated 5 clauses out of 11 (45%) of length 22
c [cce-8-1] eliminated 10 clauses out of 14 (71%) of length 21
c [cce-8-1] eliminated 6 clauses out of 15 (40%) of length 20
c [cce-8-1] eliminated 10 clauses out of 13 (77%) of length 19
c [cce-8-1] eliminated 6 clauses out of 14 (43%) of length 18
c [cce-8-1] eliminated 10 clauses out of 13 (77%) of length 17
c [cce-8-1] eliminated 6 clauses out of 14 (43%) of length 16
c [cce-8-1] eliminated 11 clauses out of 14 (79%) of length 15
c [cce-8-1] eliminated 6 clauses out of 16 (38%) of length 14
c [cce-8-1] eliminated 11 clauses out of 13 (85%) of length 13
c [cce-8-1] eliminated 7 clauses out of 16 (44%) of length 12
c [cce-8-1] eliminated 10 clauses out of 17 (59%) of length 11
c [cce-8-1] eliminated 13 clauses out of 21 (62%) of length 10
c [cce-8-1] eliminated 16 clauses out of 31 (52%) of length 9
c [cce-8-1] eliminated 18 clauses out of 30 (60%) of length 8
c [cce-8-1] eliminated 25 clauses out of 87 (29%) of length 7
c [cce-8-1] eliminated 21 clauses out of 2841 (1%) of length 6
c [cce-8-1] eliminated 86 clauses out of 8884 (1%) of length 5
c [cce-8-1] eliminated 1212 clauses out of 14356 (8%) of length 4
c [cce-8-1] completed large round (ATE)
c [cce-8-1] eliminated 1908 large clauses in 513217804 steps
c [cce-8-1] allowing another 256608902 steps for small clauses
c [cce-8-1] scheduling 164029 clauses = 125916 binary + 38113 ternary
c [cce-8-1] tried to eliminate 46977 small clauses 29%
c [cce-8-1] eliminated 5795 binary clauses 5%
c [cce-8-1] eliminated 2388 ternary clauses 6%
c [cce-8-1] eliminated 8183 small clauses 5%
c [cce-8-1] eliminated 8479 small clauses in 1176226793 steps
c [cce-8-1] incomplete small round (ATE)
c [cce-8-1] eliminated 10387 covered clauses in round 1
c [cce-8] eliminated 10387 covered clauses in TOTAL during 1 rounds
c [bca-15] limit of 10000000 steps and 409123 added (scaled 2)
c [bca-15] 56095 out of 73642 literals actually usable 76%
c [bca-15] added 14 blocked clauses in 162930 steps
c [sweep-15] limit 28229443 penalty 0 = 0 + 0
c [sweep-15-1] 239 pos 9.5% + 2289 neg 90.5% = 2528 sched 6.9% ret 34292
c [sweep-15-1] 28276609 steps 840 queries 31.67 avg class size
c [sweep-15-1] 5163 decisions 767 SAT calls 78.24 avg env size
c [sweep-15-1] 1028 variables remain 3% (35786 retained 97%)
c [decomp-47] removed 161 variables
c [sweep-15-1] removed 161 vars (0 failed, 73 eqs, 221 impls)
c [sweep-15] removed 161 vars in TOTAL (1 rounds, 839 queries)
c [sort-queue-19] sorted 11144 enqueued variables after 326831 conflicts
c [score-dist-19] active 25515 (70%), one 3345 (9%), zero 7799 (21%)
c [score-dist-19] max exp 510, different 425 (83%)
c [score-dist-19] median active exp 502, avg 431.5
c [simplification-19] removed 311 variables 0.8% (36659 remain 14%)
c [simplification-19] removed 15562 irredundant clauses 7.1% (203749 remain 18%)
c [simplification-19] maximum reduction of 7% = max (1%, 7%)
c [simplification-19] large reduction 7% >= 5% limit
c [simplification-19] next conflict interval 3268 = min (326831/100, 64998)
c [simplification-19] penalized conflict interval 3268 = 1 * 3268
c [simplification-19] hard conflict limit 340099 (soft 330099 + delta 10000)
c [simplification-19] new conflict limit 330099 (hard 340099)
c 
c [simplification-20] limit 330099 conflicts (hard 340099) hit after 340101 conflicts
c [quatres-16] found 13928 quaternary clauses 45% in total
c [quatres-16-1] removed 2 duplicate quaternary clauses
c [quatres-16-2] added 1 single-self-subsuming ternary resolvents
c [ternres-16] limit 97102182 with penalty 0 = 0 + 0
c [ternres-16] all 36659 free variables schedulable
c [ternres-16] 411 ternary resolvents (0 bin, 411 trn)
c [ternres-16] fully completed ternary resolution
c [basicprobe-5] limit 400000000 penalty 0 = 0 + 0
c [basicprobe-5-0] 11353 sched 32%, 464 failed, 47 lifted, 203626 hbrs
c [decomp-49] removed 1276 variables
c [basicprobe-5-1] 8693 probes remain 25% after last round
c [basicprobe-5-1] 567 units = 520 failed (92%) + 47 lifted (8%)
c [basicprobe-5-1] removed 1408 variables, found 211233 hbrs
c [bate-4] eliminated 105 asymmetric tautologies during probing
c [unhide-20] limit 4855109 with penalty 2 = 0 + 2
c [unhide-20-44] 1 units, 19 failed, 56552 tauts, 0 hbrs, 431420 literals
c [transred-16] limit 2000000 with penalty 0 = 0 + 0
c [transred-16] removed 253 transitive binary clauses
c [block-6] scheduling all variables this time
c [block-6] scheduled 35232 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 89 blocked clauses
c [block-6] 89 < 1/100 * 193805 = 1938 considered unsuccessful
c [elim-16] scheduling all variables this time
c [elim-16] scheduled 35232 variables 100%
c [elim-16] limit of 400000000 steps penalty 1 = 1 + 0
c [elim-16] rescheduling of touched variables disabled
c [elim-16-1] eliminated 1597 variables 5% in round 1 in 18186291 steps
c [elim-16-1] backward subsumption/strengthening limit 18186200
c [elim-16-1-1] backward checking 7977 touched variables 23%
c [elim-16-1-1] fully completed backward checking in 1 rounds
c [elim-16-1] subsumed 15 and strengthened 35 clauses in 1412314 steps
c [elim-16-1] rescheduled 123 variables 0% by backward subsumption
c [elim-16-2] eliminated 12 variables 0% in round 2 in 117516 steps
c [elim-16-2] backward subsumption/strengthening limit 117500
c [elim-16-2-1] backward checking 100 touched variables 0%
c [elim-16-2-1] fully completed backward checking in 1 rounds
c [elim-16-2] subsumed 6 and strengthened 9 clauses in 78724 steps
c [elim-16-2] rescheduled 32 variables 0% by backward subsumption
c [elim-16-3] eliminated 3 variables 0% in round 3 in 43226 steps
c [elim-16-3] backward subsumption/strengthening limit 43200
c [elim-16-3-1] backward checking 25 touched variables 0%
c [elim-16-3-1] incomplete backward checking 0 remain 0%
c [elim-16-3] subsumed 0 and strengthened 0 clauses in 43201 steps
c [elim-16] fully completed in 3 rounds
c [elim-16] transition to [ all 0 rem 0 ] state
c [elim-16] eliminated 1612 = 5% variables out of 35232 scheduled
c [bca-16] limit of 10000000 steps and 385486 added (scaled 2)
c [bca-16] 49983 out of 67242 literals actually usable 74%
c [bca-16] added 10 blocked clauses in 150613 steps
c [sweep-16] limit 29130654 penalty 0 = 0 + 0
c [sweep-16-1] 63 pos 7.6% + 771 neg 92.4% = 834 sched 2.5% ret 32786
c [sweep-16-1] 11696115 steps 608 queries 15.91 avg class size
c [sweep-16-1] 3094 decisions 521 SAT calls 50.84 avg env size
c [sweep-16-1] fully completed sweeping round
c [decomp-50] removed 136 variables
c [sweep-16-1] removed 136 vars (0 failed, 86 eqs, 153 impls)
c [sweep-16-2] 3191 pos 9.5% + 30293 neg 90.5% = 33484 sched 100.0% ret 0
c [sweep-16-2] 17469236 steps 320 queries 689.18 avg class size
c [sweep-16-2] 7190 decisions 311 SAT calls 153.71 avg env size
c [sweep-16-2] 24924 variables remain 74% (8533 retained 26%)
c [decomp-51] removed 47 variables
c [sweep-16-2] removed 47 vars (0 failed, 14 eqs, 26 impls)
c [sweep-16] removed 183 vars in TOTAL (2 rounds, 926 queries)
c [sort-queue-20] sorted 8682 enqueued variables after 340101 conflicts
c [score-dist-20] active 24755 (74%), one 2818 (8%), zero 5864 (18%)
c [score-dist-20] max exp 510, different 403 (79%)
c [score-dist-20] median active exp 502, avg 439.3
c [simplification-20] removed 3222 variables 8.8% (33437 remain 13%)
c [simplification-20] removed 12185 irredundant clauses 6.0% (191564 remain 17%)
c [simplification-20] maximum reduction of 9% = max (9%, 6%)
c [simplification-20] large reduction 9% >= 5% limit
c [simplification-20] next conflict interval 3401 = min (340101/100, 64998)
c [simplification-20] penalized conflict interval 3401 = 1 * 3401
c [simplification-20] hard conflict limit 353502 (soft 343502 + delta 10000)
c [simplification-20] new conflict limit 343502 (hard 353502)
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  683.4   33436   191564    341430   43886   6508 467422   54    78   86  69%    210  -29   26   70   38%
c 
c [simplification-21] limit 343502 conflicts (hard 353502) hit after 353502 conflicts
c [quatres-17] found 14149 quaternary clauses 44% in total
c [quatres-17-1] removed 2 duplicate quaternary clauses
c [quatres-17-2] added 5 quaternary resolvents
c [ternres-17] limit 99563681 with penalty 0 = 0 + 0
c [ternres-17] all 33428 free variables schedulable
c [ternres-17] 766 ternary resolvents (9 bin, 757 trn)
c [ternres-17] fully completed ternary resolution
c [card-6] limit 3111365 penalty 4 = 4 + 0
c [card-6] found 3646 at-most-one constraints of average size 4.0
c [card-6] no at-most-two constraint found
c [card-6] using previous limit 3111365 for elimination
c [card-6] 3646 out of 3646 constraints (100%) meet size limits
c [card-6] no units found
c [card-6] no at-most-one constraints generated
c [gauss-7] limit 1244546 penalty 4 = 4 + 0
c [gauss-7] extracted 38 xors of average arity 3.0
c [gauss-7] connected 114 occurrences of 105 variables (average 1.1)
c [gauss-7] limit 1244546 penalty 4 = 4 + 0
c [gauss-7] fully completed
c [gauss-7] exported 0 unary, 0 binary and 0 ternary equations
c [simpleprobe-6] all 33428 free variables schedulable
c [simpleprobe-6] limit 200000000 penalty 0 = 0 + 0
c [decomp-53] removed 68 variables
c [simpleprobe-6] fully completed simple probing
c [simpleprobe-6] removed 68 variables, found 132173 hbrs, 23 units
c [unhide-21] limit 9956368 with penalty 1 = 0 + 1
c [unhide-21-48] 1 units, 12 failed, 144382 tauts, 0 hbrs, 319993 literals
c [transred-17] limit 2000000 with penalty 0 = 0 + 0
c [transred-17] removed 285 transitive binary clauses
c [cce-9] limit of 248909202 steps penalty 1 = 1 + 0
c [cce-9-1] eliminated 2 clauses out of 2 (100%) of length 211
c [cce-9-1] eliminated 1 clauses out of 2 (50%) of length 210
c [cce-9-1] eliminated 1 clauses out of 2 (50%) of length 209
c [cce-9-1] eliminated 2 clauses out of 2 (100%) of length 208
c [cce-9-1] eliminated 2 clauses out of 3 (67%) of length 137
c [cce-9-1] eliminated 1 clauses out of 3 (33%) of length 136
c [cce-9-1] eliminated 1 clauses out of 3 (33%) of length 135
c [cce-9-1] eliminated 1 clauses out of 3 (33%) of length 134
c [cce-9-1] eliminated 1 clauses out of 2 (50%) of length 133
c [cce-9-1] eliminated 1 clauses out of 4 (25%) of length 132
c [cce-9-1] eliminated 1 clauses out of 3 (33%) of length 131
c [cce-9-1] eliminated 1 clauses out of 3 (33%) of length 130
c [cce-9-1] eliminated 1 clauses out of 3 (33%) of length 129
c [cce-9-1] eliminated 1 clauses out of 3 (33%) of length 128
c [cce-9-1] eliminated 1 clauses out of 2 (50%) of length 127
c [cce-9-1] eliminated 1 clauses out of 3 (33%) of length 126
c [cce-9-1] eliminated 1 clauses out of 4 (25%) of length 125
c [cce-9-1] eliminated 1 clauses out of 3 (33%) of length 124
c [cce-9-1] eliminated 1 clauses out of 4 (25%) of length 123
c [cce-9-1] eliminated 1 clauses out of 3 (33%) of length 122
c [cce-9-1] eliminated 1 clauses out of 4 (25%) of length 121
c [cce-9-1] eliminated 1 clauses out of 3 (33%) of length 120
c [cce-9-1] eliminated 1 clauses out of 4 (25%) of length 119
c [cce-9-1] eliminated 1 clauses out of 3 (33%) of length 118
c [cce-9-1] eliminated 1 clauses out of 3 (33%) of length 117
c [cce-9-1] eliminated 2 clauses out of 3 (67%) of length 116
c [cce-9-1] eliminated 1 clauses out of 3 (33%) of length 115
c [cce-9-1] eliminated 2 clauses out of 3 (67%) of length 114
c [cce-9-1] eliminated 1 clauses out of 4 (25%) of length 113
c [cce-9-1] eliminated 1 clauses out of 3 (33%) of length 112
c [cce-9-1] eliminated 1 clauses out of 4 (25%) of length 111
c [cce-9-1] eliminated 2 clauses out of 4 (50%) of length 110
c [cce-9-1] eliminated 1 clauses out of 3 (33%) of length 109
c [cce-9-1] eliminated 2 clauses out of 4 (50%) of length 108
c [cce-9-1] eliminated 1 clauses out of 2 (50%) of length 107
c [cce-9-1] eliminated 1 clauses out of 3 (33%) of length 106
c [cce-9-1] eliminated 1 clauses out of 3 (33%) of length 105
c [cce-9-1] eliminated 1 clauses out of 2 (50%) of length 104
c [cce-9-1] eliminated 1 clauses out of 4 (25%) of length 103
c [cce-9-1] eliminated 1 clauses out of 3 (33%) of length 102
c [cce-9-1] eliminated 1 clauses out of 4 (25%) of length 101
c [cce-9-1] eliminated 1 clauses out of 4 (25%) of length 100
c [cce-9-1] eliminated 2 clauses out of 3 (67%) of length 99
c [cce-9-1] eliminated 1 clauses out of 4 (25%) of length 98
c [cce-9-1] eliminated 1 clauses out of 4 (25%) of length 97
c [cce-9-1] eliminated 1 clauses out of 5 (20%) of length 96
c [cce-9-1] eliminated 1 clauses out of 3 (33%) of length 95
c [cce-9-1] eliminated 1 clauses out of 4 (25%) of length 94
c [cce-9-1] eliminated 1 clauses out of 4 (25%) of length 93
c [cce-9-1] eliminated 1 clauses out of 3 (33%) of length 92
c [cce-9-1] eliminated 1 clauses out of 4 (25%) of length 91
c [cce-9-1] eliminated 1 clauses out of 3 (33%) of length 90
c [cce-9-1] eliminated 1 clauses out of 4 (25%) of length 89
c [cce-9-1] eliminated 1 clauses out of 4 (25%) of length 88
c [cce-9-1] eliminated 1 clauses out of 4 (25%) of length 87
c [cce-9-1] eliminated 1 clauses out of 3 (33%) of length 86
c [cce-9-1] eliminated 1 clauses out of 4 (25%) of length 85
c [cce-9-1] eliminated 1 clauses out of 4 (25%) of length 84
c [cce-9-1] eliminated 1 clauses out of 3 (33%) of length 83
c [cce-9-1] eliminated 1 clauses out of 3 (33%) of length 82
c [cce-9-1] eliminated 1 clauses out of 4 (25%) of length 81
c [cce-9-1] eliminated 1 clauses out of 3 (33%) of length 80
c [cce-9-1] eliminated 2 clauses out of 4 (50%) of length 79
c [cce-9-1] eliminated 1 clauses out of 3 (33%) of length 78
c [cce-9-1] eliminated 1 clauses out of 3 (33%) of length 76
c [cce-9-1] eliminated 2 clauses out of 4 (50%) of length 75
c [cce-9-1] eliminated 1 clauses out of 3 (33%) of length 74
c [cce-9-1] eliminated 1 clauses out of 3 (33%) of length 73
c [cce-9-1] eliminated 1 clauses out of 3 (33%) of length 72
c [cce-9-1] eliminated 1 clauses out of 4 (25%) of length 70
c [cce-9-1] eliminated 1 clauses out of 3 (33%) of length 69
c [cce-9-1] eliminated 1 clauses out of 2 (50%) of length 68
c [cce-9-1] eliminated 1 clauses out of 4 (25%) of length 67
c [cce-9-1] eliminated 1 clauses out of 3 (33%) of length 66
c [cce-9-1] eliminated 1 clauses out of 4 (25%) of length 65
c [cce-9-1] eliminated 1 clauses out of 3 (33%) of length 64
c [cce-9-1] eliminated 1 clauses out of 4 (25%) of length 63
c [cce-9-1] eliminated 1 clauses out of 4 (25%) of length 62
c [cce-9-1] eliminated 1 clauses out of 4 (25%) of length 61
c [cce-9-1] eliminated 1 clauses out of 4 (25%) of length 60
c [cce-9-1] eliminated 1 clauses out of 5 (20%) of length 59
c [cce-9-1] eliminated 1 clauses out of 4 (25%) of length 58
c [cce-9-1] eliminated 1 clauses out of 4 (25%) of length 57
c [cce-9-1] eliminated 1 clauses out of 4 (25%) of length 56
c [cce-9-1] eliminated 1 clauses out of 3 (33%) of length 55
c [cce-9-1] eliminated 1 clauses out of 4 (25%) of length 54
c [cce-9-1] eliminated 2 clauses out of 3 (67%) of length 53
c [cce-9-1] eliminated 1 clauses out of 5 (20%) of length 52
c [cce-9-1] eliminated 3 clauses out of 6 (50%) of length 51
c [cce-9-1] eliminated 1 clauses out of 4 (25%) of length 50
c [cce-9-1] eliminated 1 clauses out of 3 (33%) of length 49
c [cce-9-1] eliminated 1 clauses out of 5 (20%) of length 48
c [cce-9-1] eliminated 1 clauses out of 5 (20%) of length 47
c [cce-9-1] eliminated 1 clauses out of 5 (20%) of length 46
c [cce-9-1] eliminated 1 clauses out of 4 (25%) of length 45
c [cce-9-1] eliminated 1 clauses out of 7 (14%) of length 44
c [cce-9-1] eliminated 1 clauses out of 4 (25%) of length 43
c [cce-9-1] eliminated 1 clauses out of 4 (25%) of length 42
c [cce-9-1] eliminated 1 clauses out of 6 (17%) of length 41
c [cce-9-1] eliminated 1 clauses out of 2 (50%) of length 40
c [cce-9-1] eliminated 1 clauses out of 5 (20%) of length 39
c [cce-9-1] eliminated 2 clauses out of 3 (67%) of length 38
c [cce-9-1] eliminated 1 clauses out of 7 (14%) of length 37
c [cce-9-1] eliminated 1 clauses out of 4 (25%) of length 36
c [cce-9-1] eliminated 3 clauses out of 8 (38%) of length 35
c [cce-9-1] eliminated 3 clauses out of 6 (50%) of length 34
c [cce-9-1] eliminated 2 clauses out of 10 (20%) of length 33
c [cce-9-1] eliminated 4 clauses out of 7 (57%) of length 32
c [cce-9-1] eliminated 5 clauses out of 11 (45%) of length 31
c [cce-9-1] eliminated 7 clauses out of 13 (54%) of length 30
c [cce-9-1] eliminated 6 clauses out of 14 (43%) of length 29
c [cce-9-1] eliminated 5 clauses out of 11 (45%) of length 28
c [cce-9-1] eliminated 6 clauses out of 14 (43%) of length 27
c [cce-9-1] eliminated 3 clauses out of 9 (33%) of length 26
c [cce-9-1] eliminated 3 clauses out of 12 (25%) of length 25
c [cce-9-1] eliminated 5 clauses out of 10 (50%) of length 24
c [cce-9-1] eliminated 3 clauses out of 10 (30%) of length 23
c [cce-9-1] eliminated 2 clauses out of 12 (17%) of length 22
c [cce-9-1] eliminated 5 clauses out of 13 (38%) of length 21
c [cce-9-1] eliminated 8 clauses out of 21 (38%) of length 20
c [cce-9-1] eliminated 9 clauses out of 16 (56%) of length 19
c [cce-9-1] eliminated 9 clauses out of 19 (47%) of length 18
c [cce-9-1] eliminated 8 clauses out of 19 (42%) of length 17
c [cce-9-1] eliminated 10 clauses out of 21 (48%) of length 16
c [cce-9-1] eliminated 8 clauses out of 18 (44%) of length 15
c [cce-9-1] eliminated 11 clauses out of 24 (46%) of length 14
c [cce-9-1] eliminated 10 clauses out of 21 (48%) of length 13
c [cce-9-1] eliminated 13 clauses out of 23 (57%) of length 12
c [cce-9-1] eliminated 10 clauses out of 30 (33%) of length 11
c [cce-9-1] eliminated 14 clauses out of 30 (47%) of length 10
c [cce-9-1] eliminated 13 clauses out of 37 (35%) of length 9
c [cce-9-1] eliminated 13 clauses out of 44 (30%) of length 8
c [cce-9-1] eliminated 20 clauses out of 108 (19%) of length 7
c [cce-9-1] eliminated 26 clauses out of 2938 (1%) of length 6
c [cce-9-1] eliminated 74 clauses out of 8585 (1%) of length 5
c [cce-9-1] eliminated 5 clauses out of 12880 (0%) of length 4
c [cce-9-1] incomplete large round (ACCE)
c [cce-9-1] eliminated 441 large clauses in 248909205 steps
c [cce-9-1] allowing another 124454602 steps for small clauses
c [cce-9-1] scheduling 134959 clauses = 115017 binary + 19942 ternary
c [cce-9-1] tried to eliminate 6735 small clauses 5%
c [cce-9-1] eliminated 807 binary clauses 1%
c [cce-9-1] eliminated 194 ternary clauses 1%
c [cce-9-1] eliminated 1001 small clauses 1%
c [cce-9-1] eliminated 1027 small clauses in 248909205 steps
c [cce-9-1] incomplete small round (ACCE)
c [cce-9-1] eliminated 1468 covered clauses in round 1
c [cce-9] eliminated 1468 covered clauses in TOTAL during 1 rounds
c [cce-9] 1468 < 1/100 * 189950 = 1899 considered unsuccessful
c [elim-17] scheduling all variables this time
c [elim-17] scheduled 33352 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 314 variables 1% in round 1 in 17694469 steps
c [elim-17-1] backward subsumption/strengthening limit 17694400
c [elim-17-1-1] backward checking 2075 touched variables 6%
c [elim-17-1-1] fully completed backward checking in 1 rounds
c [elim-17-1] subsumed 4 and strengthened 9 clauses in 415112 steps
c [elim-17-1] rescheduled 28 variables 0% by backward subsumption
c [elim-17-2] eliminated 2 variables 0% in round 2 in 14374 steps
c [elim-17-2] backward subsumption/strengthening limit 14300
c [elim-17-2-1] backward checking 20 touched variables 0%
c [elim-17-2-1] incomplete backward checking 0 remain 0%
c [elim-17-2] subsumed 0 and strengthened 0 clauses in 14301 steps
c [elim-17-2] fully rescheduled 33036 variables 99%
c [elim-17-3] eliminated 14 variables 0% in round 3 in 17672138 steps
c [elim-17-3] backward subsumption/strengthening limit 17672100
c [elim-17-3-1] backward checking 144 touched variables 0%
c [elim-17-3-1] fully completed backward checking in 1 rounds
c [elim-17-3] subsumed 0 and strengthened 3 clauses in 65662 steps
c [elim-17] incomplete 6 not tried 0% in round 3
c [elim-17] transition to [ all 1 rem 1 ] state
c [elim-17] eliminated 330 = 1% variables out of 33352 scheduled
c [elim-17] 330 < 1/100 * 33352 = 333 considered unsuccessful
c [bca-17] limit of 10000000 steps and 377517 added (scaled 2)
c [bca-17] 48231 out of 66046 literals actually usable 73%
c [bca-17] added 14 blocked clauses in 155913 steps
c [sweep-17] limit 29869104 penalty 0 = 0 + 0
c [sweep-17-1] 2678 pos 10.9% + 21994 neg 89.1% = 24672 sched 74.7% ret 8350
c [sweep-17-1] 29874620 steps 492 queries 432.29 avg class size
c [sweep-17-1] 10286 decisions 471 SAT calls 178.56 avg env size
c [sweep-17-1] 18772 variables remain 57% (14240 retained 43%)
c [decomp-54] removed 34 variables
c [sweep-17-1] removed 34 vars (0 failed, 26 eqs, 48 impls)
c [sweep-17] removed 34 vars in TOTAL (1 rounds, 491 queries)
c [sort-queue-21] sorted 8137 enqueued variables after 353502 conflicts
c [score-dist-21] active 24851 (75%), one 2578 (8%), zero 5559 (17%)
c [score-dist-21] max exp 510, different 412 (81%)
c [score-dist-21] median active exp 502, avg 449.8
c [simplification-21] removed 440 variables 1.3% (32988 remain 13%)
c [simplification-21] removed 3551 irredundant clauses 1.9% (188013 remain 16%)
c [simplification-21] maximum reduction of 2% = max (1%, 2%)
c [simplification-21] geometric conflict interval increment 21666 = 64998 / 3
c [simplification-21] new conflict interval 86664
c [simplification-21] penalized conflict interval 86664 = 1 * 86664
c [simplification-21] hard conflict limit 483498 (soft 440166 + delta 43332)
c [simplification-21] new conflict limit 440166 (hard 483498)
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 -  725.0   32988   188013    367721   31117   7025 438283  144   209   52  69%    228   99  120   78  154%
c i  763.6   32987   188013    410894   61767   7135 438377   59    83   96  71%    612  -24   46   74   62%
c -  765.8   32984   188013    413298   32976   7148 438395  104   168   53  62%   -331   61  244   76  319%
c 
c [simplification-22] limit 440166 conflicts (hard 483498) hit after 454357 conflicts
c [quatres-18] found 14188 quaternary clauses 42% in total
c [quatres-18-2] added 3 single-self-subsuming ternary resolvents
c [quatres-18-2] added 3 quaternary resolvents
c [ternres-18] limit 122315811 with penalty 0 = 0 + 0
c [ternres-18] all 32984 free variables schedulable
c [ternres-18] 225 ternary resolvents (5 bin, 220 trn)
c [ternres-18] fully completed ternary resolution
c [decomp-55] removed 4 variables
c [treelook-6] limit 6115790 penalty 1 = 1 + 0 boost 1
c [treelook-6] scheduled 36222 literals 55%
c [treelook-6] scheduling used 730167 steps
c [treelook-6] scheduled completely
c [treelook-6] limit 6115790 penalty 1 = 1 + 0 boost 1
c [treelook-6] used 6115799 steps
c [treelook-6] 36128 literals remain 55%
c [treelook-6] 4878 variables remain to probed next time 15%
c [decomp-56] removed 4 variables
c [treelook-6] removed 10 variables, found 33120 hbrs
c [unhide-22] limit 10000000 with penalty 1 = 0 + 1
c [unhide-22-53] 0 units, 8 failed, 82510 tauts, 0 hbrs, 405207 literals
c [transred-18] limit 2000000 with penalty 0 = 0 + 0
c [transred-18] removed 204 transitive binary clauses
c [bca-18] limit of 10000000 steps and 375346 added (scaled 2)
c [bca-18] 47505 out of 65916 literals actually usable 72%
c [bca-18] added 8 blocked clauses in 163332 steps
c [sweep-18] almost no limit of 4000000000 steps
c [sweep-18-1] 2546 pos 13.6% + 16223 neg 86.4% = 18769 sched 56.9% ret 14188
c [sweep-18-1] 171184238 steps 4215 queries 40.19 avg class size
c [sweep-18-1] 39493 decisions 3965 SAT calls 78.17 avg env size
c [sweep-18-1] fully completed sweeping round
c [decomp-57] removed 324 variables
c [sweep-18-1] removed 324 vars (0 failed, 260 eqs, 753 impls)
c [sweep-18-2] 3282 pos 10.1% + 29351 neg 89.9% = 32633 sched 100.0% ret 0
c [sweep-18-2] 197248515 steps 4511 queries 38.73 avg class size
c [sweep-18-2] 52231 decisions 4337 SAT calls 97.01 avg env size
c [sweep-18-2] fully completed sweeping round
c [decomp-58] removed 220 variables
c [sweep-18-2] removed 220 vars (0 failed, 188 eqs, 566 impls)
c [sweep-18-3] 3279 pos 10.1% + 29134 neg 89.9% = 32413 sched 100.0% ret 0
c [sweep-18-3] 196246724 steps 4499 queries 53.71 avg class size
c [sweep-18-3] 49406 decisions 4374 SAT calls 90.30 avg env size
c [sweep-18-3] fully completed sweeping round
c [decomp-59] removed 261 variables
c [sweep-18-3] removed 261 vars (0 failed, 132 eqs, 425 impls)
c [sweep-18] removed 805 vars in TOTAL (3 rounds, 13222 queries)
c [sort-queue-22] sorted 6223 enqueued variables after 454357 conflicts
c [score-dist-22] active 25929 (81%), one 1409 (4%), zero 4814 (15%)
c [score-dist-22] max exp 512, different 352 (69%)
c [score-dist-22] median active exp 504, avg 480.5
c [simplification-22] removed 832 variables 2.5% (32152 remain 12%)
c [simplification-22] removed 3823 irredundant clauses 2.0% (184190 remain 16%)
c [simplification-22] maximum reduction of 3% = max (3%, 2%)
c [simplification-22] geometric conflict interval increment 21666 = 86664 / 4
c [simplification-22] new conflict interval 108330
c [simplification-22] penalized conflict interval 108330 = 1 * 108330
c [simplification-22] hard conflict limit 616852 (soft 562687 + delta 54165)
c [simplification-22] new conflict limit 562687 (hard 616852)
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 -  838.1   32152   184190    458937   35245   7200 431027   85   118   52  72%    296    6  143   79  180%
c -  871.4   32152   184190    499981   36895   7264 431086   63    91   53  70%    635  -16   64   75   86%
c -  902.1   32152   184190    537955   38056   7313 431139   51    71   53  71%    806  -26   47   66   71%
c -  934.6   32152   184190    576184   38949   7374 431163   24    32   53  73%    902  -45   17   52   33%
c 
c [simplification-23] limit 562687 conflicts (hard 616852) hit after 591014 conflicts
c [quatres-19] found 14115 quaternary clauses 39% in total
c [quatres-19-1] added 1 double-self-subsuming ternary resolvents
c [quatres-19-2] added 17 single-self-subsuming ternary resolvents
c [quatres-19-2] added 5 quaternary resolvents
c [ternres-19] limit 150172412 with penalty 0 = 0 + 0
c [ternres-19] all 32152 free variables schedulable
c [ternres-19] 435 ternary resolvents (9 bin, 426 trn)
c [ternres-19] fully completed ternary resolution
c [decomp-60] removed 2 variables
c [basicprobe-6] limit 400000000 penalty 0 = 0 + 0
c [basicprobe-6-0] 8169 sched 26%, 308 failed, 20 lifted, 33093 hbrs
c [decomp-61] removed 624 variables
c [basicprobe-6-1] 2481 probes remain 8% after last round
c [basicprobe-6-1] 473 units = 450 failed (95%) + 23 lifted (5%)
c [basicprobe-6-1] removed 839 variables, found 51512 hbrs
c [bate-5] eliminated 138 asymmetric tautologies during probing
c [unhide-23] limit 10000000 with penalty 1 = 0 + 1
c [unhide-23-58] 1 units, 13 failed, 104553 tauts, 0 hbrs, 291132 literals
c [transred-19] limit 2000000 with penalty 0 = 0 + 0
c [transred-19] removed 281 transitive binary clauses
c [elim-18] no untried remaining variables left
c [elim-18] scheduled 31286 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 652 variables 2% in round 1 in 16446906 steps
c [elim-18-1] backward subsumption/strengthening limit 16446900
c [elim-18-1-1] backward checking 2945 touched variables 9%
c [elim-18-1-1] fully completed backward checking in 1 rounds
c [elim-18-1] subsumed 26 and strengthened 7 clauses in 437037 steps
c [elim-18-1] rescheduled 99 variables 0% by backward subsumption
c [elim-18-2] eliminated 5 variables 0% in round 2 in 41199 steps
c [elim-18-2] backward subsumption/strengthening limit 41100
c [elim-18-2-1] backward checking 35 touched variables 0%
c [elim-18-2-1] fully completed backward checking in 1 rounds
c [elim-18-2] subsumed 0 and strengthened 7 clauses in 34436 steps
c [elim-18-2] rescheduled 12 variables 0% by backward subsumption
c [elim-18-3] no variable eliminated in round 3 in 6694 steps
c [elim-18] fully completed in 3 rounds
c [elim-18] transition to [ all 0 rem 0 ] state
c [elim-18] eliminated 657 = 2% variables out of 31286 scheduled
c [bca-19] limit of 10000000 steps and 350514 added (scaled 2)
c [bca-19] 41432 out of 61260 literals actually usable 68%
c [bca-19] added 10 blocked clauses in 134148 steps
c [sweep-19] limit 45051723 penalty 0 = 0 + 0
c [sweep-19-1] 3168 pos 10.3% + 27461 neg 89.7% = 30629 sched 100.0% ret 0
c [sweep-19-1] 45250031 steps 931 queries 153.19 avg class size
c [sweep-19-1] 18281 decisions 922 SAT calls 135.00 avg env size
c [sweep-19-1] 14474 variables remain 48% (15953 retained 52%)
c [decomp-62] removed 220 variables
c [sweep-19-1] removed 220 vars (0 failed, 13 eqs, 63 impls)
c [sweep-19] removed 220 vars in TOTAL (1 rounds, 930 queries)
c [sort-queue-23] sorted 9286 enqueued variables after 591014 conflicts
c [score-dist-23] active 21123 (69%), one 5755 (19%), zero 3531 (12%)
c [score-dist-23] max exp 510, different 380 (74%)
c [score-dist-23] median active exp 502, avg 464.0
c [simplification-23] removed 1743 variables 5.4% (30409 remain 12%)
c [simplification-23] removed 10288 irredundant clauses 5.6% (173902 remain 15%)
c [simplification-23] maximum reduction of 6% = max (5%, 6%)
c [simplification-23] large reduction 6% >= 5% limit
c [simplification-23] next conflict interval 5910 = min (591014/100, 108330)
c [simplification-23] penalized conflict interval 5910 = 1 * 5910
c [simplification-23] hard conflict limit 606924 (soft 596924 + delta 10000)
c [simplification-23] new conflict limit 596924 (hard 606924)
c 
c [simplification-24] limit 596924 conflicts (hard 606924) hit after 606925 conflicts
c [quatres-20] found 13598 quaternary clauses 38% in total
c [quatres-20-1] removed 1 duplicate quaternary clauses
c [quatres-20-2] added 3 single-self-subsuming ternary resolvents
c [quatres-20-2] added 5 quaternary resolvents
c [ternres-20] limit 152867848 with penalty 0 = 0 + 0
c [ternres-20] all 30409 free variables schedulable
c [ternres-20] 302 ternary resolvents (2 bin, 300 trn)
c [ternres-20] fully completed ternary resolution
c [simpleprobe-7] all 30409 free variables schedulable
c [simpleprobe-7] limit 200000000 penalty 0 = 0 + 0
c [decomp-64] removed 25 variables
c [simpleprobe-7] fully completed simple probing
c [simpleprobe-7] removed 25 variables, found 56426 hbrs, 10 units
c [unhide-24] limit 10000000 with penalty 1 = 0 + 1
c [unhide-24-63] 1 units, 6 failed, 88840 tauts, 0 hbrs, 227734 literals
c [transred-20] limit 2000000 with penalty 0 = 0 + 0
c [transred-20] removed 289 transitive binary clauses
c [cce-10] limit of 191084810 steps penalty 2 = 2 + 0
c [cce-10-1] eliminated 1 clauses out of 5 (20%) of length 37
c [cce-10-1] eliminated 2 clauses out of 7 (29%) of length 36
c [cce-10-1] eliminated 1 clauses out of 4 (25%) of length 35
c [cce-10-1] eliminated 1 clauses out of 7 (14%) of length 34
c [cce-10-1] eliminated 2 clauses out of 7 (29%) of length 33
c [cce-10-1] eliminated 1 clauses out of 6 (17%) of length 32
c [cce-10-1] eliminated 2 clauses out of 6 (33%) of length 31
c [cce-10-1] eliminated 1 clauses out of 8 (12%) of length 30
c [cce-10-1] eliminated 1 clauses out of 5 (20%) of length 29
c [cce-10-1] eliminated 1 clauses out of 9 (11%) of length 28
c [cce-10-1] eliminated 1 clauses out of 6 (17%) of length 27
c [cce-10-1] eliminated 1 clauses out of 8 (12%) of length 26
c [cce-10-1] eliminated 1 clauses out of 9 (11%) of length 25
c [cce-10-1] eliminated 1 clauses out of 7 (14%) of length 24
c [cce-10-1] eliminated 1 clauses out of 9 (11%) of length 23
c [cce-10-1] eliminated 1 clauses out of 10 (10%) of length 22
c [cce-10-1] eliminated 2 clauses out of 14 (14%) of length 21
c [cce-10-1] eliminated 1 clauses out of 11 (9%) of length 20
c [cce-10-1] eliminated 2 clauses out of 12 (17%) of length 19
c [cce-10-1] eliminated 2 clauses out of 11 (18%) of length 18
c [cce-10-1] eliminated 2 clauses out of 11 (18%) of length 17
c [cce-10-1] eliminated 3 clauses out of 18 (17%) of length 16
c [cce-10-1] eliminated 3 clauses out of 17 (18%) of length 15
c [cce-10-1] eliminated 1 clauses out of 18 (6%) of length 14
c [cce-10-1] eliminated 4 clauses out of 19 (21%) of length 13
c [cce-10-1] eliminated 3 clauses out of 19 (16%) of length 12
c [cce-10-1] eliminated 3 clauses out of 17 (18%) of length 11
c [cce-10-1] eliminated 4 clauses out of 36 (11%) of length 10
c [cce-10-1] eliminated 8 clauses out of 36 (22%) of length 9
c [cce-10-1] eliminated 8 clauses out of 39 (21%) of length 8
c [cce-10-1] eliminated 12 clauses out of 100 (12%) of length 7
c [cce-10-1] eliminated 20 clauses out of 2973 (1%) of length 6
c [cce-10-1] eliminated 29 clauses out of 8338 (0%) of length 5
c [cce-10-1] eliminated 8 clauses out of 11876 (0%) of length 4
c [cce-10-1] incomplete large round (ATE)
c [cce-10-1] eliminated 134 large clauses in 191084812 steps
c [cce-10-1] allowing another 95542406 steps for small clauses
c [cce-10-1] scheduling 133118 clauses = 109207 binary + 23911 ternary
c [cce-10-1] tried to eliminate 5813 small clauses 4%
c [cce-10-1] eliminated 572 binary clauses 1%
c [cce-10-1] eliminated 155 ternary clauses 1%
c [cce-10-1] eliminated 727 small clauses 1%
c [cce-10-1] eliminated 736 small clauses in 191084812 steps
c [cce-10-1] incomplete small round (ATE)
c [cce-10-1] eliminated 870 covered clauses in round 1
c [cce-10] eliminated 870 covered clauses in TOTAL during 1 rounds
c [cce-10] 870 < 1/100 * 173183 = 1731 considered unsuccessful
c [elim-19] scheduling all variables this time
c [elim-19] scheduled 30379 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 240 variables 1% in round 1 in 16203598 steps
c [elim-19-1] backward subsumption/strengthening limit 16203500
c [elim-19-1-1] backward checking 1549 touched variables 5%
c [elim-19-1-1] fully completed backward checking in 1 rounds
c [elim-19-1] subsumed 1 and strengthened 6 clauses in 318847 steps
c [elim-19-1] rescheduled 18 variables 0% by backward subsumption
c [elim-19-2] eliminated 1 variables 0% in round 2 in 6572 steps
c [elim-19-2] backward subsumption/strengthening limit 6500
c [elim-19-2-1] backward checking 10 touched variables 0%
c [elim-19-2-1] incomplete backward checking 0 remain 0%
c [elim-19-2] subsumed 0 and strengthened 0 clauses in 6501 steps
c [elim-19-2] fully rescheduled 30138 variables 99%
c [elim-19-3] eliminated 9 variables 0% in round 3 in 16218629 steps
c [elim-19-3] backward subsumption/strengthening limit 16218600
c [elim-19-3-1] backward checking 73 touched variables 0%
c [elim-19-3-1] fully completed backward checking in 1 rounds
c [elim-19-3] subsumed 0 and strengthened 0 clauses in 62787 steps
c [elim-19] fully completed in 3 rounds
c [elim-19] transition to [ all 0 rem 0 ] state
c [elim-19] eliminated 250 = 1% variables out of 30379 scheduled
c [elim-19] 250 < 1/100 * 30379 = 303 considered unsuccessful
c [bca-20] limit of 10000000 steps and 345421 added (scaled 2)
c [bca-20] 40300 out of 60260 literals actually usable 67%
c [bca-20] added 9 blocked clauses in 142403 steps
c [sweep-20] limit 45860354 penalty 0 = 0 + 0
c [sweep-20-1] 1837 pos 12.8% + 12503 neg 87.2% = 14340 sched 47.6% ret 15789
c [sweep-20-1] 45865904 steps 1037 queries 91.97 avg class size
c [sweep-20-1] 15802 decisions 1011 SAT calls 109.54 avg env size
c [sweep-20-1] 8192 variables remain 27% (21936 retained 73%)
c [decomp-65] removed 28 variables
c [sweep-20-1] removed 28 vars (0 failed, 30 eqs, 75 impls)
c [sweep-20] 28 < 1/1000 * 30129 = 30 considered unsuccessful
c [sweep-20] removed 28 vars in TOTAL (1 rounds, 1036 queries)
c [sort-queue-24] sorted 8676 enqueued variables after 606925 conflicts
c [score-dist-24] active 21425 (71%), one 5286 (18%), zero 3390 (11%)
c [score-dist-24] max exp 511, different 369 (72%)
c [score-dist-24] median active exp 502, avg 464.9
c [simplification-24] removed 308 variables 1.0% (30101 remain 12%)
c [simplification-24] removed 1859 irredundant clauses 1.1% (172043 remain 15%)
c [simplification-24] maximum reduction of 1% = max (1%, 1%)
c [simplification-24] geometric conflict interval increment 54165 = 108330 / 2
c [simplification-24] new conflict interval 162495
c [simplification-24] penalized conflict interval 162495 = 1 * 162495
c [simplification-24] hard conflict limit 850667 (soft 769420 + delta 81247)
c [simplification-24] new conflict limit 769420 (hard 850667)
c
c CAUGHT SIGNAL 15 SIGTERM
c
c s UNKNOWN
c bate: 2169 basic ate = 2136 trn 98% + 33 lrg 2% in 5 updates
c bcas: 20 count, 1455 added (402 skipped), 5269861 steps
c bkwd: tried 695104 clauses, 1389651 lits, 2.00 lits/clause
c bkwd: checked 19865259 occs, 28.58 occs/clause, 14.30 occs/lit
c bkwd: subsumed 18 binary, 376 ternary, 54 large
c bkwd: strengthened 1 binary, 0 ternary (0% self), 637 large (0% self)
c blkd: 6 bces, 11092 removed, 8068523 resolutions, 22145888 steps
c blkd: 13398 blocking literals 2%, 20 pure
c bump: 618550 bumped seen, 461632167 lits 746.3 on average
c card: 6 count, 0 units, 0 am1, 231883482 steps
c card: 0 rescheduled, 0 eliminated, 0 resolved, 115160 subsumed
c card: 29028 at-most-one constraints found, average size 4.31
c card: 29028 at-most-one constraints used 100%, average size 4.31
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: 10 cces, 72059 eliminated, 71565 ate 99%, 494 abce 1%
c cces: 0 probed, 0 lifted, 0 failed
c cces: 0 cached, 0 rsz, 0 cols 0%, 0 srch, 0 hits 0%
c clls: 1 sat, 0 simp, 0 freeze, 0 melt
c clls: 3859783 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 208 gcs, 0 rescored clauses, 2381 rescored vars
c dcps: 65 decompositions, 15751 equivalent 6%
c deco: 107777 decision-only clauses 17%, 72% reduction
c decs: 5294552 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 19 elims, 127284 eliminated 47%, 162 pure 0%
c elms: 52 rounds, 2.7 rounds/bve
c elms: 107700 small 85%, 19402 large 15%
c elms: 460694 tried small, 107700 succeeded 23%, 352994 failed 77%
c elms: 46572 subsumed, 78824 strengthened, 1075 blocked
c elms: 25358855 copies, 24025471 resolutions, 19271873 ipos
c elms: 6446897 subchks, 6071316 strchks
c gaus: 7 extractions, 946 extracted, 2.3 size, 3 max
c gaus: exported 0 units, 3 binary and 0 ternary equations
c gaus: 0 gc, 28128336 steps, 14064168 extr 50%, 21335 elim 0%
c glue: 83.3 orig avg, 83.3 real avg, 7.4 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 1733497 = 502757 simple 29% + 1200683 trn 69% + 30057 lrg 2%, 5193 sub 0%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 618549 clauses, 294.0 length
c lrnd: 181824657 lits = 301630004 orig - 119805347 removed 40%
c lrnd: 286995 uips 46%, 289646 flips 47%
c mins: 487417 mins 81%, 2404 bin 0%, 6107 size 1%
c mins: 322312991 poisoned searches, 76194161 hits, 24% hit rate
c mins: 419144724 used twice searches, 19664083 hits, 5% hit rate
c move: moved 45080, 26970 bin 60%, 18110 trn 40%
c otfs: 2631 driving 35%, 4842 restarting 65%
c otfs: str 7473, 7342 red 98%, 131 irr 2%
c otfs: str 7473, 0 bin 0%, 102 trn 1%, 7371 lrg 99%
c otfs: sub 57, 57 red 100%, 0 irr 0%
c otfs: sub 57, 0 bin 0%, 0 trn 0%, 57 lrg 100%
c phas: 17 computed, 121664 set, 5 pos (0%), 121659 neg (100%)
c prbs: 6 basic, 91216 probed, 3142 failed, 178 lifted
c prbs: 7 simple, 1123022 probed, 1363 failed, 6617 eqs
c prbs: 6 treelook, 313 probed, 3 failed, 0 lifted
c prom: 51148 locked 3% out of 1663815 tried
c prps: 2619397447 props, 457 props/dec
c prps: 92% srch, 8% simp, 0% lkhd
c quat: 20 count, 188 quat, 82 self1, 1 self2, 1185 dup
c queu: 24 sorted, 5294552 next (66467 steps 0.01)
c queu: 534001664 enq (856687039 steps 1.60), 461634484 deq 86%
c redc: 2679 clauses 20%, 13153 tried 2%, 37 sat 0%
c redc: 6294 lits 5%, 132530 tried 0%, 37 sat 0%
c redc: 289 times jump level reduced, 44.3 levels on average
c reds: 11 count, 55653.8 conflicts per reduce
c reds: 0 memlim 0%, 11 arith 100%
c reds: 302568 collected 91%, 29601 retired 9%
c rmbd: 52308 removed, 18388 red 35%
c rsts: 9898 restarts 100%, 0 skipped 0%
c rsts: 0 saturating 0%, 0 reuse 0%
c rsts: 0 kept 0.0% average 0.0%
c scnc: 0 count, 1.000 min (0/1000), 1.000 max (0/1000)
c simp: 24 count, 22 confs 92%, 0 vars 0%
c simp: 1 its 4%, 1 bin 4%, 0 trns 0%
c subl: 618549 count (832203 tried 1.3), 127953 sub out of 612082 (20.9%)
c swps: 20 count, 23 rounds, 24714 queries (1074.5/round)
c swps: 22899 sat calls, 224 unsat (0.4% success rate)
c swps: 257244 decisions 11.2, 8989 conflicts 0.4
c swps; 210.8 avg class size, 90.9 avg environment size
c swps: 2 failed, 4221 impls, 1984 equivs
c swp0: 8229 type 0 queries, 4150 unsat (50.4%), 7648 sat (92.9%)
c swp1: 16485 type 1 queries, 9274 unsat (56.3%), 15082 sat (91.5%)
c sync: 0 produced units, 0 successful consumptions 0%
c sync: 0 consume units calls, 0 tried 0%, 0 success 0%
c sync: 0 produced clauses, 0 successful consumptions 0%
c sync: 0 consume clause calls, 0 tried 0%, 0 success 0%
c time: 11831805 calls to obtain time
c tops: 95122 fixed 35%, 368 its, 1663.57 confs/it
c trds: 20 transitive reductions, 3753 removed, 27 failed
c trds: 24371 nodes, 70503 edges, 40047005 steps
c trim: 3148204 words, 12.0 MB
c trnr: 20 count, 71 bin, 14117 trn, 121040148 steps
c unhd: 24 count, 63 rounds, 157123598 steps
c unhd: 3670 non-trivial sccs of average size 2.1
c unhd: 125 units, 124 bin, 1 trn, 0 lrg
c unhd: 8110 failed, 8028 stamp, 0 lits, 47 bin, 20 trn, 0 lrg
c unhd: 1000902 tauts, 10540 bin 1%, 22534 trn 2%, 733 lrg 0%
c unhd: 1000902 tauts, 967095 stamp 97%, 938577 red 94%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 12295581 str, 124 bin 0%, 11055 trn 0%, 12284402 lrg 100%, 12243379 red 100%
c vars: 30101 remaining 11% and 238157 removed 89% out of 268258
c vars: 95122 fixed 35%, 127284 eliminated 47%, 15751 equivalent 6%
c vsts: 17206867587 visits, 89% srch, 11% simp, 0% lkhd
c vsts: 6.4 search visits per propagation, 25117.7 per conflict
c wchs: 1558696608 pushed, 70336612 enlarged, 297 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all         612270        302568         29601      40050718       7941699        272816
c 
c  0 0         16713   3       684   0         0   0  16449073  41   2326276  29     48647  18     1.7
c  1 5          5379   1       940   0       815   3   2904812   7    467340   6     15505   6     0.7
c  2 6         18090   3      6204   2      1692   6   4369822  11    844106  11     28077  10     2.2
c  3 9         31966   5     15062   5      2143   7   3462528   9<   749241   9<    24818   9     3.9
c  4 14        39458   6     20353   7      2090   7   3252486   8    791602  10     24134   9     7.0
c  5 21        44700   7     24638   8      2368   8   2602746   6    656259   8     21530   8<    9.9
c  6 30        56725   9     32644  11      2769   9   2519790   6    605757   8     21945   8    10.5
c  7 41        64357  11     39316  13<     2838  10<  1619167   4    440294   6     19364   7    11.2
c  8 54        68525  11<    45342  15      2829  10   1141296   3    360872   5     18286   7    16.4
c  9 69        79546  13     52966  18      2927  10    637378   2    265511   3     16957   6    48.3
c 10 86        78192  13     40271  13      3447  12    595678   1    236885   3     16340   6    20.4
c 11 126       66534  11     14089   5      3423  12    338365   1    132086   2     10191   4    10.8
c 12 230       37413   6      9113   3      2072   7    142656   0     58441   1      5971   2    20.5
c 13 534        4672   1       946   0       188   1     14921   0      7029   0      1051   0     3.9
c 
c avg                  7.5           7.4           7.3           2.5           3.5           4.7
c std                  3.0           2.5           3.1           2.9           3.2           3.6
c 
c   97.282  10% cce
c   92.064   9% bump
c   82.287   8% unhide
c   53.414   5% probe
c   52.554   5% sweep
c   31.071   3% elim
c    9.334   1% rescore
c    3.974   0% bca
c    3.217   0% decide
c 
c   10.516 < 1% rest (below)
c 
c    3.131   0% gauss
c    2.934   0% block
c    2.183   0% transred
c    0.969   0% ternres
c    0.783   0% quatres
c    0.516   0% card
c    0.000   0% locs
c    0.000   0% queuesort
c ==================================
c    5.394   1% preprocessing     2%
c  339.042  34% inprocessing     98%
c ==================================
c  344.436  34% simplifying
c  654.952  66% search
c ==================================
c  999.393 100% all
c 
c        612192 conflicts,         612.6 confs/sec
c          2017 ternaries,         303.5 confs/ternary
c          2107 binaries,          290.6 confs/binary
c           368 iterations,       1663.6 confs/iteration
c 
c            11 reductions,          0.0 redus/sec,  55653.8 confs/reduction
c          9898 restarts,            9.9 rests/sec,     61.9 confs/restart
c       5294552 decisions,        5297.8 decis/sec,      8.6 decis/conflict
c    2619397447 propagations,  2620987.9 props/sec,    494.7 props/decision
c 
c 999.4 seconds, 245.1 MB
c
c CAUGHT SIGNAL 15 SIGTERM
c
c launch: done
