c launch: /data/cnf/sc2014/app/atco_enc1_opt2_05_4.cnf.bz2
c host: atom27
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/atco_enc1_opt2_05_4.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/atco_enc1_opt2_05_4.cnf.bz2
c no embedded options
c found 'p cnf 14636 386163' header
c read 14636 variables, 386163 clauses, 1652800 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 14409 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   14409   371044         0       0      0     0    0     0   23   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 3123 at-most-one constraints of average size 3.0
c [card-1] found 64 at-most-two constraints of average size 4.0
c [card-1] using previous limit 2000000 for elimination
c [card-1] 3186 out of 3187 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 1111 variables
c [simpleprobe-1] all 13525 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 258 variables
c [simpleprobe-1] 11193 variables remain 84% (2074 retained 16%)
c [simpleprobe-1] removed 258 variables, found 1943 hbrs, 8 units
c [unhide-1] limit 100000 with penalty 0 = 0 + 0
c [unhide-1-1] 54 units, 20 failed, 5914 tauts, 0 hbrs, 58 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 13195 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 3538 variables 27% in round 1 in 15295870 steps
c [elim-1-1] backward subsumption/strengthening limit 4704130
c [elim-1-1-1] backward checking 9353 touched variables 71%
c [elim-1-1-1] incomplete backward checking 8888 remain 95%
c [elim-1-1] subsumed 148 and strengthened 0 clauses in 4705085 steps
c [elim-1] incomplete 23 not tried 0% in round 1
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 3538 = 27% variables out of 13195 scheduled
c [elim-1] considered successful since not run to completion yet
c [phase-count-1] 321821 negative 93.0% of 345904 except 24083 7.0%
c [phase-count-1] 326580 positive 94.4% of 345904 except 19324 5.6%
c [phase-1] phase bias: 4898 positive 51%, 4759 negative 49%
c [score-distribution-1] 0 pos 0.00%, 0 min 0.00%, 9657 zero 100.00%
c [score-distribution-1] 1 different 0.01% out of total 9657 variables
c [simplification-1] removed 4507 variables 31.8% (9657 remain 67%)
c [simplification-1] removed 25140 irredundant clauses 6.8% (345904 remain 93%)
c [simplification-1] maximum reduction of 32% = max (32%, 7%)
c [simplification-1] large reduction 32% >= 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 [simplification-2] limit 1000 conflicts (hard 11000) hit after 1000 conflicts
c [decomp-3] removed 11 variables
c [simpleprobe-2] 8197 schedulable variables 85%
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [simpleprobe-2] 8226 variables remain 85% (1420 retained 15%)
c [simpleprobe-2] removed 0 variables, found 155 hbrs, 0 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 6593 literals 34%
c [treelook-1] scheduling used 301368 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 308399 steps
c [treelook-1] 6579 literals remain 34%
c [treelook-1] 5711 variables remain to probed next time 59%
c [decomp-5] removed 1 variables
c [treelook-1] removed 1 variables, found 71 hbrs
c [basicprobe-1] limit 2766976 based on 345872 irredundant clauses
c [basicprobe-1-0] 897 probes remain 9% after last round
c [basicprobe-1-0] 14 units = 14 failed (100%) + 0 lifted (0%)
c [basicprobe-1-0] removed 14 variables, found 4314 hbrs
c [unhide-2] limit 100000 with penalty 0 = 0 + 0
c [unhide-2-2] 0 units, 3 failed, 1439 tauts, 0 hbrs, 712 literals
c [elim-2] no untried remaining variables left
c [elim-2] scheduled 9627 variables 100%
c [elim-2] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-2] rescheduling of touched variables disabled
c [elim-2] incomplete 2455 not tried 26% in round 1
c [elim-2] transition to [ all 1 rem 1 ] state
c [elim-2] eliminated 99 = 1% variables out of 9627 scheduled
c [elim-2] considered successful since not run to completion yet
c [phase-count-2] 321023 negative 93.0% of 345075 except 24052 7.0%
c [phase-count-2] 325857 positive 94.4% of 345075 except 19218 5.6%
c [phase-2] phase bias: 7 positive 37%, 12 negative 63%
c [score-distribution-2] 1580 pos 16.58%, 0 min 0.00%, 7948 zero 83.42%
c [score-distribution-2] 877 different 9.20% out of total 9528 variables
c [simplification-2] removed 129 variables 1.3% (9528 remain 66%)
c [simplification-2] removed 817 irredundant clauses 0.2% (345075 remain 93%)
c [simplification-2] maximum reduction of 1% = max (1%, 0%)
c [simplification-2] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-2] new conflict interval 10000
c [simplification-2] penalized conflict interval 10000 = 1 * 10000
c [simplification-2] hard conflict limit 21000 (soft 11000 + delta 10000)
c [simplification-2] new conflict limit 11000 (hard 21000)
c 
c [simplification-3] limit of 178 binary hit after 178 binaries
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 1292 at-most-one constraints of average size 3.1
c [card-2] no at-most-two constraint found
c [card-2] using previous limit 1000000 for elimination
c [card-2] 1292 out of 1292 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [decomp-6] removed 166 variables
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] scheduled 6651 literals 36%
c [treelook-2] scheduling used 300002 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] used 302792 steps
c [treelook-2] 6626 literals remain 35%
c [treelook-2] 3844 variables remain to probed next time 41%
c [decomp-7] removed 2 variables
c [treelook-2] removed 2 variables, found 16 hbrs
c [unhide-3] limit 100000 with penalty 0 = 0 + 0
c [unhide-3-3] 0 units, 38 failed, 997 tauts, 0 hbrs, 7009 literals
c [elim-3] 2312 variables 25% will be scheduled this time
c [elim-3] scheduled 2312 variables 25%
c [elim-3] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-3] rescheduling of touched variables disabled
c [elim-3] incomplete 1392 not tried 15% in round 1
c [elim-3] transition to [ all 0 rem 1 ] state
c [elim-3] eliminated 0 = 0% variables out of 2312 scheduled
c [elim-3] considered successful since not run to completion yet
c [phase-count-3] 317436 negative 92.5% of 343056 except 25620 7.5%
c [phase-count-3] 323033 positive 94.2% of 343056 except 20023 5.8%
c [phase-3] phase bias: 1 positive 50%, 1 negative 50%
c [score-distribution-3] 1194 pos 12.77%, 940 min 10.06%, 7213 zero 77.17%
c [score-distribution-3] 838 different 8.97% out of total 9347 variables
c [simplification-3] removed 181 variables 1.9% (9347 remain 65%)
c [simplification-3] removed 2015 irredundant clauses 0.6% (343056 remain 92%)
c [simplification-3] maximum reduction of 2% = max (2%, 1%)
c [simplification-3] forced so keeping old conflict interval 10000
c [simplification-3] conflict limit remains at 11000 (hard 21000)
c [simplification-3] new binary interval 1000
c 
c [simplification-4] limit 11000 conflicts (hard 21000) hit after 11000 conflicts
c [basicprobe-2] limit 2744416 based on 343052 irredundant clauses
c [basicprobe-2-0] 171 probes remain 2% after last round
c [basicprobe-2-0] 12 units = 10 failed (83%) + 2 lifted (17%)
c [basicprobe-2-0] removed 10 variables, found 2238 hbrs
c [unhide-4] limit 103849 with penalty 0 = 0 + 0
c [unhide-4-4] 0 units, 0 failed, 1004 tauts, 0 hbrs, 9297 literals
c [elim-4] scheduling all variables this time
c [elim-4] scheduled 9337 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] incomplete 486 not tried 5% in round 1
c [elim-4] transition to [ all 1 rem 1 ] state
c [elim-4] eliminated 88 = 1% variables out of 9337 scheduled
c [elim-4] considered successful since not run to completion yet
c [phase-count-4] 316477 negative 92.5% of 342090 except 25613 7.5%
c [phase-count-4] 323256 positive 94.5% of 342090 except 18834 5.5%
c [phase-4] phase bias: 0 positive 0%, 2 negative 100%
c [score-distribution-4] 1634 pos 17.67%, 699 min 7.56%, 6916 zero 74.78%
c [score-distribution-4] 1137 different 12.29% out of total 9249 variables
c [simplification-4] removed 98 variables 1.0% (9249 remain 64%)
c [simplification-4] removed 962 irredundant clauses 0.3% (342090 remain 92%)
c [simplification-4] maximum reduction of 1% = max (1%, 0%)
c [simplification-4] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-4] new conflict interval 20000
c [simplification-4] penalized conflict interval 20000 = 1 * 20000
c [simplification-4] hard conflict limit 41000 (soft 31000 + delta 10000)
c [simplification-4] new conflict limit 31000 (hard 41000)
c 
c [simplification-5] limit 31000 conflicts (hard 41000) hit after 31000 conflicts
c [quatres-1] found 62268 quaternary clauses 27% in total
c [quatres-1-2] added 11 single-self-subsuming ternary resolvents
c [quatres-1-2] added 7 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 9249 free variables schedulable
c [ternres-1] 1175 ternary resolvents (3 bin, 1172 trn)
c [ternres-1] 1 variables remain 0% (9248 retained 100%)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 156 xors of average arity 2.6
c [gauss-1] connected 402 occurrences of 331 variables (average 1.2)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] fully completed
c [gauss-1] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-9] removed 70 variables
c [transred-1] limit 1634789 with penalty 0 = 0 + 0
c [transred-1] removed 1143 transitive binary clauses
c [block-1] scheduling all variables this time
c [block-1] scheduled 9179 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 1187 blocked clauses
c [block-1] 1187 < 1/100 * 341300 = 3413 considered unsuccessful
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 1 clauses out of 1 (100%) of length 17
c [cce-1-1] eliminated 192 clauses out of 3051 (6%) of length 12
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 193 large clauses in 30000013 steps
c [cce-1-1] allowing another 15000006 steps for small clauses
c [cce-1-1] scheduling 22456 clauses = 18653 binary + 3803 ternary
c [cce-1-1] tried to eliminate 898 small clauses 4%
c [cce-1-1] eliminated 41 binary clauses 0%
c [cce-1-1] eliminated 18 ternary clauses 0%
c [cce-1-1] eliminated 59 small clauses 0%
c [cce-1-1] eliminated 59 small clauses in 30000006 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 252 covered clauses in round 1
c [cce-1] eliminated 252 covered clauses in TOTAL during 1 rounds
c [cce-1] 252 < 1/100 * 340113 = 3401 considered unsuccessful
c [elim-5] 429 variables 5% will be scheduled this time
c [elim-5] scheduled 429 variables 5%
c [elim-5] limit of 32695782 steps penalty 0 = 0 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5] incomplete 400 not tried 4% in round 1
c [elim-5] transition to [ all 0 rem 1 ] state
c [elim-5] eliminated 0 = 0% variables out of 429 scheduled
c [bca-1] limit of 10000000 steps and 680222 added (scaled 2)
c [bca-1] 15365 out of 18360 literals actually usable 84%
c [bca-1] added 297 blocked clauses in 62772 steps
c [sweep-1] limit 1000000 penalty 0 = 0 + 0
c [sweep-1-1] 5275 pos 57.5% + 3904 neg 42.5% = 9179 sched 100.0% ret 0
c [sweep-1-1] 1120582 steps 11 queries 1502.55 avg class size
c [sweep-1-1] 657 decisions 10 SAT calls 138.20 avg env size
c [sweep-1-1] 9078 variables remain 99% (101 retained 1%)
c [decomp-10] removed 1 variables
c [sweep-1-1] removed 1 vars (0 failed, 0 eqs, 0 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 1 vars in TOTAL (1 rounds, 10 queries)
c [phase-count-5] 313940 negative 92.4% of 339861 except 25921 7.6%
c [phase-count-5] 321130 positive 94.5% of 339861 except 18731 5.5%
c [phase-5] phase bias: 0 positive 0%, 2 negative 100%
c [score-distribution-5] 1747 pos 19.03%, 748 min 8.15%, 6683 zero 72.82%
c [score-distribution-5] 1013 different 11.04% out of total 9178 variables
c [simplification-5] removed 71 variables 0.8% (9178 remain 64%)
c [simplification-5] removed 2228 irredundant clauses 0.7% (339861 remain 92%)
c [simplification-5] maximum reduction of 1% = max (1%, 1%)
c [simplification-5] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-5] new conflict interval 30000
c [simplification-5] penalized conflict interval 30000 = 1 * 30000
c [simplification-5] hard conflict limit 76000 (soft 61000 + delta 15000)
c [simplification-5] new conflict limit 61000 (hard 76000)
c 
c [simplification-6] limit 61000 conflicts (hard 76000) hit after 61000 conflicts
c [quatres-2] found 62327 quaternary clauses 26% in total
c [quatres-2-2] added 4 single-self-subsuming ternary resolvents
c [quatres-2-2] added 5 quaternary resolvents
c [ternres-2] limit 4054658 with penalty 0 = 0 + 0
c [ternres-2] 1 schedulable variables 0%
c [ternres-2] 0 ternary resolvents (0 bin, 0 trn)
c [ternres-2] fully completed ternary resolution
c [card-3] limit 506832 penalty 2 = 2 + 0
c [card-3] found 514 at-most-one constraints of average size 3.3
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 506832 for elimination
c [card-3] 514 out of 514 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [decomp-11] removed 16 variables
c [simpleprobe-3] 7820 schedulable variables 85%
c [simpleprobe-3] limit 8109317 penalty 1 = 1 + 0
c [decomp-12] removed 7 variables
c [simpleprobe-3] 7699 variables remain 84% (1456 retained 16%)
c [simpleprobe-3] removed 7 variables, found 418 hbrs, 0 units
c [unhide-5] limit 405465 with penalty 1 = 1 + 0
c [unhide-5-5] 0 units, 0 failed, 673 tauts, 0 hbrs, 57400 literals
c [transred-2] limit 2000000 with penalty 0 = 0 + 0
c [transred-2] removed 576 transitive binary clauses
c [bca-2] limit of 10000000 steps and 679084 added (scaled 2)
c [bca-2] 14596 out of 18312 literals actually usable 80%
c [bca-2] added 21 blocked clauses in 88291 steps
c [sweep-2] limit 1216397 penalty 0 = 0 + 0
c [sweep-2-1] 5305 pos 58.6% + 3749 neg 41.4% = 9054 sched 98.9% ret 101
c [sweep-2-1] 1607073 steps 30 queries 1232.07 avg class size
c [sweep-2-1] 1247 decisions 28 SAT calls 121.79 avg env size
c [sweep-2-1] 8813 variables remain 96% (342 retained 4%)
c [decomp-13] removed 8 variables
c [sweep-2-1] removed 8 vars (0 failed, 1 eqs, 1 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 8 vars in TOTAL (1 rounds, 29 queries)
c [phase-count-6] 313322 negative 92.4% of 339210 except 25888 7.6%
c [phase-count-6] 320874 positive 94.6% of 339210 except 18336 5.4%
c [phase-6] phase bias: 0 positive 0%, 0 negative 0%
c [score-distribution-6] 2321 pos 25.37%, 716 min 7.83%, 6110 zero 66.80%
c [score-distribution-6] 1446 different 15.81% out of total 9147 variables
c [simplification-6] removed 31 variables 0.3% (9147 remain 63%)
c [simplification-6] removed 651 irredundant clauses 0.2% (339210 remain 91%)
c [simplification-6] maximum reduction of 0% = max (0%, 0%)
c [simplification-6] full geometric conflict interval increment 30000
c [simplification-6] new conflict interval 60000
c [simplification-6] penalized conflict interval 60000 = 1 * 60000
c [simplification-6] hard conflict limit 151000 (soft 121000 + delta 30000)
c [simplification-6] new conflict limit 121000 (hard 151000)
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 -   25.1    9147   339210     63580   20029   2616  3527    8    33   26  25%    630   13    8    5  143%
c -   48.6    9147   339210    113814   29799   3013  3720    9    51   46  18%    841   17   10    7  142%
c 
c [simplification-7] limit 121000 conflicts (hard 151000) hit after 121001 conflicts
c [quatres-3] found 62848 quaternary clauses 26% in total
c [quatres-3-1] removed 3 duplicate quaternary clauses
c [quatres-3-1] added 1 double-self-subsuming ternary resolvents
c [quatres-3-2] added 23 single-self-subsuming ternary resolvents
c [quatres-3-2] added 16 quaternary resolvents
c [gauss-2] limit 1411519 penalty 1 = 1 + 0
c [gauss-2] extracted 96 xors of average arity 2.8
c [gauss-2] connected 272 occurrences of 218 variables (average 1.2)
c [gauss-2] limit 1411519 penalty 1 = 1 + 0
c [gauss-2] fully completed
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-14] removed 52 variables
c [treelook-3] limit 1411519 penalty 0 = 0 + 0 boost 1
c [treelook-3] scheduled 15199 literals 84%
c [treelook-3] scheduling used 816373 steps
c [treelook-3] scheduled completely
c [treelook-3] limit 1411519 penalty 0 = 0 + 0 boost 1
c [treelook-3] used 1442882 steps
c [treelook-3] 15109 literals remain 83%
c [treelook-3] 3608 variables remain to probed next time 40%
c [treelook-3] removed 26 variables, found 325 hbrs
c [transred-3] limit 2000000 with penalty 0 = 0 + 0
c [transred-3] removed 471 transitive binary clauses
c [transred-3] found 24 units
c [block-2] scheduling all variables this time
c [block-2] scheduled 9031 variables 100%
c [block-2] limit of 70575966 steps penalty 1 = 1 + 0
c [block-2] fully completed
c [block-2] transition to [ all 0 rem 0 ] state
c [block-2] eliminated 92 blocked clauses
c [block-2] 92 < 1/100 * 335774 = 3357 considered unsuccessful
c [cce-2] limit of 35287983 steps penalty 1 = 1 + 0
c [cce-2-1] eliminated 293 clauses out of 2482 (12%) of length 12
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] eliminated 293 large clauses in 35288183 steps
c [cce-2-1] allowing another 17644091 steps for small clauses
c [cce-2-1] scheduling 22811 clauses = 18265 binary + 4546 ternary
c [cce-2-1] tried to eliminate 932 small clauses 4%
c [cce-2-1] eliminated 64 binary clauses 0%
c [cce-2-1] eliminated 22 ternary clauses 0%
c [cce-2-1] eliminated 86 small clauses 0%
c [cce-2-1] eliminated 86 small clauses in 35287993 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 379 covered clauses in round 1
c [cce-2] eliminated 379 covered clauses in TOTAL during 1 rounds
c [cce-2] 379 < 1/100 * 334022 = 3340 considered unsuccessful
c [elim-6] scheduling all variables this time
c [elim-6] scheduled 9026 variables 100%
c [elim-6] limit of 141151933 steps penalty 1 = 1 + 0
c [elim-6] rescheduling of touched variables disabled
c [elim-6] incomplete 693 not tried 8% in round 1
c [elim-6] transition to [ all 1 rem 1 ] state
c [elim-6] eliminated 109 = 1% variables out of 9026 scheduled
c [bca-3] limit of 10000000 steps and 663091 added (scaled 2)
c [bca-3] 13530 out of 17836 literals actually usable 76%
c [bca-3] added 66 blocked clauses in 58823 steps
c [sweep-3] limit 4234557 penalty 0 = 0 + 0
c [sweep-3-1] 5129 pos 59.7% + 3462 neg 40.3% = 8591 sched 96.3% ret 326
c [sweep-3-1] 4545438 steps 60 queries 665.17 avg class size
c [sweep-3-1] 2309 decisions 59 SAT calls 101.17 avg env size
c [sweep-3-1] 7752 variables remain 87% (1165 retained 13%)
c [decomp-16] removed 12 variables
c [sweep-3-1] removed 12 vars (0 failed, 6 eqs, 4 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 12 vars in TOTAL (1 rounds, 59 queries)
c [score-distribution-7] 2609 pos 29.30%, 1251 min 14.05%, 5045 zero 56.65%
c [score-distribution-7] 1580 different 17.74% out of total 8905 variables
c [simplification-7] removed 242 variables 2.6% (8905 remain 62%)
c [simplification-7] removed 8262 irredundant clauses 2.4% (330948 remain 89%)
c [simplification-7] maximum reduction of 3% = max (3%, 2%)
c [simplification-7] geometric conflict interval increment 15000 = 60000 / 4
c [simplification-7] new conflict interval 75000
c [simplification-7] penalized conflict interval 75000 = 1 * 75000
c [simplification-7] hard conflict limit 233501 (soft 196001 + delta 37500)
c [simplification-7] new conflict limit 196001 (hard 233501)
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 -   77.6    8905   330948    164204   33661   2791  3669    9    29   43  32%    939   -9   10    8  116%
c -   97.8    8905   330948    207181   41706   2884  3690   10    27   44  37%    980   -5   10    9  113%
c 
c [simplification-8] limit 196001 conflicts (hard 233501) hit after 233502 conflicts
c [quatres-4] found 62507 quaternary clauses 25% in total
c [quatres-4-1] removed 6 duplicate quaternary clauses
c [quatres-4-1] added 70 double-self-subsuming ternary resolvents
c [quatres-4-2] added 71 single-self-subsuming ternary resolvents
c [quatres-4-2] added 196 quaternary resolvents
c [ternres-3] limit 18162671 with penalty 1 = 1 + 0
c [ternres-3] all 8905 free variables schedulable
c [ternres-3] 535 ternary resolvents (1 bin, 534 trn)
c [ternres-3] 27 variables remain 0% (8878 retained 100%)
c [decomp-17] removed 19 variables
c [basicprobe-3] limit 181626716 penalty 0 = 0 + 0
c [basicprobe-3-0] 229 sched 3%, 29 failed, 0 lifted, 1216 hbrs
c [decomp-18] removed 69 variables
c [basicprobe-3-1] 1360 sched 16%, 54 failed, 0 lifted, 2074 hbrs
c [decomp-19] removed 72 variables
c [basicprobe-3-2] 1388 sched 16%, 38 failed, 0 lifted, 774 hbrs
c [decomp-20] removed 68 variables
c [basicprobe-3-3] 1383 sched 16%, 22 failed, 1 lifted, 422 hbrs
c [decomp-21] removed 53 variables
c [basicprobe-3-4] 1374 sched 16%, 17 failed, 0 lifted, 161 hbrs
c [decomp-22] removed 30 variables
c [basicprobe-3-5] 1372 sched 16%, 9 failed, 0 lifted, 174 hbrs
c [decomp-23] removed 9 variables
c [basicprobe-3-6] 1371 sched 16%, 7 failed, 0 lifted, 107 hbrs
c [decomp-24] removed 13 variables
c [basicprobe-3-7] 1370 sched 16%, 1 failed, 0 lifted, 37 hbrs
c [decomp-25] removed 2 variables
c [basicprobe-3-8] 1370 sched 16%, 1 failed, 0 lifted, 1 hbrs
c [basicprobe-3-8] round limit 8 hit
c [basicprobe-3-8] 179 units = 178 failed (99%) + 1 lifted (1%)
c [basicprobe-3-8] removed 317 variables, found 4966 hbrs
c [bate-1] eliminated 1330 asymmetric tautologies during probing
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 1738 transitive binary clauses
c [elim-7] 307 variables 4% will be scheduled this time
c [elim-7] scheduled 307 variables 4%
c [elim-7] limit of 726506865 steps penalty 0 = 0 + 0
c [elim-7] rescheduling of touched variables disabled
c [elim-7-1] no variable eliminated in round 1 in 512915981 steps
c [elim-7] fully completed in 1 rounds
c [elim-7] transition to [ all 0 rem 0 ] state
c [elim-7] eliminated 0 = 0% variables out of 307 scheduled
c [bca-4] limit of 10000000 steps and 631830 added (scaled 2)
c [bca-4] 12566 out of 17140 literals actually usable 73%
c [bca-4] added 36 blocked clauses in 93432 steps
c [sweep-4] limit 10897602 penalty 0 = 0 + 0
c [sweep-4-1] 4503 pos 60.3% + 2970 neg 39.7% = 7473 sched 87.2% ret 1096
c [sweep-4-1] 10929358 steps 134 queries 225.75 avg class size
c [sweep-4-1] 5675 decisions 139 SAT calls 99.61 avg env size
c [sweep-4-1] 5790 variables remain 68% (2771 retained 32%)
c [decomp-26] removed 22 variables
c [sweep-4-1] removed 22 vars (0 failed, 13 eqs, 3 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 22 vars in TOTAL (1 rounds, 133 queries)
c [score-distribution-8] 1771 pos 20.72%, 2169 min 25.38%, 4607 zero 53.90%
c [score-distribution-8] 888 different 10.39% out of total 8547 variables
c [simplification-8] removed 358 variables 4.0% (8547 remain 59%)
c [simplification-8] removed 15965 irredundant clauses 4.8% (314983 remain 85%)
c [simplification-8] maximum reduction of 5% = max (4%, 5%)
c [simplification-8] large reduction 5% >= 5% limit
c [simplification-8] next conflict interval 2335 = min (233502/100, 75000)
c [simplification-8] penalized conflict interval 2335 = 1 * 2335
c [simplification-8] hard conflict limit 245837 (soft 235837 + delta 10000)
c [simplification-8] new conflict limit 235837 (hard 245837)
c 
c [simplification-9] limit 235837 conflicts (hard 245837) hit after 238369 conflicts
c [quatres-5] found 60155 quaternary clauses 26% in total
c [quatres-5-1] removed 8 duplicate quaternary clauses
c [quatres-5-1] added 9 double-self-subsuming ternary resolvents
c [quatres-5-2] added 231 single-self-subsuming ternary resolvents
c [quatres-5-2] added 874 quaternary resolvents
c [ternres-4] limit 37339802 with penalty 0 = 0 + 0
c [ternres-4] 25 schedulable variables 0%
c [ternres-4] 6220 ternary resolvents (412 bin, 5808 trn)
c [ternres-4] fully completed ternary resolution
c [decomp-27] removed 1 variables
c [simpleprobe-4] 7190 schedulable variables 84%
c [simpleprobe-4] limit 149359208 penalty 0 = 0 + 0
c [decomp-28] removed 9 variables
c [simpleprobe-4] 4488 variables remain 53% (4049 retained 47%)
c [simpleprobe-4] removed 9 variables, found 3016 hbrs, 0 units
c [unhide-6] limit 1866990 with penalty 2 = 2 + 0
c [unhide-6-6] 0 units, 2 failed, 3933 tauts, 0 hbrs, 49626 literals
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 1947 transitive binary clauses
c [bca-5] limit of 10000000 steps and 628336 added (scaled 2)
c [bca-5] 12347 out of 17072 literals actually usable 72%
c [bca-5] added 21 blocked clauses in 97706 steps
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 112019400 penalty 0 = 0 + 0
c [sweep-5-1] 3578 pos 61.9% + 2202 neg 38.1% = 5780 sched 67.7% ret 2755
c [sweep-5-1] 55561202 steps 1595 queries 20.39 avg class size
c [sweep-5-1] 47505 decisions 1535 SAT calls 85.91 avg env size
c [sweep-5-1] fully completed sweeping round
c [decomp-29] removed 147 variables
c [sweep-5-1] removed 147 vars (0 failed, 119 eqs, 26 impls)
c [sweep-5-2] 4892 pos 58.3% + 3496 neg 41.7% = 8388 sched 100.0% ret 0
c [sweep-5-2] 56480184 steps 977 queries 34.04 avg class size
c [sweep-5-2] 30730 decisions 966 SAT calls 85.70 avg env size
c [sweep-5-2] 1303 variables remain 16% (7067 retained 84%)
c [decomp-30] removed 72 variables
c [sweep-5-2] removed 72 vars (0 failed, 42 eqs, 18 impls)
c [sweep-5] removed 219 vars in TOTAL (2 rounds, 2570 queries)
c [score-distribution-9] 3248 pos 39.06%, 1423 min 17.11%, 3645 zero 43.83%
c [score-distribution-9] 1659 different 19.95% out of total 8316 variables
c [simplification-9] removed 231 variables 2.7% (8316 remain 58%)
c [simplification-9] removed 4610 irredundant clauses 1.5% (310373 remain 84%)
c [simplification-9] maximum reduction of 3% = max (3%, 1%)
c [simplification-9] geometric conflict interval increment 18750 = 75000 / 4
c [simplification-9] new conflict interval 93750
c [simplification-9] penalized conflict interval 93750 = 1 * 93750
c [simplification-9] hard conflict limit 378994 (soft 332119 + delta 46875)
c [simplification-9] new conflict limit 332119 (hard 378994)
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 -  129.7    8316   310373    243442   46486   7037  8711    9    17   27  53%    999  -10    9    9  102%
c -  145.5    8316   310373    281977   50356   7050  8712   10    15   28  63%   1010   -7   11    9  113%
c -  162.0    8316   310373    321229   52070   7055  8712    9    11   28  76%   1016   -8    9    9   93%
c 
c [simplification-10] limit 332119 conflicts (hard 378994) hit after 345278 conflicts
c [quatres-6] found 61242 quaternary clauses 26% in total
c [quatres-6-1] removed 110 duplicate quaternary clauses
c [quatres-6-1] added 37 double-self-subsuming ternary resolvents
c [quatres-6-2] added 281 single-self-subsuming ternary resolvents
c [quatres-6-2] added 943 quaternary resolvents
c [ternres-5] limit 58603404 with penalty 0 = 0 + 0
c [ternres-5] all 8316 free variables schedulable
c [ternres-5] 4546 ternary resolvents (246 bin, 4300 trn)
c [ternres-5] 1 variables remain 0% (8315 retained 100%)
c [card-4] limit 3662712 penalty 3 = 3 + 0
c [card-4] found 1192 at-most-one constraints of average size 3.2
c [card-4] found 272 at-most-two constraints of average size 4.1
c [card-4] using previous limit 3662712 for elimination
c [card-4] 1461 out of 1464 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [gauss-3] limit 2930170 penalty 2 = 2 + 0
c [gauss-3] extracted 115 xors of average arity 3.0
c [gauss-3] connected 345 occurrences of 184 variables (average 1.9)
c [gauss-3] limit 2930170 penalty 2 = 2 + 0
c [gauss-3] fully completed
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [treelook-4] limit 5860340 penalty 0 = 0 + 0 boost 1
c [treelook-4] scheduled 13325 literals 80%
c [treelook-4] scheduling used 839172 steps
c [treelook-4] scheduled completely
c [treelook-4] limit 5860340 penalty 0 = 0 + 0 boost 1
c [treelook-4] used 5995884 steps
c [treelook-4] 13040 literals remain 78%
c [treelook-4] 3116 variables remain to probed next time 38%
c [decomp-32] removed 3 variables
c [treelook-4] removed 13 variables, found 423 hbrs
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 2347 transitive binary clauses
c [transred-6] found 23 units
c [block-3] scheduling all variables this time
c [block-3] scheduled 8266 variables 100%
c [block-3] limit of 146508510 steps penalty 2 = 2 + 0
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 1701 blocked clauses
c [block-3] 1701 < 1/100 * 307839 = 3078 considered unsuccessful
c [cce-3] limit of 73254255 steps penalty 2 = 2 + 0
c [cce-3-1] eliminated 557 clauses out of 966 (58%) of length 12
c [cce-3-1] eliminated 250 clauses out of 296 (84%) of length 11
c [cce-3-1] eliminated 43 clauses out of 322 (13%) of length 10
c [cce-3-1] eliminated 201 clauses out of 1015 (20%) of length 9
c [cce-3-1] eliminated 193 clauses out of 1942 (10%) of length 8
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 1244 large clauses in 73254266 steps
c [cce-3-1] allowing another 36627133 steps for small clauses
c [cce-3-1] scheduling 92973 clauses = 18764 binary + 74209 ternary
c [cce-3-1] tried to eliminate 2690 small clauses 3%
c [cce-3-1] eliminated 110 binary clauses 1%
c [cce-3-1] eliminated 368 ternary clauses 0%
c [cce-3-1] eliminated 478 small clauses 1%
c [cce-3-1] eliminated 478 small clauses in 73254261 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 1722 covered clauses in round 1
c [cce-3] eliminated 1722 covered clauses in TOTAL during 1 rounds
c [cce-3] 1722 < 1/100 * 304372 = 3043 considered unsuccessful
c [elim-8] scheduling all variables this time
c [elim-8] scheduled 8190 variables 100%
c [elim-8] boosting limit by 20
c [elim-8] limit of 8000000000 steps penalty 1 = 1 + 0
c [elim-8] rescheduling of touched variables disabled
c [elim-8-1] eliminated 92 variables 1% in round 1 in 975468884 steps
c [elim-8-1] backward subsumption/strengthening limit 975468800
c [elim-8-1-1] backward checking 1545 touched variables 19%
c [elim-8-1-1] fully completed backward checking in 1 rounds
c [elim-8-1] subsumed 1866 and strengthened 1091 clauses in 513608252 steps
c [elim-8-1] rescheduled 408 variables 5% by backward subsumption
c [elim-8-2] eliminated 1 variables 0% in round 2 in 125505206 steps
c [elim-8-2] backward subsumption/strengthening limit 125505200
c [elim-8-2-1] backward checking 17 touched variables 0%
c [elim-8-2-1] fully completed backward checking in 1 rounds
c [elim-8-2] subsumed 0 and strengthened 0 clauses in 481317 steps
c [elim-8] fully completed in 2 rounds
c [elim-8] transition to [ all 0 rem 0 ] state
c [elim-8] eliminated 93 = 1% variables out of 8190 scheduled
c [bca-6] limit of 10000000 steps and 568294 added (scaled 2)
c [bca-6] 10877 out of 16196 literals actually usable 67%
c [bca-6] added 130 blocked clauses in 95048 steps
c [sweep-6] limit 17581021 penalty 0 = 0 + 0
c [sweep-6-1] 850 pos 68.1% + 399 neg 31.9% = 1249 sched 15.4% ret 6848
c [sweep-6-1] 14996404 steps 621 queries 11.85 avg class size
c [sweep-6-1] 17387 decisions 598 SAT calls 86.57 avg env size
c [sweep-6-1] fully completed sweeping round
c [decomp-33] removed 24 variables
c [sweep-6-1] removed 24 vars (0 failed, 40 eqs, 5 impls)
c [sweep-6-2] 4621 pos 57.2% + 3452 neg 42.8% = 8073 sched 100.0% ret 0
c [sweep-6-2] 2608437 steps 31 queries 1139.77 avg class size
c [sweep-6-2] 1201 decisions 30 SAT calls 101.77 avg env size
c [sweep-6-2] 7655 variables remain 95% (418 retained 5%)
c [sweep-6-2] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-6] removed 24 vars in TOTAL (2 rounds, 650 queries)
c [score-distribution-10] 2080 pos 25.76%, 2651 min 32.84%, 3342 zero 41.40%
c [score-distribution-10] 1048 different 12.98% out of total 8073 variables
c [simplification-10] removed 243 variables 2.9% (8073 remain 56%)
c [simplification-10] removed 26609 irredundant clauses 8.6% (283764 remain 76%)
c [simplification-10] maximum reduction of 9% = max (3%, 9%)
c [simplification-10] large reduction 9% >= 5% limit
c [simplification-10] next conflict interval 3452 = min (345278/100, 93750)
c [simplification-10] penalized conflict interval 3452 = 1 * 3452
c [simplification-10] hard conflict limit 358730 (soft 348730 + delta 10000)
c [simplification-10] new conflict limit 348730 (hard 358730)
c 
c [simplification-11] limit 348730 conflicts (hard 358730) hit after 348730 conflicts
c [quatres-7] found 58326 quaternary clauses 27% in total
c [quatres-7-1] removed 2 duplicate quaternary clauses
c [quatres-7-1] added 17 double-self-subsuming ternary resolvents
c [quatres-7-2] added 87 single-self-subsuming ternary resolvents
c [quatres-7-2] added 558 quaternary resolvents
c [ternres-6] limit 59380723 with penalty 0 = 0 + 0
c [ternres-6] 1 schedulable variables 0%
c [ternres-6] 4544 ternary resolvents (94 bin, 4450 trn)
c [ternres-6] fully completed ternary resolution
c [decomp-35] removed 1 variables
c [basicprobe-4] limit 296903618 penalty 0 = 0 + 0
c [basicprobe-4-0] 1326 sched 16%, 7 failed, 0 lifted, 1777 hbrs
c [decomp-36] removed 7 variables
c [basicprobe-4-1] 1323 sched 16%, 3 failed, 0 lifted, 274 hbrs
c [decomp-37] removed 3 variables
c [basicprobe-4-2] 1321 sched 16%, 1 failed, 0 lifted, 19 hbrs
c [decomp-38] removed 1 variables
c [basicprobe-4-3] 1320 sched 16%, 0 failed, 0 lifted, 30 hbrs
c [basicprobe-4-4] 1320 sched 16%, 0 failed, 0 lifted, 1 hbrs
c [basicprobe-4-5] 1320 sched 16%, 0 failed, 0 lifted, 7 hbrs
c [basicprobe-4-6] 1320 sched 16%, 0 failed, 0 lifted, 12 hbrs
c [basicprobe-4-7] 1320 sched 16%, 0 failed, 0 lifted, 1 hbrs
c [basicprobe-4-8] 1320 sched 16%, 0 failed, 0 lifted, 1 hbrs
c [basicprobe-4-8] round limit 8 hit
c [basicprobe-4-8] 11 units = 11 failed (100%) + 0 lifted (0%)
c [basicprobe-4-8] removed 11 variables, found 2122 hbrs
c [bate-2] eliminated 1324 asymmetric tautologies during probing
c [unhide-7] limit 5938072 with penalty 1 = 1 + 0
c [unhide-7-8] 0 units, 0 failed, 11964 tauts, 0 hbrs, 19342 literals
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 715 transitive binary clauses
c [elim-9] scheduling all variables this time
c [elim-9] scheduled 8061 variables 100%
c [elim-9] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-9] rescheduling of touched variables disabled
c [elim-9] incomplete 15 not tried 0% in round 1
c [elim-9] transition to [ all 1 rem 1 ] state
c [elim-9] eliminated 89 = 1% variables out of 8061 scheduled
c [bca-7] limit of 10000000 steps and 545063 added (scaled 2)
c [bca-7] 10590 out of 15946 literals actually usable 66%
c [bca-7] added 50 blocked clauses in 94902 steps
c [sweep-7] limit 17814217 penalty 0 = 0 + 0
c [sweep-7-1] 4377 pos 57.9% + 3187 neg 42.1% = 7564 sched 94.9% ret 408
c [sweep-7-1] 18714540 steps 473 queries 58.07 avg class size
c [sweep-7-1] 13473 decisions 481 SAT calls 77.58 avg env size
c [sweep-7-1] 3117 variables remain 39% (4845 retained 61%)
c [decomp-44] removed 41 variables
c [sweep-7-1] removed 41 vars (0 failed, 19 eqs, 3 impls)
c [sweep-7] removed 41 vars in TOTAL (1 rounds, 472 queries)
c [score-distribution-11] 2324 pos 29.30%, 2430 min 30.64%, 3177 zero 40.06%
c [score-distribution-11] 1156 different 14.58% out of total 7931 variables
c [simplification-11] removed 142 variables 1.8% (7931 remain 55%)
c [simplification-11] removed 12301 irredundant clauses 4.3% (271463 remain 73%)
c [simplification-11] maximum reduction of 4% = max (2%, 4%)
c [simplification-11] geometric conflict interval increment 18750 = 93750 / 5
c [simplification-11] new conflict interval 112500
c [simplification-11] penalized conflict interval 112500 = 1 * 112500
c [simplification-11] hard conflict limit 517480 (soft 461230 + delta 56250)
c [simplification-11] new conflict limit 461230 (hard 517480)
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 -  219.2    7931   271463    363092   51297  12171  6556   11    17   25  64%   1020    0   12   10  125%
c -  235.4    7931   271463    404907   53566  12178  6556   11    16   26  69%   1022    0   12   10  123%
c i  251.1    7930   271463    455253   90051  12238  6566    7     9   32  86%   1023   -4    5    9   55%
c -  251.1    7794   271463    455321   57681  12238  6566    7     9   26  85%    560   -4    6    9   63%
c i  266.5    7793   271463    497952   91917  12305  6580    8    10   33  80%  -2743   -2    5    9   58%
c -  267.2    7597   271463    499830   59409  12306  6580    8    11   26  79%  -3187   -2    9    9   97%
c i  271.6    7596   271463    514361   69883  12339  6590    8     9   30  84%  -2436   -3    6    9   63%
c 
c [simplification-12] limit 461230 conflicts (hard 517480) hit after 517481 conflicts
c [quatres-8] found 46701 quaternary clauses 29% in total
c [quatres-8-1] removed 74 duplicate quaternary clauses
c [quatres-8-2] added 174 single-self-subsuming ternary resolvents
c [quatres-8-2] added 352 quaternary resolvents
c [ternres-7] limit 91045787 with penalty 0 = 0 + 0
c [ternres-7] all 7527 free variables schedulable
c [ternres-7] 7937 ternary resolvents (268 bin, 7669 trn)
c [ternres-7] fully completed ternary resolution
c [decomp-45] removed 452 variables
c [simpleprobe-5] 3879 schedulable variables 52%
c [simpleprobe-5] limit 200000000 penalty 0 = 0 + 0
c [decomp-46] removed 25 variables
c [simpleprobe-5] 3138 variables remain 42% (4316 retained 58%)
c [simpleprobe-5] removed 25 variables, found 4135 hbrs, 6 units
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 2605 transitive binary clauses
c [transred-8] found 11 units
c [elim-10] 10 variables 0% will be scheduled this time
c [elim-10] scheduled 10 variables 0%
c [elim-10] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-10] rescheduling of touched variables disabled
c [elim-10-1] no variable eliminated in round 1 in 109853679 steps
c [elim-10] fully completed in 1 rounds
c [elim-10] transition to [ all 0 rem 0 ] state
c [elim-10] eliminated 0 = 0% variables out of 10 scheduled
c [bca-8] limit of 10000000 steps and 470302 added (scaled 2)
c [bca-8] 10250 out of 14878 literals actually usable 69%
c [bca-8] added 50 blocked clauses in 71626 steps
c [sweep-8] limit 27313736 penalty 0 = 0 + 0
c [sweep-8-1] 1864 pos 63.1% + 1089 neg 36.9% = 2953 sched 39.7% ret 4485
c [sweep-8-1] 25447444 steps 1018 queries 15.05 avg class size
c [sweep-8-1] 27224 decisions 1012 SAT calls 78.93 avg env size
c [sweep-8-1] fully completed sweeping round
c [decomp-47] removed 71 variables
c [sweep-8-1] removed 71 vars (0 failed, 41 eqs, 16 impls)
c [sweep-8-2] 4271 pos 58.0% + 3096 neg 42.0% = 7367 sched 100.0% ret 0
c [sweep-8-2] 1921522 steps 28 queries 1227.64 avg class size
c [sweep-8-2] 1116 decisions 27 SAT calls 106.30 avg env size
c [sweep-8-2] 7209 variables remain 98% (157 retained 2%)
c [decomp-48] removed 2 variables
c [sweep-8-2] removed 2 vars (0 failed, 0 eqs, 0 impls)
c [sweep-8] removed 73 vars in TOTAL (2 rounds, 1044 queries)
c [score-distribution-12] 2549 pos 34.61%, 2036 min 27.64%, 2780 zero 37.75%
c [score-distribution-12] 1280 different 17.38% out of total 7365 variables
c [simplification-12] removed 162 variables 2.2% (7365 remain 51%)
c [simplification-12] removed 37111 irredundant clauses 13.7% (234352 remain 63%)
c [simplification-12] maximum reduction of 14% = max (2%, 14%)
c [simplification-12] large reduction 14% >= 5% limit
c [simplification-12] next conflict interval 5174 = min (517481/100, 112500)
c [simplification-12] penalized conflict interval 5174 = 1 * 5174
c [simplification-12] hard conflict limit 532655 (soft 522655 + delta 10000)
c [simplification-12] new conflict limit 522655 (hard 532655)
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  280.9    7364   234352    529815   59399   9753  9418    8     9   24  82%  -1915   -2    6    9   69%
c i  281.1    7333   234352    530605   59905   9768  9423    8     9   24  83%  -2009   -3    6    9   66%
c i  281.6    7328   234352    532267   60970   9799  9433    7     8   24  83%  -2031   -3    5    9   54%
c 
c [simplification-13] limit 522655 conflicts (hard 532655) hit after 532655 conflicts
c [quatres-9] found 49044 quaternary clauses 31% in total
c [quatres-9-1] removed 96 duplicate quaternary clauses
c [quatres-9-1] added 15 double-self-subsuming ternary resolvents
c [quatres-9-2] added 206 single-self-subsuming ternary resolvents
c [quatres-9-2] added 191 quaternary resolvents
c [ternres-8] limit 93512612 with penalty 0 = 0 + 0
c [ternres-8] all 7304 free variables schedulable
c [ternres-8] 6907 ternary resolvents (146 bin, 6761 trn)
c [ternres-8] fully completed ternary resolution
c [decomp-49] removed 67 variables
c [treelook-5] limit 9351261 penalty 0 = 0 + 0 boost 1
c [treelook-5] scheduled 11184 literals 77%
c [treelook-5] scheduling used 615025 steps
c [treelook-5] scheduled completely
c [treelook-5] limit 9351261 penalty 0 = 0 + 0 boost 1
c [treelook-5] used 9375576 steps
c [treelook-5] 10908 literals remain 75%
c [treelook-5] 2611 variables remain to probed next time 36%
c [decomp-50] removed 1 variables
c [treelook-5] removed 2 variables, found 475 hbrs
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 2523 transitive binary clauses
c [transred-9] found 20 units
c [bca-9] limit of 10000000 steps and 451729 added (scaled 2)
c [bca-9] 9682 out of 14482 literals actually usable 67%
c [bca-9] added 24 blocked clauses in 63535 steps
c [sweep-9] limit 28053783 penalty 0 = 0 + 0
c [sweep-9-1] 4112 pos 58.0% + 2973 neg 42.0% = 7085 sched 97.9% ret 155
c [sweep-9-1] 28066402 steps 699 queries 37.76 avg class size
c [sweep-9-1] 17980 decisions 691 SAT calls 75.37 avg env size
c [sweep-9-1] 1707 variables remain 24% (5475 retained 76%)
c [decomp-51] removed 100 variables
c [sweep-9-1] removed 100 vars (0 failed, 37 eqs, 28 impls)
c [sweep-9] removed 100 vars in TOTAL (1 rounds, 698 queries)
c [score-distribution-13] 2370 pos 33.19%, 2198 min 30.78%, 2572 zero 36.02%
c [score-distribution-13] 1252 different 17.54% out of total 7140 variables
c [simplification-13] removed 164 variables 2.2% (7140 remain 50%)
c [simplification-13] removed 10840 irredundant clauses 4.6% (223512 remain 60%)
c [simplification-13] maximum reduction of 5% = max (2%, 5%)
c [simplification-13] large reduction 5% >= 5% limit
c [simplification-13] next conflict interval 5326 = min (532655/100, 112500)
c [simplification-13] penalized conflict interval 5326 = 1 * 5326
c [simplification-13] hard conflict limit 547981 (soft 537981 + delta 10000)
c [simplification-13] new conflict limit 537981 (hard 547981)
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  285.0    7139   223512    533502   35802  15464  8938    7     9   21  78%  -2009   -3    5    9   55%
c i  285.1    6963   223512    533839   35980  15479  8943    7     8   21  79%  -2003   -3    5    9   59%
c i  285.2    6956   223512    534126   36143  15490  8946    7     8   21  79%  -1997   -3    5    9   55%
c i  285.2    6925   223512    534204   36151  15506  8953    6     8   21  79%  -1995   -3    4    9   51%
c i  285.2    6900   223512    534266   36172  15513  8955    6     8   21  79%  -1994   -3    4    9   50%
c i  285.2    6897   223512    534272   36172  15514  8958    6     8   21  79%  -1994   -3    4    9   49%
c i  285.2    6870   223512    534289   36174  15516  8959    6     8   21  79%  -1994   -4    4    9   49%
c i  285.2    6715   223512    534299   36176  15517  8960    6     8   21  79%  -1993   -4    4    9   49%
c i  285.2    6099   223512    534301   36176  15517  8961    6     8   21  79%  -1993   -4    4    9   48%
c 0  285.2    5742   223512    534301   36176  15517  8961    6     8   21  79%  -1993   -4    4    9   48%
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: 2654 basic ate = 296 trn 11% + 2358 lrg 89% in 2 updates
c bcas: 9 count, 695 added (1292 skipped), 726135 steps
c bkwd: tried 168835 clauses, 334565 lits, 1.98 lits/clause
c bkwd: checked 267918673 occs, 1586.87 occs/clause, 800.80 occs/lit
c bkwd: subsumed 1 binary, 604 ternary, 1409 large
c bkwd: strengthened 0 binary, 263 ternary (100% self), 828 large (0% self)
c blkd: 3 bces, 2980 removed, 4421747 resolutions, 14515222 steps
c blkd: 910 blocking literals 3%, 81 pure
c bump: 541503 bumped seen, 24641198 lits 45.5 on average
c card: 4 count, 0 units, 0 am1, 15889668 steps
c card: 0 rescheduled, 0 eliminated, 0 resolved, 17597 subsumed
c card: 6121 at-most-one constraints found, average size 3.10
c card: 6121 at-most-one constraints used 100%, average size 3.10
c card: 336 at-most-two constraints found, average size 4.06
c card: 332 at-most-two constraints used 99%, average size 4.06
c cces: 3 cces, 2353 eliminated, 2102 ate 89%, 251 abce 11%
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: 2038963 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 81 gcs, 0 rescored clauses, 284 rescored vars
c dcps: 51 decompositions, 1685 equivalent 12%
c deco: 0 decision-only clauses 0%, 0% reduction
c decs: 1723470 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c dsch: 5828867 push, 5814251 pop (5814251 dec 100%)
c dsch: 113174110 swaps, 0 down, 39019960 up
c elms: 10 elims, 4097 eliminated 28%, 619 pure 15%
c elms: 13 rounds, 1.3 rounds/bve
c elms: 2499 small 61%, 898 large 22%
c elms: 3291 tried small, 2499 succeeded 76%, 792 failed 24%
c elms: 30279 subsumed, 2545 strengthened, 48 blocked
c elms: 5425516 copies, 6318316 resolutions, 57945 ipos
c elms: 16923565 subchks, 4603879 strchks
c gaus: 3 extractions, 367 extracted, 2.8 size, 3 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 12692336 steps, 6346168 extr 50%, 4854 elim 0%
c glue: 9.1 orig avg, 9.1 real avg, 2.3 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 33310 = 9667 simple 29% + 23125 trn 69% + 518 lrg 2%, 1520 sub 5%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 541503 clauses, 18.9 length
c lrnd: 10225497 lits = 16022335 orig - 5796838 removed 36%
c lrnd: 165121 uips 30%, 322981 flips 60%
c mins: 535027 mins 99%, 765 bin 0%, 5711 size 1%
c mins: 12348358 poisoned searches, 2086037 hits, 17% hit rate
c mins: 25709010 used twice searches, 2383005 hits, 9% hit rate
c move: moved 3613, 242 bin 7%, 3371 trn 93%
c otfs: 3449 driving 35%, 6475 restarting 65%
c otfs: str 9924, 9704 red 98%, 220 irr 2%
c otfs: str 9924, 0 bin 0%, 245 trn 2%, 9679 lrg 98%
c otfs: sub 182, 123 red 68%, 59 irr 32%
c otfs: sub 182, 0 bin 0%, 49 trn 27%, 133 lrg 73%
c phas: 6 computed, 9682 set, 4906 pos (51%), 4776 neg (49%)
c prbs: 4 basic, 48971 probed, 213 failed, 3 lifted
c prbs: 5 simple, 37992 probed, 14 failed, 263 eqs
c prbs: 5 treelook, 620 probed, 11 failed, 0 lifted
c prom: 122074 locked 11% out of 1097804 tried
c prps: 260061704 props, 146 props/dec
c prps: 97% srch, 3% simp, 0% lkhd
c quat: 9 count, 3142 quat, 1088 self1, 149 self2, 3335 dup
c redc: 18693 clauses 12%, 150177 tried 28%, 2 sat 0%
c redc: 26369 lits 1%, 1881195 tried 12%, 2 sat 0%
c redc: 1017 times jump level reduced, 3.8 levels on average
c reds: 11 count, 48572.8 conflicts per reduce
c reds: 0 memlim 0%, 11 arith 100%
c reds: 302516 collected 82%, 67988 retired 18%
c rmbd: 1269 removed, 512 red 40%
c rsts: 20817 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: 13 count, 12 confs 92%, 0 vars 0%
c simp: 0 its 0%, 1 bin 8%, 0 trns 0%
c subl: 541503 count (189974 tried 0.4), 66124 sub out of 538011 (12.3%)
c swps: 9 count, 12 rounds, 5665 queries (472.1/round)
c swps: 5576 sat calls, 235 unsat (1.9% success rate)
c swps: 166504 decisions 29.9, 10651 conflicts 1.9
c swps; 59.3 avg class size, 83.6 avg environment size
c swps: 0 failed, 104 impls, 318 equivs
c swp0: 1884 type 0 queries, 888 unsat (47.1%), 1795 sat (95.3%)
c swp1: 3781 type 1 queries, 2139 unsat (56.6%), 3552 sat (93.9%)
c sync: 0 produced units, 0 successful consumptions 0%
c sync: 0 consume units calls, 0 tried 0%, 0 success 0%
c sync: 0 produced clauses, 0 successful consumptions 0%
c sync: 0 consume clause calls, 0 tried 0%, 0 success 0%
c time: 4530773 calls to obtain time
c tops: 3112 fixed 21%, 15 its, 35620.07 confs/it
c trds: 9 transitive reductions, 14065 removed, 78 failed
c trds: 148956 nodes, 186854 edges, 6806689 steps
c trim: 339615 words, 1.3 MB
c trnr: 8 count, 1170 bin, 30694 trn, 378046667 steps
c unhd: 7 count, 8 rounds, 24686359 steps
c unhd: 448 non-trivial sccs of average size 2.0
c unhd: 54 units, 54 bin, 0 trn, 0 lrg
c unhd: 63 failed, 61 stamp, 0 lits, 0 bin, 2 trn, 0 lrg
c unhd: 25924 tauts, 498 bin 2%, 5218 trn 20%, 7043 lrg 27%
c unhd: 25924 tauts, 13165 stamp 51%, 12979 red 50%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 143444 str, 54 bin 0%, 583 trn 0%, 142807 lrg 100%, 137860 red 96%
c vars: 5742 remaining 39% and 8894 removed 61% out of 14636
c vars: 3112 fixed 21%, 4097 eliminated 28%, 1685 equivalent 12%
c vsts: 9709226646 visits, 97% srch, 3% simp, 0% lkhd
c vsts: 37.3 search visits per propagation, 17545.9 per conflict
c wchs: 3541305534 pushed, 12434228 enlarged, 145 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all         541153        302516         67988      10955553       4065988        340200
c 
c  0 0         56526  10      6382   2         0   0   6121110  56   1785431  44    115964  34     1.4
c  1 5         45892   8     24480   8      6020   9   1637722  15<   661120  16<    58241  17<    0.5
c  2 6        174970  32<   109156  36     19752  29   2291719  21   1109932  27    114513  34     1.9
c  3 9        193337  36    122245  40<    24558  36<   772877   7    432519  11     45006  13     2.0
c  4 14        60625  11     35730  12     13735  20    119059   1     70282   2      6017   2     0.9
c  5 21         8742   2      4128   1      3387   5     11739   0      6144   0       423   0     0.2
c  6 30          977   0       372   0       496   1      1228   0       523   0        30   0     0.1
c  7 41           81   0        23   0        39   0        96   0        37   0         6   0     0.0
c  8 54            3   0         0   0         1   0         3   0         0   0         0   0     0.0
c 
c avg                  2.3           2.6           2.9           0.8           1.1           1.3
c std                  1.2           0.9           1.0           1.1           1.1           1.1
c 
c   41.514  15% elim
c   11.054   4% probe
c    9.010   3% sweep
c    3.587   1% ternres
c    3.199   1% quatres
c    2.032   1% cce
c    2.011   1% unhide
c    1.469   1% decide
c    1.066   0% block
c 
c    3.230 < 1% rest (below)
c 
c    0.957   0% bca
c    0.767   0% transred
c    0.730   0% bump
c    0.408   0% gauss
c    0.297   0% card
c    0.072   0% rescore
c    0.000   0% locs
c    0.000   0% queuesort
c ==================================
c    1.358   0% preprocessing     2%
c   77.321  27% inprocessing     98%
c ==================================
c   78.679  28% simplifying
c  206.534  72% search
c ==================================
c  285.213 100% all
c 
c        534301 conflicts,        1873.3 confs/sec
c          1449 ternaries,         368.7 confs/ternary
c           722 binaries,          740.0 confs/binary
c            15 iterations,      35620.1 confs/iteration
c 
c            11 reductions,          0.0 redus/sec,  48572.8 confs/reduction
c         20817 restarts,           73.0 rests/sec,     25.7 confs/restart
c       1723470 decisions,        6042.7 decis/sec,      3.2 decis/conflict
c     260061704 propagations,   911815.1 props/sec,    150.9 props/decision
c 
c 285.2 seconds, 73.0 MB
c launch: done
