c launch: /data/cnf/sc2014/app/atco_enc3_opt2_10_12.cnf.bz2
c host: atom24
c Lingeling SAT Solver
c 
c Version b7ztzud 55d9a3e9649fc56eacf3e72d8e2e2d5c615d5f18
c 
c Copyright (C) 2010-2014 Armin Biere JKU Linz Austria.
c All rights reserved.
c 
c released Fri May  1 11:44:04 CEST 2015
c compiled Fri May  1 11:44:04 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-49-generic x86_64
c 
c piping '/data/cnf/sc2014/app/atco_enc3_opt2_10_12.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/atco_enc3_opt2_10_12.cnf.bz2
c no embedded options
c found 'p cnf 1236271 4932603' header
c read 1236271 variables, 4932603 clauses, 12310782 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 --randec=0
c --randecint=1000
c --redcls=1
c --redclsglue=6
c --redclsmaxdec=5
c --redclsmaxdepth=10
c --redclsmaxlrg=10
c --redclsmaxprops=100
c --redclsatlimlo=0
c --redclsatlimhi=100
c --redclsize=30
c --redclstype=4
c --reducefixed=0
c --reduceinc=1000
c --reduceinit=50000
c --reduce=1
c --restart=4
c --restartglcint=10
c --restartglclim=115
c --restartinit=0
c --restartint=5
c --restartpen=1
c --retirenb=1
c --retireint=4
c --retiremin=1
c --reusetrail=0
c --rmincpen=4
c --rstinoutinc=110
c --satlimdelay=10000
c --scincinc=200
c --scincincsatlimhi=100
c --scincincdelta=10
c --scincincincint=100000
c --scincincmin=200
c --scincincmode=1
c --scoreshift=0
c --scoreresetint=2147483647
c --seed=0
c --simpbintinc=100
c --simpbintinclim=10000
c --simpcintdelay=2000
c --simpcintinc=20000
c --simpcintincdiv=1
c --simpcintmaxhard=10000000
c --simpcintmaxsoft=1000000
c --simpincdelmaxfact=50
c --simpincdelmaxmin=10000
c --simpinitdelay=0
c --simpintsizepen=0
c --simpen=0
c --simpidiv=3
c --simpiscale=100
c --simpitdelay=10
c --simpitintinc=10
c --simpitintinclim=1000
c --simplify=2
c --simprtc=5
c --simptintinc=1000
c --simptintinclim=10000
c --simpvarchg=100
c --simpvarlim=100
c --sizemaxpen=5
c --sizepen=1000000
c --sleeponabort=0
c --smallirr=90
c --smallve=1
c --smallvevars=10
c --smallvewait=0
c --sortlits=0
c --subl=9
c --sweep=1
c --sweepboost=10
c --sweepboostdel=4
c --sweepboostint=7
c --sweepboostvlim=1000000
c --sweepfacdec=10
c --sweepforgive=2
c --sweepirr=3
c --sweepmaxeff=200000000
c --sweepmaxdec=10000
c --sweepmaxround=3
c --sweepmindec=100
c --sweepmineff=1000000
c --sweepred=3
c --sweepreleff=3
c --sweeprtc=0
c --sweeprtcint=14
c --sweeprtcintvlim=100000
c --sweepsuccessmaxwortc=6
c --sweepsuccessrat=1000
c --sweepwait=2
c --synclsall=1
c --synclsglue=8
c --synclsint=100
c --synclslen=40
c --syncunint=111111
c --termint=122222
c --ternres=1
c --ternresboost=5
c --ternresrtc=0
c --ternreswait=2
c --transred=1
c --transredwait=2
c --trapiflush=0
c --trdmaxeff=2000000
c --trdmineff=100000
c --trdreleff=10
c --treelook=1
c --treelookboost=10
c --treelookfull=0
c --treelookmaxeff=50000000
c --treelookmineff=300000
c --treelookreleff=2
c --treelookrtc=0
c --trep=1
c --trepint=55555
c --trnreleff=10
c --trnrmaxeff=200000000
c --trnrmineff=4000000
c --unhdatrn=2
c --unhdextstamp=1
c --unhdhbr=0
c --unhdlnpr=3
c --unhdmaxeff=20000000
c --unhdmineff=100000
c --unhdreleff=2
c --unhdroundlim=20
c --unhide=1
c --unhidewait=0
c --usedtwice=1
c --vsidsdint=256
c --wait=1
c --waitmax=4
c --witness=0
c --check=0
c --log=-1
c --profile=1
c --profilelong=1
c --verbose=1
c [freezer] frozen 0 variables out of 1235855 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 [set-score-increment-1] factor 1.200000d+00 (200/1000) after 0 conflicts
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 1235855  4932185         0       0      0     0    0     0  251   0%      0    0    0    0    0%
c 
c [simplification-1] limit 0 conflicts (hard 0) hit after 0 conflicts
c [card-1] limit 1233046 based on 4932185 irredundant clauses
c [card-1] found 317 at-most-one constraints of average size 3.7
c [card-1] no at-most-two constraint found
c [card-1] using previous limit 1233046 for elimination
c [card-1] 317 out of 317 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 240908 variables
c [simpleprobe-1] all 995363 free variables schedulable
c [simpleprobe-1] boosting simple probing limit by 10
c [simpleprobe-1] limit 7948536 based on 3974268 irredundant clauses
c [decomp-2] removed 21 variables
c [simpleprobe-1] 995342 variables remain 100% (0 retained 0%)
c [simpleprobe-1] removed 21 variables, found 2 hbrs, 0 units
c [unhide-1] limit 248387 based on 3974198 irredundant clauses
c [unhide-1-1] 1 units, 211 failed, 4366 tauts, 0 hbrs, 734 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 992123 variables 100%
c [elim-1] limit of 5000000 steps penalty 2 = 0 + 2
c [elim-1] rescheduling of touched variables disabled
c [elim-1] incomplete 964258 not tried 97% in round 1
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 27861 = 3% variables out of 992123 scheduled
c [elim-1] considered successful since not run to completion yet
c [phase-count-1] 3932865 negative 99.9% of 3936003 except 3138 0.1%
c [phase-count-1] 3919558 positive 99.6% of 3936003 except 16445 0.4%
c [phase-count-1] less non-negative clauses 3138 than limit 393600 (10.0%)
c [phase-count-1] non-pos/non-neg = 16445/3138 = 5.24 >= 2.00 = 200/100
c [lucky-phase-1] forcing lucky phase -1
c [phase-1] phase bias: 0 positive 0%, 964262 negative 100%
c [score-distribution-1] 0 pos 0.00%, 0 min 0.00%, 964262 zero 100.00%
c [score-distribution-1] 1 different 0.00% out of total 964262 variables
c [simplification-1] removed 31763 variables 3.2% (964262 remain 78%)
c [simplification-1] removed 996182 irredundant clauses 20.2% (3936003 remain 80%)
c [simplification-1] maximum reduction of 20% = max (3%, 20%)
c [simplification-1] large reduction 20% >= 5% limit
c [simplification-1] next conflict interval 1000 = 2000/2
c [simplification-1] penalized conflict interval 1000 = 1 * 1000
c [simplification-1] hard conflict limit 11000 (soft 1000 + delta 10000)
c [simplification-1] new conflict limit 1000 (hard 11000)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i    9.8  964261  3936003        21       6      7     8    0     0  271   3%      0    0    0    0 24739%
c i    9.9  964236  3936003        24       6      7    10    0     0  275   3%      0    0    0    0 24497%
c i    9.9  964213  3936003        27       6      7    12    0     0  275   3%      0    0    0    0 24266%
c i   10.0  964179  3936003        29       6      7    13    0     0  275   3%      0    0    0    0 24108%
c i   10.0  964131  3936003        33       6      8    15    0     0  275   4%      0    0    0    0 23865%
c i   10.4  964111  3936003       106      16     43    39    0     1  275   6%      0    1    1    0 21321%
c i   10.5  964000  3936003       112      16     45    42    0     1  275   6%      0    1    1    0 21003%
c i   10.5  963934  3936003       113      16     45    42    0     1  275   6%      0    1    1    0 20921%
c i   10.6  963922  3936003       140      18     59    51    0     1  275   5%      0    1    1    0 19994%
c i   10.7  963772  3936003       147      18     62    54    0     1  275   6%      0    1    1    0 19654%
c 
c [simplification-2] limit of 10 iterations hit after 10 iterations
c [decomp-3] removed 695 variables
c [simpleprobe-2] all 963567 free variables schedulable
c [simpleprobe-2] limit 7865080 based on 3932540 irredundant clauses
c [decomp-4] removed 99 variables
c [simpleprobe-2] 849071 variables remain 88% (114397 retained 12%)
c [simpleprobe-2] removed 99 variables, found 137 hbrs, 1 units
c [treelook-1] limit 983032 based on 3932131 irredundant clauses
c [treelook-1] scheduled 126078 literals 7%
c [treelook-1] scheduling used 983035 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 983032 based on 3932131 irredundant clauses
c [treelook-1] used 1019359 steps
c [treelook-1] 125684 literals remain 7%
c [treelook-1] 67387 variables remain to probed next time 7%
c [decomp-5] removed 85 variables
c [treelook-1] removed 470 variables, found 598 hbrs
c [basicprobe-1] limit 31437080 based on 3929635 irredundant clauses
c [basicprobe-1-0] 643 probes remain 0% after last round
c [basicprobe-1-0] 78 units = 78 failed (100%) + 0 lifted (0%)
c [basicprobe-1-0] removed 645 variables, found 35834 hbrs
c [unhide-2] limit 245602 based on 3929635 irredundant clauses
c [unhide-2-2] 15 units, 55 failed, 18338 tauts, 0 hbrs, 847 literals
c [elim-2] 958098 variables 100% will be scheduled this time
c [elim-2] scheduled 958098 variables 100%
c [elim-2] limit of 5000000 steps penalty 2 = 0 + 2
c [elim-2] rescheduling of touched variables disabled
c [elim-2] incomplete 934818 not tried 98% in round 1
c [elim-2] transition to [ all 0 rem 1 ] state
c [elim-2] eliminated 23279 = 2% variables out of 958098 scheduled
c [elim-2] considered successful since not run to completion yet
c [phase-count-2] 3895598 negative 99.9% of 3898806 except 3208 0.1%
c [phase-count-2] 3879423 positive 99.5% of 3898806 except 19383 0.5%
c [phase-count-2] less non-negative clauses 3208 than limit 389800 (10.0%)
c [phase-count-2] non-pos/non-neg = 19383/3208 = 6.04 >= 2.00 = 200/100
c [lucky-phase-2] forcing lucky phase -1
c [phase-2] phase bias: 0 positive 0%, 492664 negative 100%
c [score-distribution-2] 1329 pos 0.14%, 0 min 0.00%, 933494 zero 99.86%
c [score-distribution-2] 265 different 0.03% out of total 934823 variables
c [simplification-2] removed 28912 variables 3.0% (934823 remain 76%)
c [simplification-2] removed 37197 irredundant clauses 0.9% (3898806 remain 79%)
c [simplification-2] maximum reduction of 3% = max (3%, 1%)
c [simplification-2] forced so keeping old conflict interval 0
c [simplification-2] conflict limit remains at 1025 (hard 11000)
c [simplification-2] new iteration interval 100
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   23.2  934822  3898806       148      16     41 11793    0     1  272   6%      0    1    1    0 19577%
c i   23.2  934821  3898806       149      16     41 11793    0     1  272   6%      0    1    1    0 19501%
c i   23.2  934820  3898806       151      16     41 11794    0     1  272   6%      0    1    1    0 19376%
c i   28.5  934794  3898806      1025     507    289 11878    1    11  282   7%      4   11    4    0 7192%
c 
c [simplification-3] limit 1050 conflicts (hard 11000) hit after 1051 conflicts
c [card-2] limit 974701 based on 3898806 irredundant clauses
c [card-2] found 227 at-most-one constraints of average size 3.1
c [card-2] no at-most-two constraint found
c [card-2] using previous limit 974701 for elimination
c [card-2] 227 out of 227 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [decomp-6] removed 1506 variables
c [treelook-2] limit 973154 based on 3892618 irredundant clauses
c [treelook-2] scheduled 189488 literals 10%
c [treelook-2] scheduling used 1134147 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 973154 based on 3892618 irredundant clauses
c [treelook-2] used 986692 steps
c [treelook-2] 189342 literals remain 10%
c [treelook-2] 10328 variables remain to probed next time 1%
c [decomp-7] removed 4 variables
c [treelook-2] removed 114 variables, found 193 hbrs
c [unhide-3] limit 243249 based on 3891999 irredundant clauses
c [unhide-3-3] 0 units, 75 failed, 13773 tauts, 0 hbrs, 797 literals
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 932495 variables 100%
c [elim-3] limit of 11437136 steps penalty 2 = 0 + 2
c [elim-3] rescheduling of touched variables disabled
c [elim-3] incomplete 882369 not tried 95% in round 1
c [elim-3] transition to [ all 1 rem 1 ] state
c [elim-3] eliminated 50033 = 5% variables out of 932495 scheduled
c [elim-3] considered successful since not run to completion yet
c [phase-count-3] 3864044 negative 99.9% of 3867225 except 3181 0.1%
c [phase-count-3] 3850431 positive 99.6% of 3867225 except 16794 0.4%
c [phase-count-3] less non-negative clauses 3181 than limit 386700 (10.0%)
c [phase-count-3] non-pos/non-neg = 16794/3181 = 5.28 >= 2.00 = 200/100
c [lucky-phase-3] forcing lucky phase -1
c [phase-3] phase bias: 0 positive 0%, 248107 negative 100%
c [score-distribution-3] 7158 pos 0.81%, 0 min 0.00%, 875304 zero 99.19%
c [score-distribution-3] 1305 different 0.15% out of total 882462 variables
c [simplification-3] removed 51078 variables 5.5% (882462 remain 71%)
c [simplification-3] removed 31581 irredundant clauses 0.8% (3867225 remain 78%)
c [simplification-3] maximum reduction of 5% = max (5%, 1%)
c [simplification-3] large reduction 5% >= 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 13051 (soft 3051 + delta 10000)
c [simplification-3] new conflict limit 3051 (hard 13051)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   41.0  882461  3867225      1809     868    471 11269    1    15  280   8%      6   15    4    0 3919%
c 
c [simplification-4] limit 3051 conflicts (hard 13051) hit after 3051 conflicts
c [decomp-8] removed 496 variables
c [basicprobe-2] limit 30918808 based on 3864851 irredundant clauses
c [basicprobe-2-0] 222 probes remain 0% after last round
c [basicprobe-2-0] 214 units = 156 failed (73%) + 58 lifted (27%)
c [basicprobe-2-0] removed 3257 variables, found 18856 hbrs
c [unhide-4] limit 241553 based on 3864851 irredundant clauses
c [unhide-4-4] 2 units, 246 failed, 10123 tauts, 0 hbrs, 4201 literals
c [elim-4] 875146 variables 100% will be scheduled this time
c [elim-4] scheduled 875146 variables 100%
c [elim-4] boosting limit by 20
c [elim-4] limit of 402250635 steps penalty 2 = 0 + 2
c [elim-4] rescheduling of touched variables disabled
c [elim-4] incomplete 3248 not tried 0% in round 1
c [elim-4] transition to [ all 0 rem 1 ] state
c [elim-4] eliminated 288882 = 33% variables out of 875146 scheduled
c [elim-4] considered successful since not run to completion yet
c [phase-count-4] 3792294 negative 99.9% of 3795750 except 3456 0.1%
c [phase-count-4] 3777273 positive 99.5% of 3795750 except 18477 0.5%
c [phase-count-4] less non-negative clauses 3456 than limit 379500 (10.0%)
c [phase-count-4] non-pos/non-neg = 18477/3456 = 5.35 >= 2.00 = 200/100
c [lucky-phase-4] forcing lucky phase -1
c [phase-4] phase bias: 0 positive 0%, 165001 negative 100%
c [score-distribution-4] 12429 pos 2.12%, 2 min 0.00%, 573927 zero 97.88%
c [score-distribution-4] 3332 different 0.57% out of total 586358 variables
c [simplification-4] removed 295651 variables 33.5% (586358 remain 47%)
c [simplification-4] removed 71475 irredundant clauses 1.8% (3795750 remain 77%)
c [simplification-4] maximum reduction of 34% = max (34%, 2%)
c [simplification-4] large reduction 34% >= 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 15051 (soft 5051 + delta 10000)
c [simplification-4] new conflict limit 5051 (hard 15051)
c 
c [simplification-5] limit 5051 conflicts (hard 15051) hit after 5051 conflicts
c [quatres-1] found 710485 quaternary clauses 100% in total
c [quatres-1-1] removed 1 duplicate quaternary clauses
c [quatres-1-2] added 28 single-self-subsuming ternary resolvents
c [quatres-1-2] added 109 quaternary resolvents
c [ternres-1] boosting ternary resolution limit by 5
c [ternres-1] limit 15183000 based on 3795750 irredundant clauses
c [ternres-1] all 586358 free variables schedulable
c [ternres-1] 355 ternary resolvents (0 bin, 355 trn)
c [ternres-1] 571089 variables remain 97% (15269 retained 3%)
c [gauss-1] limit 1897875 based on 3795750 irredundant clauses
c [gauss-1] extracted 36 xors of average arity 2.1
c [gauss-1] connected 75 occurrences of 67 variables (average 1.1)
c [gauss-1] limit 1897875 based on 3795750 irredundant clauses
c [gauss-1] fully completed
c [gauss-1] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-9] removed 294 variables
c [simpleprobe-3] 516489 schedulable variables 88%
c [simpleprobe-3] limit 7590198 based on 3795099 irredundant clauses
c [decomp-10] removed 6 variables
c [simpleprobe-3] 479222 variables remain 82% (106836 retained 18%)
c [simpleprobe-3] removed 6 variables, found 312 hbrs, 1 units
c [unhide-5] limit 237192 based on 3795074 irredundant clauses
c [unhide-5-5] 0 units, 90 failed, 5927 tauts, 0 hbrs, 8995 literals
c [transred-1] limit 3788041 based on 3788041 irredundant clauses
c [transred-1] removed 3 transitive binary clauses
c [block-1] scheduling all variables this time
c [block-1] scheduled 585645 variables 100%
c [block-1] boosting limit by 10
c [block-1] limit of 134054127 steps penalty 2 = 0 + 2
c [block-1] fully completed
c [block-1] transition to [ all 0 rem 0 ] state
c [block-1] eliminated 1163 blocked clauses
c [block-1] 1163 < 1/100 * 3788039 = 37880 considered unsuccessful
c [cce-1] limit of 7500000 steps penalty 2 = 0 + 2
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] allowing another 3750001 steps for small clauses
c [cce-1-1] scheduling 2593377 clauses = 1193546 binary + 1399831 ternary
c [cce-1-1] tried to eliminate 22 small clauses 0%
c [cce-1-1] eliminated 2 binary clauses 0%
c [cce-1-1] eliminated 2 small clauses 0%
c [cce-1-1] eliminated 2 small clauses in 7500000 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 2 covered clauses in round 1
c [cce-1] eliminated 2 covered clauses in TOTAL during 1 rounds
c [cce-1] 2 < 1/100 * 3784355 = 37843 considered unsuccessful
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 585645 variables 100%
c [elim-5] limit of 26810825 steps penalty 2 = 0 + 2
c [elim-5] rescheduling of touched variables disabled
c [elim-5] incomplete 462839 not tried 79% in round 1
c [elim-5] transition to [ all 1 rem 1 ] state
c [elim-5] eliminated 1541 = 0% variables out of 585645 scheduled
c [elim-5] 1541 < 1/100 * 585645 = 5856 considered unsuccessful
c [bca-1] limit of 10000000 steps and 7566270 added (scaled 2)
c [bca-1] 1164997 out of 1168210 literals actually usable 100%
c [bca-1] added 3 blocked clauses in 2333738 steps
c [sweep-1] limit 7565770 based on 3782885 irredundant clauses
c [sweep-1-1] 230889 pos 39.5% + 353215 neg 60.5% = 584104 sched 100.0% ret 0
c [sweep-1-1] 7576117 steps 33 queries 151080.64 avg class size
c [sweep-1-1] 306 decisions 27 SAT calls 65.67 avg env size
c [sweep-1-1] 584019 variables remain 100% (85 retained 0%)
c [decomp-11] removed 19 variables
c [sweep-1-1] removed 19 vars (0 failed, 6 eqs, 11 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 19 vars in TOTAL (1 rounds, 32 queries)
c [phase-count-5] 3779550 negative 99.9% of 3782868 except 3318 0.1%
c [phase-count-5] 3765499 positive 99.5% of 3782868 except 17369 0.5%
c [phase-count-5] less non-negative clauses 3318 than limit 378200 (10.0%)
c [phase-count-5] non-pos/non-neg = 17369/3318 = 5.23 >= 2.00 = 200/100
c [lucky-phase-5] forcing lucky phase -1
c [phase-5] phase bias: 0 positive 0%, 164210 negative 100%
c [score-distribution-5] 9399 pos 1.61%, 3625 min 0.62%, 571061 zero 97.77%
c [score-distribution-5] 2760 different 0.47% out of total 584085 variables
c [simplification-5] removed 2273 variables 0.4% (584085 remain 47%)
c [simplification-5] removed 12882 irredundant clauses 0.3% (3782868 remain 77%)
c [simplification-5] maximum reduction of 0% = max (0%, 0%)
c [simplification-5] full geometric conflict interval increment 20000
c [simplification-5] new conflict interval 20000
c [simplification-5] penalized conflict interval 20000 = 1 * 20000
c [simplification-5] hard conflict limit 35051 (soft 25051 + delta 10000)
c [simplification-5] new conflict limit 25051 (hard 35051)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i  147.3  584084  3782868     15029   11098   1248 11026   15    37  296  40%    174   31   17    2  675%
c i  159.0  584083  3782868     18558   13932   1336 11050   14    36  297  39%     26   28   12    3  379%
c i  160.7  584082  3782868     18923   14241   1345 11055   14    36  297  39%     13   28   11    3  336%
c i  165.0  584081  3782868     19840   14995   1384 11065   13    36  297  37%     -2   28   10    3  303%
c 
c [simplification-6] limit of 368 binary hit after 368 binaries
c [quatres-2] found 697615 quaternary clauses 99% in total
c [quatres-2-2] added 18 single-self-subsuming ternary resolvents
c [quatres-2-2] added 36 quaternary resolvents
c [ternres-2] limit 15131444 based on 3782861 irredundant clauses
c [ternres-2] 568866 schedulable variables 97%
c [ternres-2] 848 ternary resolvents (0 bin, 848 trn)
c [ternres-2] 553568 variables remain 95% (30513 retained 5%)
c [card-3] limit 945715 based on 3782861 irredundant clauses
c [card-3] found 159 at-most-one constraints of average size 3.1
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 945715 for elimination
c [card-3] 159 out of 159 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [decomp-12] removed 77 variables
c [treelook-3] limit 945640 based on 3782563 irredundant clauses
c [treelook-3] scheduled 83284 literals 7%
c [treelook-3] scheduling used 985224 steps
c [treelook-3] not fully scheduled
c [treelook-3] limit 945640 based on 3782563 irredundant clauses
c [treelook-3] used 1106420 steps
c [treelook-3] 82891 literals remain 7%
c [treelook-3] 2923 variables remain to probed next time 1%
c [decomp-13] removed 1 variables
c [treelook-3] removed 274 variables, found 389 hbrs
c [unhide-6] limit 294913 with penalty 4 = 0 + 4
c [unhide-6-6] 2 units, 1250 failed, 1045 tauts, 0 hbrs, 34292 literals
c [transred-2] limit 3776687 based on 3776687 irredundant clauses
c [transred-2] removed 3 transitive binary clauses
c [bca-2] limit of 10000000 steps and 7517763 added (scaled 2)
c [bca-2] 1154842 out of 1160998 literals actually usable 99%
c [bca-2] added 3 blocked clauses in 2327024 steps
c [sweep-2] limit 7517262 based on 3758631 irredundant clauses
c [sweep-2-1] 281035 pos 48.4% + 299384 neg 51.6% = 580419 sched 100.0% ret 79
c [sweep-2-1] 7671670 steps 31 queries 159427.23 avg class size
c [sweep-2-1] 174 decisions 25 SAT calls 17.28 avg env size
c [sweep-2-1] 580337 variables remain 100% (161 retained 0%)
c [decomp-14] removed 64 variables
c [sweep-2-1] removed 64 vars (0 failed, 6 eqs, 7 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 64 vars in TOTAL (1 rounds, 30 queries)
c [phase-count-6] 3755109 negative 99.9% of 3758511 except 3402 0.1%
c [phase-count-6] 3741410 positive 99.5% of 3758511 except 17101 0.5%
c [phase-count-6] less non-negative clauses 3402 than limit 375800 (10.0%)
c [phase-count-6] non-pos/non-neg = 17101/3402 = 5.03 >= 2.00 = 200/100
c [lucky-phase-6] forcing lucky phase -1
c [phase-6] phase bias: 0 positive 0%, 58070 negative 100%
c [score-distribution-6] 7548 pos 1.30%, 8620 min 1.49%, 564266 zero 97.21%
c [score-distribution-6] 2325 different 0.40% out of total 580434 variables
c [simplification-6] removed 3647 variables 0.6% (580434 remain 47%)
c [simplification-6] removed 24357 irredundant clauses 0.6% (3758511 remain 76%)
c [simplification-6] maximum reduction of 1% = max (1%, 1%)
c [simplification-6] forced so keeping old conflict interval 20000
c [simplification-6] conflict limit remains at 25051 (hard 35051)
c [simplification-6] new binary interval 1000
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i  201.6  580433  3758511     23846   18029   2265  9973   11    40  296  29%     27   30    9    4  250%
c i  202.1  580431  3758511     23950   18110   2270  9974   11    40  296  29%     23   30    9    4  240%
c i  202.3  580430  3758511     24022   18168   2277  9976   11    39  296  29%     20   30    9    4  240%
c i  203.0  580429  3758511     24136   18266   2279  9980   11    39  296  29%     16   30    9    4  239%
c i  214.2  580428  3758511     25747   19769   2309  9991   11    41  296  27%     -0   31   10    4  250%
c i  214.9  580427  3758511     25843   19859   2311  9992   11    41  296  26%     -2   31    9    4  244%
c i  216.8  580426  3758511     26147   20144   2317  9994   11    41  296  26%     -6   30   10    4  246%
c 
c [simplification-7] limit 25051 conflicts (hard 35051) hit after 28186 conflicts
c [quatres-3] found 680470 quaternary clauses 99% in total
c [quatres-3-1] removed 2 duplicate quaternary clauses
c [quatres-3-2] added 7 single-self-subsuming ternary resolvents
c [quatres-3-2] added 7 quaternary resolvents
c [ternres-3] limit 15034036 based on 3758509 irredundant clauses
c [ternres-3] 550104 schedulable variables 95%
c [ternres-3] 965 ternary resolvents (0 bin, 965 trn)
c [ternres-3] 534413 variables remain 92% (46011 retained 8%)
c [gauss-2] limit 1879254 based on 3758509 irredundant clauses
c [gauss-2] extracted 13 xors of average arity 2.0
c [gauss-2] connected 26 occurrences of 26 variables (average 1.0)
c [gauss-2] limit 1878775 based on 3757551 irredundant clauses
c [gauss-2] fully completed
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-15] removed 186 variables
c [basicprobe-3] limit 43841831 penalty 2 = 0 + 2
c [basicprobe-3-0] 528 sched 0%, 421 failed, 955 lifted, 2858 hbrs
c [decomp-16] removed 7493 variables
c [basicprobe-3-1] 944 probes remain 0% after last round
c [basicprobe-3-1] 1534 units = 547 failed (36%) + 987 lifted (64%)
c [basicprobe-3-1] removed 8175 variables, found 5012 hbrs
c [bate-1] eliminated 257 asymmetric tautologies during probing
c [unhide-7] limit 438418 with penalty 4 = 0 + 4
c [unhide-7-7] 21 units, 312 failed, 8534 tauts, 0 hbrs, 14374 literals
c [transred-3] limit 3693699 based on 3693699 irredundant clauses
c [transred-3] removed 4 transitive binary clauses
c [block-2] scheduling all variables this time
c [block-2] scheduled 569950 variables 100%
c [block-2] limit of 43841831 steps penalty 3 = 1 + 2
c [block-2] fully completed
c [block-2] transition to [ all 0 rem 0 ] state
c [block-2] eliminated 139 blocked clauses
c [block-2] 139 < 1/100 * 3693695 = 36936 considered unsuccessful
c [cce-2] limit of 21920915 steps penalty 3 = 1 + 2
c [cce-2-1] eliminated 18 clauses out of 242 (7%) of length 8
c [cce-2-1] eliminated 9 clauses out of 134 (7%) of length 7
c [cce-2-1] eliminated 19 clauses out of 68 (28%) of length 6
c [cce-2-1] eliminated 2 clauses out of 1123 (0%) of length 5
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] eliminated 48 large clauses in 21920915 steps
c [cce-2-1] allowing another 10960457 steps for small clauses
c [cce-2-1] scheduling 2537206 clauses = 1166666 binary + 1370540 ternary
c [cce-2-1] tried to eliminate 81 small clauses 0%
c [cce-2-1] eliminated 4 binary clauses 0%
c [cce-2-1] eliminated 4 small clauses 0%
c [cce-2-1] eliminated 4 small clauses in 21920921 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 52 covered clauses in round 1
c [cce-2] eliminated 52 covered clauses in TOTAL during 1 rounds
c [cce-2] 52 < 1/100 * 3677836 = 36778 considered unsuccessful
c [elim-6] 3144 variables 1% will be scheduled this time
c [elim-6] scheduled 3144 variables 1%
c [elim-6] limit of 87683662 steps penalty 3 = 1 + 2
c [elim-6] rescheduling of touched variables disabled
c [elim-6] incomplete 2908 not tried 1% in round 1
c [elim-6] transition to [ all 0 rem 1 ] state
c [elim-6] eliminated 0 = 0% variables out of 3144 scheduled
c [bca-3] limit of 10000000 steps and 7355677 added (scaled 2)
c [bca-3] 1134423 out of 1139902 literals actually usable 100%
c [bca-3] added 2 blocked clauses in 2286893 steps
c [sweep-3] limit 7355174 based on 3677587 irredundant clauses
c [sweep-3-1] 279800 pos 49.1% + 289995 neg 50.9% = 569795 sched 100.0% ret 155
c [sweep-3-1] 7454858 steps 20 queries 150665.95 avg class size
c [sweep-3-1] 248 decisions 12 SAT calls 148.75 avg env size
c [sweep-3-1] 569765 variables remain 100% (185 retained 0%)
c [decomp-17] removed 2104 variables
c [sweep-3-1] removed 2104 vars (0 failed, 7 eqs, 5 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 2104 vars in TOTAL (1 rounds, 19 queries)
c [phase-count-7] 3670287 negative 99.9% of 3673379 except 3092 0.1%
c [phase-count-7] 3657639 positive 99.6% of 3673379 except 15740 0.4%
c [phase-count-7] less non-negative clauses 3092 than limit 367300 (10.0%)
c [phase-count-7] non-pos/non-neg = 15740/3092 = 5.09 >= 2.00 = 200/100
c [lucky-phase-7] forcing lucky phase -1
c [phase-7] phase bias: 0 positive 0%, 52905 negative 100%
c [score-distribution-7] 5121 pos 0.90%, 10102 min 1.78%, 552623 zero 97.32%
c [score-distribution-7] 1537 different 0.27% out of total 567846 variables
c [simplification-7] removed 12578 variables 2.2% (567846 remain 46%)
c [simplification-7] removed 85132 irredundant clauses 2.3% (3673379 remain 74%)
c [simplification-7] maximum reduction of 2% = max (2%, 2%)
c [simplification-7] geometric conflict interval increment 6666 = 20000 / 3
c [simplification-7] new conflict interval 26666
c [simplification-7] penalized conflict interval 26666 = 1 * 26666
c [simplification-7] hard conflict limit 68185 (soft 54852 + delta 13333)
c [simplification-7] new conflict limit 54852 (hard 68185)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i  256.5  567845  3673379     28315   17413   2945 13342   10    40  289  26%      2   28    9    4  227%
c i  256.5  567841  3673379     28316   17413   2945 13342   10    40  289  26%      2   28    9    4  226%
c i  256.5  567712  3673379     28331   17422   2949 13342   10    39  289  26%      1   28    9    4  220%
c i  256.6  567678  3673379     28363   17446   2955 13343   10    39  289  26%      1   28    9    4  214%
c i  256.6  567603  3673379     28364   17446   2955 13343   10    39  289  26%      1   28    9    4  214%
c i  258.3  567602  3673379     28637   17700   2962 13348   10    39  289  26%     -4   28    9    4  217%
c i  258.3  566817  3673379     28638   17700   2962 13348   10    39  289  26%     -4   28    9    4  217%
c i  259.8  565282  3673379     28891   17934   2967 13350   10    39  291  26%     -7   27    9    4  216%
c i  364.5  562770  3673379     49063   37320   3171 13397   10    24  293  41%    245    7    9    5  173%
c i  383.4  562768  3673379     53340   41416   3201 13403   10    23  293  43%     -1    6   10    6  176%
c 
c [simplification-8] limit 54882 conflicts (hard 68185) hit after 57861 conflicts
c [quatres-4] found 646098 quaternary clauses 99% in total
c [quatres-4-1] removed 2 duplicate quaternary clauses
c [quatres-4-2] added 4 single-self-subsuming ternary resolvents
c [quatres-4-2] added 7 quaternary resolvents
c [ternres-4] limit 20030509 with penalty 2 = 0 + 2
c [ternres-4] 518067 schedulable variables 91%
c [ternres-4] 1150 ternary resolvents (0 bin, 1150 trn)
c [ternres-4] 499278 variables remain 89% (63367 retained 11%)
c [decomp-18] removed 9381 variables
c [simpleprobe-4] 456567 schedulable variables 82%
c [simpleprobe-4] limit 50000000 penalty 2 = 0 + 2
c [decomp-19] removed 2463 variables
c [simpleprobe-4] 438877 variables remain 79% (117125 retained 21%)
c [simpleprobe-4] removed 2463 variables, found 1447 hbrs, 9 units
c [unhide-8] limit 1001525 with penalty 4 = 0 + 4
c [unhide-8-8] 27 units, 1447 failed, 2978 tauts, 0 hbrs, 25445 literals
c [transred-4] limit 3585246 based on 3585246 irredundant clauses
c [transred-4] removed 7 transitive binary clauses
c [bca-4] limit of 10000000 steps and 7079002 added (scaled 2)
c [bca-4] 1092420 out of 1097332 literals actually usable 100%
c [bca-4] added 1 blocked clauses in 2227173 steps
c [sweep-4] limit 7078498 based on 3539249 irredundant clauses
c [sweep-4-1] 295408 pos 53.9% + 253083 neg 46.1% = 548491 sched 100.0% ret 174
c [sweep-4-1] 7190173 steps 30 queries 133395.27 avg class size
c [sweep-4-1] 138 decisions 26 SAT calls 16.73 avg env size
c [sweep-4-1] 548349 variables remain 100% (268 retained 0%)
c [decomp-20] removed 2806 variables
c [sweep-4-1] removed 2806 vars (0 failed, 6 eqs, 4 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 2806 vars in TOTAL (1 rounds, 29 queries)
c [phase-count-8] 3530187 negative 99.9% of 3533315 except 3128 0.1%
c [phase-count-8] 3518413 positive 99.6% of 3533315 except 14902 0.4%
c [phase-count-8] less non-negative clauses 3128 than limit 353300 (10.0%)
c [phase-count-8] non-pos/non-neg = 14902/3128 = 4.76 >= 2.00 = 200/100
c [lucky-phase-8] forcing lucky phase -1
c [phase-8] phase bias: 0 positive 0%, 22590 negative 100%
c [score-distribution-8] 2340 pos 0.43%, 12072 min 2.21%, 531447 zero 97.36%
c [score-distribution-8] 971 different 0.18% out of total 545859 variables
c [simplification-8] removed 16786 variables 3.0% (545859 remain 44%)
c [simplification-8] removed 140064 irredundant clauses 3.8% (3533315 remain 72%)
c [simplification-8] maximum reduction of 4% = max (3%, 4%)
c [simplification-8] geometric conflict interval increment 5333 = 26666 / 5
c [simplification-8] new conflict interval 31999
c [simplification-8] penalized conflict interval 31999 = 1 * 31999
c [simplification-8] hard conflict limit 105859 (soft 89860 + delta 15999)
c [simplification-8] new conflict limit 89860 (hard 105859)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i  472.4  545858  3533315     70372   53386   4042 11376   11    20  287  53%    177    2   11    7  154%
c -  491.3  545566  3533315     74872   20385   4055 11381   11    20  281  54%    -16    2   12    7  166%
c 
c [simplification-9] limit 89860 conflicts (hard 105859) hit after 89862 conflicts
c [quatres-5] found 612321 quaternary clauses 99% in total
c [quatres-5-1] removed 10 duplicate quaternary clauses
c [quatres-5-2] added 2 single-self-subsuming ternary resolvents
c [quatres-5-2] added 13 quaternary resolvents
c [ternres-5] limit 30070994 with penalty 2 = 0 + 2
c [ternres-5] 484050 schedulable variables 89%
c [ternres-5] 3153 ternary resolvents (0 bin, 3153 trn)
c [ternres-5] 453986 variables remain 83% (91580 retained 17%)
c [decomp-21] removed 1186 variables
c [treelook-4] limit 3007099 penalty 2 = 0 + 2 boost 1
c [treelook-4] scheduled 189612 literals 17%
c [treelook-4] scheduling used 3007102 steps
c [treelook-4] not fully scheduled
c [treelook-4] limit 3007099 penalty 2 = 0 + 2 boost 1
c [treelook-4] used 3061705 steps
c [treelook-4] 189290 literals remain 17%
c [treelook-4] 2326 variables remain to probed next time 0%
c [decomp-22] removed 48 variables
c [treelook-4] removed 79 variables, found 3903 hbrs
c [unhide-9] limit 1250000 with penalty 4 = 0 + 4
c [unhide-9-9] 2 units, 223 failed, 8927 tauts, 0 hbrs, 11455 literals
c [transred-5] limit 3510664 based on 3510664 irredundant clauses
c [transred-5] removed 3 transitive binary clauses
c [bca-5] limit of 10000000 steps and 6991836 added (scaled 2)
c [bca-5] 1080391 out of 1084264 literals actually usable 100%
c [bca-5] added 2 blocked clauses in 2195663 steps
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 90212982 penalty 2 = 0 + 2
c [sweep-5-1] 299700 pos 55.3% + 242173 neg 44.7% = 541873 sched 100.0% ret 258
c [sweep-5-1] 93472324 steps 150 queries 48708.20 avg class size
c [sweep-5-1] 1714 decisions 116 SAT calls 75.61 avg env size
c [sweep-5-1] 540786 variables remain 100% (1342 retained 0%)
c [decomp-23] removed 675 variables
c [sweep-5-1] removed 675 vars (0 failed, 33 eqs, 42 impls)
c [sweep-5] considered successful since not run to completion yet
c [sweep-5] removed 675 vars in TOTAL (1 rounds, 149 queries)
c [phase-count-9] 3491299 negative 99.9% of 3494311 except 3012 0.1%
c [phase-count-9] 3479923 positive 99.6% of 3494311 except 14388 0.4%
c [phase-count-9] less non-negative clauses 3012 than limit 349400 (10.0%)
c [phase-count-9] non-pos/non-neg = 14388/3012 = 4.78 >= 2.00 = 200/100
c [lucky-phase-9] forcing lucky phase -1
c [phase-9] phase bias: 0 positive 0%, 12526 negative 100%
c [score-distribution-9] 2347 pos 0.43%, 12172 min 2.25%, 526937 zero 97.32%
c [score-distribution-9] 1014 different 0.19% out of total 541456 variables
c [simplification-9] removed 4110 variables 0.8% (541456 remain 44%)
c [simplification-9] removed 39004 irredundant clauses 1.1% (3494311 remain 71%)
c [simplification-9] maximum reduction of 1% = max (1%, 1%)
c [simplification-9] geometric conflict interval increment 15999 = 31999 / 2
c [simplification-9] new conflict interval 47998
c [simplification-9] penalized conflict interval 47998 = 1 * 47998
c [simplification-9] hard conflict limit 161859 (soft 137860 + delta 23999)
c [simplification-9] new conflict limit 137860 (hard 161859)
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 -  663.8  541456  3494311    119204   28496   7087 15533    9    12  280  76%    494   -6    8    9   93%
c i  785.1  541455  3494311    159993   61495   7258 15572    8    10  286  78%    739   -6    5    9   59%
c 
c [simplification-10] limit 137860 conflicts (hard 161859) hit after 161859 conflicts
c [quatres-6] found 596741 quaternary clauses 98% in total
c [quatres-6-1] removed 3 duplicate quaternary clauses
c [quatres-6-2] added 2 single-self-subsuming ternary resolvents
c [quatres-6-2] added 13 quaternary resolvents
c [ternres-6] limit 48958316 with penalty 2 = 0 + 2
c [ternres-6] 450474 schedulable variables 83%
c [ternres-6] 6725 ternary resolvents (0 bin, 6725 trn)
c [ternres-6] 402253 variables remain 74% (139129 retained 26%)
c [card-4] limit 3059894 penalty 5 = 3 + 2
c [card-4] found 390 at-most-one constraints of average size 3.1
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 3059894 for elimination
c [card-4] 390 out of 390 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [gauss-3] limit 2447915 penalty 4 = 2 + 2
c [gauss-3] extracted 9 xors of average arity 2.3
c [gauss-3] connected 21 occurrences of 21 variables (average 1.0)
c [gauss-3] limit 2447915 penalty 4 = 2 + 2
c [gauss-3] fully completed
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-24] removed 23 variables
c [basicprobe-4] limit 100000000 penalty 2 = 0 + 2
c [basicprobe-4-0] 993 sched 0%, 267 failed, 6 lifted, 5627 hbrs
c [decomp-25] removed 2607 variables
c [basicprobe-4-1] 1374 sched 0%, 345 failed, 21 lifted, 4505 hbrs
c [decomp-26] removed 2347 variables
c [basicprobe-4-2] 1056 probes remain 0% after last round
c [basicprobe-4-2] 730 units = 703 failed (96%) + 27 lifted (4%)
c [basicprobe-4-2] removed 5811 variables, found 11752 hbrs
c [bate-2] eliminated 336 asymmetric tautologies during probing
c [unhide-10] limit 1250000 with penalty 4 = 0 + 4
c [unhide-10-10] 8 units, 3797 failed, 7293 tauts, 0 hbrs, 24798 literals
c [transred-6] limit 3453260 based on 3453260 irredundant clauses
c [transred-6] removed 5 transitive binary clauses
c [block-3] scheduling all variables this time
c [block-3] scheduled 533300 variables 100%
c [block-3] limit of 50000000 steps penalty 4 = 2 + 2
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 219 blocked clauses
c [block-3] 219 < 1/100 * 3453257 = 34532 considered unsuccessful
c [cce-3] limit of 61197896 steps penalty 4 = 2 + 2
c [cce-3-1] eliminated 13 clauses out of 147 (9%) of length 8
c [cce-3-1] eliminated 1 clauses out of 199 (1%) of length 7
c [cce-3-1] eliminated 1 clauses out of 53 (2%) of length 6
c [cce-3-1] eliminated 267 clauses out of 706 (38%) of length 5
c [cce-3-1] eliminated 2 clauses out of 572210 (0%) of length 4
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 284 large clauses in 61197896 steps
c [cce-3-1] allowing another 30598948 steps for small clauses
c [cce-3-1] scheduling 2392887 clauses = 1089780 binary + 1303107 ternary
c [cce-3-1] tried to eliminate 236 small clauses 0%
c [cce-3-1] eliminated 6 binary clauses 0%
c [cce-3-1] eliminated 6 small clauses 0%
c [cce-3-1] eliminated 6 small clauses in 61197903 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 290 covered clauses in round 1
c [cce-3] eliminated 290 covered clauses in TOTAL during 1 rounds
c [cce-3] 290 < 1/100 * 3439939 = 34399 considered unsuccessful
c [elim-7] scheduling all variables this time
c [elim-7] scheduled 533299 variables 100%
c [elim-7] limit of 50000000 steps penalty 4 = 2 + 2
c [elim-7] rescheduling of touched variables disabled
c [elim-7] incomplete 345405 not tried 65% in round 1
c [elim-7] transition to [ all 1 rem 1 ] state
c [elim-7] eliminated 7161 = 1% variables out of 533299 scheduled
c [bca-6] limit of 10000000 steps and 6855219 added (scaled 2)
c [bca-6] 1048337 out of 1052278 literals actually usable 100%
c [bca-6] added 2 blocked clauses in 2133693 steps
c [sweep-6] limit 14687495 penalty 2 = 0 + 2
c [sweep-6-1] 294264 pos 56.1% + 230714 neg 43.9% = 524978 sched 99.8% ret 1160
c [sweep-6-1] 15023394 steps 33 queries 119407.94 avg class size
c [sweep-6-1] 251 decisions 25 SAT calls 23.64 avg env size
c [sweep-6-1] 524901 variables remain 100% (1237 retained 0%)
c [decomp-27] removed 65 variables
c [sweep-6-1] removed 65 vars (0 failed, 9 eqs, 17 impls)
c [sweep-6] considered successful since not run to completion yet
c [sweep-6] removed 65 vars in TOTAL (1 rounds, 32 queries)
c [phase-count-10] 3423912 negative 99.9% of 3427236 except 3324 0.1%
c [phase-count-10] 3412626 positive 99.6% of 3427236 except 14610 0.4%
c [phase-count-10] less non-negative clauses 3324 than limit 342700 (10.0%)
c [phase-count-10] non-pos/non-neg = 14610/3324 = 4.40 >= 2.00 = 200/100
c [lucky-phase-10] forcing lucky phase -1
c [phase-10] phase bias: 0 positive 0%, 8925 negative 100%
c [score-distribution-10] 1523 pos 0.29%, 13146 min 2.50%, 511404 zero 97.21%
c [score-distribution-10] 626 different 0.12% out of total 526073 variables
c [simplification-10] removed 15309 variables 2.8% (526073 remain 43%)
c [simplification-10] removed 67075 irredundant clauses 1.9% (3427236 remain 69%)
c [simplification-10] maximum reduction of 3% = max (3%, 2%)
c [simplification-10] geometric conflict interval increment 11999 = 47998 / 4
c [simplification-10] new conflict interval 59997
c [simplification-10] penalized conflict interval 59997 = 1 * 59997
c [simplification-10] hard conflict limit 251854 (soft 221856 + delta 29998)
c [simplification-10] new conflict limit 221856 (hard 251854)
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 -  924.7  526073  3427236    195758   34845  11090 13989   10    14  277  72%     35   -1    8    9   92%
c i  931.0  526072  3427236    198151   36541  11121 13997    9    12  279  75%     70   -3    6    9   64%
c i  944.1  526031  3427236    203300   40592  11151 14005    7     9  279  77%   -414   -5    6    9   64%
c i  961.6  525413  3427236    209261   45110  11186 14016    8    10  279  77%   -367   -4    7    9   77%
c i  962.4  524999  3427236    209536   45273  11197 14021    8    10  279  77%   -383   -4    6    9   71%
c i  963.5  524994  3427236    209889   45493  11208 14026    7    10  279  77%   -397   -4    6    9   66%
c i  965.2  524991  3427236    210366   45789  11218 14032    7     9  279  78%   -409   -4    6    9   65%
c i  965.4  519200  3427236    210419   45810  11220 14035    7     9  279  78%   -410   -4    6    9   63%
c i  965.5  515917  3427236    210439   45826  11220 14035    7     9  279  78%   -410   -4    5    9   62%
c i  965.5  515872  3427236    210445   45828  11221 14036    7     9  279  78%   -410   -4    5    9   61%
c i  965.6  514260  3427236    210459   45833  11225 14037    7     9  279  78%   -411   -4    5    9   60%
c i  965.6  512327  3427236    210466   45831  11226 14038    7     9  279  78%   -411   -4    5    9   58%
c 0  965.6  510293  3427236    210466   45831  11226 14038    7     9  279  78%   -411   -4    5    9   58%
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 
s UNSATISFIABLE
c
c bate: 593 basic ate = 500 trn 84% + 93 lrg 16% in 2 updates
c bcas: 6 count, 13 added (169 skipped), 13504184 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, 1521 removed, 34663693 resolutions, 101113672 steps
c blkd: 1337 blocking literals 0%, 1 pure
c bump: 210095 bumped seen, 12650190 lits 60.2 on average
c card: 4 count, 0 units, 0 am1, 12540841 steps
c card: 0 rescheduled, 0 eliminated, 0 resolved, 11474 subsumed
c card: 1093 at-most-one constraints found, average size 3.26
c card: 1093 at-most-one constraints used 100%, average size 3.26
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: 3 cces, 344 eliminated, 335 ate 97%, 9 abce 3%
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: 17243385 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 65 gcs, 0 rescored clauses, 110 rescored vars
c dcps: 27 decompositions, 17069 equivalent 1%
c deco: 0 decision-only clauses 0%, 0% reduction
c decs: 637605 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c dsch: 4089411 push, 2853492 pop (2853492 dec 100%)
c dsch: 78889213 swaps, 0 down, 265952015 up
c elms: 7 elims, 398256 eliminated 32%, 0 pure 0%
c elms: 7 rounds, 1.0 rounds/bve
c elms: 398236 small 100%, 19 large 0%
c elms: 1276254 tried small, 398236 succeeded 31%, 878018 failed 69%
c elms: 14406 subsumed, 4394 strengthened, 0 blocked
c elms: 25036669 copies, 20009717 resolutions, 66815616 ipos
c elms: 2451118 subchks, 1282793 strchks
c gaus: 3 extractions, 58 extracted, 2.1 size, 3 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 12450246 steps, 6225123 extr 50%, 199 elim 0%
c glue: 9.9 orig avg, 9.9 real avg, 2.5 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 81146 = 1898 simple 2% + 77048 trn 95% + 2200 lrg 3%, 8165 sub 10%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 210095 clauses, 19.0 length
c lrnd: 4001403 lits = 6237497 orig - 2236094 removed 36%
c lrnd: 66008 uips 31%, 125274 flips 60%
c mins: 204618 mins 97%, 455 bin 0%, 5022 size 2%
c mins: 8215422 poisoned searches, 779490 hits, 9% hit rate
c mins: 13440721 used twice searches, 1145236 hits, 9% hit rate
c move: moved 8386, 100 bin 1%, 8286 trn 99%
c otfs: 984 driving 32%, 2114 restarting 68%
c otfs: str 3098, 2952 red 95%, 146 irr 5%
c otfs: str 3098, 0 bin 0%, 151 trn 5%, 2947 lrg 95%
c otfs: sub 15, 15 red 100%, 0 irr 0%
c otfs: sub 15, 0 bin 0%, 2 trn 13%, 13 lrg 87%
c phas: 10 computed, 2189260 set, 0 pos (0%), 2189260 neg (100%)
c prbs: 4 basic, 9187 probed, 1484 failed, 1072 lifted
c prbs: 4 simple, 1063570 probed, 11 failed, 50 eqs
c prbs: 4 treelook, 312 probed, 24 failed, 0 lifted
c prom: 29135 locked 7% out of 423764 tried
c prps: 2442480069 props, 3795 props/dec
c prps: 99% srch, 1% simp, 0% lkhd
c quat: 6 count, 185 quat, 61 self1, 0 self2, 37 dup
c redc: 4711 clauses 9%, 49917 tried 24%, 15 sat 0%
c redc: 5780 lits 1%, 571253 tried 9%, 15 sat 0%
c redc: 310 times jump level reduced, 2.4 levels on average
c reds: 3 count, 70155.3 conflicts per reduce
c reds: 0 memlim 0%, 3 arith 100%
c reds: 76505 collected 78%, 21987 retired 22%
c rmbd: 32927 removed, 526 red 2%
c rsts: 12390 restarts 100%, 0 skipped 0%
c rsts: 0 saturating 0%, 0 reuse 0%
c rsts: 0 kept 0.0% average 0.0%
c scnc: 1 count, 1.200 min (200/1000), 1.200 max (200/1000)
c simp: 10 count, 8 confs 80%, 0 vars 0%
c simp: 1 its 10%, 1 bin 10%, 0 trns 0%
c subl: 210095 count (86730 tried 0.4), 24771 sub out of 206556 (12.0%)
c swps: 6 count, 6 rounds, 291 queries (48.5/round)
c swps: 231 sat calls, 8 unsat (2.7% success rate)
c swps: 2831 decisions 12.3, 613 conflicts 2.7
c swps; 96872.1 avg class size, 59.7 avg environment size
c swps: 0 failed, 86 impls, 67 equivs
c swp0: 94 type 0 queries, 19 unsat (20.2%), 90 sat (95.7%)
c swp1: 197 type 1 queries, 176 unsat (89.3%), 134 sat (68.0%)
c sync: 0 produced units, 0 successful consumptions 0%
c sync: 0 consume units calls, 0 tried 0%, 0 success 0%
c sync: 0 produced clauses, 0 successful consumptions 0%
c sync: 0 consume clause calls, 0 tried 0%, 0 success 0%
c time: 1695851 calls to obtain time
c tops: 310653 fixed 25%, 49 its, 4295.22 confs/it
c trds: 6 transitive reductions, 25 removed, 0 failed
c trds: 2679 nodes, 2724 edges, 21865331 steps
c trim: 138893 words, 0.5 MB
c trnr: 6 count, 0 bin, 13196 trn, 144408303 steps
c unhd: 10 count, 10 rounds, 191513901 steps
c unhd: 291 non-trivial sccs of average size 8.1
c unhd: 78 units, 74 bin, 1 trn, 3 lrg
c unhd: 7706 failed, 7511 stamp, 0 lits, 14 bin, 150 trn, 3 lrg
c unhd: 81304 tauts, 144 bin 0%, 14994 trn 18%, 1451 lrg 2%
c unhd: 81304 tauts, 64715 stamp 80%, 47559 red 58%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 125938 str, 74 bin 0%, 7055 trn 6%, 118809 lrg 94%, 51558 red 41%
c vars: 510293 remaining 41% and 725978 removed 59% out of 1236271
c vars: 310653 fixed 25%, 398256 eliminated 32%, 17069 equivalent 1%
c vsts: 24776928347 visits, 99% srch, 1% simp, 0% lkhd
c vsts: 10.1 search visits per propagation, 116557.8 per conflict
c wchs: 1863734122 pushed, 179534663 enlarged, 102 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all         206741         76505         21987       5287707       1755061        124448
c 
c  0 0         20463  10      1426   2         0   0   3265731  62    928478  53     53593  43     0.6
c  1 5         15108   7      3651   5       735   3    673871  13<   242160  14<    18371  15<    0.4
c  2 6         58544  28     21424  28      4007  18    924490  17    371600  21     32275  26     1.4
c  3 9         70834  34<    31134  41<     8776  40<   318505   6    158645   9     15312  12     1.6
c  4 14        32832  16     15670  20      6647  30     83503   2     42812   2      3847   3     1.1
c  5 21         7134   3      2769   4      1568   7     16853   0      8817   1       798   1     0.3
c  6 30         1468   1       351   0       216   1      3956   0      2068   0       193   0     0.2
c  7 41          307   0        68   0        34   0       721   0       430   0        54   0     0.1
c  8 54           48   0        11   0         3   0        74   0        49   0         5   0     0.0
c  9 69            2   0         1   0         0   0         2   0         2   0         0   0     0.0
c 10 86            1   0         0   0         1   0         1   0         0   0         0   0     0.0
c 
c avg                  2.5           2.9           3.2           0.7           1.0           1.2
c std                  1.3           1.0           1.0           1.1           1.2           1.3
c 
c   62.899   7% elim
c   31.607   3% probe
c   27.051   3% quatres
c   17.282   2% sweep
c   17.213   2% unhide
c    9.742   1% block
c    8.622   1% bca
c    7.564   1% cce
c 
c   13.220 < 1% rest (below)
c 
c    4.430   0% gauss
c    2.634   0% transred
c    2.013   0% rescore
c    1.571   0% ternres
c    1.075   0% card
c    0.856   0% decide
c    0.641   0% bump
c    0.000   0% locs
c    0.000   0% queuesort
c ==================================
c    9.683   1% preprocessing     4%
c  210.755  22% inprocessing     96%
c ==================================
c  220.437  23% simplifying
c  745.145  77% search
c ==================================
c  965.605 100% all
c 
c        210466 conflicts,         218.0 confs/sec
c          2650 ternaries,          79.4 confs/ternary
c           612 binaries,          343.9 confs/binary
c            49 iterations,       4295.2 confs/iteration
c 
c             3 reductions,          0.0 redus/sec,  70155.3 confs/reduction
c         12390 restarts,           12.8 rests/sec,     17.0 confs/restart
c        637605 decisions,         660.3 decis/sec,      3.0 decis/conflict
c    2442480069 propagations,  2529480.7 props/sec,   3830.7 props/decision
c 
c 965.6 seconds, 438.8 MB
c launch: done
