c launch: /data/cnf/sc2014/app/stable-400-0.1-5-9876543214005.cnf.bz2
c host: atom04
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/stable-400-0.1-5-9876543214005.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/stable-400-0.1-5-9876543214005.cnf.bz2
c no embedded options
c found 'p cnf 400 30584' header
c read 400 variables, 30584 clauses, 629054 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=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 400 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] INC (--score=1)
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     400    30584         0       0      0     0    0     0    3   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 163 at-most-one constraints of average size 4.1
c [card-1] no at-most-two constraint found
c [card-1] using previous limit 2000000 for elimination
c [card-1] 163 out of 163 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [simpleprobe-1] all 400 free variables schedulable
c [simpleprobe-1] boosting simple probing limit by 10
c [simpleprobe-1] limit 20000000 penalty 0 = 0 + 0
c [simpleprobe-1] 31 variables remain 8% (369 retained 92%)
c [unhide-1] limit 100000 with penalty 0 = 0 + 0
c [unhide-1-1] 0 units, 0 failed, 0 tauts, 0 hbrs, 2811 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 400 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 400 scheduled
c [phase-count-1] 29407 negative 98.7% of 29807 except 400 1.3%
c [phase-count-1] 14715 positive 49.4% of 29807 except 15092 50.6%
c [phase-count-1] less non-negative clauses 400 than limit 2900 (10.0%)
c [phase-count-1] non-pos/non-neg = 15092/400 = 37.73 >= 2.00 = 200/100
c [lucky-phase-1] forcing lucky phase -1
c [phase-1] phase bias: 0 positive 0%, 400 negative 100%
c [sort-queue-1] sorted 400 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 400 (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% (400 remain 100%)
c [simplification-1] removed 777 irredundant clauses 2.5% (29807 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 800 literals 100%
c [treelook-1] scheduling used 88861 steps
c [treelook-1] scheduled completely
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 487307 steps
c [treelook-1] 798 literals remain 100%
c [treelook-1] 400 variables remain to probed next time 100%
c [basicprobe-1] limit 1023722 penalty 0 = 0 + 0
c [basicprobe-1-0] 118 probes remain 30% after last round
c [block-1] scheduling all variables this time
c [block-1] scheduled 400 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 13 clauses out of 14 (93%) of length 58
c [cce-1-1] eliminated 7 clauses out of 7 (100%) of length 57
c [cce-1-1] eliminated 115 clauses out of 119 (97%) of length 56
c [cce-1-1] eliminated 109 clauses out of 112 (97%) of length 55
c [cce-1-1] eliminated 130 clauses out of 134 (97%) of length 54
c [cce-1-1] eliminated 87 clauses out of 126 (69%) of length 53
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 461 large clauses in 30001152 steps
c [cce-1-1] allowing another 15000576 steps for small clauses
c [cce-1-1] scheduling 15092 clauses = 15092 binary + 0 ternary
c [cce-1-1] tried to eliminate 182 small clauses 1%
c [cce-1-1] eliminated 144 binary clauses 1%
c [cce-1-1] eliminated 144 small clauses 1%
c [cce-1-1] eliminated 144 small clauses in 30000385 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 605 covered clauses in round 1
c [cce-1] eliminated 605 covered clauses in TOTAL during 1 rounds
c [bca-1] limit of 10000000 steps and 58904 added (scaled 2)
c [bca-1] 161 out of 802 literals actually usable 20%
c [bca-1] added 0 blocked clauses in 4408 steps
c [sweep-1] limit 1000000 penalty 0 = 0 + 0
c [sweep-1-1] 18 pos 4.5% + 382 neg 95.5% = 400 sched 100.0% ret 0
c [sweep-1-1] 1038709 steps 29 queries 25.34 avg class size
c [sweep-1-1] 2800 decisions 28 SAT calls 395.57 avg env size
c [sweep-1-1] 3 variables remain 1% (397 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, 28 queries)
c [score-dist-2] active 400 (100%), one 0 (0%), zero 0 (0%)
c [score-dist-2] max exp 513, different 5 (1%)
c [score-dist-2] median active exp 512, avg 512.1
c [simplification-2] removed 0 variables 0.0% (400 remain 100%)
c [simplification-2] removed 605 irredundant clauses 2.0% (29202 remain 95%)
c [simplification-2] maximum reduction of 2% = max (0%, 2%)
c [simplification-2] geometric conflict interval increment 6666 = 20000 / 3
c [simplification-2] new conflict interval 11666
c [simplification-2] penalized conflict interval 11666 = 1 * 11666
c [simplification-2] hard conflict limit 26666 (soft 16666 + delta 10000)
c [simplification-2] new conflict limit 16666 (hard 26666)
c 
c [simplification-3] limit 16666 conflicts (hard 26666) hit after 16667 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 400 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 86 at-most-one constraints of average size 4.2
c [card-2] no at-most-two constraint found
c [card-2] using previous limit 1000000 for elimination
c [card-2] 86 out of 86 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] 31 schedulable variables 8%
c [simpleprobe-2] limit 1496688 penalty 1 = 1 + 0
c [simpleprobe-2] 31 variables remain 8% (369 retained 92%)
c [unhide-2] limit 74834 with penalty 1 = 1 + 0
c [unhide-2-2] 0 units, 0 failed, 0 tauts, 0 hbrs, 7000 literals
c [transred-1] limit 748344 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 29 clauses out of 32 (91%) of length 53
c [cce-2-1] eliminated 88 clauses out of 91 (97%) of length 52
c [cce-2-1] eliminated 242 clauses out of 253 (96%) of length 51
c [cce-2-1] eliminated 170 clauses out of 256 (66%) of length 50
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] eliminated 529 large clauses in 30000403 steps
c [cce-2-1] allowing another 15000201 steps for small clauses
c [cce-2-1] scheduling 14948 clauses = 14948 binary + 0 ternary
c [cce-2-1] tried to eliminate 124 small clauses 1%
c [cce-2-1] eliminated 65 binary clauses 0%
c [cce-2-1] eliminated 65 small clauses 0%
c [cce-2-1] eliminated 65 small clauses in 30000906 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 594 covered clauses in round 1
c [cce-2] eliminated 594 covered clauses in TOTAL during 1 rounds
c [elim-2] scheduling all variables this time
c [elim-2] scheduled 400 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 400 scheduled
c [sweep-2] limit 1000000 penalty 0 = 0 + 0
c [sweep-2-1] 0 pos 0.0% + 3 neg 100.0% = 3 sched 0.8% ret 397
c [sweep-2-1] 103073 steps 3 queries 1.67 avg class size
c [sweep-2-1] 200 decisions 2 SAT calls 396.50 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] 15 pos 3.8% + 385 neg 96.2% = 400 sched 100.0% ret 0
c [sweep-2-2] 940543 steps 20 queries 40.35 avg class size
c [sweep-2-2] 1900 decisions 19 SAT calls 397.21 avg env size
c [sweep-2-2] 102 variables remain 26% (298 retained 74%)
c [sweep-2-2] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-2] removed 0 vars in TOTAL (2 rounds, 21 queries)
c [score-dist-3] active 400 (100%), one 0 (0%), zero 0 (0%)
c [score-dist-3] max exp 515, different 5 (1%)
c [score-dist-3] median active exp 514, avg 514.0
c [simplification-3] removed 0 variables 0.0% (400 remain 100%)
c [simplification-3] removed 594 irredundant clauses 2.0% (28608 remain 94%)
c [simplification-3] maximum reduction of 2% = max (0%, 2%)
c [simplification-3] geometric conflict interval increment 6666 = 20000 / 3
c [simplification-3] new conflict interval 18332
c [simplification-3] penalized conflict interval 18332 = 1 * 18332
c [simplification-3] hard conflict limit 44999 (soft 34999 + delta 10000)
c [simplification-3] new conflict limit 34999 (hard 44999)
c 
c [simplification-4] limit 34999 conflicts (hard 44999) hit after 35003 conflicts
c [block-2] scheduling all variables this time
c [block-2] scheduled 400 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 75 clauses out of 85 (88%) of length 50
c [cce-3-1] eliminated 277 clauses out of 287 (97%) of length 49
c [cce-3-1] eliminated 147 clauses out of 478 (31%) of length 48
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 499 large clauses in 30000432 steps
c [cce-3-1] allowing another 15000216 steps for small clauses
c [cce-3-1] scheduling 14883 clauses = 14883 binary + 0 ternary
c [cce-3-1] tried to eliminate 122 small clauses 1%
c [cce-3-1] eliminated 52 binary clauses 0%
c [cce-3-1] eliminated 52 small clauses 0%
c [cce-3-1] eliminated 52 small clauses in 30000886 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 551 covered clauses in round 1
c [cce-3] eliminated 551 covered clauses in TOTAL during 1 rounds
c [bca-2] limit of 10000000 steps and 56614 added (scaled 2)
c [bca-2] 59 out of 802 literals actually usable 7%
c [bca-2] not enough literals usable
c [bca-2] added 0 blocked clauses in 28309 steps
c [score-dist-4] active 400 (100%), one 0 (0%), zero 0 (0%)
c [score-dist-4] max exp 516, different 5 (1%)
c [score-dist-4] median active exp 515, avg 515.0
c [simplification-4] removed 0 variables 0.0% (400 remain 100%)
c [simplification-4] removed 551 irredundant clauses 1.9% (28057 remain 92%)
c [simplification-4] maximum reduction of 2% = max (0%, 2%)
c [simplification-4] geometric conflict interval increment 6666 = 20000 / 3
c [simplification-4] new conflict interval 24998
c [simplification-4] penalized conflict interval 24998 = 1 * 24998
c [simplification-4] hard conflict limit 72500 (soft 60001 + delta 12499)
c [simplification-4] new conflict limit 60001 (hard 72500)
c 
c [simplification-5] limit 60001 conflicts (hard 72500) hit after 60001 conflicts
c [quatres-2] found 0 quaternary clauses 0% in total
c [ternres-2] limit 2093693 with penalty 1 = 1 + 0
c [ternres-2] all 400 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 209369 penalty 1 = 1 + 0 boost 1
c [treelook-2] scheduled 788 literals 98%
c [treelook-2] scheduling used 209632 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 209369 penalty 1 = 1 + 0 boost 1
c [treelook-2] used 408442 steps
c [treelook-2] 786 literals remain 98%
c [treelook-2] 400 variables remain to probed next time 100%
c [transred-2] limit 1000000 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 298 clauses out of 323 (92%) of length 48
c [cce-4-1] eliminated 517 clauses out of 542 (95%) of length 47
c [cce-4-1] eliminated 540 clauses out of 561 (96%) of length 46
c [cce-4-1] eliminated 587 clauses out of 612 (96%) of length 45
c [cce-4-1] eliminated 600 clauses out of 625 (96%) of length 44
c [cce-4-1] eliminated 722 clauses out of 752 (96%) of length 43
c [cce-4-1] eliminated 728 clauses out of 768 (95%) of length 42
c [cce-4-1] eliminated 873 clauses out of 909 (96%) of length 41
c [cce-4-1] eliminated 813 clauses out of 845 (96%) of length 40
c [cce-4-1] eliminated 850 clauses out of 898 (95%) of length 39
c [cce-4-1] eliminated 886 clauses out of 940 (94%) of length 38
c [cce-4-1] eliminated 720 clauses out of 756 (95%) of length 37
c [cce-4-1] eliminated 855 clauses out of 917 (93%) of length 36
c [cce-4-1] eliminated 627 clauses out of 655 (96%) of length 35
c [cce-4-1] eliminated 644 clauses out of 676 (95%) of length 34
c [cce-4-1] eliminated 538 clauses out of 571 (94%) of length 33
c [cce-4-1] eliminated 428 clauses out of 451 (95%) of length 32
c [cce-4-1] eliminated 445 clauses out of 467 (95%) of length 31
c [cce-4-1] eliminated 210 clauses out of 231 (91%) of length 30
c [cce-4-1] eliminated 180 clauses out of 193 (93%) of length 29
c [cce-4-1] eliminated 132 clauses out of 144 (92%) of length 28
c [cce-4-1] eliminated 72 clauses out of 140 (51%) of length 27
c [cce-4-1] incomplete large round (ATE)
c [cce-4-1] eliminated 12265 large clauses in 300000026 steps
c [cce-4-1] allowing another 150000013 steps for small clauses
c [cce-4-1] scheduling 14831 clauses = 14831 binary + 0 ternary
c [cce-4-1] tried to eliminate 12935 small clauses 87%
c [cce-4-1] eliminated 211 binary clauses 1%
c [cce-4-1] eliminated 211 small clauses 1%
c [cce-4-1] eliminated 211 small clauses in 300000034 steps
c [cce-4-1] incomplete small round (ATE)
c [cce-4-1] eliminated 12476 covered clauses in round 1
c [cce-4] eliminated 12476 covered clauses in TOTAL during 1 rounds
c [sweep-3] limit 628108 penalty 1 = 1 + 0
c [sweep-3-1] 3 pos 2.9% + 99 neg 97.1% = 102 sched 25.5% ret 298
c [sweep-3-1] 634746 steps 12 queries 10.83 avg class size
c [sweep-3-1] 1049 decisions 11 SAT calls 343.18 avg env size
c [sweep-3-1] 36 variables remain 9% (364 retained 91%)
c [sweep-3-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-3] removed 0 vars in TOTAL (1 rounds, 11 queries)
c [score-dist-5] active 400 (100%), one 0 (0%), zero 0 (0%)
c [score-dist-5] max exp 517, different 5 (1%)
c [score-dist-5] median active exp 516, avg 515.9
c [simplification-5] removed 0 variables 0.0% (400 remain 100%)
c [simplification-5] removed 12476 irredundant clauses 44.5% (15581 remain 51%)
c [simplification-5] maximum reduction of 44% = max (0%, 44%)
c [simplification-5] geometric conflict interval increment 555 = 24998 / 45
c [simplification-5] new conflict interval 25553
c [simplification-5] penalized conflict interval 25553 = 1 * 25553
c [simplification-5] hard conflict limit 98330 (soft 85554 + delta 12776)
c [simplification-5] new conflict limit 85554 (hard 98330)
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 -   21.6     400    15581     64760   22304      0   472   98   126   14  77%    637   48  102   62  164%
c 
c [simplification-6] limit 85554 conflicts (hard 98330) hit after 85554 conflicts
c [card-3] limit 719653 penalty 2 = 2 + 0
c [card-3] found 89 at-most-one constraints of average size 4.2
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 719653 for elimination
c [card-3] 89 out of 89 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [unhide-3] limit 287861 with penalty 2 = 2 + 0
c [unhide-3-3] 0 units, 0 failed, 0 tauts, 0 hbrs, 34839 literals
c [cce-5] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-5-1] eliminated 8 clauses out of 58 (14%) of length 27
c [cce-5-1] eliminated 16 clauses out of 73 (22%) of length 26
c [cce-5-1] eliminated 10 clauses out of 30 (33%) of length 25
c [cce-5-1] eliminated 4 clauses out of 14 (29%) of length 24
c [cce-5-1] eliminated 4 clauses out of 23 (17%) of length 23
c [cce-5-1] eliminated 1 clauses out of 19 (5%) of length 22
c [cce-5-1] eliminated 1 clauses out of 16 (6%) of length 20
c [cce-5-1] eliminated 1 clauses out of 10 (10%) of length 19
c [cce-5-1] completed large round (ACCE)
c [cce-5-1] eliminated 45 large clauses in 7018583 steps
c [cce-5-1] allowing another 3509291 steps for small clauses
c [cce-5-1] scheduling 14620 clauses = 14620 binary + 0 ternary
c [cce-5-1] tried to eliminate 2373 small clauses 16%
c [cce-5-1] eliminated 3 binary clauses 0%
c [cce-5-1] eliminated 3 small clauses 0%
c [cce-5-1] eliminated 3 small clauses in 30000064 steps
c [cce-5-1] incomplete small round (ACCE)
c [cce-5-1] eliminated 48 covered clauses in round 1
c [cce-5] eliminated 48 covered clauses in TOTAL during 1 rounds
c [cce-5] 48 < 1/100 * 15581 = 155 considered unsuccessful
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 400 variables 100%
c [elim-3] limit of 28786148 steps penalty 2 = 2 + 0
c [elim-3] rescheduling of touched variables disabled
c [elim-3-1] no variable eliminated in round 1 in 42669 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 400 scheduled
c [score-dist-6] active 400 (100%), one 0 (0%), zero 0 (0%)
c [score-dist-6] max exp 518, different 6 (1%)
c [score-dist-6] median active exp 516, avg 516.4
c [simplification-6] removed 0 variables 0.0% (400 remain 100%)
c [simplification-6] removed 48 irredundant clauses 0.3% (15533 remain 51%)
c [simplification-6] maximum reduction of 0% = max (0%, 0%)
c [simplification-6] full geometric conflict interval increment 25553
c [simplification-6] new conflict interval 51106
c [simplification-6] penalized conflict interval 51106 = 1 * 51106
c [simplification-6] hard conflict limit 162213 (soft 136660 + delta 25553)
c [simplification-6] new conflict limit 136660 (hard 162213)
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 -   31.9     400    15533    106233   23960      0   475  102   124   16  82%    818   23  104   81  128%
c 
c [simplification-7] limit 136660 conflicts (hard 162213) hit after 136660 conflicts
c [basicprobe-2] limit 23767099 penalty 1 = 1 + 0
c [basicprobe-2-0] 118 sched 30%, 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 400 variables 100%
c [block-3] limit of 23767099 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 31566 added (scaled 2)
c [bca-3] 62 out of 802 literals actually usable 8%
c [bca-3] not enough literals usable
c [bca-3] added 0 blocked clauses in 44292 steps
c [score-dist-7] active 400 (100%), one 0 (0%), zero 0 (0%)
c [score-dist-7] max exp 518, different 5 (1%)
c [score-dist-7] median active exp 517, avg 517.0
c [simplification-7] removed 0 variables 0.0% (400 remain 100%)
c [simplification-7] removed 0 irredundant clauses 0.0% (15533 remain 51%)
c [simplification-7] maximum reduction of 0% = max (0%, 0%)
c [simplification-7] full geometric conflict interval increment 51106
c [simplification-7] new conflict interval 102212
c [simplification-7] penalized conflict interval 102212 = 1 * 102212
c [simplification-7] hard conflict limit 289978 (soft 238872 + delta 51106)
c [simplification-7] new conflict limit 238872 (hard 289978)
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 -   41.6     400    15533    148362   24189      0   475   96   119   16  81%    916    8  102   89  115%
c -   50.6     400    15533    191994   23356      0   475   94   116   15  81%    968    2   87   91   95%
c -   61.6     400    15533    240004   24321      0   475   89   111   15  80%    997   -3   79   92   86%
c 
c [simplification-8] limit 238872 conflicts (hard 289978) hit after 250734 conflicts
c [quatres-3] found 0 quaternary clauses 0% in total
c [ternres-3] limit 4273968 with penalty 2 = 2 + 0
c [ternres-3] all 400 free variables schedulable
c [ternres-3] 0 ternary resolvents (0 bin, 0 trn)
c [ternres-3] fully completed ternary resolution
c [gauss-3] limit 854793 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 42739683 steps penalty 1 = 1 + 0
c [cce-6-1] completed large round (ATE)
c [cce-6-1] allowing another 3208008 steps for small clauses
c [cce-6-1] scheduling 14617 clauses = 14617 binary + 0 ternary
c [cce-6-1] tried to eliminate 3556 small clauses 24%
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 1282190 penalty 2 = 2 + 0
c [sweep-4-1] 0 pos 0.0% + 36 neg 100.0% = 36 sched 9.0% ret 364
c [sweep-4-1] 1171920 steps 16 queries 6.62 avg class size
c [sweep-4-1] 1457 decisions 15 SAT calls 333.20 avg env size
c [sweep-4-1] fully completed sweeping round
c [sweep-4-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-4-2] 16 pos 4.0% + 384 neg 96.0% = 400 sched 100.0% ret 0
c [sweep-4-2] 112056 steps 3 queries 136.67 avg class size
c [sweep-4-2] 200 decisions 2 SAT calls 394.00 avg env size
c [sweep-4-2] 399 variables remain 100% (1 retained 0%)
c [sweep-4-2] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-4] removed 0 vars in TOTAL (2 rounds, 17 queries)
c [score-dist-8] active 400 (100%), one 0 (0%), zero 0 (0%)
c [score-dist-8] max exp 519, different 4 (1%)
c [score-dist-8] median active exp 518, avg 518.0
c [simplification-8] removed 0 variables 0.0% (400 remain 100%)
c [simplification-8] removed 0 irredundant clauses 0.0% (15533 remain 51%)
c [simplification-8] maximum reduction of 0% = max (0%, 0%)
c [simplification-8] full geometric conflict interval increment 102212
c [simplification-8] new conflict interval 204424
c [simplification-8] penalized conflict interval 204424 = 1 * 204424
c [simplification-8] hard conflict limit 557370 (soft 455158 + delta 102212)
c [simplification-8] new conflict limit 455158 (hard 557370)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c -   72.6     400    15533    285687   24778      0   475   87   110   15  79%   1011   -3   88   90   97%
c -   82.1     400    15533    330454   25491      0   475   82   107   13  77%   1017   -5   86   88   97%
c -   92.3     400    15533    377600   25570      0   475   93   116   15  80%   1021    4   88   90   98%
c -  104.3     400    15533    427117   25954      0   475   92   113   16  82%   1022    1   94   89  105%
c -  116.3     400    15533    476908   26566      0   475   85   108   16  79%   1023   -3   86   88   98%
c 
c [simplification-9] limit 455158 conflicts (hard 557370) hit after 478233 conflicts
c [score-dist-9] active 400 (100%), one 0 (0%), zero 0 (0%)
c [score-dist-9] max exp 520, different 5 (1%)
c [score-dist-9] median active exp 519, avg 519.0
c [simplification-9] removed 0 variables 0.0% (400 remain 100%)
c [simplification-9] removed 0 irredundant clauses 0.0% (15533 remain 51%)
c [simplification-9] maximum reduction of 0% = max (0%, 0%)
c [simplification-9] full geometric conflict interval increment 204424
c [simplification-9] new conflict interval 408848
c [simplification-9] penalized conflict interval 408848 = 1 * 408848
c [simplification-9] hard conflict limit 1091505 (soft 887081 + delta 204424)
c [simplification-9] new conflict limit 887081 (hard 1091505)
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 -  127.1     400    15533    524476   27414      0   475   82   107   16  77%   1024   -2   84   86   97%
c -  139.1     400    15533    572214   27718      0   475   92   112   17  82%   1024    3   86   87   99%
c -  150.9     400    15533    618185   27912      0   475   91   113   16  80%   1024    5   90   86  105%
c -  162.1     400    15533    664113   28632      0   475   77   103   16  74%   1024   -4   72   84   86%
c -  173.1     400    15533    709818   29113      0   475   85   106   17  80%   1024    1   87   83  104%
c -  184.7     400    15533    760346   29246      0   475   87   108   17  81%   1024    2   89   84  106%
c -  198.3     400    15533    814389   29715      0   475   82   103   17  79%   1024   -4   80   86   94%
c -  210.3     400    15533    860876   30661      0   475   89   107   18  83%   1024    3   86   83  103%
c 
c [simplification-10] limit 887081 conflicts (hard 1091505) hit after 890520 conflicts
c [card-4] limit 3987599 penalty 3 = 3 + 0
c [card-4] found 333 at-most-one constraints of average size 4.2
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 3987599 for elimination
c [card-4] 333 out of 333 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [simpleprobe-3] 31 schedulable variables 8%
c [simpleprobe-3] limit 50000000 penalty 2 = 2 + 0
c [simpleprobe-3] fully completed simple probing
c [unhide-4] limit 1595039 with penalty 3 = 3 + 0
c [unhide-4-6] 0 units, 0 failed, 0 tauts, 0 hbrs, 109149 literals
c [elim-4] scheduling all variables this time
c [elim-4] scheduled 400 variables 100%
c [elim-4] boosting limit by 20
c [elim-4] limit of 2000000000 steps penalty 3 = 3 + 0
c [elim-4] rescheduling of touched variables disabled
c [elim-4-1] no variable eliminated in round 1 in 6117128 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 400 scheduled
c [score-dist-10] active 400 (100%), one 0 (0%), zero 0 (0%)
c [score-dist-10] max exp 521, different 4 (1%)
c [score-dist-10] median active exp 520, avg 519.9
c [simplification-10] removed 0 variables 0.0% (400 remain 100%)
c [simplification-10] removed 0 irredundant clauses 0.0% (15533 remain 51%)
c [simplification-10] maximum reduction of 0% = max (0%, 0%)
c [simplification-10] full geometric conflict interval increment 408848
c [simplification-10] new conflict interval 817696
c [simplification-10] penalized conflict interval 817696 = 1 * 817696
c [simplification-10] hard conflict limit 2117064 (soft 1708216 + delta 408848)
c [simplification-10] new conflict limit 1708216 (hard 2117064)
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 -  226.2     400    15533    910249   31533      0   475   84   107   18  79%   1024    2   86   83  103%
c -  237.4     400    15533    957215   31775      0   475   83   107   14  77%   1024    3   91   82  112%
c -  251.9     400    15533   1014104   31469      0   475   85   102   18  83%   1024   -4   93   85  110%
c -  264.1     400    15533   1064144   32084      0   475   83   105   18  79%   1024    1   83   83  100%
c -  277.8     400    15533   1116984   32751      0   475   79    99   18  80%   1024   -5   79   83   96%
c -  291.7     400    15533   1167579   33388      0   475   83   103   19  81%   1024    1   83   82  102%
c -  304.3     400    15533   1215161   34061      0   475   75    98   19  77%   1024   -2   74   79   93%
c -  316.8     400    15533   1263350   34642      0   475   81   104   16  78%   1024    4   79   78  101%
c -  332.1     400    15533   1318535   34721      0   475   83   104   19  80%   1024    0   84   82  102%
c -  346.7     400    15533   1368424   35054      0   475   74    96   16  77%   1024   -6   68   79   86%
c -  361.1     400    15533   1417906   36035      0   475   71    94   19  76%   1024   -5   74   77   97%
c -  377.3     400    15533   1467745   36833      0   475   82   102   21  80%   1024    2   79   77  102%
c -  392.3     400    15533   1517889   37059      0   475   83   107   20  77%   1024    7   84   77  110%
c -  408.5     400    15533   1572237   37038      0   475   86   107   20  81%   1024    6   91   79  116%
c -  425.4     400    15533   1629387   37855      0   475   82   102   20  80%   1024    0   79   81   97%
c -  440.0     400    15533   1680579   38492      0   475   75    95   22  80%   1024   -4   74   78   95%
c 
c [simplification-11] limit 1708216 conflicts (hard 2117064) hit after 1708217 conflicts
c [block-4] scheduling all variables this time
c [block-4] scheduled 400 variables 100%
c [block-4] limit of 100000000 steps penalty 3 = 3 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 0 blocked clauses
c [cce-7] limit of 170830985 steps penalty 2 = 2 + 0
c [cce-7-1] completed large round (ACCE)
c [cce-7-1] allowing another 3123989 steps for small clauses
c [cce-7-1] scheduling 14617 clauses = 14617 binary + 0 ternary
c [cce-7-1] tried to eliminate 14617 small clauses 100%
c [cce-7-1] eliminated 3 binary clauses 0%
c [cce-7-1] eliminated 3 small clauses 0%
c [cce-7-1] eliminated 3 small clauses in 160833714 steps
c [cce-7-1] completed small round (ACCE)
c [cce-7-1] completed small and large (ACCE)
c [cce-7-1] eliminated 3 covered clauses in round 1
c [cce-7-2] completed large round (ACCE)
c [cce-7-2] allowing another 3121087 steps for small clauses
c [cce-7-2] scheduling 14614 clauses = 14614 binary + 0 ternary
c [cce-7-2] tried to eliminate 650 small clauses 4%
c [cce-7-2] incomplete small round (ACCE)
c [cce-7-2] eliminated 0 covered clauses in round 2
c [cce-7] eliminated 3 covered clauses in TOTAL during 2 rounds
c [cce-7] 3 < 1/100 * 15533 = 155 considered unsuccessful
c [bca-4] limit of 10000000 steps and 31560 added (scaled 2)
c [bca-4] 81 out of 802 literals actually usable 10%
c [bca-4] not enough literals usable
c [bca-4] added 0 blocked clauses in 64012 steps
c [score-dist-11] active 400 (100%), one 0 (0%), zero 0 (0%)
c [score-dist-11] max exp 522, different 4 (1%)
c [score-dist-11] median active exp 521, avg 520.9
c [simplification-11] removed 0 variables 0.0% (400 remain 100%)
c [simplification-11] removed 3 irredundant clauses 0.0% (15530 remain 51%)
c [simplification-11] maximum reduction of 0% = max (0%, 0%)
c [simplification-11] full geometric conflict interval increment 817696
c [simplification-11] conflict interval soft limit 1000000 reached
c [simplification-11] new conflict interval 1000000
c [simplification-11] penalized conflict interval 1000000 = 1 * 1000000
c [simplification-11] hard conflict limit 3208217 (soft 2708217 + delta 500000)
c [simplification-11] new conflict limit 2708217 (hard 3208217)
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 -  457.9     400    15530   1731291   39256      0   478   74    92   21  80%   1024   -5   71   76   93%
c -  472.6     400    15530   1782212   39528      0   478   75    97   21  77%   1024    1   74   75   99%
c -  490.8     400    15530   1839331   39562      0   478   78    97   21  80%   1024   -2   77   79   97%
c -  508.1     400    15530   1894382   39953      0   478   80   103   22  77%   1024    4   77   77  100%
c -  527.7     400    15530   1953408   40732      0   478   78    99   23  80%   1024   -2   85   79  107%
c -  545.1     400    15530   2007623   41542      0   478   73    95   22  77%   1024   -2   73   77   96%
c -  566.4     400    15530   2063492   41281      0   478   82   100   22  82%   1024    3   76   77   99%
c -  584.1     400    15530   2120322   42064      0   478   78   100   22  78%   1024    4   80   76  105%
c -  602.0     400    15530   2182043   41748      0   478   80   103   22  78%   1024    3   79   79  100%
c -  623.0     400    15530   2252727   42110      0   478   85   107   18  80%   1024    2   87   84  104%
c -  643.4     400    15530   2318134   42661      0   478   77    97   23  79%   1024   -5   73   82   89%
c -  663.1     400    15530   2379298   44031      0   478   73    95   23  77%   1024   -5   72   78   91%
c -  681.2     400    15530   2439878   44896      0   478   78    99   23  79%   1024    0   78   78  101%
c -  705.9     400    15530   2509740   44170      0   478   87   105   24  83%   1024    2   84   83  101%
c -  727.4     400    15530   2574727   43982      0   478   74    93   23  80%   1024   -6   70   80   88%
c -  746.2     400    15530   2638477   45498      0   478   79    97   20  81%   1024    0   86   77  112%
c -  765.9     400    15530   2704483   46272      0   478   78    96   20  81%   1024   -2   77   79   98%
c -  783.3     400    15530   2765683   46526      0   478   72    92   20  78%   1024   -3   71   75   95%
c 
c [simplification-12] limit 2708217 conflicts (hard 3208217) hit after 2774125 conflicts
c [quatres-4] found 0 quaternary clauses 0% in total
c [ternres-4] limit 25000000 with penalty 3 = 3 + 0
c [ternres-4] all 400 free variables schedulable
c [ternres-4] 0 ternary resolvents (0 bin, 0 trn)
c [ternres-4] fully completed ternary resolution
c [gauss-4] limit 6231555 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 93473332 penalty 3 = 3 + 0
c [sweep-5-1] 20 pos 5.0% + 379 neg 95.0% = 399 sched 99.8% ret 1
c [sweep-5-1] 4714667 steps 42 queries 27.60 avg class size
c [sweep-5-1] 3995 decisions 41 SAT calls 365.17 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] 20 pos 5.0% + 380 neg 95.0% = 400 sched 100.0% ret 0
c [sweep-5-2] 4529418 steps 38 queries 20.24 avg class size
c [sweep-5-2] 3666 decisions 37 SAT calls 372.32 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] 20 pos 5.0% + 380 neg 95.0% = 400 sched 100.0% ret 0
c [sweep-5-3] 5604256 steps 42 queries 17.93 avg class size
c [sweep-5-3] 4100 decisions 41 SAT calls 371.66 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, 119 queries)
c [score-dist-12] active 400 (100%), one 0 (0%), zero 0 (0%)
c [score-dist-12] max exp 523, different 4 (1%)
c [score-dist-12] median active exp 521, avg 521.5
c [simplification-12] removed 0 variables 0.0% (400 remain 100%)
c [simplification-12] removed 0 irredundant clauses 0.0% (15530 remain 51%)
c [simplification-12] maximum reduction of 0% = max (0%, 0%)
c [simplification-12] full geometric conflict interval increment 1000000
c [simplification-12] new conflict interval 2000000
c [simplification-12] penalized conflict interval 2000000 = 1 * 2000000
c [simplification-12] hard conflict limit 5774125 (soft 4774125 + delta 1000000)
c [simplification-12] new conflict limit 4774125 (hard 5774125)
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 -  807.7     400    15530   2829686   46319      0   478   72    91   24  79%   1024   -3   69   76   90%
c -  832.6     400    15530   2901073   47157      0   478   78    95   25  82%   1024   -4   81   80  102%
c -  852.4     400    15530   2965581   47985      0   478   69    93   20  75%   1024   -2   67   75   89%
c -  872.4     400    15530   3032022   48101      0   478   79   100   25  79%   1024    3   79   77  103%
c -  901.2     400    15530   3112534   47933      0   478   84   104   25  80%   1024    1   81   83   97%
c -  927.6     400    15530   3188279   49056      0   478   79    97   21  81%   1024   -4   80   82   97%
c -  952.1     400    15530   3261324   49518      0   478   77    96   21  80%   1024   -3   82   80  103%
c -  976.6     400    15530   3331490   50247      0   478   69    88   26  78%   1024   -7   68   76   89%
c -  998.1     400    15530   3400966   51079      0   478   76   100   26  76%   1024    5   74   75   98%
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), 141021 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, 1456459 resolutions, 4140721 steps
c blkd: 2 blocking literals 0%, 0 pure
c bump: 3369565 bumped seen, 613161526 lits 182.0 on average
c card: 4 count, 0 units, 0 am1, 15852342 steps
c card: 34 rescheduled, 162 eliminated, 68772 resolved, 305 subsumed
c card: 671 at-most-one constraints found, average size 4.15
c card: 671 at-most-one constraints used 100%, average size 4.15
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, 14277 eliminated, 14276 ate 100%, 1 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: 659638 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 38 gcs, 0 rescored clauses, 0 rescored vars
c dcps: 24 decompositions, 0 equivalent 0%
c deco: 508088 decision-only clauses 15%, 48% reduction
c decs: 4984408 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, 581 strengthened, 0 blocked
c elms: 40870 copies, 45722 resolutions, 0 ipos
c elms: 371815 subchks, 131482 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, 15218976 steps, 7609488 extr 50%, 0 elim 0%
c glue: 81.5 orig avg, 81.5 real avg, 9.0 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: 3369565 clauses, 131.9 length
c lrnd: 444420755 lits = 565862915 orig - 121442160 removed 21%
c lrnd: 642075 uips 19%, 2295858 flips 68%
c mins: 2861353 mins 85%, 0 bin 0%, 124 size 0%
c mins: 141360023 poisoned searches, 100290069 hits, 71% hit rate
c mins: 495377294 used twice searches, 197693914 hits, 40% hit rate
c move: moved 478, 478 bin 100%, 0 trn 0%
c otfs: 41232 driving 23%, 137288 restarting 77%
c otfs: str 178520, 173090 red 97%, 5430 irr 3%
c otfs: str 178520, 0 bin 0%, 0 trn 0%, 178520 lrg 100%
c otfs: sub 133, 133 red 100%, 0 irr 0%
c otfs: sub 133, 0 bin 0%, 0 trn 0%, 133 lrg 100%
c phas: 1 computed, 400 set, 0 pos (0%), 400 neg (100%)
c prbs: 2 basic, 800 probed, 0 failed, 0 lifted
c prbs: 3 simple, 833 probed, 0 failed, 0 eqs
c prbs: 2 treelook, 4 probed, 0 failed, 0 lifted
c prom: 5955 locked 12% out of 48399 tried
c prps: 111290404 props, 22 props/dec
c prps: 100% srch, 0% simp, 0% lkhd
c quat: 4 count, 0 quat, 0 self1, 0 self2, 0 dup
c queu: 1 sorted, 4984408 next (137049 steps 0.03)
c queu: 613162326 enq (738381952 steps 1.20), 613161526 deq 100%
c redc: 47 clauses 87%, 54 tried 0%, 0 sat 0%
c redc: 150 lits 16%, 958 tried 0%, 0 sat 0%
c redc: 2 times jump level reduced, 4.5 levels on average
c reds: 61 count, 55878.6 conflicts per reduce
c reds: 0 memlim 0%, 61 arith 100%
c reds: 2440138 collected 92%, 206686 retired 8%
c rmbd: 777 removed, 0 red 0%
c rsts: 4137 restarts 100%, 0 skipped 0%
c rsts: 0 saturating 0%, 0 reuse 0%
c rsts: 0 kept 0.0% average 0.0%
c scnc: 0 count, 1.000 min (0/1000), 1.000 max (0/1000)
c simp: 12 count, 12 confs 100%, 0 vars 0%
c simp: 0 its 0%, 0 bin 0%, 0 trns 0%
c subl: 3369565 count (3866603 tried 1.1), 664572 sub out of 3369565 (19.7%)
c swps: 5 count, 9 rounds, 196 queries (21.8/round)
c swps: 196 sat calls, 0 unsat (11.2% success rate)
c swps: 19367 decisions 98.8, 2201 conflicts 11.2
c swps; 24.9 avg class size, 372.3 avg environment size
c swps: 0 failed, 0 impls, 0 equivs
c swp0: 61 type 0 queries, 0 unsat (0.0%), 61 sat (100.0%)
c swp1: 135 type 1 queries, 0 unsat (0.0%), 135 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: 16708161 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: 1566 nodes, 32752 edges, 2498509 steps
c trim: 2421143 words, 9.2 MB
c trnr: 4 count, 0 bin, 0 trn, 473184 steps
c unhd: 4 count, 6 rounds, 3354284 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: 153799 str, 0 bin 0%, 0 trn 0%, 153799 lrg 100%, 147947 red 96%
c vars: 400 remaining 100% and 0 removed 0% out of 400
c vars: 0 fixed 0%, 0 eliminated 0%, 0 equivalent 0%
c vsts: 32150138926 visits, 100% srch, 0% simp, 0% lkhd
c vsts: 289.0 search visits per propagation, 9426.1 per conflict
c wchs: 19089448157 pushed, 665038 enlarged, 479 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all        3369565       2440138        206686      57468071      21724025       2368735
c 
c  0 0             6   0         1   0         0   0      3047   0       682   0        65   0     0.0
c  1 5            27   0         6   0         9   0     25855   0      7912   0       619   0     0.0
c  2 6           335   0        97   0        82   0    229847   0     71558   0      7449   0     0.0
c  3 9          5063   0      2385   0       856   0   2651086   5    831131   4    136664   6     0.2
c  4 14        24381   1     14064   1      3960   2  14066390  24   4248254  20    608314  26     0.9
c  5 21        64910   2     41524   2     14357   7  16484344  29   5194267  24    466850  20     2.1
c  6 30       142457   4    105919   4     23597  11  11041484  19<  3923782  18<   429717  18<    4.3
c  7 41       259306   8    221797   9     26524  13   5492045  10   2382835  11    294336  12     5.8
c  8 54       417158  12    383870  16     26796  13<  2837055   5   1577060   7    184908   8     6.5
c  9 69       689608  20<   641125  26<    33319  16   1936706   3   1359539   6    130395   6    14.8
c 10 86      1727513  51   1015959  42     76290  37   2637123   5   2085938  10    107871   5    26.3
c 11 126       38801   1     13391   1       896   0     63089   0     41067   0      1547   0     6.5
c 
c avg                  9.0           8.9           8.2           5.6           6.1           5.7
c std                  1.4           1.3           1.8           1.7           2.0           1.8
c 
c   79.944   8% bump
c    4.731   0% cce
c    3.053   0% decide
c 
c    6.009 < 1% rest (below)
c 
c    2.891   0% unhide
c    1.754   0% sweep
c    1.313   0% block
c    0.962   0% probe
c    0.750   0% card
c    0.490   0% transred
c    0.342   0% elim
c    0.294   0% gauss
c    0.096   0% bca
c    0.006   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.798   0% preprocessing     5%
c   14.115   1% inprocessing     95%
c ==================================
c   14.913   1% simplifying
c  985.111  99% search
c ==================================
c 1000.025 100% all
c 
c       3408596 conflicts,        3408.5 confs/sec
c             0 ternaries,           0.0 confs/ternary
c             0 binaries,            0.0 confs/binary
c             0 iterations,          0.0 confs/iteration
c 
c            61 reductions,          0.1 redus/sec,  55878.6 confs/reduction
c          4137 restarts,            4.1 rests/sec,    823.9 confs/restart
c       4984408 decisions,        4984.3 decis/sec,      1.5 decis/conflict
c     111290404 propagations,   111287.6 props/sec,     22.3 props/decision
c 
c 1000.0 seconds, 100.5 MB
c
c CAUGHT SIGNAL 15 SIGTERM
c
c launch: done
