c launch: /data/cnf/sc2014/app/UR-20-10p1.cnf.bz2
c host: atom31
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/UR-20-10p1.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/UR-20-10p1.cnf.bz2
c no embedded options
c found 'p cnf 259234 1387934' header
c read 259234 variables, 1387934 clauses, 3351923 literals in 0.00 seconds
c
c --abstime=0
c --bate=1
c --batewait=2
c --bca=1
c --bcaddlimldscale=2
c --bcamaxeff=10000000
c --bcaminuse=100
c --bcawait=2
c --bkwdscale=100
c --bkwdroundlim=7
c --bkwdresched=1
c --blkboost=10
c --blkboostvlim=10000000
c --blkclslim=1000000
c --blklarge=1
c --blkmaxeff=800000000
c --blkmineff=50000000
c --blkocclim1=100000
c --blkocclim=1000000
c --blkocclim2=10000
c --blkreleff=100
c --blkresched=1
c --blkrtc=0
c --blksmall=1
c --blksuccessmaxwortc=6
c --blksuccessrat=100
c --block=1
c --blockwait=1
c --boost=1
c --bumpsimp=1
c --card=1
c --cardcut=2
c --cardexpam1=3
c --cardglue=0
c --cardignused=0
c --cardmaxeff=300000000
c --cardmaxlen=1000
c --cardmineff=2000000
c --cardminlen=3
c --cardocclim1=300
c --cardocclim2=15
c --cardreleff=5
c --cardreschedint=10
c --carduse=2
c --cardwait=0
c --cce2wait=1
c --cce=3
c --cceateint=2
c --cceboost=10
c --cceboostdel=3
c --cceboostint=5
c --cceboostvlim=10000000
c --cce3wait=2
c --ccemaxround=3
c --ccemaxeff=2147483647
c --ccemineff=30000000
c --ccereleff=50
c --ccertc=0
c --ccertcint=15
c --ccertcintvlim=2000000
c --ccesuccessrat=100
c --ccewait=2
c --clim=-1
c --compact=0
c --deco=1
c --decolim=100
c --deco1opt=1
c --decompose=1
c --defragfree=50
c --defragint=10000000
c --delmax=10
c --dlim=-1
c --druplig=0
c --drupligcheck=0
c --drupligtrace=0
c --drupligtraceorig=0
c --elim=1
c --elmaxeff=800000000
c --elmblk=1
c --elmblkwait=1
c --elmboost=20
c --elmboostdel=3
c --elmboostint=5
c --elmboostvlim=4000000
c --elmclslim=1000000
c --elmfull=0
c --elmineff=20000000
c --elmlitslim=200
c --elmocclim1=1000
c --elmocclim=1000000
c --elmocclim2=100
c --elmoccsumforced=0
c --elmreleff=200
c --elmresched=0
c --elmroundlim=3
c --elmrtc=0
c --elmrtcint=10
c --elmrtcintvlim=500000
c --elmsuccessmaxwortc=4
c --elmsuccessrat=100
c --exitonabort=0
c --factmax=100000
c --factor=3
c --gauss=1
c --gaussexptrn=1
c --gaussextrall=1
c --gaussmaxeff=50000000
c --gaussmaxor=20
c --gaussmineff=2000000
c --gaussreleff=2
c --gausswait=2
c --gluekeep=4
c --gluekeepsize=15
c --gluescale=4
c --hbrdom=2
c --import=1
c --incredcint=1
c --incredconfslim=0
c --incsavevisits=0
c --inprocessing=1
c --irrlim=1
c --jwhred=1
c --keepmaxglue=1
c --keepmaxglueint=100
c --lhbr=1
c --lkhd=2
c --locs=0
c --locsbanner=0
c --locsclim=1000000
c --locsboost=2
c --locscint=10000
c --locset=2
c --locsexport=1
c --locsmaxeff=100000
c --locsmineff=1000
c --locsred=0
c --locsreleff=5
c --locsrtc=0
c --locsvared=100
c --locswait=2
c --maxscaledglue=15
c --memlim=-1
c --minimize=2
c --minlocalgluelim=200
c --minlocalsizelim=3000
c --minrecgluelim=100
c --minrecsizelim=1000
c --norestartsatlimlo=85
c --move=2
c --otfs=1
c --penmax=4
c --phase=0
c --phaseluckfactor=200
c --phaselucklim=100
c --phaseluckmaxround=10
c --phasesave=1
c --plain=0
c --plim=-1
c --poison=1
c --prbasic=1
c --prbasicmaxeff=400000000
c --prbasicmineff=1000000
c --prbasicreleff=50
c --prbasicroundlim=8
c --prbasicrtc=0
c --prbrtc=0
c --prbsimple=2
c --prbsimpleboost=10
c --prbsimpleliftdepth=2
c --prbsimplemaxeff=200000000
c --prbsimplemineff=2000000
c --prbsimplereleff=40
c --prbsimplertc=0
c --probe=1
c --promote=1
c --promotegluelim=8
c --pure=1
c --quatres=1
c --quatreswait=2
c --queuesort=1
c --queuesortjwh=0
c --randec=0
c --randecint=1000
c --redcls=1
c --redclsglue=6
c --redclsmaxdec=5
c --redclsmaxdepth=10
c --redclsmaxlrg=10
c --redclsmaxprops=100
c --redclsatlimlo=0
c --redclsatlimhi=100
c --redclsize=30
c --redclstype=4
c --reducefixed=0
c --reduceinc=1000
c --reduceinit=50000
c --reduce=1
c --restart=4
c --restartglcint=10
c --restartglclim=115
c --restartinit=0
c --restartint=5
c --restartpen=1
c --retirenb=1
c --retireint=4
c --retiremin=1
c --reusetrail=0
c --rmincpen=4
c --rstinoutinc=110
c --satlimdelay=10000
c --scincinc=200
c --scincincsatlimhi=100
c --scincincdelta=10
c --scincincincint=100000
c --scincincmin=200
c --scincincmode=1
c --score=6
c --scoreshift=0
c --scoreresetint=2147483647
c --seed=0
c --simpbintinc=100
c --simpbintinclim=10000
c --simpcintdelay=2000
c --simpcintinc=20000
c --simpcintincdiv=1
c --simpcintmaxhard=10000000
c --simpcintmaxsoft=1000000
c --simpincdelmaxfact=50
c --simpincdelmaxmin=10000
c --simpinitdelay=0
c --simpintsizepen=0
c --simpen=0
c --simpidiv=3
c --simpiscale=100
c --simpitdelay=10
c --simpitintinc=10
c --simpitintinclim=1000
c --simplify=2
c --simprtc=5
c --simptintinc=1000
c --simptintinclim=10000
c --simpvarchg=100
c --simpvarlim=100
c --sizemaxpen=5
c --sizepen=1000000
c --sleeponabort=0
c --smallirr=90
c --smallve=1
c --smallvevars=10
c --smallvewait=0
c --sortlits=0
c --subl=9
c --sweep=1
c --sweepboost=10
c --sweepboostdel=4
c --sweepboostint=7
c --sweepboostvlim=1000000
c --sweepfacdec=10
c --sweepforgive=2
c --sweepirr=3
c --sweepmaxeff=200000000
c --sweepmaxdec=10000
c --sweepmaxround=3
c --sweepmindec=100
c --sweepmineff=1000000
c --sweepred=3
c --sweepreleff=3
c --sweeprtc=0
c --sweeprtcint=14
c --sweeprtcintvlim=100000
c --sweepsuccessmaxwortc=6
c --sweepsuccessrat=1000
c --sweepwait=2
c --synclsall=1
c --synclsglue=8
c --synclsint=100
c --synclslen=40
c --syncunint=111111
c --termint=122222
c --ternres=1
c --ternresboost=5
c --ternresrtc=0
c --ternreswait=2
c --transred=1
c --transredwait=2
c --trapiflush=0
c --trdmaxeff=2000000
c --trdmineff=100000
c --trdreleff=10
c --treelook=1
c --treelookboost=10
c --treelookfull=0
c --treelookmaxeff=50000000
c --treelookmineff=300000
c --treelookreleff=2
c --treelookrtc=0
c --trep=1
c --trepint=55555
c --trnreleff=10
c --trnrmaxeff=200000000
c --trnrmineff=4000000
c --unhdatrn=2
c --unhdextstamp=1
c --unhdhbr=0
c --unhdlnpr=3
c --unhdmaxeff=20000000
c --unhdmineff=100000
c --unhdreleff=2
c --unhdroundlim=20
c --unhide=1
c --unhidewait=0
c --usedtwice=1
c --vsidsdint=256
c --wait=1
c --waitmax=4
c --witness=0
c --check=0
c --log=-1
c --profile=1
c --profilelong=1
c --verbose=1
c [freezer] frozen 0 variables out of 246085 free variables 0%
c [limits] no decision limit
c [limits] no conflict limit
c [limits] no propagation limit
c [limits] simplification not delayed since 'simpdelay' zero
c [set-maximum-score] maximum score limit 1.000000d+500
c [set-minimum-score] minimum score limit 1.000000d-500
c [score-type] AVG (--score=6)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c *    0.0  246085  1373915         0       0      0     0    0     0   58   0%      0    0    0    0    0%
c 
c [simplification-1] limit 0 conflicts (hard 0) hit after 0 conflicts
c [card-1] limit 2000000 penalty 0 = 0 + 0
c [card-1] found 6535 at-most-one constraints of average size 5.7
c [card-1] no at-most-two constraint found
c [card-1] using previous limit 2000000 for elimination
c [card-1] 6535 out of 6535 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 62780 variables
c [simpleprobe-1] all 196454 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 144 variables
c [simpleprobe-1] 15292 variables remain 8% (181018 retained 92%)
c [simpleprobe-1] removed 144 variables, found 17443 hbrs, 1 units
c [unhide-1] limit 66116 based on 1057870 irredundant clauses
c [unhide-1-1] 1 units, 672 failed, 9916 tauts, 0 hbrs, 9346 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 195745 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 62823 not tried 32% in round 1
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 74694 = 38% variables out of 195745 scheduled
c [elim-1] considered successful since not run to completion yet
c [phase-count-1] 889020 negative 99.3% of 895640 except 6620 0.7%
c [phase-count-1] 723947 positive 80.8% of 895640 except 171693 19.2%
c [phase-count-1] less non-negative clauses 6620 than limit 89500 (10.0%)
c [phase-count-1] non-pos/non-neg = 171693/6620 = 25.94 >= 2.00 = 200/100
c [lucky-phase-1] forcing lucky phase -1
c [phase-1] phase bias: 0 positive 0%, 121051 negative 100%
c [sort-queue-1] sorted 121051 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 121051 (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 81605 variables 40.3% (121051 remain 49%)
c [simplification-1] removed 478275 irredundant clauses 34.8% (895640 remain 65%)
c [simplification-1] maximum reduction of 40% = max (40%, 35%)
c [simplification-1] large reduction 40% >= 5% limit
c [simplification-1] next conflict interval 1000 = 2000/2
c [simplification-1] penalized conflict interval 1000 = 1 * 1000
c [simplification-1] hard conflict limit 11000 (soft 1000 + delta 10000)
c [simplification-1] new conflict limit 1000 (hard 11000)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i    5.2  121050   895640        41      32      2 12554    0     7   59   1%      0    7    1    0 23348%
c i    5.2  120362   895640        43      32      2 12555    0     7   59   1%      0    7    1    0 23173%
c i    5.3  120353   895640        84      63      9 12557    0     8   59   1%      0    8    2    0 20975%
c i    5.4  119592   895640       103      80      9 12558    0     9   59   2%      0    9    2    0 20694%
c i    5.4  119378   895640       114      90      9 12558    0     9   59   2%      0    9    2    0 20147%
c i    5.4  119164   895640       115      90      9 12558    0     9   59   2%      0    9    2    0 20069%
c i    5.6  119152   895640       174     135     14 12566    0    14   59   2%      0   14    3    0 18357%
c i    5.6  119145   895640       187     146     15 12566    0    15   59   2%      0   15    3    0 17844%
c i    5.7  118972   895640       204     161     16 12566    0    15   59   2%      0   15    3    0 17256%
c i    5.7  118243   895640       215     169     17 12567    0    16   59   2%      0   16    3    0 16829%
c 
c [simplification-2] limit of 10 iterations hit after 10 iterations
c [decomp-3] removed 3374 variables
c [simpleprobe-2] 14433 schedulable variables 12%
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [simpleprobe-2] 15532 variables remain 13% (102145 retained 87%)
c [simpleprobe-2] removed 0 variables, found 1592 hbrs, 0 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 80497 literals 34%
c [treelook-1] scheduling used 641380 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 333006 steps
c [treelook-1] 80493 literals remain 34%
c [treelook-1] 80345 variables remain to probed next time 68%
c [decomp-5] removed 1 variables
c [treelook-1] removed 1 variables, found 2297 hbrs
c [basicprobe-1] limit 6966840 based on 870855 irredundant clauses
c [basicprobe-1-0] 42197 probes remain 37% after last round
c [basicprobe-1-0] 29 units = 29 failed (100%) + 0 lifted (0%)
c [basicprobe-1-0] removed 4734 variables, found 23872 hbrs
c [unhide-2] limit 54428 based on 870855 irredundant clauses
c [unhide-2-2] 3 units, 1527 failed, 8516 tauts, 0 hbrs, 1538 literals
c [elim-2] 59489 variables 54% will be scheduled this time
c [elim-2] scheduled 59489 variables 54%
c [elim-2] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-2] rescheduling of touched variables disabled
c [elim-2] incomplete 24388 not tried 22% in round 1
c [elim-2] transition to [ all 0 rem 1 ] state
c [elim-2] eliminated 87 = 0% variables out of 59489 scheduled
c [elim-2] considered successful since not run to completion yet
c [phase-count-2] 800411 negative 99.2% of 807031 except 6620 0.8%
c [phase-count-2] 650884 positive 80.7% of 807031 except 156147 19.3%
c [phase-count-2] less non-negative clauses 6620 than limit 80700 (10.0%)
c [phase-count-2] non-pos/non-neg = 156147/6620 = 23.59 >= 2.00 = 200/100
c [lucky-phase-2] forcing lucky phase -1
c [phase-2] phase bias: 0 positive 0%, 11147 negative 100%
c [sort-queue-2] sorted 99228 enqueued variables after 215 conflicts
c [score-dist-2] active 11486 (10%), one 0 (0%), zero 99228 (90%)
c [score-dist-2] max exp 509, different 10 (2%)
c [score-dist-2] median active exp 508, avg 507.5
c [simplification-2] removed 7090 variables 6.0% (110714 remain 45%)
c [simplification-2] removed 88609 irredundant clauses 9.9% (807031 remain 59%)
c [simplification-2] maximum reduction of 10% = max (6%, 10%)
c [simplification-2] forced so keeping old conflict interval 0
c [simplification-2] conflict limit remains at 1015 (hard 11000)
c [simplification-2] new iteration interval 100
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i    9.1  110713   807031       225     164     19 28398    0    16   54   2%      0   16    3    0 16329%
c i    9.1  110711   807031       252     184     20 28403    0    17   55   2%      0   17    3    0 15813%
c i    9.1  110701   807031       265     195     21 28403    0    18   55   3%      0   17    5    0 17382%
c i    9.2  110688   807031       271     199     21 28404    1    18   55   3%      0   18    6    0 18239%
c i    9.2  110677   807031       302     226     21 28405    1    20   55   5%      0   20   13    0 20020%
c i    9.2  110660   807031       316     239     21 28405    1    21   55   5%      0   21   14    0 19357%
c i    9.2  110649   807031       321     243     21 28405    1    21   55   5%      0   21   13    0 19003%
c i    9.3  110635   807031       352     266     28 28405    1    22   55   5%      0   22   13    0 17301%
c i    9.4  110624   807031       403     301     34 28414    1    26   55   5%      0   26   13    0 15251%
c i    9.4  110615   807031       405     302     34 28414    1    26   55   5%      0   26   13    0 15211%
c i    9.4  110602   807031       416     309     35 28416    1    26   55   5%      0   26   13    0 14886%
c i    9.5  110226   807031       454     336     39 28421    1    28   55   5%      0   28   12    0 13240%
c i    9.6  110090   807031       571     422     45 28433    2    31   55   5%      0   31   10    0 10025%
c i    9.8  110077   807031       736     562     57 28443    2    37   55   5%      0   37    9    0 7117%
c i    9.9  109925   807031       764     582     59 28446    2    38   55   5%      0   38    9    0 7013%
c i    9.9  109914   807031       765     582     59 28446    2    38   55   5%      0   38    9    0 6986%
c i   10.0  109903   807031       847     647     66 28454    2    41   55   5%      0   40   10    0 7020%
c i   10.1  109529   807031       882     676     67 28457    2    42   55   5%      0   42    9    0 6518%
c i   10.2  109298   807031       958     728     76 28470    2    45   55   5%      0   45    8    0 5579%
c 
c [simplification-3] limit 1034 conflicts (hard 11000) hit after 1034 conflicts
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 3788 at-most-one constraints of average size 4.7
c [card-2] no at-most-two constraint found
c [card-2] using previous limit 1000000 for elimination
c [card-2] 3788 out of 3788 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [decomp-6] removed 1530 variables
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] scheduled 66012 literals 30%
c [treelook-2] scheduling used 555289 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] used 306329 steps
c [treelook-2] 66002 literals remain 30%
c [treelook-2] 54580 variables remain to probed next time 50%
c [treelook-2] removed 2 variables, found 1946 hbrs
c [unhide-3] limit 55864 with penalty 1 = 0 + 1
c [unhide-3-3] 2 units, 802 failed, 19870 tauts, 0 hbrs, 381 literals
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 108492 variables 100%
c [elim-3] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-3] rescheduling of touched variables disabled
c [elim-3] incomplete 32234 not tried 30% in round 1
c [elim-3] transition to [ all 1 rem 1 ] state
c [elim-3] eliminated 2288 = 2% variables out of 108492 scheduled
c [elim-3] considered successful since not run to completion yet
c [phase-count-3] 767323 negative 99.2% of 773793 except 6470 0.8%
c [phase-count-3] 625777 positive 80.9% of 773793 except 148016 19.1%
c [phase-count-3] less non-negative clauses 6470 than limit 77300 (10.0%)
c [phase-count-3] non-pos/non-neg = 148016/6470 = 22.88 >= 2.00 = 200/100
c [lucky-phase-3] forcing lucky phase -1
c [phase-3] phase bias: 0 positive 0%, 7282 negative 100%
c [sort-queue-3] sorted 83077 enqueued variables after 1034 conflicts
c [score-dist-3] active 23127 (22%), one 0 (0%), zero 83077 (78%)
c [score-dist-3] max exp 512, different 13 (3%)
c [score-dist-3] median active exp 510, avg 509.8
c [simplification-3] removed 3086 variables 2.8% (106204 remain 43%)
c [simplification-3] removed 33238 irredundant clauses 4.1% (773793 remain 56%)
c [simplification-3] maximum reduction of 4% = max (3%, 4%)
c [simplification-3] geometric conflict interval increment 4000 = 20000 / 5
c [simplification-3] new conflict interval 4000
c [simplification-3] penalized conflict interval 4000 = 1 * 4000
c [simplification-3] hard conflict limit 15034 (soft 5034 + delta 10000)
c [simplification-3] new conflict limit 5034 (hard 15034)
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   13.1  106203   773793      1173     864     92 25458    3    49   54   5%      1   48   10    0 5175%
c i   13.4  106093   773793      1345     994    108 25480    3    56   55   5%      1   55   12    0 5283%
c i   13.5  106012   773793      1364    1003    109 25488    3    57   55   5%      1   56   11    0 4993%
c i   13.6  105967   773793      1437    1058    120 25494    3    59   55   5%      1   58   10    0 4349%
c i   13.6  105945   773793      1444    1064    120 25494    3    59   55   5%      1   58   10    0 4256%
c i   13.6  105940   773793      1465    1078    123 25497    3    59   55   5%      1   58    9    0 4044%
c i   13.8  105160   773793      1612    1205    127 25508    4    65   55   6%      1   65   20    0 6655%
c i   13.8  105157   773793      1621    1210    128 25510    4    66   55   6%      1   66   20    0 6484%
c i   13.9  105144   773793      1647    1230    131 25511    4    69   55   6%      1   68   19    0 6126%
c i   14.1  104874   773793      1777    1330    144 25526    5    76   55   6%      1   75   18    0 5184%
c i   14.1  104858   773793      1778    1330    144 25526    5    76   55   6%      1   75   18    0 5164%
c i   14.2  104847   773793      1794    1342    144 25529    5    76   55   6%      1   75   17    0 4915%
c i   14.2  104834   773793      1839    1372    149 25534    5    77   55   7%      1   75   21    0 5648%
c i   14.3  104180   773793      1969    1482    157 25541    5    80   55   7%      1   79   18    0 4373%
c 
c [simplification-4] limit of 201 binary hit after 201 binaries
c [decomp-8] removed 2095 variables
c [basicprobe-2] limit 6082304 based on 760288 irredundant clauses
c [basicprobe-2-0] 36925 probes remain 36% after last round
c [basicprobe-2-0] 29 units = 29 failed (100%) + 0 lifted (0%)
c [basicprobe-2-0] removed 1376 variables, found 19780 hbrs
c [unhide-4] limit 96786 with penalty 1 = 0 + 1
c [unhide-4-4] 6 units, 1089 failed, 6692 tauts, 0 hbrs, 2279 literals
c [elim-4] 23493 variables 23% will be scheduled this time
c [elim-4] scheduled 23493 variables 23%
c [elim-4] boosting limit by 20
c [elim-4] limit of 400000000 steps penalty 0 = 0 + 0
c [elim-4] rescheduling of touched variables disabled
c [elim-4-1] eliminated 1 variables 0% in round 1 in 47448278 steps
c [elim-4-1] backward subsumption/strengthening limit 47448200
c [elim-4-1-1] backward checking 33 touched variables 0%
c [elim-4-1-1] fully completed backward checking in 1 rounds
c [elim-4-1] subsumed 2 and strengthened 0 clauses in 119191 steps
c [elim-4-1] rescheduled 4 variables 0% by backward subsumption
c [elim-4-2] no variable eliminated in round 2 in 1241 steps
c [elim-4] fully completed in 2 rounds
c [elim-4] transition to [ all 0 rem 0 ] state
c [elim-4] eliminated 1 = 0% variables out of 23493 scheduled
c [elim-4] 1 < 1/100 * 23493 = 234 considered unsuccessful
c [phase-count-4] 726788 negative 99.1% of 733258 except 6470 0.9%
c [phase-count-4] 592329 positive 80.8% of 733258 except 140929 19.2%
c [phase-count-4] less non-negative clauses 6470 than limit 73300 (10.0%)
c [phase-count-4] non-pos/non-neg = 140929/6470 = 21.78 >= 2.00 = 200/100
c [lucky-phase-4] forcing lucky phase -1
c [phase-4] phase bias: 0 positive 0%, 4701 negative 100%
c [sort-queue-4] sorted 71908 enqueued variables after 2009 conflicts
c [score-dist-4] active 29253 (29%), one 0 (0%), zero 71908 (71%)
c [score-dist-4] max exp 512, different 13 (3%)
c [score-dist-4] median active exp 512, avg 511.0
c [simplification-4] removed 3007 variables 2.9% (101161 remain 41%)
c [simplification-4] removed 40535 irredundant clauses 5.2% (733258 remain 53%)
c [simplification-4] maximum reduction of 5% = max (3%, 5%)
c [simplification-4] forced so keeping old conflict interval 4000
c [simplification-4] conflict limit remains at 5046 (hard 15034)
c [simplification-4] new binary interval 1000
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   16.8  101160   733258      2052    1519    165 35787    5    84   53   6%      1   83   15    0 3673%
c i   16.8  100636   733258      2053    1519    165 35787    5    84   53   6%      1   83   15    0 3659%
c i   17.1  100500   733258      2130    1579    179 35788    5    90   53   6%      1   89   14    0 3200%
c i   17.4  100493   733258      2246    1682    186 35793    6    99   53   6%      1   97   17    0 3667%
c i   17.8  100485   733258      2396    1806    194 35799    6   114   53   6%      1  113   18    1 3533%
c i   18.1  100471   733258      2611    1986    214 35808    7   123   53   6%      1  120   20    1 3402%
c i   18.2  100458   733258      2646    2010    221 35811    7   124   53   6%      1  122   18    1 3160%
c i   18.6  100424   733258      2946    2275    231 35824    9   130   53   7%      1  127   27    1 3860%
c i   18.7  100423   733258      2990    2312    232 35827    9   133   53   7%      1  130   26    1 3695%
c i   19.0  100412   733258      3167    2472    238 35834   10   146   53   7%      1  143   39    1 4593%
c i   19.1  100287   733258      3208    2503    244 35836   11   150   53   7%      1  147   36    1 4186%
c i   19.1  100274   733258      3214    2508    244 35836   11   151   53   7%      1  147   35    1 4133%
c i   19.6  100185   733258      3482    2724    260 35860   12   162   53   7%      1  158   34    1 3522%
c i   19.7   99927   733258      3531    2761    265 35866   12   165   53   7%      1  160   32    1 3211%
c i   19.7   99913   733258      3537    2763    266 35868   12   165   53   7%      1  160   31    1 3151%
c i   20.5   99775   733258      3890    3049    297 35898   13   175   53   7%      2  170   22    1 2004%
c i   20.7   99740   733258      3947    3092    300 35904   13   178   53   7%      2  173   25    1 2215%
c i   20.7   99736   733258      3967    3108    302 35904   13   179   53   7%      2  174   25    1 2199%
c i   20.7   99733   733258      3972    3112    302 35904   13   179   53   7%      2  174   25    1 2208%
c i   20.9   99730   733258      4075    3195    305 35913   13   178   54   7%      2  172   20    1 1737%
c i   21.1   99722   733258      4176    3281    308 35919   13   181   54   7%      2  175   23    1 1910%
c i   21.3   99721   733258      4263    3345    319 35924   13   186   54   7%      1  180   21    1 1705%
c i   21.3   99720   733258      4264    3345    319 35924   13   186   54   7%      1  180   20    1 1698%
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   21.8   99719   733258      4544    3597    324 35934   16   206   54   8%      2  199   38    1 2685%
c i   22.2   99711   733258      4680    3720    328 35937   16   225   54   7%      2  218   38    1 2571%
c i   22.9   99707   733258      5001    3995    349 35952   18   256   54   7%      2  247   48    2 2874%
c i   22.9   99706   733258      5004    3997    349 35952   18   256   54   7%      2  248   49    2 2907%
c i   23.0   99705   733258      5029    4009    355 35954   18   256   54   7%      2  247   46    2 2723%
c 
c [simplification-5] limit 5073 conflicts (hard 15034) hit after 5073 conflicts
c [quatres-1] found 42349 quaternary clauses 40% in total
c [ternres-1] boosting ternary resolution limit by 5
c [ternres-1] limit 20000000 with penalty 0 = 0 + 0
c [ternres-1] all 99701 free variables schedulable
c [ternres-1] 14 ternary resolvents (1 bin, 13 trn)
c [ternres-1] fully completed ternary resolution
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 171 xors of average arity 2.3
c [gauss-1] connected 390 occurrences of 264 variables (average 1.5)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] fully completed
c [gauss-1] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-9] removed 232 variables
c [unhide-5] limit 287300 with penalty 1 = 0 + 1
c [unhide-5-5] 1 units, 480 failed, 14009 tauts, 0 hbrs, 6830 literals
c [transred-1] limit 2000000 with penalty 0 = 0 + 0
c [transred-1] removed 163 transitive binary clauses
c [transred-1] found 7 units
c [block-1] scheduling all variables this time
c [block-1] scheduled 98978 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 10588 blocked clauses
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 9 clauses out of 314 (3%) of length 10
c [cce-1-1] eliminated 181 clauses out of 2211 (8%) of length 9
c [cce-1-1] eliminated 56 clauses out of 491 (11%) of length 8
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 246 large clauses in 30000014 steps
c [cce-1-1] allowing another 15000007 steps for small clauses
c [cce-1-1] scheduling 343096 clauses = 325586 binary + 17510 ternary
c [cce-1-1] tried to eliminate 464 small clauses 0%
c [cce-1-1] eliminated 166 binary clauses 0%
c [cce-1-1] eliminated 12 ternary clauses 0%
c [cce-1-1] eliminated 178 small clauses 0%
c [cce-1-1] eliminated 178 small clauses in 30000008 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 424 covered clauses in round 1
c [cce-1] eliminated 424 covered clauses in TOTAL during 1 rounds
c [cce-1] 424 < 1/100 * 695696 = 6956 considered unsuccessful
c [bca-1] limit of 10000000 steps and 1391044 added (scaled 2)
c [bca-1] 173360 out of 197958 literals actually usable 88%
c [bca-1] added 227 blocked clauses in 492938 steps
c [sweep-1] limit 1390544 based on 695272 irredundant clauses
c [sweep-1-1] 4988 pos 5.0% + 93990 neg 95.0% = 98978 sched 100.0% ret 0
c [sweep-1-1] 1508013 steps 13 queries 19469.85 avg class size
c [sweep-1-1] 155 decisions 9 SAT calls 174.78 avg env size
c [sweep-1-1] 98956 variables remain 100% (22 retained 0%)
c [decomp-10] removed 3 variables
c [sweep-1-1] removed 3 vars (0 failed, 3 eqs, 6 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 3 vars in TOTAL (1 rounds, 12 queries)
c [phase-count-5] 688822 negative 99.1% of 695272 except 6450 0.9%
c [phase-count-5] 571386 positive 82.2% of 695272 except 123886 17.8%
c [phase-count-5] less non-negative clauses 6450 than limit 69500 (10.0%)
c [phase-count-5] non-pos/non-neg = 123886/6450 = 19.21 >= 2.00 = 200/100
c [lucky-phase-5] forcing lucky phase -1
c [phase-5] phase bias: 0 positive 0%, 976 negative 100%
c [sort-queue-5] sorted 48899 enqueued variables after 5073 conflicts
c [score-dist-5] active 50076 (51%), one 0 (0%), zero 48899 (49%)
c [score-dist-5] max exp 514, different 14 (3%)
c [score-dist-5] median active exp 513, avg 513.1
c [simplification-5] removed 726 variables 0.7% (98975 remain 40%)
c [simplification-5] removed 37986 irredundant clauses 5.2% (695272 remain 51%)
c [simplification-5] maximum reduction of 5% = max (1%, 5%)
c [simplification-5] large reduction 5% >= 5% limit
c [simplification-5] next conflict interval 2000 = 2000/1
c [simplification-5] penalized conflict interval 2000 = 1 * 2000
c [simplification-5] hard conflict limit 17073 (soft 7073 + delta 10000)
c [simplification-5] new conflict limit 7073 (hard 17073)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   27.1   98974   695272      5181    4116    385 46894   20   268   54   7%      2  258   51    2 2782%
c i   27.2   98911   695272      5199    4123    390 46898   20   269   54   7%      2  260   48    2 2626%
c i   27.2   98903   695272      5202    4123    390 46900   20   269   54   7%      2  260   47    2 2596%
c i   27.2   98897   695272      5205    4123    390 46902   20   269   54   7%      2  260   47    2 2566%
c i   27.2   98885   695272      5207    4124    390 46902   20   269   54   7%      2  260   47    2 2559%
c i   27.4   98745   695272      5271    4179    392 46907   20   277   54   7%      2  268   46    2 2490%
c i   27.5   98744   695272      5308    4211    395 46908   21   281   54   7%      2  271   49    2 2568%
c i   27.7   98737   695272      5419    4302    402 46916   21   283   54   7%      1  273   40    2 2069%
c i   28.1   98728   695272      5596    4458    411 46922   23   303   54   7%      1  292   51    2 2396%
c i   28.2   98718   695272      5662    4508    416 46929   23   305   54   7%      1  294   44    2 2064%
c i   28.2   98710   695272      5664    4509    416 46929   23   305   54   7%      1  293   44    2 2060%
c i   28.2   98628   695272      5665    4509    416 46929   23   305   54   7%      1  293   44    2 2052%
c i   28.2   98620   695272      5668    4509    418 46929   23   304   54   7%      1  293   43    2 2029%
c i   28.2   98618   695272      5671    4511    418 46929   23   304   54   7%      1  293   43    2 2012%
c i   28.7   98617   695272      5946    4748    427 46938   24   305   54   8%      2  292   42    2 1834%
c i   28.8   98605   695272      5983    4781    429 46938   24   307   54   8%      1  294   39    2 1692%
c i   28.9   98477   695272      6028    4818    431 46941   24   310   54   8%      1  297   37    2 1590%
c i   29.1   98330   695272      6070    4845    437 46949   24   311   54   8%      1  298   32    2 1387%
c i   29.4   98321   695272      6271    5025    444 46957   25   307   54   8%      1  294   37    2 1525%
c i   29.4   98314   695272      6277    5028    444 46959   25   307   54   8%      1  293   37    2 1496%
c i   29.6   98313   695272      6441    5172    453 46967   25   308   54   8%      1  293   36    3 1435%
c i   30.1   98306   695272      6877    5547    476 46987   27   310   54   9%      2  293   39    3 1379%
c 
c [simplification-6] limit 7106 conflicts (hard 17073) hit after 7106 conflicts
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] all 98299 free variables schedulable
c [ternres-2] 0 ternary resolvents (0 bin, 0 trn)
c [ternres-2] 73732 variables remain 75% (24567 retained 25%)
c [card-3] limit 500000 penalty 2 = 2 + 0
c [card-3] found 1824 at-most-one constraints of average size 4.2
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 500000 for elimination
c [card-3] 1824 out of 1824 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [decomp-11] removed 710 variables
c [simpleprobe-3] 13775 schedulable variables 14%
c [simpleprobe-3] limit 7787683 penalty 1 = 1 + 0
c [decomp-12] removed 27 variables
c [simpleprobe-3] 13891 variables remain 14% (84347 retained 86%)
c [simpleprobe-3] removed 27 variables, found 10260 hbrs, 15 units
c [unhide-6] limit 389384 with penalty 1 = 0 + 1
c [unhide-6-6] 9 units, 547 failed, 7229 tauts, 0 hbrs, 11453 literals
c [transred-2] limit 2000000 with penalty 0 = 0 + 0
c [transred-2] removed 208 transitive binary clauses
c [transred-2] found 6 units
c [block-2] scheduling all variables this time
c [block-2] scheduled 97319 variables 100%
c [block-2] limit of 50000000 steps penalty 0 = 0 + 0
c [block-2] fully completed
c [block-2] transition to [ all 0 rem 0 ] state
c [block-2] eliminated 1405 blocked clauses
c [block-2] 1405 < 1/100 * 690329 = 6903 considered unsuccessful
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 97319 variables 100%
c [elim-5] limit of 38938416 steps penalty 1 = 1 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5] incomplete 11310 not tried 12% in round 1
c [elim-5] transition to [ all 1 rem 1 ] state
c [elim-5] eliminated 2650 = 3% variables out of 97319 scheduled
c [bca-2] limit of 10000000 steps and 1351675 added (scaled 2)
c [bca-2] 165017 out of 189340 literals actually usable 87%
c [bca-2] added 108 blocked clauses in 474910 steps
c [sweep-2] limit 1351062 based on 675531 irredundant clauses
c [sweep-2-1] 5577 pos 5.9% + 89073 neg 94.1% = 94650 sched 100.0% ret 19
c [sweep-2-1] 1490086 steps 27 queries 25386.33 avg class size
c [sweep-2-1] 208 decisions 17 SAT calls 70.59 avg env size
c [sweep-2-1] 94557 variables remain 100% (112 retained 0%)
c [decomp-13] removed 11 variables
c [sweep-2-1] removed 11 vars (0 failed, 9 eqs, 16 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 11 vars in TOTAL (1 rounds, 26 queries)
c [phase-count-6] 669634 negative 99.1% of 675518 except 5884 0.9%
c [phase-count-6] 553665 positive 82.0% of 675518 except 121853 18.0%
c [phase-count-6] less non-negative clauses 5884 than limit 67500 (10.0%)
c [phase-count-6] non-pos/non-neg = 121853/5884 = 20.71 >= 2.00 = 200/100
c [lucky-phase-6] forcing lucky phase -1
c [phase-6] phase bias: 0 positive 0%, 852 negative 100%
c [sort-queue-6] sorted 45195 enqueued variables after 7106 conflicts
c [score-dist-6] active 49463 (52%), one 0 (0%), zero 45195 (48%)
c [score-dist-6] max exp 514, different 14 (3%)
c [score-dist-6] median active exp 514, avg 513.5
c [simplification-6] removed 3641 variables 3.7% (94658 remain 38%)
c [simplification-6] removed 19754 irredundant clauses 2.8% (675518 remain 49%)
c [simplification-6] maximum reduction of 4% = max (4%, 3%)
c [simplification-6] geometric conflict interval increment 4000 = 20000 / 5
c [simplification-6] new conflict interval 8000
c [simplification-6] penalized conflict interval 8000 = 1 * 8000
c [simplification-6] hard conflict limit 25106 (soft 15106 + delta 10000)
c [simplification-6] new conflict limit 15106 (hard 25106)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   35.0   94657   675518      7201    5510    453 51241   27   307   54   9%      2  289   25    3  852%
c i   35.1   94602   675518      7221    5526    454 51243   27   307   54   9%      2  289   26    3  902%
c i   35.9   94487   675518      7577    5812    479 51275   27   316   54   8%      2  297   28    3  904%
c i   35.9   94482   675518      7578    5812    479 51275   27   316   54   8%      2  297   27    3  900%
c i   36.0   94474   675518      7638    5863    482 51279   27   318   54   8%      2  298   29    3  935%
c i   36.0   94467   675518      7650    5872    481 51280   27   317   54   8%      2  297   28    3  912%
c i   36.0   94464   675518      7653    5867    482 51280   27   317   54   8%      2  297   28    3  902%
c i   36.2   94463   675518      7768    5958    492 51288   27   316   54   8%      2  295   27    3  854%
c i   36.2   94462   675518      7779    5968    492 51288   27   316   54   8%      2  295   27    3  854%
c i   36.5   94459   675518      7969    6135    499 51299   28   315   54   9%      2  294   44    3 1360%
c i   38.0   94234   675518      8797    6850    550 51338   31   330   54   9%      5  305   52    4 1373%
c i   38.7   94233   675518      9077    7076    563 51374   31   342   54   9%      4  316   46    4 1172%
c i   38.7   94226   675518      9078    7076    563 51374   31   342   54   9%      4  315   46    4 1168%
c i   38.9   94219   675518      9220    7196    575 51379   31   341   54   9%      4  314   39    4  967%
c i   39.0   94154   675518      9266    7236    576 51383   31   341   54   9%      4  313   35    4  887%
c i   39.2   94151   675518      9371    7319    585 51395   31   339   54   9%      3  311   33    4  824%
c i   39.5   94057   675518      9539    7464    590 51396   32   343   54   9%      3  314   47    4 1122%
c i   39.6   94052   675518      9540    7464    590 51396   32   343   54   9%      3  314   47    4 1118%
c i   39.6   94045   675518      9541    7464    590 51396   32   343   54   9%      3  314   47    4 1113%
c i   39.6   94038   675518      9542    7464    590 51396   32   343   54   9%      3  314   46    4 1109%
c i   39.6   94031   675518      9543    7464    590 51396   32   343   54   9%      3  314   46    4 1105%
c i   39.6   94024   675518      9544    7464    590 51396   32   343   54   9%      3  314   46    4 1101%
c i   39.6   94017   675518      9546    7464    590 51397   32   342   54   9%      3  314   46    4 1092%
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   40.1   94010   675518      9747    7642    600 51403   32   346   54   9%      3  317   37    4  860%
c i   40.9   94009   675518     10097    7943    609 51424   32   358   54   9%      3  327   33    4  741%
c i   41.3   94008   675518     10326    8152    616 51428   33   365   56   9%      2  332   47    5 1024%
c i   41.7   94000   675518     10517    8319    628 51436   35   374   56   9%      2  340   61    5 1291%
c i   41.7   93999   675518     10518    8319    628 51436   35   374   56   9%      2  340   61    5 1286%
c i   41.7   93998   675518     10535    8329    628 51438   36   373   56  10%      2  340   70    5 1448%
c i   43.1   93992   675518     11166    8861    657 51488   38   394   56  10%      4  357   70    5 1321%
c i   43.1   93985   675518     11167    8861    657 51488   38   394   56  10%      4  357   70    5 1316%
c i   43.1   93978   675518     11168    8861    657 51488   38   394   56  10%      4  357   69    5 1311%
c i   43.1   93971   675518     11169    8861    657 51488   38   394   56  10%      4  357   69    5 1306%
c i   43.1   93964   675518     11170    8861    657 51488   38   394   56  10%      4  357   69    5 1301%
c i   43.2   93957   675518     11188    8876    659 51488   38   395   56  10%      3  358   65    5 1237%
c i   43.8   93749   675518     11529    9193    668 51493   38   398   57  10%      3  359   48    5  874%
c i   43.8   93744   675518     11564    9225    668 51493   39   396   57  10%      3  357   50    5  907%
c i   44.4   93743   675518     11800    9434    676 51504   39   394   57  10%      3  354   42    6  751%
c i   44.9   93735   675518     12088    9670    691 51516   39   387   57  10%      3  346   41    6  717%
c i   45.6   93734   675518     12373    9928    698 51529   39   407   58  10%      2  364   44    6  745%
c i   46.0   93726   675518     12527   10071    703 51533   40   416   58  10%      2  372   50    6  827%
c i   46.4   93715   675518     12711   10236    705 51543   39   425   58   9%      2  379   38    6  629%
c i   46.6   93448   675518     12764   10287    706 51543   39   427   58   9%      2  381   42    6  683%
c i   46.7   92915   675518     12805   10322    707 51545   39   430   58   9%      2  385   40    6  647%
c i   46.7   92906   675518     12809   10325    707 51545   39   430   58   9%      2  385   41    6  665%
c i   46.8   92893   675518     12850   10364    708 51545   39   434   58   9%      2  387   39    6  630%
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   47.2   92874   675518     13062   10548    716 51553   39   434   58   9%      2  386   42    6  662%
c i   48.1   92869   675518     13428   10858    738 51576   39   439   58   9%      2  390   33    6  518%
c i   48.2   92861   675518     13479   10904    738 51578   39   439   58   9%      2  389   40    6  615%
c i   48.2   92857   675518     13482   10905    738 51579   39   438   58   9%      2  388   40    6  613%
c i   48.2   92850   675518     13483   10905    738 51579   39   438   58   9%      2  388   40    6  611%
c i   48.2   92845   675518     13484   10905    738 51579   39   438   58   9%      2  388   40    6  608%
c i   48.2   92840   675518     13485   10905    738 51579   39   438   58   9%      2  388   39    6  606%
c i   48.2   92830   675518     13486   10905    738 51579   39   438   58   9%      2  388   39    6  604%
c i   48.3   92820   675518     13514   10928    742 51579   39   438   58   9%      2  388   38    7  591%
c i   48.4   92819   675518     13519   10930    744 51579   39   438   58   9%      2  388   38    7  587%
c i   48.4   92812   675518     13553   10959    746 51579   39   438   58   9%      2  388   40    7  610%
c i   48.8   92809   675518     13714   11101    752 51587   40   443   58   9%      2  392   45    7  671%
c i   49.4   92795   675518     13957   11315    763 51598   41   452   59   9%      2  400   56    7  823%
c i   49.4   92794   675518     13967   11322    763 51598   41   454   59   9%      2  401   56    7  818%
c i   49.5   92784   675518     14011   11363    763 51599   41   457   59   9%      2  404   57    7  833%
c i   50.6   92780   675518     14556   11844    784 51618   42   457   59   9%      3  401   51    7  705%
c i   50.9   92779   675518     14687   11965    785 51620   42   455   59   9%      2  398   55    7  760%
c i   50.9   92776   675518     14688   11965    785 51620   42   455   59   9%      2  398   55    7  757%
c i   51.2   92772   675518     14795   12062    788 51626   43   464   59   9%      2  406   64    7  859%
c i   51.2   92766   675518     14811   12075    788 51627   43   463   59   9%      2  405   63    7  843%
c i   51.3   92765   675518     14826   12088    788 51628   43   463   59   9%      2  405   64    7  860%
c i   51.6   92530   675518     14979   12233    789 51629   45   467   60  10%      2  408   70    8  921%
c i   51.6   92529   675518     14980   12233    789 51629   45   467   60  10%      2  408   70    8  917%
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   51.7   92520   675518     15003   12252    791 51629   45   467   60  10%      2  408   69    8  911%
c i   52.0   92519   675518     15169   12396    799 51640   45   469   60  10%      2  409   64    8  824%
c 
c [simplification-7] limit 15302 conflicts (hard 25106) hit after 15302 conflicts
c [quatres-2] found 42437 quaternary clauses 43% in total
c [quatres-2-2] added 1 single-self-subsuming ternary resolvents
c [quatres-2-2] added 2 quaternary resolvents
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] extracted 25 xors of average arity 2.4
c [gauss-2] connected 60 occurrences of 58 variables (average 1.0)
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] fully completed
c [decomp-14] removed 75 variables
c [gauss-2] exported 1 unary, 0 binary and 0 ternary equations
c [treelook-3] limit 907229 penalty 0 = 0 + 0 boost 1
c [treelook-3] scheduled 107508 literals 58%
c [treelook-3] scheduling used 907368 steps
c [treelook-3] not fully scheduled
c [treelook-3] limit 907229 penalty 0 = 0 + 0 boost 1
c [treelook-3] used 2261835 steps
c [treelook-3] 107496 literals remain 58%
c [treelook-3] 43858 variables remain to probed next time 47%
c [treelook-3] removed 4 variables, found 3781 hbrs
c [unhide-7] limit 907229 with penalty 1 = 0 + 1
c [unhide-7-7] 13 units, 270 failed, 11253 tauts, 0 hbrs, 49109 literals
c [transred-3] limit 2000000 with penalty 0 = 0 + 0
c [transred-3] removed 248 transitive binary clauses
c [transred-3] found 7 units
c [cce-2] limit of 22680732 steps penalty 1 = 1 + 0
c [cce-2-1] eliminated 2 clauses out of 491 (0%) of length 8
c [cce-2-1] eliminated 17 clauses out of 808 (2%) of length 7
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] eliminated 19 large clauses in 22680736 steps
c [cce-2-1] allowing another 11340368 steps for small clauses
c [cce-2-1] scheduling 531749 clauses = 300502 binary + 231247 ternary
c [cce-2-1] tried to eliminate 152 small clauses 0%
c [cce-2-1] eliminated 39 binary clauses 0%
c [cce-2-1] eliminated 3 ternary clauses 0%
c [cce-2-1] eliminated 42 small clauses 0%
c [cce-2-1] eliminated 4626 small clauses in 22680749 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 4645 covered clauses in round 1
c [cce-2] eliminated 4645 covered clauses in TOTAL during 1 rounds
c [cce-2] 4645 < 1/100 * 653592 = 6535 considered unsuccessful
c [elim-6] 11215 variables 12% will be scheduled this time
c [elim-6] scheduled 11215 variables 12%
c [elim-6] limit of 181445857 steps penalty 0 = 0 + 0
c [elim-6] rescheduling of touched variables disabled
c [elim-6-1] no variable eliminated in round 1 in 27508548 steps
c [elim-6] fully completed in 1 rounds
c [elim-6] transition to [ all 0 rem 0 ] state
c [elim-6] eliminated 0 = 0% variables out of 11215 scheduled
c [bca-3] limit of 10000000 steps and 1295365 added (scaled 2)
c [bca-3] 152387 out of 183762 literals actually usable 83%
c [bca-3] added 51 blocked clauses in 424618 steps
c [sweep-3] limit 2721687 penalty 0 = 0 + 0
c [sweep-3-1] 4599 pos 5.0% + 87184 neg 95.0% = 91783 sched 99.9% ret 97
c [sweep-3-1] 3161346 steps 34 queries 16406.21 avg class size
c [sweep-3-1] 418 decisions 32 SAT calls 71.28 avg env size
c [sweep-3-1] 91377 variables remain 99% (488 retained 1%)
c [decomp-17] removed 54 variables
c [sweep-3-1] removed 54 vars (0 failed, 3 eqs, 6 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 54 vars in TOTAL (1 rounds, 33 queries)
c [phase-count-7] 641204 negative 99.1% of 647084 except 5880 0.9%
c [phase-count-7] 531828 positive 82.2% of 647084 except 115256 17.8%
c [phase-count-7] less non-negative clauses 5880 than limit 64700 (10.0%)
c [phase-count-7] non-pos/non-neg = 115256/5880 = 19.60 >= 2.00 = 200/100
c [lucky-phase-7] forcing lucky phase -1
c [phase-7] phase bias: 0 positive 0%, 511 negative 100%
c [sort-queue-7] sorted 38727 enqueued variables after 15302 conflicts
c [score-dist-7] active 53099 (58%), one 0 (0%), zero 38727 (42%)
c [score-dist-7] max exp 515, different 13 (3%)
c [score-dist-7] median active exp 515, avg 514.5
c [simplification-7] removed 690 variables 0.7% (91826 remain 37%)
c [simplification-7] removed 28434 irredundant clauses 4.2% (647084 remain 47%)
c [simplification-7] maximum reduction of 4% = max (1%, 4%)
c [simplification-7] geometric conflict interval increment 4000 = 20000 / 5
c [simplification-7] new conflict interval 12000
c [simplification-7] penalized conflict interval 12000 = 1 * 12000
c [simplification-7] hard conflict limit 37302 (soft 27302 + delta 10000)
c [simplification-7] new conflict limit 27302 (hard 37302)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   57.6   91825   647084     15477   12581    755 54737   47   472   62  10%      2  410   68    8  840%
c i   57.8   91819   647084     15552   12646    755 54741   47   473   62  10%      2  410   65    8  796%
c i   59.1   91817   647084     16187   13225    775 54756   51   474   62  11%      3  407   62    9  713%
c i   59.3   91809   647084     16272   13300    776 54762   51   470   62  11%      3  403   59    9  674%
c i   59.3   91799   647084     16273   13300    776 54762   51   470   62  11%      3  402   59    9  671%
c i   59.3   91790   647084     16274   13300    776 54762   51   469   62  11%      3  402   59    9  669%
c i   59.3   91780   647084     16275   13300    776 54762   51   469   62  11%      3  402   58    9  666%
c i   59.3   91769   647084     16276   13300    776 54762   51   469   62  11%      3  402   58    9  663%
c i   59.4   91760   647084     16316   13337    776 54762   51   471   62  11%      3  404   58    9  654%
c i   59.6   91752   647084     16381   13393    778 54768   51   475   62  11%      3  407   57    9  648%
c i   60.3   91742   647084     16820   13786    788 54786   52   467   62  11%      3  397   56    9  607%
c i   60.5   91726   647084     16920   13871    791 54793   52   464   62  11%      3  393   47    9  503%
c i   61.8   91723   647084     17577   14465    810 54814   53   464   62  11%      4  389   67   10  681%
c i   62.4   91722   647084     18022   14846    835 54825   54   449   62  12%      4  372   54   10  529%
c i   62.8   91721   647084     18161   14972    839 54828   53   449   62  12%      3  370   49   10  484%
c i   63.7   91713   647084     18564   15335    850 54839   54   451   62  12%      3  371   58   11  550%
c i   63.7   91704   647084     18565   15335    850 54839   54   451   62  12%      3  371   58   11  548%
c i   65.6   91698   647084     19443   16112    869 54873   60   457   62  13%      5  371   64   11  554%
c i   67.2   91693   647084     20151   16744    888 54907   60   464   62  13%      5  374   57   12  477%
c i   67.7   91692   647084     20424   16981    894 54915   60   456   62  13%      5  365   59   12  479%
c i   68.4   91691   647084     20675   17217    896 54921   62   462   62  13%      4  369   82   12  655%
c i   69.4   91687   647084     21072   17575    902 54931   63   461   63  14%      3  366   79   13  614%
c i   70.2   91686   647084     21432   17881    921 54961   62   464   63  13%      3  367   56   13  427%
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   72.1   91624   647084     22315   18671    946 54981   63   466   66  13%      5  364   57   14  414%
c i   72.8   91623   647084     22654   18982    955 54986   64   473   67  14%      4  370   77   14  540%
c i   74.1   91622   647084     23229   19493    966 55008   67   486   67  14%      4  379   80   15  546%
c i   74.1   91617   647084     23241   19504    966 55008   67   484   67  14%      4  377   81   15  546%
c i   74.1   91609   647084     23251   19513    966 55008   66   483   67  14%      4  376   78   15  530%
c i   74.3   91600   647084     23350   19604    970 55009   66   481   67  14%      4  373   72   15  486%
c i   74.3   91594   647084     23354   19606    970 55010   66   480   67  14%      4  373   71   15  480%
c i   75.8   91586   647084     24018   20188    998 55030   65   482   67  14%      4  370   71   15  466%
c i   75.8   91578   647084     24036   20201    999 55032   65   480   67  14%      4  369   67   15  441%
c i   75.9   91567   647084     24090   20252   1000 55032   66   481   67  14%      4  369   75   15  489%
c i   75.9   91563   647084     24096   20255   1001 55032   66   481   67  14%      4  369   74   15  483%
c i   76.2   91562   647084     24259   20403   1004 55035   66   474   67  14%      3  361   75   16  485%
c i   76.3   91557   647084     24347   20473   1005 55047   66   470   67  14%      3  357   71   16  454%
c i   76.6   91554   647084     24482   20597   1007 55048   67   473   68  14%      3  360   76   16  485%
c i   77.6   91553   647084     24929   20991   1024 55062   67   474   69  14%      3  358   70   16  438%
c i   77.6   91548   647084     24930   20991   1024 55062   67   474   69  14%      3  358   70   16  436%
c i   78.2   91540   647084     25164   21202   1032 55071   67   483   69  14%      2  365   64   16  391%
c i   78.9   91537   647084     25496   21502   1038 55085   67   491   69  14%      2  372   71   17  431%
c i   78.9   91533   647084     25497   21502   1038 55085   67   491   69  14%      2  371   71   17  430%
c i   80.1   91527   647084     25962   21919   1051 55101   69   501   71  14%      2  379   82   17  480%
c i   81.1   91517   647084     26301   22238   1055 55105   71   503   72  14%      2  379   80   17  459%
c i   83.1   91515   647084     27285   23152   1066 55126   71   484   72  15%      6  354   74   18  406%
c i   83.1   91512   647084     27287   23153   1066 55126   71   483   72  15%      6  354   74   18  405%
c 
c [simplification-8] limit 27381 conflicts (hard 37302) hit after 27381 conflicts
c [quatres-3] found 43902 quaternary clauses 43% in total
c [quatres-3-1] removed 1 duplicate quaternary clauses
c [quatres-3-2] added 3 single-self-subsuming ternary resolvents
c [quatres-3-2] added 5 quaternary resolvents
c [ternres-3] limit 8019461 with penalty 1 = 1 + 0
c [ternres-3] 68569 schedulable variables 75%
c [ternres-3] 28 ternary resolvents (1 bin, 27 trn)
c [ternres-3] 19959 variables remain 22% (71553 retained 78%)
c [gauss-3] limit 3207784 penalty 0 = 0 + 0
c [gauss-3] extracted 134 xors of average arity 2.5
c [gauss-3] connected 331 occurrences of 214 variables (average 1.5)
c [gauss-3] limit 3207784 penalty 0 = 0 + 0
c [gauss-3] fully completed
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-18] removed 84 variables
c [basicprobe-3] limit 80194616 penalty 0 = 0 + 0
c [basicprobe-3-0] 29722 probes remain 33% after last round
c [basicprobe-3-0] 403 units = 396 failed (98%) + 7 lifted (2%)
c [basicprobe-3-0] removed 1553 variables, found 205765 hbrs
c [bate-1] eliminated 152 asymmetric tautologies during probing
c [unhide-8] limit 1603892 with penalty 1 = 0 + 1
c [unhide-8-8] 5 units, 838 failed, 37160 tauts, 0 hbrs, 146709 literals
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 127 transitive binary clauses
c [transred-4] found 4 units
c [block-3] scheduling all variables this time
c [block-3] scheduled 89212 variables 100%
c [block-3] limit of 80194616 steps penalty 1 = 1 + 0
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 87 blocked clauses
c [block-3] 87 < 1/100 * 634767 = 6347 considered unsuccessful
c [bca-4] limit of 10000000 steps and 1255149 added (scaled 2)
c [bca-4] 143214 out of 178426 literals actually usable 80%
c [bca-4] added 53 blocked clauses in 405307 steps
c [sweep-4] limit 4811676 penalty 0 = 0 + 0
c [sweep-4-1] 4740 pos 5.3% + 84036 neg 94.7% = 88776 sched 99.5% ret 436
c [sweep-4-1] 4950405 steps 47 queries 9935.47 avg class size
c [sweep-4-1] 670 decisions 37 SAT calls 214.14 avg env size
c [sweep-4-1] 87987 variables remain 99% (1218 retained 1%)
c [decomp-19] removed 175 variables
c [sweep-4-1] removed 175 vars (0 failed, 9 eqs, 20 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 175 vars in TOTAL (1 rounds, 46 queries)
c [phase-count-8] 620979 negative 99.1% of 626855 except 5876 0.9%
c [phase-count-8] 513893 positive 82.0% of 626855 except 112962 18.0%
c [phase-count-8] less non-negative clauses 5876 than limit 62600 (10.0%)
c [phase-count-8] non-pos/non-neg = 112962/5876 = 19.22 >= 2.00 = 200/100
c [lucky-phase-8] forcing lucky phase -1
c [phase-8] phase bias: 0 positive 0%, 317 negative 100%
c [sort-queue-8] sorted 34655 enqueued variables after 27381 conflicts
c [score-dist-8] active 54382 (61%), one 0 (0%), zero 34655 (39%)
c [score-dist-8] max exp 516, different 14 (3%)
c [score-dist-8] median active exp 516, avg 515.5
c [simplification-8] removed 2475 variables 2.7% (89037 remain 36%)
c [simplification-8] removed 20229 irredundant clauses 3.1% (626855 remain 46%)
c [simplification-8] maximum reduction of 3% = max (3%, 3%)
c [simplification-8] geometric conflict interval increment 5000 = 20000 / 4
c [simplification-8] new conflict interval 17000
c [simplification-8] penalized conflict interval 17000 = 1 * 17000
c [simplification-8] hard conflict limit 54381 (soft 44381 + delta 10000)
c [simplification-8] new conflict limit 44381 (hard 54381)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   93.0   89036   626855     28170   23749   1144 218741   71   475   80  15%      6  341   67   19  355%
c i   93.1   89035   626855     28210   23783   1146 218742   71   474   80  15%      6  339   61   19  323%
c i   93.1   89034   626855     28211   23783   1146 218742   71   474   80  15%      6  339   61   19  322%
c i   94.9   89033   626855     29049   24545   1172 218755   73   462   80  16%      6  323   86   20  437%
c i   96.8   89032   626855     30008   25415   1190 218776   74   462   80  16%      7  319   81   21  396%
c i   96.8   89028   626855     30037   25440   1190 218777   75   462   80  16%      7  318   87   21  421%
c i   97.0   89027   626855     30088   25485   1190 218778   75   460   80  16%      6  316   85   21  410%
c i   97.2   89026   626855     30170   25553   1193 218786   74   460   80  16%      6  315   74   21  356%
c i   98.1   89022   626855     30615   25951   1204 218802   75   456   80  16%      5  309   82   21  388%
c i   98.1   89017   626855     30643   25977   1205 218802   75   454   80  16%      4  308   76   21  362%
c i   99.3   89016   626855     31074   26375   1219 218812   74   459   80  16%      4  311   76   21  355%
c i   99.5   89013   626855     31166   26461   1220 218813   74   458   80  16%      3  309   81   22  375%
c i   99.8   89012   626855     31294   26567   1232 218816   74   455   80  16%      3  306   78   22  359%
c i  100.2   89011   626855     31474   26737   1233 218817   75   464   80  16%      2  313   83   22  379%
c i  101.0   89010   626855     31806   27051   1234 218820   77   468   80  16%      2  316   99   22  446%
c i  101.1   89009   626855     31820   27063   1234 218820   77   468   80  16%      2  316   99   22  445%
c i  101.6   89008   626855     32103   27318   1239 218834   79   477   80  16%      2  323  109   23  483%
c i  101.7   89002   626855     32139   27348   1240 218837   78   477   80  16%      2  323  102   23  452%
c i  102.1   89001   626855     32269   27470   1243 218839   79   478   80  16%      1  323   95   23  417%
c i  103.1   88999   626855     32672   27836   1255 218850   80   486   80  16%      2  330   78   23  339%
c i  103.9   88996   626855     32964   28099   1265 218856   80   486   80  16%      1  328   85   23  362%
c i  104.5   88993   626855     33247   28347   1270 218875   81   490   80  16%      1  331   81   24  341%
c i  104.5   88989   626855     33250   28348   1271 218875   80   490   80  16%      1  331   80   24  337%
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  104.6   88984   626855     33255   28349   1273 218875   80   489   80  16%      1  330   79   24  332%
c i  104.6   88914   626855     33271   28364   1273 218875   80   488   80  16%      1  329   77   24  327%
c i  106.0   88913   626855     33956   28986   1287 218887   83   485   80  17%      3  323  100   24  410%
c i  106.3   88912   626855     34058   29079   1289 218890   84   491   80  17%      3  328  108   25  439%
c i  108.2   88911   626855     34938   29875   1305 218912   82   482   80  17%      5  315   83   25  327%
c i  108.8   88908   626855     35234   30150   1310 218912   84   479   81  18%      4  310   93   26  363%
c i  111.6   88841   626855     36442   31259   1332 218941   85   477   81  18%      8  302   76   27  283%
c i  111.6   88840   626855     36454   31269   1332 218942   85   475   81  18%      8  301   73   27  274%
c i  113.7   88836   626855     37401   32142   1353 218961   84   482   81  17%      7  304   90   28  326%
c i  114.4   88828   626855     37647   32369   1359 218964   90   494   81  18%      6  314  163   28  580%
c i  114.7   88819   626855     37749   32467   1359 218965   89   494   81  18%      5  313  131   28  464%
c i  116.1   88811   626855     38281   32949   1372 218980   88   486   81  18%      4  303   89   29  311%
c i  117.1   88804   626855     38732   33362   1379 218984   88   485   84  18%      3  301   93   29  321%
c i  117.2   88803   626855     38750   33372   1380 218986   88   484   84  18%      3  299   90   29  309%
c i  117.5   88802   626855     38895   33501   1385 218987   89   485   84  18%      3  299  113   29  388%
c i  118.0   88801   626855     39127   33714   1390 218992   88   481   84  18%      2  295   79   29  270%
c i  119.4   88800   626855     39825   34359   1397 218997   91   474   84  19%      3  285  110   30  365%
c i  122.0   88796   626855     40865   35305   1410 219023   93   494   88  19%      6  300   91   31  292%
c i  122.6   88792   626855     41134   35541   1415 219038   93   490   88  19%      5  295   87   32  276%
c i  123.0   88781   626855     41334   35721   1421 219042   92   488   88  19%      4  291   76   32  241%
c i  123.0   88779   626855     41335   35721   1421 219042   92   487   88  19%      4  291   76   32  240%
c i  123.0   88775   626855     41336   35721   1421 219042   92   487   88  19%      4  291   76   32  240%
c i  123.0   88767   626855     41337   35721   1421 219042   92   487   88  19%      4  291   75   32  239%
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i  123.1   88761   626855     41338   35721   1421 219042   92   487   88  19%      4  291   75   32  238%
c i  125.4   88755   626855     42266   36566   1430 219058   93   495   88  19%      5  294   97   33  297%
c i  126.1   88752   626855     42585   36851   1437 219070   94   499   88  19%      4  297  100   33  304%
c i  128.1   88552   626855     43428   37581   1452 219110   93   496   92  19%      5  290   71   34  211%
c i  128.1   88545   626855     43429   37581   1452 219110   93   496   92  19%      5  290   71   34  210%
c i  129.1   88538   626855     43805   37926   1458 219122   92   500   94  18%      4  292   77   34  228%
c i  129.1   88535   626855     43816   37935   1458 219123   92   499   94  18%      4  291   74   34  219%
c 
c [simplification-9] limit 44446 conflicts (hard 54381) hit after 44448 conflicts
c [quatres-4] found 43188 quaternary clauses 45% in total
c [quatres-4-1] removed 1 duplicate quaternary clauses
c [quatres-4-2] added 2 single-self-subsuming ternary resolvents
c [quatres-4-2] added 5 quaternary resolvents
c [ternres-4] limit 25862749 with penalty 0 = 0 + 0
c [ternres-4] 19289 schedulable variables 22%
c [ternres-4] 14 ternary resolvents (1 bin, 13 trn)
c [ternres-4] fully completed ternary resolution
c [decomp-20] removed 530 variables
c [simpleprobe-4] 12963 schedulable variables 15%
c [simpleprobe-4] limit 103450998 penalty 0 = 0 + 0
c [decomp-21] removed 668 variables
c [simpleprobe-4] fully completed simple probing
c [simpleprobe-4] removed 668 variables, found 80260 hbrs, 298 units
c [unhide-9] limit 1293137 with penalty 2 = 0 + 2
c [unhide-9-9] 7 units, 138 failed, 14396 tauts, 0 hbrs, 270688 literals
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 209 transitive binary clauses
c [transred-5] found 5 units
c [elim-7] scheduling all variables this time
c [elim-7] scheduled 87416 variables 100%
c [elim-7] limit of 258627496 steps penalty 1 = 1 + 0
c [elim-7] rescheduling of touched variables disabled
c [elim-7-1] eliminated 3761 variables 4% in round 1 in 60049742 steps
c [elim-7-1] backward subsumption/strengthening limit 60049700
c [elim-7-1-1] backward checking 11263 touched variables 13%
c [elim-7-1-1] fully completed backward checking in 1 rounds
c [elim-7-1] subsumed 6 and strengthened 380 clauses in 4020178 steps
c [elim-7-1] rescheduled 869 variables 1% by backward subsumption
c [elim-7-2] eliminated 133 variables 0% in round 2 in 1570199 steps
c [elim-7-2] backward subsumption/strengthening limit 1570100
c [elim-7-2-1] backward checking 974 touched variables 1%
c [elim-7-2-1] fully completed backward checking in 1 rounds
c [elim-7-2] subsumed 9 and strengthened 6 clauses in 604135 steps
c [elim-7-2] rescheduled 35 variables 0% by backward subsumption
c [elim-7-3] eliminated 5 variables 0% in round 3 in 35427 steps
c [elim-7-3] backward subsumption/strengthening limit 35400
c [elim-7-3-1] backward checking 43 touched variables 0%
c [elim-7-3-1] incomplete backward checking 0 remain 0%
c [elim-7-3] subsumed 3 and strengthened 6 clauses in 35401 steps
c [elim-7] incomplete 27 not tried 0% in round 3
c [elim-7] transition to [ all 1 rem 1 ] state
c [elim-7] eliminated 3908 = 4% variables out of 87416 scheduled
c [bca-5] limit of 10000000 steps and 1195365 added (scaled 2)
c [bca-5] 135935 out of 167018 literals actually usable 81%
c [bca-5] added 92 blocked clauses in 391377 steps
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 77588240 penalty 0 = 0 + 0
c [sweep-5-1] 4403 pos 5.3% + 78056 neg 94.7% = 82459 sched 98.7% ret 1049
c [sweep-5-1] 77866792 steps 777 queries 738.10 avg class size
c [sweep-5-1] 10215 decisions 679 SAT calls 141.35 avg env size
c [sweep-5-1] 54683 variables remain 66% (28363 retained 34%)
c [decomp-22] removed 1103 variables
c [sweep-5-1] removed 1103 vars (0 failed, 120 eqs, 208 impls)
c [sweep-5] considered successful since not run to completion yet
c [sweep-5] removed 1103 vars in TOTAL (1 rounds, 776 queries)
c [phase-count-9] 586451 negative 99.1% of 592015 except 5564 0.9%
c [phase-count-9] 484030 positive 81.8% of 592015 except 107985 18.2%
c [phase-count-9] less non-negative clauses 5564 than limit 59200 (10.0%)
c [phase-count-9] non-pos/non-neg = 107985/5564 = 19.41 >= 2.00 = 200/100
c [lucky-phase-9] forcing lucky phase -1
c [phase-9] phase bias: 0 positive 0%, 143 negative 100%
c [sort-queue-9] sorted 30082 enqueued variables after 44448 conflicts
c [score-dist-9] active 52323 (63%), one 0 (0%), zero 30082 (37%)
c [score-dist-9] max exp 517, different 14 (3%)
c [score-dist-9] median active exp 517, avg 516.4
c [simplification-9] removed 6130 variables 6.9% (82405 remain 33%)
c [simplification-9] removed 34840 irredundant clauses 5.6% (592015 remain 43%)
c [simplification-9] maximum reduction of 7% = max (7%, 6%)
c [simplification-9] large reduction 7% >= 5% limit
c [simplification-9] next conflict interval 2000 = 2000/1
c [simplification-9] penalized conflict interval 2000 = 1 * 2000
c [simplification-9] hard conflict limit 56448 (soft 46448 + delta 10000)
c [simplification-9] new conflict limit 46448 (hard 56448)
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  143.2   82404   592015     44670   22748   1290 353649   94   498   75  19%      5  287  103   35  297%
c i  143.7   82403   592015     44916   22978   1291 353651   94   502   75  19%      4  289   95   35  271%
c i  143.7   82399   592015     44917   22978   1291 353651   93   502   75  19%      4  289   94   35  270%
c i  143.7   82395   592015     44918   22978   1291 353651   93   501   75  19%      4  289   94   35  269%
c i  143.7   82372   592015     44919   22978   1291 353651   93   501   75  19%      4  289   94   35  268%
c i  143.7   82368   592015     44920   22978   1291 353651   93   501   75  19%      4  289   93   35  267%
c i  143.7   82360   592015     44921   22978   1291 353651   93   501   75  19%      4  289   93   35  266%
c i  143.7   82356   592015     44922   22978   1291 353651   93   501   75  19%      4  288   93   35  265%
c i  143.7   82352   592015     44923   22978   1291 353651   93   501   75  19%      4  288   92   35  264%
c i  143.7   82348   592015     44924   22978   1291 353651   93   501   75  19%      4  288   92   35  263%
c i  143.8   82342   592015     44942   22993   1291 353652   93   502   75  19%      4  289   89   35  254%
c i  144.1   82341   592015     45068   23108   1292 353656   93   504   75  19%      3  290   94   35  269%
c i  144.1   82336   592015     45084   23123   1292 353656   93   503   75  19%      3  289   91   35  259%
c i  144.1   82335   592015     45085   23123   1292 353656   93   502   75  19%      3  289   91   35  258%
c i  145.5   82334   592015     45661   23644   1310 353675   89   507   75  17%      3  291   62   35  175%
c i  145.6   82333   592015     45718   23695   1311 353675   89   506   75  17%      3  290   64   35  181%
c i  146.0   82330   592015     45892   23849   1315 353683   87   502   75  17%      2  285   61   35  171%
c i  146.9   82329   592015     46362   24258   1321 353688   92   497   75  18%      2  278  113   36  313%
c i  146.9   82327   592015     46363   24258   1321 353688   92   497   75  18%      2  278  113   36  312%
c i  146.9   82323   592015     46364   24258   1321 353688   92   496   75  18%      2  278  112   36  311%
c 
c [simplification-10] limit 46558 conflicts (hard 56448) hit after 46558 conflicts
c [quatres-5] found 40639 quaternary clauses 44% in total
c [quatres-5-2] added 53 quaternary resolvents
c [ternres-5] limit 27047776 with penalty 0 = 0 + 0
c [ternres-5] all 82319 free variables schedulable
c [ternres-5] 191 ternary resolvents (1 bin, 190 trn)
c [ternres-5] fully completed ternary resolution
c [card-4] limit 1690486 penalty 3 = 3 + 0
c [card-4] found 3301 at-most-one constraints of average size 4.1
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 1690486 for elimination
c [card-4] 3301 out of 3301 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [gauss-4] limit 2704777 penalty 1 = 1 + 0
c [gauss-4] extracted 45 xors of average arity 2.8
c [gauss-4] connected 127 occurrences of 122 variables (average 1.0)
c [gauss-4] limit 2704777 penalty 1 = 1 + 0
c [gauss-4] fully completed
c [gauss-4] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-23] removed 20 variables
c [treelook-4] limit 2704777 penalty 0 = 0 + 0 boost 1
c [treelook-4] scheduled 144415 literals 88%
c [treelook-4] scheduling used 2331573 steps
c [treelook-4] scheduled completely
c [treelook-4] limit 2704777 penalty 0 = 0 + 0 boost 1
c [treelook-4] used 3049092 steps
c [treelook-4] 144388 literals remain 88%
c [treelook-4] 37444 variables remain to probed next time 46%
c [treelook-4] removed 9 variables, found 1374 hbrs
c [unhide-10] limit 2704777 with penalty 1 = 0 + 1
c [unhide-10-10] 10 units, 506 failed, 45707 tauts, 0 hbrs, 68110 literals
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 183 transitive binary clauses
c [cce-3] limit of 33809720 steps penalty 2 = 2 + 0
c [cce-3-1] eliminated 40 clauses out of 809 (5%) of length 7
c [cce-3-1] eliminated 2935 clauses out of 5188 (57%) of length 6
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 2975 large clauses in 33809728 steps
c [cce-3-1] allowing another 16904864 steps for small clauses
c [cce-3-1] scheduling 478804 clauses = 270449 binary + 208355 ternary
c [cce-3-1] tried to eliminate 230 small clauses 0%
c [cce-3-1] eliminated 27 binary clauses 0%
c [cce-3-1] eliminated 6 ternary clauses 0%
c [cce-3-1] eliminated 33 small clauses 0%
c [cce-3-1] eliminated 6964 small clauses in 33809724 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 9939 covered clauses in round 1
c [cce-3] eliminated 9939 covered clauses in TOTAL during 1 rounds
c [elim-8] no untried remaining variables left
c [elim-8] scheduled 81509 variables 100%
c [elim-8] boosting limit by 20
c [elim-8] limit of 10819110660 steps penalty 0 = 0 + 0
c [elim-8] rescheduling of touched variables disabled
c [elim-8-1] eliminated 2061 variables 3% in round 1 in 60078659 steps
c [elim-8-1] backward subsumption/strengthening limit 60078600
c [elim-8-1-1] backward checking 6710 touched variables 8%
c [elim-8-1-1] fully completed backward checking in 1 rounds
c [elim-8-1] subsumed 15 and strengthened 191 clauses in 3023957 steps
c [elim-8-1] rescheduled 474 variables 1% by backward subsumption
c [elim-8-2] eliminated 68 variables 0% in round 2 in 1571878 steps
c [elim-8-2] backward subsumption/strengthening limit 1571800
c [elim-8-2-1] backward checking 538 touched variables 1%
c [elim-8-2-1] fully completed backward checking in 1 rounds
c [elim-8-2] subsumed 4 and strengthened 13 clauses in 384811 steps
c [elim-8-2] rescheduled 58 variables 0% by backward subsumption
c [elim-8-3] eliminated 9 variables 0% in round 3 in 56813 steps
c [elim-8-3] backward subsumption/strengthening limit 56800
c [elim-8-3-1] backward checking 86 touched variables 0%
c [elim-8-3-1] incomplete backward checking 0 remain 0%
c [elim-8-3] subsumed 15 and strengthened 11 clauses in 56801 steps
c [elim-8] incomplete 95 not tried 0% in round 3
c [elim-8] transition to [ all 1 rem 1 ] state
c [elim-8] eliminated 2147 = 3% variables out of 81509 scheduled
c [bca-6] limit of 10000000 steps and 1147023 added (scaled 2)
c [bca-6] 130308 out of 158726 literals actually usable 82%
c [bca-6] added 185 blocked clauses in 373610 steps
c [sweep-6] limit 8114333 penalty 0 = 0 + 0
c [sweep-6-1] 3781 pos 7.2% + 48559 neg 92.8% = 52340 sched 66.0% ret 27022
c [sweep-6-1] 8143719 steps 98 queries 4281.44 avg class size
c [sweep-6-1] 1837 decisions 87 SAT calls 162.01 avg env size
c [sweep-6-1] 51428 variables remain 65% (27928 retained 35%)
c [decomp-25] removed 52 variables
c [sweep-6-1] removed 52 vars (0 failed, 11 eqs, 23 impls)
c [sweep-6] considered successful since not run to completion yet
c [sweep-6] removed 52 vars in TOTAL (1 rounds, 97 queries)
c [phase-count-10] 570530 negative 99.6% of 572996 except 2466 0.4%
c [phase-count-10] 466271 positive 81.4% of 572996 except 106725 18.6%
c [phase-count-10] less non-negative clauses 2466 than limit 57200 (10.0%)
c [phase-count-10] non-pos/non-neg = 106725/2466 = 43.28 >= 2.00 = 200/100
c [lucky-phase-10] forcing lucky phase -1
c [phase-10] phase bias: 0 positive 0%, 142 negative 100%
c [sort-queue-10] sorted 27949 enqueued variables after 46558 conflicts
c [score-dist-10] active 51361 (65%), one 0 (0%), zero 27949 (35%)
c [score-dist-10] max exp 517, different 14 (3%)
c [score-dist-10] median active exp 517, avg 516.4
c [simplification-10] removed 3009 variables 3.7% (79310 remain 32%)
c [simplification-10] removed 19019 irredundant clauses 3.2% (572996 remain 42%)
c [simplification-10] maximum reduction of 4% = max (4%, 3%)
c [simplification-10] geometric conflict interval increment 4000 = 20000 / 5
c [simplification-10] new conflict interval 21000
c [simplification-10] penalized conflict interval 21000 = 1 * 21000
c [simplification-10] hard conflict limit 78058 (soft 67558 + delta 10500)
c [simplification-10] new conflict limit 67558 (hard 78058)
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  154.7   79309   572996     46740   19189   1376 295161   91   502   70  18%      2  281   92   36  252%
c i  154.7   79305   572996     46741   19189   1376 295161   91   501   70  18%      2  281   91   36  251%
c i  155.1   79300   572996     46937   19354   1382 295175   90   502   70  18%      1  281   75   36  205%
c i  155.2   79299   572996     46973   19381   1383 295176   89   499   70  18%      1  278   69   36  189%
c i  155.6   79296   572996     47131   19523   1387 295181   87   496   70  18%      1  274   56   36  153%
c i  155.6   79289   572996     47145   19536   1387 295181   87   495   70  18%      1  273   54   36  149%
c i  155.6   79288   572996     47146   19536   1387 295181   87   495   70  18%      1  272   54   36  148%
c i  155.7   79287   572996     47231   19612   1389 295182   87   493   70  18%      1  270   56   36  153%
c i  155.8   79282   572996     47258   19635   1389 295183   87   493   70  18%      1  270   69   37  189%
c i  155.8   79281   572996     47259   19635   1389 295183   87   493   70  18%      1  270   69   37  188%
c i  156.0   79280   572996     47340   19712   1389 295183   87   494   70  18%      0  271   71   37  194%
c i  156.2   79279   572996     47470   19817   1396 295189   85   485   70  18%      0  261   55   37  151%
c i  156.4   79278   572996     47542   19883   1397 295189   86   487   70  18%      0  264   68   37  187%
c i  156.8   79277   572996     47723   20045   1398 295195   85   485   70  18%      0  261   67   37  184%
c i  157.0   79276   572996     47817   20133   1399 295198   84   483   70  17%     -0  258   62   37  168%
c i  157.0   79275   572996     47844   20154   1399 295200   84   483   70  17%     -0  258   62   37  169%
c i  157.0   79272   572996     47845   20154   1399 295200   84   483   70  17%     -0  258   62   37  168%
c i  158.8   79270   572996     48724   20950   1409 295228   80   475   70  17%      3  247   58   37  157%
c i  160.1   79235   572996     49395   21554   1426 295250   76   461   70  16%      3  230   50   37  133%
c i  160.3   79228   572996     49525   21672   1432 295255   75   457   70  16%      3  226   49   37  132%
c i  161.0   79224   572996     49852   21967   1437 295261   77   461   70  17%      2  228   85   38  227%
c i  161.2   79223   572996     49929   22036   1439 295264   76   462   70  17%      2  229   81   38  216%
c i  161.5   79222   572996     50132   22222   1442 295271   76   463   70  16%      1  230   67   38  179%
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  162.0   79220   572996     50462   22515   1448 295279   76   463   70  16%      1  229   70   38  186%
c i  162.1   79214   572996     50485   22536   1449 295279   76   464   70  16%      1  229   72   38  191%
c i  162.8   79213   572996     50885   22904   1455 295289   77   465   70  17%      1  229   93   38  244%
c i  162.9   79207   572996     50965   22980   1455 295290   77   472   70  16%      1  236   92   38  241%
c i  163.2   79206   572996     51235   23226   1459 295295   75   460   70  16%      1  222   63   38  166%
c i  163.7   79204   572996     51534   23498   1467 295303   74   451   70  16%      1  213   54   38  140%
c i  163.7   79198   572996     51535   23498   1467 295303   74   451   70  16%      1  213   53   38  139%
c i  164.3   79194   572996     51937   23875   1471 295305   78   478   70  16%      1  239   97   39  250%
c i  164.4   79193   572996     51980   23914   1471 295307   78   478   70  16%      1  238   86   39  222%
c i  164.5   79192   572996     52050   23979   1473 295308   77   475   70  16%      1  235   71   39  184%
c i  164.8   79187   572996     52247   24154   1478 295318   75   470   70  16%      0  229   61   39  156%
c i  165.4   79186   572996     52623   24488   1480 295327   74   470   70  16%      0  228   59   39  151%
c i  165.4   79180   572996     52624   24488   1480 295327   74   470   70  16%      0  228   59   39  151%
c i  165.7   79169   572996     52808   24659   1480 295329   76   476   71  16%      0  233   86   39  219%
c i  166.1   79166   572996     53067   24886   1483 295336   76   467   71  16%      0  224   78   39  199%
c i  167.7   79162   572996     54023   25738   1504 295350   75   455   71  17%      4  208   72   40  182%
c i  168.1   79156   572996     54322   26016   1511 295355   74   449   71  17%      3  202   68   40  170%
c i  168.1   79130   572996     54323   26016   1511 295355   74   449   71  17%      3  202   68   40  170%
c i  168.8   79056   572996     54663   26301   1516 295366   77   453   71  17%      2  205  103   40  257%
c i  168.8   79055   572996     54677   26313   1516 295366   77   453   71  17%      2  205  106   40  263%
c i  168.8   79052   572996     54721   26350   1517 295369   78   454   71  17%      2  206  112   40  277%
c i  169.0   79047   572996     54805   26429   1517 295372   78   457   71  17%      2  208   98   40  243%
c i  169.4   79044   572996     55043   26655   1518 295373   77   455   72  17%      1  206   80   40  197%
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  169.4   78950   572996     55066   26674   1518 295374   77   455   72  17%      1  205   74   40  182%
c i  169.4   78943   572996     55075   26679   1518 295374   76   454   72  17%      1  204   72   40  177%
c i  169.5   78942   572996     55140   26737   1518 295374   76   450   72  17%      1  200   66   40  164%
c i  169.7   78939   572996     55207   26801   1519 295375   75   447   74  17%      1  197   58   40  144%
c i  169.7   78935   572996     55255   26839   1519 295377   76   448   74  17%      1  198   64   41  158%
c i  170.3   78934   572996     55594   27151   1526 295380   74   444   74  17%      1  193   64   41  158%
c i  170.9   78930   572996     55885   27417   1532 295384   76   449   74  17%      1  196   95   41  232%
c i  171.1   78928   572996     56033   27552   1533 295387   77   453   74  17%      0  201  101   41  246%
c i  171.3   78925   572996     56106   27621   1533 295387   78   456   74  17%      0  203  103   41  251%
c i  171.5   78924   572996     56243   27747   1535 295389   78   454   75  17%      0  200  101   41  246%
c i  173.3   78923   572996     57310   28711   1551 295397   85   474   80  18%      5  218   88   42  207%
c i  175.3   78922   572996     58360   29675   1564 295417   86   493   82  18%      6  232  104   43  243%
c i  175.4   78921   572996     58441   29749   1565 295420   87   496   82  17%      6  235  103   43  239%
c i  175.9   78920   572996     58707   29988   1569 295425   85   495   82  17%      4  234   79   43  184%
c i  175.9   78916   572996     58710   29989   1569 295425   85   495   82  17%      4  234   79   43  182%
c i  176.0   78915   572996     58711   29989   1569 295425   85   495   82  17%      4  233   78   43  182%
c i  176.0   78911   572996     58712   29989   1569 295425   85   495   82  17%      4  233   78   43  181%
c i  176.0   78908   572996     58713   29989   1569 295425   85   495   82  17%      4  233   78   43  180%
c i  176.0   78904   572996     58714   29989   1569 295425   85   495   82  17%      4  233   78   43  179%
c i  176.0   78902   572996     58715   29989   1569 295425   85   495   82  17%      4  233   77   43  179%
c i  176.0   78897   572996     58716   29989   1569 295425   85   494   82  17%      4  233   77   43  178%
c i  176.0   78895   572996     58719   29991   1569 295425   85   494   82  17%      4  233   76   43  176%
c i  178.1   78892   572996     60004   31152   1584 295449   85   480   84  18%      8  214   83   44  188%
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  179.0   78889   572996     60468   31565   1587 295466   91   489   84  19%      6  222  129   45  288%
c i  180.4   78888   572996     61263   32293   1593 295477   94   509   85  19%      5  239  128   45  281%
c i  180.6   78887   572996     61335   32358   1593 295477   96   511   85  19%      4  240  139   46  304%
c i  181.2   78882   572996     61739   32715   1602 295483   94   504   86  19%      3  232   84   46  184%
c i  181.6   78881   572996     62030   32970   1607 295490   95   504   86  19%      2  231   95   46  206%
c i  181.7   78875   572996     62053   32992   1607 295490   95   503   86  19%      2  230   89   46  193%
c i  182.2   78874   572996     62388   33283   1609 295493   96   495   86  19%      2  221   94   46  204%
c i  183.3   78873   572996     63065   33879   1634 295511   96   495   86  19%      2  219   97   47  206%
c i  184.1   78872   572996     63505   34282   1639 295514   99   519   86  19%      2  241  110   47  232%
c i  184.6   78866   572996     63807   34554   1645 295520   99   523   86  19%      1  244  104   48  218%
c i  185.2   78865   572996     64123   34836   1651 295529   98   519   87  19%      1  238  101   48  210%
c i  185.3   78862   572996     64216   34912   1653 295530   99   513   87  19%      1  233  108   48  225%
c i  185.9   78855   572996     64534   35202   1655 295537  100   520   89  19%      1  238  111   48  231%
c i  187.6   78824   572996     65501   36045   1674 295546  107   527   89  20%      4  241  153   50  309%
c i  188.3   78823   572996     65866   36378   1676 295551  109   525   92  21%      3  238  149   50  297%
c i  190.3   78818   572996     66907   37309   1689 295565  110   512   92  21%      5  222  119   51  233%
c i  190.5   78817   572996     67056   37439   1692 295568  109   515   92  21%      4  224  106   51  208%
c i  191.2   78810   572996     67410   37770   1694 295576  108   520   92  21%      3  228   90   51  175%
c 
c [simplification-11] limit 67695 conflicts (hard 78058) hit after 67696 conflicts
c [quatres-6] found 36246 quaternary clauses 44% in total
c [quatres-6-2] added 1 single-self-subsuming ternary resolvents
c [quatres-6-2] added 7 quaternary resolvents
c [ternres-6] limit 36419258 with penalty 0 = 0 + 0
c [ternres-6] all 78775 free variables schedulable
c [ternres-6] 182 ternary resolvents (0 bin, 182 trn)
c [ternres-6] fully completed ternary resolution
c [decomp-26] removed 611 variables
c [basicprobe-4] limit 182096293 penalty 0 = 0 + 0
c [basicprobe-4-0] 21145 probes remain 27% after last round
c [basicprobe-4-0] 869 units = 856 failed (99%) + 13 lifted (1%)
c [basicprobe-4-0] removed 1805 variables, found 392569 hbrs
c [bate-2] eliminated 447 asymmetric tautologies during probing
c [unhide-11] limit 1820962 with penalty 2 = 0 + 2
c [unhide-11-11] 14 units, 159 failed, 8668 tauts, 0 hbrs, 379699 literals
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 231 transitive binary clauses
c [transred-7] found 2 units
c [block-4] scheduling all variables this time
c [block-4] scheduled 76688 variables 100%
c [block-4] limit of 91048146 steps penalty 2 = 2 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 103 blocked clauses
c [block-4] 103 < 1/100 * 550415 = 5504 considered unsuccessful
c [elim-9] no untried remaining variables left
c [elim-9] scheduled 76686 variables 100%
c [elim-9] limit of 728385173 steps penalty 0 = 0 + 0
c [elim-9] rescheduling of touched variables disabled
c [elim-9-1] eliminated 2253 variables 3% in round 1 in 54307463 steps
c [elim-9-1] backward subsumption/strengthening limit 54307400
c [elim-9-1-1] backward checking 8011 touched variables 10%
c [elim-9-1-1] fully completed backward checking in 1 rounds
c [elim-9-1] subsumed 52 and strengthened 313 clauses in 2794387 steps
c [elim-9-1] rescheduled 809 variables 1% by backward subsumption
c [elim-9-2] eliminated 111 variables 0% in round 2 in 1072152 steps
c [elim-9-2] backward subsumption/strengthening limit 1072100
c [elim-9-2-1] backward checking 844 touched variables 1%
c [elim-9-2-1] fully completed backward checking in 1 rounds
c [elim-9-2] subsumed 31 and strengthened 20 clauses in 464926 steps
c [elim-9-2] rescheduled 107 variables 0% by backward subsumption
c [elim-9-3] eliminated 14 variables 0% in round 3 in 124191 steps
c [elim-9-3] backward subsumption/strengthening limit 124100
c [elim-9-3-1] backward checking 146 touched variables 0%
c [elim-9-3-1] incomplete backward checking 0 remain 0%
c [elim-9-3] subsumed 18 and strengthened 13 clauses in 124101 steps
c [elim-9] incomplete 75 not tried 0% in round 3
c [gc-75] reconnected 661557 binary clauses (produced 0 empty 1 units)
c [elim-9] transition to [ all 1 rem 1 ] state
c [elim-9] eliminated 2393 = 3% variables out of 76686 scheduled
c [bca-7] limit of 10000000 steps and 1082348 added (scaled 2)
c [bca-7] 119547 out of 148588 literals actually usable 80%
c [bca-7] added 54 blocked clauses in 339227 steps
c [sweep-7] limit 10925777 penalty 0 = 0 + 0
c [sweep-7-1] 3607 pos 7.4% + 45029 neg 92.6% = 48636 sched 65.5% ret 25657
c [sweep-7-1] 10942925 steps 131 queries 3349.48 avg class size
c [sweep-7-1] 1941 decisions 118 SAT calls 197.65 avg env size
c [sweep-7-1] 47056 variables remain 63% (27171 retained 37%)
c [decomp-27] removed 149 variables
c [sweep-7-1] removed 149 vars (0 failed, 15 eqs, 31 impls)
c [sweep-7] removed 149 vars in TOTAL (1 rounds, 130 queries)
c [phase-count-11] 537880 negative 99.6% of 540156 except 2276 0.4%
c [phase-count-11] 439408 positive 81.3% of 540156 except 100748 18.7%
c [phase-count-11] skipping relative phase luck test
c [phase-11] phase bias: 15 positive 100%, 0 negative 0%
c [sort-queue-11] sorted 24150 enqueued variables after 67696 conflicts
c [score-dist-11] active 49994 (67%), one 0 (0%), zero 24150 (33%)
c [score-dist-11] max exp 518, different 14 (3%)
c [score-dist-11] median active exp 518, avg 517.2
c [simplification-11] removed 4631 variables 5.9% (74144 remain 30%)
c [simplification-11] removed 32840 irredundant clauses 5.7% (540156 remain 39%)
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 79696 (soft 69696 + delta 10000)
c [simplification-11] new conflict limit 69696 (hard 79696)
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  207.6   74143   540156     67728   21521   1850 646048  104   505   78  21%      2  212   71   51  138%
c i  207.8   74140   540156     67830   21615   1852 646048  103   501   79  21%      2  207   63   51  123%
c i  207.9   74137   540156     67978   21742   1853 646048  102   498   79  21%      1  204   79   51  153%
c i  208.3   74136   540156     68172   21915   1856 646050  101   496   79  20%      1  202   73   51  142%
c i  208.3   74130   540156     68176   21918   1856 646050  101   496   79  20%      1  201   73   51  141%
c i  208.6   74128   540156     68347   22077   1857 646056  100   499   79  20%      1  204   82   52  159%
c i  208.9   74127   540156     68510   22232   1859 646058   98   498   79  20%      0  202   62   52  120%
c 
c [simplification-12] limit 69698 conflicts (hard 79696) hit after 69698 conflicts
c [quatres-7] found 34350 quaternary clauses 45% in total
c [quatres-7-2] added 8 quaternary resolvents
c [ternres-7] limit 37115735 with penalty 0 = 0 + 0
c [ternres-7] all 74074 free variables schedulable
c [ternres-7] 419 ternary resolvents (0 bin, 419 trn)
c [ternres-7] fully completed ternary resolution
c [decomp-28] removed 73 variables
c [simpleprobe-5] all 74071 free variables schedulable
c [simpleprobe-5] limit 148462941 penalty 0 = 0 + 0
c [decomp-29] removed 1229 variables
c [simpleprobe-5] fully completed simple probing
c [simpleprobe-5] removed 1229 variables, found 93739 hbrs, 678 units
c [unhide-12] limit 3711573 with penalty 1 = 0 + 1
c [unhide-12-12] 2 units, 211 failed, 105579 tauts, 0 hbrs, 67783 literals
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 223 transitive binary clauses
c [transred-8] found 1 units
c [cce-4] boosting limit by 10
c [cce-4] limit of 927893385 steps penalty 1 = 1 + 0
c [cce-4-1] eliminated 2 clauses out of 136 (1%) of length 10
c [cce-4-1] eliminated 1 clauses out of 477 (0%) of length 8
c [cce-4-1] eliminated 8 clauses out of 716 (1%) of length 7
c [cce-4-1] eliminated 65 clauses out of 2233 (3%) of length 6
c [cce-4-1] eliminated 22344 clauses out of 33063 (68%) of length 5
c [cce-4-1] eliminated 17747 clauses out of 32268 (55%) of length 4
c [cce-4-1] completed large round (ATE)
c [cce-4-1] eliminated 40167 large clauses in 748630185 steps
c [cce-4-1] allowing another 374315092 steps for small clauses
c [cce-4-1] scheduling 268143 clauses = 245639 binary + 22504 ternary
c [cce-4-1] tried to eliminate 23463 small clauses 9%
c [cce-4-1] eliminated 5774 binary clauses 2%
c [cce-4-1] eliminated 1080 ternary clauses 5%
c [cce-4-1] eliminated 6854 small clauses 3%
c [cce-4-1] eliminated 8143 small clauses in 927893395 steps
c [cce-4-1] incomplete small round (ATE)
c [cce-4-1] eliminated 48310 covered clauses in round 1
c [cce-4] eliminated 48310 covered clauses in TOTAL during 1 rounds
c [elim-10] no untried remaining variables left
c [elim-10] scheduled 72723 variables 100%
c [elim-10] limit of 742314709 steps penalty 0 = 0 + 0
c [elim-10] rescheduling of touched variables disabled
c [elim-10-1] eliminated 16271 variables 22% in round 1 in 44876724 steps
c [elim-10-1] backward subsumption/strengthening limit 44876700
c [elim-10-1-1] backward checking 35856 touched variables 49%
c [elim-10-1-1] fully completed backward checking in 1 rounds
c [elim-10-1] subsumed 28 and strengthened 52 clauses in 5403498 steps
c [elim-10-1] rescheduled 180 variables 0% by backward subsumption
c [elim-10-2] eliminated 10 variables 0% in round 2 in 132577 steps
c [elim-10-2] backward subsumption/strengthening limit 132500
c [elim-10-2-1] backward checking 131 touched variables 0%
c [elim-10-2-1] incomplete backward checking 0 remain 0%
c [elim-10-2] subsumed 4 and strengthened 11 clauses in 132501 steps
c [elim-10-2] rescheduled 49 variables 0% by backward subsumption
c [elim-10-3] eliminated 3 variables 0% in round 3 in 115411 steps
c [elim-10-3] backward subsumption/strengthening limit 115400
c [elim-10-3-1] backward checking 43 touched variables 0%
c [elim-10-3-1] incomplete backward checking 0 remain 0%
c [elim-10-3] subsumed 0 and strengthened 6 clauses in 115401 steps
c [elim-10] incomplete 24 not tried 0% in round 3
c [elim-10] transition to [ all 1 rem 1 ] state
c [elim-10] eliminated 16284 = 22% variables out of 72723 scheduled
c [bca-8] limit of 10000000 steps and 888547 added (scaled 2)
c [bca-8] 100559 out of 112880 literals actually usable 89%
c [bca-8] added 298 blocked clauses in 235289 steps
c [sweep-8] limit 11134720 penalty 0 = 0 + 0
c [sweep-8-1] 3819 pos 9.9% + 34601 neg 90.1% = 38420 sched 68.1% ret 18019
c [sweep-8-1] 11148868 steps 192 queries 2156.41 avg class size
c [sweep-8-1] 2832 decisions 179 SAT calls 102.54 avg env size
c [sweep-8-1] 36104 variables remain 64% (20133 retained 36%)
c [decomp-30] removed 281 variables
c [sweep-8-1] removed 281 vars (0 failed, 14 eqs, 27 impls)
c [sweep-8] removed 281 vars in TOTAL (1 rounds, 191 queries)
c [phase-count-12] 441564 negative 99.8% of 442515 except 951 0.2%
c [phase-count-12] 348656 positive 78.8% of 442515 except 93859 21.2%
c [phase-count-12] skipping relative phase luck test
c [phase-12] phase bias: 0 positive 0%, 8 negative 100%
c [sort-queue-12] sorted 17464 enqueued variables after 69698 conflicts
c [score-dist-12] active 38694 (69%), one 0 (0%), zero 17464 (31%)
c [score-dist-12] max exp 518, different 14 (3%)
c [score-dist-12] median active exp 518, avg 517.4
c [simplification-12] removed 17916 variables 24.2% (56158 remain 23%)
c [simplification-12] removed 97641 irredundant clauses 18.1% (442515 remain 32%)
c [simplification-12] maximum reduction of 24% = max (24%, 18%)
c [simplification-12] large reduction 24% >= 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 81698 (soft 71698 + delta 10000)
c [simplification-12] new conflict limit 71698 (hard 81698)
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  245.3   56157   442515     70005    5349   2890 541734   87   499   54  17%      9  199   47   52   90%
c i  245.8   56156   442515     70589    5867   2906 541748   83   518   54  16%      6  216   65   52  126%
c i  246.1   56150   442515     71011    6239   2912 541753   80   509   55  16%      4  206   63   52  122%
c i  246.2   56147   442515     71120    6335   2913 541754   80   518   55  15%      3  215   66   52  127%
c i  246.6   56144   442515     71625    6764   2919 541761   77   488   55  16%      3  183   75   52  145%
c 
c [simplification-13] limit 71698 conflicts (hard 81698) hit after 71698 conflicts
c [quatres-8] found 23785 quaternary clauses 55% in total
c [quatres-8-1] removed 4 duplicate quaternary clauses
c [quatres-8-2] added 12 quaternary resolvents
c [ternres-8] limit 37633882 with penalty 0 = 0 + 0
c [ternres-8] all 56143 free variables schedulable
c [ternres-8] 468 ternary resolvents (0 bin, 468 trn)
c [ternres-8] fully completed ternary resolution
c [gauss-5] limit 1881694 penalty 2 = 2 + 0
c [gauss-5] extracted 16 xors of average arity 2.9
c [gauss-5] connected 46 occurrences of 46 variables (average 1.0)
c [gauss-5] limit 1881694 penalty 2 = 2 + 0
c [gauss-5] fully completed
c [gauss-5] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-31] removed 4 variables
c [treelook-5] limit 3763388 penalty 0 = 0 + 0 boost 1
c [treelook-5] scheduled 90478 literals 81%
c [treelook-5] scheduling used 2015219 steps
c [treelook-5] scheduled completely
c [treelook-5] limit 3763388 penalty 0 = 0 + 0 boost 1
c [treelook-5] used 3843310 steps
c [treelook-5] 90413 literals remain 81%
c [treelook-5] 21551 variables remain to probed next time 38%
c [treelook-5] removed 4 variables, found 12755 hbrs
c [unhide-13] limit 7526776 with penalty 0 = 0 + 0
c [unhide-13-16] 8 units, 543 failed, 69257 tauts, 0 hbrs, 35652 literals
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 170 transitive binary clauses
c [cce-5] limit of 188169413 steps penalty 0 = 0 + 0
c [cce-5-1] eliminated 2 clauses out of 3 (67%) of length 9
c [cce-5-1] eliminated 4 clauses out of 45 (9%) of length 7
c [cce-5-1] eliminated 391 clauses out of 3274 (12%) of length 6
c [cce-5-1] eliminated 1912 clauses out of 13951 (14%) of length 5
c [cce-5-1] incomplete large round (ACCE)
c [cce-5-1] eliminated 2309 large clauses in 188169430 steps
c [cce-5-1] allowing another 94084715 steps for small clauses
c [cce-5-1] scheduling 371961 clauses = 185852 binary + 186109 ternary
c [cce-5-1] tried to eliminate 1961 small clauses 1%
c [cce-5-1] eliminated 275 binary clauses 0%
c [cce-5-1] eliminated 91 ternary clauses 0%
c [cce-5-1] eliminated 366 small clauses 0%
c [cce-5-1] eliminated 916 small clauses in 188169424 steps
c [cce-5-1] incomplete small round (ACCE)
c [cce-5-1] eliminated 3225 covered clauses in round 1
c [cce-5] eliminated 3225 covered clauses in TOTAL during 1 rounds
c [cce-5] 3225 < 1/100 * 433263 = 4332 considered unsuccessful
c [elim-11] no untried remaining variables left
c [elim-11] scheduled 55839 variables 100%
c [elim-11] limit of 752677655 steps penalty 0 = 0 + 0
c [elim-11] rescheduling of touched variables disabled
c [elim-11-1] eliminated 434 variables 1% in round 1 in 40090888 steps
c [elim-11-1] backward subsumption/strengthening limit 40090800
c [elim-11-1-1] backward checking 3057 touched variables 5%
c [elim-11-1-1] fully completed backward checking in 1 rounds
c [elim-11-1] subsumed 10 and strengthened 19 clauses in 973035 steps
c [elim-11-1] rescheduled 76 variables 0% by backward subsumption
c [elim-11-2] eliminated 5 variables 0% in round 2 in 87974 steps
c [elim-11-2] backward subsumption/strengthening limit 87900
c [elim-11-2-1] backward checking 63 touched variables 0%
c [elim-11-2-1] fully completed backward checking in 1 rounds
c [elim-11-2] subsumed 0 and strengthened 4 clauses in 78083 steps
c [elim-11-2] rescheduled 16 variables 0% by backward subsumption
c [elim-11-3] eliminated 1 variables 0% in round 3 in 18722 steps
c [elim-11-3] backward subsumption/strengthening limit 18700
c [elim-11-3-1] backward checking 12 touched variables 0%
c [elim-11-3-1] incomplete backward checking 0 remain 0%
c [elim-11-3] subsumed 0 and strengthened 2 clauses in 18701 steps
c [elim-11] incomplete 8 not tried 0% in round 3
c [elim-11] transition to [ all 1 rem 1 ] state
c [elim-11] eliminated 440 = 1% variables out of 55839 scheduled
c [elim-11] 440 < 1/100 * 55839 = 558 considered unsuccessful
c [bca-9] limit of 10000000 steps and 858162 added (scaled 2)
c [bca-9] 95799 out of 110800 literals actually usable 86%
c [bca-9] added 633 blocked clauses in 224136 steps
c [sweep-9] limit 11290164 penalty 0 = 0 + 0
c [sweep-9-1] 3334 pos 9.3% + 32391 neg 90.7% = 35725 sched 64.5% ret 19674
c [sweep-9-1] 11293814 steps 198 queries 1829.31 avg class size
c [sweep-9-1] 2647 decisions 182 SAT calls 141.34 avg env size
c [sweep-9-1] 33956 variables remain 61% (21433 retained 39%)
c [decomp-33] removed 93 variables
c [sweep-9-1] removed 93 vars (0 failed, 18 eqs, 29 impls)
c [sweep-9] removed 93 vars in TOTAL (1 rounds, 197 queries)
c [phase-count-13] 427459 negative 99.8% of 428373 except 914 0.2%
c [phase-count-13] 337261 positive 78.7% of 428373 except 91112 21.3%
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 16238 enqueued variables after 71698 conflicts
c [score-dist-13] active 39068 (71%), one 0 (0%), zero 16238 (29%)
c [score-dist-13] max exp 518, different 13 (3%)
c [score-dist-13] median active exp 518, avg 517.5
c [simplification-13] removed 837 variables 1.5% (55306 remain 22%)
c [simplification-13] removed 14142 irredundant clauses 3.2% (428373 remain 31%)
c [simplification-13] maximum reduction of 3% = max (1%, 3%)
c [simplification-13] geometric conflict interval increment 5250 = 21000 / 4
c [simplification-13] new conflict interval 26250
c [simplification-13] penalized conflict interval 26250 = 1 * 26250
c [simplification-13] hard conflict limit 111073 (soft 97948 + delta 13125)
c [simplification-13] new conflict limit 97948 (hard 111073)
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  257.4   55305   428373     71705    6719   3167 495960   76   484   55  16%      2  179   61   52  117%
c i  260.8   55304   428373     76873   11440   3219 495998   57   367   62  15%     60   55   66   51  129%
c i  260.8   55211   428373     76881   11447   3219 495998   57   367   62  16%     59   55   69   51  134%
c i  261.3   55208   428373     77524   12027   3231 496014   54   345   64  16%     32   33   32   51   63%
c i  261.8   55189   428373     78102   12538   3236 496030   53   332   64  16%     18   20   60   51  117%
c i  263.8   55187   428373     80779   14959   3274 496042   55   363   68  15%     23   48   58   51  112%
c i  265.8   55165   428373     83115   17063   3306 496057   56   335   72  17%     18   20   63   52  122%
c i  266.4   55163   428373     83955   17804   3328 496076   56   331   72  17%      8   16   60   52  116%
c i  268.7   55028   428373     86271   19966   3356 496092   57   341   76  17%     16   24   52   52  100%
c i  268.8   55027   428373     86339   20026   3357 496092   58   341   77  17%     15   24   70   52  134%
c i  268.9   55026   428373     86487   20151   3357 496092   61   345   78  18%     12   28  102   52  195%
c i  269.2   55025   428373     86694   20326   3366 496096   63   351   78  18%      9   35   98   52  188%
c i  269.6   55018   428373     87084   20690   3370 496100   63   348   78  18%      5   32   72   52  137%
c i  270.1   55017   428373     87556   21116   3377 496104   67   363   78  18%      2   45   96   53  182%
c i  271.5   55016   428373     89241   22628   3405 496143   64   340   78  19%      8   22   66   53  125%
c i  271.8   55015   428373     89497   22856   3407 496148   64   341   78  19%      5   23   64   53  120%
c i  271.8   55005   428373     89525   22873   3409 496150   63   339   78  19%      5   21   57   53  109%
c i  273.5   55001   428373     91023   24217   3425 496160   67   358   78  19%      7   40   72   53  135%
c i  274.7   55000   428373     92086   25174   3433 496185   66   351   80  19%      4   31   61   54  115%
c i  277.7   54874   428373     95569   28337   3480 496200   63   289   86  22%     31  -30   89   54  166%
c i  278.5   54873   428373     96216   28930   3484 496206   66   322   87  20%     15    3   79   54  145%
c 
c [simplification-14] limit 97949 conflicts (hard 111073) hit after 97949 conflicts
c [quatres-9] found 23781 quaternary clauses 57% in total
c [quatres-9-2] added 5 single-self-subsuming ternary resolvents
c [quatres-9-2] added 3 quaternary resolvents
c [ternres-9] limit 44464059 with penalty 0 = 0 + 0
c [ternres-9] all 54872 free variables schedulable
c [ternres-9] 324 ternary resolvents (0 bin, 324 trn)
c [ternres-9] fully completed ternary resolution
c [decomp-34] removed 468 variables
c [basicprobe-5] limit 222320299 penalty 0 = 0 + 0
c [basicprobe-5-0] 5375 probes remain 10% after last round
c [basicprobe-5-0] 1103 units = 995 failed (90%) + 108 lifted (10%)
c [basicprobe-5-0] removed 1896 variables, found 502530 hbrs
c [bate-3] eliminated 1750 asymmetric tautologies during probing
c [unhide-14] limit 2223202 with penalty 2 = 0 + 2
c [unhide-14-17] 1 units, 172 failed, 107399 tauts, 0 hbrs, 375167 literals
c [transred-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 235 transitive binary clauses
c [transred-10] found 1 units
c [bca-10] limit of 10000000 steps and 806238 added (scaled 2)
c [bca-10] 82043 out of 105580 literals actually usable 78%
c [bca-10] added 257 blocked clauses in 213272 steps
c [sweep-10] limit 13339217 penalty 0 = 0 + 0
c [sweep-10-1] 3273 pos 10.0% + 29381 neg 90.0% = 32654 sched 61.9% ret 20135
c [sweep-10-1] 13491093 steps 247 queries 1789.89 avg class size
c [sweep-10-1] 5473 decisions 234 SAT calls 199.54 avg env size
c [sweep-10-1] 30020 variables remain 57% (22719 retained 43%)
c [decomp-35] removed 162 variables
c [sweep-10-1] removed 162 vars (0 failed, 15 eqs, 29 impls)
c [sweep-10] removed 162 vars in TOTAL (1 rounds, 246 queries)
c [phase-count-14] 401129 negative 99.8% of 402035 except 906 0.2%
c [phase-count-14] 313210 positive 77.9% of 402035 except 88825 22.1%
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 13947 enqueued variables after 97949 conflicts
c [score-dist-14] active 38680 (73%), one 0 (0%), zero 13947 (27%)
c [score-dist-14] max exp 518, different 13 (3%)
c [score-dist-14] median active exp 518, avg 517.8
c [simplification-14] removed 2245 variables 4.1% (52627 remain 21%)
c [simplification-14] removed 26338 irredundant clauses 6.1% (402035 remain 29%)
c [simplification-14] maximum reduction of 6% = max (4%, 6%)
c [simplification-14] large reduction 6% >= 5% limit
c [simplification-14] next conflict interval 2000 = 2000/1
c [simplification-14] penalized conflict interval 2000 = 1 * 2000
c [simplification-14] hard conflict limit 109949 (soft 99949 + delta 10000)
c [simplification-14] new conflict limit 99949 (hard 109949)
c 
c [simplification-15] limit 99949 conflicts (hard 109949) hit after 99949 conflicts
c [quatres-10] found 22594 quaternary clauses 58% in total
c [quatres-10-1] removed 4 duplicate quaternary clauses
c [quatres-10-1] added 1 double-self-subsuming ternary resolvents
c [quatres-10-2] added 5 quaternary resolvents
c [ternres-10] limit 45113184 with penalty 0 = 0 + 0
c [ternres-10] all 52627 free variables schedulable
c [ternres-10] 659 ternary resolvents (1 bin, 658 trn)
c [ternres-10] fully completed ternary resolution
c [card-5] limit 1409787 penalty 4 = 4 + 0
c [card-5] found 1102 at-most-one constraints of average size 4.1
c [card-5] no at-most-two constraint found
c [card-5] using previous limit 1409787 for elimination
c [card-5] 1102 out of 1102 constraints (100%) meet size limits
c [card-5] no units found
c [card-5] no at-most-one constraints generated
c [decomp-36] removed 1 variables
c [simpleprobe-6] all 52626 free variables schedulable
c [simpleprobe-6] limit 180452737 penalty 0 = 0 + 0
c [decomp-37] removed 305 variables
c [simpleprobe-6] 450 variables remain 1% (51871 retained 99%)
c [simpleprobe-6] removed 305 variables, found 142396 hbrs, 176 units
c [unhide-15] limit 2255659 with penalty 2 = 0 + 2
c [unhide-15-19] 1 units, 83 failed, 88779 tauts, 0 hbrs, 312592 literals
c [transred-11] limit 2000000 with penalty 0 = 0 + 0
c [transred-11] removed 248 transitive binary clauses
c [transred-11] found 1 units
c [block-5] scheduling all variables this time
c [block-5] scheduled 52257 variables 100%
c [block-5] limit of 56391480 steps penalty 3 = 3 + 0
c [block-5] fully completed
c [block-5] transition to [ all 0 rem 0 ] state
c [block-5] eliminated 416 blocked clauses
c [block-5] 416 < 1/100 * 392135 = 3921 considered unsuccessful
c [cce-6] limit of 112782961 steps penalty 1 = 1 + 0
c [cce-6-1] eliminated 4 clauses out of 36 (11%) of length 7
c [cce-6-1] eliminated 2 clauses out of 2712 (0%) of length 6
c [cce-6-1] eliminated 91 clauses out of 9931 (1%) of length 5
c [cce-6-1] incomplete large round (ATE)
c [cce-6-1] eliminated 97 large clauses in 112782968 steps
c [cce-6-1] allowing another 56391484 steps for small clauses
c [cce-6-1] scheduling 197459 clauses = 177524 binary + 19935 ternary
c [cce-6-1] tried to eliminate 2975 small clauses 2%
c [cce-6-1] eliminated 712 binary clauses 0%
c [cce-6-1] eliminated 95 ternary clauses 0%
c [cce-6-1] eliminated 807 small clauses 0%
c [cce-6-1] eliminated 807 small clauses in 112782965 steps
c [cce-6-1] incomplete small round (ATE)
c [cce-6-1] eliminated 904 covered clauses in round 1
c [cce-6] eliminated 904 covered clauses in TOTAL during 1 rounds
c [cce-6] 904 < 1/100 * 391276 = 3912 considered unsuccessful
c [elim-12] no untried remaining variables left
c [elim-12] scheduled 52253 variables 100%
c [elim-12] limit of 400000000 steps penalty 1 = 1 + 0
c [elim-12] rescheduling of touched variables disabled
c [elim-12-1] eliminated 917 variables 2% in round 1 in 35404548 steps
c [elim-12-1] backward subsumption/strengthening limit 35404500
c [elim-12-1-1] backward checking 5456 touched variables 10%
c [elim-12-1-1] fully completed backward checking in 1 rounds
c [elim-12-1] subsumed 12 and strengthened 62 clauses in 1448521 steps
c [elim-12-1] rescheduled 163 variables 0% by backward subsumption
c [elim-12-2] eliminated 15 variables 0% in round 2 in 188291 steps
c [elim-12-2] backward subsumption/strengthening limit 188200
c [elim-12-2-1] backward checking 147 touched variables 0%
c [elim-12-2-1] fully completed backward checking in 1 rounds
c [elim-12-2] subsumed 5 and strengthened 5 clauses in 116898 steps
c [elim-12-2] rescheduled 30 variables 0% by backward subsumption
c [elim-12-3] eliminated 7 variables 0% in round 3 in 159285 steps
c [elim-12-3] backward subsumption/strengthening limit 159200
c [elim-12-3-1] backward checking 57 touched variables 0%
c [elim-12-3-1] fully completed backward checking in 1 rounds
c [elim-12-3] subsumed 7 and strengthened 4 clauses in 94219 steps
c [elim-12] incomplete 29 not tried 0% in round 3
c [elim-12] transition to [ all 1 rem 1 ] state
c [elim-12] eliminated 939 = 2% variables out of 52253 scheduled
c [bca-11] limit of 10000000 steps and 777999 added (scaled 2)
c [bca-11] 79529 out of 102630 literals actually usable 77%
c [bca-11] added 268 blocked clauses in 205250 steps
c [sweep-11] boosting sweeping limit by 10
c [sweep-11] limit 135339550 penalty 0 = 0 + 0
c [sweep-11-1] 3054 pos 10.5% + 26138 neg 89.5% = 29192 sched 56.9% ret 22122
c [sweep-11-1] 135362425 steps 3668 queries 86.62 avg class size
c [sweep-11-1] 32184 decisions 3326 SAT calls 88.90 avg env size
c [sweep-11-1] 7865 variables remain 15% (43240 retained 85%)
c [decomp-38] removed 1165 variables
c [sweep-11-1] removed 1165 vars (0 failed, 358 eqs, 653 impls)
c [sweep-11] removed 1165 vars in TOTAL (1 rounds, 3667 queries)
c [phase-count-15] 384960 negative 99.8% of 385840 except 880 0.2%
c [phase-count-15] 301210 positive 78.1% of 385840 except 84630 21.9%
c [phase-count-15] skipping relative phase luck test
c [phase-15] phase bias: 1 positive 100%, 0 negative 0%
c [sort-queue-15] sorted 12651 enqueued variables after 99949 conflicts
c [score-dist-15] active 37498 (75%), one 0 (0%), zero 12651 (25%)
c [score-dist-15] max exp 518, different 13 (3%)
c [score-dist-15] median active exp 518, avg 517.9
c [simplification-15] removed 2478 variables 4.7% (50149 remain 20%)
c [simplification-15] removed 16195 irredundant clauses 4.0% (385840 remain 28%)
c [simplification-15] maximum reduction of 5% = max (5%, 4%)
c [simplification-15] large reduction 5% >= 5% limit
c [simplification-15] next conflict interval 2000 = 2000/1
c [simplification-15] penalized conflict interval 2000 = 1 * 2000
c [simplification-15] hard conflict limit 111949 (soft 101949 + delta 10000)
c [simplification-15] new conflict limit 101949 (hard 111949)
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  319.7   50148   385840    101614   30568   4982 971175   66   325   96  20%     58    4   91   55  165%
c i  319.7   50144   385840    101640   30588   4983 971175   66   324   96  20%     57    4   88   55  159%
c 
c [simplification-16] limit 101949 conflicts (hard 111949) hit after 101949 conflicts
c [quatres-11] found 21512 quaternary clauses 55% in total
c [quatres-11-2] added 2 single-self-subsuming ternary resolvents
c [quatres-11-2] added 6 quaternary resolvents
c [ternres-11] limit 45636328 with penalty 0 = 0 + 0
c [ternres-11] all 50144 free variables schedulable
c [ternres-11] 456 ternary resolvents (2 bin, 454 trn)
c [ternres-11] fully completed ternary resolution
c [decomp-39] removed 6 variables
c [treelook-6] limit 4563632 penalty 0 = 0 + 0 boost 1
c [treelook-6] scheduled 81881 literals 82%
c [treelook-6] scheduling used 2524426 steps
c [treelook-6] scheduled completely
c [treelook-6] limit 4563632 penalty 0 = 0 + 0 boost 1
c [treelook-6] used 4631076 steps
c [treelook-6] 81653 literals remain 81%
c [treelook-6] 19252 variables remain to probed next time 38%
c [treelook-6] removed 24 variables, found 25202 hbrs
c [unhide-16] limit 4563632 with penalty 1 = 0 + 1
c [unhide-16-21] 17 units, 217 failed, 73913 tauts, 0 hbrs, 251450 literals
c [transred-12] limit 2000000 with penalty 0 = 0 + 0
c [transred-12] removed 224 transitive binary clauses
c [elim-13] no untried remaining variables left
c [elim-13] scheduled 50005 variables 100%
c [elim-13] almost no limit of 100000000000 steps
c [elim-13] rescheduling of touched variables disabled
c [elim-13-1] eliminated 256 variables 1% in round 1 in 37298775 steps
c [elim-13-1] backward subsumption/strengthening limit 37298700
c [elim-13-1-1] backward checking 2043 touched variables 4%
c [elim-13-1-1] fully completed backward checking in 1 rounds
c [elim-13-1] subsumed 7 and strengthened 14 clauses in 682046 steps
c [elim-13-1] rescheduled 55 variables 0% by backward subsumption
c [elim-13-2] eliminated 5 variables 0% in round 2 in 33180 steps
c [elim-13-2] backward subsumption/strengthening limit 33100
c [elim-13-2-1] backward checking 57 touched variables 0%
c [elim-13-2-1] incomplete backward checking 0 remain 0%
c [elim-13-2] subsumed 1 and strengthened 5 clauses in 33101 steps
c [elim-13-2] rescheduled 18 variables 0% by backward subsumption
c [elim-13-3] eliminated 3 variables 0% in round 3 in 19008 steps
c [elim-13-3] backward subsumption/strengthening limit 19000
c [elim-13-3-1] backward checking 20 touched variables 0%
c [elim-13-3-1] incomplete backward checking 6 remain 30%
c [elim-13-3] subsumed 4 and strengthened 2 clauses in 19003 steps
c [elim-13] incomplete 14 not tried 0% in round 3
c [elim-13] transition to [ all 1 rem 1 ] state
c [elim-13] eliminated 264 = 1% variables out of 50005 scheduled
c [elim-13] 264 < 1/100 * 50005 = 500 considered unsuccessful
c [bca-12] limit of 10000000 steps and 757689 added (scaled 2)
c [bca-12] 74229 out of 99484 literals actually usable 75%
c [bca-12] added 139 blocked clauses in 193204 steps
c [sweep-12] limit 13690898 penalty 0 = 0 + 0
c [sweep-12-1] 861 pos 12.1% + 6270 neg 87.9% = 7131 sched 14.3% ret 42610
c [sweep-12-1] 13774274 steps 457 queries 263.05 avg class size
c [sweep-12-1] 3905 decisions 414 SAT calls 79.90 avg env size
c [sweep-12-1] 5981 variables remain 12% (43648 retained 88%)
c [decomp-41] removed 168 variables
c [sweep-12-1] removed 168 vars (0 failed, 48 eqs, 66 impls)
c [sweep-12] removed 168 vars in TOTAL (1 rounds, 456 queries)
c [phase-count-16] 376640 negative 99.8% of 377468 except 828 0.2%
c [phase-count-16] 295068 positive 78.2% of 377468 except 82400 21.8%
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 12460 enqueued variables after 101949 conflicts
c [score-dist-16] active 37113 (75%), one 0 (0%), zero 12460 (25%)
c [score-dist-16] max exp 518, different 13 (3%)
c [score-dist-16] median active exp 518, avg 517.9
c [simplification-16] removed 571 variables 1.1% (49573 remain 20%)
c [simplification-16] removed 8372 irredundant clauses 2.2% (377468 remain 27%)
c [simplification-16] maximum reduction of 2% = max (1%, 2%)
c [simplification-16] geometric conflict interval increment 8750 = 26250 / 3
c [simplification-16] new conflict interval 35000
c [simplification-16] penalized conflict interval 35000 = 1 * 35000
c [simplification-16] hard conflict limit 154449 (soft 136949 + delta 17500)
c [simplification-16] new conflict limit 136949 (hard 154449)
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  327.5   49572   377468    101976   30418   5242 924431   66   325   88  20%     38    4   65   55  118%
c i  328.1   49571   377468    102569   30930   5253 924444   65   309   97  21%     19  -12   72   55  131%
c i  328.7   49570   377468    102953   31289   5257 924448   68   323   97  21%     11    3  104   56  188%
c i  329.8   49568   377468    103955   32195   5266 924452   65   317   97  21%      3   -3   41   56   74%
c i  330.3   49534   377468    104501   32694   5276 924458   65   334   97  20%     -1   14   70   56  127%
c i  331.0   49533   377468    105331   33408   5297 924460   65   317   97  20%     -2   -4   70   56  126%
c i  331.2   49532   377468    105439   33502   5297 924460   67   322   97  21%     -3    2   95   56  170%
c i  331.4   49531   377468    105610   33653   5301 924460   68   325   97  21%     -4    4   94   56  167%
c i  338.5   49529   377468    111740   39227   5362 924497   75   329   98  23%     67    6   93   58  160%
c i  338.7   49511   377468    111892   39363   5367 924497   74   328   98  23%     56    5   69   58  120%
c i  339.2   49510   377468    112258   39696   5370 924505   74   329   98  22%     36    6   69   58  119%
c i  340.9   49467   377468    113612   40919   5381 924513   77   349  100  22%      9   26   85   58  146%
c i  341.9   49466   377468    114379   41604   5386 924518   79   354  100  22%      0   30   96   59  162%
c i  342.0   49388   377468    114423   41642   5386 924518   80   356  100  22%     -0   33  106   59  180%
c i  344.1   49387   377468    116319   43324   5423 924538   83   363  103  23%      4   38   76   60  127%
c i  346.5   49386   377468    118173   45030   5436 924540   83   358  107  23%      5   32   92   60  152%
c i  347.4   49385   377468    118740   45534   5444 924545   84   357  107  23%     -1   31   86   61  141%
c i  348.8   49381   377468    119807   46509   5458 924551   84   366  111  23%     -3   40   87   61  143%
c i  350.2   49380   377468    120787   47406   5466 924566   85   374  115  23%     -4   47   88   61  142%
c i  353.1   49378   377468    122949   49395   5480 924576   96   408  115  24%      7   78  105   63  166%
c i  355.0   49377   377468    124323   50628   5494 924580   98   404  116  24%      1   73  113   64  176%
c i  355.7   49376   377468    124849   51103   5499 924584   97   398  116  24%     -3   67   83   64  129%
c i  356.2   49335   377468    125220   51446   5500 924584   97   394  116  25%     -5   63   98   64  153%
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  360.0   49332   377468    127978   53970   5520 924597   93   381  125  25%     15   47   64   65   99%
c i  362.9   49329   377468    130164   55925   5535 924605   91   355  129  26%     10   20   85   66  129%
c -  364.7   49328   377468    131436   19452   5555 924612   95   364   66  26%      1   29   99   67  149%
c i  369.5   49327   377468    136037   23550   5592 924639   83   329   75  25%     60   -8   68   68  101%
c i  374.4   49326   377468    141133   28004   5641 924664   72   264   88  27%     46  -71   45   68   66%
c i  375.3   49325   377468    141941   28701   5645 924669   75   264   89  28%     15  -70  104   68  153%
c i  376.8   49324   377468    143190   29851   5650 924672   80   290   89  27%     -0  -43   82   69  119%
c i  378.7   49319   377468    144880   31373   5658 924675   84   300   91  28%     -1  -32  123   69  179%
c i  379.0   49318   377468    145112   31590   5659 924675   84   302   91  28%     -4  -30  103   69  148%
c i  380.3   49289   377468    146064   32476   5663 924685   87   322   91  27%     -7  -10   77   70  110%
c i  383.0   49027   377468    148566   34763   5669 924696   83   302   93  28%      8  -28  122   70  176%
c i  387.0   49026   377468    151950   37719   5691 924721   92   319  105  29%     20   -9  138   71  194%
c 
c [simplification-17] limit 136949 conflicts (hard 154449) hit after 152903 conflicts
c [quatres-12] found 20361 quaternary clauses 52% in total
c [quatres-12-2] added 5 single-self-subsuming ternary resolvents
c [ternres-12] limit 61410096 with penalty 0 = 0 + 0
c [ternres-12] all 49026 free variables schedulable
c [ternres-12] 224 ternary resolvents (0 bin, 224 trn)
c [ternres-12] fully completed ternary resolution
c [gauss-6] limit 1535252 penalty 3 = 3 + 0
c [gauss-6] extracted 27 xors of average arity 2.6
c [gauss-6] connected 70 occurrences of 65 variables (average 1.1)
c [gauss-6] limit 1535252 penalty 3 = 3 + 0
c [gauss-6] fully completed
c [decomp-42] removed 61 variables
c [gauss-6] exported 0 unary, 2 binary and 0 ternary equations
c [basicprobe-6] limit 307050481 penalty 0 = 0 + 0
c [basicprobe-6-0] 6028 sched 13%, 773 failed, 47 lifted, 303443 hbrs
c [decomp-44] removed 1266 variables
c [basicprobe-6-1] 8531 probes remain 18% after last round
c [basicprobe-6-1] 1009 units = 959 failed (95%) + 50 lifted (5%)
c [basicprobe-6-1] removed 1514 variables, found 442228 hbrs
c [bate-4] eliminated 530 asymmetric tautologies during probing
c [unhide-17] limit 3070504 with penalty 2 = 0 + 2
c [unhide-17-23] 2 units, 60 failed, 121108 tauts, 0 hbrs, 592771 literals
c [transred-13] limit 2000000 with penalty 0 = 0 + 0
c [transred-13] removed 232 transitive binary clauses
c [bca-13] limit of 10000000 steps and 692222 added (scaled 2)
c [bca-13] 68844 out of 94780 literals actually usable 73%
c [bca-13] added 46 blocked clauses in 187146 steps
c [sweep-13] limit 18423028 penalty 0 = 0 + 0
c [sweep-13-1] 582 pos 10.4% + 5010 neg 89.6% = 5592 sched 11.8% ret 41797
c [sweep-13-1] 18425351 steps 822 queries 159.28 avg class size
c [sweep-13-1] 6582 decisions 750 SAT calls 64.61 avg env size
c [sweep-13-1] 3657 variables remain 8% (43626 retained 92%)
c [decomp-45] removed 251 variables
c [sweep-13-1] removed 251 vars (0 failed, 71 eqs, 153 impls)
c [sweep-13] removed 251 vars in TOTAL (1 rounds, 821 queries)
c [sort-queue-17] sorted 10616 enqueued variables after 152903 conflicts
c [score-dist-17] active 36522 (77%), one 0 (0%), zero 10616 (23%)
c [score-dist-17] max exp 519, different 13 (2%)
c [score-dist-17] median active exp 519, avg 518.6
c [simplification-17] removed 1888 variables 3.9% (47138 remain 19%)
c [simplification-17] removed 32859 irredundant clauses 8.7% (344609 remain 25%)
c [simplification-17] maximum reduction of 9% = max (4%, 9%)
c [simplification-17] large reduction 9% >= 5% limit
c [simplification-17] next conflict interval 2000 = 2000/1
c [simplification-17] penalized conflict interval 2000 = 1 * 2000
c [simplification-17] hard conflict limit 164903 (soft 154903 + delta 10000)
c [simplification-17] new conflict limit 154903 (hard 164903)
c 
c [simplification-18] limit 154903 conflicts (hard 164903) hit after 154903 conflicts
c [quatres-13] found 19983 quaternary clauses 51% in total
c [quatres-13-1] removed 1 duplicate quaternary clauses
c [quatres-13-2] added 2 single-self-subsuming ternary resolvents
c [ternres-13] limit 62079302 with penalty 0 = 0 + 0
c [ternres-13] all 47138 free variables schedulable
c [ternres-13] 275 ternary resolvents (1 bin, 274 trn)
c [ternres-13] fully completed ternary resolution
c [decomp-46] removed 2 variables
c [simpleprobe-7] 420 schedulable variables 1%
c [simpleprobe-7] limit 200000000 penalty 0 = 0 + 0
c [decomp-47] removed 105 variables
c [simpleprobe-7] 2884 variables remain 6% (44147 retained 94%)
c [simpleprobe-7] removed 105 variables, found 109627 hbrs, 43 units
c [unhide-18] limit 3103965 with penalty 2 = 0 + 2
c [unhide-18-24] 1 units, 22 failed, 89908 tauts, 0 hbrs, 171354 literals
c [transred-14] limit 2000000 with penalty 0 = 0 + 0
c [transred-14] removed 243 transitive binary clauses
c [cce-7] limit of 77599128 steps penalty 2 = 2 + 0
c [cce-7-1] eliminated 1 clauses out of 1 (100%) of length 51
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 50
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 49
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 48
c [cce-7-1] eliminated 1 clauses out of 1 (100%) of length 47
c [cce-7-1] eliminated 2 clauses out of 3 (67%) of length 46
c [cce-7-1] eliminated 1 clauses out of 1 (100%) of length 45
c [cce-7-1] eliminated 2 clauses out of 3 (67%) of length 44
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 43
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 42
c [cce-7-1] eliminated 1 clauses out of 1 (100%) of length 41
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 40
c [cce-7-1] eliminated 3 clauses out of 3 (100%) of length 39
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 38
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 37
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 36
c [cce-7-1] eliminated 1 clauses out of 1 (100%) of length 35
c [cce-7-1] eliminated 2 clauses out of 3 (67%) of length 34
c [cce-7-1] eliminated 1 clauses out of 1 (100%) of length 33
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 32
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 31
c [cce-7-1] eliminated 2 clauses out of 3 (67%) of length 30
c [cce-7-1] eliminated 2 clauses out of 3 (67%) of length 29
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 28
c [cce-7-1] eliminated 4 clauses out of 4 (100%) of length 27
c [cce-7-1] eliminated 2 clauses out of 4 (50%) of length 26
c [cce-7-1] eliminated 2 clauses out of 4 (50%) of length 25
c [cce-7-1] eliminated 2 clauses out of 4 (50%) of length 24
c [cce-7-1] eliminated 3 clauses out of 4 (75%) of length 23
c [cce-7-1] eliminated 3 clauses out of 4 (75%) of length 22
c [cce-7-1] eliminated 3 clauses out of 5 (60%) of length 21
c [cce-7-1] eliminated 3 clauses out of 4 (75%) of length 20
c [cce-7-1] eliminated 3 clauses out of 4 (75%) of length 19
c [cce-7-1] eliminated 3 clauses out of 4 (75%) of length 18
c [cce-7-1] eliminated 3 clauses out of 4 (75%) of length 17
c [cce-7-1] eliminated 3 clauses out of 4 (75%) of length 16
c [cce-7-1] eliminated 2 clauses out of 4 (50%) of length 15
c [cce-7-1] eliminated 3 clauses out of 5 (60%) of length 14
c [cce-7-1] eliminated 1 clauses out of 3 (33%) of length 13
c [cce-7-1] eliminated 2 clauses out of 3 (67%) of length 12
c [cce-7-1] eliminated 2 clauses out of 4 (50%) of length 11
c [cce-7-1] eliminated 3 clauses out of 12 (25%) of length 10
c [cce-7-1] eliminated 3 clauses out of 4 (75%) of length 9
c [cce-7-1] eliminated 3 clauses out of 5 (60%) of length 8
c [cce-7-1] eliminated 4 clauses out of 35 (11%) of length 7
c [cce-7-1] eliminated 33 clauses out of 2581 (1%) of length 6
c [cce-7-1] eliminated 54 clauses out of 9541 (1%) of length 5
c [cce-7-1] incomplete large round (ACCE)
c [cce-7-1] eliminated 181 large clauses in 77599135 steps
c [cce-7-1] allowing another 38799567 steps for small clauses
c [cce-7-1] scheduling 185071 clauses = 169359 binary + 15712 ternary
c [cce-7-1] tried to eliminate 2438 small clauses 1%
c [cce-7-1] eliminated 588 binary clauses 0%
c [cce-7-1] eliminated 54 ternary clauses 0%
c [cce-7-1] eliminated 642 small clauses 0%
c [cce-7-1] eliminated 806 small clauses in 77599133 steps
c [cce-7-1] incomplete small round (ACCE)
c [cce-7-1] eliminated 987 covered clauses in round 1
c [cce-7] eliminated 987 covered clauses in TOTAL during 1 rounds
c [cce-7] 987 < 1/100 * 343124 = 3431 considered unsuccessful
c [elim-14] no untried remaining variables left
c [elim-14] scheduled 47014 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 734 variables 2% in round 1 in 31589759 steps
c [elim-14-1] backward subsumption/strengthening limit 31589700
c [elim-14-1-1] backward checking 4168 touched variables 9%
c [elim-14-1-1] fully completed backward checking in 1 rounds
c [elim-14-1] subsumed 7 and strengthened 28 clauses in 1113424 steps
c [elim-14-1] rescheduled 117 variables 0% by backward subsumption
c [elim-14-2] eliminated 6 variables 0% in round 2 in 88567 steps
c [elim-14-2] backward subsumption/strengthening limit 88500
c [elim-14-2-1] backward checking 90 touched variables 0%
c [elim-14-2-1] fully completed backward checking in 1 rounds
c [elim-14-2] subsumed 6 and strengthened 2 clauses in 79927 steps
c [elim-14-2] rescheduled 20 variables 0% by backward subsumption
c [elim-14-3] eliminated 2 variables 0% in round 3 in 16236 steps
c [elim-14-3] backward subsumption/strengthening limit 16200
c [elim-14-3-1] backward checking 25 touched variables 0%
c [elim-14-3-1] incomplete backward checking 0 remain 0%
c [elim-14-3] subsumed 2 and strengthened 4 clauses in 16201 steps
c [elim-14] incomplete 14 not tried 0% in round 3
c [elim-14] transition to [ all 1 rem 1 ] state
c [elim-14] eliminated 742 = 2% variables out of 47014 scheduled
c [bca-14] limit of 10000000 steps and 683277 added (scaled 2)
c [bca-14] 66990 out of 92546 literals actually usable 72%
c [bca-14] added 86 blocked clauses in 181834 steps
c [sweep-14] limit 18623790 penalty 0 = 0 + 0
c [sweep-14-1] 333 pos 9.7% + 3109 neg 90.3% = 3442 sched 7.4% ret 42830
c [sweep-14-1] 18690308 steps 843 queries 87.65 avg class size
c [sweep-14-1] 6649 decisions 755 SAT calls 72.31 avg env size
c [sweep-14-1] 1923 variables remain 4% (44285 retained 96%)
c [decomp-48] removed 190 variables
c [sweep-14-1] removed 190 vars (0 failed, 88 eqs, 148 impls)
c [sweep-14] removed 190 vars in TOTAL (1 rounds, 842 queries)
c [sort-queue-18] sorted 10432 enqueued variables after 154903 conflicts
c [score-dist-18] active 35650 (77%), one 0 (0%), zero 10432 (23%)
c [score-dist-18] max exp 519, different 12 (2%)
c [score-dist-18] median active exp 519, avg 518.7
c [simplification-18] removed 1056 variables 2.2% (46082 remain 19%)
c [simplification-18] removed 4223 irredundant clauses 1.2% (340386 remain 25%)
c [simplification-18] maximum reduction of 2% = max (2%, 1%)
c [simplification-18] geometric conflict interval increment 11666 = 35000 / 3
c [simplification-18] new conflict interval 46666
c [simplification-18] penalized conflict interval 46666 = 1 * 46666
c [simplification-18] hard conflict limit 224902 (soft 201569 + delta 23333)
c [simplification-18] new conflict limit 201569 (hard 224902)
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  423.6   46081   340386    156229   37889   5656 1128642   90   337  105  27%     33    8   55   72   76%
c i  424.5   46078   340386    156933   38502   5670 1128644   91   335  105  27%     10    6   94   73  129%
c i  424.9   46063   340386    157276   38819   5672 1128646   91   339  105  27%      2    9   91   73  126%
c i  427.5   46057   340386    159687   40986   5687 1128662   87   314  105  28%      6  -15  104   73  143%
c i  430.4   46056   340386    161986   42995   5706 1128679   94   337  105  28%      5    8   87   74  118%
c i  432.1   46052   340386    163255   44138   5715 1128685   96   353  105  27%     -4   24  107   75  143%
c i  445.4   46051   340386    174039   53516   5809 1128747  100   326  125  31%    125   -2   97   78  124%
c -  455.5   46049   340386    181118   23619   5858 1128801  107   340   70  31%     64   11   73   82   89%
c i  463.0   46048   340386    187937   29318   5892 1128830   89   255   82  35%    159  -71  108   82  132%
c i  464.2   46044   340386    189019   30285   5895 1128837   94   292   88  32%     32  -33  120   82  146%
c 
c [simplification-19] limit 201569 conflicts (hard 224902) hit after 216254 conflicts
c [quatres-14] found 20106 quaternary clauses 49% in total
c [quatres-14-1] removed 1 duplicate quaternary clauses
c [quatres-14-2] added 3 single-self-subsuming ternary resolvents
c [quatres-14-2] added 2 quaternary resolvents
c [ternres-14] limit 79892689 with penalty 0 = 0 + 0
c [ternres-14] all 46019 free variables schedulable
c [ternres-14] 443 ternary resolvents (1 bin, 442 trn)
c [ternres-14] fully completed ternary resolution
c [gauss-7] limit 3994634 penalty 2 = 2 + 0
c [gauss-7] extracted 47 xors of average arity 2.7
c [gauss-7] connected 129 occurrences of 121 variables (average 1.1)
c [gauss-7] limit 3994634 penalty 2 = 2 + 0
c [gauss-7] fully completed
c [gauss-7] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-49] removed 20 variables
c [treelook-7] limit 7989268 penalty 0 = 0 + 0 boost 1
c [treelook-7] scheduled 76025 literals 83%
c [treelook-7] scheduling used 2733222 steps
c [treelook-7] scheduled completely
c [treelook-7] limit 7989268 penalty 0 = 0 + 0 boost 1
c [treelook-7] used 8048435 steps
c [treelook-7] 75942 literals remain 83%
c [treelook-7] 17247 variables remain to probed next time 37%
c [treelook-7] removed 0 variables, found 25235 hbrs
c [unhide-19] limit 3994634 with penalty 2 = 0 + 2
c [unhide-19-26] 1 units, 15 failed, 55718 tauts, 0 hbrs, 1506356 literals
c [transred-15] limit 2000000 with penalty 0 = 0 + 0
c [transred-15] removed 142 transitive binary clauses
c [elim-15] no untried remaining variables left
c [elim-15] scheduled 45940 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 219 variables 0% in round 1 in 33047552 steps
c [elim-15-1] backward subsumption/strengthening limit 33047500
c [elim-15-1-1] backward checking 1430 touched variables 3%
c [elim-15-1-1] fully completed backward checking in 1 rounds
c [elim-15-1] subsumed 5 and strengthened 6 clauses in 443654 steps
c [elim-15-1] rescheduled 33 variables 0% by backward subsumption
c [elim-15-2] eliminated 3 variables 0% in round 2 in 106520 steps
c [elim-15-2] backward subsumption/strengthening limit 106500
c [elim-15-2-1] backward checking 36 touched variables 0%
c [elim-15-2-1] fully completed backward checking in 1 rounds
c [elim-15-2] subsumed 0 and strengthened 6 clauses in 67864 steps
c [elim-15-2] rescheduled 24 variables 0% by backward subsumption
c [elim-15-3] eliminated 3 variables 0% in round 3 in 101060 steps
c [elim-15-3] backward subsumption/strengthening limit 101000
c [elim-15-3-1] backward checking 30 touched variables 0%
c [elim-15-3-1] fully completed backward checking in 1 rounds
c [elim-15-3] subsumed 0 and strengthened 6 clauses in 68021 steps
c [elim-15] incomplete 24 not tried 0% in round 3
c [elim-15] transition to [ all 1 rem 1 ] state
c [elim-15] eliminated 225 = 0% variables out of 45940 scheduled
c [elim-15] 225 < 1/100 * 45940 = 459 considered unsuccessful
c [bca-15] limit of 10000000 steps and 671526 added (scaled 2)
c [bca-15] 63980 out of 91432 literals actually usable 70%
c [bca-15] added 37 blocked clauses in 189354 steps
c [sweep-15] limit 23967806 penalty 0 = 0 + 0
c [sweep-15-1] 120 pos 6.6% + 1708 neg 93.4% = 1828 sched 4.0% ret 43887
c [sweep-15-1] 23618654 steps 1334 queries 23.04 avg class size
c [sweep-15-1] 9054 decisions 1184 SAT calls 51.06 avg env size
c [sweep-15-1] fully completed sweeping round
c [decomp-51] removed 166 variables
c [sweep-15-1] removed 166 vars (0 failed, 150 eqs, 195 impls)
c [sweep-15-2] 4305 pos 9.5% + 41244 neg 90.5% = 45549 sched 100.0% ret 0
c [sweep-15-2] 533052 steps 11 queries 16279.36 avg class size
c [sweep-15-2] 280 decisions 10 SAT calls 196.20 avg env size
c [sweep-15-2] 45520 variables remain 100% (29 retained 0%)
c [sweep-15-2] removed 0 vars (0 failed, 0 eqs, 2 impls)
c [sweep-15] removed 166 vars in TOTAL (2 rounds, 1343 queries)
c [sort-queue-19] sorted 10075 enqueued variables after 216254 conflicts
c [score-dist-19] active 35474 (78%), one 0 (0%), zero 10075 (22%)
c [score-dist-19] max exp 519, different 12 (2%)
c [score-dist-19] median active exp 519, avg 518.8
c [simplification-19] removed 470 variables 1.0% (45549 remain 19%)
c [simplification-19] removed 5774 irredundant clauses 1.7% (334612 remain 24%)
c [simplification-19] maximum reduction of 2% = max (1%, 2%)
c [simplification-19] geometric conflict interval increment 15555 = 46666 / 3
c [simplification-19] new conflict interval 62221
c [simplification-19] penalized conflict interval 62221 = 1 * 62221
c [simplification-19] hard conflict limit 309585 (soft 278475 + delta 31110)
c [simplification-19] new conflict limit 278475 (hard 309585)
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  514.3   45548   334612    220208   54992   6279 1075519  109   295  140  37%    350  -12  136   89  153%
c i  523.7   45547   334612    226913   60614   6301 1075546  106   288  140  37%    -31  -15  114   90  127%
c -  526.4   45546   334612    228626   26875   6311 1075557  112   309   70  36%    -88    5  112   91  123%
c i  577.2   45545   334612    271554   62650   6500 1075731  111   313  172  35%    436   34  128   94  137%
c -  580.4   45431   334612    273405   29632   6505 1075746  119   325   72  37%   -121   45  144   95  151%
c 
c [simplification-20] limit 278475 conflicts (hard 309585) hit after 309586 conflicts
c [quatres-15] found 20376 quaternary clauses 47% in total
c [quatres-15-1] removed 1 duplicate quaternary clauses
c [quatres-15-2] added 5 single-self-subsuming ternary resolvents
c [quatres-15-2] added 3 quaternary resolvents
c [ternres-15] limit 106081309 with penalty 0 = 0 + 0
c [ternres-15] all 45431 free variables schedulable
c [ternres-15] 137 ternary resolvents (0 bin, 137 trn)
c [ternres-15] fully completed ternary resolution
c [decomp-53] removed 120 variables
c [basicprobe-7] limit 400000000 penalty 0 = 0 + 0
c [basicprobe-7-0] 8655 sched 19%, 324 failed, 12 lifted, 181051 hbrs
c [decomp-54] removed 571 variables
c [basicprobe-7-1] 6022 probes remain 13% after last round
c [basicprobe-7-1] 463 units = 447 failed (97%) + 16 lifted (3%)
c [basicprobe-7-1] removed 738 variables, found 240948 hbrs
c [bate-5] eliminated 281 asymmetric tautologies during probing
c [unhide-20] limit 5000000 with penalty 2 = 0 + 2
c [unhide-20-27] 0 units, 11 failed, 80278 tauts, 0 hbrs, 807991 literals
c [transred-16] limit 2000000 with penalty 0 = 0 + 0
c [transred-16] removed 177 transitive binary clauses
c [block-6] scheduling all variables this time
c [block-6] scheduled 44683 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 55 blocked clauses
c [block-6] 55 < 1/100 * 323108 = 3231 considered unsuccessful
c [bca-16] limit of 10000000 steps and 647715 added (scaled 2)
c [bca-16] 60962 out of 89368 literals actually usable 68%
c [bca-16] added 28 blocked clauses in 189320 steps
c [sweep-16] limit 31824392 penalty 0 = 0 + 0
c [sweep-16-1] 4178 pos 9.4% + 40476 neg 90.6% = 44654 sched 99.9% ret 29
c [sweep-16-1] 31855701 steps 524 queries 343.90 avg class size
c [sweep-16-1] 15042 decisions 519 SAT calls 275.54 avg env size
c [sweep-16-1] 27613 variables remain 62% (17026 retained 38%)
c [decomp-55] removed 75 variables
c [sweep-16-1] removed 75 vars (0 failed, 9 eqs, 24 impls)
c [sweep-16] removed 75 vars in TOTAL (1 rounds, 523 queries)
c [sort-queue-20] sorted 9121 enqueued variables after 309586 conflicts
c [score-dist-20] active 35487 (80%), one 0 (0%), zero 9121 (20%)
c [score-dist-20] max exp 520, different 13 (2%)
c [score-dist-20] median active exp 520, avg 519.7
c [simplification-20] removed 823 variables 1.8% (44608 remain 18%)
c [simplification-20] removed 11987 irredundant clauses 3.6% (322625 remain 23%)
c [simplification-20] maximum reduction of 4% = max (2%, 4%)
c [simplification-20] geometric conflict interval increment 12444 = 62221 / 5
c [simplification-20] new conflict interval 74665
c [simplification-20] penalized conflict interval 74665 = 1 * 74665
c [simplification-20] hard conflict limit 421583 (soft 384251 + delta 37332)
c [simplification-20] new conflict limit 384251 (hard 421583)
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 -  659.6   44608   322625    319012   31242   6638 1200936  110   260   73  42%    395   -4  139   99  140%
c i  667.2   44607   322625    325268   36287   6658 1200953  107   253   89  42%    453  -10  149  100  150%
c -  717.8   44596   322625    365339   32486   6808 1201034  113   254   74  45%    251   -1  119  103  115%
c 
c [simplification-21] limit 384251 conflicts (hard 421583) hit after 384976 conflicts
c [quatres-16] found 20390 quaternary clauses 46% in total
c [quatres-16-1] removed 2 duplicate quaternary clauses
c [quatres-16-2] added 5 single-self-subsuming ternary resolvents
c [ternres-16] limit 127475372 with penalty 0 = 0 + 0
c [ternres-16] all 44596 free variables schedulable
c [ternres-16] 85 ternary resolvents (1 bin, 84 trn)
c [ternres-16] fully completed ternary resolution
c [card-6] limit 3983605 penalty 4 = 4 + 0
c [card-6] found 2376 at-most-one constraints of average size 4.0
c [card-6] no at-most-two constraint found
c [card-6] using previous limit 3983605 for elimination
c [card-6] 2376 out of 2376 constraints (100%) meet size limits
c [card-6] no units found
c [card-6] no at-most-one constraints generated
c [decomp-56] removed 12 variables
c [simpleprobe-8] 2664 schedulable variables 6%
c [simpleprobe-8] limit 200000000 penalty 0 = 0 + 0
c [decomp-57] removed 35 variables
c [simpleprobe-8] 1670 variables remain 4% (42891 retained 96%)
c [simpleprobe-8] removed 35 variables, found 74183 hbrs, 22 units
c [unhide-21] limit 5000000 with penalty 2 = 0 + 2
c [unhide-21-29] 0 units, 3 failed, 82871 tauts, 0 hbrs, 793461 literals
c [transred-17] limit 2000000 with penalty 0 = 0 + 0
c [transred-17] removed 143 transitive binary clauses
c [elim-16] no untried remaining variables left
c [elim-16] scheduled 44557 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 197 variables 0% in round 1 in 30470582 steps
c [elim-16-1] backward subsumption/strengthening limit 30470500
c [elim-16-1-1] backward checking 1368 touched variables 3%
c [elim-16-1-1] fully completed backward checking in 1 rounds
c [elim-16-1] subsumed 4 and strengthened 9 clauses in 404956 steps
c [elim-16-1] rescheduled 40 variables 0% by backward subsumption
c [elim-16-2] eliminated 2 variables 0% in round 2 in 56681 steps
c [elim-16-2] backward subsumption/strengthening limit 56600
c [elim-16-2-1] backward checking 24 touched variables 0%
c [elim-16-2-1] incomplete backward checking 0 remain 0%
c [elim-16-2] subsumed 1 and strengthened 2 clauses in 56601 steps
c [elim-16-2] rescheduled 10 variables 0% by backward subsumption
c [elim-16-3] no variable eliminated in round 3 in 64972 steps
c [elim-16] fully completed in 3 rounds
c [elim-16] transition to [ all 0 rem 0 ] state
c [elim-16] eliminated 199 = 0% variables out of 44557 scheduled
c [elim-16] 199 < 1/100 * 44557 = 445 considered unsuccessful
c [bca-17] limit of 10000000 steps and 633737 added (scaled 2)
c [bca-17] 60909 out of 88718 literals actually usable 69%
c [bca-17] added 35 blocked clauses in 177383 steps
c [sweep-17] limit 38242611 penalty 0 = 0 + 0
c [sweep-17-1] 3386 pos 12.3% + 24076 neg 87.7% = 27462 sched 61.9% ret 16896
c [sweep-17-1] 38262706 steps 806 queries 271.50 avg class size
c [sweep-17-1] 17901 decisions 786 SAT calls 167.82 avg env size
c [sweep-17-1] 18670 variables remain 42% (25681 retained 58%)
c [decomp-58] removed 26 variables
c [sweep-17-1] removed 26 vars (0 failed, 19 eqs, 63 impls)
c [sweep-17] 26 < 1/1000 * 44358 = 44 considered unsuccessful
c [sweep-17] removed 26 vars in TOTAL (1 rounds, 805 queries)
c [sort-queue-21] sorted 8892 enqueued variables after 384976 conflicts
c [score-dist-21] active 35440 (80%), one 0 (0%), zero 8892 (20%)
c [score-dist-21] max exp 520, different 13 (2%)
c [score-dist-21] median active exp 520, avg 519.8
c [simplification-21] removed 264 variables 0.6% (44332 remain 18%)
c [simplification-21] removed 6719 irredundant clauses 2.1% (315906 remain 23%)
c [simplification-21] maximum reduction of 2% = max (1%, 2%)
c [simplification-21] geometric conflict interval increment 24888 = 74665 / 3
c [simplification-21] new conflict interval 99553
c [simplification-21] penalized conflict interval 99553 = 1 * 99553
c [simplification-21] hard conflict limit 534305 (soft 484529 + delta 49776)
c [simplification-21] new conflict limit 484529 (hard 534305)
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 -  792.7   44332   315906    413462   33050   6793 1178779  125   301   72  42%    653   48  145  108  134%
c -  855.2   44332   315906    460922   34447   6918 1178851   93   198   74  47%    844  -51  134  108  124%
c 
c [simplification-22] limit 484529 conflicts (hard 534305) hit after 489402 conflicts
c [quatres-17] found 20607 quaternary clauses 46% in total
c [quatres-17-2] added 2 single-self-subsuming ternary resolvents
c [quatres-17-2] added 1 quaternary resolvents
c [ternres-17] limit 158118151 with penalty 0 = 0 + 0
c [ternres-17] all 44332 free variables schedulable
c [ternres-17] 204 ternary resolvents (0 bin, 204 trn)
c [ternres-17] fully completed ternary resolution
c [gauss-8] limit 3952953 penalty 3 = 3 + 0
c [gauss-8] extracted 37 xors of average arity 3.0
c [gauss-8] connected 110 occurrences of 104 variables (average 1.1)
c [gauss-8] limit 3952953 penalty 3 = 3 + 0
c [gauss-8] fully completed
c [gauss-8] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-59] removed 1 variables
c [unhide-22] limit 5000000 with penalty 2 = 0 + 2
c [unhide-22-30] 0 units, 0 failed, 33682 tauts, 0 hbrs, 846977 literals
c [transred-18] limit 2000000 with penalty 0 = 0 + 0
c [transred-18] removed 175 transitive binary clauses
c [cce-8] boosting limit by 10
c [cce-8] limit of 988238445 steps penalty 3 = 3 + 0
c [cce-8-1] eliminated 1 clauses out of 1 (100%) of length 127
c [cce-8-1] eliminated 2 clauses out of 2 (100%) of length 126
c [cce-8-1] eliminated 1 clauses out of 1 (100%) of length 125
c [cce-8-1] eliminated 1 clauses out of 3 (33%) of length 124
c [cce-8-1] eliminated 2 clauses out of 2 (100%) of length 123
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 122
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 121
c [cce-8-1] eliminated 1 clauses out of 1 (100%) of length 120
c [cce-8-1] eliminated 1 clauses out of 3 (33%) of length 119
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 118
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 117
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 116
c [cce-8-1] eliminated 1 clauses out of 1 (100%) of length 115
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 114
c [cce-8-1] eliminated 1 clauses out of 3 (33%) of length 113
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 112
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 111
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 110
c [cce-8-1] eliminated 1 clauses out of 1 (100%) of length 109
c [cce-8-1] eliminated 1 clauses out of 3 (33%) of length 108
c [cce-8-1] eliminated 1 clauses out of 1 (100%) of length 107
c [cce-8-1] eliminated 1 clauses out of 3 (33%) of length 106
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 105
c [cce-8-1] eliminated 2 clauses out of 2 (100%) of length 104
c [cce-8-1] eliminated 1 clauses out of 1 (100%) of length 103
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 102
c [cce-8-1] eliminated 2 clauses out of 3 (67%) of length 101
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 99
c [cce-8-1] eliminated 2 clauses out of 2 (100%) of length 98
c [cce-8-1] eliminated 1 clauses out of 1 (100%) of length 97
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 96
c [cce-8-1] eliminated 3 clauses out of 3 (100%) of length 95
c [cce-8-1] eliminated 1 clauses out of 1 (100%) of length 94
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 93
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 91
c [cce-8-1] eliminated 2 clauses out of 3 (67%) of length 90
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 89
c [cce-8-1] eliminated 2 clauses out of 2 (100%) of length 88
c [cce-8-1] eliminated 1 clauses out of 1 (100%) of length 87
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 86
c [cce-8-1] eliminated 2 clauses out of 3 (67%) of length 85
c [cce-8-1] eliminated 2 clauses out of 2 (100%) of length 84
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 83
c [cce-8-1] eliminated 1 clauses out of 1 (100%) of length 82
c [cce-8-1] eliminated 2 clauses out of 3 (67%) of length 81
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 80
c [cce-8-1] eliminated 2 clauses out of 2 (100%) of length 79
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 78
c [cce-8-1] eliminated 2 clauses out of 2 (100%) of length 77
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 76
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 75
c [cce-8-1] eliminated 2 clauses out of 2 (100%) of length 74
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 73
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 72
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 71
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 70
c [cce-8-1] eliminated 2 clauses out of 2 (100%) of length 69
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 68
c [cce-8-1] eliminated 2 clauses out of 2 (100%) of length 67
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 66
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 65
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 63
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 62
c [cce-8-1] eliminated 2 clauses out of 2 (100%) of length 61
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 60
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 59
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 58
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 57
c [cce-8-1] eliminated 2 clauses out of 3 (67%) of length 56
c [cce-8-1] eliminated 2 clauses out of 3 (67%) of length 55
c [cce-8-1] eliminated 3 clauses out of 4 (75%) of length 54
c [cce-8-1] eliminated 3 clauses out of 4 (75%) of length 53
c [cce-8-1] eliminated 2 clauses out of 3 (67%) of length 52
c [cce-8-1] eliminated 2 clauses out of 2 (100%) of length 51
c [cce-8-1] eliminated 1 clauses out of 3 (33%) of length 50
c [cce-8-1] eliminated 2 clauses out of 2 (100%) of length 49
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 48
c [cce-8-1] eliminated 2 clauses out of 2 (100%) of length 47
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 46
c [cce-8-1] eliminated 1 clauses out of 3 (33%) of length 45
c [cce-8-1] eliminated 2 clauses out of 3 (67%) of length 44
c [cce-8-1] eliminated 3 clauses out of 4 (75%) of length 43
c [cce-8-1] eliminated 3 clauses out of 4 (75%) of length 42
c [cce-8-1] eliminated 2 clauses out of 6 (33%) of length 41
c [cce-8-1] eliminated 3 clauses out of 5 (60%) of length 40
c [cce-8-1] eliminated 5 clauses out of 7 (71%) of length 39
c [cce-8-1] eliminated 4 clauses out of 6 (67%) of length 38
c [cce-8-1] eliminated 4 clauses out of 8 (50%) of length 37
c [cce-8-1] eliminated 4 clauses out of 8 (50%) of length 36
c [cce-8-1] eliminated 7 clauses out of 11 (64%) of length 35
c [cce-8-1] eliminated 9 clauses out of 12 (75%) of length 34
c [cce-8-1] eliminated 8 clauses out of 12 (67%) of length 33
c [cce-8-1] eliminated 9 clauses out of 12 (75%) of length 32
c [cce-8-1] eliminated 8 clauses out of 12 (67%) of length 31
c [cce-8-1] eliminated 9 clauses out of 14 (64%) of length 30
c [cce-8-1] eliminated 7 clauses out of 11 (64%) of length 29
c [cce-8-1] eliminated 11 clauses out of 13 (85%) of length 28
c [cce-8-1] eliminated 6 clauses out of 12 (50%) of length 27
c [cce-8-1] eliminated 11 clauses out of 13 (85%) of length 26
c [cce-8-1] eliminated 6 clauses out of 14 (43%) of length 25
c [cce-8-1] eliminated 12 clauses out of 17 (71%) of length 24
c [cce-8-1] eliminated 9 clauses out of 18 (50%) of length 23
c [cce-8-1] eliminated 18 clauses out of 22 (82%) of length 22
c [cce-8-1] eliminated 11 clauses out of 20 (55%) of length 21
c [cce-8-1] eliminated 16 clauses out of 23 (70%) of length 20
c [cce-8-1] eliminated 15 clauses out of 22 (68%) of length 19
c [cce-8-1] eliminated 19 clauses out of 26 (73%) of length 18
c [cce-8-1] eliminated 15 clauses out of 26 (58%) of length 17
c [cce-8-1] eliminated 23 clauses out of 31 (74%) of length 16
c [cce-8-1] eliminated 22 clauses out of 32 (69%) of length 15
c [cce-8-1] eliminated 28 clauses out of 41 (68%) of length 14
c [cce-8-1] eliminated 21 clauses out of 34 (62%) of length 13
c [cce-8-1] eliminated 27 clauses out of 41 (66%) of length 12
c [cce-8-1] eliminated 32 clauses out of 44 (73%) of length 11
c [cce-8-1] eliminated 36 clauses out of 55 (65%) of length 10
c [cce-8-1] eliminated 38 clauses out of 53 (72%) of length 9
c [cce-8-1] eliminated 34 clauses out of 53 (64%) of length 8
c [cce-8-1] eliminated 37 clauses out of 85 (44%) of length 7
c [cce-8-1] eliminated 39 clauses out of 2622 (1%) of length 6
c [cce-8-1] eliminated 260 clauses out of 9208 (3%) of length 5
c [cce-8-1] eliminated 1500 clauses out of 18604 (8%) of length 4
c [cce-8-1] completed large round (ATE)
c [cce-8-1] eliminated 2441 large clauses in 460020004 steps
c [cce-8-1] allowing another 230010002 steps for small clauses
c [cce-8-1] scheduling 175679 clauses = 161162 binary + 14517 ternary
c [cce-8-1] tried to eliminate 50888 small clauses 29%
c [cce-8-1] eliminated 9316 binary clauses 6%
c [cce-8-1] eliminated 1293 ternary clauses 9%
c [cce-8-1] eliminated 10609 small clauses 6%
c [cce-8-1] eliminated 10609 small clauses in 988238450 steps
c [cce-8-1] incomplete small round (ATE)
c [cce-8-1] eliminated 13050 covered clauses in round 1
c [cce-8] eliminated 13050 covered clauses in TOTAL during 1 rounds
c [bca-18] limit of 10000000 steps and 607438 added (scaled 2)
c [bca-18] 60168 out of 88664 literals actually usable 68%
c [bca-18] added 23 blocked clauses in 184487 steps
c [sort-queue-22] sorted 8797 enqueued variables after 489402 conflicts
c [score-dist-22] active 35534 (80%), one 0 (0%), zero 8797 (20%)
c [score-dist-22] max exp 520, different 13 (2%)
c [score-dist-22] median active exp 520, avg 519.8
c [simplification-22] removed 1 variables 0.0% (44331 remain 18%)
c [simplification-22] removed 13086 irredundant clauses 4.1% (302820 remain 22%)
c [simplification-22] maximum reduction of 4% = max (0%, 4%)
c [simplification-22] geometric conflict interval increment 19910 = 99553 / 5
c [simplification-22] new conflict interval 119463
c [simplification-22] penalized conflict interval 119463 = 1 * 119463
c [simplification-22] hard conflict limit 668596 (soft 608865 + delta 59731)
c [simplification-22] new conflict limit 608865 (hard 668596)
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 -  942.5   44331   302820    509466   35825   8492 1154462  107   218   72  49%    938  -13  122  105  115%
c
c CAUGHT SIGNAL 15 SIGTERM
c
c s UNKNOWN
c bate: 3160 basic ate = 2990 trn 95% + 170 lrg 5% in 5 updates
c bcas: 18 count, 2620 added (427 skipped), 5082662 steps
c bkwd: tried 475352 clauses, 950182 lits, 2.00 lits/clause
c bkwd: checked 15442602 occs, 32.49 occs/clause, 16.25 occs/lit
c bkwd: subsumed 34 binary, 164 ternary, 60 large
c bkwd: strengthened 5 binary, 1 ternary (100% self), 1196 large (0% self)
c blkd: 6 bces, 12654 removed, 10658557 resolutions, 29915516 steps
c blkd: 16495 blocking literals 3%, 6 pure
c bump: 551782 bumped seen, 359353326 lits 651.3 on average
c card: 6 count, 0 units, 0 am1, 471840415 steps
c card: 0 rescheduled, 0 eliminated, 0 resolved, 79253 subsumed
c card: 18926 at-most-one constraints found, average size 4.78
c card: 18926 at-most-one constraints used 100%, average size 4.78
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: 8 cces, 67966 eliminated, 67192 ate 99%, 774 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: 4739857 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 165 gcs, 0 rescored clauses, 0 rescored vars
c dcps: 59 decompositions, 10313 equivalent 4%
c deco: 91271 decision-only clauses 17%, 74% reduction
c decs: 11438329 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 16 elims, 107234 eliminated 41%, 102 pure 0%
c elms: 46 rounds, 2.9 rounds/bve
c elms: 85588 small 80%, 21538 large 20%
c elms: 210602 tried small, 85588 succeeded 41%, 125014 failed 59%
c elms: 49753 subsumed, 70832 strengthened, 1599 blocked
c elms: 23455974 copies, 22999910 resolutions, 5402858 ipos
c elms: 7275136 subchks, 4077475 strchks
c gaus: 8 extractions, 502 extracted, 2.5 size, 3 max
c gaus: exported 1 units, 2 binary and 0 ternary equations
c gaus: 0 gc, 40561268 steps, 20280634 extr 50%, 3989 elim 0%
c glue: 95.0 orig avg, 95.0 real avg, 7.1 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 2760959 = 529500 simple 19% + 2207228 trn 80% + 24231 lrg 1%, 6244 sub 0%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 551781 clauses, 337.6 length
c lrnd: 186307652 lits = 273978568 orig - 87670916 removed 32%
c lrnd: 271526 uips 49%, 226795 flips 41%
c mins: 426049 mins 81%, 3176 bin 1%, 7465 size 1%
c mins: 320678141 poisoned searches, 77599277 hits, 24% hit rate
c mins: 365280040 used twice searches, 17407078 hits, 5% hit rate
c move: moved 43054, 29103 bin 68%, 13951 trn 32%
c otfs: 2199 driving 23%, 7394 restarting 77%
c otfs: str 9593, 9455 red 99%, 138 irr 1%
c otfs: str 9593, 0 bin 0%, 156 trn 2%, 9437 lrg 98%
c otfs: sub 31, 31 red 100%, 0 irr 0%
c otfs: sub 31, 0 bin 0%, 0 trn 0%, 31 lrg 100%
c phas: 16 computed, 147146 set, 16 pos (0%), 147130 neg (100%)
c prbs: 7 basic, 87490 probed, 3711 failed, 194 lifted
c prbs: 8 simple, 976344 probed, 1233 failed, 797 eqs
c prbs: 7 treelook, 368 probed, 27 failed, 0 lifted
c prom: 101864 locked 6% out of 1764227 tried
c prps: 1921669064 props, 158 props/dec
c prps: 94% srch, 6% simp, 0% lkhd
c quat: 17 count, 112 quat, 36 self1, 1 self2, 1725 dup
c queu: 22 sorted, 11438329 next (2841 steps 0.00)
c queu: 360368177 enq (4808839436 steps 13.34), 359353959 deq 100%
c redc: 6547 clauses 30%, 21580 tried 4%, 148 sat 1%
c redc: 17249 lits 7%, 236059 tried 0%, 148 sat 0%
c redc: 864 times jump level reduced, 57.9 levels on average
c reds: 9 count, 61207.3 conflicts per reduce
c reds: 0 memlim 0%, 9 arith 100%
c reds: 243040 collected 75%, 80016 retired 25%
c rmbd: 54233 removed, 11753 red 22%
c rsts: 15525 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: 22 count, 20 confs 91%, 0 vars 0%
c simp: 1 its 5%, 1 bin 5%, 0 trns 0%
c subl: 551781 count (722259 tried 1.3), 81017 sub out of 542212 (14.9%)
c swps: 17 count, 18 rounds, 10211 queries (567.3/round)
c swps: 9318 sat calls, 113 unsat (0.3% success rate)
c swps: 117993 decisions 12.7, 3115 conflicts 0.3
c swps; 574.4 avg class size, 108.0 avg environment size
c swps: 0 failed, 1699 impls, 960 equivs
c swp0: 3397 type 0 queries, 1421 unsat (41.8%), 3124 sat (92.0%)
c swp1: 6814 type 1 queries, 3776 unsat (55.4%), 6127 sat (89.9%)
c sync: 0 produced units, 0 successful consumptions 0%
c sync: 0 consume units calls, 0 tried 0%, 0 success 0%
c sync: 0 produced clauses, 0 successful consumptions 0%
c sync: 0 consume clause calls, 0 tried 0%, 0 success 0%
c time: 23981098 calls to obtain time
c tops: 97356 fixed 38%, 452 its, 1218.73 confs/it
c trds: 18 transitive reductions, 3581 removed, 34 failed
c trds: 17379 nodes, 55787 edges, 36035551 steps
c trim: 2222313 words, 8.5 MB
c trnr: 17 count, 10 bin, 4113 trn, 280613901 steps
c unhd: 22 count, 30 rounds, 111771265 steps
c unhd: 791 non-trivial sccs of average size 2.3
c unhd: 104 units, 104 bin, 0 trn, 0 lrg
c unhd: 8365 failed, 8305 stamp, 0 lits, 42 bin, 11 trn, 0 lrg
c unhd: 1091908 tauts, 29220 bin 3%, 17563 trn 2%, 644 lrg 0%
c unhd: 1091908 tauts, 1044481 stamp 96%, 1003915 red 92%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 6707696 str, 104 bin 0%, 2859 trn 0%, 6704733 lrg 100%, 6690539 red 100%
c vars: 44331 remaining 17% and 214903 removed 83% out of 259234
c vars: 97356 fixed 38%, 107234 eliminated 41%, 10313 equivalent 4%
c vsts: 18826629013 visits, 94% srch, 6% simp, 0% lkhd
c vsts: 9.8 search visits per propagation, 32052.1 per conflict
c wchs: 1888662065 pushed, 69865921 enlarged, 246 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all         542324        243040         80016      45091248       5514830        284383
c 
c  0 0         28553   5      6570   3         0   0  19631684  44   1649753  30     40081  14     2.0
c  1 5         11095   2      4824   2      1106   1   3435400   8    370317   7     14915   5     1.1
c  2 6         29459   5     14854   6      3169   4   5121852  11<   615305  11     28296  10     3.5
c  3 9         34685   6     18330   8      4049   5   3932139   9    508069   9<    25645   9     4.0
c  4 14        35518   7     19413   8      4516   6   3223031   7    465761   8     25944   9     4.9
c  5 21        38534   7     21416   9      5219   7   2872431   6    448690   8     26346   9<    5.7
c  6 30        42395   8     24725  10      6042   8   2070900   5    377598   7     24014   8     6.2
c  7 41        44731   8<    26108  11<     6754   8   2034395   5    353518   6     23755   8     9.7
c  8 54        47201   9     27653  11      7475   9<  1139192   3    249079   5     19778   7    16.0
c  9 69        43493   8     25522  11      6976   9    681713   2    159513   3     15952   6    17.2
c 10 86        51583  10     26480  11      9109  11    538599   1    149043   3     16980   6    14.5
c 11 126       73094  13     17847   7     10733  13    304522   1    115376   2     14866   5     7.4
c 12 230       55742  10      8578   4     13075  16     97529   0     49190   1      7280   3     7.9
c 13 534        6241   1       720   0      1793   2      7861   0      3618   0       531   0     1.9
c 
c avg                  7.2           6.7           8.2           2.3           3.4           5.0
c std                  3.6           3.1           3.2           2.8           3.3           3.5
c 
c  147.140  15% bump
c   72.134   7% probe
c   61.759   6% cce
c   39.676   4% unhide
c   30.702   3% sweep
c   21.579   2% elim
c    6.949   1% decide
c    4.794   0% bca
c 
c   13.385 < 1% rest (below)
c 
c    3.905   0% gauss
c    3.691   0% block
c    2.459   0% transred
c    1.882   0% ternres
c    0.992   0% quatres
c    0.457   0% card
c    0.000   0% locs
c    0.000   0% queuesort
c    0.000   0% rescore
c ==================================
c    5.130   1% preprocessing     2%
c  254.623  25% inprocessing     98%
c ==================================
c  259.753  26% simplifying
c  739.478  74% search
c ==================================
c  999.235 100% all
c 
c        550866 conflicts,         551.3 confs/sec
c          4286 ternaries,         128.5 confs/ternary
c          3996 binaries,          137.9 confs/binary
c           452 iterations,       1218.7 confs/iteration
c 
c             9 reductions,          0.0 redus/sec,  61207.3 confs/reduction
c         15525 restarts,           15.5 rests/sec,     35.5 confs/restart
c      11438329 decisions,       11447.1 decis/sec,     20.8 decis/conflict
c    1921669064 propagations,  1923140.2 props/sec,    168.0 props/decision
c 
c 999.2 seconds, 190.2 MB
c
c CAUGHT SIGNAL 15 SIGTERM
c
c launch: done
