c launch: /data/cnf/sc2014/app/dated-10-13-u.cnf.bz2
c host: atom22
c Lingeling SAT Solver
c 
c Version b7ztzud 55d9a3e9649fc56eacf3e72d8e2e2d5c615d5f18
c 
c Copyright (C) 2010-2014 Armin Biere JKU Linz Austria.
c All rights reserved.
c 
c released Fri May  1 11:44:04 CEST 2015
c compiled Fri May  1 11:44:04 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-49-generic x86_64
c 
c piping '/data/cnf/sc2014/app/dated-10-13-u.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/dated-10-13-u.cnf.bz2
c no embedded options
c found 'p cnf 180608 815261' header
c read 180608 variables, 815261 clauses, 1862226 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 --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 --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 172976 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 [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  172976   800029         0       0      0     0    0     0   34   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 10630 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] 10630 out of 10630 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 87203 variables
c [simpleprobe-1] all 93405 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 61509 variables
c [simpleprobe-1] fully completed simple probing
c [simpleprobe-1] removed 61509 variables, found 8077 hbrs, 953 units
c [unhide-1] limit 100000 with penalty 0 = 0 + 0
c [unhide-1-1] 0 units, 598 failed, 5905 tauts, 0 hbrs, 271 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 31023 variables 100%
c [elim-1] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-1] rescheduling of touched variables disabled
c [elim-1-1] eliminated 11526 variables 37% in round 1 in 12273088 steps
c [elim-1-1] backward subsumption/strengthening limit 7726912
c [elim-1-1-1] backward checking 20321 touched variables 66%
c [elim-1-1-1] fully completed backward checking in 1 rounds
c [elim-1-1] subsumed 65 and strengthened 198 clauses in 2428622 steps
c [elim-1-1] rescheduled 489 variables 2% by backward subsumption
c [elim-1-2] eliminated 114 variables 0% in round 2 in 260506 steps
c [elim-1-2] backward subsumption/strengthening limit 260500
c [elim-1-2-1] backward checking 515 touched variables 2%
c [elim-1-2-1] incomplete backward checking 0 remain 0%
c [elim-1-2] subsumed 62 and strengthened 49 clauses in 260501 steps
c [elim-1-2] rescheduled 191 variables 1% by backward subsumption
c [elim-1-3] eliminated 51 variables 0% in round 3 in 105347 steps
c [elim-1-3] backward subsumption/strengthening limit 105300
c [elim-1-3-1] backward checking 220 touched variables 1%
c [elim-1-3-1] incomplete backward checking 0 remain 0%
c [elim-1-3] subsumed 48 and strengthened 31 clauses in 105301 steps
c [elim-1] incomplete 132 not tried 0% in round 3
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 11798 = 38% variables out of 31023 scheduled
c [elim-1] considered successful since not run to completion yet
c [phase-count-1] 139013 negative 99.0% of 140400 except 1387 1.0%
c [phase-count-1] 117578 positive 83.7% of 140400 except 22822 16.3%
c [phase-count-1] less non-negative clauses 1387 than limit 14000 (10.0%)
c [phase-count-1] non-pos/non-neg = 22822/1387 = 16.45 >= 2.00 = 200/100
c [lucky-phase-1] forcing lucky phase -1
c [phase-1] phase bias: 0 positive 0%, 19225 negative 100%
c [score-distribution-1] 0 pos 0.00%, 0 min 0.00%, 19225 zero 100.00%
c [score-distribution-1] 1 different 0.01% out of total 19225 variables
c [simplification-1] removed 118677 variables 86.1% (19225 remain 11%)
c [simplification-1] removed 659629 irredundant clauses 82.5% (140400 remain 18%)
c [simplification-1] maximum reduction of 86% = max (86%, 82%)
c [simplification-1] large reduction 86% >= 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    1.8   19224   140400       292     253      9  6263    1     5   13  11%      1    5    6    0 15334%
c i    1.8   19223   140400       325     281      9  6263    1     5   13  13%      1    5    7    0 15857%
c i    1.8   19220   140400       330     285      9  6263    1     5   13  13%      1    5    7    0 15683%
c i    1.8   19219   140400       331     285      9  6263    1     5   13  13%      1    5    7    0 15622%
c i    1.9   19216   140400       572     502     13  6273    1     8   13  15%      1    8    8    0 10386%
c i    1.9   19213   140400       602     527     15  6274    1     8   13  15%      1    8    8    0 10065%
c i    1.9   19210   140400       619     535     17  6280    1     8   13  15%      1    8    8    0 9496%
c i    2.0   18195   140400       712     612     22  6289    1     9   13  16%      1    9    8    0 8101%
c i    2.0   18194   140400       769     653     25  6296    2     9   13  17%      1    9    9    0 8638%
c i    2.0   18185   140400       780     661     25  6298    2     9   13  18%      1    9    9    0 8575%
c 
c [simplification-2] limit of 10 iterations hit after 10 iterations
c [decomp-3] removed 1238 variables
c [simpleprobe-2] all 17987 free variables schedulable
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [decomp-4] removed 1208 variables
c [simpleprobe-2] 6896 variables remain 41% (9883 retained 59%)
c [simpleprobe-2] removed 1208 variables, found 2187 hbrs, 350 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 31477 literals 94%
c [treelook-1] scheduling used 300002 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 315032 steps
c [treelook-1] 31468 literals remain 94%
c [treelook-1] 16774 variables remain to probed next time 100%
c [treelook-1] removed 3 variables, found 3585 hbrs
c [basicprobe-1] limit 1000000 penalty 0 = 0 + 0
c [basicprobe-1-0] 2395 probes remain 14% after last round
c [basicprobe-1-0] 9 units = 9 failed (100%) + 0 lifted (0%)
c [basicprobe-1-0] removed 16 variables, found 4655 hbrs
c [unhide-2] limit 100000 with penalty 0 = 0 + 0
c [unhide-2-2] 2 units, 207 failed, 3219 tauts, 0 hbrs, 2078 literals
c [elim-2] no untried remaining variables left
c [elim-2] scheduled 16376 variables 100%
c [elim-2] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-2] rescheduling of touched variables disabled
c [elim-2-1] eliminated 1182 variables 7% in round 1 in 8523752 steps
c [elim-2-1] backward subsumption/strengthening limit 8523700
c [elim-2-1-1] backward checking 4398 touched variables 27%
c [elim-2-1-1] fully completed backward checking in 1 rounds
c [elim-2-1] subsumed 70 and strengthened 85 clauses in 813331 steps
c [elim-2-1] rescheduled 375 variables 2% by backward subsumption
c [elim-2-2] eliminated 76 variables 0% in round 2 in 210260 steps
c [elim-2-2] backward subsumption/strengthening limit 210200
c [elim-2-2-1] backward checking 279 touched variables 2%
c [elim-2-2-1] fully completed backward checking in 1 rounds
c [elim-2-2] subsumed 14 and strengthened 21 clauses in 77857 steps
c [elim-2-2] rescheduled 73 variables 0% by backward subsumption
c [elim-2-3] eliminated 23 variables 0% in round 3 in 35802 steps
c [elim-2-3] backward subsumption/strengthening limit 35800
c [elim-2-3-1] backward checking 100 touched variables 1%
c [elim-2-3-1] incomplete backward checking 0 remain 0%
c [elim-2-3] subsumed 17 and strengthened 9 clauses in 35801 steps
c [elim-2] incomplete 39 not tried 0% in round 3
c [elim-2] transition to [ all 1 rem 1 ] state
c [elim-2] eliminated 1354 = 8% variables out of 16376 scheduled
c [elim-2] considered successful since not run to completion yet
c [phase-count-2] 107612 negative 99.0% of 108681 except 1069 1.0%
c [phase-count-2] 88785 positive 81.7% of 108681 except 19896 18.3%
c [phase-count-2] less non-negative clauses 1069 than limit 10800 (10.0%)
c [phase-count-2] non-pos/non-neg = 19896/1069 = 18.61 >= 2.00 = 200/100
c [lucky-phase-2] forcing lucky phase -1
c [phase-2] phase bias: 0 positive 0%, 104 negative 100%
c [score-distribution-2] 5946 pos 39.58%, 0 min 0.00%, 9076 zero 60.42%
c [score-distribution-2] 1330 different 8.85% out of total 15022 variables
c [simplification-2] removed 3161 variables 17.4% (15022 remain 9%)
c [simplification-2] removed 31719 irredundant clauses 22.6% (108681 remain 14%)
c [simplification-2] maximum reduction of 23% = max (17%, 23%)
c [simplification-2] forced so keeping old conflict interval 0
c [simplification-2] conflict limit remains at 1012 (hard 11000)
c [simplification-2] new iteration interval 100
c 
c [simplification-3] limit 1012 conflicts (hard 11000) hit after 1012 conflicts
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 5143 at-most-one constraints of average size 3.6
c [card-2] no at-most-two constraint found
c [card-2] using previous limit 1000000 for elimination
c [card-2] 5143 out of 5143 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [decomp-6] removed 24 variables
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] scheduled 29132 literals 97%
c [treelook-2] scheduling used 300024 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] used 351170 steps
c [treelook-2] 29093 literals remain 97%
c [treelook-2] 14992 variables remain to probed next time 100%
c [decomp-7] removed 27 variables
c [treelook-2] removed 32 variables, found 2969 hbrs
c [unhide-3] limit 100000 with penalty 0 = 0 + 0
c [unhide-3-3] 0 units, 148 failed, 5011 tauts, 0 hbrs, 658 literals
c [elim-3] no untried remaining variables left
c [elim-3] scheduled 14836 variables 100%
c [elim-3] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-3] rescheduling of touched variables disabled
c [elim-3-1] eliminated 451 variables 3% in round 1 in 7742521 steps
c [elim-3-1] backward subsumption/strengthening limit 7742500
c [elim-3-1-1] backward checking 2169 touched variables 15%
c [elim-3-1-1] fully completed backward checking in 1 rounds
c [elim-3-1] subsumed 39 and strengthened 33 clauses in 396608 steps
c [elim-3-1] rescheduled 170 variables 1% by backward subsumption
c [elim-3-2] eliminated 46 variables 0% in round 2 in 108035 steps
c [elim-3-2] backward subsumption/strengthening limit 108000
c [elim-3-2-1] backward checking 223 touched variables 2%
c [elim-3-2-1] fully completed backward checking in 1 rounds
c [elim-3-2] subsumed 27 and strengthened 25 clauses in 61024 steps
c [elim-3-2] rescheduled 81 variables 1% by backward subsumption
c [elim-3-3] eliminated 25 variables 0% in round 3 in 54135 steps
c [elim-3-3] backward subsumption/strengthening limit 54100
c [elim-3-3-1] backward checking 97 touched variables 1%
c [elim-3-3-1] fully completed backward checking in 1 rounds
c [elim-3-3] subsumed 26 and strengthened 5 clauses in 39035 steps
c [elim-3] incomplete 37 not tried 0% in round 3
c [elim-3] transition to [ all 1 rem 1 ] state
c [elim-3] eliminated 562 = 4% variables out of 14836 scheduled
c [elim-3] considered successful since not run to completion yet
c [phase-count-3] 99461 negative 99.0% of 100453 except 992 1.0%
c [phase-count-3] 82874 positive 82.5% of 100453 except 17579 17.5%
c [phase-count-3] less non-negative clauses 992 than limit 10000 (10.0%)
c [phase-count-3] non-pos/non-neg = 17579/992 = 17.72 >= 2.00 = 200/100
c [lucky-phase-3] forcing lucky phase -1
c [phase-3] phase bias: 0 positive 0%, 55 negative 100%
c [score-distribution-3] 6273 pos 43.95%, 0 min 0.00%, 8001 zero 56.05%
c [score-distribution-3] 1881 different 13.18% out of total 14274 variables
c [simplification-3] removed 748 variables 5.0% (14274 remain 8%)
c [simplification-3] removed 8228 irredundant clauses 7.6% (100453 remain 13%)
c [simplification-3] maximum reduction of 8% = max (5%, 8%)
c [simplification-3] large reduction 8% >= 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 13012 (soft 3012 + delta 10000)
c [simplification-3] new conflict limit 3012 (hard 13012)
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    3.4   14273   100453      1118     781     20  7867    3    13   11  19%      1   13   12    0 6913%
c i    3.5   14272   100453      1439    1079     26  7873    4    16   11  22%      2   16   14    0 5623%
c i    3.6   14271   100453      1754    1363     35  7877    5    20   11  24%      2   20   18    0 5020%
c i    3.8   14269   100453      2315    1885     45  7886    6    25   12  25%      3   25   16    0 3239%
c i    3.8   14268   100453      2332    1900     45  7887    6    25   12  25%      3   25   16    1 3114%
c 
c [simplification-4] limit 3012 conflicts (hard 13012) hit after 3012 conflicts
c [decomp-8] removed 15 variables
c [basicprobe-2] limit 2111058 penalty 0 = 0 + 0
c [basicprobe-2-0] 2167 probes remain 15% after last round
c [basicprobe-2-0] 27 units = 27 failed (100%) + 0 lifted (0%)
c [basicprobe-2-0] removed 91 variables, found 6772 hbrs
c [unhide-4] limit 100000 with penalty 0 = 0 + 0
c [unhide-4-4] 0 units, 169 failed, 1372 tauts, 0 hbrs, 2528 literals
c [elim-4] no untried remaining variables left
c [elim-4] scheduled 14046 variables 100%
c [elim-4] boosting limit by 20
c [elim-4] limit of 400000000 steps penalty 0 = 0 + 0
c [elim-4] rescheduling of touched variables disabled
c [elim-4-1] eliminated 211 variables 2% in round 1 in 7224929 steps
c [elim-4-1] backward subsumption/strengthening limit 7224900
c [elim-4-1-1] backward checking 1062 touched variables 8%
c [elim-4-1-1] fully completed backward checking in 1 rounds
c [elim-4-1] subsumed 18 and strengthened 12 clauses in 204936 steps
c [elim-4-1] rescheduled 68 variables 0% by backward subsumption
c [elim-4-2] eliminated 10 variables 0% in round 2 in 54934 steps
c [elim-4-2] backward subsumption/strengthening limit 54900
c [elim-4-2-1] backward checking 71 touched variables 1%
c [elim-4-2-1] fully completed backward checking in 1 rounds
c [elim-4-2] subsumed 8 and strengthened 8 clauses in 38202 steps
c [elim-4-2] rescheduled 31 variables 0% by backward subsumption
c [elim-4-3] eliminated 12 variables 0% in round 3 in 19992 steps
c [elim-4-3] backward subsumption/strengthening limit 19900
c [elim-4-3-1] backward checking 60 touched variables 0%
c [elim-4-3-1] incomplete backward checking 0 remain 0%
c [elim-4-3] subsumed 10 and strengthened 2 clauses in 19901 steps
c [elim-4] incomplete 26 not tried 0% in round 3
c [elim-4] transition to [ all 1 rem 1 ] state
c [elim-4] eliminated 268 = 2% variables out of 14046 scheduled
c [elim-4] considered successful since not run to completion yet
c [phase-count-4] 95693 negative 99.0% of 96629 except 936 1.0%
c [phase-count-4] 78943 positive 81.7% of 96629 except 17686 18.3%
c [phase-count-4] less non-negative clauses 936 than limit 9600 (10.0%)
c [phase-count-4] non-pos/non-neg = 17686/936 = 18.90 >= 2.00 = 200/100
c [lucky-phase-4] forcing lucky phase -1
c [phase-4] phase bias: 0 positive 0%, 46 negative 100%
c [score-distribution-4] 7255 pos 52.66%, 0 min 0.00%, 6523 zero 47.34%
c [score-distribution-4] 2364 different 17.16% out of total 13778 variables
c [simplification-4] removed 489 variables 3.4% (13778 remain 8%)
c [simplification-4] removed 3824 irredundant clauses 3.8% (96629 remain 12%)
c [simplification-4] maximum reduction of 4% = max (3%, 4%)
c [simplification-4] geometric conflict interval increment 4000 = 20000 / 5
c [simplification-4] new conflict interval 4000
c [simplification-4] penalized conflict interval 4000 = 1 * 4000
c [simplification-4] hard conflict limit 17012 (soft 7012 + delta 10000)
c [simplification-4] new conflict limit 7012 (hard 17012)
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    4.6   13777    96629      3013    2409     50 11498    9    32   11  27%      4   31   22    1 3015%
c i    4.6   13773    96629      3145    2535     52 11499    9    34   12  28%      4   33   25    1 3212%
c i    4.7   13770    96629      3147    2535     52 11499    9    34   12  28%      4   33   25    1 3191%
c i    4.7   13769    96629      3152    2538     52 11499    9    34   12  28%      4   33   25    1 3168%
c i    4.7   13768    96629      3173    2542     53 11500    9    34   12  28%      4   33   24    1 3072%
c i    4.7   13767    96629      3358    2704     56 11506   10    36   12  29%      3   35   27    1 3142%
c i    4.9   13766    96629      3833    3144     60 11511   12    41   12  29%      4   40   23    1 2258%
c i    5.0   13765    96629      4027    3323     62 11513   12    43   13  29%      3   42   22    1 2020%
c i    5.1   13764    96629      4296    3581     63 11515   13    46   13  29%      3   44   26    1 2131%
c i    5.2   13761    96629      4574    3827     66 11516   14    47   13  29%      3   45   21    1 1671%
c i    5.2   12970    96629      4660    3907     67 11517   14    47   13  29%      3   45   19    1 1441%
c i    5.4   12966    96629      5033    4237     73 11527   15    49   13  31%      3   47   29    1 1947%
c i    5.5   12962    96629      5472    4649     76 11530   16    50   13  32%      3   48   24    2 1507%
c i    5.8   12961    96629      6134    5280     83 11533   17    53   13  32%      4   50   24    2 1300%
c 
c [simplification-5] limit 7019 conflicts (hard 17012) hit after 7019 conflicts
c [quatres-1] found 6125 quaternary clauses 73% in total
c [quatres-1-2] added 13 quaternary resolvents
c [ternres-1] boosting ternary resolution limit by 5
c [ternres-1] limit 20000000 with penalty 0 = 0 + 0
c [ternres-1] all 12961 free variables schedulable
c [ternres-1] 170 ternary resolvents (0 bin, 170 trn)
c [ternres-1] fully completed ternary resolution
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 644 xors of average arity 2.2
c [gauss-1] connected 1423 occurrences of 408 variables (average 3.5)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] fully completed
c [gauss-1] exported 0 unary, 0 binary and 1 ternary equations
c [decomp-9] removed 127 variables
c [simpleprobe-3] 5034 schedulable variables 39%
c [simpleprobe-3] limit 3909086 penalty 0 = 0 + 0
c [decomp-10] removed 324 variables
c [simpleprobe-3] 221 variables remain 2% (12289 retained 98%)
c [simpleprobe-3] removed 324 variables, found 6720 hbrs, 103 units
c [unhide-5] limit 195454 with penalty 0 = 0 + 0
c [unhide-5-5] 1 units, 64 failed, 4976 tauts, 0 hbrs, 6128 literals
c [transred-1] limit 977271 with penalty 0 = 0 + 0
c [transred-1] removed 319 transitive binary clauses
c [transred-1] found 13 units
c [block-1] scheduling all variables this time
c [block-1] scheduled 12404 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 525 blocked clauses
c [block-1] 525 < 1/100 * 82154 = 821 considered unsuccessful
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 1 clauses out of 2 (50%) of length 8
c [cce-1-1] eliminated 2 clauses out of 37 (5%) of length 7
c [cce-1-1] eliminated 49 clauses out of 360 (14%) of length 6
c [cce-1-1] eliminated 207 clauses out of 1050 (20%) of length 5
c [cce-1-1] eliminated 2503 clauses out of 5585 (45%) of length 4
c [cce-1-1] completed large round (ATE)
c [cce-1-1] eliminated 2762 large clauses in 24490002 steps
c [cce-1-1] allowing another 12245001 steps for small clauses
c [cce-1-1] scheduling 57315 clauses = 43609 binary + 13706 ternary
c [cce-1-1] tried to eliminate 1894 small clauses 3%
c [cce-1-1] eliminated 542 binary clauses 1%
c [cce-1-1] eliminated 101 ternary clauses 1%
c [cce-1-1] eliminated 643 small clauses 1%
c [cce-1-1] eliminated 643 small clauses in 30000003 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 3405 covered clauses in round 1
c [cce-1] eliminated 3405 covered clauses in TOTAL during 1 rounds
c [elim-5] no untried remaining variables left
c [elim-5] scheduled 12404 variables 100%
c [elim-5] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5-1] eliminated 1318 variables 11% in round 1 in 5336222 steps
c [elim-5-1] backward subsumption/strengthening limit 5336200
c [elim-5-1-1] backward checking 3993 touched variables 32%
c [elim-5-1-1] fully completed backward checking in 1 rounds
c [elim-5-1] subsumed 13 and strengthened 41 clauses in 586844 steps
c [elim-5-1] rescheduled 171 variables 1% by backward subsumption
c [elim-5-2] eliminated 48 variables 0% in round 2 in 65018 steps
c [elim-5-2] backward subsumption/strengthening limit 65000
c [elim-5-2-1] backward checking 207 touched variables 2%
c [elim-5-2-1] fully completed backward checking in 1 rounds
c [elim-5-2] subsumed 13 and strengthened 16 clauses in 42500 steps
c [elim-5-2] rescheduled 54 variables 0% by backward subsumption
c [elim-5-3] eliminated 13 variables 0% in round 3 in 21089 steps
c [elim-5-3] backward subsumption/strengthening limit 21000
c [elim-5-3-1] backward checking 66 touched variables 1%
c [elim-5-3-1] incomplete backward checking 0 remain 0%
c [elim-5-3] subsumed 3 and strengthened 7 clauses in 21001 steps
c [elim-5] incomplete 15 not tried 0% in round 3
c [elim-5] transition to [ all 1 rem 1 ] state
c [elim-5] eliminated 1391 = 11% variables out of 12404 scheduled
c [bca-1] limit of 10000000 steps and 149444 added (scaled 2)
c [bca-1] 18117 out of 22028 literals actually usable 82%
c [bca-1] added 14 blocked clauses in 41616 steps
c [sweep-1] limit 1000000 penalty 0 = 0 + 0
c [sweep-1-1] 1846 pos 16.8% + 9167 neg 83.2% = 11013 sched 100.0% ret 0
c [sweep-1-1] 1004947 steps 23 queries 1107.48 avg class size
c [sweep-1-1] 193 decisions 20 SAT calls 99.75 avg env size
c [sweep-1-1] 10631 variables remain 97% (378 retained 3%)
c [decomp-11] removed 10 variables
c [sweep-1-1] removed 10 vars (0 failed, 2 eqs, 6 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 10 vars in TOTAL (1 rounds, 22 queries)
c [phase-count-5] 73876 negative 99.3% of 74413 except 537 0.7%
c [phase-count-5] 60595 positive 81.4% of 74413 except 13818 18.6%
c [phase-count-5] less non-negative clauses 537 than limit 7400 (10.0%)
c [phase-count-5] non-pos/non-neg = 13818/537 = 25.73 >= 2.00 = 200/100
c [lucky-phase-5] forcing lucky phase -1
c [phase-5] phase bias: 0 positive 0%, 29 negative 100%
c [score-distribution-5] 5965 pos 54.21%, 491 min 4.46%, 4547 zero 41.33%
c [score-distribution-5] 2504 different 22.76% out of total 11003 variables
c [simplification-5] removed 1958 variables 15.1% (11003 remain 6%)
c [simplification-5] removed 22216 irredundant clauses 23.0% (74413 remain 9%)
c [simplification-5] maximum reduction of 23% = max (15%, 23%)
c [simplification-5] large reduction 23% >= 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 19019 (soft 9019 + delta 10000)
c [simplification-5] new conflict limit 9019 (hard 19019)
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.1   11002    74413      7483    4505    307 14721   21    62   12  34%     10   58   28    2 1136%
c i    8.2   10999    74413      7516    4535    308 14722   21    62   12  34%     10   58   27    2 1090%
c i    8.2   10997    74413      7517    4535    308 14722   21    62   12  34%     10   58   26    2 1085%
c i    8.2   10996    74413      7522    4534    310 14722   21    62   12  34%     10   58   26    2 1070%
c i    8.6   10691    74413      8887    5801    325 14730   23    66   12  35%     12   61   26    3  872%
c 
c [simplification-6] limit 9031 conflicts (hard 19019) hit after 9031 conflicts
c [quatres-2] found 3249 quaternary clauses 62% in total
c [quatres-2-1] removed 2 duplicate quaternary clauses
c [quatres-2-2] added 3 quaternary resolvents
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] all 10688 free variables schedulable
c [ternres-2] 107 ternary resolvents (0 bin, 107 trn)
c [ternres-2] fully completed ternary resolution
c [card-3] limit 500000 penalty 2 = 2 + 0
c [card-3] found 2625 at-most-one constraints of average size 3.5
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 500000 for elimination
c [card-3] 2625 out of 2625 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [gauss-2] limit 2000000 penalty 0 = 0 + 0
c [gauss-2] extracted 286 xors of average arity 2.2
c [gauss-2] connected 624 occurrences of 170 variables (average 3.7)
c [gauss-2] limit 2000000 penalty 0 = 0 + 0
c [gauss-2] fully completed
c [decomp-12] removed 66 variables
c [gauss-2] exported 0 unary, 4 binary and 0 ternary equations
c [treelook-3] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-3] scheduled 21243 literals 100%
c [treelook-3] scheduling used 264794 steps
c [treelook-3] scheduled completely
c [treelook-3] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-3] used 320935 steps
c [treelook-3] 21224 literals remain 100%
c [treelook-3] 10616 variables remain to probed next time 100%
c [treelook-3] removed 5 variables, found 3072 hbrs
c [unhide-6] limit 244399 with penalty 0 = 0 + 0
c [unhide-6-6] 7 units, 254 failed, 3088 tauts, 0 hbrs, 7835 literals
c [transred-2] limit 1221997 with penalty 0 = 0 + 0
c [transred-2] removed 466 transitive binary clauses
c [transred-2] found 6 units
c [cce-2] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-2-1] eliminated 4 clauses out of 334 (1%) of length 6
c [cce-2-1] eliminated 51 clauses out of 958 (5%) of length 5
c [cce-2-1] eliminated 423 clauses out of 3142 (13%) of length 4
c [cce-2-1] completed large round (ATE)
c [cce-2-1] eliminated 478 large clauses in 18048802 steps
c [cce-2-1] allowing another 9024401 steps for small clauses
c [cce-2-1] scheduling 50889 clauses = 38996 binary + 11893 ternary
c [cce-2-1] tried to eliminate 2300 small clauses 5%
c [cce-2-1] eliminated 673 binary clauses 2%
c [cce-2-1] eliminated 103 ternary clauses 1%
c [cce-2-1] eliminated 776 small clauses 2%
c [cce-2-1] eliminated 2360 small clauses in 30000001 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 2838 covered clauses in round 1
c [cce-2] eliminated 2838 covered clauses in TOTAL during 1 rounds
c [elim-6] no untried remaining variables left
c [elim-6] scheduled 10448 variables 100%
c [elim-6] limit of 24439956 steps penalty 0 = 0 + 0
c [elim-6] rescheduling of touched variables disabled
c [elim-6-1] eliminated 441 variables 4% in round 1 in 4658156 steps
c [elim-6-1] backward subsumption/strengthening limit 4658100
c [elim-6-1-1] backward checking 1805 touched variables 17%
c [elim-6-1-1] fully completed backward checking in 1 rounds
c [elim-6-1] subsumed 6 and strengthened 23 clauses in 280579 steps
c [elim-6-1] rescheduled 80 variables 1% by backward subsumption
c [elim-6-2] eliminated 11 variables 0% in round 2 in 30118 steps
c [elim-6-2] backward subsumption/strengthening limit 30100
c [elim-6-2-1] backward checking 59 touched variables 1%
c [elim-6-2-1] fully completed backward checking in 1 rounds
c [elim-6-2] subsumed 1 and strengthened 4 clauses in 15911 steps
c [elim-6-2] rescheduled 16 variables 0% by backward subsumption
c [elim-6-3] no variable eliminated in round 3 in 8601 steps
c [elim-6] fully completed in 3 rounds
c [elim-6] transition to [ all 0 rem 0 ] state
c [elim-6] eliminated 458 = 4% variables out of 10448 scheduled
c [bca-2] limit of 10000000 steps and 135021 added (scaled 2)
c [bca-2] 15896 out of 19982 literals actually usable 80%
c [bca-2] added 16 blocked clauses in 38596 steps
c [sweep-2] limit 1000000 penalty 0 = 0 + 0
c [sweep-2-1] 1560 pos 16.2% + 8098 neg 83.8% = 9658 sched 96.7% ret 332
c [sweep-2-1] 1002633 steps 21 queries 1112.57 avg class size
c [sweep-2-1] 161 decisions 19 SAT calls 97.89 avg env size
c [sweep-2-1] 9370 variables remain 94% (609 retained 6%)
c [decomp-15] removed 13 variables
c [sweep-2-1] removed 13 vars (0 failed, 2 eqs, 7 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 13 vars in TOTAL (1 rounds, 20 queries)
c [phase-count-6] 66674 negative 99.3% of 67138 except 464 0.7%
c [phase-count-6] 54462 positive 81.1% of 67138 except 12676 18.9%
c [phase-count-6] less non-negative clauses 464 than limit 6700 (10.0%)
c [phase-count-6] non-pos/non-neg = 12676/464 = 27.32 >= 2.00 = 200/100
c [lucky-phase-6] forcing lucky phase -1
c [phase-6] phase bias: 0 positive 0%, 15 negative 100%
c [score-distribution-6] 5522 pos 55.35%, 485 min 4.86%, 3970 zero 39.79%
c [score-distribution-6] 2187 different 21.92% out of total 9977 variables
c [simplification-6] removed 711 variables 6.7% (9977 remain 6%)
c [simplification-6] removed 7275 irredundant clauses 9.8% (67138 remain 8%)
c [simplification-6] maximum reduction of 10% = max (7%, 10%)
c [simplification-6] large reduction 10% >= 5% limit
c [simplification-6] next conflict interval 2000 = 2000/1
c [simplification-6] penalized conflict interval 2000 = 1 * 2000
c [simplification-6] hard conflict limit 21031 (soft 11031 + delta 10000)
c [simplification-6] new conflict limit 11031 (hard 21031)
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   10.6    9976    67138      9970    6517    414 13825   24    68   13  35%     10   62   25    3  734%
c i   10.8    9975    67138     10835    7351    416 13828   24    68   13  35%      8   61   23    4  628%
c i   10.9    9974    67138     10841    7356    416 13828   24    68   13  35%      8   61   23    4  620%
c i   10.9    9969    67138     10905    7416    417 13830   24    68   13  35%      8   61   23    4  628%
c i   10.9    9968    67138     10906    7416    417 13830   24    68   13  35%      8   61   23    4  626%
c 
c [simplification-7] limit 11042 conflicts (hard 21031) hit after 11043 conflicts
c [quatres-3] found 2893 quaternary clauses 58% in total
c [quatres-3-1] removed 1 duplicate quaternary clauses
c [quatres-3-2] added 1 quaternary resolvents
c [ternres-3] limit 4000000 with penalty 0 = 0 + 0
c [ternres-3] all 9968 free variables schedulable
c [ternres-3] 80 ternary resolvents (0 bin, 80 trn)
c [ternres-3] fully completed ternary resolution
c [gauss-3] limit 2000000 penalty 0 = 0 + 0
c [gauss-3] extracted 46 xors of average arity 2.9
c [gauss-3] connected 134 occurrences of 59 variables (average 2.3)
c [gauss-3] limit 2000000 penalty 0 = 0 + 0
c [gauss-3] fully completed
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [basicprobe-3] limit 7286379 penalty 0 = 0 + 0
c [basicprobe-3-0] 1422 probes remain 15% after last round
c [basicprobe-3-0] 136 units = 127 failed (93%) + 9 lifted (7%)
c [basicprobe-3-0] removed 201 variables, found 16336 hbrs
c [bate-1] eliminated 62 asymmetric tautologies during probing
c [unhide-7] limit 291455 with penalty 0 = 0 + 0
c [unhide-7-7] 4 units, 109 failed, 1747 tauts, 0 hbrs, 6027 literals
c [transred-3] limit 1457275 with penalty 0 = 0 + 0
c [transred-3] removed 467 transitive binary clauses
c [transred-3] found 7 units
c [block-2] scheduling all variables this time
c [block-2] scheduled 9703 variables 100%
c [block-2] limit of 25000000 steps penalty 1 = 1 + 0
c [block-2] fully completed
c [block-2] transition to [ all 0 rem 0 ] state
c [block-2] eliminated 133 blocked clauses
c [block-2] 133 < 1/100 * 62787 = 627 considered unsuccessful
c [cce-3] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 10
c [cce-3-1] eliminated 3 clauses out of 49 (6%) of length 7
c [cce-3-1] eliminated 7 clauses out of 301 (2%) of length 6
c [cce-3-1] eliminated 33 clauses out of 904 (4%) of length 5
c [cce-3-1] eliminated 154 clauses out of 2570 (6%) of length 4
c [cce-3-1] completed large round (ACCE)
c [cce-3-1] eliminated 198 large clauses in 13640829 steps
c [cce-3-1] allowing another 6820414 steps for small clauses
c [cce-3-1] scheduling 45792 clauses = 35169 binary + 10623 ternary
c [cce-3-1] tried to eliminate 2716 small clauses 6%
c [cce-3-1] eliminated 794 binary clauses 2%
c [cce-3-1] eliminated 122 ternary clauses 1%
c [cce-3-1] eliminated 916 small clauses 2%
c [cce-3-1] eliminated 916 small clauses in 30000005 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 1114 covered clauses in round 1
c [cce-3] eliminated 1114 covered clauses in TOTAL during 1 rounds
c [elim-7] scheduling all variables this time
c [elim-7] scheduled 9701 variables 100%
c [elim-7] limit of 29145517 steps penalty 0 = 0 + 0
c [elim-7] rescheduling of touched variables disabled
c [elim-7-1] eliminated 450 variables 5% in round 1 in 4084442 steps
c [elim-7-1] backward subsumption/strengthening limit 4084400
c [elim-7-1-1] backward checking 2290 touched variables 24%
c [elim-7-1-1] fully completed backward checking in 1 rounds
c [elim-7-1] subsumed 0 and strengthened 7 clauses in 347253 steps
c [elim-7-1] rescheduled 22 variables 0% by backward subsumption
c [elim-7-2] eliminated 4 variables 0% in round 2 in 7971 steps
c [elim-7-2] backward subsumption/strengthening limit 7900
c [elim-7-2-1] backward checking 20 touched variables 0%
c [elim-7-2-1] incomplete backward checking 0 remain 0%
c [elim-7-2] subsumed 3 and strengthened 1 clauses in 7901 steps
c [elim-7-2] rescheduled 6 variables 0% by backward subsumption
c [elim-7-3] eliminated 3 variables 0% in round 3 in 2788 steps
c [elim-7-3] backward subsumption/strengthening limit 2700
c [elim-7-3-1] backward checking 23 touched variables 0%
c [elim-7-3-1] incomplete backward checking 3 remain 13%
c [elim-7-3] subsumed 2 and strengthened 2 clauses in 2730 steps
c [elim-7] incomplete 7 not tried 0% in round 3
c [elim-7] transition to [ all 1 rem 1 ] state
c [elim-7] eliminated 460 = 5% variables out of 9701 scheduled
c [bca-3] limit of 10000000 steps and 121041 added (scaled 2)
c [bca-3] 14444 out of 18484 literals actually usable 78%
c [bca-3] added 26 blocked clauses in 36646 steps
c [sweep-3] limit 1000000 penalty 0 = 0 + 0
c [sweep-3-1] 1464 pos 16.9% + 7220 neg 83.1% = 8684 sched 94.0% ret 557
c [sweep-3-1] 1031425 steps 16 queries 1050.69 avg class size
c [sweep-3-1] 383 decisions 14 SAT calls 195.71 avg env size
c [sweep-3-1] 8562 variables remain 93% (669 retained 7%)
c [decomp-17] removed 18 variables
c [sweep-3-1] removed 18 vars (0 failed, 2 eqs, 3 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 18 vars in TOTAL (1 rounds, 15 queries)
c [phase-count-7] 59715 negative 99.3% of 60144 except 429 0.7%
c [phase-count-7] 49051 positive 81.6% of 60144 except 11093 18.4%
c [phase-count-7] less non-negative clauses 429 than limit 6000 (10.0%)
c [phase-count-7] non-pos/non-neg = 11093/429 = 25.86 >= 2.00 = 200/100
c [lucky-phase-7] forcing lucky phase -1
c [phase-7] phase bias: 0 positive 0%, 12 negative 100%
c [score-distribution-7] 5456 pos 59.16%, 307 min 3.33%, 3460 zero 37.51%
c [score-distribution-7] 2287 different 24.80% out of total 9223 variables
c [simplification-7] removed 745 variables 7.5% (9223 remain 5%)
c [simplification-7] removed 6994 irredundant clauses 10.4% (60144 remain 8%)
c [simplification-7] maximum reduction of 10% = max (7%, 10%)
c [simplification-7] large reduction 10% >= 5% limit
c [simplification-7] next conflict interval 2000 = 2000/1
c [simplification-7] penalized conflict interval 2000 = 1 * 2000
c [simplification-7] hard conflict limit 23043 (soft 13043 + delta 10000)
c [simplification-7] new conflict limit 13043 (hard 23043)
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   12.7    9222    60144     11046    6795    509 26170   24    68   12  35%      7   61   20    4  548%
c i   12.7    9221    60144     11203    6946    509 26170   24    68   13  35%      6   61   25    4  675%
c i   12.9    9220    60144     11766    7488    514 26170   24    68   13  36%      5   60   29    4  744%
c i   12.9    9219    60144     11834    7553    514 26170   24    68   13  36%      5   60   27    4  677%
c i   12.9    9217    60144     11846    7558    515 26170   24    68   13  36%      5   60   26    4  660%
c i   13.1    9211    60144     12279    7973    522 26171   24    66   13  36%      4   58   23    4  551%
c i   13.1    9210    60144     12321    8009    522 26172   24    67   13  37%      4   58   27    4  652%
c i   13.1    9206    60144     12338    8025    522 26172   24    67   13  37%      4   58   28    4  670%
c 
c [simplification-8] limit 13043 conflicts (hard 23043) hit after 13045 conflicts
c [quatres-4] found 2611 quaternary clauses 57% in total
c [quatres-4-2] added 3 quaternary resolvents
c [ternres-4] limit 4000000 with penalty 0 = 0 + 0
c [ternres-4] all 9204 free variables schedulable
c [ternres-4] 114 ternary resolvents (0 bin, 114 trn)
c [ternres-4] fully completed ternary resolution
c [decomp-18] removed 25 variables
c [simpleprobe-4] 160 schedulable variables 2%
c [simpleprobe-4] limit 6723650 penalty 0 = 0 + 0
c [decomp-19] removed 28 variables
c [simpleprobe-4] fully completed simple probing
c [simpleprobe-4] removed 28 variables, found 2160 hbrs, 13 units
c [unhide-8] limit 336182 with penalty 0 = 0 + 0
c [unhide-8-8] 7 units, 46 failed, 3132 tauts, 0 hbrs, 14742 literals
c [transred-4] limit 1680912 with penalty 0 = 0 + 0
c [transred-4] removed 470 transitive binary clauses
c [transred-4] found 15 units
c [cce-4] boosting limit by 10
c [cce-4] limit of 300000000 steps penalty 0 = 0 + 0
c [cce-4-1] eliminated 1 clauses out of 1 (100%) of length 11
c [cce-4-1] eliminated 1 clauses out of 12 (8%) of length 8
c [cce-4-1] eliminated 2 clauses out of 63 (3%) of length 7
c [cce-4-1] eliminated 12 clauses out of 306 (4%) of length 6
c [cce-4-1] eliminated 31 clauses out of 905 (3%) of length 5
c [cce-4-1] eliminated 136 clauses out of 2442 (6%) of length 4
c [cce-4-1] completed large round (ATE)
c [cce-4-1] eliminated 183 large clauses in 13072273 steps
c [cce-4-1] allowing another 6536136 steps for small clauses
c [cce-4-1] scheduling 45117 clauses = 33173 binary + 11944 ternary
c [cce-4-1] tried to eliminate 35192 small clauses 78%
c [cce-4-1] eliminated 7339 binary clauses 22%
c [cce-4-1] eliminated 1463 ternary clauses 12%
c [cce-4-1] eliminated 8802 small clauses 20%
c [cce-4-1] eliminated 9400 small clauses in 300000000 steps
c [cce-4-1] incomplete small round (ATE)
c [cce-4-1] eliminated 9583 covered clauses in round 1
c [cce-4] eliminated 9583 covered clauses in TOTAL during 1 rounds
c [elim-8] no untried remaining variables left
c [elim-8] scheduled 9104 variables 100%
c [elim-8] boosting limit by 20
c [elim-8] limit of 672365000 steps penalty 0 = 0 + 0
c [elim-8] rescheduling of touched variables disabled
c [elim-8-1] eliminated 761 variables 8% in round 1 in 3246386 steps
c [elim-8-1] backward subsumption/strengthening limit 3246300
c [elim-8-1-1] backward checking 3304 touched variables 36%
c [elim-8-1-1] fully completed backward checking in 1 rounds
c [elim-8-1] subsumed 10 and strengthened 26 clauses in 380199 steps
c [elim-8-1] rescheduled 140 variables 2% by backward subsumption
c [elim-8-2] eliminated 7 variables 0% in round 2 in 51315 steps
c [elim-8-2] backward subsumption/strengthening limit 51300
c [elim-8-2-1] backward checking 28 touched variables 0%
c [elim-8-2-1] fully completed backward checking in 1 rounds
c [elim-8-2] subsumed 0 and strengthened 3 clauses in 16297 steps
c [elim-8-2] rescheduled 6 variables 0% by backward subsumption
c [elim-8-3] eliminated 2 variables 0% in round 3 in 2467 steps
c [elim-8-3] backward subsumption/strengthening limit 2400
c [elim-8-3-1] backward checking 6 touched variables 0%
c [elim-8-3-1] incomplete backward checking 0 remain 0%
c [elim-8-3] subsumed 0 and strengthened 0 clauses in 2401 steps
c [elim-8] fully completed in 3 rounds
c [elim-8] transition to [ all 0 rem 0 ] state
c [elim-8] eliminated 770 = 8% variables out of 9104 scheduled
c [bca-4] limit of 10000000 steps and 98168 added (scaled 2)
c [bca-4] 13301 out of 16670 literals actually usable 80%
c [bca-4] added 25 blocked clauses in 31993 steps
c [sweep-4] limit 1000000 penalty 0 = 0 + 0
c [sweep-4-1] 1218 pos 15.8% + 6499 neg 84.2% = 7717 sched 92.6% ret 617
c [sweep-4-1] 1098609 steps 26 queries 858.69 avg class size
c [sweep-4-1] 402 decisions 21 SAT calls 60.81 avg env size
c [sweep-4-1] 7277 variables remain 88% (1036 retained 12%)
c [decomp-20] removed 33 variables
c [sweep-4-1] removed 33 vars (0 failed, 5 eqs, 10 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 33 vars in TOTAL (1 rounds, 25 queries)
c [phase-count-8] 48302 negative 99.3% of 48650 except 348 0.7%
c [phase-count-8] 40458 positive 83.2% of 48650 except 8192 16.8%
c [phase-count-8] less non-negative clauses 348 than limit 4800 (10.0%)
c [phase-count-8] non-pos/non-neg = 8192/348 = 23.54 >= 2.00 = 200/100
c [lucky-phase-8] forcing lucky phase -1
c [phase-8] phase bias: 0 positive 0%, 3 negative 100%
c [score-distribution-8] 4968 pos 59.85%, 323 min 3.89%, 3010 zero 36.26%
c [score-distribution-8] 2295 different 27.65% out of total 8301 variables
c [simplification-8] removed 903 variables 9.8% (8301 remain 5%)
c [simplification-8] removed 11494 irredundant clauses 19.1% (48650 remain 6%)
c [simplification-8] maximum reduction of 19% = max (10%, 19%)
c [simplification-8] large reduction 19% >= 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 25045 (soft 15045 + delta 10000)
c [simplification-8] new conflict limit 15045 (hard 25045)
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.1    8300    48650     13238    4569   1408 27443   25    67   11  37%      6   58   24    4  529%
c i   20.5    8298    48650     14506    5790   1417 27447   25    66   11  38%      9   56   21    5  424%
c i   20.5    8297    48650     14514    5797   1417 27447   25    66   11  38%      9   56   21    5  432%
c i   20.5    8295    48650     14518    5800   1417 27447   25    66   11  38%      9   56   21    5  427%
c i   20.5    8293    48650     14593    5871   1418 27448   25    66   11  38%      8   55   21    5  423%
c 
c [simplification-9] limit 15048 conflicts (hard 25045) hit after 15049 conflicts
c [quatres-5] found 2324 quaternary clauses 53% in total
c [quatres-5-1] removed 4 duplicate quaternary clauses
c [ternres-5] limit 4000000 with penalty 0 = 0 + 0
c [ternres-5] all 8291 free variables schedulable
c [ternres-5] 205 ternary resolvents (0 bin, 205 trn)
c [ternres-5] fully completed ternary resolution
c [gauss-4] limit 1000000 penalty 1 = 1 + 0
c [gauss-4] extracted 18 xors of average arity 2.7
c [gauss-4] connected 48 occurrences of 25 variables (average 1.9)
c [gauss-4] limit 1000000 penalty 1 = 1 + 0
c [gauss-4] fully completed
c [gauss-4] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-21] removed 1 variables
c [treelook-4] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-4] scheduled 16579 literals 100%
c [treelook-4] scheduling used 232333 steps
c [treelook-4] scheduled completely
c [treelook-4] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-4] used 334491 steps
c [treelook-4] 16538 literals remain 100%
c [treelook-4] 8277 variables remain to probed next time 100%
c [treelook-4] removed 12 variables, found 1710 hbrs
c [unhide-9] limit 377607 with penalty 0 = 0 + 0
c [unhide-9-10] 7 units, 170 failed, 2320 tauts, 0 hbrs, 6524 literals
c [transred-5] limit 1888038 with penalty 0 = 0 + 0
c [transred-5] removed 493 transitive binary clauses
c [transred-5] found 24 units
c [cce-5] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-5-1] eliminated 2 clauses out of 5 (40%) of length 17
c [cce-5-1] eliminated 2 clauses out of 3 (67%) of length 15
c [cce-5-1] eliminated 1 clauses out of 2 (50%) of length 14
c [cce-5-1] eliminated 1 clauses out of 5 (20%) of length 13
c [cce-5-1] eliminated 2 clauses out of 6 (33%) of length 12
c [cce-5-1] eliminated 1 clauses out of 5 (20%) of length 10
c [cce-5-1] eliminated 4 clauses out of 17 (24%) of length 9
c [cce-5-1] eliminated 3 clauses out of 39 (8%) of length 8
c [cce-5-1] eliminated 5 clauses out of 114 (4%) of length 7
c [cce-5-1] eliminated 25 clauses out of 322 (8%) of length 6
c [cce-5-1] eliminated 51 clauses out of 839 (6%) of length 5
c [cce-5-1] eliminated 203 clauses out of 2116 (10%) of length 4
c [cce-5-1] completed large round (ACCE)
c [cce-5-1] eliminated 300 large clauses in 11127589 steps
c [cce-5-1] allowing another 5563794 steps for small clauses
c [cce-5-1] scheduling 34049 clauses = 24630 binary + 9419 ternary
c [cce-5-1] tried to eliminate 3553 small clauses 10%
c [cce-5-1] eliminated 346 binary clauses 1%
c [cce-5-1] eliminated 190 ternary clauses 2%
c [cce-5-1] eliminated 536 small clauses 2%
c [cce-5-1] eliminated 1341 small clauses in 30000001 steps
c [cce-5-1] incomplete small round (ACCE)
c [cce-5-1] eliminated 1641 covered clauses in round 1
c [cce-5] eliminated 1641 covered clauses in TOTAL during 1 rounds
c [elim-9] scheduling all variables this time
c [elim-9] scheduled 8151 variables 100%
c [elim-9] limit of 37760763 steps penalty 0 = 0 + 0
c [elim-9] rescheduling of touched variables disabled
c [elim-9-1] eliminated 279 variables 3% in round 1 in 3010640 steps
c [elim-9-1] backward subsumption/strengthening limit 3010600
c [elim-9-1-1] backward checking 1595 touched variables 20%
c [elim-9-1-1] fully completed backward checking in 1 rounds
c [elim-9-1] subsumed 6 and strengthened 15 clauses in 194570 steps
c [elim-9-1] rescheduled 54 variables 1% by backward subsumption
c [elim-9-2] eliminated 6 variables 0% in round 2 in 19813 steps
c [elim-9-2] backward subsumption/strengthening limit 19800
c [elim-9-2-1] backward checking 33 touched variables 0%
c [elim-9-2-1] fully completed backward checking in 1 rounds
c [elim-9-2] subsumed 0 and strengthened 2 clauses in 13185 steps
c [elim-9-2] rescheduled 6 variables 0% by backward subsumption
c [elim-9-3] no variable eliminated in round 3 in 2668 steps
c [elim-9] fully completed in 3 rounds
c [elim-9] transition to [ all 0 rem 0 ] state
c [elim-9] eliminated 285 = 3% variables out of 8151 scheduled
c [bca-5] limit of 10000000 steps and 92854 added (scaled 2)
c [bca-5] 12371 out of 15734 literals actually usable 79%
c [bca-5] added 16 blocked clauses in 31127 steps
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 10000000 penalty 0 = 0 + 0
c [sweep-5-1] 1177 pos 17.1% + 5712 neg 82.9% = 6889 sched 87.6% ret 977
c [sweep-5-1] 10018945 steps 345 queries 54.14 avg class size
c [sweep-5-1] 2763 decisions 308 SAT calls 52.84 avg env size
c [sweep-5-1] 1828 variables remain 23% (5965 retained 77%)
c [decomp-23] removed 131 variables
c [sweep-5-1] removed 131 vars (0 failed, 50 eqs, 72 impls)
c [sweep-5] considered successful since not run to completion yet
c [sweep-5] removed 131 vars in TOTAL (1 rounds, 344 queries)
c [phase-count-9] 45132 negative 99.3% of 45452 except 320 0.7%
c [phase-count-9] 37709 positive 83.0% of 45452 except 7743 17.0%
c [phase-count-9] less non-negative clauses 320 than limit 4500 (10.0%)
c [phase-count-9] non-pos/non-neg = 7743/320 = 24.20 >= 2.00 = 200/100
c [lucky-phase-9] forcing lucky phase -1
c [phase-9] phase bias: 0 positive 0%, 2 negative 100%
c [score-distribution-9] 4381 pos 56.64%, 697 min 9.01%, 2657 zero 34.35%
c [score-distribution-9] 2025 different 26.18% out of total 7735 variables
c [simplification-9] removed 556 variables 6.7% (7735 remain 4%)
c [simplification-9] removed 3198 irredundant clauses 6.6% (45452 remain 6%)
c [simplification-9] maximum reduction of 7% = max (7%, 7%)
c [simplification-9] large reduction 7% >= 5% limit
c [simplification-9] next conflict interval 2000 = 2000/1
c [simplification-9] penalized conflict interval 2000 = 1 * 2000
c [simplification-9] hard conflict limit 27049 (soft 17049 + delta 10000)
c [simplification-9] new conflict limit 17049 (hard 27049)
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   22.5    7734    45452     15383    5796   1300 31335   24    63   11  38%      7   52   20    5  399%
c i   22.5    7733    45452     15644    6048   1301 31335   24    62   11  38%      6   50   18    5  352%
c i   22.8    7730    45452     16672    7030   1316 31341   22    58   11  39%      7   46   19    5  355%
c 
c [simplification-10] limit 17049 conflicts (hard 27049) hit after 17049 conflicts
c [ternres-6] limit 4000000 with penalty 0 = 0 + 0
c [ternres-6] all 7730 free variables schedulable
c [ternres-6] 202 ternary resolvents (0 bin, 202 trn)
c [ternres-6] fully completed ternary resolution
c [card-4] limit 250000 penalty 3 = 3 + 0
c [card-4] found 840 at-most-one constraints of average size 3.5
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 250000 for elimination
c [card-4] 840 out of 840 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [decomp-24] removed 5 variables
c [basicprobe-4] limit 10439501 penalty 0 = 0 + 0
c [basicprobe-4-0] 867 probes remain 12% after last round
c [basicprobe-4-0] 269 units = 252 failed (94%) + 17 lifted (6%)
c [basicprobe-4-0] removed 424 variables, found 16722 hbrs
c [bate-2] eliminated 50 asymmetric tautologies during probing
c [unhide-10] limit 417580 with penalty 0 = 0 + 0
c [unhide-10-12] 14 units, 191 failed, 3855 tauts, 0 hbrs, 5618 literals
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 568 transitive binary clauses
c [transred-6] found 15 units
c [block-3] scheduling all variables this time
c [block-3] scheduled 7132 variables 100%
c [block-3] limit of 12500000 steps penalty 2 = 2 + 0
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 173 blocked clauses
c [block-3] 173 < 1/100 * 40584 = 405 considered unsuccessful
c [cce-6] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-6-1] eliminated 1 clauses out of 3 (33%) of length 12
c [cce-6-1] eliminated 1 clauses out of 5 (20%) of length 9
c [cce-6-1] eliminated 2 clauses out of 190 (1%) of length 6
c [cce-6-1] eliminated 26 clauses out of 622 (4%) of length 5
c [cce-6-1] eliminated 82 clauses out of 1583 (5%) of length 4
c [cce-6-1] completed large round (ATE)
c [cce-6-1] eliminated 112 large clauses in 6649789 steps
c [cce-6-1] allowing another 3324894 steps for small clauses
c [cce-6-1] scheduling 29393 clauses = 22107 binary + 7286 ternary
c [cce-6-1] tried to eliminate 4364 small clauses 15%
c [cce-6-1] eliminated 426 binary clauses 2%
c [cce-6-1] eliminated 111 ternary clauses 2%
c [cce-6-1] eliminated 537 small clauses 2%
c [cce-6-1] eliminated 537 small clauses in 30000000 steps
c [cce-6-1] incomplete small round (ATE)
c [cce-6-1] eliminated 649 covered clauses in round 1
c [cce-6] eliminated 649 covered clauses in TOTAL during 1 rounds
c [elim-10] scheduling all variables this time
c [elim-10] scheduled 7132 variables 100%
c [elim-10] limit of 41758007 steps penalty 0 = 0 + 0
c [elim-10] rescheduling of touched variables disabled
c [elim-10-1] eliminated 605 variables 8% in round 1 in 2510646 steps
c [elim-10-1] backward subsumption/strengthening limit 2510600
c [elim-10-1-1] backward checking 2440 touched variables 34%
c [elim-10-1-1] fully completed backward checking in 1 rounds
c [elim-10-1] subsumed 3 and strengthened 18 clauses in 275086 steps
c [elim-10-1] rescheduled 80 variables 1% by backward subsumption
c [elim-10-2] eliminated 4 variables 0% in round 2 in 29773 steps
c [elim-10-2] backward subsumption/strengthening limit 29700
c [elim-10-2-1] backward checking 25 touched variables 0%
c [elim-10-2-1] fully completed backward checking in 1 rounds
c [elim-10-2] subsumed 0 and strengthened 2 clauses in 12081 steps
c [elim-10-2] rescheduled 5 variables 0% by backward subsumption
c [elim-10-3] eliminated 2 variables 0% in round 3 in 2692 steps
c [elim-10-3] backward subsumption/strengthening limit 2600
c [elim-10-3-1] backward checking 5 touched variables 0%
c [elim-10-3-1] incomplete backward checking 0 remain 0%
c [elim-10-3] subsumed 0 and strengthened 0 clauses in 2601 steps
c [elim-10] fully completed in 3 rounds
c [elim-10] transition to [ all 0 rem 0 ] state
c [elim-10] eliminated 615 = 9% variables out of 7132 scheduled
c [bca-6] limit of 10000000 steps and 77738 added (scaled 2)
c [bca-6] 10054 out of 13036 literals actually usable 77%
c [bca-6] added 15 blocked clauses in 27269 steps
c [sweep-6] limit 1000000 penalty 0 = 0 + 0
c [sweep-6-1] 483 pos 32.2% + 1018 neg 67.8% = 1501 sched 23.0% ret 5016
c [sweep-6-1] 1005026 steps 66 queries 80.21 avg class size
c [sweep-6-1] 384 decisions 61 SAT calls 27.38 avg env size
c [sweep-6-1] 1305 variables remain 20% (5206 retained 80%)
c [decomp-25] removed 16 variables
c [sweep-6-1] removed 16 vars (0 failed, 6 eqs, 10 impls)
c [sweep-6] considered successful since not run to completion yet
c [sweep-6] removed 16 vars in TOTAL (1 rounds, 65 queries)
c [score-distribution-10] 3621 pos 55.70%, 732 min 11.26%, 2148 zero 33.04%
c [score-distribution-10] 1823 different 28.04% out of total 6501 variables
c [simplification-10] removed 1229 variables 15.9% (6501 remain 4%)
c [simplification-10] removed 6934 irredundant clauses 15.3% (38518 remain 5%)
c [simplification-10] maximum reduction of 16% = max (16%, 15%)
c [simplification-10] large reduction 16% >= 5% limit
c [simplification-10] next conflict interval 2000 = 2000/1
c [simplification-10] penalized conflict interval 2000 = 1 * 2000
c [simplification-10] hard conflict limit 29049 (soft 19049 + delta 10000)
c [simplification-10] new conflict limit 19049 (hard 29049)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   24.7    6500    38518     17551    6537    840 29989   23    57   11  40%      7   45   22    6  398%
c i   24.9    6499    38518     18215    7179    842 29989   23    56   11  41%      6   43   20    6  343%
c i   24.9    6494    38518     18257    7219    843 29989   23    56   11  41%      5   43   21    6  368%
c i   25.1    6493    38518     18915    7851    846 29992   22    54   11  41%      5   41   21    6  351%
c i   25.1    6492    38518     18969    7903    846 29992   22    54   11  41%      4   41   22    6  376%
c 
c [simplification-11] limit 19049 conflicts (hard 29049) hit after 19049 conflicts
c [quatres-6] found 1780 quaternary clauses 49% in total
c [quatres-6-1] removed 3 duplicate quaternary clauses
c [quatres-6-2] added 1 single-self-subsuming ternary resolvents
c [quatres-6-2] added 1 quaternary resolvents
c [ternres-7] limit 4000000 with penalty 0 = 0 + 0
c [ternres-7] all 6492 free variables schedulable
c [ternres-7] 100 ternary resolvents (0 bin, 100 trn)
c [ternres-7] fully completed ternary resolution
c [decomp-26] removed 13 variables
c [simpleprobe-5] all 6488 free variables schedulable
c [simpleprobe-5] limit 9016254 penalty 0 = 0 + 0
c [decomp-27] removed 94 variables
c [simpleprobe-5] fully completed simple probing
c [simpleprobe-5] removed 94 variables, found 3254 hbrs, 57 units
c [unhide-11] limit 450812 with penalty 0 = 0 + 0
c [unhide-11-14] 1 units, 72 failed, 3198 tauts, 0 hbrs, 8779 literals
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 702 transitive binary clauses
c [transred-7] found 13 units
c [cce-7] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 17
c [cce-7-1] eliminated 2 clauses out of 3 (67%) of length 15
c [cce-7-1] eliminated 1 clauses out of 1 (100%) of length 11
c [cce-7-1] eliminated 2 clauses out of 3 (67%) of length 10
c [cce-7-1] eliminated 2 clauses out of 6 (33%) of length 9
c [cce-7-1] eliminated 2 clauses out of 25 (8%) of length 8
c [cce-7-1] eliminated 5 clauses out of 85 (6%) of length 7
c [cce-7-1] eliminated 16 clauses out of 231 (7%) of length 6
c [cce-7-1] eliminated 35 clauses out of 660 (5%) of length 5
c [cce-7-1] eliminated 144 clauses out of 1536 (9%) of length 4
c [cce-7-1] completed large round (ACCE)
c [cce-7-1] eliminated 210 large clauses in 7939675 steps
c [cce-7-1] allowing another 3969837 steps for small clauses
c [cce-7-1] scheduling 27947 clauses = 20333 binary + 7614 ternary
c [cce-7-1] tried to eliminate 4467 small clauses 16%
c [cce-7-1] eliminated 558 binary clauses 3%
c [cce-7-1] eliminated 120 ternary clauses 2%
c [cce-7-1] eliminated 678 small clauses 2%
c [cce-7-1] eliminated 855 small clauses in 30000001 steps
c [cce-7-1] incomplete small round (ACCE)
c [cce-7-1] eliminated 1065 covered clauses in round 1
c [cce-7] eliminated 1065 covered clauses in TOTAL during 1 rounds
c [elim-11] scheduling all variables this time
c [elim-11] scheduled 6365 variables 100%
c [elim-11] limit of 45081273 steps penalty 0 = 0 + 0
c [elim-11] rescheduling of touched variables disabled
c [elim-11-1] eliminated 226 variables 4% in round 1 in 2296380 steps
c [elim-11-1] backward subsumption/strengthening limit 2296300
c [elim-11-1-1] backward checking 1191 touched variables 19%
c [elim-11-1-1] fully completed backward checking in 1 rounds
c [elim-11-1] subsumed 1 and strengthened 12 clauses in 145795 steps
c [elim-11-1] rescheduled 41 variables 1% by backward subsumption
c [elim-11-2] eliminated 2 variables 0% in round 2 in 15374 steps
c [elim-11-2] backward subsumption/strengthening limit 15300
c [elim-11-2-1] backward checking 15 touched variables 0%
c [elim-11-2-1] fully completed backward checking in 1 rounds
c [elim-11-2] subsumed 0 and strengthened 0 clauses in 7523 steps
c [elim-11] fully completed in 2 rounds
c [elim-11] transition to [ all 0 rem 0 ] state
c [elim-11] eliminated 228 = 4% variables out of 6365 scheduled
c [bca-7] limit of 10000000 steps and 72598 added (scaled 2)
c [bca-7] 9205 out of 12276 literals actually usable 75%
c [bca-7] added 29 blocked clauses in 27282 steps
c [sweep-7] limit 1000000 penalty 0 = 0 + 0
c [sweep-7-1] 391 pos 32.4% + 817 neg 67.6% = 1208 sched 19.7% ret 4929
c [sweep-7-1] 1019741 steps 24 queries 143.21 avg class size
c [sweep-7-1] 297 decisions 22 SAT calls 35.68 avg env size
c [sweep-7-1] 1151 variables remain 19% (4986 retained 81%)
c [decomp-28] removed 3 variables
c [sweep-7-1] removed 3 vars (0 failed, 1 eqs, 2 impls)
c [sweep-7] 3 < 1/1000 * 6137 = 6 considered unsuccessful
c [sweep-7] removed 3 vars in TOTAL (1 rounds, 23 queries)
c [score-distribution-11] 3416 pos 55.69%, 753 min 12.28%, 1965 zero 32.03%
c [score-distribution-11] 1631 different 26.59% out of total 6134 variables
c [simplification-11] removed 358 variables 5.5% (6134 remain 4%)
c [simplification-11] removed 2501 irredundant clauses 6.5% (36017 remain 5%)
c [simplification-11] maximum reduction of 6% = max (6%, 6%)
c [simplification-11] large reduction 6% >= 5% limit
c [simplification-11] next conflict interval 2000 = 2000/1
c [simplification-11] penalized conflict interval 2000 = 1 * 2000
c [simplification-11] hard conflict limit 31049 (soft 21049 + delta 10000)
c [simplification-11] new conflict limit 21049 (hard 31049)
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.6    6133    36017     19688    8425    879 26540   22    53   12  42%      5   39   23    6  378%
c i   26.7    6132    36017     20190    8913    879 26542   22    52   12  42%      4   38   22    6  364%
c i   26.7    6130    36017     20280    8999    880 26542   22    52   12  42%      3   38   21    6  344%
c i   26.7    6129    36017     20281    8999    880 26542   22    52   12  42%      3   38   21    6  342%
c 
c [simplification-12] limit 21059 conflicts (hard 31049) hit after 21060 conflicts
c [quatres-7] found 1593 quaternary clauses 47% in total
c [quatres-7-1] removed 2 duplicate quaternary clauses
c [ternres-8] limit 4000000 with penalty 0 = 0 + 0
c [ternres-8] all 6126 free variables schedulable
c [ternres-8] 85 ternary resolvents (0 bin, 85 trn)
c [ternres-8] fully completed ternary resolution
c [gauss-5] limit 500000 penalty 2 = 2 + 0
c [gauss-5] extracted 15 xors of average arity 2.5
c [gauss-5] connected 38 occurrences of 32 variables (average 1.2)
c [gauss-5] limit 500000 penalty 2 = 2 + 0
c [gauss-5] fully completed
c [gauss-5] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-29] removed 3 variables
c [treelook-5] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-5] scheduled 12245 literals 100%
c [treelook-5] scheduling used 193119 steps
c [treelook-5] scheduled completely
c [treelook-5] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-5] used 313863 steps
c [treelook-5] 12170 literals remain 100%
c [treelook-5] 6106 variables remain to probed next time 100%
c [decomp-30] removed 1 variables
c [treelook-5] removed 17 variables, found 2653 hbrs
c [unhide-12] limit 485637 with penalty 0 = 0 + 0
c [unhide-12-16] 5 units, 27 failed, 1708 tauts, 0 hbrs, 7674 literals
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 550 transitive binary clauses
c [transred-8] found 6 units
c [cce-8] boosting limit by 10
c [cce-8] limit of 300000000 steps penalty 0 = 0 + 0
c [cce-8-1] eliminated 1 clauses out of 3 (33%) of length 12
c [cce-8-1] eliminated 2 clauses out of 6 (33%) of length 9
c [cce-8-1] eliminated 1 clauses out of 25 (4%) of length 8
c [cce-8-1] eliminated 1 clauses out of 90 (1%) of length 7
c [cce-8-1] eliminated 5 clauses out of 226 (2%) of length 6
c [cce-8-1] eliminated 2 clauses out of 633 (0%) of length 5
c [cce-8-1] eliminated 35 clauses out of 1392 (3%) of length 4
c [cce-8-1] completed large round (ATE)
c [cce-8-1] eliminated 47 large clauses in 7205170 steps
c [cce-8-1] allowing another 3602585 steps for small clauses
c [cce-8-1] scheduling 25781 clauses = 19233 binary + 6548 ternary
c [cce-8-1] tried to eliminate 25781 small clauses 100%
c [cce-8-1] eliminated 1847 binary clauses 10%
c [cce-8-1] eliminated 581 ternary clauses 9%
c [cce-8-1] eliminated 2428 small clauses 9%
c [cce-8-1] eliminated 2542 small clauses in 138193802 steps
c [cce-8-1] completed small round (ATE)
c [cce-8-1] completed small and large (ATE)
c [cce-8-1] eliminated 2589 covered clauses in round 1
c [cce-8-2] completed large round (ATE)
c [cce-8-2] allowing another 3141193 steps for small clauses
c [cce-8-2] scheduling 23353 clauses = 17386 binary + 5967 ternary
c [cce-8-2] tried to eliminate 23353 small clauses 100%
c [cce-8-2] completed small round (ATE)
c [cce-8-2] eliminated 0 covered clauses in round 2
c [cce-8] eliminated 2589 covered clauses in TOTAL during 2 rounds
c [elim-12] scheduling all variables this time
c [elim-12] scheduled 6077 variables 100%
c [elim-12] limit of 48563735 steps penalty 0 = 0 + 0
c [elim-12] rescheduling of touched variables disabled
c [elim-12-1] eliminated 264 variables 4% in round 1 in 2087105 steps
c [elim-12-1] backward subsumption/strengthening limit 2087100
c [elim-12-1-1] backward checking 1694 touched variables 28%
c [elim-12-1-1] fully completed backward checking in 1 rounds
c [elim-12-1] subsumed 1 and strengthened 4 clauses in 184641 steps
c [elim-12-1] rescheduled 23 variables 0% by backward subsumption
c [elim-12-2] eliminated 4 variables 0% in round 2 in 8998 steps
c [elim-12-2] backward subsumption/strengthening limit 8900
c [elim-12-2-1] backward checking 20 touched variables 0%
c [elim-12-2-1] fully completed backward checking in 1 rounds
c [elim-12-2] subsumed 2 and strengthened 0 clauses in 7754 steps
c [elim-12-2] rescheduled 4 variables 0% by backward subsumption
c [elim-12-3] eliminated 1 variables 0% in round 3 in 827 steps
c [elim-12-3] backward subsumption/strengthening limit 800
c [elim-12-3-1] backward checking 7 touched variables 0%
c [elim-12-3-1] incomplete backward checking 0 remain 0%
c [elim-12-3] subsumed 1 and strengthened 0 clauses in 801 steps
c [elim-12] incomplete 5 not tried 0% in round 3
c [elim-12] transition to [ all 1 rem 1 ] state
c [elim-12] eliminated 269 = 4% variables out of 6077 scheduled
c [bca-8] limit of 10000000 steps and 65920 added (scaled 2)
c [bca-8] 8571 out of 11618 literals actually usable 74%
c [bca-8] added 17 blocked clauses in 26834 steps
c [score-distribution-12] 3241 pos 55.80%, 756 min 13.02%, 1811 zero 31.18%
c [score-distribution-12] 1628 different 28.03% out of total 5808 variables
c [simplification-12] removed 318 variables 5.2% (5808 remain 3%)
c [simplification-12] removed 3342 irredundant clauses 9.3% (32675 remain 4%)
c [simplification-12] maximum reduction of 9% = max (5%, 9%)
c [simplification-12] large reduction 9% >= 5% limit
c [simplification-12] next conflict interval 2000 = 2000/1
c [simplification-12] penalized conflict interval 2000 = 1 * 2000
c [simplification-12] hard conflict limit 33060 (soft 23060 + delta 10000)
c [simplification-12] new conflict limit 23060 (hard 33060)
c 
c [simplification-13] limit 23060 conflicts (hard 33060) hit after 23060 conflicts
c [ternres-9] limit 4000000 with penalty 0 = 0 + 0
c [ternres-9] all 5808 free variables schedulable
c [ternres-9] 39 ternary resolvents (0 bin, 39 trn)
c [ternres-9] fully completed ternary resolution
c [basicprobe-5] limit 12931782 penalty 0 = 0 + 0
c [basicprobe-5-0] 94 probes remain 2% after last round
c [basicprobe-5-0] 389 units = 347 failed (89%) + 42 lifted (11%)
c [basicprobe-5-0] removed 455 variables, found 17651 hbrs
c [bate-3] eliminated 52 asymmetric tautologies during probing
c [unhide-13] limit 517271 with penalty 0 = 0 + 0
c [unhide-13-18] 1 units, 15 failed, 2763 tauts, 0 hbrs, 5715 literals
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 629 transitive binary clauses
c [transred-9] found 6 units
c [cce-9] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-9-1] eliminated 1 clauses out of 4 (25%) of length 9
c [cce-9-1] eliminated 2 clauses out of 17 (12%) of length 8
c [cce-9-1] eliminated 4 clauses out of 75 (5%) of length 7
c [cce-9-1] eliminated 5 clauses out of 169 (3%) of length 6
c [cce-9-1] eliminated 18 clauses out of 491 (4%) of length 5
c [cce-9-1] eliminated 66 clauses out of 1197 (6%) of length 4
c [cce-9-1] completed large round (ACCE)
c [cce-9-1] eliminated 96 large clauses in 4973542 steps
c [cce-9-1] allowing another 2486771 steps for small clauses
c [cce-9-1] scheduling 22284 clauses = 16627 binary + 5657 ternary
c [cce-9-1] tried to eliminate 5920 small clauses 27%
c [cce-9-1] eliminated 471 binary clauses 3%
c [cce-9-1] eliminated 126 ternary clauses 2%
c [cce-9-1] eliminated 597 small clauses 3%
c [cce-9-1] eliminated 729 small clauses in 30000007 steps
c [cce-9-1] incomplete small round (ACCE)
c [cce-9-1] eliminated 825 covered clauses in round 1
c [cce-9] eliminated 825 covered clauses in TOTAL during 1 rounds
c [elim-13] no untried remaining variables left
c [elim-13] scheduled 5319 variables 100%
c [elim-13] almost no limit of 100000000000 steps
c [elim-13] rescheduling of touched variables disabled
c [elim-13-1] eliminated 408 variables 8% in round 1 in 1770227 steps
c [elim-13-1] backward subsumption/strengthening limit 1770200
c [elim-13-1-1] backward checking 1656 touched variables 31%
c [elim-13-1-1] fully completed backward checking in 1 rounds
c [elim-13-1] subsumed 4 and strengthened 6 clauses in 174617 steps
c [elim-13-1] rescheduled 37 variables 1% by backward subsumption
c [elim-13-2] eliminated 1 variables 0% in round 2 in 14574 steps
c [elim-13-2] backward subsumption/strengthening limit 14500
c [elim-13-2-1] backward checking 8 touched variables 0%
c [elim-13-2-1] fully completed backward checking in 1 rounds
c [elim-13-2] subsumed 0 and strengthened 0 clauses in 5804 steps
c [elim-13] fully completed in 2 rounds
c [elim-13] transition to [ all 0 rem 0 ] state
c [elim-13] eliminated 409 = 8% variables out of 5319 scheduled
c [bca-9] limit of 10000000 steps and 56783 added (scaled 2)
c [bca-9] 7128 out of 9822 literals actually usable 73%
c [bca-9] added 32 blocked clauses in 24712 steps
c [sweep-8] limit 500000 penalty 1 = 1 + 0
c [sweep-8-1] 282 pos 30.1% + 654 neg 69.9% = 936 sched 19.1% ret 3974
c [sweep-8-1] 546609 steps 14 queries 128.43 avg class size
c [sweep-8-1] 293 decisions 13 SAT calls 89.46 avg env size
c [sweep-8-1] 908 variables remain 18% (4002 retained 82%)
c [decomp-32] removed 6 variables
c [sweep-8-1] removed 6 vars (0 failed, 0 eqs, 0 impls)
c [sweep-8] removed 6 vars in TOTAL (1 rounds, 13 queries)
c [score-distribution-13] 2860 pos 58.32%, 618 min 12.60%, 1426 zero 29.08%
c [score-distribution-13] 1361 different 27.75% out of total 4904 variables
c [simplification-13] removed 904 variables 15.6% (4904 remain 3%)
c [simplification-13] removed 4585 irredundant clauses 14.0% (28090 remain 4%)
c [simplification-13] maximum reduction of 16% = max (16%, 14%)
c [simplification-13] large reduction 16% >= 5% limit
c [simplification-13] next conflict interval 2000 = 2000/1
c [simplification-13] penalized conflict interval 2000 = 1 * 2000
c [simplification-13] hard conflict limit 35060 (soft 25060 + delta 10000)
c [simplification-13] new conflict limit 25060 (hard 35060)
c 
c [simplification-14] limit 25060 conflicts (hard 35060) hit after 25060 conflicts
c [quatres-8] found 1365 quaternary clauses 44% in total
c [quatres-8-2] added 3 quaternary resolvents
c [ternres-10] limit 4000000 with penalty 0 = 0 + 0
c [ternres-10] all 4904 free variables schedulable
c [ternres-10] 56 ternary resolvents (0 bin, 56 trn)
c [ternres-10] fully completed ternary resolution
c [simpleprobe-6] all 4904 free variables schedulable
c [simpleprobe-6] limit 10918616 penalty 0 = 0 + 0
c [decomp-34] removed 24 variables
c [simpleprobe-6] fully completed simple probing
c [simpleprobe-6] removed 24 variables, found 2591 hbrs, 13 units
c [unhide-14] limit 545930 with penalty 0 = 0 + 0
c [unhide-14-20] 0 units, 3 failed, 1977 tauts, 0 hbrs, 4502 literals
c [transred-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 663 transitive binary clauses
c [block-4] scheduling all variables this time
c [block-4] scheduled 4878 variables 100%
c [block-4] limit of 6250000 steps penalty 3 = 3 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 51 blocked clauses
c [block-4] 51 < 1/100 * 27825 = 278 considered unsuccessful
c [cce-10] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-10-1] eliminated 2 clauses out of 4 (50%) of length 11
c [cce-10-1] eliminated 1 clauses out of 12 (8%) of length 9
c [cce-10-1] eliminated 1 clauses out of 71 (1%) of length 7
c [cce-10-1] eliminated 3 clauses out of 194 (2%) of length 6
c [cce-10-1] eliminated 10 clauses out of 535 (2%) of length 5
c [cce-10-1] eliminated 40 clauses out of 1157 (3%) of length 4
c [cce-10-1] completed large round (ATE)
c [cce-10-1] eliminated 57 large clauses in 5578957 steps
c [cce-10-1] allowing another 2789478 steps for small clauses
c [cce-10-1] scheduling 20410 clauses = 15532 binary + 4878 ternary
c [cce-10-1] tried to eliminate 6328 small clauses 31%
c [cce-10-1] eliminated 304 binary clauses 2%
c [cce-10-1] eliminated 65 ternary clauses 1%
c [cce-10-1] eliminated 369 small clauses 2%
c [cce-10-1] eliminated 369 small clauses in 30000001 steps
c [cce-10-1] incomplete small round (ATE)
c [cce-10-1] eliminated 426 covered clauses in round 1
c [cce-10] eliminated 426 covered clauses in TOTAL during 1 rounds
c [elim-14] scheduling all variables this time
c [elim-14] scheduled 4878 variables 100%
c [elim-14] limit of 54593080 steps penalty 0 = 0 + 0
c [elim-14] rescheduling of touched variables disabled
c [elim-14-1] eliminated 62 variables 1% in round 1 in 1686490 steps
c [elim-14-1] backward subsumption/strengthening limit 1686400
c [elim-14-1-1] backward checking 483 touched variables 10%
c [elim-14-1-1] fully completed backward checking in 1 rounds
c [elim-14-1] subsumed 0 and strengthened 0 clauses in 61315 steps
c [elim-14] fully completed in 1 rounds
c [elim-14] transition to [ all 0 rem 0 ] state
c [elim-14] eliminated 62 = 1% variables out of 4878 scheduled
c [bca-10] limit of 10000000 steps and 55181 added (scaled 2)
c [bca-10] 6833 out of 9634 literals actually usable 71%
c [bca-10] added 8 blocked clauses in 26010 steps
c [sweep-9] limit 1000000 penalty 0 = 0 + 0
c [sweep-9-1] 284 pos 32.0% + 604 neg 68.0% = 888 sched 18.4% ret 3928
c [sweep-9-1] 1226703 steps 32 queries 113.38 avg class size
c [sweep-9-1] 457 decisions 31 SAT calls 42.48 avg env size
c [sweep-9-1] 815 variables remain 17% (4001 retained 83%)
c [sweep-9-1] removed 0 vars (0 failed, 0 eqs, 1 impls)
c [sweep-9] removed 0 vars in TOTAL (1 rounds, 31 queries)
c [score-distribution-14] 2861 pos 59.41%, 602 min 12.50%, 1353 zero 28.09%
c [score-distribution-14] 1593 different 33.08% out of total 4816 variables
c [simplification-14] removed 88 variables 1.8% (4816 remain 3%)
c [simplification-14] removed 797 irredundant clauses 2.8% (27293 remain 3%)
c [simplification-14] maximum reduction of 3% = max (2%, 3%)
c [simplification-14] geometric conflict interval increment 5000 = 20000 / 4
c [simplification-14] new conflict interval 9000
c [simplification-14] penalized conflict interval 9000 = 1 * 9000
c [simplification-14] hard conflict limit 44060 (soft 34060 + delta 10000)
c [simplification-14] new conflict limit 34060 (hard 44060)
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   36.9    4815    27293     26044   12294    717 22041   21    45   12  48%     70   28   24    7  329%
c i   37.4    4814    27293     28437   14601    726 22043   21    42   14  50%     25   24   17    8  212%
c 
c [simplification-15] limit 34060 conflicts (hard 44060) hit after 34060 conflicts
c [quatres-9] found 1398 quaternary clauses 41% in total
c [ternres-11] limit 4000000 with penalty 0 = 0 + 0
c [ternres-11] all 4814 free variables schedulable
c [ternres-11] 20 ternary resolvents (0 bin, 20 trn)
c [ternres-11] fully completed ternary resolution
c [card-5] limit 125000 penalty 4 = 4 + 0
c [card-5] found 445 at-most-one constraints of average size 3.6
c [card-5] no at-most-two constraint found
c [card-5] using previous limit 125000 for elimination
c [card-5] 445 out of 445 constraints (100%) meet size limits
c [card-5] no units found
c [card-5] no at-most-one constraints generated
c [decomp-36] removed 2 variables
c [treelook-6] limit 340234 penalty 0 = 0 + 0 boost 1
c [treelook-6] scheduled 9627 literals 100%
c [treelook-6] scheduling used 177940 steps
c [treelook-6] scheduled completely
c [treelook-6] limit 340234 penalty 0 = 0 + 0 boost 1
c [treelook-6] used 347723 steps
c [treelook-6] 9591 literals remain 100%
c [treelook-6] 4809 variables remain to probed next time 100%
c [decomp-37] removed 3 variables
c [treelook-6] removed 7 variables, found 3861 hbrs
c [unhide-15] limit 680469 with penalty 0 = 0 + 0
c [unhide-15-22] 0 units, 1 failed, 1407 tauts, 0 hbrs, 12842 literals
c [transred-11] limit 2000000 with penalty 0 = 0 + 0
c [transred-11] removed 417 transitive binary clauses
c [transred-11] found 4 units
c [cce-11] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-11-1] eliminated 1 clauses out of 1 (100%) of length 18
c [cce-11-1] eliminated 1 clauses out of 8 (12%) of length 10
c [cce-11-1] eliminated 3 clauses out of 17 (18%) of length 9
c [cce-11-1] eliminated 1 clauses out of 193 (1%) of length 6
c [cce-11-1] eliminated 7 clauses out of 509 (1%) of length 5
c [cce-11-1] eliminated 39 clauses out of 1158 (3%) of length 4
c [cce-11-1] completed large round (ACCE)
c [cce-11-1] eliminated 52 large clauses in 5743957 steps
c [cce-11-1] allowing another 2871978 steps for small clauses
c [cce-11-1] scheduling 20415 clauses = 15058 binary + 5357 ternary
c [cce-11-1] tried to eliminate 6094 small clauses 30%
c [cce-11-1] eliminated 341 binary clauses 2%
c [cce-11-1] eliminated 139 ternary clauses 3%
c [cce-11-1] eliminated 480 small clauses 2%
c [cce-11-1] eliminated 499 small clauses in 30000001 steps
c [cce-11-1] incomplete small round (ACCE)
c [cce-11-1] eliminated 551 covered clauses in round 1
c [cce-11] eliminated 551 covered clauses in TOTAL during 1 rounds
c [elim-15] scheduling all variables this time
c [elim-15] scheduled 4802 variables 100%
c [elim-15] limit of 68046938 steps penalty 0 = 0 + 0
c [elim-15] rescheduling of touched variables disabled
c [elim-15-1] eliminated 77 variables 2% in round 1 in 1632602 steps
c [elim-15-1] backward subsumption/strengthening limit 1632600
c [elim-15-1-1] backward checking 468 touched variables 10%
c [elim-15-1-1] fully completed backward checking in 1 rounds
c [elim-15-1] subsumed 3 and strengthened 0 clauses in 55809 steps
c [elim-15-1] rescheduled 5 variables 0% by backward subsumption
c [elim-15-2] eliminated 1 variables 0% in round 2 in 1882 steps
c [elim-15-2] backward subsumption/strengthening limit 1800
c [elim-15-2-1] backward checking 6 touched variables 0%
c [elim-15-2-1] incomplete backward checking 0 remain 0%
c [elim-15-2] subsumed 0 and strengthened 0 clauses in 1823 steps
c [elim-15-2] fully rescheduled 4724 variables 98%
c [elim-15-3] eliminated 4 variables 0% in round 3 in 1619773 steps
c [elim-15-3] backward subsumption/strengthening limit 1619700
c [elim-15-3-1] backward checking 15 touched variables 0%
c [elim-15-3-1] fully completed backward checking in 1 rounds
c [elim-15-3] subsumed 0 and strengthened 1 clauses in 5002 steps
c [elim-15] incomplete 9 not tried 0% in round 3
c [elim-15] transition to [ all 1 rem 1 ] state
c [elim-15] eliminated 82 = 2% variables out of 4802 scheduled
c [bca-11] limit of 10000000 steps and 53541 added (scaled 2)
c [bca-11] 6415 out of 9442 literals actually usable 68%
c [bca-11] added 6 blocked clauses in 30604 steps
c [score-distribution-15] 2700 pos 57.20%, 749 min 15.87%, 1271 zero 26.93%
c [score-distribution-15] 1423 different 30.15% out of total 4720 variables
c [simplification-15] removed 94 variables 2.0% (4720 remain 3%)
c [simplification-15] removed 822 irredundant clauses 3.0% (26471 remain 3%)
c [simplification-15] maximum reduction of 3% = max (2%, 3%)
c [simplification-15] geometric conflict interval increment 5000 = 20000 / 4
c [simplification-15] new conflict interval 14000
c [simplification-15] penalized conflict interval 14000 = 1 * 14000
c [simplification-15] hard conflict limit 58060 (soft 48060 + delta 10000)
c [simplification-15] new conflict limit 48060 (hard 58060)
c 
c [simplification-16] limit 48060 conflicts (hard 58060) hit after 48060 conflicts
c [ternres-12] limit 4589432 with penalty 0 = 0 + 0
c [ternres-12] all 4720 free variables schedulable
c [ternres-12] 28 ternary resolvents (0 bin, 28 trn)
c [ternres-12] fully completed ternary resolution
c [gauss-6] limit 250000 penalty 3 = 3 + 0
c [gauss-6] extracted 6 xors of average arity 3.0
c [gauss-6] connected 18 occurrences of 12 variables (average 1.5)
c [gauss-6] limit 250000 penalty 3 = 3 + 0
c [gauss-6] fully completed
c [gauss-6] exported 0 unary, 0 binary and 0 ternary equations
c [basicprobe-6] limit 22947160 penalty 0 = 0 + 0
c [basicprobe-6-0] 350 sched 8%, 130 failed, 3 lifted, 5918 hbrs
c [decomp-39] removed 195 variables
c [basicprobe-6-1] 1086 sched 25%, 107 failed, 12 lifted, 21544 hbrs
c [decomp-40] removed 153 variables
c [basicprobe-6-2] 916 probes remain 21% after last round
c [basicprobe-6-2] 263 units = 248 failed (94%) + 15 lifted (6%)
c [basicprobe-6-2] removed 364 variables, found 28721 hbrs
c [bate-4] eliminated 56 asymmetric tautologies during probing
c [unhide-16] limit 917886 with penalty 0 = 0 + 0
c [unhide-16-24] 0 units, 2 failed, 3341 tauts, 0 hbrs, 21557 literals
c [transred-12] limit 2000000 with penalty 0 = 0 + 0
c [transred-12] removed 450 transitive binary clauses
c [cce-12] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-12-1] eliminated 1 clauses out of 3 (33%) of length 14
c [cce-12-1] eliminated 2 clauses out of 13 (15%) of length 9
c [cce-12-1] eliminated 1 clauses out of 18 (6%) of length 8
c [cce-12-1] eliminated 6 clauses out of 476 (1%) of length 5
c [cce-12-1] eliminated 9 clauses out of 1003 (1%) of length 4
c [cce-12-1] completed large round (ATE)
c [cce-12-1] eliminated 19 large clauses in 4029918 steps
c [cce-12-1] allowing another 2014959 steps for small clauses
c [cce-12-1] scheduling 18074 clauses = 14289 binary + 3785 ternary
c [cce-12-1] tried to eliminate 7626 small clauses 42%
c [cce-12-1] eliminated 358 binary clauses 3%
c [cce-12-1] eliminated 37 ternary clauses 1%
c [cce-12-1] eliminated 395 small clauses 2%
c [cce-12-1] eliminated 395 small clauses in 30000005 steps
c [cce-12-1] incomplete small round (ATE)
c [cce-12-1] eliminated 414 covered clauses in round 1
c [cce-12] eliminated 414 covered clauses in TOTAL during 1 rounds
c [elim-16] no untried remaining variables left
c [elim-16] scheduled 4355 variables 100%
c [elim-16] limit of 91788640 steps penalty 0 = 0 + 0
c [elim-16] rescheduling of touched variables disabled
c [elim-16-1] eliminated 186 variables 4% in round 1 in 1422745 steps
c [elim-16-1] backward subsumption/strengthening limit 1422700
c [elim-16-1-1] backward checking 1030 touched variables 24%
c [elim-16-1-1] fully completed backward checking in 1 rounds
c [elim-16-1] subsumed 1 and strengthened 2 clauses in 112995 steps
c [elim-16-1] rescheduled 8 variables 0% by backward subsumption
c [elim-16-2] no variable eliminated in round 2 in 1636 steps
c [elim-16] fully completed in 2 rounds
c [elim-16] transition to [ all 0 rem 0 ] state
c [elim-16] eliminated 186 = 4% variables out of 4355 scheduled
c [bca-12] limit of 10000000 steps and 47108 added (scaled 2)
c [bca-12] 5295 out of 8340 literals actually usable 63%
c [bca-12] added 17 blocked clauses in 36505 steps
c [sweep-10] limit 688414 penalty 1 = 1 + 0
c [sweep-10-1] 198 pos 27.1% + 532 neg 72.9% = 730 sched 17.5% ret 3439
c [sweep-10-1] 698104 steps 42 queries 83.40 avg class size
c [sweep-10-1] 360 decisions 41 SAT calls 32.83 avg env size
c [sweep-10-1] 584 variables remain 14% (3585 retained 86%)
c [decomp-41] removed 1 variables
c [sweep-10-1] removed 1 vars (0 failed, 0 eqs, 0 impls)
c [sweep-10] 1 < 1/1000 * 4169 = 4 considered unsuccessful
c [sweep-10] removed 1 vars in TOTAL (1 rounds, 41 queries)
c [score-distribution-16] 2480 pos 59.50%, 742 min 17.80%, 946 zero 22.70%
c [score-distribution-16] 1359 different 32.61% out of total 4168 variables
c [simplification-16] removed 552 variables 11.7% (4168 remain 2%)
c [simplification-16] removed 3219 irredundant clauses 12.2% (23252 remain 3%)
c [simplification-16] maximum reduction of 12% = max (12%, 12%)
c [simplification-16] large reduction 12% >= 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 60060 (soft 50060 + delta 10000)
c [simplification-16] new conflict limit 50060 (hard 60060)
c 
c [simplification-17] limit 50060 conflicts (hard 60060) hit after 50061 conflicts
c [quatres-10] found 1374 quaternary clauses 38% in total
c [quatres-10-2] added 1 single-self-subsuming ternary resolvents
c [ternres-13] limit 4763147 with penalty 0 = 0 + 0
c [ternres-13] all 4168 free variables schedulable
c [ternres-13] 45 ternary resolvents (1 bin, 44 trn)
c [ternres-13] fully completed ternary resolution
c [simpleprobe-7] all 4168 free variables schedulable
c [simpleprobe-7] limit 19052590 penalty 0 = 0 + 0
c [decomp-43] removed 5 variables
c [simpleprobe-7] fully completed simple probing
c [simpleprobe-7] removed 5 variables, found 3049 hbrs, 2 units
c [unhide-17] limit 952629 with penalty 0 = 0 + 0
c [unhide-17-26] 0 units, 2 failed, 2693 tauts, 0 hbrs, 12289 literals
c [transred-13] limit 2000000 with penalty 0 = 0 + 0
c [transred-13] removed 481 transitive binary clauses
c [cce-13] boosting limit by 10
c [cce-13] limit of 300000000 steps penalty 0 = 0 + 0
c [cce-13-1] eliminated 1 clauses out of 2 (50%) of length 12
c [cce-13-1] eliminated 2 clauses out of 3 (67%) of length 11
c [cce-13-1] eliminated 2 clauses out of 14 (14%) of length 9
c [cce-13-1] eliminated 2 clauses out of 21 (10%) of length 8
c [cce-13-1] eliminated 6 clauses out of 74 (8%) of length 7
c [cce-13-1] eliminated 4 clauses out of 190 (2%) of length 6
c [cce-13-1] eliminated 5 clauses out of 515 (1%) of length 5
c [cce-13-1] eliminated 41 clauses out of 1104 (4%) of length 4
c [cce-13-1] completed large round (ACCE)
c [cce-13-1] eliminated 63 large clauses in 5164945 steps
c [cce-13-1] allowing another 2582472 steps for small clauses
c [cce-13-1] scheduling 17482 clauses = 13470 binary + 4012 ternary
c [cce-13-1] tried to eliminate 17482 small clauses 100%
c [cce-13-1] eliminated 951 binary clauses 7%
c [cce-13-1] eliminated 217 ternary clauses 5%
c [cce-13-1] eliminated 1168 small clauses 7%
c [cce-13-1] eliminated 1188 small clauses in 68308177 steps
c [cce-13-1] completed small round (ACCE)
c [cce-13-1] completed small and large (ACCE)
c [cce-13-1] eliminated 1251 covered clauses in round 1
c [cce-13-2] eliminated 2 clauses out of 1063 (0%) of length 4
c [cce-13-2] completed large round (ACCE)
c [cce-13-2] eliminated 2 large clauses in 4745198 steps
c [cce-13-2] allowing another 2372599 steps for small clauses
c [cce-13-2] scheduling 16314 clauses = 12519 binary + 3795 ternary
c [cce-13-2] tried to eliminate 16314 small clauses 100%
c [cce-13-2] eliminated 29 binary clauses 0%
c [cce-13-2] eliminated 15 ternary clauses 0%
c [cce-13-2] eliminated 44 small clauses 0%
c [cce-13-2] eliminated 44 small clauses in 62801984 steps
c [cce-13-2] completed small round (ACCE)
c [cce-13-2] eliminated 46 covered clauses in round 2
c [cce-13-3] completed large round (ACCE)
c [cce-13-3] allowing another 2361973 steps for small clauses
c [cce-13-3] scheduling 16270 clauses = 12490 binary + 3780 ternary
c [cce-13-3] tried to eliminate 16270 small clauses 100%
c [cce-13-3] eliminated 8 binary clauses 0%
c [cce-13-3] eliminated 1 ternary clauses 0%
c [cce-13-3] eliminated 9 small clauses 0%
c [cce-13-3] eliminated 9 small clauses in 62612570 steps
c [cce-13-3] completed small round (ACCE)
c [cce-13-3] eliminated 9 covered clauses in round 3
c [cce-13] eliminated 1306 covered clauses in TOTAL during 3 rounds
c [elim-17] scheduling all variables this time
c [elim-17] scheduled 4160 variables 100%
c [elim-17] limit of 95262952 steps penalty 0 = 0 + 0
c [elim-17] rescheduling of touched variables disabled
c [elim-17-1] eliminated 150 variables 4% in round 1 in 1330344 steps
c [elim-17-1] backward subsumption/strengthening limit 1330300
c [elim-17-1-1] backward checking 771 touched variables 19%
c [elim-17-1-1] fully completed backward checking in 1 rounds
c [elim-17-1] subsumed 0 and strengthened 2 clauses in 78018 steps
c [elim-17-1] rescheduled 7 variables 0% by backward subsumption
c [elim-17-2] no variable eliminated in round 2 in 3236 steps
c [elim-17] fully completed in 2 rounds
c [elim-17] transition to [ all 0 rem 0 ] state
c [elim-17] eliminated 150 = 4% variables out of 4160 scheduled
c [bca-13] limit of 10000000 steps and 44110 added (scaled 2)
c [bca-13] 5117 out of 8022 literals actually usable 64%
c [bca-13] added 8 blocked clauses in 35154 steps
c [score-distribution-17] 2453 pos 61.17%, 654 min 16.31%, 903 zero 22.52%
c [score-distribution-17] 1284 different 32.02% out of total 4010 variables
c [simplification-17] removed 158 variables 3.8% (4010 remain 2%)
c [simplification-17] removed 1502 irredundant clauses 6.5% (21750 remain 3%)
c [simplification-17] maximum reduction of 6% = max (4%, 6%)
c [simplification-17] large reduction 6% >= 5% limit
c [simplification-17] next conflict interval 2000 = 2000/1
c [simplification-17] penalized conflict interval 2000 = 1 * 2000
c [simplification-17] hard conflict limit 62061 (soft 52061 + delta 10000)
c [simplification-17] new conflict limit 52061 (hard 62061)
c 
c [simplification-18] limit 52061 conflicts (hard 62061) hit after 52061 conflicts
c [quatres-11] found 1371 quaternary clauses 38% in total
c [ternres-14] limit 4932429 with penalty 0 = 0 + 0
c [ternres-14] all 4010 free variables schedulable
c [ternres-14] 18 ternary resolvents (0 bin, 18 trn)
c [ternres-14] fully completed ternary resolution
c [treelook-7] limit 493242 penalty 0 = 0 + 0 boost 1
c [treelook-7] scheduled 8019 literals 100%
c [treelook-7] scheduling used 194800 steps
c [treelook-7] scheduled completely
c [treelook-7] limit 493242 penalty 0 = 0 + 0 boost 1
c [treelook-7] used 494553 steps
c [treelook-7] 7950 literals remain 99%
c [treelook-7] 4003 variables remain to probed next time 100%
c [treelook-7] removed 6 variables, found 391 hbrs
c [unhide-18] limit 986485 with penalty 0 = 0 + 0
c [unhide-18-28] 0 units, 0 failed, 1002 tauts, 0 hbrs, 8076 literals
c [transred-14] limit 2000000 with penalty 0 = 0 + 0
c [transred-14] removed 374 transitive binary clauses
c [transred-14] found 1 units
c [cce-14] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-14-1] eliminated 1 clauses out of 1 (100%) of length 29
c [cce-14-1] eliminated 2 clauses out of 2 (100%) of length 20
c [cce-14-1] eliminated 1 clauses out of 3 (33%) of length 14
c [cce-14-1] eliminated 1 clauses out of 14 (7%) of length 9
c [cce-14-1] eliminated 2 clauses out of 23 (9%) of length 8
c [cce-14-1] eliminated 1 clauses out of 76 (1%) of length 7
c [cce-14-1] eliminated 2 clauses out of 206 (1%) of length 6
c [cce-14-1] eliminated 1 clauses out of 523 (0%) of length 5
c [cce-14-1] eliminated 10 clauses out of 1086 (1%) of length 4
c [cce-14-1] completed large round (ATE)
c [cce-14-1] eliminated 21 large clauses in 4992405 steps
c [cce-14-1] allowing another 2496202 steps for small clauses
c [cce-14-1] scheduling 16057 clauses = 12324 binary + 3733 ternary
c [cce-14-1] tried to eliminate 7536 small clauses 47%
c [cce-14-1] eliminated 35 binary clauses 0%
c [cce-14-1] eliminated 6 ternary clauses 0%
c [cce-14-1] eliminated 41 small clauses 0%
c [cce-14-1] eliminated 45 small clauses in 30000007 steps
c [cce-14-1] incomplete small round (ATE)
c [cce-14-1] eliminated 66 covered clauses in round 1
c [cce-14] eliminated 66 covered clauses in TOTAL during 1 rounds
c [cce-14] 66 < 1/100 * 21669 = 216 considered unsuccessful
c [elim-18] scheduling all variables this time
c [elim-18] scheduled 4003 variables 100%
c [elim-18] boosting limit by 20
c [elim-18] limit of 1972971780 steps penalty 0 = 0 + 0
c [elim-18] rescheduling of touched variables disabled
c [elim-18-1] eliminated 16 variables 0% in round 1 in 1302434 steps
c [elim-18-1] backward subsumption/strengthening limit 1302400
c [elim-18-1-1] backward checking 130 touched variables 3%
c [elim-18-1-1] fully completed backward checking in 1 rounds
c [elim-18-1] subsumed 0 and strengthened 1 clauses in 15180 steps
c [elim-18-1] rescheduled 31 variables 1% by backward subsumption
c [elim-18-2] no variable eliminated in round 2 in 9592 steps
c [elim-18] fully completed in 2 rounds
c [elim-18] transition to [ all 0 rem 0 ] state
c [elim-18] eliminated 16 = 0% variables out of 4003 scheduled
c [elim-18] 16 < 1/100 * 4003 = 40 considered unsuccessful
c [bca-14] limit of 10000000 steps and 43774 added (scaled 2)
c [bca-14] 5054 out of 7976 literals actually usable 63%
c [bca-14] added 17 blocked clauses in 36109 steps
c [score-distribution-18] 2489 pos 62.43%, 607 min 15.22%, 891 zero 22.35%
c [score-distribution-18] 1361 different 34.14% out of total 3987 variables
c [simplification-18] removed 23 variables 0.6% (3987 remain 2%)
c [simplification-18] removed 170 irredundant clauses 0.8% (21580 remain 3%)
c [simplification-18] maximum reduction of 1% = max (1%, 1%)
c [simplification-18] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-18] new conflict interval 24000
c [simplification-18] penalized conflict interval 24000 = 1 * 24000
c [simplification-18] hard conflict limit 88061 (soft 76061 + delta 12000)
c [simplification-18] new conflict limit 76061 (hard 88061)
c 
c [simplification-19] limit 76061 conflicts (hard 88061) hit after 76062 conflicts
c [ternres-15] limit 6991985 with penalty 0 = 0 + 0
c [ternres-15] all 3987 free variables schedulable
c [ternres-15] 6 ternary resolvents (0 bin, 6 trn)
c [ternres-15] fully completed ternary resolution
c [basicprobe-7] limit 34959928 penalty 0 = 0 + 0
c [basicprobe-7-0] 967 sched 25%, 64 failed, 6 lifted, 7527 hbrs
c [decomp-47] removed 85 variables
c [basicprobe-7-1] 1092 sched 28%, 16 failed, 0 lifted, 5898 hbrs
c [decomp-48] removed 19 variables
c [basicprobe-7-2] 249 probes remain 6% after last round
c [basicprobe-7-2] 96 units = 90 failed (94%) + 6 lifted (6%)
c [basicprobe-7-2] removed 116 variables, found 14852 hbrs
c [bate-5] eliminated 24 asymmetric tautologies during probing
c [transred-15] limit 2000000 with penalty 0 = 0 + 0
c [transred-15] removed 414 transitive binary clauses
c [block-5] scheduling all variables this time
c [block-5] scheduled 3871 variables 100%
c [block-5] limit of 4369991 steps penalty 4 = 4 + 0
c [block-5] fully completed
c [block-5] transition to [ all 0 rem 0 ] state
c [block-5] eliminated 21 blocked clauses
c [block-5] 21 < 1/100 * 20788 = 207 considered unsuccessful
c [bca-15] limit of 10000000 steps and 41963 added (scaled 2)
c [bca-15] 4591 out of 7742 literals actually usable 59%
c [bca-15] added 3 blocked clauses in 57655 steps
c [sweep-11] boosting sweeping limit by 10
c [sweep-11] limit 5243987 penalty 2 = 2 + 0
c [sweep-11-1] 146 pos 27.2% + 391 neg 72.8% = 537 sched 13.9% ret 3333
c [sweep-11-1] 5338015 steps 110 queries 18.56 avg class size
c [sweep-11-1] 1697 decisions 107 SAT calls 55.31 avg env size
c [sweep-11-1] 263 variables remain 7% (3607 retained 93%)
c [decomp-49] removed 3 variables
c [sweep-11-1] removed 3 vars (0 failed, 2 eqs, 5 impls)
c [sweep-11] removed 3 vars in TOTAL (1 rounds, 109 queries)
c [score-distribution-19] 2387 pos 61.73%, 687 min 17.77%, 793 zero 20.51%
c [score-distribution-19] 1254 different 32.43% out of total 3867 variables
c [simplification-19] removed 120 variables 3.0% (3867 remain 2%)
c [simplification-19] removed 914 irredundant clauses 4.2% (20666 remain 3%)
c [simplification-19] maximum reduction of 4% = max (3%, 4%)
c [simplification-19] geometric conflict interval increment 4800 = 24000 / 5
c [simplification-19] new conflict interval 28800
c [simplification-19] penalized conflict interval 28800 = 1 * 28800
c [simplification-19] hard conflict limit 119262 (soft 104862 + delta 14400)
c [simplification-19] new conflict limit 104862 (hard 119262)
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 -   62.1    3867    20666     80999   19795    636 38999   18    27   16  66%    555   -0   13   15   91%
c 
c [simplification-20] limit 104862 conflicts (hard 119262) hit after 108675 conflicts
c [quatres-12] found 1396 quaternary clauses 32% in total
c [quatres-12-2] added 2 quaternary resolvents
c [ternres-16] limit 9461251 with penalty 0 = 0 + 0
c [ternres-16] all 3867 free variables schedulable
c [ternres-16] 1 ternary resolvents (0 bin, 1 trn)
c [ternres-16] fully completed ternary resolution
c [simpleprobe-8] all 3867 free variables schedulable
c [simpleprobe-8] limit 37845006 penalty 0 = 0 + 0
c [decomp-51] removed 3 variables
c [simpleprobe-8] fully completed simple probing
c [simpleprobe-8] removed 3 variables, found 2145 hbrs, 2 units
c [unhide-19] limit 946125 with penalty 1 = 1 + 0
c [unhide-19-30] 0 units, 0 failed, 3182 tauts, 0 hbrs, 31276 literals
c [transred-16] limit 2000000 with penalty 0 = 0 + 0
c [transred-16] removed 401 transitive binary clauses
c [cce-15] limit of 23653128 steps penalty 1 = 1 + 0
c [cce-15-1] eliminated 1 clauses out of 1 (100%) of length 26
c [cce-15-1] eliminated 1 clauses out of 2 (50%) of length 17
c [cce-15-1] eliminated 1 clauses out of 12 (8%) of length 9
c [cce-15-1] eliminated 1 clauses out of 198 (1%) of length 6
c [cce-15-1] eliminated 2 clauses out of 497 (0%) of length 5
c [cce-15-1] eliminated 12 clauses out of 1010 (1%) of length 4
c [cce-15-1] completed large round (ACCE)
c [cce-15-1] eliminated 18 large clauses in 4596282 steps
c [cce-15-1] allowing another 2298141 steps for small clauses
c [cce-15-1] scheduling 15518 clauses = 12179 binary + 3339 ternary
c [cce-15-1] tried to eliminate 6072 small clauses 39%
c [cce-15-1] eliminated 168 binary clauses 1%
c [cce-15-1] eliminated 19 ternary clauses 1%
c [cce-15-1] eliminated 187 small clauses 1%
c [cce-15-1] eliminated 187 small clauses in 23653132 steps
c [cce-15-1] incomplete small round (ACCE)
c [cce-15-1] eliminated 205 covered clauses in round 1
c [cce-15] eliminated 205 covered clauses in TOTAL during 1 rounds
c [cce-15] 205 < 1/100 * 20622 = 206 considered unsuccessful
c [elim-19] scheduling all variables this time
c [elim-19] scheduled 3864 variables 100%
c [elim-19] limit of 94612515 steps penalty 1 = 1 + 0
c [elim-19] rescheduling of touched variables disabled
c [elim-19-1] eliminated 86 variables 2% in round 1 in 1220326 steps
c [elim-19-1] backward subsumption/strengthening limit 1220300
c [elim-19-1-1] backward checking 503 touched variables 13%
c [elim-19-1-1] fully completed backward checking in 1 rounds
c [elim-19-1] subsumed 1 and strengthened 0 clauses in 55532 steps
c [elim-19-1] rescheduled 3 variables 0% by backward subsumption
c [elim-19-2] no variable eliminated in round 2 in 797 steps
c [elim-19] fully completed in 2 rounds
c [elim-19] transition to [ all 0 rem 0 ] state
c [elim-19] eliminated 86 = 2% variables out of 3864 scheduled
c [bca-16] limit of 10000000 steps and 41294 added (scaled 2)
c [bca-16] 4757 out of 7558 literals actually usable 63%
c [bca-16] added 13 blocked clauses in 48160 steps
c [score-distribution-20] 2210 pos 58.50%, 809 min 21.41%, 759 zero 20.09%
c [score-distribution-20] 1326 different 35.10% out of total 3778 variables
c [simplification-20] removed 89 variables 2.3% (3778 remain 2%)
c [simplification-20] removed 331 irredundant clauses 1.6% (20335 remain 3%)
c [simplification-20] maximum reduction of 2% = max (2%, 2%)
c [simplification-20] geometric conflict interval increment 9600 = 28800 / 3
c [simplification-20] new conflict interval 38400
c [simplification-20] penalized conflict interval 38400 = 1 * 38400
c [simplification-20] hard conflict limit 166275 (soft 147075 + delta 19200)
c [simplification-20] new conflict limit 147075 (hard 166275)
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 -   72.9    3778    20335    126412   25167    632 35793   18    27   16  68%    789    0   15   16   90%
c -   79.4    3778    20335    160546   27338    641 35795   14    18   22  80%    885   -7   17   16  107%
c 
c [simplification-21] limit 147075 conflicts (hard 166275) hit after 166275 conflicts
c [quatres-13] found 1459 quaternary clauses 29% in total
c [quatres-13-1] removed 2 duplicate quaternary clauses
c [ternres-17] limit 14388735 with penalty 0 = 0 + 0
c [ternres-17] all 3778 free variables schedulable
c [ternres-17] 20 ternary resolvents (0 bin, 20 trn)
c [ternres-17] fully completed ternary resolution
c [card-6] limit 449647 penalty 4 = 4 + 0
c [card-6] found 776 at-most-one constraints of average size 3.6
c [card-6] no at-most-two constraint found
c [card-6] using previous limit 449647 for elimination
c [card-6] 776 out of 776 constraints (100%) meet size limits
c [card-6] no units found
c [card-6] no at-most-one constraints generated
c [gauss-7] limit 179859 penalty 4 = 4 + 0
c [gauss-7] extracted 3 xors of average arity 3.0
c [gauss-7] connected 9 occurrences of 9 variables (average 1.0)
c [gauss-7] limit 179859 penalty 4 = 4 + 0
c [gauss-7] fully completed
c [gauss-7] exported 0 unary, 0 binary and 0 ternary equations
c [treelook-8] limit 1438873 penalty 0 = 0 + 0 boost 1
c [treelook-8] scheduled 7555 literals 100%
c [treelook-8] scheduling used 214466 steps
c [treelook-8] scheduled completely
c [treelook-8] limit 1438873 penalty 0 = 0 + 0 boost 1
c [treelook-8] used 1457452 steps
c [treelook-8] 7465 literals remain 99%
c [treelook-8] 3777 variables remain to probed next time 100%
c [treelook-8] removed 0 variables, found 9113 hbrs
c [transred-17] limit 2000000 with penalty 0 = 0 + 0
c [transred-17] removed 387 transitive binary clauses
c [elim-20] scheduling all variables this time
c [elim-20] scheduled 3778 variables 100%
c [elim-20] limit of 287774707 steps penalty 0 = 0 + 0
c [elim-20] rescheduling of touched variables disabled
c [elim-20-1] eliminated 3 variables 0% in round 1 in 1212030 steps
c [elim-20-1] backward subsumption/strengthening limit 1212000
c [elim-20-1-1] backward checking 24 touched variables 1%
c [elim-20-1-1] fully completed backward checking in 1 rounds
c [elim-20-1] subsumed 0 and strengthened 0 clauses in 4355 steps
c [elim-20] fully completed in 1 rounds
c [elim-20] transition to [ all 0 rem 0 ] state
c [elim-20] eliminated 3 = 0% variables out of 3778 scheduled
c [elim-20] 3 < 1/100 * 3778 = 37 considered unsuccessful
c [bca-17] limit of 10000000 steps and 41283 added (scaled 2)
c [bca-17] 4800 out of 7552 literals actually usable 64%
c [bca-17] added 1 blocked clauses in 42993 steps
c [sweep-12] limit 2158310 penalty 1 = 1 + 0
c [sweep-12-1] 63 pos 24.5% + 194 neg 75.5% = 257 sched 6.8% ret 3518
c [sweep-12-1] 1241273 steps 180 queries 8.18 avg class size
c [sweep-12-1] 885 decisions 177 SAT calls 20.31 avg env size
c [sweep-12-1] fully completed sweeping round
c [decomp-54] removed 1 variables
c [sweep-12-1] removed 1 vars (0 failed, 2 eqs, 4 impls)
c [sweep-12-2] 583 pos 15.4% + 3191 neg 84.6% = 3774 sched 100.0% ret 0
c [sweep-12-2] 1080839 steps 17 queries 427.06 avg class size
c [sweep-12-2] 653 decisions 16 SAT calls 156.62 avg env size
c [sweep-12-2] 3592 variables remain 95% (180 retained 5%)
c [decomp-55] removed 2 variables
c [sweep-12-2] removed 2 vars (0 failed, 0 eqs, 0 impls)
c [sweep-12] removed 3 vars in TOTAL (2 rounds, 195 queries)
c [score-distribution-21] 1939 pos 51.41%, 1093 min 28.98%, 740 zero 19.62%
c [score-distribution-21] 1072 different 28.42% out of total 3772 variables
c [simplification-21] removed 6 variables 0.2% (3772 remain 2%)
c [simplification-21] removed 37 irredundant clauses 0.2% (20298 remain 3%)
c [simplification-21] maximum reduction of 0% = max (0%, 0%)
c [simplification-21] full geometric conflict interval increment 38400
c [simplification-21] new conflict interval 76800
c [simplification-21] penalized conflict interval 76800 = 1 * 76800
c [simplification-21] hard conflict limit 281475 (soft 243075 + delta 38400)
c [simplification-21] new conflict limit 243075 (hard 281475)
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 -   86.1    3772    20298    192779   27117    677 44446   20    28   16  71%    939    3   16   17   94%
c i   91.8    3771    20298    222566   52445    689 44450   21    31   32  66%    970    8   27   16  164%
c -   93.3    3771    20298    228720   28323    693 44454   19    28   23  69%  -1823    4   14   17   80%
c i   97.2    3770    20298    251678   47857    719 44461   11    14   28  80%   -987   -8    8   15   52%
c -  100.0    3747    20298    264225   28899    727 44463   27    42   23  65%  -1018   18   39   17  227%
c i  101.2    3746    20298    271167   35386    737 44471   25    38   27  65%   -813   12    8   18   45%
c i  101.3    3745    20298    271595   35786    737 44471   24    37   27  66%   -905   11   20   18  109%
c 
c [simplification-22] limit 243075 conflicts (hard 281475) hit after 281478 conflicts
c [ternres-18] limit 23926191 with penalty 0 = 0 + 0
c [ternres-18] all 3745 free variables schedulable
c [ternres-18] 2 ternary resolvents (0 bin, 2 trn)
c [ternres-18] fully completed ternary resolution
c [decomp-56] removed 31 variables
c [basicprobe-8] limit 119630959 penalty 0 = 0 + 0
c [basicprobe-8-0] 289 sched 8%, 13 failed, 0 lifted, 1234 hbrs
c [decomp-57] removed 21 variables
c [basicprobe-8-1] 1063 sched 29%, 43 failed, 1 lifted, 3904 hbrs
c [decomp-58] removed 50 variables
c [basicprobe-8-2] 1038 sched 28%, 13 failed, 0 lifted, 2101 hbrs
c [decomp-59] removed 17 variables
c [basicprobe-8-3] 1037 sched 28%, 7 failed, 1 lifted, 742 hbrs
c [decomp-60] removed 9 variables
c [basicprobe-8-4] 1034 sched 28%, 2 failed, 0 lifted, 191 hbrs
c [decomp-61] removed 2 variables
c [basicprobe-8-5] 1034 sched 28%, 0 failed, 0 lifted, 31 hbrs
c [basicprobe-8-6] 1034 sched 28%, 0 failed, 0 lifted, 25 hbrs
c [basicprobe-8-7] 1034 sched 28%, 0 failed, 0 lifted, 14 hbrs
c [basicprobe-8-8] 1034 sched 28%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-8-8] round limit 8 hit
c [basicprobe-8-8] 80 units = 78 failed (98%) + 2 lifted (2%)
c [basicprobe-8-8] removed 99 variables, found 8242 hbrs
c [bate-6] eliminated 34 asymmetric tautologies during probing
c [transred-18] limit 2000000 with penalty 0 = 0 + 0
c [transred-18] removed 568 transitive binary clauses
c [bca-18] limit of 10000000 steps and 39017 added (scaled 2)
c [bca-18] 4598 out of 7286 literals actually usable 63%
c [bca-18] added 3 blocked clauses in 44273 steps
c [sweep-13] limit 7177857 penalty 0 = 0 + 0
c [sweep-13-1] 460 pos 13.3% + 3006 neg 86.7% = 3466 sched 95.2% ret 176
c [sweep-13-1] 7246185 steps 56 queries 92.11 avg class size
c [sweep-13-1] 2366 decisions 56 SAT calls 188.80 avg env size
c [sweep-13-1] 1705 variables remain 47% (1932 retained 53%)
c [decomp-65] removed 5 variables
c [sweep-13-1] removed 5 vars (0 failed, 2 eqs, 1 impls)
c [sweep-13] removed 5 vars in TOTAL (1 rounds, 55 queries)
c [score-distribution-22] 2155 pos 59.25%, 840 min 23.10%, 642 zero 17.65%
c [score-distribution-22] 1230 different 33.82% out of total 3637 variables
c [simplification-22] removed 108 variables 2.9% (3637 remain 2%)
c [simplification-22] removed 1134 irredundant clauses 5.6% (19164 remain 2%)
c [simplification-22] maximum reduction of 6% = max (3%, 6%)
c [simplification-22] large reduction 6% >= 5% limit
c [simplification-22] next conflict interval 2814 = min (281478/100, 76800)
c [simplification-22] penalized conflict interval 2814 = 1 * 2814
c [simplification-22] hard conflict limit 294292 (soft 284292 + delta 10000)
c [simplification-22] new conflict limit 284292 (hard 294292)
c 
c [simplification-23] limit 284292 conflicts (hard 294292) hit after 294294 conflicts
c [quatres-14] found 1588 quaternary clauses 27% in total
c [quatres-14-1] removed 4 duplicate quaternary clauses
c [quatres-14-2] added 3 single-self-subsuming ternary resolvents
c [quatres-14-2] added 2 quaternary resolvents
c [ternres-19] limit 24944278 with penalty 0 = 0 + 0
c [ternres-19] all 3637 free variables schedulable
c [ternres-19] 1 ternary resolvents (0 bin, 1 trn)
c [ternres-19] fully completed ternary resolution
c [simpleprobe-9] all 3637 free variables schedulable
c [simpleprobe-9] limit 99777115 penalty 0 = 0 + 0
c [decomp-67] removed 3 variables
c [simpleprobe-9] fully completed simple probing
c [simpleprobe-9] removed 3 variables, found 2188 hbrs, 0 units
c [unhide-20] limit 1247213 with penalty 2 = 2 + 0
c [unhide-20-32] 0 units, 0 failed, 5312 tauts, 0 hbrs, 43167 literals
c [transred-19] limit 2000000 with penalty 0 = 0 + 0
c [transred-19] removed 433 transitive binary clauses
c [cce-16] limit of 31180348 steps penalty 2 = 2 + 0
c [cce-16-1] eliminated 1 clauses out of 4 (25%) of length 11
c [cce-16-1] eliminated 2 clauses out of 190 (1%) of length 6
c [cce-16-1] eliminated 4 clauses out of 467 (1%) of length 5
c [cce-16-1] eliminated 12 clauses out of 971 (1%) of length 4
c [cce-16-1] completed large round (ATE)
c [cce-16-1] eliminated 19 large clauses in 4156320 steps
c [cce-16-1] allowing another 2078160 steps for small clauses
c [cce-16-1] scheduling 14582 clauses = 11666 binary + 2916 ternary
c [cce-16-1] tried to eliminate 8870 small clauses 61%
c [cce-16-1] eliminated 287 binary clauses 2%
c [cce-16-1] eliminated 16 ternary clauses 1%
c [cce-16-1] eliminated 303 small clauses 2%
c [cce-16-1] eliminated 303 small clauses in 31180357 steps
c [cce-16-1] incomplete small round (ATE)
c [cce-16-1] eliminated 322 covered clauses in round 1
c [cce-16] eliminated 322 covered clauses in TOTAL during 1 rounds
c [elim-21] scheduling all variables this time
c [elim-21] scheduled 3634 variables 100%
c [elim-21] limit of 249442789 steps penalty 1 = 1 + 0
c [elim-21] rescheduling of touched variables disabled
c [elim-21-1] eliminated 97 variables 3% in round 1 in 1108968 steps
c [elim-21-1] backward subsumption/strengthening limit 1108900
c [elim-21-1-1] backward checking 588 touched variables 16%
c [elim-21-1-1] fully completed backward checking in 1 rounds
c [elim-21-1] subsumed 1 and strengthened 2 clauses in 60984 steps
c [elim-21-1] rescheduled 25 variables 1% by backward subsumption
c [elim-21-2] eliminated 1 variables 0% in round 2 in 8805 steps
c [elim-21-2] backward subsumption/strengthening limit 8800
c [elim-21-2-1] backward checking 16 touched variables 0%
c [elim-21-2-1] fully completed backward checking in 1 rounds
c [elim-21-2] subsumed 0 and strengthened 0 clauses in 4076 steps
c [elim-21] fully completed in 2 rounds
c [elim-21] transition to [ all 0 rem 0 ] state
c [elim-21] eliminated 98 = 3% variables out of 3634 scheduled
c [bca-19] limit of 10000000 steps and 38043 added (scaled 2)
c [bca-19] 4368 out of 7074 literals actually usable 62%
c [bca-19] added 23 blocked clauses in 51904 steps
c [sweep-14] limit 7483283 penalty 0 = 0 + 0
c [sweep-14-1] 278 pos 16.8% + 1379 neg 83.2% = 1657 sched 46.9% ret 1879
c [sweep-14-1] 7494084 steps 75 queries 49.53 avg class size
c [sweep-14-1] 2079 decisions 71 SAT calls 116.61 avg env size
c [sweep-14-1] 1088 variables remain 31% (2448 retained 69%)
c [decomp-68] removed 3 variables
c [sweep-14-1] removed 3 vars (0 failed, 3 eqs, 4 impls)
c [sweep-14] removed 3 vars in TOTAL (1 rounds, 74 queries)
c [score-distribution-23] 2217 pos 62.75%, 701 min 19.84%, 615 zero 17.41%
c [score-distribution-23] 1211 different 34.28% out of total 3533 variables
c [simplification-23] removed 104 variables 2.9% (3533 remain 2%)
c [simplification-23] removed 465 irredundant clauses 2.4% (18699 remain 2%)
c [simplification-23] maximum reduction of 3% = max (3%, 2%)
c [simplification-23] geometric conflict interval increment 19200 = 76800 / 4
c [simplification-23] new conflict interval 96000
c [simplification-23] penalized conflict interval 96000 = 1 * 96000
c [simplification-23] hard conflict limit 438294 (soft 390294 + delta 48000)
c [simplification-23] new conflict limit 390294 (hard 438294)
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 -  115.9    3533    18699    313636   27567    687 38906   21    29   17  70%   -102   -1   31   20  153%
c -  123.4    3533    18699    351085   30925    706 38911   13    17   24  79%    388  -12   13   19   64%
c -  130.6    3533    18699    386685   31632    716 38915   21    30   24  71%    655    3   27   19  141%
c 
c [simplification-24] limit 390294 conflicts (hard 438294) hit after 390294 conflicts
c [quatres-15] found 1742 quaternary clauses 25% in total
c [quatres-15-1] removed 8 duplicate quaternary clauses
c [ternres-20] limit 33205070 with penalty 0 = 0 + 0
c [ternres-20] all 3533 free variables schedulable
c [ternres-20] 9 ternary resolvents (0 bin, 9 trn)
c [ternres-20] fully completed ternary resolution
c [transred-20] limit 2000000 with penalty 0 = 0 + 0
c [transred-20] removed 423 transitive binary clauses
c [elim-22] scheduling all variables this time
c [elim-22] scheduled 3533 variables 100%
c [elim-22] limit of 664101419 steps penalty 0 = 0 + 0
c [elim-22] rescheduling of touched variables disabled
c [elim-22-1] eliminated 4 variables 0% in round 1 in 1100240 steps
c [elim-22-1] backward subsumption/strengthening limit 1100200
c [elim-22-1-1] backward checking 45 touched variables 1%
c [elim-22-1-1] fully completed backward checking in 1 rounds
c [elim-22-1] subsumed 0 and strengthened 0 clauses in 7200 steps
c [elim-22] fully completed in 1 rounds
c [elim-22] transition to [ all 0 rem 0 ] state
c [elim-22] eliminated 4 = 0% variables out of 3533 scheduled
c [elim-22] 4 < 1/100 * 3533 = 35 considered unsuccessful
c [bca-20] limit of 10000000 steps and 38018 added (scaled 2)
c [bca-20] 4398 out of 7060 literals actually usable 62%
c [bca-20] added 2 blocked clauses in 44903 steps
c [sweep-15] limit 9961521 penalty 0 = 0 + 0
c [sweep-15-1] 232 pos 21.3% + 856 neg 78.7% = 1088 sched 30.8% ret 2441
c [sweep-15-1] 8063605 steps 395 queries 8.92 avg class size
c [sweep-15-1] 2974 decisions 387 SAT calls 33.03 avg env size
c [sweep-15-1] fully completed sweeping round
c [decomp-70] removed 11 variables
c [sweep-15-1] removed 11 vars (0 failed, 13 eqs, 12 impls)
c [sweep-15-2] 539 pos 15.3% + 2979 neg 84.7% = 3518 sched 100.0% ret 0
c [sweep-15-2] 2001575 steps 29 queries 150.90 avg class size
c [sweep-15-2] 1103 decisions 29 SAT calls 152.34 avg env size
c [sweep-15-2] 2416 variables remain 69% (1102 retained 31%)
c [sweep-15-2] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-15] removed 11 vars in TOTAL (2 rounds, 422 queries)
c [score-distribution-24] 2292 pos 65.15%, 642 min 18.25%, 584 zero 16.60%
c [score-distribution-24] 1280 different 36.38% out of total 3518 variables
c [simplification-24] removed 15 variables 0.4% (3518 remain 2%)
c [simplification-24] removed 32 irredundant clauses 0.2% (18667 remain 2%)
c [simplification-24] maximum reduction of 0% = max (0%, 0%)
c [simplification-24] full geometric conflict interval increment 96000
c [simplification-24] new conflict interval 192000
c [simplification-24] penalized conflict interval 192000 = 1 * 192000
c [simplification-24] hard conflict limit 678294 (soft 582294 + delta 96000)
c [simplification-24] new conflict limit 582294 (hard 678294)
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 -  138.5    3518    18667    423166   32301    740 38566   17    21   16  77%    812   -6   10   19   52%
c i  139.0    3517    18667    426928   35649    755 38574   12    15   19  78%    824  -12    6   19   33%
c -  146.4    3517    18667    460787   33250    773 38580   20    28   23  72%   -566    2   23   19  126%
c i  152.2    3516    18667    488927   58894    789 38586   24    34   33  72%    -11    8   27   19  140%
c -  154.3    3516    18667    498205   33475    792 38589   22    31   23  71%   -728    3   19   20   98%
c -  160.9    3516    18667    535934   35406    797 38590   14    17   23  81%     39   -8   14   18   78%
c -  169.2    3516    18667    573083   34744    812 38599   21    28   23  74%    465    1   27   20  136%
c 
c [simplification-25] limit 582294 conflicts (hard 678294) hit after 582295 conflicts
c [ternres-21] limit 50357699 with penalty 0 = 0 + 0
c [ternres-21] all 3516 free variables schedulable
c [ternres-21] 22 ternary resolvents (0 bin, 22 trn)
c [ternres-21] fully completed ternary resolution
c [decomp-72] removed 3 variables
c [treelook-9] limit 2517884 penalty 1 = 1 + 0 boost 1
c [treelook-9] scheduled 7029 literals 100%
c [treelook-9] scheduling used 234714 steps
c [treelook-9] scheduled completely
c [treelook-9] limit 2517884 penalty 1 = 1 + 0 boost 1
c [treelook-9] used 2534742 steps
c [treelook-9] 6770 literals remain 97%
c [treelook-9] 3486 variables remain to probed next time 100%
c [treelook-9] removed 28 variables, found 16210 hbrs
c [transred-21] limit 2000000 with penalty 0 = 0 + 0
c [transred-21] removed 551 transitive binary clauses
c [transred-21] found 1 units
c [block-6] scheduling all variables this time
c [block-6] scheduled 3486 variables 100%
c [block-6] limit of 31473562 steps penalty 4 = 4 + 0
c [block-6] fully completed
c [block-6] transition to [ all 0 rem 0 ] state
c [block-6] eliminated 29 blocked clauses
c [block-6] 29 < 1/100 * 18367 = 183 considered unsuccessful
c [cce-17] limit of 125894249 steps penalty 1 = 1 + 0
c [cce-17-1] eliminated 1 clauses out of 1 (100%) of length 23
c [cce-17-1] eliminated 1 clauses out of 1 (100%) of length 16
c [cce-17-1] eliminated 1 clauses out of 16 (6%) of length 8
c [cce-17-1] eliminated 3 clauses out of 474 (1%) of length 5
c [cce-17-1] eliminated 37 clauses out of 1010 (4%) of length 4
c [cce-17-1] completed large round (ACCE)
c [cce-17-1] eliminated 43 large clauses in 4721138 steps
c [cce-17-1] allowing another 2360569 steps for small clauses
c [cce-17-1] scheduling 13795 clauses = 11113 binary + 2682 ternary
c [cce-17-1] tried to eliminate 13795 small clauses 100%
c [cce-17-1] eliminated 420 binary clauses 4%
c [cce-17-1] eliminated 89 ternary clauses 3%
c [cce-17-1] eliminated 509 small clauses 4%
c [cce-17-1] eliminated 509 small clauses in 48104604 steps
c [cce-17-1] completed small round (ACCE)
c [cce-17-1] eliminated 552 covered clauses in round 1
c [cce-17-2] eliminated 1 clauses out of 471 (0%) of length 5
c [cce-17-2] eliminated 6 clauses out of 973 (1%) of length 4
c [cce-17-2] completed large round (ACCE)
c [cce-17-2] eliminated 7 large clauses in 4480291 steps
c [cce-17-2] allowing another 2240145 steps for small clauses
c [cce-17-2] scheduling 13286 clauses = 10693 binary + 2593 ternary
c [cce-17-2] tried to eliminate 13286 small clauses 100%
c [cce-17-2] eliminated 10 binary clauses 0%
c [cce-17-2] eliminated 7 ternary clauses 0%
c [cce-17-2] eliminated 17 small clauses 0%
c [cce-17-2] eliminated 17 small clauses in 46306623 steps
c [cce-17-2] completed small round (ACCE)
c [cce-17-2] eliminated 24 covered clauses in round 2
c [cce-17-3] eliminated 2 clauses out of 470 (0%) of length 5
c [cce-17-3] completed large round (ACCE)
c [cce-17-3] eliminated 2 large clauses in 4447025 steps
c [cce-17-3] allowing another 2223512 steps for small clauses
c [cce-17-3] scheduling 13269 clauses = 10683 binary + 2586 ternary
c [cce-17-3] tried to eliminate 8831 small clauses 67%
c [cce-17-3] eliminated 2 binary clauses 0%
c [cce-17-3] eliminated 1 ternary clauses 0%
c [cce-17-3] eliminated 3 small clauses 0%
c [cce-17-3] eliminated 3 small clauses in 31483029 steps
c [cce-17-3] incomplete small round (ACCE)
c [cce-17-3] eliminated 5 covered clauses in round 3
c [cce-17] eliminated 581 covered clauses in TOTAL during 3 rounds
c [bca-21] limit of 10000000 steps and 36147 added (scaled 2)
c [bca-21] 4218 out of 6974 literals actually usable 60%
c [bca-21] added 9 blocked clauses in 52676 steps
c [sweep-16] limit 15107309 penalty 0 = 0 + 0
c [sweep-16-1] 426 pos 17.8% + 1961 neg 82.2% = 2387 sched 68.5% ret 1099
c [sweep-16-1] 15797599 steps 167 queries 30.19 avg class size
c [sweep-16-1] 3639 decisions 164 SAT calls 101.96 avg env size
c [sweep-16-1] 713 variables remain 20% (2772 retained 80%)
c [decomp-74] removed 4 variables
c [sweep-16-1] removed 4 vars (0 failed, 3 eqs, 4 impls)
c [sweep-16] removed 4 vars in TOTAL (1 rounds, 166 queries)
c [score-distribution-25] 1923 pos 55.23%, 1028 min 29.52%, 531 zero 15.25%
c [score-distribution-25] 1100 different 31.59% out of total 3482 variables
c [simplification-25] removed 34 variables 1.0% (3482 remain 2%)
c [simplification-25] removed 923 irredundant clauses 4.9% (17744 remain 2%)
c [simplification-25] maximum reduction of 5% = max (1%, 5%)
c [simplification-25] large reduction 5% >= 5% limit
c [simplification-25] next conflict interval 5822 = min (582295/100, 192000)
c [simplification-25] penalized conflict interval 5822 = 1 * 5822
c [simplification-25] hard conflict limit 598117 (soft 588117 + delta 10000)
c [simplification-25] new conflict limit 588117 (hard 598117)
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  175.9    3481    17744    588451   49447    910 53069   20    27   25  75%    582   -2   16   21   76%
c i  177.7    3480    17744    597012   57419    910 53069   23    31   27  75%   -750    2   22   21  104%
c 
c [simplification-26] limit 588117 conflicts (hard 598117) hit after 598117 conflicts
c [quatres-16] found 1869 quaternary clauses 22% in total
c [quatres-16-1] removed 2 duplicate quaternary clauses
c [ternres-22] limit 51811723 with penalty 0 = 0 + 0
c [ternres-22] all 3479 free variables schedulable
c [ternres-22] 17 ternary resolvents (0 bin, 17 trn)
c [ternres-22] fully completed ternary resolution
c [decomp-75] removed 3 variables
c [basicprobe-9] limit 259058616 penalty 0 = 0 + 0
c [basicprobe-9-0] 1010 sched 30%, 52 failed, 0 lifted, 2871 hbrs
c [decomp-76] removed 64 variables
c [basicprobe-9-1] 982 sched 29%, 20 failed, 0 lifted, 2989 hbrs
c [decomp-77] removed 21 variables
c [basicprobe-9-2] 972 sched 29%, 8 failed, 0 lifted, 571 hbrs
c [decomp-78] removed 8 variables
c [basicprobe-9-3] 970 sched 29%, 1 failed, 0 lifted, 124 hbrs
c [decomp-79] removed 1 variables
c [basicprobe-9-4] 970 sched 29%, 0 failed, 0 lifted, 83 hbrs
c [basicprobe-9-5] 970 sched 29%, 0 failed, 0 lifted, 12 hbrs
c [basicprobe-9-6] 970 sched 29%, 0 failed, 0 lifted, 9 hbrs
c [basicprobe-9-7] 970 sched 29%, 0 failed, 0 lifted, 9 hbrs
c [basicprobe-9-8] 970 sched 29%, 0 failed, 0 lifted, 11 hbrs
c [basicprobe-9-8] round limit 8 hit
c [basicprobe-9-8] 81 units = 81 failed (100%) + 0 lifted (0%)
c [basicprobe-9-8] removed 94 variables, found 6679 hbrs
c [bate-7] eliminated 16 asymmetric tautologies during probing
c [transred-22] limit 2000000 with penalty 0 = 0 + 0
c [transred-22] removed 638 transitive binary clauses
c [cce-18] almost no limit of 4000000000 steps
c [cce-18-1] eliminated 1 clauses out of 445 (0%) of length 5
c [cce-18-1] eliminated 2 clauses out of 915 (0%) of length 4
c [cce-18-1] completed large round (ATE)
c [cce-18-1] eliminated 3 large clauses in 3891800 steps
c [cce-18-1] allowing another 1945900 steps for small clauses
c [cce-18-1] scheduling 12886 clauses = 10518 binary + 2368 ternary
c [cce-18-1] tried to eliminate 12886 small clauses 100%
c [cce-18-1] eliminated 117 binary clauses 1%
c [cce-18-1] eliminated 16 ternary clauses 1%
c [cce-18-1] eliminated 133 small clauses 1%
c [cce-18-1] eliminated 133 small clauses in 42179820 steps
c [cce-18-1] completed small round (ATE)
c [cce-18-1] eliminated 136 covered clauses in round 1
c [cce-18-2] completed large round (ATE)
c [cce-18-2] allowing another 1941122 steps for small clauses
c [cce-18-2] scheduling 12753 clauses = 10401 binary + 2352 ternary
c [cce-18-2] tried to eliminate 12753 small clauses 100%
c [cce-18-2] completed small round (ATE)
c [cce-18-2] eliminated 0 covered clauses in round 2
c [cce-18] eliminated 136 covered clauses in TOTAL during 2 rounds
c [cce-18] 136 < 1/100 * 17063 = 170 considered unsuccessful
c [elim-23] scheduling all variables this time
c [elim-23] scheduled 3385 variables 100%
c [elim-23] almost no limit of 100000000000 steps
c [elim-23] rescheduling of touched variables disabled
c [elim-23-1] eliminated 137 variables 4% in round 1 in 988701 steps
c [elim-23-1] backward subsumption/strengthening limit 988700
c [elim-23-1-1] backward checking 715 touched variables 21%
c [elim-23-1-1] fully completed backward checking in 1 rounds
c [elim-23-1] subsumed 1 and strengthened 2 clauses in 66993 steps
c [elim-23-1] rescheduled 22 variables 1% by backward subsumption
c [elim-23-2] no variable eliminated in round 2 in 7620 steps
c [elim-23] fully completed in 2 rounds
c [elim-23] transition to [ all 0 rem 0 ] state
c [elim-23] eliminated 137 = 4% variables out of 3385 scheduled
c [bca-22] limit of 10000000 steps and 34214 added (scaled 2)
c [bca-22] 3906 out of 6498 literals actually usable 60%
c [bca-22] added 9 blocked clauses in 63001 steps
c [sweep-17] limit 15543516 penalty 0 = 0 + 0
c [sweep-17-1] 152 pos 23.3% + 499 neg 76.7% = 651 sched 20.0% ret 2597
c [sweep-17-1] 6295216 steps 320 queries 8.49 avg class size
c [sweep-17-1] 2328 decisions 317 SAT calls 42.82 avg env size
c [sweep-17-1] fully completed sweeping round
c [decomp-84] removed 3 variables
c [sweep-17-1] removed 3 vars (0 failed, 5 eqs, 7 impls)
c [sweep-17-2] 473 pos 14.6% + 2772 neg 85.4% = 3245 sched 100.0% ret 0
c [sweep-17-2] 9883692 steps 51 queries 97.29 avg class size
c [sweep-17-2] 2179 decisions 49 SAT calls 164.41 avg env size
c [sweep-17-2] 1631 variables remain 50% (1614 retained 50%)
c [sweep-17-2] removed 0 vars (0 failed, 1 eqs, 1 impls)
c [sweep-17] removed 3 vars in TOTAL (2 rounds, 369 queries)
c [score-distribution-26] 1961 pos 60.43%, 831 min 25.61%, 453 zero 13.96%
c [score-distribution-26] 1082 different 33.34% out of total 3245 variables
c [simplification-26] removed 234 variables 6.7% (3245 remain 2%)
c [simplification-26] removed 968 irredundant clauses 5.5% (16776 remain 2%)
c [simplification-26] maximum reduction of 7% = max (7%, 5%)
c [simplification-26] large reduction 7% >= 5% limit
c [simplification-26] next conflict interval 5981 = min (598117/100, 192000)
c [simplification-26] penalized conflict interval 5981 = 1 * 5981
c [simplification-26] hard conflict limit 614098 (soft 604098 + delta 10000)
c [simplification-26] new conflict limit 604098 (hard 614098)
c 
c [simplification-27] limit 604098 conflicts (hard 614098) hit after 614098 conflicts
c [ternres-23] limit 53351770 with penalty 0 = 0 + 0
c [ternres-23] all 3245 free variables schedulable
c [ternres-23] 4 ternary resolvents (0 bin, 4 trn)
c [ternres-23] fully completed ternary resolution
c [gauss-8] limit 666897 penalty 4 = 4 + 0
c [gauss-8] extracted 7 xors of average arity 3.0
c [gauss-8] connected 21 occurrences of 9 variables (average 2.3)
c [gauss-8] limit 666897 penalty 4 = 4 + 0
c [gauss-8] fully completed
c [gauss-8] exported 0 unary, 0 binary and 0 ternary equations
c [simpleprobe-10] all 3245 free variables schedulable
c [simpleprobe-10] limit 200000000 penalty 0 = 0 + 0
c [simpleprobe-10] fully completed simple probing
c [simpleprobe-10] removed 0 variables, found 2113 hbrs, 0 units
c [unhide-21] limit 1333794 with penalty 3 = 3 + 0
c [unhide-21-34] 0 units, 0 failed, 7793 tauts, 0 hbrs, 91156 literals
c [transred-23] limit 2000000 with penalty 0 = 0 + 0
c [transred-23] removed 438 transitive binary clauses
c [elim-24] scheduling all variables this time
c [elim-24] scheduled 3245 variables 100%
c [elim-24] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-24] rescheduling of touched variables disabled
c [elim-24-1] eliminated 10 variables 0% in round 1 in 972781 steps
c [elim-24-1] backward subsumption/strengthening limit 972700
c [elim-24-1-1] backward checking 88 touched variables 3%
c [elim-24-1-1] fully completed backward checking in 1 rounds
c [elim-24-1] subsumed 0 and strengthened 4 clauses in 9873 steps
c [elim-24-1] rescheduled 13 variables 0% by backward subsumption
c [elim-24-2] no variable eliminated in round 2 in 5534 steps
c [elim-24] fully completed in 2 rounds
c [elim-24] transition to [ all 0 rem 0 ] state
c [elim-24] eliminated 10 = 0% variables out of 3245 scheduled
c [elim-24] 10 < 1/100 * 3245 = 32 considered unsuccessful
c [bca-23] limit of 10000000 steps and 34162 added (scaled 2)
c [bca-23] 3819 out of 6472 literals actually usable 59%
c [bca-23] added 10 blocked clauses in 76349 steps
c [sweep-18] almost no limit of 4000000000 steps
c [sweep-18-1] 304 pos 18.7% + 1318 neg 81.3% = 1622 sched 50.1% ret 1613
c [sweep-18-1] 42129974 steps 414 queries 10.69 avg class size
c [sweep-18-1] 6848 decisions 412 SAT calls 63.57 avg env size
c [sweep-18-1] fully completed sweeping round
c [decomp-88] removed 2 variables
c [sweep-18-1] removed 2 vars (0 failed, 2 eqs, 2 impls)
c [sweep-18-2] 478 pos 14.8% + 2755 neg 85.2% = 3233 sched 100.0% ret 0
c [sweep-18-2] 43221933 steps 451 queries 15.23 avg class size
c [sweep-18-2] 8585 decisions 448 SAT calls 74.86 avg env size
c [sweep-18-2] fully completed sweeping round
c [decomp-89] removed 5 variables
c [sweep-18-2] removed 5 vars (0 failed, 4 eqs, 3 impls)
c [sweep-18-3] 477 pos 14.8% + 2751 neg 85.2% = 3228 sched 100.0% ret 0
c [sweep-18-3] 49588547 steps 455 queries 11.81 avg class size
c [sweep-18-3] 8561 decisions 452 SAT calls 73.19 avg env size
c [sweep-18-3] fully completed sweeping round
c [decomp-90] removed 5 variables
c [sweep-18-3] removed 5 vars (0 failed, 4 eqs, 1 impls)
c [sweep-18] removed 12 vars in TOTAL (3 rounds, 1317 queries)
c [score-distribution-27] 2072 pos 64.29%, 729 min 22.62%, 422 zero 13.09%
c [score-distribution-27] 1148 different 35.62% out of total 3223 variables
c [simplification-27] removed 22 variables 0.7% (3223 remain 2%)
c [simplification-27] removed 92 irredundant clauses 0.5% (16684 remain 2%)
c [simplification-27] maximum reduction of 1% = max (1%, 1%)
c [simplification-27] geometric conflict interval increment 96000 = 192000 / 2
c [simplification-27] new conflict interval 288000
c [simplification-27] penalized conflict interval 288000 = 1 * 288000
c [simplification-27] hard conflict limit 1046098 (soft 902098 + delta 144000)
c [simplification-27] new conflict limit 902098 (hard 1046098)
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 -  193.8    3223    16684    614098   37355    752 41749   19    24   12  78%   -448   -4   17   21   81%
c -  201.4    3223    16684    652734   37040    764 41750   18    22   20  80%    208   -6   17   21   83%
c -  209.3    3223    16684    694488   37959    786 41754   31    43   21  73%    592   16   44   21  212%
c -  218.6    3223    16684    737757   38963    804 41756   15    20   21  73%    801   -9    7   22   33%
c i  221.5    3222    16684    753607   53045    827 41762   20    28   28  72%    849   -1   17   22   81%
c i  224.8    3221    16684    769506   66262    843 41766   21    27   40  77%  -1064   -2   26   22  119%
c i  225.1    3219    16684    770844   67488    843 41767   24    32   40  74%  -1200    3   34   22  156%
c -  227.7    3219    16684    781604   39300    848 41767   27    36   31  75%   -940    7   34   22  151%
c i  228.5    3218    16684    786118   43395    849 41768   25    36   35  69%   -809    7   21   22   92%
c i  229.3    3115    16684    790536   47297    855 41770   27    37   36  72%   -913    7   23   23  100%
c i  229.4    3065    16684    790936   47644    855 41770   26    36   36  73%   -924    6   20   23   88%
c i  233.5    3062    16684    813423   66864    880 41776   19    25   40  76%   -398   -4   20   21   93%
c i  234.9    3061    16684    819984   72444    886 41777   25    34   43  73%   -585    6   33   22  151%
c -  236.5    3061    16684    826969   40366    896 41778   21    27   31  76%   -516   -2   15   22   68%
c i  240.4    3060    16684    848164   57668    938 41787   14    18   38  81%    -91  -10   10   21   46%
c i  240.5    3025    16684    848661   58131    938 41787   15    18   38  81%   -251  -10   15   21   71%
c -  246.5    3024    16684    874992   41849    959 41790   20    24   31  81%    -19   -5   16   22   72%
c i  248.4    3023    16684    886410   51069    971 41792   19    24   35  79%    148   -4   21   22   97%
c 
c [simplification-28] limit 902098 conflicts (hard 1046098) hit after 910332 conflicts
c [ternres-24] limit 79934483 with penalty 0 = 0 + 0
c [ternres-24] all 3022 free variables schedulable
c [ternres-24] 22 ternary resolvents (0 bin, 22 trn)
c [ternres-24] fully completed ternary resolution
c [card-7] limit 2497952 penalty 4 = 4 + 0
c [card-7] found 1632 at-most-one constraints of average size 3.5
c [card-7] found 29 at-most-two constraints of average size 4.1
c [card-7] using previous limit 2497952 for elimination
c [card-7] 1660 out of 1661 constraints (100%) meet size limits
c [card-7] no units found
c [card-7] generated 1725 at-most-one constraints, 1187 used 69%
c [card-7] exported 7791 binary clauses, 6.6 per/constraint
c [decomp-91] removed 227 variables
c [treelook-10] limit 7993448 penalty 0 = 0 + 0 boost 1
c [treelook-10] scheduled 5992 literals 100%
c [treelook-10] scheduling used 264112 steps
c [treelook-10] scheduled completely
c [treelook-10] limit 7993448 penalty 0 = 0 + 0 boost 1
c [treelook-10] used 8013712 steps
c [treelook-10] 4830 literals remain 84%
c [treelook-10] 2842 variables remain to probed next time 99%
c [decomp-92] removed 45 variables
c [treelook-10] removed 183 variables, found 53545 hbrs
c [transred-24] limit 2000000 with penalty 0 = 0 + 0
c [transred-24] removed 1927 transitive binary clauses
c [transred-24] found 6 units
c [cce-19] limit of 199836208 steps penalty 1 = 1 + 0
c [cce-19-1] eliminated 1 clauses out of 5 (20%) of length 9
c [cce-19-1] eliminated 1 clauses out of 10 (10%) of length 8
c [cce-19-1] eliminated 1 clauses out of 37 (3%) of length 7
c [cce-19-1] eliminated 5 clauses out of 128 (4%) of length 6
c [cce-19-1] eliminated 9 clauses out of 307 (3%) of length 5
c [cce-19-1] eliminated 69 clauses out of 805 (9%) of length 4
c [cce-19-1] completed large round (ACCE)
c [cce-19-1] eliminated 86 large clauses in 3006786 steps
c [cce-19-1] allowing another 1503393 steps for small clauses
c [cce-19-1] scheduling 10740 clauses = 8765 binary + 1975 ternary
c [cce-19-1] tried to eliminate 10740 small clauses 100%
c [cce-19-1] eliminated 541 binary clauses 6%
c [cce-19-1] eliminated 182 ternary clauses 9%
c [cce-19-1] eliminated 723 small clauses 7%
c [cce-19-1] eliminated 767 small clauses in 32000955 steps
c [cce-19-1] completed small round (ACCE)
c [cce-19-1] eliminated 853 covered clauses in round 1
c [cce-19-2] eliminated 3 clauses out of 298 (1%) of length 5
c [cce-19-2] eliminated 12 clauses out of 736 (2%) of length 4
c [cce-19-2] completed large round (ACCE)
c [cce-19-2] eliminated 15 large clauses in 2785096 steps
c [cce-19-2] allowing another 1392548 steps for small clauses
c [cce-19-2] scheduling 10017 clauses = 8224 binary + 1793 ternary
c [cce-19-2] tried to eliminate 10017 small clauses 100%
c [cce-19-2] eliminated 28 binary clauses 0%
c [cce-19-2] eliminated 15 ternary clauses 1%
c [cce-19-2] eliminated 43 small clauses 0%
c [cce-19-2] eliminated 43 small clauses in 29459423 steps
c [cce-19-2] completed small round (ACCE)
c [cce-19-2] eliminated 58 covered clauses in round 2
c [cce-19-3] eliminated 1 clauses out of 123 (1%) of length 6
c [cce-19-3] eliminated 2 clauses out of 295 (1%) of length 5
c [cce-19-3] eliminated 1 clauses out of 724 (0%) of length 4
c [cce-19-3] completed large round (ACCE)
c [cce-19-3] eliminated 4 large clauses in 2737609 steps
c [cce-19-3] allowing another 1368804 steps for small clauses
c [cce-19-3] scheduling 9974 clauses = 8196 binary + 1778 ternary
c [cce-19-3] tried to eliminate 9974 small clauses 100%
c [cce-19-3] eliminated 3 binary clauses 0%
c [cce-19-3] eliminated 1 ternary clauses 0%
c [cce-19-3] eliminated 4 small clauses 0%
c [cce-19-3] eliminated 4 small clauses in 29199704 steps
c [cce-19-3] completed small round (ACCE)
c [cce-19-3] eliminated 8 covered clauses in round 3
c [cce-19] eliminated 919 covered clauses in TOTAL during 3 rounds
c [bca-24] limit of 10000000 steps and 26325 added (scaled 2)
c [bca-24] 3522 out of 5614 literals actually usable 63%
c [bca-24] added 9 blocked clauses in 70222 steps
c [sweep-19] limit 23980345 penalty 0 = 0 + 0
c [sweep-19-1] 536 pos 19.1% + 2270 neg 80.9% = 2806 sched 100.0% ret 0
c [sweep-19-1] 24201293 steps 168 queries 25.58 avg class size
c [sweep-19-1] 4621 decisions 153 SAT calls 149.27 avg env size
c [sweep-19-1] 706 variables remain 25% (2087 retained 75%)
c [decomp-93] removed 35 variables
c [sweep-19-1] removed 35 vars (0 failed, 21 eqs, 10 impls)
c [sweep-19] removed 35 vars in TOTAL (1 rounds, 167 queries)
c [score-distribution-28] 1587 pos 57.27%, 851 min 30.71%, 333 zero 12.02%
c [score-distribution-28] 809 different 29.20% out of total 2771 variables
c [simplification-28] removed 251 variables 8.3% (2771 remain 2%)
c [simplification-28] removed 3978 irredundant clauses 23.8% (12706 remain 2%)
c [simplification-28] maximum reduction of 24% = max (8%, 24%)
c [simplification-28] large reduction 24% >= 5% limit
c [simplification-28] next conflict interval 9103 = min (910332/100, 288000)
c [simplification-28] penalized conflict interval 9103 = 1 * 9103
c [simplification-28] hard conflict limit 929435 (soft 919435 + delta 10000)
c [simplification-28] new conflict limit 919435 (hard 929435)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i  257.4    2770    12706    910766   63882   1063 76101   29    38   28  77%      7    9   31   22  140%
c -  261.5    2770    12706    928255   39617   1067 76103   20    25   20  81%    -51   -5   20   23   88%
c 
c [simplification-29] limit 919435 conflicts (hard 929435) hit after 929436 conflicts
c [quatres-17] found 1966 quaternary clauses 24% in total
c [quatres-17-1] removed 34 duplicate quaternary clauses
c [quatres-17-2] added 10 single-self-subsuming ternary resolvents
c [quatres-17-2] added 5 quaternary resolvents
c [ternres-25] limit 82127754 with penalty 0 = 0 + 0
c [ternres-25] all 2770 free variables schedulable
c [ternres-25] 22 ternary resolvents (0 bin, 22 trn)
c [ternres-25] fully completed ternary resolution
c [decomp-94] removed 2 variables
c [basicprobe-10] limit 400000000 penalty 0 = 0 + 0
c [basicprobe-10-0] 751 sched 29%, 128 failed, 4 lifted, 6223 hbrs
c [decomp-95] removed 202 variables
c [basicprobe-10-1] 685 sched 27%, 33 failed, 0 lifted, 4795 hbrs
c [decomp-96] removed 53 variables
c [basicprobe-10-2] 677 sched 27%, 8 failed, 0 lifted, 657 hbrs
c [decomp-97] removed 11 variables
c [basicprobe-10-3] 678 sched 27%, 5 failed, 0 lifted, 174 hbrs
c [decomp-98] removed 5 variables
c [basicprobe-10-4] 676 sched 27%, 3 failed, 0 lifted, 125 hbrs
c [decomp-99] removed 4 variables
c [basicprobe-10-5] 673 sched 27%, 1 failed, 0 lifted, 28 hbrs
c [decomp-100] removed 1 variables
c [basicprobe-10-6] 673 sched 27%, 0 failed, 0 lifted, 21 hbrs
c [basicprobe-10-7] 673 sched 27%, 0 failed, 0 lifted, 13 hbrs
c [basicprobe-10-8] 673 sched 27%, 0 failed, 0 lifted, 21 hbrs
c [basicprobe-10-8] round limit 8 hit
c [basicprobe-10-8] 182 units = 178 failed (98%) + 4 lifted (2%)
c [basicprobe-10-8] removed 276 variables, found 12057 hbrs
c [bate-8] eliminated 42 asymmetric tautologies during probing
c [transred-25] limit 2000000 with penalty 0 = 0 + 0
c [transred-25] removed 1879 transitive binary clauses
c [cce-20] limit of 410638774 steps penalty 0 = 0 + 0
c [cce-20-1] eliminated 2 clauses out of 224 (1%) of length 5
c [cce-20-1] eliminated 15 clauses out of 623 (2%) of length 4
c [cce-20-1] completed large round (ATE)
c [cce-20-1] eliminated 17 large clauses in 1915751 steps
c [cce-20-1] allowing another 957875 steps for small clauses
c [cce-20-1] scheduling 8826 clauses = 7448 binary + 1378 ternary
c [cce-20-1] tried to eliminate 8826 small clauses 100%
c [cce-20-1] eliminated 185 binary clauses 2%
c [cce-20-1] eliminated 12 ternary clauses 1%
c [cce-20-1] eliminated 197 small clauses 2%
c [cce-20-1] eliminated 197 small clauses in 21406911 steps
c [cce-20-1] completed small round (ATE)
c [cce-20-1] eliminated 214 covered clauses in round 1
c [cce-20-2] completed large round (ATE)
c [cce-20-2] allowing another 939988 steps for small clauses
c [cce-20-2] scheduling 8629 clauses = 7263 binary + 1366 ternary
c [cce-20-2] tried to eliminate 8629 small clauses 100%
c [cce-20-2] completed small round (ATE)
c [cce-20-2] eliminated 0 covered clauses in round 2
c [cce-20] eliminated 214 covered clauses in TOTAL during 2 rounds
c [elim-25] scheduling all variables this time
c [elim-25] scheduled 2493 variables 100%
c [elim-25] limit of 400000000 steps penalty 1 = 1 + 0
c [elim-25] rescheduling of touched variables disabled
c [elim-25-1] eliminated 378 variables 15% in round 1 in 618977 steps
c [elim-25-1] backward subsumption/strengthening limit 618900
c [elim-25-1-1] backward checking 1113 touched variables 45%
c [elim-25-1-1] fully completed backward checking in 1 rounds
c [elim-25-1] subsumed 0 and strengthened 2 clauses in 84618 steps
c [elim-25-1] rescheduled 16 variables 1% by backward subsumption
c [elim-25-2] eliminated 2 variables 0% in round 2 in 4721 steps
c [elim-25-2] backward subsumption/strengthening limit 4700
c [elim-25-2-1] backward checking 13 touched variables 1%
c [elim-25-2-1] incomplete backward checking 0 remain 0%
c [elim-25-2] subsumed 0 and strengthened 0 clauses in 4701 steps
c [elim-25-2] fully rescheduled 2113 variables 85%
c [elim-25-3] eliminated 10 variables 0% in round 3 in 585660 steps
c [elim-25-3] backward subsumption/strengthening limit 585600
c [elim-25-3-1] backward checking 59 touched variables 2%
c [elim-25-3-1] fully completed backward checking in 1 rounds
c [elim-25-3] subsumed 1 and strengthened 0 clauses in 10444 steps
c [elim-25] incomplete 3 not tried 0% in round 3
c [elim-25] transition to [ all 1 rem 1 ] state
c [elim-25] eliminated 390 = 16% variables out of 2493 scheduled
c [bca-25] limit of 10000000 steps and 21364 added (scaled 2)
c [bca-25] 2814 out of 4208 literals actually usable 67%
c [bca-25] added 20 blocked clauses in 32948 steps
c [sweep-20] limit 24638326 penalty 0 = 0 + 0
c [sweep-20-1] 141 pos 28.2% + 359 neg 71.8% = 500 sched 23.8% ret 1603
c [sweep-20-1] 6012103 steps 246 queries 9.19 avg class size
c [sweep-20-1] 2116 decisions 245 SAT calls 41.87 avg env size
c [sweep-20-1] fully completed sweeping round
c [decomp-103] removed 1 variables
c [sweep-20-1] removed 1 vars (0 failed, 1 eqs, 1 impls)
c [sweep-20-2] 370 pos 17.6% + 1732 neg 82.4% = 2102 sched 100.0% ret 0
c [sweep-20-2] 18646513 steps 210 queries 36.62 avg class size
c [sweep-20-2] 5653 decisions 210 SAT calls 80.08 avg env size
c [sweep-20-2] 322 variables remain 15% (1778 retained 85%)
c [decomp-104] removed 2 variables
c [sweep-20-2] removed 2 vars (0 failed, 1 eqs, 0 impls)
c [sweep-20] removed 3 vars in TOTAL (2 rounds, 454 queries)
c [score-distribution-29] 1143 pos 54.43%, 756 min 36.00%, 201 zero 9.57%
c [score-distribution-29] 677 different 32.24% out of total 2100 variables
c [simplification-29] removed 670 variables 24.2% (2100 remain 1%)
c [simplification-29] removed 2377 irredundant clauses 18.7% (10329 remain 1%)
c [simplification-29] maximum reduction of 24% = max (24%, 19%)
c [simplification-29] large reduction 24% >= 5% limit
c [simplification-29] next conflict interval 9294 = min (929436/100, 288000)
c [simplification-29] penalized conflict interval 9294 = 1 * 9294
c [simplification-29] hard conflict limit 948730 (soft 938730 + delta 10000)
c [simplification-29] new conflict limit 938730 (hard 948730)
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  266.8    2099    10329    938302   35328    765 40618   17    20   14  82%    102   -8   26   22  118%
c 
c [simplification-30] limit 938730 conflicts (hard 948730) hit after 948730 conflicts
c [ternres-26] limit 83222591 with penalty 0 = 0 + 0
c [ternres-26] all 2099 free variables schedulable
c [ternres-26] 33 ternary resolvents (1 bin, 32 trn)
c [ternres-26] fully completed ternary resolution
c [decomp-105] removed 1 variables
c [transred-26] limit 2000000 with penalty 0 = 0 + 0
c [transred-26] removed 1240 transitive binary clauses
c [cce-21] limit of 416112955 steps penalty 0 = 0 + 0
c [cce-21-1] eliminated 1 clauses out of 2 (50%) of length 21
c [cce-21-1] eliminated 1 clauses out of 3 (33%) of length 17
c [cce-21-1] eliminated 3 clauses out of 6 (50%) of length 13
c [cce-21-1] eliminated 1 clauses out of 2 (50%) of length 10
c [cce-21-1] eliminated 1 clauses out of 15 (7%) of length 9
c [cce-21-1] eliminated 1 clauses out of 26 (4%) of length 8
c [cce-21-1] eliminated 1 clauses out of 42 (2%) of length 7
c [cce-21-1] eliminated 6 clauses out of 138 (4%) of length 6
c [cce-21-1] eliminated 11 clauses out of 256 (4%) of length 5
c [cce-21-1] eliminated 28 clauses out of 666 (4%) of length 4
c [cce-21-1] completed large round (ACCE)
c [cce-21-1] eliminated 54 large clauses in 2479226 steps
c [cce-21-1] allowing another 1239613 steps for small clauses
c [cce-21-1] scheduling 7824 clauses = 6629 binary + 1195 ternary
c [cce-21-1] tried to eliminate 7824 small clauses 100%
c [cce-21-1] eliminated 171 binary clauses 3%
c [cce-21-1] eliminated 57 ternary clauses 5%
c [cce-21-1] eliminated 228 small clauses 3%
c [cce-21-1] eliminated 228 small clauses in 20965891 steps
c [cce-21-1] completed small round (ACCE)
c [cce-21-1] eliminated 282 covered clauses in round 1
c [cce-21-2] eliminated 1 clauses out of 1 (100%) of length 21
c [cce-21-2] eliminated 1 clauses out of 245 (0%) of length 5
c [cce-21-2] eliminated 2 clauses out of 638 (0%) of length 4
c [cce-21-2] completed large round (ACCE)
c [cce-21-2] eliminated 4 large clauses in 2285729 steps
c [cce-21-2] allowing another 1142864 steps for small clauses
c [cce-21-2] scheduling 7596 clauses = 6458 binary + 1138 ternary
c [cce-21-2] tried to eliminate 7596 small clauses 100%
c [cce-21-2] eliminated 3 binary clauses 0%
c [cce-21-2] eliminated 2 ternary clauses 0%
c [cce-21-2] eliminated 5 small clauses 0%
c [cce-21-2] eliminated 5 small clauses in 19931858 steps
c [cce-21-2] completed small round (ACCE)
c [cce-21-2] eliminated 9 covered clauses in round 2
c [cce-21-3] eliminated 1 clauses out of 25 (4%) of length 8
c [cce-21-3] eliminated 1 clauses out of 132 (1%) of length 6
c [cce-21-3] completed large round (ACCE)
c [cce-21-3] eliminated 2 large clauses in 2271543 steps
c [cce-21-3] allowing another 1135771 steps for small clauses
c [cce-21-3] scheduling 7591 clauses = 6455 binary + 1136 ternary
c [cce-21-3] tried to eliminate 7591 small clauses 100%
c [cce-21-3] completed small round (ACCE)
c [cce-21-3] eliminated 2 covered clauses in round 3
c [cce-21] eliminated 293 covered clauses in TOTAL during 3 rounds
c [elim-26] no untried remaining variables left
c [elim-26] scheduled 2099 variables 100%
c [elim-26] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-26] rescheduling of touched variables disabled
c [elim-26-1] eliminated 47 variables 2% in round 1 in 562410 steps
c [elim-26-1] backward subsumption/strengthening limit 562400
c [elim-26-1-1] backward checking 309 touched variables 15%
c [elim-26-1-1] fully completed backward checking in 1 rounds
c [elim-26-1] subsumed 1 and strengthened 0 clauses in 26190 steps
c [elim-26-1] rescheduled 2 variables 0% by backward subsumption
c [elim-26-2] no variable eliminated in round 2 in 621 steps
c [elim-26] fully completed in 2 rounds
c [elim-26] transition to [ all 0 rem 0 ] state
c [elim-26] eliminated 47 = 2% variables out of 2099 scheduled
c [bca-26] limit of 10000000 steps and 20550 added (scaled 2)
c [bca-26] 2635 out of 4106 literals actually usable 64%
c [bca-26] added 7 blocked clauses in 50778 steps
c [sweep-21] limit 24966777 penalty 0 = 0 + 0
c [sweep-21-1] 97 pos 30.8% + 218 neg 69.2% = 315 sched 15.4% ret 1737
c [sweep-21-1] 3856254 steps 178 queries 7.04 avg class size
c [sweep-21-1] 1346 decisions 177 SAT calls 38.79 avg env size
c [sweep-21-1] fully completed sweeping round
c [decomp-106] removed 1 variables
c [sweep-21-1] removed 1 vars (0 failed, 1 eqs, 0 impls)
c [sweep-21-2] 330 pos 16.1% + 1721 neg 83.9% = 2051 sched 100.0% ret 0
c [sweep-21-2] 21698940 steps 177 queries 17.02 avg class size
c [sweep-21-2] 5683 decisions 175 SAT calls 99.45 avg env size
c [sweep-21-2] 388 variables remain 19% (1663 retained 81%)
c [decomp-107] removed 2 variables
c [sweep-21-2] removed 2 vars (0 failed, 2 eqs, 3 impls)
c [sweep-21] removed 3 vars in TOTAL (2 rounds, 353 queries)
c [score-distribution-30] 1051 pos 51.29%, 800 min 39.04%, 198 zero 9.66%
c [score-distribution-30] 701 different 34.21% out of total 2049 variables
c [simplification-30] removed 50 variables 2.4% (2049 remain 1%)
c [simplification-30] removed 395 irredundant clauses 3.8% (9934 remain 1%)
c [simplification-30] maximum reduction of 4% = max (2%, 4%)
c [simplification-30] geometric conflict interval increment 57600 = 288000 / 5
c [simplification-30] new conflict interval 345600
c [simplification-30] penalized conflict interval 345600 = 1 * 345600
c [simplification-30] hard conflict limit 1467130 (soft 1294330 + delta 172800)
c [simplification-30] new conflict limit 1294330 (hard 1467130)
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  270.5    2048     9934    949000   46379    846 37916   17    21   19  79%   -131   -7   16   21   73%
c -  277.3    2048     9934    989070   40522    877 37920   18    24   17  75%    305   -2   14   20   69%
c i  279.6    2047     9934   1003890   52134    918 37934   16    19   21  82%    451   -6   12   20   59%
c i  281.5    1949     9934   1015845   61648    931 37939   17    20   24  82%   -180   -4   12   19   59%
c i  281.5    1948     9934   1015923   61688    941 37941   16    20   24  82%   -192   -5   10   19   51%
c i  281.5    1858     9934   1015924   61688    941 37941   16    20   24  82%   -192   -5   10   19   51%
c i  281.5    1802     9934   1015925   61688    941 37941   16    20   24  82%   -192   -5   10   19   51%
c i  281.5    1119     9934   1015928   61687    942 37942   16    20   24  82%   -193   -5   10   19   50%
c i  281.5    1117     9934   1015930   61687    942 37943   16    20   24  82%   -193   -5   10   19   50%
c 0  281.5     949     9934   1015930   61687    942 37943   16    20   24  82%   -193   -5   10   19   50%
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
s UNSATISFIABLE
c
c bate: 336 basic ate = 306 trn 91% + 30 lrg 9% in 8 updates
c bcas: 26 count, 355 added (267 skipped), 1086319 steps
c bkwd: tried 253627 clauses, 506615 lits, 2.00 lits/clause
c bkwd: checked 5357318 occs, 21.12 occs/clause, 10.57 occs/lit
c bkwd: subsumed 85 binary, 207 ternary, 190 large
c bkwd: strengthened 21 binary, 4 ternary (100% self), 658 large (0% self)
c blkd: 6 bces, 932 removed, 775721 resolutions, 2122002 steps
c blkd: 2630 blocking literals 1%, 3 pure
c bump: 1035752 bumped seen, 126935121 lits 122.6 on average
c card: 7 count, 0 units, 7791 am1, 20777632 steps
c card: 64 rescheduled, 590 eliminated, 7459 resolved, 69619 subsumed
c card: 22091 at-most-one constraints found, average size 4.36
c card: 22091 at-most-one constraints used 100%, average size 4.36
c card: 29 at-most-two constraints found, average size 4.10
c card: 28 at-most-two constraints used 97%, average size 4.11
c cces: 21 cces, 25645 eliminated, 23884 ate 93%, 1761 abce 7%
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: 2677487 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 232 gcs, 0 rescored clauses, 544 rescored vars
c dcps: 107 decompositions, 52002 equivalent 29%
c deco: 320 decision-only clauses 0%, 48% reduction
c decs: 2337108 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c dsch: 5522135 push, 5341734 pop (5341734 dec 100%)
c dsch: 143777326 swaps, 0 down, 96576735 up
c elms: 26 elims, 19861 eliminated 11%, 152 pure 1%
c elms: 79 rounds, 3.0 rounds/bve
c elms: 18749 small 94%, 957 large 5%
c elms: 73942 tried small, 18750 succeeded 25%, 55192 failed 75%
c elms: 5509 subsumed, 9728 strengthened, 738 blocked
c elms: 4502219 copies, 4100253 resolutions, 2308144 ipos
c elms: 727271 subchks, 511246 strchks
c gaus: 8 extractions, 1025 extracted, 2.3 size, 3 max
c gaus: exported 0 units, 4 binary and 1 ternary equations
c gaus: 0 gc, 16321170 steps, 8160585 extr 50%, 40443 elim 0%
c glue: 19.9 orig avg, 19.9 real avg, 4.1 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 284515 = 34484 simple 12% + 198468 trn 70% + 51563 lrg 18%, 1735 sub 1%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 1035752 clauses, 45.9 length
c lrnd: 47576303 lits = 84113548 orig - 36537245 removed 43%
c lrnd: 318349 uips 31%, 663081 flips 64%
c mins: 1031804 mins 100%, 302 bin 0%, 3312 size 0%
c mins: 196582679 poisoned searches, 16740846 hits, 9% hit rate
c mins: 262789072 used twice searches, 13906963 hits, 5% hit rate
c move: moved 22135, 17248 bin 78%, 4887 trn 22%
c otfs: 1549 driving 27%, 4207 restarting 73%
c otfs: str 5756, 5707 red 99%, 49 irr 1%
c otfs: str 5756, 0 bin 0%, 42 trn 1%, 5714 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: 9 computed, 19491 set, 0 pos (0%), 19491 neg (100%)
c prbs: 10 basic, 58764 probed, 1437 failed, 95 lifted
c prbs: 10 simple, 283835 probed, 1493 failed, 21182 eqs
c prbs: 10 treelook, 1449 probed, 123 failed, 0 lifted
c prom: 194391 locked 7% out of 2858335 tried
c prps: 415640664 props, 159 props/dec
c prps: 90% srch, 10% simp, 0% lkhd
c quat: 17 count, 33 quat, 15 self1, 0 self2, 70 dup
c redc: 7354 clauses 16%, 47131 tried 5%, 5 sat 0%
c redc: 20421 lits 3%, 596188 tried 1%, 5 sat 0%
c redc: 890 times jump level reduced, 4.7 levels on average
c reds: 23 count, 44170.9 conflicts per reduce
c reds: 0 memlim 0%, 23 arith 100%
c reds: 703629 collected 90%, 76493 retired 10%
c rmbd: 3642 removed, 1417 red 39%
c rsts: 21307 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: 30 count, 29 confs 97%, 0 vars 0%
c simp: 1 its 3%, 0 bin 0%, 0 trns 0%
c subl: 1035752 count (734387 tried 0.7), 112414 sub out of 1033881 (10.9%)
c swps: 21 count, 28 rounds, 4280 queries (152.9/round)
c swps: 4195 sat calls, 72 unsat (5.1% success rate)
c swps: 69009 decisions 16.5, 21371 conflicts 5.1
c swps; 46.7 avg class size, 67.7 avg environment size
c swps: 0 failed, 169 impls, 135 equivs
c swp0: 1414 type 0 queries, 531 unsat (37.6%), 1387 sat (98.1%)
c swp1: 2866 type 1 queries, 1322 unsat (46.1%), 2758 sat (96.2%)
c sync: 0 produced units, 0 successful consumptions 0%
c sync: 0 consume units calls, 0 tried 0%, 0 success 0%
c sync: 0 produced clauses, 0 successful consumptions 0%
c sync: 0 consume clause calls, 0 tried 0%, 0 success 0%
c time: 6747512 calls to obtain time
c tops: 107796 fixed 60%, 95 its, 10694.00 confs/it
c trds: 26 transitive reductions, 16348 removed, 117 failed
c trds: 80252 nodes, 206699 edges, 49077307 steps
c trim: 988551 words, 3.8 MB
c trnr: 26 count, 2 bin, 1426 trn, 34504626 steps
c unhd: 21 count, 34 rounds, 17625696 steps
c unhd: 508 non-trivial sccs of average size 2.2
c unhd: 49 units, 48 bin, 0 trn, 1 lrg
c unhd: 2078 failed, 2053 stamp, 0 lits, 15 bin, 5 trn, 1 lrg
c unhd: 69001 tauts, 3361 bin 5%, 1460 trn 2%, 1518 lrg 2%
c unhd: 69001 tauts, 62662 stamp 91%, 52597 red 76%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 299442 str, 48 bin 0%, 936 trn 0%, 298458 lrg 100%, 296224 red 99%
c vars: 949 remaining 1% and 179659 removed 99% out of 180608
c vars: 107796 fixed 60%, 19861 eliminated 11%, 52002 equivalent 29%
c vsts: 9432553550 visits, 94% srch, 6% simp, 0% lkhd
c vsts: 23.8 search visits per propagation, 8726.3 per conflict
c wchs: 2734359448 pushed, 13916223 enlarged, 369 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all        1033914        703629         76493      33179772       9017328        460988
c 
c  0 0         21393   2      3539   1         0   0  11921308  36   1969786  22     45324  10     0.5
c  1 5         18218   2      7543   1      2548   3   3387941  10    876249  10     27625   6     0.3
c  2 6         94926   9     54332   8      9284  12   6406260  19<  1956591  22<    82636  18     1.3
c  3 9        236221  23    165558  24     14506  19   6418501  19   2141600  24    119536  26<    2.7
c  4 14       286396  28<   211677  30<    15592  20<  2885816   9   1146715  13     87898  19     3.5
c  5 21       198814  19    142305  20     14313  19   1330201   4    536993   6     53249  12     2.6
c  6 30       103093  10     70401  10     10355  14    492407   1    230117   3     24088   5     1.8
c  7 41        47686   5     31683   5      5811   8    198529   1     99532   1     12346   3     1.1
c  8 54        19603   2     12530   2      2754   4     97801   0     44160   0      6248   1     0.6
c  9 69         5647   1      3345   0       983   1     26531   0     12567   0      1676   0     0.2
c 10 86         1627   0       703   0       332   0     12961   0      2596   0       304   0     0.1
c 11 126         275   0        13   0        14   0      1497   0       413   0        56   0     0.1
c 12 230          15   0         0   0         1   0        19   0         9   0         2   0     0.0
c 
c avg                  4.1           4.2           4.4           1.8           2.3           3.2
c std                  1.6           1.5           1.8           1.7           1.8           1.8
c 
c   33.303  12% cce
c   15.056   5% probe
c    9.759   3% sweep
c    5.632   2% unhide
c    5.090   2% bump
c    4.180   1% elim
c    2.816   1% transred
c 
c    3.921 < 1% rest (below)
c 
c    1.741   1% decide
c    0.691   0% bca
c    0.448   0% gauss
c    0.338   0% block
c    0.314   0% card
c    0.205   0% ternres
c    0.093   0% rescore
c    0.091   0% quatres
c    0.000   0% locs
c    0.000   0% queuesort
c ==================================
c    1.692   1% preprocessing     2%
c   73.540  26% inprocessing     98%
c ==================================
c   75.232  27% simplifying
c  206.270  73% search
c ==================================
c  281.506 100% all
c 
c       1015930 conflicts,        3608.9 confs/sec
c           956 ternaries,        1062.7 confs/ternary
c           414 binaries,         2453.9 confs/binary
c            95 iterations,      10694.0 confs/iteration
c 
c            23 reductions,          0.1 redus/sec,  44170.9 confs/reduction
c         21307 restarts,           75.7 rests/sec,     47.7 confs/restart
c       2337108 decisions,        8302.2 decis/sec,      2.3 decis/conflict
c     415640664 propagations,  1476490.7 props/sec,    177.8 props/decision
c 
c 281.5 seconds, 56.3 MB
c launch: done
