c launch: /data/cnf/sc2014/app/9vliw_m_9stages_iq3_C1_bug7.cnf.bz2
c host: atom22
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/9vliw_m_9stages_iq3_C1_bug7.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/9vliw_m_9stages_iq3_C1_bug7.cnf.bz2
c no embedded options
c found 'p cnf 521147 13378010' header
c read 521147 variables, 13378010 clauses, 39203144 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=3
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 521146 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] SUM (--score=3)
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  521146 13378009         0       0      0     0    0     0  341   0%      0    0    0    0    0%
c 
c [simplification-1] limit 0 conflicts (hard 0) hit after 0 conflicts
c [card-1] limit 3344502 based on 13378009 irredundant clauses
c [card-1] found 8 at-most-one constraints of average size 3.0
c [card-1] no at-most-two constraint found
c [card-1] using previous limit 3344502 for elimination
c [card-1] 8 out of 8 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 6 variables
c [simpleprobe-1] all 521141 free variables schedulable
c [simpleprobe-1] boosting simple probing limit by 10
c [simpleprobe-1] limit 26755946 based on 13377973 irredundant clauses
c [simpleprobe-1] 521141 variables remain 100% (0 retained 0%)
c [simpleprobe-1] removed 0 variables, found 530 hbrs, 0 units
c [unhide-1] limit 836123 based on 13377973 irredundant clauses
c [unhide-1-1] 0 units, 3 failed, 227 tauts, 0 hbrs, 13789 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 521138 variables 100%
c [elim-1] limit of 13377724 steps based on 13377724 irredundant clauses
c [elim-1] rescheduling of touched variables disabled
c [elim-1] incomplete 516040 not tried 99% in round 1
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 4234 = 1% variables out of 521138 scheduled
c [elim-1] considered successful since not run to completion yet
c [phase-count-1] 13368047 negative 100.0% of 13369093 except 1046 0.0%
c [phase-count-1] 7133289 positive 53.4% of 13369093 except 6235804 46.6%
c [phase-count-1] less non-negative clauses 1046 than limit 1336900 (10.0%)
c [phase-count-1] non-pos/non-neg = 6235804/1046 = 5961.57 >= 2.00 = 200/100
c [lucky-phase-1] forcing lucky phase -1
c [phase-1] phase bias: 0 positive 0%, 516904 negative 100%
c [sort-queue-1] sorted 516904 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 516904 (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 4237 variables 0.8% (516904 remain 99%)
c [simplification-1] removed 8916 irredundant clauses 0.1% (13369093 remain 100%)
c [simplification-1] maximum reduction of 1% = max (1%, 0%)
c [simplification-1] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-1] new conflict interval 10000
c [simplification-1] penalized conflict interval 10000 = 1 * 10000
c [simplification-1] hard conflict limit 20000 (soft 10000 + delta 10000)
c [simplification-1] new conflict limit 10000 (hard 20000)
c 
c [simplification-2] limit 10000 conflicts (hard 20000) hit after 10000 conflicts
c [decomp-3] removed 1 variables
c [treelook-1] limit 3342272 based on 13369091 irredundant clauses
c [treelook-1] scheduled 386391 literals 37%
c [treelook-1] scheduling used 3342668 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 3342272 based on 13369091 irredundant clauses
c [treelook-1] used 5082078 steps
c [treelook-1] 386389 literals remain 37%
c [treelook-1] 384095 variables remain to probed next time 74%
c [treelook-1] removed 0 variables, found 579 hbrs
c [basicprobe-1] limit 106952728 based on 13369091 irredundant clauses
c [basicprobe-1-0] 503315 probes remain 97% after last round
c [basicprobe-1-0] 29 units = 29 failed (100%) + 0 lifted (0%)
c [basicprobe-1-0] removed 29 variables, found 56936 hbrs
c [unhide-2] limit 835568 based on 13369091 irredundant clauses
c [unhide-2-2] 5834 units, 3 failed, 64 tauts, 0 hbrs, 249891 literals
c [elim-2] 510173 variables 100% will be scheduled this time
c [elim-2] scheduled 510173 variables 100%
c [elim-2] limit of 24719367 steps penalty 4 = 0 + 4
c [elim-2] rescheduling of touched variables disabled
c [elim-2] incomplete 492831 not tried 96% in round 1
c [elim-2] transition to [ all 0 rem 1 ] state
c [elim-2] eliminated 8919 = 2% variables out of 510173 scheduled
c [elim-2] considered successful since not run to completion yet
c [sort-queue-2] sorted 436334 enqueued variables after 10000 conflicts
c [score-dist-2] active 65784 (13%), one 0 (0%), zero 436334 (87%)
c [score-dist-2] max exp 527, different 26 (5%)
c [score-dist-2] median active exp 515, avg 515.9
c [simplification-2] removed 14786 variables 2.9% (502118 remain 96%)
c [simplification-2] removed 134730 irredundant clauses 1.0% (13234363 remain 99%)
c [simplification-2] maximum reduction of 3% = max (3%, 1%)
c [simplification-2] geometric conflict interval increment 5000 = 20000 / 4
c [simplification-2] new conflict interval 15000
c [simplification-2] penalized conflict interval 15000 = 1 * 15000
c [simplification-2] hard conflict limit 35000 (soft 25000 + delta 10000)
c [simplification-2] new conflict limit 25000 (hard 35000)
c 
c [simplification-3] limit 25000 conflicts (hard 35000) hit after 25000 conflicts
c [card-2] limit 3308590 based on 13234363 irredundant clauses
c [card-2] found 10 at-most-one constraints of average size 3.3
c [card-2] no at-most-two constraint found
c [card-2] using previous limit 3308590 for elimination
c [card-2] 10 out of 10 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [decomp-5] removed 4 variables
c [simpleprobe-2] all 502114 free variables schedulable
c [simpleprobe-2] limit 26468714 based on 13234357 irredundant clauses
c [simpleprobe-2] 502114 variables remain 100% (0 retained 0%)
c [simpleprobe-2] removed 0 variables, found 3980 hbrs, 0 units
c [unhide-3] limit 827147 based on 13234357 irredundant clauses
c [unhide-3-3] 196 units, 5 failed, 12388 tauts, 0 hbrs, 14441 literals
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 501916 variables 100%
c [elim-3] limit of 48205918 steps penalty 4 = 0 + 4
c [elim-3] rescheduling of touched variables disabled
c [elim-3] incomplete 474583 not tried 95% in round 1
c [elim-3] transition to [ all 1 rem 1 ] state
c [elim-3] eliminated 6728 = 1% variables out of 501916 scheduled
c [elim-3] considered successful since not run to completion yet
c [sort-queue-3] sorted 429350 enqueued variables after 25000 conflicts
c [score-dist-3] active 65838 (13%), one 0 (0%), zero 429350 (87%)
c [score-dist-3] max exp 530, different 29 (5%)
c [score-dist-3] median active exp 516, avg 516.7
c [simplification-3] removed 6930 variables 1.4% (495188 remain 95%)
c [simplification-3] removed 28854 irredundant clauses 0.2% (13205509 remain 99%)
c [simplification-3] maximum reduction of 1% = max (1%, 0%)
c [simplification-3] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-3] new conflict interval 25000
c [simplification-3] penalized conflict interval 25000 = 1 * 25000
c [simplification-3] hard conflict limit 62500 (soft 50000 + delta 12500)
c [simplification-3] new conflict limit 50000 (hard 62500)
c 
c [simplification-4] limit 50000 conflicts (hard 62500) hit after 50001 conflicts
c [decomp-7] removed 1 variables
c [unhide-4] limit 825344 based on 13205507 irredundant clauses
c [unhide-4-4] 285 units, 4 failed, 24 tauts, 0 hbrs, 38961 literals
c [elim-4] 474143 variables 96% will be scheduled this time
c [elim-4] scheduled 474143 variables 96%
c [elim-4] boosting limit by 20
c [elim-4] limit of 1000000000 steps penalty 4 = 0 + 4
c [elim-4] rescheduling of touched variables disabled
c [elim-4] incomplete 50386 not tried 10% in round 1
c [elim-4] transition to [ all 0 rem 1 ] state
c [elim-4] eliminated 23006 = 5% variables out of 474143 scheduled
c [elim-4] considered successful since not run to completion yet
c [sort-queue-4] sorted 408431 enqueued variables after 50001 conflicts
c [score-dist-4] active 63461 (13%), one 0 (0%), zero 408431 (87%)
c [score-dist-4] max exp 532, different 31 (6%)
c [score-dist-4] median active exp 517, avg 517.7
c [simplification-4] removed 23296 variables 4.7% (471892 remain 91%)
c [simplification-4] removed 50244 irredundant clauses 0.4% (13155265 remain 98%)
c [simplification-4] maximum reduction of 5% = max (5%, 0%)
c [simplification-4] large reduction 5% >= 5% limit
c [simplification-4] next conflict interval 2000 = 2000/1
c [simplification-4] penalized conflict interval 2000 = 1 * 2000
c [simplification-4] hard conflict limit 62001 (soft 52001 + delta 10000)
c [simplification-4] new conflict limit 52001 (hard 62001)
c 
c [simplification-5] limit 52001 conflicts (hard 62001) hit after 52002 conflicts
c [quatres-1] found 77577 quaternary clauses 14% in total
c [quatres-1-2] added 1929 single-self-subsuming ternary resolvents
c [quatres-1-2] added 5724 quaternary resolvents
c [ternres-1] boosting ternary resolution limit by 5
c [ternres-1] limit 52621060 based on 13155265 irredundant clauses
c [ternres-1] all 471892 free variables schedulable
c [ternres-1] 2418 ternary resolvents (0 bin, 2418 trn)
c [ternres-1] 461863 variables remain 98% (10029 retained 2%)
c [gauss-1] limit 6577632 based on 13155265 irredundant clauses
c [gauss-1] extracted 0 xors of average arity 0.0
c [gauss-1] exported 0 unary, 0 binary and 0 ternary equations
c [treelook-2] limit 3288816 based on 13155265 irredundant clauses
c [treelook-2] scheduled 374164 literals 40%
c [treelook-2] scheduling used 3288874 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 3288816 based on 13155265 irredundant clauses
c [treelook-2] used 7164520 steps
c [treelook-2] 374162 literals remain 40%
c [treelook-2] 339411 variables remain to probed next time 72%
c [treelook-2] removed 0 variables, found 178 hbrs
c [unhide-5] limit 822204 based on 13155265 irredundant clauses
c [unhide-5-5] 4 units, 4 failed, 39470 tauts, 0 hbrs, 36863 literals
c [transred-1] limit 13117233 based on 13117233 irredundant clauses
c [transred-1] removed 0 transitive binary clauses
c [block-1] scheduling all variables this time
c [block-1] scheduled 471887 variables 100%
c [block-1] boosting limit by 10
c [block-1] limit of 300305273 steps penalty 4 = 0 + 4
c [block-1] incomplete 5779 not tried 1%
c [block-1] transition to [ all 1 rem 1 ] state
c [block-1] eliminated 180556 blocked clauses
c [block-1] considered successful since not run to completion yet
c [cce-1] limit of 15015263 steps penalty 4 = 0 + 4
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] allowing another 7507632 steps for small clauses
c [cce-1-1] scheduling 10743228 clauses = 8090527 binary + 2652701 ternary
c [cce-1-1] tried to eliminate 5 small clauses 0%
c [cce-1-1] eliminated 1 binary clauses 0%
c [cce-1-1] eliminated 1 small clauses 0%
c [cce-1-1] eliminated 1 small clauses in 15015478 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 1 covered clauses in round 1
c [cce-1] eliminated 1 covered clauses in TOTAL during 1 rounds
c [cce-1] 1 < 1/100 * 12936534 = 129365 considered unsuccessful
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 471861 variables 100%
c [elim-5] limit of 50000000 steps penalty 4 = 0 + 4
c [elim-5] rescheduling of touched variables disabled
c [elim-5] incomplete 469847 not tried 100% in round 1
c [elim-5] transition to [ all 1 rem 1 ] state
c [elim-5] eliminated 2014 = 0% variables out of 471861 scheduled
c [elim-5] 2014 < 1/100 * 471861 = 4718 considered unsuccessful
c [bca-1] limit of 10000000 steps and 25869538 added (scaled 2)
c [bca-1] 910129 out of 939696 literals actually usable 97%
c [bca-1] added 1299709 blocked clauses in 4137433 steps
c [sweep-1] limit 25869038 based on 12934519 irredundant clauses
c [sweep-1-1] 4005 pos 0.9% + 465842 neg 99.1% = 469847 sched 100.0% ret 0
c [sweep-1-1] 26899782 steps 28 queries 38731.43 avg class size
c [sweep-1-1] 1124 decisions 24 SAT calls 3438.29 avg env size
c [sweep-1-1] 469559 variables remain 100% (288 retained 0%)
c [decomp-10] removed 197 variables
c [sweep-1-1] removed 197 vars (0 failed, 3 eqs, 6 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 197 vars in TOTAL (1 rounds, 27 queries)
c [sort-queue-5] sorted 407588 enqueued variables after 52002 conflicts
c [score-dist-5] active 62062 (13%), one 0 (0%), zero 407588 (87%)
c [score-dist-5] max exp 532, different 31 (6%)
c [score-dist-5] median active exp 517, avg 517.8
c [simplification-5] removed 2242 variables 0.5% (469650 remain 90%)
c [simplification-5] removed 221132 irredundant clauses 1.7% (12934133 remain 97%)
c [simplification-5] maximum reduction of 2% = max (0%, 2%)
c [simplification-5] geometric conflict interval increment 8333 = 25000 / 3
c [simplification-5] new conflict interval 33333
c [simplification-5] penalized conflict interval 33333 = 1 * 33333
c [simplification-5] hard conflict limit 102001 (soft 85335 + delta 16666)
c [simplification-5] new conflict limit 85335 (hard 102001)
c 
c [simplification-6] limit 85335 conflicts (hard 102001) hit after 85336 conflicts
c [quatres-2] found 77538 quaternary clauses 14% in total
c [quatres-2-2] added 191 single-self-subsuming ternary resolvents
c [quatres-2-2] added 3271 quaternary resolvents
c [ternres-2] limit 51736532 based on 12934133 irredundant clauses
c [ternres-2] 459676 schedulable variables 98%
c [ternres-2] 6340 ternary resolvents (0 bin, 6340 trn)
c [ternres-2] 451823 variables remain 96% (17827 retained 4%)
c [card-3] limit 3233533 based on 12934133 irredundant clauses
c [card-3] found 8 at-most-one constraints of average size 3.0
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 3233533 for elimination
c [card-3] 8 out of 8 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [basicprobe-2] limit 103473064 based on 12934133 irredundant clauses
c [basicprobe-2-0] 445012 probes remain 95% after last round
c [basicprobe-2-0] 32 units = 32 failed (100%) + 0 lifted (0%)
c [basicprobe-2-0] removed 32 variables, found 24884 hbrs
c [unhide-6] limit 808383 based on 12934133 irredundant clauses
c [unhide-6-6] 43 units, 23 failed, 2023 tauts, 0 hbrs, 143436 literals
c [block-2] 332 variables 0% will be scheduled this time
c [block-2] scheduled 332 variables 0%
c [block-2] limit of 30852930 steps penalty 4 = 0 + 4
c [block-2] fully completed
c [block-2] transition to [ all 0 rem 0 ] state
c [block-2] eliminated 0 blocked clauses
c [bca-2] limit of 10000000 steps and 26512434 added (scaled 2)
c [bca-2] 908518 out of 939118 literals actually usable 97%
c [bca-2] added 1093 blocked clauses in 4126372 steps
c [sweep-2] limit 25862080 based on 12931040 irredundant clauses
c [sweep-2-1] 3893 pos 0.8% + 465378 neg 99.2% = 469271 sched 99.9% ret 287
c [sweep-2-1] 27285848 steps 22 queries 56413.50 avg class size
c [sweep-2-1] 672 decisions 14 SAT calls 220.21 avg env size
c [sweep-2-1] 469177 variables remain 100% (381 retained 0%)
c [decomp-12] removed 51 variables
c [sweep-2-1] removed 51 vars (0 failed, 7 eqs, 16 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 51 vars in TOTAL (1 rounds, 21 queries)
c [sort-queue-6] sorted 407415 enqueued variables after 85336 conflicts
c [score-dist-6] active 62092 (13%), one 0 (0%), zero 407415 (87%)
c [score-dist-6] max exp 533, different 32 (6%)
c [score-dist-6] median active exp 517, avg 517.9
c [simplification-6] removed 143 variables 0.0% (469507 remain 90%)
c [simplification-6] removed 3550 irredundant clauses 0.0% (12930583 remain 97%)
c [simplification-6] maximum reduction of 0% = max (0%, 0%)
c [simplification-6] full geometric conflict interval increment 33333
c [simplification-6] new conflict interval 66666
c [simplification-6] penalized conflict interval 66666 = 1 * 66666
c [simplification-6] hard conflict limit 185335 (soft 152002 + delta 33333)
c [simplification-6] new conflict limit 152002 (hard 185335)
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 -  547.6  469507 12930583     96727   31192  14668 1504812   20   377  611   5%    786  120   16   80   21%
c 
c [simplification-7] limit 152002 conflicts (hard 185335) hit after 152003 conflicts
c [quatres-3] found 80830 quaternary clauses 15% in total
c [quatres-3-2] added 2688 quaternary resolvents
c [ternres-3] limit 51722328 based on 12930582 irredundant clauses
c [ternres-3] 451683 schedulable variables 96%
c [ternres-3] 5062 ternary resolvents (2 bin, 5060 trn)
c [ternres-3] 429679 variables remain 92% (39828 retained 8%)
c [gauss-2] limit 6465291 based on 12930582 irredundant clauses
c [gauss-2] extracted 0 xors of average arity 0.0
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [unhide-7] limit 808161 based on 12930582 irredundant clauses
c [unhide-7-7] 0 units, 5 failed, 18789 tauts, 0 hbrs, 61289 literals
c [transred-2] limit 12911826 based on 12911826 irredundant clauses
c [transred-2] removed 29 transitive binary clauses
c [transred-2] found 4 units
c [cce-2] limit of 12911826 steps based on 12911826 irredundant clauses
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] allowing another 6455913 steps for small clauses
c [cce-2-1] scheduling 10725539 clauses = 8072670 binary + 2652869 ternary
c [cce-2-1] tried to eliminate 190 small clauses 0%
c [cce-2-1] eliminated 23 binary clauses 0%
c [cce-2-1] eliminated 23 small clauses 0%
c [cce-2-1] eliminated 183 small clauses in 12911842 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 183 covered clauses in round 1
c [cce-2] eliminated 183 covered clauses in TOTAL during 1 rounds
c [cce-2] 183 < 1/100 * 12911826 = 129118 considered unsuccessful
c [elim-6] 50290 variables 11% will be scheduled this time
c [elim-6] scheduled 50290 variables 11%
c [elim-6] limit of 25000000 steps penalty 5 = 1 + 4
c [elim-6] rescheduling of touched variables disabled
c [elim-6] incomplete 48883 not tried 10% in round 1
c [elim-6] transition to [ all 0 rem 1 ] state
c [elim-6] eliminated 123 = 0% variables out of 50290 scheduled
c [elim-6] 123 < 1/100 * 50290 = 502 considered unsuccessful
c [bca-3] limit of 10000000 steps and 26472593 added (scaled 2)
c [bca-3] 908812 out of 938756 literals actually usable 97%
c [bca-3] added 38148 blocked clauses in 4197494 steps
c [sweep-3] limit 25821692 based on 12910846 irredundant clauses
c [sweep-3-1] 3903 pos 0.8% + 465100 neg 99.2% = 469003 sched 99.9% ret 374
c [sweep-3-1] 26427618 steps 25 queries 77713.40 avg class size
c [sweep-3-1] 1223 decisions 22 SAT calls 478.55 avg env size
c [sweep-3-1] 468757 variables remain 100% (620 retained 0%)
c [decomp-14] removed 14 variables
c [sweep-3-1] removed 14 vars (0 failed, 2 eqs, 5 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 14 vars in TOTAL (1 rounds, 24 queries)
c [sort-queue-7] sorted 404778 enqueued variables after 152003 conflicts
c [score-dist-7] active 64585 (14%), one 0 (0%), zero 404778 (86%)
c [score-dist-7] max exp 535, different 34 (6%)
c [score-dist-7] median active exp 518, avg 518.9
c [simplification-7] removed 144 variables 0.0% (469363 remain 90%)
c [simplification-7] removed 19761 irredundant clauses 0.2% (12910822 remain 97%)
c [simplification-7] maximum reduction of 0% = max (0%, 0%)
c [simplification-7] full geometric conflict interval increment 66666
c [simplification-7] new conflict interval 133332
c [simplification-7] penalized conflict interval 133332 = 1 * 133332
c [simplification-7] hard conflict limit 352001 (soft 285335 + delta 66666)
c [simplification-7] new conflict limit 285335 (hard 352001)
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 -  648.9  469363 12910822    172498   35403  19655 1527258  200   216  611  93%    949  -53  118  162   73%
c 
c [simplification-8] limit 285335 conflicts (hard 352001) hit after 285336 conflicts
c [quatres-4] found 83378 quaternary clauses 15% in total
c [quatres-4-2] added 22 single-self-subsuming ternary resolvents
c [quatres-4-2] added 2612 quaternary resolvents
c [ternres-4] limit 51643288 based on 12910822 irredundant clauses
c [ternres-4] 429551 schedulable variables 92%
c [ternres-4] 3750 ternary resolvents (16 bin, 3734 trn)
c [ternres-4] 421751 variables remain 90% (47612 retained 10%)
c [unhide-8] limit 806926 based on 12910822 irredundant clauses
c [unhide-8-8] 368 units, 32 failed, 512 tauts, 0 hbrs, 170274 literals
c [transred-3] limit 12910811 based on 12910811 irredundant clauses
c [transred-3] removed 23 transitive binary clauses
c [transred-3] found 2 units
c [block-3] scheduling all variables this time
c [block-3] scheduled 468963 variables 100%
c [block-3] limit of 25000000 steps penalty 5 = 1 + 4
c [block-3] incomplete 157502 not tried 34%
c [block-3] transition to [ all 1 rem 1 ] state
c [block-3] eliminated 4553 blocked clauses
c [block-3] 4553 < 1/100 * 12910811 = 129108 considered unsuccessful
c [bca-4] limit of 10000000 steps and 26474247 added (scaled 2)
c [bca-4] 902142 out of 937928 literals actually usable 96%
c [bca-4] added 3298 blocked clauses in 4102994 steps
c [sweep-4] limit 25804272 based on 12902136 irredundant clauses
c [sweep-4-1] 3837 pos 0.8% + 464508 neg 99.2% = 468345 sched 99.9% ret 618
c [sweep-4-1] 27030799 steps 22 queries 35438.59 avg class size
c [sweep-4-1] 888 decisions 21 SAT calls 434.57 avg env size
c [sweep-4-1] 468129 variables remain 100% (832 retained 0%)
c [decomp-16] removed 13 variables
c [sweep-4-1] removed 13 vars (0 failed, 1 eqs, 3 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 13 vars in TOTAL (1 rounds, 21 queries)
c [sort-queue-8] sorted 401240 enqueued variables after 285336 conflicts
c [score-dist-8] active 67710 (14%), one 0 (0%), zero 401240 (86%)
c [score-dist-8] max exp 537, different 36 (7%)
c [score-dist-8] median active exp 519, avg 520.5
c [simplification-8] removed 413 variables 0.1% (468950 remain 90%)
c [simplification-8] removed 8717 irredundant clauses 0.1% (12902105 remain 96%)
c [simplification-8] maximum reduction of 0% = max (0%, 0%)
c [simplification-8] full geometric conflict interval increment 133332
c [simplification-8] new conflict interval 266664
c [simplification-8] penalized conflict interval 266664 = 1 * 266664
c [simplification-8] hard conflict limit 685332 (soft 552000 + delta 133332)
c [simplification-8] new conflict limit 552000 (hard 685332)
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, 1342248 added (56641 skipped), 16564293 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: 3 bces, 185109 removed, 64909163 resolutions, 342169734 steps
c blkd: 14847 blocking literals 1%, 26 pure
c bump: 577931 bumped seen, 466562985 lits 807.3 on average
c card: 3 count, 0 units, 0 am1, 204849106 steps
c card: 0 rescheduled, 0 eliminated, 0 resolved, 113 subsumed
c card: 26 at-most-one constraints found, average size 3.12
c card: 26 at-most-one constraints used 100%, average size 3.12
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: 2 cces, 24 eliminated, 24 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: 52581154 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 41 gcs, 0 rescored clauses, 0 rescored vars
c dcps: 16 decompositions, 279 equivalent 0%
c deco: 472011 decision-only clauses 82%, 56% reduction
c decs: 7070085 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 6 elims, 45050 eliminated 9%, 0 pure 0%
c elms: 6 rounds, 1.0 rounds/bve
c elms: 22373 small 50%, 22651 large 50%
c elms: 24105 tried small, 22373 succeeded 93%, 1732 failed 7%
c elms: 3065 subsumed, 318070 strengthened, 0 blocked
c elms: 8638755 copies, 18947163 resolutions, 563220 ipos
c elms: 25656297 subchks, 10382400 strchks
c gaus: 2 extractions, 0 extracted, 0.0 size, 0 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 26155940 steps, 13077970 extr 50%, 0 elim 0%
c glue: 318.3 orig avg, 318.3 real avg, 11.1 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 113105 = 4510 simple 4% + 108460 trn 96% + 135 lrg 0%, 1910 sub 2%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 577930 clauses, 331.9 length
c lrnd: 191831371 lits = 422834087 orig - 231002716 removed 55%
c lrnd: 157334 uips 27%, 263405 flips 46%
c mins: 100554 mins 18%, 46 bin 0%, 576 size 0%
c mins: 10618033 poisoned searches, 3656108 hits, 34% hit rate
c mins: 20817597 used twice searches, 3724852 hits, 18% hit rate
c move: moved 183726, 176782 bin 96%, 6944 trn 4%
c otfs: 1307 driving 32%, 2817 restarting 68%
c otfs: str 4124, 4000 red 97%, 124 irr 3%
c otfs: str 4124, 0 bin 0%, 9 trn 0%, 4115 lrg 100%
c otfs: sub 352, 352 red 100%, 0 irr 0%
c otfs: sub 352, 0 bin 0%, 0 trn 0%, 352 lrg 100%
c phas: 1 computed, 516904 set, 0 pos (0%), 516904 neg (100%)
c prbs: 2 basic, 643 probed, 61 failed, 0 lifted
c prbs: 2 simple, 387548 probed, 0 failed, 0 eqs
c prbs: 2 treelook, 4 probed, 0 failed, 0 lifted
c prom: 427 locked 0% out of 160684 tried
c prps: 2077091040 props, 288 props/dec
c prps: 98% srch, 2% simp, 0% lkhd
c quat: 4 count, 14295 quat, 2142 self1, 0 self2, 1 dup
c queu: 8 sorted, 7070085 next (168245 steps 0.02)
c queu: 470496675 enq (706540923 steps 1.50), 466564331 deq 99%
c redc: 164 clauses 16%, 1040 tried 0%, 15 sat 1%
c redc: 741 lits 7%, 10944 tried 0%, 15 sat 0%
c redc: 37 times jump level reduced, 328.4 levels on average
c reds: 2 count, 289601.5 conflicts per reduce
c reds: 0 memlim 0%, 2 arith 100%
c reds: 50506 collected 93%, 3681 retired 7%
c rmbd: 2088 removed, 1229 red 59%
c rsts: 3174 restarts 35%, 5779 skipped 65%
c rsts: 5779 saturating 100%, 0 reuse 0%
c rsts: 0 kept 0.0% average 0.0%
c scnc: 0 count, 1.000 min (0/1000), 1.000 max (0/1000)
c simp: 8 count, 8 confs 100%, 0 vars 0%
c simp: 0 its 0%, 0 bin 0%, 0 trns 0%
c subl: 577930 count (1095019 tried 1.9), 471737 sub out of 577653 (81.7%)
c swps: 4 count, 4 rounds, 93 queries (23.2/round)
c swps: 81 sat calls, 1 unsat (0.4% success rate)
c swps: 3907 decisions 48.2, 35 conflicts 0.4
c swps; 54280.2 avg class size, 1299.5 avg environment size
c swps: 0 failed, 30 impls, 13 equivs
c swp0: 31 type 0 queries, 13 unsat (41.9%), 26 sat (83.9%)
c swp1: 62 type 1 queries, 21 unsat (33.9%), 54 sat (87.1%)
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: 15296161 calls to obtain time
c tops: 6868 fixed 1%, 0 its, 0.00 confs/it
c trds: 3 transitive reductions, 52 removed, 6 failed
c trds: 516 nodes, 2579 edges, 39073380 steps
c trim: 1663742 words, 6.3 MB
c trnr: 4 count, 18 bin, 17552 trn, 207723211 steps
c unhd: 8 count, 8 rounds, 161891027 steps
c unhd: 6 non-trivial sccs of average size 2.0
c unhd: 6730 units, 6730 bin, 0 trn, 0 lrg
c unhd: 79 failed, 74 stamp, 0 lits, 1 bin, 1 trn, 0 lrg
c unhd: 73497 tauts, 47 bin 0%, 2932 trn 4%, 15760 lrg 21%
c unhd: 73497 tauts, 54758 stamp 75%, 4477 red 6%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 728944 str, 6730 bin 1%, 1109 trn 0%, 721105 lrg 99%, 254716 red 35%
c vars: 468950 remaining 90% and 52197 removed 10% out of 521147
c vars: 6868 fixed 1%, 45050 eliminated 9%, 279 equivalent 0%
c vsts: 16053041776 visits, 99% srch, 1% simp, 0% lkhd
c vsts: 7.8 search visits per propagation, 27352.5 per conflict
c wchs: 1244423782 pushed, 107730679 enlarged, 65 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all         591948         50506          3681      14159658       7796945        274697
c 
c  0 0         14817   3         1   0         0   0   2155738  15    207220   3      1910   1     0.3
c  1 5           433   0         5   0        65   2    535794   4     44502   1       320   0     0.0
c  2 6          1524   0        26   0       146   4   1413244  10    432888   6      3107   1     0.1
c  3 9          3538   1       251   0       183   5   2066816  15    808362  10     10305   4     0.3
c  4 14        11762   2      1882   4       320   9   2093356  15<  1604019  21     16975   6     1.8
c  5 21        10928   2      3889   8       333   9   1788749  13   1517051  19     35026  13     1.6
c  6 30        11896   2      6066  12       286   8   1158604   8    925194  12<    10968   4     1.8
c  7 41        12586   2      7424  15       162   4    445255   3    350185   4     12681   5     2.6
c  8 54        12739   2      8580  17<      181   5<   297171   2    215722   3     14170   5     2.9
c  9 69        20263   3     15155  30       212   6    311464   2    208157   3     13990   5<    6.9
c 10 86        10203   2      4549   9        91   2    385864   3    324770   4     39625  14     4.0
c 11 126       31153   5<      733   1       380  10    952355   7    815963  10    111277  41     9.1
c 12 230      447012  76      1944   4      1320  36    550852   4    340732   4      4332   2   433.0
c 13 534        3094   1         1   0         2   0      4396   0      2180   0        11   0     5.5
c 
c avg                 10.8           7.9           8.4           4.5           5.8           8.5
c std                  2.7           1.9           3.6           3.4           3.0           2.9
c 
c  225.944  23% block
c   87.545   9% bump
c   78.664   8% elim
c   63.026   6% probe
c   35.358   4% unhide
c   29.404   3% bca
c   23.192   2% sweep
c   14.579   1% quatres
c    7.776   1% cce
c 
c   12.909 < 1% rest (below)
c 
c    5.492   1% decide
c    3.992   0% gauss
c    1.912   0% ternres
c    1.055   0% transred
c    0.458   0% card
c    0.000   0% locs
c    0.000   0% queuesort
c    0.000   0% rescore
c ==================================
c   21.193   2% preprocessing     4%
c  509.308  51% inprocessing     96%
c ==================================
c  530.501  54% simplifying
c  461.060  46% search
c ==================================
c  991.571 100% all
c 
c        579203 conflicts,         584.1 confs/sec
c           164 ternaries,        3531.7 confs/ternary
c            97 binaries,         5971.2 confs/binary
c             0 iterations,          0.0 confs/iteration
c 
c             2 reductions,          0.0 redus/sec, 289601.5 confs/reduction
c          3174 restarts,            3.2 rests/sec,    182.5 confs/restart
c       7070085 decisions,        7130.2 decis/sec,     12.2 decis/conflict
c    2077091040 propagations,  2094748.7 props/sec,    293.8 props/decision
c 
c 991.6 seconds, 1268.4 MB
c
c CAUGHT SIGNAL 15 SIGTERM
c
c launch: done
