c launch: /data/cnf/sc2014/app/UR-20-10p1.cnf.bz2
c host: atom18
c Lingeling SAT Solver
c 
c Version b7ztzu 7b29300825af9bcc1c8b2c5ebcf65fa1cb101cad
c 
c Copyright (C) 2010-2014 Armin Biere JKU Linz Austria.
c All rights reserved.
c 
c released Sun Apr 26 19:26:13 CEST 2015
c compiled Sun Apr 26 19:26:13 CEST 2015
c 
c gcc (Ubuntu 4.8.2-19ubuntu1) 4.8.2
c -Wall -O3 -I../yalsat -I../druplig -DNLGLOG -DNDEBUG -DNCHKSOL
c Linux cluster2 3.13.0-45-generic x86_64
c 
c piping '/data/cnf/sc2014/app/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=4
c --scoreshift=0
c --scoreresetint=2147483647
c --seed=0
c --simpbintinc=100
c --simpbintinclim=10000
c --simpcintdelay=2000
c --simpcintinc=20000
c --simpcintincdiv=1
c --simpcintmaxhard=10000000
c --simpcintmaxsoft=1000000
c --simpincdelmaxfact=50
c --simpincdelmaxmin=10000
c --simpinitdelay=0
c --simpintsizepen=0
c --simpen=0
c --simpidiv=3
c --simpiscale=100
c --simpitdelay=10
c --simpitintinc=10
c --simpitintinclim=1000
c --simplify=2
c --simprtc=5
c --simptintinc=1000
c --simptintinclim=10000
c --simpvarchg=100
c --simpvarlim=100
c --sizemaxpen=5
c --sizepen=1000000
c --sleeponabort=0
c --smallirr=90
c --smallve=1
c --smallvevars=10
c --smallvewait=0
c --sortlits=0
c --subl=9
c --sweep=1
c --sweepboost=10
c --sweepboostdel=4
c --sweepboostint=7
c --sweepboostvlim=1000000
c --sweepfacdec=10
c --sweepforgive=2
c --sweepirr=3
c --sweepmaxeff=200000000
c --sweepmaxdec=10000
c --sweepmaxround=3
c --sweepmindec=100
c --sweepmineff=1000000
c --sweepred=3
c --sweepreleff=3
c --sweeprtc=0
c --sweeprtcint=14
c --sweeprtcintvlim=100000
c --sweepsuccessmaxwortc=6
c --sweepsuccessrat=1000
c --sweepwait=2
c --synclsall=1
c --synclsglue=8
c --synclsint=100
c --synclslen=40
c --syncunint=111111
c --termint=122222
c --ternres=1
c --ternresboost=5
c --ternresrtc=0
c --ternreswait=2
c --transred=1
c --transredwait=2
c --trapiflush=0
c --trdmaxeff=2000000
c --trdmineff=100000
c --trdreleff=10
c --treelook=1
c --treelookboost=10
c --treelookfull=0
c --treelookmaxeff=50000000
c --treelookmineff=300000
c --treelookreleff=2
c --treelookrtc=0
c --trep=1
c --trepint=55555
c --trnreleff=10
c --trnrmaxeff=200000000
c --trnrmineff=4000000
c --unhdatrn=2
c --unhdextstamp=1
c --unhdhbr=0
c --unhdlnpr=3
c --unhdmaxeff=20000000
c --unhdmineff=100000
c --unhdreleff=2
c --unhdroundlim=20
c --unhide=1
c --unhidewait=0
c --usedtwice=1
c --vsidsdint=256
c --wait=1
c --waitmax=4
c --witness=0
c --check=0
c --log=-1
c --profile=1
c --profilelong=1
c --verbose=1
c [freezer] frozen 0 variables out of 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] VSIDS (--score=4) decay interval 256 (--vsidsdint=256)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c *    0.0  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        15      12      1 12549    0     5   59   1%      0    5    1    0 24855%
c i    5.2  120891   895640        34      26      3 12551    0     5   59   2%      0    5    2    0 24038%
c i    5.2  120775   895640        38      27      4 12552    0     6   59   2%      0    6    2    0 23742%
c i    5.3  120109   895640       114      84     15 12557    0     7   59   3%      0    7    3    0 19865%
c i    5.3  120099   895640       115      84     15 12557    0     7   59   3%      0    7    3    0 19788%
c i    5.3  119395   895640       116      84     15 12557    0     7   59   3%      0    7    3    0 19711%
c i    5.5  119378   895640       192     142     20 12568    1    12   59   4%      0   12    6    0 18100%
c i    5.5  119150   895640       194     142     21 12568    1    12   59   4%      0   12    6    0 17966%
c i    5.8  119136   895640       320     235     32 12580    1    20   60   4%      0   20    8    0 14793%
c i    5.9  119062   895640       460     352     40 12586    2    27   60   6%      0   27   15    0 14689%
c 
c [simplification-2] limit of 10 iterations hit after 10 iterations
c [decomp-3] removed 2113 variables
c [simpleprobe-2] 14574 schedulable variables 12%
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [simpleprobe-2] 12827 variables remain 11% (106111 retained 89%)
c [simpleprobe-2] removed 0 variables, found 1505 hbrs, 0 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 28212 literals 12%
c [treelook-1] scheduling used 309843 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 334103 steps
c [treelook-1] 28203 literals remain 12%
c [treelook-1] 28164 variables remain to probed next time 24%
c [treelook-1] removed 5 variables, found 2223 hbrs
c [basicprobe-1] limit 7050904 based on 881363 irredundant clauses
c [basicprobe-1-0] 43537 probes remain 38% after last round
c [basicprobe-1-0] 25 units = 25 failed (100%) + 0 lifted (0%)
c [basicprobe-1-0] removed 3487 variables, found 26522 hbrs
c [unhide-2] limit 55085 based on 881363 irredundant clauses
c [unhide-2-2] 5 units, 2015 failed, 9220 tauts, 0 hbrs, 1662 literals
c [elim-2] 60540 variables 53% will be scheduled this time
c [elim-2] scheduled 60540 variables 53%
c [elim-2] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-2] rescheduling of touched variables disabled
c [elim-2] incomplete 25503 not tried 22% in round 1
c [elim-2] transition to [ all 0 rem 1 ] state
c [elim-2] eliminated 54 = 0% variables out of 60540 scheduled
c [elim-2] considered successful since not run to completion yet
c [phase-count-2] 823128 negative 99.2% of 829748 except 6620 0.8%
c [phase-count-2] 667142 positive 80.4% of 829748 except 162606 19.6%
c [phase-count-2] less non-negative clauses 6620 than limit 82900 (10.0%)
c [phase-count-2] non-pos/non-neg = 162606/6620 = 24.56 >= 2.00 = 200/100
c [lucky-phase-2] forcing lucky phase -1
c [phase-2] phase bias: 0 positive 0%, 15527 negative 100%
c [sort-queue-2] sorted 100120 enqueued variables after 460 conflicts
c [score-dist-2] active 13665 (12%), one 0 (0%), zero 100120 (88%)
c [score-dist-2] max exp 507, different 8 (2%)
c [score-dist-2] median active exp 503, avg 502.9
c [simplification-2] removed 5212 variables 4.4% (113785 remain 46%)
c [simplification-2] removed 65892 irredundant clauses 7.4% (829748 remain 60%)
c [simplification-2] maximum reduction of 7% = max (4%, 7%)
c [simplification-2] forced so keeping old conflict interval 0
c [simplification-2] conflict limit remains at 1027 (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.4  113784   829748       491     375     39 29687    2    28   56   7%      0   28   20    0 15230%
c i   10.0  113632   829748       804     614     77 29710    3    56   56   6%      1   56   22    0 9560%
c i   10.1  113598   829748       868     655     84 29719    4    61   56   6%      1   61   25    0 9409%
c 
c [simplification-3] limit 1027 conflicts (hard 11000) hit after 1027 conflicts
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 3024 at-most-one constraints of average size 4.4
c [card-2] no at-most-two constraint found
c [card-2] using previous limit 1000000 for elimination
c [card-2] 3024 out of 3024 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [decomp-6] removed 450 variables
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] scheduled 77822 literals 34%
c [treelook-2] scheduling used 615097 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] used 463636 steps
c [treelook-2] 77729 literals remain 34%
c [treelook-2] 23781 variables remain to probed next time 21%
c [treelook-2] removed 88 variables, found 3206 hbrs
c [unhide-3] limit 51655 based on 826488 irredundant clauses
c [unhide-3-3] 4 units, 681 failed, 17228 tauts, 0 hbrs, 735 literals
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 112048 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 34351 not tried 31% in round 1
c [elim-3] transition to [ all 1 rem 1 ] state
c [elim-3] eliminated 2514 = 2% variables out of 112048 scheduled
c [elim-3] considered successful since not run to completion yet
c [phase-count-3] 788384 negative 99.2% of 794978 except 6594 0.8%
c [phase-count-3] 640100 positive 80.5% of 794978 except 154878 19.5%
c [phase-count-3] less non-negative clauses 6594 than limit 79400 (10.0%)
c [phase-count-3] non-pos/non-neg = 154878/6594 = 23.49 >= 2.00 = 200/100
c [lucky-phase-3] forcing lucky phase -1
c [phase-3] phase bias: 0 positive 0%, 9189 negative 100%
c [sort-queue-3] sorted 87754 enqueued variables after 1027 conflicts
c [score-dist-3] active 21780 (20%), one 0 (0%), zero 87754 (80%)
c [score-dist-3] max exp 507, different 11 (2%)
c [score-dist-3] median active exp 501, avg 500.9
c [simplification-3] removed 3863 variables 3.4% (109534 remain 45%)
c [simplification-3] removed 34770 irredundant clauses 4.2% (794978 remain 58%)
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 15027 (soft 5027 + delta 10000)
c [simplification-3] new conflict limit 5027 (hard 15027)
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.4  109533   794978      1187     786    118 29684    5    71   55   7%      1   70   19    0 5268%
c i   13.4  109524   794978      1188     786    118 29684    5    71   55   7%      1   70   19    0 5247%
c i   13.5  108808   794978      1255     833    129 29688    5    74   55   7%      1   73   16    0 4258%
c i   13.6  108745   794978      1269     840    132 29690    5    74   55   7%      1   73   15    0 4124%
c i   13.6  108538   794978      1273     839    134 29691    5    74   55   7%      1   73   15    0 4064%
c i   13.6  108520   794978      1274     839    134 29691    5    74   55   7%      1   73   15    0 4048%
c i   13.8  108513   794978      1404     942    142 29702    5    78   55   7%      1   77   15    0 3691%
c i   14.0  108276   794978      1483    1004    145 29709    6    84   55   7%      1   83   14    0 3454%
c i   14.2  108129   794978      1544    1059    149 29709    6    89   55   6%      1   88   14    0 3280%
c i   14.3  108059   794978      1547    1061    149 29709    6    89   55   6%      1   88   14    0 3280%
c i   14.3  107829   794978      1548    1061    149 29709    6    89   55   6%      1   88   14    0 3267%
c i   14.5  107823   794978      1609    1110    151 29713    6    92   55   6%      1   91   14    0 3267%
c i   14.8  107811   794978      1690    1177    156 29719    6   100   55   6%      1   99   17    0 3640%
c i   14.8  107800   794978      1691    1177    156 29719    6   100   55   6%      1   99   17    0 3626%
c i   14.8  107788   794978      1692    1177    156 29719    6   100   55   6%      1   99   17    0 3612%
c i   14.8  107775   794978      1693    1177    156 29719    6   100   55   6%      1   99   17    0 3598%
c i   14.8  107484   794978      1694    1177    156 29719    6   100   55   6%      1   99   17    0 3584%
c i   14.8  107472   794978      1695    1177    156 29719    6   100   55   6%      1   99   17    0 3570%
c i   15.4  107463   794978      1929    1365    167 29736    8   120   55   6%      1  118   26    1 4412%
c i   15.6  107458   794978      1974    1402    169 29736    8   123   55   7%      1  121   30    1 4841%
c i   15.7  107191   794978      2031    1447    170 29739    9   130   55   7%      1  128   40    1 5736%
c i   15.7  107187   794978      2032    1447    170 29739    9   130   55   7%      1  128   40    1 5714%
c i   15.8  107175   794978      2045    1457    170 29739    9   132   55   7%      1  130   39    1 5651%
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.4  106741   794978      2223    1601    186 29748   12   164   55   7%      1  162   62    1 6883%
c i   16.6  106713   794978      2247    1619    186 29753   13   168   55   8%      1  166   72    1 7436%
c i   17.8  106705   794978      2642    1967    195 29759   26   230   56  11%      2  226  141    2 7472%
c i   17.8  106693   794978      2643    1967    195 29759   26   230   56  11%      2  226  140    2 7443%
c i   18.2  106685   794978      2786    2095    197 29761   29   252   56  11%      2  248  127    2 5998%
c i   18.5  106671   794978      2893    2187    197 29765   32   269   57  12%      2  265  131    2 5634%
c i   18.6  106231   794978      2911    2202    199 29765   33   272   57  12%      2  268  146    2 6004%
c i   18.6  106230   794978      2912    2202    199 29765   33   272   57  12%      2  268  145    2 5981%
c i   18.6  106229   794978      2913    2202    199 29765   33   272   57  12%      2  267  145    2 5957%
c 
c [simplification-4] limit of 177 binary hit after 177 binaries
c [decomp-8] removed 3404 variables
c [basicprobe-2] limit 11507884 penalty 0 = 0 + 0
c [basicprobe-2-0] 36891 probes remain 36% after last round
c [basicprobe-2-0] 68 units = 68 failed (100%) + 0 lifted (0%)
c [basicprobe-2-0] removed 3584 variables, found 33339 hbrs
c [unhide-4] limit 230157 with penalty 1 = 0 + 1
c [unhide-4-4] 6 units, 999 failed, 9411 tauts, 0 hbrs, 10393 literals
c [elim-4] 24637 variables 24% will be scheduled this time
c [elim-4] scheduled 24637 variables 24%
c [elim-4] boosting limit by 20
c [elim-4] limit of 920630720 steps penalty 0 = 0 + 0
c [elim-4] rescheduling of touched variables disabled
c [elim-4-1] eliminated 5 variables 0% in round 1 in 48467099 steps
c [elim-4-1] backward subsumption/strengthening limit 48467000
c [elim-4-1-1] backward checking 148 touched variables 0%
c [elim-4-1-1] fully completed backward checking in 1 rounds
c [elim-4-1] subsumed 6 and strengthened 0 clauses in 148735 steps
c [elim-4-1] rescheduled 14 variables 0% by backward subsumption
c [elim-4-2] eliminated 1 variables 0% in round 2 in 11679 steps
c [elim-4-2] backward subsumption/strengthening limit 11600
c [elim-4-2-1] backward checking 9 touched variables 0%
c [elim-4-2-1] incomplete backward checking 0 remain 0%
c [elim-4-2] subsumed 1 and strengthened 2 clauses in 11601 steps
c [elim-4-2] rescheduled 6 variables 0% by backward subsumption
c [elim-4-3] eliminated 2 variables 0% in round 3 in 2827 steps
c [elim-4-3] backward subsumption/strengthening limit 2800
c [elim-4-3-1] backward checking 10 touched variables 0%
c [elim-4-3-1] incomplete backward checking 5 remain 50%
c [elim-4-3] subsumed 0 and strengthened 0 clauses in 2815 steps
c [elim-4] fully completed in 3 rounds
c [elim-4] transition to [ all 0 rem 0 ] state
c [elim-4] eliminated 8 = 0% variables out of 24637 scheduled
c [elim-4] 8 < 1/100 * 24637 = 246 considered unsuccessful
c [phase-count-4] 728140 negative 99.1% of 734734 except 6594 0.9%
c [phase-count-4] 592740 positive 80.7% of 734734 except 141994 19.3%
c [phase-count-4] less non-negative clauses 6594 than limit 73400 (10.0%)
c [phase-count-4] non-pos/non-neg = 141994/6594 = 21.53 >= 2.00 = 200/100
c [lucky-phase-4] forcing lucky phase -1
c [phase-4] phase bias: 0 positive 0%, 2317 negative 100%
c [sort-queue-4] sorted 59066 enqueued variables after 3038 conflicts
c [score-dist-4] active 42614 (42%), one 0 (0%), zero 59066 (58%)
c [score-dist-4] max exp 509, different 20 (4%)
c [score-dist-4] median active exp 501, avg 500.5
c [simplification-4] removed 4549 variables 4.3% (101680 remain 41%)
c [simplification-4] removed 60244 irredundant clauses 7.6% (734734 remain 53%)
c [simplification-4] maximum reduction of 8% = max (4%, 8%)
c [simplification-4] forced so keeping old conflict interval 4000
c [simplification-4] conflict limit remains at 5152 (hard 15027)
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   21.8  101679   734734      3115    2336    174 47968   41   293   54  14%      2  288  161    3 5326%
c i   21.8  101668   734734      3124    2344    174 47968   41   293   54  14%      2  288  158    3 5216%
c i   22.0  101665   734734      3259    2425    208 47982   41   296   54  14%      1  290  112    3 3607%
c i   22.4  101655   734734      3557    2625    226 47995   47   299   54  16%      2  292  125    4 3374%
c i   23.4  101653   734734      3960    2974    251 48007   54   345   55  16%      2  336  142    4 3211%
c i   24.4  101539   734734      4375    3304    254 48057   67   397   55  17%      3  385  163    6 2940%
c i   25.0  101533   734734      4608    3517    257 48063   71   427   56  17%      2  414  164    6 2721%
c i   25.9  101522   734734      4992    3860    258 48063   90   467   57  19%      3  451  256    8 3366%
c i   25.9  101518   734734      4993    3860    258 48063   90   467   57  19%      3  451  255    8 3353%
c i   25.9  101512   734734      4995    3861    258 48063   89   467   57  19%      3  451  254    8 3331%
c i   25.9  101510   734734      4997    3861    258 48064   89   466   57  19%      3  451  252    8 3305%
c i   25.9  101503   734734      4999    3861    258 48065   89   466   57  19%      3  451  250    8 3279%
c 
c [simplification-5] limit 5178 conflicts (hard 15027) hit after 5178 conflicts
c [quatres-1] found 42969 quaternary clauses 40% in total
c [quatres-1-2] added 2 single-self-subsuming ternary resolvents
c [ternres-1] boosting ternary resolution limit by 5
c [ternres-1] limit 20000000 with penalty 0 = 0 + 0
c [ternres-1] all 101501 free variables schedulable
c [ternres-1] 14 ternary resolvents (0 bin, 14 trn)
c [ternres-1] fully completed ternary resolution
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 36 xors of average arity 2.4
c [gauss-1] connected 88 occurrences of 88 variables (average 1.0)
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 68 variables
c [unhide-5] limit 375955 with penalty 1 = 0 + 1
c [unhide-5-5] 3 units, 300 failed, 12060 tauts, 0 hbrs, 33832 literals
c [transred-1] limit 2000000 with penalty 0 = 0 + 0
c [transred-1] removed 185 transitive binary clauses
c [transred-1] found 8 units
c [block-1] scheduling all variables this time
c [block-1] scheduled 100970 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 11210 blocked clauses
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 12 clauses out of 341 (4%) of length 10
c [cce-1-1] eliminated 116 clauses out of 2337 (5%) of length 9
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 128 large clauses in 30000001 steps
c [cce-1-1] allowing another 15000000 steps for small clauses
c [cce-1-1] scheduling 347557 clauses = 330706 binary + 16851 ternary
c [cce-1-1] tried to eliminate 396 small clauses 0%
c [cce-1-1] eliminated 121 binary clauses 0%
c [cce-1-1] eliminated 10 ternary clauses 0%
c [cce-1-1] eliminated 131 small clauses 0%
c [cce-1-1] eliminated 131 small clauses in 30000001 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 259 covered clauses in round 1
c [cce-1] eliminated 259 covered clauses in TOTAL during 1 rounds
c [cce-1] 259 < 1/100 * 706379 = 7063 considered unsuccessful
c [bca-1] limit of 10000000 steps and 1412740 added (scaled 2)
c [bca-1] 180975 out of 201942 literals actually usable 90%
c [bca-1] added 200 blocked clauses in 536156 steps
c [sweep-1] limit 1412240 based on 706120 irredundant clauses
c [sweep-1-1] 4694 pos 4.6% + 96276 neg 95.4% = 100970 sched 100.0% ret 0
c [sweep-1-1] 1726024 steps 15 queries 19042.13 avg class size
c [sweep-1-1] 197 decisions 13 SAT calls 76.46 avg env size
c [sweep-1-1] 100679 variables remain 100% (30 retained 0%)
c [decomp-10] removed 262 variables
c [sweep-1-1] removed 262 vars (0 failed, 2 eqs, 6 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 262 vars in TOTAL (1 rounds, 14 queries)
c [phase-count-5] 698445 negative 99.1% of 705019 except 6574 0.9%
c [phase-count-5] 578278 positive 82.0% of 705019 except 126741 18.0%
c [phase-count-5] less non-negative clauses 6574 than limit 70500 (10.0%)
c [phase-count-5] non-pos/non-neg = 126741/6574 = 19.28 >= 2.00 = 200/100
c [lucky-phase-5] forcing lucky phase -1
c [phase-5] phase bias: 0 positive 0%, 2135 negative 100%
c [sort-queue-5] sorted 51951 enqueued variables after 5178 conflicts
c [score-dist-5] active 48757 (48%), one 0 (0%), zero 51951 (52%)
c [score-dist-5] max exp 509, different 29 (6%)
c [score-dist-5] median active exp 498, avg 496.9
c [simplification-5] removed 793 variables 0.8% (100708 remain 41%)
c [simplification-5] removed 29715 irredundant clauses 4.0% (705019 remain 51%)
c [simplification-5] maximum reduction of 4% = max (1%, 4%)
c [simplification-5] geometric conflict interval increment 4000 = 20000 / 5
c [simplification-5] new conflict interval 8000
c [simplification-5] penalized conflict interval 8000 = 1 * 8000
c [simplification-5] hard conflict limit 23178 (soft 13178 + delta 10000)
c [simplification-5] new conflict limit 13178 (hard 23178)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   30.8  100707   705019      5277    4084    301 60041   98   479   58  21%      2  461  253    9 2969%
c i   31.8  100697   705019      5846    4574    308 60046  115   508   58  23%      3  487  245   10 2359%
c i   32.6  100693   705019      6223    4890    321 60065  116   546   58  21%      3  522  138   11 1249%
c i   32.8  100683   705019      6266    4929    321 60068  116   551   58  21%      3  527  130   11 1171%
c i   32.8  100616   705019      6280    4942    321 60068  116   553   58  21%      3  528  127   11 1142%
c i   32.9  100581   705019      6285    4946    321 60068  116   553   58  21%      3  529  126   11 1129%
c i   32.9  100571   705019      6286    4946    321 60068  116   553   58  21%      3  528  125   11 1124%
c i   32.9  100557   705019      6287    4946    321 60068  116   553   58  21%      3  528  125   11 1120%
c i   33.0  100548   705019      6336    4989    321 60070  118   558   58  21%      3  533  160   11 1412%
c i   33.3  100387   705019      6422    5062    326 60074  117   566   58  21%      3  540  135   11 1183%
c i   35.3  100379   705019      7127    5678    341 60096  130   643   60  20%      4  611  217   13 1620%
c i   36.1  100378   705019      7404    5822    341 60098  153   644   60  24%      4  609  379   15 2462%
c i   36.1  100377   705019      7406    5823    341 60098  153   644   60  24%      4  609  376   15 2443%
c i   36.9  100376   705019      7769    6123    342 60099  155   648   60  24%      3  610  228   16 1403%
c i   37.0  100363   705019      7770    6123    342 60099  155   648   60  24%      3  610  227   16 1398%
c i   37.2  100353   705019      7873    6190    343 60127  155   653   62  24%      3  614  206   16 1250%
c i   37.2  100330   705019      7874    6190    343 60127  155   653   62  24%      3  614  205   16 1245%
c i   37.2  100320   705019      7875    6190    343 60127  155   653   62  24%      3  614  204   16 1240%
c i   37.2  100310   705019      7876    6190    343 60127  155   653   62  24%      3  614  204   16 1235%
c i   37.3  100300   705019      7877    6190    343 60127  155   653   62  24%      3  614  203   16 1231%
c i   37.3  100288   705019      7878    6190    343 60127  155   652   62  24%      3  613  202   16 1226%
c i   37.3  100278   705019      7879    6190    343 60127  155   652   62  24%      3  613  201   16 1221%
c i   38.7  100264   705019      8386    6602    348 60135  176   677   62  26%      3  633  286   19 1506%
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   38.7  100255   705019      8387    6602    348 60135  176   677   62  26%      3  633  284   19 1501%
c i   38.7  100245   705019      8388    6602    348 60135  176   677   62  26%      3  633  283   19 1495%
c i   38.7  100219   705019      8389    6602    348 60135  176   676   62  26%      3  633  282   19 1489%
c i   38.7  100199   705019      8390    6602    348 60135  176   676   62  26%      3  633  281   19 1483%
c i   38.7  100174   705019      8391    6602    348 60135  176   676   62  26%      3  632  280   19 1477%
c i   38.8  100157   705019      8392    6602    348 60135  176   676   62  26%      3  632  279   19 1472%
c i   38.8  100150   705019      8393    6602    348 60135  176   676   62  26%      3  632  278   19 1466%
c i   38.8  100138   705019      8394    6602    348 60135  176   676   62  26%      3  632  277   19 1460%
c i   38.8  100126   705019      8395    6602    348 60135  176   675   62  26%      3  632  276   19 1454%
c i   39.1  100119   705019      8482    6684    348 60136  175   679   62  26%      3  634  240   19 1253%
c i   39.1  100114   705019      8483    6684    348 60136  175   679   62  26%      3  634  239   19 1249%
c i   40.1  100070   705019      8882    7033    355 60141  175   682   63  26%      3  633  177   20  886%
c i   40.2  100069   705019      8898    7043    355 60143  175   682   63  26%      3  634  180   20  898%
c i   40.8  100058   705019      9094    7161    360 60145  188   687   66  27%      3  636  316   21 1482%
c i   41.0   99874   705019      9153    7189    366 60145  192   687   66  28%      3  636  345   22 1589%
c i   41.4   99863   705019      9327    7337    373 60146  191   696   66  27%      2  643  266   22 1201%
c i   41.5   99861   705019      9453    7426    373 60146  195   697   66  28%      2  643  292   23 1288%
c i   41.6   99856   705019      9488    7450    373 60147  196   695   66  28%      2  641  288   23 1263%
c i   41.6   99852   705019      9572    7518    379 60147  196   689   66  29%      2  634  274   23 1187%
c i   41.6   99843   705019      9573    7518    379 60147  196   688   66  29%      2  634  273   23 1182%
c i   41.6   99842   705019      9574    7518    379 60147  196   688   66  29%      2  633  272   23 1177%
c i   41.6   99833   705019      9575    7518    379 60147  196   688   66  29%      2  633  270   23 1173%
c i   41.6   99832   705019      9576    7518    379 60147  196   688   66  29%      2  633  269   23 1168%
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   42.8   99820   705019     10477    8219    393 60155  204   658   67  31%      5  595  179   26  693%
c i   43.1   99647   705019     10607    8326    397 60160  201   670   67  30%      5  606  154   26  590%
c i   43.3   99637   705019     10662    8376    397 60161  201   671   67  30%      4  606  155   26  594%
c i   43.3   99634   705019     10672    8382    397 60161  201   671   67  30%      4  606  163   26  624%
c i   43.4   99633   705019     10718    8419    397 60165  201   671   67  30%      4  607  164   26  622%
c i   43.6   99632   705019     10802    8497    397 60168  198   676   67  29%      4  611  132   26  503%
c i   44.1   99627   705019     11021    8695    398 60171  194   693   67  28%      3  625  143   27  536%
c i   44.5   99621   705019     11168    8824    406 60171  192   702   67  27%      3  633  130   27  483%
c i   44.8   99218   705019     11263    8903    410 60174  193   705   67  27%      3  635  172   27  630%
c i   44.8   99217   705019     11264    8903    410 60174  193   704   67  27%      3  634  171   27  627%
c i   44.8   99216   705019     11265    8903    410 60174  193   704   67  27%      3  634  170   27  625%
c i   44.8   99215   705019     11266    8903    410 60174  193   704   67  27%      3  634  170   27  622%
c i   44.8   99214   705019     11267    8903    410 60174  193   704   67  27%      3  634  169   27  620%
c i   44.8   99213   705019     11268    8903    410 60174  193   704   67  27%      3  634  168   27  617%
c i   44.8   99212   705019     11269    8903    410 60174  193   704   67  27%      3  633  168   27  615%
c i   44.8   99211   705019     11270    8903    410 60174  193   703   67  27%      3  633  167   27  613%
c i   44.9   99210   705019     11273    8904    410 60175  193   703   67  27%      3  633  165   27  607%
c i   45.3   99209   705019     11496    9094    414 60179  195   715   71  27%      3  642  201   28  720%
c i   46.1   99208   705019     11798    9367    418 60190  187   754   72  25%      2  678  118   28  419%
c i   46.5   99167   705019     11932    9486    420 60197  190   767   72  25%      2  691  184   29  644%
c i   47.7   98700   705019     12422    9908    438 60202  200   807   73  25%      3  725  223   31  730%
c i   47.7   98699   705019     12423    9908    438 60202  200   807   73  25%      3  725  222   31  727%
c i   47.7   98698   705019     12424    9908    438 60202  200   807   73  25%      3  725  221   31  724%
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.8   98697   705019     12425    9908    438 60202  200   807   73  25%      3  725  220   31  721%
c i   48.4   98696   705019     12666   10105    446 60205  199   807   73  25%      2  722  200   31  642%
c i   48.4   98695   705019     12669   10107    446 60205  199   806   73  25%      2  722  199   31  640%
c i   48.5   98694   705019     12672   10109    446 60205  199   806   73  25%      2  722  199   31  639%
c i   49.3   98693   705019     12972   10357    449 60215  206   823   73  25%      2  735  292   32  902%
c i   49.7   98687   705019     13130   10466    450 60218  220   831   73  27%      2  741  421   34 1250%
c i   49.8   98679   705019     13131   10466    450 60218  220   831   73  27%      2  741  419   34 1246%
c i   49.8   98667   705019     13132   10466    450 60218  220   830   73  27%      2  741  417   34 1241%
c i   49.8   98655   705019     13133   10466    450 60218  220   830   73  27%      2  740  416   34 1236%
c i   49.9   98647   705019     13185   10514    450 60218  220   831   73  26%      2  741  376   34 1115%
c i   49.9   98641   705019     13186   10514    450 60218  220   831   73  26%      2  741  375   34 1110%
c i   50.3   98629   705019     13316   10614    450 60219  225   834   73  27%      2  742  369   34 1072%
c 
c [simplification-6] limit 13565 conflicts (hard 23178) hit after 13565 conflicts
c [quatres-2] found 38858 quaternary clauses 39% in total
c [ternres-2] limit 9606317 with penalty 0 = 0 + 0
c [ternres-2] all 98629 free variables schedulable
c [ternres-2] 0 ternary resolvents (0 bin, 0 trn)
c [ternres-2] 39898 variables remain 40% (58731 retained 60%)
c [card-3] limit 1200789 penalty 2 = 2 + 0
c [card-3] found 4089 at-most-one constraints of average size 4.2
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 1200789 for elimination
c [card-3] 4089 out of 4089 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [decomp-11] removed 2567 variables
c [simpleprobe-3] 11294 schedulable variables 12%
c [simpleprobe-3] limit 19212635 penalty 1 = 1 + 0
c [decomp-12] removed 38 variables
c [simpleprobe-3] 5685 variables remain 6% (92418 retained 94%)
c [simpleprobe-3] removed 38 variables, found 20334 hbrs, 19 units
c [unhide-6] limit 960631 with penalty 1 = 0 + 1
c [unhide-6-6] 3 units, 585 failed, 10383 tauts, 0 hbrs, 207255 literals
c [transred-2] limit 2000000 with penalty 0 = 0 + 0
c [transred-2] removed 281 transitive binary clauses
c [block-2] scheduling all variables this time
c [block-2] scheduled 97468 variables 100%
c [block-2] limit of 96063178 steps penalty 0 = 0 + 0
c [block-2] fully completed
c [block-2] transition to [ all 0 rem 0 ] state
c [block-2] eliminated 758 blocked clauses
c [block-2] 758 < 1/100 * 689979 = 6899 considered unsuccessful
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 97467 variables 100%
c [elim-5] limit of 96063178 steps penalty 1 = 1 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5-1] eliminated 3101 variables 3% in round 1 in 66982286 steps
c [elim-5-1] backward subsumption/strengthening limit 29080892
c [elim-5-1-1] backward checking 10156 touched variables 10%
c [elim-5-1-1] fully completed backward checking in 1 rounds
c [elim-5-1] subsumed 1 and strengthened 55 clauses in 4087955 steps
c [elim-5-1] rescheduled 136 variables 0% by backward subsumption
c [elim-5-2] eliminated 18 variables 0% in round 2 in 163440 steps
c [elim-5-2] backward subsumption/strengthening limit 163400
c [elim-5-2-1] backward checking 141 touched variables 0%
c [elim-5-2-1] incomplete backward checking 0 remain 0%
c [elim-5-2] subsumed 0 and strengthened 0 clauses in 163401 steps
c [elim-5-2] fully rescheduled 94348 variables 97%
c [elim-5] incomplete 19696 not tried 20% in round 3
c [elim-5] transition to [ all 1 rem 1 ] state
c [elim-5] eliminated 3128 = 3% variables out of 97467 scheduled
c [bca-2] limit of 10000000 steps and 1353370 added (scaled 2)
c [bca-2] 164864 out of 188680 literals actually usable 87%
c [bca-2] added 157 blocked clauses in 478457 steps
c [sweep-2] limit 2881895 penalty 0 = 0 + 0
c [sweep-2-1] 4964 pos 5.3% + 89346 neg 94.7% = 94310 sched 100.0% ret 29
c [sweep-2-1] 3080516 steps 35 queries 14358.66 avg class size
c [sweep-2-1] 143 decisions 29 SAT calls 62.62 avg env size
c [sweep-2-1] 93879 variables remain 100% (451 retained 0%)
c [decomp-13] removed 14 variables
c [sweep-2-1] removed 14 vars (0 failed, 5 eqs, 9 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 14 vars in TOTAL (1 rounds, 34 queries)
c [phase-count-6] 670065 negative 99.1% of 676280 except 6215 0.9%
c [phase-count-6] 553948 positive 81.9% of 676280 except 122332 18.1%
c [phase-count-6] less non-negative clauses 6215 than limit 67600 (10.0%)
c [phase-count-6] non-pos/non-neg = 122332/6215 = 19.68 >= 2.00 = 200/100
c [lucky-phase-6] forcing lucky phase -1
c [phase-6] phase bias: 0 positive 0%, 1255 negative 100%
c [sort-queue-6] sorted 42450 enqueued variables after 13565 conflicts
c [score-dist-6] active 51875 (55%), one 0 (0%), zero 42450 (45%)
c [score-dist-6] max exp 509, different 60 (12%)
c [score-dist-6] median active exp 499, avg 491.8
c [simplification-6] removed 4304 variables 4.4% (94325 remain 38%)
c [simplification-6] removed 28739 irredundant clauses 4.1% (676280 remain 49%)
c [simplification-6] maximum reduction of 4% = max (4%, 4%)
c [simplification-6] geometric conflict interval increment 4000 = 20000 / 5
c [simplification-6] new conflict interval 12000
c [simplification-6] penalized conflict interval 12000 = 1 * 12000
c [simplification-6] hard conflict limit 35565 (soft 25565 + delta 10000)
c [simplification-6] new conflict limit 25565 (hard 35565)
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   59.2   94324   676280     14034    7923    420 72459  274   865   63  32%      4  765  598   40 1501%
c i   59.2   94323   676280     14036    7924    420 72459  274   864   63  32%      4  765  596   40 1497%
c i   59.2   94322   676280     14037    7924    420 72459  274   864   63  32%      4  764  594   40 1492%
c i   59.2   94321   676280     14040    7926    420 72459  275   864   63  32%      4  764  594   40 1491%
c i   59.3   94320   676280     14045    7930    420 72459  275   864   63  32%      4  764  595   40 1492%
c i   59.3   94319   676280     14051    7935    420 72459  276   864   63  32%      4  764  599   40 1498%
c i   59.8   94318   676280     14257    8062    421 72459  289   862   63  34%      3  759  556   42 1338%
c i   59.8   94317   676280     14265    8068    421 72459  289   862   63  34%      3  759  546   42 1313%
c i   59.8   94316   676280     14267    8069    421 72459  289   861   63  34%      3  759  544   42 1308%
c i   59.8   94315   676280     14271    8072    421 72459  289   861   63  34%      3  759  539   42 1296%
c i   59.8   94314   676280     14273    8073    421 72459  289   861   63  34%      3  758  535   42 1286%
c i   59.9   94313   676280     14276    8075    421 72459  289   861   63  34%      3  758  532   42 1279%
c i   59.9   94312   676280     14279    8077    421 72459  289   861   63  34%      3  758  530   42 1273%
c i   61.6   94311   676280     14972    8698    429 72472  294   917   67  32%      4  806  396   44  890%
c i   61.6   94305   676280     14973    8698    429 72472  294   916   67  32%      4  805  395   44  887%
c i   61.6   94296   676280     14974    8698    429 72472  294   916   67  32%      4  805  393   44  883%
c i   61.6   94284   676280     14975    8698    429 72472  294   916   67  32%      4  805  392   44  880%
c i   61.6   94276   676280     14976    8698    429 72472  294   916   67  32%      4  805  390   44  877%
c i   61.6   94268   676280     14977    8698    429 72472  294   915   67  32%      4  805  388   44  873%
c i   61.7   94260   676280     14978    8698    429 72472  293   915   67  32%      4  804  387   44  870%
c i   62.7   94251   676280     15394    9052    433 72473  320   989   67  32%      4  873  574   48 1203%
c i   62.7   94250   676280     15395    9052    433 72473  320   988   67  32%      4  872  572   48 1198%
c i   62.7   94249   676280     15396    9052    433 72473  320   988   67  32%      4  872  570   48 1193%
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   62.7   94248   676280     15410    9059    433 72479  321   990   67  32%      4  874  567   48 1185%
c i   63.1   94247   676280     15529    9148    434 72489  335  1010   68  33%      3  892  654   49 1330%
c i   63.1   94246   676280     15530    9148    434 72489  334  1010   68  33%      3  892  652   49 1325%
c i   63.1   94245   676280     15531    9148    434 72489  334  1010   68  33%      3  892  649   49 1320%
c i   63.6   94244   676280     15717    9303    434 72489  351  1033   68  34%      3  913  676   51 1324%
c i   63.7   94243   676280     15718    9303    434 72489  351  1033   68  34%      3  913  673   51 1318%
c i   63.7   94242   676280     15719    9303    434 72489  351  1033   68  34%      3  912  671   51 1313%
c i   63.7   94241   676280     15720    9303    434 72489  351  1032   68  34%      3  912  668   51 1308%
c i   63.7   94240   676280     15721    9303    434 72489  351  1032   68  34%      3  912  665   51 1303%
c i   66.1   94239   676280     16658   10009    448 72511  418  1122   74  37%      6  989  541   60  902%
c i   68.7   94073   676280     17515   10662    473 72599  424  1134   74  37%      6  987  345   65  530%
c i   68.7   94072   676280     17523   10666    473 72602  423  1133   74  37%      6  986  336   65  516%
c i   69.6   94071   676280     17942   10994    512 72617  398  1118   74  36%      5  965  205   66  312%
c i   70.1   94070   676280     18130   11119    517 72634  403  1115   74  36%      4  960  373   67  558%
c i   70.1   94060   676280     18131   11119    517 72634  403  1115   74  36%      4  959  372   67  556%
c i   70.2   94049   676280     18162   11145    517 72636  401  1112   74  36%      4  956  350   67  523%
c i   70.2   94048   676280     18164   11146    517 72636  401  1112   74  36%      4  955  348   67  520%
c i   70.2   94047   676280     18166   11147    517 72636  401  1111   74  36%      4  955  347   67  518%
c i   70.5   94046   676280     18249   11218    517 72636  397  1106   74  36%      4  949  312   67  464%
c i   71.0   94037   676280     18437   11386    523 72640  387  1100   78  35%      3  940  240   67  356%
c i   73.0   94029   676280     19289   12022    555 72711  364  1072   78  34%      5  901  239   70  342%
c i   73.5   94028   676280     19531   12232    563 72712  359  1065   78  34%      4  890  271   71  384%
c i   73.5   94021   676280     19536   12234    563 72712  359  1064   78  34%      4  889  275   71  389%
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   73.6   94020   676280     19551   12248    563 72712  359  1063   78  34%      4  888  274   71  387%
c i   74.8   94019   676280     19997   12622    577 72725  355  1066   78  33%      4  885  385   72  532%
c i   74.8   94016   676280     20002   12626    577 72725  355  1066   78  33%      4  885  385   72  532%
c i   74.9   94013   676280     20003   12626    577 72725  355  1066   78  33%      4  885  383   72  529%
c i   75.2   94007   676280     20108   12707    579 72725  365  1069   78  34%      3  887  511   73  695%
c i   75.2   94006   676280     20116   12711    579 72728  365  1069   78  34%      3  886  507   74  690%
c i   75.2   94005   676280     20122   12716    579 72728  366  1069   78  34%      3  886  510   74  694%
c i   75.2   94004   676280     20124   12717    579 72728  366  1069   78  34%      3  886  510   74  694%
c i   75.4   94003   676280     20175   12759    579 72728  370  1070   78  35%      3  887  544   74  734%
c i   75.6   93667   676280     20264   12842    581 72729  367  1074   78  34%      3  889  461   74  620%
c i   75.9   93625   676280     20388   12947    586 72732  367  1076   78  34%      3  890  427   75  570%
c i   75.9   93618   676280     20390   12947    586 72732  367  1076   78  34%      3  890  428   75  572%
c i   76.0   93611   676280     20432   12978    586 72738  368  1076   78  34%      2  889  434   75  578%
c i   76.9   93610   676280     20761   13216    601 72752  376  1090   78  35%      2  899  471   77  612%
c i   76.9   93609   676280     20763   13217    601 72752  376  1090   78  35%      2  898  472   77  612%
c i   77.0   93608   676280     20794   13243    601 72752  376  1090   78  35%      2  898  460   77  596%
c i   77.0   93607   676280     20796   13244    601 72752  376  1090   78  34%      2  898  457   77  592%
c i   77.1   93606   676280     20798   13245    601 72752  376  1090   78  34%      2  898  454   77  588%
c i   77.1   93605   676280     20800   13246    601 72752  376  1089   78  34%      2  898  451   77  585%
c i   77.1   93604   676280     20825   13256    603 72762  375  1090   78  34%      2  898  428   77  554%
c i   77.2   93600   676280     20844   13273    603 72763  374  1090   78  34%      2  898  419   77  542%
c i   77.2   93592   676280     20845   13273    603 72763  374  1090   78  34%      2  898  417   77  540%
c i   77.8   93591   676280     21078   13465    612 72766  373  1091   78  34%      2  896  363   78  464%
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   78.1   93583   676280     21183   13538    612 72767  379  1090   90  35%      2  893  456   79  576%
c i   78.4   93582   676280     21266   13591    616 72768  380  1090   90  35%      1  891  450   80  565%
c i   79.1   93574   676280     21568   13811    632 72770  385  1086   92  35%      1  884  422   81  520%
c i   82.7   93567   676280     22913   14723    668 72816  431  1057   92  41%      9  838  677   91  748%
c i   82.7   93560   676280     22914   14723    668 72816  431  1057   92  41%      9  837  674   91  745%
c i   82.8   93559   676280     22915   14723    668 72816  431  1057   92  41%      9  837  672   91  742%
c i   84.2   93558   676280     23415   15039    675 72861  430  1029   92  42%      7  803  471   93  507%
c i   85.1   93549   676280     23787   15243    675 72864  437  1001   93  44%      5  771  488   95  511%
c i   85.6   93548   676280     23960   15298    676 72864  439   985   93  45%      4  753  487   96  505%
c i   87.4   93547   676280     24608   15668    678 72864  426   927   94  46%      4  688  356   99  360%
c i   87.4   93540   676280     24611   15670    678 72864  426   927   94  46%      4  688  351   99  355%
c i   87.4   93536   676280     24612   15670    678 72864  426   927   94  46%      4  688  350   99  354%
c i   87.4   93534   676280     24614   15671    678 72864  426   927   94  46%      4  687  347   99  351%
c i   87.4   93529   676280     24615   15671    678 72864  426   926   94  46%      4  687  346   99  350%
c i   87.4   93522   676280     24617   15672    678 72864  425   926   94  46%      4  687  343   99  347%
c i   87.5   93516   676280     24619   15673    678 72864  425   926   94  46%      4  686  341   99  345%
c i   87.5   93514   676280     24621   15674    678 72864  425   926   94  46%      4  686  338   99  342%
c i   87.5   93506   676280     24623   15675    678 72864  425   925   94  46%      4  686  335   99  339%
c i   88.6   93501   676280     25134   16086    688 72872  401   903   95  44%      4  659  238  100  238%
c i   88.7   93500   676280     25200   16141    688 72873  400   904   95  44%      4  659  262  100  262%
c i   89.6   93499   676280     25512   16375    702 72884  409   916   95  45%      3  668  466  102  456%
c i   89.6   93498   676280     25513   16375    702 72884  409   916   95  45%      3  668  464  102  454%
c i   89.6   93497   676280     25516   16377    702 72884  409   916   95  45%      3  667  459  102  450%
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   90.4   93496   676280     25817   16543    707 72892  416   902   95  46%      3  650  502  104  483%
c 
c [simplification-7] limit 25903 conflicts (hard 35565) hit after 25903 conflicts
c [gauss-2] limit 1907871 penalty 1 = 1 + 0
c [gauss-2] extracted 45 xors of average arity 2.5
c [gauss-2] connected 113 occurrences of 106 variables (average 1.1)
c [gauss-2] limit 1907871 penalty 1 = 1 + 0
c [gauss-2] fully completed
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-14] removed 57 variables
c [treelook-3] limit 1907871 penalty 0 = 0 + 0 boost 1
c [treelook-3] scheduled 140326 literals 75%
c [treelook-3] scheduling used 1893824 steps
c [treelook-3] scheduled completely
c [treelook-3] limit 1907871 penalty 0 = 0 + 0 boost 1
c [treelook-3] used 1920909 steps
c [treelook-3] 140103 literals remain 75%
c [treelook-3] 18479 variables remain to probed next time 20%
c [treelook-3] removed 103 variables, found 14556 hbrs
c [unhide-7] limit 953935 with penalty 2 = 0 + 2
c [unhide-7-7] 1 units, 268 failed, 10700 tauts, 0 hbrs, 482278 literals
c [transred-3] limit 2000000 with penalty 0 = 0 + 0
c [transred-3] removed 197 transitive binary clauses
c [transred-3] found 2 units
c [cce-2] limit of 47696783 steps penalty 1 = 1 + 0
c [cce-2-1] eliminated 46 clauses out of 1769 (3%) of length 9
c [cce-2-1] eliminated 40 clauses out of 554 (7%) of length 8
c [cce-2-1] eliminated 78 clauses out of 821 (10%) of length 7
c [cce-2-1] eliminated 3471 clauses out of 6014 (58%) of length 6
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] eliminated 3635 large clauses in 47696785 steps
c [cce-2-1] allowing another 23848392 steps for small clauses
c [cce-2-1] scheduling 324935 clauses = 302802 binary + 22133 ternary
c [cce-2-1] tried to eliminate 615 small clauses 0%
c [cce-2-1] eliminated 198 binary clauses 0%
c [cce-2-1] eliminated 21 ternary clauses 0%
c [cce-2-1] eliminated 219 small clauses 0%
c [cce-2-1] eliminated 3392 small clauses in 47696791 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 7027 covered clauses in round 1
c [cce-2] eliminated 7027 covered clauses in TOTAL during 1 rounds
c [elim-6] 19554 variables 21% will be scheduled this time
c [elim-6] scheduled 19554 variables 21%
c [elim-6] limit of 381574267 steps penalty 0 = 0 + 0
c [elim-6] rescheduling of touched variables disabled
c [elim-6-1] no variable eliminated in round 1 in 40528776 steps
c [elim-6] fully completed in 1 rounds
c [elim-6] transition to [ all 0 rem 0 ] state
c [elim-6] eliminated 4 = 0% variables out of 19554 scheduled
c [elim-6] 4 < 1/100 * 19554 = 195 considered unsuccessful
c [bca-3] limit of 10000000 steps and 1307630 added (scaled 2)
c [bca-3] 155554 out of 186050 literals actually usable 84%
c [bca-3] added 43 blocked clauses in 445885 steps
c [sweep-3] limit 5723614 penalty 0 = 0 + 0
c [sweep-3-1] 4675 pos 5.0% + 87930 neg 95.0% = 92605 sched 99.5% ret 419
c [sweep-3-1] 5778340 steps 44 queries 13836.43 avg class size
c [sweep-3-1] 500 decisions 39 SAT calls 124.87 avg env size
c [sweep-3-1] 91696 variables remain 99% (1309 retained 1%)
c [decomp-16] removed 25 variables
c [sweep-3-1] removed 25 vars (0 failed, 6 eqs, 12 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 25 vars in TOTAL (1 rounds, 43 queries)
c [phase-count-7] 650475 negative 99.6% of 653217 except 2742 0.4%
c [phase-count-7] 535141 positive 81.9% of 653217 except 118076 18.1%
c [phase-count-7] less non-negative clauses 2742 than limit 65300 (10.0%)
c [phase-count-7] non-pos/non-neg = 118076/2742 = 43.06 >= 2.00 = 200/100
c [lucky-phase-7] forcing lucky phase -1
c [phase-7] phase bias: 0 positive 0%, 396 negative 100%
c [sort-queue-7] sorted 35668 enqueued variables after 25903 conflicts
c [score-dist-7] active 57331 (62%), one 0 (0%), zero 35668 (38%)
c [score-dist-7] max exp 509, different 109 (21%)
c [score-dist-7] median active exp 487, avg 477.5
c [simplification-7] removed 497 variables 0.5% (92999 remain 38%)
c [simplification-7] removed 23063 irredundant clauses 3.4% (653217 remain 48%)
c [simplification-7] maximum reduction of 3% = max (1%, 3%)
c [simplification-7] geometric conflict interval increment 5000 = 20000 / 4
c [simplification-7] new conflict interval 17000
c [simplification-7] penalized conflict interval 17000 = 1 * 17000
c [simplification-7] hard conflict limit 52903 (soft 42903 + delta 10000)
c [simplification-7] new conflict limit 42903 (hard 52903)
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   98.7   92998   653217     26143   16683    713 89460  412   882   98  47%      2  627  411  105  391%
c i   98.7   92995   653217     26159   16694    714 89461  411   881   98  47%      2  627  399  105  379%
c i   98.8   92993   653217     26165   16695    714 89461  411   881   98  47%      2  626  396  105  376%
c i   98.8   92990   653217     26168   16695    714 89461  411   881   98  47%      2  626  397  105  377%
c i   99.0   92988   653217     26266   16740    714 89466  413   877   98  47%      2  621  438  106  413%
c i  100.2   92984   653217     26704   17008    717 89491  415   858   98  48%      2  598  391  108  362%
c i  100.2   92983   653217     26723   17018    717 89491  415   857   98  48%      2  597  394  108  364%
c i  100.9   92979   653217     27009   17248    719 89496  412   850   98  48%      2  587  372  109  341%
c i  101.0   92978   653217     27066   17292    720 89496  409   849   98  48%      2  586  340  109  312%
c i  101.1   92970   653217     27112   17322    725 89497  407   849   98  48%      2  586  326  109  298%
c i  103.6   92966   653217     27939   17939    734 89503  410   847   98  48%      4  576  321  113  283%
c i  103.7   92959   653217     27978   17972    737 89503  410   846   98  48%      4  575  333  113  293%
c i  107.6   92958   653217     29790   19467    768 89533  372   838   98  44%     14  551  238  119  201%
c i  107.6   92957   653217     29794   19470    768 89533  372   838   98  44%     14  551  241  119  203%
c i  107.6   92956   653217     29795   19470    768 89533  372   837   98  44%     14  551  240  119  203%
c i  107.6   92955   653217     29796   19470    768 89533  372   837   98  44%     14  551  239  119  202%
c i  107.6   92954   653217     29797   19470    768 89533  372   837   98  44%     14  550  238  119  201%
c i  107.6   92953   653217     29798   19470    768 89533  372   837   98  44%     14  550  237  119  200%
c i  107.7   92952   653217     29815   19480    768 89534  373   837   98  44%     14  551  261  119  220%
c i  107.7   92951   653217     29816   19480    768 89534  372   837   98  44%     14  550  260  119  219%
c i  107.7   92950   653217     29817   19480    768 89534  372   837   98  44%     14  550  259  119  218%
c i  107.8   92949   653217     29828   19489    768 89534  373   837   98  45%     14  550  268  119  226%
c i  107.9   92948   653217     29850   19502    768 89534  374   838   98  45%     14  551  304  119  255%
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i  107.9   92947   653217     29851   19502    768 89534  374   838   98  45%     14  551  302  119  254%
c i  107.9   92946   653217     29852   19502    768 89534  374   838   98  45%     14  550  301  119  253%
c i  107.9   92945   653217     29857   19506    768 89534  374   837   98  45%     13  550  303  119  255%
c i  108.1   92937   653217     29917   19559    767 89535  375   840   98  45%     13  552  332  119  278%
c i  109.0   92899   653217     30314   19884    768 89538  380   862   98  44%      9  571  417  121  344%
c i  109.1   92898   653217     30349   19907    768 89539  382   862   98  44%      9  571  435  121  358%
c i  109.1   92897   653217     30350   19907    768 89539  382   862   98  44%      9  571  433  121  357%
c i  109.2   92896   653217     30366   19909    768 89539  383   862   98  44%      9  571  454  121  374%
c i  109.7   92895   653217     30519   20005    768 89540  386   861   98  45%      7  569  450  122  368%
c i  110.3   92894   653217     30721   20172    769 89541  387   860   98  45%      6  566  423  123  344%
c i  111.9   92889   653217     31280   20559    773 89545  404   869   98  47%      5  570  506  126  400%
c i  112.2   92888   653217     31354   20592    773 89545  411   869   98  47%      4  569  572  127  450%
c i  115.3   92887   653217     32539   21487    782 89549  445   911   98  49%      8  600  607  135  451%
c i  115.5   92886   653217     32643   21555    782 89550  449   911   98  49%      7  600  605  135  447%
c i  117.7   92885   653217     33390   22134    789 89556  450   921   98  49%      6  603  441  139  318%
c i  117.7   92884   653217     33391   22134    789 89556  450   920   98  49%      6  603  439  139  316%
c i  118.6   92883   653217     33710   22309    794 89557  469   923  120  51%      4  602  611  142  432%
c i  121.7   92882   653217     34601   22782    795 89559  511   923  120  55%      5  595  610  149  410%
c i  122.3   92881   653217     34813   22923    796 89560  515   919  120  56%      4  588  596  150  397%
c i  122.4   92880   653217     34839   22945    796 89560  515   918  120  56%      4  587  599  150  398%
c i  122.9   92874   653217     34976   23048    796 89560  522   914  120  57%      4  583  656  152  433%
c i  123.0   92864   653217     34985   23055    796 89560  522   914  120  57%      3  582  653  152  431%
c i  123.0   92859   653217     34989   23057    796 89560  522   914  120  57%      3  582  651  152  429%
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.0   92849   653217     34990   23057    796 89560  522   913  120  57%      3  581  649  152  428%
c i  123.0   92840   653217     34991   23057    796 89560  522   913  120  57%      3  581  646  152  426%
c i  123.0   92835   653217     34992   23057    796 89560  522   913  120  57%      3  581  644  152  424%
c i  123.0   92830   653217     34993   23057    796 89560  522   913  120  57%      3  581  641  152  423%
c i  123.0   92825   653217     34994   23057    796 89560  522   913  120  57%      3  581  639  152  421%
c i  123.0   92818   653217     34995   23057    796 89560  522   912  120  57%      3  580  636  152  419%
c i  123.0   92813   653217     34996   23057    796 89560  522   912  120  57%      3  580  634  152  418%
c i  125.7   92807   653217     35843   23586    821 89583  513   882  120  58%      5  543  462  156  296%
c i  125.7   92806   653217     35844   23586    821 89583  513   882  120  58%      5  543  460  156  295%
c i  125.8   92805   653217     35891   23607    821 89586  513   880  120  58%      4  541  472  156  303%
c i  126.7   92804   653217     36216   23821    827 89588  507   875  120  58%      3  533  455  157  289%
c i  127.2   92803   653217     36378   23953    827 89588  503   875  120  58%      3  532  438  158  277%
c i  130.3   92802   653217     37494   24746    834 89591  481   851  120  57%      6  498  363  162  224%
c i  131.1   92801   653217     37754   24914    839 89596  471   839  120  56%      5  485  323  163  198%
c i  131.2   92797   653217     37789   24946    839 89596  469   837  120  56%      5  483  311  163  191%
c i  131.9   92796   653217     38101   25191    839 89597  463   819  120  56%      4  462  357  164  218%
c i  133.3   92795   653217     38855   25678    840 89597  451   779  120  58%      4  418  412  166  248%
c i  133.3   92785   653217     38857   25678    840 89597  451   779  120  58%      4  418  410  166  247%
c i  134.2   92776   653217     39271   25997    858 89603  437   761  132  57%      3  397  334  167  200%
c i  134.5   92771   653217     39396   26086    857 89604  435   754  132  58%      3  389  337  168  201%
c i  135.7   92764   653217     40016   26563    868 89607  414   728  132  57%      3  360  276  169  163%
c i  136.0   92763   653217     40110   26641    868 89607  410   726  132  56%      2  357  253  169  150%
c i  136.4   92762   653217     40247   26755    868 89607  404   725  132  56%      2  355  243  169  144%
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i  136.5   92761   653217     40295   26786    868 89607  403   725  132  56%      2  355  260  169  154%
c i  136.6   92760   653217     40327   26812    869 89607  403   725  132  56%      2  355  269  169  159%
c i  136.6   92759   653217     40328   26812    869 89607  403   725  132  56%      2  355  268  169  158%
c i  136.7   92754   653217     40353   26834    869 89607  403   724  132  56%      2  354  280  169  166%
c i  136.7   92753   653217     40355   26834    869 89607  403   724  132  56%      2  354  281  169  166%
c i  136.9   92752   653217     40423   26895    869 89607  400   725  132  55%      1  355  268  169  158%
c i  138.3   92751   653217     40989   27389    870 89627  390   758  132  51%      2  385  278  170  163%
c i  138.9   92750   653217     41211   27580    870 89628  395   780  132  51%      1  406  414  171  241%
c i  138.9   92749   653217     41212   27580    870 89628  395   780  132  51%      1  406  412  171  240%
c i  138.9   92748   653217     41213   27580    870 89628  395   780  132  51%      1  405  410  171  239%
c i  140.0   92747   653217     41586   27885    886 89633  391   821  137  48%      1  444  361  172  209%
c i  141.2   92733   653217     42085   28319    889 89634  403   859  137  47%      2  479  489  175  279%
c i  141.8   92732   653217     42366   28580    889 89634  399   867  137  46%      1  484  381  176  217%
c i  142.1   92713   653217     42462   28665    890 89634  397   871  137  46%      1  488  367  176  209%
c i  142.2   92712   653217     42501   28699    890 89635  398   873  137  46%      1  489  375  176  213%
c i  142.4   92689   653217     42580   28766    890 89637  399   875  137  46%      1  491  397  176  225%
c i  142.7   92688   653217     42668   28834    890 89637  406   877  137  46%      1  493  493  177  279%
c i  142.7   92687   653217     42669   28834    890 89637  405   877  137  46%      1  492  492  177  278%
c 
c [simplification-8] limit 43144 conflicts (hard 52903) hit after 43145 conflicts
c [quatres-3] found 40958 quaternary clauses 43% in total
c [quatres-3-2] added 4 quaternary resolvents
c [ternres-3] limit 15614873 with penalty 1 = 1 + 0
c [ternres-3] 37441 schedulable variables 40%
c [ternres-3] 62 ternary resolvents (0 bin, 62 trn)
c [ternres-3] fully completed ternary resolution
c [decomp-17] removed 361 variables
c [basicprobe-3] limit 156148737 penalty 0 = 0 + 0
c [basicprobe-3-0] 28891 probes remain 32% after last round
c [basicprobe-3-0] 578 units = 574 failed (99%) + 4 lifted (1%)
c [basicprobe-3-0] removed 2409 variables, found 385687 hbrs
c [bate-1] eliminated 279 asymmetric tautologies during probing
c [unhide-8] limit 780743 with penalty 3 = 0 + 3
c [unhide-8-8] 10 units, 862 failed, 62377 tauts, 0 hbrs, 599869 literals
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 154 transitive binary clauses
c [transred-4] found 1 units
c [block-3] scheduling all variables this time
c [block-3] scheduled 89588 variables 100%
c [block-3] limit of 156148737 steps penalty 1 = 1 + 0
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 694 blocked clauses
c [block-3] 694 < 1/100 * 634667 = 6346 considered unsuccessful
c [cce-3] limit of 156148737 steps penalty 0 = 0 + 0
c [cce-3-1] eliminated 1 clauses out of 869 (0%) of length 7
c [cce-3-1] eliminated 120 clauses out of 2300 (5%) of length 6
c [cce-3-1] eliminated 7408 clauses out of 43146 (17%) of length 5
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 7529 large clauses in 156148739 steps
c [cce-3-1] allowing another 78074369 steps for small clauses
c [cce-3-1] scheduling 314794 clauses = 294151 binary + 20643 ternary
c [cce-3-1] tried to eliminate 2476 small clauses 1%
c [cce-3-1] eliminated 707 binary clauses 0%
c [cce-3-1] eliminated 82 ternary clauses 0%
c [cce-3-1] eliminated 789 small clauses 0%
c [cce-3-1] eliminated 789 small clauses in 156148740 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 8318 covered clauses in round 1
c [cce-3] eliminated 8318 covered clauses in TOTAL during 1 rounds
c [bca-4] limit of 10000000 steps and 1237904 added (scaled 2)
c [bca-4] 145886 out of 179126 literals actually usable 81%
c [bca-4] added 52 blocked clauses in 409166 steps
c [sweep-4] limit 9368924 penalty 0 = 0 + 0
c [sweep-4-1] 4404 pos 5.0% + 84024 neg 95.0% = 88428 sched 98.7% ret 1134
c [sweep-4-1] 9399408 steps 80 queries 6746.76 avg class size
c [sweep-4-1] 1558 decisions 65 SAT calls 269.49 avg env size
c [sweep-4-1] 85665 variables remain 96% (3878 retained 4%)
c [decomp-18] removed 144 variables
c [sweep-4-1] removed 144 vars (0 failed, 15 eqs, 30 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 144 vars in TOTAL (1 rounds, 79 queries)
c [phase-count-8] 616669 negative 99.8% of 618161 except 1492 0.2%
c [phase-count-8] 503868 positive 81.5% of 618161 except 114293 18.5%
c [phase-count-8] less non-negative clauses 1492 than limit 61800 (10.0%)
c [phase-count-8] non-pos/non-neg = 114293/1492 = 76.60 >= 2.00 = 200/100
c [lucky-phase-8] forcing lucky phase -1
c [phase-8] phase bias: 0 positive 0%, 293 negative 100%
c [sort-queue-8] sorted 31307 enqueued variables after 43145 conflicts
c [score-dist-8] active 58111 (65%), one 0 (0%), zero 31307 (35%)
c [score-dist-8] max exp 510, different 174 (34%)
c [score-dist-8] median active exp 493, avg 462.2
c [simplification-8] removed 3269 variables 3.5% (89418 remain 36%)
c [simplification-8] removed 35056 irredundant clauses 5.4% (618161 remain 45%)
c [simplification-8] maximum reduction of 5% = max (4%, 5%)
c [simplification-8] large reduction 5% >= 5% limit
c [simplification-8] next conflict interval 2000 = 2000/1
c [simplification-8] penalized conflict interval 2000 = 1 * 2000
c [simplification-8] hard conflict limit 55145 (soft 45145 + delta 10000)
c [simplification-8] new conflict limit 45145 (hard 55145)
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  165.9   89417   618161     43716   29522   1244 403175  397   862  149  46%      5  470  318  180  177%
c i  165.9   89416   618161     43721   29526   1244 403175  397   862  149  46%      5  470  324  180  180%
c i  166.2   89415   618161     43808   29575   1244 403186  396   860  149  46%      4  467  330  180  183%
c i  169.4   89414   618161     44851   30246   1249 403207  408   834  149  49%      6  433  421  185  228%
c i  169.6   89412   618161     44927   30311   1249 403207  406   832  149  49%      6  432  398  185  215%
c i  169.6   89411   618161     44936   30317   1249 403207  405   832  149  49%      6  431  385  185  208%
c i  169.6   89410   618161     44938   30318   1249 403207  405   832  149  49%      5  431  382  185  207%
c i  169.6   89409   618161     44948   30326   1249 403208  404   831  149  49%      5  430  368  185  199%
c 
c [simplification-9] limit 45154 conflicts (hard 55145) hit after 45154 conflicts
c [quatres-4] found 42461 quaternary clauses 50% in total
c [quatres-4-2] added 1 single-self-subsuming ternary resolvents
c [quatres-4-2] added 1 quaternary resolvents
c [ternres-4] limit 32769263 with penalty 0 = 0 + 0
c [ternres-4] all 89409 free variables schedulable
c [ternres-4] 28 ternary resolvents (0 bin, 28 trn)
c [ternres-4] fully completed ternary resolution
c [decomp-19] removed 9 variables
c [simpleprobe-4] 5262 schedulable variables 6%
c [simpleprobe-4] limit 131077053 penalty 0 = 0 + 0
c [decomp-20] removed 856 variables
c [simpleprobe-4] fully completed simple probing
c [simpleprobe-4] removed 856 variables, found 106150 hbrs, 386 units
c [unhide-9] limit 819231 with penalty 3 = 0 + 3
c [unhide-9-9] 7 units, 83 failed, 11049 tauts, 0 hbrs, 694044 literals
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 205 transitive binary clauses
c [transred-5] found 4 units
c [cce-4] boosting limit by 10
c [cce-4] limit of 1638463160 steps penalty 0 = 0 + 0
c [cce-4-1] eliminated 23333 clauses out of 35388 (66%) of length 5
c [cce-4-1] eliminated 25219 clauses out of 41018 (61%) of length 4
c [cce-4-1] completed large round (ATE)
c [cce-4-1] eliminated 48552 large clauses in 972451437 steps
c [cce-4-1] allowing another 486225718 steps for small clauses
c [cce-4-1] scheduling 496984 clauses = 286012 binary + 210972 ternary
c [cce-4-1] tried to eliminate 23371 small clauses 5%
c [cce-4-1] eliminated 3686 binary clauses 1%
c [cce-4-1] eliminated 904 ternary clauses 0%
c [cce-4-1] eliminated 4590 small clauses 1%
c [cce-4-1] eliminated 7614 small clauses in 1638463165 steps
c [cce-4-1] incomplete small round (ATE)
c [cce-4-1] eliminated 56166 covered clauses in round 1
c [cce-4] eliminated 56166 covered clauses in TOTAL during 1 rounds
c [elim-7] scheduling all variables this time
c [elim-7] scheduled 88315 variables 100%
c [elim-7] limit of 327692633 steps penalty 1 = 1 + 0
c [elim-7] rescheduling of touched variables disabled
c [elim-7-1] eliminated 24750 variables 28% in round 1 in 50327438 steps
c [elim-7-1] backward subsumption/strengthening limit 50327400
c [elim-7-1-1] backward checking 49555 touched variables 56%
c [elim-7-1-1] fully completed backward checking in 1 rounds
c [elim-7-1] subsumed 6 and strengthened 52 clauses in 6565662 steps
c [elim-7-1] rescheduled 124 variables 0% by backward subsumption
c [elim-7-2] eliminated 5 variables 0% in round 2 in 75749 steps
c [elim-7-2] backward subsumption/strengthening limit 75700
c [elim-7-2-1] backward checking 57 touched variables 0%
c [elim-7-2-1] incomplete backward checking 0 remain 0%
c [elim-7-2] subsumed 0 and strengthened 2 clauses in 75701 steps
c [elim-7-2] rescheduled 5 variables 0% by backward subsumption
c [elim-7-3] no variable eliminated in round 3 in 3921 steps
c [elim-7] fully completed in 3 rounds
c [elim-7] transition to [ all 0 rem 0 ] state
c [elim-7] eliminated 24755 = 28% variables out of 88315 scheduled
c [bca-5] limit of 10000000 steps and 986694 added (scaled 2)
c [bca-5] 119945 out of 127122 literals actually usable 94%
c [bca-5] added 275 blocked clauses in 281038 steps
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 98307790 penalty 0 = 0 + 0
c [sweep-5-1] 3883 pos 6.4% + 56989 neg 93.6% = 60872 sched 95.8% ret 2688
c [sweep-5-1] 98328247 steps 1709 queries 464.26 avg class size
c [sweep-5-1] 14729 decisions 1562 SAT calls 78.26 avg env size
c [sweep-5-1] 31663 variables remain 51% (30573 retained 49%)
c [decomp-21] removed 1953 variables
c [sweep-5-1] removed 1953 vars (0 failed, 160 eqs, 317 impls)
c [sweep-5] considered successful since not run to completion yet
c [sweep-5] removed 1953 vars in TOTAL (1 rounds, 1708 queries)
c [phase-count-9] 482336 negative 99.8% of 483087 except 751 0.2%
c [phase-count-9] 378023 positive 78.3% of 483087 except 105064 21.7%
c [phase-count-9] less non-negative clauses 751 than limit 48300 (10.0%)
c [phase-count-9] non-pos/non-neg = 105064/751 = 139.90 >= 2.00 = 200/100
c [lucky-phase-9] forcing lucky phase -1
c [phase-9] phase bias: 0 positive 0%, 128 negative 100%
c [sort-queue-9] sorted 18057 enqueued variables after 45154 conflicts
c [score-dist-9] active 43550 (71%), one 0 (0%), zero 18057 (29%)
c [score-dist-9] max exp 509, different 180 (35%)
c [score-dist-9] median active exp 503, avg 489.9
c [simplification-9] removed 27802 variables 31.1% (61607 remain 25%)
c [simplification-9] removed 135074 irredundant clauses 21.9% (483087 remain 35%)
c [simplification-9] maximum reduction of 31% = max (31%, 22%)
c [simplification-9] large reduction 31% >= 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 57154 (soft 47154 + delta 10000)
c [simplification-9] new conflict limit 47154 (hard 57154)
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  227.7   61606   483087     45595    2990   1853 496587  360   784   51  46%      4  379   78  184   43%
c i  227.8   61605   483087     45819    3179   1855 496591  345   766   51  45%      3  360   76  184   41%
c i  227.9   61604   483087     46111    3420   1861 496597  328   731   51  45%      3  323   82  183   45%
c i  228.0   61603   483087     46179    3483   1864 496597  323   724   51  45%      2  316   74  183   40%
c i  228.1   61602   483087     46426    3685   1871 496597  307   702   52  44%      2  293   58  182   32%
c 
c [simplification-10] limit 47154 conflicts (hard 57154) hit after 47154 conflicts
c [quatres-5] found 25929 quaternary clauses 55% in total
c [quatres-5-1] removed 2 duplicate quaternary clauses
c [quatres-5-2] added 1 single-self-subsuming ternary resolvents
c [quatres-5-2] added 6 quaternary resolvents
c [ternres-5] limit 33262957 with penalty 0 = 0 + 0
c [ternres-5] all 61599 free variables schedulable
c [ternres-5] 1596 ternary resolvents (0 bin, 1596 trn)
c [ternres-5] fully completed ternary resolution
c [card-4] limit 2078934 penalty 3 = 3 + 0
c [card-4] found 2321 at-most-one constraints of average size 4.2
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 2078934 for elimination
c [card-4] 2321 out of 2321 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [gauss-3] limit 1663147 penalty 2 = 2 + 0
c [gauss-3] extracted 13 xors of average arity 2.8
c [gauss-3] connected 37 occurrences of 37 variables (average 1.0)
c [gauss-3] limit 1663147 penalty 2 = 2 + 0
c [gauss-3] fully completed
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-22] removed 4 variables
c [treelook-4] limit 3326295 penalty 0 = 0 + 0 boost 1
c [treelook-4] scheduled 88772 literals 72%
c [treelook-4] scheduling used 1680291 steps
c [treelook-4] scheduled completely
c [treelook-4] limit 3326295 penalty 0 = 0 + 0 boost 1
c [treelook-4] used 3386364 steps
c [treelook-4] 88691 literals remain 72%
c [treelook-4] 10758 variables remain to probed next time 17%
c [treelook-4] removed 13 variables, found 29169 hbrs
c [unhide-10] limit 6652591 with penalty 0 = 0 + 0
c [unhide-10-12] 15 units, 1279 failed, 103602 tauts, 0 hbrs, 15453 literals
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 165 transitive binary clauses
c [transred-6] found 2 units
c [cce-5] limit of 166314789 steps penalty 0 = 0 + 0
c [cce-5-1] eliminated 8 clauses out of 36 (22%) of length 7
c [cce-5-1] eliminated 309 clauses out of 3707 (8%) of length 6
c [cce-5-1] eliminated 1185 clauses out of 15693 (8%) of length 5
c [cce-5-1] incomplete large round (ACCE)
c [cce-5-1] eliminated 1502 large clauses in 166314795 steps
c [cce-5-1] allowing another 83157397 steps for small clauses
c [cce-5-1] scheduling 224431 clauses = 200340 binary + 24091 ternary
c [cce-5-1] tried to eliminate 3609 small clauses 2%
c [cce-5-1] eliminated 959 binary clauses 0%
c [cce-5-1] eliminated 144 ternary clauses 1%
c [cce-5-1] eliminated 1103 small clauses 0%
c [cce-5-1] eliminated 3772 small clauses in 166314798 steps
c [cce-5-1] incomplete small round (ACCE)
c [cce-5-1] eliminated 5274 covered clauses in round 1
c [cce-5] eliminated 5274 covered clauses in TOTAL during 1 rounds
c [elim-8] scheduling all variables this time
c [elim-8] scheduled 60615 variables 100%
c [elim-8] boosting limit by 20
c [elim-8] limit of 13305183120 steps penalty 0 = 0 + 0
c [elim-8] rescheduling of touched variables disabled
c [elim-8-1] eliminated 791 variables 1% in round 1 in 43964520 steps
c [elim-8-1] backward subsumption/strengthening limit 43964500
c [elim-8-1-1] backward checking 4782 touched variables 8%
c [elim-8-1-1] fully completed backward checking in 1 rounds
c [elim-8-1] subsumed 2 and strengthened 56 clauses in 1514597 steps
c [elim-8-1] rescheduled 158 variables 0% by backward subsumption
c [elim-8-2] eliminated 3 variables 0% in round 2 in 70850 steps
c [elim-8-2] backward subsumption/strengthening limit 70800
c [elim-8-2-1] backward checking 69 touched variables 0%
c [elim-8-2-1] fully completed backward checking in 1 rounds
c [elim-8-2] subsumed 0 and strengthened 0 clauses in 65719 steps
c [elim-8] fully completed in 2 rounds
c [elim-8] transition to [ all 0 rem 0 ] state
c [elim-8] eliminated 795 = 1% variables out of 60615 scheduled
c [bca-6] limit of 10000000 steps and 920733 added (scaled 2)
c [bca-6] 107707 out of 119642 literals actually usable 90%
c [bca-6] added 232 blocked clauses in 249292 steps
c [sweep-6] limit 9978887 penalty 0 = 0 + 0
c [sweep-6-1] 2641 pos 8.6% + 27967 neg 91.4% = 30608 sched 51.2% ret 29212
c [sweep-6-1] 9980610 steps 219 queries 2212.71 avg class size
c [sweep-6-1] 2307 decisions 201 SAT calls 90.54 avg env size
c [sweep-6-1] 29679 variables remain 50% (30129 retained 50%)
c [decomp-24] removed 72 variables
c [sweep-6-1] removed 72 vars (0 failed, 17 eqs, 30 impls)
c [sweep-6] considered successful since not run to completion yet
c [sweep-6] removed 72 vars in TOTAL (1 rounds, 218 queries)
c [phase-count-10] 459002 negative 99.9% of 459670 except 668 0.1%
c [phase-count-10] 358679 positive 78.0% of 459670 except 100991 22.0%
c [phase-count-10] less non-negative clauses 668 than limit 45900 (10.0%)
c [phase-count-10] non-pos/non-neg = 100991/668 = 151.18 >= 2.00 = 200/100
c [lucky-phase-10] forcing lucky phase -1
c [phase-10] phase bias: 0 positive 0%, 117 negative 100%
c [sort-queue-10] sorted 16784 enqueued variables after 47154 conflicts
c [score-dist-10] active 42964 (72%), one 0 (0%), zero 16784 (28%)
c [score-dist-10] max exp 509, different 188 (37%)
c [score-dist-10] median active exp 495, avg 486.5
c [simplification-10] removed 1851 variables 3.0% (59748 remain 24%)
c [simplification-10] removed 23417 irredundant clauses 4.8% (459670 remain 33%)
c [simplification-10] maximum reduction of 5% = max (3%, 5%)
c [simplification-10] large reduction 5% >= 5% limit
c [simplification-10] next conflict interval 2000 = 2000/1
c [simplification-10] penalized conflict interval 2000 = 1 * 2000
c [simplification-10] hard conflict limit 59154 (soft 49154 + delta 10000)
c [simplification-10] new conflict limit 49154 (hard 59154)
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  239.0   59747   459670     47579    4363   3268 428021  262   598   54  44%      6  184  110  181   61%
c i  239.0   59743   459670     47612    4389   3272 428023  260   595   54  44%      6  182   98  181   54%
c 
c [simplification-11] limit 49154 conflicts (hard 59154) hit after 49154 conflicts
c [quatres-6] found 26228 quaternary clauses 57% in total
c [quatres-6-2] added 32 quaternary resolvents
c [ternres-6] limit 33699215 with penalty 0 = 0 + 0
c [ternres-6] all 59743 free variables schedulable
c [ternres-6] 574 ternary resolvents (0 bin, 574 trn)
c [ternres-6] fully completed ternary resolution
c [decomp-25] removed 19 variables
c [basicprobe-4] limit 168496077 penalty 0 = 0 + 0
c [basicprobe-4-0] 9896 probes remain 17% after last round
c [basicprobe-4-0] 839 units = 789 failed (94%) + 50 lifted (6%)
c [basicprobe-4-0] removed 1512 variables, found 538601 hbrs
c [bate-2] eliminated 1582 asymmetric tautologies during probing
c [unhide-11] limit 6739843 with penalty 0 = 0 + 0
c [unhide-11-15] 17 units, 239 failed, 81370 tauts, 0 hbrs, 17828 literals
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 125 transitive binary clauses
c [block-4] scheduling all variables this time
c [block-4] scheduled 57975 variables 100%
c [block-4] limit of 84248038 steps penalty 2 = 2 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 504 blocked clauses
c [block-4] 504 < 1/100 * 434686 = 4346 considered unsuccessful
c [cce-6] limit of 168496077 steps penalty 0 = 0 + 0
c [cce-6-1] eliminated 1 clauses out of 1 (100%) of length 10
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 9
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 8
c [cce-6-1] eliminated 2 clauses out of 27 (7%) of length 7
c [cce-6-1] eliminated 3 clauses out of 3245 (0%) of length 6
c [cce-6-1] eliminated 1003 clauses out of 13417 (7%) of length 5
c [cce-6-1] incomplete large round (ATE)
c [cce-6-1] eliminated 1012 large clauses in 168496084 steps
c [cce-6-1] allowing another 84248042 steps for small clauses
c [cce-6-1] scheduling 211655 clauses = 190035 binary + 21620 ternary
c [cce-6-1] tried to eliminate 4203 small clauses 2%
c [cce-6-1] eliminated 1006 binary clauses 1%
c [cce-6-1] eliminated 177 ternary clauses 1%
c [cce-6-1] eliminated 1183 small clauses 1%
c [cce-6-1] eliminated 1183 small clauses in 168496078 steps
c [cce-6-1] incomplete small round (ATE)
c [cce-6-1] eliminated 2195 covered clauses in round 1
c [cce-6] eliminated 2195 covered clauses in TOTAL during 1 rounds
c [cce-6] 2195 < 1/100 * 433994 = 4339 considered unsuccessful
c [elim-9] scheduling all variables this time
c [elim-9] scheduled 57975 variables 100%
c [elim-9] limit of 673984308 steps penalty 0 = 0 + 0
c [elim-9] rescheduling of touched variables disabled
c [elim-9-1] eliminated 1028 variables 2% in round 1 in 41012957 steps
c [elim-9-1] backward subsumption/strengthening limit 41012900
c [elim-9-1-1] backward checking 6047 touched variables 10%
c [elim-9-1-1] fully completed backward checking in 1 rounds
c [elim-9-1] subsumed 2 and strengthened 37 clauses in 1585714 steps
c [elim-9-1] rescheduled 73 variables 0% by backward subsumption
c [elim-9-2] eliminated 7 variables 0% in round 2 in 68457 steps
c [elim-9-2] backward subsumption/strengthening limit 68400
c [elim-9-2-1] backward checking 59 touched variables 0%
c [elim-9-2-1] fully completed backward checking in 1 rounds
c [elim-9-2] subsumed 1 and strengthened 0 clauses in 68109 steps
c [elim-9-2] rescheduled 3 variables 0% by backward subsumption
c [elim-9-3] no variable eliminated in round 3 in 1143 steps
c [elim-9] fully completed in 3 rounds
c [elim-9] transition to [ all 0 rem 0 ] state
c [elim-9] eliminated 1035 = 2% variables out of 57975 scheduled
c [bca-7] limit of 10000000 steps and 861255 added (scaled 2)
c [bca-7] 100207 out of 113882 literals actually usable 88%
c [bca-7] added 105 blocked clauses in 230391 steps
c [sweep-7] limit 10109764 penalty 0 = 0 + 0
c [sweep-7-1] 3237 pos 11.5% + 24904 neg 88.5% = 28141 sched 49.4% ret 28799
c [sweep-7-1] 10203072 steps 260 queries 1727.02 avg class size
c [sweep-7-1] 2405 decisions 243 SAT calls 95.31 avg env size
c [sweep-7-1] 26798 variables remain 47% (30133 retained 53%)
c [decomp-26] removed 74 variables
c [sweep-7-1] removed 74 vars (0 failed, 19 eqs, 33 impls)
c [sweep-7] removed 74 vars in TOTAL (1 rounds, 259 queries)
c [phase-count-11] 429220 negative 99.8% of 429916 except 696 0.2%
c [phase-count-11] 335185 positive 78.0% of 429916 except 94731 22.0%
c [phase-count-11] skipping relative phase luck test
c [phase-11] phase bias: 9 positive 100%, 0 negative 0%
c [sort-queue-11] sorted 15310 enqueued variables after 49154 conflicts
c [score-dist-11] active 41556 (73%), one 0 (0%), zero 15310 (27%)
c [score-dist-11] max exp 508, different 193 (38%)
c [score-dist-11] median active exp 494, avg 485.9
c [simplification-11] removed 2877 variables 4.8% (56866 remain 23%)
c [simplification-11] removed 29754 irredundant clauses 6.5% (429916 remain 31%)
c [simplification-11] maximum reduction of 6% = max (5%, 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 61154 (soft 51154 + delta 10000)
c [simplification-11] new conflict limit 51154 (hard 61154)
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.8   56865   429916     49270    4931   4389 812813  192   556   61  35%     12  140   67  178   38%
c i  257.9   56853   429916     49432    5068   4392 812814  188   572   62  33%     10  156   70  178   39%
c i  258.4   56851   429916     49971    5533   4396 812816  186   585   62  32%      7  167  167  178   94%
c i  258.5   56767   429916     50148    5677   4398 812817  185   587   63  32%      5  168  176  178   99%
c i  258.9   56763   429916     50690    6132   4402 812829  188   613   63  31%      4  193  272  178  153%
c 
c [simplification-12] limit 51154 conflicts (hard 61154) hit after 51154 conflicts
c [quatres-7] found 23958 quaternary clauses 58% in total
c [quatres-7-1] removed 1 duplicate quaternary clauses
c [quatres-7-2] added 24 quaternary resolvents
c [ternres-7] limit 34250840 with penalty 0 = 0 + 0
c [ternres-7] all 56688 free variables schedulable
c [ternres-7] 639 ternary resolvents (1 bin, 638 trn)
c [ternres-7] fully completed ternary resolution
c [decomp-27] removed 181 variables
c [simpleprobe-5] all 56685 free variables schedulable
c [simpleprobe-5] limit 137003361 penalty 0 = 0 + 0
c [decomp-28] removed 324 variables
c [simpleprobe-5] 705 variables remain 1% (55656 retained 99%)
c [simpleprobe-5] removed 324 variables, found 135049 hbrs, 166 units
c [unhide-12] limit 6850168 with penalty 0 = 0 + 0
c [unhide-12-18] 7 units, 113 failed, 94292 tauts, 0 hbrs, 32473 literals
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 197 transitive binary clauses
c [elim-10] scheduling all variables this time
c [elim-10] scheduled 56275 variables 100%
c [elim-10] limit of 685016807 steps penalty 0 = 0 + 0
c [elim-10] rescheduling of touched variables disabled
c [elim-10-1] eliminated 296 variables 1% in round 1 in 40745385 steps
c [elim-10-1] backward subsumption/strengthening limit 40745300
c [elim-10-1-1] backward checking 1737 touched variables 3%
c [elim-10-1-1] fully completed backward checking in 1 rounds
c [elim-10-1] subsumed 3 and strengthened 9 clauses in 501097 steps
c [elim-10-1] rescheduled 27 variables 0% by backward subsumption
c [elim-10-2] eliminated 2 variables 0% in round 2 in 51085 steps
c [elim-10-2] backward subsumption/strengthening limit 51000
c [elim-10-2-1] backward checking 89 touched variables 0%
c [elim-10-2-1] incomplete backward checking 0 remain 0%
c [elim-10-2] subsumed 3 and strengthened 2 clauses in 51001 steps
c [elim-10-2] rescheduled 11 variables 0% by backward subsumption
c [elim-10-3] no variable eliminated in round 3 in 17994 steps
c [elim-10] fully completed in 3 rounds
c [elim-10] transition to [ all 0 rem 0 ] state
c [elim-10] eliminated 298 = 1% variables out of 56275 scheduled
c [elim-10] 298 < 1/100 * 56275 = 562 considered unsuccessful
c [bca-8] limit of 10000000 steps and 845248 added (scaled 2)
c [bca-8] 96757 out of 111956 literals actually usable 86%
c [bca-8] added 102 blocked clauses in 223572 steps
c [sweep-8] limit 10275252 penalty 0 = 0 + 0
c [sweep-8-1] 2653 pos 10.1% + 23685 neg 89.9% = 26338 sched 47.1% ret 29639
c [sweep-8-1] 10296373 steps 299 queries 1477.01 avg class size
c [sweep-8-1] 3327 decisions 284 SAT calls 112.19 avg env size
c [sweep-8-1] 24943 variables remain 45% (31010 retained 55%)
c [decomp-29] removed 49 variables
c [sweep-8-1] removed 49 vars (0 failed, 17 eqs, 39 impls)
c [sweep-8] 49 < 1/1000 * 55977 = 55 considered unsuccessful
c [sweep-8] removed 49 vars in TOTAL (1 rounds, 298 queries)
c [phase-count-12] 421137 negative 99.8% of 421817 except 680 0.2%
c [phase-count-12] 328402 positive 77.9% of 421817 except 93415 22.1%
c [phase-count-12] skipping relative phase luck test
c [phase-12] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-12] sorted 14606 enqueued variables after 51154 conflicts
c [score-dist-12] active 41322 (74%), one 0 (0%), zero 14606 (26%)
c [score-dist-12] max exp 509, different 200 (39%)
c [score-dist-12] median active exp 497, avg 487.6
c [simplification-12] removed 760 variables 1.3% (55928 remain 23%)
c [simplification-12] removed 8099 irredundant clauses 1.9% (421817 remain 31%)
c [simplification-12] maximum reduction of 2% = max (1%, 2%)
c [simplification-12] geometric conflict interval increment 6666 = 20000 / 3
c [simplification-12] new conflict interval 23666
c [simplification-12] penalized conflict interval 23666 = 1 * 23666
c [simplification-12] hard conflict limit 86653 (soft 74820 + delta 11833)
c [simplification-12] new conflict limit 74820 (hard 86653)
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  267.4   55927   421817     51496    6762   4708 838852  185   646   65  29%      4  224  181  178  102%
c i  268.8   55907   421817     52814    7762   4747 838868  193   611   67  32%      8  184  209  179  117%
c i  269.3   55825   421817     53156    7995   4750 838870  203   606   67  33%      6  178  284  179  159%
c i  274.2   55824   421817     58459   12257   4798 838932  193   560   72  34%     62  121  206  181  114%
c i  278.6   55821   421817     63210   15910   4828 838953  218   548   84  40%     52  101  144  186   77%
c i  278.6   55820   421817     63211   15910   4828 838953  218   548   84  40%     52  101  143  186   77%
c 
c [simplification-13] limit 74830 conflicts (hard 86653) hit after 74835 conflicts
c [quatres-8] found 23845 quaternary clauses 56% in total
c [quatres-8-2] added 1 single-self-subsuming ternary resolvents
c [quatres-8-2] added 11 quaternary resolvents
c [ternres-8] limit 41870028 with penalty 0 = 0 + 0
c [ternres-8] all 55819 free variables schedulable
c [ternres-8] 239 ternary resolvents (0 bin, 239 trn)
c [ternres-8] fully completed ternary resolution
c [decomp-30] removed 114 variables
c [treelook-5] limit 4187002 penalty 0 = 0 + 0 boost 1
c [treelook-5] scheduled 77431 literals 69%
c [treelook-5] scheduling used 1619517 steps
c [treelook-5] scheduled completely
c [treelook-5] limit 4187002 penalty 0 = 0 + 0 boost 1
c [treelook-5] used 4259540 steps
c [treelook-5] 77347 literals remain 69%
c [treelook-5] 9042 variables remain to probed next time 16%
c [treelook-5] removed 12 variables, found 21646 hbrs
c [unhide-13] limit 2093501 with penalty 2 = 0 + 2
c [unhide-13-19] 1 units, 3 failed, 2799 tauts, 0 hbrs, 184203 literals
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 143 transitive binary clauses
c [transred-9] found 1 units
c [cce-7] limit of 104675071 steps penalty 1 = 1 + 0
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 77
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 76
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 75
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 74
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 73
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 72
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 71
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 70
c [cce-7-1] eliminated 1 clauses out of 1 (100%) of length 69
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 68
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 67
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 66
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 65
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 64
c [cce-7-1] eliminated 2 clauses out of 3 (67%) of length 63
c [cce-7-1] eliminated 2 clauses out of 3 (67%) of length 62
c [cce-7-1] eliminated 4 clauses out of 4 (100%) of length 61
c [cce-7-1] eliminated 3 clauses out of 5 (60%) of length 60
c [cce-7-1] eliminated 2 clauses out of 4 (50%) of length 59
c [cce-7-1] eliminated 3 clauses out of 3 (100%) of length 58
c [cce-7-1] eliminated 2 clauses out of 4 (50%) of length 57
c [cce-7-1] eliminated 2 clauses out of 4 (50%) of length 56
c [cce-7-1] eliminated 2 clauses out of 4 (50%) of length 55
c [cce-7-1] eliminated 3 clauses out of 4 (75%) of length 54
c [cce-7-1] eliminated 3 clauses out of 4 (75%) of length 53
c [cce-7-1] eliminated 3 clauses out of 4 (75%) of length 52
c [cce-7-1] eliminated 3 clauses out of 4 (75%) of length 51
c [cce-7-1] eliminated 3 clauses out of 4 (75%) of length 50
c [cce-7-1] eliminated 3 clauses out of 5 (60%) of length 49
c [cce-7-1] eliminated 4 clauses out of 4 (100%) of length 48
c [cce-7-1] eliminated 2 clauses out of 4 (50%) of length 47
c [cce-7-1] eliminated 3 clauses out of 4 (75%) of length 46
c [cce-7-1] eliminated 3 clauses out of 4 (75%) of length 45
c [cce-7-1] eliminated 3 clauses out of 4 (75%) of length 44
c [cce-7-1] eliminated 3 clauses out of 4 (75%) of length 43
c [cce-7-1] eliminated 3 clauses out of 4 (75%) of length 42
c [cce-7-1] eliminated 3 clauses out of 4 (75%) of length 41
c [cce-7-1] eliminated 3 clauses out of 4 (75%) of length 40
c [cce-7-1] eliminated 3 clauses out of 4 (75%) of length 39
c [cce-7-1] eliminated 3 clauses out of 4 (75%) of length 38
c [cce-7-1] eliminated 3 clauses out of 4 (75%) of length 37
c [cce-7-1] eliminated 3 clauses out of 5 (60%) of length 36
c [cce-7-1] eliminated 5 clauses out of 6 (83%) of length 35
c [cce-7-1] eliminated 4 clauses out of 6 (67%) of length 34
c [cce-7-1] eliminated 5 clauses out of 7 (71%) of length 33
c [cce-7-1] eliminated 6 clauses out of 8 (75%) of length 32
c [cce-7-1] eliminated 5 clauses out of 9 (56%) of length 31
c [cce-7-1] eliminated 9 clauses out of 10 (90%) of length 30
c [cce-7-1] eliminated 6 clauses out of 10 (60%) of length 29
c [cce-7-1] eliminated 9 clauses out of 10 (90%) of length 28
c [cce-7-1] eliminated 6 clauses out of 10 (60%) of length 27
c [cce-7-1] eliminated 8 clauses out of 9 (89%) of length 26
c [cce-7-1] eliminated 6 clauses out of 10 (60%) of length 25
c [cce-7-1] eliminated 9 clauses out of 10 (90%) of length 24
c [cce-7-1] eliminated 6 clauses out of 10 (60%) of length 23
c [cce-7-1] eliminated 7 clauses out of 10 (70%) of length 22
c [cce-7-1] eliminated 7 clauses out of 11 (64%) of length 21
c [cce-7-1] eliminated 8 clauses out of 10 (80%) of length 20
c [cce-7-1] eliminated 6 clauses out of 11 (55%) of length 19
c [cce-7-1] eliminated 10 clauses out of 12 (83%) of length 18
c [cce-7-1] eliminated 7 clauses out of 12 (58%) of length 17
c [cce-7-1] eliminated 10 clauses out of 12 (83%) of length 16
c [cce-7-1] eliminated 8 clauses out of 12 (67%) of length 15
c [cce-7-1] eliminated 11 clauses out of 12 (92%) of length 14
c [cce-7-1] eliminated 6 clauses out of 12 (50%) of length 13
c [cce-7-1] eliminated 11 clauses out of 12 (92%) of length 12
c [cce-7-1] eliminated 6 clauses out of 14 (43%) of length 11
c [cce-7-1] eliminated 19 clauses out of 19 (100%) of length 10
c [cce-7-1] eliminated 8 clauses out of 17 (47%) of length 9
c [cce-7-1] eliminated 14 clauses out of 16 (88%) of length 8
c [cce-7-1] eliminated 13 clauses out of 46 (28%) of length 7
c [cce-7-1] eliminated 21 clauses out of 3225 (1%) of length 6
c [cce-7-1] eliminated 8 clauses out of 12446 (0%) of length 5
c [cce-7-1] incomplete large round (ACCE)
c [cce-7-1] eliminated 363 large clauses in 104675075 steps
c [cce-7-1] allowing another 52337537 steps for small clauses
c [cce-7-1] scheduling 205290 clauses = 184612 binary + 20678 ternary
c [cce-7-1] tried to eliminate 2176 small clauses 1%
c [cce-7-1] eliminated 518 binary clauses 0%
c [cce-7-1] eliminated 74 ternary clauses 0%
c [cce-7-1] eliminated 592 small clauses 0%
c [cce-7-1] eliminated 651 small clauses in 104675081 steps
c [cce-7-1] incomplete small round (ACCE)
c [cce-7-1] eliminated 1014 covered clauses in round 1
c [cce-7] eliminated 1014 covered clauses in TOTAL during 1 rounds
c [cce-7] 1014 < 1/100 * 419589 = 4195 considered unsuccessful
c [bca-9] limit of 10000000 steps and 838233 added (scaled 2)
c [bca-9] 89982 out of 111592 literals actually usable 81%
c [bca-9] added 10 blocked clauses in 225576 steps
c [phase-count-13] 417896 negative 99.8% of 418575 except 679 0.2%
c [phase-count-13] 326464 positive 78.0% of 418575 except 92111 22.0%
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 13779 enqueued variables after 74835 conflicts
c [score-dist-13] active 42016 (75%), one 0 (0%), zero 13779 (25%)
c [score-dist-13] max exp 509, different 286 (56%)
c [score-dist-13] median active exp 472, avg 457.8
c [simplification-13] removed 24 variables 0.0% (55795 remain 23%)
c [simplification-13] removed 3242 irredundant clauses 0.8% (418575 remain 30%)
c [simplification-13] maximum reduction of 1% = max (0%, 1%)
c [simplification-13] geometric conflict interval increment 11833 = 23666 / 2
c [simplification-13] new conflict interval 35499
c [simplification-13] penalized conflict interval 35499 = 1 * 35499
c [simplification-13] hard conflict limit 128083 (soft 110334 + delta 17749)
c [simplification-13] new conflict limit 110334 (hard 128083)
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  301.6   55794   418575     78056   27000   5215 858606  258   682  108  38%    188  207  187  204   92%
c i  304.5   55729   418575     82065   30230   5250 858623  187   561  108  33%     21   78   52  201   26%
c i  306.7   55728   418575     84229   31773   5256 858627  144   424  108  34%     -5  -59   72  197   37%
c 
c [simplification-14] limit 110334 conflicts (hard 128083) hit after 112423 conflicts
c [quatres-9] found 23879 quaternary clauses 56% in total
c [ternres-9] limit 53325943 with penalty 0 = 0 + 0
c [ternres-9] all 55651 free variables schedulable
c [ternres-9] 30 ternary resolvents (0 bin, 30 trn)
c [ternres-9] fully completed ternary resolution
c [gauss-4] limit 1333148 penalty 3 = 3 + 0
c [gauss-4] extracted 7 xors of average arity 3.0
c [gauss-4] connected 21 occurrences of 21 variables (average 1.0)
c [gauss-4] limit 1333148 penalty 3 = 3 + 0
c [gauss-4] fully completed
c [gauss-4] exported 0 unary, 0 binary and 0 ternary equations
c [basicprobe-5] limit 266629718 penalty 0 = 0 + 0
c [basicprobe-5-0] 564 probes remain 1% after last round
c [basicprobe-5-0] 1170 units = 1089 failed (93%) + 81 lifted (7%)
c [basicprobe-5-0] removed 1577 variables, found 611823 hbrs
c [bate-3] eliminated 1076 asymmetric tautologies during probing
c [unhide-14] limit 2666297 with penalty 2 = 0 + 2
c [unhide-14-20] 0 units, 75 failed, 116521 tauts, 0 hbrs, 274240 literals
c [transred-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 200 transitive binary clauses
c [transred-10] found 1 units
c [elim-11] scheduling all variables this time
c [elim-11] scheduled 53971 variables 100%
c [elim-11] limit of 400000000 steps penalty 1 = 1 + 0
c [elim-11] rescheduling of touched variables disabled
c [elim-11-1] eliminated 685 variables 1% in round 1 in 37409576 steps
c [elim-11-1] backward subsumption/strengthening limit 37409500
c [elim-11-1-1] backward checking 4122 touched variables 8%
c [elim-11-1-1] fully completed backward checking in 1 rounds
c [elim-11-1] subsumed 1 and strengthened 34 clauses in 1086685 steps
c [elim-11-1] rescheduled 87 variables 0% by backward subsumption
c [elim-11-2] eliminated 7 variables 0% in round 2 in 62419 steps
c [elim-11-2] backward subsumption/strengthening limit 62400
c [elim-11-2-1] backward checking 58 touched variables 0%
c [elim-11-2-1] incomplete backward checking 0 remain 0%
c [elim-11-2] subsumed 4 and strengthened 4 clauses in 62401 steps
c [elim-11-2] rescheduled 11 variables 0% by backward subsumption
c [elim-11-3] eliminated 2 variables 0% in round 3 in 10008 steps
c [elim-11-3] backward subsumption/strengthening limit 10000
c [elim-11-3-1] backward checking 13 touched variables 0%
c [elim-11-3-1] incomplete backward checking 0 remain 0%
c [elim-11-3] subsumed 2 and strengthened 0 clauses in 10001 steps
c [elim-11] incomplete 4 not tried 0% in round 3
c [elim-11] transition to [ all 1 rem 1 ] state
c [elim-11] eliminated 694 = 1% variables out of 53971 scheduled
c [bca-10] limit of 10000000 steps and 799126 added (scaled 2)
c [bca-10] 82966 out of 106556 literals actually usable 78%
c [bca-10] added 74 blocked clauses in 226941 steps
c [sweep-9] limit 7998891 penalty 1 = 1 + 0
c [sweep-9-1] 2531 pos 10.7% + 21229 neg 89.3% = 23760 sched 44.6% ret 29517
c [sweep-9-1] 8020365 steps 134 queries 1534.41 avg class size
c [sweep-9-1] 2759 decisions 130 SAT calls 219.21 avg env size
c [sweep-9-1] 23061 variables remain 43% (30144 retained 57%)
c [decomp-33] removed 194 variables
c [sweep-9-1] removed 194 vars (0 failed, 5 eqs, 7 impls)
c [sweep-9] removed 194 vars in TOTAL (1 rounds, 133 queries)
c [phase-count-14] 397833 negative 99.8% of 398529 except 696 0.2%
c [phase-count-14] 309713 positive 77.7% of 398529 except 88816 22.3%
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 12382 enqueued variables after 112423 conflicts
c [score-dist-14] active 40701 (77%), one 0 (0%), zero 12382 (23%)
c [score-dist-14] max exp 509, different 420 (82%)
c [score-dist-14] median active exp 490, avg 422.0
c [simplification-14] removed 2568 variables 4.6% (53083 remain 22%)
c [simplification-14] removed 20046 irredundant clauses 4.8% (398529 remain 29%)
c [simplification-14] maximum reduction of 5% = max (5%, 5%)
c [simplification-14] large reduction 5% >= 5% limit
c [simplification-14] next conflict interval 2000 = 2000/1
c [simplification-14] penalized conflict interval 2000 = 1 * 2000
c [simplification-14] hard conflict limit 124423 (soft 114423 + delta 10000)
c [simplification-14] new conflict limit 114423 (hard 124423)
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  353.8   53082   398529    113747   43501   5532 1250080  184   447  149  41%    341   40  247  183  135%
c 
c [simplification-15] limit 114423 conflicts (hard 124423) hit after 114423 conflicts
c [ternres-10] limit 53990591 with penalty 0 = 0 + 0
c [ternres-10] all 53062 free variables schedulable
c [ternres-10] 4874 ternary resolvents (0 bin, 4874 trn)
c [ternres-10] fully completed ternary resolution
c [card-5] limit 1687205 penalty 4 = 4 + 0
c [card-5] found 925 at-most-one constraints of average size 4.1
c [card-5] no at-most-two constraint found
c [card-5] using previous limit 1687205 for elimination
c [card-5] 925 out of 925 constraints (100%) meet size limits
c [card-5] no units found
c [card-5] no at-most-one constraints generated
c [decomp-34] removed 21 variables
c [simpleprobe-6] 661 schedulable variables 1%
c [simpleprobe-6] limit 200000000 penalty 0 = 0 + 0
c [decomp-35] removed 184 variables
c [simpleprobe-6] 2274 variables remain 4% (50604 retained 96%)
c [simpleprobe-6] removed 184 variables, found 124734 hbrs, 83 units
c [unhide-15] limit 2699529 with penalty 2 = 0 + 2
c [unhide-15-22] 2 units, 63 failed, 92845 tauts, 0 hbrs, 415944 literals
c [transred-11] limit 2000000 with penalty 0 = 0 + 0
c [transred-11] removed 217 transitive binary clauses
c [block-5] scheduling all variables this time
c [block-5] scheduled 52823 variables 100%
c [block-5] limit of 67488239 steps penalty 3 = 3 + 0
c [block-5] fully completed
c [block-5] transition to [ all 0 rem 0 ] state
c [block-5] eliminated 55 blocked clauses
c [block-5] 55 < 1/100 * 392081 = 3920 considered unsuccessful
c [elim-12] no untried remaining variables left
c [elim-12] scheduled 52821 variables 100%
c [elim-12] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-12] rescheduling of touched variables disabled
c [elim-12-1] eliminated 270 variables 1% in round 1 in 37252605 steps
c [elim-12-1] backward subsumption/strengthening limit 37252600
c [elim-12-1-1] backward checking 1698 touched variables 3%
c [elim-12-1-1] fully completed backward checking in 1 rounds
c [elim-12-1] subsumed 164 and strengthened 8 clauses in 525648 steps
c [elim-12-1] rescheduled 233 variables 0% by backward subsumption
c [elim-12-2] eliminated 4 variables 0% in round 2 in 358465 steps
c [elim-12-2] backward subsumption/strengthening limit 358400
c [elim-12-2-1] backward checking 78 touched variables 0%
c [elim-12-2-1] fully completed backward checking in 1 rounds
c [elim-12-2] subsumed 6 and strengthened 0 clauses in 87307 steps
c [elim-12-2] rescheduled 7 variables 0% by backward subsumption
c [elim-12-3] no variable eliminated in round 3 in 13847 steps
c [elim-12] fully completed in 3 rounds
c [elim-12] transition to [ all 0 rem 0 ] state
c [elim-12] eliminated 274 = 1% variables out of 52821 scheduled
c [elim-12] 274 < 1/100 * 52821 = 528 considered unsuccessful
c [bca-11] limit of 10000000 steps and 783279 added (scaled 2)
c [bca-11] 81568 out of 105096 literals actually usable 78%
c [bca-11] added 49 blocked clauses in 223329 steps
c [sweep-10] limit 16197177 penalty 0 = 0 + 0
c [sweep-10-1] 2327 pos 10.2% + 20391 neg 89.8% = 22718 sched 43.2% ret 29829
c [sweep-10-1] 16236747 steps 422 queries 689.87 avg class size
c [sweep-10-1] 5865 decisions 394 SAT calls 153.03 avg env size
c [sweep-10-1] 20618 variables remain 39% (31925 retained 61%)
c [decomp-36] removed 48 variables
c [sweep-10-1] removed 48 vars (0 failed, 27 eqs, 69 impls)
c [sweep-10] 48 < 1/1000 * 52547 = 52 considered unsuccessful
c [sweep-10] removed 48 vars in TOTAL (1 rounds, 421 queries)
c [phase-count-15] 390271 negative 99.8% of 390966 except 695 0.2%
c [phase-count-15] 303615 positive 77.7% of 390966 except 87351 22.3%
c [phase-count-15] skipping relative phase luck test
c [phase-15] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-15] sorted 12126 enqueued variables after 114423 conflicts
c [score-dist-15] active 40373 (77%), one 0 (0%), zero 12126 (23%)
c [score-dist-15] max exp 510, different 420 (82%)
c [score-dist-15] median active exp 497, avg 435.6
c [simplification-15] removed 563 variables 1.1% (52499 remain 21%)
c [simplification-15] removed 7563 irredundant clauses 1.9% (390966 remain 28%)
c [simplification-15] maximum reduction of 2% = max (1%, 2%)
c [simplification-15] geometric conflict interval increment 11833 = 35499 / 3
c [simplification-15] new conflict interval 47332
c [simplification-15] penalized conflict interval 47332 = 1 * 47332
c [simplification-15] hard conflict limit 185421 (soft 161755 + delta 23666)
c [simplification-15] new conflict limit 161755 (hard 185421)
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  370.5   52498   390966    115476   43174   8641 1241697  242   523  144  46%    -11  114  410  188  219%
c i  372.0   52495   390966    116519   44069   8646 1241699  244   537  144  45%    -66  126  282  189  149%
c i  373.2   52493   390966    117258   44630   8648 1241700  250   548  144  46%    -82  136  340  190  179%
c i  375.4   52465   390966    118501   45482   8649 1241708  275   564  144  49%    -89  149  396  192  206%
c -  395.1   52426   390966    134735   23781   8718 1241817  206   319   77  65%    131  -93  187  197   95%
c i  397.9   52425   390966    137789   25632   8726 1241825  197   335   89  59%    171  -73  293  196  149%
c i  401.2   52309   390966    140384   27494   8743 1241838  254   447   93  57%    -65   40  249  201  124%
c i  401.2   52308   390966    140421   27502   8747 1241854  252   444   93  57%    -67   37  217  201  108%
c i  401.2   52062   390966    140422   27502   8747 1241854  252   444   93  57%    -67   37  216  201  108%
c i  403.5   52061   390966    142781   29407   8755 1241859  253   525   95  48%    -84  115  380  203  187%
c i  403.5   52060   390966    142783   29407   8755 1241859  253   524   95  48%    -84  115  378  203  187%
c i  406.4   52059   390966    144804   31027   8762 1241860  296   597  106  50%    -86  182  351  207  169%
c i  407.0   52057   390966    145177   31255   8762 1241860  310   604  106  51%    -92  188  436  209  209%
c i  421.4   52052   390966    156275   39520   8814 1241920  338   670  141  50%     55  208  225  236   95%
c i  429.4   52051   390966    163095   44225   8825 1241937  334   666  147  50%     -8  191  304  242  125%
c 
c [simplification-16] limit 161770 conflicts (hard 185421) hit after 170140 conflicts
c [quatres-10] found 21503 quaternary clauses 54% in total
c [quatres-10-2] added 3 single-self-subsuming ternary resolvents
c [ternres-11] limit 74867409 with penalty 0 = 0 + 0
c [ternres-11] all 52051 free variables schedulable
c [ternres-11] 121 ternary resolvents (0 bin, 121 trn)
c [ternres-11] fully completed ternary resolution
c [decomp-37] removed 464 variables
c [treelook-6] limit 7486740 penalty 0 = 0 + 0 boost 1
c [treelook-6] scheduled 70509 literals 68%
c [treelook-6] scheduling used 1754390 steps
c [treelook-6] scheduled completely
c [treelook-6] limit 7486740 penalty 0 = 0 + 0 boost 1
c [treelook-6] used 7487059 steps
c [treelook-6] 70175 literals remain 68%
c [treelook-6] 8021 variables remain to probed next time 15%
c [treelook-6] removed 69 variables, found 28661 hbrs
c [unhide-16] limit 3743370 with penalty 2 = 0 + 2
c [unhide-16-23] 2 units, 50 failed, 50072 tauts, 0 hbrs, 658997 literals
c [transred-12] limit 2000000 with penalty 0 = 0 + 0
c [transred-12] removed 170 transitive binary clauses
c [cce-8] boosting limit by 10
c [cce-8] limit of 935842617 steps penalty 2 = 2 + 0
c [cce-8-1] eliminated 2 clauses out of 3 (67%) of length 58
c [cce-8-1] eliminated 1 clauses out of 3 (33%) of length 57
c [cce-8-1] eliminated 2 clauses out of 4 (50%) of length 56
c [cce-8-1] eliminated 1 clauses out of 4 (25%) of length 55
c [cce-8-1] eliminated 2 clauses out of 4 (50%) of length 54
c [cce-8-1] eliminated 1 clauses out of 3 (33%) of length 53
c [cce-8-1] eliminated 4 clauses out of 6 (67%) of length 52
c [cce-8-1] eliminated 2 clauses out of 4 (50%) of length 51
c [cce-8-1] eliminated 4 clauses out of 6 (67%) of length 50
c [cce-8-1] eliminated 3 clauses out of 6 (50%) of length 49
c [cce-8-1] eliminated 5 clauses out of 6 (83%) of length 48
c [cce-8-1] eliminated 4 clauses out of 7 (57%) of length 47
c [cce-8-1] eliminated 5 clauses out of 8 (62%) of length 46
c [cce-8-1] eliminated 4 clauses out of 6 (67%) of length 45
c [cce-8-1] eliminated 5 clauses out of 8 (62%) of length 44
c [cce-8-1] eliminated 4 clauses out of 6 (67%) of length 43
c [cce-8-1] eliminated 5 clauses out of 9 (56%) of length 42
c [cce-8-1] eliminated 6 clauses out of 8 (75%) of length 41
c [cce-8-1] eliminated 6 clauses out of 10 (60%) of length 40
c [cce-8-1] eliminated 6 clauses out of 8 (75%) of length 39
c [cce-8-1] eliminated 6 clauses out of 10 (60%) of length 38
c [cce-8-1] eliminated 6 clauses out of 8 (75%) of length 37
c [cce-8-1] eliminated 6 clauses out of 11 (55%) of length 36
c [cce-8-1] eliminated 6 clauses out of 9 (67%) of length 35
c [cce-8-1] eliminated 6 clauses out of 9 (67%) of length 34
c [cce-8-1] eliminated 6 clauses out of 10 (60%) of length 33
c [cce-8-1] eliminated 6 clauses out of 10 (60%) of length 32
c [cce-8-1] eliminated 6 clauses out of 12 (50%) of length 31
c [cce-8-1] eliminated 6 clauses out of 8 (75%) of length 30
c [cce-8-1] eliminated 5 clauses out of 13 (38%) of length 29
c [cce-8-1] eliminated 8 clauses out of 9 (89%) of length 28
c [cce-8-1] eliminated 7 clauses out of 15 (47%) of length 27
c [cce-8-1] eliminated 7 clauses out of 10 (70%) of length 26
c [cce-8-1] eliminated 8 clauses out of 14 (57%) of length 25
c [cce-8-1] eliminated 7 clauses out of 10 (70%) of length 24
c [cce-8-1] eliminated 8 clauses out of 15 (53%) of length 23
c [cce-8-1] eliminated 7 clauses out of 11 (64%) of length 22
c [cce-8-1] eliminated 8 clauses out of 15 (53%) of length 21
c [cce-8-1] eliminated 7 clauses out of 12 (58%) of length 20
c [cce-8-1] eliminated 8 clauses out of 16 (50%) of length 19
c [cce-8-1] eliminated 9 clauses out of 14 (64%) of length 18
c [cce-8-1] eliminated 9 clauses out of 17 (53%) of length 17
c [cce-8-1] eliminated 9 clauses out of 15 (60%) of length 16
c [cce-8-1] eliminated 10 clauses out of 19 (53%) of length 15
c [cce-8-1] eliminated 15 clauses out of 19 (79%) of length 14
c [cce-8-1] eliminated 10 clauses out of 22 (45%) of length 13
c [cce-8-1] eliminated 16 clauses out of 19 (84%) of length 12
c [cce-8-1] eliminated 12 clauses out of 26 (46%) of length 11
c [cce-8-1] eliminated 18 clauses out of 22 (82%) of length 10
c [cce-8-1] eliminated 13 clauses out of 31 (42%) of length 9
c [cce-8-1] eliminated 26 clauses out of 34 (76%) of length 8
c [cce-8-1] eliminated 22 clauses out of 69 (32%) of length 7
c [cce-8-1] eliminated 33 clauses out of 3010 (1%) of length 6
c [cce-8-1] eliminated 305 clauses out of 10864 (3%) of length 5
c [cce-8-1] eliminated 2226 clauses out of 21128 (11%) of length 4
c [cce-8-1] completed large round (ATE)
c [cce-8-1] eliminated 2939 large clauses in 590156852 steps
c [cce-8-1] allowing another 295078426 steps for small clauses
c [cce-8-1] scheduling 330507 clauses = 178341 binary + 152166 ternary
c [cce-8-1] tried to eliminate 16042 small clauses 5%
c [cce-8-1] eliminated 2214 binary clauses 1%
c [cce-8-1] eliminated 458 ternary clauses 0%
c [cce-8-1] eliminated 2672 small clauses 1%
c [cce-8-1] eliminated 3701 small clauses in 935842618 steps
c [cce-8-1] incomplete small round (ATE)
c [cce-8-1] eliminated 6640 covered clauses in round 1
c [cce-8] eliminated 6640 covered clauses in TOTAL during 1 rounds
c [bca-12] limit of 10000000 steps and 760161 added (scaled 2)
c [bca-12] 78718 out of 103752 literals actually usable 76%
c [bca-12] added 43 blocked clauses in 219062 steps
c [phase-count-16] 378842 negative 99.8% of 379506 except 664 0.2%
c [phase-count-16] 293754 positive 77.4% of 379506 except 85752 22.6%
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 12116 enqueued variables after 170140 conflicts
c [score-dist-16] active 39759 (77%), one 477 (1%), zero 11639 (22%)
c [score-dist-16] max exp 510, different 479 (94%)
c [score-dist-16] median active exp 486, avg 403.1
c [simplification-16] removed 176 variables 0.3% (51875 remain 21%)
c [simplification-16] removed 11460 irredundant clauses 2.9% (379506 remain 28%)
c [simplification-16] maximum reduction of 3% = max (0%, 3%)
c [simplification-16] geometric conflict interval increment 11833 = 47332 / 4
c [simplification-16] new conflict interval 59165
c [simplification-16] penalized conflict interval 59165 = 1 * 59165
c [simplification-16] hard conflict limit 258887 (soft 229305 + delta 29582)
c [simplification-16] new conflict limit 229305 (hard 258887)
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  470.1   51874   379506    174230   48932   8816 1210407  291   575  154  51%     62   82  217  251   87%
c i  475.2   51873   379506    177958   51464   8822 1210418  277   506  154  55%    -47    7  175  252   69%
c -  486.0   51873   379506    186246   26451   8834 1210435  279   456   76  61%     24  -41  236  257   92%
c i  515.0   51872   379506    215713   43976   9018 1210536  265   440  146  60%    386  -34  360  255  141%
c -  547.9   51823   379506    242008   28898   9097 1210619  196   286   77  68%    196 -159  164  249   66%
c 
c [simplification-17] limit 229305 conflicts (hard 258887) hit after 258888 conflicts
c [quatres-11] found 19936 quaternary clauses 52% in total
c [quatres-11-1] removed 3 duplicate quaternary clauses
c [quatres-11-2] added 1 single-self-subsuming ternary resolvents
c [ternres-12] limit 104634314 with penalty 0 = 0 + 0
c [ternres-12] all 51823 free variables schedulable
c [ternres-12] 317 ternary resolvents (0 bin, 317 trn)
c [ternres-12] fully completed ternary resolution
c [decomp-39] removed 82 variables
c [basicprobe-6] limit 400000000 penalty 0 = 0 + 0
c [basicprobe-6-0] 1859 sched 4%, 466 failed, 22 lifted, 100880 hbrs
c [decomp-40] removed 716 variables
c [basicprobe-6-1] 2194 probes remain 4% after last round
c [basicprobe-6-1] 909 units = 869 failed (96%) + 40 lifted (4%)
c [basicprobe-6-1] removed 1641 variables, found 388705 hbrs
c [bate-4] eliminated 390 asymmetric tautologies during probing
c [unhide-17] limit 10000000 with penalty 1 = 0 + 1
c [unhide-17-26] 0 units, 38 failed, 113548 tauts, 0 hbrs, 102729 literals
c [transred-13] limit 2000000 with penalty 0 = 0 + 0
c [transred-13] removed 119 transitive binary clauses
c [elim-13] scheduling all variables this time
c [elim-13] scheduled 50066 variables 100%
c [elim-13] almost no limit of 100000000000 steps
c [elim-13] rescheduling of touched variables disabled
c [elim-13-1] eliminated 792 variables 2% in round 1 in 31290007 steps
c [elim-13-1] backward subsumption/strengthening limit 31290000
c [elim-13-1-1] backward checking 4651 touched variables 9%
c [elim-13-1-1] fully completed backward checking in 1 rounds
c [elim-13-1] subsumed 5 and strengthened 59 clauses in 1195530 steps
c [elim-13-1] rescheduled 143 variables 0% by backward subsumption
c [elim-13-2] eliminated 9 variables 0% in round 2 in 75312 steps
c [elim-13-2] backward subsumption/strengthening limit 75300
c [elim-13-2-1] backward checking 110 touched variables 0%
c [elim-13-2-1] fully completed backward checking in 1 rounds
c [elim-13-2] subsumed 1 and strengthened 0 clauses in 74407 steps
c [elim-13-2] rescheduled 3 variables 0% by backward subsumption
c [elim-13-3] no variable eliminated in round 3 in 1643 steps
c [elim-13] fully completed in 3 rounds
c [elim-13] transition to [ all 0 rem 0 ] state
c [elim-13] eliminated 801 = 2% variables out of 50066 scheduled
c [bca-13] limit of 10000000 steps and 707967 added (scaled 2)
c [bca-13] 75202 out of 98532 literals actually usable 76%
c [bca-13] added 32 blocked clauses in 199610 steps
c [sweep-11] boosting sweeping limit by 10
c [sweep-11] limit 156951470 penalty 1 = 1 + 0
c [sweep-11-1] 2016 pos 10.5% + 17099 neg 89.5% = 19115 sched 38.8% ret 30150
c [sweep-11-1] 157093232 steps 5646 queries 53.78 avg class size
c [sweep-11-1] 37504 decisions 5051 SAT calls 76.60 avg env size
c [sweep-11-1] 885 variables remain 2% (48232 retained 98%)
c [decomp-41] removed 1074 variables
c [sweep-11-1] removed 1074 vars (1 failed, 620 eqs, 1100 impls)
c [sweep-11] removed 1074 vars in TOTAL (1 rounds, 5645 queries)
c [phase-count-17] 351163 negative 99.8% of 351829 except 666 0.2%
c [phase-count-17] 272061 positive 77.3% of 351829 except 79768 22.7%
c [phase-count-17] skipping relative phase luck test
c [phase-17] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-17] sorted 13246 enqueued variables after 258888 conflicts
c [score-dist-17] active 34945 (73%), one 2961 (6%), zero 10285 (21%)
c [score-dist-17] max exp 510, different 489 (96%)
c [score-dist-17] median active exp 502, avg 461.5
c [simplification-17] removed 3632 variables 7.0% (48191 remain 20%)
c [simplification-17] removed 27677 irredundant clauses 7.3% (351829 remain 26%)
c [simplification-17] maximum reduction of 7% = max (7%, 7%)
c [simplification-17] large reduction 7% >= 5% limit
c [simplification-17] next conflict interval 2588 = min (258888/100, 59165)
c [simplification-17] penalized conflict interval 2588 = 1 * 2588
c [simplification-17] hard conflict limit 271476 (soft 261476 + delta 10000)
c [simplification-17] new conflict limit 261476 (hard 271476)
c 
c [simplification-18] limit 261476 conflicts (hard 271476) hit after 271476 conflicts
c [quatres-12] found 18859 quaternary clauses 50% in total
c [quatres-12-2] added 2 single-self-subsuming ternary resolvents
c [quatres-12-2] added 2 quaternary resolvents
c [ternres-13] limit 109566011 with penalty 0 = 0 + 0
c [ternres-13] all 48191 free variables schedulable
c [ternres-13] 746 ternary resolvents (1 bin, 745 trn)
c [ternres-13] fully completed ternary resolution
c [simpleprobe-7] 2009 schedulable variables 4%
c [simpleprobe-7] limit 200000000 penalty 0 = 0 + 0
c [decomp-43] removed 49 variables
c [simpleprobe-7] 3451 variables remain 7% (44691 retained 93%)
c [simpleprobe-7] removed 49 variables, found 89618 hbrs, 21 units
c [unhide-18] limit 5000000 with penalty 2 = 0 + 2
c [unhide-18-27] 0 units, 13 failed, 133673 tauts, 0 hbrs, 48635 literals
c [transred-14] limit 2000000 with penalty 0 = 0 + 0
c [transred-14] removed 158 transitive binary clauses
c [cce-9] limit of 273915029 steps penalty 1 = 1 + 0
c [cce-9-1] eliminated 2 clauses out of 2 (100%) of length 86
c [cce-9-1] eliminated 1 clauses out of 2 (50%) of length 85
c [cce-9-1] eliminated 1 clauses out of 2 (50%) of length 84
c [cce-9-1] eliminated 2 clauses out of 2 (100%) of length 83
c [cce-9-1] eliminated 1 clauses out of 2 (50%) of length 82
c [cce-9-1] eliminated 1 clauses out of 2 (50%) of length 81
c [cce-9-1] eliminated 1 clauses out of 2 (50%) of length 80
c [cce-9-1] eliminated 1 clauses out of 2 (50%) of length 79
c [cce-9-1] eliminated 2 clauses out of 3 (67%) of length 78
c [cce-9-1] eliminated 1 clauses out of 2 (50%) of length 77
c [cce-9-1] eliminated 2 clauses out of 2 (100%) of length 76
c [cce-9-1] eliminated 1 clauses out of 3 (33%) of length 75
c [cce-9-1] eliminated 1 clauses out of 3 (33%) of length 74
c [cce-9-1] eliminated 1 clauses out of 2 (50%) of length 73
c [cce-9-1] eliminated 1 clauses out of 3 (33%) of length 72
c [cce-9-1] eliminated 1 clauses out of 2 (50%) of length 71
c [cce-9-1] eliminated 2 clauses out of 3 (67%) of length 70
c [cce-9-1] eliminated 2 clauses out of 5 (40%) of length 34
c [cce-9-1] eliminated 1 clauses out of 7 (14%) of length 33
c [cce-9-1] eliminated 4 clauses out of 9 (44%) of length 32
c [cce-9-1] eliminated 2 clauses out of 8 (25%) of length 31
c [cce-9-1] eliminated 4 clauses out of 9 (44%) of length 30
c [cce-9-1] eliminated 6 clauses out of 14 (43%) of length 29
c [cce-9-1] eliminated 6 clauses out of 12 (50%) of length 28
c [cce-9-1] eliminated 5 clauses out of 13 (38%) of length 27
c [cce-9-1] eliminated 5 clauses out of 11 (45%) of length 26
c [cce-9-1] eliminated 3 clauses out of 12 (25%) of length 25
c [cce-9-1] eliminated 7 clauses out of 12 (58%) of length 24
c [cce-9-1] eliminated 5 clauses out of 16 (31%) of length 23
c [cce-9-1] eliminated 7 clauses out of 11 (64%) of length 22
c [cce-9-1] eliminated 4 clauses out of 15 (27%) of length 21
c [cce-9-1] eliminated 9 clauses out of 13 (69%) of length 20
c [cce-9-1] eliminated 5 clauses out of 17 (29%) of length 19
c [cce-9-1] eliminated 7 clauses out of 12 (58%) of length 18
c [cce-9-1] eliminated 5 clauses out of 16 (31%) of length 17
c [cce-9-1] eliminated 7 clauses out of 14 (50%) of length 16
c [cce-9-1] eliminated 6 clauses out of 20 (30%) of length 15
c [cce-9-1] eliminated 10 clauses out of 17 (59%) of length 14
c [cce-9-1] eliminated 7 clauses out of 21 (33%) of length 13
c [cce-9-1] eliminated 10 clauses out of 17 (59%) of length 12
c [cce-9-1] eliminated 7 clauses out of 26 (27%) of length 11
c [cce-9-1] eliminated 11 clauses out of 20 (55%) of length 10
c [cce-9-1] eliminated 11 clauses out of 37 (30%) of length 9
c [cce-9-1] eliminated 20 clauses out of 39 (51%) of length 8
c [cce-9-1] eliminated 20 clauses out of 79 (25%) of length 7
c [cce-9-1] eliminated 23 clauses out of 2953 (1%) of length 6
c [cce-9-1] eliminated 177 clauses out of 9787 (2%) of length 5
c [cce-9-1] eliminated 34 clauses out of 17944 (0%) of length 4
c [cce-9-1] incomplete large round (ACCE)
c [cce-9-1] eliminated 452 large clauses in 273915030 steps
c [cce-9-1] allowing another 136957515 steps for small clauses
c [cce-9-1] scheduling 181673 clauses = 167678 binary + 13995 ternary
c [cce-9-1] tried to eliminate 8104 small clauses 4%
c [cce-9-1] eliminated 1888 binary clauses 1%
c [cce-9-1] eliminated 213 ternary clauses 2%
c [cce-9-1] eliminated 2101 small clauses 1%
c [cce-9-1] eliminated 2365 small clauses in 273915033 steps
c [cce-9-1] incomplete small round (ACCE)
c [cce-9-1] eliminated 2817 covered clauses in round 1
c [cce-9] eliminated 2817 covered clauses in TOTAL during 1 rounds
c [cce-9] 2817 < 1/100 * 351396 = 3513 considered unsuccessful
c [elim-14] scheduling all variables this time
c [elim-14] scheduled 48089 variables 100%
c [elim-14] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-14] rescheduling of touched variables disabled
c [elim-14-1] eliminated 375 variables 1% in round 1 in 32610487 steps
c [elim-14-1] backward subsumption/strengthening limit 32610400
c [elim-14-1-1] backward checking 2221 touched variables 5%
c [elim-14-1-1] fully completed backward checking in 1 rounds
c [elim-14-1] subsumed 1 and strengthened 23 clauses in 556528 steps
c [elim-14-1] rescheduled 44 variables 0% by backward subsumption
c [elim-14-2] eliminated 1 variables 0% in round 2 in 27723 steps
c [elim-14-2] backward subsumption/strengthening limit 27700
c [elim-14-2-1] backward checking 19 touched variables 0%
c [elim-14-2-1] incomplete backward checking 0 remain 0%
c [elim-14-2] subsumed 0 and strengthened 0 clauses in 27701 steps
c [elim-14-2] fully rescheduled 47713 variables 99%
c [elim-14-3] eliminated 8 variables 0% in round 3 in 32704500 steps
c [elim-14-3] backward subsumption/strengthening limit 32704500
c [elim-14-3-1] backward checking 60 touched variables 0%
c [elim-14-3-1] fully completed backward checking in 1 rounds
c [elim-14-3] subsumed 0 and strengthened 0 clauses in 59570 steps
c [elim-14] fully completed in 3 rounds
c [elim-14] transition to [ all 0 rem 0 ] state
c [elim-14] eliminated 384 = 1% variables out of 48089 scheduled
c [elim-14] 384 < 1/100 * 48089 = 480 considered unsuccessful
c [bca-14] limit of 10000000 steps and 696311 added (scaled 2)
c [bca-14] 69823 out of 95412 literals actually usable 73%
c [bca-14] added 165 blocked clauses in 191869 steps
c [sweep-12] limit 32869803 penalty 0 = 0 + 0
c [sweep-12-1] 20 pos 3.7% + 524 neg 96.3% = 544 sched 1.1% ret 47161
c [sweep-12-1] 3965504 steps 417 queries 14.62 avg class size
c [sweep-12-1] 2058 decisions 336 SAT calls 52.14 avg env size
c [sweep-12-1] fully completed sweeping round
c [decomp-44] removed 120 variables
c [sweep-12-1] removed 120 vars (1 failed, 80 eqs, 96 impls)
c [sweep-12-2] 4303 pos 9.0% + 43282 neg 91.0% = 47585 sched 100.0% ret 0
c [sweep-12-2] 28965917 steps 466 queries 394.55 avg class size
c [sweep-12-2] 11625 decisions 451 SAT calls 233.02 avg env size
c [sweep-12-2] 31968 variables remain 67% (15583 retained 33%)
c [decomp-45] removed 48 variables
c [sweep-12-2] removed 48 vars (0 failed, 15 eqs, 31 impls)
c [sweep-12] removed 168 vars in TOTAL (2 rounds, 881 queries)
c [phase-count-18] 346226 negative 99.8% of 346869 except 643 0.2%
c [phase-count-18] 268922 positive 77.5% of 346869 except 77947 22.5%
c [phase-count-18] skipping relative phase luck test
c [phase-18] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-18] sorted 13032 enqueued variables after 271476 conflicts
c [score-dist-18] active 34505 (73%), one 2835 (6%), zero 10197 (21%)
c [score-dist-18] max exp 510, different 477 (93%)
c [score-dist-18] median active exp 497, avg 457.1
c [simplification-18] removed 654 variables 1.4% (47537 remain 19%)
c [simplification-18] removed 4960 irredundant clauses 1.4% (346869 remain 25%)
c [simplification-18] maximum reduction of 1% = max (1%, 1%)
c [simplification-18] geometric conflict interval increment 29582 = 59165 / 2
c [simplification-18] new conflict interval 88747
c [simplification-18] penalized conflict interval 88747 = 1 * 88747
c [simplification-18] hard conflict limit 404596 (soft 360223 + delta 44373)
c [simplification-18] new conflict limit 360223 (hard 404596)
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  631.1   47536   346869    275562   43445   6260 1316072  232   343  107  68%    528  -41  216  235   92%
c i  642.6   47535   346869    284113   47787   6271 1316083  263   373  128  71%   -245   -8  274  238  115%
c i  644.2   47530   346869    286121   49104   6273 1316083  247   385  128  64%   -320    5  246  237  104%
c i  650.2   47528   346869    292723   52379   6291 1316094  220   323  128  68%   -237  -54  252  234  108%
c -  671.3   47528   346869    311278   29596   6306 1316134  231   296   76  78%     -5  -78  198  239   83%
c i  695.8   47527   346869    334436   38071   6354 1316182  303   441  113  69%    301  100  448  235  191%
c i  697.5   47522   346869    335720   38759   6376 1316189  342   503  117  68%   -145  160  476  239  200%
c 
c [simplification-19] limit 360223 conflicts (hard 404596) hit after 369601 conflicts
c [quatres-13] found 18569 quaternary clauses 49% in total
c [quatres-13-1] removed 1 duplicate quaternary clauses
c [quatres-13-2] added 9 single-self-subsuming ternary resolvents
c [quatres-13-2] added 4 quaternary resolvents
c [ternres-14] limit 143866074 with penalty 0 = 0 + 0
c [ternres-14] all 47522 free variables schedulable
c [ternres-14] 161 ternary resolvents (1 bin, 160 trn)
c [ternres-14] fully completed ternary resolution
c [gauss-5] limit 1798325 penalty 4 = 4 + 0
c [gauss-5] extracted 19 xors of average arity 2.9
c [gauss-5] connected 56 occurrences of 50 variables (average 1.1)
c [gauss-5] limit 1798325 penalty 4 = 4 + 0
c [gauss-5] fully completed
c [gauss-5] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-46] removed 3 variables
c [treelook-7] limit 14386607 penalty 0 = 0 + 0 boost 1
c [treelook-7] scheduled 61929 literals 65%
c [treelook-7] scheduling used 1627554 steps
c [treelook-7] scheduled completely
c [treelook-7] limit 14386607 penalty 0 = 0 + 0 boost 1
c [treelook-7] used 14457370 steps
c [treelook-7] 61413 literals remain 65%
c [treelook-7] 7018 variables remain to probed next time 15%
c [treelook-7] removed 77 variables, found 7945 hbrs
c [unhide-19] limit 5000000 with penalty 2 = 0 + 2
c [unhide-19-29] 0 units, 8 failed, 54732 tauts, 0 hbrs, 300985 literals
c [transred-15] limit 2000000 with penalty 0 = 0 + 0
c [transred-15] removed 175 transitive binary clauses
c [bca-15] limit of 10000000 steps and 687213 added (scaled 2)
c [bca-15] 68624 out of 94868 literals actually usable 72%
c [bca-15] added 56 blocked clauses in 203089 steps
c [sweep-13] limit 43159822 penalty 0 = 0 + 0
c [sweep-13-1] 3590 pos 11.2% + 28366 neg 88.8% = 31956 sched 67.4% ret 15477
c [sweep-13-1] 43206078 steps 944 queries 203.20 avg class size
c [sweep-13-1] 17895 decisions 918 SAT calls 185.67 avg env size
c [sweep-13-1] 21127 variables remain 45% (26297 retained 55%)
c [decomp-48] removed 42 variables
c [sweep-13-1] removed 42 vars (0 failed, 30 eqs, 91 impls)
c [sweep-13] 42 < 1/1000 * 47433 = 47 considered unsuccessful
c [sweep-13] removed 42 vars in TOTAL (1 rounds, 943 queries)
c [phase-count-19] 342107 negative 99.8% of 342754 except 647 0.2%
c [phase-count-19] 265588 positive 77.5% of 342754 except 77166 22.5%
c [phase-count-19] skipping relative phase luck test
c [phase-19] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-19] sorted 13189 enqueued variables after 369601 conflicts
c [score-dist-19] active 34202 (72%), one 3168 (7%), zero 10021 (21%)
c [score-dist-19] max exp 510, different 461 (90%)
c [score-dist-19] median active exp 497, avg 414.5
c [simplification-19] removed 131 variables 0.3% (47391 remain 19%)
c [simplification-19] removed 4115 irredundant clauses 1.2% (342754 remain 25%)
c [simplification-19] maximum reduction of 1% = max (0%, 1%)
c [simplification-19] geometric conflict interval increment 44373 = 88747 / 2
c [simplification-19] new conflict interval 133120
c [simplification-19] penalized conflict interval 133120 = 1 * 133120
c [simplification-19] hard conflict limit 569281 (soft 502721 + delta 66560)
c [simplification-19] new conflict limit 502721 (hard 569281)
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 -  775.3   47391   342754    384905   31402   6435 1279867  225   298   76  75%    373  -50  196  243   81%
c -  885.2   47391   342754    477925   32482   6533 1279917  235   281   78  84%    867  -10  195  225   87%
c 
c [simplification-20] limit 502721 conflicts (hard 569281) hit after 507348 conflicts
c [quatres-14] found 18581 quaternary clauses 48% in total
c [quatres-14-2] added 2 single-self-subsuming ternary resolvents
c [quatres-14-2] added 1 quaternary resolvents
c [ternres-15] limit 194558577 with penalty 0 = 0 + 0
c [ternres-15] all 47391 free variables schedulable
c [ternres-15] 48 ternary resolvents (1 bin, 47 trn)
c [ternres-15] fully completed ternary resolution
c [basicprobe-7] limit 400000000 penalty 0 = 0 + 0
c [basicprobe-7-0] 2959 sched 6%, 201 failed, 7 lifted, 70291 hbrs
c [decomp-50] removed 276 variables
c [basicprobe-7-1] 2747 probes remain 6% after last round
c [basicprobe-7-1] 357 units = 346 failed (97%) + 11 lifted (3%)
c [basicprobe-7-1] removed 558 variables, found 209135 hbrs
c [bate-5] eliminated 277 asymmetric tautologies during probing
c [unhide-20] limit 10000000 with penalty 1 = 0 + 1
c [unhide-20-32] 2 units, 12 failed, 104141 tauts, 0 hbrs, 111699 literals
c [transred-16] limit 2000000 with penalty 0 = 0 + 0
c [transred-16] removed 147 transitive binary clauses
c [block-6] scheduling all variables this time
c [block-6] scheduled 46805 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 124 blocked clauses
c [block-6] 124 < 1/100 * 334526 = 3345 considered unsuccessful
c [elim-15] scheduling all variables this time
c [elim-15] scheduled 46797 variables 100%
c [elim-15] limit of 400000000 steps penalty 1 = 1 + 0
c [elim-15] rescheduling of touched variables disabled
c [elim-15-1] eliminated 269 variables 1% in round 1 in 30560879 steps
c [elim-15-1] backward subsumption/strengthening limit 30560800
c [elim-15-1-1] backward checking 1762 touched variables 4%
c [elim-15-1-1] fully completed backward checking in 1 rounds
c [elim-15-1] subsumed 1 and strengthened 14 clauses in 489764 steps
c [elim-15-1] rescheduled 59 variables 0% by backward subsumption
c [elim-15-2] eliminated 1 variables 0% in round 2 in 25645 steps
c [elim-15-2] backward subsumption/strengthening limit 25600
c [elim-15-2-1] backward checking 26 touched variables 0%
c [elim-15-2-1] incomplete backward checking 0 remain 0%
c [elim-15-2] subsumed 0 and strengthened 2 clauses in 25601 steps
c [elim-15-2] rescheduled 8 variables 0% by backward subsumption
c [elim-15-3] eliminated 1 variables 0% in round 3 in 6240 steps
c [elim-15-3] backward subsumption/strengthening limit 6200
c [elim-15-3-1] backward checking 10 touched variables 0%
c [elim-15-3-1] incomplete backward checking 3 remain 30%
c [elim-15-3] subsumed 0 and strengthened 2 clauses in 6201 steps
c [elim-15] incomplete 8 not tried 0% in round 3
c [elim-15] transition to [ all 1 rem 1 ] state
c [elim-15] eliminated 273 = 1% variables out of 46797 scheduled
c [elim-15] 273 < 1/100 * 46797 = 467 considered unsuccessful
c [bca-16] limit of 10000000 steps and 669315 added (scaled 2)
c [bca-16] 67911 out of 93050 literals actually usable 73%
c [bca-16] added 64 blocked clauses in 185133 steps
c [sort-queue-20] sorted 19972 enqueued variables after 507348 conflicts
c [score-dist-20] active 26552 (57%), one 10340 (22%), zero 9632 (21%)
c [score-dist-20] max exp 510, different 454 (89%)
c [score-dist-20] median active exp 492, avg 426.0
c [simplification-20] removed 867 variables 1.8% (46524 remain 19%)
c [simplification-20] removed 8745 irredundant clauses 2.6% (334009 remain 24%)
c [simplification-20] maximum reduction of 3% = max (2%, 3%)
c [simplification-20] geometric conflict interval increment 33280 = 133120 / 4
c [simplification-20] new conflict interval 166400
c [simplification-20] penalized conflict interval 166400 = 1 * 166400
c [simplification-20] hard conflict limit 756948 (soft 673748 + delta 83200)
c [simplification-20] new conflict limit 673748 (hard 756948)
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  947.2   46523   334009    514092   41842   6512 1319559  233   281  104  83%    933   -3  214  227   94%
c i  949.0   46521   334009    515773   42381   6516 1319561  219   267  104  82%  -1276  -17  209  226   93%
c
c CAUGHT SIGNAL 15 SIGTERM
c
c s UNKNOWN
c bate: 3604 basic ate = 3370 trn 94% + 234 lrg 6% in 5 updates
c bcas: 16 count, 1659 added (1439 skipped), 4528566 steps
c bkwd: tried 434676 clauses, 869023 lits, 2.00 lits/clause
c bkwd: checked 12688092 occs, 29.19 occs/clause, 14.60 occs/lit
c bkwd: subsumed 7 binary, 193 ternary, 10 large
c bkwd: strengthened 0 binary, 1 ternary (100% self), 360 large (0% self)
c blkd: 6 bces, 13345 removed, 10224560 resolutions, 28865270 steps
c blkd: 16704 blocking literals 3%, 37 pure
c bump: 554869 bumped seen, 499591266 lits 900.4 on average
c card: 5 count, 0 units, 0 am1, 387946245 steps
c card: 0 rescheduled, 0 eliminated, 0 resolved, 76302 subsumed
c card: 16894 at-most-one constraints found, average size 4.83
c card: 16894 at-most-one constraints used 100%, average size 4.83
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: 9 cces, 79492 eliminated, 78635 ate 99%, 857 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: 158 gcs, 0 rescored clauses, 2154 rescored vars
c dcps: 50 decompositions, 9648 equivalent 4%
c deco: 281098 decision-only clauses 51%, 67% reduction
c decs: 10742274 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 15 elims, 109741 eliminated 42%, 238 pure 0%
c elms: 41 rounds, 2.7 rounds/bve
c elms: 85860 small 78%, 23606 large 22%
c elms: 222474 tried small, 85860 succeeded 39%, 136614 failed 61%
c elms: 45903 subsumed, 74353 strengthened, 1517 blocked
c elms: 24514000 copies, 23837369 resolutions, 5714520 ipos
c elms: 7115085 subchks, 4281055 strchks
c gaus: 5 extractions, 120 extracted, 2.6 size, 3 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 17408150 steps, 8704075 extr 50%, 462 elim 0%
c glue: 240.6 orig avg, 240.6 real avg, 10.1 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 3096066 = 494833 simple 16% + 2567196 trn 83% + 34037 lrg 1%, 4880 sub 0%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 554869 clauses, 318.8 length
c lrnd: 176911529 lits = 367482899 orig - 190571370 removed 52%
c lrnd: 274508 uips 49%, 243788 flips 44%
c mins: 199217 mins 41%, 2050 bin 0%, 5195 size 1%
c mins: 77617361 poisoned searches, 17490475 hits, 23% hit rate
c mins: 98207812 used twice searches, 12712120 hits, 13% hit rate
c move: moved 33178, 23919 bin 72%, 9259 trn 28%
c otfs: 5834 driving 32%, 12117 restarting 68%
c otfs: str 17951, 17855 red 99%, 96 irr 1%
c otfs: str 17951, 0 bin 0%, 88 trn 0%, 17863 lrg 100%
c otfs: sub 104, 104 red 100%, 0 irr 0%
c otfs: sub 104, 0 bin 0%, 0 trn 0%, 104 lrg 100%
c phas: 19 computed, 152417 set, 9 pos (0%), 152408 neg (100%)
c prbs: 7 basic, 100403 probed, 3760 failed, 186 lifted
c prbs: 7 simple, 791968 probed, 676 failed, 536 eqs
c prbs: 7 treelook, 801 probed, 55 failed, 0 lifted
c prom: 20651 locked 2% out of 1367703 tried
c prps: 2343840735 props, 207 props/dec
c prps: 95% srch, 5% simp, 0% lkhd
c quat: 14 count, 85 quat, 22 self1, 0 self2, 600 dup
c queu: 20 sorted, 10742274 next (62144 steps 0.01)
c queu: 577917945 enq (923316289 steps 1.60), 499591266 deq 86%
c redc: 2728 clauses 24%, 11199 tried 2%, 59 sat 1%
c redc: 7683 lits 7%, 112575 tried 0%, 59 sat 0%
c redc: 292 times jump level reduced, 98.3 levels on average
c reds: 6 count, 92853.2 conflicts per reduce
c reds: 0 memlim 0%, 6 arith 100%
c reds: 157552 collected 86%, 25574 retired 14%
c rmbd: 59140 removed, 19678 red 33%
c rsts: 9851 restarts 97%, 269 skipped 3%
c rsts: 269 saturating 100%, 0 reuse 0%
c rsts: 0 kept 0.0% average 0.0%
c scnc: 0 count, 1.000 min (0/1000), 1.000 max (0/1000)
c simp: 20 count, 18 confs 90%, 0 vars 0%
c simp: 1 its 5%, 1 bin 5%, 0 trns 0%
c subl: 554869 count (717416 tried 1.3), 262301 sub out of 548523 (47.8%)
c swps: 13 count, 14 rounds, 10676 queries (762.6/round)
c swps: 9716 sat calls, 102 unsat (0.4% success rate)
c swps: 102872 decisions 10.6, 3584 conflicts 0.4
c swps; 495.3 avg class size, 101.8 avg environment size
c swps: 2 failed, 1870 impls, 1018 equivs
c swp0: 3553 type 0 queries, 1711 unsat (48.2%), 3195 sat (89.9%)
c swp1: 7123 type 1 queries, 3721 unsat (52.2%), 6463 sat (90.7%)
c sync: 0 produced units, 0 successful consumptions 0%
c sync: 0 consume units calls, 0 tried 0%, 0 success 0%
c sync: 0 produced clauses, 0 successful consumptions 0%
c sync: 0 consume clause calls, 0 tried 0%, 0 success 0%
c time: 22599343 calls to obtain time
c tops: 93363 fixed 36%, 373 its, 1493.62 confs/it
c trds: 16 transitive reductions, 2838 removed, 19 failed
c trds: 14330 nodes, 51815 edges, 32037992 steps
c trim: 4369791 words, 16.7 MB
c trnr: 15 count, 4 bin, 9445 trn, 283501020 steps
c unhd: 20 count, 32 rounds, 119805679 steps
c unhd: 873 non-trivial sccs of average size 2.2
c unhd: 86 units, 85 bin, 1 trn, 0 lrg
c unhd: 8358 failed, 8303 stamp, 0 lits, 39 bin, 8 trn, 0 lrg
c unhd: 1099939 tauts, 29876 bin 3%, 8725 trn 1%, 369 lrg 0%
c unhd: 1099939 tauts, 1060969 stamp 96%, 1020578 red 93%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 4202600 str, 85 bin 0%, 3741 trn 0%, 4198774 lrg 100%, 4186170 red 100%
c vars: 46482 remaining 18% and 212752 removed 82% out of 259234
c vars: 93363 fixed 36%, 109741 eliminated 42%, 9648 equivalent 4%
c vsts: 22535561237 visits, 94% srch, 6% simp, 0% lkhd
c vsts: 9.5 search visits per propagation, 38106.4 per conflict
c wchs: 1138848946 pushed, 54374459 enlarged, 228 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all         548608        157552         25574      55353476       9007337        290988
c 
c  0 0         12542   2      1024   1         0   0  16820897  30   1638585  18     24357   8     0.9
c  1 5          3119   1       667   0       374   1   2778333   5    364966   4      7185   2     0.3
c  2 6          7396   1      1950   1       769   3   4286102   8    578575   6     14673   5     0.8
c  3 9          9034   2      2775   2       770   3   4660974   8    653511   7     16439   6     1.0
c  4 14        10218   2      3802   2       855   3   3375222   6<   570868   6     16542   6     1.3
c  5 21        12214   2      4542   3       860   3   4897267   9    843325   9<    23220   8     1.6
c  6 30        16540   3      7199   5      1060   4   4814899   9    955369  11     26557   9     2.7
c  7 41        17500   3      8658   5      1178   5   4169484   8    840230   9     24828   9<    3.4
c  8 54        18883   3     11294   7      1288   5   3299470   6    677339   8     20647   7     2.9
c  9 69        20749   4     13750   9      1299   5   2226190   4    503085   6     18525   6     4.2
c 10 86        38148   7<    25223  16<     2316   9<  2068117   4    560865   6     30744  11     7.5
c 11 126      104332  19     31642  20      4187  16   1097707   2    417555   5     28575  10    22.5
c 12 230      238080  43     37624  24      8430  33    731760   1    348350   4     30849  11    47.3
c 13 534       39560   7      7402   5      2188   9    126263   0     54444   1      7812   3    35.0
c 14 1526        293   0         0   0         0   0       791   0       270   0        35   0     1.9
c 15 5046          0   0         0   0         0   0         0   0         0   0         0   0     0.0
c 
c avg                 10.2           9.6           9.7           3.8           5.2           7.0
c std                  3.0           2.7           3.2           3.5           3.7           3.8
c 
c   99.783  10% bump
c   92.429   9% cce
c   71.695   7% probe
c   43.043   4% unhide
c   27.006   3% sweep
c   21.809   2% elim
c   10.427   1% rescore
c    6.286   1% decide
c    4.503   0% bca
c 
c   11.257 < 1% rest (below)
c 
c    3.807   0% block
c    2.144   0% gauss
c    2.128   0% transred
c    1.977   0% ternres
c    0.782   0% quatres
c    0.419   0% card
c    0.000   0% locs
c    0.000   0% queuesort
c ==================================
c    5.138   1% preprocessing     2%
c  283.511  28% inprocessing     98%
c ==================================
c  288.649  29% simplifying
c  710.580  71% search
c ==================================
c  999.233 100% all
c 
c        557119 conflicts,         557.5 confs/sec
c          2624 ternaries,         212.3 confs/ternary
c          2359 binaries,          236.2 confs/binary
c           373 iterations,       1493.6 confs/iteration
c 
c             6 reductions,          0.0 redus/sec,  92853.2 confs/reduction
c          9851 restarts,            9.9 rests/sec,     56.6 confs/restart
c      10742274 decisions,       10750.5 decis/sec,     19.3 decis/conflict
c    2343840735 propagations,  2345640.3 props/sec,    218.2 props/decision
c 
c 999.2 seconds, 201.6 MB
c
c CAUGHT SIGNAL 15 SIGTERM
c
c launch: done
