c launch: /data/cnf/sc2014/app/hitag2-10-60-0-0xe14721bd199894a-99.cnf.bz2
c host: atom11
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-10-60-0-0xe14721bd199894a-99.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/hitag2-10-60-0-0xe14721bd199894a-99.cnf.bz2
c no embedded options
c found 'p cnf 2294 30374' header
c read 2294 variables, 30374 clauses, 178542 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=6
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 2215 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] AVG (--score=6)
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    2215    30304         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 2056 free variables schedulable
c [simpleprobe-1] boosting simple probing limit by 10
c [simpleprobe-1] limit 20000000 penalty 0 = 0 + 0
c [simpleprobe-1] 358 variables remain 17% (1698 retained 83%)
c [simpleprobe-1] removed 0 variables, found 236 hbrs, 0 units
c [unhide-1] limit 100000 with penalty 0 = 0 + 0
c [unhide-1-1] 0 units, 0 failed, 5166 tauts, 0 hbrs, 7743 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 2056 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 358 variables 17% in round 1 in 2678036 steps
c [elim-1-1] backward subsumption/strengthening limit 2678000
c [elim-1-1-1] backward checking 876 touched variables 43%
c [elim-1-1-1] incomplete backward checking 884 remain 101%
c [elim-1-1] subsumed 106 and strengthened 278 clauses in 2678386 steps
c [elim-1-1] rescheduled 129 variables 6% by backward subsumption
c [elim-1-2] eliminated 15 variables 1% in round 2 in 175814 steps
c [elim-1-2] backward subsumption/strengthening limit 175800
c [elim-1-2-1] backward checking 884 touched variables 43%
c [elim-1-2-1] incomplete backward checking 885 remain 100%
c [elim-1-2] subsumed 2 and strengthened 16 clauses in 176192 steps
c [elim-1-2] rescheduled 24 variables 1% by backward subsumption
c [elim-1-3] no variable eliminated in round 3 in 22974 steps
c [elim-1] fully completed in 3 rounds
c [elim-1] transition to [ all 0 rem 0 ] state
c [elim-1] eliminated 373 = 18% variables out of 2056 scheduled
c [phase-count-1] 21286 negative 98.0% of 21721 except 435 2.0%
c [phase-count-1] 20254 positive 93.2% of 21721 except 1467 6.8%
c [phase-count-1] less non-negative clauses 435 than limit 2100 (10.0%)
c [phase-count-1] non-pos/non-neg = 1467/435 = 3.37 >= 2.00 = 200/100
c [lucky-phase-1] forcing lucky phase -1
c [phase-1] phase bias: 0 positive 0%, 1683 negative 100%
c [sort-queue-1] sorted 1683 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 1683 (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 532 variables 24.0% (1683 remain 76%)
c [simplification-1] removed 8583 irredundant clauses 28.3% (21721 remain 72%)
c [simplification-1] maximum reduction of 28% = max (24%, 28%)
c [simplification-1] large reduction 28% >= 5% limit
c [simplification-1] next conflict interval 1000 = 2000/2
c [simplification-1] penalized conflict interval 1000 = 1 * 1000
c [simplification-1] hard conflict limit 11000 (soft 1000 + delta 10000)
c [simplification-1] new conflict limit 1000 (hard 11000)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i    0.4    1682    21721       359     318     18   178    1     3    3  36%      1    3    9    0 14197%
c 
c [simplification-2] limit 1000 conflicts (hard 11000) hit after 1002 conflicts
c [decomp-3] removed 1 variables
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 3364 literals 100%
c [treelook-1] scheduling used 65023 steps
c [treelook-1] scheduled completely
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 302683 steps
c [treelook-1] 3267 literals remain 97%
c [treelook-1] 1682 variables remain to probed next time 100%
c [treelook-1] removed 0 variables, found 27 hbrs
c [basicprobe-1] limit 1000000 penalty 0 = 0 + 0
c [basicprobe-1-0] 1154 sched 69%, 14 failed, 0 lifted, 86 hbrs
c [decomp-5] removed 14 variables
c [basicprobe-1-1] 1129 sched 68%, 0 failed, 0 lifted, 21 hbrs
c [basicprobe-1-2] 1122 sched 67%, 0 failed, 0 lifted, 2 hbrs
c [basicprobe-1-3] 1122 sched 67%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-1-3] fully completed probing
c [basicprobe-1-3] 14 units = 14 failed (100%) + 0 lifted (0%)
c [basicprobe-1-3] removed 14 variables, found 109 hbrs
c [block-1] scheduling all variables this time
c [block-1] scheduled 1668 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 934 blocked clauses
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 1 clauses out of 1 (100%) of length 8
c [cce-1-1] eliminated 449 clauses out of 9529 (5%) of length 7
c [cce-1-1] eliminated 1365 clauses out of 2325 (59%) of length 6
c [cce-1-1] eliminated 705 clauses out of 3440 (20%) of length 5
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 2520 large clauses in 30000159 steps
c [cce-1-1] allowing another 15000079 steps for small clauses
c [cce-1-1] scheduling 3392 clauses = 2856 binary + 536 ternary
c [cce-1-1] tried to eliminate 3392 small clauses 100%
c [cce-1-1] eliminated 27 binary clauses 1%
c [cce-1-1] eliminated 5 ternary clauses 1%
c [cce-1-1] eliminated 32 small clauses 1%
c [cce-1-1] eliminated 32 small clauses in 17860333 steps
c [cce-1-1] completed small round (ATE)
c [cce-1-1] eliminated 2552 covered clauses in round 1
c [cce-1-2] incomplete large round (ATE)
c [cce-1-2] allowing another 6069954 steps for small clauses
c [cce-1-2] scheduling 3360 clauses = 2829 binary + 531 ternary
c [cce-1-2] tried to eliminate 3360 small clauses 100%
c [cce-1-2] completed small round (ATE)
c [cce-1-2] eliminated 0 covered clauses in round 2
c [cce-1] eliminated 2552 covered clauses in TOTAL during 2 rounds
c [elim-2] scheduling all variables this time
c [elim-2] scheduled 1665 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 294 variables 18% in round 1 in 3229250 steps
c [elim-2-1] backward subsumption/strengthening limit 3229200
c [elim-2-1-1] backward checking 657 touched variables 39%
c [elim-2-1-1] incomplete backward checking 525 remain 80%
c [elim-2-1] subsumed 49 and strengthened 369 clauses in 3229964 steps
c [elim-2-1] rescheduled 291 variables 17% by backward subsumption
c [elim-2-2] eliminated 34 variables 2% in round 2 in 276096 steps
c [elim-2-2] backward subsumption/strengthening limit 276000
c [elim-2-2-1] backward checking 599 touched variables 36%
c [elim-2-2-1] incomplete backward checking 606 remain 101%
c [elim-2-2] subsumed 2 and strengthened 24 clauses in 276034 steps
c [elim-2-2] rescheduled 44 variables 3% by backward subsumption
c [elim-2-3] eliminated 1 variables 0% in round 3 in 43278 steps
c [elim-2-3] backward subsumption/strengthening limit 43200
c [elim-2-3-1] backward checking 610 touched variables 37%
c [elim-2-3-1] incomplete backward checking 600 remain 98%
c [elim-2-3] subsumed 0 and strengthened 1 clauses in 43460 steps
c [elim-2] incomplete 5 not tried 0% in round 3
c [elim-2] transition to [ all 1 rem 1 ] state
c [elim-2] eliminated 329 = 20% variables out of 1665 scheduled
c [bca-1] limit of 10000000 steps and 33904 added (scaled 2)
c [bca-1] 1927 out of 2674 literals actually usable 72%
c [bca-1] added 0 blocked clauses in 7880 steps
c [sweep-1] limit 1000000 penalty 0 = 0 + 0
c [sweep-1-1] 308 pos 23.1% + 1028 neg 76.9% = 1336 sched 100.0% ret 0
c [sweep-1-1] 1037277 steps 92 queries 43.34 avg class size
c [sweep-1-1] 1693 decisions 91 SAT calls 26.00 avg env size
c [sweep-1-1] 19 variables remain 1% (1317 retained 99%)
c [sweep-1-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 0 vars in TOTAL (1 rounds, 91 queries)
c [sort-queue-2] sorted 302 enqueued variables after 1002 conflicts
c [score-dist-2] active 1034 (77%), one 0 (0%), zero 302 (23%)
c [score-dist-2] max exp 512, different 10 (2%)
c [score-dist-2] median active exp 512, avg 511.4
c [simplification-2] removed 346 variables 20.6% (1336 remain 60%)
c [simplification-2] removed 5019 irredundant clauses 23.1% (16701 remain 55%)
c [simplification-2] maximum reduction of 23% = max (21%, 23%)
c [simplification-2] large reduction 23% >= 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 13002 (soft 3002 + delta 10000)
c [simplification-2] new conflict limit 3002 (hard 13002)
c 
c [simplification-3] limit 3002 conflicts (hard 13002) hit after 3002 conflicts
c [quatres-1] found 2228 quaternary clauses 15% in total
c [quatres-1-1] removed 11 duplicate quaternary clauses
c [quatres-1-1] added 7 double-self-subsuming ternary resolvents
c [quatres-1-2] added 19 single-self-subsuming ternary resolvents
c [quatres-1-2] added 180 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 1336 free variables schedulable
c [ternres-1] 127 ternary resolvents (0 bin, 127 trn)
c [ternres-1] fully completed ternary resolution
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] no at-most-one constraint found
c [card-2] no at-most-two constraint found
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 832 xors of average arity 6.1
c [gauss-1] connected 5048 occurrences of 88 variables (average 57.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 [simpleprobe-2] 249 schedulable variables 19%
c [simpleprobe-2] limit 1000000 penalty 1 = 1 + 0
c [simpleprobe-2] 217 variables remain 16% (1119 retained 84%)
c [simpleprobe-2] removed 0 variables, found 5 hbrs, 0 units
c [unhide-2] limit 50000 with penalty 1 = 1 + 0
c [unhide-2-2] 0 units, 0 failed, 41 tauts, 0 hbrs, 1903 literals
c [transred-1] limit 100000 with penalty 0 = 0 + 0
c [transred-1] removed 33 transitive binary clauses
c [block-2] scheduling all variables this time
c [block-2] scheduled 1336 variables 100%
c [block-2] limit of 50000000 steps penalty 0 = 0 + 0
c [block-2] fully completed
c [block-2] transition to [ all 0 rem 0 ] state
c [block-2] eliminated 34 blocked clauses
c [block-2] 34 < 1/100 * 16680 = 166 considered unsuccessful
c [cce-2] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-2-1] eliminated 1 clauses out of 8798 (0%) of length 7
c [cce-2-1] eliminated 14 clauses out of 666 (2%) of length 6
c [cce-2-1] eliminated 711 clauses out of 2033 (35%) of length 5
c [cce-2-1] eliminated 482 clauses out of 2236 (22%) of length 4
c [cce-2-1] completed large round (ATE)
c [cce-2-1] eliminated 1208 large clauses in 28826111 steps
c [cce-2-1] allowing another 14413055 steps for small clauses
c [cce-2-1] scheduling 2327 clauses = 1993 binary + 334 ternary
c [cce-2-1] tried to eliminate 2327 small clauses 100%
c [cce-2-1] eliminated 34 binary clauses 2%
c [cce-2-1] eliminated 39 ternary clauses 12%
c [cce-2-1] eliminated 73 small clauses 3%
c [cce-2-1] eliminated 73 small clauses in 16333654 steps
c [cce-2-1] completed small round (ATE)
c [cce-2-1] completed small and large (ATE)
c [cce-2-1] eliminated 1281 covered clauses in round 1
c [cce-2-2] incomplete large round (ATE)
c [cce-2-2] allowing another 6833298 steps for small clauses
c [cce-2-2] scheduling 2254 clauses = 1959 binary + 295 ternary
c [cce-2-2] tried to eliminate 2254 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 1281 covered clauses in TOTAL during 2 rounds
c [elim-3] no untried remaining variables left
c [elim-3] scheduled 1334 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 453 variables 34% in round 1 in 8334007 steps
c [elim-3-1] backward subsumption/strengthening limit 8334000
c [elim-3-1-1] backward checking 751 touched variables 56%
c [elim-3-1-1] fully completed backward checking in 1 rounds
c [elim-3-1] subsumed 52 and strengthened 328 clauses in 4309514 steps
c [elim-3-1] rescheduled 314 variables 24% by backward subsumption
c [elim-3-2] eliminated 44 variables 3% in round 2 in 3408308 steps
c [elim-3-2] backward subsumption/strengthening limit 3408300
c [elim-3-2-1] backward checking 133 touched variables 10%
c [elim-3-2-1] fully completed backward checking in 1 rounds
c [elim-3-2] subsumed 0 and strengthened 9 clauses in 806827 steps
c [elim-3-2] rescheduled 27 variables 2% by backward subsumption
c [elim-3-3] no variable eliminated in round 3 in 8930 steps
c [elim-3] fully completed in 3 rounds
c [elim-3] transition to [ all 0 rem 0 ] state
c [elim-3] eliminated 497 = 37% variables out of 1334 scheduled
c [sweep-2] limit 1000000 penalty 0 = 0 + 0
c [sweep-2-1] 4 pos 30.8% + 9 neg 69.2% = 13 sched 1.6% ret 824
c [sweep-2-1] 332719 steps 8 queries 4.88 avg class size
c [sweep-2-1] 361 decisions 7 SAT calls 36.71 avg env size
c [sweep-2-1] fully completed sweeping round
c [sweep-2-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-2-2] 275 pos 32.9% + 562 neg 67.1% = 837 sched 100.0% ret 0
c [sweep-2-2] 709963 steps 34 queries 68.88 avg class size
c [sweep-2-2] 1077 decisions 34 SAT calls 41.59 avg env size
c [sweep-2-2] 192 variables remain 23% (645 retained 77%)
c [sweep-2-2] removed 0 vars (0 failed, 0 eqs, 1 impls)
c [sweep-2] removed 0 vars in TOTAL (2 rounds, 40 queries)
c [sort-queue-3] sorted 165 enqueued variables after 3002 conflicts
c [score-dist-3] active 672 (80%), one 0 (0%), zero 165 (20%)
c [score-dist-3] max exp 513, different 10 (2%)
c [score-dist-3] median active exp 513, avg 512.4
c [simplification-3] removed 499 variables 37.4% (837 remain 38%)
c [simplification-3] removed 2937 irredundant clauses 17.6% (13758 remain 45%)
c [simplification-3] maximum reduction of 37% = max (37%, 18%)
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 15002 (soft 5002 + delta 10000)
c [simplification-3] new conflict limit 5002 (hard 15002)
c 
c [simplification-4] limit 5002 conflicts (hard 15002) hit after 5002 conflicts
c [quatres-2] found 2297 quaternary clauses 18% in total
c [quatres-2-1] removed 20 duplicate quaternary clauses
c [quatres-2-1] added 5 double-self-subsuming ternary resolvents
c [quatres-2-2] added 26 single-self-subsuming ternary resolvents
c [quatres-2-2] added 295 quaternary resolvents
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] all 837 free variables schedulable
c [ternres-2] 65 ternary resolvents (0 bin, 65 trn)
c [ternres-2] fully completed ternary resolution
c [transred-2] limit 104521 with penalty 0 = 0 + 0
c [transred-2] removed 10 transitive binary clauses
c [cce-3] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-3-1] eliminated 2 clauses out of 566 (0%) of length 6
c [cce-3-1] eliminated 63 clauses out of 1031 (6%) of length 5
c [cce-3-1] eliminated 56 clauses out of 1879 (3%) of length 4
c [cce-3-1] completed large round (ACCE)
c [cce-3-1] eliminated 121 large clauses in 27290211 steps
c [cce-3-1] allowing another 13645105 steps for small clauses
c [cce-3-1] scheduling 1216 clauses = 810 binary + 406 ternary
c [cce-3-1] tried to eliminate 1216 small clauses 100%
c [cce-3-1] eliminated 60 binary clauses 7%
c [cce-3-1] eliminated 8 ternary clauses 2%
c [cce-3-1] eliminated 68 small clauses 6%
c [cce-3-1] eliminated 68 small clauses in 14897454 steps
c [cce-3-1] completed small round (ACCE)
c [cce-3-1] completed small and large (ACCE)
c [cce-3-1] eliminated 189 covered clauses in round 1
c [cce-3-2] incomplete large round (ACCE)
c [cce-3-2] allowing another 7551273 steps for small clauses
c [cce-3-2] scheduling 1148 clauses = 750 binary + 398 ternary
c [cce-3-2] tried to eliminate 1148 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 189 covered clauses in TOTAL during 2 rounds
c [elim-4] scheduling all variables this time
c [elim-4] scheduled 837 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 42 variables 5% in round 1 in 30260794 steps
c [elim-4-1] backward subsumption/strengthening limit 30260700
c [elim-4-1-1] backward checking 206 touched variables 25%
c [elim-4-1-1] fully completed backward checking in 1 rounds
c [elim-4-1] subsumed 3 and strengthened 39 clauses in 899675 steps
c [elim-4-1] rescheduled 50 variables 6% by backward subsumption
c [elim-4-2] eliminated 10 variables 1% in round 2 in 4910224 steps
c [elim-4-2] backward subsumption/strengthening limit 4910200
c [elim-4-2-1] backward checking 34 touched variables 4%
c [elim-4-2-1] fully completed backward checking in 1 rounds
c [elim-4-2] subsumed 0 and strengthened 2 clauses in 153303 steps
c [elim-4-2] rescheduled 5 variables 1% by backward subsumption
c [elim-4-3] no variable eliminated in round 3 in 1259082 steps
c [elim-4] fully completed in 3 rounds
c [elim-4] transition to [ all 0 rem 0 ] state
c [elim-4] eliminated 52 = 6% variables out of 837 scheduled
c [bca-2] limit of 10000000 steps and 27238 added (scaled 2)
c [bca-2] 597 out of 1572 literals actually usable 38%
c [bca-2] added 0 blocked clauses in 6716 steps
c [sort-queue-4] sorted 162 enqueued variables after 5002 conflicts
c [score-dist-4] active 623 (79%), one 0 (0%), zero 162 (21%)
c [score-dist-4] max exp 514, different 11 (2%)
c [score-dist-4] median active exp 514, avg 513.1
c [simplification-4] removed 52 variables 6.2% (785 remain 35%)
c [simplification-4] removed 386 irredundant clauses 2.8% (13369 remain 44%)
c [simplification-4] maximum reduction of 6% = max (6%, 3%)
c [simplification-4] large reduction 6% >= 5% limit
c [simplification-4] next conflict interval 2000 = 2000/1
c [simplification-4] penalized conflict interval 2000 = 1 * 2000
c [simplification-4] hard conflict limit 17002 (soft 7002 + delta 10000)
c [simplification-4] new conflict limit 7002 (hard 17002)
c 
c [simplification-5] limit 7002 conflicts (hard 17002) hit after 7002 conflicts
c [quatres-3] found 2508 quaternary clauses 19% in total
c [quatres-3-1] removed 8 duplicate quaternary clauses
c [quatres-3-1] added 5 double-self-subsuming ternary resolvents
c [quatres-3-2] added 12 single-self-subsuming ternary resolvents
c [quatres-3-2] added 169 quaternary resolvents
c [ternres-3] limit 4000000 with penalty 0 = 0 + 0
c [ternres-3] all 785 free variables schedulable
c [ternres-3] 14 ternary resolvents (0 bin, 14 trn)
c [ternres-3] fully completed ternary resolution
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] extracted 403 xors of average arity 5.9
c [gauss-2] connected 2365 occurrences of 45 variables (average 52.6)
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 [treelook-2] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-2] scheduled 1570 literals 100%
c [treelook-2] scheduling used 64032 steps
c [treelook-2] scheduled completely
c [treelook-2] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-2] used 150269 steps
c [treelook-2] 1491 literals remain 95%
c [treelook-2] 785 variables remain to probed next time 100%
c [treelook-2] removed 0 variables, found 17 hbrs
c [transred-3] limit 154022 with penalty 0 = 0 + 0
c [transred-3] removed 3 transitive binary clauses
c [block-3] scheduling all variables this time
c [block-3] scheduled 785 variables 100%
c [block-3] limit of 25000000 steps penalty 1 = 1 + 0
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 0 blocked clauses
c [cce-4] boosting limit by 10
c [cce-4] limit of 300000000 steps penalty 0 = 0 + 0
c [cce-4-1] eliminated 3 clauses out of 866 (0%) of length 5
c [cce-4-1] eliminated 10 clauses out of 1863 (1%) of length 4
c [cce-4-1] completed large round (ATE)
c [cce-4-1] eliminated 13 large clauses in 25534626 steps
c [cce-4-1] allowing another 12767313 steps for small clauses
c [cce-4-1] scheduling 1026 clauses = 636 binary + 390 ternary
c [cce-4-1] tried to eliminate 1026 small clauses 100%
c [cce-4-1] eliminated 1 ternary clauses 0%
c [cce-4-1] eliminated 1 small clauses 0%
c [cce-4-1] eliminated 1 small clauses in 13804437 steps
c [cce-4-1] completed small round (ATE)
c [cce-4-1] eliminated 14 covered clauses in round 1
c [cce-4-2] completed large round (ATE)
c [cce-4-2] allowing another 12764977 steps for small clauses
c [cce-4-2] scheduling 1025 clauses = 636 binary + 389 ternary
c [cce-4-2] tried to eliminate 1025 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 14 covered clauses in TOTAL during 2 rounds
c [cce-4] 14 < 1/100 * 13366 = 133 considered unsuccessful
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 785 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 27 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 785 scheduled
c [sweep-3] limit 500000 penalty 1 = 1 + 0
c [sweep-3-1] 60 pos 32.3% + 126 neg 67.7% = 186 sched 23.7% ret 599
c [sweep-3-1] 556894 steps 16 queries 29.88 avg class size
c [sweep-3-1] 485 decisions 15 SAT calls 47.47 avg env size
c [sweep-3-1] 109 variables remain 14% (676 retained 86%)
c [sweep-3-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-3] removed 0 vars in TOTAL (1 rounds, 15 queries)
c [sort-queue-5] sorted 159 enqueued variables after 7002 conflicts
c [score-dist-5] active 626 (80%), one 0 (0%), zero 159 (20%)
c [score-dist-5] max exp 514, different 11 (2%)
c [score-dist-5] median active exp 514, avg 513.2
c [simplification-5] removed 0 variables 0.0% (785 remain 35%)
c [simplification-5] removed 14 irredundant clauses 0.1% (13352 remain 44%)
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 20000
c [simplification-5] penalized conflict interval 20000 = 1 * 20000
c [simplification-5] hard conflict limit 37002 (soft 27002 + delta 10000)
c [simplification-5] new conflict limit 27002 (hard 37002)
c 
c [simplification-6] limit 27002 conflicts (hard 37002) hit after 27002 conflicts
c [quatres-4] found 2810 quaternary clauses 20% in total
c [quatres-4-1] removed 1 duplicate quaternary clauses
c [quatres-4-1] added 2 double-self-subsuming ternary resolvents
c [quatres-4-2] added 3 single-self-subsuming ternary resolvents
c [quatres-4-2] added 91 quaternary resolvents
c [ternres-4] limit 4000000 with penalty 0 = 0 + 0
c [ternres-4] all 785 free variables schedulable
c [ternres-4] 7 ternary resolvents (0 bin, 7 trn)
c [ternres-4] fully completed ternary resolution
c [card-3] limit 500000 penalty 2 = 2 + 0
c [card-3] no at-most-one constraint found
c [card-3] found 1 at-most-two constraints of average size 4.0
c [card-3] using previous limit 500000 for elimination
c [card-3] 1 out of 1 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [basicprobe-2] limit 5722080 penalty 0 = 0 + 0
c [basicprobe-2-0] 354 sched 45%, 3 failed, 0 lifted, 52 hbrs
c [decomp-18] removed 3 variables
c [basicprobe-2-1] 381 sched 49%, 0 failed, 0 lifted, 3 hbrs
c [basicprobe-2-2] 380 sched 49%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-2-2] fully completed probing
c [basicprobe-2-2] 3 units = 3 failed (100%) + 0 lifted (0%)
c [basicprobe-2-2] removed 3 variables, found 55 hbrs
c [unhide-3] limit 57220 with penalty 2 = 2 + 0
c [unhide-3-3] 0 units, 0 failed, 1 tauts, 0 hbrs, 2907 literals
c [transred-4] limit 1144416 with penalty 0 = 0 + 0
c [transred-4] removed 4 transitive binary clauses
c [sort-queue-6] sorted 156 enqueued variables after 27002 conflicts
c [score-dist-6] active 626 (80%), one 0 (0%), zero 156 (20%)
c [score-dist-6] max exp 516, different 13 (3%)
c [score-dist-6] median active exp 516, avg 514.6
c [simplification-6] removed 3 variables 0.4% (782 remain 35%)
c [simplification-6] removed 15 irredundant clauses 0.1% (13336 remain 44%)
c [simplification-6] maximum reduction of 0% = max (0%, 0%)
c [simplification-6] full geometric conflict interval increment 20000
c [simplification-6] new conflict interval 40000
c [simplification-6] penalized conflict interval 40000 = 1 * 40000
c [simplification-6] hard conflict limit 87002 (soft 67002 + delta 20000)
c [simplification-6] new conflict limit 67002 (hard 87002)
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 -   17.1     782    13335     55464   17350    374   161   16    23    9  73%    575   10   16    9  173%
c 
c [simplification-7] limit 67002 conflicts (hard 87002) hit after 67003 conflicts
c [quatres-5] found 3106 quaternary clauses 21% in total
c [quatres-5-1] added 2 double-self-subsuming ternary resolvents
c [quatres-5-2] added 10 single-self-subsuming ternary resolvents
c [quatres-5-2] added 64 quaternary resolvents
c [ternres-5] limit 4836586 with penalty 0 = 0 + 0
c [ternres-5] all 782 free variables schedulable
c [ternres-5] 11 ternary resolvents (1 bin, 10 trn)
c [ternres-5] fully completed ternary resolution
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 0 transitive binary clauses
c [cce-5] limit of 15000000 steps penalty 1 = 1 + 0
c [cce-5-1] incomplete large round (ACCE)
c [cce-5-1] allowing another 7500247 steps for small clauses
c [cce-5-1] scheduling 978 clauses = 629 binary + 349 ternary
c [cce-5-1] tried to eliminate 978 small clauses 100%
c [cce-5-1] eliminated 31 binary clauses 5%
c [cce-5-1] eliminated 31 small clauses 3%
c [cce-5-1] eliminated 31 small clauses in 8573473 steps
c [cce-5-1] completed small round (ACCE)
c [cce-5-1] eliminated 31 covered clauses in round 1
c [cce-5-2] incomplete large round (ACCE)
c [cce-5-2] allowing another 3213368 steps for small clauses
c [cce-5-2] scheduling 947 clauses = 598 binary + 349 ternary
c [cce-5-2] tried to eliminate 947 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 31 covered clauses in TOTAL during 2 rounds
c [cce-5] 31 < 1/100 * 13335 = 133 considered unsuccessful
c [elim-6] 27 variables 3% will be scheduled this time
c [elim-6] scheduled 27 variables 3%
c [elim-6] limit of 48365868 steps penalty 1 = 1 + 0
c [elim-6] rescheduling of touched variables disabled
c [elim-6-1] no variable eliminated in round 1 in 24419602 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 27 scheduled
c [bca-3] limit of 10000000 steps and 27096 added (scaled 2)
c [bca-3] 558 out of 1566 literals actually usable 36%
c [bca-3] added 0 blocked clauses in 31153 steps
c [sort-queue-7] sorted 155 enqueued variables after 67003 conflicts
c [score-dist-7] active 627 (80%), one 0 (0%), zero 155 (20%)
c [score-dist-7] max exp 518, different 15 (3%)
c [score-dist-7] median active exp 518, avg 516.0
c [simplification-7] removed 0 variables 0.0% (782 remain 35%)
c [simplification-7] removed 37 irredundant clauses 0.3% (13298 remain 44%)
c [simplification-7] maximum reduction of 0% = max (0%, 0%)
c [simplification-7] full geometric conflict interval increment 40000
c [simplification-7] new conflict interval 80000
c [simplification-7] penalized conflict interval 80000 = 1 * 80000
c [simplification-7] hard conflict limit 187003 (soft 147003 + delta 40000)
c [simplification-7] new conflict limit 147003 (hard 187003)
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 -   27.5     782    13298     94592   23634    398   193   16    22   14  75%    777    5   17   13  133%
c -   35.2     782    13298    130611   26841    401   193   13    15   14  84%    881   -3   13   14   93%
c -   40.7     782    13298    166396   28301    403   193   12    14    8  84%    941   -2   12   13   96%
c 
c [simplification-8] limit 147003 conflicts (hard 187003) hit after 187004 conflicts
c [quatres-6] found 3265 quaternary clauses 20% in total
c [quatres-6-1] added 2 double-self-subsuming ternary resolvents
c [quatres-6-2] added 4 single-self-subsuming ternary resolvents
c [quatres-6-2] added 76 quaternary resolvents
c [ternres-6] limit 15623331 with penalty 0 = 0 + 0
c [ternres-6] all 782 free variables schedulable
c [ternres-6] 12 ternary resolvents (0 bin, 12 trn)
c [ternres-6] fully completed ternary resolution
c [gauss-3] limit 781166 penalty 2 = 2 + 0
c [gauss-3] extracted 329 xors of average arity 5.7
c [gauss-3] connected 1871 occurrences of 42 variables (average 44.5)
c [gauss-3] limit 781166 penalty 2 = 2 + 0
c [gauss-3] fully completed
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [block-4] scheduling all variables this time
c [block-4] scheduled 782 variables 100%
c [block-4] limit of 39058328 steps penalty 2 = 2 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 0 blocked clauses
c [sweep-4] limit 1171749 penalty 2 = 2 + 0
c [sweep-4-1] 39 pos 35.8% + 70 neg 64.2% = 109 sched 13.9% ret 673
c [sweep-4-1] 1581933 steps 7 queries 42.14 avg class size
c [sweep-4-1] 314 decisions 6 SAT calls 42.50 avg env size
c [sweep-4-1] 98 variables remain 13% (684 retained 87%)
c [sweep-4-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-4] removed 0 vars in TOTAL (1 rounds, 6 queries)
c [sort-queue-8] sorted 151 enqueued variables after 187004 conflicts
c [score-dist-8] active 631 (81%), one 0 (0%), zero 151 (19%)
c [score-dist-8] max exp 519, different 15 (3%)
c [score-dist-8] median active exp 519, avg 517.3
c [simplification-8] removed 0 variables 0.0% (782 remain 35%)
c [simplification-8] removed 0 irredundant clauses 0.0% (13298 remain 44%)
c [simplification-8] maximum reduction of 0% = max (0%, 0%)
c [simplification-8] full geometric conflict interval increment 80000
c [simplification-8] new conflict interval 160000
c [simplification-8] penalized conflict interval 160000 = 1 * 160000
c [simplification-8] hard conflict limit 427004 (soft 347004 + delta 80000)
c [simplification-8] new conflict limit 347004 (hard 427004)
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 -   47.2     782    13298    200208   29776    423   193   16    21   10  76%    975    4   15   13  117%
c -   52.9     782    13298    234675   30061    424   193   13    15   10  85%    995   -2   13   13   99%
c -   59.4     782    13298    272646   31393    424   193   12    14   10  86%   1008   -1   13   13  103%
c -   66.8     782    13298    314484   33003    425   193   11    12   16  88%   1015   -2   10   12   83%
c 
c [simplification-9] limit 347004 conflicts (hard 427004) hit after 347510 conflicts
c [quatres-7] found 3384 quaternary clauses 19% in total
c [quatres-7-2] added 33 quaternary resolvents
c [ternres-7] limit 31075111 with penalty 0 = 0 + 0
c [ternres-7] all 782 free variables schedulable
c [ternres-7] 1 ternary resolvents (0 bin, 1 trn)
c [ternres-7] fully completed ternary resolution
c [simpleprobe-3] 116 schedulable variables 15%
c [simpleprobe-3] limit 31075111 penalty 2 = 2 + 0
c [simpleprobe-3] fully completed simple probing
c [simpleprobe-3] removed 0 variables, found 20 hbrs, 0 units
c [transred-6] limit 1000000 with penalty 1 = 1 + 0
c [transred-6] removed 10 transitive binary clauses
c [sort-queue-9] sorted 150 enqueued variables after 347510 conflicts
c [score-dist-9] active 632 (81%), one 0 (0%), zero 150 (19%)
c [score-dist-9] max exp 520, different 16 (3%)
c [score-dist-9] median active exp 520, avg 518.2
c [simplification-9] removed 0 variables 0.0% (782 remain 35%)
c [simplification-9] removed 0 irredundant clauses 0.0% (13298 remain 44%)
c [simplification-9] maximum reduction of 0% = max (0%, 0%)
c [simplification-9] full geometric conflict interval increment 160000
c [simplification-9] new conflict interval 320000
c [simplification-9] penalized conflict interval 320000 = 1 * 320000
c [simplification-9] hard conflict limit 827510 (soft 667510 + delta 160000)
c [simplification-9] new conflict limit 667510 (hard 827510)
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 -   75.1     782    13298    356307   33163    428   203   16    20   10  78%   1019    6   16   12  132%
c -   82.3     782    13298    391297   32520    433   203   14    18   11  78%   1021    1   14   14   99%
c -   89.1     782    13298    430123   34551    433   203   13    16   17  84%   1023   -1   14   13  107%
c -   96.9     782    13298    473078   35200    433   203   13    15   17  85%   1023   -0   13   13  102%
c -  104.9     782    13298    513281   37098    435   203   13    16   14  85%   1024   -1   14   13  100%
c -  112.5     782    13298    554224   38204    437   203   12    13   14  87%   1024   -2   11   13   83%
c -  119.9     782    13298    596611   39566    437   203   13    15   12  87%   1024   -0   14   13  110%
c -  128.2     782    13298    640988   39852    437   203   12    14   12  89%   1024   -0   12   12  100%
c 
c [simplification-10] limit 667510 conflicts (hard 827510) hit after 682157 conflicts
c [quatres-8] found 3490 quaternary clauses 16% in total
c [quatres-8-1] removed 1 duplicate quaternary clauses
c [quatres-8-2] added 1 single-self-subsuming ternary resolvents
c [quatres-8-2] added 30 quaternary resolvents
c [ternres-8] limit 67213534 with penalty 0 = 0 + 0
c [ternres-8] all 782 free variables schedulable
c [ternres-8] 0 ternary resolvents (0 bin, 0 trn)
c [ternres-8] fully completed ternary resolution
c [card-4] limit 4200845 penalty 3 = 3 + 0
c [card-4] found 1 at-most-one constraints of average size 3.0
c [card-4] found 1 at-most-two constraints of average size 4.0
c [card-4] using previous limit 4200845 for elimination
c [card-4] 2 out of 2 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [unhide-4] limit 1680338 with penalty 3 = 3 + 0
c [unhide-4-5] 0 units, 0 failed, 7 tauts, 0 hbrs, 5477 literals
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 3 transitive binary clauses
c [cce-6] limit of 84016918 steps penalty 2 = 2 + 0
c [cce-6-1] eliminated 3 clauses out of 598 (1%) of length 5
c [cce-6-1] eliminated 15 clauses out of 2013 (1%) of length 4
c [cce-6-1] completed large round (ATE)
c [cce-6-1] eliminated 18 large clauses in 24807860 steps
c [cce-6-1] allowing another 12403930 steps for small clauses
c [cce-6-1] scheduling 1041 clauses = 613 binary + 428 ternary
c [cce-6-1] tried to eliminate 1041 small clauses 100%
c [cce-6-1] eliminated 11 binary clauses 2%
c [cce-6-1] eliminated 11 small clauses 1%
c [cce-6-1] eliminated 11 small clauses in 13428353 steps
c [cce-6-1] completed small round (ATE)
c [cce-6-1] eliminated 29 covered clauses in round 1
c [cce-6-2] completed large round (ATE)
c [cce-6-2] allowing another 12391494 steps for small clauses
c [cce-6-2] scheduling 1030 clauses = 602 binary + 428 ternary
c [cce-6-2] tried to eliminate 1030 small clauses 100%
c [cce-6-2] completed small round (ATE)
c [cce-6-2] eliminated 0 covered clauses in round 2
c [cce-6] eliminated 29 covered clauses in TOTAL during 2 rounds
c [cce-6] 29 < 1/100 * 13298 = 132 considered unsuccessful
c [elim-7] scheduling all variables this time
c [elim-7] scheduled 782 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 187 variables 24% in round 1 in 45765636 steps
c [elim-7-1] backward subsumption/strengthening limit 45765600
c [elim-7-1-1] backward checking 342 touched variables 44%
c [elim-7-1-1] fully completed backward checking in 1 rounds
c [elim-7-1] subsumed 2 and strengthened 21 clauses in 674920 steps
c [elim-7-1] rescheduled 58 variables 7% by backward subsumption
c [elim-7-2] eliminated 3 variables 0% in round 2 in 17892150 steps
c [elim-7-2] backward subsumption/strengthening limit 17892100
c [elim-7-2-1] backward checking 7 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 87427 steps
c [elim-7] fully completed in 2 rounds
c [elim-7] transition to [ all 0 rem 0 ] state
c [elim-7] eliminated 190 = 24% variables out of 782 scheduled
c [sort-queue-10] sorted 102 enqueued variables after 682157 conflicts
c [score-dist-10] active 490 (83%), one 0 (0%), zero 102 (17%)
c [score-dist-10] max exp 521, different 16 (3%)
c [score-dist-10] median active exp 521, avg 519.2
c [simplification-10] removed 190 variables 24.3% (592 remain 27%)
c [simplification-10] removed 545 irredundant clauses 4.1% (12753 remain 42%)
c [simplification-10] maximum reduction of 24% = max (24%, 4%)
c [simplification-10] large reduction 24% >= 5% limit
c [simplification-10] next conflict interval 6821 = min (682157/100, 320000)
c [simplification-10] penalized conflict interval 6821 = 1 * 6821
c [simplification-10] hard conflict limit 698978 (soft 688978 + delta 10000)
c [simplification-10] new conflict limit 688978 (hard 698978)
c 
c [simplification-11] limit 688978 conflicts (hard 698978) hit after 688979 conflicts
c [quatres-9] found 3475 quaternary clauses 17% in total
c [quatres-9-1] removed 16 duplicate quaternary clauses
c [quatres-9-2] added 2 single-self-subsuming ternary resolvents
c [quatres-9-2] added 177 quaternary resolvents
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 0 transitive binary clauses
c [bca-4] limit of 10000000 steps and 26006 added (scaled 2)
c [bca-4] 281 out of 1186 literals actually usable 24%
c [bca-4] added 0 blocked clauses in 70588 steps
c [sort-queue-11] sorted 102 enqueued variables after 688979 conflicts
c [score-dist-11] active 490 (83%), one 0 (0%), zero 102 (17%)
c [score-dist-11] max exp 521, different 16 (3%)
c [score-dist-11] median active exp 521, avg 519.2
c [simplification-11] removed 0 variables 0.0% (592 remain 27%)
c [simplification-11] removed 0 irredundant clauses 0.0% (12753 remain 42%)
c [simplification-11] maximum reduction of 0% = max (0%, 0%)
c [simplification-11] full geometric conflict interval increment 320000
c [simplification-11] new conflict interval 640000
c [simplification-11] penalized conflict interval 640000 = 1 * 640000
c [simplification-11] hard conflict limit 1648979 (soft 1328979 + delta 320000)
c [simplification-11] new conflict limit 1328979 (hard 1648979)
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 -  141.1     592    12753    696055   39620    379    34   16    21   12  78%   1024    7   16   13  130%
c -  148.8     592    12753    738446   40200    382    34   13    15   12  84%   1024   -1   13   13   95%
c -  156.7     592    12753    781420   41083    385    34   14    17   13  79%   1024    1   13   13   99%
c -  165.8     592    12753    826695   41916    387    34   14    17   13  83%   1024    0   14   14  103%
c -  175.6     592    12753    878760   43637    387    34   13    15   13  87%   1024   -1   13   13   98%
c -  185.5     592    12753    930560   45099    387    34   13    15   13  87%   1024    0   14   13  108%
c -  195.8     592    12753    984029   45712    387    34   11    12   13  90%   1024   -2   10   12   83%
c -  206.8     592    12753   1039157   45080    388    34   10    12   20  89%   1024   -2   10   12   82%
c -  217.3     592    12753   1094204   45810    388    34   13    14   20  89%   1024    0   12   12   98%
c -  228.4     592    12753   1149670   45967    391    34   11    12   20  90%   1024   -1   10   12   81%
c -  239.7     592    12753   1203714   46645    392    34   12    14   20  88%   1024    1   12   12   99%
c -  251.1     592    12753   1258417   48411    392    34   11    13   10  90%   1024   -1   11   12   95%
c -  263.4     592    12753   1318624   49026    392    34   11    12   15  90%   1024   -0   12   11  102%
c 
c [simplification-12] limit 1328979 conflicts (hard 1648979) hit after 1366062 conflicts
c [quatres-10] found 3686 quaternary clauses 14% in total
c [quatres-10-1] removed 2 duplicate quaternary clauses
c [quatres-10-1] added 3 double-self-subsuming ternary resolvents
c [quatres-10-2] added 1 single-self-subsuming ternary resolvents
c [quatres-10-2] added 53 quaternary resolvents
c [ternres-9] limit 75724856 with penalty 1 = 1 + 0
c [ternres-9] all 592 free variables schedulable
c [ternres-9] 19 ternary resolvents (0 bin, 19 trn)
c [ternres-9] fully completed ternary resolution
c [gauss-4] limit 3786242 penalty 3 = 3 + 0
c [gauss-4] extracted 1381 xors of average arity 6.5
c [gauss-4] connected 9018 occurrences of 72 variables (average 125.2)
c [gauss-4] limit 3786242 penalty 3 = 3 + 0
c [gauss-4] fully completed
c [gauss-4] exported 0 unary, 0 binary and 0 ternary equations
c [treelook-3] limit 3786242 penalty 2 = 2 + 0 boost 1
c [treelook-3] scheduled 1184 literals 100%
c [treelook-3] scheduling used 299366 steps
c [treelook-3] scheduled completely
c [treelook-3] limit 3786242 penalty 2 = 2 + 0 boost 1
c [treelook-3] used 560458 steps
c [treelook-3] fully completed tree based probing
c [treelook-3] removed 0 variables, found 11 hbrs
c [block-5] scheduling all variables this time
c [block-5] scheduled 592 variables 100%
c [block-5] limit of 100000000 steps penalty 3 = 3 + 0
c [block-5] fully completed
c [block-5] transition to [ all 0 rem 0 ] state
c [block-5] eliminated 0 blocked clauses
c [elim-8] scheduling all variables this time
c [elim-8] scheduled 592 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 2 variables 0% in round 1 in 45315896 steps
c [elim-8-1] backward subsumption/strengthening limit 45315800
c [elim-8-1-1] backward checking 18 touched variables 3%
c [elim-8-1-1] fully completed backward checking in 1 rounds
c [elim-8-1] subsumed 0 and strengthened 0 clauses in 65914 steps
c [elim-8] fully completed in 1 rounds
c [elim-8] transition to [ all 0 rem 0 ] state
c [elim-8] eliminated 2 = 0% variables out of 592 scheduled
c [elim-8] 2 < 1/100 * 592 = 5 considered unsuccessful
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 56793641 penalty 3 = 3 + 0
c [sweep-5-1] 37 pos 41.6% + 52 neg 58.4% = 89 sched 15.1% ret 501
c [sweep-5-1] 8171540 steps 30 queries 10.07 avg class size
c [sweep-5-1] 1255 decisions 29 SAT calls 62.38 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] 255 pos 43.2% + 335 neg 56.8% = 590 sched 100.0% ret 0
c [sweep-5-2] 18912541 steps 49 queries 29.76 avg class size
c [sweep-5-2] 2522 decisions 48 SAT calls 83.15 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] 255 pos 43.2% + 335 neg 56.8% = 590 sched 100.0% ret 0
c [sweep-5-3] 23336359 steps 47 queries 29.74 avg class size
c [sweep-5-3] 2784 decisions 46 SAT calls 103.78 avg env size
c [sweep-5-3] fully completed sweeping round
c [sweep-5-3] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-5] removed 0 vars in TOTAL (3 rounds, 123 queries)
c [sort-queue-12] sorted 61 enqueued variables after 1366062 conflicts
c [score-dist-12] active 529 (90%), one 0 (0%), zero 61 (10%)
c [score-dist-12] max exp 522, different 10 (2%)
c [score-dist-12] median active exp 522, avg 521.6
c [simplification-12] removed 2 variables 0.3% (590 remain 27%)
c [simplification-12] removed 6 irredundant clauses 0.0% (12747 remain 42%)
c [simplification-12] maximum reduction of 0% = max (0%, 0%)
c [simplification-12] full geometric conflict interval increment 640000
c [simplification-12] conflict interval soft limit 1000000 reached
c [simplification-12] new conflict interval 1000000
c [simplification-12] penalized conflict interval 1000000 = 1 * 1000000
c [simplification-12] hard conflict limit 2866062 (soft 2366062 + delta 500000)
c [simplification-12] new conflict limit 2366062 (hard 2866062)
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 -  279.2     590    12747   1377881   49601    414    45   16    20   14  80%   1024    7   16   12  133%
c -  291.5     590    12747   1428899   50239    415    45   13    15   15  87%   1024   -1   12   13   92%
c -  303.3     590    12747   1483827   51488    415    45   13    14   24  88%   1024   -1   12   13   95%
c -  315.1     590    12747   1539496   52916    415    45   13    15   24  88%   1024    1   14   13  112%
c -  327.5     590    12747   1595705   54408    416    45   12    13   24  88%   1024   -1   12   12   98%
c -  339.5     590    12747   1652144   53721    416    45   11    12   24  90%   1024   -1   10   12   85%
c -  351.8     590    12747   1710506   56068    417    45   12    14   13  88%   1024    2   13   11  122%
c -  365.3     590    12747   1771690   55944    417    45   13    15   19  89%   1024    1   13   12  108%
c -  379.8     590    12747   1836342   57457    418    45   12    14   19  89%   1024    0   11   12   91%
c -  393.5     590    12747   1898813   57618    418    45   10    12   16  89%   1024   -2   13   12  114%
c -  407.8     590    12747   1963555   58128    419    45   12    13   16  91%   1024   -0   11   12   96%
c -  424.2     590    12747   2033808   58416    419    45   10    11   17  92%   1024   -2    9   11   82%
c -  441.1     590    12747   2104798   60142    419    45   11    13   17  89%   1024   -0   12   11  104%
c -  457.6     590    12747   2175843   61047    419    45   11    12   17  89%   1024   -0   12   11  106%
c -  475.2     590    12747   2251821   62208    419    45   10    11   17  91%   1024   -1   12   11  108%
c -  491.9     590    12747   2324223   63233    420    45    9    10   17  90%   1024   -1   10   10   98%
c 
c [simplification-13] limit 2366062 conflicts (hard 2866062) hit after 2366063 conflicts
c [quatres-11] found 3839 quaternary clauses 12% in total
c [quatres-11-2] added 2 single-self-subsuming ternary resolvents
c [quatres-11-2] added 39 quaternary resolvents
c [ternres-10] limit 200000000 with penalty 0 = 0 + 0
c [ternres-10] all 590 free variables schedulable
c [ternres-10] 9 ternary resolvents (0 bin, 9 trn)
c [ternres-10] fully completed ternary resolution
c [basicprobe-3] limit 400000000 penalty 0 = 0 + 0
c [basicprobe-3-0] 155 sched 26%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-3-0] fully completed probing
c [transred-9] limit 1000000 with penalty 1 = 1 + 0
c [transred-9] removed 0 transitive binary clauses
c [sort-queue-13] sorted 60 enqueued variables after 2366063 conflicts
c [score-dist-13] active 530 (90%), one 0 (0%), zero 60 (10%)
c [score-dist-13] max exp 523, different 11 (2%)
c [score-dist-13] median active exp 523, avg 522.3
c [simplification-13] removed 0 variables 0.0% (590 remain 27%)
c [simplification-13] removed 0 irredundant clauses 0.0% (12747 remain 42%)
c [simplification-13] maximum reduction of 0% = max (0%, 0%)
c [simplification-13] full geometric conflict interval increment 1000000
c [simplification-13] new conflict interval 2000000
c [simplification-13] penalized conflict interval 2000000 = 1 * 2000000
c [simplification-13] hard conflict limit 5366063 (soft 4366063 + delta 1000000)
c [simplification-13] new conflict limit 4366063 (hard 5366063)
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 -  511.0     590    12747   2391598   63842    432    45   16    20   15  79%   1024    6   16   12  133%
c -  527.1     590    12747   2455932   63353    433    45   13    15   26  87%   1024   -1   14   13  105%
c -  544.9     590    12747   2527458   64763    433    45   12    13   26  89%   1024   -1   11   13   88%
c -  562.3     590    12747   2600512   66550    434    45   12    14   26  89%   1024   -0   11   12   94%
c -  580.5     590    12747   2677372   68837    435    45   12    13   26  90%   1024   -0   12   12   98%
c -  599.9     590    12747   2754256   69266    436    45   11    13   26  90%   1024   -0   11   12   93%
c -  617.9     590    12747   2829281   69858    436    45   11    13   26  89%   1024   -0   11   11   95%
c -  637.6     590    12747   2909346   70954    437    45   10    11   26  91%   1024   -2    9   11   82%
c -  657.7     590    12747   2989931   71849    438    45   12    13   26  91%   1024    0   12   11  104%
c -  677.9     590    12747   3070940   72249    439    45   11    12   26  90%   1024   -0   11   11  100%
c -  699.5     590    12747   3155485   73543    440    45   12    14   26  86%   1024    2   12   10  114%
c -  719.3     590    12747   3231931   75068    440    45   11    12   27  89%   1024   -0   11   11   95%
c -  743.9     590    12747   3302604   75488    440    45   13    15   18  85%   1024   -0   12   13   88%
c -  764.9     590    12747   3380543   74914    440    45   13    14   28  87%   1024    0   13   12  106%
c -  788.3     590    12747   3468127   78111    440    45   12    14   28  89%   1024    0   13   12  108%
c -  812.8     590    12747   3557718   80660    440    45   11    12   28  91%   1024   -1   11   11   97%
c -  835.9     590    12747   3643450   79485    440    45   11    12   17  89%   1024   -0   13   11  112%
c -  860.1     590    12747   3730161   79615    440    45   11    12   17  89%   1024   -1   11   11   93%
c -  886.3     590    12747   3818777   80176    440    45   10    11   18  90%   1024   -1   10   11   94%
c -  914.8     590    12747   3916315   82092    440    45   10    10   18  92%   1024   -1    8   10   82%
c -  937.4     590    12747   4003869   83678    441    45   11    12   19  89%   1024   -1    9   11   81%
c -  960.5     590    12747   4091179   84514    441    45   12    14   19  89%   1024    1   13   12  109%
c -  986.0     590    12747   4185312   84029    441    45   10    11   19  92%   1024   -2    9   11   82%
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 (2 skipped), 116337 steps
c bkwd: tried 18965 clauses, 36984 lits, 1.95 lits/clause
c bkwd: checked 6435684 occs, 339.35 occs/clause, 174.01 occs/lit
c bkwd: subsumed 0 binary, 5 ternary, 211 large
c bkwd: strengthened 0 binary, 0 ternary (0% self), 1087 large (0% self)
c blkd: 5 bces, 968 removed, 1794221 resolutions, 2905883 steps
c blkd: 271 blocking literals 6%, 5 pure
c bump: 4244999 bumped seen, 225380829 lits 53.1 on average
c card: 4 count, 0 units, 0 am1, 2878670 steps
c card: 1 rescheduled, 3 eliminated, 1975 resolved, 86 subsumed
c card: 1 at-most-one constraints found, average size 3.00
c card: 1 at-most-one constraints used 100%, average size 3.00
c card: 2 at-most-two constraints found, average size 4.00
c card: 2 at-most-two constraints used 100%, average size 4.00
c cces: 6 cces, 4096 eliminated, 4005 ate 98%, 91 abce 2%
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: 208916 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 56 gcs, 0 rescored clauses, 0 rescored vars
c dcps: 32 decompositions, 159 equivalent 7%
c deco: 0 decision-only clauses 0%, 0% reduction
c decs: 4661725 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 8 elims, 1448 eliminated 63%, 4 pure 0%
c elms: 20 rounds, 2.5 rounds/bve
c elms: 1439 small 99%, 0 large 0%
c elms: 5633 tried small, 1439 succeeded 26%, 4194 failed 74%
c elms: 1096 subsumed, 1995 strengthened, 24 blocked
c elms: 605991 copies, 2829350 resolutions, 472409 ipos
c elms: 382295 subchks, 491501 strchks
c gaus: 4 extractions, 2945 extracted, 6.2 size, 7 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 15135050 steps, 7567525 extr 50%, 28892 elim 0%
c glue: 12.0 orig avg, 12.0 real avg, 3.2 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 484 = 261 simple 54% + 193 trn 40% + 30 lrg 6%, 20 sub 4%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 4244999 clauses, 20.6 length
c lrnd: 87466926 lits = 141913933 orig - 54447007 removed 38%
c lrnd: 399006 uips 9%, 3741646 flips 88%
c mins: 4237785 mins 100%, 8 bin 0%, 7206 size 0%
c mins: 48675298 poisoned searches, 5879733 hits, 12% hit rate
c mins: 180412776 used twice searches, 24465915 hits, 14% hit rate
c move: moved 338, 273 bin 81%, 65 trn 19%
c otfs: 1891 driving 18%, 8423 restarting 82%
c otfs: str 10314, 10174 red 99%, 140 irr 1%
c otfs: str 10314, 0 bin 0%, 1 trn 0%, 10313 lrg 100%
c otfs: sub 128, 109 red 85%, 19 irr 15%
c otfs: sub 128, 0 bin 0%, 0 trn 0%, 128 lrg 100%
c phas: 1 computed, 1683 set, 0 pos (0%), 1683 neg (100%)
c prbs: 3 basic, 11583 probed, 17 failed, 0 lifted
c prbs: 3 simple, 4499 probed, 0 failed, 0 eqs
c prbs: 3 treelook, 1360 probed, 0 failed, 0 lifted
c prom: 648537 locked 9% out of 7284420 tried
c prps: 334445278 props, 72 props/dec
c prps: 100% srch, 0% simp, 0% lkhd
c quat: 11 count, 1207 quat, 80 self1, 26 self2, 116 dup
c queu: 13 sorted, 4661725 next (2532 steps 0.00)
c queu: 225386522 enq (669358941 steps 2.97), 225380829 deq 100%
c redc: 575 clauses 0%, 167744 tried 4%, 0 sat 0%
c redc: 620 lits 0%, 2124582 tried 1%, 0 sat 0%
c redc: 3 times jump level reduced, 10.3 levels on average
c reds: 68 count, 62382.6 conflicts per reduce
c reds: 0 memlim 0%, 68 arith 100%
c reds: 2839051 collected 92%, 259048 retired 8%
c rmbd: 24 removed, 24 red 100%
c rsts: 11467 restarts 82%, 2528 skipped 18%
c rsts: 2528 saturating 100%, 0 reuse 0%
c rsts: 0 kept 0.0% average 0.0%
c scnc: 0 count, 1.000 min (0/1000), 1.000 max (0/1000)
c simp: 13 count, 13 confs 100%, 0 vars 0%
c simp: 0 its 0%, 0 bin 0%, 0 trns 0%
c subl: 4244999 count (2447019 tried 0.6), 1011034 sub out of 4244786 (23.8%)
c swps: 5 count, 8 rounds, 275 queries (34.4/round)
c swps: 276 sat calls, 1 unsat (17.7% success rate)
c swps: 10491 decisions 38.0, 4875 conflicts 17.7
c swps; 37.5 avg class size, 56.4 avg environment size
c swps: 0 failed, 1 impls, 0 equivs
c swp0: 90 type 0 queries, 6 unsat (6.7%), 90 sat (100.0%)
c swp1: 185 type 1 queries, 18 unsat (9.7%), 185 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: 17813726 calls to obtain time
c tops: 88 fixed 4%, 1 its, 4242015.00 confs/it
c trds: 9 transitive reductions, 63 removed, 0 failed
c trds: 13947 nodes, 7518 edges, 54118 steps
c trim: 3550390 words, 13.5 MB
c trnr: 10 count, 1 bin, 264 trn, 10721388 steps
c unhd: 4 count, 5 rounds, 3239277 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: 5215 tauts, 0 bin 0%, 18 trn 0%, 5165 lrg 99%
c unhd: 5215 tauts, 32 stamp 1%, 51 red 1%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 18030 str, 0 bin 0%, 19 trn 0%, 18011 lrg 100%, 8740 red 48%
c vars: 599 remaining 26% and 1695 removed 74% out of 2294
c vars: 88 fixed 4%, 1448 eliminated 63%, 159 equivalent 7%
c vsts: 64378203119 visits, 100% srch, 0% simp, 0% lkhd
c vsts: 192.6 search visits per propagation, 15163.1 per conflict
c wchs: 18417024825 pushed, 5776900 enlarged, 116 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all        4245993       2839051        259048     123132321      42678541       2552769
c 
c  0 0         36939   1      3215   0         0   0  83751293  68  22850718  54   1349443  53     1.4
c  1 5         47889   1     30576   1      8782   3  14764485  12<  5904509  14<   400243  16<    0.4
c  2 6        479041  11    329824  12     66627  26  18154459  15   8716117  20    611166  24     2.3
c  3 9       2418326  57<  1591154  56<   140925  54<  5030975   4   3890895   9    165667   6     6.5
c  4 14      1192432  28    833239  29     34930  13   1353040   1   1250641   3     24902   1     3.2
c  5 21        71321   2     51031   2      7782   3     78017   0     65634   0      1347   0     1.7
c  6 30           45   0        12   0         2   0        52   0        27   0         1   0     0.0
c 
c avg                  3.2           3.2           2.9           0.6           0.9           0.9
c std                  0.7           0.7           0.8           1.0           1.2           1.1
c 
c   13.203   1% bump
c    2.849   0% elim
c    2.584   0% decide
c 
c    3.333 < 1% rest (below)
c 
c    1.868   0% sweep
c    1.657   0% cce
c    0.439   0% probe
c    0.427   0% unhide
c    0.290   0% quatres
c    0.204   0% block
c    0.155   0% gauss
c    0.058   0% bca
c    0.050   0% ternres
c    0.044   0% card
c    0.009   0% transred
c    0.000   0% locs
c    0.000   0% queuesort
c    0.000   0% rescore
c ==================================
c    0.390   0% preprocessing     5%
c    8.119   1% inprocessing     95%
c ==================================
c    8.509   1% simplifying
c  991.563  99% search
c ==================================
c 1000.072 100% all
c 
c       4242015 conflicts,        4241.7 confs/sec
c           172 ternaries,       24662.9 confs/ternary
c             6 binaries,       707002.5 confs/binary
c             1 iterations,    4242015.0 confs/iteration
c 
c            68 reductions,          0.1 redus/sec,  62382.6 confs/reduction
c         11467 restarts,           11.5 rests/sec,    369.9 confs/restart
c       4661725 decisions,        4661.4 decis/sec,      1.1 decis/conflict
c     334445278 propagations,   334421.1 props/sec,     71.7 props/decision
c 
c 1000.1 seconds, 48.0 MB
c
c CAUGHT SIGNAL 15 SIGTERM
c
c launch: done
