c launch: /data/cnf/sc2014/app/SAT_dat.k95-24_1_rule_2.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/SAT_dat.k95-24_1_rule_2.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/SAT_dat.k95-24_1_rule_2.cnf.bz2
c no embedded options
c found 'p cnf 1540071 6036162' header
c read 1540071 variables, 6036162 clauses, 15152823 literals in 0.00 seconds
c
c --abstime=0
c --bate=1
c --batewait=2
c --bca=1
c --bcaddlimldscale=2
c --bcamaxeff=10000000
c --bcaminuse=100
c --bcawait=2
c --bkwdscale=100
c --bkwdroundlim=7
c --bkwdresched=1
c --blkboost=10
c --blkboostvlim=10000000
c --blkclslim=1000000
c --blklarge=1
c --blkmaxeff=800000000
c --blkmineff=50000000
c --blkocclim1=100000
c --blkocclim=1000000
c --blkocclim2=10000
c --blkreleff=100
c --blkresched=1
c --blkrtc=0
c --blksmall=1
c --blksuccessmaxwortc=6
c --blksuccessrat=100
c --block=1
c --blockwait=1
c --boost=1
c --bumpsimp=1
c --card=1
c --cardcut=2
c --cardexpam1=3
c --cardglue=0
c --cardignused=0
c --cardmaxeff=300000000
c --cardmaxlen=1000
c --cardmineff=2000000
c --cardminlen=3
c --cardocclim1=300
c --cardocclim2=15
c --cardreleff=5
c --cardreschedint=10
c --carduse=2
c --cardwait=0
c --cce2wait=1
c --cce=3
c --cceateint=2
c --cceboost=10
c --cceboostdel=3
c --cceboostint=5
c --cceboostvlim=10000000
c --cce3wait=2
c --ccemaxround=3
c --ccemaxeff=2147483647
c --ccemineff=30000000
c --ccereleff=50
c --ccertc=0
c --ccertcint=15
c --ccertcintvlim=2000000
c --ccesuccessrat=100
c --ccewait=2
c --clim=-1
c --compact=0
c --deco=1
c --decolim=100
c --deco1opt=1
c --decompose=1
c --defragfree=50
c --defragint=10000000
c --delmax=10
c --dlim=-1
c --druplig=0
c --drupligcheck=0
c --drupligtrace=0
c --drupligtraceorig=0
c --elim=1
c --elmaxeff=800000000
c --elmblk=1
c --elmblkwait=1
c --elmboost=20
c --elmboostdel=3
c --elmboostint=5
c --elmboostvlim=4000000
c --elmclslim=1000000
c --elmfull=0
c --elmineff=20000000
c --elmlitslim=200
c --elmocclim1=1000
c --elmocclim=1000000
c --elmocclim2=100
c --elmoccsumforced=0
c --elmreleff=200
c --elmresched=0
c --elmroundlim=3
c --elmrtc=0
c --elmrtcint=10
c --elmrtcintvlim=500000
c --elmsuccessmaxwortc=4
c --elmsuccessrat=100
c --exitonabort=0
c --factmax=100000
c --factor=3
c --gauss=1
c --gaussexptrn=1
c --gaussextrall=1
c --gaussmaxeff=50000000
c --gaussmaxor=20
c --gaussmineff=2000000
c --gaussreleff=2
c --gausswait=2
c --gluekeep=4
c --gluekeepsize=15
c --gluescale=4
c --hbrdom=2
c --import=1
c --incredcint=1
c --incredconfslim=0
c --incsavevisits=0
c --inprocessing=1
c --irrlim=1
c --jwhred=1
c --keepmaxglue=1
c --keepmaxglueint=100
c --lhbr=1
c --lkhd=2
c --locs=0
c --locsbanner=0
c --locsclim=1000000
c --locsboost=2
c --locscint=10000
c --locset=2
c --locsexport=1
c --locsmaxeff=100000
c --locsmineff=1000
c --locsred=0
c --locsreleff=5
c --locsrtc=0
c --locsvared=100
c --locswait=2
c --maxscaledglue=15
c --memlim=-1
c --minimize=2
c --minlocalgluelim=200
c --minlocalsizelim=3000
c --minrecgluelim=100
c --minrecsizelim=1000
c --norestartsatlimlo=85
c --move=2
c --otfs=1
c --penmax=4
c --phase=0
c --phaseluckfactor=200
c --phaselucklim=100
c --phaseluckmaxround=10
c --phasesave=1
c --plain=0
c --plim=-1
c --poison=1
c --prbasic=1
c --prbasicmaxeff=400000000
c --prbasicmineff=1000000
c --prbasicreleff=50
c --prbasicroundlim=8
c --prbasicrtc=0
c --prbrtc=0
c --prbsimple=2
c --prbsimpleboost=10
c --prbsimpleliftdepth=2
c --prbsimplemaxeff=200000000
c --prbsimplemineff=2000000
c --prbsimplereleff=40
c --prbsimplertc=0
c --probe=1
c --promote=1
c --promotegluelim=8
c --pure=1
c --quatres=1
c --quatreswait=2
c --queuesort=1
c --queuesortjwh=0
c --randec=0
c --randecint=1000
c --redcls=1
c --redclsglue=6
c --redclsmaxdec=5
c --redclsmaxdepth=10
c --redclsmaxlrg=10
c --redclsmaxprops=100
c --redclsatlimlo=0
c --redclsatlimhi=100
c --redclsize=30
c --redclstype=4
c --reducefixed=0
c --reduceinc=1000
c --reduceinit=50000
c --reduce=1
c --restart=4
c --restartglcint=10
c --restartglclim=115
c --restartinit=0
c --restartint=5
c --restartpen=1
c --retirenb=1
c --retireint=4
c --retiremin=1
c --reusetrail=0
c --rmincpen=4
c --rstinoutinc=110
c --satlimdelay=10000
c --scincinc=200
c --scincincsatlimhi=100
c --scincincdelta=10
c --scincincincint=100000
c --scincincmin=200
c --scincincmode=1
c --score=3
c --scoreshift=0
c --scoreresetint=2147483647
c --seed=0
c --simpbintinc=100
c --simpbintinclim=10000
c --simpcintdelay=2000
c --simpcintinc=20000
c --simpcintincdiv=1
c --simpcintmaxhard=10000000
c --simpcintmaxsoft=1000000
c --simpincdelmaxfact=50
c --simpincdelmaxmin=10000
c --simpinitdelay=0
c --simpintsizepen=0
c --simpen=0
c --simpidiv=3
c --simpiscale=100
c --simpitdelay=10
c --simpitintinc=10
c --simpitintinclim=1000
c --simplify=2
c --simprtc=5
c --simptintinc=1000
c --simptintinclim=10000
c --simpvarchg=100
c --simpvarlim=100
c --sizemaxpen=5
c --sizepen=1000000
c --sleeponabort=0
c --smallirr=90
c --smallve=1
c --smallvevars=10
c --smallvewait=0
c --sortlits=0
c --subl=9
c --sweep=1
c --sweepboost=10
c --sweepboostdel=4
c --sweepboostint=7
c --sweepboostvlim=1000000
c --sweepfacdec=10
c --sweepforgive=2
c --sweepirr=3
c --sweepmaxeff=200000000
c --sweepmaxdec=10000
c --sweepmaxround=3
c --sweepmindec=100
c --sweepmineff=1000000
c --sweepred=3
c --sweepreleff=3
c --sweeprtc=0
c --sweeprtcint=14
c --sweeprtcintvlim=100000
c --sweepsuccessmaxwortc=6
c --sweepsuccessrat=1000
c --sweepwait=2
c --synclsall=1
c --synclsglue=8
c --synclsint=100
c --synclslen=40
c --syncunint=111111
c --termint=122222
c --ternres=1
c --ternresboost=5
c --ternresrtc=0
c --ternreswait=2
c --transred=1
c --transredwait=2
c --trapiflush=0
c --trdmaxeff=2000000
c --trdmineff=100000
c --trdreleff=10
c --treelook=1
c --treelookboost=10
c --treelookfull=0
c --treelookmaxeff=50000000
c --treelookmineff=300000
c --treelookreleff=2
c --treelookrtc=0
c --trep=1
c --trepint=55555
c --trnreleff=10
c --trnrmaxeff=200000000
c --trnrmineff=4000000
c --unhdatrn=2
c --unhdextstamp=1
c --unhdhbr=0
c --unhdlnpr=3
c --unhdmaxeff=20000000
c --unhdmineff=100000
c --unhdreleff=2
c --unhdroundlim=20
c --unhide=1
c --unhidewait=0
c --usedtwice=1
c --vsidsdint=256
c --wait=1
c --waitmax=4
c --witness=0
c --check=0
c --log=-1
c --profile=1
c --profilelong=1
c --verbose=1
c [freezer] frozen 0 variables out of 1492293 free variables 0%
c [limits] no decision limit
c [limits] no conflict limit
c [limits] no propagation limit
c [limits] simplification not delayed since 'simpdelay' zero
c [set-maximum-score] maximum score limit 1.000000d+500
c [set-minimum-score] minimum score limit 1.000000d-500
c [score-type] SUM (--score=3)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c *    0.0 1492293  5988250         0       0      0     0    0     0  291   0%      0    0    0    0    0%
c 
c [simplification-1] limit 0 conflicts (hard 0) hit after 0 conflicts
c [card-1] limit 1497062 based on 5988250 irredundant clauses
c [card-1] found 1424 at-most-one constraints of average size 3.0
c [card-1] no at-most-two constraint found
c [card-1] using previous limit 1497062 for elimination
c [card-1] 1424 out of 1424 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 311739 variables
c [simpleprobe-1] all 1228332 free variables schedulable
c [simpleprobe-1] boosting simple probing limit by 10
c [simpleprobe-1] limit 9996520 based on 4998260 irredundant clauses
c [decomp-2] removed 4188 variables
c [simpleprobe-1] 1088492 variables remain 89% (135652 retained 11%)
c [simpleprobe-1] removed 4188 variables, found 18917 hbrs, 622 units
c [unhide-1] limit 311069 based on 4977109 irredundant clauses
c [unhide-1-1] 1735 units, 1346 failed, 10715 tauts, 0 hbrs, 61346 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 1218766 variables 100%
c [elim-1] limit of 5000000 steps penalty 2 = 0 + 2
c [elim-1] rescheduling of touched variables disabled
c [elim-1] incomplete 1137621 not tried 93% in round 1
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 81149 = 7% variables out of 1218766 scheduled
c [elim-1] considered successful since not run to completion yet
c [phase-count-1] 4458203 negative 95.2% of 4683166 except 224963 4.8%
c [phase-count-1] 4386441 positive 93.7% of 4683166 except 296725 6.3%
c [phase-1] phase bias: 528916 positive 46%, 608701 negative 54%
c [sort-queue-1] sorted 1137617 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 1137617 (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 185236 variables 14.0% (1137617 remain 76%)
c [simplification-1] removed 1305084 irredundant clauses 21.8% (4683166 remain 78%)
c [simplification-1] maximum reduction of 22% = max (14%, 22%)
c [simplification-1] large reduction 22% >= 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   18.9 1137616  4683166         3       2     27 14344    0     0  281   0%      0    0    0    0 25451%
c i   19.0 1137352  4683166         5       2     28 14344    0     0  281   1%      0    0    0    0 25288%
c i   19.0 1137351  4683166        10       2     29 14347    0     0  281   1%      0    0    0    0 25001%
c i   19.0 1137199  4683166        12       2     29 14348    0     0  281   1%      0    0    0    0 24864%
c i   19.0 1137169  4683166        15       2     30 14349    0     0  281   1%      0    0    0    0 24747%
c i   19.1 1137132  4683166        70      40     36 14357    0     1  281  12%      0    1    1    0 23841%
c i   19.1 1137131  4683166        91      55     37 14359    0     1  282  16%      0    1    2    0 22878%
c i   19.2 1136975  4683166       109      59     37 14363    0     1  282  19%      0    1    2    0 22091%
c i   19.3 1136973  4683166       179     102     53 14373    0     1  282  18%      0    1    3    0 18213%
c i   19.3 1136972  4683166       180     102     53 14373    0     1  282  18%      0    1    3    0 18142%
c 
c [simplification-2] limit of 10 iterations hit after 10 iterations
c [decomp-3] removed 4164 variables
c [simpleprobe-2] 1008027 schedulable variables 89%
c [simpleprobe-2] limit 9343840 based on 4671920 irredundant clauses
c [decomp-4] removed 1261 variables
c [simpleprobe-2] 1000134 variables remain 88% (132058 retained 12%)
c [simpleprobe-2] removed 1261 variables, found 40568 hbrs, 159 units
c [treelook-1] limit 1166737 based on 4666951 irredundant clauses
c [treelook-1] scheduled 233113 literals 10%
c [treelook-1] scheduling used 1166809 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 1166737 based on 4666951 irredundant clauses
c [treelook-1] used 1171824 steps
c [treelook-1] 232902 literals remain 10%
c [treelook-1] 230269 variables remain to probed next time 20%
c [decomp-5] removed 126 variables
c [treelook-1] removed 131 variables, found 6039 hbrs
c [basicprobe-1] limit 37331984 based on 4666498 irredundant clauses
c [basicprobe-1-0] 1026653 probes remain 92% after last round
c [basicprobe-1-0] 5019 units = 2488 failed (50%) + 2531 lifted (50%)
c [basicprobe-1-0] removed 11254 variables, found 241340 hbrs
c [unhide-2] limit 291656 based on 4666498 irredundant clauses
c [unhide-2-2] 1006 units, 1205 failed, 14785 tauts, 0 hbrs, 44906 literals
c [elim-2] 1118423 variables 100% will be scheduled this time
c [elim-2] scheduled 1118423 variables 100%
c [elim-2] limit of 5000000 steps penalty 2 = 0 + 2
c [elim-2] rescheduling of touched variables disabled
c [elim-2] incomplete 1037407 not tried 93% in round 1
c [elim-2] transition to [ all 0 rem 1 ] state
c [elim-2] eliminated 81020 = 7% variables out of 1118423 scheduled
c [elim-2] considered successful since not run to completion yet
c [phase-count-2] 4199149 negative 95.1% of 4414367 except 215218 4.9%
c [phase-count-2] 4126345 positive 93.5% of 4414367 except 288022 6.5%
c [phase-2] phase bias: 2295 positive 31%, 5005 negative 69%
c [sort-queue-2] sorted 1035020 enqueued variables after 180 conflicts
c [score-dist-2] active 2383 (0%), one 0 (0%), zero 1035020 (100%)
c [score-dist-2] max exp 513, different 13 (3%)
c [score-dist-2] median active exp 510, avg 509.4
c [simplification-2] removed 99569 variables 8.8% (1037403 remain 70%)
c [simplification-2] removed 268799 irredundant clauses 5.7% (4414367 remain 74%)
c [simplification-2] maximum reduction of 9% = max (9%, 6%)
c [simplification-2] forced so keeping old conflict interval 0
c [simplification-2] conflict limit remains at 1028 (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   45.9 1037402  4414367       205      84     22 221963    0     2  276  14%      0    2    3    0 16887%
c i   46.3 1037362  4414367       358     189     50 221977    0     3  276  10%      0    3    3    0 12912%
c i   47.5 1037361  4414367       698     450     94 222000    1    11  277   5%      1   11    4    0 8482%
c i   48.9 1037360  4414367       879     583    124 222011    1    15  277   5%      1   15    3    0 6848%
c i   48.9 1037330  4414367       880     583    124 222011    1    15  277   5%      1   15    3    0 6822%
c 
c [simplification-3] limit 1038 conflicts (hard 11000) hit after 1038 conflicts
c [card-2] limit 1103591 based on 4414367 irredundant clauses
c [card-2] found 994 at-most-one constraints of average size 3.0
c [card-2] no at-most-two constraint found
c [card-2] using previous limit 1103591 for elimination
c [card-2] 994 out of 994 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [decomp-6] removed 6227 variables
c [treelook-2] limit 1101035 based on 4404142 irredundant clauses
c [treelook-2] scheduled 211020 literals 10%
c [treelook-2] scheduling used 1101579 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 1101035 based on 4404142 irredundant clauses
c [treelook-2] used 1110537 steps
c [treelook-2] 210902 literals remain 10%
c [treelook-2] 129641 variables remain to probed next time 13%
c [decomp-7] removed 185 variables
c [treelook-2] removed 208 variables, found 4198 hbrs
c [unhide-3] limit 275203 based on 4403254 irredundant clauses
c [unhide-3-3] 490 units, 847 failed, 23643 tauts, 0 hbrs, 20026 literals
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 1029588 variables 100%
c [elim-3] limit of 5000000 steps penalty 2 = 0 + 2
c [elim-3] rescheduling of touched variables disabled
c [elim-3] incomplete 954369 not tried 93% in round 1
c [elim-3] transition to [ all 1 rem 1 ] state
c [elim-3] eliminated 75278 = 7% variables out of 1029588 scheduled
c [elim-3] considered successful since not run to completion yet
c [phase-count-3] 3997302 negative 95.0% of 4206240 except 208938 5.0%
c [phase-count-3] 3926595 positive 93.4% of 4206240 except 279645 6.6%
c [phase-3] phase bias: 571 positive 29%, 1396 negative 71%
c [sort-queue-3] sorted 940518 enqueued variables after 1038 conflicts
c [score-dist-3] active 13792 (1%), one 0 (0%), zero 940518 (99%)
c [score-dist-3] max exp 517, different 17 (3%)
c [score-dist-3] median active exp 511, avg 511.6
c [simplification-3] removed 83014 variables 8.0% (954310 remain 64%)
c [simplification-3] removed 208127 irredundant clauses 4.7% (4206240 remain 70%)
c [simplification-3] maximum reduction of 8% = max (8%, 5%)
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 13038 (soft 3038 + delta 10000)
c [simplification-3] new conflict limit 3038 (hard 13038)
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   68.0  954309  4206240      1075     558    148 192519    1    16  268   6%      1   16    5    0 7547%
c i   68.4  954308  4206240      1183     642    156 192531    1    17  269   7%      1   17    5    0 6730%
c i   71.3  954307  4206240      1759    1053    250 192583    2    29  270   5%      3   29    5    0 4473%
c i   72.1  954305  4206240      1889    1166    260 192587    2    32  270   6%      3   31    7    0 4913%
c i   72.4  954304  4206240      1906    1180    260 192588    2    32  270   6%      2   32    7    0 4730%
c i   72.7  954302  4206240      1935    1203    264 192588    2    33  270   6%      2   32    7    0 5047%
c i   72.8  954301  4206240      1951    1217    265 192588    2    33  270   6%      2   33    7    0 4894%
c i   73.5  954300  4206240      2068    1327    269 192588    2    34  270   6%      2   34    9    0 5562%
c i   73.9  954299  4206240      2120    1372    275 192588    2    36  270   6%      2   35    8    0 4820%
c i   73.9  954298  4206240      2121    1372    275 192588    2    36  270   6%      2   35    8    0 4801%
c i   74.0  954297  4206240      2122    1372    275 192588    2    36  270   6%      2   35    8    0 4783%
c i   74.1  954296  4206240      2127    1375    276 192588    2    36  270   6%      2   35    8    0 4703%
c i   74.2  954293  4206240      2137    1380    280 192588    2    36  270   6%      2   35    8    0 4564%
c i   74.6  954292  4206240      2193    1426    285 192592    2    38  270   6%      2   37    7    0 4045%
c i   74.8  954291  4206240      2220    1448    288 192593    2    38  270   6%      2   38    7    0 3846%
c i   74.8  954290  4206240      2221    1448    288 192593    2    38  270   6%      2   38    7    0 3831%
c i   75.6  954289  4206240      2309    1516    297 192600    2    43  270   5%      2   42    6    0 3200%
c i   79.4  954288  4206240      2961    2072    347 192624    4    63  270   6%      4   62   14    0 4876%
c i   79.4  954287  4206240      2962    2072    347 192624    4    63  270   6%      4   62   14    0 4857%
c 
c [simplification-4] limit of 193 binary hit after 193 binaries
c [decomp-8] removed 1186 variables
c [basicprobe-2] limit 33629736 based on 4203717 irredundant clauses
c [basicprobe-2-0] 732228 probes remain 77% after last round
c [basicprobe-2-0] 1920 units = 1632 failed (85%) + 288 lifted (15%)
c [basicprobe-2-0] removed 3669 variables, found 166037 hbrs
c [unhide-4] limit 262732 based on 4203717 irredundant clauses
c [unhide-4-4] 323 units, 672 failed, 16244 tauts, 0 hbrs, 32908 literals
c [elim-4] 948428 variables 100% will be scheduled this time
c [elim-4] scheduled 948428 variables 100%
c [elim-4] boosting limit by 20
c [elim-4] limit of 274363390 steps penalty 2 = 0 + 2
c [elim-4] rescheduling of touched variables disabled
c [elim-4] incomplete 36304 not tried 4% in round 1
c [elim-4] transition to [ all 0 rem 1 ] state
c [elim-4] eliminated 555182 = 59% variables out of 948428 scheduled
c [elim-4] considered successful since not run to completion yet
c [phase-count-4] 2683270 negative 95.6% of 2805966 except 122696 4.4%
c [phase-count-4] 2637945 positive 94.0% of 2805966 except 168021 6.0%
c [phase-4] phase bias: 4225 positive 40%, 6359 negative 60%
c [sort-queue-4] sorted 375952 enqueued variables after 2972 conflicts
c [score-dist-4] active 17294 (4%), one 0 (0%), zero 375952 (96%)
c [score-dist-4] max exp 519, different 19 (4%)
c [score-dist-4] median active exp 514, avg 514.1
c [simplification-4] removed 561041 variables 58.8% (393246 remain 26%)
c [simplification-4] removed 1400274 irredundant clauses 33.3% (2805966 remain 47%)
c [simplification-4] maximum reduction of 59% = max (59%, 33%)
c [simplification-4] forced so keeping old conflict interval 0
c [simplification-4] conflict limit remains at 3081 (hard 13038)
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  111.7  393245  2805966      3051     559    189 80513    4    68  237   6%      3   67   15    0 4759%
c 
c [simplification-5] limit 3081 conflicts (hard 13038) hit after 3081 conflicts
c [quatres-1] found 342488 quaternary clauses 38% in total
c [quatres-1-1] removed 4 duplicate quaternary clauses
c [quatres-1-1] added 103 double-self-subsuming ternary resolvents
c [quatres-1-2] added 5020 single-self-subsuming ternary resolvents
c [quatres-1-2] added 11133 quaternary resolvents
c [ternres-1] boosting ternary resolution limit by 5
c [ternres-1] limit 11221756 based on 2805439 irredundant clauses
c [ternres-1] all 393245 free variables schedulable
c [ternres-1] 46150 ternary resolvents (81 bin, 46069 trn)
c [ternres-1] 271581 variables remain 69% (121664 retained 31%)
c [gauss-1] limit 1402719 based on 2805439 irredundant clauses
c [gauss-1] extracted 6293 xors of average arity 3.0
c [gauss-1] connected 18681 occurrences of 7540 variables (average 2.5)
c [gauss-1] limit 1402716 based on 2805433 irredundant clauses
c [gauss-1] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-9] removed 1831 variables
c [simpleprobe-3] 347006 schedulable variables 89%
c [simpleprobe-3] limit 5640066 penalty 1 = 0 + 1
c [decomp-10] removed 294 variables
c [simpleprobe-3] 348412 variables remain 89% (42708 retained 11%)
c [simpleprobe-3] removed 294 variables, found 15492 hbrs, 82 units
c [unhide-5] limit 174982 based on 2799720 irredundant clauses
c [unhide-5-5] 101 units, 245 failed, 92707 tauts, 0 hbrs, 118736 literals
c [transred-1] limit 2726235 based on 2726235 irredundant clauses
c [transred-1] removed 1109 transitive binary clauses
c [transred-1] found 20 units
c [block-1] scheduling all variables this time
c [block-1] scheduled 390669 variables 100%
c [block-1] boosting limit by 10
c [block-1] limit of 250000000 steps penalty 1 = 0 + 1
c [block-1] fully completed
c [block-1] transition to [ all 0 rem 0 ] state
c [block-1] eliminated 28700 blocked clauses
c [cce-1] limit of 15000000 steps penalty 1 = 0 + 1
c [cce-1-1] eliminated 1 clauses out of 1 (100%) of length 28
c [cce-1-1] eliminated 5 clauses out of 7 (71%) of length 27
c [cce-1-1] eliminated 2 clauses out of 6 (33%) of length 26
c [cce-1-1] eliminated 3 clauses out of 4 (75%) of length 25
c [cce-1-1] eliminated 1 clauses out of 5 (20%) of length 24
c [cce-1-1] eliminated 2 clauses out of 8 (25%) of length 23
c [cce-1-1] eliminated 11 clauses out of 18 (61%) of length 22
c [cce-1-1] eliminated 5 clauses out of 9 (56%) of length 21
c [cce-1-1] eliminated 4 clauses out of 11 (36%) of length 20
c [cce-1-1] eliminated 11 clauses out of 57 (19%) of length 19
c [cce-1-1] eliminated 346 clauses out of 1397 (25%) of length 18
c [cce-1-1] eliminated 180 clauses out of 1502 (12%) of length 17
c [cce-1-1] eliminated 269 clauses out of 819 (33%) of length 16
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 840 large clauses in 15000067 steps
c [cce-1-1] allowing another 7500033 steps for small clauses
c [cce-1-1] scheduling 1550444 clauses = 1200208 binary + 350236 ternary
c [cce-1-1] tried to eliminate 1547 small clauses 0%
c [cce-1-1] eliminated 312 binary clauses 0%
c [cce-1-1] eliminated 34 ternary clauses 0%
c [cce-1-1] eliminated 346 small clauses 0%
c [cce-1-1] eliminated 346 small clauses in 15000005 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 1186 covered clauses in round 1
c [cce-1] eliminated 1186 covered clauses in TOTAL during 1 rounds
c [cce-1] 1186 < 1/100 * 2691962 = 26919 considered unsuccessful
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 390057 variables 100%
c [elim-5] limit of 28200331 steps penalty 1 = 0 + 1
c [elim-5] rescheduling of touched variables disabled
c [elim-5] incomplete 250668 not tried 64% in round 1
c [elim-5] transition to [ all 1 rem 1 ] state
c [elim-5] eliminated 16278 = 4% variables out of 390057 scheduled
c [bca-1] limit of 10000000 steps and 5322848 added (scaled 2)
c [bca-1] 720152 out of 747560 literals actually usable 96%
c [bca-1] added 8767 blocked clauses in 2291053 steps
c [sweep-1] limit 5322348 based on 2661174 irredundant clauses
c [sweep-1-1] 118324 pos 31.7% + 255455 neg 68.3% = 373779 sched 100.0% ret 0
c [sweep-1-1] 5351067 steps 105 queries 113560.97 avg class size
c [sweep-1-1] 1598 decisions 99 SAT calls 31.23 avg env size
c [sweep-1-1] 373045 variables remain 100% (659 retained 0%)
c [decomp-11] removed 621 variables
c [sweep-1-1] removed 621 vars (0 failed, 9 eqs, 11 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 621 vars in TOTAL (1 rounds, 104 queries)
c [phase-count-5] 2543097 negative 95.6% of 2658883 except 115786 4.4%
c [phase-count-5] 2514622 positive 94.6% of 2658883 except 144261 5.4%
c [phase-5] phase bias: 1706 positive 54%, 1454 negative 46%
c [sort-queue-5] sorted 355553 enqueued variables after 3081 conflicts
c [score-dist-5] active 17605 (5%), one 0 (0%), zero 355553 (95%)
c [score-dist-5] max exp 520, different 20 (4%)
c [score-dist-5] median active exp 514, avg 514.2
c [simplification-5] removed 20087 variables 5.1% (373158 remain 25%)
c [simplification-5] removed 147083 irredundant clauses 5.2% (2658883 remain 44%)
c [simplification-5] maximum reduction of 5% = max (5%, 5%)
c [simplification-5] large reduction 5% >= 5% limit
c [simplification-5] next conflict interval 2000 = 2000/1
c [simplification-5] penalized conflict interval 2000 = 1 * 2000
c [simplification-5] hard conflict limit 15081 (soft 5081 + delta 10000)
c [simplification-5] new conflict limit 5081 (hard 15081)
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.1  373157  2658883      3144    9963  41462 93972    4    70  235   6%      3   69   13    0 3923%
c i  139.2  373156  2658882      3148    9965  41462 93972    4    70  235   6%      3   69   13    0 3888%
c i  139.2  373155  2658882      3150    9965  41462 93972    4    70  235   6%      3   69   13    0 3872%
c i  141.7  373154  2658879      4090   10773  41515 93996    7    85  235   8%      6   83   23    1 4215%
c i  141.7  373153  2658879      4118   10791  41515 93998    7    85  235   8%      6   83   23    1 4236%
c i  142.6  373150  2658878      4462   11106  41525 94002    7    84  235   9%      5   81   18    1 2869%
c 
c [simplification-6] limit 5088 conflicts (hard 15081) hit after 5088 conflicts
c [quatres-2] found 350933 quaternary clauses 40% in total
c [quatres-2-1] removed 5 duplicate quaternary clauses
c [quatres-2-1] added 59 double-self-subsuming ternary resolvents
c [quatres-2-2] added 2259 single-self-subsuming ternary resolvents
c [quatres-2-2] added 8122 quaternary resolvents
c [ternres-2] limit 10634752 based on 2658688 irredundant clauses
c [ternres-2] 257705 schedulable variables 69%
c [ternres-2] 41613 ternary resolvents (871 bin, 40742 trn)
c [ternres-2] 169650 variables remain 45% (203499 retained 55%)
c [card-3] limit 664672 based on 2658688 irredundant clauses
c [card-3] found 353 at-most-one constraints of average size 3.1
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 664672 for elimination
c [card-3] 353 out of 353 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [decomp-12] removed 290 variables
c [treelook-3] limit 664545 based on 2658183 irredundant clauses
c [treelook-3] scheduled 76399 literals 10%
c [treelook-3] scheduling used 664547 steps
c [treelook-3] not fully scheduled
c [treelook-3] limit 664545 based on 2658183 irredundant clauses
c [treelook-3] used 679396 steps
c [treelook-3] 76362 literals remain 10%
c [treelook-3] 45580 variables remain to probed next time 12%
c [decomp-13] removed 4 variables
c [treelook-3] removed 6 variables, found 849 hbrs
c [unhide-6] limit 166134 based on 2658151 irredundant clauses
c [unhide-6-6] 227 units, 596 failed, 4578 tauts, 0 hbrs, 69633 literals
c [transred-2] limit 2655310 based on 2655310 irredundant clauses
c [transred-2] removed 902 transitive binary clauses
c [transred-2] found 13 units
c [block-2] scheduling all variables this time
c [block-2] scheduled 372111 variables 100%
c [block-2] limit of 25000000 steps penalty 1 = 0 + 1
c [block-2] incomplete 10870 not tried 3%
c [block-2] transition to [ all 1 rem 1 ] state
c [block-2] eliminated 9649 blocked clauses
c [block-2] 9649 < 1/100 * 2654608 = 26546 considered unsuccessful
c [elim-6] 35549 variables 10% will be scheduled this time
c [elim-6] scheduled 35549 variables 10%
c [elim-6] limit of 39462603 steps penalty 1 = 0 + 1
c [elim-6] rescheduling of touched variables disabled
c [elim-6] incomplete 17193 not tried 5% in round 1
c [elim-6] transition to [ all 0 rem 1 ] state
c [elim-6] eliminated 331 = 1% variables out of 35549 scheduled
c [elim-6] 331 < 1/100 * 35549 = 355 considered unsuccessful
c [bca-2] limit of 10000000 steps and 5216989 added (scaled 2)
c [bca-2] 700336 out of 743368 literals actually usable 94%
c [bca-2] added 2333 blocked clauses in 2211896 steps
c [sweep-2] limit 5212106 based on 2606053 irredundant clauses
c [sweep-2-1] 117565 pos 31.7% + 253477 neg 68.3% = 371042 sched 99.8% ret 641
c [sweep-2-1] 5230466 steps 104 queries 121022.80 avg class size
c [sweep-2-1] 1333 decisions 99 SAT calls 32.97 avg env size
c [sweep-2-1] 370371 variables remain 100% (1311 retained 0%)
c [decomp-14] removed 768 variables
c [sweep-2-1] removed 768 vars (0 failed, 8 eqs, 14 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 768 vars in TOTAL (1 rounds, 103 queries)
c [phase-count-6] 2489808 negative 95.6% of 2604375 except 114567 4.4%
c [phase-count-6] 2457482 positive 94.4% of 2604375 except 146893 5.6%
c [phase-6] phase bias: 1164 positive 60%, 785 negative 40%
c [sort-queue-6] sorted 348795 enqueued variables after 5088 conflicts
c [score-dist-6] active 22120 (6%), one 0 (0%), zero 348795 (94%)
c [score-dist-6] max exp 523, different 22 (4%)
c [score-dist-6] median active exp 515, avg 515.5
c [simplification-6] removed 2234 variables 0.6% (370915 remain 25%)
c [simplification-6] removed 54503 irredundant clauses 2.0% (2604375 remain 43%)
c [simplification-6] maximum reduction of 2% = max (1%, 2%)
c [simplification-6] geometric conflict interval increment 6666 = 20000 / 3
c [simplification-6] new conflict interval 6666
c [simplification-6] penalized conflict interval 6666 = 1 * 6666
c [simplification-6] hard conflict limit 21754 (soft 11754 + delta 10000)
c [simplification-6] new conflict limit 11754 (hard 21754)
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  173.6  370914  2604375      7917   20831  77317 96389    9   129  236   7%     38  122    8    1  673%
c i  173.6  370913  2604375      7918   20831  77317 96389    9   129  236   7%     38  122    8    1  670%
c i  173.7  370912  2604375      7919   20831  77317 96389    9   129  236   7%     38  122    8    1  668%
c i  174.2  370911  2604375      8040   20944  77320 96391    9   132  236   7%     33  125   10    1  871%
c i  184.5  370910  2604375      9823   22468  77437 96432   10   154  236   6%     19  144   10    1  711%
c i  194.7  370909  2604373     11588   23998  77519 96490   12   163  236   7%     16  148   15    2  826%
c 
c [simplification-7] limit 11774 conflicts (hard 21754) hit after 11774 conflicts
c [quatres-3] found 357771 quaternary clauses 42% in total
c [quatres-3-1] removed 10 duplicate quaternary clauses
c [quatres-3-1] added 22 double-self-subsuming ternary resolvents
c [quatres-3-2] added 749 single-self-subsuming ternary resolvents
c [quatres-3-2] added 5500 quaternary resolvents
c [ternres-3] limit 10417224 based on 2604306 irredundant clauses
c [ternres-3] 168413 schedulable variables 45%
c [ternres-3] 49056 ternary resolvents (1512 bin, 47544 trn)
c [ternres-3] 97757 variables remain 26% (273152 retained 74%)
c [gauss-2] limit 1302153 based on 2604306 irredundant clauses
c [gauss-2] extracted 5385 xors of average arity 3.0
c [gauss-2] connected 16087 occurrences of 6468 variables (average 2.5)
c [gauss-2] limit 1302134 based on 2604269 irredundant clauses
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-15] removed 488 variables
c [basicprobe-3] limit 25220641 penalty 1 = 0 + 1
c [basicprobe-3-0] 240955 probes remain 66% after last round
c [basicprobe-3-0] 1959 units = 1860 failed (95%) + 99 lifted (5%)
c [basicprobe-3-0] removed 2763 variables, found 126662 hbrs
c [bate-1] eliminated 3383 asymmetric tautologies during probing
c [unhide-7] limit 252206 with penalty 3 = 0 + 3
c [unhide-7-7] 208 units, 316 failed, 42820 tauts, 0 hbrs, 36461 literals
c [transred-3] limit 2533865 based on 2533865 irredundant clauses
c [transred-3] removed 1321 transitive binary clauses
c [transred-3] found 12 units
c [cce-2] limit of 12610320 steps penalty 2 = 1 + 1
c [cce-2-1] eliminated 2 clauses out of 2 (100%) of length 26
c [cce-2-1] eliminated 8 clauses out of 10 (80%) of length 25
c [cce-2-1] eliminated 2 clauses out of 3 (67%) of length 24
c [cce-2-1] eliminated 4 clauses out of 8 (50%) of length 23
c [cce-2-1] eliminated 6 clauses out of 9 (67%) of length 22
c [cce-2-1] eliminated 5 clauses out of 11 (45%) of length 21
c [cce-2-1] eliminated 1 clauses out of 11 (9%) of length 20
c [cce-2-1] eliminated 5 clauses out of 17 (29%) of length 19
c [cce-2-1] eliminated 14 clauses out of 864 (2%) of length 18
c [cce-2-1] eliminated 15 clauses out of 1126 (1%) of length 17
c [cce-2-1] eliminated 27 clauses out of 883 (3%) of length 16
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] eliminated 89 large clauses in 12610356 steps
c [cce-2-1] allowing another 6305178 steps for small clauses
c [cce-2-1] scheduling 1387057 clauses = 1103480 binary + 283577 ternary
c [cce-2-1] tried to eliminate 2850 small clauses 0%
c [cce-2-1] eliminated 376 binary clauses 0%
c [cce-2-1] eliminated 138 ternary clauses 0%
c [cce-2-1] eliminated 514 small clauses 0%
c [cce-2-1] eliminated 5213 small clauses in 12610497 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 5302 covered clauses in round 1
c [cce-2] eliminated 5302 covered clauses in TOTAL during 1 rounds
c [cce-2] 5302 < 1/100 * 2533268 = 25332 considered unsuccessful
c [bca-3] limit of 10000000 steps and 5061982 added (scaled 2)
c [bca-3] 675534 out of 734168 literals actually usable 92%
c [bca-3] added 372 blocked clauses in 2079509 steps
c [sweep-3] limit 5055932 based on 2527966 irredundant clauses
c [sweep-3-1] 131210 pos 35.9% + 234581 neg 64.1% = 365791 sched 99.6% ret 1292
c [sweep-3-1] 5060112 steps 96 queries 116810.31 avg class size
c [sweep-3-1] 1757 decisions 98 SAT calls 41.87 avg env size
c [sweep-3-1] 365191 variables remain 99% (1878 retained 1%)
c [decomp-16] removed 3212 variables
c [sweep-3-1] removed 3212 vars (0 failed, 19 eqs, 13 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 3212 vars in TOTAL (1 rounds, 95 queries)
c [phase-count-7] 2406300 negative 95.4% of 2522391 except 116091 4.6%
c [phase-count-7] 2381543 positive 94.4% of 2522391 except 140848 5.6%
c [phase-7] phase bias: 649 positive 62%, 397 negative 38%
c [sort-queue-7] sorted 320595 enqueued variables after 11774 conflicts
c [score-dist-7] active 43276 (12%), one 0 (0%), zero 320595 (88%)
c [score-dist-7] max exp 524, different 23 (4%)
c [score-dist-7] median active exp 517, avg 516.7
c [simplification-7] removed 7038 variables 1.9% (363871 remain 24%)
c [simplification-7] removed 81982 irredundant clauses 3.1% (2522391 remain 42%)
c [simplification-7] maximum reduction of 3% = max (2%, 3%)
c [simplification-7] geometric conflict interval increment 5000 = 20000 / 4
c [simplification-7] new conflict interval 11666
c [simplification-7] penalized conflict interval 11666 = 1 * 11666
c [simplification-7] hard conflict limit 33440 (soft 23440 + delta 10000)
c [simplification-7] new conflict limit 23440 (hard 33440)
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  221.0  363870  2522388     12723   29728 110088 179013   12   159  237   8%     11  142   11    2  568%
c i  229.3  363869  2522388     13634   30479 110133 179029   22   202  239  11%      8  183  100    3 3604%
c i  231.8  363868  2522387     14039   30799 110176 179046   23   226  239  10%      6  205   41    3 1405%
c i  235.8  363867  2522387     14649   31270 110249 179092   24   258  239   9%      4  235   35    3 1096%
c i  241.6  363866  2522386     15461   31959 110318 179117   23   283  239   8%      5  257   26    3  771%
c i  241.7  363865  2522386     15462   31959 110318 179117   23   283  239   8%      5  257   26    3  768%
c i  242.1  363864  2522386     15511   31998 110321 179122   23   283  239   8%      4  258   26    3  750%
c i  242.3  363863  2522386     15542   32026 110321 179124   23   284  239   8%      4  258   25    3  737%
c i  253.6  363862  2522384     17250   33172 110387 179205   48   285  241  17%     12  252   91    6 1577%
c i  261.7  363861  2522384     19414   34973 110430 179246   45   264  241  17%     19  223   24    7  342%
c i  263.7  363860  2522384     20249   35730 110455 179257   41   240  241  17%     11  197   23    7  318%
c i  268.6  363859  2522384     21913   37294 110468 179274   39   181  241  21%     12  134   28    8  358%
c i  270.2  363858  2522384     22469   37815 110475 179274   39   165  243  24%      8  117   39    8  482%
c 
c [simplification-8] limit 23450 conflicts (hard 33440) hit after 23450 conflicts
c [quatres-4] found 355977 quaternary clauses 43% in total
c [quatres-4-1] removed 13 duplicate quaternary clauses
c [quatres-4-1] added 32 double-self-subsuming ternary resolvents
c [quatres-4-2] added 902 single-self-subsuming ternary resolvents
c [quatres-4-2] added 3310 quaternary resolvents
c [ternres-4] limit 11049593 with penalty 1 = 0 + 1
c [ternres-4] 95733 schedulable variables 26%
c [ternres-4] 52291 ternary resolvents (2203 bin, 50088 trn)
c [ternres-4] 32061 variables remain 9% (331791 retained 91%)
c [decomp-17] removed 742 variables
c [simpleprobe-4] 323326 schedulable variables 89%
c [simpleprobe-4] limit 44198373 penalty 1 = 0 + 1
c [decomp-18] removed 2737 variables
c [simpleprobe-4] 248473 variables remain 69% (111919 retained 31%)
c [simpleprobe-4] removed 2737 variables, found 98443 hbrs, 503 units
c [unhide-8] limit 552479 with penalty 3 = 0 + 3
c [unhide-8-8] 236 units, 387 failed, 27156 tauts, 0 hbrs, 50903 literals
c [transred-4] limit 2499572 based on 2499572 irredundant clauses
c [transred-4] removed 1514 transitive binary clauses
c [transred-4] found 14 units
c [block-3] 10734 variables 3% will be scheduled this time
c [block-3] scheduled 10734 variables 3%
c [block-3] limit of 55247967 steps penalty 2 = 1 + 1
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 31 blocked clauses
c [block-3] 31 < 1/100 * 2498923 = 24989 considered unsuccessful
c [elim-7] scheduling all variables this time
c [elim-7] scheduled 359735 variables 100%
c [elim-7] limit of 110495934 steps penalty 2 = 1 + 1
c [elim-7] rescheduling of touched variables disabled
c [elim-7] incomplete 52170 not tried 15% in round 1
c [elim-7] transition to [ all 1 rem 1 ] state
c [elim-7] eliminated 17418 = 5% variables out of 359735 scheduled
c [bca-4] limit of 10000000 steps and 4878134 added (scaled 2)
c [bca-4] 619776 out of 684636 literals actually usable 91%
c [bca-4] added 783 blocked clauses in 1934590 steps
c [sweep-4] limit 4871898 based on 2435949 irredundant clauses
c [sweep-4-1] 130983 pos 38.5% + 209575 neg 61.5% = 340558 sched 99.5% ret 1759
c [sweep-4-1] 4908055 steps 98 queries 106265.56 avg class size
c [sweep-4-1] 1440 decisions 101 SAT calls 38.22 avg env size
c [sweep-4-1] 340110 variables remain 99% (2204 retained 1%)
c [decomp-19] removed 684 variables
c [sweep-4-1] removed 684 vars (0 failed, 1 eqs, 2 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 684 vars in TOTAL (1 rounds, 97 queries)
c [phase-count-8] 2319815 negative 95.3% of 2434030 except 114215 4.7%
c [phase-count-8] 2299244 positive 94.5% of 2434030 except 134786 5.5%
c [phase-8] phase bias: 314 positive 43%, 408 negative 57%
c [sort-queue-8] sorted 275999 enqueued variables after 23450 conflicts
c [score-dist-8] active 65634 (19%), one 0 (0%), zero 275999 (81%)
c [score-dist-8] max exp 528, different 27 (5%)
c [score-dist-8] median active exp 518, avg 518.6
c [simplification-8] removed 22219 variables 6.1% (341633 remain 23%)
c [simplification-8] removed 88353 irredundant clauses 3.5% (2434030 remain 41%)
c [simplification-8] maximum reduction of 6% = max (6%, 4%)
c [simplification-8] large reduction 6% >= 5% limit
c [simplification-8] next conflict interval 2000 = 2000/1
c [simplification-8] penalized conflict interval 2000 = 1 * 2000
c [simplification-8] hard conflict limit 35450 (soft 25450 + delta 10000)
c [simplification-8] new conflict limit 25450 (hard 35450)
c 
c [simplification-9] limit 25450 conflicts (hard 35450) hit after 25451 conflicts
c [quatres-5] found 359295 quaternary clauses 43% in total
c [quatres-5-1] removed 204 duplicate quaternary clauses
c [quatres-5-1] added 17 double-self-subsuming ternary resolvents
c [quatres-5-2] added 1904 single-self-subsuming ternary resolvents
c [quatres-5-2] added 5240 quaternary resolvents
c [ternres-5] limit 11955770 with penalty 1 = 0 + 1
c [ternres-5] 29976 schedulable variables 9%
c [ternres-5] 62930 ternary resolvents (2194 bin, 60736 trn)
c [ternres-5] 6640 variables remain 2% (334993 retained 98%)
c [decomp-20] removed 617 variables
c [treelook-4] limit 1195577 penalty 1 = 0 + 1 boost 1
c [treelook-4] scheduled 109144 literals 16%
c [treelook-4] scheduling used 1195648 steps
c [treelook-4] not fully scheduled
c [treelook-4] limit 1195577 penalty 1 = 0 + 1 boost 1
c [treelook-4] used 1199539 steps
c [treelook-4] 108991 literals remain 16%
c [treelook-4] 39637 variables remain to probed next time 12%
c [decomp-21] removed 9 variables
c [treelook-4] removed 19 variables, found 1527 hbrs
c [unhide-9] limit 597788 with penalty 3 = 0 + 3
c [unhide-9-9] 74 units, 199 failed, 25492 tauts, 0 hbrs, 25672 literals
c [transred-5] limit 2412484 based on 2412484 irredundant clauses
c [transred-5] removed 1350 transitive binary clauses
c [transred-5] found 12 units
c [elim-8] 16629 variables 5% will be scheduled this time
c [elim-8] scheduled 16629 variables 5%
c [elim-8] boosting limit by 20
c [elim-8] limit of 4782308380 steps penalty 1 = 0 + 1
c [elim-8] rescheduling of touched variables disabled
c [elim-8-1] eliminated 15 variables 0% in round 1 in 717113576 steps
c [elim-8-1] backward subsumption/strengthening limit 717113500
c [elim-8-1-1] backward checking 63221 touched variables 19%
c [elim-8-1-1] fully completed backward checking in 1 rounds
c [elim-8-1] subsumed 1626 and strengthened 4085 clauses in 133046560 steps
c [elim-8-1] rescheduled 12261 variables 4% by backward subsumption
c [elim-8-2] eliminated 425 variables 0% in round 2 in 169596962 steps
c [elim-8-2] backward subsumption/strengthening limit 169596900
c [elim-8-2-1] backward checking 10291 touched variables 3%
c [elim-8-2-1] fully completed backward checking in 1 rounds
c [elim-8-2] subsumed 261 and strengthened 449 clauses in 30166780 steps
c [elim-8-2] rescheduled 2190 variables 1% by backward subsumption
c [elim-8-3] eliminated 96 variables 0% in round 3 in 44338259 steps
c [elim-8-3] backward subsumption/strengthening limit 44338200
c [elim-8-3-1] backward checking 1335 touched variables 0%
c [elim-8-3-1] fully completed backward checking in 1 rounds
c [elim-8-3] subsumed 78 and strengthened 45 clauses in 5714392 steps
c [elim-8] incomplete 408 not tried 0% in round 3
c [elim-8] transition to [ all 0 rem 1 ] state
c [elim-8] eliminated 660 = 4% variables out of 16629 scheduled
c [elim-8] 660 < 1/100 * 16629 = 166 considered unsuccessful
c [bca-5] limit of 10000000 steps and 4754725 added (scaled 2)
c [bca-5] 608567 out of 680052 literals actually usable 89%
c [bca-5] added 799 blocked clauses in 1898506 steps
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 35867310 penalty 1 = 0 + 1
c [sweep-5-1] 131392 pos 38.9% + 206456 neg 61.1% = 337848 sched 99.4% ret 2177
c [sweep-5-1] 35873330 steps 707 queries 61985.34 avg class size
c [sweep-5-1] 9135 decisions 652 SAT calls 35.22 avg env size
c [sweep-5-1] 332335 variables remain 98% (7645 retained 2%)
c [decomp-22] removed 825 variables
c [sweep-5-1] removed 825 vars (0 failed, 111 eqs, 164 impls)
c [sweep-5] considered successful since not run to completion yet
c [sweep-5] removed 825 vars in TOTAL (1 rounds, 706 queries)
c [phase-count-9] 2257696 negative 95.2% of 2371466 except 113770 4.8%
c [phase-count-9] 2237993 positive 94.4% of 2371466 except 133473 5.6%
c [phase-9] phase bias: 145 positive 61%, 91 negative 39%
c [sort-queue-9] sorted 270335 enqueued variables after 25451 conflicts
c [score-dist-9] active 68865 (20%), one 0 (0%), zero 270335 (80%)
c [score-dist-9] max exp 528, different 27 (5%)
c [score-dist-9] median active exp 519, avg 518.8
c [simplification-9] removed 2433 variables 0.7% (339200 remain 23%)
c [simplification-9] removed 62560 irredundant clauses 2.6% (2371466 remain 40%)
c [simplification-9] maximum reduction of 3% = max (1%, 3%)
c [simplification-9] geometric conflict interval increment 5000 = 20000 / 4
c [simplification-9] new conflict interval 16666
c [simplification-9] penalized conflict interval 16666 = 1 * 16666
c [simplification-9] hard conflict limit 52117 (soft 42117 + delta 10000)
c [simplification-9] new conflict limit 42117 (hard 52117)
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  349.1  339199  2371466     26399   42019 162202 219014   28   147  239  19%     41   92   23    9  254%
c i  349.3  339198  2371466     26454   42071 162203 219015   28   146  239  19%     39   91   21    9  232%
c i  359.0  339197  2371466     28099   43631 162226 219028   26   140  240  19%     17   83   11    9  122%
c 
c [simplification-10] limit 42117 conflicts (hard 52117) hit after 42117 conflicts
c [quatres-6] found 354101 quaternary clauses 44% in total
c [quatres-6-1] removed 68 duplicate quaternary clauses
c [quatres-6-1] added 17 double-self-subsuming ternary resolvents
c [quatres-6-2] added 611 single-self-subsuming ternary resolvents
c [quatres-6-2] added 2776 quaternary resolvents
c [ternres-6] limit 25264994 with penalty 1 = 0 + 1
c [ternres-6] 6533 schedulable variables 2%
c [ternres-6] 93981 ternary resolvents (3129 bin, 90852 trn)
c [ternres-6] 275 variables remain 0% (338922 retained 100%)
c [card-4] limit 1579062 penalty 4 = 3 + 1
c [card-4] found 857 at-most-one constraints of average size 3.1
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 1579062 for elimination
c [card-4] 857 out of 857 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [gauss-3] limit 1263249 penalty 3 = 2 + 1
c [gauss-3] extracted 3983 xors of average arity 3.0
c [gauss-3] connected 11878 occurrences of 3760 variables (average 3.2)
c [gauss-3] limit 1263249 penalty 3 = 2 + 1
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-23] removed 638 variables
c [basicprobe-4] limit 126324972 penalty 1 = 0 + 1
c [basicprobe-4-0] 79905 probes remain 24% after last round
c [basicprobe-4-0] 8532 units = 7950 failed (93%) + 582 lifted (7%)
c [basicprobe-4-0] removed 10747 variables, found 313103 hbrs
c [bate-2] eliminated 5874 asymmetric tautologies during probing
c [unhide-10] limit 1263249 with penalty 3 = 0 + 3
c [unhide-10-10] 175 units, 446 failed, 67908 tauts, 0 hbrs, 84994 literals
c [transred-6] limit 2239385 based on 2239385 irredundant clauses
c [transred-6] removed 2013 transitive binary clauses
c [transred-6] found 8 units
c [cce-3] limit of 31581243 steps penalty 3 = 2 + 1
c [cce-3-1] eliminated 1 clauses out of 4 (25%) of length 21
c [cce-3-1] eliminated 3 clauses out of 7 (43%) of length 19
c [cce-3-1] eliminated 25 clauses out of 816 (3%) of length 18
c [cce-3-1] eliminated 43 clauses out of 688 (6%) of length 17
c [cce-3-1] eliminated 41 clauses out of 479 (9%) of length 16
c [cce-3-1] eliminated 88 clauses out of 1243 (7%) of length 15
c [cce-3-1] eliminated 462 clauses out of 1791 (26%) of length 14
c [cce-3-1] eliminated 892 clauses out of 4604 (19%) of length 13
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 1555 large clauses in 31581247 steps
c [cce-3-1] allowing another 15790623 steps for small clauses
c [cce-3-1] scheduling 1213360 clauses = 952543 binary + 260817 ternary
c [cce-3-1] tried to eliminate 5669 small clauses 0%
c [cce-3-1] eliminated 1250 binary clauses 0%
c [cce-3-1] eliminated 362 ternary clauses 0%
c [cce-3-1] eliminated 1612 small clauses 0%
c [cce-3-1] eliminated 5357 small clauses in 31581246 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 6912 covered clauses in round 1
c [cce-3] eliminated 6912 covered clauses in TOTAL during 1 rounds
c [cce-3] 6912 < 1/100 * 2238659 = 22386 considered unsuccessful
c [bca-6] limit of 10000000 steps and 4470521 added (scaled 2)
c [bca-6] 572559 out of 654770 literals actually usable 87%
c [bca-6] added 913 blocked clauses in 1719192 steps
c [sweep-6] limit 7579498 penalty 1 = 0 + 1
c [sweep-6-1] 126338 pos 39.5% + 193768 neg 60.5% = 320106 sched 97.8% ret 7278
c [sweep-6-1] 7585748 steps 155 queries 88465.47 avg class size
c [sweep-6-1] 2360 decisions 147 SAT calls 43.88 avg env size
c [sweep-6-1] 318872 variables remain 97% (8510 retained 3%)
c [decomp-24] removed 8474 variables
c [sweep-6-1] removed 8474 vars (0 failed, 11 eqs, 12 impls)
c [sweep-6] considered successful since not run to completion yet
c [sweep-6] removed 8474 vars in TOTAL (1 rounds, 154 queries)
c [phase-count-10] 2101524 negative 94.8% of 2216231 except 114707 5.2%
c [phase-count-10] 2081968 positive 93.9% of 2216231 except 134263 6.1%
c [phase-10] phase bias: 134 positive 62%, 83 negative 38%
c [sort-queue-10] sorted 234017 enqueued variables after 42117 conflicts
c [score-dist-10] active 84893 (27%), one 0 (0%), zero 234017 (73%)
c [score-dist-10] max exp 529, different 27 (5%)
c [score-dist-10] median active exp 520, avg 520.5
c [simplification-10] removed 20287 variables 6.0% (318910 remain 21%)
c [simplification-10] removed 155235 irredundant clauses 6.5% (2216231 remain 37%)
c [simplification-10] maximum reduction of 7% = max (6%, 7%)
c [simplification-10] large reduction 7% >= 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 54117 (soft 44117 + delta 10000)
c [simplification-10] new conflict limit 44117 (hard 54117)
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  528.2  318909  2216231     43699   54572 161267 338164  162   290  249  56%    200  191  278   31  888%
c i  528.8  318908  2216231     43787   54626 161280 338182  159   294  249  54%    181  195  199   31  637%
c 
c [simplification-11] limit 44117 conflicts (hard 54117) hit after 44118 conflicts
c [quatres-7] found 340990 quaternary clauses 45% in total
c [quatres-7-1] removed 227 duplicate quaternary clauses
c [quatres-7-1] added 41 double-self-subsuming ternary resolvents
c [quatres-7-2] added 1003 single-self-subsuming ternary resolvents
c [quatres-7-2] added 2696 quaternary resolvents
c [ternres-7] limit 27756531 with penalty 1 = 0 + 1
c [ternres-7] 254 schedulable variables 0%
c [ternres-7] 72849 ternary resolvents (1776 bin, 71073 trn)
c [ternres-7] 8 variables remain 0% (318900 retained 100%)
c [decomp-25] removed 487 variables
c [simpleprobe-5] 217871 schedulable variables 68%
c [simpleprobe-5] limit 100000000 penalty 1 = 0 + 1
c [decomp-26] removed 4957 variables
c [simpleprobe-5] 133286 variables remain 43% (180180 retained 57%)
c [simpleprobe-5] removed 4957 variables, found 164077 hbrs, 631 units
c [unhide-11] limit 1387826 with penalty 3 = 0 + 3
c [unhide-11-11] 53 units, 107 failed, 22360 tauts, 0 hbrs, 28918 literals
c [transred-7] limit 2164584 based on 2164584 irredundant clauses
c [transred-7] removed 1885 transitive binary clauses
c [transred-7] found 8 units
c [block-4] scheduling all variables this time
c [block-4] scheduled 313323 variables 100%
c [block-4] limit of 69391329 steps penalty 3 = 2 + 1
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 22295 blocked clauses
c [elim-9] scheduling all variables this time
c [elim-9] scheduled 312617 variables 100%
c [elim-9] limit of 200000000 steps penalty 2 = 1 + 1
c [elim-9] rescheduling of touched variables disabled
c [elim-9] incomplete 7546 not tried 2% in round 1
c [gc-82] reconnected 471917 binary clauses (produced 0 empty 1 units)
c [elim-9] transition to [ all 1 rem 1 ] state
c [elim-9] eliminated 18597 = 6% variables out of 312617 scheduled
c [bca-7] limit of 10000000 steps and 4156189 added (scaled 2)
c [bca-7] 513284 out of 588042 literals actually usable 87%
c [bca-7] added 1855 blocked clauses in 1605520 steps
c [sweep-7] limit 8326959 penalty 1 = 0 + 1
c [sweep-7-1] 111151 pos 38.9% + 174920 neg 61.1% = 286071 sched 97.3% ret 7949
c [sweep-7-1] 8350724 steps 191 queries 77743.22 avg class size
c [sweep-7-1] 2717 decisions 182 SAT calls 37.17 avg env size
c [sweep-7-1] 284721 variables remain 97% (9293 retained 3%)
c [decomp-27] removed 610 variables
c [sweep-7-1] removed 610 vars (0 failed, 32 eqs, 31 impls)
c [sweep-7] removed 610 vars in TOTAL (1 rounds, 190 queries)
c [phase-count-11] 1967468 negative 94.9% of 2072585 except 105117 5.1%
c [phase-count-11] 1945387 positive 93.9% of 2072585 except 127198 6.1%
c [phase-count-11] skipping relative phase luck test
c [phase-11] phase bias: 72 positive 45%, 89 negative 55%
c [sort-queue-11] sorted 212405 enqueued variables after 44118 conflicts
c [score-dist-11] active 81005 (28%), one 0 (0%), zero 212405 (72%)
c [score-dist-11] max exp 530, different 26 (5%)
c [score-dist-11] median active exp 521, avg 520.8
c [simplification-11] removed 25498 variables 8.0% (293410 remain 20%)
c [simplification-11] removed 143646 irredundant clauses 6.5% (2072585 remain 35%)
c [simplification-11] maximum reduction of 8% = max (8%, 6%)
c [simplification-11] large reduction 8% >= 5% limit
c [simplification-11] next conflict interval 2000 = 2000/1
c [simplification-11] penalized conflict interval 2000 = 1 * 2000
c [simplification-11] hard conflict limit 56118 (soft 46118 + delta 10000)
c [simplification-11] new conflict limit 46118 (hard 56118)
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  558.7  293409  2072585     44138   45998 169764 420314  147   307  229  48%    120  207   64   31  206%
c i  559.2  293408  2072585     44234   46089 169767 420315  144   313  230  46%    107  212   47   31  150%
c i  559.3  293407  2072585     44238   46091 169767 420315  144   313  230  46%    106  212   46   31  148%
c i  559.3  293406  2072585     44239   46091 169767 420315  144   313  230  46%    106  212   46   31  148%
c i  559.3  293405  2072585     44242   46093 169767 420315  144   313  230  46%    106  212   45   31  146%
c i  559.4  293404  2072585     44249   46096 169770 420315  143   313  230  46%    105  212   44   31  143%
c i  559.5  293403  2072585     44250   46096 169770 420315  143   313  230  46%    105  212   44   31  142%
c i  561.2  293402  2072585     45286   47052 169807 420331  114   373  230  31%     25  268   15   31   49%
c i  561.5  293401  2072585     45501   47255 169811 420332  110   381  230  29%     14  275   17   31   57%
c i  561.6  293400  2072585     45548   47297 169811 420334  109   383  230  28%     12  277   19   31   61%
c i  561.7  293399  2072585     45714   47450 169817 420335  105   388  230  27%      6  281   16   31   53%
c i  561.8  293398  2072585     45715   47450 169817 420335  105   387  230  27%      6  281   16   31   53%
c i  562.8  293397  2072585     46505   48189 169844 420343   90   404  230  22%    -10  294   23   31   76%
c i  562.9  293396  2072585     46619   48298 169844 420345   88   405  230  22%    -12  295   23   31   75%
c i  563.3  293395  2072585     46909   48572 169854 420350   84   408  230  21%    -16  296   24   31   79%
c i  563.3  293394  2072585     46911   48572 169854 420351   84   408  230  21%    -16  296   24   31   78%
c i  563.4  293393  2072585     46928   48587 169855 420351   84   408  230  21%    -16  296   25   31   81%
c i  563.7  293392  2072585     47195   48846 169856 420355   80   408  230  20%    -18  295   30   31   97%
c i  564.2  293391  2072585     47448   49072 169864 420361   77   407  230  19%    -20  292   28   31   90%
c i  564.3  293390  2072585     47474   49095 169865 420362   77   406  230  19%    -21  292   27   31   89%
c i  564.4  293389  2072585     47509   49126 169866 420363   77   406  230  19%    -21  291   27   31   88%
c i  564.7  293388  2072585     47627   49229 169873 420368   75   404  230  19%    -22  289   23   31   77%
c i  566.1  293387  2072585     48094   49652 169889 420381   69   402  231  17%    -23  285   24   30   78%
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  567.1  293386  2072584     48426   49940 169907 420395   65   405  231  16%    -24  286   16   30   52%
c i  567.1  293385  2072584     48431   49943 169907 420395   65   405  231  16%    -24  286   16   30   52%
c i  567.1  293384  2072584     48451   49960 169907 420395   65   404  231  16%    -24  286   17   30   55%
c i  567.2  293383  2072584     48452   49960 169907 420395   65   404  231  16%    -24  286   17   30   55%
c i  567.2  293382  2072584     48468   49973 169908 420395   64   404  231  16%    -24  285   16   30   53%
c i  567.2  293381  2072584     48470   49973 169909 420395   64   404  231  16%    -24  285   16   30   53%
c i  567.3  293380  2072584     48491   49987 169912 420397   64   404  231  16%    -24  285   16   30   51%
c i  567.6  293379  2072584     48628   50108 169916 420404   62   403  231  15%    -25  284   14   30   46%
c i  568.8  293378  2072584     49257   50684 169943 420415   56   408  231  14%    -24  286   14   30   46%
c i  569.1  293377  2072584     49367   50790 169942 420416   55   407  231  13%    -25  284   17   30   56%
c i  569.1  293376  2072584     49398   50819 169942 420416   54   406  231  13%    -25  283   18   30   60%
c i  570.0  293246  2072584     49868   51259 169955 420424   51   401  231  13%    -25  276   23   30   78%
c i  570.3  293245  2072583     50011   51386 169965 420426   50   399  231  13%    -25  274   22   30   74%
c i  570.3  293244  2072583     50024   51393 169965 420431   50   399  231  13%    -25  274   22   30   71%
c i  570.5  293243  2072583     50129   51488 169968 420433   49   397  231  12%    -25  271   22   30   74%
c i  574.5  293240  2072583     51699   52902 170040 420475   40   446  231   9%    -16  314   12   30   42%
c i  574.5  293239  2072583     51764   52963 170042 420475   39   453  231   9%    -16  320   12   30   42%
c i  575.1  293238  2072583     52169   53323 170064 420480   37   485  231   8%    -19  350   16   30   52%
c i  575.9  293237  2072583     52447   53551 170083 420502   35   498  231   7%    -21  362   13   30   44%
c i  576.1  293236  2072582     52531   53625 170089 420502   35   501  231   7%    -21  365   12   30   41%
c i  578.1  293235  2072582     53446   54426 170146 420525   31   518  231   6%    -20  376   15   29   51%
c i  578.3  293234  2072582     53499   54469 170153 420527   30   520  231   6%    -20  377   13   29   46%
c i  578.5  293233  2072582     53579   54545 170153 420528   30   521  231   6%    -21  378   13   29   45%
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  579.1  293232  2072582     53808   54746 170168 420535   29   522  231   6%    -22  378   12   29   43%
c i  580.3  293231  2072582     54307   55197 170192 420541   28   521  231   5%    -22  374   17   29   59%
c 
c [simplification-12] limit 46176 conflicts (hard 56118) hit after 56119 conflicts
c [quatres-8] found 335271 quaternary clauses 45% in total
c [quatres-8-1] removed 728 duplicate quaternary clauses
c [quatres-8-1] added 37 double-self-subsuming ternary resolvents
c [quatres-8-2] added 771 single-self-subsuming ternary resolvents
c [quatres-8-2] added 4474 quaternary resolvents
c [ternres-8] limit 30683486 with penalty 1 = 0 + 1
c [ternres-8] 7 schedulable variables 0%
c [ternres-8] 20276 ternary resolvents (377 bin, 19899 trn)
c [ternres-8] fully completed ternary resolution
c [decomp-28] removed 304 variables
c [treelook-5] limit 3068348 penalty 1 = 0 + 1 boost 1
c [treelook-5] scheduled 178900 literals 31%
c [treelook-5] scheduling used 3068350 steps
c [treelook-5] not fully scheduled
c [treelook-5] limit 3068348 penalty 1 = 0 + 1 boost 1
c [treelook-5] used 3075795 steps
c [treelook-5] 178587 literals remain 30%
c [treelook-5] 32302 variables remain to probed next time 11%
c [decomp-29] removed 20 variables
c [treelook-5] removed 43 variables, found 2858 hbrs
c [unhide-12] limit 1534174 with penalty 3 = 0 + 3
c [unhide-12-12] 152 units, 212 failed, 43702 tauts, 0 hbrs, 39191 literals
c [transred-8] limit 2068616 based on 2068616 irredundant clauses
c [transred-8] removed 1915 transitive binary clauses
c [transred-8] found 3 units
c [elim-10] no untried remaining variables left
c [elim-10] scheduled 292677 variables 100%
c [elim-10] limit of 400000000 steps penalty 1 = 0 + 1
c [elim-10] rescheduling of touched variables disabled
c [elim-10] incomplete 1667 not tried 1% in round 1
c [elim-10] transition to [ all 1 rem 1 ] state
c [elim-10] eliminated 5168 = 2% variables out of 292677 scheduled
c [bca-8] limit of 10000000 steps and 4082929 added (scaled 2)
c [bca-8] 494527 out of 575020 literals actually usable 86%
c [bca-8] added 979 blocked clauses in 1551505 steps
c [sweep-8] limit 9205045 penalty 1 = 0 + 1
c [sweep-8-1] 108337 pos 38.9% + 170103 neg 61.1% = 278440 sched 96.8% ret 9069
c [sweep-8-1] 9217439 steps 214 queries 68985.48 avg class size
c [sweep-8-1] 2928 decisions 198 SAT calls 37.53 avg env size
c [sweep-8-1] 276837 variables remain 96% (10666 retained 4%)
c [decomp-30] removed 767 variables
c [sweep-8-1] removed 767 vars (0 failed, 41 eqs, 62 impls)
c [sweep-8] removed 767 vars in TOTAL (1 rounds, 213 queries)
c [phase-count-12] 1931463 negative 94.9% of 2035566 except 104103 5.1%
c [phase-count-12] 1910460 positive 93.9% of 2035566 except 125106 6.1%
c [phase-count-12] skipping relative phase luck test
c [phase-12] phase bias: 29 positive 36%, 51 negative 64%
c [sort-queue-12] sorted 203840 enqueued variables after 56119 conflicts
c [score-dist-12] active 82902 (29%), one 0 (0%), zero 203840 (71%)
c [score-dist-12] max exp 530, different 26 (5%)
c [score-dist-12] median active exp 521, avg 521.0
c [simplification-12] removed 6489 variables 2.2% (286742 remain 19%)
c [simplification-12] removed 37016 irredundant clauses 1.8% (2035566 remain 34%)
c [simplification-12] maximum reduction of 2% = max (2%, 2%)
c [simplification-12] geometric conflict interval increment 6666 = 20000 / 3
c [simplification-12] new conflict interval 23332
c [simplification-12] penalized conflict interval 23332 = 1 * 23332
c [simplification-12] hard conflict limit 91117 (soft 79451 + delta 11666)
c [simplification-12] new conflict limit 79451 (hard 91117)
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  610.3  286741  2035566     56219   56751 166617 368577   23   497  229   5%    -10  340   16   29   54%
c i  620.4  286740  2035566     59011   59260 166725 368633   20   471  229   4%      3  300   20   28   72%
c i  624.2  286739  2035566     60381   60500 166794 368651   19   489  229   4%     -9  312   20   28   71%
c i  626.9  286738  2035566     60922   60996 166820 368657   19   475  229   4%    -14  296   19   28   67%
c i  627.2  286737  2035566     61035   61102 166821 368660   20   470  229   4%    -15  289   23   28   81%
c i  627.4  286736  2035566     61095   61156 166822 368662   20   468  229   4%    -16  287   21   28   74%
c i  627.7  286735  2035566     61177   61221 166830 368665   19   467  229   4%    -17  286   18   28   64%
c i  628.3  286734  2035566     61313   61351 166832 368666   20   466  229   4%    -18  284   21   28   75%
c i  628.7  286733  2035566     61431   61458 166833 368671   20   463  229   4%    -18  282   21   28   76%
c i  629.0  286732  2035566     61526   61549 166833 368671   20   463  229   4%    -19  280   20   28   73%
c i  631.0  286731  2035566     62060   62043 166850 368680   20   446  229   5%    -20  262   26   28   93%
c i  634.8  286480  2035566     63016   62949 166865 368687   22   426  229   5%    -18  238   32   28  116%
c i  660.8  286010  2035565     68448   66881 166934 368734   97   311  232  31%     43  111  220   33  656%
c i  660.8  286009  2035565     68449   66881 166934 368734   97   311  232  31%     43  111  219   33  654%
c i  665.8  286008  2035565     69442   67737 166957 368742   82   316  232  26%      5  114   15   33   45%
c 
c [simplification-13] limit 79461 conflicts (hard 91117) hit after 79461 conflicts
c [quatres-9] found 334527 quaternary clauses 46% in total
c [quatres-9-1] removed 44 duplicate quaternary clauses
c [quatres-9-1] added 32 double-self-subsuming ternary resolvents
c [quatres-9-2] added 281 single-self-subsuming ternary resolvents
c [quatres-9-2] added 2145 quaternary resolvents
c [ternres-9] limit 38946767 with penalty 1 = 0 + 1
c [ternres-9] all 286008 free variables schedulable
c [ternres-9] 36932 ternary resolvents (760 bin, 36172 trn)
c [ternres-9] 14282 variables remain 5% (271726 retained 95%)
c [decomp-31] removed 1300 variables
c [basicprobe-5] limit 194733838 penalty 1 = 0 + 1
c [basicprobe-5-0] 69014 sched 25%, 3727 failed, 213 lifted, 123377 hbrs
c [decomp-32] removed 12800 variables
c [basicprobe-5-1] 83322 probes remain 31% after last round
c [basicprobe-5-1] 6163 units = 5804 failed (94%) + 359 lifted (6%)
c [basicprobe-5-1] removed 16813 variables, found 179919 hbrs
c [bate-3] eliminated 7880 asymmetric tautologies during probing
c [unhide-13] limit 1947338 with penalty 3 = 0 + 3
c [unhide-13-13] 83 units, 187 failed, 25267 tauts, 0 hbrs, 46260 literals
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 2231 transitive binary clauses
c [transred-9] found 1 units
c [block-5] scheduling all variables this time
c [block-5] scheduled 268322 variables 100%
c [block-5] limit of 389467677 steps penalty 1 = 1 + 0
c [block-5] fully completed
c [block-5] transition to [ all 0 rem 0 ] state
c [block-5] eliminated 10192 blocked clauses
c [block-5] 10192 < 1/100 * 1863504 = 18635 considered unsuccessful
c [elim-11] 1664 variables 1% will be scheduled this time
c [elim-11] scheduled 1664 variables 1%
c [elim-11] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-11] rescheduling of touched variables disabled
c [elim-11-1] no variable eliminated in round 1 in 279149987 steps
c [elim-11] fully completed in 1 rounds
c [elim-11] transition to [ all 0 rem 0 ] state
c [elim-11] eliminated 2 = 0% variables out of 1664 scheduled
c [elim-11] 2 < 1/100 * 1664 = 16 considered unsuccessful
c [bca-9] limit of 10000000 steps and 3701698 added (scaled 2)
c [bca-9] 456098 out of 535754 literals actually usable 85%
c [bca-9] added 541 blocked clauses in 1420621 steps
c [sweep-9] limit 23368060 penalty 0 = 0 + 0
c [sweep-9-1] 98117 pos 38.0% + 159757 neg 62.0% = 257874 sched 96.3% ret 10002
c [sweep-9-1] 23373238 steps 543 queries 45809.70 avg class size
c [sweep-9-1] 7593 decisions 507 SAT calls 37.18 avg env size
c [sweep-9-1] 253186 variables remain 95% (14668 retained 5%)
c [decomp-33] removed 3226 variables
c [sweep-9-1] removed 3226 vars (0 failed, 99 eqs, 134 impls)
c [sweep-9] removed 3226 vars in TOTAL (1 rounds, 542 queries)
c [phase-count-13] 1742031 negative 94.7% of 1839230 except 97199 5.3%
c [phase-count-13] 1718574 positive 93.4% of 1839230 except 120656 6.6%
c [phase-count-13] skipping relative phase luck test
c [phase-13] phase bias: 69 positive 62%, 43 negative 38%
c [sort-queue-13] sorted 182680 enqueued variables after 79461 conflicts
c [score-dist-13] active 81970 (31%), one 0 (0%), zero 182680 (69%)
c [score-dist-13] max exp 531, different 26 (5%)
c [score-dist-13] median active exp 521, avg 521.4
c [simplification-13] removed 21358 variables 7.5% (264650 remain 18%)
c [simplification-13] removed 196335 irredundant clauses 9.6% (1839230 remain 31%)
c [simplification-13] maximum reduction of 10% = max (7%, 10%)
c [simplification-13] large reduction 10% >= 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 91461 (soft 81461 + delta 10000)
c [simplification-13] new conflict limit 81461 (hard 91461)
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  722.2  264649  1839230     79464   73768 158870 435799   20   263  222   8%    108   54   34   30  112%
c i  722.3  264585  1839230     79473   73776 158870 435799   20   263  225   8%    107   54   33   30  109%
c i  723.0  264584  1839230     79760   74040 158878 435803   22   267  232   8%     73   58   44   30  145%
c i  723.2  264583  1839230     79861   74126 158884 435805   22   267  232   8%     63   58   41   30  135%
c i  725.3  264582  1839230     80778   74947 158939 435824   22   259  232   9%     11   50   19   30   64%
c i  732.1  264580  1839230     82691   76707 159005 435855   22   273  232   8%    -10   61   19   30   62%
c i  737.6  264579  1839230     84349   78286 159042 435868   21   259  232   8%    -15   46   24   30   79%
c i  745.2  264578  1839230     87499   81342 159078 435881   26   201  234  13%      3  -13   31   30  105%
c i  745.7  264577  1839230     87714   81535 159081 435883   27   198  234  13%     -4  -15   41   30  138%
c i  745.7  264576  1839230     87722   81541 159081 435884   27   198  234  13%     -4  -15   41   30  137%
c i  745.8  264575  1839230     87760   81574 159082 435885   27   197  234  14%     -5  -16   43   30  145%
c i  746.7  264574  1839230     88097   81887 159091 435890   27   198  234  13%    -12  -16   26   30   87%
c i  746.9  264573  1839230     88236   82013 159096 435894   26   197  234  13%    -14  -17   23   30   78%
c 
c [simplification-14] limit 81463 conflicts (hard 91461) hit after 91461 conflicts
c [quatres-10] found 308814 quaternary clauses 46% in total
c [quatres-10-1] removed 222 duplicate quaternary clauses
c [quatres-10-1] added 98 double-self-subsuming ternary resolvents
c [quatres-10-2] added 1438 single-self-subsuming ternary resolvents
c [quatres-10-2] added 2735 quaternary resolvents
c [ternres-10] limit 84642525 with penalty 0 = 0 + 0
c [ternres-10] 12362 schedulable variables 5%
c [ternres-10] 68632 ternary resolvents (2036 bin, 66596 trn)
c [ternres-10] 71 variables remain 0% (264502 retained 100%)
c [gauss-4] limit 2116063 penalty 3 = 3 + 0
c [gauss-4] extracted 5331 xors of average arity 3.0
c [gauss-4] connected 15878 occurrences of 6000 variables (average 2.6)
c [gauss-4] limit 2116063 penalty 3 = 3 + 0
c [gauss-4] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-34] removed 553 variables
c [simpleprobe-6] 109376 schedulable variables 41%
c [simpleprobe-6] limit 200000000 penalty 0 = 0 + 0
c [decomp-35] removed 6379 variables
c [simpleprobe-6] 57304 variables remain 22% (200337 retained 78%)
c [simpleprobe-6] removed 6379 variables, found 225238 hbrs, 536 units
c [unhide-14] limit 2116063 with penalty 3 = 0 + 3
c [unhide-14-14] 27 units, 191 failed, 93686 tauts, 0 hbrs, 132419 literals
c [transred-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 2361 transitive binary clauses
c [transred-10] found 2 units
c [cce-4] boosting limit by 10
c [cce-4] limit of 529015782 steps penalty 3 = 3 + 0
c [cce-4-1] eliminated 1 clauses out of 1 (100%) of length 25
c [cce-4-1] eliminated 1 clauses out of 2 (50%) of length 21
c [cce-4-1] eliminated 1 clauses out of 4 (25%) of length 20
c [cce-4-1] eliminated 5 clauses out of 749 (1%) of length 18
c [cce-4-1] eliminated 14 clauses out of 485 (3%) of length 17
c [cce-4-1] eliminated 16 clauses out of 404 (4%) of length 16
c [cce-4-1] eliminated 67 clauses out of 1505 (4%) of length 15
c [cce-4-1] eliminated 51 clauses out of 1385 (4%) of length 14
c [cce-4-1] eliminated 327 clauses out of 3046 (11%) of length 13
c [cce-4-1] eliminated 1440 clauses out of 6323 (23%) of length 12
c [cce-4-1] eliminated 1423 clauses out of 7976 (18%) of length 11
c [cce-4-1] eliminated 7157 clauses out of 19539 (37%) of length 10
c [cce-4-1] eliminated 6217 clauses out of 18528 (34%) of length 9
c [cce-4-1] eliminated 7639 clauses out of 31232 (24%) of length 8
c [cce-4-1] eliminated 6798 clauses out of 38837 (18%) of length 7
c [cce-4-1] eliminated 9352 clauses out of 68211 (14%) of length 6
c [cce-4-1] eliminated 13485 clauses out of 141768 (10%) of length 5
c [cce-4-1] incomplete large round (ATE)
c [cce-4-1] eliminated 53994 large clauses in 529015800 steps
c [cce-4-1] allowing another 264507900 steps for small clauses
c [cce-4-1] scheduling 945669 clauses = 732695 binary + 212974 ternary
c [cce-4-1] tried to eliminate 144375 small clauses 15%
c [cce-4-1] eliminated 15557 binary clauses 2%
c [cce-4-1] eliminated 6406 ternary clauses 3%
c [cce-4-1] eliminated 21963 small clauses 2%
c [cce-4-1] eliminated 23185 small clauses in 529015856 steps
c [cce-4-1] incomplete small round (ATE)
c [cce-4-1] eliminated 77179 covered clauses in round 1
c [cce-4] eliminated 77179 covered clauses in TOTAL during 1 rounds
c [bca-10] limit of 10000000 steps and 3457553 added (scaled 2)
c [bca-10] 433236 out of 514976 literals actually usable 84%
c [bca-10] added 1822 blocked clauses in 1332368 steps
c [sweep-10] limit 25392757 penalty 0 = 0 + 0
c [sweep-10-1] 92644 pos 38.1% + 150578 neg 61.9% = 243222 sched 94.5% ret 14265
c [sweep-10-1] 25394853 steps 575 queries 44215.20 avg class size
c [sweep-10-1] 9332 decisions 552 SAT calls 45.59 avg env size
c [sweep-10-1] 236887 variables remain 92% (20596 retained 8%)
c [decomp-36] removed 528 variables
c [sweep-10-1] removed 528 vars (0 failed, 64 eqs, 75 impls)
c [sweep-10] removed 528 vars in TOTAL (1 rounds, 574 queries)
c [phase-count-14] 1626536 negative 94.4% of 1723008 except 96472 5.6%
c [phase-count-14] 1604323 positive 93.1% of 1723008 except 118685 6.9%
c [phase-count-14] skipping relative phase luck test
c [phase-14] phase bias: 78 positive 71%, 32 negative 29%
c [sort-queue-14] sorted 175788 enqueued variables after 91461 conflicts
c [score-dist-14] active 81171 (32%), one 0 (0%), zero 175788 (68%)
c [score-dist-14] max exp 532, different 27 (5%)
c [score-dist-14] median active exp 521, avg 521.6
c [simplification-14] removed 7614 variables 2.9% (256959 remain 17%)
c [simplification-14] removed 116222 irredundant clauses 6.3% (1723008 remain 29%)
c [simplification-14] maximum reduction of 6% = max (3%, 6%)
c [simplification-14] large reduction 6% >= 5% limit
c [simplification-14] next conflict interval 2000 = 2000/1
c [simplification-14] penalized conflict interval 2000 = 1 * 2000
c [simplification-14] hard conflict limit 103461 (soft 93461 + delta 10000)
c [simplification-14] new conflict limit 93461 (hard 103461)
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  796.0  256958  1723008     92857   86598 195130 537840   30   170  235  18%     25  -42   23   30   76%
c i  796.0  256957  1723008     92860   86598 195132 537840   30   169  235  18%     25  -42   23   30   75%
c i  796.4  256956  1723008     93010   86744 195132 537840   30   167  235  18%     17  -44   27   30   89%
c i  796.4  256955  1723008     93019   86751 195132 537841   30   167  235  18%     17  -44   27   30   88%
c i  796.5  256954  1723008     93041   86772 195132 537841   30   167  235  18%     16  -45   27   30   89%
c i  796.7  256953  1723008     93155   86876 195138 537844   30   165  235  18%     11  -46   26   30   86%
c i  796.9  256952  1723008     93226   86942 195139 537844   30   164  235  18%      8  -47   25   30   82%
c i  800.1  256951  1723008     94065   87722 195167 537852   28   165  236  17%    -10  -45   18   30   59%
c i  800.2  256950  1723008     94121   87769 195170 537853   28   164  236  17%    -11  -46   20   30   65%
c -  814.3  256950  1723008     99338   62372 195247 537891   23   162  214  14%     34  -45   21   29   73%
c i  816.7  256949  1723008    100063   63061 195254 537892   22   153  218  14%     45  -53   16   29   54%
c i  826.7  256948  1723008    102568   65400 195306 537911   20   166  218  12%     -1  -39   14   29   50%
c 
c [simplification-15] limit 93465 conflicts (hard 103461) hit after 103461 conflicts
c [quatres-11] found 301799 quaternary clauses 50% in total
c [quatres-11-1] removed 1512 duplicate quaternary clauses
c [quatres-11-1] added 37 double-self-subsuming ternary resolvents
c [quatres-11-2] added 854 single-self-subsuming ternary resolvents
c [quatres-11-2] added 1030 quaternary resolvents
c [ternres-11] limit 92892087 with penalty 0 = 0 + 0
c [ternres-11] 69 schedulable variables 0%
c [ternres-11] 27378 ternary resolvents (885 bin, 26493 trn)
c [ternres-11] fully completed ternary resolution
c [card-5] limit 2902877 penalty 4 = 4 + 0
c [card-5] found 1812 at-most-one constraints of average size 3.2
c [card-5] no at-most-two constraint found
c [card-5] using previous limit 2902877 for elimination
c [card-5] 1812 out of 1812 constraints (100%) meet size limits
c [card-5] no units found
c [card-5] no at-most-one constraints generated
c [decomp-37] removed 259 variables
c [treelook-6] limit 9289208 penalty 0 = 0 + 0 boost 1
c [treelook-6] scheduled 211373 literals 41%
c [treelook-6] scheduling used 4495612 steps
c [treelook-6] scheduled completely
c [treelook-6] limit 9289208 penalty 0 = 0 + 0 boost 1
c [treelook-6] used 9292948 steps
c [treelook-6] 210830 literals remain 41%
c [treelook-6] 27903 variables remain to probed next time 11%
c [decomp-38] removed 34 variables
c [treelook-6] removed 128 variables, found 30147 hbrs
c [unhide-15] limit 2322302 with penalty 3 = 0 + 3
c [unhide-15-15] 26 units, 29 failed, 14836 tauts, 0 hbrs, 15896 literals
c [transred-11] limit 2000000 with penalty 0 = 0 + 0
c [transred-11] removed 1750 transitive binary clauses
c [transred-11] found 1 units
c [elim-12] scheduling all variables this time
c [elim-12] scheduled 256519 variables 100%
c [elim-12] limit of 400000000 steps penalty 1 = 1 + 0
c [elim-12] rescheduling of touched variables disabled
c [elim-12] incomplete 578 not tried 0% in round 1
c [elim-12] transition to [ all 1 rem 1 ] state
c [elim-12] eliminated 25266 = 10% variables out of 256519 scheduled
c [bca-11] limit of 10000000 steps and 3244008 added (scaled 2)
c [bca-11] 392929 out of 462508 literals actually usable 85%
c [bca-11] added 3292 blocked clauses in 1228848 steps
c [sweep-11] boosting sweeping limit by 10
c [sweep-11] limit 278676260 penalty 0 = 0 + 0
c [sweep-11-1] 80542 pos 37.8% + 132281 neg 62.2% = 212823 sched 92.0% ret 18430
c [sweep-11-1] 278699511 steps 5940 queries 6476.56 avg class size
c [sweep-11-1] 77214 decisions 5756 SAT calls 33.72 avg env size
c [sweep-11-1] 132482 variables remain 57% (98530 retained 43%)
c [decomp-39] removed 2415 variables
c [sweep-11-1] removed 2415 vars (0 failed, 1105 eqs, 1077 impls)
c [sweep-11] removed 2415 vars in TOTAL (1 rounds, 5939 queries)
c [phase-count-15] 1516136 negative 94.4% of 1606560 except 90424 5.6%
c [phase-count-15] 1496405 positive 93.1% of 1606560 except 110155 6.9%
c [phase-count-15] skipping relative phase luck test
c [phase-15] phase bias: 29 positive 34%, 56 negative 66%
c [sort-queue-15] sorted 139933 enqueued variables after 103461 conflicts
c [score-dist-15] active 88905 (39%), one 0 (0%), zero 139933 (61%)
c [score-dist-15] max exp 532, different 26 (5%)
c [score-dist-15] median active exp 521, avg 521.6
c [simplification-15] removed 28090 variables 10.9% (228838 remain 15%)
c [simplification-15] removed 116448 irredundant clauses 6.8% (1606560 remain 27%)
c [simplification-15] maximum reduction of 11% = max (11%, 7%)
c [simplification-15] large reduction 11% >= 5% limit
c [simplification-15] next conflict interval 2000 = 2000/1
c [simplification-15] penalized conflict interval 2000 = 1 * 2000
c [simplification-15] hard conflict limit 115461 (soft 105461 + delta 10000)
c [simplification-15] new conflict limit 105461 (hard 115461)
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  885.9  228837  1606560    103489   56395 174265 468048   20   157  206  13%    -15  -47   19   29   67%
c i  886.1  228836  1606560    103584   56482 174269 468049   20   155  207  13%    -16  -49   18   29   62%
c i  902.2  228835  1606560    109693   62322 174322 468075   20   109  208  18%     47  -88   19   28   69%
c i  905.5  228832  1606560    111807   64333 174346 468088   19    90  209  20%     -4 -104   12   28   42%
c i  905.5  228831  1606560    111811   64335 174346 468089   18    90  209  20%     -4 -104   11   28   41%
c i  905.7  228822  1606560    111956   64462 174348 468094   19    89  209  21%     -8 -104   16   28   57%
c i  908.5  228821  1606560    113501   65931 174373 468104   17    81  210  21%    -15 -110   11   27   40%
c 
c [simplification-16] limit 105463 conflicts (hard 115461) hit after 115463 conflicts
c [quatres-12] found 288282 quaternary clauses 49% in total
c [quatres-12-1] removed 142 duplicate quaternary clauses
c [quatres-12-1] added 20 double-self-subsuming ternary resolvents
c [quatres-12-2] added 1350 single-self-subsuming ternary resolvents
c [quatres-12-2] added 5255 quaternary resolvents
c [ternres-12] limit 98800903 with penalty 0 = 0 + 0
c [ternres-12] all 228818 free variables schedulable
c [ternres-12] 41144 ternary resolvents (2046 bin, 39098 trn)
c [ternres-12] 134 variables remain 0% (228684 retained 100%)
c [decomp-40] removed 291 variables
c [basicprobe-6] limit 400000000 penalty 0 = 0 + 0
c [basicprobe-6-0] 69762 sched 31%, 1404 failed, 55 lifted, 46549 hbrs
c [decomp-41] removed 5989 variables
c [basicprobe-6-1] 143855 sched 65%, 1407 failed, 58 lifted, 37686 hbrs
c [decomp-42] removed 3340 variables
c [basicprobe-6-2] 101298 probes remain 46% after last round
c [basicprobe-6-2] 3014 units = 2900 failed (96%) + 114 lifted (4%)
c [basicprobe-6-2] removed 9812 variables, found 87660 hbrs
c [bate-4] eliminated 5932 asymmetric tautologies during probing
c [unhide-16] limit 2470022 with penalty 3 = 0 + 3
c [unhide-16-16] 7 units, 43 failed, 67585 tauts, 0 hbrs, 60387 literals
c [transred-12] limit 2000000 with penalty 0 = 0 + 0
c [transred-12] removed 2548 transitive binary clauses
c [transred-12] found 1 units
c [block-6] scheduling all variables this time
c [block-6] scheduled 218712 variables 100%
c [block-6] limit of 200000000 steps penalty 2 = 2 + 0
c [block-6] fully completed
c [block-6] transition to [ all 0 rem 0 ] state
c [block-6] eliminated 14878 blocked clauses
c [block-6] 14878 < 1/100 * 1516083 = 15160 considered unsuccessful
c [cce-5] limit of 123501129 steps penalty 2 = 2 + 0
c [cce-5-1] eliminated 2 clauses out of 7 (29%) of length 20
c [cce-5-1] eliminated 1 clauses out of 135 (1%) of length 19
c [cce-5-1] eliminated 2 clauses out of 722 (0%) of length 18
c [cce-5-1] eliminated 4 clauses out of 608 (1%) of length 17
c [cce-5-1] eliminated 6 clauses out of 621 (1%) of length 16
c [cce-5-1] eliminated 18 clauses out of 1249 (1%) of length 15
c [cce-5-1] eliminated 97 clauses out of 1324 (7%) of length 14
c [cce-5-1] eliminated 504 clauses out of 2496 (20%) of length 13
c [cce-5-1] eliminated 596 clauses out of 4462 (13%) of length 12
c [cce-5-1] eliminated 1213 clauses out of 6033 (20%) of length 11
c [cce-5-1] eliminated 1857 clauses out of 10449 (18%) of length 10
c [cce-5-1] eliminated 2471 clauses out of 14123 (17%) of length 9
c [cce-5-1] incomplete large round (ACCE)
c [cce-5-1] eliminated 6771 large clauses in 123501131 steps
c [cce-5-1] allowing another 61750565 steps for small clauses
c [cce-5-1] scheduling 813412 clauses = 600352 binary + 213060 ternary
c [cce-5-1] tried to eliminate 33159 small clauses 4%
c [cce-5-1] eliminated 6114 binary clauses 1%
c [cce-5-1] eliminated 1681 ternary clauses 1%
c [cce-5-1] eliminated 7795 small clauses 1%
c [cce-5-1] eliminated 7795 small clauses in 123501237 steps
c [cce-5-1] incomplete small round (ACCE)
c [cce-5-1] eliminated 14566 covered clauses in round 1
c [cce-5] eliminated 14566 covered clauses in TOTAL during 1 rounds
c [cce-5] 14566 < 1/100 * 1500979 = 15009 considered unsuccessful
c [elim-13] 578 variables 0% will be scheduled this time
c [elim-13] scheduled 578 variables 0%
c [elim-13] almost no limit of 100000000000 steps
c [elim-13] rescheduling of touched variables disabled
c [elim-13-1] no variable eliminated in round 1 in 104838892 steps
c [elim-13] fully completed in 1 rounds
c [elim-13] transition to [ all 0 rem 0 ] state
c [elim-13] eliminated 0 = 0% variables out of 578 scheduled
c [bca-12] limit of 10000000 steps and 2981278 added (scaled 2)
c [bca-12] 359882 out of 436296 literals actually usable 82%
c [bca-12] added 2571 blocked clauses in 1119696 steps
c [sweep-12] limit 29640270 penalty 0 = 0 + 0
c [sweep-12-1] 47815 pos 38.1% + 77694 neg 61.9% = 125509 sched 57.5% ret 92638
c [sweep-12-1] 29653875 steps 1135 queries 17636.69 avg class size
c [sweep-12-1] 12484 decisions 1035 SAT calls 30.64 avg env size
c [sweep-12-1] 120184 variables remain 55% (97946 retained 45%)
c [decomp-43] removed 889 variables
c [sweep-12-1] removed 889 vars (0 failed, 262 eqs, 292 impls)
c [sweep-12] removed 889 vars in TOTAL (1 rounds, 1134 queries)
c [phase-count-16] 1397184 negative 94.2% of 1482525 except 85341 5.8%
c [phase-count-16] 1375061 positive 92.8% of 1482525 except 107464 7.2%
c [phase-count-16] skipping relative phase luck test
c [phase-16] phase bias: 37 positive 57%, 28 negative 43%
c [sort-queue-16] sorted 130877 enqueued variables after 115463 conflicts
c [score-dist-16] active 86381 (40%), one 0 (0%), zero 130877 (60%)
c [score-dist-16] max exp 532, different 26 (5%)
c [score-dist-16] median active exp 521, avg 521.7
c [simplification-16] removed 11560 variables 5.1% (217258 remain 15%)
c [simplification-16] removed 124035 irredundant clauses 7.7% (1482525 remain 25%)
c [simplification-16] maximum reduction of 8% = max (5%, 8%)
c [simplification-16] large reduction 8% >= 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 127463 (soft 117463 + delta 10000)
c [simplification-16] new conflict limit 117463 (hard 127463)
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  962.6  217257  1482525    119717   73853 182352 436391   19    61  205  31%     48 -120   19   26   73%
c i  970.6  217256  1482525    124333   78279 182387 436427   18    71  206  25%     23 -101   12   26   47%
c i  973.4  217255  1482525    125269   79116 182428 436449   17   118  206  14%     -6  -53   14   26   56%
c 
c [simplification-17] limit 117463 conflicts (hard 127463) hit after 127463 conflicts
c [quatres-13] found 266420 quaternary clauses 49% in total
c [quatres-13-1] removed 145 duplicate quaternary clauses
c [quatres-13-1] added 33 double-self-subsuming ternary resolvents
c [quatres-13-2] added 1367 single-self-subsuming ternary resolvents
c [quatres-13-2] added 1210 quaternary resolvents
c [ternres-13] limit 104619252 with penalty 0 = 0 + 0
c [ternres-13] 123 schedulable variables 0%
c [ternres-13] 13084 ternary resolvents (323 bin, 12761 trn)
c [ternres-13] fully completed ternary resolution
c [decomp-44] removed 80 variables
c [simpleprobe-7] 46255 schedulable variables 21%
c [simpleprobe-7] limit 200000000 penalty 0 = 0 + 0
c [decomp-45] removed 2729 variables
c [simpleprobe-7] 28985 variables remain 14% (185464 retained 86%)
c [simpleprobe-7] removed 2729 variables, found 140144 hbrs, 87 units
c [unhide-17] limit 2500000 with penalty 3 = 0 + 3
c [unhide-17-17] 0 units, 5 failed, 13841 tauts, 0 hbrs, 22754 literals
c [transred-13] limit 2000000 with penalty 0 = 0 + 0
c [transred-13] removed 2529 transitive binary clauses
c [bca-13] limit of 10000000 steps and 2931279 added (scaled 2)
c [bca-13] 349816 out of 428862 literals actually usable 82%
c [bca-13] added 187 blocked clauses in 1100083 steps
c [sweep-13] limit 31385775 penalty 0 = 0 + 0
c [sweep-13-1] 44283 pos 37.6% + 73505 neg 62.4% = 117788 sched 54.9% ret 96642
c [sweep-13-1] 31386446 steps 1170 queries 16141.57 avg class size
c [sweep-13-1] 13019 decisions 1081 SAT calls 32.43 avg env size
c [sweep-13-1] 112205 variables remain 52% (102154 retained 48%)
c
c CAUGHT SIGNAL 15 SIGTERM
c
c s UNKNOWN
c bate: 23069 basic ate = 17545 trn 76% + 5524 lrg 24% in 4 updates
c bcas: 13 count, 25214 added (24505 skipped), 21493387 steps
c bkwd: tried 1247747 clauses, 2491436 lits, 2.00 lits/clause
c bkwd: checked 118870610 occs, 95.27 occs/clause, 47.71 occs/lit
c bkwd: subsumed 20 binary, 887 ternary, 1058 large
c bkwd: strengthened 33 binary, 28 ternary (100% self), 4518 large (0% self)
c blkd: 6 bces, 85745 removed, 52160363 resolutions, 136747613 steps
c blkd: 46321 blocking literals 2%, 2424 pure
c bump: 138059 bumped seen, 41965413 lits 304.0 on average
c card: 5 count, 0 units, 0 am1, 87925747 steps
c card: 0 rescheduled, 0 eliminated, 0 resolved, 12578 subsumed
c card: 5440 at-most-one constraints found, average size 3.08
c card: 5440 at-most-one constraints used 100%, average size 3.08
c card: 0 at-most-two constraints found, average size 0.00
c card: 0 at-most-two constraints used 0%, average size 0.00
c cces: 5 cces, 95479 eliminated, 89802 ate 94%, 5677 abce 6%
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: 21188985 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 132 gcs, 0 rescored clauses, 0 rescored vars
c dcps: 46 decompositions, 159258 equivalent 10%
c deco: 7669 decision-only clauses 6%, 72% reduction
c decs: 4031752 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 13 elims, 878257 eliminated 57%, 12578 pure 1%
c elms: 16 rounds, 1.2 rounds/bve
c elms: 759596 small 86%, 103659 large 12%
c elms: 949779 tried small, 759596 succeeded 80%, 190183 failed 20%
c elms: 337801 subsumed, 442756 strengthened, 11899 blocked
c elms: 50449206 copies, 63481302 resolutions, 17887319 ipos
c elms: 38783417 subchks, 72343291 strchks
c gaus: 4 extractions, 20992 extracted, 3.0 size, 3 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 12171138 steps, 6085569 extr 50%, 6116427 elim 50%
c glue: 32.5 orig avg, 32.5 real avg, 3.6 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 1891637 = 702879 simple 37% + 1177390 trn 62% + 11368 lrg 1%, 47239 sub 2%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 138059 clauses, 76.7 length
c lrnd: 10588595 lits = 19268158 orig - 8679563 removed 45%
c lrnd: 58351 uips 42%, 28558 flips 21%
c mins: 120554 mins 87%, 3047 bin 2%, 6698 size 5%
c mins: 31622766 poisoned searches, 4038586 hits, 13% hit rate
c mins: 38811081 used twice searches, 1413310 hits, 4% hit rate
c move: moved 161020, 63464 bin 39%, 97556 trn 61%
c otfs: 1476 driving 42%, 2020 restarting 58%
c otfs: str 3496, 2769 red 79%, 727 irr 21%
c otfs: str 3496, 0 bin 0%, 860 trn 25%, 2636 lrg 75%
c otfs: sub 131, 102 red 78%, 29 irr 22%
c otfs: sub 131, 0 bin 0%, 51 trn 39%, 80 lrg 61%
c phas: 16 computed, 1165411 set, 540433 pos (46%), 624978 neg (54%)
c prbs: 6 basic, 1340698 probed, 22634 failed, 3973 lifted
c prbs: 7 simple, 2593987 probed, 2620 failed, 20208 eqs
c prbs: 6 treelook, 1255 probed, 85 failed, 0 lifted
c prom: 987 locked 0% out of 212225 tried
c prps: 1735071596 props, 409 props/dec
c prps: 95% srch, 5% simp, 0% lkhd
c quat: 13 count, 55626 quat, 18509 self1, 548 self2, 5755 dup
c queu: 16 sorted, 4031752 next (94900 steps 0.02)
c queu: 49845408 enq (219686652 steps 4.41), 41965413 deq 84%
c redc: 5349 clauses 15%, 34944 tried 27%, 231 sat 1%
c redc: 9845 lits 3%, 282396 tried 1%, 232 sat 0%
c redc: 859 times jump level reduced, 70.1 levels on average
c reds: 1 count, 127463.0 conflicts per reduce
c reds: 0 memlim 0%, 1 arith 100%
c reds: 25006 collected 82%, 5331 retired 18%
c rmbd: 395866 removed, 268613 red 68%
c rsts: 4180 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: 17 count, 15 confs 88%, 0 vars 0%
c simp: 1 its 6%, 1 bin 6%, 0 trns 0%
c subl: 138059 count (206028 tried 1.5), 10896 sub out of 126644 (8.6%)
c swps: 13 count, 13 rounds, 11020 queries (847.7/round)
c swps: 10507 sat calls, 1567 unsat (1.1% success rate)
c swps: 142910 decisions 13.6, 12072 conflicts 1.1
c swps; 23680.4 avg class size, 34.5 avg environment size
c swps: 0 failed, 2148 impls, 2018 equivs
c swp0: 3668 type 0 queries, 635 unsat (17.3%), 3459 sat (94.3%)
c swp1: 7352 type 1 queries, 4586 unsat (62.4%), 5543 sat (75.4%)
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: 8340102 calls to obtain time
c tops: 288589 fixed 19%, 162 its, 786.81 confs/it
c trds: 13 transitive reductions, 23428 removed, 95 failed
c trds: 352951 nodes, 582276 edges, 29301386 steps
c trim: 620010 words, 2.4 MB
c trnr: 13 count, 18193 bin, 608123 trn, 558885647 steps
c unhd: 17 count, 17 rounds, 276251775 steps
c unhd: 41575 non-trivial sccs of average size 2.4
c unhd: 4923 units, 4896 bin, 22 trn, 5 lrg
c unhd: 7033 failed, 6131 stamp, 0 lits, 49 bin, 718 trn, 5 lrg
c unhd: 607325 tauts, 13009 bin 2%, 162895 trn 27%, 45629 lrg 8%
c unhd: 607325 tauts, 385792 stamp 64%, 408364 red 67%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 891410 str, 4896 bin 1%, 83923 trn 9%, 802591 lrg 90%, 329781 red 37%
c vars: 213967 remaining 14% and 1326104 removed 86% out of 1540071
c vars: 288589 fixed 19%, 878257 eliminated 57%, 159258 equivalent 10%
c vsts: 11205908440 visits, 93% srch, 7% simp, 0% lkhd
c vsts: 6.3 search visits per propagation, 82078.1 per conflict
c wchs: 1511553598 pushed, 234133400 enlarged, 193 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all         182270         25006          5331      13117171       1852621         43996
c 
c  0 0         79902  44       163   1         0   0  10216793  78   1075258  58     18935  43     1.2
c  1 5          5695   3       287   1       445   8    787915   6<   147474   8<     3107   7     0.3
c  2 6         14307   8      2072   8      1003  19    933488   7    223404  12      6370  14<    1.2
c  3 9         17678  10<     4547  18      1028  19    527033   4    147746   8      5174  12     2.5
c  4 14        16994   9      4513  18       882  17<   262653   2     90375   5      3433   8     2.1
c  5 21        14013   8      3786  15<      657  12    150786   1     56745   3      2551   6     1.8
c  6 30        10594   6      3126  13       440   8     91355   1     37795   2      1732   4     1.7
c  7 41         7199   4      2766  11       305   6     58790   0     28159   2      1053   2     1.8
c  8 54         4664   3      2186   9       243   5     36664   0     17971   1       642   1     1.5
c  9 69         2071   1       949   4       120   2     21050   0     10785   1       322   1     0.7
c 10 86         1312   1       498   2        69   1     17180   0     10162   1       593   1     0.6
c 11 126         535   0        52   0        34   1      1673   0       718   0        46   0     0.2
c 12 230        7306   4        61   0       105   2     11791   0      6029   0        38   0     4.2
c 
c avg                  2.8           5.0           4.2           0.6           1.4           2.1
c std                  3.2           2.2           2.4           1.4           2.1           2.4
c 
c   97.101  10% probe
c   95.240  10% elim
c   92.453   9% sweep
c   39.740   4% unhide
c   28.954   3% cce
c   21.843   2% block
c   19.448   2% bca
c   18.403   2% bump
c   15.011   2% quatres
c    8.236   1% gauss
c 
c   13.271 < 1% rest (below)
c 
c    6.331   1% ternres
c    4.290   0% decide
c    1.872   0% transred
c    0.778   0% card
c    0.000   0% locs
c    0.000   0% queuesort
c    0.000   0% rescore
c ==================================
c   18.722   2% preprocessing     4%
c  467.948  47% inprocessing     96%
c ==================================
c  486.670  49% simplifying
c  509.270  51% search
c ==================================
c  995.967 100% all
c 
c        127463 conflicts,         128.0 confs/sec
c          3406 ternaries,          37.4 confs/ternary
c          1834 binaries,           69.5 confs/binary
c           162 iterations,        786.8 confs/iteration
c 
c             1 reductions,          0.0 redus/sec, 127463.0 confs/reduction
c          4180 restarts,            4.2 rests/sec,     30.5 confs/restart
c       4031752 decisions,        4048.1 decis/sec,     31.6 decis/conflict
c    1735071596 propagations,  1742096.6 props/sec,    430.4 props/decision
c 
c 996.0 seconds, 614.6 MB
c
c CAUGHT SIGNAL 15 SIGTERM
c
c launch: done
