c launch: /data/cnf/sc2014/app/hitag2-8-60-0-0x1eb82244d7f1c3c-47.cnf.bz2
c host: atom23
c Lingeling SAT Solver
c 
c Version b7ztzu 7b29300825af9bcc1c8b2c5ebcf65fa1cb101cad
c 
c Copyright (C) 2010-2014 Armin Biere JKU Linz Austria.
c All rights reserved.
c 
c released Sun Apr 26 19:26:13 CEST 2015
c compiled Sun Apr 26 19:26:13 CEST 2015
c 
c gcc (Ubuntu 4.8.2-19ubuntu1) 4.8.2
c -Wall -O3 -I../yalsat -I../druplig -DNLGLOG -DNDEBUG -DNCHKSOL
c Linux cluster2 3.13.0-45-generic x86_64
c 
c piping '/data/cnf/sc2014/app/hitag2-8-60-0-0x1eb82244d7f1c3c-47.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/hitag2-8-60-0-0x1eb82244d7f1c3c-47.cnf.bz2
c no embedded options
c found 'p cnf 2282 30260' header
c read 2282 variables, 30260 clauses, 177908 literals in 0.00 seconds
c
c --abstime=0
c --bate=1
c --batewait=2
c --bca=1
c --bcaddlimldscale=2
c --bcamaxeff=10000000
c --bcaminuse=100
c --bcawait=2
c --bkwdscale=100
c --bkwdroundlim=7
c --bkwdresched=1
c --blkboost=10
c --blkboostvlim=10000000
c --blkclslim=1000000
c --blklarge=1
c --blkmaxeff=800000000
c --blkmineff=50000000
c --blkocclim1=100000
c --blkocclim=1000000
c --blkocclim2=10000
c --blkreleff=100
c --blkresched=1
c --blkrtc=0
c --blksmall=1
c --blksuccessmaxwortc=6
c --blksuccessrat=100
c --block=1
c --blockwait=1
c --boost=1
c --bumpsimp=1
c --card=1
c --cardcut=2
c --cardexpam1=3
c --cardglue=0
c --cardignused=0
c --cardmaxeff=300000000
c --cardmaxlen=1000
c --cardmineff=2000000
c --cardminlen=3
c --cardocclim1=300
c --cardocclim2=15
c --cardreleff=5
c --cardreschedint=10
c --carduse=2
c --cardwait=0
c --cce2wait=1
c --cce=3
c --cceateint=2
c --cceboost=10
c --cceboostdel=3
c --cceboostint=5
c --cceboostvlim=10000000
c --cce3wait=2
c --ccemaxround=3
c --ccemaxeff=2147483647
c --ccemineff=30000000
c --ccereleff=50
c --ccertc=0
c --ccertcint=15
c --ccertcintvlim=2000000
c --ccesuccessrat=100
c --ccewait=2
c --clim=-1
c --compact=0
c --deco=1
c --decolim=100
c --deco1opt=1
c --decompose=1
c --defragfree=50
c --defragint=10000000
c --delmax=10
c --dlim=-1
c --druplig=0
c --drupligcheck=0
c --drupligtrace=0
c --drupligtraceorig=0
c --elim=1
c --elmaxeff=800000000
c --elmblk=1
c --elmblkwait=1
c --elmboost=20
c --elmboostdel=3
c --elmboostint=5
c --elmboostvlim=4000000
c --elmclslim=1000000
c --elmfull=0
c --elmineff=20000000
c --elmlitslim=200
c --elmocclim1=1000
c --elmocclim=1000000
c --elmocclim2=100
c --elmoccsumforced=0
c --elmreleff=200
c --elmresched=0
c --elmroundlim=3
c --elmrtc=0
c --elmrtcint=10
c --elmrtcintvlim=500000
c --elmsuccessmaxwortc=4
c --elmsuccessrat=100
c --exitonabort=0
c --factmax=100000
c --factor=3
c --gauss=1
c --gaussexptrn=1
c --gaussextrall=1
c --gaussmaxeff=50000000
c --gaussmaxor=20
c --gaussmineff=2000000
c --gaussreleff=2
c --gausswait=2
c --gluekeep=4
c --gluekeepsize=15
c --gluescale=4
c --hbrdom=2
c --import=1
c --incredcint=1
c --incredconfslim=0
c --incsavevisits=0
c --inprocessing=1
c --irrlim=1
c --jwhred=1
c --keepmaxglue=1
c --keepmaxglueint=100
c --lhbr=1
c --lkhd=2
c --locs=0
c --locsbanner=0
c --locsclim=1000000
c --locsboost=2
c --locscint=10000
c --locset=2
c --locsexport=1
c --locsmaxeff=100000
c --locsmineff=1000
c --locsred=0
c --locsreleff=5
c --locsrtc=0
c --locsvared=100
c --locswait=2
c --maxscaledglue=15
c --memlim=-1
c --minimize=2
c --minlocalgluelim=200
c --minlocalsizelim=3000
c --minrecgluelim=100
c --minrecsizelim=1000
c --norestartsatlimlo=85
c --move=2
c --otfs=1
c --penmax=4
c --phase=0
c --phaseluckfactor=200
c --phaselucklim=100
c --phaseluckmaxround=10
c --phasesave=1
c --plain=0
c --plim=-1
c --poison=1
c --prbasic=1
c --prbasicmaxeff=400000000
c --prbasicmineff=1000000
c --prbasicreleff=50
c --prbasicroundlim=8
c --prbasicrtc=0
c --prbrtc=0
c --prbsimple=2
c --prbsimpleboost=10
c --prbsimpleliftdepth=2
c --prbsimplemaxeff=200000000
c --prbsimplemineff=2000000
c --prbsimplereleff=40
c --prbsimplertc=0
c --probe=1
c --promote=1
c --promotegluelim=8
c --pure=1
c --quatres=1
c --quatreswait=2
c --queuesort=1
c --queuesortjwh=0
c --randec=0
c --randecint=1000
c --redcls=1
c --redclsglue=6
c --redclsmaxdec=5
c --redclsmaxdepth=10
c --redclsmaxlrg=10
c --redclsmaxprops=100
c --redclsatlimlo=0
c --redclsatlimhi=100
c --redclsize=30
c --redclstype=4
c --reducefixed=0
c --reduceinc=1000
c --reduceinit=50000
c --reduce=1
c --restart=4
c --restartglcint=10
c --restartglclim=115
c --restartinit=0
c --restartint=5
c --restartpen=1
c --retirenb=1
c --retireint=4
c --retiremin=1
c --reusetrail=0
c --rmincpen=4
c --rstinoutinc=110
c --satlimdelay=10000
c --scincinc=200
c --scincincsatlimhi=100
c --scincincdelta=10
c --scincincincint=100000
c --scincincmin=200
c --scincincmode=1
c --score=0
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 2209 free variables 0%
c [limits] no decision limit
c [limits] no conflict limit
c [limits] no propagation limit
c [limits] simplification not delayed since 'simpdelay' zero
c [set-maximum-score] maximum score limit 1.000000d+500
c [set-minimum-score] minimum score limit 1.000000d-500
c [score-type] STATIC (--score=0)
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    2209    30192         0       0      0     0    0     0    2   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] no at-most-one constraint found
c [card-1] no at-most-two constraint found
c [decomp-1] removed 229 variables
c [simpleprobe-1] all 2048 free variables schedulable
c [simpleprobe-1] boosting simple probing limit by 10
c [simpleprobe-1] limit 20000000 penalty 0 = 0 + 0
c [simpleprobe-1] 378 variables remain 18% (1670 retained 82%)
c [simpleprobe-1] removed 0 variables, found 217 hbrs, 0 units
c [unhide-1] limit 100000 with penalty 0 = 0 + 0
c [unhide-1-1] 0 units, 0 failed, 4934 tauts, 0 hbrs, 7528 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 2048 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 373 variables 18% in round 1 in 2883422 steps
c [elim-1-1] backward subsumption/strengthening limit 2883400
c [elim-1-1-1] backward checking 860 touched variables 42%
c [elim-1-1-1] incomplete backward checking 825 remain 96%
c [elim-1-1] subsumed 163 and strengthened 393 clauses in 2883682 steps
c [elim-1-1] rescheduled 119 variables 6% by backward subsumption
c [elim-1-2] eliminated 28 variables 1% in round 2 in 175769 steps
c [elim-1-2] backward subsumption/strengthening limit 175700
c [elim-1-2-1] backward checking 861 touched variables 42%
c [elim-1-2-1] incomplete backward checking 860 remain 100%
c [elim-1-2] subsumed 9 and strengthened 27 clauses in 176261 steps
c [elim-1-2] rescheduled 26 variables 1% by backward subsumption
c [elim-1-3] eliminated 4 variables 0% in round 3 in 20345 steps
c [elim-1-3] backward subsumption/strengthening limit 20300
c [elim-1-3-1] backward checking 860 touched variables 42%
c [elim-1-3-1] incomplete backward checking 856 remain 100%
c [elim-1-3] subsumed 0 and strengthened 4 clauses in 20885 steps
c [elim-1] incomplete 11 not tried 1% in round 3
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 405 = 20% variables out of 2048 scheduled
c [elim-1] considered successful since not run to completion yet
c [phase-count-1] 20927 negative 98.0% of 21352 except 425 2.0%
c [phase-count-1] 19956 positive 93.5% of 21352 except 1396 6.5%
c [phase-count-1] less non-negative clauses 425 than limit 2100 (10.0%)
c [phase-count-1] non-pos/non-neg = 1396/425 = 3.28 >= 2.00 = 200/100
c [lucky-phase-1] forcing lucky phase -1
c [phase-1] phase bias: 0 positive 0%, 1643 negative 100%
c [sort-queue-1] sorted 1643 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 1643 (100%)
c [score-dist-1] max exp 0, different 1 (100%)
c [score-dist-1] median active exp 0, avg 0.0
c [simplification-1] removed 566 variables 25.6% (1643 remain 74%)
c [simplification-1] removed 8840 irredundant clauses 29.3% (21352 remain 71%)
c [simplification-1] maximum reduction of 29% = max (26%, 29%)
c [simplification-1] large reduction 29% >= 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 1001 conflicts
c [decomp-3] removed 1 variables
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 3284 literals 100%
c [treelook-1] scheduling used 64375 steps
c [treelook-1] scheduled completely
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 303440 steps
c [treelook-1] 3140 literals remain 96%
c [treelook-1] 1642 variables remain to probed next time 100%
c [treelook-1] removed 0 variables, found 42 hbrs
c [basicprobe-1] limit 1000000 penalty 0 = 0 + 0
c [basicprobe-1-0] 1138 sched 70%, 16 failed, 0 lifted, 92 hbrs
c [decomp-5] removed 16 variables
c [basicprobe-1-1] 1107 sched 68%, 1 failed, 0 lifted, 10 hbrs
c [decomp-6] removed 1 variables
c [basicprobe-1-2] 1101 sched 68%, 0 failed, 0 lifted, 3 hbrs
c [basicprobe-1-3] 1099 sched 68%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-1-3] fully completed probing
c [basicprobe-1-3] 17 units = 17 failed (100%) + 0 lifted (0%)
c [basicprobe-1-3] removed 17 variables, found 105 hbrs
c [elim-2] no untried remaining variables left
c [elim-2] scheduled 1625 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 151 variables 9% in round 1 in 4612253 steps
c [elim-2-1] backward subsumption/strengthening limit 4612200
c [elim-2-1-1] backward checking 401 touched variables 25%
c [elim-2-1-1] incomplete backward checking 305 remain 76%
c [elim-2-1] subsumed 24 and strengthened 463 clauses in 4612669 steps
c [elim-2-1] rescheduled 281 variables 17% by backward subsumption
c [elim-2-2] eliminated 1 variables 0% in round 2 in 333187 steps
c [elim-2-2] backward subsumption/strengthening limit 333100
c [elim-2-2-1] backward checking 328 touched variables 20%
c [elim-2-2-1] incomplete backward checking 293 remain 89%
c [elim-2-2] subsumed 1 and strengthened 1 clauses in 333524 steps
c [elim-2-2] rescheduled 4 variables 0% by backward subsumption
c [elim-2-3] no variable eliminated in round 3 in 1563 steps
c [elim-2] fully completed in 3 rounds
c [elim-2] transition to [ all 0 rem 0 ] state
c [elim-2] eliminated 152 = 9% variables out of 1625 scheduled
c [sort-queue-2] sorted 1473 enqueued variables after 1001 conflicts
c [score-dist-2] active 0 (0%), one 0 (0%), zero 1473 (100%)
c [score-dist-2] max exp 0, different 1 (100%)
c [score-dist-2] median active exp 0, avg 0.0
c [simplification-2] removed 170 variables 10.3% (1473 remain 67%)
c [simplification-2] removed 2183 irredundant clauses 10.2% (19169 remain 63%)
c [simplification-2] maximum reduction of 10% = max (10%, 10%)
c [simplification-2] large reduction 10% >= 5% limit
c [simplification-2] next conflict interval 2000 = 2000/1
c [simplification-2] penalized conflict interval 2000 = 1 * 2000
c [simplification-2] hard conflict limit 13001 (soft 3001 + delta 10000)
c [simplification-2] new conflict limit 3001 (hard 13001)
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.0    1472    19167      1062     657     77   213    2    18    2  10%      6   18    8    0 6474%
c 
c [simplification-3] limit 3001 conflicts (hard 13001) hit after 3001 conflicts
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 4 at-most-one constraints of average size 3.0
c [card-2] no at-most-two constraint found
c [card-2] using previous limit 1000000 for elimination
c [card-2] 4 out of 4 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] generated 6 at-most-one constraints, 5 used 83%
c [card-2] exported 5 binary clauses, 1.0 per/constraint
c [decomp-8] removed 1 variables
c [simpleprobe-2] 234 schedulable variables 16%
c [simpleprobe-2] limit 1000000 penalty 1 = 1 + 0
c [decomp-9] removed 1 variables
c [simpleprobe-2] 95 variables remain 6% (1376 retained 94%)
c [simpleprobe-2] removed 1 variables, found 28 hbrs, 1 units
c [unhide-2] limit 50000 with penalty 1 = 1 + 0
c [unhide-2-2] 0 units, 0 failed, 8 tauts, 0 hbrs, 2628 literals
c [block-1] scheduling all variables this time
c [block-1] scheduled 1471 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 8 blocked clauses
c [block-1] 8 < 1/100 * 19133 = 191 considered unsuccessful
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 138 clauses out of 8632 (2%) of length 7
c [cce-1-1] eliminated 539 clauses out of 1295 (42%) of length 6
c [cce-1-1] eliminated 1670 clauses out of 2997 (56%) of length 5
c [cce-1-1] eliminated 927 clauses out of 2722 (34%) of length 4
c [cce-1-1] completed large round (ATE)
c [cce-1-1] eliminated 3274 large clauses in 28877433 steps
c [cce-1-1] allowing another 14438716 steps for small clauses
c [cce-1-1] scheduling 3105 clauses = 2427 binary + 678 ternary
c [cce-1-1] tried to eliminate 3105 small clauses 100%
c [cce-1-1] eliminated 61 binary clauses 3%
c [cce-1-1] eliminated 84 ternary clauses 12%
c [cce-1-1] eliminated 145 small clauses 5%
c [cce-1-1] eliminated 145 small clauses in 16582957 steps
c [cce-1-1] completed small round (ATE)
c [cce-1-1] completed small and large (ATE)
c [cce-1-1] eliminated 3419 covered clauses in round 1
c [cce-1-2] incomplete large round (ABCE)
c [cce-1-2] allowing another 6708533 steps for small clauses
c [cce-1-2] scheduling 2960 clauses = 2366 binary + 594 ternary
c [cce-1-2] tried to eliminate 2960 small clauses 100%
c [cce-1-2] eliminated 179 binary clauses 8%
c [cce-1-2] eliminated 5 ternary clauses 1%
c [cce-1-2] eliminated 184 small clauses 6%
c [cce-1-2] eliminated 184 small clauses in 8731837 steps
c [cce-1-2] completed small round (ABCE)
c [cce-1-2] eliminated 184 covered clauses in round 2
c [cce-1-3] incomplete large round (ABCE)
c [cce-1-3] allowing another 2342625 steps for small clauses
c [cce-1-3] scheduling 2776 clauses = 2187 binary + 589 ternary
c [cce-1-3] tried to eliminate 2776 small clauses 100%
c [cce-1-3] completed small round (ABCE)
c [cce-1-3] eliminated 0 covered clauses in round 3
c [cce-1] eliminated 3603 covered clauses in TOTAL during 3 rounds
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 1471 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 506 variables 34% in round 1 in 8866634 steps
c [elim-3-1] backward subsumption/strengthening limit 8866600
c [elim-3-1-1] backward checking 817 touched variables 56%
c [elim-3-1-1] fully completed backward checking in 1 rounds
c [elim-3-1] subsumed 20 and strengthened 186 clauses in 2381087 steps
c [elim-3-1] rescheduled 236 variables 16% by backward subsumption
c [elim-3-2] eliminated 25 variables 2% in round 2 in 3745629 steps
c [elim-3-2] backward subsumption/strengthening limit 3745600
c [elim-3-2-1] backward checking 80 touched variables 5%
c [elim-3-2-1] fully completed backward checking in 1 rounds
c [elim-3-2] subsumed 3 and strengthened 21 clauses in 268002 steps
c [elim-3-2] rescheduled 30 variables 2% by backward subsumption
c [elim-3-3] eliminated 7 variables 0% in round 3 in 262469 steps
c [elim-3-3] backward subsumption/strengthening limit 262400
c [elim-3-3-1] backward checking 25 touched variables 2%
c [elim-3-3-1] fully completed backward checking in 1 rounds
c [elim-3-3] subsumed 0 and strengthened 0 clauses in 141464 steps
c [elim-3] fully completed in 3 rounds
c [elim-3] transition to [ all 0 rem 0 ] state
c [elim-3] eliminated 538 = 37% variables out of 1471 scheduled
c [bca-1] limit of 10000000 steps and 27982 added (scaled 2)
c [bca-1] 688 out of 1868 literals actually usable 37%
c [bca-1] added 0 blocked clauses in 3312 steps
c [sweep-1] limit 1000000 penalty 0 = 0 + 0
c [sweep-1-1] 320 pos 34.3% + 613 neg 65.7% = 933 sched 100.0% ret 0
c [sweep-1-1] 527242 steps 73 queries 49.21 avg class size
c [sweep-1-1] 1399 decisions 72 SAT calls 28.49 avg env size
c [sweep-1-1] fully completed sweeping round
c [sweep-1-1] removed 0 vars (0 failed, 0 eqs, 1 impls)
c [sweep-1-2] 320 pos 34.3% + 613 neg 65.7% = 933 sched 100.0% ret 0
c [sweep-1-2] 491844 steps 25 queries 119.92 avg class size
c [sweep-1-2] 734 decisions 24 SAT calls 33.54 avg env size
c [sweep-1-2] 493 variables remain 53% (440 retained 47%)
c [sweep-1-2] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-1] removed 0 vars in TOTAL (2 rounds, 96 queries)
c [sort-queue-3] sorted 933 enqueued variables after 3001 conflicts
c [score-dist-3] active 0 (0%), one 0 (0%), zero 933 (100%)
c [score-dist-3] max exp 0, different 1 (100%)
c [score-dist-3] median active exp 0, avg 0.0
c [simplification-3] removed 539 variables 36.6% (933 remain 42%)
c [simplification-3] removed 5421 irredundant clauses 28.3% (13739 remain 46%)
c [simplification-3] maximum reduction of 37% = max (37%, 28%)
c [simplification-3] large reduction 37% >= 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 15001 (soft 5001 + delta 10000)
c [simplification-3] new conflict limit 5001 (hard 15001)
c 
c [simplification-4] limit 5001 conflicts (hard 15001) hit after 5001 conflicts
c [quatres-1] found 2351 quaternary clauses 18% in total
c [quatres-1-1] removed 14 duplicate quaternary clauses
c [quatres-1-1] added 3 double-self-subsuming ternary resolvents
c [quatres-1-2] added 23 single-self-subsuming ternary resolvents
c [quatres-1-2] added 188 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 933 free variables schedulable
c [ternres-1] 136 ternary resolvents (0 bin, 136 trn)
c [ternres-1] fully completed ternary resolution
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 837 xors of average arity 6.1
c [gauss-1] connected 5067 occurrences of 70 variables (average 72.4)
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 [transred-1] limit 101773 with penalty 0 = 0 + 0
c [transred-1] removed 12 transitive binary clauses
c [cce-2] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-2-1] eliminated 1 clauses out of 8461 (0%) of length 7
c [cce-2-1] eliminated 12 clauses out of 1085 (1%) of length 5
c [cce-2-1] eliminated 25 clauses out of 1732 (1%) of length 4
c [cce-2-1] completed large round (ATE)
c [cce-2-1] eliminated 38 large clauses in 24989013 steps
c [cce-2-1] allowing another 12494506 steps for small clauses
c [cce-2-1] scheduling 1335 clauses = 995 binary + 340 ternary
c [cce-2-1] tried to eliminate 1335 small clauses 100%
c [cce-2-1] eliminated 1 binary clauses 0%
c [cce-2-1] eliminated 10 ternary clauses 3%
c [cce-2-1] eliminated 11 small clauses 1%
c [cce-2-1] eliminated 11 small clauses in 13642226 steps
c [cce-2-1] completed small round (ATE)
c [cce-2-1] eliminated 49 covered clauses in round 1
c [cce-2-2] incomplete large round (ATE)
c [cce-2-2] allowing another 8178897 steps for small clauses
c [cce-2-2] scheduling 1324 clauses = 994 binary + 330 ternary
c [cce-2-2] tried to eliminate 1324 small clauses 100%
c [cce-2-2] completed small round (ATE)
c [cce-2-2] eliminated 0 covered clauses in round 2
c [cce-2] eliminated 49 covered clauses in TOTAL during 2 rounds
c [cce-2] 49 < 1/100 * 13732 = 137 considered unsuccessful
c [elim-4] scheduling all variables this time
c [elim-4] scheduled 933 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 14 variables 2% in round 1 in 31080771 steps
c [elim-4-1] backward subsumption/strengthening limit 31080700
c [elim-4-1-1] backward checking 135 touched variables 14%
c [elim-4-1-1] fully completed backward checking in 1 rounds
c [elim-4-1] subsumed 1 and strengthened 6 clauses in 825967 steps
c [elim-4-1] rescheduled 11 variables 1% by backward subsumption
c [elim-4-2] eliminated 3 variables 0% in round 2 in 1705279 steps
c [elim-4-2] backward subsumption/strengthening limit 1705200
c [elim-4-2-1] backward checking 7 touched variables 1%
c [elim-4-2-1] fully completed backward checking in 1 rounds
c [elim-4-2] subsumed 0 and strengthened 0 clauses in 82757 steps
c [elim-4] fully completed in 2 rounds
c [elim-4] transition to [ all 0 rem 0 ] state
c [elim-4] eliminated 17 = 2% variables out of 933 scheduled
c [sort-queue-4] sorted 916 enqueued variables after 5001 conflicts
c [score-dist-4] active 0 (0%), one 0 (0%), zero 916 (100%)
c [score-dist-4] max exp 0, different 1 (100%)
c [score-dist-4] median active exp 0, avg 0.0
c [simplification-4] removed 17 variables 1.8% (916 remain 41%)
c [simplification-4] removed 119 irredundant clauses 0.9% (13615 remain 45%)
c [simplification-4] maximum reduction of 2% = max (2%, 1%)
c [simplification-4] geometric conflict interval increment 6666 = 20000 / 3
c [simplification-4] new conflict interval 6666
c [simplification-4] penalized conflict interval 6666 = 1 * 6666
c [simplification-4] hard conflict limit 21667 (soft 11667 + delta 10000)
c [simplification-4] new conflict limit 11667 (hard 21667)
c 
c [simplification-5] limit 11667 conflicts (hard 21667) hit after 11668 conflicts
c [quatres-2] found 2938 quaternary clauses 21% in total
c [quatres-2-1] added 1 double-self-subsuming ternary resolvents
c [quatres-2-2] added 23 single-self-subsuming ternary resolvents
c [quatres-2-2] added 171 quaternary resolvents
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] all 916 free variables schedulable
c [ternres-2] 61 ternary resolvents (0 bin, 61 trn)
c [ternres-2] fully completed ternary resolution
c [treelook-2] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-2] scheduled 1832 literals 100%
c [treelook-2] scheduling used 76661 steps
c [treelook-2] scheduled completely
c [treelook-2] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-2] used 151084 steps
c [treelook-2] 1712 literals remain 94%
c [treelook-2] 912 variables remain to probed next time 100%
c [treelook-2] removed 1 variables, found 25 hbrs
c [transred-2] limit 284264 with penalty 0 = 0 + 0
c [transred-2] removed 5 transitive binary clauses
c [block-2] scheduling all variables this time
c [block-2] scheduled 915 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 0 blocked clauses
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 915 variables 100%
c [elim-5] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5] incomplete 26 not tried 3% in round 1
c [elim-5] transition to [ all 1 rem 1 ] state
c [elim-5] eliminated 0 = 0% variables out of 915 scheduled
c [bca-2] limit of 10000000 steps and 27706 added (scaled 2)
c [bca-2] 132 out of 1832 literals actually usable 7%
c [bca-2] added 0 blocked clauses in 10092 steps
c [sweep-2] limit 500000 penalty 1 = 1 + 0
c [sweep-2-1] 186 pos 38.2% + 301 neg 61.8% = 487 sched 53.2% ret 428
c [sweep-2-1] 522147 steps 7 queries 109.14 avg class size
c [sweep-2-1] 504 decisions 6 SAT calls 193.33 avg env size
c [sweep-2-1] 455 variables remain 50% (459 retained 50%)
c [decomp-15] removed 1 variables
c [sweep-2-1] removed 1 vars (0 failed, 0 eqs, 0 impls)
c [sweep-2] removed 1 vars in TOTAL (1 rounds, 6 queries)
c [sort-queue-5] sorted 914 enqueued variables after 11668 conflicts
c [score-dist-5] active 0 (0%), one 0 (0%), zero 914 (100%)
c [score-dist-5] max exp 0, different 1 (100%)
c [score-dist-5] median active exp 0, avg 0.0
c [simplification-5] removed 2 variables 0.2% (914 remain 41%)
c [simplification-5] removed 16 irredundant clauses 0.1% (13598 remain 45%)
c [simplification-5] maximum reduction of 0% = max (0%, 0%)
c [simplification-5] full geometric conflict interval increment 20000
c [simplification-5] new conflict interval 26666
c [simplification-5] penalized conflict interval 26666 = 1 * 26666
c [simplification-5] hard conflict limit 51667 (soft 38334 + delta 13333)
c [simplification-5] new conflict limit 38334 (hard 51667)
c 
c [simplification-6] limit 38334 conflicts (hard 51667) hit after 38334 conflicts
c [quatres-3] found 3941 quaternary clauses 23% in total
c [quatres-3-2] added 15 single-self-subsuming ternary resolvents
c [quatres-3-2] added 200 quaternary resolvents
c [ternres-3] limit 4000000 with penalty 0 = 0 + 0
c [ternres-3] all 914 free variables schedulable
c [ternres-3] 57 ternary resolvents (2 bin, 55 trn)
c [ternres-3] fully completed ternary resolution
c [card-3] limit 500000 penalty 2 = 2 + 0
c [card-3] found 1 at-most-one constraints of average size 3.0
c [card-3] found 5 at-most-two constraints of average size 4.0
c [card-3] using previous limit 500000 for elimination
c [card-3] 6 out of 6 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] extracted 558 xors of average arity 5.7
c [gauss-2] connected 3170 occurrences of 62 variables (average 51.1)
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] fully completed
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [basicprobe-2] limit 8491077 penalty 0 = 0 + 0
c [basicprobe-2-0] 481 sched 53%, 6 failed, 0 lifted, 137 hbrs
c [decomp-17] removed 6 variables
c [basicprobe-2-1] 504 sched 56%, 0 failed, 0 lifted, 5 hbrs
c [basicprobe-2-2] 502 sched 55%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-2-2] fully completed probing
c [basicprobe-2-2] 6 units = 6 failed (100%) + 0 lifted (0%)
c [basicprobe-2-2] removed 6 variables, found 142 hbrs
c [unhide-3] limit 84910 with penalty 2 = 2 + 0
c [unhide-3-3] 0 units, 0 failed, 15 tauts, 0 hbrs, 7152 literals
c [transred-3] limit 1698215 with penalty 0 = 0 + 0
c [transred-3] removed 17 transitive binary clauses
c [cce-3] limit of 15000000 steps penalty 1 = 1 + 0
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] allowing another 7500088 steps for small clauses
c [cce-3-1] scheduling 1297 clauses = 933 binary + 364 ternary
c [cce-3-1] tried to eliminate 1297 small clauses 100%
c [cce-3-1] eliminated 61 binary clauses 7%
c [cce-3-1] eliminated 61 small clauses 5%
c [cce-3-1] eliminated 61 small clauses in 8719380 steps
c [cce-3-1] completed small round (ACCE)
c [cce-3-1] eliminated 61 covered clauses in round 1
c [cce-3-2] incomplete large round (ACCE)
c [cce-3-2] allowing another 3140422 steps for small clauses
c [cce-3-2] scheduling 1236 clauses = 872 binary + 364 ternary
c [cce-3-2] tried to eliminate 1236 small clauses 100%
c [cce-3-2] completed small round (ACCE)
c [cce-3-2] eliminated 0 covered clauses in round 2
c [cce-3] eliminated 61 covered clauses in TOTAL during 2 rounds
c [cce-3] 61 < 1/100 * 13562 = 135 considered unsuccessful
c [sweep-3] limit 1000000 penalty 0 = 0 + 0
c [sweep-3-1] 176 pos 38.9% + 277 neg 61.1% = 453 sched 49.9% ret 455
c [sweep-3-1] 1050643 steps 4 queries 143.25 avg class size
c [sweep-3-1] 300 decisions 3 SAT calls 148.33 avg env size
c [sweep-3-1] 449 variables remain 49% (459 retained 51%)
c [sweep-3-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-3] removed 0 vars in TOTAL (1 rounds, 3 queries)
c [sort-queue-6] sorted 908 enqueued variables after 38334 conflicts
c [score-dist-6] active 0 (0%), one 0 (0%), zero 908 (100%)
c [score-dist-6] max exp 0, different 1 (100%)
c [score-dist-6] median active exp 0, avg 0.0
c [simplification-6] removed 6 variables 0.7% (908 remain 41%)
c [simplification-6] removed 96 irredundant clauses 0.7% (13501 remain 45%)
c [simplification-6] maximum reduction of 1% = max (1%, 1%)
c [simplification-6] geometric conflict interval increment 13333 = 26666 / 2
c [simplification-6] new conflict interval 39999
c [simplification-6] penalized conflict interval 39999 = 1 * 39999
c [simplification-6] hard conflict limit 98332 (soft 78333 + delta 19999)
c [simplification-6] new conflict limit 78333 (hard 98332)
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 -   18.9     908    13501     60157   13670    938   393   13    55    8  23%    602   22   13    7  179%
c 
c [simplification-7] limit 78333 conflicts (hard 98332) hit after 78333 conflicts
c [quatres-4] found 4892 quaternary clauses 23% in total
c [quatres-4-1] removed 2 duplicate quaternary clauses
c [quatres-4-1] added 1 double-self-subsuming ternary resolvents
c [quatres-4-2] added 24 single-self-subsuming ternary resolvents
c [quatres-4-2] added 217 quaternary resolvents
c [ternres-4] limit 4596407 with penalty 0 = 0 + 0
c [ternres-4] all 908 free variables schedulable
c [ternres-4] 46 ternary resolvents (0 bin, 46 trn)
c [ternres-4] fully completed ternary resolution
c [simpleprobe-3] 49 schedulable variables 5%
c [simpleprobe-3] limit 18385631 penalty 0 = 0 + 0
c [simpleprobe-3] fully completed simple probing
c [simpleprobe-3] removed 0 variables, found 13 hbrs, 0 units
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 15 transitive binary clauses
c [elim-6] 26 variables 3% will be scheduled this time
c [elim-6] scheduled 26 variables 3%
c [elim-6] limit of 45964077 steps penalty 1 = 1 + 0
c [elim-6] rescheduling of touched variables disabled
c [elim-6-1] no variable eliminated in round 1 in 22803183 steps
c [elim-6] fully completed in 1 rounds
c [elim-6] transition to [ all 0 rem 0 ] state
c [elim-6] eliminated 0 = 0% variables out of 26 scheduled
c [sort-queue-7] sorted 908 enqueued variables after 78333 conflicts
c [score-dist-7] active 0 (0%), one 0 (0%), zero 908 (100%)
c [score-dist-7] max exp 0, different 1 (100%)
c [score-dist-7] median active exp 0, avg 0.0
c [simplification-7] removed 0 variables 0.0% (908 remain 41%)
c [simplification-7] removed 5 irredundant clauses 0.0% (13496 remain 45%)
c [simplification-7] maximum reduction of 0% = max (0%, 0%)
c [simplification-7] full geometric conflict interval increment 39999
c [simplification-7] new conflict interval 79998
c [simplification-7] penalized conflict interval 79998 = 1 * 79998
c [simplification-7] hard conflict limit 198330 (soft 158331 + delta 39999)
c [simplification-7] new conflict limit 158331 (hard 198330)
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 -   35.3     908    13496    109696   20145   1111   394   13    54    8  24%    826   10   13   10  133%
c -   49.8     908    13496    157168   26645   1186   397   13    43    9  30%    928   -5   12   12  105%
c 
c [simplification-8] limit 158331 conflicts (hard 198330) hit after 191368 conflicts
c [quatres-5] found 6041 quaternary clauses 21% in total
c [quatres-5-2] added 16 single-self-subsuming ternary resolvents
c [quatres-5-2] added 200 quaternary resolvents
c [ternres-5] limit 13760544 with penalty 0 = 0 + 0
c [ternres-5] all 908 free variables schedulable
c [ternres-5] 51 ternary resolvents (0 bin, 51 trn)
c [ternres-5] fully completed ternary resolution
c [treelook-3] limit 1376054 penalty 0 = 0 + 0 boost 1
c [treelook-3] scheduled 1814 literals 100%
c [treelook-3] scheduling used 227203 steps
c [treelook-3] scheduled completely
c [treelook-3] limit 1376054 penalty 0 = 0 + 0 boost 1
c [treelook-3] used 1189158 steps
c [treelook-3] fully completed tree based probing
c [treelook-3] removed 0 variables, found 53 hbrs
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 6 transitive binary clauses
c [block-3] scheduling all variables this time
c [block-3] scheduled 908 variables 100%
c [block-3] limit of 34401360 steps penalty 2 = 2 + 0
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 1 blocked clauses
c [block-3] 1 < 1/100 * 13496 = 134 considered unsuccessful
c [bca-3] limit of 10000000 steps and 27490 added (scaled 2)
c [bca-3] 45 out of 1818 literals actually usable 2%
c [bca-3] not enough literals usable
c [bca-3] added 0 blocked clauses in 60436 steps
c [sweep-4] limit 2064081 penalty 1 = 1 + 0
c [sweep-4-1] 159 pos 35.4% + 290 neg 64.6% = 449 sched 49.4% ret 459
c [sweep-4-1] 2834470 steps 5 queries 97.20 avg class size
c [sweep-4-1] 400 decisions 4 SAT calls 296.50 avg env size
c [sweep-4-1] 431 variables remain 47% (477 retained 53%)
c [sweep-4-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-4] removed 0 vars in TOTAL (1 rounds, 4 queries)
c [sort-queue-8] sorted 908 enqueued variables after 191368 conflicts
c [score-dist-8] active 0 (0%), one 0 (0%), zero 908 (100%)
c [score-dist-8] max exp 0, different 1 (100%)
c [score-dist-8] median active exp 0, avg 0.0
c [simplification-8] removed 0 variables 0.0% (908 remain 41%)
c [simplification-8] removed 1 irredundant clauses 0.0% (13495 remain 45%)
c [simplification-8] maximum reduction of 0% = max (0%, 0%)
c [simplification-8] full geometric conflict interval increment 79998
c [simplification-8] new conflict interval 159996
c [simplification-8] penalized conflict interval 159996 = 1 * 159996
c [simplification-8] hard conflict limit 431362 (soft 351364 + delta 79998)
c [simplification-8] new conflict limit 351364 (hard 431362)
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 -   60.2     908    13495    202581   36819   1316   445   13    37   10  34%    976   -6   12   12  103%
c -   69.3     908    13495    242271   41652   1365   445   13    42    7  32%    998    1   14   12  110%
c -   77.4     908    13495    279864   44149   1404   445   13    33   11  39%   1009   -6   12   13   94%
c -   86.8     908    13495    318706   46615   1442   445   13    36    7  37%   1016   -2   14   13  106%
c 
c [simplification-9] limit 351364 conflicts (hard 431362) hit after 356867 conflicts
c [quatres-6] found 7158 quaternary clauses 18% in total
c [quatres-6-2] added 16 single-self-subsuming ternary resolvents
c [quatres-6-2] added 167 quaternary resolvents
c [ternres-6] limit 29070436 with penalty 0 = 0 + 0
c [ternres-6] all 908 free variables schedulable
c [ternres-6] 60 ternary resolvents (0 bin, 60 trn)
c [ternres-6] fully completed ternary resolution
c [gauss-3] limit 1453521 penalty 2 = 2 + 0
c [gauss-3] extracted 802 xors of average arity 6.0
c [gauss-3] connected 4774 occurrences of 71 variables (average 67.2)
c [gauss-3] limit 1453521 penalty 2 = 2 + 0
c [gauss-3] fully completed
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [basicprobe-3] limit 145352183 penalty 0 = 0 + 0
c [basicprobe-3-0] 521 sched 57%, 0 failed, 0 lifted, 1 hbrs
c [basicprobe-3-1] 522 sched 57%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-3-1] fully completed probing
c [basicprobe-3-1] removed 0 variables, found 1 hbrs
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 1 transitive binary clauses
c [cce-4] boosting limit by 10
c [cce-4] limit of 363380457 steps penalty 2 = 2 + 0
c [cce-4-1] eliminated 3 clauses out of 828 (0%) of length 5
c [cce-4-1] eliminated 20 clauses out of 1864 (1%) of length 4
c [cce-4-1] completed large round (ATE)
c [cce-4-1] eliminated 23 large clauses in 24308776 steps
c [cce-4-1] allowing another 12154388 steps for small clauses
c [cce-4-1] scheduling 1254 clauses = 872 binary + 382 ternary
c [cce-4-1] tried to eliminate 1254 small clauses 100%
c [cce-4-1] completed small round (ATE)
c [cce-4-1] eliminated 23 covered clauses in round 1
c [cce-4-2] completed large round (ATE)
c [cce-4-2] allowing another 12137272 steps for small clauses
c [cce-4-2] scheduling 1254 clauses = 872 binary + 382 ternary
c [cce-4-2] tried to eliminate 1254 small clauses 100%
c [cce-4-2] completed small round (ATE)
c [cce-4-2] eliminated 0 covered clauses in round 2
c [cce-4] eliminated 23 covered clauses in TOTAL during 2 rounds
c [cce-4] 23 < 1/100 * 13495 = 134 considered unsuccessful
c [sort-queue-9] sorted 908 enqueued variables after 356867 conflicts
c [score-dist-9] active 0 (0%), one 0 (0%), zero 908 (100%)
c [score-dist-9] max exp 0, different 1 (100%)
c [score-dist-9] median active exp 0, avg 0.0
c [simplification-9] removed 0 variables 0.0% (908 remain 41%)
c [simplification-9] removed 23 irredundant clauses 0.2% (13472 remain 45%)
c [simplification-9] maximum reduction of 0% = max (0%, 0%)
c [simplification-9] full geometric conflict interval increment 159996
c [simplification-9] new conflict interval 319992
c [simplification-9] penalized conflict interval 319992 = 1 * 319992
c [simplification-9] hard conflict limit 836855 (soft 676859 + delta 159996)
c [simplification-9] new conflict limit 676859 (hard 836855)
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 -   97.2     908    13472    358210   49588   1552   445   14    42    7  33%   1020    4   15   13  110%
c -  107.7     908    13472    398258   51956   1603   445   14    42   12  35%   1022    4   14   14  106%
c -  118.7     908    13472    439441   54763   1662   445   14    33   12  42%   1023   -4   15   14  107%
c -  130.0     908    13472    480776   57525   1710   445   15    39    8  37%   1023    2   16   14  111%
c -  141.4     908    13472    521898   60006   1748   445   15    38    8  39%   1024   -2   16   14  110%
c -  152.9     908    13472    563312   62468   1782   445   15    45    8  34%   1024    4   17   15  114%
c -  165.1     908    13472    605534   64316   1807   446   15    44   14  35%   1024   -1   16   15  111%
c -  177.4     908    13472    648876   66915   1841   448   15    35    9  43%   1024   -8   13   15   89%
c 
c [simplification-10] limit 676859 conflicts (hard 836855) hit after 687235 conflicts
c [quatres-7] found 8560 quaternary clauses 15% in total
c [quatres-7-1] added 1 double-self-subsuming ternary resolvents
c [quatres-7-2] added 29 single-self-subsuming ternary resolvents
c [quatres-7-2] added 128 quaternary resolvents
c [ternres-7] limit 66579461 with penalty 0 = 0 + 0
c [ternres-7] all 908 free variables schedulable
c [ternres-7] 122 ternary resolvents (3 bin, 119 trn)
c [ternres-7] fully completed ternary resolution
c [card-4] limit 4161216 penalty 3 = 3 + 0
c [card-4] found 9 at-most-one constraints of average size 3.0
c [card-4] found 14 at-most-two constraints of average size 4.0
c [card-4] using previous limit 4161216 for elimination
c [card-4] 23 out of 23 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [unhide-4] limit 1664486 with penalty 3 = 3 + 0
c [unhide-4-5] 0 units, 0 failed, 49 tauts, 0 hbrs, 36595 literals
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 14 transitive binary clauses
c [elim-7] scheduling all variables this time
c [elim-7] scheduled 908 variables 100%
c [elim-7] limit of 200000000 steps penalty 2 = 2 + 0
c [elim-7] rescheduling of touched variables disabled
c [elim-7-1] eliminated 312 variables 34% in round 1 in 43854642 steps
c [elim-7-1] backward subsumption/strengthening limit 43854600
c [elim-7-1-1] backward checking 509 touched variables 56%
c [elim-7-1-1] fully completed backward checking in 1 rounds
c [elim-7-1] subsumed 6 and strengthened 19 clauses in 652604 steps
c [elim-7-1] rescheduled 73 variables 8% by backward subsumption
c [elim-7-2] eliminated 5 variables 1% in round 2 in 19050041 steps
c [elim-7-2] backward subsumption/strengthening limit 19050000
c [elim-7-2-1] backward checking 13 touched variables 1%
c [elim-7-2-1] fully completed backward checking in 1 rounds
c [elim-7-2] subsumed 0 and strengthened 0 clauses in 72712 steps
c [elim-7] fully completed in 2 rounds
c [elim-7] transition to [ all 0 rem 0 ] state
c [elim-7] eliminated 317 = 35% variables out of 908 scheduled
c [sort-queue-10] sorted 591 enqueued variables after 687235 conflicts
c [score-dist-10] active 0 (0%), one 0 (0%), zero 591 (100%)
c [score-dist-10] max exp 0, different 1 (100%)
c [score-dist-10] median active exp 0, avg 0.0
c [simplification-10] removed 317 variables 34.9% (591 remain 27%)
c [simplification-10] removed 915 irredundant clauses 6.8% (12557 remain 42%)
c [simplification-10] maximum reduction of 35% = max (35%, 7%)
c [simplification-10] large reduction 35% >= 5% limit
c [simplification-10] next conflict interval 6872 = min (687235/100, 319992)
c [simplification-10] penalized conflict interval 6872 = 1 * 6872
c [simplification-10] hard conflict limit 704107 (soft 694107 + delta 10000)
c [simplification-10] new conflict limit 694107 (hard 704107)
c 
c [simplification-11] limit 694107 conflicts (hard 704107) hit after 704107 conflicts
c [quatres-8] found 6870 quaternary clauses 17% in total
c [quatres-8-1] removed 87 duplicate quaternary clauses
c [quatres-8-1] added 1 double-self-subsuming ternary resolvents
c [quatres-8-2] added 16 single-self-subsuming ternary resolvents
c [quatres-8-2] added 246 quaternary resolvents
c [ternres-8] limit 67894171 with penalty 0 = 0 + 0
c [ternres-8] all 591 free variables schedulable
c [ternres-8] 30 ternary resolvents (2 bin, 28 trn)
c [ternres-8] fully completed ternary resolution
c [simpleprobe-4] all 591 free variables schedulable
c [simpleprobe-4] limit 100000000 penalty 1 = 1 + 0
c [simpleprobe-4] fully completed simple probing
c [simpleprobe-4] removed 0 variables, found 17 hbrs, 0 units
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 15 transitive binary clauses
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 50920627 penalty 2 = 2 + 0
c [sweep-5-1] 148 pos 48.5% + 157 neg 51.5% = 305 sched 51.6% ret 286
c [sweep-5-1] 19489251 steps 43 queries 14.72 avg class size
c [sweep-5-1] 3777 decisions 42 SAT calls 245.74 avg env size
c [sweep-5-1] fully completed sweeping round
c [sweep-5-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-5-2] 277 pos 46.9% + 314 neg 53.1% = 591 sched 100.0% ret 0
c [sweep-5-2] 24870435 steps 47 queries 29.02 avg class size
c [sweep-5-2] 4377 decisions 46 SAT calls 243.02 avg env size
c [sweep-5-2] fully completed sweeping round
c [sweep-5-2] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-5-3] 277 pos 46.9% + 314 neg 53.1% = 591 sched 100.0% ret 0
c [sweep-5-3] 7023744 steps 10 queries 91.90 avg class size
c [sweep-5-3] 900 decisions 9 SAT calls 324.56 avg env size
c [sweep-5-3] 364 variables remain 62% (227 retained 38%)
c [sweep-5-3] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-5] removed 0 vars in TOTAL (3 rounds, 97 queries)
c [sort-queue-11] sorted 591 enqueued variables after 704107 conflicts
c [score-dist-11] active 0 (0%), one 0 (0%), zero 591 (100%)
c [score-dist-11] max exp 0, different 1 (100%)
c [score-dist-11] median active exp 0, avg 0.0
c [simplification-11] removed 0 variables 0.0% (591 remain 27%)
c [simplification-11] removed 0 irredundant clauses 0.0% (12557 remain 42%)
c [simplification-11] maximum reduction of 0% = max (0%, 0%)
c [simplification-11] full geometric conflict interval increment 319992
c [simplification-11] new conflict interval 639984
c [simplification-11] penalized conflict interval 639984 = 1 * 639984
c [simplification-11] hard conflict limit 1664083 (soft 1344091 + delta 319992)
c [simplification-11] new conflict limit 1344091 (hard 1664083)
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 -  201.4     591    12557    730882   53815   1164    55   13    32    8  42%   1024   -6   13   15   89%
c -  212.8     591    12557    776950   57814   1184    55   14    35    8  41%   1024   -2   15   15  104%
c -  225.0     591    12557    822499   60609   1205    55   15    36    8  41%   1024   -1   13   15   89%
c -  236.8     591    12557    868251   62478   1225    55   15    35    9  43%   1024   -1   15   15  100%
c -  249.2     591    12557    915559   65697   1241    55   15    38    9  39%   1024    3   16   14  107%
c -  262.4     591    12557    962652   68488   1255    55   13    35    9  39%   1024   -1   16   14  115%
c -  276.1     591    12557   1010446   70572   1272    55   15    35    9  43%   1024    0   16   14  112%
c -  290.9     591    12557   1059352   73226   1282    55   15    38    9  40%   1024    1   15   15  101%
c -  306.0     591    12557   1108822   76378   1294    56   15    37   10  40%   1024    0   14   15   93%
c -  321.5     591    12557   1158764   79512   1309    56   14    36   10  38%   1024    0   13   14   89%
c -  336.8     591    12557   1208456   81781   1318    56   15    36   10  42%   1024    1   14   15   97%
c -  354.0     591    12557   1258806   83743   1332    56   15    43   10  35%   1024    8   14   15   93%
c -  371.3     591    12557   1310875   86486   1338    56   15    33   11  44%   1024   -0   16   14  112%
c 
c [simplification-12] limit 1344091 conflicts (hard 1664083) hit after 1346861 conflicts
c [quatres-9] found 8553 quaternary clauses 12% in total
c [quatres-9-1] removed 6 duplicate quaternary clauses
c [quatres-9-2] added 21 single-self-subsuming ternary resolvents
c [quatres-9-2] added 227 quaternary resolvents
c [ternres-9] limit 147384032 with penalty 0 = 0 + 0
c [ternres-9] all 591 free variables schedulable
c [ternres-9] 107 ternary resolvents (1 bin, 106 trn)
c [ternres-9] fully completed ternary resolution
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 7 transitive binary clauses
c [block-4] scheduling all variables this time
c [block-4] scheduled 591 variables 100%
c [block-4] limit of 100000000 steps penalty 3 = 3 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 0 blocked clauses
c [elim-8] scheduling all variables this time
c [elim-8] scheduled 591 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 18 variables 3% in round 1 in 43388401 steps
c [elim-8-1] backward subsumption/strengthening limit 43388400
c [elim-8-1-1] backward checking 79 touched variables 13%
c [elim-8-1-1] fully completed backward checking in 1 rounds
c [elim-8-1] subsumed 0 and strengthened 5 clauses in 307359 steps
c [elim-8-1] rescheduled 12 variables 2% by backward subsumption
c [elim-8-2] eliminated 1 variables 0% in round 2 in 5637672 steps
c [elim-8-2] backward subsumption/strengthening limit 5637600
c [elim-8-2-1] backward checking 5 touched variables 1%
c [elim-8-2-1] fully completed backward checking in 1 rounds
c [elim-8-2] subsumed 0 and strengthened 0 clauses in 54138 steps
c [elim-8] fully completed in 2 rounds
c [elim-8] transition to [ all 0 rem 0 ] state
c [elim-8] eliminated 19 = 3% variables out of 591 scheduled
c [bca-4] limit of 10000000 steps and 25506 added (scaled 2)
c [bca-4] 1 out of 1146 literals actually usable 0%
c [bca-4] not enough literals usable
c [bca-4] added 0 blocked clauses in 102668 steps
c [sort-queue-12] sorted 572 enqueued variables after 1346861 conflicts
c [score-dist-12] active 0 (0%), one 0 (0%), zero 572 (100%)
c [score-dist-12] max exp 0, different 1 (100%)
c [score-dist-12] median active exp 0, avg 0.0
c [simplification-12] removed 19 variables 3.2% (572 remain 26%)
c [simplification-12] removed 54 irredundant clauses 0.4% (12503 remain 41%)
c [simplification-12] maximum reduction of 3% = max (3%, 0%)
c [simplification-12] geometric conflict interval increment 159996 = 639984 / 4
c [simplification-12] new conflict interval 799980
c [simplification-12] penalized conflict interval 799980 = 1 * 799980
c [simplification-12] hard conflict limit 2546831 (soft 2146841 + delta 399990)
c [simplification-12] new conflict limit 2146841 (hard 2546831)
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 -  395.6     572    12503   1378649   85044   1314    27   14    34   11  42%   1024   -0   14   14  100%
c -  416.7     572    12503   1432218   87490   1335    27   15    41   11  37%   1024    5   15   15  104%
c -  435.1     572    12503   1485980   90529   1343    27   15    40   11  38%   1024    2   15   15   99%
c -  453.2     572    12503   1540129   92867   1352    27   15    33   11  44%   1024   -5   14   15   92%
c -  474.7     572    12503   1595109   95185   1360    27   16    42   11  38%   1024    5   14   15   90%
c -  493.9     572    12503   1650811   98112   1365    28   15    30   12  49%   1024   -6   15   15   99%
c -  517.2     572    12503   1706700  100037   1370    28   15    62   12  25%   1024   24   16   15  103%
c -  541.3     572    12503   1763626  102386   1377    28   16    38   12  43%   1024   -0   16   16  103%
c -  562.7     572    12503   1821355  105418   1384    28   16    34   13  47%   1024   -2   18   16  113%
c -  586.3     572    12503   1878505  106480   1389    29   15    42   13  37%   1024    3   17   15  109%
c -  612.8     572    12503   1937367  109370   1403    29   16    45   13  36%   1024    5   17   16  111%
c -  637.0     572    12503   1997321  112583   1406    30   14    29   13  50%   1024   -5   14   15   91%
c -  663.7     572    12503   2056064  114363   1411    30   16    48   14  33%   1024   13   17   15  116%
c -  693.6     572    12503   2116444  116319   1417    30   15    34   14  43%   1024   -1   14   15   89%
c 
c [simplification-13] limit 2146841 conflicts (hard 2546831) hit after 2146842 conflicts
c [quatres-10] found 9770 quaternary clauses 10% in total
c [quatres-10-1] removed 21 duplicate quaternary clauses
c [quatres-10-2] added 14 single-self-subsuming ternary resolvents
c [quatres-10-2] added 168 quaternary resolvents
c [ternres-10] limit 200000000 with penalty 0 = 0 + 0
c [ternres-10] all 572 free variables schedulable
c [ternres-10] 43 ternary resolvents (1 bin, 42 trn)
c [ternres-10] fully completed ternary resolution
c [gauss-4] limit 6250000 penalty 3 = 3 + 0
c [gauss-4] extracted 2617 xors of average arity 6.5
c [gauss-4] connected 17135 occurrences of 105 variables (average 163.2)
c [gauss-4] limit 6250000 penalty 3 = 3 + 0
c [gauss-4] connected 1110 occurrences of 105 variables (average 10.6)
c [gauss-4] fully completed
c [gauss-4] exported 0 unary, 0 binary and 0 ternary equations
c [treelook-4] limit 13748065 penalty 1 = 1 + 0 boost 1
c [treelook-4] scheduled 1144 literals 100%
c [treelook-4] scheduling used 544884 steps
c [treelook-4] scheduled completely
c [treelook-4] limit 13748065 penalty 1 = 1 + 0 boost 1
c [treelook-4] used 514047 steps
c [treelook-4] fully completed tree based probing
c [transred-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 5 transitive binary clauses
c [cce-5] limit of 171850814 steps penalty 3 = 3 + 0
c [cce-5-1] eliminated 9 clauses out of 543 (2%) of length 5
c [cce-5-1] eliminated 25 clauses out of 2077 (1%) of length 4
c [cce-5-1] completed large round (ACCE)
c [cce-5-1] eliminated 34 large clauses in 24310086 steps
c [cce-5-1] allowing another 12155043 steps for small clauses
c [cce-5-1] scheduling 588 clauses = 182 binary + 406 ternary
c [cce-5-1] tried to eliminate 588 small clauses 100%
c [cce-5-1] eliminated 2 binary clauses 1%
c [cce-5-1] eliminated 2 ternary clauses 0%
c [cce-5-1] eliminated 4 small clauses 1%
c [cce-5-1] eliminated 4 small clauses in 12802467 steps
c [cce-5-1] completed small round (ACCE)
c [cce-5-1] completed small and large (ACCE)
c [cce-5-1] eliminated 38 covered clauses in round 1
c [cce-5-2] completed large round (ACCE)
c [cce-5-2] allowing another 12098736 steps for small clauses
c [cce-5-2] scheduling 584 clauses = 180 binary + 404 ternary
c [cce-5-2] tried to eliminate 584 small clauses 100%
c [cce-5-2] completed small round (ACCE)
c [cce-5-2] eliminated 0 covered clauses in round 2
c [cce-5] eliminated 38 covered clauses in TOTAL during 2 rounds
c [cce-5] 38 < 1/100 * 12503 = 125 considered unsuccessful
c [elim-9] scheduling all variables this time
c [elim-9] scheduled 572 variables 100%
c [elim-9] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-9] rescheduling of touched variables disabled
c [elim-9-1] eliminated 3 variables 1% in round 1 in 43153017 steps
c [elim-9-1] backward subsumption/strengthening limit 43153000
c [elim-9-1-1] backward checking 21 touched variables 4%
c [elim-9-1-1] fully completed backward checking in 1 rounds
c [elim-9-1] subsumed 0 and strengthened 0 clauses in 67943 steps
c [elim-9] fully completed in 1 rounds
c [elim-9] transition to [ all 0 rem 0 ] state
c [elim-9] eliminated 3 = 1% variables out of 572 scheduled
c [elim-9] 3 < 1/100 * 572 = 5 considered unsuccessful
c [sort-queue-13] sorted 569 enqueued variables after 2146842 conflicts
c [score-dist-13] active 0 (0%), one 0 (0%), zero 569 (100%)
c [score-dist-13] max exp 0, different 1 (100%)
c [score-dist-13] median active exp 0, avg 0.0
c [simplification-13] removed 3 variables 0.5% (569 remain 26%)
c [simplification-13] removed 48 irredundant clauses 0.4% (12455 remain 41%)
c [simplification-13] maximum reduction of 1% = max (1%, 0%)
c [simplification-13] geometric conflict interval increment 399990 = 799980 / 2
c [simplification-13] conflict interval soft limit 1000000 reached
c [simplification-13] new conflict interval 1000000
c [simplification-13] penalized conflict interval 1000000 = 1 * 1000000
c [simplification-13] hard conflict limit 3646842 (soft 3146842 + delta 500000)
c [simplification-13] new conflict limit 3146842 (hard 3646842)
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 -  723.9     569    12455   2177665  119292   1470    26   15    39   14  40%   1024    3   17   15  110%
c -  753.7     569    12455   2238585  121306   1474    26   16    35   14  44%   1024   -1   15   15   94%
c -  779.7     569    12455   2300083  124274   1474    26   15    34   15  44%   1024   -1   15   15   99%
c -  811.6     569    12455   2362115  126061   1476    26   15    38   15  40%   1024    3   15   15  101%
c -  847.6     569    12455   2425750  128269   1483    26   15    32   15  47%   1024   -4   13   15   86%
c -  880.4     569    12455   2490004  131447   1487    26   15    41   15  38%   1024    5   17   15  112%
c -  912.1     569    12455   2553917  133505   1491    26   15    32   15  45%   1024   -6   14   15   92%
c -  945.4     569    12455   2618600  136008   1492    26   16    34   15  45%   1024   -1   16   15  105%
c -  979.1     569    12455   2683739  138242   1497    26   15    32   16  46%   1024   -3   15   15   97%
c
c CAUGHT SIGNAL 15 SIGTERM
c
c s UNKNOWN
c bate: 0 basic ate = 0 trn 0% + 0 lrg 0% in 0 updates
c bcas: 4 count, 0 added (0 skipped), 176508 steps
c bkwd: tried 20701 clauses, 40318 lits, 1.95 lits/clause
c bkwd: checked 6183596 occs, 298.71 occs/clause, 153.37 occs/lit
c bkwd: subsumed 0 binary, 9 ternary, 218 large
c bkwd: strengthened 0 binary, 0 ternary (0% self), 1125 large (0% self)
c blkd: 4 bces, 9 removed, 1357416 resolutions, 2133650 steps
c blkd: 194 blocking literals 4%, 0 pure
c bump: 0 bumped seen, 0 lits 0.0 on average
c card: 4 count, 0 units, 5 am1, 6402387 steps
c card: 4 rescheduled, 10 eliminated, 2388 resolved, 195 subsumed
c card: 14 at-most-one constraints found, average size 3.00
c card: 14 at-most-one constraints used 100%, average size 3.00
c card: 19 at-most-two constraints found, average size 4.00
c card: 19 at-most-two constraints used 100%, average size 4.00
c cces: 5 cces, 3774 eliminated, 3555 ate 94%, 219 abce 6%
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: 208168 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 57 gcs, 0 rescored clauses, 0 rescored vars
c dcps: 34 decompositions, 162 equivalent 7%
c deco: 0 decision-only clauses 0%, 0% reduction
c decs: 7881517 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 9 elims, 1451 eliminated 64%, 3 pure 0%
c elms: 24 rounds, 2.7 rounds/bve
c elms: 1448 small 100%, 0 large 0%
c elms: 5983 tried small, 1448 succeeded 24%, 4535 failed 76%
c elms: 1509 subsumed, 2070 strengthened, 5 blocked
c elms: 725942 copies, 3283215 resolutions, 550813 ipos
c elms: 460082 subchks, 588839 strchks
c gaus: 4 extractions, 4814 extracted, 6.3 size, 7 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 1 gc, 21407234 steps, 10703617 extr 50%, 50911 elim 0%
c glue: 14.7 orig avg, 14.7 real avg, 3.4 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 654 = 275 simple 42% + 313 trn 48% + 66 lrg 10%, 20 sub 3%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 2724667 clauses, 25.9 length
c lrnd: 70630988 lits = 91070423 orig - 20439435 removed 22%
c lrnd: 1146098 uips 42%, 1086028 flips 40%
c mins: 2646672 mins 97%, 36 bin 0%, 77959 size 3%
c mins: 38059936 poisoned searches, 6538821 hits, 17% hit rate
c mins: 119335222 used twice searches, 27209008 hits, 23% hit rate
c move: moved 415, 308 bin 74%, 107 trn 26%
c otfs: 6596 driving 37%, 11305 restarting 63%
c otfs: str 17901, 17643 red 99%, 258 irr 1%
c otfs: str 17901, 0 bin 0%, 17 trn 0%, 17884 lrg 100%
c otfs: sub 128, 110 red 86%, 18 irr 14%
c otfs: sub 128, 0 bin 0%, 3 trn 2%, 125 lrg 98%
c phas: 1 computed, 1643 set, 0 pos (0%), 1643 neg (100%)
c prbs: 3 basic, 13939 probed, 23 failed, 0 lifted
c prbs: 4 simple, 5701 probed, 1 failed, 0 eqs
c prbs: 4 treelook, 3221 probed, 1 failed, 0 lifted
c prom: 659438 locked 21% out of 3113798 tried
c prps: 217442305 props, 28 props/dec
c prps: 100% srch, 0% simp, 0% lkhd
c quat: 10 count, 1912 quat, 197 self1, 7 self2, 245 dup
c queu: 13 sorted, 7881517 next (0 steps 0.00)
c queu: 14111 enq (14097 steps 1.00), 0 deq 0%
c redc: 7890 clauses 2%, 318757 tried 12%, 1 sat 0%
c redc: 8394 lits 0%, 3442383 tried 4%, 1 sat 0%
c redc: 165 times jump level reduced, 5.6 levels on average
c reds: 51 count, 53440.7 conflicts per reduce
c reds: 0 memlim 0%, 51 arith 100%
c reds: 1912562 collected 80%, 485636 retired 20%
c rmbd: 60 removed, 60 red 100%
c rsts: 17105 restarts 100%, 0 skipped 0%
c rsts: 0 saturating 0%, 0 reuse 0%
c rsts: 0 kept 0.0% average 0.0%
c scnc: 0 count, 1.000 min (0/1000), 1.000 max (0/1000)
c simp: 13 count, 13 confs 100%, 0 vars 0%
c simp: 0 its 0%, 0 bin 0%, 0 trns 0%
c subl: 2724667 count (785047 tried 0.3), 69801 sub out of 2722912 (2.6%)
c swps: 5 count, 8 rounds, 206 queries (25.8/round)
c swps: 206 sat calls, 0 unsat (28.1% success rate)
c swps: 12391 decisions 60.2, 5785 conflicts 28.1
c swps; 55.0 avg class size, 146.0 avg environment size
c swps: 0 failed, 1 impls, 0 equivs
c swp0: 68 type 0 queries, 5 unsat (7.4%), 68 sat (100.0%)
c swp1: 138 type 1 queries, 13 unsat (9.4%), 138 sat (100.0%)
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: 15763295 calls to obtain time
c tops: 95 fixed 4%, 1 its, 2725478.00 confs/it
c trds: 10 transitive reductions, 97 removed, 0 failed
c trds: 15915 nodes, 9598 edges, 64282 steps
c trim: 413857 words, 1.6 MB
c trnr: 10 count, 9 bin, 704 trn, 17602389 steps
c unhd: 4 count, 5 rounds, 4322734 steps
c unhd: 0 non-trivial sccs of average size 0.0
c unhd: 0 units, 0 bin, 0 trn, 0 lrg
c unhd: 0 failed, 0 stamp, 0 lits, 0 bin, 0 trn, 0 lrg
c unhd: 5006 tauts, 2 bin 0%, 70 trn 1%, 4928 lrg 98%
c unhd: 5006 tauts, 6 stamp 0%, 76 red 2%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 53903 str, 0 bin 0%, 31 trn 0%, 53872 lrg 100%, 43483 red 81%
c vars: 574 remaining 25% and 1708 removed 75% out of 2282
c vars: 95 fixed 4%, 1451 eliminated 64%, 162 equivalent 7%
c vsts: 38820601626 visits, 100% srch, 0% simp, 0% lkhd
c vsts: 178.8 search visits per propagation, 14221.8 per conflict
c wchs: 22335298536 pushed, 6649525 enlarged, 1575 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all        2724824       1912562        485636     126145192      27024225       1615474
c 
c  0 0        132331   5      9005   0         0   0  99694195  79< 19442915  72   1092028  68     3.6
c  1 5        109105   4     51096   3     29352   6  14204401  11   2825615  10<   205053  13<    0.8
c  2 6        408020  15    283153  15     90010  19   7540896   6   1995162   7    149373   9     1.3
c  3 9        676322  25<   533136  28    116221  24   2078898   2   1098897   4     74349   5     1.9
c  4 14       784634  29    612442  32<   127995  26<  1610961   1   1015999   4     63296   4     2.9
c  5 21       529323  19    373443  20     97469  20    892645   1    574622   2     28710   2     2.1
c  6 30        78926   3     47055   2     22232   5    114616   0     66628   0      2513   0     0.5
c  7 41         5663   0      3000   0      2141   0      7913   0      4064   0       138   0     0.1
c  8 54          457   0       213   0       197   0       621   0       298   0        13   0     0.0
c  9 69           41   0        18   0        18   0        44   0        24   0         1   0     0.0
c 10 86            2   0         1   0         1   0         2   0         1   0         0   0     0.0
c 
c avg                  3.4           3.6           3.5           0.4           0.6           0.7
c std                  1.4           1.1           1.3           0.9           1.3           1.2
c 
c    4.692   0% decide
c    3.383   0% elim
c    2.021   0% sweep
c 
c    2.315 < 1% rest (below)
c 
c    1.493   0% cce
c    0.662   0% probe
c    0.536   0% unhide
c    0.512   0% quatres
c    0.230   0% gauss
c    0.172   0% block
c    0.085   0% ternres
c    0.079   0% card
c    0.023   0% bca
c    0.015   0% transred
c    0.000   0% bump
c    0.000   0% locs
c    0.000   0% queuesort
c    0.000   0% rescore
c ==================================
c    0.413   0% preprocessing     4%
c    9.328   1% inprocessing     96%
c ==================================
c    9.741   1% simplifying
c  990.270  99% search
c ==================================
c 1000.011 100% all
c 
c       2725478 conflicts,        2725.4 confs/sec
c          1681 ternaries,        1621.3 confs/ternary
c            60 binaries,        45424.6 confs/binary
c             1 iterations,    2725478.0 confs/iteration
c 
c            51 reductions,          0.1 redus/sec,  53440.7 confs/reduction
c         17105 restarts,           17.1 rests/sec,    159.3 confs/restart
c       7881517 decisions,        7881.4 decis/sec,      2.9 decis/conflict
c     217442305 propagations,   217439.9 props/sec,     27.6 props/decision
c 
c 1000.0 seconds, 42.4 MB
c
c CAUGHT SIGNAL 15 SIGTERM
c
c launch: done
