c launch: /data/cnf/sc2014/app/partial-10-17-s.cnf.bz2
c host: atom32
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/partial-10-17-s.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/partial-10-17-s.cnf.bz2
c no embedded options
c found 'p cnf 298900 1409628' header
c read 298900 variables, 1409628 clauses, 3261218 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=5
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 287740 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] EVSIDS (--score=5)
c [set-score-increment-1] factor 1.200000d+00 (200/1000) after 0 conflicts
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  287740  1385857         0       0      0     0    0     0   64   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 11220 at-most-one constraints of average size 5.2
c [card-1] no at-most-two constraint found
c [card-1] using previous limit 2000000 for elimination
c [card-1] 11220 out of 11220 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 129705 variables
c [simpleprobe-1] all 169195 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 1390 variables
c [simpleprobe-1] 7799 variables remain 5% (160006 retained 95%)
c [simpleprobe-1] removed 1390 variables, found 18529 hbrs, 9 units
c [unhide-1] limit 60588 based on 969417 irredundant clauses
c [unhide-1-1] 1 units, 196 failed, 8012 tauts, 0 hbrs, 9081 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 167330 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 60911 not tried 36% in round 1
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 62796 = 38% variables out of 167330 scheduled
c [elim-1] considered successful since not run to completion yet
c [phase-count-1] 733852 negative 99.2% of 739575 except 5723 0.8%
c [phase-count-1] 592701 positive 80.1% of 739575 except 146874 19.9%
c [phase-count-1] less non-negative clauses 5723 than limit 73900 (10.0%)
c [phase-count-1] non-pos/non-neg = 146874/5723 = 25.66 >= 2.00 = 200/100
c [lucky-phase-1] forcing lucky phase -1
c [phase-1] phase bias: 0 positive 0%, 104534 negative 100%
c [sort-queue-1] sorted 104534 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 104534 (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 136559 variables 56.6% (104534 remain 36%)
c [simplification-1] removed 646282 irredundant clauses 46.6% (739575 remain 53%)
c [simplification-1] maximum reduction of 57% = max (57%, 47%)
c [simplification-1] large reduction 57% >= 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.0  104533   739575       149     128     11 10795    1    10   57   5%      0   10    6    0 17367%
c i    5.1  104485   739575       201     162     19 10804    1    11   57   5%      0   11    5    0 14861%
c i    5.2  102950   739575       263     172     19 10806    1    12   57   5%      0   12    5    0 14320%
c i    5.2  102770   739575       304     200     24 10811    1    12   57   5%      0   12    5    0 13320%
c i    5.3  102759   739575       374     249     36 10815    1    12   57   6%      0   12    5    0 11776%
c i    5.4  102657   739575       512     358     50 10824    1    16   57   6%      0   16    7    0 10450%
c i    5.5  101947   739575       536     374     53 10828    1    17   57   6%      0   17    6    0 9734%
c i    5.5  101790   739575       543     380     53 10828    1    17   57   6%      0   17    6    0 9576%
c i    5.5  101301   739575       544     380     53 10828    1    17   57   6%      0   17    6    0 9538%
c i    5.5  101288   739575       548     380     55 10829    1    17   57   6%      0   17    6    0 9410%
c 
c [simplification-2] limit of 10 iterations hit after 10 iterations
c [decomp-3] removed 3345 variables
c [simpleprobe-2] 7487 schedulable variables 7%
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [simpleprobe-2] 7240 variables remain 7% (93949 retained 93%)
c [simpleprobe-2] removed 0 variables, found 1872 hbrs, 0 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 66633 literals 33%
c [treelook-1] scheduling used 335186 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 303214 steps
c [treelook-1] 66605 literals remain 33%
c [treelook-1] 64079 variables remain to probed next time 63%
c [treelook-1] removed 20 variables, found 1215 hbrs
c [basicprobe-1] limit 5736864 based on 717108 irredundant clauses
c [basicprobe-1-0] 34003 probes remain 35% after last round
c [basicprobe-1-0] 28 units = 28 failed (100%) + 0 lifted (0%)
c [basicprobe-1-0] removed 4924 variables, found 10579 hbrs
c [unhide-2] limit 100000 with penalty 0 = 0 + 0
c [unhide-2-2] 0 units, 284 failed, 5216 tauts, 0 hbrs, 14199 literals
c [elim-2] 57362 variables 60% will be scheduled this time
c [elim-2] scheduled 57362 variables 60%
c [elim-2] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-2] rescheduling of touched variables disabled
c [elim-2] incomplete 18840 not tried 20% in round 1
c [elim-2] transition to [ all 0 rem 1 ] state
c [elim-2] eliminated 610 = 1% variables out of 57362 scheduled
c [elim-2] considered successful since not run to completion yet
c [phase-count-2] 650748 negative 99.1% of 656471 except 5723 0.9%
c [phase-count-2] 527046 positive 80.3% of 656471 except 129425 19.7%
c [phase-count-2] less non-negative clauses 5723 than limit 65600 (10.0%)
c [phase-count-2] non-pos/non-neg = 129425/5723 = 22.61 >= 2.00 = 200/100
c [lucky-phase-2] forcing lucky phase -1
c [phase-2] phase bias: 0 positive 0%, 5169 negative 100%
c [sort-queue-2] sorted 84084 enqueued variables after 548 conflicts
c [score-dist-2] active 10176 (11%), one 0 (0%), zero 84084 (89%)
c [score-dist-2] max exp 630, different 125 (20%)
c [score-dist-2] median active exp 589, avg 582.2
c [simplification-2] removed 7027 variables 6.9% (94260 remain 33%)
c [simplification-2] removed 83104 irredundant clauses 11.2% (656471 remain 47%)
c [simplification-2] maximum reduction of 11% = max (7%, 11%)
c [simplification-2] forced so keeping old conflict interval 0
c [simplification-2] conflict limit remains at 1013 (hard 11000)
c [simplification-2] new iteration interval 100
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i    8.6   94259   656471       550     352     50 16779    1    17   52   6%      0   17    6    0 9340%
c i    8.6   94045   656471       552     353     50 16779    1    17   52   6%      0   17    6    0 9279%
c i    8.6   94032   656471       562     356     52 16783    1    17   52   6%      0   17    6    0 8989%
c i    8.6   93532   656471       572     360     52 16787    1    18   52   6%      0   17    6    0 8702%
c i    9.0   93251   656471       887     610     76 16817    2    26   53   6%      1   26    8    0 7652%
c i    9.0   93239   656471       941     654     78 16821    2    28   53   6%      1   27   10    0 8106%
c 
c [simplification-3] limit 1025 conflicts (hard 11000) hit after 1026 conflicts
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 4029 at-most-one constraints of average size 4.7
c [card-2] no at-most-two constraint found
c [card-2] using previous limit 1000000 for elimination
c [card-2] 4029 out of 4029 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [decomp-6] removed 1228 variables
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] scheduled 51529 literals 28%
c [treelook-2] scheduling used 300003 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] used 305411 steps
c [treelook-2] 51498 literals remain 28%
c [treelook-2] 42074 variables remain to probed next time 45%
c [decomp-7] removed 2 variables
c [treelook-2] removed 17 variables, found 745 hbrs
c [unhide-3] limit 100000 with penalty 0 = 0 + 0
c [unhide-3-3] 0 units, 112 failed, 12372 tauts, 0 hbrs, 1837 literals
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 92793 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 24909 not tried 27% in round 1
c [elim-3] transition to [ all 1 rem 1 ] state
c [elim-3] eliminated 5320 = 6% variables out of 92793 scheduled
c [elim-3] considered successful since not run to completion yet
c [phase-count-3] 618467 negative 99.1% of 623995 except 5528 0.9%
c [phase-count-3] 502221 positive 80.5% of 623995 except 121774 19.5%
c [phase-count-3] less non-negative clauses 5528 than limit 62300 (10.0%)
c [phase-count-3] non-pos/non-neg = 121774/5528 = 22.03 >= 2.00 = 200/100
c [lucky-phase-3] forcing lucky phase -1
c [phase-3] phase bias: 0 positive 0%, 4196 negative 100%
c [sort-queue-3] sorted 71634 enqueued variables after 1026 conflicts
c [score-dist-3] active 15839 (18%), one 0 (0%), zero 71634 (82%)
c [score-dist-3] max exp 756, different 228 (30%)
c [score-dist-3] median active exp 674, avg 665.0
c [simplification-3] removed 5755 variables 6.2% (87473 remain 30%)
c [simplification-3] removed 32476 irredundant clauses 4.9% (623995 remain 45%)
c [simplification-3] maximum reduction of 6% = max (6%, 5%)
c [simplification-3] large reduction 6% >= 5% limit
c [simplification-3] next conflict interval 2000 = 2000/1
c [simplification-3] penalized conflict interval 2000 = 1 * 2000
c [simplification-3] hard conflict limit 13026 (soft 3026 + delta 10000)
c [simplification-3] new conflict limit 3026 (hard 13026)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   11.9   87472   623995      1214     721    113 14631    2    33   51   7%      1   33    9    0 5597%
c i   11.9   87311   623995      1231     736    114 14631    2    33   51   7%      1   33    8    0 5365%
c i   12.0   87304   623995      1346     835    124 14636    2    37   51   6%      1   36    8    0 4884%
c i   12.2   87293   623995      1479     920    143 14661    2    39   51   6%      1   39    8    0 4167%
c i   12.4   87281   623995      1746    1123    174 14684    3    45   52   7%      1   45   10    0 4464%
c i   12.7   87264   623995      1858    1196    189 14703    3    50   52   7%      1   49   10    0 3951%
c i   12.7   87021   623995      1870    1200    193 14706    3    50   52   7%      1   49    9    0 3804%
c 
c [simplification-4] limit of 186 binary hit after 186 binaries
c [decomp-8] removed 550 variables
c [basicprobe-2] limit 4962488 based on 620311 irredundant clauses
c [basicprobe-2-0] 28666 probes remain 33% after last round
c [basicprobe-2-0] 25 units = 25 failed (100%) + 0 lifted (0%)
c [basicprobe-2-0] removed 489 variables, found 16496 hbrs
c [unhide-4] limit 128670 with penalty 0 = 0 + 0
c [unhide-4-4] 0 units, 395 failed, 2774 tauts, 0 hbrs, 1522 literals
c [elim-4] 18680 variables 22% will be scheduled this time
c [elim-4] scheduled 18680 variables 22%
c [elim-4] boosting limit by 20
c [elim-4] limit of 400000000 steps penalty 0 = 0 + 0
c [elim-4] rescheduling of touched variables disabled
c [elim-4-1] no variable eliminated in round 1 in 35012120 steps
c [elim-4] fully completed in 1 rounds
c [elim-4] transition to [ all 0 rem 0 ] state
c [elim-4] eliminated 0 = 0% variables out of 18680 scheduled
c [phase-count-4] 605536 negative 99.1% of 611064 except 5528 0.9%
c [phase-count-4] 491098 positive 80.4% of 611064 except 119966 19.6%
c [phase-count-4] less non-negative clauses 5528 than limit 61100 (10.0%)
c [phase-count-4] non-pos/non-neg = 119966/5528 = 21.70 >= 2.00 = 200/100
c [lucky-phase-4] forcing lucky phase -1
c [phase-4] phase bias: 0 positive 0%, 1969 negative 100%
c [sort-queue-4] sorted 62561 enqueued variables after 1955 conflicts
c [score-dist-4] active 23421 (27%), one 0 (0%), zero 62561 (73%)
c [score-dist-4] max exp 998, different 402 (40%)
c [score-dist-4] median active exp 911, avg 847.4
c [simplification-4] removed 956 variables 1.1% (85982 remain 30%)
c [simplification-4] removed 12931 irredundant clauses 2.1% (611064 remain 44%)
c [simplification-4] maximum reduction of 2% = max (1%, 2%)
c [simplification-4] forced so keeping old conflict interval 0
c [simplification-4] conflict limit remains at 3026 (hard 13026)
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   14.8   85981   611064      1965    1257    202 27041    3    51   51   7%      1   51    9    0 3538%
c i   14.9   85903   611064      2033    1291    216 27059    3    52   51   7%      1   51    8    0 2972%
c i   14.9   85293   611064      2077    1329    218 27062    4    53   51   7%      1   52    9    0 3185%
c i   15.0   85214   611064      2131    1369    226 27066    4    54   51   7%      1   53    8    0 2842%
c i   15.1   85164   611064      2214    1430    238 27074    4    56   51   6%      1   55    7    0 2606%
c i   15.2   84924   611064      2244    1450    241 27079    4    56   51   6%      1   55    7    0 2510%
c i   15.2   84807   611064      2260    1458    245 27082    4    56   51   6%      1   55    7    0 2394%
c i   15.5   84738   611064      2511    1662    267 27103    4    62   51   6%      1   61    8    0 2375%
c i   15.6   84548   611064      2536    1680    270 27106    4    62   51   6%      1   61    7    0 2262%
c i   15.7   84419   611064      2659    1773    285 27116    4    66   51   6%      1   64    7    0 2124%
c i   16.1   84407   611064      2966    2029    303 27141    5    76   51   6%      2   74   13    0 3242%
c 
c [simplification-5] limit 3026 conflicts (hard 13026) hit after 3026 conflicts
c [quatres-1] found 33271 quaternary clauses 38% in total
c [ternres-1] boosting ternary resolution limit by 5
c [ternres-1] limit 20000000 with penalty 0 = 0 + 0
c [ternres-1] all 84398 free variables schedulable
c [ternres-1] 72 ternary resolvents (0 bin, 72 trn)
c [ternres-1] fully completed ternary resolution
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 305 xors of average arity 2.2
c [gauss-1] connected 674 occurrences of 350 variables (average 1.9)
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 200 variables
c [unhide-5] limit 201277 with penalty 0 = 0 + 0
c [unhide-5-5] 4 units, 117 failed, 11253 tauts, 0 hbrs, 3131 literals
c [transred-1] limit 1006387 with penalty 0 = 0 + 0
c [transred-1] removed 99 transitive binary clauses
c [transred-1] found 3 units
c [block-1] scheduling all variables this time
c [block-1] scheduled 83797 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 9883 blocked clauses
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 4 clauses out of 71 (6%) of length 10
c [cce-1-1] eliminated 923 clauses out of 2291 (40%) of length 9
c [cce-1-1] eliminated 365 clauses out of 895 (41%) of length 8
c [cce-1-1] eliminated 251 clauses out of 3041 (8%) of length 7
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 1543 large clauses in 30000004 steps
c [cce-1-1] allowing another 15000002 steps for small clauses
c [cce-1-1] scheduling 394243 clauses = 273709 binary + 120534 ternary
c [cce-1-1] tried to eliminate 313 small clauses 0%
c [cce-1-1] eliminated 91 binary clauses 0%
c [cce-1-1] eliminated 22 ternary clauses 0%
c [cce-1-1] eliminated 113 small clauses 0%
c [cce-1-1] eliminated 113 small clauses in 30000009 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 1656 covered clauses in round 1
c [cce-1] eliminated 1656 covered clauses in TOTAL during 1 rounds
c [cce-1] 1656 < 1/100 * 579936 = 5799 considered unsuccessful
c [bca-1] limit of 10000000 steps and 1157060 added (scaled 2)
c [bca-1] 154331 out of 167596 literals actually usable 92%
c [bca-1] added 275 blocked clauses in 454427 steps
c [sweep-1] limit 1156560 based on 578280 irredundant clauses
c [sweep-1-1] 5491 pos 6.6% + 78306 neg 93.4% = 83797 sched 100.0% ret 0
c [sweep-1-1] 1327926 steps 16 queries 22884.25 avg class size
c [sweep-1-1] 85 decisions 10 SAT calls 69.90 avg env size
c [sweep-1-1] 83750 variables remain 100% (41 retained 0%)
c [decomp-10] removed 27 variables
c [sweep-1-1] removed 27 vars (0 failed, 5 eqs, 10 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 27 vars in TOTAL (1 rounds, 15 queries)
c [phase-count-5] 572678 negative 99.0% of 578186 except 5508 1.0%
c [phase-count-5] 472749 positive 81.8% of 578186 except 105437 18.2%
c [phase-count-5] less non-negative clauses 5508 than limit 57800 (10.0%)
c [phase-count-5] non-pos/non-neg = 105437/5508 = 19.14 >= 2.00 = 200/100
c [lucky-phase-5] forcing lucky phase -1
c [phase-5] phase bias: 0 positive 0%, 1711 negative 100%
c [sort-queue-5] sorted 56217 enqueued variables after 3026 conflicts
c [score-dist-5] active 27553 (33%), one 0 (0%), zero 56217 (67%)
c [score-dist-5] max exp 778, different 564 (72%)
c [score-dist-5] median active exp 627, avg 567.2
c [simplification-5] removed 628 variables 0.7% (83770 remain 29%)
c [simplification-5] removed 32878 irredundant clauses 5.4% (578186 remain 42%)
c [simplification-5] maximum reduction of 5% = max (1%, 5%)
c [simplification-5] large reduction 5% >= 5% limit
c [simplification-5] next conflict interval 2000 = 2000/1
c [simplification-5] penalized conflict interval 2000 = 1 * 2000
c [simplification-5] hard conflict limit 15026 (soft 5026 + delta 10000)
c [simplification-5] new conflict limit 5026 (hard 15026)
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   20.3   83769   578186      3397    2333    436 38389    6    82   51   7%      2   80   17    1 3233%
c i   20.6   83603   578186      3592    2485    450 38414    6    86   51   7%      2   84   14    1 2513%
c i   20.8   83572   578186      3678    2549    462 38421    7    88   51   8%      2   85   15    1 2641%
c i   20.9   83566   578186      3847    2683    474 38431    8    93   51   8%      2   90   22    1 3405%
c i   21.0   83555   578186      3860    2690    476 38434    8    93   51   8%      2   90   22    1 3260%
c i   21.6   83431   578186      4283    3034    510 38472    9   106   51   8%      2  103   19    1 2479%
c i   21.7   83321   578186      4305    3054    511 38472    9   109   51   8%      2  105   19    1 2430%
c i   21.8   83307   578186      4342    3083    514 38475    9   111   51   8%      2  107   18    1 2326%
c i   21.9   83306   578186      4368    3100    517 38479    9   110   51   8%      2  107   17    1 2155%
c i   21.9   83299   578186      4438    3152    526 38486    9   113   51   8%      2  109   18    1 2217%
c i   22.3   83014   578186      4606    3282    544 38502    9   119   51   8%      2  115   17    1 1955%
c i   22.5   82940   578186      4711    3374    551 38506   10   126   51   8%      2  122   18    1 2012%
c i   22.9   82905   578186      4944    3569    570 38518   10   135   51   8%      2  131   19    1 1950%
c i   22.9   82892   578186      4945    3569    570 38518   10   135   51   8%      2  131   18    1 1942%
c i   23.0   82881   578186      4993    3606    575 38522   10   137   51   8%      2  132   19    1 1961%
c i   23.0   82838   578186      4994    3606    575 38522   10   137   51   8%      2  132   19    1 1953%
c i   23.1   82817   578186      5021    3624    581 38524   10   137   51   8%      2  132   17    1 1800%
c 
c [simplification-6] limit 5046 conflicts (hard 15026) hit after 5046 conflicts
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] all 82807 free variables schedulable
c [ternres-2] 10 ternary resolvents (0 bin, 10 trn)
c [ternres-2] 54549 variables remain 66% (28258 retained 34%)
c [card-3] limit 500000 penalty 2 = 2 + 0
c [card-3] found 1619 at-most-one constraints of average size 4.1
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 500000 for elimination
c [card-3] 1619 out of 1619 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [decomp-11] removed 1446 variables
c [simpleprobe-3] 6892 schedulable variables 8%
c [simpleprobe-3] limit 3800761 penalty 1 = 1 + 0
c [decomp-12] removed 41 variables
c [simpleprobe-3] 9686 variables remain 12% (72597 retained 88%)
c [simpleprobe-3] removed 41 variables, found 6826 hbrs, 6 units
c [unhide-6] limit 380076 with penalty 0 = 0 + 0
c [unhide-6-6] 0 units, 166 failed, 3799 tauts, 0 hbrs, 6999 literals
c [transred-2] limit 1900380 with penalty 0 = 0 + 0
c [transred-2] removed 202 transitive binary clauses
c [transred-2] found 3 units
c [block-2] scheduling all variables this time
c [block-2] scheduled 81956 variables 100%
c [block-2] limit of 50000000 steps penalty 0 = 0 + 0
c [block-2] fully completed
c [block-2] transition to [ all 0 rem 0 ] state
c [block-2] eliminated 1218 blocked clauses
c [block-2] 1218 < 1/100 * 570813 = 5708 considered unsuccessful
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 81956 variables 100%
c [elim-5] limit of 19003809 steps penalty 1 = 1 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5] incomplete 19381 not tried 24% in round 1
c [elim-5] transition to [ all 1 rem 1 ] state
c [elim-5] eliminated 1769 = 2% variables out of 81956 scheduled
c [bca-2] limit of 10000000 steps and 1126261 added (scaled 2)
c [bca-2] 143553 out of 160376 literals actually usable 90%
c [bca-2] added 149 blocked clauses in 407407 steps
c [sweep-2] limit 1125624 based on 562812 irredundant clauses
c [sweep-2-1] 4820 pos 6.0% + 75334 neg 94.0% = 80154 sched 100.0% ret 33
c [sweep-2-1] 1332029 steps 16 queries 21793.44 avg class size
c [sweep-2-1] 178 decisions 13 SAT calls 131.08 avg env size
c [sweep-2-1] 80067 variables remain 100% (71 retained 0%)
c [decomp-13] removed 54 variables
c [sweep-2-1] removed 54 vars (0 failed, 4 eqs, 6 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 54 vars in TOTAL (1 rounds, 15 queries)
c [phase-count-6] 557475 negative 99.1% of 562559 except 5084 0.9%
c [phase-count-6] 459248 positive 81.6% of 562559 except 103311 18.4%
c [phase-count-6] less non-negative clauses 5084 than limit 56200 (10.0%)
c [phase-count-6] non-pos/non-neg = 103311/5084 = 20.32 >= 2.00 = 200/100
c [lucky-phase-6] forcing lucky phase -1
c [phase-6] phase bias: 0 positive 0%, 826 negative 100%
c [sort-queue-6] sorted 48077 enqueued variables after 5046 conflicts
c [score-dist-6] active 32056 (40%), one 3316 (4%), zero 44761 (56%)
c [score-dist-6] max exp 808, different 625 (77%)
c [score-dist-6] median active exp 683, avg 613.0
c [simplification-6] removed 2674 variables 3.2% (80133 remain 28%)
c [simplification-6] removed 15627 irredundant clauses 2.7% (562559 remain 41%)
c [simplification-6] maximum reduction of 3% = max (3%, 3%)
c [simplification-6] geometric conflict interval increment 5000 = 20000 / 4
c [simplification-6] new conflict interval 5000
c [simplification-6] penalized conflict interval 5000 = 1 * 5000
c [simplification-6] hard conflict limit 20046 (soft 10046 + delta 10000)
c [simplification-6] new conflict limit 10046 (hard 20046)
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   26.9   80132   562559      5157    2951    571 41784   10   137   50   7%      2  132   13    1 1306%
c i   26.9   80131   562559      5183    2974    573 41784   10   137   50   7%      2  132   13    1 1338%
c i   27.3   80130   562559      5519    3222    610 41819   11   142   50   8%      2  136   17    1 1547%
c i   27.4   80128   562559      5544    3240    614 41821   11   143   50   7%      2  137   16    1 1460%
c i   27.6   79895   562559      5637    3305    628 41833   11   145   50   7%      2  139   14    1 1287%
c i   27.6   79883   562559      5651    3313    630 41836   11   145   50   7%      2  139   13    1 1232%
c i   27.9   79745   562559      5834    3471    639 41849   11   147   50   7%      2  141   16    1 1412%
c i   28.2   79735   562559      6117    3695    668 41867   11   147   50   7%      2  140   12    1 1057%
c i   29.0   79731   562559      6536    4035    705 41900   11   161   50   7%      2  153   15    1 1164%
c i   29.1   79720   562559      6600    4086    712 41904   11   161   50   7%      2  153   15    1 1184%
c i   29.3   79715   562559      6783    4230    721 41921   12   162   50   7%      2  154   23    1 1681%
c i   29.5   79714   562559      6909    4340    724 41931   12   164   51   8%      2  155   23    1 1688%
c i   29.7   79709   562559      7031    4435    733 41945   13   164   51   8%      2  155   20    1 1444%
c i   29.8   79664   562559      7087    4474    740 41953   13   164   51   8%      2  154   20    1 1374%
c i   29.9   79641   562559      7202    4568    749 41958   14   164   51   8%      2  155   30    2 2021%
c i   30.0   79635   562559      7307    4656    756 41965   14   164   51   8%      1  154   24    2 1590%
c i   30.1   79629   562559      7357    4700    758 41966   14   163   51   8%      1  153   22    2 1413%
c i   30.5   79619   562559      7685    4980    780 41981   14   171   51   8%      2  161   23    2 1413%
c i   30.6   79607   562559      7779    5046    794 41994   14   172   51   8%      2  161   19    2 1122%
c i   31.0   79466   562559      7954    5170    815 42014   14   177   51   8%      2  165   17    2  986%
c i   31.4   79456   562559      8186    5347    836 42043   15   183   51   8%      2  171   24    2 1309%
c i   31.5   79449   562559      8227    5379    840 42047   15   185   51   8%      2  172   22    2 1225%
c i   31.5   79439   562559      8234    5384    841 42047   15   185   51   8%      2  173   22    2 1197%
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   31.9   79299   562559      8484    5585    865 42066   15   190   52   8%      2  178   18    2  976%
c i   31.9   79234   562559      8516    5606    872 42069   15   190   52   8%      2  177   18    2  976%
c i   32.2   79227   562559      8693    5763    880 42079   15   190   52   8%      1  177   18    2  960%
c i   32.3   79211   562559      8740    5802    883 42081   16   192   52   8%      1  179   20    2 1029%
c i   32.7   79210   562559      8989    6017    895 42094   16   197   52   8%      1  183   24    2 1200%
c i   33.2   79095   562559      9301    6275    913 42123   18   205   52   9%      2  190   33    2 1533%
c i   33.9   79094   562559      9730    6638    947 42146   18   213   52   9%      2  197   25    2 1076%
c i   33.9   79087   562559      9733    6640    947 42146   18   213   52   9%      2  197   25    2 1067%
c i   33.9   79082   562559      9734    6640    947 42146   18   213   52   9%      2  197   25    2 1063%
c i   33.9   79075   562559      9735    6640    947 42146   18   213   52   9%      2  197   25    2 1059%
c i   33.9   79074   562559      9739    6643    947 42146   18   213   52   9%      2  197   24    2 1047%
c i   33.9   79068   562559      9740    6643    947 42146   18   213   52   9%      2  197   24    2 1043%
c i   34.3   79066   562559      9979    6855    956 42161   19   221   52   8%      2  204   22    2  929%
c 
c [simplification-7] limit 10082 conflicts (hard 20046) hit after 10082 conflicts
c [quatres-2] found 30639 quaternary clauses 38% in total
c [quatres-2-2] added 2 single-self-subsuming ternary resolvents
c [quatres-2-2] added 230 quaternary resolvents
c [ternres-3] limit 4000000 with penalty 0 = 0 + 0
c [ternres-3] 52093 schedulable variables 65%
c [ternres-3] 40 ternary resolvents (0 bin, 40 trn)
c [ternres-3] 24937 variables remain 32% (54124 retained 68%)
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] extracted 16 xors of average arity 2.7
c [gauss-2] connected 43 occurrences of 40 variables (average 1.1)
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] fully completed
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-14] removed 24 variables
c [treelook-3] limit 394593 penalty 0 = 0 + 0 boost 1
c [treelook-3] scheduled 51160 literals 32%
c [treelook-3] scheduling used 404181 steps
c [treelook-3] not fully scheduled
c [treelook-3] limit 394593 penalty 0 = 0 + 0 boost 1
c [treelook-3] used 513978 steps
c [treelook-3] 51154 literals remain 32%
c [treelook-3] 28073 variables remain to probed next time 36%
c [treelook-3] removed 1 variables, found 2390 hbrs
c [unhide-7] limit 789186 with penalty 0 = 0 + 0
c [unhide-7-7] 3 units, 278 failed, 8134 tauts, 0 hbrs, 19854 literals
c [transred-3] limit 2000000 with penalty 0 = 0 + 0
c [transred-3] removed 142 transitive binary clauses
c [transred-3] found 8 units
c [cce-2] limit of 15000000 steps penalty 1 = 1 + 0
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] allowing another 7500002 steps for small clauses
c [cce-2-1] scheduling 375618 clauses = 259123 binary + 116495 ternary
c [cce-2-1] tried to eliminate 145 small clauses 0%
c [cce-2-1] eliminated 37 binary clauses 0%
c [cce-2-1] eliminated 13 ternary clauses 0%
c [cce-2-1] eliminated 50 small clauses 0%
c [cce-2-1] eliminated 3416 small clauses in 15000014 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 3416 covered clauses in round 1
c [cce-2] eliminated 3416 covered clauses in TOTAL during 1 rounds
c [cce-2] 3416 < 1/100 * 548787 = 5487 considered unsuccessful
c [elim-6] 19336 variables 25% will be scheduled this time
c [elim-6] scheduled 19336 variables 25%
c [elim-6] limit of 78918688 steps penalty 0 = 0 + 0
c [elim-6] rescheduling of touched variables disabled
c [elim-6-1] no variable eliminated in round 1 in 33023261 steps
c [elim-6] fully completed in 1 rounds
c [elim-6] transition to [ all 0 rem 0 ] state
c [elim-6] eliminated 0 = 0% variables out of 19336 scheduled
c [bca-3] limit of 10000000 steps and 1087534 added (scaled 2)
c [bca-3] 132655 out of 157340 literals actually usable 84%
c [bca-3] added 61 blocked clauses in 361185 steps
c [sweep-3] limit 1183780 penalty 0 = 0 + 0
c [sweep-3-1] 4443 pos 5.7% + 74164 neg 94.3% = 78607 sched 99.9% ret 62
c [sweep-3-1] 1244930 steps 12 queries 16876.58 avg class size
c [sweep-3-1] 128 decisions 11 SAT calls 55.36 avg env size
c [sweep-3-1] 78551 variables remain 100% (118 retained 0%)
c [decomp-16] removed 1 variables
c [sweep-3-1] removed 1 vars (0 failed, 0 eqs, 1 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 1 vars in TOTAL (1 rounds, 11 queries)
c [phase-count-7] 538324 negative 99.1% of 543410 except 5086 0.9%
c [phase-count-7] 444880 positive 81.9% of 543410 except 98530 18.1%
c [phase-count-7] less non-negative clauses 5086 than limit 54300 (10.0%)
c [phase-count-7] non-pos/non-neg = 98530/5086 = 19.37 >= 2.00 = 200/100
c [lucky-phase-7] forcing lucky phase -1
c [phase-7] phase bias: 0 positive 0%, 430 negative 100%
c [sort-queue-7] sorted 48023 enqueued variables after 10082 conflicts
c [score-dist-7] active 30645 (39%), one 10206 (13%), zero 37817 (48%)
c [score-dist-7] max exp 629, different 560 (89%)
c [score-dist-7] median active exp 518, avg 447.1
c [simplification-7] removed 393 variables 0.5% (78668 remain 27%)
c [simplification-7] removed 19149 irredundant clauses 3.4% (543410 remain 39%)
c [simplification-7] maximum reduction of 3% = max (0%, 3%)
c [simplification-7] geometric conflict interval increment 5000 = 20000 / 4
c [simplification-7] new conflict interval 10000
c [simplification-7] penalized conflict interval 10000 = 1 * 10000
c [simplification-7] hard conflict limit 30082 (soft 20082 + delta 10000)
c [simplification-7] new conflict limit 20082 (hard 30082)
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.3   78667   543410     10177    7099   1086 45571   19   222   53   8%      2  204   22    2  906%
c i   38.3   78661   543410     10178    7099   1086 45571   19   222   53   8%      2  204   22    2  902%
c i   38.8   78622   543410     10392    7276   1100 45587   19   224   53   8%      2  205   21    3  830%
c i   38.9   78616   543410     10445    7318   1102 45594   19   224   53   8%      2  206   21    3  839%
c i   39.1   78605   543410     10579    7434   1107 45601   19   227   53   8%      2  208   22    3  837%
c i   40.3   78600   543410     11214    7954   1159 45649   20   240   53   8%      3  219   18    3  658%
c i   40.5   78599   543410     11370    8092   1163 45658   20   237   53   8%      3  215   22    3  774%
c i   40.6   78274   543410     11453    8160   1168 45661   20   235   53   8%      3  213   20    3  711%
c i   40.8   78267   543410     11550    8241   1175 45668   20   234   53   8%      3  212   19    3  666%
c i   41.2   78258   543410     11750    8416   1182 45685   20   243   53   8%      2  220   23    3  795%
c i   41.3   78208   543410     11777    8429   1186 45692   20   243   53   8%      2  220   22    3  739%
c i   41.3   78149   543410     11790    8438   1186 45694   20   243   53   8%      2  220   21    3  711%
c i   41.8   78137   543410     12041    8662   1194 45710   21   246   53   9%      2  222   34    3 1111%
c i   42.1   78104   543410     12166    8765   1200 45722   21   249   53   9%      2  225   34    3 1070%
c i   42.7   78099   543410     12564    9099   1225 45748   23   253   53   9%      2  227   36    3 1078%
c i   43.3   78073   543410     12916    9396   1246 45769   23   259   53   9%      2  232   28    3  819%
c i   43.3   78069   543410     12918    9397   1246 45769   23   259   53   9%      2  232   28    3  813%
c i   43.4   78066   543410     12970    9442   1247 45773   23   258   53   9%      2  231   26    3  749%
c i   43.4   78060   543410     12971    9442   1247 45773   23   258   53   9%      2  231   26    3  746%
c i   44.2   78054   543410     13446    9856   1264 45799   24   264   53   9%      3  236   28    4  771%
c i   44.5   78049   543410     13702   10076   1273 45816   24   266   53   9%      3  236   24    4  649%
c i   44.6   78048   543410     13750   10113   1277 45821   23   265   53   9%      2  235   23    4  621%
c i   45.3   77908   543410     14186   10500   1291 45847   25   270   54   9%      3  239   36    4  913%
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   46.0   77906   543410     14602   10845   1327 45875   24   267   54   9%      3  234   24    4  588%
c i   46.3   77781   543410     14747   10956   1339 45891   24   267   54   9%      3  234   22    4  534%
c i   46.4   77780   543410     14786   10985   1342 45894   25   267   54   9%      2  234   30    4  733%
c i   46.5   77771   543410     14830   11020   1347 45897   25   270   55   9%      2  236   29    4  705%
c i   46.5   77701   543410     14835   11023   1348 45897   25   270   55   9%      2  236   29    4  694%
c i   46.7   77414   543410     14919   11093   1351 45903   24   272   55   9%      2  239   26    4  622%
c i   46.7   77295   543410     14941   11109   1352 45907   24   273   55   9%      2  239   26    4  622%
c i   46.8   77193   543410     14974   11134   1354 45910   24   274   55   9%      2  240   25    4  590%
c i   46.9   77098   543410     15023   11174   1359 45913   24   275   56   9%      2  241   25    4  590%
c i   47.6   77096   543410     15362   11432   1386 45943   26   278   56   9%      2  243   33    4  747%
c i   47.9   77044   543410     15484   11538   1392 45948   27   286   56   9%      2  250   39    4  875%
c i   48.4   77043   543410     15744   11777   1399 45960   27   298   57   9%      2  261   43    5  931%
c i   48.6   77036   543410     15835   11856   1405 45964   28   301   57   9%      2  263   39    5  828%
c i   48.9   77032   543410     15963   11965   1408 45970   28   301   57   9%      2  264   37    5  775%
c i   49.2   77029   543410     16173   12148   1418 45982   28   305   57   9%      2  266   32    5  658%
c i   49.4   77021   543410     16251   12214   1422 45987   28   306   57   9%      1  267   32    5  669%
c i   50.1   77009   543410     16706   12605   1441 46012   29   308   57  10%      2  267   39    5  776%
c i   50.1   76999   543410     16708   12605   1441 46013   29   308   57  10%      2  267   39    5  770%
c i   50.3   76955   543410     16792   12673   1448 46021   29   306   57  10%      2  265   34    5  665%
c i   50.8   76951   543410     17057   12915   1453 46034   30   311   57  10%      2  269   39    5  737%
c i   51.1   76950   543410     17312   13140   1459 46045   31   305   57  10%      2  262   43    5  790%
c i   51.5   76933   543410     17576   13367   1465 46064   31   302   57  10%      2  257   35    5  645%
c i   52.2   76932   543410     17974   13706   1483 46091   31   314   58  10%      2  268   33    6  590%
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   52.3   76910   543410     18024   13751   1486 46092   31   315   58  10%      2  269   31    6  544%
c i   52.3   76900   543410     18032   13757   1486 46093   31   315   58  10%      2  269   30    6  530%
c i   53.0   76899   543410     18463   14140   1502 46109   33   315   58  10%      2  267   57    6  964%
c i   53.1   76572   543410     18524   14186   1510 46114   33   314   58  10%      2  266   49    6  816%
c i   53.6   76523   543410     18871   14493   1520 46133   33   314   59  10%      2  265   37    6  609%
c i   54.7   76517   543410     19468   15016   1544 46162   35   317   59  11%      3  265   47    7  718%
c i   55.2   76507   543410     19984   15471   1561 46171   38   304   59  12%      3  250   56    7  812%
c 
c [simplification-8] limit 20115 conflicts (hard 30082) hit after 20115 conflicts
c [quatres-3] found 26808 quaternary clauses 36% in total
c [quatres-3-2] added 2 single-self-subsuming ternary resolvents
c [quatres-3-2] added 2 quaternary resolvents
c [ternres-4] limit 8180075 with penalty 0 = 0 + 0
c [ternres-4] 24109 schedulable variables 31%
c [ternres-4] 90 ternary resolvents (0 bin, 90 trn)
c [ternres-4] fully completed ternary resolution
c [decomp-17] removed 2798 variables
c [basicprobe-3] limit 40900378 penalty 0 = 0 + 0
c [basicprobe-3-0] 22197 probes remain 30% after last round
c [basicprobe-3-0] 185 units = 185 failed (100%) + 0 lifted (0%)
c [basicprobe-3-0] removed 710 variables, found 130473 hbrs
c [bate-1] eliminated 47 asymmetric tautologies during probing
c [unhide-8] limit 818007 with penalty 1 = 0 + 1
c [unhide-8-8] 7 units, 418 failed, 17825 tauts, 0 hbrs, 67348 literals
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 161 transitive binary clauses
c [transred-4] found 4 units
c [block-3] scheduling all variables this time
c [block-3] scheduled 74452 variables 100%
c [block-3] limit of 40900378 steps penalty 1 = 1 + 0
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 28 blocked clauses
c [block-3] 28 < 1/100 * 523307 = 5233 considered unsuccessful
c [bca-4] limit of 10000000 steps and 1035466 added (scaled 2)
c [bca-4] 117264 out of 148906 literals actually usable 79%
c [bca-4] added 66 blocked clauses in 315012 steps
c [sweep-4] limit 2454022 penalty 0 = 0 + 0
c [sweep-4-1] 5024 pos 6.8% + 69326 neg 93.2% = 74350 sched 99.9% ret 102
c [sweep-4-1] 2721980 steps 36 queries 13052.56 avg class size
c [sweep-4-1] 499 decisions 27 SAT calls 184.41 avg env size
c [sweep-4-1] 73389 variables remain 99% (1043 retained 1%)
c [decomp-18] removed 116 variables
c [sweep-4-1] removed 116 vars (0 failed, 8 eqs, 15 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 116 vars in TOTAL (1 rounds, 35 queries)
c [phase-count-8] 511856 negative 99.0% of 516941 except 5085 1.0%
c [phase-count-8] 423255 positive 81.9% of 516941 except 93686 18.1%
c [phase-count-8] less non-negative clauses 5085 than limit 51600 (10.0%)
c [phase-count-8] non-pos/non-neg = 93686/5085 = 18.42 >= 2.00 = 200/100
c [lucky-phase-8] forcing lucky phase -1
c [phase-8] phase bias: 0 positive 0%, 209 negative 100%
c [sort-queue-8] sorted 43656 enqueued variables after 20115 conflicts
c [score-dist-8] active 30680 (41%), one 13619 (18%), zero 30037 (40%)
c [score-dist-8] max exp 755, different 608 (80%)
c [score-dist-8] median active exp 654, avg 562.3
c [simplification-8] removed 2162 variables 2.8% (74336 remain 26%)
c [simplification-8] removed 26469 irredundant clauses 4.9% (516941 remain 37%)
c [simplification-8] maximum reduction of 5% = max (3%, 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 32115 (soft 22115 + delta 10000)
c [simplification-8] new conflict limit 22115 (hard 32115)
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   60.7   74335   516941     20213   15521   1532 152715   37   305   63  12%      3  250   44    7  634%
c i   61.2   74284   516941     20493   15777   1540 152725   38   305   64  12%      3  249   50    7  693%
c i   61.9   74283   516941     20825   16066   1556 152738   39   318   64  12%      3  261   48    7  648%
c i   62.0   74280   516941     20909   16136   1562 152743   39   319   64  12%      2  261   41    7  552%
c i   62.3   74266   516941     21059   16261   1573 152753   38   320   64  12%      2  262   31    7  423%
c i   62.5   74264   516941     21153   16344   1574 152755   38   318   64  12%      2  259   41    8  543%
c i   62.6   74263   516941     21190   16376   1577 152756   39   319   64  12%      2  260   42    8  559%
c i   62.7   74255   516941     21282   16463   1577 152758   39   317   64  12%      2  259   40    8  530%
c i   62.8   74254   516941     21305   16480   1577 152763   38   317   64  12%      2  258   38    8  497%
c i   62.8   74008   516941     21317   16489   1577 152765   38   317   64  12%      2  258   38    8  498%
c i   62.9   74007   516941     21376   16529   1585 152773   38   316   64  12%      2  257   35    8  466%
c i   63.0   74002   516941     21446   16592   1588 152775   38   313   64  12%      1  253   34    8  447%
c i   63.4   73996   516941     21836   16933   1601 152788   39   305   64  13%      2  244   40    8  502%
c 
c [simplification-9] limit 22115 conflicts (hard 32115) hit after 22115 conflicts
c [quatres-4] found 29529 quaternary clauses 39% in total
c [ternres-5] limit 8948808 with penalty 0 = 0 + 0
c [ternres-5] all 73996 free variables schedulable
c [ternres-5] 19 ternary resolvents (0 bin, 19 trn)
c [ternres-5] 19365 variables remain 26% (54631 retained 74%)
c [decomp-19] removed 531 variables
c [simpleprobe-4] 9355 schedulable variables 13%
c [simpleprobe-4] limit 35795232 penalty 0 = 0 + 0
c [decomp-20] removed 860 variables
c [simpleprobe-4] 380 variables remain 1% (72565 retained 99%)
c [simpleprobe-4] removed 860 variables, found 45272 hbrs, 303 units
c [unhide-9] limit 894880 with penalty 1 = 0 + 1
c [unhide-9-9] 6 units, 160 failed, 11447 tauts, 0 hbrs, 49329 literals
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 190 transitive binary clauses
c [transred-5] found 3 units
c [elim-7] scheduling all variables this time
c [elim-7] scheduled 72655 variables 100%
c [elim-7] limit of 89488081 steps penalty 1 = 1 + 0
c [elim-7] rescheduling of touched variables disabled
c [elim-7-1] eliminated 2538 variables 3% in round 1 in 46033678 steps
c [elim-7-1] backward subsumption/strengthening limit 43454403
c [elim-7-1-1] backward checking 9523 touched variables 13%
c [elim-7-1-1] fully completed backward checking in 1 rounds
c [elim-7-1] subsumed 18 and strengthened 38 clauses in 3123319 steps
c [elim-7-1] rescheduled 116 variables 0% by backward subsumption
c [elim-7-2] eliminated 15 variables 0% in round 2 in 379624 steps
c [elim-7-2] backward subsumption/strengthening limit 379600
c [elim-7-2-1] backward checking 115 touched variables 0%
c [elim-7-2-1] fully completed backward checking in 1 rounds
c [elim-7-2] subsumed 9 and strengthened 7 clauses in 164853 steps
c [elim-7-2] rescheduled 26 variables 0% by backward subsumption
c [elim-7-3] eliminated 4 variables 0% in round 3 in 24661 steps
c [elim-7-3] backward subsumption/strengthening limit 24600
c [elim-7-3-1] backward checking 32 touched variables 0%
c [elim-7-3-1] incomplete backward checking 0 remain 0%
c [elim-7-3] subsumed 0 and strengthened 4 clauses in 24601 steps
c [elim-7] incomplete 15 not tried 0% in round 3
c [elim-7] transition to [ all 1 rem 1 ] state
c [elim-7] eliminated 2559 = 4% variables out of 72655 scheduled
c [bca-5] limit of 10000000 steps and 986221 added (scaled 2)
c [bca-5] 114220 out of 140194 literals actually usable 81%
c [bca-5] added 69 blocked clauses in 312124 steps
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 26846420 penalty 0 = 0 + 0
c [sweep-5-1] 4827 pos 7.0% + 64484 neg 93.0% = 69311 sched 98.9% ret 785
c [sweep-5-1] 26863819 steps 246 queries 2061.93 avg class size
c [sweep-5-1] 2334 decisions 219 SAT calls 120.58 avg env size
c [sweep-5-1] 51854 variables remain 74% (18156 retained 26%)
c [decomp-21] removed 132 variables
c [sweep-5-1] removed 132 vars (0 failed, 28 eqs, 60 impls)
c [sweep-5] considered successful since not run to completion yet
c [sweep-5] removed 132 vars in TOTAL (1 rounds, 245 queries)
c [phase-count-9] 487514 negative 99.1% of 491720 except 4206 0.9%
c [phase-count-9] 400760 positive 81.5% of 491720 except 90960 18.5%
c [phase-count-9] less non-negative clauses 4206 than limit 49100 (10.0%)
c [phase-count-9] non-pos/non-neg = 90960/4206 = 21.63 >= 2.00 = 200/100
c [lucky-phase-9] forcing lucky phase -1
c [phase-9] phase bias: 0 positive 0%, 190 negative 100%
c [sort-queue-9] sorted 38969 enqueued variables after 22115 conflicts
c [score-dist-9] active 30995 (44%), one 11326 (16%), zero 27643 (40%)
c [score-dist-9] max exp 799, different 622 (78%)
c [score-dist-9] median active exp 683, avg 594.1
c [simplification-9] removed 4032 variables 5.4% (69964 remain 24%)
c [simplification-9] removed 25221 irredundant clauses 4.9% (491720 remain 35%)
c [simplification-9] maximum reduction of 5% = max (5%, 5%)
c [simplification-9] large reduction 5% >= 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 34115 (soft 24115 + delta 10000)
c [simplification-9] new conflict limit 24115 (hard 34115)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   70.4   69963   491720     22268   11375   1487 209829   40   310   55  13%      2  247   39    8  474%
c i   70.7   69962   491720     22463   11552   1496 209836   39   309   56  13%      2  246   31    8  384%
c i   70.9   69958   491720     22588   11655   1506 209844   39   306   56  13%      2  242   28    8  338%
c i   71.0   69928   491720     22684   11736   1512 209850   38   303   56  13%      2  239   22    8  273%
c i   71.2   69927   491720     22798   11832   1520 209855   37   303   56  12%      1  239   21    8  253%
c i   71.3   69924   491720     22819   11847   1521 209857   37   303   56  12%      1  238   20    8  243%
c i   71.3   69923   491720     22826   11852   1521 209858   37   302   56  12%      1  238   20    8  238%
c i   71.5   69922   491720     22959   11967   1525 209866   37   301   56  12%      1  236   22    8  272%
c i   71.8   69921   491720     23114   12093   1538 209875   37   303   56  12%      1  237   27    8  323%
c i   72.1   69903   491720     23289   12241   1545 209891   36   300   56  12%      1  233   20    8  244%
c i   72.3   69902   491720     23412   12345   1551 209900   36   299   56  12%      1  232   25    8  298%
c i   72.3   69898   491720     23436   12365   1552 209902   36   298   56  12%      1  232   25    8  293%
c i   72.4   69892   491720     23492   12405   1558 209910   35   299   56  12%      1  232   25    8  299%
c i   72.9   69891   491720     23851   12733   1566 209921   34   292   56  12%      1  223   24    8  281%
c 
c [simplification-10] limit 24116 conflicts (hard 34115) hit after 24116 conflicts
c [ternres-6] limit 9782287 with penalty 0 = 0 + 0
c [ternres-6] 18301 schedulable variables 26%
c [ternres-6] 63 ternary resolvents (0 bin, 63 trn)
c [ternres-6] fully completed ternary resolution
c [card-4] limit 611392 penalty 3 = 3 + 0
c [card-4] found 1602 at-most-one constraints of average size 4.1
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 611392 for elimination
c [card-4] 1602 out of 1602 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [gauss-3] limit 500000 penalty 2 = 2 + 0
c [gauss-3] extracted 7 xors of average arity 2.7
c [gauss-3] connected 19 occurrences of 17 variables (average 1.1)
c [gauss-3] limit 500000 penalty 2 = 2 + 0
c [gauss-3] fully completed
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-22] removed 12 variables
c [treelook-4] limit 978228 penalty 0 = 0 + 0 boost 1
c [treelook-4] scheduled 94649 literals 68%
c [treelook-4] scheduling used 978238 steps
c [treelook-4] not fully scheduled
c [treelook-4] limit 978228 penalty 0 = 0 + 0 boost 1
c [treelook-4] used 1124173 steps
c [treelook-4] 94632 literals remain 68%
c [treelook-4] 22593 variables remain to probed next time 32%
c [treelook-4] removed 0 variables, found 2041 hbrs
c [unhide-10] limit 1956457 with penalty 0 = 0 + 0
c [unhide-10-10] 7 units, 384 failed, 19721 tauts, 0 hbrs, 20259 literals
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 212 transitive binary clauses
c [transred-6] found 7 units
c [cce-3] limit of 12227859 steps penalty 2 = 2 + 0
c [cce-3-1] eliminated 5 clauses out of 966 (1%) of length 9
c [cce-3-1] eliminated 4 clauses out of 436 (1%) of length 8
c [cce-3-1] eliminated 2 clauses out of 1662 (0%) of length 7
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 11 large clauses in 12227867 steps
c [cce-3-1] allowing another 6113933 steps for small clauses
c [cce-3-1] scheduling 340025 clauses = 236467 binary + 103558 ternary
c [cce-3-1] tried to eliminate 125 small clauses 0%
c [cce-3-1] eliminated 30 binary clauses 0%
c [cce-3-1] eliminated 6 ternary clauses 0%
c [cce-3-1] eliminated 36 small clauses 0%
c [cce-3-1] eliminated 3604 small clauses in 12227859 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 3615 covered clauses in round 1
c [cce-3] eliminated 3615 covered clauses in TOTAL during 1 rounds
c [cce-3] 3615 < 1/100 * 491132 = 4911 considered unsuccessful
c [elim-8] no untried remaining variables left
c [elim-8] scheduled 69380 variables 100%
c [elim-8] boosting limit by 20
c [elim-8] limit of 3912914880 steps penalty 0 = 0 + 0
c [elim-8] rescheduling of touched variables disabled
c [elim-8-1] eliminated 645 variables 1% in round 1 in 45047264 steps
c [elim-8-1] backward subsumption/strengthening limit 45047200
c [elim-8-1-1] backward checking 2334 touched variables 3%
c [elim-8-1-1] fully completed backward checking in 1 rounds
c [elim-8-1] subsumed 10 and strengthened 9 clauses in 889409 steps
c [elim-8-1] rescheduled 48 variables 0% by backward subsumption
c [elim-8-2] eliminated 4 variables 0% in round 2 in 56538 steps
c [elim-8-2] backward subsumption/strengthening limit 56500
c [elim-8-2-1] backward checking 40 touched variables 0%
c [elim-8-2-1] incomplete backward checking 0 remain 0%
c [elim-8-2] subsumed 3 and strengthened 8 clauses in 56501 steps
c [elim-8-2] rescheduled 16 variables 0% by backward subsumption
c [elim-8-3] eliminated 2 variables 0% in round 3 in 18227 steps
c [elim-8-3] backward subsumption/strengthening limit 18200
c [elim-8-3-1] backward checking 18 touched variables 0%
c [elim-8-3-1] incomplete backward checking 0 remain 0%
c [elim-8-3] subsumed 0 and strengthened 2 clauses in 18201 steps
c [elim-8] incomplete 8 not tried 0% in round 3
c [elim-8] transition to [ all 1 rem 1 ] state
c [elim-8] eliminated 651 = 1% variables out of 69380 scheduled
c [elim-8] 651 < 1/100 * 69380 = 693 considered unsuccessful
c [bca-6] limit of 10000000 steps and 971752 added (scaled 2)
c [bca-6] 110543 out of 137460 literals actually usable 80%
c [bca-6] added 103 blocked clauses in 301347 steps
c [sweep-6] limit 2934686 penalty 0 = 0 + 0
c [sweep-6-1] 4565 pos 8.9% + 46516 neg 91.1% = 51081 sched 74.3% ret 17648
c [sweep-6-1] 3066920 steps 36 queries 6652.86 avg class size
c [sweep-6-1] 373 decisions 31 SAT calls 126.55 avg env size
c [sweep-6-1] 50790 variables remain 74% (17936 retained 26%)
c [decomp-24] removed 25 variables
c [sweep-6-1] removed 25 vars (0 failed, 4 eqs, 9 impls)
c [sweep-6] considered successful since not run to completion yet
c [sweep-6] removed 25 vars in TOTAL (1 rounds, 35 queries)
c [phase-count-10] 481234 negative 99.1% of 485417 except 4183 0.9%
c [phase-count-10] 395162 positive 81.4% of 485417 except 90255 18.6%
c [phase-count-10] less non-negative clauses 4183 than limit 48500 (10.0%)
c [phase-count-10] non-pos/non-neg = 90255/4183 = 21.58 >= 2.00 = 200/100
c [lucky-phase-10] forcing lucky phase -1
c [phase-10] phase bias: 0 positive 0%, 137 negative 100%
c [sort-queue-10] sorted 38432 enqueued variables after 24116 conflicts
c [score-dist-10] active 30272 (44%), one 11630 (17%), zero 26802 (39%)
c [score-dist-10] max exp 824, different 700 (85%)
c [score-dist-10] median active exp 745, avg 638.4
c [simplification-10] removed 1187 variables 1.7% (68704 remain 24%)
c [simplification-10] removed 6303 irredundant clauses 1.3% (485417 remain 35%)
c [simplification-10] maximum reduction of 2% = max (2%, 1%)
c [simplification-10] geometric conflict interval increment 6666 = 20000 / 3
c [simplification-10] new conflict interval 16666
c [simplification-10] penalized conflict interval 16666 = 1 * 16666
c [simplification-10] hard conflict limit 50782 (soft 40782 + delta 10000)
c [simplification-10] new conflict limit 40782 (hard 50782)
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.5   68703   485417     24515   12893   1570 190882   34   292   56  11%      3  221   30    9  343%
c i   78.6   68693   485417     24578   12947   1574 190884   33   293   56  11%      3  222   29    9  337%
c i   78.6   68673   485417     24579   12947   1574 190884   33   293   56  11%      3  222   29    9  336%
c i   78.7   68664   485417     24615   12972   1578 190889   33   292   56  11%      3  221   27    9  313%
c i   79.9   68489   485417     25414   13682   1614 190921   35   296   56  12%      5  223   36    9  395%
c i   80.0   68488   485417     25496   13739   1619 190937   35   300   56  12%      4  226   38    9  415%
c i   80.3   68473   485417     25625   13847   1625 190946   34   297   56  11%      4  223   28    9  303%
c i   80.4   68472   485417     25754   13961   1628 190949   34   296   56  12%      3  221   32    9  348%
c i   81.1   68465   485417     26094   14262   1641 190970   34   300   56  11%      3  224   30    9  323%
c i   81.6   68459   485417     26463   14599   1648 190977   35   306   56  11%      3  229   46   10  480%
c i   82.4   68456   485417     26860   14952   1665 190992   36   306   56  12%      3  227   47   10  486%
c i   82.9   68454   485417     27146   15203   1681 191002   36   313   56  11%      2  233   42   10  432%
c i   83.1   68449   485417     27264   15310   1686 191002   37   314   56  12%      2  234   55   10  553%
c i   83.2   68448   485417     27319   15358   1689 191003   37   315   56  12%      2  235   51   10  515%
c i   83.5   68447   485417     27574   15590   1694 191008   38   315   56  12%      2  234   52   10  517%
c i   83.6   68441   485417     27625   15637   1695 191009   38   316   56  12%      2  235   54   10  529%
c i   83.6   68437   485417     27629   15639   1695 191010   38   316   56  12%      2  235   53   10  523%
c i   84.5   68436   485417     28166   16106   1729 191026   39   327   57  12%      3  244   45   10  427%
c i   85.1   68432   485417     28613   16493   1745 191047   39   319   58  12%      3  234   38   11  357%
c i   87.1   68428   485417     29755   17513   1796 191092   40   339   60  12%      7  250   35   11  317%
c i   88.1   68419   485417     30395   18099   1818 191117   40   340   60  12%      6  249   38   11  330%
c i   88.6   68415   485417     30686   18343   1834 191141   39   338   60  12%      5  246   34   12  291%
c i   90.1   68209   485417     31441   19027   1867 191165   39   353   61  11%      5  258   37   12  314%
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.5   68207   485417     31751   19305   1880 191170   40   355   61  11%      4  259   41   12  340%
c i   90.6   68196   485417     31797   19345   1882 191173   39   355   61  11%      4  259   38   12  317%
c i   90.6   68195   485417     31840   19384   1883 191175   39   352   61  11%      4  255   35   12  289%
c i   91.4   68194   485417     32310   19809   1903 191188   39   352   61  11%      3  254   32   12  260%
c i   91.5   68177   485417     32331   19827   1904 191189   39   352   61  11%      3  253   33   12  271%
c i   91.5   68173   485417     32332   19827   1904 191189   39   352   61  11%      3  253   33   12  270%
c i   91.5   68170   485417     32333   19827   1904 191189   39   352   61  11%      3  253   33   12  269%
c i   91.5   68168   485417     32334   19827   1904 191189   39   352   61  11%      3  253   33   12  268%
c i   92.6   68164   485417     32929   20365   1923 191205   42   365   61  11%      4  264   54   13  428%
c i   93.3   68160   485417     33327   20710   1940 191224   43   375   62  11%      3  273   54   13  416%
c i   93.3   68159   485417     33382   20758   1941 191227   43   372   62  12%      3  269   49   13  381%
c i   93.5   68117   485417     33439   20805   1942 191232   43   372   62  11%      3  269   45   13  348%
c i   93.9   68114   485417     33653   20997   1948 191238   45   374   62  12%      2  270   67   13  508%
c i   95.1   68113   485417     34432   21675   1985 191272   44   373   62  12%      4  265   41   13  305%
c i   95.3   68112   485417     34531   21758   1989 191276   44   374   62  12%      4  266   42   14  309%
c i   96.1   68103   485417     35001   22187   2010 191289   44   377   64  12%      3  268   42   14  303%
c i   96.3   68102   485417     35139   22315   2012 191292   44   378   65  12%      3  267   47   14  339%
c i   96.5   68100   485417     35226   22391   2016 191296   44   376   65  12%      3  266   46   14  329%
c i   98.9   68099   485417     36730   23743   2068 191346   44   364   66  12%     11  248   43   15  295%
c i   99.5   68093   485417     37040   24020   2081 191356   44   362   66  12%      8  244   42   15  289%
c i  100.3   68088   485417     37536   24474   2099 191366   46   366   70  13%      6  247   53   15  355%
c i  100.5   68087   485417     37685   24604   2106 191373   46   363   70  13%      5  243   44   15  290%
c i  100.6   68085   485417     37744   24659   2107 191373   45   362   70  13%      5  242   42   15  280%
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i  101.3   68071   485417     38142   25015   2126 191386   45   361   70  12%      4  239   37   15  245%
c i  101.4   68067   485417     38169   25040   2126 191387   45   362   70  12%      4  240   37   15  242%
c i  101.9   68066   485417     38434   25273   2135 191404   44   361   70  12%      3  238   32   15  208%
c i  102.7   68065   485417     38946   25730   2147 191419   45   362   70  13%      3  237   50   16  322%
c i  103.0   68064   485417     39067   25832   2155 191424   45   359   70  12%      3  234   42   16  269%
c i  104.9   68063   485417     40100   26773   2187 191451   48   376   71  13%      6  247   68   16  418%
c i  105.2   68062   485417     40261   26901   2200 191463   47   375   71  13%      5  246   50   16  304%
c i  105.4   67994   485417     40387   27019   2204 191465   47   373   71  13%      4  243   43   16  261%
c 
c [simplification-11] limit 40824 conflicts (hard 50782) hit after 40824 conflicts
c [quatres-5] found 28304 quaternary clauses 40% in total
c [quatres-5-2] added 4 single-self-subsuming ternary resolvents
c [quatres-5-2] added 20 quaternary resolvents
c [ternres-7] limit 16423861 with penalty 0 = 0 + 0
c [ternres-7] all 67994 free variables schedulable
c [ternres-7] 176 ternary resolvents (0 bin, 176 trn)
c [ternres-7] fully completed ternary resolution
c [decomp-25] removed 835 variables
c [basicprobe-4] limit 82119306 penalty 0 = 0 + 0
c [basicprobe-4-0] 17915 probes remain 27% after last round
c [basicprobe-4-0] 447 units = 444 failed (99%) + 3 lifted (1%)
c [basicprobe-4-0] removed 1192 variables, found 210343 hbrs
c [bate-2] eliminated 159 asymmetric tautologies during probing
c [unhide-11] limit 1642386 with penalty 1 = 0 + 1
c [unhide-11-11] 5 units, 117 failed, 8821 tauts, 0 hbrs, 135738 literals
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 160 transitive binary clauses
c [transred-7] found 3 units
c [block-4] scheduling all variables this time
c [block-4] scheduled 66440 variables 100%
c [block-4] limit of 41059653 steps penalty 2 = 2 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 265 blocked clauses
c [block-4] 265 < 1/100 * 467429 = 4674 considered unsuccessful
c [bca-7] limit of 10000000 steps and 931039 added (scaled 2)
c [bca-7] 97179 out of 132882 literals actually usable 73%
c [bca-7] added 56 blocked clauses in 269547 steps
c [sweep-7] limit 4927158 penalty 0 = 0 + 0
c [sweep-7-1] 4714 pos 9.5% + 44657 neg 90.5% = 49371 sched 74.3% ret 17069
c [sweep-7-1] 4971637 steps 56 queries 4259.16 avg class size
c [sweep-7-1] 1164 decisions 45 SAT calls 303.07 avg env size
c [sweep-7-1] 48706 variables remain 73% (17729 retained 27%)
c [decomp-26] removed 112 variables
c [sweep-7-1] removed 112 vars (0 failed, 10 eqs, 21 impls)
c [sweep-7] removed 112 vars in TOTAL (1 rounds, 55 queries)
c [phase-count-11] 460719 negative 99.1% of 464902 except 4183 0.9%
c [phase-count-11] 378543 positive 81.4% of 464902 except 86359 18.6%
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 35465 enqueued variables after 40824 conflicts
c [score-dist-11] active 30863 (47%), one 12262 (18%), zero 23203 (35%)
c [score-dist-11] max exp 707, different 650 (92%)
c [score-dist-11] median active exp 611, avg 551.2
c [simplification-11] removed 1666 variables 2.5% (66328 remain 23%)
c [simplification-11] removed 20515 irredundant clauses 4.2% (464902 remain 34%)
c [simplification-11] maximum reduction of 4% = max (2%, 4%)
c [simplification-11] geometric conflict interval increment 4000 = 20000 / 5
c [simplification-11] new conflict interval 20666
c [simplification-11] penalized conflict interval 20666 = 1 * 20666
c [simplification-11] hard conflict limit 71823 (soft 61490 + delta 10333)
c [simplification-11] new conflict limit 61490 (hard 71823)
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  115.9   66327   464902     41638   28022   2431 391092   49   372   81  13%      8  238   49   17  285%
c i  116.5   66293   464902     41962   28297   2449 391105   50   372   81  13%      6  237   54   17  313%
c i  118.0   66292   464902     42903   29157   2471 391121   52   377   81  14%      6  238   61   18  338%
c i  118.4   66290   464902     43045   29282   2481 391126   52   381   81  14%      6  241   54   18  297%
c i  119.7   66289   464902     43701   29855   2518 391147   52   390   81  13%      5  248   66   18  359%
c i  120.3   66280   464902     44013   30130   2529 391150   54   386   81  14%      4  243   78   19  421%
c i  122.5   66264   464902     45132   31146   2558 391188   56   401   81  14%      7  253   55   19  285%
c i  123.0   66263   464902     45512   31506   2561 391195   56   392   81  14%      5  243   62   20  315%
c i  124.5   66254   464902     46293   32211   2578 391214   57   390   81  15%      5  239   54   20  269%
c i  124.7   66253   464902     46400   32312   2581 391214   58   400   81  14%      4  248   62   20  306%
c i  124.8   66007   464902     46440   32347   2582 391215   57   399   81  14%      4  247   57   20  281%
c i  124.8   66001   464902     46441   32347   2582 391215   57   399   81  14%      4  247   57   20  280%
c i  126.0   65973   464902     47015   32862   2603 391238   58   403   81  14%      4  249   70   21  341%
c i  126.2   65967   464902     47112   32952   2605 391238   58   405   81  14%      3  250   73   21  355%
c i  127.3   65962   464902     47767   33549   2625 391251   57   392   81  15%      3  235   56   21  266%
c i  127.5   65961   464902     47864   33643   2625 391252   57   397   81  14%      3  240   57   21  271%
c i  127.6   65959   464902     47866   33644   2625 391252   57   397   81  14%      3  240   57   21  272%
c i  127.8   65958   464902     48007   33760   2633 391267   56   396   81  14%      2  238   44   21  210%
c i  129.3   65955   464902     48830   34488   2662 391294   57   393   81  15%      4  232   68   21  316%
c i  129.5   65954   464902     48909   34562   2662 391295   58   397   81  15%      3  236   76   22  350%
c i  132.2   65953   464902     50398   35899   2713 391333   62   408   83  15%     10  241   50   23  220%
c i  132.8   65952   464902     50813   36285   2722 391339   62   417   83  15%      7  249   64   23  279%
c i  132.9   65950   464902     50958   36418   2725 391341   61   412   83  15%      6  244   52   23  226%
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  134.2   65949   464902     51856   37234   2739 391356   67   435   84  15%      6  263   80   24  335%
c i  136.0   65948   464902     53275   38497   2773 391388   71   446   85  16%     10  268   72   25  286%
c i  140.1   65947   464902     56020   40968   2841 391448   74   474   90  16%     26  284   80   27  294%
c i  140.5   65946   464902     56278   41214   2844 391450   73   472   93  16%     20  281   68   27  248%
c i  141.1   65942   464902     56671   41546   2857 391462   76   478   97  16%     13  285   90   28  323%
c i  141.5   65941   464902     56965   41825   2862 391466   75   485   97  15%     10  291   72   28  256%
c i  141.7   65940   464902     57097   41947   2864 391467   74   481   97  15%      8  286   64   28  228%
c i  142.0   65939   464902     57291   42129   2869 391468   75   485   97  15%      7  289   75   28  267%
c i  145.3   65938   464902     59272   43950   2907 391508   78   516   97  15%     15  311   70   30  235%
c i  145.5   65937   464902     59422   44069   2911 391515   79   511   97  16%     13  306   86   30  288%
c i  146.6   65936   464902     60113   44706   2922 391529   79   522  101  15%      8  314   69   31  226%
c 
c [simplification-12] limit 61505 conflicts (hard 71823) hit after 61505 conflicts
c [quatres-6] found 28987 quaternary clauses 42% in total
c [quatres-6-1] removed 1 duplicate quaternary clauses
c [quatres-6-2] added 2 quaternary resolvents
c [ternres-8] limit 23711416 with penalty 0 = 0 + 0
c [ternres-8] all 65936 free variables schedulable
c [ternres-8] 23 ternary resolvents (1 bin, 22 trn)
c [ternres-8] fully completed ternary resolution
c [decomp-27] removed 500 variables
c [simpleprobe-5] 335 schedulable variables 1%
c [simpleprobe-5] limit 94845665 penalty 0 = 0 + 0
c [decomp-28] removed 328 variables
c [simpleprobe-5] fully completed simple probing
c [simpleprobe-5] removed 328 variables, found 18886 hbrs, 135 units
c [unhide-12] limit 1185570 with penalty 2 = 0 + 2
c [unhide-12-12] 7 units, 467 failed, 45418 tauts, 0 hbrs, 326200 literals
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 162 transitive binary clauses
c [transred-8] found 6 units
c [elim-9] no untried remaining variables left
c [elim-9] scheduled 65125 variables 100%
c [elim-9] limit of 237114164 steps penalty 1 = 1 + 0
c [elim-9] rescheduling of touched variables disabled
c [elim-9-1] eliminated 1554 variables 2% in round 1 in 44395589 steps
c [elim-9-1] backward subsumption/strengthening limit 44395500
c [elim-9-1-1] backward checking 5598 touched variables 9%
c [elim-9-1-1] fully completed backward checking in 1 rounds
c [elim-9-1] subsumed 21 and strengthened 74 clauses in 2108126 steps
c [elim-9-1] rescheduled 195 variables 0% by backward subsumption
c [elim-9-2] eliminated 20 variables 0% in round 2 in 2464868 steps
c [elim-9-2] backward subsumption/strengthening limit 2464800
c [elim-9-2-1] backward checking 189 touched variables 0%
c [elim-9-2-1] fully completed backward checking in 1 rounds
c [elim-9-2] subsumed 5 and strengthened 5 clauses in 258273 steps
c [elim-9-2] rescheduled 30 variables 0% by backward subsumption
c [elim-9-3] eliminated 2 variables 0% in round 3 in 29055 steps
c [elim-9-3] backward subsumption/strengthening limit 29000
c [elim-9-3-1] backward checking 25 touched variables 0%
c [elim-9-3-1] incomplete backward checking 0 remain 0%
c [elim-9-3] subsumed 0 and strengthened 4 clauses in 29001 steps
c [elim-9] incomplete 16 not tried 0% in round 3
c [elim-9] transition to [ all 1 rem 1 ] state
c [elim-9] eliminated 1580 = 2% variables out of 65125 scheduled
c [bca-8] limit of 10000000 steps and 903993 added (scaled 2)
c [bca-8] 91968 out of 127092 literals actually usable 72%
c [bca-8] added 104 blocked clauses in 261125 steps
c [sweep-8] limit 7113424 penalty 0 = 0 + 0
c [sweep-8-1] 4595 pos 9.8% + 42304 neg 90.2% = 46899 sched 73.8% ret 16646
c [sweep-8-1] 7223078 steps 88 queries 3135.98 avg class size
c [sweep-8-1] 1817 decisions 81 SAT calls 246.93 avg env size
c [sweep-8-1] 45210 variables remain 71% (18335 retained 29%)
c [decomp-29] removed 15 variables
c [sweep-8-1] removed 15 vars (0 failed, 7 eqs, 16 impls)
c [sweep-8] 15 < 1/1000 * 63545 = 63 considered unsuccessful
c [sweep-8] removed 15 vars in TOTAL (1 rounds, 87 queries)
c [phase-count-12] 447556 negative 99.1% of 451515 except 3959 0.9%
c [phase-count-12] 366675 positive 81.2% of 451515 except 84840 18.8%
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 33554 enqueued variables after 61505 conflicts
c [score-dist-12] active 29976 (47%), one 12605 (20%), zero 20949 (33%)
c [score-dist-12] max exp 635, different 558 (88%)
c [score-dist-12] median active exp 561, avg 492.9
c [simplification-12] removed 2406 variables 3.6% (63530 remain 22%)
c [simplification-12] removed 13387 irredundant clauses 2.9% (451515 remain 33%)
c [simplification-12] maximum reduction of 4% = max (4%, 3%)
c [simplification-12] geometric conflict interval increment 4133 = 20666 / 5
c [simplification-12] new conflict interval 24799
c [simplification-12] penalized conflict interval 24799 = 1 * 24799
c [simplification-12] hard conflict limit 98703 (soft 86304 + delta 12399)
c [simplification-12] new conflict limit 86304 (hard 98703)
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  157.1   63529   451515     62656   31712   2795 356251   73   497   79  15%     22  277   47   32  146%
c i  158.0   63528   451515     63123   32138   2803 356255   75   506   79  15%     14  284   83   32  256%
c i  158.1   63524   451515     63220   32220   2809 356263   74   504   79  15%     12  282   69   32  214%
c i  158.3   63523   451515     63311   32306   2811 356265   73   506   79  14%     11  283   63   32  195%
c i  158.4   63522   451515     63362   32352   2813 356267   73   506   79  14%     10  283   58   32  178%
c i  159.2   63521   451515     63933   32852   2825 356271   77   514   79  15%      6  289   88   33  266%
c i  161.1   63520   451515     65265   34096   2855 356297   73   524   79  14%      8  293   61   34  182%
c i  162.2   63519   451515     66071   34828   2865 356313   77   524   79  15%      5  289   92   34  267%
c i  162.3   63517   451515     66138   34889   2865 356316   77   525   79  15%      4  290   87   34  254%
c i  162.4   63516   451515     66192   34937   2867 356318   76   524   79  15%      4  289   77   34  224%
c i  162.4   63515   451515     66193   34937   2867 356318   76   524   79  15%      4  289   77   34  224%
c i  163.7   63514   451515     67250   35899   2885 356342   74   522   79  14%      5  282   62   35  177%
c i  163.7   63508   451515     67251   35899   2885 356342   74   521   79  14%      5  282   62   35  177%
c i  163.7   63497   451515     67252   35899   2885 356342   74   521   79  14%      5  282   61   35  176%
c i  168.0   63438   451515     70336   38727   2942 356396   78   529   83  15%     28  277   74   37  200%
c i  168.1   63437   451515     70403   38786   2947 356398   78   527   83  15%     26  275   64   37  173%
c i  169.7   63436   451515     71902   40130   2966 356418   78   478   86  16%     13  220   81   38  214%
c i  170.5   63428   451515     72509   40683   2982 356429   79   480   91  16%      7  220   83   38  215%
c i  170.5   63427   451515     72510   40683   2982 356429   79   480   91  16%      7  220   82   38  214%
c i  170.5   63425   451515     72513   40685   2982 356429   79   480   91  16%      7  220   81   38  212%
c i  170.7   63424   451515     72672   40825   2988 356429   78   467   91  17%      5  207   68   38  176%
c i  171.8   63423   451515     73442   41533   3015 356446   75   480   91  16%      3  217   51   39  133%
c i  172.4   63422   451515     73900   41957   3025 356454   73   481   94  15%      1  217   58   39  149%
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  174.6   63421   451515     75480   43419   3053 356480   79   498   94  16%      8  228  124   40  311%
c i  174.9   63420   451515     75633   43550   3056 356481   82   502   94  16%      6  232  137   40  340%
c i  175.4   63419   451515     75951   43843   3066 356485   81   508   97  16%      4  236   93   40  230%
c i  176.3   63411   451515     76622   44477   3077 356488   81   519   97  16%      2  245   66   41  162%
c i  179.0   63410   451515     78390   46102   3139 356520   73   529   97  14%     10  249   58   41  141%
c i  181.1   63409   451515     79883   47452   3170 356538   77   527   97  15%      9  241  108   42  254%
c i  186.1   63408   451515     83290   50568   3216 356577   89   547  105  16%     32  248   64   45  141%
c i  186.5   63407   451515     83570   50817   3221 356584   89   534  105  17%     23  234   72   45  159%
c i  189.2   63390   451515     85420   52517   3251 356608   87   525  133  17%     13  218   89   46  191%
c 
c [simplification-13] limit 86347 conflicts (hard 98703) hit after 86349 conflicts
c [quatres-7] found 29266 quaternary clauses 43% in total
c [quatres-7-1] removed 2 duplicate quaternary clauses
c [quatres-7-1] added 1 double-self-subsuming ternary resolvents
c [quatres-7-2] added 1 single-self-subsuming ternary resolvents
c [quatres-7-2] added 3 quaternary resolvents
c [ternres-9] limit 31171956 with penalty 0 = 0 + 0
c [ternres-9] all 63379 free variables schedulable
c [ternres-9] 212 ternary resolvents (0 bin, 212 trn)
c [ternres-9] fully completed ternary resolution
c [decomp-30] removed 162 variables
c [unhide-13] limit 1558597 with penalty 2 = 0 + 2
c [unhide-13-13] 3 units, 93 failed, 5706 tauts, 0 hbrs, 652503 literals
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 188 transitive binary clauses
c [transred-9] found 3 units
c [elim-10] no untried remaining variables left
c [elim-10] scheduled 63224 variables 100%
c [elim-10] limit of 623439136 steps penalty 0 = 0 + 0
c [elim-10] rescheduling of touched variables disabled
c [elim-10-1] eliminated 219 variables 0% in round 1 in 42616139 steps
c [elim-10-1] backward subsumption/strengthening limit 42616100
c [elim-10-1-1] backward checking 1400 touched variables 2%
c [elim-10-1-1] fully completed backward checking in 1 rounds
c [elim-10-1] subsumed 14 and strengthened 19 clauses in 689721 steps
c [elim-10-1] rescheduled 41 variables 0% by backward subsumption
c [elim-10-2] eliminated 2 variables 0% in round 2 in 989940 steps
c [elim-10-2] backward subsumption/strengthening limit 989900
c [elim-10-2-1] backward checking 17 touched variables 0%
c [elim-10-2-1] fully completed backward checking in 1 rounds
c [elim-10-2] subsumed 0 and strengthened 0 clauses in 72883 steps
c [elim-10] fully completed in 2 rounds
c [elim-10] transition to [ all 0 rem 0 ] state
c [elim-10] eliminated 224 = 0% variables out of 63224 scheduled
c [elim-10] 224 < 1/100 * 63224 = 632 considered unsuccessful
c [bca-9] limit of 10000000 steps and 890097 added (scaled 2)
c [bca-9] 85155 out of 126002 literals actually usable 68%
c [bca-9] added 39 blocked clauses in 255594 steps
c [phase-count-13] 440643 negative 99.1% of 444578 except 3935 0.9%
c [phase-count-13] 361267 positive 81.3% of 444578 except 83311 18.7%
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 31749 enqueued variables after 86349 conflicts
c [score-dist-13] active 31251 (50%), one 12665 (20%), zero 19084 (30%)
c [score-dist-13] max exp 647, different 589 (91%)
c [score-dist-13] median active exp 541, avg 486.7
c [simplification-13] removed 379 variables 0.6% (63000 remain 22%)
c [simplification-13] removed 6937 irredundant clauses 1.5% (444578 remain 32%)
c [simplification-13] maximum reduction of 2% = max (1%, 2%)
c [simplification-13] geometric conflict interval increment 8266 = 24799 / 3
c [simplification-13] new conflict interval 33065
c [simplification-13] penalized conflict interval 33065 = 1 * 33065
c [simplification-13] hard conflict limit 135946 (soft 119414 + delta 16532)
c [simplification-13] new conflict limit 119414 (hard 135946)
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  196.2   62999   444578     86386   46682   3395 351003   84   516  104  16%      6  207   70   47  150%
c i  196.6   62993   444578     86645   46916   3399 351005   84   514  107  16%      4  203   74   47  159%
c i  203.5   62992   444578     91490   51351   3471 351095   82   492  107  17%     51  168   85   49  174%
c i  204.3   62991   444578     92044   51864   3477 351104   84   508  107  17%     28  183   89   50  180%
c i  206.1   62990   444578     93298   52969   3497 351122   89   505  108  18%     10  176  147   51  291%
c i  206.1   62980   444578     93299   52969   3497 351122   89   505  108  18%     10  176  147   51  289%
c i  207.1   62890   444578     93933   53560   3508 351138   83   487  108  17%      3  156   52   51  103%
c i  208.9   62889   444578     95293   54796   3521 351151   84   471  108  18%      3  137   79   51  153%
c i  210.0   62888   444578     95985   55438   3531 351164   83   482  108  17%      0  147   75   52  145%
c i  212.5   62887   444578     97563   56880   3559 351192   87   512  108  17%      5  173   96   53  183%
c -  212.6   62887   444578     97630   18161   3560 351192   86   512   55  17%      4  173   82   53  157%
c i  213.5   62886   444578     98432   18884   3585 351210   81   507   59  16%      1  166   61   53  117%
c i  217.3   62882   444578    101669   21882   3628 351252   80   508   64  16%     26  160   87   54  161%
c i  218.7   62881   444578    103058   23131   3663 351272   75   494   67  15%      9  142   46   54   85%
c i  219.2   62880   444578    103635   23668   3668 351275   74   497   68  15%      3  144   75   54  138%
c i  219.5   62879   444578    103825   23845   3672 351277   74   497   68  15%      1  144   72   54  133%
c i  219.5   62878   444578    103826   23845   3672 351277   74   497   68  15%      1  144   72   54  133%
c i  219.6   62877   444578    103863   23878   3672 351279   74   496   68  15%      0  143   71   54  131%
c i  222.3   62876   444578    105869   25737   3699 351300   76   516   71  15%      9  158   72   55  131%
c i  225.1   62875   444578    108062   27796   3738 351326   78   520  103  15%     12  157   69   56  124%
c i  225.6   62874   444578    108393   28098   3743 351332   78   524  107  15%      7  160   80   56  143%
c i  225.7   62873   444578    108426   28130   3743 351332   78   525  107  15%      6  161   75   56  135%
c i  225.7   62872   444578    108429   28131   3743 351333   78   525  107  15%      6  161   75   56  134%
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  228.1   62869   444578    110164   29723   3774 351350   81   538  110  15%      7  170   71   57  125%
c i  229.1   62868   444578    111106   30587   3783 351366   82   506  110  16%      1  136   83   57  146%
c i  229.4   62867   444578    111307   30777   3786 351370   80   509  110  16%     -0  138   69   57  121%
c i  230.9   62865   444578    112745   32038   3815 351399   77   502  110  15%      2  128   62   57  108%
c i  231.0   62864   444578    112900   32184   3815 351400   75   493  110  15%      1  119   45   57   78%
c i  231.3   62863   444578    113204   32464   3819 351405   75   492  110  15%     -1  117   68   57  119%
c i  232.4   62840   444578    114021   33211   3831 351419   76   496  115  15%     -2  120   67   58  117%
c i  234.5   62839   444578    115588   34656   3853 351442   77   500  118  15%      3  121   63   58  108%
c i  235.6   62838   444578    116548   35558   3861 351450   74   490  118  15%      0  109   57   58   99%
c i  236.3   62837   444578    117125   36103   3864 351454   74   501  122  15%     -2  119   66   58  113%
c i  237.6   62833   444578    117936   36869   3872 351463   76   521  125  15%     -3  138   85   59  145%
c i  237.8   62832   444578    118102   37024   3876 351466   76   526  125  14%     -4  142   86   59  147%
c 
c [simplification-14] limit 119437 conflicts (hard 135946) hit after 119439 conflicts
c [quatres-8] found 29279 quaternary clauses 43% in total
c [quatres-8-2] added 1 quaternary resolvents
c [ternres-10] limit 40193895 with penalty 0 = 0 + 0
c [ternres-10] all 62832 free variables schedulable
c [ternres-10] 94 ternary resolvents (1 bin, 93 trn)
c [ternres-10] fully completed ternary resolution
c [gauss-4] limit 1004847 penalty 3 = 3 + 0
c [gauss-4] extracted 14 xors of average arity 2.9
c [gauss-4] connected 40 occurrences of 40 variables (average 1.0)
c [gauss-4] limit 1004847 penalty 3 = 3 + 0
c [gauss-4] fully completed
c [gauss-4] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-31] removed 15 variables
c [treelook-5] limit 2009694 penalty 1 = 1 + 0 boost 1
c [treelook-5] scheduled 109274 literals 87%
c [treelook-5] scheduling used 1896974 steps
c [treelook-5] scheduled completely
c [treelook-5] limit 2009694 penalty 1 = 1 + 0 boost 1
c [treelook-5] used 2011235 steps
c [treelook-5] 109208 literals remain 87%
c [treelook-5] 19042 variables remain to probed next time 30%
c [decomp-32] removed 1 variables
c [treelook-5] removed 11 variables, found 6015 hbrs
c [unhide-14] limit 2009694 with penalty 2 = 0 + 2
c [unhide-14-14] 6 units, 270 failed, 19922 tauts, 0 hbrs, 398059 literals
c [transred-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 204 transitive binary clauses
c [transred-10] found 6 units
c [cce-4] boosting limit by 10
c [cce-4] limit of 251211843 steps penalty 3 = 3 + 0
c [cce-4-1] eliminated 4 clauses out of 635 (1%) of length 9
c [cce-4-1] eliminated 9 clauses out of 442 (2%) of length 8
c [cce-4-1] eliminated 588 clauses out of 1202 (49%) of length 7
c [cce-4-1] eliminated 2881 clauses out of 5425 (53%) of length 6
c [cce-4-1] eliminated 17410 clauses out of 26133 (67%) of length 5
c [cce-4-1] incomplete large round (ATE)
c [cce-4-1] eliminated 20892 large clauses in 251211845 steps
c [cce-4-1] allowing another 125605922 steps for small clauses
c [cce-4-1] scheduling 284507 clauses = 214301 binary + 70206 ternary
c [cce-4-1] tried to eliminate 4028 small clauses 1%
c [cce-4-1] eliminated 885 binary clauses 0%
c [cce-4-1] eliminated 196 ternary clauses 0%
c [cce-4-1] eliminated 1081 small clauses 0%
c [cce-4-1] eliminated 3231 small clauses in 251211844 steps
c [cce-4-1] incomplete small round (ATE)
c [cce-4-1] eliminated 24123 covered clauses in round 1
c [cce-4] eliminated 24123 covered clauses in TOTAL during 1 rounds
c [bca-10] limit of 10000000 steps and 838953 added (scaled 2)
c [bca-10] 84742 out of 124852 literals actually usable 68%
c [bca-10] added 45 blocked clauses in 226257 steps
c [sweep-9] limit 6029084 penalty 1 = 1 + 0
c [sweep-9-1] 4211 pos 9.4% + 40377 neg 90.6% = 44588 sched 71.4% ret 17837
c [sweep-9-1] 6036230 steps 89 queries 4660.49 avg class size
c [sweep-9-1] 1361 decisions 81 SAT calls 228.62 avg env size
c [sweep-9-1] 43085 variables remain 69% (19335 retained 31%)
c [decomp-33] removed 16 variables
c [sweep-9-1] removed 16 vars (0 failed, 7 eqs, 16 impls)
c [sweep-9] 16 < 1/1000 * 62425 = 62 considered unsuccessful
c [sweep-9] removed 16 vars in TOTAL (1 rounds, 88 queries)
c [phase-count-14] 417684 negative 99.7% of 418939 except 1255 0.3%
c [phase-count-14] 336896 positive 80.4% of 418939 except 82043 19.6%
c [phase-count-14] skipping relative phase luck test
c [phase-14] phase bias: 0 positive 0%, 4 negative 100%
c [sort-queue-14] sorted 30686 enqueued variables after 119439 conflicts
c [score-dist-14] active 31723 (51%), one 13569 (22%), zero 17117 (27%)
c [score-dist-14] max exp 833, different 723 (87%)
c [score-dist-14] median active exp 760, avg 677.0
c [simplification-14] removed 423 variables 0.7% (62409 remain 22%)
c [simplification-14] removed 25639 irredundant clauses 5.8% (418939 remain 30%)
c [simplification-14] maximum reduction of 6% = max (1%, 6%)
c [simplification-14] large reduction 6% >= 5% limit
c [simplification-14] next conflict interval 2000 = 2000/1
c [simplification-14] penalized conflict interval 2000 = 1 * 2000
c [simplification-14] hard conflict limit 131439 (soft 121439 + delta 10000)
c [simplification-14] new conflict limit 121439 (hard 131439)
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  253.9   62408   418939    120066   38722   4120 345398   77   519  106  15%      8  132   91   59  154%
c i  254.3   62404   418939    120259   38903   4125 345401   77   527  106  15%      5  139   91   59  153%
c 
c [simplification-15] limit 121439 conflicts (hard 131439) hit after 121439 conflicts
c [quatres-9] found 29215 quaternary clauses 61% in total
c [quatres-9-1] removed 2 duplicate quaternary clauses
c [quatres-9-2] added 1 quaternary resolvents
c [ternres-11] limit 40753834 with penalty 0 = 0 + 0
c [ternres-11] all 62404 free variables schedulable
c [ternres-11] 22 ternary resolvents (0 bin, 22 trn)
c [ternres-11] fully completed ternary resolution
c [card-5] limit 1273557 penalty 4 = 4 + 0
c [card-5] found 2381 at-most-one constraints of average size 4.1
c [card-5] no at-most-two constraint found
c [card-5] using previous limit 1273557 for elimination
c [card-5] 2381 out of 2381 constraints (100%) meet size limits
c [card-5] no units found
c [card-5] no at-most-one constraints generated
c [decomp-34] removed 6 variables
c [basicprobe-5] limit 203769174 penalty 0 = 0 + 0
c [basicprobe-5-0] 12108 probes remain 20% after last round
c [basicprobe-5-0] 1088 units = 1079 failed (99%) + 9 lifted (1%)
c [basicprobe-5-0] removed 1618 variables, found 495981 hbrs
c [bate-3] eliminated 417 asymmetric tautologies during probing
c [unhide-15] limit 2037691 with penalty 2 = 0 + 2
c [unhide-15-15] 2 units, 311 failed, 3866 tauts, 0 hbrs, 252109 literals
c [transred-11] limit 2000000 with penalty 0 = 0 + 0
c [transred-11] removed 182 transitive binary clauses
c [block-5] scheduling all variables this time
c [block-5] scheduled 60652 variables 100%
c [block-5] limit of 50942293 steps penalty 3 = 3 + 0
c [block-5] fully completed
c [block-5] transition to [ all 0 rem 0 ] state
c [block-5] eliminated 745 blocked clauses
c [block-5] 745 < 1/100 * 406619 = 4066 considered unsuccessful
c [elim-11] scheduling all variables this time
c [elim-11] scheduled 60609 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 9920 variables 16% in round 1 in 36820330 steps
c [elim-11-1] backward subsumption/strengthening limit 36820300
c [elim-11-1-1] backward checking 24633 touched variables 41%
c [elim-11-1-1] fully completed backward checking in 1 rounds
c [elim-11-1] subsumed 17 and strengthened 34 clauses in 4333879 steps
c [elim-11-1] rescheduled 120 variables 0% by backward subsumption
c [elim-11-2] eliminated 10 variables 0% in round 2 in 1068684 steps
c [elim-11-2] backward subsumption/strengthening limit 1068600
c [elim-11-2-1] backward checking 92 touched variables 0%
c [elim-11-2-1] fully completed backward checking in 1 rounds
c [elim-11-2] subsumed 11 and strengthened 21 clauses in 448317 steps
c [elim-11-2] rescheduled 42 variables 0% by backward subsumption
c [elim-11-3] eliminated 2 variables 0% in round 3 in 991074 steps
c [elim-11-3] backward subsumption/strengthening limit 991000
c [elim-11-3-1] backward checking 19 touched variables 0%
c [elim-11-3-1] fully completed backward checking in 1 rounds
c [elim-11-3] subsumed 0 and strengthened 0 clauses in 348299 steps
c [elim-11] fully completed in 3 rounds
c [elim-11] transition to [ all 0 rem 0 ] state
c [elim-11] eliminated 9935 = 16% variables out of 60609 scheduled
c [bca-11] limit of 10000000 steps and 763373 added (scaled 2)
c [bca-11] 82790 out of 101350 literals actually usable 82%
c [bca-11] added 43 blocked clauses in 196705 steps
c [phase-count-15] 380194 negative 99.7% of 381195 except 1001 0.3%
c [phase-count-15] 301799 positive 79.2% of 381195 except 79396 20.8%
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 25817 enqueued variables after 121439 conflicts
c [score-dist-15] active 24857 (49%), one 11233 (22%), zero 14584 (29%)
c [score-dist-15] max exp 858, different 739 (86%)
c [score-dist-15] median active exp 752, avg 659.0
c [simplification-15] removed 11730 variables 18.8% (50674 remain 18%)
c [simplification-15] removed 37744 irredundant clauses 9.0% (381195 remain 28%)
c [simplification-15] maximum reduction of 19% = max (19%, 9%)
c [simplification-15] large reduction 19% >= 5% limit
c [simplification-15] next conflict interval 2000 = 2000/1
c [simplification-15] penalized conflict interval 2000 = 1 * 2000
c [simplification-15] hard conflict limit 133439 (soft 123439 + delta 10000)
c [simplification-15] new conflict limit 123439 (hard 133439)
c 
c [simplification-16] limit 123439 conflicts (hard 133439) hit after 123440 conflicts
c [quatres-10] found 31013 quaternary clauses 66% in total
c [quatres-10-1] removed 3 duplicate quaternary clauses
c [quatres-10-2] added 1 single-self-subsuming ternary resolvents
c [quatres-10-2] added 7 quaternary resolvents
c [ternres-12] limit 40998086 with penalty 0 = 0 + 0
c [ternres-12] all 50674 free variables schedulable
c [ternres-12] 444 ternary resolvents (0 bin, 444 trn)
c [ternres-12] fully completed ternary resolution
c [decomp-35] removed 20 variables
c [simpleprobe-6] all 50654 free variables schedulable
c [simpleprobe-6] limit 163992345 penalty 0 = 0 + 0
c [decomp-36] removed 1063 variables
c [simpleprobe-6] fully completed simple probing
c [simpleprobe-6] removed 1063 variables, found 69347 hbrs, 457 units
c [unhide-16] limit 8199617 with penalty 0 = 0 + 0
c [unhide-16-18] 9 units, 328 failed, 136857 tauts, 0 hbrs, 71923 literals
c [transred-12] limit 2000000 with penalty 0 = 0 + 0
c [transred-12] removed 203 transitive binary clauses
c [transred-12] found 3 units
c [cce-5] limit of 51247607 steps penalty 2 = 2 + 0
c [cce-5-1] eliminated 10 clauses out of 89 (11%) of length 7
c [cce-5-1] eliminated 357 clauses out of 3357 (11%) of length 6
c [cce-5-1] eliminated 6 clauses out of 8743 (0%) of length 5
c [cce-5-1] incomplete large round (ACCE)
c [cce-5-1] eliminated 373 large clauses in 51247612 steps
c [cce-5-1] allowing another 25623806 steps for small clauses
c [cce-5-1] scheduling 236458 clauses = 172693 binary + 63765 ternary
c [cce-5-1] tried to eliminate 840 small clauses 0%
c [cce-5-1] eliminated 184 binary clauses 0%
c [cce-5-1] eliminated 43 ternary clauses 0%
c [cce-5-1] eliminated 227 small clauses 0%
c [cce-5-1] eliminated 1195 small clauses in 51247611 steps
c [cce-5-1] incomplete small round (ACCE)
c [cce-5-1] eliminated 1568 covered clauses in round 1
c [cce-5] eliminated 1568 covered clauses in TOTAL during 1 rounds
c [cce-5] 1568 < 1/100 * 366042 = 3660 considered unsuccessful
c [elim-12] scheduling all variables this time
c [elim-12] scheduled 49275 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 526 variables 1% in round 1 in 32693490 steps
c [elim-12-1] backward subsumption/strengthening limit 32693400
c [elim-12-1-1] backward checking 3087 touched variables 6%
c [elim-12-1-1] fully completed backward checking in 1 rounds
c [elim-12-1] subsumed 14 and strengthened 6 clauses in 914069 steps
c [elim-12-1] rescheduled 57 variables 0% by backward subsumption
c [elim-12-2] eliminated 5 variables 0% in round 2 in 425863 steps
c [elim-12-2] backward subsumption/strengthening limit 425800
c [elim-12-2-1] backward checking 45 touched variables 0%
c [elim-12-2-1] fully completed backward checking in 1 rounds
c [elim-12-2] subsumed 12 and strengthened 5 clauses in 274549 steps
c [elim-12-2] rescheduled 34 variables 0% by backward subsumption
c [elim-12-3] eliminated 6 variables 0% in round 3 in 413253 steps
c [elim-12-3] backward subsumption/strengthening limit 413200
c [elim-12-3-1] backward checking 50 touched variables 0%
c [elim-12-3-1] fully completed backward checking in 1 rounds
c [elim-12-3] subsumed 7 and strengthened 4 clauses in 104390 steps
c [elim-12] incomplete 25 not tried 0% in round 3
c [elim-12] transition to [ all 1 rem 1 ] state
c [elim-12] eliminated 539 = 1% variables out of 49275 scheduled
c [bca-12] limit of 10000000 steps and 726579 added (scaled 2)
c [bca-12] 78134 out of 97474 literals actually usable 80%
c [bca-12] added 44 blocked clauses in 185718 steps
c [phase-count-16] 361927 negative 99.8% of 362787 except 860 0.2%
c [phase-count-16] 284596 positive 78.4% of 362787 except 78191 21.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 25766 enqueued variables after 123440 conflicts
c [score-dist-16] active 22970 (47%), one 12542 (26%), zero 13224 (27%)
c [score-dist-16] max exp 883, different 699 (79%)
c [score-dist-16] median active exp 669, avg 584.0
c [simplification-16] removed 1938 variables 3.8% (48736 remain 17%)
c [simplification-16] removed 18408 irredundant clauses 4.8% (362787 remain 26%)
c [simplification-16] maximum reduction of 5% = max (4%, 5%)
c [simplification-16] large reduction 5% >= 5% limit
c [simplification-16] next conflict interval 2000 = 2000/1
c [simplification-16] penalized conflict interval 2000 = 1 * 2000
c [simplification-16] hard conflict limit 135440 (soft 125440 + delta 10000)
c [simplification-16] new conflict limit 125440 (hard 135440)
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  282.0   48735   362787    123985   11250   3993 564465   67   489   59  14%     32   95   70   59  118%
c 
c [simplification-17] limit 125440 conflicts (hard 135440) hit after 125440 conflicts
c [quatres-11] found 29189 quaternary clauses 66% in total
c [quatres-11-1] removed 4 duplicate quaternary clauses
c [quatres-11-2] added 6 single-self-subsuming ternary resolvents
c [quatres-11-2] added 5 quaternary resolvents
c [ternres-13] limit 41277137 with penalty 0 = 0 + 0
c [ternres-13] all 48735 free variables schedulable
c [ternres-13] 403 ternary resolvents (0 bin, 403 trn)
c [ternres-13] fully completed ternary resolution
c [decomp-37] removed 32 variables
c [treelook-6] limit 4127713 penalty 0 = 0 + 0 boost 1
c [treelook-6] scheduled 79387 literals 81%
c [treelook-6] scheduling used 1759959 steps
c [treelook-6] scheduled completely
c [treelook-6] limit 4127713 penalty 0 = 0 + 0 boost 1
c [treelook-6] used 4170385 steps
c [treelook-6] 79294 literals remain 81%
c [treelook-6] 11506 variables remain to probed next time 24%
c [decomp-38] removed 3 variables
c [treelook-6] removed 11 variables, found 12783 hbrs
c [unhide-17] limit 8255427 with penalty 0 = 0 + 0
c [unhide-17-22] 4 units, 117 failed, 31963 tauts, 0 hbrs, 119124 literals
c [transred-13] limit 2000000 with penalty 0 = 0 + 0
c [transred-13] removed 158 transitive binary clauses
c [transred-13] found 2 units
c [elim-13] no untried remaining variables left
c [elim-13] scheduled 48552 variables 100%
c [elim-13] almost no limit of 100000000000 steps
c [elim-13] rescheduling of touched variables disabled
c [elim-13-1] eliminated 293 variables 1% in round 1 in 32366410 steps
c [elim-13-1] backward subsumption/strengthening limit 32366400
c [elim-13-1-1] backward checking 1833 touched variables 4%
c [elim-13-1-1] fully completed backward checking in 1 rounds
c [elim-13-1] subsumed 8 and strengthened 3 clauses in 533558 steps
c [elim-13-1] rescheduled 28 variables 0% by backward subsumption
c [elim-13-2] eliminated 3 variables 0% in round 2 in 20805 steps
c [elim-13-2] backward subsumption/strengthening limit 20800
c [elim-13-2-1] backward checking 39 touched variables 0%
c [elim-13-2-1] incomplete backward checking 37 remain 95%
c [elim-13-2] subsumed 0 and strengthened 0 clauses in 20814 steps
c [elim-13-2] fully rescheduled 48256 variables 99%
c [elim-13-3] eliminated 35 variables 0% in round 3 in 32219589 steps
c [elim-13-3] backward subsumption/strengthening limit 32219500
c [elim-13-3-1] backward checking 261 touched variables 1%
c [elim-13-3-1] fully completed backward checking in 1 rounds
c [elim-13-3] subsumed 3 and strengthened 2 clauses in 173397 steps
c [elim-13] incomplete 13 not tried 0% in round 3
c [elim-13] transition to [ all 1 rem 1 ] state
c [elim-13] eliminated 331 = 1% variables out of 48552 scheduled
c [elim-13] 331 < 1/100 * 48552 = 485 considered unsuccessful
c [bca-13] limit of 10000000 steps and 715947 added (scaled 2)
c [bca-13] 76217 out of 96444 literals actually usable 79%
c [bca-13] added 30 blocked clauses in 181364 steps
c [sweep-10] limit 3095785 penalty 2 = 2 + 0
c [sweep-10-1] 4413 pos 12.5% + 30928 neg 87.5% = 35341 sched 73.3% ret 12880
c [sweep-10-1] 3108761 steps 68 queries 3642.19 avg class size
c [sweep-10-1] 894 decisions 61 SAT calls 151.11 avg env size
c [sweep-10-1] 34407 variables remain 71% (13814 retained 29%)
c [decomp-39] removed 21 variables
c [sweep-10-1] removed 21 vars (0 failed, 7 eqs, 9 impls)
c [sweep-10] 21 < 1/1000 * 48221 = 48 considered unsuccessful
c [sweep-10] removed 21 vars in TOTAL (1 rounds, 67 queries)
c [phase-count-17] 356588 negative 99.8% of 357426 except 838 0.2%
c [phase-count-17] 280206 positive 78.4% of 357426 except 77220 21.6%
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 25210 enqueued variables after 125440 conflicts
c [score-dist-17] active 22990 (48%), one 12685 (26%), zero 12525 (26%)
c [score-dist-17] max exp 919, different 639 (69%)
c [score-dist-17] median active exp 860, avg 727.1
c [simplification-17] removed 535 variables 1.1% (48200 remain 17%)
c [simplification-17] removed 5361 irredundant clauses 1.5% (357426 remain 26%)
c [simplification-17] maximum reduction of 1% = max (1%, 1%)
c [simplification-17] geometric conflict interval increment 16532 = 33065 / 2
c [simplification-17] new conflict interval 49597
c [simplification-17] penalized conflict interval 49597 = 1 * 49597
c [simplification-17] hard conflict limit 199835 (soft 175037 + delta 24798)
c [simplification-17] new conflict limit 175037 (hard 199835)
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  289.1   48199   357426    125720   11585   4217 534970   64   480   57  13%     11   84   43   59   73%
c i  289.2   48190   357426    125986   11802   4224 534979   61   461   57  13%      6   65   31   59   52%
c i  291.4   48165   357426    130211   15694   4258 535004   57   365   64  16%     38  -32   78   59  133%
c i  292.2   48145   357426    131556   16911   4270 535024   58   385   65  15%     10  -12   64   59  108%
c i  292.6   48143   357426    132675   17835   4286 535039   55   339   66  16%      2  -57   63   59  107%
c i  306.4   48112   357426    152246   36289   4407 535109   58   341  174  17%    243  -27   64   56  115%
c i  306.4   48090   357426    152247   36289   4407 535109   57   340  174  17%    242  -27   64   56  115%
c i  308.6   48089   357426    155206   39020   4432 535124   59   333  177  18%     -2  -33   61   56  109%
c i  311.7   48088   357426    160642   43871   4490 535168   53   315  178  17%     20  -46   63   56  113%
c i  317.3   48087   357426    169799   52136   4560 535225   56   308  186  18%     76  -52   84   56  151%
c i  319.5   48086   357426    172635   54759   4579 535240   59   337  186  17%    -14  -23   70   56  125%
c -  321.7   48081   357426    175039   25090   4601 535254   62   331   60  19%    -24  -27   73   56  130%
c 
c [simplification-18] limit 175047 conflicts (hard 199835) hit after 177506 conflicts
c [quatres-12] found 28778 quaternary clauses 64% in total
c [quatres-12-1] removed 1 duplicate quaternary clauses
c [quatres-12-2] added 2 single-self-subsuming ternary resolvents
c [quatres-12-2] added 3 quaternary resolvents
c [ternres-14] limit 48400971 with penalty 0 = 0 + 0
c [ternres-14] all 48081 free variables schedulable
c [ternres-14] 261 ternary resolvents (0 bin, 261 trn)
c [ternres-14] fully completed ternary resolution
c [decomp-40] removed 123 variables
c [basicprobe-6] limit 242004856 penalty 0 = 0 + 0
c [basicprobe-6-0] 1439 probes remain 3% after last round
c [basicprobe-6-0] 921 units = 857 failed (93%) + 64 lifted (7%)
c [basicprobe-6-0] removed 1414 variables, found 556160 hbrs
c [bate-4] eliminated 1767 asymmetric tautologies during probing
c [unhide-18] limit 4840097 with penalty 1 = 0 + 1
c [unhide-18-24] 3 units, 46 failed, 97897 tauts, 0 hbrs, 107262 literals
c [transred-14] limit 2000000 with penalty 0 = 0 + 0
c [transred-14] removed 115 transitive binary clauses
c [transred-14] found 2 units
c [bca-14] limit of 10000000 steps and 674340 added (scaled 2)
c [bca-14] 67513 out of 93130 literals actually usable 72%
c [bca-14] added 13 blocked clauses in 173911 steps
c [sort-queue-18] sorted 28880 enqueued variables after 177506 conflicts
c [score-dist-18] active 17684 (38%), one 18077 (39%), zero 10803 (23%)
c [score-dist-18] max exp 572, different 440 (77%)
c [score-dist-18] median active exp 484, avg 441.8
c [simplification-18] removed 1517 variables 3.2% (46564 remain 16%)
c [simplification-18] removed 20777 irredundant clauses 5.8% (336649 remain 24%)
c [simplification-18] maximum reduction of 6% = max (3%, 6%)
c [simplification-18] large reduction 6% >= 5% limit
c [simplification-18] next conflict interval 2000 = 2000/1
c [simplification-18] penalized conflict interval 2000 = 1 * 2000
c [simplification-18] hard conflict limit 189506 (soft 179506 + delta 10000)
c [simplification-18] new conflict limit 179506 (hard 189506)
c 
c [simplification-19] limit 179506 conflicts (hard 189506) hit after 179871 conflicts
c [quatres-13] found 24781 quaternary clauses 61% in total
c [quatres-13-1] removed 2 duplicate quaternary clauses
c [quatres-13-2] added 1 quaternary resolvents
c [ternres-15] limit 48842697 with penalty 0 = 0 + 0
c [ternres-15] all 46564 free variables schedulable
c [ternres-15] 84 ternary resolvents (0 bin, 84 trn)
c [ternres-15] fully completed ternary resolution
c [gauss-5] limit 610533 penalty 4 = 4 + 0
c [gauss-5] extracted 30 xors of average arity 2.3
c [gauss-5] connected 70 occurrences of 67 variables (average 1.0)
c [gauss-5] limit 610533 penalty 4 = 4 + 0
c [gauss-5] fully completed
c [gauss-5] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-41] removed 257 variables
c [simpleprobe-7] all 46307 free variables schedulable
c [simpleprobe-7] limit 195370791 penalty 0 = 0 + 0
c [decomp-42] removed 328 variables
c [simpleprobe-7] fully completed simple probing
c [simpleprobe-7] removed 328 variables, found 75007 hbrs, 126 units
c [unhide-19] limit 4884269 with penalty 1 = 0 + 1
c [unhide-19-26] 3 units, 38 failed, 67248 tauts, 0 hbrs, 106144 literals
c [transred-15] limit 2000000 with penalty 0 = 0 + 0
c [transred-15] removed 186 transitive binary clauses
c [transred-15] found 1 units
c [cce-6] limit of 30526686 steps penalty 3 = 3 + 0
c [cce-6-1] eliminated 3 clauses out of 2948 (0%) of length 6
c [cce-6-1] eliminated 6 clauses out of 8264 (0%) of length 5
c [cce-6-1] incomplete large round (ATE)
c [cce-6-1] eliminated 9 large clauses in 30526699 steps
c [cce-6-1] allowing another 15263349 steps for small clauses
c [cce-6-1] scheduling 217813 clauses = 161311 binary + 56502 ternary
c [cce-6-1] tried to eliminate 825 small clauses 0%
c [cce-6-1] eliminated 163 binary clauses 0%
c [cce-6-1] eliminated 33 ternary clauses 0%
c [cce-6-1] eliminated 196 small clauses 0%
c [cce-6-1] eliminated 1012 small clauses in 30526690 steps
c [cce-6-1] incomplete small round (ATE)
c [cce-6-1] eliminated 1021 covered clauses in round 1
c [cce-6] eliminated 1021 covered clauses in TOTAL during 1 rounds
c [cce-6] 1021 < 1/100 * 331514 = 3315 considered unsuccessful
c [elim-14] no untried remaining variables left
c [elim-14] scheduled 45838 variables 100%
c [elim-14] limit of 400000000 steps penalty 1 = 1 + 0
c [elim-14] rescheduling of touched variables disabled
c [elim-14-1] eliminated 1178 variables 3% in round 1 in 29964094 steps
c [elim-14-1] backward subsumption/strengthening limit 29964000
c [elim-14-1-1] backward checking 5997 touched variables 13%
c [elim-14-1-1] fully completed backward checking in 1 rounds
c [elim-14-1] subsumed 13 and strengthened 15 clauses in 1688515 steps
c [elim-14-1] rescheduled 83 variables 0% by backward subsumption
c [elim-14-2] eliminated 4 variables 0% in round 2 in 63279 steps
c [elim-14-2] backward subsumption/strengthening limit 63200
c [elim-14-2-1] backward checking 76 touched variables 0%
c [elim-14-2-1] incomplete backward checking 5 remain 7%
c [elim-14-2] subsumed 5 and strengthened 2 clauses in 63210 steps
c [elim-14-2] rescheduled 18 variables 0% by backward subsumption
c [elim-14-3] eliminated 1 variables 0% in round 3 in 312082 steps
c [elim-14-3] backward subsumption/strengthening limit 312000
c [elim-14-3-1] backward checking 18 touched variables 0%
c [elim-14-3-1] fully completed backward checking in 1 rounds
c [elim-14-3] subsumed 1 and strengthened 2 clauses in 71852 steps
c [elim-14] incomplete 11 not tried 0% in round 3
c [elim-14] transition to [ all 1 rem 1 ] state
c [elim-14] eliminated 1183 = 3% variables out of 45838 scheduled
c [bca-15] limit of 10000000 steps and 656328 added (scaled 2)
c [bca-15] 65557 out of 89312 literals actually usable 73%
c [bca-15] added 13 blocked clauses in 164974 steps
c [sort-queue-19] sorted 24970 enqueued variables after 179871 conflicts
c [score-dist-19] active 19685 (44%), one 14857 (33%), zero 10113 (23%)
c [score-dist-19] max exp 691, different 558 (81%)
c [score-dist-19] median active exp 626, avg 519.3
c [simplification-19] removed 1909 variables 4.1% (44655 remain 16%)
c [simplification-19] removed 9009 irredundant clauses 2.7% (327640 remain 24%)
c [simplification-19] maximum reduction of 4% = max (4%, 3%)
c [simplification-19] geometric conflict interval increment 9919 = 49597 / 5
c [simplification-19] new conflict interval 59516
c [simplification-19] penalized conflict interval 59516 = 1 * 59516
c [simplification-19] hard conflict limit 269145 (soft 239387 + delta 29758)
c [simplification-19] new conflict limit 239387 (hard 269145)
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  352.6   44654   327640    184035   26259   5182 802026   67   378   75  18%    106   20   91   58  157%
c i  354.8   44651   327640    187108   29105   5208 802037   66   372   79  18%    -15   13   68   58  117%
c i  355.5   44646   327640    188031   29943   5222 802037   68   376   79  18%    -34   17   82   58  140%
c i  359.2   44644   327640    193126   34638   5252 802054   68   344   87  20%     10  -14   91   59  155%
c i  359.3   44643   327640    193295   34782   5252 802055   68   337   87  20%      0  -21   85   59  144%
c i  361.4   44639   327640    195895   37210   5272 802067   68   358   93  19%    -23    0   76   59  129%
c i  365.5   44600   327640    201254   42190   5302 802081   69   345  108  20%     16  -12   93   60  156%
c i  367.4   44568   327640    203947   44681   5319 802097   64   381  120  17%    -19   24   69   60  115%
c i  369.1   44559   327640    206241   46795   5346 802108   65   373  120  17%    -25   14   80   60  134%
c -  380.7   44548   327640    219151   25085   5454 802160   73   385   63  19%    128   20   84   62  134%
c 
c [simplification-20] limit 239387 conflicts (hard 269145) hit after 239389 conflicts
c [quatres-14] found 24788 quaternary clauses 60% in total
c [quatres-14-1] removed 1 duplicate quaternary clauses
c [quatres-14-2] added 3 single-self-subsuming ternary resolvents
c [quatres-14-2] added 5 quaternary resolvents
c [ternres-16] limit 58903915 with penalty 0 = 0 + 0
c [ternres-16] all 44548 free variables schedulable
c [ternres-16] 357 ternary resolvents (0 bin, 357 trn)
c [ternres-16] fully completed ternary resolution
c [decomp-43] removed 114 variables
c [treelook-7] limit 5890391 penalty 0 = 0 + 0 boost 1
c [treelook-7] scheduled 71102 literals 80%
c [treelook-7] scheduling used 1903313 steps
c [treelook-7] scheduled completely
c [treelook-7] limit 5890391 penalty 0 = 0 + 0 boost 1
c [treelook-7] used 5997491 steps
c [treelook-7] 70969 literals remain 80%
c [treelook-7] 10390 variables remain to probed next time 23%
c [treelook-7] removed 19 variables, found 26861 hbrs
c [unhide-20] limit 2945195 with penalty 2 = 0 + 2
c [unhide-20-27] 1 units, 42 failed, 27169 tauts, 0 hbrs, 662958 literals
c [transred-16] limit 2000000 with penalty 0 = 0 + 0
c [transred-16] removed 212 transitive binary clauses
c [block-6] scheduling all variables this time
c [block-6] scheduled 44489 variables 100%
c [block-6] limit of 36814947 steps penalty 4 = 4 + 0
c [block-6] fully completed
c [block-6] transition to [ all 0 rem 0 ] state
c [block-6] eliminated 14 blocked clauses
c [block-6] 14 < 1/100 * 326612 = 3266 considered unsuccessful
c [elim-15] no untried remaining variables left
c [elim-15] scheduled 44488 variables 100%
c [elim-15] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-15] rescheduling of touched variables disabled
c [elim-15-1] eliminated 138 variables 0% in round 1 in 29617236 steps
c [elim-15-1] backward subsumption/strengthening limit 29617200
c [elim-15-1-1] backward checking 752 touched variables 2%
c [elim-15-1-1] fully completed backward checking in 1 rounds
c [elim-15-1] subsumed 3 and strengthened 6 clauses in 309988 steps
c [elim-15-1] rescheduled 27 variables 0% by backward subsumption
c [elim-15-2] eliminated 4 variables 0% in round 2 in 29814 steps
c [elim-15-2] backward subsumption/strengthening limit 29800
c [elim-15-2-1] backward checking 39 touched variables 0%
c [elim-15-2-1] incomplete backward checking 13 remain 33%
c [elim-15-2] subsumed 0 and strengthened 4 clauses in 29803 steps
c [elim-15-2] rescheduled 16 variables 0% by backward subsumption
c [elim-15-3] eliminated 2 variables 0% in round 3 in 18925 steps
c [elim-15-3] backward subsumption/strengthening limit 18900
c [elim-15-3-1] backward checking 31 touched variables 0%
c [elim-15-3-1] incomplete backward checking 12 remain 39%
c [elim-15-3] subsumed 0 and strengthened 3 clauses in 18902 steps
c [elim-15] incomplete 12 not tried 0% in round 3
c [elim-15] transition to [ all 1 rem 1 ] state
c [elim-15] eliminated 144 = 0% variables out of 44488 scheduled
c [elim-15] 144 < 1/100 * 44488 = 444 considered unsuccessful
c [bca-16] limit of 10000000 steps and 653063 added (scaled 2)
c [bca-16] 60132 out of 88690 literals actually usable 68%
c [bca-16] added 6 blocked clauses in 168559 steps
c [sort-queue-20] sorted 22460 enqueued variables after 239389 conflicts
c [score-dist-20] active 21884 (49%), one 12847 (29%), zero 9613 (22%)
c [score-dist-20] max exp 790, different 661 (84%)
c [score-dist-20] median active exp 698, avg 600.2
c [simplification-20] removed 204 variables 0.5% (44344 remain 15%)
c [simplification-20] removed 1636 irredundant clauses 0.5% (326004 remain 24%)
c [simplification-20] maximum reduction of 0% = max (0%, 0%)
c [simplification-20] full geometric conflict interval increment 59516
c [simplification-20] new conflict interval 119032
c [simplification-20] penalized conflict interval 119032 = 1 * 119032
c [simplification-20] hard conflict limit 417937 (soft 358421 + delta 59516)
c [simplification-20] new conflict limit 358421 (hard 417937)
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  408.5   44343   326004    245038   43405   5900 785759   76   361  104  21%    421    7   82   65  127%
c -  427.0   44272   326004    263685   26415   6023 785836   86   397   63  22%    107   31  103   70  148%
c i  427.3   44271   326004    263924   26628   6024 785836   86   396   69  22%    110   30  100   70  143%
c i  429.7   44199   326004    266974   29462   6043 785842   81   394   72  21%   -119   26   60   70   85%
c i  430.7   44150   326004    268230   30642   6058 785850   82   413   75  20%   -141   44   81   71  115%
c i  441.7   44147   326004    282461   43825   6105 785887   75   372  111  20%     55    7   92   70  131%
c -  456.5   44142   326004    301689   29091   6173 785924   76   394   64  19%    133   34  115   69  166%
c -  489.2   44142   326004    339394   28859   6395 786070   82   421   97  20%    523   42   71   74   96%
c 
c [simplification-21] limit 358421 conflicts (hard 417937) hit after 358421 conflicts
c [quatres-15] found 24559 quaternary clauses 58% in total
c [quatres-15-1] removed 2 duplicate quaternary clauses
c [quatres-15-2] added 4 single-self-subsuming ternary resolvents
c [ternres-17] limit 79991116 with penalty 0 = 0 + 0
c [ternres-17] all 44142 free variables schedulable
c [ternres-17] 77 ternary resolvents (0 bin, 77 trn)
c [ternres-17] fully completed ternary resolution
c [card-6] limit 2499722 penalty 4 = 4 + 0
c [card-6] found 2082 at-most-one constraints of average size 4.0
c [card-6] no at-most-two constraint found
c [card-6] using previous limit 2499722 for elimination
c [card-6] 2082 out of 2082 constraints (100%) meet size limits
c [card-6] no units found
c [card-6] no at-most-one constraints generated
c [decomp-45] removed 206 variables
c [basicprobe-7] limit 399955584 penalty 0 = 0 + 0
c [basicprobe-7-0] 3155 sched 7%, 557 failed, 22 lifted, 171741 hbrs
c [decomp-46] removed 873 variables
c [basicprobe-7-1] 11214 sched 26%, 435 failed, 24 lifted, 227330 hbrs
c [decomp-47] removed 639 variables
c [basicprobe-7-2] 10831 probes remain 25% after last round
c [basicprobe-7-2] 1049 units = 1003 failed (96%) + 46 lifted (4%)
c [basicprobe-7-2] removed 1527 variables, found 401827 hbrs
c [bate-5] eliminated 1157 asymmetric tautologies during probing
c [unhide-21] limit 3999555 with penalty 2 = 0 + 2
c [unhide-21-29] 0 units, 4 failed, 95420 tauts, 0 hbrs, 1119733 literals
c [transred-17] limit 2000000 with penalty 0 = 0 + 0
c [transred-17] removed 203 transitive binary clauses
c [bca-17] limit of 10000000 steps and 610610 added (scaled 2)
c [bca-17] 55109 out of 85218 literals actually usable 65%
c [bca-17] added 5 blocked clauses in 164761 steps
c [sweep-11] boosting sweeping limit by 10
c [sweep-11] limit 29996668 penalty 3 = 3 + 0
c [sweep-11-1] 4042 pos 12.6% + 28088 neg 87.4% = 32130 sched 75.4% ret 10478
c [sweep-11-1] 30006009 steps 774 queries 287.39 avg class size
c [sweep-11-1] 14004 decisions 730 SAT calls 171.24 avg env size
c [sweep-11-1] 19543 variables remain 46% (23061 retained 54%)
c [decomp-48] removed 77 variables
c [sweep-11-1] removed 77 vars (0 failed, 47 eqs, 101 impls)
c [sweep-11] removed 77 vars in TOTAL (1 rounds, 773 queries)
c [sort-queue-21] sorted 21824 enqueued variables after 358421 conflicts
c [score-dist-21] active 20707 (49%), one 14157 (33%), zero 7667 (18%)
c [score-dist-21] max exp 572, different 513 (90%)
c [score-dist-21] median active exp 428, avg 390.7
c [simplification-21] removed 1611 variables 3.6% (42531 remain 15%)
c [simplification-21] removed 21385 irredundant clauses 6.6% (304619 remain 22%)
c [simplification-21] maximum reduction of 7% = max (4%, 7%)
c [simplification-21] large reduction 7% >= 5% limit
c [simplification-21] next conflict interval 3584 = min (358421/100, 119032)
c [simplification-21] penalized conflict interval 3584 = 1 * 3584
c [simplification-21] hard conflict limit 372005 (soft 362005 + delta 10000)
c [simplification-21] new conflict limit 362005 (hard 372005)
c 
c [simplification-22] limit 362005 conflicts (hard 372005) hit after 362340 conflicts
c [quatres-16] found 23569 quaternary clauses 57% in total
c [quatres-16-1] removed 3 duplicate quaternary clauses
c [quatres-16-2] added 1 single-self-subsuming ternary resolvents
c [ternres-18] limit 80737875 with penalty 0 = 0 + 0
c [ternres-18] all 42531 free variables schedulable
c [ternres-18] 44 ternary resolvents (0 bin, 44 trn)
c [ternres-18] fully completed ternary resolution
c [simpleprobe-8] all 42531 free variables schedulable
c [simpleprobe-8] limit 200000000 penalty 0 = 0 + 0
c [decomp-50] removed 57 variables
c [simpleprobe-8] fully completed simple probing
c [simpleprobe-8] removed 57 variables, found 48057 hbrs, 19 units
c [unhide-22] limit 4036893 with penalty 2 = 0 + 2
c [unhide-22-30] 0 units, 38 failed, 61628 tauts, 0 hbrs, 280107 literals
c [transred-18] limit 2000000 with penalty 0 = 0 + 0
c [transred-18] removed 213 transitive binary clauses
c [elim-16] no untried remaining variables left
c [elim-16] scheduled 42425 variables 100%
c [elim-16] limit of 400000000 steps penalty 1 = 1 + 0
c [elim-16] rescheduling of touched variables disabled
c [elim-16-1] eliminated 618 variables 1% in round 1 in 27309689 steps
c [elim-16-1] backward subsumption/strengthening limit 27309600
c [elim-16-1-1] backward checking 3534 touched variables 8%
c [elim-16-1-1] fully completed backward checking in 1 rounds
c [elim-16-1] subsumed 9 and strengthened 14 clauses in 988532 steps
c [elim-16-1] rescheduled 66 variables 0% by backward subsumption
c [elim-16-2] eliminated 4 variables 0% in round 2 in 50285 steps
c [elim-16-2] backward subsumption/strengthening limit 50200
c [elim-16-2-1] backward checking 55 touched variables 0%
c [elim-16-2-1] incomplete backward checking 0 remain 0%
c [elim-16-2] subsumed 1 and strengthened 4 clauses in 50201 steps
c [elim-16-2] rescheduled 20 variables 0% by backward subsumption
c [elim-16-3] eliminated 1 variables 0% in round 3 in 30307 steps
c [elim-16-3] backward subsumption/strengthening limit 30300
c [elim-16-3-1] backward checking 19 touched variables 0%
c [elim-16-3-1] incomplete backward checking 0 remain 0%
c [elim-16-3] subsumed 0 and strengthened 2 clauses in 30301 steps
c [elim-16] incomplete 8 not tried 0% in round 3
c [elim-16] transition to [ all 1 rem 1 ] state
c [elim-16] eliminated 623 = 1% variables out of 42425 scheduled
c [bca-18] limit of 10000000 steps and 606280 added (scaled 2)
c [bca-18] 54585 out of 83606 literals actually usable 65%
c [bca-18] added 11 blocked clauses in 157255 steps
c [sort-queue-22] sorted 23772 enqueued variables after 362340 conflicts
c [score-dist-22] active 18030 (43%), one 16267 (39%), zero 7505 (18%)
c [score-dist-22] max exp 603, different 479 (79%)
c [score-dist-22] median active exp 519, avg 425.1
c [simplification-22] removed 729 variables 1.7% (41802 remain 15%)
c [simplification-22] removed 2009 irredundant clauses 0.7% (302610 remain 22%)
c [simplification-22] maximum reduction of 2% = max (2%, 1%)
c [simplification-22] geometric conflict interval increment 39677 = 119032 / 3
c [simplification-22] new conflict interval 158709
c [simplification-22] penalized conflict interval 158709 = 1 * 158709
c [simplification-22] hard conflict limit 600403 (soft 521049 + delta 79354)
c [simplification-22] new conflict limit 521049 (hard 600403)
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  542.9   41801   302610    362367   39490   6429 845013   85   385   87  22%    671    1  100   77  129%
c i  547.4   41797   302610    367994   44656   6451 845032   83   447   88  19%   -459   61  101   78  130%
c i  550.8   41787   302610    371772   48165   6471 845039   86   445  105  19%   -463   56   87   78  112%
c i  552.7   41747   302610    373764   49985   6482 845044   89   450  105  20%   -470   59  100   79  127%
c i  552.7   41721   302610    373765   49985   6482 845044   89   450  105  20%   -470   59   99   79  127%
c -  565.0   41681   302610    390332   30018   6527 845076   65   289   64  23%   -167  -97   47   77   60%
c -  599.0   41681   302610    430938   30469   6709 845151   95   395   63  24%    383    6  102   83  122%
c i  601.8   41680   302610    434703   33850   6727 845153   91   401   74  23%    419   12   91   83  109%
c i  608.4   41664   302610    443142   41498   6752 845166   87   401  124  22%   -358   11   84   84  100%
c i  611.4   41633   302610    447554   45529   6777 845177   86   411  136  21%   -392   21  117   84  140%
c -  632.8   41633   302610    472495   31541   6875 845228  100   428   97  23%      7   34  118   87  135%
c -  666.1   41633   302610    514373   33399   6979 845273   93   399   97  23%    487   12  101   87  115%
c 
c [simplification-23] limit 521059 conflicts (hard 600403) hit after 521059 conflicts
c [quatres-17] found 23564 quaternary clauses 55% in total
c [quatres-17-2] added 1 single-self-subsuming ternary resolvents
c [quatres-17-2] added 10 quaternary resolvents
c [ternres-19] limit 107456101 with penalty 0 = 0 + 0
c [ternres-19] all 41633 free variables schedulable
c [ternres-19] 270 ternary resolvents (8 bin, 262 trn)
c [ternres-19] fully completed ternary resolution
c [decomp-51] removed 245 variables
c [treelook-8] limit 10745610 penalty 0 = 0 + 0 boost 1
c [treelook-8] scheduled 66693 literals 80%
c [treelook-8] scheduling used 1787583 steps
c [treelook-8] scheduled completely
c [treelook-8] limit 10745610 penalty 0 = 0 + 0 boost 1
c [treelook-8] used 11057792 steps
c [treelook-8] 66523 literals remain 80%
c [treelook-8] 9523 variables remain to probed next time 23%
c [treelook-8] removed 17 variables, found 18140 hbrs
c [unhide-23] limit 10000000 with penalty 1 = 0 + 1
c [unhide-23-34] 0 units, 10 failed, 45250 tauts, 0 hbrs, 376048 literals
c [transred-19] limit 2000000 with penalty 0 = 0 + 0
c [transred-19] removed 138 transitive binary clauses
c [cce-7] limit of 33580031 steps penalty 4 = 4 + 0
c [cce-7-1] eliminated 1 clauses out of 1 (100%) of length 48
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 47
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 46
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 45
c [cce-7-1] eliminated 1 clauses out of 1 (100%) of length 44
c [cce-7-1] eliminated 2 clauses out of 3 (67%) of length 43
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 42
c [cce-7-1] eliminated 2 clauses out of 3 (67%) of length 41
c [cce-7-1] eliminated 2 clauses out of 3 (67%) of length 40
c [cce-7-1] eliminated 4 clauses out of 4 (100%) of length 39
c [cce-7-1] eliminated 2 clauses out of 4 (50%) of length 38
c [cce-7-1] eliminated 4 clauses out of 4 (100%) of length 37
c [cce-7-1] eliminated 2 clauses out of 3 (67%) of length 36
c [cce-7-1] eliminated 3 clauses out of 4 (75%) of length 35
c [cce-7-1] eliminated 2 clauses out of 3 (67%) of length 34
c [cce-7-1] eliminated 4 clauses out of 4 (100%) of length 33
c [cce-7-1] eliminated 3 clauses out of 5 (60%) of length 32
c [cce-7-1] eliminated 4 clauses out of 5 (80%) of length 31
c [cce-7-1] eliminated 5 clauses out of 6 (83%) of length 30
c [cce-7-1] eliminated 4 clauses out of 5 (80%) of length 29
c [cce-7-1] eliminated 4 clauses out of 6 (67%) of length 28
c [cce-7-1] eliminated 6 clauses out of 7 (86%) of length 27
c [cce-7-1] eliminated 3 clauses out of 6 (50%) of length 26
c [cce-7-1] eliminated 7 clauses out of 7 (100%) of length 25
c [cce-7-1] eliminated 3 clauses out of 5 (60%) of length 24
c [cce-7-1] eliminated 5 clauses out of 6 (83%) of length 23
c [cce-7-1] eliminated 4 clauses out of 6 (67%) of length 22
c [cce-7-1] eliminated 5 clauses out of 5 (100%) of length 21
c [cce-7-1] eliminated 4 clauses out of 7 (57%) of length 20
c [cce-7-1] eliminated 5 clauses out of 6 (83%) of length 19
c [cce-7-1] eliminated 4 clauses out of 6 (67%) of length 18
c [cce-7-1] eliminated 5 clauses out of 8 (62%) of length 17
c [cce-7-1] eliminated 7 clauses out of 8 (88%) of length 16
c [cce-7-1] eliminated 6 clauses out of 8 (75%) of length 15
c [cce-7-1] eliminated 8 clauses out of 11 (73%) of length 14
c [cce-7-1] eliminated 7 clauses out of 11 (64%) of length 13
c [cce-7-1] eliminated 10 clauses out of 14 (71%) of length 12
c [cce-7-1] eliminated 11 clauses out of 15 (73%) of length 11
c [cce-7-1] eliminated 12 clauses out of 14 (86%) of length 10
c [cce-7-1] eliminated 12 clauses out of 16 (75%) of length 9
c [cce-7-1] eliminated 12 clauses out of 17 (71%) of length 8
c [cce-7-1] eliminated 13 clauses out of 90 (14%) of length 7
c [cce-7-1] eliminated 26 clauses out of 2958 (1%) of length 6
c [cce-7-1] eliminated 17 clauses out of 8246 (0%) of length 5
c [cce-7-1] incomplete large round (ACCE)
c [cce-7-1] eliminated 247 large clauses in 33580031 steps
c [cce-7-1] allowing another 16790015 steps for small clauses
c [cce-7-1] scheduling 199903 clauses = 151696 binary + 48207 ternary
c [cce-7-1] tried to eliminate 824 small clauses 0%
c [cce-7-1] eliminated 136 binary clauses 0%
c [cce-7-1] eliminated 24 ternary clauses 0%
c [cce-7-1] eliminated 160 small clauses 0%
c [cce-7-1] eliminated 191 small clauses in 33580045 steps
c [cce-7-1] incomplete small round (ACCE)
c [cce-7-1] eliminated 438 covered clauses in round 1
c [cce-7] eliminated 438 covered clauses in TOTAL during 1 rounds
c [cce-7] 438 < 1/100 * 298632 = 2986 considered unsuccessful
c [elim-17] no untried remaining variables left
c [elim-17] scheduled 41524 variables 100%
c [elim-17] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-17] rescheduling of touched variables disabled
c [elim-17-1] eliminated 224 variables 1% in round 1 in 26433466 steps
c [elim-17-1] backward subsumption/strengthening limit 26433400
c [elim-17-1-1] backward checking 1248 touched variables 3%
c [elim-17-1-1] fully completed backward checking in 1 rounds
c [elim-17-1] subsumed 4 and strengthened 6 clauses in 409936 steps
c [elim-17-1] rescheduled 25 variables 0% by backward subsumption
c [elim-17-2] eliminated 1 variables 0% in round 2 in 35179 steps
c [elim-17-2] backward subsumption/strengthening limit 35100
c [elim-17-2-1] backward checking 13 touched variables 0%
c [elim-17-2-1] incomplete backward checking 0 remain 0%
c [elim-17-2] subsumed 0 and strengthened 0 clauses in 35101 steps
c [elim-17-2] fully rescheduled 41299 variables 99%
c [elim-17-3] eliminated 10 variables 0% in round 3 in 26461053 steps
c [elim-17-3] backward subsumption/strengthening limit 26461000
c [elim-17-3-1] backward checking 229 touched variables 1%
c [elim-17-3-1] fully completed backward checking in 1 rounds
c [elim-17-3] subsumed 1 and strengthened 4 clauses in 164567 steps
c [elim-17] incomplete 19 not tried 0% in round 3
c [elim-17] transition to [ all 1 rem 1 ] state
c [elim-17] eliminated 235 = 1% variables out of 41524 scheduled
c [elim-17] 235 < 1/100 * 41524 = 415 considered unsuccessful
c [bca-19] limit of 10000000 steps and 597050 added (scaled 2)
c [bca-19] 53980 out of 82580 literals actually usable 65%
c [bca-19] added 14 blocked clauses in 152206 steps
c [sweep-12] limit 8059207 penalty 2 = 2 + 0
c [sweep-12-1] 3406 pos 18.0% + 15522 neg 82.0% = 18928 sched 45.8% ret 22361
c [sweep-12-1] 8140587 steps 245 queries 582.30 avg class size
c [sweep-12-1] 4145 decisions 227 SAT calls 135.46 avg env size
c [sweep-12-1] 17585 variables remain 43% (23704 retained 57%)
c [decomp-53] removed 18 variables
c [sweep-12-1] removed 18 vars (0 failed, 17 eqs, 31 impls)
c [sweep-12] 18 < 1/1000 * 41289 = 41 considered unsuccessful
c [sweep-12] removed 18 vars in TOTAL (1 rounds, 244 queries)
c [sort-queue-23] sorted 21594 enqueued variables after 521059 conflicts
c [score-dist-23] active 19677 (48%), one 14494 (35%), zero 7100 (17%)
c [score-dist-23] max exp 753, different 567 (75%)
c [score-dist-23] median active exp 645, avg 586.6
c [simplification-23] removed 362 variables 0.9% (41271 remain 14%)
c [simplification-23] removed 4636 irredundant clauses 1.5% (297974 remain 22%)
c [simplification-23] maximum reduction of 2% = max (1%, 2%)
c [simplification-23] geometric conflict interval increment 52903 = 158709 / 3
c [simplification-23] new conflict interval 211612
c [simplification-23] penalized conflict interval 211612 = 1 * 211612
c [simplification-23] hard conflict limit 838477 (soft 732671 + delta 105806)
c [simplification-23] new conflict limit 732671 (hard 838477)
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  687.4   41270   297974    530176   44173   7024 792360   96   430   92  22%    602   38  110   88  124%
c -  712.0   41256   297974    560056   33296   7119 792406   97   399   62  24%    -75    5  117   91  128%
c -  746.6   41256   297974    603103   34837   7272 792466  104   429   94  24%    454   36  108   92  117%
c -  779.8   41256   297974    646434   36187   7383 792510   98   387   95  25%    730    2  107   92  117%
c i  794.2   41255   297974    663906   51614   7439 792534   99   387  144  26%    799    7  111   92  120%
c i  814.0   41251   297974    686913   72168   7502 792563  102   415  197  25%   -629   28   98   94  104%
c -  817.2   41251   297974    690409   36411   7512 792575  101   374   64  27%   -877  -13  103   95  109%
c i  847.8   41250   297974    728569   69442   7580 792607  108   401  173  27%    -45   38  138   96  144%
c -  854.1   41236   297974    735985   37485   7602 792612  105   471   65  22%   -520  103  127   97  131%
c 
c [simplification-24] limit 732671 conflicts (hard 838477) hit after 769188 conflicts
c [quatres-18] found 24014 quaternary clauses 54% in total
c [quatres-18-1] removed 2 duplicate quaternary clauses
c [quatres-18-2] added 5 single-self-subsuming ternary resolvents
c [quatres-18-2] added 1 quaternary resolvents
c [ternres-20] limit 148545756 with penalty 0 = 0 + 0
c [ternres-20] all 41236 free variables schedulable
c [ternres-20] 110 ternary resolvents (7 bin, 103 trn)
c [ternres-20] fully completed ternary resolution
c [decomp-54] removed 36 variables
c [basicprobe-8] limit 400000000 penalty 0 = 0 + 0
c [basicprobe-8-0] 10787 sched 26%, 233 failed, 13 lifted, 118588 hbrs
c [decomp-55] removed 350 variables
c [basicprobe-8-1] 2805 probes remain 7% after last round
c [basicprobe-8-1] 315 units = 301 failed (96%) + 14 lifted (4%)
c [basicprobe-8-1] removed 445 variables, found 141317 hbrs
c [bate-6] eliminated 464 asymmetric tautologies during probing
c [unhide-24] limit 5000000 with penalty 2 = 0 + 2
c [unhide-24-36] 0 units, 0 failed, 46713 tauts, 0 hbrs, 1991901 literals
c [transred-20] limit 2000000 with penalty 0 = 0 + 0
c [transred-20] removed 208 transitive binary clauses
c [bca-20] limit of 10000000 steps and 584081 added (scaled 2)
c [bca-20] 48595 out of 81582 literals actually usable 60%
c [bca-20] added 4 blocked clauses in 170634 steps
c [sort-queue-24] sorted 22222 enqueued variables after 769188 conflicts
c [score-dist-24] active 18568 (46%), one 15761 (39%), zero 6461 (16%)
c [score-dist-24] max exp 825, different 580 (70%)
c [score-dist-24] median active exp 737, avg 652.6
c [simplification-24] removed 446 variables 1.1% (40790 remain 14%)
c [simplification-24] removed 6470 irredundant clauses 2.2% (291504 remain 21%)
c [simplification-24] maximum reduction of 2% = max (1%, 2%)
c [simplification-24] geometric conflict interval increment 70537 = 211612 / 3
c [simplification-24] new conflict interval 282149
c [simplification-24] penalized conflict interval 282149 = 1 * 282149
c [simplification-24] hard conflict limit 1192411 (soft 1051337 + delta 141074)
c [simplification-24] new conflict limit 1051337 (hard 1192411)
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 -  920.1   40790   291504    782138   38343   7673 827892   95   384   65  25%    260    9   39   99   40%
c -  959.0   40790   291504    828690   38652   7789 827929   96   397   99  24%    649   -3   40  103   39%
c -  998.2   40790   291504    878004   40634   7887 827956  105   425  100  25%    847   62   70  101   69%
c
c CAUGHT SIGNAL 15 SIGTERM
c
c s UNKNOWN
c bate: 4011 basic ate = 3002 trn 75% + 1009 lrg 25% in 6 updates
c bcas: 20 count, 1150 added (1364 skipped), 4880112 steps
c bkwd: tried 386576 clauses, 772830 lits, 2.00 lits/clause
c bkwd: checked 12041659 occs, 31.15 occs/clause, 15.58 occs/lit
c bkwd: subsumed 10 binary, 118 ternary, 61 large
c bkwd: strengthened 4 binary, 1 ternary (100% self), 302 large (0% self)
c blkd: 6 bces, 12153 removed, 9442227 resolutions, 26281892 steps
c blkd: 16870 blocking literals 3%, 44 pure
c bump: 877426 bumped seen, 501595483 lits 571.7 on average
c card: 6 count, 0 units, 0 am1, 146918405 steps
c card: 0 rescheduled, 0 eliminated, 0 resolved, 48917 subsumed
c card: 22933 at-most-one constraints found, average size 4.72
c card: 22933 at-most-one constraints used 100%, average size 4.72
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: 7 cces, 24938 eliminated, 24672 ate 99%, 266 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: 4670846 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 166 gcs, 0 rescored clauses, 461 rescored vars
c dcps: 55 decompositions, 76482 equivalent 26%
c deco: 79437 decision-only clauses 9%, 69% reduction
c decs: 14142021 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 17 elims, 88529 eliminated 30%, 13 pure 0%
c elms: 49 rounds, 2.9 rounds/bve
c elms: 59133 small 67%, 29339 large 33%
c elms: 209096 tried small, 59133 succeeded 28%, 149963 failed 72%
c elms: 52354 subsumed, 113002 strengthened, 876 blocked
c elms: 24377034 copies, 23544914 resolutions, 6320319 ipos
c elms: 6809450 subchks, 3594852 strchks
c gaus: 5 extractions, 372 extracted, 2.3 size, 3 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 10232224 steps, 5116112 extr 50%, 4155 elim 0%
c glue: 83.2 orig avg, 83.2 real avg, 7.1 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 2411125 = 283796 simple 12% + 2103327 trn 87% + 24002 lrg 1%, 5775 sub 0%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 877426 clauses, 400.0 length
c lrnd: 350971850 lits = 433993352 orig - 83021502 removed 19%
c lrnd: 411014 uips 47%, 401705 flips 46%
c mins: 758573 mins 89%, 3765 bin 0%, 10369 size 1%
c mins: 765219111 poisoned searches, 160875941 hits, 21% hit rate
c mins: 838756215 used twice searches, 25079176 hits, 3% hit rate
c move: moved 24487, 12983 bin 53%, 11504 trn 47%
c otfs: 2846 driving 29%, 7023 restarting 71%
c otfs: str 9869, 9606 red 97%, 263 irr 3%
c otfs: str 9869, 0 bin 0%, 123 trn 1%, 9746 lrg 99%
c otfs: sub 12, 12 red 100%, 0 irr 0%
c otfs: sub 12, 0 bin 0%, 0 trn 0%, 12 lrg 100%
c phas: 17 computed, 119384 set, 9 pos (0%), 119375 neg (100%)
c prbs: 8 basic, 95409 probed, 3922 failed, 136 lifted
c prbs: 8 simple, 851390 probed, 1055 failed, 2582 eqs
c prbs: 8 treelook, 461 probed, 51 failed, 0 lifted
c prom: 105121 locked 14% out of 740675 tried
c prps: 1914612154 props, 127 props/dec
c prps: 94% srch, 6% simp, 0% lkhd
c quat: 18 count, 291 quat, 32 self1, 1 self2, 1066 dup
c queu: 24 sorted, 14142021 next (677443 steps 0.05)
c queu: 512810639 enq (541333794 steps 1.06), 501595483 deq 98%
c redc: 9560 clauses 38%, 25411 tried 3%, 155 sat 1%
c redc: 22487 lits 10%, 232329 tried 0%, 155 sat 0%
c redc: 1232 times jump level reduced, 53.8 levels on average
c reds: 18 count, 48866.4 conflicts per reduce
c reds: 0 memlim 0%, 18 arith 100%
c reds: 526723 collected 80%, 131797 retired 20%
c rmbd: 47396 removed, 6684 red 14%
c rsts: 21021 restarts 100%, 0 skipped 0%
c rsts: 0 saturating 0%, 0 reuse 0%
c rsts: 0 kept 0.0% average 0.0%
c scnc: 1 count, 1.200 min (200/1000), 1.200 max (200/1000)
c simp: 24 count, 22 confs 92%, 0 vars 0%
c simp: 1 its 4%, 1 bin 4%, 0 trns 0%
c subl: 877426 count (1042398 tried 1.2), 74982 sub out of 864772 (8.7%)
c swps: 12 count, 12 rounds, 1670 queries (139.2/round)
c swps: 1536 sat calls, 22 unsat (0.4% success rate)
c swps: 26982 decisions 17.6, 676 conflicts 0.4
c swps; 2201.2 avg class size, 166.3 avg environment size
c swps: 0 failed, 295 impls, 144 equivs
c swp0: 552 type 0 queries, 149 unsat (27.0%), 537 sat (97.3%)
c swp1: 1118 type 1 queries, 615 unsat (55.0%), 989 sat (88.5%)
c sync: 0 produced units, 0 successful consumptions 0%
c sync: 0 consume units calls, 0 tried 0%, 0 success 0%
c sync: 0 produced clauses, 0 successful consumptions 0%
c sync: 0 consume clause calls, 0 tried 0%, 0 success 0%
c time: 30040626 calls to obtain time
c tops: 93099 fixed 31%, 361 its, 2436.55 confs/it
c trds: 20 transitive reductions, 3538 removed, 54 failed
c trds: 18621 nodes, 52109 edges, 38944504 steps
c trim: 1389463 words, 5.3 MB
c trnr: 20 count, 17 bin, 2854 trn, 240194199 steps
c unhd: 24 count, 36 rounds, 116402224 steps
c unhd: 1356 non-trivial sccs of average size 2.2
c unhd: 71 units, 70 bin, 1 trn, 0 lrg
c unhd: 4391 failed, 4218 stamp, 0 lits, 92 bin, 22 trn, 0 lrg
c unhd: 794431 tauts, 24576 bin 3%, 17323 trn 2%, 955 lrg 0%
c unhd: 794431 tauts, 751577 stamp 95%, 724805 red 91%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 6793368 str, 70 bin 0%, 3090 trn 0%, 6790208 lrg 100%, 6761965 red 100%
c vars: 40790 remaining 14% and 258110 removed 86% out of 298900
c vars: 93099 fixed 31%, 88529 eliminated 30%, 76482 equivalent 26%
c vsts: 17776610903 visits, 94% srch, 6% simp, 0% lkhd
c vsts: 9.3 search visits per propagation, 19022.7 per conflict
c wchs: 2518977733 pushed, 70237548 enlarged, 246 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all         865063        526723        131797      69899954       5715336        317897
c 
c  0 0         21231   2       963   0         0   0  25130455  36    764150  13     24186   8     0.6
c  1 5          5895   1       924   0      1965   1   4981662   7    212967   4      6907   2     0.2
c  2 6         17856   2      5214   1      4760   4  10408136  15<   549960  10     20472   6     0.6
c  3 9         41437   5     20388   4      7920   6   9738725  14    871256  15     40093  13     1.8
c  4 14        75983   9     47278   9     11373   9   8034484  11   1011301  18<    58153  18     3.9
c  5 21        99888  12     69772  13     13586  10   4880684   7    744726  13     47403  15<    7.6
c  6 30       108416  13     79529  15     13796  10   2872899   4    519423   9     36483  11    23.0
c  7 41       105328  12<    78839  15<    13226  10<  1597916   2    327065   6     24579   8    28.8
c  8 54        97254  11     72145  14     12555  10    939057   1    241291   4     19099   6    18.7
c  9 69        82129   9     59976  11     11258   9    515342   1    171442   3     14506   5    17.4
c 10 86        75796   9     51718  10     13693  10    450498   1    142888   3     12984   4    17.3
c 11 126       57490   7     25196   5     11193   8    214852   0     83012   1      7838   2     6.8
c 12 230       64079   7     13119   2     12758  10    119495   0     66939   1      4681   1     7.6
c 13 534       12271   1      1659   0      3714   3     15736   0      8906   0       510   0     2.7
c 14 1526         10   0         3   0         0   0        13   0        10   0         3   0     0.0
c 15 5046          0   0         0   0         0   0         0   0         0   0         0   0     0.0
c 
c avg                  7.2           7.1           7.5           2.3           4.2           5.0
c std                  3.0           2.3           3.1           2.4           2.8           2.8
c 
c   88.912   9% bump
c   84.112   8% probe
c   42.457   4% unhide
c   22.075   2% elim
c   14.887   1% cce
c    9.825   1% sweep
c    9.056   1% decide
c    4.450   0% bca
c 
c   12.316 < 1% rest (below)
c 
c    3.371   0% block
c    2.703   0% transred
c    1.709   0% ternres
c    1.523   0% rescore
c    1.500   0% gauss
c    1.023   0% quatres
c    0.486   0% card
c    0.000   0% locs
c    0.000   0% queuesort
c ==================================
c    4.785   0% preprocessing     2%
c  199.654  20% inprocessing     98%
c ==================================
c  204.439  20% simplifying
c  794.819  80% search
c ==================================
c  999.264 100% all
c 
c        879596 conflicts,         880.2 confs/sec
c          6849 ternaries,         128.4 confs/ternary
c          5260 binaries,          167.2 confs/binary
c           361 iterations,       2436.6 confs/iteration
c 
c            18 reductions,          0.0 redus/sec,  48866.4 confs/reduction
c         21021 restarts,           21.0 rests/sec,     41.8 confs/restart
c      14142021 decisions,       14152.4 decis/sec,     16.1 decis/conflict
c    1914612154 propagations,  1916022.3 props/sec,    135.4 props/decision
c 
c 999.3 seconds, 238.4 MB
c
c CAUGHT SIGNAL 15 SIGTERM
c
c launch: done
