c launch: /data/cnf/sc2014/app/9dlx_vliw_at_b_iq7.cnf.bz2
c host: atom04
c Lingeling SAT Solver
c 
c Version b7ztzu 7b29300825af9bcc1c8b2c5ebcf65fa1cb101cad
c 
c Copyright (C) 2010-2014 Armin Biere JKU Linz Austria.
c All rights reserved.
c 
c released Sun Apr 26 19:26:13 CEST 2015
c compiled Sun Apr 26 19:26:13 CEST 2015
c 
c gcc (Ubuntu 4.8.2-19ubuntu1) 4.8.2
c -Wall -O3 -I../yalsat -I../druplig -DNLGLOG -DNDEBUG -DNCHKSOL
c Linux cluster2 3.13.0-45-generic x86_64
c 
c piping '/data/cnf/sc2014/app/9dlx_vliw_at_b_iq7.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/9dlx_vliw_at_b_iq7.cnf.bz2
c no embedded options
c found 'p cnf 306095 6069108' header
c read 306095 variables, 6069108 clauses, 17675754 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 306094 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  306094  6069107         0       0      0     0    0     0  183   0%      0    0    0    0    0%
c 
c [simplification-1] limit 0 conflicts (hard 0) hit after 0 conflicts
c [card-1] limit 1517276 based on 6069107 irredundant clauses
c [card-1] found 5 at-most-one constraints of average size 3.0
c [card-1] no at-most-two constraint found
c [card-1] using previous limit 1517276 for elimination
c [card-1] 5 out of 5 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 10 variables
c [simpleprobe-1] all 306085 free variables schedulable
c [simpleprobe-1] boosting simple probing limit by 10
c [simpleprobe-1] limit 12138134 based on 6069067 irredundant clauses
c [simpleprobe-1] 289785 variables remain 95% (16300 retained 5%)
c [simpleprobe-1] removed 0 variables, found 11628 hbrs, 0 units
c [unhide-1] limit 379316 based on 6069067 irredundant clauses
c [unhide-1-1] 1374 units, 1 failed, 19070 tauts, 0 hbrs, 158589 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 304710 variables 100%
c [elim-1] limit of 6028263 steps based on 6028263 irredundant clauses
c [elim-1] rescheduling of touched variables disabled
c [elim-1] incomplete 304049 not tried 100% in round 1
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 661 = 0% variables out of 304710 scheduled
c [elim-1] considered successful since not run to completion yet
c [phase-count-1] 6026332 negative 100.0% of 6026941 except 609 0.0%
c [phase-count-1] 1545779 positive 25.6% of 6026941 except 4481162 74.4%
c [phase-count-1] less non-negative clauses 609 than limit 602600 (10.0%)
c [phase-count-1] non-pos/non-neg = 4481162/609 = 7358.23 >= 2.00 = 200/100
c [lucky-phase-1] forcing lucky phase -1
c [phase-1] phase bias: 0 positive 0%, 304049 negative 100%
c [sort-queue-1] sorted 304049 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 304049 (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 2036 variables 0.7% (304049 remain 99%)
c [simplification-1] removed 42166 irredundant clauses 0.7% (6026941 remain 99%)
c [simplification-1] maximum reduction of 1% = max (1%, 1%)
c [simplification-1] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-1] new conflict interval 10000
c [simplification-1] penalized conflict interval 10000 = 1 * 10000
c [simplification-1] hard conflict limit 20000 (soft 10000 + delta 10000)
c [simplification-1] new conflict limit 10000 (hard 20000)
c 
c [simplification-2] limit of 100 binary hit after 100 binaries
c [decomp-3] removed 3 variables
c [treelook-1] limit 1506733 based on 6026935 irredundant clauses
c [treelook-1] scheduled 248777 literals 41%
c [treelook-1] scheduling used 1506738 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 1506733 based on 6026935 irredundant clauses
c [treelook-1] used 9300527 steps
c [treelook-1] 248774 literals remain 41%
c [treelook-1] 239056 variables remain to probed next time 79%
c [treelook-1] removed 0 variables, found 866 hbrs
c [basicprobe-1] limit 48215480 based on 6026935 irredundant clauses
c [basicprobe-1-0] 297511 probes remain 99% after last round
c [basicprobe-1-0] 96 units = 96 failed (100%) + 0 lifted (0%)
c [basicprobe-1-0] removed 3914 variables, found 9812 hbrs
c [unhide-2] limit 376683 based on 6026935 irredundant clauses
c [unhide-2-2] 27282 units, 6 failed, 203 tauts, 0 hbrs, 179736 literals
c [elim-2] 272848 variables 100% will be scheduled this time
c [elim-2] scheduled 272848 variables 100%
c [elim-2] limit of 12098149 steps penalty 3 = 0 + 3
c [elim-2] rescheduling of touched variables disabled
c [elim-2] incomplete 272711 not tried 100% in round 1
c [elim-2] transition to [ all 0 rem 1 ] state
c [elim-2] eliminated 137 = 0% variables out of 272848 scheduled
c [elim-2] considered successful since not run to completion yet
c [sort-queue-2] sorted 231279 enqueued variables after 4398 conflicts
c [score-dist-2] active 41432 (15%), one 0 (0%), zero 231279 (85%)
c [score-dist-2] max exp 514, different 13 (3%)
c [score-dist-2] median active exp 512, avg 512.1
c [simplification-2] removed 31338 variables 10.3% (272711 remain 89%)
c [simplification-2] removed 613547 irredundant clauses 10.2% (5413394 remain 89%)
c [simplification-2] maximum reduction of 10% = max (10%, 10%)
c [simplification-2] forced so keeping old conflict interval 10000
c [simplification-2] conflict limit remains at 10000 (hard 20000)
c [simplification-2] new binary interval 1000
c 
c [simplification-3] limit 10000 conflicts (hard 20000) hit after 10010 conflicts
c [card-2] limit 1353348 based on 5413394 irredundant clauses
c [card-2] found 10 at-most-one constraints of average size 3.1
c [card-2] no at-most-two constraint found
c [card-2] using previous limit 1353348 for elimination
c [card-2] 10 out of 10 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [decomp-5] removed 155 variables
c [simpleprobe-2] 258025 schedulable variables 95%
c [simpleprobe-2] limit 10826200 based on 5413100 irredundant clauses
c [decomp-6] removed 2022 variables
c [simpleprobe-2] 236044 variables remain 87% (34490 retained 13%)
c [simpleprobe-2] removed 2022 variables, found 536 hbrs, 1988 units
c [unhide-3] limit 335357 based on 5365714 irredundant clauses
c [unhide-3-3] 494 units, 2 failed, 4681 tauts, 0 hbrs, 25036 literals
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 270038 variables 100%
c [elim-3] limit of 24595434 steps penalty 3 = 0 + 3
c [elim-3] rescheduling of touched variables disabled
c [elim-3] incomplete 268183 not tried 99% in round 1
c [elim-3] transition to [ all 1 rem 1 ] state
c [elim-3] eliminated 1855 = 1% variables out of 270038 scheduled
c [elim-3] considered successful since not run to completion yet
c [sort-queue-3] sorted 211011 enqueued variables after 10010 conflicts
c [score-dist-3] active 57172 (21%), one 0 (0%), zero 211011 (79%)
c [score-dist-3] max exp 515, different 14 (3%)
c [score-dist-3] median active exp 514, avg 513.2
c [simplification-3] removed 4528 variables 1.7% (268183 remain 88%)
c [simplification-3] removed 65319 irredundant clauses 1.2% (5348075 remain 88%)
c [simplification-3] maximum reduction of 2% = max (2%, 1%)
c [simplification-3] geometric conflict interval increment 6666 = 20000 / 3
c [simplification-3] new conflict interval 16666
c [simplification-3] penalized conflict interval 16666 = 1 * 16666
c [simplification-3] hard conflict limit 36676 (soft 26676 + delta 10000)
c [simplification-3] new conflict limit 26676 (hard 36676)
c 
c [simplification-4] limit 26676 conflicts (hard 36676) hit after 26679 conflicts
c [decomp-7] removed 10 variables
c [unhide-4] limit 334253 based on 5348059 irredundant clauses
c [unhide-4-4] 7601 units, 18 failed, 228 tauts, 0 hbrs, 105728 literals
c [elim-4] 256653 variables 100% will be scheduled this time
c [elim-4] scheduled 256653 variables 100%
c [elim-4] boosting limit by 20
c [elim-4] limit of 1096610925 steps penalty 3 = 0 + 3
c [elim-4] rescheduling of touched variables disabled
c [elim-4] incomplete 10426 not tried 4% in round 1
c [elim-4] transition to [ all 0 rem 1 ] state
c [elim-4] eliminated 45661 = 18% variables out of 256653 scheduled
c [elim-4] considered successful since not run to completion yet
c [sort-queue-4] sorted 145697 enqueued variables after 26679 conflicts
c [score-dist-4] active 65295 (31%), one 0 (0%), zero 145697 (69%)
c [score-dist-4] max exp 516, different 15 (3%)
c [score-dist-4] median active exp 516, avg 514.8
c [simplification-4] removed 57191 variables 21.3% (210992 remain 69%)
c [simplification-4] removed 450817 irredundant clauses 8.4% (4897258 remain 81%)
c [simplification-4] maximum reduction of 21% = max (21%, 8%)
c [simplification-4] large reduction 21% >= 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 38679 (soft 28679 + delta 10000)
c [simplification-4] new conflict limit 28679 (hard 38679)
c 
c [simplification-5] limit 28679 conflicts (hard 38679) hit after 28679 conflicts
c [quatres-1] found 27844 quaternary clauses 8% in total
c [quatres-1-1] removed 3 duplicate quaternary clauses
c [quatres-1-2] added 6 single-self-subsuming ternary resolvents
c [quatres-1-2] added 1936 quaternary resolvents
c [ternres-1] boosting ternary resolution limit by 5
c [ternres-1] limit 29118435 with penalty 2 = 0 + 2
c [ternres-1] all 210992 free variables schedulable
c [ternres-1] 37564 ternary resolvents (4 bin, 37560 trn)
c [ternres-1] 26792 variables remain 13% (184200 retained 87%)
c [gauss-1] limit 2448627 based on 4897255 irredundant clauses
c [gauss-1] extracted 12 xors of average arity 2.0
c [gauss-1] connected 24 occurrences of 22 variables (average 1.1)
c [gauss-1] limit 2448627 based on 4897255 irredundant clauses
c [gauss-1] fully completed
c [gauss-1] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-8] removed 171 variables
c [treelook-2] limit 1224228 based on 4896913 irredundant clauses
c [treelook-2] scheduled 171443 literals 41%
c [treelook-2] scheduling used 1224270 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 1224228 based on 4896913 irredundant clauses
c [treelook-2] used 26027506 steps
c [treelook-2] 171441 literals remain 41%
c [treelook-2] 151557 variables remain to probed next time 72%
c [treelook-2] removed 0 variables, found 7120 hbrs
c [unhide-5] limit 306057 based on 4896913 irredundant clauses
c [unhide-5-5] 234 units, 8 failed, 31655 tauts, 0 hbrs, 26164 literals
c [transred-1] limit 4865455 based on 4865455 irredundant clauses
c [transred-1] removed 0 transitive binary clauses
c [transred-1] found 9 units
c [block-1] scheduling all variables this time
c [block-1] scheduled 210526 variables 100%
c [block-1] boosting limit by 10
c [block-1] limit of 582368707 steps penalty 2 = 0 + 2
c [block-1] fully completed
c [block-1] transition to [ all 0 rem 0 ] state
c [block-1] eliminated 616844 blocked clauses
c [cce-1] limit of 29118435 steps penalty 2 = 0 + 2
c [cce-1-1] eliminated 2 clauses out of 4 (50%) of length 147
c [cce-1-1] eliminated 2 clauses out of 4 (50%) of length 144
c [cce-1-1] eliminated 3 clauses out of 8 (38%) of length 143
c [cce-1-1] eliminated 5 clauses out of 10 (50%) of length 142
c [cce-1-1] eliminated 5 clauses out of 5 (100%) of length 141
c [cce-1-1] eliminated 4 clauses out of 7 (57%) of length 140
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 21 large clauses in 29118812 steps
c [cce-1-1] allowing another 14559406 steps for small clauses
c [cce-1-1] scheduling 3807801 clauses = 3795031 binary + 12770 ternary
c [cce-1-1] tried to eliminate 35 small clauses 0%
c [cce-1-1] eliminated 1 binary clauses 0%
c [cce-1-1] eliminated 1 small clauses 0%
c [cce-1-1] eliminated 1 small clauses in 29118725 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 22 covered clauses in round 1
c [cce-1] eliminated 22 covered clauses in TOTAL during 1 rounds
c [cce-1] 22 < 1/100 * 4245144 = 42451 considered unsuccessful
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 206176 variables 100%
c [elim-5] limit of 116473741 steps penalty 2 = 0 + 2
c [elim-5] rescheduling of touched variables disabled
c [elim-5] incomplete 85599 not tried 42% in round 1
c [elim-5] transition to [ all 1 rem 1 ] state
c [elim-5] eliminated 14596 = 7% variables out of 206176 scheduled
c [bca-1] limit of 10000000 steps and 8460204 added (scaled 2)
c [bca-1] 345039 out of 383162 literals actually usable 90%
c [bca-1] added 33858 blocked clauses in 1283586 steps
c [sweep-1] limit 8459704 based on 4229852 irredundant clauses
c [sweep-1-1] 4252 pos 2.2% + 187328 neg 97.8% = 191580 sched 100.0% ret 0
c [sweep-1-1] 8471533 steps 23 queries 19921.78 avg class size
c [sweep-1-1] 768 decisions 17 SAT calls 2419.82 avg env size
c [sweep-1-1] 191397 variables remain 100% (183 retained 0%)
c [decomp-10] removed 20 variables
c [sweep-1-1] removed 20 vars (0 failed, 4 eqs, 5 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 20 vars in TOTAL (1 rounds, 22 queries)
c [sort-queue-5] sorted 126052 enqueued variables after 28679 conflicts
c [score-dist-5] active 65508 (34%), one 0 (0%), zero 126052 (66%)
c [score-dist-5] max exp 516, different 15 (3%)
c [score-dist-5] median active exp 516, avg 514.9
c [simplification-5] removed 19432 variables 9.2% (191560 remain 63%)
c [simplification-5] removed 667478 irredundant clauses 13.6% (4229778 remain 70%)
c [simplification-5] maximum reduction of 14% = max (9%, 14%)
c [simplification-5] large reduction 14% >= 5% limit
c [simplification-5] next conflict interval 2000 = 2000/1
c [simplification-5] penalized conflict interval 2000 = 1 * 2000
c [simplification-5] hard conflict limit 40679 (soft 30679 + delta 10000)
c [simplification-5] new conflict limit 30679 (hard 40679)
c 
c [simplification-6] limit 30679 conflicts (hard 40679) hit after 30680 conflicts
c [quatres-2] found 27485 quaternary clauses 8% in total
c [quatres-2-2] added 1 single-self-subsuming ternary resolvents
c [quatres-2-2] added 3095 quaternary resolvents
c [ternres-2] limit 16919104 based on 4229776 irredundant clauses
c [ternres-2] 24717 schedulable variables 13%
c [ternres-2] 38500 ternary resolvents (6 bin, 38494 trn)
c [ternres-2] 2241 variables remain 1% (189319 retained 99%)
c [card-3] limit 1057444 based on 4229776 irredundant clauses
c [card-3] found 7 at-most-one constraints of average size 3.1
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 1057444 for elimination
c [card-3] 7 out of 7 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [basicprobe-2] limit 33838208 based on 4229776 irredundant clauses
c [basicprobe-2-0] 173681 probes remain 95% after last round
c [basicprobe-2-0] 61 units = 61 failed (100%) + 0 lifted (0%)
c [basicprobe-2-0] removed 8150 variables, found 22405 hbrs
c [unhide-6] limit 308673 with penalty 4 = 0 + 4
c [unhide-6-6] 4540 units, 45 failed, 1431 tauts, 0 hbrs, 146380 literals
c [transred-2] limit 4078703 based on 4078703 irredundant clauses
c [transred-2] removed 3 transitive binary clauses
c [transred-2] found 9 units
c [block-2] scheduling all variables this time
c [block-2] scheduled 174631 variables 100%
c [block-2] limit of 61734660 steps penalty 2 = 0 + 2
c [block-2] fully completed
c [block-2] transition to [ all 0 rem 0 ] state
c [block-2] eliminated 38881 blocked clauses
c [block-2] 38881 < 1/100 * 4078702 = 40787 considered unsuccessful
c [elim-6] 10308 variables 6% will be scheduled this time
c [elim-6] scheduled 10308 variables 6%
c [elim-6] limit of 123469320 steps penalty 2 = 0 + 2
c [elim-6] rescheduling of touched variables disabled
c [elim-6] incomplete 5330 not tried 3% in round 1
c [elim-6] transition to [ all 0 rem 1 ] state
c [elim-6] eliminated 31 = 0% variables out of 10308 scheduled
c [elim-6] 31 < 1/100 * 10308 = 103 considered unsuccessful
c [bca-2] limit of 10000000 steps and 7777771 added (scaled 2)
c [bca-2] 306364 out of 348224 literals actually usable 88%
c [bca-2] added 93458 blocked clauses in 1260946 steps
c [sweep-2] limit 7760342 based on 3880171 irredundant clauses
c [sweep-2-1] 4707 pos 2.7% + 169226 neg 97.3% = 173933 sched 99.9% ret 178
c [sweep-2-1] 7762823 steps 25 queries 26313.92 avg class size
c [sweep-2-1] 903 decisions 20 SAT calls 119.00 avg env size
c [sweep-2-1] 173786 variables remain 100% (325 retained 0%)
c [decomp-12] removed 411 variables
c [sweep-2-1] removed 411 vars (0 failed, 4 eqs, 10 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 411 vars in TOTAL (1 rounds, 24 queries)
c [sort-queue-6] sorted 111812 enqueued variables after 30680 conflicts
c [score-dist-6] active 61888 (36%), one 0 (0%), zero 111812 (64%)
c [score-dist-6] max exp 516, different 14 (3%)
c [score-dist-6] median active exp 516, avg 515.1
c [simplification-6] removed 17860 variables 9.3% (173700 remain 57%)
c [simplification-6] removed 350683 irredundant clauses 8.3% (3879093 remain 64%)
c [simplification-6] maximum reduction of 9% = max (9%, 8%)
c [simplification-6] large reduction 9% >= 5% limit
c [simplification-6] next conflict interval 2000 = 2000/1
c [simplification-6] penalized conflict interval 2000 = 1 * 2000
c [simplification-6] hard conflict limit 42680 (soft 32680 + delta 10000)
c [simplification-6] new conflict limit 32680 (hard 42680)
c 
c [simplification-7] limit 32680 conflicts (hard 42680) hit after 32680 conflicts
c [quatres-3] found 32866 quaternary clauses 11% in total
c [quatres-3-1] removed 3 duplicate quaternary clauses
c [quatres-3-1] added 1 double-self-subsuming ternary resolvents
c [quatres-3-2] added 134 single-self-subsuming ternary resolvents
c [quatres-3-2] added 1755 quaternary resolvents
c [ternres-3] limit 15516304 based on 3879076 irredundant clauses
c [ternres-3] 2205 schedulable variables 1%
c [ternres-3] 7767 ternary resolvents (0 bin, 7767 trn)
c [ternres-3] 1967 variables remain 1% (171733 retained 99%)
c [gauss-2] limit 1939538 based on 3879076 irredundant clauses
c [gauss-2] extracted 1 xors of average arity 3.0
c [gauss-2] connected 3 occurrences of 3 variables (average 1.0)
c [gauss-2] limit 1939538 based on 3879076 irredundant clauses
c [gauss-2] fully completed
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [simpleprobe-3] 151629 schedulable variables 87%
c [simpleprobe-3] limit 25880790 penalty 2 = 0 + 2
c [decomp-14] removed 2278 variables
c [simpleprobe-3] 149628 variables remain 87% (21794 retained 13%)
c [simpleprobe-3] removed 2278 variables, found 3897 hbrs, 936 units
c [unhide-7] limit 323509 with penalty 4 = 0 + 4
c [unhide-7-7] 375 units, 67 failed, 44722 tauts, 0 hbrs, 30419 literals
c [transred-3] limit 3779748 based on 3779748 irredundant clauses
c [transred-3] removed 12 transitive binary clauses
c [transred-3] found 4 units
c [cce-2] limit of 16175494 steps penalty 3 = 1 + 2
c [cce-2-1] eliminated 1 clauses out of 4 (25%) of length 152
c [cce-2-1] eliminated 1 clauses out of 1 (100%) of length 148
c [cce-2-1] eliminated 7 clauses out of 11 (64%) of length 147
c [cce-2-1] eliminated 3 clauses out of 3 (100%) of length 146
c [cce-2-1] eliminated 2 clauses out of 2 (100%) of length 145
c [cce-2-1] eliminated 1 clauses out of 1 (100%) of length 141
c [cce-2-1] eliminated 1 clauses out of 3 (33%) of length 137
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] eliminated 16 large clauses in 16182259 steps
c [cce-2-1] allowing another 8091129 steps for small clauses
c [cce-2-1] scheduling 3501632 clauses = 3389382 binary + 112250 ternary
c [cce-2-1] tried to eliminate 43 small clauses 0%
c [cce-2-1] eliminated 6 binary clauses 0%
c [cce-2-1] eliminated 6 small clauses 0%
c [cce-2-1] eliminated 5681 small clauses in 16175760 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 5697 covered clauses in round 1
c [cce-2] eliminated 5697 covered clauses in TOTAL during 1 rounds
c [cce-2] 5697 < 1/100 * 3779744 = 37797 considered unsuccessful
c [bca-3] limit of 10000000 steps and 7612252 added (scaled 2)
c [bca-3] 299315 out of 341964 literals actually usable 88%
c [bca-3] added 42035 blocked clauses in 1303282 steps
c [sweep-3] limit 7548094 based on 3774047 irredundant clauses
c [sweep-3-1] 5690 pos 3.3% + 164976 neg 96.7% = 170666 sched 99.8% ret 315
c [sweep-3-1] 7926262 steps 25 queries 22409.68 avg class size
c [sweep-3-1] 1070 decisions 19 SAT calls 1524.79 avg env size
c [sweep-3-1] 170535 variables remain 100% (446 retained 0%)
c [decomp-15] removed 18 variables
c [sweep-3-1] removed 18 vars (0 failed, 6 eqs, 10 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 18 vars in TOTAL (1 rounds, 24 queries)
c [sort-queue-7] sorted 109249 enqueued variables after 32680 conflicts
c [score-dist-7] active 61714 (36%), one 0 (0%), zero 109249 (64%)
c [score-dist-7] max exp 516, different 14 (3%)
c [score-dist-7] median active exp 516, avg 515.1
c [simplification-7] removed 2737 variables 1.6% (170963 remain 56%)
c [simplification-7] removed 105088 irredundant clauses 2.7% (3774005 remain 62%)
c [simplification-7] maximum reduction of 3% = max (2%, 3%)
c [simplification-7] geometric conflict interval increment 5000 = 20000 / 4
c [simplification-7] new conflict interval 21666
c [simplification-7] penalized conflict interval 21666 = 1 * 21666
c [simplification-7] hard conflict limit 65179 (soft 54346 + delta 10833)
c [simplification-7] new conflict limit 54346 (hard 65179)
c 
c [simplification-8] limit 54346 conflicts (hard 65179) hit after 54346 conflicts
c [quatres-4] found 31533 quaternary clauses 12% in total
c [quatres-4-1] removed 1 duplicate quaternary clauses
c [quatres-4-2] added 3 single-self-subsuming ternary resolvents
c [quatres-4-2] added 1564 quaternary resolvents
c [ternres-4] limit 15096016 based on 3774004 irredundant clauses
c [ternres-4] 1967 schedulable variables 1%
c [ternres-4] 23033 ternary resolvents (46 bin, 22987 trn)
c [ternres-4] 848 variables remain 0% (170115 retained 100%)
c [decomp-16] removed 1 variables
c [unhide-8] limit 474359 with penalty 4 = 0 + 4
c [unhide-8-8] 795 units, 33 failed, 1275 tauts, 0 hbrs, 43619 literals
c [transred-4] limit 3765637 based on 3765637 irredundant clauses
c [transred-4] removed 1 transitive binary clauses
c [transred-4] found 3 units
c [block-3] scheduling all variables this time
c [block-3] scheduled 168197 variables 100%
c [block-3] limit of 47435948 steps penalty 3 = 1 + 2
c [block-3] incomplete 726 not tried 0%
c [block-3] transition to [ all 1 rem 1 ] state
c [block-3] eliminated 77607 blocked clauses
c [elim-7] scheduling all variables this time
c [elim-7] scheduled 166894 variables 100%
c [elim-7] limit of 94871897 steps penalty 3 = 1 + 2
c [elim-7] rescheduling of touched variables disabled
c [elim-7] incomplete 76913 not tried 46% in round 1
c [elim-7] transition to [ all 1 rem 1 ] state
c [elim-7] eliminated 6058 = 4% variables out of 166894 scheduled
c [bca-4] limit of 10000000 steps and 7319513 added (scaled 2)
c [bca-4] 266924 out of 321674 literals actually usable 83%
c [bca-4] added 24422 blocked clauses in 1223658 steps
c [sweep-4] limit 7234338 based on 3617169 irredundant clauses
c [sweep-4-1] 3378 pos 2.1% + 157025 neg 97.9% = 160403 sched 99.7% ret 433
c [sweep-4-1] 7685789 steps 17 queries 24901.94 avg class size
c [sweep-4-1] 574 decisions 13 SAT calls 547.00 avg env size
c [sweep-4-1] 160298 variables remain 100% (538 retained 0%)
c [decomp-17] removed 16 variables
c [sweep-4-1] removed 16 vars (0 failed, 3 eqs, 6 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 16 vars in TOTAL (1 rounds, 16 queries)
c [sort-queue-8] sorted 92549 enqueued variables after 54346 conflicts
c [score-dist-8] active 68271 (42%), one 0 (0%), zero 92549 (58%)
c [score-dist-8] max exp 517, different 15 (3%)
c [score-dist-8] median active exp 517, avg 516.0
c [simplification-8] removed 10143 variables 5.9% (160820 remain 53%)
c [simplification-8] removed 156860 irredundant clauses 4.2% (3617144 remain 60%)
c [simplification-8] maximum reduction of 6% = max (6%, 4%)
c [simplification-8] large reduction 6% >= 5% limit
c [simplification-8] next conflict interval 2000 = 2000/1
c [simplification-8] penalized conflict interval 2000 = 1 * 2000
c [simplification-8] hard conflict limit 66346 (soft 56346 + delta 10000)
c [simplification-8] new conflict limit 56346 (hard 66346)
c 
c [simplification-9] limit 56346 conflicts (hard 66346) hit after 56352 conflicts
c [quatres-5] found 32688 quaternary clauses 13% in total
c [quatres-5-2] added 71 single-self-subsuming ternary resolvents
c [quatres-5-2] added 988 quaternary resolvents
c [ternres-5] limit 14468572 based on 3617143 irredundant clauses
c [ternres-5] 843 schedulable variables 1%
c [ternres-5] 12886 ternary resolvents (1 bin, 12885 trn)
c [ternres-5] 317 variables remain 0% (160503 retained 100%)
c [unhide-9] limit 482726 with penalty 4 = 0 + 4
c [unhide-9-9] 355 units, 49 failed, 34377 tauts, 0 hbrs, 18575 literals
c [transred-5] limit 3583787 based on 3583787 irredundant clauses
c [transred-5] removed 3 transitive binary clauses
c [transred-5] found 6 units
c [block-4] 726 variables 0% will be scheduled this time
c [block-4] scheduled 726 variables 0%
c [block-4] limit of 96545308 steps penalty 2 = 0 + 2
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 1 blocked clauses
c [block-4] 1 < 1/100 * 3583786 = 35837 considered unsuccessful
c [elim-8] 5267 variables 3% will be scheduled this time
c [elim-8] scheduled 5267 variables 3%
c [elim-8] boosting limit by 20
c [elim-8] limit of 3861812345 steps penalty 2 = 0 + 2
c [elim-8] rescheduling of touched variables disabled
c [elim-8-1] eliminated 2 variables 0% in round 1 in 728321036 steps
c [elim-8-1] backward subsumption/strengthening limit 728321000
c [elim-8-1-1] backward checking 10328 touched variables 6%
c [elim-8-1-1] incomplete backward checking 10348 remain 100%
c [elim-8-1] subsumed 52 and strengthened 136 clauses in 728327792 steps
c [elim-8-1] rescheduled 1368 variables 1% by backward subsumption
c [elim-8-2] eliminated 45 variables 0% in round 2 in 68574290 steps
c [elim-8-2] backward subsumption/strengthening limit 68574200
c [elim-8-2-1] backward checking 10484 touched variables 7%
c [elim-8-2-1] incomplete backward checking 10481 remain 100%
c [elim-8-2] subsumed 0 and strengthened 76 clauses in 68576685 steps
c [elim-8-2] rescheduled 156 variables 0% by backward subsumption
c [elim-8-3] no variable eliminated in round 3 in 61528178 steps
c [elim-8] fully completed in 3 rounds
c [elim-8] transition to [ all 0 rem 0 ] state
c [elim-8] eliminated 47 = 1% variables out of 5267 scheduled
c [elim-8] 47 < 1/100 * 5267 = 52 considered unsuccessful
c [bca-5] limit of 10000000 steps and 7230434 added (scaled 2)
c [bca-5] 265420 out of 320696 literals actually usable 83%
c [bca-5] added 15908 blocked clauses in 1192689 steps
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 28963592 penalty 2 = 0 + 2
c [sweep-5-1] 3368 pos 2.1% + 156445 neg 97.9% = 159813 sched 99.7% ret 534
c [sweep-5-1] 29345300 steps 82 queries 7496.26 avg class size
c [sweep-5-1] 3234 decisions 62 SAT calls 799.52 avg env size
c [sweep-5-1] 154248 variables remain 99% (1912 retained 1%)
c [decomp-19] removed 4248 variables
c [sweep-5-1] removed 4248 vars (0 failed, 20 eqs, 43 impls)
c [sweep-5] considered successful since not run to completion yet
c [sweep-5] removed 4248 vars in TOTAL (1 rounds, 81 queries)
c [sort-queue-9] sorted 89829 enqueued variables after 56352 conflicts
c [score-dist-9] active 66270 (42%), one 0 (0%), zero 89829 (58%)
c [score-dist-9] max exp 517, different 15 (3%)
c [score-dist-9] median active exp 517, avg 516.1
c [simplification-9] removed 4721 variables 2.9% (156099 remain 51%)
c [simplification-9] removed 108588 irredundant clauses 3.0% (3508556 remain 58%)
c [simplification-9] maximum reduction of 3% = max (3%, 3%)
c [simplification-9] geometric conflict interval increment 5416 = 21666 / 4
c [simplification-9] new conflict interval 27082
c [simplification-9] penalized conflict interval 27082 = 1 * 27082
c [simplification-9] hard conflict limit 96975 (soft 83434 + delta 13541)
c [simplification-9] new conflict limit 83434 (hard 96975)
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 -  408.3  156099  3508556     69782   22359 111382 197382   30   981  161   3%    665  446   29   18  158%
c 
c [simplification-10] limit 83434 conflicts (hard 96975) hit after 86627 conflicts
c [quatres-6] found 34996 quaternary clauses 15% in total
c [quatres-6-2] added 1746 single-self-subsuming ternary resolvents
c [quatres-6-2] added 1519 quaternary resolvents
c [ternres-6] limit 14034176 based on 3508544 irredundant clauses
c [ternres-6] 316 schedulable variables 0%
c [ternres-6] 2434 ternary resolvents (0 bin, 2434 trn)
c [ternres-6] 186 variables remain 0% (155913 retained 100%)
c [card-4] limit 877136 based on 3508544 irredundant clauses
c [card-4] found 15 at-most-one constraints of average size 3.6
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 877136 for elimination
c [card-4] 15 out of 15 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [gauss-3] limit 1754272 based on 3508544 irredundant clauses
c [gauss-3] extracted 0 xors of average arity 0.0
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [treelook-3] limit 877136 based on 3508544 irredundant clauses
c [treelook-3] scheduled 122372 literals 39%
c [treelook-3] scheduling used 877315 steps
c [treelook-3] not fully scheduled
c [treelook-3] limit 877136 based on 3508544 irredundant clauses
c [treelook-3] used 2025941 steps
c [treelook-3] 122370 literals remain 39%
c [treelook-3] 102094 variables remain to probed next time 65%
c [treelook-3] removed 0 variables, found 11 hbrs
c [unhide-10] limit 610789 with penalty 4 = 0 + 4
c [unhide-10-10] 257 units, 34 failed, 2579 tauts, 0 hbrs, 59945 literals
c [transred-6] limit 3508185 based on 3508185 irredundant clauses
c [transred-6] removed 6 transitive binary clauses
c [transred-6] found 9 units
c [cce-3] limit of 15269736 steps penalty 4 = 2 + 2
c [cce-3-1] eliminated 1 clauses out of 1 (100%) of length 146
c [cce-3-1] eliminated 12 clauses out of 13 (92%) of length 142
c [cce-3-1] eliminated 5 clauses out of 5 (100%) of length 140
c [cce-3-1] eliminated 1 clauses out of 5 (20%) of length 136
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 19 large clauses in 15269824 steps
c [cce-3-1] allowing another 7634912 steps for small clauses
c [cce-3-1] scheduling 3182643 clauses = 3165598 binary + 17045 ternary
c [cce-3-1] tried to eliminate 51 small clauses 0%
c [cce-3-1] eliminated 19 binary clauses 0%
c [cce-3-1] eliminated 19 small clauses 0%
c [cce-3-1] eliminated 3992 small clauses in 15269859 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 4011 covered clauses in round 1
c [cce-3] eliminated 4011 covered clauses in TOTAL during 1 rounds
c [cce-3] 4011 < 1/100 * 3508184 = 35081 considered unsuccessful
c [bca-6] limit of 10000000 steps and 7113686 added (scaled 2)
c [bca-6] 263142 out of 311576 literals actually usable 84%
c [bca-6] added 7212 blocked clauses in 1173704 steps
c [sweep-6] limit 7008346 based on 3504173 irredundant clauses
c [sweep-6-1] 3835 pos 2.5% + 150057 neg 97.5% = 153892 sched 98.8% ret 1895
c [sweep-6-1] 7464590 steps 12 queries 27293.08 avg class size
c [sweep-6-1] 492 decisions 11 SAT calls 554.91 avg env size
c [sweep-6-1] 153838 variables remain 99% (1949 retained 1%)
c [decomp-22] removed 19 variables
c [sweep-6-1] removed 19 vars (0 failed, 0 eqs, 2 impls)
c [sweep-6] considered successful since not run to completion yet
c [sweep-6] removed 19 vars in TOTAL (1 rounds, 11 queries)
c [sort-queue-10] sorted 84216 enqueued variables after 86627 conflicts
c [score-dist-10] active 71552 (46%), one 0 (0%), zero 84216 (54%)
c [score-dist-10] max exp 518, different 16 (3%)
c [score-dist-10] median active exp 517, avg 516.8
c [simplification-10] removed 331 variables 0.2% (155768 remain 51%)
c [simplification-10] removed 4456 irredundant clauses 0.1% (3504089 remain 58%)
c [simplification-10] maximum reduction of 0% = max (0%, 0%)
c [simplification-10] full geometric conflict interval increment 27082
c [simplification-10] new conflict interval 54164
c [simplification-10] penalized conflict interval 54164 = 1 * 54164
c [simplification-10] hard conflict limit 167873 (soft 140791 + delta 27082)
c [simplification-10] new conflict limit 140791 (hard 167873)
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  450.7  155767  3504089     98548   49263 112711 199570   25   624  170   4%    793   12   17   22   79%
c i  469.4  155766  3504089    113423   62495 112820 199636   31   708  175   4%   -407   60   27   23  116%
c -  469.7  155766  3504089    114124   30055 112824 199641   29   611  162   5%   -506  -38   14   23   61%
c i  474.8  155765  3504089    136591   49605 112861 199690   15    55  171  27%   -147 -456   10   22   44%
c i  478.2  155751  3504089    138350   51200 112896 199711   21   335  171   6%   -408 -168   32   22  145%
c i  485.0  155750  3504089    144888   57032 112930 199726   25   364  173   7%   -357 -138   23   22  104%
c -  487.2  155750  3504089    153483   35557 112936 199746   17   166  163  10%   -278 -301   14   22   66%
c i  487.7  155749  3504089    154954   36764 112954 199774   17   176  167  10%   -249 -285   17   22   79%
c 
c [simplification-11] limit 140791 conflicts (hard 167873) hit after 167873 conflicts
c [quatres-7] found 34729 quaternary clauses 16% in total
c [quatres-7-2] added 26 single-self-subsuming ternary resolvents
c [quatres-7-2] added 605 quaternary resolvents
c [ternres-7] limit 15889483 with penalty 2 = 0 + 2
c [ternres-7] 186 schedulable variables 0%
c [ternres-7] 5303 ternary resolvents (0 bin, 5303 trn)
c [ternres-7] 82 variables remain 0% (155606 retained 100%)
c [decomp-23] removed 94 variables
c [basicprobe-3] limit 79447416 penalty 2 = 0 + 2
c [basicprobe-3-0] 138386 probes remain 93% after last round
c [basicprobe-3-0] 135 units = 135 failed (100%) + 0 lifted (0%)
c [basicprobe-3-0] removed 7042 variables, found 23189 hbrs
c [bate-1] eliminated 32 asymmetric tautologies during probing
c [unhide-11] limit 794474 with penalty 4 = 0 + 4
c [unhide-11-11] 1447 units, 275 failed, 26883 tauts, 0 hbrs, 52364 literals
c [transred-7] limit 3332869 based on 3332869 irredundant clauses
c [transred-7] removed 8 transitive binary clauses
c [transred-7] found 7 units
c [block-5] scheduling all variables this time
c [block-5] scheduled 146760 variables 100%
c [block-5] limit of 79447416 steps penalty 3 = 1 + 2
c [block-5] fully completed
c [block-5] transition to [ all 0 rem 0 ] state
c [block-5] eliminated 109416 blocked clauses
c [elim-9] scheduling all variables this time
c [elim-9] scheduled 144140 variables 100%
c [elim-9] limit of 100000000 steps penalty 3 = 1 + 2
c [elim-9] rescheduling of touched variables disabled
c [elim-9] incomplete 63317 not tried 44% in round 1
c [elim-9] transition to [ all 1 rem 1 ] state
c [elim-9] eliminated 7702 = 5% variables out of 144140 scheduled
c [bca-7] limit of 10000000 steps and 6431618 added (scaled 2)
c [bca-7] 224319 out of 272878 literals actually usable 82%
c [bca-7] added 126852 blocked clauses in 1320923 steps
c [sweep-7] limit 6322672 based on 3161336 irredundant clauses
c [sweep-7-1] 3048 pos 2.3% + 131639 neg 97.7% = 134687 sched 98.7% ret 1751
c [sweep-7-1] 6656605 steps 26 queries 19033.50 avg class size
c [sweep-7-1] 724 decisions 22 SAT calls 145.68 avg env size
c [sweep-7-1] 134443 variables remain 99% (1994 retained 1%)
c [decomp-24] removed 51 variables
c [sweep-7-1] removed 51 vars (1 failed, 2 eqs, 8 impls)
c [sweep-7] 51 < 1/1000 * 136438 = 136 considered unsuccessful
c [sweep-7] removed 51 vars in TOTAL (1 rounds, 25 queries)
c [sort-queue-11] sorted 66422 enqueued variables after 167873 conflicts
c [score-dist-11] active 69965 (51%), one 0 (0%), zero 66422 (49%)
c [score-dist-11] max exp 519, different 17 (3%)
c [score-dist-11] median active exp 518, avg 517.9
c [simplification-11] removed 19301 variables 12.4% (136387 remain 45%)
c [simplification-11] removed 347592 irredundant clauses 9.9% (3156497 remain 52%)
c [simplification-11] maximum reduction of 12% = max (12%, 10%)
c [simplification-11] large reduction 12% >= 5% limit
c [simplification-11] next conflict interval 2000 = 2000/1
c [simplification-11] penalized conflict interval 2000 = 1 * 2000
c [simplification-11] hard conflict limit 179873 (soft 169873 + delta 10000)
c [simplification-11] new conflict limit 169873 (hard 179873)
c 
c [simplification-12] limit 169873 conflicts (hard 179873) hit after 176976 conflicts
c [quatres-8] found 31388 quaternary clauses 16% in total
c [quatres-8-1] removed 14 duplicate quaternary clauses
c [quatres-8-2] added 3741 single-self-subsuming ternary resolvents
c [quatres-8-2] added 309 quaternary resolvents
c [ternres-8] limit 16521245 with penalty 2 = 0 + 2
c [ternres-8] 77 schedulable variables 0%
c [ternres-8] 1088 ternary resolvents (0 bin, 1088 trn)
c [ternres-8] 3 variables remain 0% (136384 retained 100%)
c [simpleprobe-4] 119031 schedulable variables 87%
c [simpleprobe-4] limit 50000000 penalty 2 = 0 + 2
c [decomp-26] removed 145 variables
c [simpleprobe-4] 120665 variables remain 89% (15577 retained 11%)
c [simpleprobe-4] removed 145 variables, found 13457 hbrs, 120 units
c [unhide-12] limit 826062 with penalty 4 = 0 + 4
c [unhide-12-12] 3603 units, 1426 failed, 8395 tauts, 0 hbrs, 80393 literals
c [transred-8] limit 3138347 based on 3138347 irredundant clauses
c [transred-8] removed 1 transitive binary clauses
c [transred-8] found 2 units
c [block-6] scheduling all variables this time
c [block-6] scheduled 128225 variables 100%
c [block-6] limit of 165212450 steps penalty 2 = 0 + 2
c [block-6] fully completed
c [block-6] transition to [ all 0 rem 0 ] state
c [block-6] eliminated 126230 blocked clauses
c [elim-10] 61337 variables 48% will be scheduled this time
c [elim-10] scheduled 61337 variables 48%
c [elim-10] limit of 400000000 steps penalty 1 = 0 + 1
c [elim-10] rescheduling of touched variables disabled
c [elim-10] incomplete 6864 not tried 5% in round 1
c [elim-10] transition to [ all 0 rem 1 ] state
c [elim-10] eliminated 2346 = 4% variables out of 61337 scheduled
c [bca-8] limit of 10000000 steps and 5831628 added (scaled 2)
c [bca-8] 201933 out of 249010 literals actually usable 81%
c [bca-8] added 23413 blocked clauses in 918683 steps
c [sort-queue-12] sorted 58401 enqueued variables after 176976 conflicts
c [score-dist-12] active 66103 (53%), one 0 (0%), zero 58401 (47%)
c [score-dist-12] max exp 519, different 17 (3%)
c [score-dist-12] median active exp 519, avg 518.0
c [simplification-12] removed 11883 variables 8.7% (124504 remain 41%)
c [simplification-12] removed 326869 irredundant clauses 10.4% (2829628 remain 47%)
c [simplification-12] maximum reduction of 10% = max (9%, 10%)
c [simplification-12] large reduction 10% >= 5% limit
c [simplification-12] next conflict interval 2000 = 2000/1
c [simplification-12] penalized conflict interval 2000 = 1 * 2000
c [simplification-12] hard conflict limit 188976 (soft 178976 + delta 10000)
c [simplification-12] new conflict limit 178976 (hard 188976)
c 
c [simplification-13] limit 178976 conflicts (hard 188976) hit after 178976 conflicts
c [quatres-9] found 27340 quaternary clauses 15% in total
c [quatres-9-2] added 378 single-self-subsuming ternary resolvents
c [quatres-9-2] added 579 quaternary resolvents
c [ternres-9] limit 33298990 with penalty 1 = 0 + 1
c [ternres-9] 3 schedulable variables 0%
c [ternres-9] 646 ternary resolvents (0 bin, 646 trn)
c [ternres-9] fully completed ternary resolution
c [decomp-27] removed 28 variables
c [unhide-13] limit 1664949 with penalty 3 = 0 + 3
c [unhide-13-13] 29 units, 137 failed, 28736 tauts, 0 hbrs, 15913 literals
c [transred-9] limit 2804411 based on 2804411 irredundant clauses
c [transred-9] removed 7 transitive binary clauses
c [transred-9] found 5 units
c [block-7] scheduling all variables this time
c [block-7] scheduled 124301 variables 100%
c [block-7] limit of 332989903 steps penalty 1 = 0 + 1
c [block-7] fully completed
c [block-7] transition to [ all 0 rem 0 ] state
c [block-7] eliminated 47875 blocked clauses
c [elim-11] scheduling all variables this time
c [elim-11] scheduled 122613 variables 100%
c [elim-11] limit of 400000000 steps penalty 1 = 0 + 1
c [elim-11] rescheduling of touched variables disabled
c [elim-11] incomplete 6454 not tried 5% in round 1
c [elim-11] transition to [ all 1 rem 1 ] state
c [elim-11] eliminated 4274 = 3% variables out of 122613 scheduled
c [bca-9] limit of 10000000 steps and 5616103 added (scaled 2)
c [bca-9] 189130 out of 236680 literals actually usable 80%
c [bca-9] added 5798 blocked clauses in 841366 steps
c [sweep-8] limit 5432024 based on 2716012 irredundant clauses
c [sweep-8-1] 3008 pos 2.6% + 113653 neg 97.4% = 116661 sched 98.6% ret 1678
c [sweep-8-1] 5575218 steps 20 queries 19187.75 avg class size
c [sweep-8-1] 613 decisions 17 SAT calls 374.94 avg env size
c [sweep-8-1] 116564 variables remain 99% (1774 retained 1%)
c [decomp-28] removed 41 variables
c [sweep-8-1] removed 41 vars (1 failed, 1 eqs, 2 impls)
c [sweep-8] 41 < 1/1000 * 118339 = 118 considered unsuccessful
c [sweep-8] removed 41 vars in TOTAL (1 rounds, 19 queries)
c [sort-queue-13] sorted 53267 enqueued variables after 178976 conflicts
c [score-dist-13] active 65031 (55%), one 0 (0%), zero 53267 (45%)
c [score-dist-13] max exp 519, different 17 (3%)
c [score-dist-13] median active exp 519, avg 518.0
c [simplification-13] removed 6206 variables 5.0% (118298 remain 39%)
c [simplification-13] removed 113708 irredundant clauses 4.0% (2715916 remain 45%)
c [simplification-13] maximum reduction of 5% = max (5%, 4%)
c [simplification-13] large reduction 5% >= 5% limit
c [simplification-13] next conflict interval 2000 = 2000/1
c [simplification-13] penalized conflict interval 2000 = 1 * 2000
c [simplification-13] hard conflict limit 190976 (soft 180976 + delta 10000)
c [simplification-13] new conflict limit 180976 (hard 190976)
c 
c [simplification-14] limit 180976 conflicts (hard 190976) hit after 180976 conflicts
c [quatres-10] found 27106 quaternary clauses 16% in total
c [quatres-10-2] added 145 single-self-subsuming ternary resolvents
c [quatres-10-2] added 418 quaternary resolvents
c [ternres-10] limit 33544518 with penalty 1 = 0 + 1
c [ternres-10] all 118298 free variables schedulable
c [ternres-10] 2403 ternary resolvents (0 bin, 2403 trn)
c [ternres-10] 60459 variables remain 51% (57839 retained 49%)
c [gauss-4] limit 1357958 based on 2715916 irredundant clauses
c [gauss-4] extracted 2 xors of average arity 3.0
c [gauss-4] connected 6 occurrences of 3 variables (average 2.0)
c [gauss-4] limit 1357958 based on 2715916 irredundant clauses
c [gauss-4] fully completed
c [gauss-4] exported 0 unary, 0 binary and 0 ternary equations
c [unhide-14] limit 1677225 with penalty 3 = 0 + 3
c [unhide-14-14] 208 units, 698 failed, 2852 tauts, 0 hbrs, 29064 literals
c [transred-10] limit 2715485 based on 2715485 irredundant clauses
c [transred-10] removed 9 transitive binary clauses
c [transred-10] found 2 units
c [block-8] scheduling all variables this time
c [block-8] scheduled 117372 variables 100%
c [block-8] limit of 335445185 steps penalty 1 = 0 + 1
c [block-8] fully completed
c [block-8] transition to [ all 0 rem 0 ] state
c [block-8] eliminated 4770 blocked clauses
c [block-8] 4770 < 1/100 * 2715481 = 27154 considered unsuccessful
c [cce-4] boosting limit by 10
c [cce-4] limit of 209653240 steps penalty 4 = 3 + 1
c [cce-4-1] eliminated 1 clauses out of 21 (5%) of length 129
c [cce-4-1] eliminated 1 clauses out of 21 (5%) of length 127
c [cce-4-1] eliminated 4 clauses out of 40 (10%) of length 126
c [cce-4-1] eliminated 4 clauses out of 28 (14%) of length 124
c [cce-4-1] eliminated 10 clauses out of 44 (23%) of length 123
c [cce-4-1] eliminated 1 clauses out of 52 (2%) of length 122
c [cce-4-1] eliminated 15 clauses out of 42 (36%) of length 121
c [cce-4-1] eliminated 1 clauses out of 63 (2%) of length 120
c [cce-4-1] eliminated 4 clauses out of 57 (7%) of length 118
c [cce-4-1] eliminated 9 clauses out of 95 (9%) of length 116
c [cce-4-1] eliminated 1 clauses out of 55 (2%) of length 115
c [cce-4-1] eliminated 8 clauses out of 101 (8%) of length 114
c [cce-4-1] eliminated 7 clauses out of 146 (5%) of length 113
c [cce-4-1] eliminated 6 clauses out of 75 (8%) of length 112
c [cce-4-1] eliminated 14 clauses out of 123 (11%) of length 111
c [cce-4-1] eliminated 6 clauses out of 121 (5%) of length 110
c [cce-4-1] eliminated 8 clauses out of 74 (11%) of length 109
c [cce-4-1] eliminated 9 clauses out of 168 (5%) of length 108
c [cce-4-1] eliminated 5 clauses out of 148 (3%) of length 107
c [cce-4-1] eliminated 13 clauses out of 136 (10%) of length 106
c [cce-4-1] eliminated 21 clauses out of 162 (13%) of length 105
c [cce-4-1] incomplete large round (ATE)
c [cce-4-1] eliminated 148 large clauses in 209654390 steps
c [cce-4-1] allowing another 104827195 steps for small clauses
c [cce-4-1] scheduling 2444901 clauses = 2431646 binary + 13255 ternary
c [cce-4-1] tried to eliminate 1160 small clauses 0%
c [cce-4-1] eliminated 152 binary clauses 0%
c [cce-4-1] eliminated 3 ternary clauses 0%
c [cce-4-1] eliminated 155 small clauses 0%
c [cce-4-1] eliminated 155 small clauses in 209653336 steps
c [cce-4-1] incomplete small round (ATE)
c [cce-4-1] eliminated 303 covered clauses in round 1
c [cce-4] eliminated 303 covered clauses in TOTAL during 1 rounds
c [cce-4] 303 < 1/100 * 2697597 = 26975 considered unsuccessful
c [elim-12] 6438 variables 5% will be scheduled this time
c [elim-12] scheduled 6438 variables 5%
c [elim-12] limit of 400000000 steps penalty 1 = 0 + 1
c [elim-12] rescheduling of touched variables disabled
c [elim-12] incomplete 2402 not tried 2% in round 1
c [elim-12] transition to [ all 0 rem 1 ] state
c [elim-12] eliminated 32 = 0% variables out of 6438 scheduled
c [elim-12] 32 < 1/100 * 6438 = 64 considered unsuccessful
c [bca-10] limit of 10000000 steps and 5575110 added (scaled 2)
c [bca-10] 185967 out of 234276 literals actually usable 79%
c [bca-10] added 1492 blocked clauses in 811809 steps
c [sort-queue-14] sorted 52447 enqueued variables after 180976 conflicts
c [score-dist-14] active 64690 (55%), one 0 (0%), zero 52447 (45%)
c [score-dist-14] max exp 519, different 17 (3%)
c [score-dist-14] median active exp 519, avg 518.1
c [simplification-14] removed 1161 variables 1.0% (117137 remain 38%)
c [simplification-14] removed 21850 irredundant clauses 0.8% (2694066 remain 44%)
c [simplification-14] maximum reduction of 1% = max (1%, 1%)
c [simplification-14] geometric conflict interval increment 27082 = 54164 / 2
c [simplification-14] new conflict interval 81246
c [simplification-14] penalized conflict interval 81246 = 1 * 81246
c [simplification-14] hard conflict limit 302845 (soft 262222 + delta 40623)
c [simplification-14] new conflict limit 262222 (hard 302845)
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 -  630.5  117137  2694066    210415   27479  91588 133088   31   740  137   4%    409  156   34   26  132%
c -  649.9  117137  2694066    253435   32695  91722 133171   24   345  138   7%    705 -102   26   24  108%
c -  660.3  117137  2694066    291700   35717  91819 133218   15    29  138  51%    846 -276   18   22   81%
c 
c [simplification-15] limit 262222 conflicts (hard 302845) hit after 302845 conflicts
c [quatres-11] found 29392 quaternary clauses 17% in total
c [quatres-11-1] removed 4 duplicate quaternary clauses
c [quatres-11-2] added 92 single-self-subsuming ternary resolvents
c [quatres-11-2] added 378 quaternary resolvents
c [ternres-11] limit 40201985 with penalty 1 = 0 + 1
c [ternres-11] 59857 schedulable variables 51%
c [ternres-11] 4955 ternary resolvents (0 bin, 4955 trn)
c [ternres-11] 588 variables remain 1% (116549 retained 99%)
c [card-5] limit 1256312 penalty 5 = 4 + 1
c [card-5] found 22 at-most-one constraints of average size 3.1
c [card-5] no at-most-two constraint found
c [card-5] using previous limit 1256312 for elimination
c [card-5] 22 out of 22 constraints (100%) meet size limits
c [card-5] no units found
c [card-5] no at-most-one constraints generated
c [decomp-30] removed 14 variables
c [unhide-15] limit 2010099 with penalty 3 = 0 + 3
c [unhide-15-15] 43 units, 28 failed, 17169 tauts, 0 hbrs, 8529 literals
c [transred-11] limit 2673867 based on 2673867 irredundant clauses
c [transred-11] removed 7 transitive binary clauses
c [bca-11] limit of 10000000 steps and 5323656 added (scaled 2)
c [bca-11] 183922 out of 221566 literals actually usable 83%
c [bca-11] added 9083 blocked clauses in 753956 steps
c [sort-queue-15] sorted 44529 enqueued variables after 302845 conflicts
c [score-dist-15] active 66253 (60%), one 0 (0%), zero 44529 (40%)
c [score-dist-15] max exp 520, different 18 (3%)
c [score-dist-15] median active exp 519, avg 518.6
c [simplification-15] removed 6355 variables 5.4% (110782 remain 36%)
c [simplification-15] removed 126100 irredundant clauses 4.7% (2567966 remain 42%)
c [simplification-15] maximum reduction of 5% = max (5%, 5%)
c [simplification-15] large reduction 5% >= 5% limit
c [simplification-15] next conflict interval 3028 = min (302845/100, 81246)
c [simplification-15] penalized conflict interval 3028 = 1 * 3028
c [simplification-15] hard conflict limit 315873 (soft 305873 + delta 10000)
c [simplification-15] new conflict limit 305873 (hard 315873)
c 
c [simplification-16] limit 305873 conflicts (hard 315873) hit after 308288 conflicts
c [quatres-12] found 31490 quaternary clauses 19% in total
c [quatres-12-1] removed 6 duplicate quaternary clauses
c [quatres-12-2] added 2021 single-self-subsuming ternary resolvents
c [quatres-12-2] added 89 quaternary resolvents
c [ternres-12] limit 40544751 with penalty 1 = 0 + 1
c [ternres-12] 565 schedulable variables 1%
c [ternres-12] 2489 ternary resolvents (4 bin, 2485 trn)
c [ternres-12] 4 variables remain 0% (110778 retained 100%)
c [decomp-31] removed 64 variables
c [treelook-4] limit 641823 based on 2567294 irredundant clauses
c [treelook-4] scheduled 79197 literals 36%
c [treelook-4] scheduling used 645209 steps
c [treelook-4] not fully scheduled
c [treelook-4] limit 641823 based on 2567294 irredundant clauses
c [treelook-4] used 2008629 steps
c [treelook-4] 79193 literals remain 36%
c [treelook-4] 63905 variables remain to probed next time 58%
c [decomp-32] removed 1 variables
c [treelook-4] removed 1 variables, found 310 hbrs
c [unhide-16] limit 2027237 with penalty 3 = 0 + 3
c [unhide-16-16] 91 units, 50 failed, 2888 tauts, 0 hbrs, 71085 literals
c [transred-12] limit 2562743 based on 2562743 irredundant clauses
c [transred-12] removed 7 transitive binary clauses
c [transred-12] found 2 units
c [block-9] scheduling all variables this time
c [block-9] scheduled 110514 variables 100%
c [block-9] limit of 200000000 steps penalty 2 = 1 + 1
c [block-9] fully completed
c [block-9] transition to [ all 0 rem 0 ] state
c [block-9] eliminated 67796 blocked clauses
c [elim-13] scheduling all variables this time
c [elim-13] scheduled 110343 variables 100%
c [elim-13] almost no limit of 100000000000 steps
c [elim-13] rescheduling of touched variables disabled
c [elim-13-1] eliminated 5080 variables 5% in round 1 in 2868355879 steps
c [elim-13-1] backward subsumption/strengthening limit 2868355800
c [elim-13-1-1] backward checking 42557 touched variables 39%
c [elim-13-1-1] incomplete backward checking 42708 remain 100%
c [elim-13-1] subsumed 0 and strengthened 194 clauses in 2868356453 steps
c [elim-13-1] rescheduled 429 variables 0% by backward subsumption
c [elim-13-2] no variable eliminated in round 2 in 324246715 steps
c [elim-13] fully completed in 2 rounds
c [elim-13] transition to [ all 0 rem 0 ] state
c [elim-13] eliminated 5106 = 5% variables out of 110343 scheduled
c [bca-12] limit of 10000000 steps and 4992515 added (scaled 2)
c [bca-12] 173581 out of 210476 literals actually usable 82%
c [bca-12] added 7644 blocked clauses in 700129 steps
c [sweep-9] limit 4800250 based on 2400125 irredundant clauses
c [sweep-9-1] 2668 pos 2.6% + 100957 neg 97.4% = 103625 sched 98.5% ret 1612
c [sweep-9-1] 4929246 steps 34 queries 18949.29 avg class size
c [sweep-9-1] 1489 decisions 30 SAT calls 206.03 avg env size
c [sweep-9-1] 102049 variables remain 98% (1830 retained 2%)
c [decomp-33] removed 1426 variables
c [sweep-9-1] removed 1426 vars (0 failed, 3 eqs, 7 impls)
c [sweep-9] removed 1426 vars in TOTAL (1 rounds, 33 queries)
c [sort-queue-16] sorted 40216 enqueued variables after 308288 conflicts
c [score-dist-16] active 63595 (61%), one 0 (0%), zero 40216 (39%)
c [score-dist-16] max exp 520, different 18 (3%)
c [score-dist-16] median active exp 519, avg 518.7
c [simplification-16] removed 6971 variables 6.3% (103811 remain 34%)
c [simplification-16] removed 186580 irredundant clauses 7.3% (2381386 remain 39%)
c [simplification-16] maximum reduction of 7% = max (6%, 7%)
c [simplification-16] large reduction 7% >= 5% limit
c [simplification-16] next conflict interval 3082 = min (308288/100, 81246)
c [simplification-16] penalized conflict interval 3082 = 1 * 3082
c [simplification-16] hard conflict limit 321370 (soft 311370 + delta 10000)
c [simplification-16] new conflict limit 311370 (hard 321370)
c 
c [simplification-17] limit 311370 conflicts (hard 321370) hit after 311372 conflicts
c [quatres-13] found 27814 quaternary clauses 19% in total
c [quatres-13-1] removed 2 duplicate quaternary clauses
c [quatres-13-2] added 18 single-self-subsuming ternary resolvents
c [quatres-13-2] added 577 quaternary resolvents
c [ternres-13] limit 41034542 with penalty 1 = 0 + 1
c [ternres-13] 4 schedulable variables 0%
c [ternres-13] 3181 ternary resolvents (2 bin, 3179 trn)
c [ternres-13] 1 variables remain 0% (103810 retained 100%)
c [basicprobe-4] limit 200000000 penalty 1 = 0 + 1
c [basicprobe-4-0] 90883 probes remain 88% after last round
c [basicprobe-4-0] 344 units = 292 failed (85%) + 52 lifted (15%)
c [basicprobe-4-0] removed 766 variables, found 45649 hbrs
c [bate-2] eliminated 59 asymmetric tautologies during probing
c [unhide-17] limit 2051727 with penalty 3 = 0 + 3
c [unhide-17-17] 1133 units, 211 failed, 17337 tauts, 0 hbrs, 28625 literals
c [transred-13] limit 2355987 based on 2355987 irredundant clauses
c [transred-13] removed 14 transitive binary clauses
c [block-10] scheduling all variables this time
c [block-10] scheduled 101395 variables 100%
c [block-10] limit of 400000000 steps penalty 1 = 0 + 1
c [block-10] fully completed
c [block-10] transition to [ all 0 rem 0 ] state
c [block-10] eliminated 35680 blocked clauses
c [elim-14] scheduling all variables this time
c [elim-14] scheduled 101200 variables 100%
c [elim-14] limit of 400000000 steps penalty 1 = 0 + 1
c [elim-14] rescheduling of touched variables disabled
c [elim-14] incomplete 4709 not tried 5% in round 1
c [elim-14] transition to [ all 1 rem 1 ] state
c [elim-14] eliminated 3656 = 4% variables out of 101200 scheduled
c [bca-13] limit of 10000000 steps and 4698455 added (scaled 2)
c [bca-13] 156109 out of 195090 literals actually usable 80%
c [bca-13] added 23501 blocked clauses in 654755 steps
c [sort-queue-17] sorted 35968 enqueued variables after 311372 conflicts
c [score-dist-17] active 61576 (63%), one 0 (0%), zero 35968 (37%)
c [score-dist-17] max exp 520, different 18 (3%)
c [score-dist-17] median active exp 519, avg 518.8
c [simplification-17] removed 6267 variables 6.0% (97544 remain 32%)
c [simplification-17] removed 130202 irredundant clauses 5.5% (2251184 remain 37%)
c [simplification-17] maximum reduction of 6% = max (6%, 5%)
c [simplification-17] large reduction 6% >= 5% limit
c [simplification-17] next conflict interval 3113 = min (311372/100, 81246)
c [simplification-17] penalized conflict interval 3113 = 1 * 3113
c [simplification-17] hard conflict limit 324485 (soft 314485 + delta 10000)
c [simplification-17] new conflict limit 314485 (hard 324485)
c 
c [simplification-18] limit 314485 conflicts (hard 324485) hit after 314485 conflicts
c [quatres-14] found 31639 quaternary clauses 22% in total
c [quatres-14-1] added 2 double-self-subsuming ternary resolvents
c [quatres-14-2] added 46 single-self-subsuming ternary resolvents
c [quatres-14-2] added 213 quaternary resolvents
c [ternres-14] limit 41426453 with penalty 1 = 0 + 1
c [ternres-14] 1 schedulable variables 0%
c [ternres-14] 348 ternary resolvents (0 bin, 348 trn)
c [ternres-14] fully completed ternary resolution
c [decomp-35] removed 34 variables
c [simpleprobe-5] 86188 schedulable variables 88%
c [simpleprobe-5] limit 100000000 penalty 1 = 0 + 1
c [decomp-36] removed 1035 variables
c [simpleprobe-5] 70158 variables remain 73% (26317 retained 27%)
c [simpleprobe-5] removed 1035 variables, found 27161 hbrs, 846 units
c [unhide-18] limit 2071322 with penalty 3 = 0 + 3
c [unhide-18-18] 354 units, 76 failed, 4861 tauts, 0 hbrs, 26483 literals
c [transred-14] limit 2226100 based on 2226100 irredundant clauses
c [transred-14] removed 10 transitive binary clauses
c [block-11] scheduling all variables this time
c [block-11] scheduled 95972 variables 100%
c [block-11] limit of 400000000 steps penalty 1 = 0 + 1
c [block-11] fully completed
c [block-11] transition to [ all 0 rem 0 ] state
c [block-11] eliminated 47908 blocked clauses
c [elim-15] 4704 variables 5% will be scheduled this time
c [elim-15] scheduled 4704 variables 5%
c [elim-15] limit of 400000000 steps penalty 1 = 0 + 1
c [elim-15] rescheduling of touched variables disabled
c [elim-15] incomplete 1332 not tried 1% in round 1
c [elim-15] transition to [ all 0 rem 1 ] state
c [elim-15] eliminated 0 = 0% variables out of 4704 scheduled
c [bca-14] limit of 10000000 steps and 4546866 added (scaled 2)
c [bca-14] 149556 out of 191378 literals actually usable 78%
c [bca-14] added 648 blocked clauses in 587348 steps
c [sweep-10] limit 6213967 penalty 2 = 1 + 1
c [sweep-10-1] 2837 pos 3.0% + 91161 neg 97.0% = 93998 sched 98.2% ret 1690
c [sweep-10-1] 6241827 steps 36 queries 12642.25 avg class size
c [sweep-10-1] 1671 decisions 35 SAT calls 216.06 avg env size
c [sweep-10-1] 93622 variables remain 98% (2066 retained 2%)
c [decomp-37] removed 20 variables
c [sweep-10-1] removed 20 vars (0 failed, 0 eqs, 2 impls)
c [sweep-10] 20 < 1/1000 * 95688 = 95 considered unsuccessful
c [sweep-10] removed 20 vars in TOTAL (1 rounds, 35 queries)
c [sort-queue-18] sorted 34172 enqueued variables after 314485 conflicts
c [score-dist-18] active 61496 (64%), one 0 (0%), zero 34172 (36%)
c [score-dist-18] max exp 520, different 18 (3%)
c [score-dist-18] median active exp 519, avg 518.9
c [simplification-18] removed 1876 variables 1.9% (95668 remain 31%)
c [simplification-18] removed 81758 irredundant clauses 3.6% (2169426 remain 36%)
c [simplification-18] maximum reduction of 4% = max (2%, 4%)
c [simplification-18] geometric conflict interval increment 16249 = 81246 / 5
c [simplification-18] new conflict interval 97495
c [simplification-18] penalized conflict interval 97495 = 1 * 97495
c [simplification-18] hard conflict limit 460727 (soft 411980 + delta 48747)
c [simplification-18] new conflict limit 411980 (hard 460727)
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 -  831.2   95668  2169414    332202   31977  69257 171854   39  1204  123   3%    928  798   39   24  166%
c -  869.0   95668  2169414    372374   31946  69519 171976   41  1054  123   4%    972  327   44   30  148%
c -  892.7   95668  2169414    415635   35023  69671 172060   35   522  124   7%    997 -188   36   31  115%
c -  902.1   95668  2169414    458362   38426  69756 172095   21    45  125  48%   1010 -405   20   27   76%
c 
c [simplification-19] limit 411980 conflicts (hard 460727) hit after 460728 conflicts
c [quatres-15] found 33292 quaternary clauses 23% in total
c [quatres-15-1] removed 1 duplicate quaternary clauses
c [quatres-15-2] added 13 single-self-subsuming ternary resolvents
c [quatres-15-2] added 75 quaternary resolvents
c [ternres-15] limit 50597205 with penalty 1 = 0 + 1
c [ternres-15] all 95668 free variables schedulable
c [ternres-15] 3911 ternary resolvents (2 bin, 3909 trn)
c [ternres-15] 381 variables remain 0% (95287 retained 100%)
c [gauss-5] limit 1084654 based on 2169309 irredundant clauses
c [gauss-5] extracted 1 xors of average arity 2.0
c [gauss-5] connected 2 occurrences of 2 variables (average 1.0)
c [gauss-5] limit 1084654 based on 2169309 irredundant clauses
c [gauss-5] fully completed
c [gauss-5] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-38] removed 5 variables
c [unhide-19] limit 2500000 with penalty 3 = 0 + 3
c [unhide-19-19] 20 units, 60 failed, 10365 tauts, 0 hbrs, 13691 literals
c [transred-15] limit 2159062 based on 2159062 irredundant clauses
c [transred-15] removed 10 transitive binary clauses
c [block-12] scheduling all variables this time
c [block-12] scheduled 95504 variables 100%
c [block-12] limit of 400000000 steps penalty 1 = 0 + 1
c [block-12] fully completed
c [block-12] transition to [ all 0 rem 0 ] state
c [block-12] eliminated 2788 blocked clauses
c [block-12] 2788 < 1/100 * 2159058 = 21590 considered unsuccessful
c [cce-5] limit of 15811626 steps penalty 5 = 4 + 1
c [cce-5-1] incomplete large round (ACCE)
c [cce-5-1] allowing another 7905953 steps for small clauses
c [cce-5-1] scheduling 2016919 clauses = 1944564 binary + 72355 ternary
c [cce-5-1] tried to eliminate 52 small clauses 0%
c [cce-5-1] eliminated 5 binary clauses 0%
c [cce-5-1] eliminated 5 small clauses 0%
c [cce-5-1] eliminated 5 small clauses in 15811794 steps
c [cce-5-1] incomplete small round (ACCE)
c [cce-5-1] eliminated 5 covered clauses in round 1
c [cce-5] eliminated 5 covered clauses in TOTAL during 1 rounds
c [cce-5] 5 < 1/100 * 2153300 = 21533 considered unsuccessful
c [bca-15] limit of 10000000 steps and 4514752 added (scaled 2)
c [bca-15] 145252 out of 190932 literals actually usable 76%
c [bca-15] added 5259 blocked clauses in 562931 steps
c [sort-queue-19] sorted 22797 enqueued variables after 460728 conflicts
c [score-dist-19] active 72668 (76%), one 0 (0%), zero 22797 (24%)
c [score-dist-19] max exp 520, different 18 (3%)
c [score-dist-19] median active exp 520, avg 519.7
c [simplification-19] removed 203 variables 0.2% (95465 remain 31%)
c [simplification-19] removed 16119 irredundant clauses 0.7% (2153295 remain 35%)
c [simplification-19] maximum reduction of 1% = max (0%, 1%)
c [simplification-19] geometric conflict interval increment 48747 = 97495 / 2
c [simplification-19] new conflict interval 146242
c [simplification-19] penalized conflict interval 146242 = 1 * 146242
c [simplification-19] hard conflict limit 680091 (soft 606970 + delta 73121)
c [simplification-19] new conflict limit 606970 (hard 680091)
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 -  921.5   95465  2153295    497003   39075  71819 174847   25   291  123   8%   1016    3   36   25  142%
c -  933.4   95465  2153295    536764   38885  71843 174870   17    32  124  51%   1020 -161   14   22   64%
c -  945.2   95465  2153295    577681   40458  71884 174896   17    52  124  32%   1022  -78   14   19   72%
c 
c [simplification-20] limit 606970 conflicts (hard 680091) hit after 606975 conflicts
c [quatres-16] found 32801 quaternary clauses 23% in total
c [quatres-16-1] removed 47 duplicate quaternary clauses
c [quatres-16-2] added 18 single-self-subsuming ternary resolvents
c [quatres-16-2] added 17 quaternary resolvents
c [ternres-16] limit 56950986 with penalty 1 = 0 + 1
c [ternres-16] 380 schedulable variables 0%
c [ternres-16] 1854 ternary resolvents (5 bin, 1849 trn)
c [ternres-16] fully completed ternary resolution
c [decomp-39] removed 4 variables
c [treelook-5] limit 1423774 penalty 3 = 2 + 1 boost 1
c [treelook-5] scheduled 93513 literals 49%
c [treelook-5] scheduling used 1423885 steps
c [treelook-5] not fully scheduled
c [treelook-5] limit 1423774 penalty 3 = 2 + 1 boost 1
c [treelook-5] used 7531777 steps
c [treelook-5] 93511 literals remain 49%
c [treelook-5] 54872 variables remain to probed next time 57%
c [treelook-5] removed 0 variables, found 76 hbrs
c [unhide-20] limit 2500000 with penalty 3 = 0 + 3
c [unhide-20-20] 186 units, 75 failed, 6785 tauts, 0 hbrs, 93653 literals
c [transred-16] limit 2151873 based on 2151873 irredundant clauses
c [transred-16] removed 5 transitive binary clauses
c [transred-16] found 1 units
c [elim-16] scheduling all variables this time
c [elim-16] scheduled 94817 variables 100%
c [elim-16] limit of 200000000 steps penalty 2 = 1 + 1
c [elim-16] rescheduling of touched variables disabled
c [elim-16] incomplete 11291 not tried 12% in round 1
c [elim-16] transition to [ all 1 rem 1 ] state
c [elim-16] eliminated 2772 = 3% variables out of 94817 scheduled
c [bca-16] limit of 10000000 steps and 4447647 added (scaled 2)
c [bca-16] 132122 out of 184092 literals actually usable 72%
c [bca-16] added 6157 blocked clauses in 527104 steps
c [sort-queue-20] sorted 20219 enqueued variables after 606975 conflicts
c [score-dist-20] active 71826 (78%), one 0 (0%), zero 20219 (22%)
c [score-dist-20] max exp 521, different 19 (4%)
c [score-dist-20] median active exp 520, avg 520.2
c [simplification-20] removed 3420 variables 3.6% (92045 remain 30%)
c [simplification-20] removed 34867 irredundant clauses 1.6% (2118428 remain 35%)
c [simplification-20] maximum reduction of 4% = max (4%, 2%)
c [simplification-20] geometric conflict interval increment 29248 = 146242 / 5
c [simplification-20] new conflict interval 175490
c [simplification-20] penalized conflict interval 175490 = 1 * 175490
c [simplification-20] hard conflict limit 870210 (soft 782465 + delta 87745)
c [simplification-20] new conflict limit 782465 (hard 870210)
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 -  990.1   92045  2118428    621578   37583  71193 116882   40   869  122   5%   1023  428   37   26  145%
c
c CAUGHT SIGNAL 15 SIGTERM
c
c s UNKNOWN
c bate: 91 basic ate = 56 trn 62% + 35 lrg 38% in 2 updates
c bcas: 16 count, 426740 added (28462 skipped), 15116869 steps
c bkwd: tried 575782 clauses, 1151284 lits, 2.00 lits/clause
c bkwd: checked 3189884801 occs, 5540.09 occs/clause, 2770.72 occs/lit
c bkwd: subsumed 0 binary, 0 ternary, 52 large
c bkwd: strengthened 0 binary, 0 ternary (0% self), 406 large (0% self)
c blkd: 12 bces, 1175796 removed, 165714359 resolutions, 528543449 steps
c blkd: 72759 blocking literals 12%, 12717 pure
c bump: 614407 bumped seen, 66046743 lits 107.5 on average
c card: 5 count, 0 units, 0 am1, 117206537 steps
c card: 0 rescheduled, 0 eliminated, 0 resolved, 438 subsumed
c card: 59 at-most-one constraints found, average size 3.22
c card: 59 at-most-one constraints used 100%, average size 3.22
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: 5 cces, 390 eliminated, 385 ate 99%, 5 abce 1%
c cces: 0 probed, 0 lifted, 0 failed
c cces: 0 cached, 0 rsz, 0 cols 0%, 0 srch, 0 hits 0%
c clls: 1 sat, 0 simp, 0 freeze, 0 melt
c clls: 23744862 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 113 gcs, 0 rescored clauses, 0 rescored vars
c dcps: 40 decompositions, 1315 equivalent 0%
c deco: 152 decision-only clauses 0%, 46% reduction
c decs: 43625109 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 16 elims, 107613 eliminated 35%, 4806 pure 4%
c elms: 19 rounds, 1.2 rounds/bve
c elms: 27373 small 25%, 62717 large 58%
c elms: 35450 tried small, 27373 succeeded 77%, 8077 failed 23%
c elms: 71677 subsumed, 747568 strengthened, 51761 blocked
c elms: 39092650 copies, 68601247 resolutions, 702951 ipos
c elms: 262072902 subchks, 306394435 strchks
c gaus: 5 extractions, 16 extracted, 2.2 size, 3 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 17744252 steps, 8872126 extr 50%, 57 elim 0%
c glue: 25.6 orig avg, 25.6 real avg, 4.6 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 185771 = 56679 simple 31% + 127174 trn 68% + 1918 lrg 1%, 4289 sub 2%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 614407 clauses, 56.3 length
c lrnd: 34576924 lits = 53423394 orig - 18846470 removed 35%
c lrnd: 276149 uips 45%, 221443 flips 36%
c mins: 603999 mins 98%, 1191 bin 0%, 8913 size 1%
c mins: 53928567 poisoned searches, 9165924 hits, 17% hit rate
c mins: 97247957 used twice searches, 9046273 hits, 9% hit rate
c move: moved 1014650, 993179 bin 98%, 21471 trn 2%
c otfs: 16139 driving 28%, 40983 restarting 72%
c otfs: str 57122, 56195 red 98%, 927 irr 2%
c otfs: str 57122, 0 bin 0%, 375 trn 1%, 56747 lrg 99%
c otfs: sub 789, 757 red 96%, 32 irr 4%
c otfs: sub 789, 0 bin 0%, 4 trn 1%, 785 lrg 99%
c phas: 1 computed, 304049 set, 0 pos (0%), 304049 neg (100%)
c prbs: 4 basic, 10929 probed, 584 failed, 52 lifted
c prbs: 5 simple, 460440 probed, 3890 failed, 44 eqs
c prbs: 5 treelook, 13 probed, 0 failed, 0 lifted
c prom: 74691 locked 5% out of 1624225 tried
c prps: 2404056941 props, 54 props/dec
c prps: 98% srch, 2% simp, 0% lkhd
c quat: 16 count, 14117 quat, 8459 self1, 3 self2, 811 dup
c queu: 20 sorted, 43625109 next (108324 steps 0.00)
c queu: 68287019 enq (1803385560 steps 26.41), 66046743 deq 97%
c redc: 7969 clauses 26%, 30770 tried 5%, 83 sat 0%
c redc: 15765 lits 5%, 335666 tried 1%, 83 sat 0%
c redc: 645 times jump level reduced, 91.9 levels on average
c reds: 14 count, 45031.4 conflicts per reduce
c reds: 0 memlim 0%, 14 arith 100%
c reds: 395567 collected 83%, 80896 retired 17%
c rmbd: 90467 removed, 31265 red 35%
c rsts: 14484 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: 20 count, 19 confs 95%, 0 vars 0%
c simp: 0 its 0%, 1 bin 5%, 0 trns 0%
c subl: 614407 count (713106 tried 1.2), 49260 sub out of 609679 (8.1%)
c swps: 10 count, 10 rounds, 290 queries (29.0/round)
c swps: 246 sat calls, 3 unsat (0.4% success rate)
c swps: 11538 decisions 46.9, 106 conflicts 0.4
c swps; 17309.9 avg class size, 644.7 avg environment size
c swps: 2 failed, 95 impls, 43 equivs
c swp0: 94 type 0 queries, 38 unsat (40.4%), 79 sat (84.0%)
c swp1: 196 type 1 queries, 85 unsat (43.4%), 168 sat (85.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: 88479421 calls to obtain time
c tops: 105122 fixed 34%, 6 its, 105073.33 confs/it
c trds: 16 transitive reductions, 103 removed, 59 failed
c trds: 2143 nodes, 17087 edges, 49809447 steps
c trim: 597423 words, 2.3 MB
c trnr: 16 count, 70 bin, 148292 trn, 475162779 steps
c unhd: 20 count, 20 rounds, 156349679 steps
c unhd: 778 non-trivial sccs of average size 2.0
c unhd: 50421 units, 50421 bin, 0 trn, 0 lrg
c unhd: 3299 failed, 3293 stamp, 0 lits, 4 bin, 1 trn, 0 lrg
c unhd: 266492 tauts, 4410 bin 2%, 30934 trn 12%, 58649 lrg 22%
c unhd: 266492 tauts, 172499 stamp 65%, 51868 red 19%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 1213991 str, 50421 bin 4%, 26270 trn 2%, 1137300 lrg 94%, 402377 red 33%
c vars: 92045 remaining 30% and 214050 removed 70% out of 306095
c vars: 105122 fixed 34%, 107613 eliminated 35%, 1315 equivalent 0%
c vsts: 12066750584 visits, 97% srch, 3% simp, 0% lkhd
c vsts: 5.0 search visits per propagation, 18600.8 per conflict
c wchs: 1314767619 pushed, 158901624 enlarged, 173 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all         623796        395567         80896      22691927       5946456        385543
c 
c  0 0         33632   5      1671   0         0   0   9950473  44   1205059  20     24556   6     0.6
c  1 5         10530   2      3013   1      2749   3   2172959  10    546396   9     14028   4     0.2
c  2 6         42169   7     17741   4      8334  10   3399915  15<  1079809  18     41783  11     1.0
c  3 9        108766  17     67209  17     12512  15   3070368  14   1339460  23<    97373  25     3.9
c  4 14       143702  23    110446  28     11379  14   2085748   9    938168  16    106031  28<    4.2
c  5 21       105500  17<    77254  20<    12463  15<   995089   4    430058   7     53595  14     4.3
c  6 30        70165  11     47959  12     11076  14    504385   2    209417   4     23987   6     2.3
c  7 41        48729   8     31713   8      9548  12    277851   1    106361   2     13245   3     1.9
c  8 54        32332   5     20927   5      6476   8    135386   1     52846   1      5990   2     1.8
c  9 69        17575   3     11250   3      3725   5     64984   0     25520   0      2766   1     1.3
c 10 86         9207   1      5530   1      2215   3     29890   0     11804   0      2003   1     1.1
c 11 126        1408   0       812   0       398   0      4474   0      1457   0       164   0     0.3
c 12 230          78   0        42   0        21   0       401   0        97   0        21   0     0.0
c 13 534           3   0         0   0         0   0         4   0         4   0         1   0     0.0
c 
c avg                  4.5           4.8           5.1           1.7           2.6           3.7
c std                  2.2           1.8           2.3           1.9           1.9           1.8
c 
c  238.972  24% elim
c   85.545   9% block
c   46.936   5% probe
c   37.987   4% bump
c   32.018   3% unhide
c   30.340   3% decide
c   18.116   2% quatres
c   13.884   1% sweep
c   12.291   1% bca
c 
c   14.811 < 1% rest (below)
c 
c    7.541   1% cce
c    3.001   0% gauss
c    2.645   0% ternres
c    1.322   0% transred
c    0.303   0% card
c    0.000   0% locs
c    0.000   0% queuesort
c    0.000   0% rescore
c ==================================
c   14.608   1% preprocessing     3%
c  474.840  48% inprocessing     97%
c ==================================
c  489.448  49% simplifying
c  507.007  51% search
c ==================================
c  996.457 100% all
c 
c        630440 conflicts,         632.7 confs/sec
c          3138 ternaries,         200.9 confs/ternary
c          1542 binaries,          408.8 confs/binary
c             6 iterations,     105073.3 confs/iteration
c 
c            14 reductions,          0.0 redus/sec,  45031.4 confs/reduction
c         14484 restarts,           14.5 rests/sec,     43.5 confs/restart
c      43625109 decisions,       43780.2 decis/sec,     69.2 decis/conflict
c    2404056941 propagations,  2412605.6 props/sec,     55.1 props/decision
c 
c 996.5 seconds, 347.7 MB
c
c CAUGHT SIGNAL 15 SIGTERM
c
c launch: done
