c launch: /data/cnf/sc2014/app/stable-300-0.1-20-98765432130020.cnf.bz2
c host: atom11
c Lingeling SAT Solver
c 
c Version b7ztzvv 37b745a123cb37a24a48e992b1e2073d5d4068bb
c 
c Copyright (C) 2010-2014 Armin Biere JKU Linz Austria.
c All rights reserved.
c 
c released Sat May  2 12:17:55 CEST 2015
c compiled Sat May  2 12:17:55 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 fmvx1 3.13.0-51-generic x86_64
c 
c piping '/data/cnf/sc2014/app/stable-300-0.1-20-98765432130020.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/stable-300-0.1-20-98765432130020.cnf.bz2
c no embedded options
c found 'p cnf 300 17540' header
c read 300 variables, 17540 clauses, 282050 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 --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 300 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 
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     300    17540         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] found 260 at-most-one constraints of average size 4.0
c [card-1] no at-most-two constraint found
c [card-1] using previous limit 2000000 for elimination
c [card-1] 260 out of 260 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [simpleprobe-1] all 300 free variables schedulable
c [simpleprobe-1] boosting simple probing limit by 10
c [simpleprobe-1] limit 20000000 penalty 0 = 0 + 0
c [simpleprobe-1] 11 variables remain 4% (289 retained 96%)
c [unhide-1] limit 100000 with penalty 0 = 0 + 0
c [unhide-1-1] 0 units, 0 failed, 0 tauts, 0 hbrs, 1734 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 300 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] no variable eliminated in round 1 in 0 steps
c [elim-1] fully completed in 1 rounds
c [elim-1] transition to [ all 0 rem 0 ] state
c [elim-1] eliminated 0 = 0% variables out of 300 scheduled
c [phase-count-1] 16797 negative 98.2% of 17097 except 300 1.8%
c [phase-count-1] 8477 positive 49.6% of 17097 except 8620 50.4%
c [phase-count-1] less non-negative clauses 300 than limit 1700 (10.0%)
c [phase-count-1] non-pos/non-neg = 8620/300 = 28.73 >= 2.00 = 200/100
c [lucky-phase-1] forcing lucky phase -1
c [phase-1] phase bias: 0 positive 0%, 300 negative 100%
c [sort-queue-1] sorted 300 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 300 (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 0 variables 0.0% (300 remain 100%)
c [simplification-1] removed 443 irredundant clauses 2.5% (17097 remain 97%)
c [simplification-1] maximum reduction of 3% = max (0%, 3%)
c [simplification-1] geometric conflict interval increment 5000 = 20000 / 4
c [simplification-1] new conflict interval 5000
c [simplification-1] penalized conflict interval 5000 = 1 * 5000
c [simplification-1] hard conflict limit 15000 (soft 5000 + delta 10000)
c [simplification-1] new conflict limit 5000 (hard 15000)
c 
c [simplification-2] limit 5000 conflicts (hard 15000) hit after 5000 conflicts
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 600 literals 100%
c [treelook-1] scheduling used 57867 steps
c [treelook-1] scheduled completely
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 422553 steps
c [treelook-1] 597 literals remain 100%
c [treelook-1] 300 variables remain to probed next time 100%
c [basicprobe-1] limit 1000000 penalty 0 = 0 + 0
c [basicprobe-1-0] 300 sched 100%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-1-0] fully completed probing
c [block-1] scheduling all variables this time
c [block-1] scheduled 300 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 0 blocked clauses
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 30 clauses out of 31 (97%) of length 49
c [cce-1-1] eliminated 1 clauses out of 1 (100%) of length 48
c [cce-1-1] eliminated 24 clauses out of 25 (96%) of length 46
c [cce-1-1] eliminated 3 clauses out of 3 (100%) of length 45
c [cce-1-1] eliminated 21 clauses out of 22 (95%) of length 44
c [cce-1-1] eliminated 54 clauses out of 56 (96%) of length 43
c [cce-1-1] eliminated 22 clauses out of 23 (96%) of length 42
c [cce-1-1] eliminated 100 clauses out of 104 (96%) of length 41
c [cce-1-1] eliminated 158 clauses out of 164 (96%) of length 40
c [cce-1-1] eliminated 227 clauses out of 236 (96%) of length 39
c [cce-1-1] eliminated 264 clauses out of 273 (97%) of length 38
c [cce-1-1] eliminated 379 clauses out of 396 (96%) of length 37
c [cce-1-1] eliminated 5 clauses out of 394 (1%) of length 36
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 1288 large clauses in 30000315 steps
c [cce-1-1] allowing another 15000157 steps for small clauses
c [cce-1-1] scheduling 8620 clauses = 8620 binary + 0 ternary
c [cce-1-1] tried to eliminate 339 small clauses 4%
c [cce-1-1] eliminated 193 binary clauses 2%
c [cce-1-1] eliminated 193 small clauses 2%
c [cce-1-1] eliminated 193 small clauses in 30000041 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 1481 covered clauses in round 1
c [cce-1] eliminated 1481 covered clauses in TOTAL during 1 rounds
c [bca-1] limit of 10000000 steps and 31732 added (scaled 2)
c [bca-1] 0 out of 602 literals actually usable 0%
c [bca-1] not enough literals usable
c [bca-1] added 0 blocked clauses in 4641 steps
c [sweep-1] limit 1000000 penalty 0 = 0 + 0
c [sweep-1-1] 12 pos 4.0% + 288 neg 96.0% = 300 sched 100.0% ret 0
c [sweep-1-1] 1020755 steps 25 queries 22.76 avg class size
c [sweep-1-1] 2397 decisions 24 SAT calls 290.71 avg env size
c [sweep-1-1] 4 variables remain 1% (296 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, 24 queries)
c [sort-queue-2] sorted 300 enqueued variables after 5000 conflicts
c [score-dist-2] active 0 (0%), one 300 (100%), zero 0 (0%)
c [score-dist-2] max exp 1, different 1 (50%)
c [score-dist-2] median active exp 0, avg 0.0
c [simplification-2] removed 0 variables 0.0% (300 remain 100%)
c [simplification-2] removed 1481 irredundant clauses 8.7% (15616 remain 89%)
c [simplification-2] maximum reduction of 9% = max (0%, 9%)
c [simplification-2] geometric conflict interval increment 2000 = 20000 / 10
c [simplification-2] new conflict interval 7000
c [simplification-2] penalized conflict interval 7000 = 1 * 7000
c [simplification-2] hard conflict limit 22000 (soft 12000 + delta 10000)
c [simplification-2] new conflict limit 12000 (hard 22000)
c 
c [simplification-3] limit 12000 conflicts (hard 22000) hit after 12001 conflicts
c [quatres-1] found 0 quaternary clauses 0% in total
c [ternres-1] boosting ternary resolution limit by 5
c [ternres-1] limit 20000000 with penalty 0 = 0 + 0
c [ternres-1] all 300 free variables schedulable
c [ternres-1] 0 ternary resolvents (0 bin, 0 trn)
c [ternres-1] fully completed ternary resolution
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 115 at-most-one constraints of average size 4.0
c [card-2] no at-most-two constraint found
c [card-2] using previous limit 1000000 for elimination
c [card-2] 115 out of 115 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 0 xors of average arity 0.0
c [gauss-1] exported 0 unary, 0 binary and 0 ternary equations
c [simpleprobe-2] 11 schedulable variables 4%
c [simpleprobe-2] limit 1000000 penalty 1 = 1 + 0
c [simpleprobe-2] 11 variables remain 4% (289 retained 96%)
c [unhide-2] limit 50000 with penalty 1 = 1 + 0
c [unhide-2-2] 0 units, 0 failed, 0 tauts, 0 hbrs, 8185 literals
c [transred-1] limit 376443 with penalty 0 = 0 + 0
c [transred-1] removed 0 transitive binary clauses
c [cce-2] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-2-1] eliminated 308 clauses out of 333 (92%) of length 36
c [cce-2-1] eliminated 332 clauses out of 359 (92%) of length 35
c [cce-2-1] eliminated 425 clauses out of 447 (95%) of length 34
c [cce-2-1] eliminated 428 clauses out of 546 (78%) of length 33
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] eliminated 1493 large clauses in 30000135 steps
c [cce-2-1] allowing another 15000067 steps for small clauses
c [cce-2-1] scheduling 8427 clauses = 8427 binary + 0 ternary
c [cce-2-1] tried to eliminate 352 small clauses 4%
c [cce-2-1] eliminated 127 binary clauses 2%
c [cce-2-1] eliminated 127 small clauses 2%
c [cce-2-1] eliminated 127 small clauses in 30000022 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 1620 covered clauses in round 1
c [cce-2] eliminated 1620 covered clauses in TOTAL during 1 rounds
c [elim-2] scheduling all variables this time
c [elim-2] scheduled 300 variables 100%
c [elim-2] limit of 10000000 steps penalty 1 = 1 + 0
c [elim-2] rescheduling of touched variables disabled
c [elim-2-1] no variable eliminated in round 1 in 0 steps
c [elim-2] fully completed in 1 rounds
c [elim-2] transition to [ all 0 rem 0 ] state
c [elim-2] eliminated 0 = 0% variables out of 300 scheduled
c [sweep-2] limit 1000000 penalty 0 = 0 + 0
c [sweep-2-1] 0 pos 0.0% + 4 neg 100.0% = 4 sched 1.3% ret 296
c [sweep-2-1] 230463 steps 4 queries 2.25 avg class size
c [sweep-2-1] 300 decisions 3 SAT calls 298.00 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] 11 pos 3.7% + 289 neg 96.3% = 300 sched 100.0% ret 0
c [sweep-2-2] 791394 steps 15 queries 32.93 avg class size
c [sweep-2-2] 1400 decisions 14 SAT calls 297.71 avg env size
c [sweep-2-2] 99 variables remain 33% (201 retained 67%)
c [sweep-2-2] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-2] removed 0 vars in TOTAL (2 rounds, 17 queries)
c [sort-queue-3] sorted 300 enqueued variables after 12001 conflicts
c [score-dist-3] active 0 (0%), one 300 (100%), zero 0 (0%)
c [score-dist-3] max exp 1, different 1 (50%)
c [score-dist-3] median active exp 0, avg 0.0
c [simplification-3] removed 0 variables 0.0% (300 remain 100%)
c [simplification-3] removed 1620 irredundant clauses 10.4% (13996 remain 80%)
c [simplification-3] maximum reduction of 10% = max (0%, 10%)
c [simplification-3] geometric conflict interval increment 1818 = 20000 / 11
c [simplification-3] new conflict interval 8818
c [simplification-3] penalized conflict interval 8818 = 1 * 8818
c [simplification-3] hard conflict limit 30819 (soft 20819 + delta 10000)
c [simplification-3] new conflict limit 20819 (hard 30819)
c 
c [simplification-4] limit 20819 conflicts (hard 30819) hit after 20820 conflicts
c [block-2] scheduling all variables this time
c [block-2] scheduled 300 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 [cce-3] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-3-1] eliminated 74 clauses out of 107 (69%) of length 33
c [cce-3-1] eliminated 437 clauses out of 475 (92%) of length 32
c [cce-3-1] eliminated 464 clauses out of 499 (93%) of length 31
c [cce-3-1] eliminated 592 clauses out of 654 (91%) of length 30
c [cce-3-1] eliminated 341 clauses out of 598 (57%) of length 29
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 1908 large clauses in 30000039 steps
c [cce-3-1] allowing another 15000019 steps for small clauses
c [cce-3-1] scheduling 8300 clauses = 8300 binary + 0 ternary
c [cce-3-1] tried to eliminate 518 small clauses 6%
c [cce-3-1] eliminated 98 binary clauses 1%
c [cce-3-1] eliminated 98 small clauses 1%
c [cce-3-1] eliminated 98 small clauses in 30000286 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 2006 covered clauses in round 1
c [cce-3] eliminated 2006 covered clauses in TOTAL during 1 rounds
c [bca-2] limit of 10000000 steps and 24480 added (scaled 2)
c [bca-2] 0 out of 602 literals actually usable 0%
c [bca-2] not enough literals usable
c [bca-2] added 0 blocked clauses in 20046 steps
c [sort-queue-4] sorted 300 enqueued variables after 20820 conflicts
c [score-dist-4] active 0 (0%), one 300 (100%), zero 0 (0%)
c [score-dist-4] max exp 1, different 1 (50%)
c [score-dist-4] median active exp 0, avg 0.0
c [simplification-4] removed 0 variables 0.0% (300 remain 100%)
c [simplification-4] removed 2006 irredundant clauses 14.3% (11990 remain 68%)
c [simplification-4] maximum reduction of 14% = max (0%, 14%)
c [simplification-4] geometric conflict interval increment 1333 = 20000 / 15
c [simplification-4] new conflict interval 10151
c [simplification-4] penalized conflict interval 10151 = 1 * 10151
c [simplification-4] hard conflict limit 40971 (soft 30971 + delta 10000)
c [simplification-4] new conflict limit 30971 (hard 40971)
c 
c [simplification-5] limit 30971 conflicts (hard 40971) hit after 30971 conflicts
c [quatres-2] found 0 quaternary clauses 0% in total
c [ternres-2] limit 2000000 with penalty 1 = 1 + 0
c [ternres-2] all 300 free variables schedulable
c [ternres-2] 0 ternary resolvents (0 bin, 0 trn)
c [ternres-2] fully completed ternary resolution
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] extracted 0 xors of average arity 0.0
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 600 literals 100%
c [treelook-2] scheduling used 115754 steps
c [treelook-2] scheduled completely
c [treelook-2] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-2] used 214978 steps
c [treelook-2] 596 literals remain 99%
c [treelook-2] 300 variables remain to probed next time 100%
c [transred-2] limit 688986 with penalty 1 = 1 + 0
c [transred-2] removed 0 transitive binary clauses
c [cce-4] boosting limit by 10
c [cce-4] limit of 300000000 steps penalty 0 = 0 + 0
c [cce-4-1] eliminated 175 clauses out of 234 (75%) of length 29
c [cce-4-1] eliminated 423 clauses out of 486 (87%) of length 28
c [cce-4-1] eliminated 430 clauses out of 492 (87%) of length 27
c [cce-4-1] eliminated 463 clauses out of 547 (85%) of length 26
c [cce-4-1] eliminated 291 clauses out of 343 (85%) of length 25
c [cce-4-1] eliminated 244 clauses out of 294 (83%) of length 24
c [cce-4-1] eliminated 189 clauses out of 233 (81%) of length 23
c [cce-4-1] eliminated 224 clauses out of 262 (85%) of length 22
c [cce-4-1] eliminated 159 clauses out of 183 (87%) of length 21
c [cce-4-1] eliminated 98 clauses out of 118 (83%) of length 20
c [cce-4-1] eliminated 84 clauses out of 106 (79%) of length 19
c [cce-4-1] eliminated 72 clauses out of 77 (94%) of length 18
c [cce-4-1] eliminated 40 clauses out of 46 (87%) of length 17
c [cce-4-1] eliminated 17 clauses out of 21 (81%) of length 16
c [cce-4-1] eliminated 21 clauses out of 26 (81%) of length 15
c [cce-4-1] eliminated 12 clauses out of 14 (86%) of length 14
c [cce-4-1] eliminated 9 clauses out of 11 (82%) of length 13
c [cce-4-1] eliminated 3 clauses out of 5 (60%) of length 12
c [cce-4-1] eliminated 4 clauses out of 4 (100%) of length 11
c [cce-4-1] eliminated 1 clauses out of 1 (100%) of length 10
c [cce-4-1] completed large round (ATE)
c [cce-4-1] eliminated 2959 large clauses in 29186143 steps
c [cce-4-1] allowing another 14593071 steps for small clauses
c [cce-4-1] scheduling 8202 clauses = 8202 binary + 0 ternary
c [cce-4-1] tried to eliminate 8202 small clauses 100%
c [cce-4-1] eliminated 69 binary clauses 1%
c [cce-4-1] eliminated 69 small clauses 1%
c [cce-4-1] eliminated 69 small clauses in 79327141 steps
c [cce-4-1] completed small round (ATE)
c [cce-4-1] completed small and large (ATE)
c [cce-4-1] eliminated 3028 covered clauses in round 1
c [cce-4-2] completed large round (ATE)
c [cce-4-2] allowing another 2228047 steps for small clauses
c [cce-4-2] scheduling 8133 clauses = 8133 binary + 0 ternary
c [cce-4-2] tried to eliminate 8133 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 3028 covered clauses in TOTAL during 2 rounds
c [sweep-3] limit 500000 penalty 1 = 1 + 0
c [sweep-3-1] 6 pos 6.1% + 93 neg 93.9% = 99 sched 33.0% ret 201
c [sweep-3-1] 608472 steps 5 queries 21.40 avg class size
c [sweep-3-1] 400 decisions 4 SAT calls 298.00 avg env size
c [sweep-3-1] 87 variables remain 29% (213 retained 71%)
c [sweep-3-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-3] removed 0 vars in TOTAL (1 rounds, 4 queries)
c [sort-queue-5] sorted 300 enqueued variables after 30971 conflicts
c [score-dist-5] active 0 (0%), one 300 (100%), zero 0 (0%)
c [score-dist-5] max exp 1, different 1 (50%)
c [score-dist-5] median active exp 0, avg 0.0
c [simplification-5] removed 0 variables 0.0% (300 remain 100%)
c [simplification-5] removed 3028 irredundant clauses 25.3% (8962 remain 51%)
c [simplification-5] maximum reduction of 25% = max (0%, 25%)
c [simplification-5] geometric conflict interval increment 769 = 20000 / 26
c [simplification-5] new conflict interval 10920
c [simplification-5] penalized conflict interval 10920 = 1 * 10920
c [simplification-5] hard conflict limit 51891 (soft 41891 + delta 10000)
c [simplification-5] new conflict limit 41891 (hard 51891)
c 
c [simplification-6] limit 41891 conflicts (hard 51891) hit after 41891 conflicts
c [card-3] limit 500000 penalty 2 = 2 + 0
c [card-3] found 35 at-most-one constraints of average size 4.1
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 500000 for elimination
c [card-3] 35 out of 35 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [unhide-3] limit 110190 with penalty 2 = 2 + 0
c [unhide-3-3] 0 units, 0 failed, 0 tauts, 0 hbrs, 25349 literals
c [cce-5] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-5-1] completed large round (ACCE)
c [cce-5-1] allowing another 2247128 steps for small clauses
c [cce-5-1] scheduling 8133 clauses = 8133 binary + 0 ternary
c [cce-5-1] tried to eliminate 3520 small clauses 43%
c [cce-5-1] incomplete small round (ACCE)
c [cce-5-1] eliminated 0 covered clauses in round 1
c [cce-5] eliminated 0 covered clauses in TOTAL during 1 rounds
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 300 variables 100%
c [elim-3] limit of 11019004 steps penalty 2 = 2 + 0
c [elim-3] rescheduling of touched variables disabled
c [elim-3-1] no variable eliminated in round 1 in 898128 steps
c [elim-3] fully completed in 1 rounds
c [elim-3] transition to [ all 0 rem 0 ] state
c [elim-3] eliminated 0 = 0% variables out of 300 scheduled
c [sort-queue-6] sorted 300 enqueued variables after 41891 conflicts
c [score-dist-6] active 0 (0%), one 300 (100%), zero 0 (0%)
c [score-dist-6] max exp 1, different 1 (50%)
c [score-dist-6] median active exp 0, avg 0.0
c [simplification-6] removed 0 variables 0.0% (300 remain 100%)
c [simplification-6] removed 0 irredundant clauses 0.0% (8962 remain 51%)
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 30920
c [simplification-6] penalized conflict interval 30920 = 1 * 30920
c [simplification-6] hard conflict limit 88271 (soft 72811 + delta 15460)
c [simplification-6] new conflict limit 72811 (hard 88271)
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 -   20.0     300     8962     52338   12739      0   487   43    80    7  54%    556   40   42   22  191%
c 
c [simplification-7] limit 72811 conflicts (hard 88271) hit after 72813 conflicts
c [basicprobe-2] limit 10258825 penalty 1 = 1 + 0
c [basicprobe-2-0] 300 sched 100%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-2-0] fully completed probing
c [block-3] scheduling all variables this time
c [block-3] scheduled 300 variables 100%
c [block-3] limit of 12500000 steps penalty 2 = 2 + 0
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 0 blocked clauses
c [bca-3] limit of 10000000 steps and 18424 added (scaled 2)
c [bca-3] 0 out of 602 literals actually usable 0%
c [bca-3] not enough literals usable
c [bca-3] added 0 blocked clauses in 31711 steps
c [sort-queue-7] sorted 300 enqueued variables after 72813 conflicts
c [score-dist-7] active 0 (0%), one 300 (100%), zero 0 (0%)
c [score-dist-7] max exp 1, different 1 (50%)
c [score-dist-7] median active exp 0, avg 0.0
c [simplification-7] removed 0 variables 0.0% (300 remain 100%)
c [simplification-7] removed 0 irredundant clauses 0.0% (8962 remain 51%)
c [simplification-7] maximum reduction of 0% = max (0%, 0%)
c [simplification-7] full geometric conflict interval increment 30920
c [simplification-7] new conflict interval 61840
c [simplification-7] penalized conflict interval 61840 = 1 * 61840
c [simplification-7] hard conflict limit 165573 (soft 134653 + delta 30920)
c [simplification-7] new conflict limit 134653 (hard 165573)
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 -   29.7     300     8962     93872   20126      0   487   45    78    8  58%    776   24   49   31  161%
c -   36.6     300     8962    129724   22864      0   487   24    36    9  67%    880  -15   23   30   77%
c 
c [simplification-8] limit 134653 conflicts (hard 165573) hit after 148715 conflicts
c [quatres-3] found 1 quaternary clauses 0% in total
c [ternres-3] limit 2157186 with penalty 2 = 2 + 0
c [ternres-3] all 300 free variables schedulable
c [ternres-3] 0 ternary resolvents (0 bin, 0 trn)
c [ternres-3] fully completed ternary resolution
c [gauss-3] limit 500000 penalty 2 = 2 + 0
c [gauss-3] extracted 0 xors of average arity 0.0
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [transred-3] limit 500000 with penalty 2 = 2 + 0
c [transred-3] removed 0 transitive binary clauses
c [cce-6] limit of 21571864 steps penalty 1 = 1 + 0
c [cce-6-1] completed large round (ATE)
c [cce-6-1] allowing another 2095208 steps for small clauses
c [cce-6-1] scheduling 8133 clauses = 8133 binary + 0 ternary
c [cce-6-1] tried to eliminate 2530 small clauses 31%
c [cce-6-1] incomplete small round (ATE)
c [cce-6-1] eliminated 0 covered clauses in round 1
c [cce-6] eliminated 0 covered clauses in TOTAL during 1 rounds
c [sweep-4] limit 647155 penalty 2 = 2 + 0
c [sweep-4-1] 1 pos 1.1% + 86 neg 98.9% = 87 sched 29.0% ret 213
c [sweep-4-1] 655531 steps 7 queries 24.57 avg class size
c [sweep-4-1] 600 decisions 6 SAT calls 297.83 avg env size
c [sweep-4-1] 64 variables remain 21% (236 retained 79%)
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 300 enqueued variables after 148715 conflicts
c [score-dist-8] active 0 (0%), one 300 (100%), zero 0 (0%)
c [score-dist-8] max exp 1, different 1 (50%)
c [score-dist-8] median active exp 0, avg 0.0
c [simplification-8] removed 0 variables 0.0% (300 remain 100%)
c [simplification-8] removed 0 irredundant clauses 0.0% (8962 remain 51%)
c [simplification-8] maximum reduction of 0% = max (0%, 0%)
c [simplification-8] full geometric conflict interval increment 61840
c [simplification-8] new conflict interval 123680
c [simplification-8] penalized conflict interval 123680 = 1 * 123680
c [simplification-8] hard conflict limit 334235 (soft 272395 + delta 61840)
c [simplification-8] new conflict limit 272395 (hard 334235)
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 -   43.9     300     8962    163588   22346      0   487   43    71    9  60%    938   20   53   31  169%
c -   50.8     300     8962    199822   23491      0   487   23    33    7  68%    975  -13   25   28   87%
c -   58.3     300     8962    235091   23387      0   487   28    42    6  67%    995   -8   28   31   90%
c -   66.5     300     8962    271409   23632      0   487   40    64    9  63%   1007   10   35   34  102%
c 
c [simplification-9] limit 272395 conflicts (hard 334235) hit after 272399 conflicts
c [sort-queue-9] sorted 300 enqueued variables after 272399 conflicts
c [score-dist-9] active 0 (0%), one 300 (100%), zero 0 (0%)
c [score-dist-9] max exp 1, different 1 (50%)
c [score-dist-9] median active exp 0, avg 0.0
c [simplification-9] removed 0 variables 0.0% (300 remain 100%)
c [simplification-9] removed 0 irredundant clauses 0.0% (8962 remain 51%)
c [simplification-9] maximum reduction of 0% = max (0%, 0%)
c [simplification-9] full geometric conflict interval increment 123680
c [simplification-9] new conflict interval 247360
c [simplification-9] penalized conflict interval 247360 = 1 * 247360
c [simplification-9] hard conflict limit 643439 (soft 519759 + delta 123680)
c [simplification-9] new conflict limit 519759 (hard 643439)
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 -   73.8     300     8962    308996   24948      0   487   39    62    7  63%   1015   13   47   32  148%
c -   82.2     300     8962    347282   25086      0   487   20    28    7  72%   1019  -18   18   29   60%
c -   90.8     300     8962    386625   25523      0   487   29    44    7  65%   1021    2   23   28   82%
c -   99.8     300     8962    426596   26830      0   487   16    22    7  72%   1022  -14   19   23   83%
c -  109.5     300     8962    464327   25694      0   487   43    69   10  63%   1023   20   44   32  138%
c -  118.8     300     8962    505461   27142      0   487   25    38    7  67%   1024  -11   24   31   78%
c 
c [simplification-10] limit 519759 conflicts (hard 643439) hit after 542084 conflicts
c [card-4] limit 2144569 penalty 3 = 3 + 0
c [card-4] found 131 at-most-one constraints of average size 4.1
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 2144569 for elimination
c [card-4] 131 out of 131 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [simpleprobe-3] 11 schedulable variables 4%
c [simpleprobe-3] limit 34313116 penalty 2 = 2 + 0
c [simpleprobe-3] fully completed simple probing
c [unhide-4] limit 857827 with penalty 3 = 3 + 0
c [unhide-4-5] 0 units, 0 failed, 0 tauts, 0 hbrs, 35054 literals
c [elim-4] scheduling all variables this time
c [elim-4] scheduled 300 variables 100%
c [elim-4] boosting limit by 20
c [elim-4] limit of 1715655835 steps penalty 3 = 3 + 0
c [elim-4] rescheduling of touched variables disabled
c [elim-4-1] no variable eliminated in round 1 in 5097895 steps
c [elim-4] fully completed in 1 rounds
c [elim-4] transition to [ all 0 rem 0 ] state
c [elim-4] eliminated 0 = 0% variables out of 300 scheduled
c [sort-queue-10] sorted 300 enqueued variables after 542084 conflicts
c [score-dist-10] active 0 (0%), one 300 (100%), zero 0 (0%)
c [score-dist-10] max exp 1, different 1 (50%)
c [score-dist-10] median active exp 0, avg 0.0
c [simplification-10] removed 0 variables 0.0% (300 remain 100%)
c [simplification-10] removed 0 irredundant clauses 0.0% (8962 remain 51%)
c [simplification-10] maximum reduction of 0% = max (0%, 0%)
c [simplification-10] full geometric conflict interval increment 247360
c [simplification-10] new conflict interval 494720
c [simplification-10] penalized conflict interval 494720 = 1 * 494720
c [simplification-10] hard conflict limit 1284164 (soft 1036804 + delta 247360)
c [simplification-10] new conflict limit 1036804 (hard 1284164)
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 -  131.2     300     8962    547164   27993      0   487   40    62   10  64%   1024   21   52   28  186%
c -  141.4     300     8962    587643   27832      0   487   47    76   10  62%   1024   27   43   33  130%
c -  150.8     300     8962    629366   28880      0   487   23    32    8  71%   1024  -18   21   32   67%
c -  161.0     300     8962    671518   29499      0   487   33    50   11  65%   1024    7   47   29  162%
c -  171.5     300     8962    713677   29156      0   487   31    48    8  65%   1024   -0   17   32   53%
c -  182.9     300     8962    757648   30221      0   487   42    66    8  65%   1024   18   27   32   86%
c -  193.8     300     8962    801332   30818      0   487   38    60   11  63%   1024   14   51   31  165%
c -  205.0     300     8962    845812   31134      0   487   23    34   12  69%   1024  -14   19   31   63%
c -  216.9     300     8962    891272   31604      0   487   31    46    9  68%   1024   -3   34   32  104%
c -  229.3     300     8962    937922   32150      0   487   23    33    9  71%   1024  -12   21   30   72%
c -  242.4     300     8962    984230   32253      0   487   28    41   12  68%   1024  -12   22   34   65%
c -  253.6     300     8962   1031679   33424      0   487   26    38   12  68%   1024  -10   22   32   71%
c 
c [simplification-11] limit 1036804 conflicts (hard 1284164) hit after 1063038 conflicts
c [block-4] scheduling all variables this time
c [block-4] scheduled 300 variables 100%
c [block-4] limit of 90896668 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 [cce-7] limit of 90896668 steps penalty 2 = 2 + 0
c [cce-7-1] completed large round (ACCE)
c [cce-7-1] allowing another 1977072 steps for small clauses
c [cce-7-1] scheduling 8133 clauses = 8133 binary + 0 ternary
c [cce-7-1] tried to eliminate 8133 small clauses 100%
c [cce-7-1] completed small round (ACCE)
c [cce-7-1] completed small and large (ACCE)
c [cce-7-1] eliminated 0 covered clauses in round 1
c [cce-7] eliminated 0 covered clauses in TOTAL during 1 rounds
c [bca-4] limit of 10000000 steps and 18424 added (scaled 2)
c [bca-4] 0 out of 602 literals actually usable 0%
c [bca-4] not enough literals usable
c [bca-4] added 0 blocked clauses in 61289 steps
c [sort-queue-11] sorted 300 enqueued variables after 1063038 conflicts
c [score-dist-11] active 0 (0%), one 300 (100%), zero 0 (0%)
c [score-dist-11] max exp 1, different 1 (50%)
c [score-dist-11] median active exp 0, avg 0.0
c [simplification-11] removed 0 variables 0.0% (300 remain 100%)
c [simplification-11] removed 0 irredundant clauses 0.0% (8962 remain 51%)
c [simplification-11] maximum reduction of 0% = max (0%, 0%)
c [simplification-11] full geometric conflict interval increment 494720
c [simplification-11] new conflict interval 989440
c [simplification-11] penalized conflict interval 989440 = 1 * 989440
c [simplification-11] hard conflict limit 2547198 (soft 2052478 + delta 494720)
c [simplification-11] new conflict limit 2052478 (hard 2547198)
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 -  267.2     300     8962   1078811   33459      0   487   28    40   12  69%   1024   -5   24   30   81%
c -  280.2     300     8962   1126708   33622      0   487   29    44   12  66%   1024   -5   30   32   95%
c -  292.7     300     8962   1176644   34819      0   487   19    27   13  71%   1024  -13   17   27   64%
c -  307.1     300     8962   1226565   34814      0   487   42    65   12  66%   1024   25   45   28  163%
c -  321.0     300     8962   1276600   35380      0   487   22    31   13  71%   1024  -16   25   31   81%
c -  336.2     300     8962   1327480   35547      0   487   38    59    9  65%   1024   10   41   33  126%
c -  351.3     300     8962   1379145   35555      0   487   44    69   13  64%   1024   17   54   35  153%
c -  366.4     300     8962   1431681   36468      1   487   45    70   13  65%   1024   18   48   35  137%
c -  381.9     300     8962   1484334   36977      1   487   28    40   10  70%   1024  -11   26   34   76%
c -  398.8     300     8962   1538722   37589      1   487   47    70   10  67%   1024   26   42   31  137%
c -  416.2     300     8962   1592352   37354      1   487   35    54   10  65%   1024    1   29   35   84%
c -  433.6     300     8962   1648044   38836      1   487   40    61   10  66%   1024   15   31   32   98%
c -  450.6     300     8962   1703437   38349      1   487   27    38   14  72%   1024  -12   27   33   82%
c -  469.0     300     8962   1760324   39473      2   487   14    19   15  75%   1024  -23   13   28   46%
c -  489.6     300     8962   1817078   39843      6   488   52    81   15  65%   1024   32   44   34  129%
c -  507.9     300     8962   1874200   40454      6   488   23    33   11  71%   1024  -18   20   33   61%
c -  526.5     300     8962   1932390   40327      7   488   23    32   15  71%   1024  -12   49   30  163%
c -  547.2     300     8962   1991265   40702      7   488   30    43   15  69%   1024   -7   28   34   83%
c -  568.9     300     8962   2051551   41934      7   488   44    66   15  66%   1024   19   26   32   81%
c 
c [simplification-12] limit 2052478 conflicts (hard 2547198) hit after 2052480 conflicts
c [quatres-4] found 10 quaternary clauses 1% in total
c [ternres-4] limit 20129978 with penalty 3 = 3 + 0
c [ternres-4] all 300 free variables schedulable
c [ternres-4] 0 ternary resolvents (0 bin, 0 trn)
c [ternres-4] fully completed ternary resolution
c [gauss-4] limit 4025995 penalty 3 = 3 + 0
c [gauss-4] extracted 0 xors of average arity 0.0
c [gauss-4] exported 0 unary, 0 binary and 0 ternary equations
c [transred-4] limit 250000 with penalty 3 = 3 + 0
c [transred-4] removed 0 transitive binary clauses
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 60389935 penalty 3 = 3 + 0
c [sweep-5-1] 3 pos 4.7% + 61 neg 95.3% = 64 sched 21.3% ret 236
c [sweep-5-1] 3662996 steps 19 queries 6.05 avg class size
c [sweep-5-1] 1800 decisions 18 SAT calls 297.89 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] 19 pos 6.3% + 281 neg 93.7% = 300 sched 100.0% ret 0
c [sweep-5-2] 5268906 steps 27 queries 20.67 avg class size
c [sweep-5-2] 2600 decisions 26 SAT calls 297.88 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] 19 pos 6.3% + 281 neg 93.7% = 300 sched 100.0% ret 0
c [sweep-5-3] 4458462 steps 23 queries 17.70 avg class size
c [sweep-5-3] 2200 decisions 22 SAT calls 298.00 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, 66 queries)
c [sort-queue-12] sorted 300 enqueued variables after 2052480 conflicts
c [score-dist-12] active 0 (0%), one 300 (100%), zero 0 (0%)
c [score-dist-12] max exp 1, different 1 (50%)
c [score-dist-12] median active exp 0, avg 0.0
c [simplification-12] removed 0 variables 0.0% (300 remain 100%)
c [simplification-12] removed 0 irredundant clauses 0.0% (8962 remain 51%)
c [simplification-12] maximum reduction of 0% = max (0%, 0%)
c [simplification-12] full geometric conflict interval increment 989440
c [simplification-12] new conflict interval 1978880
c [simplification-12] penalized conflict interval 1978880 = 1 * 1978880
c [simplification-12] hard conflict limit 5020800 (soft 4031360 + delta 989440)
c [simplification-12] new conflict limit 4031360 (hard 5020800)
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 -  589.7     300     8962   2108924   41785      7   488   33    47   11  69%   1024   -3   28   34   82%
c -  609.8     300     8962   2169886   42606      7   488   21    28   11  73%   1024  -16   19   29   63%
c -  631.5     300     8962   2230740   42778      8   488   21    30   11  70%   1024  -17   22   31   70%
c -  652.5     300     8962   2291725   43446      8   488   27    40   12  66%   1024  -11   23   33   67%
c -  678.5     300     8962   2353750   44728      8   488   17    23   17  74%   1024  -16   12   26   48%
c -  703.4     300     8962   2415151   43851      8   488   28    42   16  68%   1024  -11   23   35   66%
c -  725.5     300     8962   2480026   44882      8   488   39    60   12  66%   1024   14   50   31  158%
c -  748.9     300     8962   2546187   44856     10   488   39    58   12  68%   1024   12   57   32  178%
c -  773.7     300     8962   2611349   44995     10   488   53    81   17  66%   1024   28   55   36  150%
c -  798.6     300     8962   2678019   46291     10   488   42    62   12  67%   1024   14   53   33  159%
c -  825.5     300     8962   2743438   46088     10   488   34    50   12  69%   1024   -5   33   37   90%
c -  852.4     300     8962   2811265   46985     10   488   52    79   12  66%   1024   29   50   35  145%
c -  877.5     300     8962   2878264   47215     10   488   31    46   13  66%   1024   -6   28   35   81%
c -  901.8     300     8962   2946980   48153     10   488   17    23   17  74%   1024  -21   15   29   52%
c -  927.5     300     8962   3016521   48569     10   488   46    70   12  66%   1024   30   59   29  204%
c -  952.6     300     8962   3085761   49288     10   488   28    39   13  71%   1024   -2   48   29  166%
c -  981.5     300     8962   3155252   49131     11   488   32    46   18  70%   1024   -0   27   32   83%
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), 117687 steps
c bkwd: tried 0 clauses, 0 lits, 0.00 lits/clause
c bkwd: checked 0 occs, 0.00 occs/clause, 0.00 occs/lit
c bkwd: subsumed 0 binary, 0 ternary, 0 large
c bkwd: strengthened 0 binary, 0 ternary (0% self), 0 large (0% self)
c blkd: 4 bces, 0 removed, 581945 resolutions, 1665953 steps
c blkd: 0 blocking literals 0%, 0 pure
c bump: 3172625 bumped seen, 375098841 lits 118.2 on average
c card: 4 count, 0 units, 0 am1, 37534473 steps
c card: 244 rescheduled, 127 eliminated, 187312 resolved, 1300 subsumed
c card: 541 at-most-one constraints found, average size 4.05
c card: 541 at-most-one constraints used 100%, average size 4.05
c card: 0 at-most-two constraints found, average size 0.00
c card: 0 at-most-two constraints used 0%, average size 0.00
c cces: 7 cces, 8135 eliminated, 8135 ate 100%, 0 abce 0%
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: 299590 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 37 gcs, 0 rescored clauses, 0 rescored vars
c dcps: 23 decompositions, 0 equivalent 0%
c deco: 4279 decision-only clauses 0%, 38% reduction
c decs: 5059017 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 4 elims, 0 eliminated 0%, 0 pure 0%
c elms: 4 rounds, 1.0 rounds/bve
c elms: 0 small 0%, 0 large 0%
c elms: 0 tried small, 0 succeeded 0%, 0 failed 0%
c elms: 0 subsumed, 515 strengthened, 0 blocked
c elms: 45304 copies, 50702 resolutions, 0 ipos
c elms: 243570 subchks, 137453 strchks
c gaus: 4 extractions, 0 extracted, 0.0 size, 0 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 15088198 steps, 7544099 extr 50%, 0 elim 0%
c glue: 32.0 orig avg, 32.0 real avg, 5.4 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 0 = 0 simple 0% + 0 trn 0% + 0 lrg 0%, 0 sub 0%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 3172625 clauses, 74.2 length
c lrnd: 235500714 lits = 331991434 orig - 96490720 removed 29%
c lrnd: 714305 uips 23%, 2148256 flips 68%
c mins: 3166216 mins 100%, 0 bin 0%, 2130 size 0%
c mins: 72210781 poisoned searches, 39648786 hits, 55% hit rate
c mins: 360511430 used twice searches, 83795991 hits, 23% hit rate
c move: moved 487, 487 bin 100%, 0 trn 0%
c otfs: 37387 driving 22%, 129269 restarting 78%
c otfs: str 166656, 160353 red 96%, 6303 irr 4%
c otfs: str 166656, 0 bin 0%, 0 trn 0%, 166656 lrg 100%
c otfs: sub 69, 69 red 100%, 0 irr 0%
c otfs: sub 69, 0 bin 0%, 0 trn 0%, 69 lrg 100%
c phas: 1 computed, 300 set, 0 pos (0%), 300 neg (100%)
c prbs: 2 basic, 1200 probed, 0 failed, 0 lifted
c prbs: 3 simple, 613 probed, 0 failed, 0 eqs
c prbs: 2 treelook, 7 probed, 0 failed, 0 lifted
c prom: 563606 locked 9% out of 5984141 tried
c prps: 89388957 props, 18 props/dec
c prps: 100% srch, 0% simp, 0% lkhd
c quat: 4 count, 0 quat, 0 self1, 0 self2, 0 dup
c queu: 12 sorted, 5059017 next (0 steps 0.00)
c queu: 375102741 enq (0 steps 0.00), 375098841 deq 100%
c redc: 6316 clauses 85%, 7438 tried 0%, 0 sat 0%
c redc: 18617 lits 13%, 144444 tried 0%, 0 sat 0%
c redc: 287 times jump level reduced, 2.9 levels on average
c reds: 61 count, 52572.4 conflicts per reduce
c reds: 0 memlim 0%, 61 arith 100%
c reds: 2440119 collected 89%, 310364 retired 11%
c rmbd: 443 removed, 0 red 0%
c rsts: 9456 restarts 100%, 0 skipped 0%
c rsts: 0 saturating 0%, 0 reuse 0%
c rsts: 0 kept 0.0% average 0.0%
c simp: 12 count, 12 confs 100%, 0 vars 0%
c simp: 0 its 0%, 0 bin 0%, 0 trns 0%
c subl: 3172625 count (2524722 tried 0.8), 327282 sub out of 3172613 (10.3%)
c swps: 5 count, 8 rounds, 117 queries (14.6/round)
c swps: 117 sat calls, 0 unsat (26.5% success rate)
c swps: 11697 decisions 100.0, 3096 conflicts 26.5
c swps; 20.8 avg class size, 296.4 avg environment size
c swps: 0 failed, 0 impls, 0 equivs
c swp0: 37 type 0 queries, 0 unsat (0.0%), 37 sat (100.0%)
c swp1: 80 type 1 queries, 2 unsat (2.5%), 80 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: 16463499 calls to obtain time
c tops: 0 fixed 0%, 0 its, 0.00 confs/it
c trds: 4 transitive reductions, 0 removed, 0 failed
c trds: 1839 nodes, 28068 edges, 1604293 steps
c trim: 3081063 words, 11.8 MB
c trnr: 4 count, 0 bin, 0 trn, 337842 steps
c unhd: 4 count, 5 rounds, 2536480 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: 0 tauts, 0 bin 0%, 0 trn 0%, 0 lrg 0%
c unhd: 0 tauts, 0 stamp 0%, 0 red 0%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 70322 str, 0 bin 0%, 0 trn 0%, 70322 lrg 100%, 67373 red 96%
c vars: 300 remaining 100% and 0 removed 0% out of 300
c vars: 0 fixed 0%, 0 eliminated 0%, 0 equivalent 0%
c vsts: 28300406443 visits, 100% srch, 0% simp, 0% lkhd
c vsts: 316.8 search visits per propagation, 8819.0 per conflict
c wchs: 21996010300 pushed, 2451022 enlarged, 1733 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all        3172613       2440119        310364      60352452      21487440       2453236
c 
c  0 0          1887   0      1119   0         0   0    542388   1    169882   1     14302   1     0.1
c  1 5          5176   0      3312   0       955   0   1059952   2    342259   2     31564   1     0.1
c  2 6         62712   2     44352   2     10787   3   7678823  13   2513513  12    287133  12     1.1
c  3 9        322395  10    242742  10     47781  15  29796554  49<  9744752  45   1163442  47<    4.7
c  4 14       636639  20    518457  21     67919  22  16288707  27   5677684  26<   689233  28     7.4
c  5 21       754744  24<   607993  25<    64256  21<  2900630   5   1470758   7    160085   7     7.0
c  6 30       621926  20    475199  19     47227  15    976959   2    728445   3     52624   2     5.9
c  7 41       356932  11    263365  11     29528  10    521470   1    398237   2     26197   1     4.6
c  8 54       199850   6    146047   6     20029   6    285249   0    215754   1     13886   1     3.0
c  9 69       127310   4     87110   4     13312   4    181077   0    136092   1      8622   0     2.2
c 10 86        79858   3     48472   2      8213   3    115796   0     86506   0      5844   0     1.4
c 11 126        3184   0      1951   0       357   0      4847   0      3558   0       304   0     0.1
c 
c avg                  5.4           5.4           5.2           3.3           3.5           3.4
c std                  1.8           1.7           1.9           1.1           1.3           1.2
c 
c   13.163   1% bump
c    2.961   0% decide
c    2.728   0% cce
c 
c    4.065 < 1% rest (below)
c 
c    1.309   0% card
c    1.243   0% unhide
c    1.029   0% sweep
c    0.641   0% probe
c    0.424   0% block
c    0.275   0% transred
c    0.225   0% elim
c    0.196   0% gauss
c    0.029   0% bca
c    0.002   0% quatres
c    0.001   0% ternres
c    0.000   0% locs
c    0.000   0% queuesort
c    0.000   0% rescore
c ==================================
c    0.513   0% preprocessing     6%
c    8.252   1% inprocessing     94%
c ==================================
c    8.765   1% simplifying
c  991.266  99% search
c ==================================
c 1000.031 100% all
c 
c       3206916 conflicts,        3206.8 confs/sec
c            11 ternaries,      291537.8 confs/ternary
c             1 binaries,      3206916.0 confs/binary
c             0 iterations,          0.0 confs/iteration
c 
c            61 reductions,          0.1 redus/sec,  52572.4 confs/reduction
c          9456 restarts,            9.5 rests/sec,    339.1 confs/restart
c       5059017 decisions,        5058.9 decis/sec,      1.6 decis/conflict
c      89388957 propagations,    89386.1 props/sec,     17.7 props/decision
c 
c 1000.0 seconds, 57.2 MB
c
c CAUGHT SIGNAL 15 SIGTERM
c
c launch: done
