c launch: /data/cnf/sc2014/app/velev-vliw-uns-2.0-uq5.cnf.bz2
c host: atom08
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/velev-vliw-uns-2.0-uq5.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/velev-vliw-uns-2.0-uq5.cnf.bz2
c no embedded options
c found 'p cnf 151669 2465731' header
c read 151669 variables, 2465731 clauses, 7141423 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 151668 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  151668  2465730         0       0      0     0    0     0   57   0%      0    0    0    0    0%
c 
c [simplification-1] limit 0 conflicts (hard 0) hit after 0 conflicts
c [card-1] limit 1000000 penalty 1 = 0 + 1
c [card-1] found 9 at-most-one constraints of average size 3.0
c [card-1] no at-most-two constraint found
c [card-1] using previous limit 1000000 for elimination
c [card-1] 9 out of 9 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 8 variables
c [simpleprobe-1] all 151661 free variables schedulable
c [simpleprobe-1] boosting simple probing limit by 10
c [simpleprobe-1] limit 10000000 penalty 1 = 0 + 1
c [decomp-2] removed 157 variables
c [simpleprobe-1] 134999 variables remain 89% (16505 retained 11%)
c [simpleprobe-1] removed 157 variables, found 9797 hbrs, 157 units
c [unhide-1] limit 153949 based on 2463187 irredundant clauses
c [unhide-1-1] 28 units, 3 failed, 3807 tauts, 0 hbrs, 17042 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 151474 variables 100%
c [elim-1] limit of 10000000 steps penalty 1 = 0 + 1
c [elim-1] rescheduling of touched variables disabled
c [elim-1] incomplete 149415 not tried 99% in round 1
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 2059 = 1% variables out of 151474 scheduled
c [elim-1] considered successful since not run to completion yet
c [phase-count-1] 2454585 negative 100.0% of 2455042 except 457 0.0%
c [phase-count-1] 659812 positive 26.9% of 2455042 except 1795230 73.1%
c [phase-count-1] less non-negative clauses 457 than limit 245500 (10.0%)
c [phase-count-1] non-pos/non-neg = 1795230/457 = 3928.29 >= 2.00 = 200/100
c [lucky-phase-1] forcing lucky phase -1
c [phase-1] phase bias: 0 positive 0%, 149415 negative 100%
c [sort-queue-1] sorted 149415 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 149415 (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 2246 variables 1.5% (149415 remain 99%)
c [simplification-1] removed 10688 irredundant clauses 0.4% (2455042 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 10002 conflicts
c [simpleprobe-2] 133150 schedulable variables 89%
c [simpleprobe-2] limit 9125455 penalty 1 = 0 + 1
c [decomp-4] removed 420 variables
c [simpleprobe-2] 134264 variables remain 90% (14731 retained 10%)
c [simpleprobe-2] removed 420 variables, found 13319 hbrs, 420 units
c [treelook-1] limit 612634 based on 2450536 irredundant clauses
c [treelook-1] scheduled 104285 literals 35%
c [treelook-1] scheduling used 612664 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 612634 based on 2450536 irredundant clauses
c [treelook-1] used 706728 steps
c [treelook-1] 104279 literals remain 35%
c [treelook-1] 101809 variables remain to probed next time 68%
c [treelook-1] removed 0 variables, found 54 hbrs
c [basicprobe-1] limit 19604288 based on 2450536 irredundant clauses
c [basicprobe-1-0] 145574 probes remain 99% after last round
c [basicprobe-1-0] 41 units = 41 failed (100%) + 0 lifted (0%)
c [basicprobe-1-0] removed 1611 variables, found 14211 hbrs
c [unhide-2] limit 153158 based on 2450536 irredundant clauses
c [unhide-2-2] 5016 units, 5 failed, 1553 tauts, 0 hbrs, 90132 literals
c [elim-2] 137877 variables 100% will be scheduled this time
c [elim-2] scheduled 137877 variables 100%
c [elim-2] limit of 45627277 steps penalty 1 = 0 + 1
c [elim-2] rescheduling of touched variables disabled
c [elim-2] incomplete 121461 not tried 88% in round 1
c [elim-2] transition to [ all 0 rem 1 ] state
c [elim-2] eliminated 16416 = 12% variables out of 137877 scheduled
c [elim-2] considered successful since not run to completion yet
c [sort-queue-2] sorted 73698 enqueued variables after 10002 conflicts
c [score-dist-2] active 47763 (39%), one 0 (0%), zero 73698 (61%)
c [score-dist-2] max exp 526, different 23 (4%)
c [score-dist-2] median active exp 516, avg 516.4
c [simplification-2] removed 27954 variables 18.7% (121461 remain 80%)
c [simplification-2] removed 247024 irredundant clauses 10.1% (2208018 remain 90%)
c [simplification-2] maximum reduction of 19% = max (19%, 10%)
c [simplification-2] large reduction 19% >= 5% limit
c [simplification-2] next conflict interval 2000 = 2000/1
c [simplification-2] penalized conflict interval 2000 = 1 * 2000
c [simplification-2] hard conflict limit 22002 (soft 12002 + delta 10000)
c [simplification-2] new conflict limit 12002 (hard 22002)
c 
c [simplification-3] limit 12002 conflicts (hard 22002) hit after 12005 conflicts
c [card-2] limit 688096 penalty 2 = 1 + 1
c [card-2] found 9 at-most-one constraints of average size 3.0
c [card-2] no at-most-two constraint found
c [card-2] using previous limit 688096 for elimination
c [card-2] 9 out of 9 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [decomp-6] removed 36 variables
c [unhide-3] limit 137997 based on 2207954 irredundant clauses
c [unhide-3-3] 333 units, 1 failed, 4600 tauts, 0 hbrs, 43921 literals
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 121091 variables 100%
c [elim-3] limit of 55047735 steps penalty 1 = 0 + 1
c [elim-3] rescheduling of touched variables disabled
c [elim-3] incomplete 85816 not tried 71% in round 1
c [elim-3] transition to [ all 1 rem 1 ] state
c [elim-3] eliminated 14661 = 12% variables out of 121091 scheduled
c [elim-3] considered successful since not run to completion yet
c [sort-queue-3] sorted 58148 enqueued variables after 12005 conflicts
c [score-dist-3] active 48282 (45%), one 0 (0%), zero 58148 (55%)
c [score-dist-3] max exp 527, different 24 (5%)
c [score-dist-3] median active exp 517, avg 517.0
c [simplification-3] removed 15031 variables 12.4% (106430 remain 70%)
c [simplification-3] removed 38764 irredundant clauses 1.8% (2169254 remain 88%)
c [simplification-3] maximum reduction of 12% = max (12%, 2%)
c [simplification-3] large reduction 12% >= 5% limit
c [simplification-3] next conflict interval 2000 = 2000/1
c [simplification-3] penalized conflict interval 2000 = 1 * 2000
c [simplification-3] hard conflict limit 24005 (soft 14005 + delta 10000)
c [simplification-3] new conflict limit 14005 (hard 24005)
c 
c [simplification-4] limit 14005 conflicts (hard 24005) hit after 14008 conflicts
c [decomp-7] removed 2 variables
c [treelook-2] limit 542279 based on 2169118 irredundant clauses
c [treelook-2] scheduled 87294 literals 41%
c [treelook-2] scheduling used 542296 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 542279 based on 2169118 irredundant clauses
c [treelook-2] used 1007154 steps
c [treelook-2] 87292 literals remain 41%
c [treelook-2] 72366 variables remain to probed next time 68%
c [treelook-2] removed 0 variables, found 42 hbrs
c [unhide-4] limit 162080 with penalty 3 = 0 + 3
c [unhide-4-4] 112 units, 4 failed, 483 tauts, 0 hbrs, 20335 literals
c [elim-4] 85728 variables 81% will be scheduled this time
c [elim-4] scheduled 85728 variables 81%
c [elim-4] boosting limit by 20
c [elim-4] limit of 1296643700 steps penalty 1 = 0 + 1
c [elim-4] rescheduling of touched variables disabled
c [elim-4-1] eliminated 6378 variables 6% in round 1 in 527943030 steps
c [elim-4-1] backward subsumption/strengthening limit 527943000
c [elim-4-1-1] backward checking 64191 touched variables 60%
c [elim-4-1-1] incomplete backward checking 64190 remain 100%
c [elim-4-1] subsumed 3 and strengthened 0 clauses in 527953138 steps
c [elim-4-1] rescheduled 5 variables 0% by backward subsumption
c [elim-4-2] no variable eliminated in round 2 in 1974 steps
c [elim-4] fully completed in 2 rounds
c [elim-4] transition to [ all 0 rem 0 ] state
c [elim-4] eliminated 6378 = 7% variables out of 85728 scheduled
c [sort-queue-4] sorted 51386 enqueued variables after 14008 conflicts
c [score-dist-4] active 48550 (49%), one 0 (0%), zero 51386 (51%)
c [score-dist-4] max exp 527, different 24 (5%)
c [score-dist-4] median active exp 517, avg 517.4
c [simplification-4] removed 6494 variables 6.1% (99936 remain 66%)
c [simplification-4] removed 85504 irredundant clauses 3.9% (2083750 remain 85%)
c [simplification-4] maximum reduction of 6% = max (6%, 4%)
c [simplification-4] large reduction 6% >= 5% limit
c [simplification-4] next conflict interval 2000 = 2000/1
c [simplification-4] penalized conflict interval 2000 = 1 * 2000
c [simplification-4] hard conflict limit 26008 (soft 16008 + delta 10000)
c [simplification-4] new conflict limit 16008 (hard 26008)
c 
c [simplification-5] limit 16008 conflicts (hard 26008) hit after 16009 conflicts
c [quatres-1] found 24329 quaternary clauses 15% in total
c [quatres-1-2] added 34 single-self-subsuming ternary resolvents
c [quatres-1-2] added 1497 quaternary resolvents
c [ternres-1] boosting ternary resolution limit by 5
c [ternres-1] limit 17397385 with penalty 1 = 0 + 1
c [ternres-1] all 99936 free variables schedulable
c [ternres-1] 33500 ternary resolvents (0 bin, 33500 trn)
c [ternres-1] 4511 variables remain 5% (95425 retained 95%)
c [gauss-1] limit 1041874 based on 2083748 irredundant clauses
c [gauss-1] extracted 8 xors of average arity 2.0
c [gauss-1] connected 16 occurrences of 14 variables (average 1.1)
c [gauss-1] limit 1041874 based on 2083748 irredundant clauses
c [gauss-1] fully completed
c [gauss-1] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-9] removed 54 variables
c [basicprobe-2] limit 17397385 penalty 1 = 0 + 1
c [basicprobe-2-0] 89200 probes remain 95% after last round
c [basicprobe-2-0] 49 units = 49 failed (100%) + 0 lifted (0%)
c [basicprobe-2-0] removed 5616 variables, found 8332 hbrs
c [unhide-5] limit 173973 with penalty 3 = 0 + 3
c [unhide-5-5] 342 units, 5 failed, 22924 tauts, 0 hbrs, 34307 literals
c [transred-1] limit 2000000 with penalty 0 = 0 + 0
c [transred-1] removed 1 transitive binary clauses
c [block-1] scheduling all variables this time
c [block-1] scheduled 93890 variables 100%
c [block-1] boosting limit by 10
c [block-1] limit of 695895410 steps penalty 0 = 0 + 0
c [block-1] fully completed
c [block-1] transition to [ all 0 rem 0 ] state
c [block-1] eliminated 227798 blocked clauses
c [cce-1] limit of 34794770 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 1 clauses out of 1 (100%) of length 122
c [cce-1-1] eliminated 1 clauses out of 3 (33%) of length 116
c [cce-1-1] eliminated 4 clauses out of 7 (57%) of length 114
c [cce-1-1] eliminated 1 clauses out of 1 (100%) of length 113
c [cce-1-1] eliminated 6 clauses out of 14 (43%) of length 112
c [cce-1-1] eliminated 1 clauses out of 2 (50%) of length 111
c [cce-1-1] eliminated 3 clauses out of 15 (20%) of length 110
c [cce-1-1] eliminated 2 clauses out of 12 (17%) of length 108
c [cce-1-1] eliminated 4 clauses out of 35 (11%) of length 107
c [cce-1-1] eliminated 4 clauses out of 21 (19%) of length 106
c [cce-1-1] eliminated 6 clauses out of 35 (17%) of length 105
c [cce-1-1] eliminated 11 clauses out of 46 (24%) of length 104
c [cce-1-1] eliminated 2 clauses out of 35 (6%) of length 103
c [cce-1-1] eliminated 7 clauses out of 39 (18%) of length 102
c [cce-1-1] eliminated 4 clauses out of 64 (6%) of length 101
c [cce-1-1] eliminated 5 clauses out of 32 (16%) of length 100
c [cce-1-1] eliminated 11 clauses out of 47 (23%) of length 99
c [cce-1-1] eliminated 2 clauses out of 72 (3%) of length 98
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 75 large clauses in 34794911 steps
c [cce-1-1] allowing another 17397455 steps for small clauses
c [cce-1-1] scheduling 1578726 clauses = 1523283 binary + 55443 ternary
c [cce-1-1] tried to eliminate 133 small clauses 0%
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 75 covered clauses in round 1
c [cce-1] eliminated 75 covered clauses in TOTAL during 1 rounds
c [cce-1] 75 < 1/100 * 1726460 = 17264 considered unsuccessful
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 90791 variables 100%
c [elim-5] limit of 139179082 steps penalty 0 = 0 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5] incomplete 26388 not tried 29% in round 1
c [elim-5] transition to [ all 1 rem 1 ] state
c [elim-5] eliminated 7697 = 8% variables out of 90791 scheduled
c [bca-1] limit of 10000000 steps and 3356218 added (scaled 2)
c [bca-1] 147152 out of 166190 literals actually usable 89%
c [bca-1] added 22809 blocked clauses in 576072 steps
c [sweep-1] limit 3355718 based on 1677859 irredundant clauses
c [sweep-1-1] 8457 pos 10.2% + 74637 neg 89.8% = 83094 sched 100.0% ret 0
c [sweep-1-1] 3595825 steps 22 queries 9395.09 avg class size
c [sweep-1-1] 730 decisions 18 SAT calls 268.78 avg env size
c [sweep-1-1] 82083 variables remain 100% (194 retained 0%)
c [decomp-10] removed 1571 variables
c [sweep-1-1] removed 1571 vars (0 failed, 4 eqs, 8 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 1571 vars in TOTAL (1 rounds, 21 queries)
c [sort-queue-5] sorted 41239 enqueued variables after 16009 conflicts
c [score-dist-5] active 40284 (49%), one 0 (0%), zero 41239 (51%)
c [score-dist-5] max exp 528, different 25 (5%)
c [score-dist-5] median active exp 517, avg 517.5
c [simplification-5] removed 18413 variables 18.4% (81523 remain 54%)
c [simplification-5] removed 429203 irredundant clauses 20.6% (1654547 remain 67%)
c [simplification-5] maximum reduction of 21% = max (18%, 21%)
c [simplification-5] large reduction 21% >= 5% limit
c [simplification-5] next conflict interval 2000 = 2000/1
c [simplification-5] penalized conflict interval 2000 = 1 * 2000
c [simplification-5] hard conflict limit 28009 (soft 18009 + delta 10000)
c [simplification-5] new conflict limit 18009 (hard 28009)
c 
c [simplification-6] limit 18009 conflicts (hard 28009) hit after 18009 conflicts
c [quatres-2] found 20154 quaternary clauses 16% in total
c [quatres-2-2] added 2112 single-self-subsuming ternary resolvents
c [quatres-2-2] added 1177 quaternary resolvents
c [ternres-2] limit 7449913 with penalty 0 = 0 + 0
c [ternres-2] 4202 schedulable variables 5%
c [ternres-2] 12731 ternary resolvents (0 bin, 12731 trn)
c [ternres-2] 1813 variables remain 2% (79710 retained 98%)
c [card-3] limit 931239 penalty 2 = 2 + 0
c [card-3] found 18 at-most-one constraints of average size 3.0
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 931239 for elimination
c [card-3] 18 out of 18 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [simpleprobe-3] 73374 schedulable variables 90%
c [simpleprobe-3] limit 29799652 penalty 0 = 0 + 0
c [decomp-12] removed 290 variables
c [simpleprobe-3] 61625 variables remain 76% (19608 retained 24%)
c [simpleprobe-3] removed 290 variables, found 57256 hbrs, 290 units
c [unhide-6] limit 372495 with penalty 2 = 0 + 2
c [unhide-6-6] 447 units, 10 failed, 2072 tauts, 0 hbrs, 17680 literals
c [transred-2] limit 2000000 with penalty 0 = 0 + 0
c [transred-2] removed 4 transitive binary clauses
c [transred-2] found 1 units
c [block-2] scheduling all variables this time
c [block-2] scheduled 80778 variables 100%
c [block-2] limit of 74499132 steps penalty 0 = 0 + 0
c [block-2] fully completed
c [block-2] transition to [ all 0 rem 0 ] state
c [block-2] eliminated 16014 blocked clauses
c [block-2] 16014 < 1/100 * 1647949 = 16479 considered unsuccessful
c [elim-6] 26116 variables 32% will be scheduled this time
c [elim-6] scheduled 26116 variables 32%
c [elim-6] limit of 148998264 steps penalty 0 = 0 + 0
c [elim-6] rescheduling of touched variables disabled
c [elim-6] incomplete 5324 not tried 7% in round 1
c [elim-6] transition to [ all 0 rem 1 ] state
c [elim-6] eliminated 320 = 1% variables out of 26116 scheduled
c [elim-6] 320 < 1/100 * 26116 = 261 considered unsuccessful
c [bca-2] limit of 10000000 steps and 3239884 added (scaled 2)
c [bca-2] 139966 out of 160466 literals actually usable 87%
c [bca-2] added 10738 blocked clauses in 537455 steps
c [sweep-2] limit 3227980 based on 1613990 irredundant clauses
c [sweep-2-1] 7780 pos 9.7% + 72272 neg 90.3% = 80052 sched 99.8% ret 180
c [sweep-2-1] 3259378 steps 25 queries 12333.32 avg class size
c [sweep-2-1] 1006 decisions 24 SAT calls 136.21 avg env size
c [sweep-2-1] 79732 variables remain 99% (500 retained 1%)
c [decomp-13] removed 7 variables
c [sweep-2-1] removed 7 vars (0 failed, 0 eqs, 1 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 7 vars in TOTAL (1 rounds, 24 queries)
c [sort-queue-6] sorted 40126 enqueued variables after 18009 conflicts
c [score-dist-6] active 40099 (50%), one 0 (0%), zero 40126 (50%)
c [score-dist-6] max exp 528, different 25 (5%)
c [score-dist-6] median active exp 517, avg 517.6
c [simplification-6] removed 1298 variables 1.6% (80225 remain 53%)
c [simplification-6] removed 40574 irredundant clauses 2.5% (1613973 remain 65%)
c [simplification-6] maximum reduction of 2% = max (2%, 2%)
c [simplification-6] geometric conflict interval increment 6666 = 20000 / 3
c [simplification-6] new conflict interval 16666
c [simplification-6] penalized conflict interval 16666 = 1 * 16666
c [simplification-6] hard conflict limit 44675 (soft 34675 + delta 10000)
c [simplification-6] new conflict limit 34675 (hard 44675)
c 
c [simplification-7] limit 34675 conflicts (hard 44675) hit after 34675 conflicts
c [quatres-3] found 19812 quaternary clauses 16% in total
c [quatres-3-2] added 42 single-self-subsuming ternary resolvents
c [quatres-3-2] added 208 quaternary resolvents
c [ternres-3] limit 12678417 with penalty 0 = 0 + 0
c [ternres-3] 1808 schedulable variables 2%
c [ternres-3] 10213 ternary resolvents (3 bin, 10210 trn)
c [ternres-3] 612 variables remain 1% (79613 retained 99%)
c [gauss-2] limit 1267841 penalty 1 = 1 + 0
c [gauss-2] extracted 1 xors of average arity 3.0
c [gauss-2] connected 3 occurrences of 3 variables (average 1.0)
c [gauss-2] limit 1267841 penalty 1 = 1 + 0
c [gauss-2] fully completed
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [unhide-7] limit 316960 with penalty 3 = 0 + 3
c [unhide-7-7] 9 units, 0 failed, 16912 tauts, 0 hbrs, 48031 literals
c [transred-3] limit 2000000 with penalty 0 = 0 + 0
c [transred-3] removed 4 transitive binary clauses
c [cce-2] limit of 31696044 steps penalty 1 = 1 + 0
c [cce-2-1] eliminated 1 clauses out of 26 (4%) of length 105
c [cce-2-1] eliminated 4 clauses out of 37 (11%) of length 104
c [cce-2-1] eliminated 4 clauses out of 39 (10%) of length 102
c [cce-2-1] eliminated 8 clauses out of 61 (13%) of length 101
c [cce-2-1] eliminated 8 clauses out of 48 (17%) of length 99
c [cce-2-1] eliminated 4 clauses out of 43 (9%) of length 97
c [cce-2-1] eliminated 8 clauses out of 72 (11%) of length 96
c [cce-2-1] eliminated 6 clauses out of 113 (5%) of length 95
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] eliminated 43 large clauses in 31696107 steps
c [cce-2-1] allowing another 15848053 steps for small clauses
c [cce-2-1] scheduling 1429732 clauses = 1406870 binary + 22862 ternary
c [cce-2-1] tried to eliminate 143 small clauses 0%
c [cce-2-1] eliminated 33 binary clauses 0%
c [cce-2-1] eliminated 2 ternary clauses 0%
c [cce-2-1] eliminated 35 small clauses 0%
c [cce-2-1] eliminated 226 small clauses in 31698089 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 269 covered clauses in round 1
c [cce-2] eliminated 269 covered clauses in TOTAL during 1 rounds
c [cce-2] 269 < 1/100 * 1599361 = 15993 considered unsuccessful
c [bca-3] limit of 10000000 steps and 3215457 added (scaled 2)
c [bca-3] 135050 out of 160434 literals actually usable 84%
c [bca-3] added 432 blocked clauses in 513341 steps
c [sweep-3] limit 3803525 penalty 0 = 0 + 0
c [sweep-3-1] 5351 pos 6.7% + 74366 neg 93.3% = 79717 sched 99.4% ret 499
c [sweep-3-1] 3831578 steps 32 queries 9229.06 avg class size
c [sweep-3-1] 1393 decisions 27 SAT calls 182.85 avg env size
c [sweep-3-1] 79421 variables remain 99% (795 retained 1%)
c [decomp-15] removed 4 variables
c [sweep-3-1] removed 4 vars (0 failed, 4 eqs, 8 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 4 vars in TOTAL (1 rounds, 31 queries)
c [sort-queue-7] sorted 38811 enqueued variables after 34675 conflicts
c [score-dist-7] active 41401 (52%), one 0 (0%), zero 38811 (48%)
c [score-dist-7] max exp 530, different 27 (5%)
c [score-dist-7] median active exp 518, avg 518.7
c [simplification-7] removed 13 variables 0.0% (80212 remain 53%)
c [simplification-7] removed 14885 irredundant clauses 0.9% (1599088 remain 65%)
c [simplification-7] maximum reduction of 1% = max (0%, 1%)
c [simplification-7] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-7] new conflict interval 26666
c [simplification-7] penalized conflict interval 26666 = 1 * 26666
c [simplification-7] hard conflict limit 74674 (soft 61341 + delta 13333)
c [simplification-7] new conflict limit 61341 (hard 74674)
c 
c [simplification-8] limit 61341 conflicts (hard 74674) hit after 61341 conflicts
c [quatres-4] found 19528 quaternary clauses 16% in total
c [quatres-4-1] added 1 double-self-subsuming ternary resolvents
c [quatres-4-2] added 22 single-self-subsuming ternary resolvents
c [quatres-4-2] added 294 quaternary resolvents
c [ternres-4] limit 19271284 with penalty 0 = 0 + 0
c [ternres-4] 612 schedulable variables 1%
c [ternres-4] 5394 ternary resolvents (16 bin, 5378 trn)
c [ternres-4] 147 variables remain 0% (80065 retained 100%)
c [unhide-8] limit 481782 with penalty 3 = 0 + 3
c [unhide-8-8] 133 units, 24 failed, 2232 tauts, 0 hbrs, 78077 literals
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 5 transitive binary clauses
c [block-3] scheduling all variables this time
c [block-3] scheduled 80043 variables 100%
c [block-3] limit of 96356422 steps penalty 1 = 1 + 0
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 14911 blocked clauses
c [block-3] 14911 < 1/100 * 1598720 = 15987 considered unsuccessful
c [elim-7] scheduling all variables this time
c [elim-7] scheduled 79650 variables 100%
c [elim-7] limit of 192712844 steps penalty 1 = 1 + 0
c [elim-7] rescheduling of touched variables disabled
c [elim-7] incomplete 4199 not tried 5% in round 1
c [elim-7] transition to [ all 1 rem 1 ] state
c [elim-7] eliminated 1149 = 1% variables out of 79650 scheduled
c [bca-4] limit of 10000000 steps and 3152567 added (scaled 2)
c [bca-4] 124917 out of 157004 literals actually usable 80%
c [bca-4] added 1707 blocked clauses in 438474 steps
c [sweep-4] limit 5781385 penalty 0 = 0 + 0
c [sweep-4-1] 5469 pos 7.0% + 72310 neg 93.0% = 77779 sched 99.1% ret 722
c [sweep-4-1] 5926331 steps 38 queries 5719.00 avg class size
c [sweep-4-1] 1311 decisions 33 SAT calls 396.97 avg env size
c [sweep-4-1] 77403 variables remain 99% (1097 retained 1%)
c [decomp-17] removed 9 variables
c [sweep-4-1] removed 9 vars (0 failed, 4 eqs, 9 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 9 vars in TOTAL (1 rounds, 37 queries)
c [sort-queue-8] sorted 29118 enqueued variables after 61341 conflicts
c [score-dist-8] active 49374 (63%), one 0 (0%), zero 29118 (37%)
c [score-dist-8] max exp 532, different 29 (5%)
c [score-dist-8] median active exp 520, avg 520.1
c [simplification-8] removed 1720 variables 2.1% (78492 remain 52%)
c [simplification-8] removed 34672 irredundant clauses 2.2% (1564399 remain 63%)
c [simplification-8] maximum reduction of 2% = max (2%, 2%)
c [simplification-8] geometric conflict interval increment 8888 = 26666 / 3
c [simplification-8] new conflict interval 35554
c [simplification-8] penalized conflict interval 35554 = 1 * 35554
c [simplification-8] hard conflict limit 114672 (soft 96895 + delta 17777)
c [simplification-8] new conflict limit 96895 (hard 114672)
c 
c [simplification-9] limit 96895 conflicts (hard 114672) hit after 114672 conflicts
c [quatres-5] found 19111 quaternary clauses 16% in total
c [quatres-5-1] removed 1 duplicate quaternary clauses
c [quatres-5-2] added 255 quaternary resolvents
c [ternres-5] limit 24155750 with penalty 0 = 0 + 0
c [ternres-5] 147 schedulable variables 0%
c [ternres-5] 1176 ternary resolvents (3 bin, 1173 trn)
c [ternres-5] 7 variables remain 0% (78485 retained 100%)
c [treelook-3] limit 603893 penalty 2 = 2 + 0 boost 1
c [treelook-3] scheduled 68056 literals 43%
c [treelook-3] scheduling used 603937 steps
c [treelook-3] not fully scheduled
c [treelook-3] limit 603893 penalty 2 = 2 + 0 boost 1
c [treelook-3] used 677462 steps
c [treelook-3] 68052 literals remain 43%
c [treelook-3] 51011 variables remain to probed next time 65%
c [treelook-3] removed 0 variables, found 25 hbrs
c [unhide-9] limit 603893 with penalty 3 = 0 + 3
c [unhide-9-9] 0 units, 0 failed, 11934 tauts, 0 hbrs, 84193 literals
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 4 transitive binary clauses
c [transred-5] found 4 units
c [elim-8] 4182 variables 5% will be scheduled this time
c [elim-8] scheduled 4182 variables 5%
c [elim-8] boosting limit by 20
c [elim-8] limit of 9662300300 steps penalty 0 = 0 + 0
c [elim-8] rescheduling of touched variables disabled
c [elim-8-1] eliminated 1 variables 0% in round 1 in 453822538 steps
c [elim-8-1] backward subsumption/strengthening limit 453822500
c [elim-8-1-1] backward checking 10591 touched variables 13%
c [elim-8-1-1] incomplete backward checking 10685 remain 101%
c [elim-8-1] subsumed 0 and strengthened 160 clauses in 453823228 steps
c [elim-8-1] rescheduled 352 variables 0% by backward subsumption
c [elim-8-2] no variable eliminated in round 2 in 49968962 steps
c [elim-8] fully completed in 2 rounds
c [elim-8] transition to [ all 0 rem 0 ] state
c [elim-8] eliminated 2 = 0% variables out of 4182 scheduled
c [elim-8] 2 < 1/100 * 4182 = 41 considered unsuccessful
c [bca-5] limit of 10000000 steps and 3098875 added (scaled 2)
c [bca-5] 124769 out of 156974 literals actually usable 79%
c [bca-5] added 1714 blocked clauses in 441845 steps
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 72467250 penalty 0 = 0 + 0
c [sweep-5-1] 5428 pos 7.0% + 71967 neg 93.0% = 77395 sched 98.6% ret 1091
c [sweep-5-1] 72626378 steps 484 queries 1476.38 avg class size
c [sweep-5-1] 12292 decisions 430 SAT calls 134.07 avg env size
c [sweep-5-1] 61218 variables remain 79% (16394 retained 21%)
c [decomp-20] removed 956 variables
c [sweep-5-1] removed 956 vars (0 failed, 56 eqs, 124 impls)
c [sweep-5] considered successful since not run to completion yet
c [sweep-5] removed 956 vars in TOTAL (1 rounds, 483 queries)
c [sort-queue-9] sorted 28031 enqueued variables after 114672 conflicts
c [score-dist-9] active 49499 (64%), one 0 (0%), zero 28031 (36%)
c [score-dist-9] max exp 534, different 31 (6%)
c [score-dist-9] median active exp 520, avg 520.8
c [simplification-9] removed 962 variables 1.2% (77530 remain 51%)
c [simplification-9] removed 44539 irredundant clauses 2.8% (1519860 remain 62%)
c [simplification-9] maximum reduction of 3% = max (1%, 3%)
c [simplification-9] geometric conflict interval increment 8888 = 35554 / 4
c [simplification-9] new conflict interval 44442
c [simplification-9] penalized conflict interval 44442 = 1 * 44442
c [simplification-9] hard conflict limit 181335 (soft 159114 + delta 22221)
c [simplification-9] new conflict limit 159114 (hard 181335)
c 
c [simplification-10] limit 159114 conflicts (hard 181335) hit after 181335 conflicts
c [quatres-6] found 16949 quaternary clauses 16% in total
c [quatres-6-1] removed 3 duplicate quaternary clauses
c [quatres-6-2] added 46 single-self-subsuming ternary resolvents
c [quatres-6-2] added 340 quaternary resolvents
c [ternres-6] limit 27871129 with penalty 0 = 0 + 0
c [ternres-6] 7 schedulable variables 0%
c [ternres-6] 379 ternary resolvents (0 bin, 379 trn)
c [ternres-6] fully completed ternary resolution
c [card-4] limit 1741945 penalty 3 = 3 + 0
c [card-4] found 24 at-most-one constraints of average size 3.4
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 1741945 for elimination
c [card-4] 24 out of 24 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [gauss-3] limit 1393556 penalty 2 = 2 + 0
c [gauss-3] extracted 1 xors of average arity 2.0
c [gauss-3] connected 2 occurrences of 2 variables (average 1.0)
c [gauss-3] limit 1393556 penalty 2 = 2 + 0
c [gauss-3] fully completed
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [basicprobe-3] limit 139355647 penalty 0 = 0 + 0
c [basicprobe-3-0] 68394 probes remain 88% after last round
c [basicprobe-3-0] 186 units = 186 failed (100%) + 0 lifted (0%)
c [basicprobe-3-0] removed 188 variables, found 21274 hbrs
c [bate-1] eliminated 7 asymmetric tautologies during probing
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 3 transitive binary clauses
c [cce-3] limit of 34838911 steps penalty 2 = 2 + 0
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 116
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 1 large clauses in 34838915 steps
c [cce-3-1] allowing another 17419457 steps for small clauses
c [cce-3-1] scheduling 1394576 clauses = 1348826 binary + 45750 ternary
c [cce-3-1] tried to eliminate 255 small clauses 0%
c [cce-3-1] eliminated 57 binary clauses 0%
c [cce-3-1] eliminated 57 small clauses 0%
c [cce-3-1] eliminated 2557 small clauses in 34838913 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 2558 covered clauses in round 1
c [cce-3] eliminated 2558 covered clauses in TOTAL during 1 rounds
c [cce-3] 2558 < 1/100 * 1519852 = 15198 considered unsuccessful
c [bca-6] limit of 10000000 steps and 3053788 added (scaled 2)
c [bca-6] 122246 out of 154686 literals actually usable 79%
c [bca-6] added 204 blocked clauses in 436885 steps
c [sweep-6] limit 8361338 penalty 0 = 0 + 0
c [sweep-6-1] 4071 pos 6.7% + 56939 neg 93.3% = 61010 sched 78.9% ret 16332
c [sweep-6-1] 8423499 steps 61 queries 4466.77 avg class size
c [sweep-6-1] 1618 decisions 48 SAT calls 164.77 avg env size
c [sweep-6-1] 60712 variables remain 79% (16628 retained 21%)
c [decomp-22] removed 44 variables
c [sweep-6-1] removed 44 vars (0 failed, 13 eqs, 19 impls)
c [sweep-6] considered successful since not run to completion yet
c [sweep-6] removed 44 vars in TOTAL (1 rounds, 60 queries)
c [sort-queue-10] sorted 27857 enqueued variables after 181335 conflicts
c [score-dist-10] active 49441 (64%), one 0 (0%), zero 27857 (36%)
c [score-dist-10] max exp 535, different 32 (6%)
c [score-dist-10] median active exp 520, avg 521.1
c [simplification-10] removed 232 variables 0.3% (77298 remain 51%)
c [simplification-10] removed 2679 irredundant clauses 0.2% (1517181 remain 62%)
c [simplification-10] maximum reduction of 0% = max (0%, 0%)
c [simplification-10] full geometric conflict interval increment 44442
c [simplification-10] new conflict interval 88884
c [simplification-10] penalized conflict interval 88884 = 1 * 88884
c [simplification-10] hard conflict limit 314661 (soft 270219 + delta 44442)
c [simplification-10] new conflict limit 270219 (hard 314661)
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 -  234.6   77298  1517181    217595   24837  47637 124057  203   238   84  85%    986  -11  118  203   58%
c 
c [simplification-11] limit 270219 conflicts (hard 314661) hit after 275654 conflicts
c [quatres-7] found 17186 quaternary clauses 16% in total
c [quatres-7-2] added 276 single-self-subsuming ternary resolvents
c [quatres-7-2] added 117 quaternary resolvents
c [ternres-7] limit 30677460 with penalty 0 = 0 + 0
c [ternres-7] all 77298 free variables schedulable
c [ternres-7] 1596 ternary resolvents (0 bin, 1596 trn)
c [ternres-7] 31896 variables remain 41% (45402 retained 59%)
c [simpleprobe-4] 58587 schedulable variables 76%
c [simpleprobe-4] limit 122709841 penalty 0 = 0 + 0
c [decomp-24] removed 4534 variables
c [simpleprobe-4] 47644 variables remain 65% (25120 retained 35%)
c [simpleprobe-4] removed 4534 variables, found 114858 hbrs, 3098 units
c [unhide-10] limit 383468 with penalty 4 = 1 + 3
c [unhide-10-10] 436 units, 14 failed, 12404 tauts, 0 hbrs, 124136 literals
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 8 transitive binary clauses
c [block-4] scheduling all variables this time
c [block-4] scheduled 72317 variables 100%
c [block-4] limit of 76693650 steps penalty 2 = 2 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 54993 blocked clauses
c [elim-9] scheduling all variables this time
c [elim-9] scheduled 71406 variables 100%
c [elim-9] limit of 306774602 steps penalty 1 = 1 + 0
c [elim-9] rescheduling of touched variables disabled
c [elim-9] incomplete 2137 not tried 3% in round 1
c [elim-9] transition to [ all 1 rem 1 ] state
c [elim-9] eliminated 2960 = 4% variables out of 71406 scheduled
c [bca-7] limit of 10000000 steps and 2790616 added (scaled 2)
c [bca-7] 113873 out of 136894 literals actually usable 83%
c [bca-7] added 3878 blocked clauses in 427269 steps
c [sweep-7] limit 9203238 penalty 0 = 0 + 0
c [sweep-7-1] 3548 pos 6.7% + 49283 neg 93.3% = 52831 sched 77.2% ret 15615
c [sweep-7-1] 9205291 steps 61 queries 3740.61 avg class size
c [sweep-7-1] 1810 decisions 58 SAT calls 99.79 avg env size
c [sweep-7-1] 52222 variables remain 76% (16224 retained 24%)
c [decomp-25] removed 6 variables
c [sweep-7-1] removed 6 vars (0 failed, 2 eqs, 11 impls)
c [sweep-7] 6 < 1/1000 * 68446 = 68 considered unsuccessful
c [sweep-7] removed 6 vars in TOTAL (1 rounds, 60 queries)
c [sort-queue-11] sorted 24175 enqueued variables after 275654 conflicts
c [score-dist-11] active 44265 (65%), one 0 (0%), zero 24175 (35%)
c [score-dist-11] max exp 537, different 34 (6%)
c [score-dist-11] median active exp 520, avg 521.2
c [simplification-11] removed 8858 variables 11.5% (68440 remain 45%)
c [simplification-11] removed 131530 irredundant clauses 8.7% (1385651 remain 56%)
c [simplification-11] maximum reduction of 11% = max (11%, 9%)
c [simplification-11] large reduction 11% >= 5% limit
c [simplification-11] next conflict interval 2756 = min (275654/100, 88884)
c [simplification-11] penalized conflict interval 2756 = 1 * 2756
c [simplification-11] hard conflict limit 288410 (soft 278410 + delta 10000)
c [simplification-11] new conflict limit 278410 (hard 288410)
c 
c [simplification-12] limit 278410 conflicts (hard 288410) hit after 283674 conflicts
c [quatres-8] found 16713 quaternary clauses 16% in total
c [quatres-8-1] removed 3 duplicate quaternary clauses
c [quatres-8-2] added 20 single-self-subsuming ternary resolvents
c [quatres-8-2] added 192 quaternary resolvents
c [ternres-8] limit 31018533 with penalty 0 = 0 + 0
c [ternres-8] 28300 schedulable variables 41%
c [ternres-8] 1889 ternary resolvents (0 bin, 1889 trn)
c [ternres-8] 148 variables remain 0% (68292 retained 100%)
c [unhide-11] limit 775463 with penalty 3 = 0 + 3
c [unhide-11-11] 2 units, 0 failed, 7911 tauts, 0 hbrs, 26655 literals
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 9 transitive binary clauses
c [elim-10] 2136 variables 3% will be scheduled this time
c [elim-10] scheduled 2136 variables 3%
c [elim-10] limit of 620370660 steps penalty 0 = 0 + 0
c [elim-10] rescheduling of touched variables disabled
c [elim-10] incomplete 40 not tried 0% in round 1
c [elim-10] transition to [ all 0 rem 1 ] state
c [elim-10] eliminated 0 = 0% variables out of 2136 scheduled
c [bca-8] limit of 10000000 steps and 2762813 added (scaled 2)
c [bca-8] 113702 out of 136868 literals actually usable 83%
c [bca-8] added 481 blocked clauses in 418049 steps
c [sort-queue-12] sorted 24167 enqueued variables after 283674 conflicts
c [score-dist-12] active 44266 (65%), one 0 (0%), zero 24167 (35%)
c [score-dist-12] max exp 537, different 34 (6%)
c [score-dist-12] median active exp 520, avg 521.3
c [simplification-12] removed 7 variables 0.0% (68433 remain 45%)
c [simplification-12] removed 14865 irredundant clauses 1.1% (1370786 remain 56%)
c [simplification-12] maximum reduction of 1% = max (0%, 1%)
c [simplification-12] geometric conflict interval increment 44442 = 88884 / 2
c [simplification-12] new conflict interval 133326
c [simplification-12] penalized conflict interval 133326 = 1 * 133326
c [simplification-12] hard conflict limit 483663 (soft 417000 + delta 66663)
c [simplification-12] new conflict limit 417000 (hard 483663)
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 -  291.1   68433  1370786    325027   26200  47958 142320  189   239   81  79%   1017    2  218  201  109%
c -  303.3   68433  1370786    367699   27435  47958 142323   85   259   82  33%   1020   23   85  175   49%
c 
c [simplification-13] limit 417000 conflicts (hard 483663) hit after 417001 conflicts
c [quatres-9] found 16605 quaternary clauses 17% in total
c [quatres-9-1] added 1 double-self-subsuming ternary resolvents
c [quatres-9-2] added 20 single-self-subsuming ternary resolvents
c [quatres-9-2] added 90 quaternary resolvents
c [ternres-9] limit 40255694 with penalty 0 = 0 + 0
c [ternres-9] 148 schedulable variables 0%
c [ternres-9] 336 ternary resolvents (1 bin, 335 trn)
c [ternres-9] fully completed ternary resolution
c [unhide-12] limit 1006392 with penalty 3 = 0 + 3
c [unhide-12-12] 28 units, 10 failed, 1227 tauts, 0 hbrs, 87078 literals
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 1 transitive binary clauses
c [block-5] scheduling all variables this time
c [block-5] scheduled 68396 variables 100%
c [block-5] limit of 201278474 steps penalty 1 = 1 + 0
c [block-5] fully completed
c [block-5] transition to [ all 0 rem 0 ] state
c [block-5] eliminated 3990 blocked clauses
c [block-5] 3990 < 1/100 * 1370770 = 13707 considered unsuccessful
c [bca-9] limit of 10000000 steps and 2754475 added (scaled 2)
c [bca-9] 113718 out of 136544 literals actually usable 83%
c [bca-9] added 1932 blocked clauses in 432223 steps
c [sweep-8] limit 6038354 penalty 1 = 1 + 0
c [sweep-8-1] 3277 pos 6.3% + 48833 neg 93.7% = 52110 sched 76.3% ret 16161
c [sweep-8-1] 6441421 steps 42 queries 5622.90 avg class size
c [sweep-8-1] 1216 decisions 38 SAT calls 119.13 avg env size
c [sweep-8-1] 51859 variables remain 76% (16412 retained 24%)
c [decomp-28] removed 8 variables
c [sweep-8-1] removed 8 vars (0 failed, 3 eqs, 10 impls)
c [sweep-8] 8 < 1/1000 * 68271 = 68 considered unsuccessful
c [sweep-8] removed 8 vars in TOTAL (1 rounds, 41 queries)
c [sort-queue-13] sorted 23875 enqueued variables after 417001 conflicts
c [score-dist-13] active 44388 (65%), one 0 (0%), zero 23875 (35%)
c [score-dist-13] max exp 538, different 35 (6%)
c [score-dist-13] median active exp 520, avg 521.7
c [simplification-13] removed 170 variables 0.2% (68263 remain 45%)
c [simplification-13] removed 4300 irredundant clauses 0.3% (1366486 remain 55%)
c [simplification-13] maximum reduction of 0% = max (0%, 0%)
c [simplification-13] full geometric conflict interval increment 133326
c [simplification-13] new conflict interval 266652
c [simplification-13] penalized conflict interval 266652 = 1 * 266652
c [simplification-13] hard conflict limit 816979 (soft 683653 + delta 133326)
c [simplification-13] new conflict limit 683653 (hard 816979)
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 -  325.8   68263  1366486    429771   23904  48304 144133  150   224   81  67%   1023  -15  208  162  128%
c -  347.0   68263  1366486    519231   26242  48305 144134  137   223   83  62%   1024  -11   92  171   53%
c -  366.6   68263  1366486    604555   26265  48305 144134  111   280   83  40%   1024   45   87  171   51%
c 
c [simplification-14] limit 683653 conflicts (hard 816979) hit after 688808 conflicts
c [quatres-10] found 16886 quaternary clauses 17% in total
c [quatres-10-2] added 90 quaternary resolvents
c [ternres-10] limit 53347599 with penalty 0 = 0 + 0
c [ternres-10] all 68263 free variables schedulable
c [ternres-10] 686 ternary resolvents (1 bin, 685 trn)
c [ternres-10] 43 variables remain 0% (68220 retained 100%)
c [gauss-4] limit 1333689 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 [unhide-13] limit 1333689 with penalty 3 = 0 + 3
c [unhide-13-13] 0 units, 0 failed, 5709 tauts, 0 hbrs, 12307 literals
c [transred-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 7 transitive binary clauses
c [cce-4] boosting limit by 10
c [cce-4] limit of 333422497 steps penalty 3 = 3 + 0
c [cce-4-1] eliminated 4 clauses out of 82 (5%) of length 92
c [cce-4-1] eliminated 8 clauses out of 109 (7%) of length 90
c [cce-4-1] eliminated 12 clauses out of 96 (12%) of length 88
c [cce-4-1] eliminated 24 clauses out of 123 (20%) of length 87
c [cce-4-1] eliminated 20 clauses out of 123 (16%) of length 85
c [cce-4-1] eliminated 4 clauses out of 133 (3%) of length 84
c [cce-4-1] eliminated 4 clauses out of 180 (2%) of length 83
c [cce-4-1] eliminated 20 clauses out of 148 (14%) of length 82
c [cce-4-1] eliminated 24 clauses out of 174 (14%) of length 80
c [cce-4-1] eliminated 12 clauses out of 176 (7%) of length 78
c [cce-4-1] eliminated 4 clauses out of 207 (2%) of length 77
c [cce-4-1] eliminated 12 clauses out of 165 (7%) of length 76
c [cce-4-1] eliminated 25 clauses out of 191 (13%) of length 75
c [cce-4-1] eliminated 6 clauses out of 237 (3%) of length 74
c [cce-4-1] eliminated 4 clauses out of 145 (3%) of length 73
c [cce-4-1] eliminated 12 clauses out of 221 (5%) of length 72
c [cce-4-1] eliminated 11 clauses out of 234 (5%) of length 71
c [cce-4-1] eliminated 20 clauses out of 237 (8%) of length 70
c [cce-4-1] eliminated 25 clauses out of 265 (9%) of length 68
c [cce-4-1] eliminated 27 clauses out of 208 (13%) of length 67
c [cce-4-1] eliminated 44 clauses out of 473 (9%) of length 66
c [cce-4-1] eliminated 4 clauses out of 231 (2%) of length 65
c [cce-4-1] incomplete large round (ATE)
c [cce-4-1] eliminated 326 large clauses in 333428011 steps
c [cce-4-1] allowing another 166714005 steps for small clauses
c [cce-4-1] scheduling 1247789 clauses = 1205754 binary + 42035 ternary
c [cce-4-1] tried to eliminate 2713 small clauses 0%
c [cce-4-1] eliminated 211 binary clauses 0%
c [cce-4-1] eliminated 17 ternary clauses 0%
c [cce-4-1] eliminated 228 small clauses 0%
c [cce-4-1] eliminated 228 small clauses in 333422499 steps
c [cce-4-1] incomplete small round (ATE)
c [cce-4-1] eliminated 554 covered clauses in round 1
c [cce-4] eliminated 554 covered clauses in TOTAL during 1 rounds
c [cce-4] 554 < 1/100 * 1360872 = 13608 considered unsuccessful
c [elim-11] scheduling all variables this time
c [elim-11] scheduled 68263 variables 100%
c [elim-11] limit of 400000000 steps penalty 1 = 1 + 0
c [elim-11] rescheduling of touched variables disabled
c [elim-11] incomplete 980 not tried 1% in round 1
c [elim-11] transition to [ all 1 rem 1 ] state
c [elim-11] eliminated 613 = 1% variables out of 68263 scheduled
c [elim-11] 613 < 1/100 * 68263 = 682 considered unsuccessful
c [bca-10] limit of 10000000 steps and 2738677 added (scaled 2)
c [bca-10] 118710 out of 135302 literals actually usable 88%
c [bca-10] added 823 blocked clauses in 464035 steps
c [sort-queue-14] sorted 23372 enqueued variables after 688808 conflicts
c [score-dist-14] active 44278 (65%), one 0 (0%), zero 23372 (35%)
c [score-dist-14] max exp 539, different 36 (7%)
c [score-dist-14] median active exp 521, avg 522.3
c [simplification-14] removed 613 variables 0.9% (67650 remain 45%)
c [simplification-14] removed 8371 irredundant clauses 0.6% (1358115 remain 55%)
c [simplification-14] maximum reduction of 1% = max (1%, 1%)
c [simplification-14] geometric conflict interval increment 133326 = 266652 / 2
c [simplification-14] new conflict interval 399978
c [simplification-14] penalized conflict interval 399978 = 1 * 399978
c [simplification-14] hard conflict limit 1288775 (soft 1088786 + delta 199989)
c [simplification-14] new conflict limit 1088786 (hard 1288775)
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 -  400.3   67650  1358115    691166   27861  48426 112315  150   240   82  63%   1024   11   86  174   49%
c -  424.3   67650  1358115    801711   28209  48426 112315  151   227   84  66%   1024   10   77  181   42%
c -  438.0   67650  1358115    865053   30147  48426 112315  204   205   84 100%   1024  -17  204  164  124%
c -  455.8   67650  1358115    943560   29874  48426 112315   90   221   85  41%   1024    5   95  153   62%
c -  472.1   67650  1358115   1020244   27146  48426 112315  179   219   84  82%   1024    9  139  175   79%
c 
c [simplification-15] limit 1088786 conflicts (hard 1288775) hit after 1116285 conflicts
c [quatres-11] found 17876 quaternary clauses 18% in total
c [quatres-11-2] added 88 quaternary resolvents
c [ternres-11] limit 71452152 with penalty 0 = 0 + 0
c [ternres-11] 43 schedulable variables 0%
c [ternres-11] 20 ternary resolvents (0 bin, 20 trn)
c [ternres-11] fully completed ternary resolution
c [card-5] limit 2232879 penalty 4 = 4 + 0
c [card-5] found 35 at-most-one constraints of average size 3.6
c [card-5] no at-most-two constraint found
c [card-5] using previous limit 2232879 for elimination
c [card-5] 35 out of 35 constraints (100%) meet size limits
c [card-5] no units found
c [card-5] no at-most-one constraints generated
c [treelook-4] limit 893151 penalty 3 = 3 + 0 boost 1
c [treelook-4] scheduled 67123 literals 50%
c [treelook-4] scheduling used 893947 steps
c [treelook-4] not fully scheduled
c [treelook-4] limit 893151 penalty 3 = 3 + 0 boost 1
c [treelook-4] used 2725834 steps
c [treelook-4] 67120 literals remain 50%
c [treelook-4] 42878 variables remain to probed next time 63%
c [treelook-4] removed 0 variables, found 28 hbrs
c [transred-11] limit 2000000 with penalty 0 = 0 + 0
c [transred-11] removed 5 transitive binary clauses
c [transred-11] found 2 units
c [bca-11] limit of 10000000 steps and 2738955 added (scaled 2)
c [bca-11] 121919 out of 135298 literals actually usable 90%
c [bca-11] added 87 blocked clauses in 485239 steps
c [sort-queue-15] sorted 23361 enqueued variables after 1116285 conflicts
c [score-dist-15] active 44287 (65%), one 0 (0%), zero 23361 (35%)
c [score-dist-15] max exp 540, different 37 (7%)
c [score-dist-15] median active exp 521, avg 522.8
c [simplification-15] removed 2 variables 0.0% (67648 remain 45%)
c [simplification-15] removed 67 irredundant clauses 0.0% (1358048 remain 55%)
c [simplification-15] maximum reduction of 0% = max (0%, 0%)
c [simplification-15] full geometric conflict interval increment 399978
c [simplification-15] new conflict interval 799956
c [simplification-15] penalized conflict interval 799956 = 1 * 799956
c [simplification-15] hard conflict limit 2316219 (soft 1916241 + delta 399978)
c [simplification-15] new conflict limit 1916241 (hard 2316219)
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 -  494.5   67648  1358048   1120974   23961  48443 112373  101   215   82  47%   1024    8   59  177   33%
c -  517.9   67648  1358048   1236497   25982  48443 112373  157   255   84  62%   1024   53   73  184   40%
c -  525.9   67648  1358048   1283553   33150  48443 112373   81   240   86  34%   1024    1   79  130   61%
c -  542.5   67648  1358048   1364926   30689  48443 112373  198   200   85  99%   1024  -21  199  151  132%
c -  561.2   67648  1358048   1455759   27110  48443 112374  121   221   84  55%   1024    9  184  156  118%
c -  588.7   67648  1358048   1578832   27755  48443 112374  206   208   84  99%   1024  -17  206  181  114%
c -  602.3   67648  1358048   1646833   33766  48443 112374  130   218   86  60%   1024  -10   86  138   62%
c -  616.0   67648  1358048   1706794   32337  48443 112374  189   208   86  91%   1024  -13  101  140   72%
c -  641.2   67648  1358048   1824331   31570  48443 112374  175   217   85  81%   1024   -8  201  163  123%
c -  666.3   67648  1358048   1932313   30113  48443 112374  204   204   87 100%   1024   -7  203  196  104%
c 
c [simplification-16] limit 1916241 conflicts (hard 2316219) hit after 1938847 conflicts
c [quatres-12] found 17965 quaternary clauses 18% in total
c [quatres-12-2] added 70 quaternary resolvents
c [ternres-12] limit 108413582 with penalty 0 = 0 + 0
c [ternres-12] all 67648 free variables schedulable
c [ternres-12] 442 ternary resolvents (0 bin, 442 trn)
c [ternres-12] fully completed ternary resolution
c [basicprobe-4] limit 400000000 penalty 0 = 0 + 0
c [basicprobe-4-0] 50972 probes remain 76% after last round
c [basicprobe-4-0] 203 units = 203 failed (100%) + 0 lifted (0%)
c [basicprobe-4-0] removed 205 variables, found 54597 hbrs
c [bate-2] eliminated 230 asymmetric tautologies during probing
c [unhide-14] limit 2500000 with penalty 3 = 1 + 2
c [unhide-14-14] 72 units, 4 failed, 1679 tauts, 0 hbrs, 90959 literals
c [transred-12] limit 2000000 with penalty 0 = 0 + 0
c [transred-12] removed 2 transitive binary clauses
c [block-6] scheduling all variables this time
c [block-6] scheduled 67365 variables 100%
c [block-6] limit of 200000000 steps penalty 2 = 2 + 0
c [block-6] fully completed
c [block-6] transition to [ all 0 rem 0 ] state
c [block-6] eliminated 6212 blocked clauses
c [block-6] 6212 < 1/100 * 1355264 = 13552 considered unsuccessful
c [bca-12] limit of 10000000 steps and 2717484 added (scaled 2)
c [bca-12] 122582 out of 134564 literals actually usable 91%
c [bca-12] added 488 blocked clauses in 457581 steps
c [sweep-9] limit 8131018 penalty 2 = 2 + 0
c [sweep-9-1] 3062 pos 6.0% + 47960 neg 94.0% = 51022 sched 75.8% ret 16259
c [sweep-9-1] 8313465 steps 64 queries 4734.62 avg class size
c [sweep-9-1] 1753 decisions 60 SAT calls 98.02 avg env size
c [sweep-9-1] 50619 variables remain 75% (16662 retained 25%)
c [decomp-33] removed 19 variables
c [sweep-9-1] removed 19 vars (0 failed, 3 eqs, 6 impls)
c [sweep-9] 19 < 1/1000 * 67281 = 67 considered unsuccessful
c [sweep-9] removed 19 vars in TOTAL (1 rounds, 63 queries)
c [sort-queue-16] sorted 23189 enqueued variables after 1938847 conflicts
c [score-dist-16] active 44073 (66%), one 0 (0%), zero 23189 (34%)
c [score-dist-16] max exp 542, different 39 (7%)
c [score-dist-16] median active exp 522, avg 523.5
c [simplification-16] removed 386 variables 0.6% (67262 remain 44%)
c [simplification-16] removed 10793 irredundant clauses 0.8% (1347255 remain 55%)
c [simplification-16] maximum reduction of 1% = max (1%, 1%)
c [simplification-16] geometric conflict interval increment 399978 = 799956 / 2
c [simplification-16] conflict interval soft limit 1000000 reached
c [simplification-16] new conflict interval 1000000
c [simplification-16] penalized conflict interval 1000000 = 1 * 1000000
c [simplification-16] hard conflict limit 3438847 (soft 2938847 + delta 500000)
c [simplification-16] new conflict limit 2938847 (hard 3438847)
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 -  714.7   67262  1347255   2084868   33828  47036 167323  114   271   88  42%   1024   40  100  153   66%
c -  724.8   67262  1347255   2140630   36470  47036 167335   88   229   89  38%   1024   -9   89  118   76%
c -  738.0   67262  1347255   2220464   35485  47036 167335  204   205   88  99%   1024  -18  204  140  145%
c -  754.6   67262  1347255   2293592   35084  47038 167338   46   408   87  11%   1024  175   16  115   14%
c -  768.1   67262  1347255   2340342   38271  47038 167338   40   309   88  13%   1024   24   38   76   51%
c -  778.4   67262  1347255   2385796   38655  47038 167338   71   268   89  27%   1024  -21   75   67  112%
c -  790.5   67262  1347255   2440994   36952  47038 167338  113   218   90  52%   1024  -39   95   80  119%
c -  809.0   67262  1347255   2527011   39351  47040 167338  141   227   91  62%   1024   -9   79  118   67%
c -  824.0   67262  1347255   2595302   39658  47040 167338   68   253   91  27%   1024   26   68  108   63%
c -  861.3   67262  1347255   2732371   35721  47041 167350  196   196   91 100%   1024  -13  195  173  113%
c -  902.7   67262  1347255   2891212   37645  47042 167350   56   284   89  20%   1024   66   65  139   47%
c -  915.1   67262  1347255   2944015   41848  47042 167350   74   225   92  33%   1024  -16   77   99   78%
c 
c [simplification-17] limit 2938847 conflicts (hard 3438847) hit after 2955737 conflicts
c [quatres-13] found 16605 quaternary clauses 17% in total
c [quatres-13-1] removed 2 duplicate quaternary clauses
c [quatres-13-2] added 1410 single-self-subsuming ternary resolvents
c [quatres-13-2] added 5 quaternary resolvents
c [ternres-13] limit 160891822 with penalty 0 = 0 + 0
c [ternres-13] all 67262 free variables schedulable
c [ternres-13] 1266 ternary resolvents (0 bin, 1266 trn)
c [ternres-13] fully completed ternary resolution
c [simpleprobe-5] 43732 schedulable variables 65%
c [simpleprobe-5] limit 200000000 penalty 0 = 0 + 0
c [decomp-35] removed 218 variables
c [simpleprobe-5] 37797 variables remain 56% (29247 retained 44%)
c [simpleprobe-5] removed 218 variables, found 169304 hbrs, 201 units
c [unhide-15] limit 2500000 with penalty 3 = 0 + 3
c [unhide-15-15] 24 units, 0 failed, 4409 tauts, 0 hbrs, 69987 literals
c [transred-13] limit 2000000 with penalty 0 = 0 + 0
c [transred-13] removed 20 transitive binary clauses
c [transred-13] found 2 units
c [elim-12] 40 variables 0% will be scheduled this time
c [elim-12] scheduled 40 variables 0%
c [elim-12] limit of 200000000 steps penalty 2 = 2 + 0
c [elim-12] rescheduling of touched variables disabled
c [elim-12] incomplete 20 not tried 0% in round 1
c [elim-12] transition to [ all 0 rem 1 ] state
c [elim-12] eliminated 0 = 0% variables out of 40 scheduled
c [bca-13] limit of 10000000 steps and 2696786 added (scaled 2)
c [bca-13] 121630 out of 134038 literals actually usable 91%
c [bca-13] added 331 blocked clauses in 475490 steps
c [sort-queue-17] sorted 22985 enqueued variables after 2955737 conflicts
c [score-dist-17] active 44033 (66%), one 0 (0%), zero 22985 (34%)
c [score-dist-17] max exp 543, different 40 (7%)
c [score-dist-17] median active exp 523, avg 524.3
c [simplification-17] removed 244 variables 0.4% (67018 remain 44%)
c [simplification-17] removed 10435 irredundant clauses 0.8% (1336820 remain 54%)
c [simplification-17] maximum reduction of 1% = max (0%, 1%)
c [simplification-17] geometric conflict interval increment 500000 = 1000000 / 2
c [simplification-17] conflict interval soft limit 1000000 reached
c [simplification-17] new conflict interval 1000000
c [simplification-17] penalized conflict interval 1000000 = 1 * 1000000
c [simplification-17] hard conflict limit 4455737 (soft 3955737 + delta 500000)
c [simplification-17] new conflict limit 3955737 (hard 4455737)
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 -  934.3   67018  1336820   2994455   42722  47775 322440   83   226   94  37%   1024  -10   77   88   87%
c -  946.1   67018  1336820   3050192   40244  47775 322440   85   221   93  38%   1024   -9   82   86   95%
c -  960.7   67018  1336820   3114104   41838  47775 322440   99   223   93  44%   1024    0  103   92  112%
c -  973.2   67018  1336820   3173469   43137  47775 322440   95   220   95  43%   1024   -0   84   91   93%
c -  987.5   67018  1336820   3236085   43140  47775 322440  148   214   95  69%   1024   -4   87  105   83%
c
c CAUGHT SIGNAL 15 SIGTERM
c
c s UNKNOWN
c bate: 237 basic ate = 202 trn 85% + 35 lrg 15% in 2 updates
c bcas: 13 count, 45624 added (7593 skipped), 6103958 steps
c bkwd: tried 76811 clauses, 153459 lits, 2.00 lits/clause
c bkwd: checked 908804705 occs, 11831.70 occs/clause, 5922.13 occs/lit
c bkwd: subsumed 0 binary, 3 ternary, 0 large
c bkwd: strengthened 0 binary, 0 ternary (0% self), 160 large (0% self)
c blkd: 6 bces, 323918 removed, 46887807 resolutions, 139709337 steps
c blkd: 24308 blocking literals 8%, 4838 pure
c bump: 3125293 bumped seen, 1323300087 lits 423.4 on average
c card: 5 count, 0 units, 0 am1, 48652779 steps
c card: 0 rescheduled, 0 eliminated, 0 resolved, 1384 subsumed
c card: 95 at-most-one constraints found, average size 3.33
c card: 95 at-most-one constraints used 100%, average size 3.33
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: 4 cces, 765 eliminated, 755 ate 99%, 10 abce 1%
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: 9607154 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 88 gcs, 0 rescored clauses, 0 rescored vars
c dcps: 35 decompositions, 2378 equivalent 2%
c deco: 1554929 decision-only clauses 50%, 60% reduction
c decs: 40223203 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 12 elims, 57092 eliminated 38%, 1102 pure 2%
c elms: 14 rounds, 1.2 rounds/bve
c elms: 21406 small 37%, 29746 large 52%
c elms: 29965 tried small, 21406 succeeded 71%, 8559 failed 29%
c elms: 63390 subsumed, 441604 strengthened, 22960 blocked
c elms: 17575762 copies, 30964297 resolutions, 567351 ipos
c elms: 98236120 subchks, 116698835 strchks
c gaus: 4 extractions, 10 extracted, 2.1 size, 3 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 10131258 steps, 5065629 extr 50%, 34 elim 0%
c glue: 150.9 orig avg, 150.9 real avg, 10.1 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 478405 = 364534 simple 76% + 113804 trn 24% + 67 lrg 0%, 3325 sub 1%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 3125293 clauses, 177.8 length
c lrnd: 555588415 lits = 1097538008 orig - 541949593 removed 49%
c lrnd: 946156 uips 30%, 1376789 flips 44%
c mins: 1429604 mins 48%, 84 bin 0%, 612 size 0%
c mins: 231035260 poisoned searches, 34807680 hits, 15% hit rate
c mins: 436641249 used twice searches, 89321572 hits, 20% hit rate
c move: moved 290127, 279898 bin 96%, 10229 trn 4%
c otfs: 155598 driving 40%, 231206 restarting 60%
c otfs: str 386804, 386610 red 100%, 194 irr 0%
c otfs: str 386804, 0 bin 0%, 20 trn 0%, 386784 lrg 100%
c otfs: sub 11318, 11301 red 100%, 17 irr 0%
c otfs: sub 11318, 0 bin 0%, 0 trn 0%, 11318 lrg 100%
c phas: 1 computed, 149415 set, 0 pos (0%), 149415 neg (100%)
c prbs: 4 basic, 19568 probed, 479 failed, 0 lifted
c prbs: 5 simple, 412997 probed, 4166 failed, 56 eqs
c prbs: 4 treelook, 15 probed, 0 failed, 0 lifted
c prom: 8776 locked 0% out of 3671212 tried
c prps: 2380512211 props, 57 props/dec
c prps: 97% srch, 3% simp, 0% lkhd
c quat: 13 count, 4423 quat, 3982 self1, 2 self2, 276 dup
c queu: 17 sorted, 40223203 next (693805 steps 0.02)
c queu: 1324154709 enq (1897187585 steps 1.43), 1323300087 deq 100%
c redc: 248 clauses 33%, 757 tried 0%, 23 sat 3%
c redc: 1314 lits 14%, 9424 tried 0%, 23 sat 0%
c redc: 39 times jump level reduced, 349.4 levels on average
c reds: 38 count, 86334.6 conflicts per reduce
c reds: 0 memlim 0%, 38 arith 100%
c reds: 1301607 collected 90%, 151122 retired 10%
c rmbd: 18913 removed, 17881 red 95%
c rsts: 10934 restarts 55%, 8950 skipped 45%
c rsts: 8950 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: 17 count, 17 confs 100%, 0 vars 0%
c simp: 0 its 0%, 0 bin 0%, 0 trns 0%
c subl: 3125293 count (8781331 tried 2.8), 1585267 sub out of 3124891 (50.7%)
c swps: 9 count, 9 rounds, 820 queries (91.1/round)
c swps: 736 sat calls, 5 unsat (0.2% success rate)
c swps: 23129 decisions 31.4, 179 conflicts 0.2
c swps; 3392.8 avg class size, 146.6 avg environment size
c swps: 0 failed, 196 impls, 89 equivs
c swp0: 272 type 0 queries, 46 unsat (16.9%), 255 sat (93.8%)
c swp1: 548 type 1 queries, 210 unsat (38.3%), 476 sat (86.9%)
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: 86697326 calls to obtain time
c tops: 25181 fixed 17%, 0 its, 0.00 confs/it
c trds: 13 transitive reductions, 73 removed, 9 failed
c trds: 1731 nodes, 11787 edges, 26027222 steps
c trim: 10655943 words, 40.6 MB
c trnr: 13 count, 24 bin, 69604 trn, 403511318 steps
c unhd: 15 count, 15 rounds, 64435787 steps
c unhd: 805 non-trivial sccs of average size 2.0
c unhd: 6982 units, 6981 bin, 1 trn, 0 lrg
c unhd: 80 failed, 76 stamp, 0 lits, 0 bin, 2 trn, 0 lrg
c unhd: 99856 tauts, 1122 bin 1%, 10453 trn 10%, 11670 lrg 12%
c unhd: 99856 tauts, 76611 stamp 77%, 27535 red 28%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 844840 str, 6981 bin 1%, 15933 trn 2%, 821926 lrg 97%, 644353 red 76%
c vars: 67018 remaining 44% and 84651 removed 56% out of 151669
c vars: 25181 fixed 17%, 57092 eliminated 38%, 2378 equivalent 2%
c vsts: 18334755585 visits, 97% srch, 3% simp, 0% lkhd
c vsts: 7.7 search visits per propagation, 5431.9 per conflict
c wchs: 2205789498 pushed, 88490216 enlarged, 140 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all        3129314       1301607        151122      63641172      44940466       1531916
c 
c  0 0          4803   0        51   0         0   0   1512729   2     61040   0       156   0     0.1
c  1 5           319   0        47   0       181   0    703792   1    144834   0      2021   0     0.0
c  2 6          2046   0       522   0       987   1   1606060   3    819607   2      6895   0     0.1
c  3 9         12946   0      7992   1      2314   2   5779398   9   2820975   6     47857   3     0.7
c  4 14        27452   1     16284   1      4306   3  15790516  25  12183029  27     58075   4     1.6
c  5 21        15095   0      9561   1      2495   2  11155843  18   9703568  22     15286   1     2.0
c  6 30        26150   1     17027   1      5578   4   6848547  11<  5522828  12<    48086   3     3.1
c  7 41        79857   3     62393   5      7515   5   4532277   7   2936873   7     30362   2    11.4
c  8 54       146835   5    108022   8     16295  11   2883839   5   1491386   3     38047   2    15.1
c  9 69       614489  20    489882  38<    28673  19<  5789669   9   3692275   8    261912  17    30.0
c 10 86       446326  14<   295781  23      8458   6   3174409   5   2100435   5    182793  12<   27.5
c 11 126     1567353  50    284848  22     71871  48   3595752   6   3277058   7    823670  54    97.3
c 12 230      185602   6      9189   1      2427   2    268260   0    186543   0     16755   1    52.4
c 13 534          41   0         8   0        22   0        81   0        15   0         1   0     0.1
c 
c avg                 10.1           9.3           9.4           5.7           5.9           9.6
c std                  1.5           1.5           2.1           2.6           2.4           2.2
c 
c  228.989  23% bump
c   81.504   8% elim
c   32.172   3% probe
c   27.946   3% decide
c   20.163   2% block
c   15.912   2% unhide
c    9.456   1% sweep
c    5.961   1% cce
c 
c   14.793 < 1% rest (below)
c 
c    5.392   1% bca
c    5.327   1% quatres
c    1.869   0% ternres
c    1.339   0% gauss
c    0.679   0% transred
c    0.187   0% card
c    0.000   0% locs
c    0.000   0% queuesort
c    0.000   0% rescore
c ==================================
c    5.527   1% preprocessing     3%
c  186.395  19% inprocessing     97%
c ==================================
c  191.922  19% simplifying
c  806.754  81% search
c ==================================
c  998.679 100% all
c 
c       3280713 conflicts,        3285.1 confs/sec
c           191 ternaries,       17176.5 confs/ternary
c           125 binaries,        26245.7 confs/binary
c             0 iterations,          0.0 confs/iteration
c 
c            38 reductions,          0.0 redus/sec,  86334.6 confs/reduction
c         10934 restarts,           10.9 rests/sec,    300.0 confs/restart
c      40223203 decisions,       40276.4 decis/sec,     12.3 decis/conflict
c    2380512211 propagations,  2383661.7 props/sec,     59.2 props/decision
c 
c 998.7 seconds, 271.3 MB
c
c CAUGHT SIGNAL 15 SIGTERM
c
c launch: done
