c launch: /data/cnf/sc2014/app/partial-10-11-s.cnf.bz2
c host: atom08
c Lingeling SAT Solver
c 
c Version b7ztzu 7b29300825af9bcc1c8b2c5ebcf65fa1cb101cad
c 
c Copyright (C) 2010-2014 Armin Biere JKU Linz Austria.
c All rights reserved.
c 
c released Sun Apr 26 19:26:13 CEST 2015
c compiled Sun Apr 26 19:26:13 CEST 2015
c 
c gcc (Ubuntu 4.8.2-19ubuntu1) 4.8.2
c -Wall -O3 -I../yalsat -I../druplig -DNLGLOG -DNDEBUG -DNCHKSOL
c Linux cluster2 3.13.0-45-generic x86_64
c 
c piping '/data/cnf/sc2014/app/partial-10-11-s.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/partial-10-11-s.cnf.bz2
c no embedded options
c found 'p cnf 189456 850574' header
c read 189456 variables, 850574 clauses, 1937804 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=2
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 182257 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] VMTF (--score=2)
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  182257   835269         0       0      0     0    0     0   35   0%      0    0    0    0    0%
c 
c [simplification-1] limit 0 conflicts (hard 0) hit after 0 conflicts
c [card-1] limit 2000000 penalty 0 = 0 + 0
c [card-1] found 8770 at-most-one constraints of average size 4.8
c [card-1] no at-most-two constraint found
c [card-1] using previous limit 2000000 for elimination
c [card-1] 8770 out of 8770 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 91571 variables
c [simpleprobe-1] all 97885 free variables schedulable
c [simpleprobe-1] boosting simple probing limit by 10
c [simpleprobe-1] limit 20000000 penalty 0 = 0 + 0
c [decomp-2] removed 882 variables
c [simpleprobe-1] fully completed simple probing
c [simpleprobe-1] removed 882 variables, found 10605 hbrs, 7 units
c [unhide-1] limit 100000 with penalty 0 = 0 + 0
c [unhide-1-1] 0 units, 153 failed, 4385 tauts, 0 hbrs, 4446 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 96765 variables 100%
c [elim-1] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-1] rescheduling of touched variables disabled
c [elim-1] incomplete 16051 not tried 17% in round 1
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 36892 = 38% variables out of 96765 scheduled
c [elim-1] considered successful since not run to completion yet
c [phase-count-1] 388178 negative 99.2% of 391439 except 3261 0.8%
c [phase-count-1] 302302 positive 77.2% of 391439 except 89137 22.8%
c [phase-count-1] less non-negative clauses 3261 than limit 39100 (10.0%)
c [phase-count-1] non-pos/non-neg = 89137/3261 = 27.33 >= 2.00 = 200/100
c [lucky-phase-1] forcing lucky phase -1
c [phase-1] phase bias: 0 positive 0%, 59873 negative 100%
c [sort-queue-1] sorted 59873 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 59873 (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 85433 variables 58.8% (59873 remain 33%)
c [simplification-1] removed 443830 irredundant clauses 53.1% (391439 remain 47%)
c [simplification-1] maximum reduction of 59% = max (59%, 53%)
c [simplification-1] large reduction 59% >= 5% limit
c [simplification-1] next conflict interval 1000 = 2000/2
c [simplification-1] penalized conflict interval 1000 = 1 * 1000
c [simplification-1] hard conflict limit 11000 (soft 1000 + delta 10000)
c [simplification-1] new conflict limit 1000 (hard 11000)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i    2.8   59872   391439        14      12      0  6849    0     9   28   1%      0    9    2    0 24941%
c i    2.8   59869   391439        44      39      0  6851    0    10   28   3%      0   10    4    0 23438%
c i    2.9   59857   391439        99      80     10  6854    0    11   28   3%      0   11    4    0 19660%
c i    2.9   59845   391439       160     120     23  6860    0    12   28   3%      0   12    4    0 16914%
c i    2.9   59381   391439       164     122     23  6861    0    12   28   3%      0   12    4    0 16678%
c i    3.0   59368   391439       188     141     26  6862    0    13   28   4%      0   13    5    0 16191%
c i    3.0   59298   391439       253     192     34  6867    1    15   28   4%      0   15    5    0 14674%
c i    3.1   59123   391439       348     276     36  6873    1    20   28   4%      0   20    8    0 13876%
c i    3.2   58838   391439       388     310     38  6876    1    22   28   4%      0   22    9    0 13791%
c i    3.3   58680   391439       506     409     47  6880    2    28   28   9%      0   28   23    0 14770%
c 
c [simplification-2] limit of 10 iterations hit after 10 iterations
c [decomp-3] removed 1364 variables
c [simpleprobe-2] all 58509 free variables schedulable
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [decomp-4] removed 262 variables
c [simpleprobe-2] 39976 variables remain 69% (18271 retained 31%)
c [simpleprobe-2] removed 262 variables, found 2200 hbrs, 105 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 50726 literals 44%
c [treelook-1] scheduling used 301147 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 340797 steps
c [treelook-1] 50718 literals remain 44%
c [treelook-1] 48558 variables remain to probed next time 83%
c [decomp-5] removed 1 variables
c [treelook-1] removed 1 variables, found 2019 hbrs
c [basicprobe-1] limit 3040168 based on 380021 irredundant clauses
c [basicprobe-1-0] 19700 probes remain 36% after last round
c [basicprobe-1-0] 21 units = 21 failed (100%) + 0 lifted (0%)
c [basicprobe-1-0] removed 2952 variables, found 10027 hbrs
c [unhide-2] limit 100000 with penalty 0 = 0 + 0
c [unhide-2-2] 1 units, 188 failed, 3747 tauts, 0 hbrs, 2068 literals
c [elim-2] 15705 variables 29% will be scheduled this time
c [elim-2] scheduled 15705 variables 29%
c [elim-2] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-2] rescheduling of touched variables disabled
c [elim-2-1] no variable eliminated in round 1 in 19985958 steps
c [elim-2] fully completed in 1 rounds
c [elim-2] transition to [ all 0 rem 0 ] state
c [elim-2] eliminated 0 = 0% variables out of 15705 scheduled
c [phase-count-2] 350700 negative 99.1% of 353961 except 3261 0.9%
c [phase-count-2] 273740 positive 77.3% of 353961 except 80221 22.7%
c [phase-count-2] less non-negative clauses 3261 than limit 35300 (10.0%)
c [phase-count-2] non-pos/non-neg = 80221/3261 = 24.60 >= 2.00 = 200/100
c [lucky-phase-2] forcing lucky phase -1
c [phase-2] phase bias: 0 positive 0%, 2601 negative 100%
c [sort-queue-2] sorted 55033 enqueued variables after 506 conflicts
c [score-dist-2] active 0 (0%), one 12881 (23%), zero 42152 (77%)
c [score-dist-2] max exp 1, different 2 (100%)
c [score-dist-2] median active exp 0, avg 0.0
c [simplification-2] removed 3520 variables 6.0% (55033 remain 30%)
c [simplification-2] removed 37478 irredundant clauses 9.6% (353961 remain 42%)
c [simplification-2] maximum reduction of 10% = max (6%, 10%)
c [simplification-2] forced so keeping old conflict interval 0
c [simplification-2] conflict limit remains at 1002 (hard 11000)
c [simplification-2] new iteration interval 100
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i    5.0   55032   353961       525     417     48 15261    2    31   26   8%      0   30   22    0 13890%
c i    5.1   54883   353961       610     490     56 15264    3    34   26   8%      0   33   19    0 10902%
c i    5.1   54755   353961       640     511     59 15269    3    35   26   8%      0   34   18    0 10137%
c i    5.2   54713   353961       715     574     60 15276    3    36   26   8%      0   36   17    0 8755%
c i    5.4   54697   353961       900     727     72 15289    4    45   26   8%      0   45   20    0 7694%
c i    5.4   54497   353961       916     737     74 15291    4    46   26   9%      0   46   24    0 8395%
c i    5.4   54392   353961       917     737     74 15291    4    46   26   9%      0   46   23    0 8362%
c i    5.4   54380   353961       932     748     74 15293    4    46   26   9%      0   46   22    0 7947%
c i    5.5   54348   353961       953     757     78 15300    4    46   26   9%      0   46   21    0 7401%
c i    5.5   54044   353961       960     760     79 15302    4    46   26   9%      0   46   20    0 7223%
c i    5.5   53655   353961      1000     784     87 15307    4    46   26   9%      0   46   18    0 6331%
c 
c [simplification-3] limit 1013 conflicts (hard 11000) hit after 1013 conflicts
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 4447 at-most-one constraints of average size 4.6
c [card-2] no at-most-two constraint found
c [card-2] using previous limit 1000000 for elimination
c [card-2] 4447 out of 4447 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [decomp-6] removed 1513 variables
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] scheduled 54172 literals 51%
c [treelook-2] scheduling used 337950 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] used 303406 steps
c [treelook-2] 54167 literals remain 51%
c [treelook-2] 43082 variables remain to probed next time 81%
c [treelook-2] removed 2 variables, found 1395 hbrs
c [unhide-3] limit 100000 with penalty 0 = 0 + 0
c [unhide-3-3] 1 units, 67 failed, 8412 tauts, 0 hbrs, 1520 literals
c [block-1] scheduling all variables this time
c [block-1] scheduled 53095 variables 100%
c [block-1] boosting limit by 10
c [block-1] limit of 500000000 steps penalty 0 = 0 + 0
c [block-1] fully completed
c [block-1] transition to [ all 0 rem 0 ] state
c [block-1] eliminated 7350 blocked clauses
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 3 clauses out of 56 (5%) of length 10
c [cce-1-1] eliminated 786 clauses out of 1825 (43%) of length 9
c [cce-1-1] eliminated 268 clauses out of 567 (47%) of length 8
c [cce-1-1] eliminated 1757 clauses out of 2239 (78%) of length 7
c [cce-1-1] eliminated 2116 clauses out of 5066 (42%) of length 6
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 4930 large clauses in 30000002 steps
c [cce-1-1] allowing another 15000001 steps for small clauses
c [cce-1-1] scheduling 225576 clauses = 176100 binary + 49476 ternary
c [cce-1-1] tried to eliminate 484 small clauses 0%
c [cce-1-1] eliminated 142 binary clauses 0%
c [cce-1-1] eliminated 9 ternary clauses 0%
c [cce-1-1] eliminated 151 small clauses 0%
c [cce-1-1] eliminated 151 small clauses in 30000003 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 5081 covered clauses in round 1
c [cce-1] eliminated 5081 covered clauses in TOTAL during 1 rounds
c [bca-1] limit of 10000000 steps and 650310 added (scaled 2)
c [bca-1] 97390 out of 106192 literals actually usable 92%
c [bca-1] added 152 blocked clauses in 287208 steps
c [sweep-1] limit 1000000 penalty 0 = 0 + 0
c [sweep-1-1] 2929 pos 5.5% + 50166 neg 94.5% = 53095 sched 100.0% ret 0
c [sweep-1-1] 1651529 steps 20 queries 10631.60 avg class size
c [sweep-1-1] 148 decisions 15 SAT calls 46.47 avg env size
c [sweep-1-1] 52892 variables remain 100% (197 retained 0%)
c [decomp-8] removed 10 variables
c [sweep-1-1] removed 10 vars (0 failed, 4 eqs, 8 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 10 vars in TOTAL (1 rounds, 19 queries)
c [phase-count-3] 323718 negative 99.7% of 324843 except 1125 0.3%
c [phase-count-3] 255770 positive 78.7% of 324843 except 69073 21.3%
c [phase-count-3] less non-negative clauses 1125 than limit 32400 (10.0%)
c [phase-count-3] non-pos/non-neg = 69073/1125 = 61.40 >= 2.00 = 200/100
c [lucky-phase-3] forcing lucky phase -1
c [phase-3] phase bias: 0 positive 0%, 1024 negative 100%
c [sort-queue-3] sorted 53085 enqueued variables after 1013 conflicts
c [score-dist-3] active 0 (0%), one 18066 (34%), zero 35019 (66%)
c [score-dist-3] max exp 1, different 2 (100%)
c [score-dist-3] median active exp 0, avg 0.0
c [simplification-3] removed 556 variables 1.0% (53085 remain 29%)
c [simplification-3] removed 29118 irredundant clauses 8.2% (324843 remain 39%)
c [simplification-3] maximum reduction of 8% = max (1%, 8%)
c [simplification-3] large reduction 8% >= 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 13013 (soft 3013 + delta 10000)
c [simplification-3] new conflict limit 3013 (hard 13013)
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    7.9   53084   324843      1109     878    121 23792    4    54   25   8%      0   53   17    0 5430%
c i    8.0   53053   324843      1228     981    128 23798    5    58   26   8%      1   57   19    0 5404%
c i    8.2   53045   324843      1453    1182    136 23804    7    65   26  10%      1   64   33    0 6698%
c i    8.3   53042   324843      1554    1269    143 23808    7    69   26  10%      1   68   28    1 5448%
c i    8.5   53035   324843      1812    1474    170 23827    8    74   26  10%      1   73   20    1 3537%
c i    8.6   53032   324843      1926    1572    178 23833    8    77   26  10%      1   75   17    1 2946%
c i    8.6   53031   324843      1937    1573    181 23836    8    77   26  10%      1   75   17    1 2842%
c i    8.6   53017   324843      1981    1597    190 23846    8    76   26  10%      1   75   15    1 2474%
c i    8.6   52823   324843      1986    1598    191 23848    8    76   26  10%      1   75   14    1 2430%
c i    8.7   52821   324843      2069    1661    198 23855    8    78   26  10%      1   76   15    1 2417%
c i    8.8   52801   324843      2103    1690    200 23857    8    78   26  10%      1   77   15    1 2353%
c i    8.9   52790   324843      2220    1794    204 23864    8    82   26  10%      1   80   15    1 2340%
c i    8.9   52649   324843      2221    1794    204 23864    8    82   26  10%      1   80   15    1 2330%
c i    8.9   52641   324843      2251    1818    208 23865    8    83   26  10%      1   81   17    1 2569%
c i    9.3   52629   324843      2733    2232    238 23888   10    93   26  11%      2   91   18    1 2156%
c i    9.3   52511   324843      2735    2233    238 23888   10    93   26  11%      2   91   18    1 2144%
c 
c [simplification-4] limit of 188 binary hit after 188 binaries
c [quatres-1] found 18907 quaternary clauses 37% in total
c [ternres-1] boosting ternary resolution limit by 5
c [ternres-1] limit 20000000 with penalty 0 = 0 + 0
c [ternres-1] all 52503 free variables schedulable
c [ternres-1] 2 ternary resolvents (0 bin, 2 trn)
c [ternres-1] fully completed ternary resolution
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 644 xors of average arity 2.2
c [gauss-1] connected 1431 occurrences of 637 variables (average 2.2)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] fully completed
c [gauss-1] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-9] removed 254 variables
c [basicprobe-2] limit 3401537 penalty 0 = 0 + 0
c [basicprobe-2-0] 17655 probes remain 34% after last round
c [basicprobe-2-0] 19 units = 19 failed (100%) + 0 lifted (0%)
c [basicprobe-2-0] removed 490 variables, found 12047 hbrs
c [bate-1] eliminated 6 asymmetric tautologies during probing
c [unhide-4] limit 136061 with penalty 0 = 0 + 0
c [unhide-4-4] 3 units, 133 failed, 1707 tauts, 0 hbrs, 8315 literals
c [transred-1] limit 680307 with penalty 0 = 0 + 0
c [transred-1] removed 57 transitive binary clauses
c [transred-1] found 4 units
c [block-2] scheduling all variables this time
c [block-2] scheduled 51289 variables 100%
c [block-2] limit of 50000000 steps penalty 0 = 0 + 0
c [block-2] fully completed
c [block-2] transition to [ all 0 rem 0 ] state
c [block-2] eliminated 979 blocked clauses
c [block-2] 979 < 1/100 * 318341 = 3183 considered unsuccessful
c [cce-2] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-2-1] eliminated 660 clauses out of 2722 (24%) of length 6
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] eliminated 660 large clauses in 30000006 steps
c [cce-2-1] allowing another 15000003 steps for small clauses
c [cce-2-1] scheduling 218295 clauses = 170255 binary + 48040 ternary
c [cce-2-1] tried to eliminate 520 small clauses 0%
c [cce-2-1] eliminated 134 binary clauses 0%
c [cce-2-1] eliminated 20 ternary clauses 0%
c [cce-2-1] eliminated 154 small clauses 0%
c [cce-2-1] eliminated 154 small clauses in 30000000 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 814 covered clauses in round 1
c [cce-2] eliminated 814 covered clauses in TOTAL during 1 rounds
c [cce-2] 814 < 1/100 * 314294 = 3142 considered unsuccessful
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 51288 variables 100%
c [elim-3] limit of 10000000 steps penalty 1 = 1 + 0
c [elim-3] rescheduling of touched variables disabled
c [elim-3] incomplete 12027 not tried 23% in round 1
c [elim-3] transition to [ all 1 rem 1 ] state
c [elim-3] eliminated 2609 = 5% variables out of 51288 scheduled
c [bca-2] limit of 10000000 steps and 617294 added (scaled 2)
c [bca-2] 88542 out of 97360 literals actually usable 91%
c [bca-2] added 410 blocked clauses in 261448 steps
c [sweep-2] limit 1000000 penalty 0 = 0 + 0
c [sweep-2-1] 2750 pos 5.7% + 45766 neg 94.3% = 48516 sched 99.7% ret 163
c [sweep-2-1] 1042952 steps 16 queries 11324.31 avg class size
c [sweep-2-1] 105 decisions 13 SAT calls 91.46 avg env size
c [sweep-2-1] 48454 variables remain 100% (214 retained 0%)
c [decomp-10] removed 16 variables
c [sweep-2-1] removed 16 vars (0 failed, 4 eqs, 5 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 16 vars in TOTAL (1 rounds, 15 queries)
c [phase-count-4] 307274 negative 99.7% of 308254 except 980 0.3%
c [phase-count-4] 241769 positive 78.4% of 308254 except 66485 21.6%
c [phase-count-4] less non-negative clauses 980 than limit 30800 (10.0%)
c [phase-count-4] non-pos/non-neg = 66485/980 = 67.84 >= 2.00 = 200/100
c [lucky-phase-4] forcing lucky phase -1
c [phase-4] phase bias: 0 positive 0%, 282 negative 100%
c [sort-queue-4] sorted 48663 enqueued variables after 2740 conflicts
c [score-dist-4] active 0 (0%), one 22739 (47%), zero 25924 (53%)
c [score-dist-4] max exp 1, different 2 (100%)
c [score-dist-4] median active exp 0, avg 0.0
c [simplification-4] removed 3840 variables 7.3% (48663 remain 27%)
c [simplification-4] removed 16589 irredundant clauses 5.1% (308254 remain 37%)
c [simplification-4] maximum reduction of 7% = max (7%, 5%)
c [simplification-4] forced so keeping old conflict interval 0
c [simplification-4] conflict limit remains at 3030 (hard 13013)
c [simplification-4] new binary interval 1000
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   12.4   48662   308254      2812    1478    254 32048   10    97   25  10%      2   94   16    1 1959%
c i   12.4   48582   308254      2831    1490    255 32053   10    97   25  10%      2   94   16    1 1872%
c i   12.5   48548   308254      2969    1597    270 32066   10    98   25  10%      2   95   14    1 1643%
c 
c [simplification-5] limit 3030 conflicts (hard 13013) hit after 3031 conflicts
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] all 48545 free variables schedulable
c [ternres-2] 45 ternary resolvents (0 bin, 45 trn)
c [ternres-2] 5815 variables remain 12% (42730 retained 88%)
c [decomp-11] removed 118 variables
c [simpleprobe-3] 33475 schedulable variables 69%
c [simpleprobe-3] limit 2941309 penalty 0 = 0 + 0
c [decomp-12] removed 248 variables
c [simpleprobe-3] 20617 variables remain 43% (27680 retained 57%)
c [simpleprobe-3] removed 248 variables, found 8559 hbrs, 106 units
c [unhide-5] limit 147065 with penalty 0 = 0 + 0
c [unhide-5-5] 0 units, 58 failed, 6440 tauts, 0 hbrs, 2054 literals
c [transred-2] limit 735327 with penalty 0 = 0 + 0
c [transred-2] removed 77 transitive binary clauses
c [transred-2] found 1 units
c [elim-4] 12015 variables 25% will be scheduled this time
c [elim-4] scheduled 12015 variables 25%
c [elim-4] boosting limit by 20
c [elim-4] limit of 400000000 steps penalty 0 = 0 + 0
c [elim-4] rescheduling of touched variables disabled
c [elim-4-1] eliminated 1 variables 0% in round 1 in 15588823 steps
c [elim-4-1] backward subsumption/strengthening limit 15588800
c [elim-4-1-1] backward checking 146 touched variables 0%
c [elim-4-1-1] fully completed backward checking in 1 rounds
c [elim-4-1] subsumed 0 and strengthened 0 clauses in 86784 steps
c [elim-4-1] fully rescheduled 48182 variables 100%
c [elim-4-2] eliminated 418 variables 1% in round 2 in 24833143 steps
c [elim-4-2] backward subsumption/strengthening limit 24833100
c [elim-4-2-1] backward checking 2780 touched variables 6%
c [elim-4-2-1] fully completed backward checking in 1 rounds
c [elim-4-2] subsumed 0 and strengthened 3 clauses in 881742 steps
c [elim-4-2] rescheduled 9 variables 0% by backward subsumption
c [elim-4-3] eliminated 2 variables 0% in round 3 in 11420 steps
c [elim-4-3] backward subsumption/strengthening limit 11400
c [elim-4-3-1] backward checking 12 touched variables 0%
c [elim-4-3-1] incomplete backward checking 0 remain 0%
c [elim-4-3] subsumed 0 and strengthened 3 clauses in 11401 steps
c [elim-4] incomplete 6 not tried 0% in round 3
c [elim-4] transition to [ all 1 rem 1 ] state
c [elim-4] eliminated 424 = 4% variables out of 12015 scheduled
c [elim-4] 424 < 1/100 * 12015 = 120 considered unsuccessful
c [bca-3] limit of 10000000 steps and 598583 added (scaled 2)
c [bca-3] 86530 out of 95520 literals actually usable 91%
c [bca-3] added 47 blocked clauses in 254437 steps
c [sweep-3] limit 1000000 penalty 0 = 0 + 0
c [sweep-3-1] 2713 pos 5.7% + 44862 neg 94.3% = 47575 sched 99.6% ret 184
c [sweep-3-1] 1006819 steps 13 queries 11322.85 avg class size
c [sweep-3-1] 106 decisions 12 SAT calls 48.42 avg env size
c [sweep-3-1] 47410 variables remain 99% (242 retained 1%)
c [decomp-13] removed 112 variables
c [sweep-3-1] removed 112 vars (0 failed, 1 eqs, 1 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 112 vars in TOTAL (1 rounds, 12 queries)
c [phase-count-5] 297230 negative 99.7% of 298136 except 906 0.3%
c [phase-count-5] 233624 positive 78.4% of 298136 except 64512 21.6%
c [phase-count-5] less non-negative clauses 906 than limit 29800 (10.0%)
c [phase-count-5] non-pos/non-neg = 64512/906 = 71.21 >= 2.00 = 200/100
c [lucky-phase-5] forcing lucky phase -1
c [phase-5] phase bias: 0 positive 0%, 282 negative 100%
c [sort-queue-5] sorted 47647 enqueued variables after 3031 conflicts
c [score-dist-5] active 0 (0%), one 22860 (48%), zero 24787 (52%)
c [score-dist-5] max exp 1, different 2 (100%)
c [score-dist-5] median active exp 0, avg 0.0
c [simplification-5] removed 898 variables 1.8% (47647 remain 26%)
c [simplification-5] removed 10118 irredundant clauses 3.3% (298136 remain 36%)
c [simplification-5] maximum reduction of 3% = max (2%, 3%)
c [simplification-5] geometric conflict interval increment 5000 = 20000 / 4
c [simplification-5] new conflict interval 5000
c [simplification-5] penalized conflict interval 5000 = 1 * 5000
c [simplification-5] hard conflict limit 18031 (soft 8031 + delta 10000)
c [simplification-5] new conflict limit 8031 (hard 18031)
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   14.9   47646   298136      3253    1582    310 39429   11   104   25  10%      2  101   23    1 2381%
c i   15.1   47639   298136      3507    1794    326 39446   11   107   25  11%      2  104   20    1 1989%
c i   15.4   47631   298136      3787    2026    340 39466   12   113   25  11%      2  109   25    1 2191%
c i   15.6   47589   298136      4169    2351    366 39493   12   114   25  11%      2  109   15    1 1225%
c i   15.7   47506   298136      4380    2514    386 39508   14   117   25  12%      2  112   33    1 2544%
c i   15.7   47500   298136      4390    2521    387 39509   14   117   25  12%      2  112   32    1 2462%
c i   15.8   47491   298136      4402    2531    388 39509   14   117   25  12%      2  112   32    1 2437%
c i   15.9   47484   298136      4574    2669    403 39522   15   126   26  12%      2  121   33    1 2326%
c i   16.1   47476   298136      4768    2834    417 39534   15   130   26  12%      2  125   29    1 1931%
c i   16.1   47392   298136      4847    2899    423 39539   15   129   26  12%      2  123   24    1 1579%
c i   16.2   47391   298136      4925    2957    433 39547   15   129   26  11%      2  123   20    2 1352%
c i   16.3   47381   298136      5098    3101    446 39560   15   133   26  11%      2  127   19    2 1245%
c i   16.4   47371   298136      5251    3224    457 39576   15   135   26  11%      2  129   20    2 1256%
c i   16.6   47370   298136      5409    3347    466 39600   15   138   26  11%      2  131   19    2 1142%
c i   16.7   47360   298136      5537    3467    468 39603   16   142   26  12%      1  135   32    2 1858%
c i   16.8   47338   298136      5660    3575    470 39613   17   145   26  12%      1  137   33    2 1863%
c i   17.0   47337   298136      5909    3790    484 39630   18   153   27  12%      1  145   36    2 1871%
c i   17.1   47149   298136      5985    3855    487 39633   19   155   27  12%      1  147   37    2 1906%
c i   17.2   47141   298136      6088    3947    492 39636   19   157   27  12%      1  149   31    2 1565%
c i   17.2   47136   298136      6096    3953    492 39637   18   158   27  12%      1  149   30    2 1532%
c i   17.5   47127   298136      6329    4155    503 39651   19   164   27  12%      1  155   29    2 1407%
c i   17.5   47126   298136      6336    4160    503 39652   19   163   27  12%      1  154   29    2 1373%
c i   17.6   47125   298136      6442    4250    513 39656   19   166   27  12%      1  157   32    2 1495%
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   17.6   47124   298136      6455    4260    513 39657   19   166   27  12%      1  157   31    2 1464%
c i   17.7   47003   298136      6552    4343    517 39664   20   169   27  12%      1  160   33    2 1511%
c i   17.8   46993   298136      6630    4411    519 39669   20   171   27  12%      1  161   32    2 1444%
c i   17.8   46978   298136      6661    4436    520 39673   20   171   27  12%      1  161   32    2 1420%
c i   18.0   46977   298136      6775    4538    528 39675   21   176   27  12%      1  166   34    2 1457%
c i   18.1   46976   298136      6918    4657    539 39685   21   176   27  12%      1  166   29    2 1241%
c i   18.2   46918   298136      6986    4713    542 39692   21   176   27  12%      1  166   28    2 1180%
c i   18.2   46879   298136      7058    4778    546 39694   21   176   27  12%      1  165   27    2 1134%
c i   18.3   46872   298136      7082    4795    548 39698   21   177   27  12%      1  166   27    2 1125%
c i   18.7   46803   298136      7569    5230    571 39711   22   184   27  12%      2  172   29    3 1117%
c i   19.0   46793   298136      7798    5436    577 39715   26   195   28  13%      2  182   76    3 2572%
c i   19.1   46782   298136      7880    5511    582 39716   26   197   28  13%      2  184   61    3 2054%
c 
c [simplification-6] limit 8034 conflicts (hard 18031) hit after 8034 conflicts
c [quatres-2] found 17841 quaternary clauses 40% in total
c [ternres-3] limit 4000000 with penalty 0 = 0 + 0
c [ternres-3] 5600 schedulable variables 12%
c [ternres-3] 56 ternary resolvents (0 bin, 56 trn)
c [ternres-3] fully completed ternary resolution
c [card-3] limit 500000 penalty 2 = 2 + 0
c [card-3] found 2509 at-most-one constraints of average size 4.3
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 500000 for elimination
c [card-3] 2509 out of 2509 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] extracted 49 xors of average arity 2.7
c [gauss-2] connected 130 occurrences of 100 variables (average 1.3)
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] fully completed
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-14] removed 29 variables
c [treelook-3] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-3] scheduled 48266 literals 52%
c [treelook-3] scheduling used 318285 steps
c [treelook-3] not fully scheduled
c [treelook-3] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-3] used 340499 steps
c [treelook-3] 48202 literals remain 52%
c [treelook-3] 36513 variables remain to probed next time 78%
c [decomp-15] removed 3 variables
c [treelook-3] removed 38 variables, found 1731 hbrs
c [unhide-6] limit 384499 with penalty 0 = 0 + 0
c [unhide-6-6] 3 units, 123 failed, 3149 tauts, 0 hbrs, 23212 literals
c [transred-3] limit 1922498 with penalty 0 = 0 + 0
c [transred-3] removed 201 transitive binary clauses
c [transred-3] found 4 units
c [block-3] scheduling all variables this time
c [block-3] scheduled 46515 variables 100%
c [block-3] limit of 25000000 steps penalty 1 = 1 + 0
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 5 blocked clauses
c [block-3] 5 < 1/100 * 292052 = 2920 considered unsuccessful
c [cce-3] limit of 15000000 steps penalty 1 = 1 + 0
c [cce-3-1] eliminated 7 clauses out of 705 (1%) of length 9
c [cce-3-1] eliminated 3 clauses out of 320 (1%) of length 8
c [cce-3-1] eliminated 30 clauses out of 555 (5%) of length 7
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 40 large clauses in 15000001 steps
c [cce-3-1] allowing another 7500000 steps for small clauses
c [cce-3-1] scheduling 201470 clauses = 154940 binary + 46530 ternary
c [cce-3-1] tried to eliminate 480 small clauses 0%
c [cce-3-1] eliminated 180 binary clauses 0%
c [cce-3-1] eliminated 5 ternary clauses 0%
c [cce-3-1] eliminated 185 small clauses 0%
c [cce-3-1] eliminated 185 small clauses in 15000004 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 225 covered clauses in round 1
c [cce-3] eliminated 225 covered clauses in TOTAL during 1 rounds
c [cce-3] 225 < 1/100 * 290635 = 2906 considered unsuccessful
c [bca-4] limit of 10000000 steps and 581624 added (scaled 2)
c [bca-4] 75700 out of 93030 literals actually usable 81%
c [bca-4] added 79 blocked clauses in 209465 steps
c [sweep-4] limit 1000000 penalty 0 = 0 + 0
c [sweep-4-1] 2765 pos 6.0% + 43519 neg 94.0% = 46284 sched 99.5% ret 230
c [sweep-4-1] 1046002 steps 16 queries 9616.69 avg class size
c [sweep-4-1] 191 decisions 11 SAT calls 150.82 avg env size
c [sweep-4-1] 46205 variables remain 99% (309 retained 1%)
c [decomp-16] removed 6 variables
c [sweep-4-1] removed 6 vars (0 failed, 4 eqs, 11 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 6 vars in TOTAL (1 rounds, 15 queries)
c [phase-count-6] 289507 negative 99.7% of 290408 except 901 0.3%
c [phase-count-6] 228690 positive 78.7% of 290408 except 61718 21.3%
c [phase-count-6] less non-negative clauses 901 than limit 29000 (10.0%)
c [phase-count-6] non-pos/non-neg = 61718/901 = 68.50 >= 2.00 = 200/100
c [lucky-phase-6] forcing lucky phase -1
c [phase-6] phase bias: 0 positive 0%, 17 negative 100%
c [sort-queue-6] sorted 46508 enqueued variables after 8034 conflicts
c [score-dist-6] active 0 (0%), one 28270 (61%), zero 18238 (39%)
c [score-dist-6] max exp 1, different 2 (100%)
c [score-dist-6] median active exp 0, avg 0.0
c [simplification-6] removed 266 variables 0.6% (46508 remain 26%)
c [simplification-6] removed 7728 irredundant clauses 2.6% (290408 remain 35%)
c [simplification-6] maximum reduction of 3% = max (1%, 3%)
c [simplification-6] geometric conflict interval increment 5000 = 20000 / 4
c [simplification-6] new conflict interval 10000
c [simplification-6] penalized conflict interval 10000 = 1 * 10000
c [simplification-6] hard conflict limit 28034 (soft 18034 + delta 10000)
c [simplification-6] new conflict limit 18034 (hard 28034)
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   21.7   46507   290408      8357    5896    624 37941   28   205   29  13%      3  191   37    3 1151%
c i   21.7   46506   290408      8448    5981    625 37943   28   204   29  14%      2  190   36    3 1092%
c i   21.9   46505   290408      8592    6115    628 37947   29   209   29  14%      2  194   44    3 1306%
c i   21.9   46142   290408      8595    6117    628 37947   29   209   29  14%      2  194   45    3 1317%
c i   22.7   45932   290408      9401    6817    655 37987   33   230   29  14%      5  213   69    4 1718%
c i   22.8   45926   290408      9417    6831    655 37987   33   230   29  14%      5  212   65    4 1627%
c i   22.8   45869   290408      9496    6895    663 37993   33   230   29  14%      4  212   51    4 1276%
c i   23.1   45828   290408      9744    7111    675 38003   33   236   29  14%      4  217   49    4 1181%
c i   23.7   45827   290408     10147    7463    686 38031   36   248   30  15%      4  228   64    5 1401%
c i   23.7   45821   290408     10160    7471    687 38034   36   249   30  15%      3  229   63    5 1377%
c i   23.8   45785   290408     10319    7611    695 38043   37   250   30  15%      3  229   56    5 1216%
c i   26.6   45784   290408     13092   10093    785 38150   42   274   33  15%     28  244   43    6  670%
c i   26.7   45779   290408     13127   10124    786 38152   42   274   33  15%     27  244   42    6  654%
c i   27.4   45778   290408     13820   10756    808 38180   40   275   34  15%     16  241   36    7  536%
c i   27.5   45651   290408     13854   10783    812 38182   40   273   34  15%     15  240   33    7  492%
c i   27.6   45650   290408     13975   10874    824 38190   39   272   34  14%     14  238   28    7  422%
c i   28.5   45649   290408     14940   11748    863 38216   41   269   35  15%     10  231   34    7  471%
c i   28.7   45644   290408     15175   11964    873 38219   41   272   35  15%      8  234   39    7  524%
c i   28.7   45643   290408     15178   11966    873 38219   41   272   35  15%      8  234   39    7  523%
c i   29.0   45637   290408     15389   12151    884 38226   42   274   35  15%      7  235   49    8  644%
c i   29.1   45631   290408     15504   12258    884 38228   43   275   36  16%      6  235   63    8  818%
c i   29.4   45630   290408     15674   12408    887 38234   45   282   36  16%      5  242   81    8 1024%
c i   29.7   45626   290408     15951   12643    900 38256   44   280   37  16%      4  239   44    8  548%
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   30.1   45625   290408     16393   13016    925 38283   44   274   37  16%      3  231   42    8  510%
c i   30.2   45555   290408     16448   13057    929 38291   44   272   37  16%      3  230   41    8  499%
c i   31.1   45551   290408     17262   13791    959 38319   46   286   37  16%      5  240   63    9  710%
c i   31.5   45550   290408     17559   14051    972 38329   48   291   37  17%      4  244   69    9  746%
c i   31.9   45478   290408     17878   14349    979 38335   49   296   38  17%      3  248   61    9  649%
c i   32.1   45477   290408     18026   14475    985 38349   49   296   38  16%      3  247   54    9  563%
c 
c [simplification-7] limit 18040 conflicts (hard 28034) hit after 18040 conflicts
c [ternres-4] limit 4454894 with penalty 0 = 0 + 0
c [ternres-4] all 45477 free variables schedulable
c [ternres-4] 68 ternary resolvents (0 bin, 68 trn)
c [ternres-4] fully completed ternary resolution
c [decomp-17] removed 1410 variables
c [basicprobe-3] limit 22274472 penalty 0 = 0 + 0
c [basicprobe-3-0] 13377 probes remain 30% after last round
c [basicprobe-3-0] 129 units = 127 failed (98%) + 2 lifted (2%)
c [basicprobe-3-0] removed 957 variables, found 86912 hbrs
c [bate-2] eliminated 44 asymmetric tautologies during probing
c [unhide-7] limit 890978 with penalty 0 = 0 + 0
c [unhide-7-7] 4 units, 233 failed, 5251 tauts, 0 hbrs, 103948 literals
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 202 transitive binary clauses
c [transred-4] found 6 units
c [elim-5] no untried remaining variables left
c [elim-5] scheduled 43831 variables 100%
c [elim-5] limit of 44548945 steps penalty 1 = 1 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5-1] eliminated 2291 variables 5% in round 1 in 23370300 steps
c [elim-5-1] backward subsumption/strengthening limit 21178645
c [elim-5-1-1] backward checking 7180 touched variables 16%
c [elim-5-1-1] fully completed backward checking in 1 rounds
c [elim-5-1] subsumed 3 and strengthened 12 clauses in 2259745 steps
c [elim-5-1] rescheduled 35 variables 0% by backward subsumption
c [elim-5-2] eliminated 6 variables 0% in round 2 in 37831 steps
c [elim-5-2] backward subsumption/strengthening limit 37800
c [elim-5-2-1] backward checking 45 touched variables 0%
c [elim-5-2-1] incomplete backward checking 50 remain 111%
c [elim-5-2] subsumed 4 and strengthened 8 clauses in 37814 steps
c [elim-5-2] rescheduled 10 variables 0% by backward subsumption
c [elim-5-3] eliminated 2 variables 0% in round 3 in 177759 steps
c [elim-5-3] backward subsumption/strengthening limit 177700
c [elim-5-3-1] backward checking 53 touched variables 0%
c [elim-5-3-1] fully completed backward checking in 1 rounds
c [elim-5-3] subsumed 5 and strengthened 8 clauses in 97160 steps
c [elim-5] incomplete 10 not tried 0% in round 3
c [elim-5] transition to [ all 1 rem 1 ] state
c [elim-5] eliminated 2303 = 5% variables out of 43831 scheduled
c [bca-5] limit of 10000000 steps and 534608 added (scaled 2)
c [bca-5] 63706 out of 83058 literals actually usable 77%
c [bca-5] added 190 blocked clauses in 172104 steps
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 13364680 penalty 0 = 0 + 0
c [sweep-5-1] 2995 pos 7.3% + 38276 neg 92.7% = 41271 sched 99.4% ret 257
c [sweep-5-1] 13368542 steps 216 queries 1030.42 avg class size
c [sweep-5-1] 3330 decisions 196 SAT calls 205.88 avg env size
c [sweep-5-1] 29560 variables remain 71% (11925 retained 29%)
c [decomp-18] removed 102 variables
c [sweep-5-1] removed 102 vars (0 failed, 21 eqs, 46 impls)
c [sweep-5] considered successful since not run to completion yet
c [sweep-5] removed 102 vars in TOTAL (1 rounds, 215 queries)
c [phase-count-7] 265706 negative 99.7% of 266394 except 688 0.3%
c [phase-count-7] 209240 positive 78.5% of 266394 except 57154 21.5%
c [phase-count-7] less non-negative clauses 688 than limit 26600 (10.0%)
c [phase-count-7] non-pos/non-neg = 57154/688 = 83.07 >= 2.00 = 200/100
c [lucky-phase-7] forcing lucky phase -1
c [phase-7] phase bias: 0 positive 0%, 10 negative 100%
c [sort-queue-7] sorted 41426 enqueued variables after 18040 conflicts
c [score-dist-7] active 0 (0%), one 29299 (71%), zero 12127 (29%)
c [score-dist-7] max exp 1, different 2 (100%)
c [score-dist-7] median active exp 0, avg 0.0
c [simplification-7] removed 4051 variables 8.9% (41426 remain 23%)
c [simplification-7] removed 24014 irredundant clauses 8.3% (266394 remain 32%)
c [simplification-7] maximum reduction of 9% = max (9%, 8%)
c [simplification-7] large reduction 9% >= 5% limit
c [simplification-7] next conflict interval 2000 = 2000/1
c [simplification-7] penalized conflict interval 2000 = 1 * 2000
c [simplification-7] hard conflict limit 30040 (soft 20040 + delta 10000)
c [simplification-7] new conflict limit 20040 (hard 30040)
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   37.2   41425   266394     18885   11301   1015 130186   49   288   36  17%      5  236   55   10  549%
c i   38.2   41424   266394     19773   12107   1048 130215   49   285   36  17%      6  231   45   11  428%
c 
c [simplification-8] limit 20040 conflicts (hard 30040) hit after 20040 conflicts
c [ternres-5] limit 4926912 with penalty 0 = 0 + 0
c [ternres-5] all 41424 free variables schedulable
c [ternres-5] 62 ternary resolvents (0 bin, 62 trn)
c [ternres-5] 2095 variables remain 5% (39329 retained 95%)
c [decomp-19] removed 2 variables
c [simpleprobe-4] 18156 schedulable variables 44%
c [simpleprobe-4] limit 19707650 penalty 0 = 0 + 0
c [decomp-20] removed 783 variables
c [simpleprobe-4] fully completed simple probing
c [simpleprobe-4] removed 783 variables, found 26459 hbrs, 338 units
c [unhide-8] limit 985382 with penalty 0 = 0 + 0
c [unhide-8-8] 3 units, 106 failed, 16053 tauts, 0 hbrs, 35186 literals
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 256 transitive binary clauses
c [transred-5] found 7 units
c [elim-6] no untried remaining variables left
c [elim-6] scheduled 40544 variables 100%
c [elim-6] limit of 98538254 steps penalty 0 = 0 + 0
c [elim-6] rescheduling of touched variables disabled
c [elim-6-1] eliminated 338 variables 1% in round 1 in 23085427 steps
c [elim-6-1] backward subsumption/strengthening limit 23085400
c [elim-6-1-1] backward checking 1823 touched variables 4%
c [elim-6-1-1] fully completed backward checking in 1 rounds
c [elim-6-1] subsumed 6 and strengthened 25 clauses in 719065 steps
c [elim-6-1] rescheduled 57 variables 0% by backward subsumption
c [elim-6-2] eliminated 7 variables 0% in round 2 in 95411 steps
c [elim-6-2] backward subsumption/strengthening limit 95400
c [elim-6-2-1] backward checking 63 touched variables 0%
c [elim-6-2-1] fully completed backward checking in 1 rounds
c [elim-6-2] subsumed 0 and strengthened 2 clauses in 65528 steps
c [elim-6-2] rescheduled 5 variables 0% by backward subsumption
c [elim-6-3] eliminated 1 variables 0% in round 3 in 1808 steps
c [elim-6-3] backward subsumption/strengthening limit 1800
c [elim-6-3-1] backward checking 10 touched variables 0%
c [elim-6-3-1] incomplete backward checking 6 remain 60%
c [elim-6-3] subsumed 0 and strengthened 0 clauses in 1835 steps
c [elim-6] fully completed in 3 rounds
c [elim-6] transition to [ all 0 rem 0 ] state
c [elim-6] eliminated 346 = 1% variables out of 40544 scheduled
c [elim-6] 346 < 1/100 * 40544 = 405 considered unsuccessful
c [bca-6] limit of 10000000 steps and 517101 added (scaled 2)
c [bca-6] 60875 out of 80398 literals actually usable 76%
c [bca-6] added 72 blocked clauses in 166975 steps
c [sweep-6] limit 1478073 penalty 0 = 0 + 0
c [sweep-6-1] 2253 pos 7.7% + 26871 neg 92.3% = 29124 sched 72.5% ret 11074
c [sweep-6-1] 1539679 steps 38 queries 4351.84 avg class size
c [sweep-6-1] 317 decisions 32 SAT calls 110.00 avg env size
c [sweep-6-1] 28844 variables remain 72% (11354 retained 28%)
c [decomp-21] removed 5 variables
c [sweep-6-1] removed 5 vars (0 failed, 5 eqs, 7 impls)
c [sweep-6] considered successful since not run to completion yet
c [sweep-6] removed 5 vars in TOTAL (1 rounds, 37 queries)
c [phase-count-8] 257466 negative 99.8% of 258072 except 606 0.2%
c [phase-count-8] 201393 positive 78.0% of 258072 except 56679 22.0%
c [phase-count-8] less non-negative clauses 606 than limit 25800 (10.0%)
c [phase-count-8] non-pos/non-neg = 56679/606 = 93.53 >= 2.00 = 200/100
c [lucky-phase-8] forcing lucky phase -1
c [phase-8] phase bias: 0 positive 0%, 10 negative 100%
c [sort-queue-8] sorted 40193 enqueued variables after 20040 conflicts
c [score-dist-8] active 0 (0%), one 29243 (73%), zero 10950 (27%)
c [score-dist-8] max exp 1, different 2 (100%)
c [score-dist-8] median active exp 0, avg 0.0
c [simplification-8] removed 1231 variables 3.0% (40193 remain 22%)
c [simplification-8] removed 8322 irredundant clauses 3.1% (258072 remain 31%)
c [simplification-8] maximum reduction of 3% = max (3%, 3%)
c [simplification-8] geometric conflict interval increment 5000 = 20000 / 4
c [simplification-8] new conflict interval 15000
c [simplification-8] penalized conflict interval 15000 = 1 * 15000
c [simplification-8] hard conflict limit 45040 (soft 35040 + delta 10000)
c [simplification-8] new conflict limit 35040 (hard 45040)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   41.3   40192   258072     20140   11115   1074 136208   48   285   34  17%      4  229   36   11  341%
c i   41.4   40191   258072     20211   11172   1083 136212   47   282   34  17%      4  226   31   11  288%
c i   41.5   40138   258072     20328   11274   1090 136216   47   282   35  17%      4  225   31   11  291%
c i   41.6   40033   258072     20452   11379   1100 136224   46   281   35  16%      3  224   27   11  251%
c i   42.1   40032   258072     20870   11753   1115 136244   45   283   35  16%      3  224   36   11  331%
c i   42.7   40031   258072     21407   12221   1136 136270   49   293   35  17%      3  233   64   11  562%
c i   42.9   39953   258072     21683   12474   1142 136282   49   294   35  17%      2  232   44   12  379%
c i   43.1   39936   258072     21837   12605   1155 136289   48   291   35  16%      2  229   36   12  313%
c i   43.8   39935   258072     22548   13254   1180 136315   47   292   35  16%      3  227   47   12  396%
c i   44.7   39934   258072     23470   14072   1219 136344   49   288   35  17%      5  221   63   13  503%
c i   46.1   39933   258072     24726   15226   1258 136378   49   299   35  16%      9  227   45   13  341%
c i   46.5   39727   258072     25127   15581   1273 136400   48   298   37  16%      6  225   37   13  278%
c i   46.6   39722   258072     25168   15617   1277 136400   48   297   37  16%      6  224   35   13  260%
c i   46.8   39714   258072     25426   15841   1289 136403   48   297   37  16%      5  223   41   14  305%
c i   47.0   39713   258072     25587   15992   1293 136406   48   295   37  16%      4  221   45   14  329%
c i   47.8   39712   258072     26298   16633   1317 136433   49   305   39  16%      4  228   67   14  472%
c i   48.9   39589   258072     27267   17526   1339 136458   51   309   41  16%      6  228   43   15  293%
c i   49.0   39533   258072     27355   17593   1351 136466   50   308   42  16%      5  227   33   15  225%
c i   49.9   39475   258072     28257   18401   1381 136493   50   292   42  17%      6  208   47   15  309%
c i   49.9   39472   258072     28329   18467   1383 136496   50   293   42  17%      5  209   45   15  297%
c i   50.1   39471   258072     28439   18560   1387 136500   50   291   42  17%      5  207   47   15  310%
c i   50.2   39470   258072     28588   18696   1390 136505   50   292   42  17%      4  207   53   15  346%
c i   50.5   39469   258072     28823   18909   1398 136514   51   292   42  17%      3  207   53   16  341%
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   50.6   39426   258072     28921   18989   1403 136524   50   290   42  17%      3  204   44   16  282%
c i   51.8   39423   258072     30003   19977   1424 136562   50   298   44  17%      6  208   41   16  253%
c i   51.9   39422   258072     30047   20008   1430 136563   50   297   44  17%      6  208   36   16  225%
c i   52.3   39331   258072     30411   20337   1439 136573   53   303   44  18%      4  212   95   17  575%
c i   52.5   39330   258072     30656   20555   1443 136583   53   301   44  18%      3  209   65   17  387%
c i   53.1   39329   258072     31165   21012   1466 136603   50   293   45  17%      3  200   30   17  179%
c i   53.2   39328   258072     31313   21122   1481 136612   49   292   45  17%      2  199   30   17  178%
c i   53.4   38991   258072     31530   21318   1481 136619   50   289   45  17%      2  195   52   17  309%
c i   53.5   38874   258072     31579   21362   1484 136620   50   291   45  17%      2  196   52   17  307%
c i   53.6   38873   258072     31694   21462   1490 136627   50   291   45  17%      1  196   48   17  280%
c i   56.7   38826   258072     34392   23941   1544 136699   54   304   60  18%     25  201   57   19  308%
c i   56.9   38822   258072     34535   24079   1545 136702   54   306   60  18%     21  203   58   19  310%
c i   57.4   38821   258072     35006   24512   1553 136720   53   300   60  18%     14  195   45   19  238%
c 
c [simplification-9] limit 35040 conflicts (hard 45040) hit after 35040 conflicts
c [quatres-3] found 15160 quaternary clauses 41% in total
c [quatres-3-2] added 4 quaternary resolvents
c [ternres-6] limit 8631022 with penalty 0 = 0 + 0
c [ternres-6] 1954 schedulable variables 5%
c [ternres-6] 110 ternary resolvents (0 bin, 110 trn)
c [ternres-6] fully completed ternary resolution
c [gauss-3] limit 500000 penalty 2 = 2 + 0
c [gauss-3] extracted 452 xors of average arity 2.0
c [gauss-3] connected 920 occurrences of 365 variables (average 2.5)
c [gauss-3] limit 500000 penalty 2 = 2 + 0
c [gauss-3] fully completed
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-22] removed 604 variables
c [treelook-4] limit 863102 penalty 0 = 0 + 0 boost 1
c [treelook-4] scheduled 69114 literals 90%
c [treelook-4] scheduling used 863205 steps
c [treelook-4] not fully scheduled
c [treelook-4] limit 863102 penalty 0 = 0 + 0 boost 1
c [treelook-4] used 965098 steps
c [treelook-4] 69091 literals remain 90%
c [treelook-4] 28809 variables remain to probed next time 75%
c [decomp-23] removed 1 variables
c [treelook-4] removed 4 variables, found 3751 hbrs
c [unhide-9] limit 1726204 with penalty 0 = 0 + 0
c [unhide-9-9] 3 units, 48 failed, 4103 tauts, 0 hbrs, 123283 literals
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 294 transitive binary clauses
c [transred-6] found 6 units
c [block-4] scheduling all variables this time
c [block-4] scheduled 38118 variables 100%
c [block-4] limit of 21577556 steps penalty 2 = 2 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 23 blocked clauses
c [block-4] 23 < 1/100 * 244369 = 2443 considered unsuccessful
c [cce-4] boosting limit by 10
c [cce-4] limit of 107887780 steps penalty 2 = 2 + 0
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 88
c [cce-4-1] eliminated 1 clauses out of 2 (50%) of length 87
c [cce-4-1] eliminated 1 clauses out of 2 (50%) of length 86
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 85
c [cce-4-1] eliminated 1 clauses out of 2 (50%) of length 84
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 83
c [cce-4-1] eliminated 1 clauses out of 2 (50%) of length 82
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 81
c [cce-4-1] eliminated 1 clauses out of 2 (50%) of length 80
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 79
c [cce-4-1] eliminated 1 clauses out of 2 (50%) of length 78
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 77
c [cce-4-1] eliminated 1 clauses out of 2 (50%) of length 76
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 75
c [cce-4-1] eliminated 1 clauses out of 2 (50%) of length 74
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 73
c [cce-4-1] eliminated 1 clauses out of 2 (50%) of length 72
c [cce-4-1] eliminated 2 clauses out of 2 (100%) of length 71
c [cce-4-1] eliminated 1 clauses out of 3 (33%) of length 70
c [cce-4-1] eliminated 4 clauses out of 4 (100%) of length 69
c [cce-4-1] eliminated 2 clauses out of 4 (50%) of length 68
c [cce-4-1] eliminated 4 clauses out of 4 (100%) of length 67
c [cce-4-1] eliminated 2 clauses out of 4 (50%) of length 66
c [cce-4-1] eliminated 4 clauses out of 4 (100%) of length 65
c [cce-4-1] eliminated 2 clauses out of 4 (50%) of length 64
c [cce-4-1] eliminated 4 clauses out of 4 (100%) of length 63
c [cce-4-1] eliminated 2 clauses out of 4 (50%) of length 62
c [cce-4-1] eliminated 4 clauses out of 4 (100%) of length 61
c [cce-4-1] eliminated 2 clauses out of 4 (50%) of length 60
c [cce-4-1] eliminated 4 clauses out of 5 (80%) of length 59
c [cce-4-1] eliminated 4 clauses out of 6 (67%) of length 58
c [cce-4-1] eliminated 5 clauses out of 5 (100%) of length 57
c [cce-4-1] eliminated 4 clauses out of 7 (57%) of length 56
c [cce-4-1] eliminated 5 clauses out of 6 (83%) of length 55
c [cce-4-1] eliminated 4 clauses out of 6 (67%) of length 54
c [cce-4-1] eliminated 5 clauses out of 6 (83%) of length 53
c [cce-4-1] eliminated 4 clauses out of 6 (67%) of length 52
c [cce-4-1] eliminated 5 clauses out of 6 (83%) of length 51
c [cce-4-1] eliminated 4 clauses out of 6 (67%) of length 50
c [cce-4-1] eliminated 5 clauses out of 5 (100%) of length 49
c [cce-4-1] eliminated 3 clauses out of 6 (50%) of length 48
c [cce-4-1] eliminated 6 clauses out of 6 (100%) of length 47
c [cce-4-1] eliminated 3 clauses out of 6 (50%) of length 46
c [cce-4-1] eliminated 6 clauses out of 6 (100%) of length 45
c [cce-4-1] eliminated 3 clauses out of 6 (50%) of length 44
c [cce-4-1] eliminated 6 clauses out of 6 (100%) of length 43
c [cce-4-1] eliminated 3 clauses out of 6 (50%) of length 42
c [cce-4-1] eliminated 5 clauses out of 6 (83%) of length 41
c [cce-4-1] eliminated 4 clauses out of 6 (67%) of length 40
c [cce-4-1] eliminated 5 clauses out of 6 (83%) of length 39
c [cce-4-1] eliminated 4 clauses out of 6 (67%) of length 38
c [cce-4-1] eliminated 5 clauses out of 6 (83%) of length 37
c [cce-4-1] eliminated 4 clauses out of 6 (67%) of length 36
c [cce-4-1] eliminated 5 clauses out of 6 (83%) of length 35
c [cce-4-1] eliminated 4 clauses out of 6 (67%) of length 34
c [cce-4-1] eliminated 5 clauses out of 6 (83%) of length 33
c [cce-4-1] eliminated 4 clauses out of 6 (67%) of length 32
c [cce-4-1] eliminated 5 clauses out of 6 (83%) of length 31
c [cce-4-1] eliminated 4 clauses out of 6 (67%) of length 30
c [cce-4-1] eliminated 5 clauses out of 6 (83%) of length 29
c [cce-4-1] eliminated 4 clauses out of 6 (67%) of length 28
c [cce-4-1] eliminated 5 clauses out of 6 (83%) of length 27
c [cce-4-1] eliminated 4 clauses out of 7 (57%) of length 26
c [cce-4-1] eliminated 6 clauses out of 7 (86%) of length 25
c [cce-4-1] eliminated 6 clauses out of 8 (75%) of length 24
c [cce-4-1] eliminated 6 clauses out of 8 (75%) of length 23
c [cce-4-1] eliminated 6 clauses out of 8 (75%) of length 22
c [cce-4-1] eliminated 6 clauses out of 8 (75%) of length 21
c [cce-4-1] eliminated 5 clauses out of 8 (62%) of length 20
c [cce-4-1] eliminated 7 clauses out of 9 (78%) of length 19
c [cce-4-1] eliminated 5 clauses out of 8 (62%) of length 18
c [cce-4-1] eliminated 7 clauses out of 8 (88%) of length 17
c [cce-4-1] eliminated 6 clauses out of 9 (67%) of length 16
c [cce-4-1] eliminated 6 clauses out of 8 (75%) of length 15
c [cce-4-1] eliminated 6 clauses out of 8 (75%) of length 14
c [cce-4-1] eliminated 6 clauses out of 8 (75%) of length 13
c [cce-4-1] eliminated 6 clauses out of 8 (75%) of length 12
c [cce-4-1] eliminated 6 clauses out of 8 (75%) of length 11
c [cce-4-1] eliminated 6 clauses out of 25 (24%) of length 10
c [cce-4-1] eliminated 6 clauses out of 405 (1%) of length 9
c [cce-4-1] eliminated 6 clauses out of 263 (2%) of length 8
c [cce-4-1] eliminated 7 clauses out of 418 (2%) of length 7
c [cce-4-1] eliminated 253 clauses out of 1939 (13%) of length 6
c [cce-4-1] eliminated 7538 clauses out of 15909 (47%) of length 5
c [cce-4-1] incomplete large round (ATE)
c [cce-4-1] eliminated 8115 large clauses in 107887781 steps
c [cce-4-1] allowing another 53943890 steps for small clauses
c [cce-4-1] scheduling 172213 clauses = 132336 binary + 39877 ternary
c [cce-4-1] tried to eliminate 2170 small clauses 1%
c [cce-4-1] eliminated 410 binary clauses 0%
c [cce-4-1] eliminated 95 ternary clauses 0%
c [cce-4-1] eliminated 505 small clauses 0%
c [cce-4-1] eliminated 505 small clauses in 107887787 steps
c [cce-4-1] incomplete small round (ATE)
c [cce-4-1] eliminated 8620 covered clauses in round 1
c [cce-4] eliminated 8620 covered clauses in TOTAL during 1 rounds
c [bca-7] limit of 10000000 steps and 470847 added (scaled 2)
c [bca-7] 50589 out of 76238 literals actually usable 66%
c [bca-7] added 38 blocked clauses in 139367 steps
c [sweep-7] limit 2589306 penalty 0 = 0 + 0
c [sweep-7-1] 3042 pos 11.2% + 24234 neg 88.8% = 27276 sched 71.6% ret 10842
c [sweep-7-1] 2639396 steps 47 queries 3102.57 avg class size
c [sweep-7-1] 1213 decisions 44 SAT calls 262.20 avg env size
c [sweep-7-1] 26419 variables remain 69% (11697 retained 31%)
c [decomp-24] removed 10 variables
c [sweep-7-1] removed 10 vars (0 failed, 2 eqs, 5 impls)
c [sweep-7] 10 < 1/1000 * 38118 = 38 considered unsuccessful
c [sweep-7] removed 10 vars in TOTAL (1 rounds, 46 queries)
c [sort-queue-9] sorted 38108 enqueued variables after 35040 conflicts
c [score-dist-9] active 0 (0%), one 28714 (75%), zero 9394 (25%)
c [score-dist-9] max exp 1, different 2 (100%)
c [score-dist-9] median active exp 0, avg 0.0
c [simplification-9] removed 713 variables 1.8% (38108 remain 21%)
c [simplification-9] removed 23160 irredundant clauses 9.0% (234912 remain 28%)
c [simplification-9] maximum reduction of 9% = max (2%, 9%)
c [simplification-9] large reduction 9% >= 5% limit
c [simplification-9] next conflict interval 2000 = 2000/1
c [simplification-9] penalized conflict interval 2000 = 1 * 2000
c [simplification-9] hard conflict limit 47040 (soft 37040 + delta 10000)
c [simplification-9] new conflict limit 37040 (hard 47040)
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   64.2   38107   234912     35694   25023   1697 134659   52   299   55  17%      9  192   51   19  264%
c i   64.3   38106   234912     35734   25056   1699 134661   52   298   55  17%      8  191   50   19  262%
c i   65.8   38100   234912     37004   26217   1728 134696   51   298   55  17%      9  187   40   20  204%
c 
c [simplification-10] limit 37040 conflicts (hard 47040) hit after 37041 conflicts
c [ternres-7] limit 9117128 with penalty 0 = 0 + 0
c [ternres-7] all 38100 free variables schedulable
c [ternres-7] 151 ternary resolvents (0 bin, 151 trn)
c [ternres-7] fully completed ternary resolution
c [card-4] limit 569820 penalty 3 = 3 + 0
c [card-4] found 1688 at-most-one constraints of average size 4.1
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 569820 for elimination
c [card-4] 1688 out of 1688 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [decomp-25] removed 10 variables
c [basicprobe-4] limit 45585642 penalty 0 = 0 + 0
c [basicprobe-4-0] 9808 probes remain 26% after last round
c [basicprobe-4-0] 320 units = 320 failed (100%) + 0 lifted (0%)
c [basicprobe-4-0] removed 487 variables, found 159603 hbrs
c [bate-3] eliminated 141 asymmetric tautologies during probing
c [unhide-10] limit 1823425 with penalty 0 = 0 + 0
c [unhide-10-10] 4 units, 154 failed, 22961 tauts, 0 hbrs, 86633 literals
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 127 transitive binary clauses
c [transred-7] found 1 units
c [elim-7] scheduling all variables this time
c [elim-7] scheduled 37466 variables 100%
c [elim-7] limit of 91171284 steps penalty 1 = 1 + 0
c [elim-7] rescheduling of touched variables disabled
c [elim-7-1] eliminated 5251 variables 14% in round 1 in 20729081 steps
c [elim-7-1] backward subsumption/strengthening limit 20729000
c [elim-7-1-1] backward checking 15235 touched variables 41%
c [elim-7-1-1] fully completed backward checking in 1 rounds
c [elim-7-1] subsumed 3 and strengthened 18 clauses in 2903002 steps
c [elim-7-1] rescheduled 59 variables 0% by backward subsumption
c [elim-7-2] eliminated 6 variables 0% in round 2 in 27183 steps
c [elim-7-2] backward subsumption/strengthening limit 27100
c [elim-7-2-1] backward checking 59 touched variables 0%
c [elim-7-2-1] incomplete backward checking 14 remain 24%
c [elim-7-2] subsumed 0 and strengthened 5 clauses in 27137 steps
c [elim-7-2] rescheduled 22 variables 0% by backward subsumption
c [elim-7-3] eliminated 2 variables 0% in round 3 in 19359 steps
c [elim-7-3] backward subsumption/strengthening limit 19300
c [elim-7-3-1] backward checking 36 touched variables 0%
c [elim-7-3-1] incomplete backward checking 8 remain 22%
c [elim-7-3] subsumed 0 and strengthened 5 clauses in 19352 steps
c [elim-7] incomplete 20 not tried 0% in round 3
c [elim-7] transition to [ all 1 rem 1 ] state
c [elim-7] eliminated 5259 = 14% variables out of 37466 scheduled
c [bca-8] limit of 10000000 steps and 439444 added (scaled 2)
c [bca-8] 53060 out of 64416 literals actually usable 82%
c [bca-8] added 221 blocked clauses in 136381 steps
c [sort-queue-10] sorted 32207 enqueued variables after 37041 conflicts
c [score-dist-10] active 0 (0%), one 23911 (74%), zero 8296 (26%)
c [score-dist-10] max exp 1, different 2 (100%)
c [score-dist-10] median active exp 0, avg 0.0
c [simplification-10] removed 5893 variables 15.5% (32207 remain 18%)
c [simplification-10] removed 15687 irredundant clauses 6.7% (219225 remain 26%)
c [simplification-10] maximum reduction of 15% = max (15%, 7%)
c [simplification-10] large reduction 15% >= 5% limit
c [simplification-10] next conflict interval 2000 = 2000/1
c [simplification-10] penalized conflict interval 2000 = 1 * 2000
c [simplification-10] hard conflict limit 49041 (soft 39041 + delta 10000)
c [simplification-10] new conflict limit 39041 (hard 49041)
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   71.3   32206   219225     37637    5909   1641 222156   47   279   27  17%      6  166   22   20  113%
c 
c [simplification-11] limit 39041 conflicts (hard 49041) hit after 39042 conflicts
c [quatres-4] found 17113 quaternary clauses 56% in total
c [quatres-4-1] removed 2 duplicate quaternary clauses
c [quatres-4-2] added 12 quaternary resolvents
c [ternres-8] limit 9429084 with penalty 0 = 0 + 0
c [ternres-8] all 32206 free variables schedulable
c [ternres-8] 174 ternary resolvents (0 bin, 174 trn)
c [ternres-8] fully completed ternary resolution
c [decomp-26] removed 2 variables
c [simpleprobe-5] all 32205 free variables schedulable
c [simpleprobe-5] limit 37716339 penalty 0 = 0 + 0
c [decomp-27] removed 431 variables
c [simpleprobe-5] fully completed simple probing
c [simpleprobe-5] removed 431 variables, found 22378 hbrs, 205 units
c [unhide-11] limit 1885816 with penalty 0 = 0 + 0
c [unhide-11-12] 3 units, 80 failed, 17725 tauts, 0 hbrs, 19915 literals
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 238 transitive binary clauses
c [transred-8] found 1 units
c [cce-5] limit of 23572712 steps penalty 1 = 1 + 0
c [cce-5-1] eliminated 1 clauses out of 1 (100%) of length 103
c [cce-5-1] eliminated 2 clauses out of 3 (67%) of length 102
c [cce-5-1] eliminated 1 clauses out of 2 (50%) of length 101
c [cce-5-1] eliminated 1 clauses out of 3 (33%) of length 100
c [cce-5-1] eliminated 2 clauses out of 2 (100%) of length 99
c [cce-5-1] eliminated 1 clauses out of 3 (33%) of length 98
c [cce-5-1] eliminated 2 clauses out of 2 (100%) of length 97
c [cce-5-1] eliminated 1 clauses out of 3 (33%) of length 96
c [cce-5-1] eliminated 1 clauses out of 2 (50%) of length 95
c [cce-5-1] eliminated 1 clauses out of 3 (33%) of length 94
c [cce-5-1] eliminated 2 clauses out of 3 (67%) of length 93
c [cce-5-1] eliminated 3 clauses out of 5 (60%) of length 92
c [cce-5-1] eliminated 3 clauses out of 3 (100%) of length 91
c [cce-5-1] eliminated 3 clauses out of 6 (50%) of length 90
c [cce-5-1] eliminated 3 clauses out of 4 (75%) of length 89
c [cce-5-1] eliminated 3 clauses out of 5 (60%) of length 88
c [cce-5-1] eliminated 3 clauses out of 4 (75%) of length 87
c [cce-5-1] eliminated 3 clauses out of 5 (60%) of length 86
c [cce-5-1] eliminated 2 clauses out of 4 (50%) of length 85
c [cce-5-1] eliminated 3 clauses out of 5 (60%) of length 84
c [cce-5-1] eliminated 3 clauses out of 4 (75%) of length 83
c [cce-5-1] eliminated 3 clauses out of 5 (60%) of length 82
c [cce-5-1] eliminated 3 clauses out of 4 (75%) of length 81
c [cce-5-1] eliminated 3 clauses out of 5 (60%) of length 80
c [cce-5-1] eliminated 3 clauses out of 4 (75%) of length 79
c [cce-5-1] eliminated 3 clauses out of 5 (60%) of length 78
c [cce-5-1] eliminated 3 clauses out of 4 (75%) of length 77
c [cce-5-1] eliminated 3 clauses out of 5 (60%) of length 76
c [cce-5-1] eliminated 3 clauses out of 4 (75%) of length 75
c [cce-5-1] eliminated 3 clauses out of 5 (60%) of length 74
c [cce-5-1] eliminated 2 clauses out of 4 (50%) of length 73
c [cce-5-1] eliminated 4 clauses out of 5 (80%) of length 72
c [cce-5-1] eliminated 2 clauses out of 4 (50%) of length 71
c [cce-5-1] eliminated 4 clauses out of 6 (67%) of length 70
c [cce-5-1] eliminated 2 clauses out of 4 (50%) of length 69
c [cce-5-1] eliminated 4 clauses out of 5 (80%) of length 68
c [cce-5-1] eliminated 2 clauses out of 5 (40%) of length 67
c [cce-5-1] eliminated 4 clauses out of 5 (80%) of length 66
c [cce-5-1] eliminated 2 clauses out of 6 (33%) of length 65
c [cce-5-1] eliminated 4 clauses out of 4 (100%) of length 64
c [cce-5-1] eliminated 2 clauses out of 7 (29%) of length 63
c [cce-5-1] eliminated 5 clauses out of 5 (100%) of length 62
c [cce-5-1] eliminated 4 clauses out of 8 (50%) of length 61
c [cce-5-1] eliminated 5 clauses out of 7 (71%) of length 60
c [cce-5-1] eliminated 4 clauses out of 8 (50%) of length 59
c [cce-5-1] eliminated 5 clauses out of 7 (71%) of length 58
c [cce-5-1] eliminated 4 clauses out of 7 (57%) of length 57
c [cce-5-1] eliminated 5 clauses out of 8 (62%) of length 56
c [cce-5-1] eliminated 4 clauses out of 7 (57%) of length 55
c [cce-5-1] eliminated 5 clauses out of 8 (62%) of length 54
c [cce-5-1] eliminated 4 clauses out of 7 (57%) of length 53
c [cce-5-1] eliminated 5 clauses out of 8 (62%) of length 52
c [cce-5-1] eliminated 4 clauses out of 7 (57%) of length 51
c [cce-5-1] eliminated 5 clauses out of 8 (62%) of length 50
c [cce-5-1] eliminated 4 clauses out of 5 (80%) of length 49
c [cce-5-1] eliminated 4 clauses out of 8 (50%) of length 48
c [cce-5-1] eliminated 5 clauses out of 6 (83%) of length 47
c [cce-5-1] eliminated 4 clauses out of 9 (44%) of length 46
c [cce-5-1] eliminated 6 clauses out of 7 (86%) of length 45
c [cce-5-1] eliminated 4 clauses out of 9 (44%) of length 44
c [cce-5-1] eliminated 5 clauses out of 6 (83%) of length 43
c [cce-5-1] eliminated 4 clauses out of 9 (44%) of length 42
c [cce-5-1] eliminated 5 clauses out of 7 (71%) of length 41
c [cce-5-1] eliminated 5 clauses out of 10 (50%) of length 40
c [cce-5-1] eliminated 6 clauses out of 8 (75%) of length 39
c [cce-5-1] eliminated 6 clauses out of 10 (60%) of length 38
c [cce-5-1] eliminated 6 clauses out of 9 (67%) of length 37
c [cce-5-1] eliminated 6 clauses out of 10 (60%) of length 36
c [cce-5-1] eliminated 6 clauses out of 9 (67%) of length 35
c [cce-5-1] eliminated 6 clauses out of 10 (60%) of length 34
c [cce-5-1] eliminated 6 clauses out of 9 (67%) of length 33
c [cce-5-1] eliminated 5 clauses out of 10 (50%) of length 32
c [cce-5-1] eliminated 6 clauses out of 10 (60%) of length 31
c [cce-5-1] eliminated 6 clauses out of 9 (67%) of length 30
c [cce-5-1] eliminated 6 clauses out of 10 (60%) of length 29
c [cce-5-1] eliminated 7 clauses out of 11 (64%) of length 28
c [cce-5-1] eliminated 7 clauses out of 11 (64%) of length 27
c [cce-5-1] eliminated 7 clauses out of 11 (64%) of length 26
c [cce-5-1] eliminated 5 clauses out of 8 (62%) of length 25
c [cce-5-1] eliminated 7 clauses out of 10 (70%) of length 24
c [cce-5-1] eliminated 5 clauses out of 9 (56%) of length 23
c [cce-5-1] eliminated 6 clauses out of 10 (60%) of length 22
c [cce-5-1] eliminated 6 clauses out of 9 (67%) of length 21
c [cce-5-1] eliminated 6 clauses out of 10 (60%) of length 20
c [cce-5-1] eliminated 6 clauses out of 10 (60%) of length 19
c [cce-5-1] eliminated 6 clauses out of 10 (60%) of length 18
c [cce-5-1] eliminated 6 clauses out of 10 (60%) of length 17
c [cce-5-1] eliminated 6 clauses out of 9 (67%) of length 16
c [cce-5-1] eliminated 6 clauses out of 9 (67%) of length 15
c [cce-5-1] eliminated 7 clauses out of 10 (70%) of length 14
c [cce-5-1] eliminated 6 clauses out of 9 (67%) of length 13
c [cce-5-1] eliminated 5 clauses out of 9 (56%) of length 12
c [cce-5-1] eliminated 7 clauses out of 9 (78%) of length 11
c [cce-5-1] eliminated 5 clauses out of 10 (50%) of length 10
c [cce-5-1] eliminated 7 clauses out of 26 (27%) of length 9
c [cce-5-1] eliminated 6 clauses out of 138 (4%) of length 8
c [cce-5-1] eliminated 14 clauses out of 203 (7%) of length 7
c [cce-5-1] eliminated 80 clauses out of 2084 (4%) of length 6
c [cce-5-1] eliminated 16 clauses out of 8332 (0%) of length 5
c [cce-5-1] incomplete large round (ACCE)
c [cce-5-1] eliminated 512 large clauses in 23572716 steps
c [cce-5-1] allowing another 11786358 steps for small clauses
c [cce-5-1] scheduling 149584 clauses = 113317 binary + 36267 ternary
c [cce-5-1] tried to eliminate 580 small clauses 0%
c [cce-5-1] eliminated 116 binary clauses 0%
c [cce-5-1] eliminated 22 ternary clauses 0%
c [cce-5-1] eliminated 138 small clauses 0%
c [cce-5-1] eliminated 657 small clauses in 23572716 steps
c [cce-5-1] incomplete small round (ACCE)
c [cce-5-1] eliminated 1169 covered clauses in round 1
c [cce-5] eliminated 1169 covered clauses in TOTAL during 1 rounds
c [cce-5] 1169 < 1/100 * 213516 = 2135 considered unsuccessful
c [elim-8] no untried remaining variables left
c [elim-8] scheduled 31686 variables 100%
c [elim-8] boosting limit by 20
c [elim-8] limit of 3771633960 steps penalty 0 = 0 + 0
c [elim-8] rescheduling of touched variables disabled
c [elim-8-1] eliminated 405 variables 1% in round 1 in 17800509 steps
c [elim-8-1] backward subsumption/strengthening limit 17800500
c [elim-8-1-1] backward checking 2299 touched variables 7%
c [elim-8-1-1] fully completed backward checking in 1 rounds
c [elim-8-1] subsumed 0 and strengthened 5 clauses in 552895 steps
c [elim-8-1] rescheduled 17 variables 0% by backward subsumption
c [elim-8-2] eliminated 2 variables 0% in round 2 in 10057 steps
c [elim-8-2] backward subsumption/strengthening limit 10000
c [elim-8-2-1] backward checking 21 touched variables 0%
c [elim-8-2-1] incomplete backward checking 3 remain 14%
c [elim-8-2] subsumed 0 and strengthened 2 clauses in 10023 steps
c [elim-8-2] rescheduled 8 variables 0% by backward subsumption
c [elim-8-3] eliminated 1 variables 0% in round 3 in 16598 steps
c [elim-8-3] backward subsumption/strengthening limit 16500
c [elim-8-3-1] backward checking 13 touched variables 0%
c [elim-8-3-1] incomplete backward checking 0 remain 0%
c [elim-8-3] subsumed 0 and strengthened 2 clauses in 16501 steps
c [elim-8] incomplete 8 not tried 0% in round 3
c [elim-8] transition to [ all 1 rem 1 ] state
c [elim-8] eliminated 408 = 1% variables out of 31686 scheduled
c [bca-9] limit of 10000000 steps and 423834 added (scaled 2)
c [bca-9] 49353 out of 62558 literals actually usable 79%
c [bca-9] added 112 blocked clauses in 123104 steps
c [sweep-8] limit 1414362 penalty 1 = 1 + 0
c [sweep-8-1] 2777 pos 12.5% + 19465 neg 87.5% = 22242 sched 71.1% ret 9036
c [sweep-8-1] 1449642 steps 40 queries 3298.80 avg class size
c [sweep-8-1] 507 decisions 35 SAT calls 118.86 avg env size
c [sweep-8-1] 21867 variables remain 70% (9411 retained 30%)
c [decomp-28] removed 11 variables
c [sweep-8-1] removed 11 vars (0 failed, 3 eqs, 8 impls)
c [sweep-8] 11 < 1/1000 * 31278 = 31 considered unsuccessful
c [sweep-8] removed 11 vars in TOTAL (1 rounds, 39 queries)
c [sort-queue-11] sorted 31267 enqueued variables after 39042 conflicts
c [score-dist-11] active 0 (0%), one 23762 (76%), zero 7505 (24%)
c [score-dist-11] max exp 1, different 2 (100%)
c [score-dist-11] median active exp 0, avg 0.0
c [simplification-11] removed 939 variables 2.9% (31267 remain 17%)
c [simplification-11] removed 7874 irredundant clauses 3.6% (211351 remain 25%)
c [simplification-11] maximum reduction of 4% = max (3%, 4%)
c [simplification-11] geometric conflict interval increment 4000 = 20000 / 5
c [simplification-11] new conflict interval 19000
c [simplification-11] penalized conflict interval 19000 = 1 * 19000
c [simplification-11] hard conflict limit 68042 (soft 58042 + delta 10000)
c [simplification-11] new conflict limit 58042 (hard 68042)
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   75.3   31266   211351     39172    6697   1745 218311   39   262   27  15%     10  147   19   20   93%
c i   75.7   31265   211351     39859    7333   1768 218320   39   256   28  15%      7  139   35   20  176%
c i   75.8   31264   211351     40009    7467   1770 218325   38   254   28  15%      5  137   33   20  164%
c i   75.9   31263   211351     40129    7579   1774 218326   38   255   28  15%      5  138   31   20  153%
c i   76.0   31262   211351     40239    7684   1775 218328   38   256   28  15%      4  138   34   20  168%
c i   77.3   31240   211351     41909    9236   1822 218366   39   254   30  15%     11  132   49   21  240%
c i   78.0   31239   211351     42901   10160   1838 218390   39   251   30  16%      8  127   41   21  198%
c i   79.1   31238   211351     44240   11396   1872 218416   41   246   31  17%      9  120   57   21  269%
c i   79.3   31226   211351     44500   11636   1880 218423   40   245   31  16%      6  119   40   21  189%
c i   79.3   31195   211351     44514   11648   1881 218423   40   245   31  16%      6  119   39   21  181%
c i   79.6   31194   211351     44888   11987   1896 218432   40   250   31  16%      4  122   44   22  204%
c i   80.0   31140   211351     45454   12482   1930 218451   40   247   32  16%      3  119   33   22  153%
c i   84.2   31139   211351     50456   17119   2042 218565   41   256   37  16%     57  119   39   23  169%
c i   85.9   31138   211351     53021   19495   2087 218592   50   279   39  18%     24  137   72   24  295%
c i   88.4   31135   211351     56621   22800   2149 218632   57   282   46  20%     34  132   63   27  238%
c 
c [simplification-12] limit 58042 conflicts (hard 68042) hit after 58046 conflicts
c [quatres-5] found 16661 quaternary clauses 55% in total
c [quatres-5-1] removed 4 duplicate quaternary clauses
c [quatres-5-2] added 1 single-self-subsuming ternary resolvents
c [quatres-5-2] added 4 quaternary resolvents
c [ternres-9] limit 12889571 with penalty 0 = 0 + 0
c [ternres-9] all 31135 free variables schedulable
c [ternres-9] 129 ternary resolvents (0 bin, 129 trn)
c [ternres-9] fully completed ternary resolution
c [decomp-29] removed 197 variables
c [treelook-5] limit 1288957 penalty 0 = 0 + 0 boost 1
c [treelook-5] scheduled 58488 literals 94%
c [treelook-5] scheduling used 1094456 steps
c [treelook-5] scheduled completely
c [treelook-5] limit 1288957 penalty 0 = 0 + 0 boost 1
c [treelook-5] used 1310702 steps
c [treelook-5] 58426 literals remain 94%
c [treelook-5] 22014 variables remain to probed next time 71%
c [treelook-5] removed 13 variables, found 2727 hbrs
c [unhide-12] limit 2577914 with penalty 0 = 0 + 0
c [unhide-12-14] 7 units, 100 failed, 9519 tauts, 0 hbrs, 196864 literals
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 194 transitive binary clauses
c [transred-9] found 2 units
c [elim-9] no untried remaining variables left
c [elim-9] scheduled 30956 variables 100%
c [elim-9] limit of 257791436 steps penalty 0 = 0 + 0
c [elim-9] rescheduling of touched variables disabled
c [elim-9-1] eliminated 236 variables 1% in round 1 in 17354178 steps
c [elim-9-1] backward subsumption/strengthening limit 17354100
c [elim-9-1-1] backward checking 1364 touched variables 4%
c [elim-9-1-1] fully completed backward checking in 1 rounds
c [elim-9-1] subsumed 2 and strengthened 3 clauses in 357040 steps
c [elim-9-1] rescheduled 15 variables 0% by backward subsumption
c [elim-9-2] eliminated 1 variables 0% in round 2 in 12286 steps
c [elim-9-2] backward subsumption/strengthening limit 12200
c [elim-9-2-1] backward checking 10 touched variables 0%
c [elim-9-2-1] incomplete backward checking 0 remain 0%
c [elim-9-2] subsumed 0 and strengthened 2 clauses in 12201 steps
c [elim-9-2] rescheduled 8 variables 0% by backward subsumption
c [elim-9-3] eliminated 1 variables 0% in round 3 in 16004 steps
c [elim-9-3] backward subsumption/strengthening limit 16000
c [elim-9-3-1] backward checking 10 touched variables 0%
c [elim-9-3-1] incomplete backward checking 0 remain 0%
c [elim-9-3] subsumed 0 and strengthened 2 clauses in 16001 steps
c [elim-9] incomplete 8 not tried 0% in round 3
c [elim-9] transition to [ all 1 rem 1 ] state
c [elim-9] eliminated 239 = 1% variables out of 30956 scheduled
c [elim-9] 239 < 1/100 * 30956 = 309 considered unsuccessful
c [bca-10] limit of 10000000 steps and 415038 added (scaled 2)
c [bca-10] 41520 out of 61436 literals actually usable 68%
c [bca-10] added 36 blocked clauses in 116163 steps
c [sort-queue-12] sorted 30717 enqueued variables after 58046 conflicts
c [score-dist-12] active 0 (0%), one 23789 (77%), zero 6928 (23%)
c [score-dist-12] max exp 1, different 2 (100%)
c [score-dist-12] median active exp 0, avg 0.0
c [simplification-12] removed 418 variables 1.3% (30717 remain 17%)
c [simplification-12] removed 4412 irredundant clauses 2.1% (206939 remain 25%)
c [simplification-12] maximum reduction of 2% = max (1%, 2%)
c [simplification-12] geometric conflict interval increment 6666 = 20000 / 3
c [simplification-12] new conflict interval 25666
c [simplification-12] penalized conflict interval 25666 = 1 * 25666
c [simplification-12] hard conflict limit 96545 (soft 83712 + delta 12833)
c [simplification-12] new conflict limit 83712 (hard 96545)
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   94.4   30716   206939     59875   21873   2192 207484   56   280   44  20%     29  124   40   28  143%
c i   95.9   30714   206939     61833   23682   2230 207513   55   286   44  19%     14  126   42   29  146%
c i   96.0   30713   206939     62020   23856   2233 207514   55   282   44  19%     10  122   43   29  149%
c i   96.9   30712   206939     63168   24925   2257 207527   58   289   44  20%      4  126   79   29  267%
c i   98.2   30711   206939     64872   26466   2286 207544   63   299   45  21%      7  133   83   31  271%
c i  103.9   30707   206939     72238   33237   2381 207636   69   308   72  22%     86  128   70   35  203%
c i  105.8   30705   206939     74588   35375   2406 207649   73   309   75  24%     18  125  105   36  292%
c i  106.0   30701   206939     74745   35522   2412 207651   72   309   75  23%     14  125   76   36  209%
c i  106.4   30700   206939     75347   36070   2417 207659   73   313   75  23%      3  127   81   37  221%
c i  107.2   30699   206939     76346   36981   2431 207678   71   307   77  23%     -2  119   65   37  175%
c i  111.3   30698   206939     81194   41419   2477 207721   75   315   78  24%     45  119  104   40  262%
c i  112.8   30695   206939     82765   42859   2495 207729   79   320   82  25%      9  122   86   41  209%
c 
c [simplification-13] limit 83712 conflicts (hard 96545) hit after 84085 conflicts
c [quatres-6] found 16944 quaternary clauses 54% in total
c [quatres-6-2] added 5 quaternary resolvents
c [ternres-10] limit 17181514 with penalty 0 = 0 + 0
c [ternres-10] all 30695 free variables schedulable
c [ternres-10] 110 ternary resolvents (0 bin, 110 trn)
c [ternres-10] fully completed ternary resolution
c [gauss-4] limit 429537 penalty 3 = 3 + 0
c [gauss-4] extracted 10 xors of average arity 2.8
c [gauss-4] connected 28 occurrences of 25 variables (average 1.1)
c [gauss-4] limit 429537 penalty 3 = 3 + 0
c [gauss-4] fully completed
c [gauss-4] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-31] removed 25 variables
c [basicprobe-5] limit 85907574 penalty 0 = 0 + 0
c [basicprobe-5-0] 4145 probes remain 14% after last round
c [basicprobe-5-0] 619 units = 610 failed (99%) + 9 lifted (1%)
c [basicprobe-5-0] removed 902 variables, found 240984 hbrs
c [bate-4] eliminated 861 asymmetric tautologies during probing
c [unhide-13] limit 1718151 with penalty 1 = 0 + 1
c [unhide-13-16] 6 units, 153 failed, 26547 tauts, 0 hbrs, 565688 literals
c [transred-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 134 transitive binary clauses
c [block-5] scheduling all variables this time
c [block-5] scheduled 29691 variables 100%
c [block-5] limit of 21476893 steps penalty 3 = 3 + 0
c [block-5] fully completed
c [block-5] transition to [ all 0 rem 0 ] state
c [block-5] eliminated 38 blocked clauses
c [block-5] 38 < 1/100 * 197842 = 1978 considered unsuccessful
c [bca-11] limit of 10000000 steps and 396120 added (scaled 2)
c [bca-11] 34746 out of 59384 literals actually usable 59%
c [bca-11] added 26 blocked clauses in 122419 steps
c [sort-queue-13] sorted 29691 enqueued variables after 84085 conflicts
c [score-dist-13] active 0 (0%), one 23958 (81%), zero 5733 (19%)
c [score-dist-13] max exp 1, different 2 (100%)
c [score-dist-13] median active exp 0, avg 0.0
c [simplification-13] removed 1004 variables 3.3% (29691 remain 16%)
c [simplification-13] removed 9468 irredundant clauses 4.6% (197471 remain 24%)
c [simplification-13] maximum reduction of 5% = max (3%, 5%)
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 96085 (soft 86085 + delta 10000)
c [simplification-13] new conflict limit 86085 (hard 96085)
c 
c [simplification-14] limit 86085 conflicts (hard 96085) hit after 86085 conflicts
c [quatres-7] found 15615 quaternary clauses 54% in total
c [quatres-7-1] removed 2 duplicate quaternary clauses
c [quatres-7-2] added 1 single-self-subsuming ternary resolvents
c [quatres-7-2] added 1 quaternary resolvents
c [ternres-11] limit 17554386 with penalty 0 = 0 + 0
c [ternres-11] all 29691 free variables schedulable
c [ternres-11] 37 ternary resolvents (0 bin, 37 trn)
c [ternres-11] fully completed ternary resolution
c [decomp-32] removed 5 variables
c [simpleprobe-6] all 29686 free variables schedulable
c [simpleprobe-6] limit 70217546 penalty 0 = 0 + 0
c [decomp-33] removed 244 variables
c [simpleprobe-6] fully completed simple probing
c [simpleprobe-6] removed 244 variables, found 26510 hbrs, 127 units
c [unhide-14] limit 1755438 with penalty 1 = 0 + 1
c [unhide-14-17] 0 units, 118 failed, 22146 tauts, 0 hbrs, 125498 literals
c [transred-11] limit 2000000 with penalty 0 = 0 + 0
c [transred-11] removed 218 transitive binary clauses
c [transred-11] found 1 units
c [cce-6] limit of 21942983 steps penalty 2 = 2 + 0
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 15
c [cce-6-1] eliminated 2 clauses out of 6 (33%) of length 14
c [cce-6-1] eliminated 1 clauses out of 4 (25%) of length 13
c [cce-6-1] eliminated 2 clauses out of 7 (29%) of length 12
c [cce-6-1] eliminated 1 clauses out of 5 (20%) of length 11
c [cce-6-1] eliminated 2 clauses out of 6 (33%) of length 10
c [cce-6-1] eliminated 1 clauses out of 15 (7%) of length 9
c [cce-6-1] eliminated 2 clauses out of 90 (2%) of length 8
c [cce-6-1] eliminated 3 clauses out of 179 (2%) of length 7
c [cce-6-1] eliminated 3 clauses out of 1984 (0%) of length 6
c [cce-6-1] eliminated 11 clauses out of 7211 (0%) of length 5
c [cce-6-1] incomplete large round (ATE)
c [cce-6-1] eliminated 29 large clauses in 21942984 steps
c [cce-6-1] allowing another 10971492 steps for small clauses
c [cce-6-1] scheduling 138923 clauses = 107011 binary + 31912 ternary
c [cce-6-1] tried to eliminate 685 small clauses 0%
c [cce-6-1] eliminated 133 binary clauses 0%
c [cce-6-1] eliminated 13 ternary clauses 0%
c [cce-6-1] eliminated 146 small clauses 0%
c [cce-6-1] eliminated 344 small clauses in 21942984 steps
c [cce-6-1] incomplete small round (ATE)
c [cce-6-1] eliminated 373 covered clauses in round 1
c [cce-6] eliminated 373 covered clauses in TOTAL during 1 rounds
c [cce-6] 373 < 1/100 * 195444 = 1954 considered unsuccessful
c [elim-10] no untried remaining variables left
c [elim-10] scheduled 29420 variables 100%
c [elim-10] limit of 175543865 steps penalty 1 = 1 + 0
c [elim-10] rescheduling of touched variables disabled
c [elim-10-1] eliminated 556 variables 2% in round 1 in 16068752 steps
c [elim-10-1] backward subsumption/strengthening limit 16068700
c [elim-10-1-1] backward checking 3089 touched variables 10%
c [elim-10-1-1] fully completed backward checking in 1 rounds
c [elim-10-1] subsumed 4 and strengthened 22 clauses in 832991 steps
c [elim-10-1] rescheduled 76 variables 0% by backward subsumption
c [elim-10-2] eliminated 6 variables 0% in round 2 in 122814 steps
c [elim-10-2] backward subsumption/strengthening limit 122800
c [elim-10-2-1] backward checking 59 touched variables 0%
c [elim-10-2-1] fully completed backward checking in 1 rounds
c [elim-10-2] subsumed 0 and strengthened 2 clauses in 57412 steps
c [elim-10-2] rescheduled 8 variables 0% by backward subsumption
c [elim-10-3] eliminated 1 variables 0% in round 3 in 15600 steps
c [elim-10-3] backward subsumption/strengthening limit 15600
c [elim-10-3-1] backward checking 10 touched variables 0%
c [elim-10-3-1] incomplete backward checking 0 remain 0%
c [elim-10-3] subsumed 0 and strengthened 2 clauses in 15601 steps
c [elim-10] incomplete 8 not tried 0% in round 3
c [elim-10] transition to [ all 1 rem 1 ] state
c [elim-10] eliminated 563 = 2% variables out of 29420 scheduled
c [bca-12] limit of 10000000 steps and 388603 added (scaled 2)
c [bca-12] 34625 out of 57716 literals actually usable 60%
c [bca-12] added 18 blocked clauses in 113399 steps
c [sweep-9] limit 1316578 penalty 2 = 2 + 0
c [sweep-9-1] 2628 pos 12.6% + 18151 neg 87.4% = 20779 sched 72.0% ret 8078
c [sweep-9-1] 1386143 steps 26 queries 3342.31 avg class size
c [sweep-9-1] 888 decisions 25 SAT calls 355.24 avg env size
c [sweep-9-1] 20469 variables remain 71% (8388 retained 29%)
c [decomp-34] removed 1 variables
c [sweep-9-1] removed 1 vars (0 failed, 0 eqs, 1 impls)
c [sweep-9] 1 < 1/1000 * 28857 = 28 considered unsuccessful
c [sweep-9] removed 1 vars in TOTAL (1 rounds, 25 queries)
c [sort-queue-14] sorted 28856 enqueued variables after 86085 conflicts
c [score-dist-14] active 0 (0%), one 23549 (82%), zero 5307 (18%)
c [score-dist-14] max exp 1, different 2 (100%)
c [score-dist-14] median active exp 0, avg 0.0
c [simplification-14] removed 835 variables 2.8% (28856 remain 16%)
c [simplification-14] removed 3767 irredundant clauses 1.9% (193704 remain 23%)
c [simplification-14] maximum reduction of 3% = max (3%, 2%)
c [simplification-14] geometric conflict interval increment 6416 = 25666 / 4
c [simplification-14] new conflict interval 32082
c [simplification-14] penalized conflict interval 32082 = 1 * 32082
c [simplification-14] hard conflict limit 134208 (soft 118167 + delta 16041)
c [simplification-14] new conflict limit 118167 (hard 134208)
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  139.3   28855   193704     95360   43526   2910 365780   82   316   85  26%    152   98   83   47  178%
c i  142.6   28854   193704     99085   46970   2943 365804   81   328   85  25%     17  105   70   49  145%
c i  145.1   28853   193704    102244   49907   2970 365818   72   296   96  24%      6   69   50   49  101%
c i  145.4   28852   193704    102770   50406   2972 365822   69   287   96  24%     -7   59   60   49  121%
c -  150.5   28852   193704    108250   17198   3007 365852   81   307   49  26%     39   74   79   52  152%
c i  151.2   28851   193704    109465   18351   3016 365855   76   293   54  26%     57   59   63   52  119%
c i  152.7   28850   193704    111848   20547   3025 365867   71   265   58  27%     -1   29   45   53   85%
c i  155.5   28849   193704    116180   24516   3056 365903   72   270   67  27%     20   32   67   54  124%
c i  155.8   28848   193704    116582   24876   3063 365903   74   279   67  27%      4   40   87   55  159%
c 
c [simplification-15] limit 118167 conflicts (hard 134208) hit after 119423 conflicts
c [quatres-8] found 15560 quaternary clauses 53% in total
c [quatres-8-1] removed 1 duplicate quaternary clauses
c [quatres-8-2] added 1 single-self-subsuming ternary resolvents
c [quatres-8-2] added 2 quaternary resolvents
c [ternres-12] limit 22812146 with penalty 0 = 0 + 0
c [ternres-12] all 28848 free variables schedulable
c [ternres-12] 225 ternary resolvents (4 bin, 221 trn)
c [ternres-12] fully completed ternary resolution
c [card-5] limit 712879 penalty 4 = 4 + 0
c [card-5] found 846 at-most-one constraints of average size 3.9
c [card-5] no at-most-two constraint found
c [card-5] using previous limit 712879 for elimination
c [card-5] 846 out of 846 constraints (100%) meet size limits
c [card-5] no units found
c [card-5] no at-most-one constraints generated
c [decomp-35] removed 9 variables
c [treelook-6] limit 2281214 penalty 0 = 0 + 0 boost 1
c [treelook-6] scheduled 54019 literals 94%
c [treelook-6] scheduling used 1334594 steps
c [treelook-6] scheduled completely
c [treelook-6] limit 2281214 penalty 0 = 0 + 0 boost 1
c [treelook-6] used 2358265 steps
c [treelook-6] 53926 literals remain 93%
c [treelook-6] 20091 variables remain to probed next time 70%
c [decomp-36] removed 2 variables
c [treelook-6] removed 11 variables, found 9024 hbrs
c [unhide-15] limit 4562429 with penalty 0 = 0 + 0
c [unhide-15-20] 6 units, 36 failed, 13653 tauts, 0 hbrs, 474695 literals
c [transred-12] limit 2000000 with penalty 0 = 0 + 0
c [transred-12] removed 188 transitive binary clauses
c [transred-12] found 1 units
c [elim-11] no untried remaining variables left
c [elim-11] scheduled 28798 variables 100%
c [elim-11] limit of 456242938 steps penalty 0 = 0 + 0
c [elim-11] rescheduling of touched variables disabled
c [elim-11-1] eliminated 149 variables 1% in round 1 in 15743955 steps
c [elim-11-1] backward subsumption/strengthening limit 15743900
c [elim-11-1-1] backward checking 936 touched variables 3%
c [elim-11-1-1] fully completed backward checking in 1 rounds
c [elim-11-1] subsumed 4 and strengthened 1 clauses in 242394 steps
c [elim-11-1] rescheduled 14 variables 0% by backward subsumption
c [elim-11-2] eliminated 1 variables 0% in round 2 in 12092 steps
c [elim-11-2] backward subsumption/strengthening limit 12000
c [elim-11-2-1] backward checking 12 touched variables 0%
c [elim-11-2-1] incomplete backward checking 5 remain 42%
c [elim-11-2] subsumed 0 and strengthened 2 clauses in 12019 steps
c [elim-11-2] rescheduled 8 variables 0% by backward subsumption
c [elim-11-3] eliminated 1 variables 0% in round 3 in 16125 steps
c [elim-11-3] backward subsumption/strengthening limit 16100
c [elim-11-3-1] backward checking 13 touched variables 0%
c [elim-11-3-1] incomplete backward checking 0 remain 0%
c [elim-11-3] subsumed 0 and strengthened 2 clauses in 16101 steps
c [elim-11] incomplete 8 not tried 0% in round 3
c [elim-11] transition to [ all 1 rem 1 ] state
c [elim-11] eliminated 151 = 1% variables out of 28798 scheduled
c [elim-11] 151 < 1/100 * 28798 = 287 considered unsuccessful
c [bca-13] limit of 10000000 steps and 383852 added (scaled 2)
c [bca-13] 37095 out of 57296 literals actually usable 65%
c [bca-13] added 29 blocked clauses in 106729 steps
c [sort-queue-15] sorted 28647 enqueued variables after 119423 conflicts
c [score-dist-15] active 0 (0%), one 23574 (82%), zero 5073 (18%)
c [score-dist-15] max exp 1, different 2 (100%)
c [score-dist-15] median active exp 0, avg 0.0
c [simplification-15] removed 201 variables 0.7% (28647 remain 16%)
c [simplification-15] removed 2378 irredundant clauses 1.2% (191326 remain 23%)
c [simplification-15] maximum reduction of 1% = max (1%, 1%)
c [simplification-15] geometric conflict interval increment 16041 = 32082 / 2
c [simplification-15] new conflict interval 48123
c [simplification-15] penalized conflict interval 48123 = 1 * 48123
c [simplification-15] hard conflict limit 191607 (soft 167546 + delta 24061)
c [simplification-15] new conflict limit 167546 (hard 191607)
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  162.8   28646   191326    119636   23129   3180 356592   68   250   45  27%      3   10   49   55   89%
c i  165.8   28645   191326    123763   26819   3209 356614   75   273   47  27%     18   32   49   56   88%
c i  167.0   28644   191326    126033   28920   3221 356616   67   242   54  28%     -5    0   75   56  133%
c -  183.7   28644   191326    154740   26702   3253 356640   33   113   39  29%    332  -97   31   50   63%
c 
c [simplification-16] limit 167546 conflicts (hard 191607) hit after 167549 conflicts
c [quatres-9] found 15644 quaternary clauses 52% in total
c [quatres-9-2] added 3 quaternary resolvents
c [ternres-13] limit 28491982 with penalty 0 = 0 + 0
c [ternres-13] all 28644 free variables schedulable
c [ternres-13] 127 ternary resolvents (1 bin, 126 trn)
c [ternres-13] fully completed ternary resolution
c [decomp-37] removed 4 variables
c [basicprobe-6] limit 142459914 penalty 0 = 0 + 0
c [basicprobe-6-0] 4687 sched 17%, 784 failed, 11 lifted, 219794 hbrs
c [decomp-38] removed 1100 variables
c [basicprobe-6-1] 5997 probes remain 22% after last round
c [basicprobe-6-1] 888 units = 875 failed (99%) + 13 lifted (1%)
c [basicprobe-6-1] removed 1228 variables, found 243214 hbrs
c [bate-5] eliminated 973 asymmetric tautologies during probing
c [unhide-16] limit 2849198 with penalty 1 = 0 + 1
c [unhide-16-21] 1 units, 6 failed, 32306 tauts, 0 hbrs, 606779 literals
c [transred-13] limit 2000000 with penalty 0 = 0 + 0
c [transred-13] removed 185 transitive binary clauses
c [bca-14] limit of 10000000 steps and 363841 added (scaled 2)
c [bca-14] 33010 out of 54814 literals actually usable 60%
c [bca-14] added 10 blocked clauses in 112413 steps
c [sort-queue-16] sorted 27406 enqueued variables after 167549 conflicts
c [score-dist-16] active 0 (0%), one 23205 (85%), zero 4201 (15%)
c [score-dist-16] max exp 1, different 2 (100%)
c [score-dist-16] median active exp 0, avg 0.0
c [simplification-16] removed 1238 variables 4.3% (27406 remain 15%)
c [simplification-16] removed 10013 irredundant clauses 5.2% (181313 remain 22%)
c [simplification-16] maximum reduction of 5% = max (4%, 5%)
c [simplification-16] large reduction 5% >= 5% limit
c [simplification-16] next conflict interval 2000 = 2000/1
c [simplification-16] penalized conflict interval 2000 = 1 * 2000
c [simplification-16] hard conflict limit 179549 (soft 169549 + delta 10000)
c [simplification-16] new conflict limit 169549 (hard 179549)
c 
c [simplification-17] limit 169549 conflicts (hard 179549) hit after 169549 conflicts
c [quatres-10] found 15438 quaternary clauses 54% in total
c [quatres-10-1] removed 2 duplicate quaternary clauses
c [quatres-10-2] added 1 single-self-subsuming ternary resolvents
c [quatres-10-2] added 1 quaternary resolvents
c [ternres-14] limit 28820253 with penalty 0 = 0 + 0
c [ternres-14] all 27406 free variables schedulable
c [ternres-14] 39 ternary resolvents (2 bin, 37 trn)
c [ternres-14] fully completed ternary resolution
c [decomp-39] removed 38 variables
c [simpleprobe-7] all 27368 free variables schedulable
c [simpleprobe-7] limit 115281015 penalty 0 = 0 + 0
c [decomp-40] removed 103 variables
c [simpleprobe-7] fully completed simple probing
c [simpleprobe-7] removed 103 variables, found 30853 hbrs, 51 units
c [unhide-17] limit 2882025 with penalty 1 = 0 + 1
c [unhide-17-23] 0 units, 14 failed, 32217 tauts, 0 hbrs, 566356 literals
c [transred-14] limit 2000000 with penalty 0 = 0 + 0
c [transred-14] removed 219 transitive binary clauses
c [elim-12] no untried remaining variables left
c [elim-12] scheduled 27252 variables 100%
c [elim-12] limit of 288202538 steps penalty 1 = 1 + 0
c [elim-12] rescheduling of touched variables disabled
c [elim-12-1] eliminated 451 variables 2% in round 1 in 14542625 steps
c [elim-12-1] backward subsumption/strengthening limit 14542600
c [elim-12-1-1] backward checking 2625 touched variables 10%
c [elim-12-1-1] fully completed backward checking in 1 rounds
c [elim-12-1] subsumed 8 and strengthened 9 clauses in 643826 steps
c [elim-12-1] rescheduled 43 variables 0% by backward subsumption
c [elim-12-2] eliminated 3 variables 0% in round 2 in 25462 steps
c [elim-12-2] backward subsumption/strengthening limit 25400
c [elim-12-2-1] backward checking 24 touched variables 0%
c [elim-12-2-1] incomplete backward checking 0 remain 0%
c [elim-12-2] subsumed 0 and strengthened 0 clauses in 25401 steps
c [elim-12-2] fully rescheduled 26798 variables 98%
c [elim-12-3] eliminated 16 variables 0% in round 3 in 14430729 steps
c [elim-12-3] backward subsumption/strengthening limit 14430700
c [elim-12-3-1] backward checking 103 touched variables 0%
c [elim-12-3-1] fully completed backward checking in 1 rounds
c [elim-12-3] subsumed 0 and strengthened 0 clauses in 52515 steps
c [elim-12] fully completed in 3 rounds
c [elim-12] transition to [ all 0 rem 0 ] state
c [elim-12] eliminated 470 = 2% variables out of 27252 scheduled
c [bca-15] limit of 10000000 steps and 355456 added (scaled 2)
c [bca-15] 32905 out of 53566 literals actually usable 61%
c [bca-15] added 9 blocked clauses in 103260 steps
c [sort-queue-17] sorted 26782 enqueued variables after 169549 conflicts
c [score-dist-17] active 0 (0%), one 22784 (85%), zero 3998 (15%)
c [score-dist-17] max exp 1, different 2 (100%)
c [score-dist-17] median active exp 0, avg 0.0
c [simplification-17] removed 624 variables 2.3% (26782 remain 15%)
c [simplification-17] removed 4195 irredundant clauses 2.3% (177118 remain 21%)
c [simplification-17] maximum reduction of 2% = max (2%, 2%)
c [simplification-17] geometric conflict interval increment 16041 = 48123 / 3
c [simplification-17] new conflict interval 64164
c [simplification-17] penalized conflict interval 64164 = 1 * 64164
c [simplification-17] hard conflict limit 265795 (soft 233713 + delta 32082)
c [simplification-17] new conflict limit 233713 (hard 265795)
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  220.5   26781   177118    184495   43388   3827 447423   72   294   78  24%    585   76   76   55  138%
c i  229.3   26780   177118    197708   55884   3860 447440   66   282  123  23%    -94   54   83   57  146%
c -  231.3   26780   177118    200417   25344   3868 447442   63   228   55  27%   -235   -2   65   57  114%
c i  249.4   26779   177118    228312   51092   3986 447506   66   230  113  29%    192   -9   78   62  126%
c -  254.7   26779   177118    237726   26669   4014 447515   61   210   38  29%   -117  -26   47   62   77%
c 
c [simplification-18] limit 233713 conflicts (hard 265795) hit after 246702 conflicts
c [quatres-11] found 15746 quaternary clauses 53% in total
c [ternres-15] limit 38357645 with penalty 0 = 0 + 0
c [ternres-15] all 26779 free variables schedulable
c [ternres-15] 173 ternary resolvents (3 bin, 170 trn)
c [ternres-15] fully completed ternary resolution
c [gauss-5] limit 479470 penalty 4 = 4 + 0
c [gauss-5] extracted 7 xors of average arity 3.0
c [gauss-5] connected 21 occurrences of 21 variables (average 1.0)
c [gauss-5] limit 479470 penalty 4 = 4 + 0
c [gauss-5] fully completed
c [gauss-5] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-41] removed 2 variables
c [treelook-7] limit 3835764 penalty 0 = 0 + 0 boost 1
c [treelook-7] scheduled 49833 literals 93%
c [treelook-7] scheduling used 1449836 steps
c [treelook-7] scheduled completely
c [treelook-7] limit 3835764 penalty 0 = 0 + 0 boost 1
c [treelook-7] used 3888957 steps
c [treelook-7] 49734 literals remain 93%
c [treelook-7] 18272 variables remain to probed next time 68%
c [decomp-42] removed 1 variables
c [treelook-7] removed 3 variables, found 13791 hbrs
c [unhide-18] limit 3835764 with penalty 1 = 0 + 1
c [unhide-18-25] 0 units, 9 failed, 11866 tauts, 0 hbrs, 445399 literals
c [transred-15] limit 2000000 with penalty 0 = 0 + 0
c [transred-15] removed 240 transitive binary clauses
c [transred-15] found 1 units
c [block-6] scheduling all variables this time
c [block-6] scheduled 26770 variables 100%
c [block-6] limit of 23973528 steps penalty 4 = 4 + 0
c [block-6] fully completed
c [block-6] transition to [ all 0 rem 0 ] state
c [block-6] eliminated 3 blocked clauses
c [block-6] 3 < 1/100 * 176298 = 1762 considered unsuccessful
c [cce-7] limit of 23973528 steps penalty 3 = 3 + 0
c [cce-7-1] eliminated 1 clauses out of 4 (25%) of length 22
c [cce-7-1] eliminated 2 clauses out of 7 (29%) of length 21
c [cce-7-1] eliminated 1 clauses out of 7 (14%) of length 20
c [cce-7-1] eliminated 2 clauses out of 4 (50%) of length 19
c [cce-7-1] eliminated 1 clauses out of 5 (20%) of length 18
c [cce-7-1] eliminated 2 clauses out of 6 (33%) of length 17
c [cce-7-1] eliminated 1 clauses out of 7 (14%) of length 16
c [cce-7-1] eliminated 1 clauses out of 6 (17%) of length 15
c [cce-7-1] eliminated 2 clauses out of 6 (33%) of length 14
c [cce-7-1] eliminated 2 clauses out of 6 (33%) of length 13
c [cce-7-1] eliminated 1 clauses out of 3 (33%) of length 12
c [cce-7-1] eliminated 1 clauses out of 3 (33%) of length 11
c [cce-7-1] eliminated 2 clauses out of 6 (33%) of length 10
c [cce-7-1] eliminated 2 clauses out of 7 (29%) of length 9
c [cce-7-1] eliminated 5 clauses out of 61 (8%) of length 8
c [cce-7-1] eliminated 12 clauses out of 118 (10%) of length 7
c [cce-7-1] eliminated 15 clauses out of 2007 (1%) of length 6
c [cce-7-1] eliminated 61 clauses out of 6440 (1%) of length 5
c [cce-7-1] incomplete large round (ACCE)
c [cce-7-1] eliminated 114 large clauses in 23973545 steps
c [cce-7-1] allowing another 11986772 steps for small clauses
c [cce-7-1] scheduling 126473 clauses = 98650 binary + 27823 ternary
c [cce-7-1] tried to eliminate 922 small clauses 1%
c [cce-7-1] eliminated 168 binary clauses 0%
c [cce-7-1] eliminated 35 ternary clauses 0%
c [cce-7-1] eliminated 203 small clauses 0%
c [cce-7-1] eliminated 203 small clauses in 23973536 steps
c [cce-7-1] incomplete small round (ACCE)
c [cce-7-1] eliminated 317 covered clauses in round 1
c [cce-7] eliminated 317 covered clauses in TOTAL during 1 rounds
c [cce-7] 317 < 1/100 * 176277 = 1762 considered unsuccessful
c [elim-13] scheduling all variables this time
c [elim-13] scheduled 26770 variables 100%
c [elim-13] almost no limit of 100000000000 steps
c [elim-13] rescheduling of touched variables disabled
c [elim-13-1] eliminated 84 variables 0% in round 1 in 14266105 steps
c [elim-13-1] backward subsumption/strengthening limit 14266100
c [elim-13-1-1] backward checking 551 touched variables 2%
c [elim-13-1-1] fully completed backward checking in 1 rounds
c [elim-13-1] subsumed 1 and strengthened 1 clauses in 147908 steps
c [elim-13-1] rescheduled 7 variables 0% by backward subsumption
c [elim-13-2] no variable eliminated in round 2 in 3556 steps
c [elim-13] fully completed in 2 rounds
c [elim-13] transition to [ all 0 rem 0 ] state
c [elim-13] eliminated 84 = 0% variables out of 26770 scheduled
c [elim-13] 84 < 1/100 * 26770 = 267 considered unsuccessful
c [bca-16] limit of 10000000 steps and 352794 added (scaled 2)
c [bca-16] 32611 out of 53374 literals actually usable 61%
c [bca-16] added 37 blocked clauses in 102295 steps
c [sweep-10] limit 1438411 penalty 3 = 3 + 0
c [sweep-10-1] 2571 pos 13.1% + 17094 neg 86.9% = 19665 sched 73.7% ret 7021
c [sweep-10-1] 1447861 steps 30 queries 2568.03 avg class size
c [sweep-10-1] 984 decisions 28 SAT calls 308.75 avg env size
c [sweep-10-1] 19197 variables remain 72% (7489 retained 28%)
c [decomp-43] removed 3 variables
c [sweep-10-1] removed 3 vars (0 failed, 1 eqs, 3 impls)
c [sweep-10] 3 < 1/1000 * 26686 = 26 considered unsuccessful
c [sweep-10] removed 3 vars in TOTAL (1 rounds, 29 queries)
c [sort-queue-18] sorted 26683 enqueued variables after 246702 conflicts
c [score-dist-18] active 0 (0%), one 22832 (86%), zero 3851 (14%)
c [score-dist-18] max exp 1, different 2 (100%)
c [score-dist-18] median active exp 0, avg 0.0
c [simplification-18] removed 96 variables 0.4% (26683 remain 15%)
c [simplification-18] removed 1337 irredundant clauses 0.8% (175781 remain 21%)
c [simplification-18] maximum reduction of 1% = max (0%, 1%)
c [simplification-18] geometric conflict interval increment 32082 = 64164 / 2
c [simplification-18] new conflict interval 96246
c [simplification-18] penalized conflict interval 96246 = 1 * 96246
c [simplification-18] hard conflict limit 391071 (soft 342948 + delta 48123)
c [simplification-18] new conflict limit 342948 (hard 391071)
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 -  288.2   26683   175781    280717   27862   4272 448679   75   220   54  34%    432   -3  106   64  166%
c i  294.2   26682   175781    293082   39594   4292 448684   59   228   98  26%    533    7   89   62  143%
c i  299.3   26681   175781    299520   45459   4326 448708   77   270  103  29%   -351   46   82   64  128%
c i  299.3   26677   175781    299521   45459   4326 448708   77   270  103  29%   -351   46   82   64  127%
c i  300.1   26676   175781    300546   46401   4333 448711   79   284  103  28%   -394   59   75   65  117%
c -  312.6   26676   175781    318315   28560   4391 448736   76   249   54  31%    -98   24   87   66  131%
c i  318.2   26675   175781    325467   35033   4435 448746  101   332   53  30%     18   99  121   70  172%
c i  321.0   26674   175781    329308   38462   4446 448756   95   320   58  30%   -289   81   99   71  139%
c i  322.1   26673   175781    330728   39736   4452 448764   93   319   62  29%   -312   79   88   72  123%
c 
c [simplification-19] limit 342958 conflicts (hard 391071) hit after 350093 conflicts
c [ternres-16] limit 51923791 with penalty 0 = 0 + 0
c [ternres-16] all 26672 free variables schedulable
c [ternres-16] 44 ternary resolvents (3 bin, 41 trn)
c [ternres-16] fully completed ternary resolution
c [decomp-44] removed 13 variables
c [basicprobe-7] limit 259618959 penalty 0 = 0 + 0
c [basicprobe-7-0] 6006 sched 23%, 291 failed, 4 lifted, 79836 hbrs
c [decomp-45] removed 395 variables
c [basicprobe-7-1] 496 probes remain 2% after last round
c [basicprobe-7-1] 395 units = 390 failed (99%) + 5 lifted (1%)
c [basicprobe-7-1] removed 528 variables, found 109423 hbrs
c [bate-6] eliminated 387 asymmetric tautologies during probing
c [unhide-19] limit 2596189 with penalty 2 = 0 + 2
c [unhide-19-27] 0 units, 0 failed, 20315 tauts, 0 hbrs, 1366827 literals
c [transred-16] limit 2000000 with penalty 0 = 0 + 0
c [transred-16] removed 160 transitive binary clauses
c [bca-17] limit of 10000000 steps and 341105 added (scaled 2)
c [bca-17] 27825 out of 52286 literals actually usable 53%
c [bca-17] added 10 blocked clauses in 119049 steps
c [sort-queue-19] sorted 26142 enqueued variables after 350093 conflicts
c [score-dist-19] active 0 (0%), one 22776 (87%), zero 3366 (13%)
c [score-dist-19] max exp 1, different 2 (100%)
c [score-dist-19] median active exp 0, avg 0.0
c [simplification-19] removed 530 variables 2.0% (26142 remain 14%)
c [simplification-19] removed 5850 irredundant clauses 3.3% (169931 remain 20%)
c [simplification-19] maximum reduction of 3% = max (2%, 3%)
c [simplification-19] geometric conflict interval increment 24061 = 96246 / 4
c [simplification-19] new conflict interval 120307
c [simplification-19] penalized conflict interval 120307 = 1 * 120307
c [simplification-19] hard conflict limit 530553 (soft 470400 + delta 60153)
c [simplification-19] new conflict limit 470400 (hard 530553)
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 -  359.9   26142   169931    358272   28278   4559 486187   67   178   38  37%    120  -69   60   73   82%
c -  384.2   26142   169931    398831   31250   4642 486227   82   295   59  28%    537   71   97   71  137%
c -  414.5   26142   169931    439032   29702   4766 486287   97   297   58  33%    760   54   63   80   79%
c 
c [simplification-20] limit 470400 conflicts (hard 530553) hit after 470401 conflicts
c [quatres-12] found 15930 quaternary clauses 52% in total
c [quatres-12-1] removed 2 duplicate quaternary clauses
c [quatres-12-2] added 2 single-self-subsuming ternary resolvents
c [quatres-12-2] added 3 quaternary resolvents
c [ternres-17] limit 67397843 with penalty 0 = 0 + 0
c [ternres-17] all 26142 free variables schedulable
c [ternres-17] 52 ternary resolvents (2 bin, 50 trn)
c [ternres-17] fully completed ternary resolution
c [decomp-46] removed 6 variables
c [simpleprobe-8] all 26136 free variables schedulable
c [simpleprobe-8] limit 200000000 penalty 0 = 0 + 0
c [decomp-47] removed 9 variables
c [simpleprobe-8] fully completed simple probing
c [simpleprobe-8] removed 9 variables, found 18618 hbrs, 2 units
c [transred-17] limit 2000000 with penalty 0 = 0 + 0
c [transred-17] removed 244 transitive binary clauses
c [elim-14] scheduling all variables this time
c [elim-14] scheduled 26127 variables 100%
c [elim-14] limit of 400000000 steps penalty 1 = 1 + 0
c [elim-14] rescheduling of touched variables disabled
c [elim-14-1] eliminated 306 variables 1% in round 1 in 13754908 steps
c [elim-14-1] backward subsumption/strengthening limit 13754900
c [elim-14-1-1] backward checking 1761 touched variables 7%
c [elim-14-1-1] fully completed backward checking in 1 rounds
c [elim-14-1] subsumed 0 and strengthened 3 clauses in 418808 steps
c [elim-14-1] rescheduled 9 variables 0% by backward subsumption
c [elim-14-2] no variable eliminated in round 2 in 4823 steps
c [elim-14] fully completed in 2 rounds
c [elim-14] transition to [ all 0 rem 0 ] state
c [elim-14] eliminated 306 = 1% variables out of 26127 scheduled
c [bca-18] limit of 10000000 steps and 339934 added (scaled 2)
c [bca-18] 28879 out of 51644 literals actually usable 56%
c [bca-18] added 8 blocked clauses in 107373 steps
c [sort-queue-20] sorted 25821 enqueued variables after 470401 conflicts
c [score-dist-20] active 0 (0%), one 22621 (88%), zero 3200 (12%)
c [score-dist-20] max exp 1, different 2 (100%)
c [score-dist-20] median active exp 0, avg 0.0
c [simplification-20] removed 321 variables 1.2% (25821 remain 14%)
c [simplification-20] removed 588 irredundant clauses 0.3% (169343 remain 20%)
c [simplification-20] maximum reduction of 1% = max (1%, 0%)
c [simplification-20] geometric conflict interval increment 60153 = 120307 / 2
c [simplification-20] new conflict interval 180460
c [simplification-20] penalized conflict interval 180460 = 1 * 180460
c [simplification-20] hard conflict limit 741091 (soft 650861 + delta 90230)
c [simplification-20] new conflict limit 650861 (hard 741091)
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 -  452.6   25821   169343    497704   33052   4792 482840   48   115   41  41%    916 -107   37   72   52%
c -  478.3   25821   169343    535738   34340   4865 482874   74   248   59  30%    964   52   59   65   90%
c -  508.2   25821   169343    575104   33071   4949 482901  102   316   58  32%    991  111   97   70  138%
c -  539.9   25821   169343    617548   33533   5054 482949   85   269   58  32%   1007   51   40   74   55%
c -  568.1   25821   169343    657420   39661   5055 482949   49   105   69  47%   1015  -63   51   62   83%
c 
c [simplification-21] limit 650861 conflicts (hard 741091) hit after 663235 conflicts
c [quatres-13] found 16300 quaternary clauses 51% in total
c [quatres-13-1] removed 1 duplicate quaternary clauses
c [quatres-13-2] added 6 quaternary resolvents
c [ternres-18] limit 91825730 with penalty 0 = 0 + 0
c [ternres-18] all 25821 free variables schedulable
c [ternres-18] 44 ternary resolvents (0 bin, 44 trn)
c [ternres-18] fully completed ternary resolution
c [card-6] limit 2869554 penalty 4 = 4 + 0
c [card-6] found 2425 at-most-one constraints of average size 4.0
c [card-6] no at-most-two constraint found
c [card-6] using previous limit 2869554 for elimination
c [card-6] 2425 out of 2425 constraints (100%) meet size limits
c [card-6] no units found
c [card-6] no at-most-one constraints generated
c [decomp-48] removed 4 variables
c [treelook-8] limit 9182573 penalty 0 = 0 + 0 boost 1
c [treelook-8] scheduled 48020 literals 93%
c [treelook-8] scheduling used 1514597 steps
c [treelook-8] scheduled completely
c [treelook-8] limit 9182573 penalty 0 = 0 + 0 boost 1
c [treelook-8] used 9191699 steps
c [treelook-8] 47756 literals remain 92%
c [treelook-8] 17438 variables remain to probed next time 68%
c [decomp-49] removed 1 variables
c [treelook-8] removed 3 variables, found 16714 hbrs
c [unhide-20] limit 4591286 with penalty 2 = 1 + 1
c [unhide-20-30] 0 units, 0 failed, 28090 tauts, 0 hbrs, 1133408 literals
c [transred-18] limit 2000000 with penalty 0 = 0 + 0
c [transred-18] removed 157 transitive binary clauses
c [elim-15] scheduling all variables this time
c [elim-15] scheduled 25814 variables 100%
c [elim-15] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-15] rescheduling of touched variables disabled
c [elim-15-1] eliminated 47 variables 0% in round 1 in 13727996 steps
c [elim-15-1] backward subsumption/strengthening limit 13727900
c [elim-15-1-1] backward checking 367 touched variables 1%
c [elim-15-1-1] fully completed backward checking in 1 rounds
c [elim-15-1] subsumed 4 and strengthened 1 clauses in 104870 steps
c [elim-15-1] rescheduled 15 variables 0% by backward subsumption
c [elim-15-2] eliminated 1 variables 0% in round 2 in 6976 steps
c [elim-15-2] backward subsumption/strengthening limit 6900
c [elim-15-2-1] backward checking 11 touched variables 0%
c [elim-15-2-1] incomplete backward checking 0 remain 0%
c [elim-15-2] subsumed 4 and strengthened 0 clauses in 6901 steps
c [elim-15-2] rescheduled 6 variables 0% by backward subsumption
c [elim-15-3] no variable eliminated in round 3 in 6229 steps
c [elim-15] fully completed in 3 rounds
c [elim-15] transition to [ all 0 rem 0 ] state
c [elim-15] eliminated 48 = 0% variables out of 25814 scheduled
c [elim-15] 48 < 1/100 * 25814 = 258 considered unsuccessful
c [bca-19] limit of 10000000 steps and 338792 added (scaled 2)
c [bca-19] 29591 out of 51534 literals actually usable 57%
c [bca-19] added 8 blocked clauses in 105032 steps
c [sort-queue-21] sorted 25766 enqueued variables after 663235 conflicts
c [score-dist-21] active 0 (0%), one 22665 (88%), zero 3101 (12%)
c [score-dist-21] max exp 1, different 2 (100%)
c [score-dist-21] median active exp 0, avg 0.0
c [simplification-21] removed 55 variables 0.2% (25766 remain 14%)
c [simplification-21] removed 573 irredundant clauses 0.3% (168770 remain 20%)
c [simplification-21] maximum reduction of 0% = max (0%, 0%)
c [simplification-21] full geometric conflict interval increment 180460
c [simplification-21] new conflict interval 360920
c [simplification-21] penalized conflict interval 360920 = 1 * 360920
c [simplification-21] hard conflict limit 1204615 (soft 1024155 + delta 180460)
c [simplification-21] new conflict limit 1024155 (hard 1204615)
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 -  602.4   25766   168770    699017   37296   5073 470698   40   103   62  39%   1019  -59   38   59   64%
c i  630.8   25765   168770    734091   69920   5179 470743   96   318  156  30%   1021  123   58   68   85%
c -  636.4   25765   168770    740179   33393   5200 470749   82   274   40  30%  -4796   68   42   70   61%
c -  670.5   25765   168770    787713   35907   5292 470790   77   200   60  39%  -1802  -18   87   73  119%
c i  687.1   25764   168770    813565   59459   5322 470803   87   266  143  33%   -881   61  134   71  189%
c -  703.1   25763   168770    834407   37940   5356 470824   71   202   61  35%  -1280  -19   71   74   97%
c -  735.1   25763   168770    881446   38628   5418 470858   80   213   62  37%   -100    3   55   75   73%
c -  771.3   25763   168770    929067   38814   5499 470890   81   211   59  38%    481   -2   83   78  106%
c i  772.8   25762   168770    930817   40333   5507 470891   93   260   69  36%    495   46  104   79  132%
c -  810.4   25762   168770    977877   38446   5602 470931   78   243   59  32%   -142    4   73   83   87%
c -  842.4   25762   168770   1026921   43622   5626 470943   53   129   45  41%    472  -70   51   73   71%
c 
c [simplification-22] limit 1024155 conflicts (hard 1204615) hit after 1041858 conflicts
c [quatres-14] found 16795 quaternary clauses 49% in total
c [quatres-14-2] added 2 quaternary resolvents
c [ternres-19] limit 143490179 with penalty 0 = 0 + 0
c [ternres-19] all 25762 free variables schedulable
c [ternres-19] 98 ternary resolvents (2 bin, 96 trn)
c [ternres-19] fully completed ternary resolution
c [decomp-50] removed 6 variables
c [basicprobe-8] limit 400000000 penalty 0 = 0 + 0
c [basicprobe-8-0] 870 sched 3%, 39 failed, 1 lifted, 7770 hbrs
c [decomp-51] removed 54 variables
c [basicprobe-8-1] 7398 sched 29%, 111 failed, 7 lifted, 31838 hbrs
c [decomp-52] removed 128 variables
c [basicprobe-8-2] 7372 sched 29%, 33 failed, 0 lifted, 11275 hbrs
c [decomp-53] removed 37 variables
c [basicprobe-8-3] 2435 probes remain 10% after last round
c [basicprobe-8-3] 194 units = 186 failed (96%) + 8 lifted (4%)
c [basicprobe-8-3] removed 222 variables, found 53464 hbrs
c [bate-7] eliminated 158 asymmetric tautologies during probing
c [transred-19] limit 2000000 with penalty 0 = 0 + 0
c [transred-19] removed 269 transitive binary clauses
c [bca-20] limit of 10000000 steps and 335314 added (scaled 2)
c [bca-20] 27621 out of 51078 literals actually usable 54%
c [bca-20] added 4 blocked clauses in 119092 steps
c [sort-queue-22] sorted 25538 enqueued variables after 1041858 conflicts
c [score-dist-22] active 0 (0%), one 22654 (89%), zero 2884 (11%)
c [score-dist-22] max exp 1, different 2 (100%)
c [score-dist-22] median active exp 0, avg 0.0
c [simplification-22] removed 224 variables 0.9% (25538 remain 14%)
c [simplification-22] removed 1741 irredundant clauses 1.0% (167029 remain 20%)
c [simplification-22] maximum reduction of 1% = max (1%, 1%)
c [simplification-22] geometric conflict interval increment 180460 = 360920 / 2
c [simplification-22] new conflict interval 541380
c [simplification-22] penalized conflict interval 541380 = 1 * 541380
c [simplification-22] hard conflict limit 1853928 (soft 1583238 + delta 270690)
c [simplification-22] new conflict limit 1583238 (hard 1853928)
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 -  896.4   25538   167029   1071622   40205   5538 506428   87   241   61  36%    745   26   62   80   78%
c -  933.5   25538   167029   1122109   41344   5606 506448   51   125   62  41%    895 -102   77   80   96%
c -  962.4   25538   167029   1168710   46533   5619 506451   31    67   48  46%    961  -93   26   58   44%
c 1  967.4   25538   167029   1176297   53846   5627 506453   52   149   92  35%    968   -3   75   57  132%
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
s SATISFIABLE
c
c bate: 2570 basic ate = 1865 trn 73% + 705 lrg 27% in 7 updates
c bcas: 20 count, 1516 added (1220 skipped), 2977713 steps
c bkwd: tried 246092 clauses, 492078 lits, 2.00 lits/clause
c bkwd: checked 7075549 occs, 28.75 occs/clause, 14.38 occs/lit
c bkwd: subsumed 3 binary, 30 ternary, 15 large
c bkwd: strengthened 0 binary, 0 ternary (0% self), 150 large (0% self)
c blkd: 6 bces, 8398 removed, 5136509 resolutions, 14336018 steps
c blkd: 9644 blocking literals 3%, 2 pure
c bump: 1174246 bumped seen, 792853709 lits 675.2 on average
c card: 6 count, 0 units, 0 am1, 59902198 steps
c card: 0 rescheduled, 0 eliminated, 0 resolved, 59908 subsumed
c card: 20685 at-most-one constraints found, average size 4.53
c card: 20685 at-most-one constraints used 100%, average size 4.53
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: 7 cces, 15882 eliminated, 15785 ate 99%, 97 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: 2788378 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 149 gcs, 0 rescored clauses, 0 rescored vars
c dcps: 53 decompositions, 50158 equivalent 26%
c deco: 103866 decision-only clauses 9%, 73% reduction
c decs: 11876279 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 15 elims, 50096 eliminated 26%, 25 pure 0%
c elms: 46 rounds, 3.1 rounds/bve
c elms: 33793 small 67%, 16276 large 32%
c elms: 127341 tried small, 33793 succeeded 27%, 93548 failed 73%
c elms: 24184 subsumed, 68027 strengthened, 1101 blocked
c elms: 13156778 copies, 12459699 resolutions, 3859988 ipos
c elms: 3444058 subchks, 3565703 strchks
c gaus: 5 extractions, 1162 extracted, 2.2 size, 3 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 8819120 steps, 4409560 extr 50%, 45296 elim 1%
c glue: 68.9 orig avg, 68.9 real avg, 6.9 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 1159429 = 146182 simple 13% + 990935 trn 85% + 22312 lrg 2%, 3228 sub 0%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 1174246 clauses, 497.8 length
c lrnd: 584538069 lits = 707576277 orig - 123038208 removed 17%
c lrnd: 490377 uips 42%, 609021 flips 52%
c mins: 1036330 mins 90%, 2468 bin 0%, 7165 size 1%
c mins: 1307279642 poisoned searches, 288533563 hits, 22% hit rate
c mins: 1421618244 used twice searches, 31475306 hits, 2% hit rate
c move: moved 16015, 9384 bin 59%, 6631 trn 41%
c otfs: 2264 driving 25%, 6831 restarting 75%
c otfs: str 9095, 8989 red 99%, 106 irr 1%
c otfs: str 9095, 0 bin 0%, 86 trn 1%, 9009 lrg 99%
c otfs: sub 20, 20 red 100%, 0 irr 0%
c otfs: sub 20, 0 bin 0%, 0 trn 0%, 20 lrg 100%
c phas: 8 computed, 64099 set, 0 pos (0%), 64099 neg (100%)
c prbs: 8 basic, 88809 probed, 2548 failed, 37 lifted
c prbs: 8 simple, 676621 probed, 941 failed, 1910 eqs
c prbs: 8 treelook, 543 probed, 32 failed, 0 lifted
c prom: 174171 locked 11% out of 1650124 tried
c prps: 1593863846 props, 126 props/dec
c prps: 94% srch, 6% simp, 0% lkhd
c quat: 14 count, 43 quat, 6 self1, 0 self2, 189 dup
c queu: 22 sorted, 11876279 next (3 steps 0.00)
c queu: 793839224 enq (793839179 steps 1.00), 792853709 deq 100%
c redc: 7529 clauses 37%, 20584 tried 2%, 119 sat 1%
c redc: 18316 lits 9%, 204323 tried 0%, 119 sat 0%
c redc: 892 times jump level reduced, 26.8 levels on average
c reds: 25 count, 47051.9 conflicts per reduce
c reds: 0 memlim 0%, 25 arith 100%
c reds: 775223 collected 83%, 164403 retired 17%
c rmbd: 28876 removed, 3483 red 12%
c rsts: 24753 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: 22 count, 20 confs 91%, 0 vars 0%
c simp: 1 its 5%, 1 bin 5%, 0 trns 0%
c subl: 1174246 count (1574253 tried 1.3), 86521 sub out of 1165795 (7.4%)
c swps: 10 count, 10 rounds, 452 queries (45.2/round)
c swps: 411 sat calls, 9 unsat (0.5% success rate)
c swps: 7789 decisions 19.0, 213 conflicts 0.5
c swps; 3372.9 avg class size, 197.6 avg environment size
c swps: 0 failed, 95 impls, 45 equivs
c swp0: 148 type 0 queries, 31 unsat (20.9%), 141 sat (95.3%)
c swp1: 304 type 1 queries, 151 unsat (49.7%), 266 sat (87.5%)
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: 26101671 calls to obtain time
c tops: 63664 fixed 34%, 197 its, 5971.05 confs/it
c trds: 19 transitive reductions, 3660 removed, 35 failed
c trds: 18303 nodes, 57490 edges, 35364244 steps
c trim: 1287900 words, 4.9 MB
c trnr: 19 count, 17 bin, 1729 trn, 103157059 steps
c unhd: 20 count, 30 rounds, 62110222 steps
c unhd: 732 non-trivial sccs of average size 2.1
c unhd: 45 units, 45 bin, 0 trn, 0 lrg
c unhd: 1779 failed, 1722 stamp, 0 lits, 29 bin, 5 trn, 0 lrg
c unhd: 290592 tauts, 10311 bin 4%, 9781 trn 3%, 505 lrg 0%
c unhd: 290592 tauts, 269995 stamp 93%, 258945 red 89%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 5892094 str, 45 bin 0%, 1536 trn 0%, 5890513 lrg 100%, 5880326 red 100%
c vars: 25538 remaining 13% and 163918 removed 87% out of 189456
c vars: 63664 fixed 34%, 50096 eliminated 26%, 50158 equivalent 26%
c vsts: 16911471257 visits, 96% srch, 4% simp, 0% lkhd
c vsts: 10.8 search visits per propagation, 13741.7 per conflict
c wchs: 4285296233 pushed, 51651851 enlarged, 231 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all        1165838        775223        164403      86539159       8327490        441746
c 
c  0 0         17749   2      1209   0         0   0  28041846  32    974311  12     25843   6     0.7
c  1 5          6234   1      1078   0      2322   1   6424561   7    297082   4      8566   2     0.2
c  2 6         25053   2      9149   1      6625   4  12719561  15<   985112  12     33686   8     1.4
c  3 9         69092   6     39504   5     11640   7  15039090  17   1702605  20     77262  17     4.9
c  4 14       115144  10     79145  10     15141   9   9163842  11   1276896  15<    77601  18    12.1
c  5 21       142837  12    108268  14     16640  10   5883994   7    918759  11     60758  14<   19.9
c  6 30       156840  13    123563  16     17407  11   3429754   4    659923   8     45405  10    33.0
c  7 41       158006  14<   126749  16<    17504  11<  2306938   3    503907   6     36620   8    38.9
c  8 54       138808  12    110726  14     15971  10   1471740   2    383473   5     27026   6    55.1
c  9 69       111632  10     87668  11     14028   9    857087   1    259129   3     20417   5    56.2
c 10 86        85063   7     55346   7     14434   9    778331   1    198821   2     16116   4    22.0
c 11 126       72332   6     22413   3     12416   8    296038   0    109518   1      8314   2     5.1
c 12 230       62886   5      9803   1     18796  11    121224   0     55214   1      3963   1     6.0
c 13 534        4162   0       602   0      1479   1      5153   0      2740   0       169   0     0.8
c 
c avg                  6.9           6.7           7.3           2.4           4.1           4.9
c std                  2.7           2.2           3.1           2.4           2.7           2.7
c 
c  107.967  11% bump
c   52.741   5% probe
c   34.355   4% unhide
c   12.291   1% elim
c    7.706   1% decide
c    7.679   1% cce
c 
c   12.379 < 1% rest (below)
c 
c    3.189   0% sweep
c    2.884   0% bca
c    1.918   0% transred
c    1.792   0% block
c    1.099   0% gauss
c    0.672   0% ternres
c    0.453   0% quatres
c    0.371   0% card
c    0.000   0% locs
c    0.000   0% queuesort
c    0.000   0% rescore
c ==================================
c    2.793   0% preprocessing     2%
c  125.517  13% inprocessing     98%
c ==================================
c  128.310  13% simplifying
c  839.055  87% search
c ==================================
c  967.378 100% all
c 
c       1176297 conflicts,        1216.0 confs/sec
c          4780 ternaries,         246.1 confs/ternary
c          3416 binaries,          344.3 confs/binary
c           197 iterations,       5971.1 confs/iteration
c 
c            25 reductions,          0.0 redus/sec,  47051.9 confs/reduction
c         24753 restarts,           25.6 rests/sec,     47.5 confs/restart
c      11876279 decisions,       12276.8 decis/sec,     10.1 decis/conflict
c    1593863846 propagations,  1647612.8 props/sec,    134.2 props/decision
c 
c 967.4 seconds, 276.9 MB
c launch: done
