c launch: /data/cnf/sc2014/app/atco_enc2_opt2_20_11.cnf.bz2
c host: atom10
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/atco_enc2_opt2_20_11.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/atco_enc2_opt2_20_11.cnf.bz2
c no embedded options
c found 'p cnf 167075 6571833' header
c read 167075 variables, 6571833 clauses, 21183250 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=6
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 166190 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] AVG (--score=6)
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  166190  6549347         0       0      0     0    0     0  290   0%      0    0    0    0    0%
c 
c [simplification-1] limit 0 conflicts (hard 0) hit after 0 conflicts
c [card-1] limit 1637336 based on 6549347 irredundant clauses
c [card-1] found 1558 at-most-one constraints of average size 3.0
c [card-1] no at-most-two constraint found
c [card-1] using previous limit 1637336 for elimination
c [card-1] 1558 out of 1558 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 5689 variables
c [simpleprobe-1] all 161386 free variables schedulable
c [simpleprobe-1] boosting simple probing limit by 10
c [simpleprobe-1] limit 12996764 based on 6498382 irredundant clauses
c [decomp-2] removed 3 variables
c [simpleprobe-1] 161383 variables remain 100% (0 retained 0%)
c [simpleprobe-1] removed 3 variables, found 1170 hbrs, 0 units
c [unhide-1] limit 406148 based on 6498379 irredundant clauses
c [unhide-1-1] 3 units, 116 failed, 98952 tauts, 0 hbrs, 15 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 161301 variables 100%
c [elim-1] limit of 6402394 steps based on 6402394 irredundant clauses
c [elim-1] rescheduling of touched variables disabled
c [elim-1] incomplete 158434 not tried 98% in round 1
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 2867 = 2% variables out of 161301 scheduled
c [elim-1] considered successful since not run to completion yet
c [phase-count-1] 5244728 negative 83.1% of 6310279 except 1065551 16.9%
c [phase-count-1] 5367308 positive 85.1% of 6310279 except 942971 14.9%
c [phase-1] phase bias: 69404 positive 44%, 89030 negative 56%
c [sort-queue-1] sorted 158434 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 158434 (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 6206 variables 3.8% (158434 remain 95%)
c [simplification-1] removed 239068 irredundant clauses 3.7% (6310279 remain 96%)
c [simplification-1] maximum reduction of 4% = max (4%, 4%)
c [simplification-1] geometric conflict interval increment 4000 = 20000 / 5
c [simplification-1] new conflict interval 4000
c [simplification-1] penalized conflict interval 4000 = 1 * 4000
c [simplification-1] hard conflict limit 14000 (soft 4000 + delta 10000)
c [simplification-1] new conflict limit 4000 (hard 14000)
c 
c [simplification-2] limit 4000 conflicts (hard 14000) hit after 4003 conflicts
c [decomp-3] removed 38 variables
c [simpleprobe-2] all 158396 free variables schedulable
c [simpleprobe-2] limit 12620482 based on 6310241 irredundant clauses
c [decomp-4] removed 187 variables
c [simpleprobe-2] 158209 variables remain 100% (0 retained 0%)
c [simpleprobe-2] removed 187 variables, found 1049 hbrs, 0 units
c [treelook-1] limit 1577513 based on 6310054 irredundant clauses
c [treelook-1] scheduled 30139 literals 10%
c [treelook-1] scheduling used 1580013 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 1577513 based on 6310054 irredundant clauses
c [treelook-1] used 1671454 steps
c [treelook-1] 30112 literals remain 10%
c [treelook-1] 29308 variables remain to probed next time 19%
c [decomp-5] removed 3 variables
c [treelook-1] removed 3 variables, found 927 hbrs
c [basicprobe-1] limit 50480432 based on 6310054 irredundant clauses
c [basicprobe-1-0] 5409 probes remain 3% after last round
c [basicprobe-1-0] 98 units = 98 failed (100%) + 0 lifted (0%)
c [basicprobe-1-0] removed 125 variables, found 37511 hbrs
c [unhide-2] limit 394378 based on 6310054 irredundant clauses
c [unhide-2-2] 0 units, 7 failed, 16130 tauts, 0 hbrs, 2261 literals
c [elim-2] 158074 variables 100% will be scheduled this time
c [elim-2] scheduled 158074 variables 100%
c [elim-2] limit of 6308395 steps based on 6308395 irredundant clauses
c [elim-2] rescheduling of touched variables disabled
c [elim-2] incomplete 155890 not tried 99% in round 1
c [elim-2] transition to [ all 0 rem 1 ] state
c [elim-2] eliminated 2184 = 1% variables out of 158074 scheduled
c [elim-2] considered successful since not run to completion yet
c [phase-count-2] 5145284 negative 83.0% of 6201722 except 1056438 17.0%
c [phase-count-2] 5258756 positive 84.8% of 6201722 except 942966 15.2%
c [phase-2] phase bias: 3025 positive 64%, 1719 negative 36%
c [sort-queue-2] sorted 153795 enqueued variables after 4003 conflicts
c [score-dist-2] active 2095 (1%), one 0 (0%), zero 153795 (99%)
c [score-dist-2] max exp 513, different 12 (2%)
c [score-dist-2] median active exp 513, avg 512.2
c [simplification-2] removed 2544 variables 1.6% (155890 remain 94%)
c [simplification-2] removed 108557 irredundant clauses 1.7% (6201722 remain 95%)
c [simplification-2] maximum reduction of 2% = max (2%, 2%)
c [simplification-2] geometric conflict interval increment 6666 = 20000 / 3
c [simplification-2] new conflict interval 10666
c [simplification-2] penalized conflict interval 10666 = 1 * 10666
c [simplification-2] hard conflict limit 24669 (soft 14669 + delta 10000)
c [simplification-2] new conflict limit 14669 (hard 24669)
c 
c [simplification-3] limit 14669 conflicts (hard 24669) hit after 14669 conflicts
c [card-2] limit 1550430 based on 6201722 irredundant clauses
c [card-2] found 1265 at-most-one constraints of average size 3.0
c [card-2] no at-most-two constraint found
c [card-2] using previous limit 1550430 for elimination
c [card-2] 1265 out of 1265 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [decomp-6] removed 2546 variables
c [treelook-2] limit 1550026 based on 6200107 irredundant clauses
c [treelook-2] scheduled 34082 literals 11%
c [treelook-2] scheduling used 1571795 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 1550026 based on 6200107 irredundant clauses
c [treelook-2] used 1560127 steps
c [treelook-2] 34026 literals remain 11%
c [treelook-2] 10249 variables remain to probed next time 7%
c [decomp-7] removed 9 variables
c [treelook-2] removed 9 variables, found 269 hbrs
c [unhide-3] limit 387506 based on 6200101 irredundant clauses
c [unhide-3-3] 0 units, 2 failed, 6341 tauts, 0 hbrs, 6534 literals
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 153333 variables 100%
c [elim-3] limit of 21028393 steps penalty 3 = 0 + 3
c [elim-3] rescheduling of touched variables disabled
c [elim-3] incomplete 121052 not tried 79% in round 1
c [elim-3] transition to [ all 1 rem 1 ] state
c [elim-3] eliminated 15358 = 10% variables out of 153333 scheduled
c [elim-3] considered successful since not run to completion yet
c [phase-count-3] 4998647 negative 82.6% of 6053142 except 1054495 17.4%
c [phase-count-3] 5150098 positive 85.1% of 6053142 except 903044 14.9%
c [phase-3] phase bias: 3619 positive 82%, 818 negative 18%
c [sort-queue-3] sorted 135717 enqueued variables after 14669 conflicts
c [score-dist-3] active 2258 (2%), one 0 (0%), zero 135717 (98%)
c [score-dist-3] max exp 515, different 13 (3%)
c [score-dist-3] median active exp 515, avg 514.2
c [simplification-3] removed 17915 variables 11.5% (137975 remain 83%)
c [simplification-3] removed 148580 irredundant clauses 2.4% (6053142 remain 92%)
c [simplification-3] maximum reduction of 11% = max (11%, 2%)
c [simplification-3] large reduction 11% >= 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 26669 (soft 16669 + delta 10000)
c [simplification-3] new conflict limit 16669 (hard 26669)
c 
c [simplification-4] limit 16669 conflicts (hard 26669) hit after 16669 conflicts
c [decomp-8] removed 123 variables
c [basicprobe-2] limit 48423256 based on 6052907 irredundant clauses
c [basicprobe-2-0] 1626 probes remain 1% after last round
c [basicprobe-2-0] 6 units = 6 failed (100%) + 0 lifted (0%)
c [basicprobe-2-0] removed 9 variables, found 22893 hbrs
c [unhide-4] limit 378306 based on 6052907 irredundant clauses
c [unhide-4-4] 0 units, 0 failed, 10266 tauts, 0 hbrs, 5989 literals
c [elim-4] 120925 variables 88% will be scheduled this time
c [elim-4] scheduled 120925 variables 88%
c [elim-4] boosting limit by 20
c [elim-4] limit of 480759995 steps penalty 3 = 0 + 3
c [elim-4] rescheduling of touched variables disabled
c [elim-4] incomplete 66976 not tried 49% in round 1
c [elim-4] transition to [ all 0 rem 1 ] state
c [elim-4] eliminated 735 = 1% variables out of 120925 scheduled
c [elim-4] considered successful since not run to completion yet
c [phase-count-4] 4993459 negative 82.6% of 6046313 except 1052854 17.4%
c [phase-count-4] 5143500 positive 85.1% of 6046313 except 902813 14.9%
c [phase-4] phase bias: 1619 positive 67%, 793 negative 33%
c [sort-queue-4] sorted 134793 enqueued variables after 16669 conflicts
c [score-dist-4] active 2315 (2%), one 0 (0%), zero 134793 (98%)
c [score-dist-4] max exp 516, different 14 (3%)
c [score-dist-4] median active exp 515, avg 514.6
c [simplification-4] removed 867 variables 0.6% (137108 remain 83%)
c [simplification-4] removed 6829 irredundant clauses 0.1% (6046313 remain 92%)
c [simplification-4] maximum reduction of 1% = max (1%, 0%)
c [simplification-4] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-4] new conflict interval 20666
c [simplification-4] penalized conflict interval 20666 = 1 * 20666
c [simplification-4] hard conflict limit 47668 (soft 37335 + delta 10333)
c [simplification-4] new conflict limit 37335 (hard 47668)
c 
c [simplification-5] limit 37335 conflicts (hard 47668) hit after 37335 conflicts
c [quatres-1] found 145438 quaternary clauses 30% in total
c [quatres-1-2] added 130 single-self-subsuming ternary resolvents
c [quatres-1-2] added 298 quaternary resolvents
c [ternres-1] boosting ternary resolution limit by 5
c [ternres-1] limit 24185248 based on 6046312 irredundant clauses
c [ternres-1] all 137108 free variables schedulable
c [ternres-1] 14 ternary resolvents (0 bin, 14 trn)
c [ternres-1] 133585 variables remain 97% (3523 retained 3%)
c [gauss-1] limit 3023156 based on 6046312 irredundant clauses
c [gauss-1] extracted 54 xors of average arity 2.7
c [gauss-1] connected 146 occurrences of 143 variables (average 1.0)
c [gauss-1] limit 3023156 based on 6046312 irredundant clauses
c [gauss-1] fully completed
c [gauss-1] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-9] removed 635 variables
c [simpleprobe-3] all 136473 free variables schedulable
c [simpleprobe-3] limit 12092118 based on 6046059 irredundant clauses
c [decomp-10] removed 11 variables
c [simpleprobe-3] 127483 variables remain 93% (8979 retained 7%)
c [simpleprobe-3] removed 11 variables, found 1008 hbrs, 0 units
c [transred-1] limit 6046038 based on 6046038 irredundant clauses
c [transred-1] removed 1958 transitive binary clauses
c [block-1] scheduling all variables this time
c [block-1] scheduled 136462 variables 100%
c [block-1] boosting limit by 10
c [block-1] limit of 273463580 steps penalty 3 = 0 + 3
c [block-1] fully completed
c [block-1] transition to [ all 0 rem 0 ] state
c [block-1] eliminated 8963 blocked clauses
c [block-1] 8963 < 1/100 * 6044891 = 60448 considered unsuccessful
c [cce-1] limit of 13673179 steps penalty 3 = 0 + 3
c [cce-1-1] eliminated 5 clauses out of 11 (45%) of length 26
c [cce-1-1] eliminated 8 clauses out of 192 (4%) of length 25
c [cce-1-1] eliminated 8 clauses out of 756 (1%) of length 24
c [cce-1-1] eliminated 6 clauses out of 2727 (0%) of length 23
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 27 large clauses in 13673181 steps
c [cce-1-1] allowing another 6836590 steps for small clauses
c [cce-1-1] scheduling 5521227 clauses = 323377 binary + 5197850 ternary
c [cce-1-1] tried to eliminate 163 small clauses 0%
c [cce-1-1] eliminated 5 binary clauses 0%
c [cce-1-1] eliminated 5 small clauses 0%
c [cce-1-1] eliminated 5 small clauses in 13673205 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 32 covered clauses in round 1
c [cce-1] eliminated 32 covered clauses in TOTAL during 1 rounds
c [cce-1] 32 < 1/100 * 6035928 = 60359 considered unsuccessful
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 136462 variables 100%
c [elim-5] limit of 54692716 steps penalty 3 = 0 + 3
c [elim-5] rescheduling of touched variables disabled
c [elim-5] incomplete 102677 not tried 75% in round 1
c [elim-5] transition to [ all 1 rem 1 ] state
c [elim-5] eliminated 418 = 0% variables out of 136462 scheduled
c [elim-5] 418 < 1/100 * 136462 = 1364 considered unsuccessful
c [bca-1] limit of 10000000 steps and 12068986 added (scaled 2)
c [bca-1] 268894 out of 272090 literals actually usable 99%
c [bca-1] added 8784 blocked clauses in 728736 steps
c [sweep-1] limit 12068486 based on 6034243 irredundant clauses
c [sweep-1-1] 26664 pos 19.6% + 109380 neg 80.4% = 136044 sched 100.0% ret 0
c [sweep-1-1] 12299441 steps 99 queries 27784.42 avg class size
c [sweep-1-1] 3804 decisions 92 SAT calls 215.59 avg env size
c [sweep-1-1] 135209 variables remain 99% (835 retained 1%)
c [decomp-11] removed 62 variables
c [sweep-1-1] removed 62 vars (0 failed, 8 eqs, 6 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 62 vars in TOTAL (1 rounds, 98 queries)
c [phase-count-5] 4983685 negative 82.6% of 6034195 except 1050510 17.4%
c [phase-count-5] 5132527 positive 85.1% of 6034195 except 901668 14.9%
c [phase-5] phase bias: 673 positive 69%, 304 negative 31%
c [sort-queue-5] sorted 132959 enqueued variables after 37335 conflicts
c [score-dist-5] active 3023 (2%), one 0 (0%), zero 132959 (98%)
c [score-dist-5] max exp 517, different 14 (3%)
c [score-dist-5] median active exp 516, avg 515.9
c [simplification-5] removed 1126 variables 0.8% (135982 remain 82%)
c [simplification-5] removed 12118 irredundant clauses 0.2% (6034195 remain 92%)
c [simplification-5] maximum reduction of 1% = max (1%, 0%)
c [simplification-5] geometric conflict interval increment 10333 = 20666 / 2
c [simplification-5] new conflict interval 30999
c [simplification-5] penalized conflict interval 30999 = 1 * 30999
c [simplification-5] hard conflict limit 83833 (soft 68334 + delta 15499)
c [simplification-5] new conflict limit 68334 (hard 83833)
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 -  114.7  135982  6034195     58262   19794   8085 31057   12    22  391  57%    596    9   12    7  177%
c 
c [simplification-6] limit 68334 conflicts (hard 83833) hit after 68334 conflicts
c [quatres-2] found 146360 quaternary clauses 30% in total
c [quatres-2-2] added 9 single-self-subsuming ternary resolvents
c [quatres-2-2] added 53 quaternary resolvents
c [ternres-2] limit 24136712 based on 6034178 irredundant clauses
c [ternres-2] 132489 schedulable variables 97%
c [ternres-2] 7 ternary resolvents (0 bin, 7 trn)
c [ternres-2] 128997 variables remain 95% (6985 retained 5%)
c [card-3] limit 1508544 based on 6034178 irredundant clauses
c [card-3] found 660 at-most-one constraints of average size 3.5
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 1508544 for elimination
c [card-3] 660 out of 660 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [decomp-12] removed 6 variables
c [treelook-3] limit 1508543 based on 6034175 irredundant clauses
c [treelook-3] scheduled 29549 literals 11%
c [treelook-3] scheduling used 1520881 steps
c [treelook-3] not fully scheduled
c [treelook-3] limit 1508543 based on 6034175 irredundant clauses
c [treelook-3] used 1620003 steps
c [treelook-3] 29519 literals remain 11%
c [treelook-3] 4654 variables remain to probed next time 3%
c [decomp-13] removed 2 variables
c [treelook-3] removed 11 variables, found 253 hbrs
c [unhide-5] limit 377131 based on 6034103 irredundant clauses
c [unhide-5-5] 0 units, 0 failed, 3725 tauts, 0 hbrs, 13940 literals
c [transred-2] limit 6031169 based on 6031169 irredundant clauses
c [transred-2] removed 1290 transitive binary clauses
c [bca-2] limit of 10000000 steps and 12066082 added (scaled 2)
c [bca-2] 268783 out of 271932 literals actually usable 99%
c [bca-2] added 52 blocked clauses in 719912 steps
c [sweep-2] limit 12061190 based on 6030595 irredundant clauses
c [sweep-2-1] 31462 pos 23.3% + 103678 neg 76.7% = 135140 sched 99.4% ret 825
c [sweep-2-1] 12090819 steps 137 queries 23821.76 avg class size
c [sweep-2-1] 4697 decisions 118 SAT calls 211.96 avg env size
c [sweep-2-1] 134155 variables remain 99% (1810 retained 1%)
c [decomp-14] removed 56 variables
c [sweep-2-1] removed 56 vars (0 failed, 20 eqs, 18 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 56 vars in TOTAL (1 rounds, 136 queries)
c [phase-count-6] 4980532 negative 82.6% of 6030548 except 1050016 17.4%
c [phase-count-6] 5129754 positive 85.1% of 6030548 except 900794 14.9%
c [phase-6] phase bias: 388 positive 53%, 348 negative 47%
c [sort-queue-6] sorted 132362 enqueued variables after 68334 conflicts
c [score-dist-6] active 3547 (3%), one 0 (0%), zero 132362 (97%)
c [score-dist-6] max exp 518, different 15 (3%)
c [score-dist-6] median active exp 517, avg 516.8
c [simplification-6] removed 73 variables 0.1% (135909 remain 82%)
c [simplification-6] removed 3647 irredundant clauses 0.1% (6030548 remain 92%)
c [simplification-6] maximum reduction of 0% = max (0%, 0%)
c [simplification-6] full geometric conflict interval increment 30999
c [simplification-6] new conflict interval 61998
c [simplification-6] penalized conflict interval 61998 = 1 * 61998
c [simplification-6] hard conflict limit 161331 (soft 130332 + delta 30999)
c [simplification-6] new conflict limit 130332 (hard 161331)
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 -  160.2  135909  6030548    100190   26321   8181 32790   13    22  390  60%    798    5   15   10  155%
c 
c [simplification-7] limit 130332 conflicts (hard 161331) hit after 130333 conflicts
c [quatres-3] found 146726 quaternary clauses 30% in total
c [quatres-3-1] removed 1 duplicate quaternary clauses
c [quatres-3-2] added 1 single-self-subsuming ternary resolvents
c [quatres-3-2] added 16 quaternary resolvents
c [ternres-3] limit 24122188 based on 6030547 irredundant clauses
c [ternres-3] 128928 schedulable variables 95%
c [ternres-3] 12 ternary resolvents (0 bin, 12 trn)
c [ternres-3] 125436 variables remain 92% (10473 retained 8%)
c [gauss-2] limit 3015273 based on 6030547 irredundant clauses
c [gauss-2] extracted 24 xors of average arity 3.0
c [gauss-2] connected 72 occurrences of 70 variables (average 1.0)
c [gauss-2] limit 3015273 based on 6030547 irredundant clauses
c [gauss-2] fully completed
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-15] removed 2 variables
c [basicprobe-3] limit 48244360 based on 6030545 irredundant clauses
c [basicprobe-3-0] 2416 sched 2%, 4 failed, 0 lifted, 24466 hbrs
c [decomp-16] removed 359 variables
c [basicprobe-3-1] 8415 probes remain 6% after last round
c [basicprobe-3-1] 4 units = 4 failed (100%) + 0 lifted (0%)
c [basicprobe-3-1] removed 359 variables, found 27435 hbrs
c [bate-1] eliminated 835 asymmetric tautologies during probing
c [transred-3] limit 6029271 based on 6029271 irredundant clauses
c [transred-3] removed 5051 transitive binary clauses
c [block-2] scheduling all variables this time
c [block-2] scheduled 135548 variables 100%
c [block-2] limit of 47170863 steps penalty 4 = 1 + 3
c [block-2] incomplete 8564 not tried 6%
c [block-2] transition to [ all 1 rem 1 ] state
c [block-2] eliminated 62 blocked clauses
c [block-2] 62 < 1/100 * 6028678 = 60286 considered unsuccessful
c [cce-2] limit of 23585431 steps penalty 4 = 1 + 3
c [cce-2-1] eliminated 1 clauses out of 1 (100%) of length 27
c [cce-2-1] eliminated 2 clauses out of 8 (25%) of length 26
c [cce-2-1] eliminated 3 clauses out of 191 (2%) of length 25
c [cce-2-1] eliminated 1 clauses out of 753 (0%) of length 24
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] eliminated 7 large clauses in 23585437 steps
c [cce-2-1] allowing another 11792718 steps for small clauses
c [cce-2-1] scheduling 5506567 clauses = 320804 binary + 5185763 ternary
c [cce-2-1] tried to eliminate 179 small clauses 0%
c [cce-2-1] eliminated 3 binary clauses 0%
c [cce-2-1] eliminated 2 ternary clauses 0%
c [cce-2-1] eliminated 5 small clauses 0%
c [cce-2-1] eliminated 5 small clauses in 23585439 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 12 covered clauses in round 1
c [cce-2] eliminated 12 covered clauses in TOTAL during 1 rounds
c [cce-2] 12 < 1/100 * 6028616 = 60286 considered unsuccessful
c [elim-6] 66924 variables 49% will be scheduled this time
c [elim-6] scheduled 66924 variables 49%
c [elim-6] limit of 50000000 steps penalty 4 = 1 + 3
c [elim-6] rescheduling of touched variables disabled
c [elim-6] incomplete 63538 not tried 47% in round 1
c [elim-6] transition to [ all 0 rem 1 ] state
c [elim-6] eliminated 0 = 0% variables out of 66924 scheduled
c [bca-3] limit of 10000000 steps and 12062126 added (scaled 2)
c [bca-3] 267515 out of 271098 literals actually usable 99%
c [bca-3] added 34 blocked clauses in 742780 steps
c [sweep-3] limit 12057208 based on 6028604 irredundant clauses
c [sweep-3-1] 35116 pos 26.3% + 98656 neg 73.7% = 133772 sched 98.7% ret 1776
c [sweep-3-1] 12618109 steps 51 queries 30218.59 avg class size
c [sweep-3-1] 2256 decisions 48 SAT calls 172.50 avg env size
c [sweep-3-1] 133356 variables remain 98% (2192 retained 2%)
c [decomp-17] removed 14 variables
c [sweep-3-1] removed 14 vars (0 failed, 2 eqs, 4 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 14 vars in TOTAL (1 rounds, 50 queries)
c [phase-count-7] 4978772 negative 82.6% of 6028593 except 1049821 17.4%
c [phase-count-7] 5127560 positive 85.1% of 6028593 except 901033 14.9%
c [phase-7] phase bias: 1795 positive 73%, 658 negative 27%
c [sort-queue-7] sorted 131489 enqueued variables after 130333 conflicts
c [score-dist-7] active 4045 (3%), one 0 (0%), zero 131489 (97%)
c [score-dist-7] max exp 518, different 15 (3%)
c [score-dist-7] median active exp 518, avg 517.3
c [simplification-7] removed 375 variables 0.3% (135534 remain 82%)
c [simplification-7] removed 1955 irredundant clauses 0.0% (6028593 remain 92%)
c [simplification-7] maximum reduction of 0% = max (0%, 0%)
c [simplification-7] full geometric conflict interval increment 61998
c [simplification-7] new conflict interval 123996
c [simplification-7] penalized conflict interval 123996 = 1 * 123996
c [simplification-7] hard conflict limit 316327 (soft 254329 + delta 61998)
c [simplification-7] new conflict limit 254329 (hard 316327)
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 -  205.0  135534  6028593    139981   33178   8467 55972   11    17  391  63%    901   -1   10   10  100%
c -  222.0  135534  6028593    176126   38004   8487 55974   11    20  392  56%    953    3   13   10  127%
c -  243.0  135534  6028593    210382   37964   8505 55978   13    19  392  66%    982    1   12   11  111%
c i  256.5  135533  6028593    235575   61054   8572 55987    9    12  397  75%    995   -5    6   11   53%
c -  264.0  135527  6028593    249497   43321   8576 55988   11    16  392  69%  -2023   -1   12   11  115%
c -  284.6  135527  6028593    284674   43829   8589 55989   12    17  392  68%   -757    0   13   11  117%
c 
c [simplification-8] limit 254329 conflicts (hard 316327) hit after 316327 conflicts
c [quatres-4] found 147118 quaternary clauses 29% in total
c [quatres-4-2] added 4 single-self-subsuming ternary resolvents
c [quatres-4-2] added 19 quaternary resolvents
c [ternres-4] limit 24114372 based on 6028593 irredundant clauses
c [ternres-4] 125083 schedulable variables 92%
c [ternres-4] 15 ternary resolvents (0 bin, 15 trn)
c [ternres-4] 121650 variables remain 90% (13877 retained 10%)
c [decomp-18] removed 8 variables
c [simpleprobe-4] 126618 schedulable variables 93%
c [simpleprobe-4] limit 25000000 penalty 3 = 0 + 3
c [decomp-19] removed 23 variables
c [simpleprobe-4] 127139 variables remain 94% (8364 retained 6%)
c [simpleprobe-4] removed 23 variables, found 2407 hbrs, 0 units
c [transred-4] limit 6028189 based on 6028189 irredundant clauses
c [transred-4] removed 4388 transitive binary clauses
c [bca-4] limit of 10000000 steps and 12060301 added (scaled 2)
c [bca-4] 267190 out of 271008 literals actually usable 99%
c [bca-4] added 28 blocked clauses in 758892 steps
c [sweep-4] limit 12055366 based on 6027683 irredundant clauses
c [sweep-4-1] 37730 pos 28.3% + 95583 neg 71.7% = 133313 sched 98.4% ret 2190
c [sweep-4-1] 12074981 steps 112 queries 29365.75 avg class size
c [sweep-4-1] 4118 decisions 105 SAT calls 228.46 avg env size
c [sweep-4-1] 132225 variables remain 98% (3278 retained 2%)
c [decomp-20] removed 76 variables
c [sweep-4-1] removed 76 vars (0 failed, 6 eqs, 4 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 76 vars in TOTAL (1 rounds, 111 queries)
c [phase-count-8] 4978292 negative 82.6% of 6027624 except 1049332 17.4%
c [phase-count-8] 5127274 positive 85.1% of 6027624 except 900350 14.9%
c [phase-8] phase bias: 272 positive 45%, 331 negative 55%
c [sort-queue-8] sorted 130922 enqueued variables after 316327 conflicts
c [score-dist-8] active 4505 (3%), one 0 (0%), zero 130922 (97%)
c [score-dist-8] max exp 520, different 17 (3%)
c [score-dist-8] median active exp 519, avg 518.6
c [simplification-8] removed 100 variables 0.1% (135427 remain 81%)
c [simplification-8] removed 969 irredundant clauses 0.0% (6027624 remain 92%)
c [simplification-8] maximum reduction of 0% = max (0%, 0%)
c [simplification-8] full geometric conflict interval increment 123996
c [simplification-8] new conflict interval 247992
c [simplification-8] penalized conflict interval 247992 = 1 * 247992
c [simplification-8] hard conflict limit 688315 (soft 564319 + delta 123996)
c [simplification-8] new conflict limit 564319 (hard 688315)
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 -  319.2  135427  6027624    324307   47245   8608 56221   12    18  393  63%     51    1   12   11  110%
c -  336.5  135427  6027624    362162   51245   8627 56224    9    14  393  68%    478   -4    9   11   82%
c -  358.6  135427  6027624    399386   52095   8641 56226   12    17  393  69%    715   -1   10   11   90%
c -  378.6  135427  6027624    439431   56372   8663 56232   12    18  393  66%    856   -0   11   11  105%
c i  380.0  135426  6027624    442083   58624   8685 56242   10    14  396  70%    863   -3    7   11   66%
c -  401.4  135426  6027624    478907   57891   8704 56244   11    18  393  62%   -937    0   11   11  101%
c i  415.1  135425  6027624    506502   84022   8722 56251   12    18  399  65%   -263    0    6   11   56%
c -  421.4  135414  6027624    519740   62128   8728 56251   10    14  394  72%   -863   -3   10   11   90%
c -  441.6  135414  6027624    559813   64403   8756 56253   13    20  394  63%      0    4   15   11  139%
c 
c [simplification-9] limit 564319 conflicts (hard 688315) hit after 564319 conflicts
c [quatres-5] found 147794 quaternary clauses 29% in total
c [quatres-5-1] removed 1 duplicate quaternary clauses
c [quatres-5-2] added 5 single-self-subsuming ternary resolvents
c [quatres-5-2] added 26 quaternary resolvents
c [ternres-5] limit 25000000 with penalty 3 = 0 + 3
c [ternres-5] 121547 schedulable variables 90%
c [ternres-5] 11 ternary resolvents (0 bin, 11 trn)
c [ternres-5] 118031 variables remain 87% (17383 retained 13%)
c [decomp-21] removed 13 variables
c [treelook-4] limit 3434182 penalty 3 = 0 + 3 boost 1
c [treelook-4] scheduled 59409 literals 22%
c [treelook-4] scheduling used 3450753 steps
c [treelook-4] not fully scheduled
c [treelook-4] limit 3434182 penalty 3 = 0 + 3 boost 1
c [treelook-4] used 3444069 steps
c [treelook-4] 59339 literals remain 22%
c [treelook-4] 3777 variables remain to probed next time 3%
c [decomp-22] removed 11 variables
c [treelook-4] removed 11 variables, found 1047 hbrs
c [unhide-6] limit 376682 based on 6026912 irredundant clauses
c [unhide-6-6] 0 units, 3 failed, 23663 tauts, 0 hbrs, 10577 literals
c [transred-5] limit 6026464 based on 6026464 irredundant clauses
c [transred-5] removed 1429 transitive binary clauses
c [bca-5] limit of 10000000 steps and 12057091 added (scaled 2)
c [bca-5] 267038 out of 270804 literals actually usable 99%
c [bca-5] added 66 blocked clauses in 751793 steps
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 103025477 penalty 3 = 0 + 3
c [sweep-5-1] 41332 pos 31.3% + 90798 neg 68.7% = 132130 sched 97.6% ret 3271
c [sweep-5-1] 103066387 steps 987 queries 5333.76 avg class size
c [sweep-5-1] 31744 decisions 857 SAT calls 187.14 avg env size
c [sweep-5-1] 121158 variables remain 89% (14243 retained 11%)
c [decomp-23] removed 345 variables
c [sweep-5-1] removed 345 vars (0 failed, 140 eqs, 124 impls)
c [sweep-5] considered successful since not run to completion yet
c [sweep-5] removed 345 vars in TOTAL (1 rounds, 986 queries)
c [phase-count-9] 4977167 negative 82.6% of 6025845 except 1048678 17.4%
c [phase-count-9] 5126436 positive 85.1% of 6025845 except 899409 14.9%
c [phase-9] phase bias: 434 positive 35%, 799 negative 65%
c [sort-queue-9] sorted 127774 enqueued variables after 564319 conflicts
c [score-dist-9] active 7282 (5%), one 0 (0%), zero 127774 (95%)
c [score-dist-9] max exp 521, different 18 (3%)
c [score-dist-9] median active exp 520, avg 519.6
c [simplification-9] removed 358 variables 0.3% (135056 remain 81%)
c [simplification-9] removed 1779 irredundant clauses 0.0% (6025845 remain 92%)
c [simplification-9] maximum reduction of 0% = max (0%, 0%)
c [simplification-9] full geometric conflict interval increment 247992
c [simplification-9] new conflict interval 495984
c [simplification-9] penalized conflict interval 495984 = 1 * 495984
c [simplification-9] hard conflict limit 1308295 (soft 1060303 + delta 247992)
c [simplification-9] new conflict limit 1060303 (hard 1308295)
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 -  483.2  135056  6025845    601037   64972   8777 46619   13    20  393  64%    478    2   15   11  130%
c -  506.9  135056  6025845    643486   68094   8790 46624   11    16  394  70%    738   -2   11   11   97%
c i  520.8  135055  6025845    670508   93125   8812 46631   11    15  400  72%    835   -2    7   11   63%
c -  528.1  135055  6025845    686070   71454   8817 46632   10    15  394  68%  -1178   -2   11   11  102%
c -  546.1  135055  6025845    727323   73845   8831 46632   13    22  394  60%   -149    4   13   11  122%
c -  566.8  135055  6025845    770752   77188   8848 46633   11    16  394  65%    419   -1   10   11   91%
c -  587.3  135055  6025845    813855   79612   8858 46633   11    17  394  66%    711   -0   14   11  132%
c -  610.2  135055  6025845    857328   81442   8870 46634   12    18  394  65%    863    1    8   11   73%
c -  633.7  135055  6025845    903437   84625   8886 46639   11    17  394  61%    944    1   10   11   97%
c -  655.9  135055  6025845    948438   86360   8894 46639   11    17  394  62%    984   -0   10   11   87%
c -  679.6  135055  6025845    994412   88996   8909 46641   11    15  395  72%   1004   -3    9   11   80%
c i  680.7  135054  6025845    996442   90691   8920 46644   10    14  399  73%   1005   -4    7   11   59%
c i  692.9  135050  6025845   1019663  111864   8963 46655    9    13  402  72%  -2620   -4    7   11   65%
c -  704.5  135050  6025845   1042587   92368   8967 46655   12    18  395  66%  -1804    1    9   11   86%
c -  727.5  135050  6025845   1089335   94696   8980 46656   12    18  395  64%   -362    2   11   11   99%
c 
c [simplification-10] limit 1060303 conflicts (hard 1308295) hit after 1116711 conflicts
c [quatres-6] found 148932 quaternary clauses 28% in total
c [quatres-6-1] removed 4 duplicate quaternary clauses
c [quatres-6-2] added 15 single-self-subsuming ternary resolvents
c [quatres-6-2] added 36 quaternary resolvents
c [ternres-6] limit 25000000 with penalty 3 = 0 + 3
c [ternres-6] 117715 schedulable variables 87%
c [ternres-6] 26 ternary resolvents (0 bin, 26 trn)
c [ternres-6] 114312 variables remain 85% (20738 retained 15%)
c [card-4] limit 3966446 penalty 6 = 3 + 3
c [card-4] found 1329 at-most-one constraints of average size 3.3
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 3966446 for elimination
c [card-4] 1329 out of 1329 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [gauss-3] limit 3012863 based on 6025726 irredundant clauses
c [gauss-3] extracted 17 xors of average arity 3.0
c [gauss-3] connected 51 occurrences of 51 variables (average 1.0)
c [gauss-3] limit 3012443 based on 6024887 irredundant clauses
c [gauss-3] fully completed
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-24] removed 2 variables
c [basicprobe-4] limit 50000000 penalty 3 = 0 + 3
c [basicprobe-4-0] 3630 probes remain 3% after last round
c [basicprobe-4-0] 6 units = 6 failed (100%) + 0 lifted (0%)
c [basicprobe-4-0] removed 12 variables, found 16569 hbrs
c [bate-2] eliminated 2350 asymmetric tautologies during probing
c [transred-6] limit 6022535 based on 6022535 irredundant clauses
c [transred-6] removed 3264 transitive binary clauses
c [transred-6] found 1 units
c [block-3] 8547 variables 6% will be scheduled this time
c [block-3] scheduled 8547 variables 6%
c [block-3] limit of 25000000 steps penalty 5 = 2 + 3
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 9 blocked clauses
c [block-3] 9 < 1/100 * 6022089 = 60220 considered unsuccessful
c [cce-3] limit of 67108863 steps penalty 5 = 2 + 3
c [cce-3-1] eliminated 27 clauses out of 2721 (1%) of length 23
c [cce-3-1] eliminated 7 clauses out of 6958 (0%) of length 22
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 34 large clauses in 67109172 steps
c [cce-3-1] allowing another 33554586 steps for small clauses
c [cce-3-1] scheduling 5501082 clauses = 319695 binary + 5181387 ternary
c [cce-3-1] tried to eliminate 1142 small clauses 0%
c [cce-3-1] eliminated 48 binary clauses 0%
c [cce-3-1] eliminated 494 ternary clauses 0%
c [cce-3-1] eliminated 542 small clauses 0%
c [cce-3-1] eliminated 542 small clauses in 67108887 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 576 covered clauses in round 1
c [cce-3] eliminated 576 covered clauses in TOTAL during 1 rounds
c [cce-3] 576 < 1/100 * 6019383 = 60193 considered unsuccessful
c [elim-7] scheduling all variables this time
c [elim-7] scheduled 135014 variables 100%
c [elim-7] limit of 25000000 steps penalty 5 = 2 + 3
c [elim-7] rescheduling of touched variables disabled
c [elim-7] incomplete 111487 not tried 83% in round 1
c [elim-7] transition to [ all 1 rem 1 ] state
c [elim-7] eliminated 206 = 0% variables out of 135014 scheduled
c [elim-7] 206 < 1/100 * 135014 = 1350 considered unsuccessful
c [bca-6] limit of 10000000 steps and 12035734 added (scaled 2)
c [bca-6] 265006 out of 269618 literals actually usable 98%
c [bca-6] added 342 blocked clauses in 814594 steps
c [sweep-6] limit 19038943 penalty 3 = 0 + 3
c [sweep-6-1] 54994 pos 45.5% + 65843 neg 54.5% = 120837 sched 89.6% ret 13971
c [sweep-6-1] 19236709 steps 143 queries 24250.45 avg class size
c [sweep-6-1] 5895 decisions 129 SAT calls 240.25 avg env size
c [sweep-6-1] 120208 variables remain 89% (14600 retained 11%)
c [decomp-25] removed 45 variables
c [sweep-6-1] removed 45 vars (0 failed, 19 eqs, 18 impls)
c [sweep-6] considered successful since not run to completion yet
c [sweep-6] removed 45 vars in TOTAL (1 rounds, 142 queries)
c [phase-count-10] 4969889 negative 82.6% of 6015347 except 1045458 17.4%
c [phase-count-10] 5117955 positive 85.1% of 6015347 except 897392 14.9%
c [phase-10] phase bias: 170 positive 41%, 242 negative 59%
c [sort-queue-10] sorted 127043 enqueued variables after 1116711 conflicts
c [score-dist-10] active 7720 (6%), one 0 (0%), zero 127043 (94%)
c [score-dist-10] max exp 522, different 18 (3%)
c [score-dist-10] median active exp 520, avg 520.1
c [simplification-10] removed 287 variables 0.2% (134763 remain 81%)
c [simplification-10] removed 10498 irredundant clauses 0.2% (6015347 remain 92%)
c [simplification-10] maximum reduction of 0% = max (0%, 0%)
c [simplification-10] full geometric conflict interval increment 495984
c [simplification-10] new conflict interval 991968
c [simplification-10] penalized conflict interval 991968 = 1 * 991968
c [simplification-10] hard conflict limit 2604663 (soft 2108679 + delta 495984)
c [simplification-10] new conflict limit 2108679 (hard 2604663)
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 -  771.2  134763  6015347   1137275   95427   9655 61569   10    15  397  70%    357   -2   11   11  102%
c -  797.6  134763  6015347   1186928   98088   9689 61574   11    15  397  74%    711   -1   11   11  100%
c i  798.0  134762  6015347   1187727   98692   9696 61583   11    14  401  75%    715   -2    8   11   73%
c i  811.1  134674  6015347   1213768  122215   9719 61586   11    16  404  71%   -976    0    9   11   83%
c i  812.8  134579  6015347   1217879  125829   9744 61599   10    13  405  73%  -1236   -3    7   11   62%
c i  817.0  134560  6015347   1227508  134658   9759 61606    9    12  408  74%   -990   -3    7   11   68%
c i  817.2  134541  6015347   1227954  135074   9760 61606    9    13  408  71%  -1029   -2    9   11   88%
c i  817.6  134493  6015347   1228831  135831   9770 61609    9    13  408  72%  -1061   -2    8   11   73%
c i  817.8  134475  6015347   1229060  136018   9777 61613    9    13  408  72%  -1065   -3    6   11   61%
c i  818.5  134454  6015347   1230497  137272   9786 61618    9    12  408  73%  -1057   -3    8   10   80%
c 0  818.5  134431  6015347   1230497  137272   9786 61618    9    12  408  73%  -1057   -3    8   10   80%
c 
s UNSATISFIABLE
c
c bate: 3185 basic ate = 562 trn 18% + 2623 lrg 82% in 2 updates
c bcas: 6 count, 9306 added (23339 skipped), 4516707 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, 9034 removed, 50278777 resolutions, 131220895 steps
c blkd: 2336 blocking literals 1%, 0 pure
c bump: 1230448 bumped seen, 79789962 lits 64.8 on average
c card: 4 count, 0 units, 0 am1, 19138359 steps
c card: 0 rescheduled, 0 eliminated, 0 resolved, 10305 subsumed
c card: 4812 at-most-one constraints found, average size 3.15
c card: 4812 at-most-one constraints used 100%, average size 3.15
c card: 0 at-most-two constraints found, average size 0.00
c card: 0 at-most-two constraints used 0%, average size 0.00
c cces: 3 cces, 620 eliminated, 134 ate 22%, 486 abce 78%
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: 27755083 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 51 gcs, 0 rescored clauses, 0 rescored vars
c dcps: 25 decompositions, 7782 equivalent 5%
c deco: 0 decision-only clauses 0%, 0% reduction
c decs: 2001048 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 7 elims, 21768 eliminated 13%, 7123 pure 33%
c elms: 7 rounds, 1.0 rounds/bve
c elms: 11741 small 54%, 2904 large 13%
c elms: 12610 tried small, 11741 succeeded 93%, 869 failed 7%
c elms: 7979 subsumed, 6081 strengthened, 0 blocked
c elms: 8275800 copies, 8341281 resolutions, 150507 ipos
c elms: 27435997 subchks, 2413441 strchks
c gaus: 3 extractions, 95 extracted, 2.8 size, 3 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 18110176 steps, 9055088 extr 50%, 371 elim 0%
c glue: 11.0 orig avg, 11.0 real avg, 2.8 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 137669 = 5634 simple 4% + 131595 trn 96% + 440 lrg 0%, 1873 sub 1%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 1230448 clauses, 26.5 length
c lrnd: 32582822 lits = 50099464 orig - 17516642 removed 35%
c lrnd: 388667 uips 32%, 777453 flips 63%
c mins: 1222088 mins 99%, 176 bin 0%, 8184 size 1%
c mins: 45437901 poisoned searches, 6234663 hits, 14% hit rate
c mins: 88029699 used twice searches, 5650862 hits, 6% hit rate
c move: moved 14856, 406 bin 3%, 14450 trn 97%
c otfs: 1476 driving 31%, 3344 restarting 69%
c otfs: str 4820, 4750 red 99%, 70 irr 1%
c otfs: str 4820, 0 bin 0%, 16 trn 0%, 4804 lrg 100%
c otfs: sub 7, 7 red 100%, 0 irr 0%
c otfs: sub 7, 0 bin 0%, 0 trn 0%, 7 lrg 100%
c phas: 10 computed, 176441 set, 81399 pos (46%), 95042 neg (54%)
c prbs: 4 basic, 35630 probed, 114 failed, 0 lifted
c prbs: 4 simple, 232530 probed, 0 failed, 195 eqs
c prbs: 4 treelook, 167 probed, 1 failed, 0 lifted
c prom: 323622 locked 19% out of 1701239 tried
c prps: 778567769 props, 386 props/dec
c prps: 99% srch, 1% simp, 0% lkhd
c quat: 6 count, 448 quat, 164 self1, 0 self2, 148 dup
c queu: 10 sorted, 2001048 next (517 steps 0.00)
c queu: 81322325 enq (554310321 steps 6.82), 79789962 deq 98%
c redc: 15403 clauses 7%, 234895 tried 19%, 3 sat 0%
c redc: 17965 lits 1%, 2873438 tried 6%, 3 sat 0%
c redc: 414 times jump level reduced, 1.8 levels on average
c reds: 28 count, 43946.3 conflicts per reduce
c reds: 0 memlim 0%, 28 arith 100%
c reds: 889070 collected 88%, 126694 retired 12%
c rmbd: 4684 removed, 2571 red 55%
c rsts: 23929 restarts 100%, 0 skipped 0%
c rsts: 0 saturating 0%, 0 reuse 0%
c rsts: 0 kept 0.0% average 0.0%
c scnc: 0 count, 1.000 min (0/1000), 1.000 max (0/1000)
c simp: 10 count, 10 confs 100%, 0 vars 0%
c simp: 0 its 0%, 0 bin 0%, 0 trns 0%
c subl: 1230448 count (525984 tried 0.4), 69738 sub out of 1228865 (5.7%)
c swps: 6 count, 6 rounds, 1523 queries (253.8/round)
c swps: 1349 sat calls, 54 unsat (1.1% success rate)
c swps: 52514 decisions 38.9, 1427 conflicts 1.1
c swps; 12854.0 avg class size, 199.0 avg environment size
c swps: 0 failed, 174 impls, 195 equivs
c swp0: 505 type 0 queries, 82 unsat (16.2%), 496 sat (98.2%)
c swp1: 1018 type 1 queries, 653 unsat (64.1%), 832 sat (81.7%)
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: 6463203 calls to obtain time
c tops: 3094 fixed 2%, 14 its, 87892.64 confs/it
c trds: 6 transitive reductions, 17380 removed, 1 failed
c trds: 352216 nodes, 454115 edges, 36184143 steps
c trim: 435144 words, 1.7 MB
c trnr: 6 count, 0 bin, 85 trn, 146558524 steps
c unhd: 6 count, 6 rounds, 56459507 steps
c unhd: 4046 non-trivial sccs of average size 2.6
c unhd: 3 units, 3 bin, 0 trn, 0 lrg
c unhd: 128 failed, 108 stamp, 0 lits, 0 bin, 0 trn, 0 lrg
c unhd: 159077 tauts, 1844 bin 1%, 10635 trn 7%, 2541 lrg 2%
c unhd: 159077 tauts, 144057 stamp 91%, 57027 red 36%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 39316 str, 3 bin 0%, 620 trn 2%, 38693 lrg 98%, 37864 red 96%
c vars: 134431 remaining 80% and 32644 removed 20% out of 167075
c vars: 3094 fixed 2%, 21768 eliminated 13%, 7782 equivalent 5%
c vsts: 55964387827 visits, 99% srch, 1% simp, 0% lkhd
c vsts: 72.0 search visits per propagation, 45213.8 per conflict
c wchs: 4481904349 pushed, 59221288 enlarged, 86 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all        1229313        889070        126694      28913969       9480852        462284
c 
c  0 0         82837   7     12418   1         0   0  16762330  58   5168974  55    213377  46     2.7
c  1 5         78278   6     43115   5     18696  15   4295611  15<  1332222  14<    68930  15<    0.7
c  2 6        302935  25    225316  25     35625  28   5623482  19   1810371  19    106346  23     1.9
c  3 9        431516  35<   344548  39<    34122  27<  1684998   6    792451   8     47896  10     2.5
c  4 14       258097  21    206194  23     25649  20    440443   2    299842   3     19554   4     1.7
c  5 21        69025   6     52568   6     11253   9     97986   0     70713   1      5639   1     0.8
c  6 30         6559   1      4863   1      1334   1      9030   0      6217   0       534   0     0.1
c  7 41           66   0        48   0        15   0        89   0        62   0         8   0     0.0
c 
c avg                  2.8           3.0           2.8           0.8           0.9           1.2
c std                  1.2           1.0           1.2           1.1           1.2           1.3
c 
c   30.630   4% probe
c   20.378   2% elim
c   18.503   2% sweep
c   12.146   1% unhide
c   10.058   1% transred
c    8.808   1% block
c    7.670   1% bca
c    6.825   1% bump
c    5.937   1% cce
c 
c   10.236 < 1% rest (below)
c 
c    4.237   1% gauss
c    3.108   0% quatres
c    1.417   0% ternres
c    1.163   0% decide
c    0.311   0% card
c    0.000   0% locs
c    0.000   0% queuesort
c    0.000   0% rescore
c ==================================
c   12.421   2% preprocessing     8%
c  149.113  18% inprocessing     92%
c ==================================
c  161.534  20% simplifying
c  656.925  80% search
c ==================================
c  818.463 100% all
c 
c       1230497 conflicts,        1503.4 confs/sec
c          1009 ternaries,        1219.5 confs/ternary
c           249 binaries,         4941.8 confs/binary
c            14 iterations,      87892.6 confs/iteration
c 
c            28 reductions,          0.0 redus/sec,  43946.3 confs/reduction
c         23929 restarts,           29.2 rests/sec,     51.4 confs/restart
c       2001048 decisions,        2444.9 decis/sec,      1.6 decis/conflict
c     778567769 propagations,   951256.3 props/sec,    389.1 props/decision
c 
c 818.5 seconds, 623.5 MB
c launch: done
