c launch: /data/cnf/sc2014/app/UCG-20-10p1.cnf.bz2
c host: atom07
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/UCG-20-10p1.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/UCG-20-10p1.cnf.bz2
c no embedded options
c found 'p cnf 259258 1388006' header
c read 259258 variables, 1388006 clauses, 3352067 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=4
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 246109 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] VSIDS (--score=4) decay interval 256 (--vsidsdint=256)
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  246109  1373987         0       0      0     0    0     0   58   0%      0    0    0    0    0%
c 
c [simplification-1] limit 0 conflicts (hard 0) hit after 0 conflicts
c [card-1] limit 2000000 penalty 0 = 0 + 0
c [card-1] found 6014 at-most-one constraints of average size 5.8
c [card-1] no at-most-two constraint found
c [card-1] using previous limit 2000000 for elimination
c [card-1] 6014 out of 6014 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 62780 variables
c [simpleprobe-1] all 196478 free variables schedulable
c [simpleprobe-1] boosting simple probing limit by 10
c [simpleprobe-1] limit 20000000 penalty 0 = 0 + 0
c [decomp-2] removed 221 variables
c [simpleprobe-1] 15148 variables remain 8% (181109 retained 92%)
c [simpleprobe-1] removed 221 variables, found 15749 hbrs, 20 units
c [unhide-1] limit 66079 based on 1057273 irredundant clauses
c [unhide-1-1] 25 units, 1431 failed, 8310 tauts, 0 hbrs, 12876 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 194130 variables 100%
c [elim-1] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-1] rescheduling of touched variables disabled
c [elim-1] incomplete 60833 not tried 31% in round 1
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 74191 = 38% variables out of 194130 scheduled
c [elim-1] considered successful since not run to completion yet
c [phase-count-1] 874938 negative 99.2% of 881558 except 6620 0.8%
c [phase-count-1] 709837 positive 80.5% of 881558 except 171721 19.5%
c [phase-count-1] less non-negative clauses 6620 than limit 88100 (10.0%)
c [phase-count-1] non-pos/non-neg = 171721/6620 = 25.94 >= 2.00 = 200/100
c [lucky-phase-1] forcing lucky phase -1
c [phase-1] phase bias: 0 positive 0%, 119939 negative 100%
c [sort-queue-1] sorted 119939 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 119939 (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 82741 variables 40.8% (119939 remain 49%)
c [simplification-1] removed 492429 irredundant clauses 35.8% (881558 remain 64%)
c [simplification-1] maximum reduction of 41% = max (41%, 36%)
c [simplification-1] large reduction 41% >= 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    5.4  119938   881558       152     116     13 11278    0    17   59   2%      0   17    4    0 18109%
c i    5.8  119642   881558       408     303     37 11305    1    27   59   3%      1   27    6    0 11818%
c i    6.1  119251   881558       502     380     44 11311    1    32   59   4%      1   32   10    0 13362%
c i    6.7  119098   881558       695     520     73 11329    2    51   59   3%      1   50   10    0 9758%
c i    6.8  118863   881558       731     553     74 11330    2    53   59   3%      1   53   11    0 9531%
c i    7.0  118613   881558       825     624     80 11337    2    55   59   4%      1   55   14    0 10009%
c i    7.0  118606   881558       864     651     86 11340    2    56   59   4%      1   55   14    0 9242%
c 
c [simplification-2] limit 1000 conflicts (hard 11000) hit after 1000 conflicts
c [decomp-3] removed 1634 variables
c [simpleprobe-2] 14391 schedulable variables 12%
c [simpleprobe-2] limit 2692580 penalty 0 = 0 + 0
c [decomp-4] removed 3 variables
c [simpleprobe-2] 13982 variables remain 12% (104320 retained 88%)
c [simpleprobe-2] removed 3 variables, found 2182 hbrs, 1 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 71295 literals 30%
c [treelook-1] scheduling used 301743 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 588230 steps
c [treelook-1] 71290 literals remain 30%
c [treelook-1] 67918 variables remain to probed next time 57%
c [treelook-1] removed 0 variables, found 4873 hbrs
c [basicprobe-1] limit 6954360 based on 869295 irredundant clauses
c [basicprobe-1-0] 42792 probes remain 38% after last round
c [basicprobe-1-0] 36 units = 32 failed (89%) + 4 lifted (11%)
c [basicprobe-1-0] removed 6106 variables, found 18051 hbrs
c [unhide-2] limit 67314 with penalty 1 = 0 + 1
c [unhide-2-2] 9 units, 2514 failed, 9481 tauts, 0 hbrs, 2105 literals
c [elim-2] 56996 variables 52% will be scheduled this time
c [elim-2] scheduled 56996 variables 52%
c [elim-2] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-2] rescheduling of touched variables disabled
c [elim-2] incomplete 22842 not tried 21% in round 1
c [elim-2] transition to [ all 0 rem 1 ] state
c [elim-2] eliminated 31 = 0% variables out of 56996 scheduled
c [elim-2] considered successful since not run to completion yet
c [phase-count-2] 775265 negative 99.2% of 781883 except 6618 0.8%
c [phase-count-2] 625308 positive 80.0% of 781883 except 156575 20.0%
c [phase-count-2] less non-negative clauses 6618 than limit 78100 (10.0%)
c [phase-count-2] non-pos/non-neg = 156575/6618 = 23.66 >= 2.00 = 200/100
c [lucky-phase-2] forcing lucky phase -1
c [phase-2] phase bias: 0 positive 0%, 1779 negative 100%
c [sort-queue-2] sorted 81617 enqueued variables after 1000 conflicts
c [score-dist-2] active 27027 (25%), one 0 (0%), zero 81617 (75%)
c [score-dist-2] max exp 508, different 11 (2%)
c [score-dist-2] median active exp 502, avg 501.7
c [simplification-2] removed 9706 variables 8.2% (108644 remain 44%)
c [simplification-2] removed 99675 irredundant clauses 11.3% (781883 remain 57%)
c [simplification-2] maximum reduction of 11% = max (8%, 11%)
c [simplification-2] large reduction 11% >= 5% limit
c [simplification-2] next conflict interval 2000 = 2000/1
c [simplification-2] penalized conflict interval 2000 = 1 * 2000
c [simplification-2] hard conflict limit 13000 (soft 3000 + delta 10000)
c [simplification-2] new conflict limit 3000 (hard 13000)
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   10.6  108643   781883      1026     762     97 24093    3    57   52   5%      1   57   14    0 7703%
c i   11.0  108638   781883      1290     976    110 24109    4    65   53   6%      1   65   19    0 7020%
c i   12.4  108150   781883      2138    1604    132 24137   16    81   54  19%      5   80  102    1 9348%
c i   12.5  108140   781883      2162    1623    133 24139   16    82   54  19%      5   81   98    1 8814%
c i   13.3  108135   781883      2649    2019    161 24152   21   114   54  19%      4  111   93    2 5895%
c i   13.4  108125   781883      2703    2059    167 24154   22   121   54  18%      4  118   95    2 5741%
c i   13.8  108115   781883      2898    2212    192 24165   24   145   54  16%      4  142   66    2 3699%
c i   13.9  108080   781883      2941    2246    194 24169   24   151   54  16%      4  148   59    2 3285%
c 
c [simplification-3] limit 3000 conflicts (hard 13000) hit after 3001 conflicts
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 3564 at-most-one constraints of average size 4.6
c [card-2] no at-most-two constraint found
c [card-2] using previous limit 1000000 for elimination
c [card-2] 3564 out of 3564 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [decomp-6] removed 876 variables
c [unhide-3] limit 177739 with penalty 1 = 0 + 1
c [unhide-3-3] 11 units, 1248 failed, 20187 tauts, 0 hbrs, 3884 literals
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 105922 variables 100%
c [elim-3] limit of 35547829 steps penalty 0 = 0 + 0
c [elim-3] rescheduling of touched variables disabled
c [elim-3] incomplete 15530 not tried 15% in round 1
c [elim-3] transition to [ all 1 rem 1 ] state
c [elim-3] eliminated 1822 = 2% variables out of 105922 scheduled
c [elim-3] considered successful since not run to completion yet
c [phase-count-3] 732279 negative 99.1% of 738791 except 6512 0.9%
c [phase-count-3] 589378 positive 79.8% of 738791 except 149413 20.2%
c [phase-count-3] less non-negative clauses 6512 than limit 73800 (10.0%)
c [phase-count-3] non-pos/non-neg = 149413/6512 = 22.94 >= 2.00 = 200/100
c [lucky-phase-3] forcing lucky phase -1
c [phase-3] phase bias: 0 positive 0%, 1452 negative 100%
c [sort-queue-3] sorted 68430 enqueued variables after 3001 conflicts
c [score-dist-3] active 35670 (34%), one 0 (0%), zero 68430 (66%)
c [score-dist-3] max exp 508, different 19 (4%)
c [score-dist-3] median active exp 502, avg 499.7
c [simplification-3] removed 3969 variables 3.7% (104100 remain 42%)
c [simplification-3] removed 43092 irredundant clauses 5.5% (738791 remain 54%)
c [simplification-3] maximum reduction of 6% = max (4%, 6%)
c [simplification-3] large reduction 6% >= 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 15001 (soft 5001 + delta 10000)
c [simplification-3] new conflict limit 5001 (hard 15001)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   17.5  104099   738791      3356    2310    207 20896   37   215   52  17%      3  211  157    3 5553%
c i   18.2  103654   738791      3642    2525    211 20900   57   255   53  22%      3  250  286    4 6709%
c i   18.4  103646   738791      3703    2565    214 20902   63   262   54  24%      3  257  316    5 6778%
c i   18.4  103637   738791      3704    2565    214 20902   63   262   54  24%      3  257  315    5 6752%
c i   18.4  103628   738791      3706    2565    214 20903   63   262   54  24%      3  257  312    5 6700%
c i   18.4  103617   738791      3707    2565    214 20903   63   262   54  24%      3  257  311    5 6673%
c i   18.5  103606   738791      3708    2565    214 20903   63   262   54  24%      3  257  310    5 6647%
c i   18.5  103596   738791      3709    2565    214 20903   63   262   54  24%      3  257  309    5 6622%
c i   19.3  103588   738791      3987    2757    216 20913   80   280   54  29%      3  273  322    6 5331%
c i   19.3  103587   738791      3993    2758    216 20914   81   280   54  29%      3  273  321    6 5295%
c 
c [simplification-4] limit of 25 iterations hit after 25 iterations
c [decomp-7] removed 586 variables
c [treelook-2] limit 183791 based on 735166 irredundant clauses
c [treelook-2] scheduled 39908 literals 19%
c [treelook-2] scheduling used 186891 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 183791 based on 735166 irredundant clauses
c [treelook-2] used 331663 steps
c [treelook-2] 39867 literals remain 19%
c [treelook-2] 32315 variables remain to probed next time 31%
c [decomp-8] removed 36 variables
c [treelook-2] removed 36 variables, found 2277 hbrs
c [unhide-4] limit 262205 with penalty 1 = 0 + 1
c [unhide-4-4] 13 units, 1265 failed, 4752 tauts, 0 hbrs, 25918 literals
c [elim-4] 15282 variables 15% will be scheduled this time
c [elim-4] scheduled 15282 variables 15%
c [elim-4] boosting limit by 20
c [elim-4] limit of 1048823380 steps penalty 0 = 0 + 0
c [elim-4] rescheduling of touched variables disabled
c [elim-4-1] no variable eliminated in round 1 in 34937895 steps
c [elim-4] fully completed in 1 rounds
c [elim-4] transition to [ all 0 rem 0 ] state
c [elim-4] eliminated 0 = 0% variables out of 15282 scheduled
c [phase-count-4] 709233 negative 99.1% of 715745 except 6512 0.9%
c [phase-count-4] 568136 positive 79.4% of 715745 except 147609 20.6%
c [phase-count-4] less non-negative clauses 6512 than limit 71500 (10.0%)
c [phase-count-4] non-pos/non-neg = 147609/6512 = 22.67 >= 2.00 = 200/100
c [lucky-phase-4] forcing lucky phase -1
c [phase-4] phase bias: 0 positive 0%, 1377 negative 100%
c [sort-queue-4] sorted 62862 enqueued variables after 3993 conflicts
c [score-dist-4] active 38877 (38%), one 0 (0%), zero 62862 (62%)
c [score-dist-4] max exp 509, different 24 (5%)
c [score-dist-4] median active exp 500, avg 498.6
c [simplification-4] removed 1783 variables 1.7% (101739 remain 41%)
c [simplification-4] removed 23046 irredundant clauses 3.1% (715745 remain 52%)
c [simplification-4] maximum reduction of 3% = max (2%, 3%)
c [simplification-4] forced so keeping old conflict interval 0
c [simplification-4] conflict limit remains at 5047 (hard 15001)
c [simplification-4] 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   22.1  101738   715745      4252    2943    210 17596   87   289   52  30%      3  282  239    7 3522%
c i   22.2  101383   715745      4286    2967    210 17596   88   291   52  30%      2  283  237    7 3446%
c i   22.4  101382   715745      4396    3051    210 17602   90   298   52  30%      2  289  207    7 2908%
c i   23.2  101222   715745      4825    3421    223 17609   95   343   53  28%      3  333  161    8 2013%
c i   23.5  101208   715745      4944    3522    230 17615   93   361   53  26%      2  350  112    8 1395%
c 
c [simplification-5] limit 5047 conflicts (hard 15001) hit after 5050 conflicts
c [quatres-1] found 35105 quaternary clauses 32% in total
c [quatres-1-2] added 1 single-self-subsuming ternary resolvents
c [quatres-1-2] added 7 quaternary resolvents
c [ternres-1] boosting ternary resolution limit by 5
c [ternres-1] limit 20000000 with penalty 0 = 0 + 0
c [ternres-1] all 101095 free variables schedulable
c [ternres-1] 9 ternary resolvents (0 bin, 9 trn)
c [ternres-1] fully completed ternary resolution
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 59 xors of average arity 2.6
c [gauss-1] connected 155 occurrences of 146 variables (average 1.1)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] fully completed
c [gauss-1] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-9] removed 48 variables
c [basicprobe-2] limit 16670115 penalty 0 = 0 + 0
c [basicprobe-2-0] 37324 probes remain 38% after last round
c [basicprobe-2-0] 65 units = 65 failed (100%) + 0 lifted (0%)
c [basicprobe-2-0] removed 2656 variables, found 31706 hbrs
c [bate-1] eliminated 22 asymmetric tautologies during probing
c [unhide-5] limit 333402 with penalty 1 = 0 + 1
c [unhide-5-5] 10 units, 578 failed, 15110 tauts, 0 hbrs, 13244 literals
c [transred-1] limit 2000000 with penalty 0 = 0 + 0
c [transred-1] removed 252 transitive binary clauses
c [transred-1] found 13 units
c [block-1] scheduling all variables this time
c [block-1] scheduled 97044 variables 100%
c [block-1] boosting limit by 10
c [block-1] limit of 500000000 steps penalty 0 = 0 + 0
c [block-1] fully completed
c [block-1] transition to [ all 0 rem 0 ] state
c [block-1] eliminated 11534 blocked clauses
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 23 clauses out of 398 (6%) of length 10
c [cce-1-1] eliminated 98 clauses out of 2364 (4%) of length 9
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 121 large clauses in 30000004 steps
c [cce-1-1] allowing another 15000002 steps for small clauses
c [cce-1-1] scheduling 344473 clauses = 324961 binary + 19512 ternary
c [cce-1-1] tried to eliminate 420 small clauses 0%
c [cce-1-1] eliminated 153 binary clauses 0%
c [cce-1-1] eliminated 12 ternary clauses 0%
c [cce-1-1] eliminated 165 small clauses 0%
c [cce-1-1] eliminated 165 small clauses in 30000006 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 286 covered clauses in round 1
c [cce-1] eliminated 286 covered clauses in TOTAL during 1 rounds
c [cce-1] 286 < 1/100 * 655944 = 6559 considered unsuccessful
c [bca-1] limit of 10000000 steps and 1311816 added (scaled 2)
c [bca-1] 173990 out of 194090 literals actually usable 90%
c [bca-1] added 262 blocked clauses in 529901 steps
c [sweep-1] limit 1311316 based on 655658 irredundant clauses
c [sweep-1-1] 5841 pos 6.0% + 91203 neg 94.0% = 97044 sched 100.0% ret 0
c [sweep-1-1] 1425715 steps 21 queries 26035.95 avg class size
c [sweep-1-1] 142 decisions 14 SAT calls 75.29 avg env size
c [sweep-1-1] 96972 variables remain 100% (48 retained 0%)
c [decomp-10] removed 109 variables
c [sweep-1-1] removed 109 vars (0 failed, 7 eqs, 13 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 109 vars in TOTAL (1 rounds, 20 queries)
c [phase-count-5] 648656 negative 99.0% of 655148 except 6492 1.0%
c [phase-count-5] 528789 positive 80.7% of 655148 except 126359 19.3%
c [phase-count-5] less non-negative clauses 6492 than limit 65500 (10.0%)
c [phase-count-5] non-pos/non-neg = 126359/6492 = 19.46 >= 2.00 = 200/100
c [lucky-phase-5] forcing lucky phase -1
c [phase-5] phase bias: 0 positive 0%, 1098 negative 100%
c [sort-queue-5] sorted 54757 enqueued variables after 5050 conflicts
c [score-dist-5] active 42178 (44%), one 0 (0%), zero 54757 (56%)
c [score-dist-5] max exp 508, different 27 (5%)
c [score-dist-5] median active exp 500, avg 498.1
c [simplification-5] removed 4160 variables 4.1% (96935 remain 39%)
c [simplification-5] removed 60597 irredundant clauses 8.5% (655148 remain 48%)
c [simplification-5] maximum reduction of 8% = max (4%, 8%)
c [simplification-5] large reduction 8% >= 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 17050 (soft 7050 + delta 10000)
c [simplification-5] new conflict limit 7050 (hard 17050)
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   28.5   96934   655148      5181    3715    287 59563   94   403   52  23%      2  391  132    8 1572%
c i   28.6   96931   655148      5189    3719    287 59566   94   404   52  23%      2  392  130    8 1539%
c i   28.7   96926   655148      5227    3752    287 59568   97   410   52  24%      2  397  159    9 1851%
c i   28.8   96918   655148      5275    3791    291 59570   98   417   52  24%      2  404  167    9 1904%
c i   28.8   96907   655148      5276    3791    291 59570   98   416   52  24%      2  404  166    9 1897%
c i   29.4   96900   655148      5593    4054    303 59583  101   447   52  22%      2  433  157    9 1684%
c i   30.0   96773   655148      5910    4300    311 59596  110   465   52  24%      2  448  206   10 1990%
c i   30.0   96772   655148      5911    4300    311 59596  110   464   52  24%      2  448  206   10 1982%
c i   30.3   96771   655148      6074    4449    316 59598  116   476   53  24%      2  458  234   11 2126%
c i   30.3   96757   655148      6081    4452    316 59598  117   476   53  25%      2  458  241   11 2182%
c i   30.3   96756   655148      6082    4452    316 59598  117   476   53  25%      2  458  240   11 2174%
c i   30.5   96691   655148      6196    4547    318 59599  116   485   53  24%      2  466  185   11 1655%
c i   30.5   96690   655148      6220    4568    318 59599  116   486   53  24%      2  467  182   11 1614%
c i   30.6   96689   655148      6224    4571    318 59599  116   486   53  24%      2  468  180   11 1600%
c i   30.6   96688   655148      6233    4578    318 59599  116   487   53  24%      2  468  181   11 1606%
c i   30.7   96687   655148      6258    4597    319 59601  119   489   53  24%      2  470  207   11 1808%
c i   30.7   96686   655148      6259    4597    319 59601  118   489   53  24%      2  470  206   11 1801%
c i   30.7   96683   655148      6270    4604    319 59603  120   490   53  24%      2  470  219   12 1900%
c i   30.7   96682   655148      6271    4604    319 59603  120   489   53  24%      2  470  218   12 1893%
c i   30.7   96681   655148      6272    4604    319 59603  120   489   53  24%      2  470  218   12 1886%
c i   30.7   96680   655148      6273    4604    319 59603  119   489   53  24%      2  470  217   12 1878%
c i   30.7   96679   655148      6286    4610    319 59606  120   490   53  25%      2  471  223   12 1924%
c i   30.8   96678   655148      6287    4610    319 59606  120   490   53  25%      2  471  222   12 1916%
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   30.8   96677   655148      6321    4636    319 59608  123   492   53  25%      2  473  258   12 2179%
c i   31.6   96670   655148      6735    4967    328 59640  131   524   53  25%      2  502  225   13 1726%
c i   31.6   96669   655148      6740    4971    328 59640  131   524   53  25%      2  502  232   13 1773%
c i   32.0   96668   655148      6915    5125    331 59641  138   534   55  26%      2  510  244   14 1771%
c i   32.1   96667   655148      6971    5178    331 59641  138   536   55  26%      2  512  235   14 1683%
c 
c [simplification-6] limit 7137 conflicts (hard 17050) hit after 7142 conflicts
c [quatres-2] found 39553 quaternary clauses 37% in total
c [quatres-2-2] added 2 single-self-subsuming ternary resolvents
c [quatres-2-2] added 2 quaternary resolvents
c [ternres-2] limit 4579005 with penalty 0 = 0 + 0
c [ternres-2] all 96382 free variables schedulable
c [ternres-2] 0 ternary resolvents (0 bin, 0 trn)
c [ternres-2] 63897 variables remain 66% (32485 retained 34%)
c [card-3] limit 572375 penalty 2 = 2 + 0
c [card-3] found 2234 at-most-one constraints of average size 4.2
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 572375 for elimination
c [card-3] 2234 out of 2234 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [decomp-11] removed 588 variables
c [simpleprobe-3] 10900 schedulable variables 11%
c [simpleprobe-3] limit 18316021 penalty 0 = 0 + 0
c [decomp-12] removed 247 variables
c [simpleprobe-3] 3454 variables remain 4% (92646 retained 96%)
c [simpleprobe-3] removed 247 variables, found 18579 hbrs, 95 units
c [unhide-6] limit 457900 with penalty 1 = 0 + 1
c [unhide-6-6] 4 units, 1394 failed, 14134 tauts, 0 hbrs, 38390 literals
c [transred-2] limit 2000000 with penalty 0 = 0 + 0
c [transred-2] removed 305 transitive binary clauses
c [transred-2] found 9 units
c [block-2] scheduling all variables this time
c [block-2] scheduled 94736 variables 100%
c [block-2] limit of 50000000 steps penalty 0 = 0 + 0
c [block-2] fully completed
c [block-2] transition to [ all 0 rem 0 ] state
c [block-2] eliminated 719 blocked clauses
c [block-2] 719 < 1/100 * 647850 = 6478 considered unsuccessful
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 94736 variables 100%
c [elim-5] limit of 45790053 steps penalty 1 = 1 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5] incomplete 5400 not tried 6% in round 1
c [elim-5] transition to [ all 1 rem 1 ] state
c [elim-5] eliminated 1148 = 1% variables out of 94736 scheduled
c [bca-2] limit of 10000000 steps and 1259287 added (scaled 2)
c [bca-2] 167811 out of 187178 literals actually usable 90%
c [bca-2] added 150 blocked clauses in 520983 steps
c [sweep-2] limit 1373701 penalty 0 = 0 + 0
c [sweep-2-1] 4825 pos 5.2% + 88722 neg 94.8% = 93547 sched 100.0% ret 41
c [sweep-2-1] 1530659 steps 12 queries 21154.17 avg class size
c [sweep-2-1] 90 decisions 9 SAT calls 79.78 avg env size
c [sweep-2-1] 93421 variables remain 100% (61 retained 0%)
c [decomp-13] removed 108 variables
c [sweep-2-1] removed 108 vars (0 failed, 2 eqs, 2 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 108 vars in TOTAL (1 rounds, 11 queries)
c [phase-count-6] 622615 negative 99.0% of 628938 except 6323 1.0%
c [phase-count-6] 503499 positive 80.1% of 628938 except 125439 19.9%
c [phase-count-6] less non-negative clauses 6323 than limit 62800 (10.0%)
c [phase-count-6] non-pos/non-neg = 125439/6323 = 19.84 >= 2.00 = 200/100
c [lucky-phase-6] forcing lucky phase -1
c [phase-6] phase bias: 0 positive 0%, 894 negative 100%
c [sort-queue-6] sorted 47924 enqueued variables after 7142 conflicts
c [score-dist-6] active 45556 (49%), one 0 (0%), zero 47924 (51%)
c [score-dist-6] max exp 510, different 37 (7%)
c [score-dist-6] median active exp 496, avg 494.6
c [simplification-6] removed 2902 variables 3.0% (93480 remain 38%)
c [simplification-6] removed 26210 irredundant clauses 4.0% (628938 remain 46%)
c [simplification-6] maximum reduction of 4% = max (3%, 4%)
c [simplification-6] geometric conflict interval increment 4000 = 20000 / 5
c [simplification-6] new conflict interval 4000
c [simplification-6] penalized conflict interval 4000 = 1 * 4000
c [simplification-6] hard conflict limit 21142 (soft 11142 + delta 10000)
c [simplification-6] new conflict limit 11142 (hard 21142)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   37.6   93479   628938      7386    4750    341 61811  142   531   53  27%      2  504  205   15 1367%
c i   37.7   93470   628938      7446    4781    342 61814  144   529   53  27%      2  501  217   15 1426%
c i   37.7   93469   628938      7447    4781    342 61814  144   529   53  27%      2  501  216   15 1420%
c i   37.7   93468   628938      7448    4781    342 61814  144   529   53  27%      2  501  215   15 1415%
c i   37.7   93467   628938      7449    4781    342 61814  144   529   53  27%      2  501  214   15 1409%
c i   37.8   93466   628938      7453    4784    342 61814  144   529   53  27%      2  501  213   15 1399%
c i   37.9   93465   628938      7527    4834    344 61814  145   528   53  28%      2  499  216   15 1399%
c i   38.9   93464   628938      7964    5085    364 61857  146   513   53  28%      3  481  131   16  805%
c i   40.4   93452   628938      8910    5914    380 61885  138   570   53  24%      6  531   96   18  545%
c 
c [simplification-7] limit of 420 binary hit after 420 binaries
c [quatres-3] found 40980 quaternary clauses 38% in total
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] extracted 20 xors of average arity 3.0
c [gauss-2] connected 60 occurrences of 57 variables (average 1.1)
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] fully completed
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-14] removed 10 variables
c [treelook-3] limit 562543 penalty 0 = 0 + 0 boost 1
c [treelook-3] scheduled 80353 literals 43%
c [treelook-3] scheduling used 563238 steps
c [treelook-3] not fully scheduled
c [treelook-3] limit 562543 penalty 0 = 0 + 0 boost 1
c [treelook-3] used 617951 steps
c [treelook-3] 80294 literals remain 43%
c [treelook-3] 27479 variables remain to probed next time 29%
c [decomp-15] removed 51 variables
c [treelook-3] removed 51 variables, found 5580 hbrs
c [unhide-7] limit 562543 with penalty 1 = 0 + 1
c [unhide-7-7] 3 units, 231 failed, 14108 tauts, 0 hbrs, 26229 literals
c [transred-3] limit 2000000 with penalty 0 = 0 + 0
c [transred-3] removed 240 transitive binary clauses
c [transred-3] found 8 units
c [cce-2] limit of 15000000 steps penalty 1 = 1 + 0
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] allowing another 7500004 steps for small clauses
c [cce-2-1] scheduling 326190 clauses = 305794 binary + 20396 ternary
c [cce-2-1] tried to eliminate 257 small clauses 0%
c [cce-2-1] eliminated 78 binary clauses 0%
c [cce-2-1] eliminated 13 ternary clauses 0%
c [cce-2-1] eliminated 91 small clauses 0%
c [cce-2-1] eliminated 3812 small clauses in 15000000 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 3812 covered clauses in round 1
c [cce-2] eliminated 3812 covered clauses in TOTAL during 1 rounds
c [cce-2] 3812 < 1/100 * 617471 = 6174 considered unsuccessful
c [elim-6] 5396 variables 6% will be scheduled this time
c [elim-6] scheduled 5396 variables 6%
c [elim-6] limit of 112508667 steps penalty 0 = 0 + 0
c [elim-6] rescheduling of touched variables disabled
c [elim-6-1] no variable eliminated in round 1 in 13682707 steps
c [elim-6] fully completed in 1 rounds
c [elim-6] transition to [ all 0 rem 0 ] state
c [elim-6] eliminated 0 = 0% variables out of 5396 scheduled
c [bca-3] limit of 10000000 steps and 1227550 added (scaled 2)
c [bca-3] 163574 out of 186026 literals actually usable 88%
c [bca-3] added 75 blocked clauses in 497426 steps
c [sweep-3] limit 1687630 penalty 0 = 0 + 0
c [sweep-3-1] 4783 pos 5.1% + 88170 neg 94.9% = 92953 sched 99.9% ret 59
c [sweep-3-1] 1774556 steps 23 queries 18819.74 avg class size
c [sweep-3-1] 250 decisions 17 SAT calls 56.88 avg env size
c [sweep-3-1] 92851 variables remain 100% (153 retained 0%)
c [decomp-16] removed 14 variables
c [sweep-3-1] removed 14 vars (0 failed, 6 eqs, 11 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 14 vars in TOTAL (1 rounds, 22 queries)
c [phase-count-7] 607004 negative 99.0% of 613327 except 6323 1.0%
c [phase-count-7] 490226 positive 79.9% of 613327 except 123101 20.1%
c [phase-count-7] less non-negative clauses 6323 than limit 61300 (10.0%)
c [phase-count-7] non-pos/non-neg = 123101/6323 = 19.47 >= 2.00 = 200/100
c [lucky-phase-7] forcing lucky phase -1
c [phase-7] phase bias: 0 positive 0%, 827 negative 100%
c [sort-queue-7] sorted 45682 enqueued variables after 9147 conflicts
c [score-dist-7] active 47316 (51%), one 0 (0%), zero 45682 (49%)
c [score-dist-7] max exp 509, different 44 (9%)
c [score-dist-7] median active exp 497, avg 492.8
c [simplification-7] removed 454 variables 0.5% (92998 remain 38%)
c [simplification-7] removed 15611 irredundant clauses 2.5% (613327 remain 45%)
c [simplification-7] maximum reduction of 2% = max (0%, 2%)
c [simplification-7] forced so keeping old conflict interval 4000
c [simplification-7] conflict limit remains at 11174 (hard 21142)
c [simplification-7] 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   44.4   92997   613327      9172    6123    389 65058  143   579   54  25%      5  538  175   18  946%
c i   44.4   92994   613327      9175    6125    389 65058  143   579   54  25%      5  538  174   18  944%
c i   44.5   92985   613327      9177    6126    389 65058  143   579   54  25%      5  538  173   18  936%
c i   44.5   92978   613327      9178    6126    389 65058  143   579   54  25%      5  538  172   18  933%
c i   44.5   92972   613327      9180    6127    389 65058  143   578   54  25%      5  537  171   18  925%
c i   44.5   92962   613327      9188    6127    389 65065  143   578   54  25%      5  537  166   18  897%
c i   44.5   92956   613327      9189    6127    389 65065  143   578   54  25%      5  537  165   18  894%
c i   44.5   92949   613327      9196    6129    389 65069  143   578   54  25%      5  536  161   18  870%
c i   45.5   92942   613327      9778    6597    415 65111  136   606   55  22%      5  560  103   19  540%
c i   46.3   92924   613327     10258    6977    439 65144  140   635   55  22%      4  585  194   20  965%
c i   46.8   92923   613327     10579    7192    447 65195  142   627   55  23%      4  574  172   21  826%
c i   47.0   92920   613327     10683    7274    455 65202  140   628   55  22%      3  575  138   21  660%
c i   47.2   92913   613327     10776    7351    458 65204  138   629   55  22%      3  575  117   21  557%
c i   47.9   92912   613327     11149    7658    469 65214  141   634   55  22%      3  576  174   22  795%
c i   48.0   92896   613327     11170    7668    475 65218  141   632   55  22%      3  574  160   22  734%
c 
c [simplification-8] limit 11209 conflicts (hard 21142) hit after 11209 conflicts
c [ternres-3] limit 3319384 with penalty 1 = 1 + 0
c [ternres-3] 61578 schedulable variables 66%
c [ternres-3] 6 ternary resolvents (0 bin, 6 trn)
c [ternres-3] 36438 variables remain 39% (56458 retained 61%)
c [decomp-17] removed 112 variables
c [basicprobe-3] limit 33193845 penalty 0 = 0 + 0
c [basicprobe-3-0] 34335 probes remain 38% after last round
c [basicprobe-3-0] 143 units = 143 failed (100%) + 0 lifted (0%)
c [basicprobe-3-0] removed 1563 variables, found 37345 hbrs
c [bate-2] eliminated 71 asymmetric tautologies during probing
c [unhide-8] limit 663876 with penalty 1 = 0 + 1
c [unhide-8-8] 12 units, 1153 failed, 11441 tauts, 0 hbrs, 37206 literals
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 244 transitive binary clauses
c [transred-4] found 4 units
c [block-3] scheduling all variables this time
c [block-3] scheduled 90247 variables 100%
c [block-3] limit of 33193845 steps penalty 1 = 1 + 0
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 34 blocked clauses
c [block-3] 34 < 1/100 * 603495 = 6034 considered unsuccessful
c [bca-4] limit of 10000000 steps and 1183989 added (scaled 2)
c [bca-4] 155528 out of 180496 literals actually usable 86%
c [bca-4] added 116 blocked clauses in 462607 steps
c [sweep-4] limit 1991630 penalty 0 = 0 + 0
c [sweep-4-1] 5441 pos 6.0% + 84675 neg 94.0% = 90116 sched 99.9% ret 131
c [sweep-4-1] 2003926 steps 28 queries 23104.75 avg class size
c [sweep-4-1] 250 decisions 24 SAT calls 41.50 avg env size
c [sweep-4-1] 90009 variables remain 100% (238 retained 0%)
c [decomp-18] removed 56 variables
c [sweep-4-1] removed 56 vars (0 failed, 3 eqs, 10 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 56 vars in TOTAL (1 rounds, 27 queries)
c [phase-count-8] 585188 negative 98.9% of 591508 except 6320 1.1%
c [phase-count-8] 470541 positive 79.5% of 591508 except 120967 20.5%
c [phase-count-8] less non-negative clauses 6320 than limit 59100 (10.0%)
c [phase-count-8] non-pos/non-neg = 120967/6320 = 19.14 >= 2.00 = 200/100
c [lucky-phase-8] forcing lucky phase -1
c [phase-8] phase bias: 0 positive 0%, 748 negative 100%
c [sort-queue-8] sorted 40754 enqueued variables after 11209 conflicts
c [score-dist-8] active 49437 (55%), one 0 (0%), zero 40754 (45%)
c [score-dist-8] max exp 509, different 52 (10%)
c [score-dist-8] median active exp 497, avg 492.4
c [simplification-8] removed 2705 variables 2.9% (90191 remain 37%)
c [simplification-8] removed 21819 irredundant clauses 3.6% (591508 remain 43%)
c [simplification-8] maximum reduction of 4% = max (3%, 4%)
c [simplification-8] geometric conflict interval increment 4000 = 20000 / 5
c [simplification-8] new conflict interval 8000
c [simplification-8] penalized conflict interval 8000 = 1 * 8000
c [simplification-8] hard conflict limit 29209 (soft 19209 + delta 10000)
c [simplification-8] new conflict limit 19209 (hard 29209)
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   51.7   90190   591508     11265    7707    484 87909  141   625   53  23%      3  566  162   22  734%
c i   51.9   90189   591508     11382    7775    492 87917  141   616   54  23%      2  556  147   22  662%
c i   52.1   90188   591508     11637    7973    512 87934  135   595   55  23%      2  533   89   22  399%
c i   52.1   90187   591508     11645    7977    512 87937  135   595   55  23%      2  533   89   22  399%
c i   52.1   90186   591508     11648    7978    512 87938  135   594   55  23%      2  532   90   22  400%
c i   52.1   90185   591508     11661    7984    512 87944  135   594   55  23%      2  531   93   22  415%
c i   52.1   90184   591508     11662    7984    512 87944  135   593   55  23%      2  531   92   22  413%
c i   52.1   90183   591508     11663    7984    512 87944  135   593   55  23%      2  531   92   22  411%
c i   52.1   90182   591508     11664    7984    512 87944  135   593   55  23%      2  531   92   22  410%
c i   52.2   90181   591508     11754    8055    515 87947  136   589   55  23%      2  525  110   23  486%
c i   52.3   90140   591508     11792    8077    515 87949  137   587   55  23%      2  523  131   23  578%
c i   52.3   90139   591508     11804    8083    515 87954  137   586   55  23%      2  522  131   23  576%
c i   52.3   90138   591508     11857    8125    515 87955  138   583   55  24%      2  519  153   23  666%
c i   52.3   90137   591508     11858    8125    515 87955  138   583   55  24%      2  519  152   23  663%
c i   52.3   90136   591508     11859    8125    515 87955  138   583   55  24%      2  519  151   23  660%
c i   52.3   90135   591508     11860    8125    515 87955  138   583   55  24%      2  519  151   23  658%
c i   52.7   90134   591508     12140    8301    522 87975  136   558   55  24%      2  492  108   23  463%
c i   52.8   89962   591508     12273    8406    523 87991  132   553   55  24%      2  486   73   23  313%
c i   52.9   89961   591508     12380    8487    523 87998  132   546   55  24%      1  478   87   23  372%
c i   53.5   89960   591508     12953    8910    556 88043  122   497   55  24%      3  426   77   24  326%
c i   53.6   89950   591508     13009    8946    557 88045  123   496   55  25%      3  424  104   24  437%
c i   53.6   89936   591508     13032    8966    557 88046  122   495   55  25%      3  423   97   24  409%
c i   53.8   89927   591508     13182    9092    558 88049  121   488   55  25%      2  415   93   24  387%
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   53.8   89926   591508     13183    9092    558 88049  121   488   55  25%      2  415   92   24  386%
c i   53.8   89925   591508     13209    9110    560 88049  121   486   55  25%      2  412   89   24  371%
c i   53.8   89924   591508     13210    9110    560 88049  121   486   55  25%      2  412   88   24  369%
c i   55.2   89921   591508     14258    9886    628 88117  116   456   57  25%      7  376  101   25  400%
c i   55.4   89916   591508     14353    9951    638 88134  114   459   57  25%      6  379   72   25  286%
c i   55.5   89411   591508     14393    9979    641 88138  113   460   57  25%      6  380   66   25  262%
c i   55.5   89410   591508     14395    9979    641 88138  113   460   57  25%      6  380   65   25  260%
c i   55.5   89409   591508     14396    9979    641 88138  113   460   57  25%      6  379   65   25  259%
c i   55.5   89408   591508     14419    9995    641 88142  112   460   57  24%      6  379   61   25  245%
c i   55.8   89407   591508     14623   10149    652 88158  112   464   57  24%      5  383   95   25  373%
c i   55.8   89406   591508     14624   10149    652 88158  112   464   57  24%      5  383   94   25  372%
c i   55.8   89405   591508     14625   10149    652 88158  112   464   57  24%      5  382   94   25  370%
c i   55.8   89404   591508     14626   10149    652 88158  112   464   57  24%      5  382   93   25  369%
c i   55.8   89403   591508     14631   10149    653 88161  112   464   57  24%      5  382   92   25  362%
c i   55.8   89402   591508     14634   10149    653 88163  112   464   57  24%      5  382   91   25  357%
c i   56.4   89401   591508     14968   10379    658 88175  120   463   57  26%      4  380  181   26  688%
c i   56.4   89400   591508     14980   10388    658 88177  121   463   57  26%      4  380  190   26  718%
c i   56.4   89395   591508     14981   10388    658 88177  121   463   57  26%      4  380  189   26  715%
c i   56.4   89390   591508     14982   10388    658 88177  121   463   57  26%      4  379  188   26  712%
c i   56.4   89386   591508     14992   10395    658 88177  121   463   57  26%      4  380  191   26  724%
c i   56.4   89385   591508     14993   10395    658 88177  121   463   57  26%      4  380  191   26  721%
c i   56.4   89384   591508     14994   10395    658 88177  121   463   57  26%      4  379  190   26  718%
c i   56.8   89383   591508     15235   10551    663 88212  127   465   57  27%      3  380  216   27  794%
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   56.8   89360   591508     15240   10552    664 88212  127   465   57  27%      3  380  212   27  779%
c i   56.8   89343   591508     15243   10552    664 88213  127   465   57  27%      3  380  210   27  771%
c i   56.8   89339   591508     15244   10552    664 88213  127   465   57  27%      3  380  209   27  768%
c i   56.9   89329   591508     15342   10622    676 88227  125   471   57  26%      3  385  150   27  553%
c i   57.0   89318   591508     15343   10622    676 88227  125   471   57  26%      3  385  150   27  550%
c i   57.4   89306   591508     15635   10851    688 88253  119   490   57  24%      3  403   72   27  266%
c i   57.4   89297   591508     15651   10865    688 88254  119   492   57  24%      3  405   70   27  258%
c i   58.0   89288   591508     15928   11108    701 88260  118   526   57  22%      2  437  101   28  365%
c i   58.1   89287   591508     15950   11128    701 88260  119   530   57  22%      2  440  118   28  426%
c i   58.1   89286   591508     15962   11139    701 88260  119   531   57  22%      2  442  124   28  448%
c i   58.2   89285   591508     15993   11161    701 88261  120   537   57  22%      2  447  145   28  522%
c i   58.2   89284   591508     15994   11161    701 88261  120   536   57  22%      2  447  145   28  519%
c i   58.2   89283   591508     15995   11161    701 88261  120   536   57  22%      2  447  144   28  517%
c i   58.2   89282   591508     15999   11164    701 88261  120   537   57  22%      2  447  144   28  518%
c i   58.2   89281   591508     16001   11165    701 88261  120   537   57  22%      2  447  144   28  517%
c i   58.2   89280   591508     16003   11166    701 88261  121   537   57  22%      2  447  147   28  527%
c i   58.3   89279   591508     16004   11166    701 88261  121   537   57  22%      2  447  146   28  525%
c i   58.3   89278   591508     16005   11166    701 88261  121   536   57  22%      2  447  146   28  523%
c i   58.3   89277   591508     16006   11166    701 88261  120   536   57  22%      2  447  145   28  521%
c i   58.3   89276   591508     16011   11170    701 88261  121   537   57  22%      2  447  146   28  525%
c i   58.3   89275   591508     16012   11170    701 88261  121   537   57  22%      2  447  146   28  523%
c i   58.4   89274   591508     16026   11182    701 88261  122   539   57  23%      2  449  164   28  587%
c i   58.4   89273   591508     16030   11185    701 88261  122   539   57  23%      2  449  171   28  612%
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   58.6   89272   591508     16132   11244    701 88270  133   549   57  24%      2  459  287   29  999%
c i   58.6   89271   591508     16141   11246    701 88270  133   550   57  24%      2  459  297   29 1029%
c i   58.7   89270   591508     16142   11246    701 88270  133   550   57  24%      2  459  296   29 1025%
c i   58.8   89269   591508     16217   11290    702 88272  139   552   57  25%      2  461  332   29 1131%
c i   59.9   89268   591508     16745   11714    708 88284  153   606   57  25%      3  511  313   31 1008%
c i   59.9   89267   591508     16748   11716    708 88284  153   606   57  25%      3  511  310   31  998%
c i   60.2   89259   591508     16862   11804    712 88286  157   617   57  25%      2  521  317   32 1005%
c i   61.2   89256   591508     17232   12061    715 88297  177   647   62  27%      2  548  354   34 1053%
c i   61.2   89248   591508     17233   12061    715 88297  177   647   62  27%      2  548  352   34 1049%
c i   61.8   89243   591508     17518   12259    715 88309  200   671   62  30%      2  570  465   36 1303%
c i   64.1   89242   591508     18434   12834    725 88326  253   704   63  36%      5  595  378   42  908%
c i   64.7   89241   591508     18677   13023    727 88328  257   719   63  36%      4  607  347   43  812%
c i   65.3   89240   591508     19003   13301    730 88343  258   755   66  34%      4  640  321   44  733%
c i   65.3   89239   591508     19004   13301    730 88343  258   755   66  34%      4  640  319   44  730%
c i   65.3   89238   591508     19005   13301    730 88343  258   754   66  34%      4  640  318   44  727%
c i   65.3   89232   591508     19006   13301    730 88343  258   754   66  34%      4  640  317   44  724%
c i   65.3   89229   591508     19007   13301    730 88343  258   754   66  34%      4  639  316   44  721%
c i   65.3   89223   591508     19008   13301    730 88343  258   754   66  34%      4  639  314   44  718%
c i   65.4   89218   591508     19009   13301    730 88343  258   754   66  34%      4  639  313   44  716%
c i   65.4   89213   591508     19010   13301    730 88343  258   753   66  34%      4  639  312   44  713%
c i   65.4   89206   591508     19011   13301    730 88343  258   753   66  34%      4  639  311   44  710%
c i   65.4   89199   591508     19012   13301    730 88343  258   753   66  34%      4  638  310   44  707%
c i   65.4   89191   591508     19013   13301    730 88343  258   753   66  34%      4  638  308   44  705%
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   65.4   89186   591508     19014   13301    730 88343  258   753   66  34%      4  638  307   44  702%
c i   65.4   89180   591508     19015   13301    730 88343  258   752   66  34%      4  638  306   44  699%
c i   65.4   89174   591508     19016   13301    730 88343  257   752   66  34%      4  638  305   44  696%
c i   65.4   89169   591508     19017   13301    730 88343  257   752   66  34%      4  637  304   44  694%
c i   65.4   89158   591508     19019   13302    730 88343  258   752   66  34%      4  637  305   44  697%
c i   65.9   89155   591508     19408   13628    731 88346  261   769   69  34%      3  651  278   45  615%
c 
c [simplification-9] limit 19654 conflicts (hard 29209) hit after 19654 conflicts
c [quatres-4] found 39570 quaternary clauses 40% in total
c [quatres-4-2] added 1 single-self-subsuming ternary resolvents
c [ternres-4] limit 10491875 with penalty 0 = 0 + 0
c [ternres-4] 34878 schedulable variables 39%
c [ternres-4] 7 ternary resolvents (0 bin, 7 trn)
c [ternres-4] fully completed ternary resolution
c [decomp-19] removed 1299 variables
c [simpleprobe-4] 2963 schedulable variables 3%
c [simpleprobe-4] limit 41967502 penalty 0 = 0 + 0
c [decomp-20] removed 866 variables
c [simpleprobe-4] fully completed simple probing
c [simpleprobe-4] removed 866 variables, found 58356 hbrs, 318 units
c [unhide-9] limit 1049187 with penalty 1 = 0 + 1
c [unhide-9-9] 5 units, 188 failed, 11912 tauts, 0 hbrs, 166212 literals
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 281 transitive binary clauses
c [transred-5] found 8 units
c [elim-7] scheduling all variables this time
c [elim-7] scheduled 87776 variables 100%
c [elim-7] limit of 104918755 steps penalty 1 = 1 + 0
c [elim-7] rescheduling of touched variables disabled
c [elim-7-1] eliminated 1896 variables 2% in round 1 in 55425336 steps
c [elim-7-1] backward subsumption/strengthening limit 49493419
c [elim-7-1-1] backward checking 6597 touched variables 8%
c [elim-7-1-1] fully completed backward checking in 1 rounds
c [elim-7-1] subsumed 0 and strengthened 262 clauses in 4879782 steps
c [elim-7-1] rescheduled 590 variables 1% by backward subsumption
c [elim-7-2] eliminated 92 variables 0% in round 2 in 3893327 steps
c [elim-7-2] backward subsumption/strengthening limit 3893300
c [elim-7-2-1] backward checking 636 touched variables 1%
c [elim-7-2-1] fully completed backward checking in 1 rounds
c [elim-7-2] subsumed 1 and strengthened 4 clauses in 469840 steps
c [elim-7-2] rescheduled 12 variables 0% by backward subsumption
c [elim-7-3] no variable eliminated in round 3 in 9479 steps
c [elim-7] fully completed in 3 rounds
c [elim-7] transition to [ all 0 rem 0 ] state
c [elim-7] eliminated 2035 = 2% variables out of 87776 scheduled
c [bca-5] limit of 10000000 steps and 1119593 added (scaled 2)
c [bca-5] 144740 out of 171484 literals actually usable 84%
c [bca-5] added 72 blocked clauses in 422640 steps
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 31475620 penalty 0 = 0 + 0
c [sweep-5-1] 5040 pos 5.9% + 80486 neg 94.1% = 85526 sched 99.7% ret 215
c [sweep-5-1] 31542451 steps 391 queries 1793.94 avg class size
c [sweep-5-1] 2676 decisions 315 SAT calls 64.03 avg env size
c [sweep-5-1] 75433 variables remain 89% (9682 retained 11%)
c [decomp-21] removed 811 variables
c [sweep-5-1] removed 811 vars (0 failed, 94 eqs, 144 impls)
c [sweep-5] considered successful since not run to completion yet
c [sweep-5] removed 811 vars in TOTAL (1 rounds, 390 queries)
c [phase-count-9] 547718 negative 98.9% of 553975 except 6257 1.1%
c [phase-count-9] 437813 positive 79.0% of 553975 except 116162 21.0%
c [phase-count-9] less non-negative clauses 6257 than limit 55300 (10.0%)
c [phase-count-9] non-pos/non-neg = 116162/6257 = 18.57 >= 2.00 = 200/100
c [lucky-phase-9] forcing lucky phase -1
c [phase-9] phase bias: 0 positive 0%, 465 negative 100%
c [sort-queue-9] sorted 31564 enqueued variables after 19654 conflicts
c [score-dist-9] active 53366 (63%), one 0 (0%), zero 31564 (37%)
c [score-dist-9] max exp 509, different 85 (17%)
c [score-dist-9] median active exp 500, avg 490.5
c [simplification-9] removed 4009 variables 4.5% (84930 remain 35%)
c [simplification-9] removed 37533 irredundant clauses 6.3% (553975 remain 40%)
c [simplification-9] maximum reduction of 6% = max (5%, 6%)
c [simplification-9] large reduction 6% >= 5% limit
c [simplification-9] next conflict interval 2000 = 2000/1
c [simplification-9] penalized conflict interval 2000 = 1 * 2000
c [simplification-9] hard conflict limit 31654 (soft 21654 + delta 10000)
c [simplification-9] new conflict limit 21654 (hard 31654)
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   76.0   84929   553975     20746    9919    656 151662  278   816   55  34%      9  684  371   51  732%
c i   76.0   84926   553975     20747    9919    656 151662  278   815   55  34%      9  684  370   51  730%
c i   76.0   84924   553975     20748    9919    656 151662  278   815   55  34%      9  683  368   51  727%
c i   76.5   84918   553975     20973   10100    656 151671  286   821   55  35%      8  687  401   52  773%
c i   76.5   84914   553975     20974   10100    656 151671  286   821   55  35%      8  687  400   52  770%
c i   76.5   84907   553975     20975   10100    656 151671  286   821   55  35%      8  687  398   52  767%
c i   76.5   84903   553975     20977   10101    656 151671  286   821   55  35%      8  687  395   52  761%
c i   77.0   84898   553975     21224   10286    664 151673  291   826   55  35%      6  689  409   53  769%
c i   77.1   84894   553975     21279   10327    664 151673  293   825   55  36%      6  688  424   53  794%
c i   77.3   84893   553975     21381   10402    664 151676  296   827   57  36%      5  688  423   54  782%
c i   77.8   84889   553975     21606   10554    664 151676  305   831   57  37%      4  690  457   55  824%
c i   77.8   84881   553975     21607   10554    664 151676  305   831   57  37%      4  690  455   55  821%
c i   78.0   84874   553975     21702   10616    664 151676  308   834   57  37%      4  693  454   56  812%
c 
c [simplification-10] limit 21709 conflicts (hard 31654) hit after 21709 conflicts
c [quatres-5] found 40473 quaternary clauses 41% in total
c [quatres-5-2] added 4 quaternary resolvents
c [ternres-5] limit 11607489 with penalty 0 = 0 + 0
c [ternres-5] all 84863 free variables schedulable
c [ternres-5] 287 ternary resolvents (0 bin, 287 trn)
c [ternres-5] fully completed ternary resolution
c [card-4] limit 725468 penalty 3 = 3 + 0
c [card-4] found 2587 at-most-one constraints of average size 4.1
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 725468 for elimination
c [card-4] 2587 out of 2587 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [gauss-3] limit 580374 penalty 2 = 2 + 0
c [gauss-3] extracted 11 xors of average arity 2.9
c [gauss-3] connected 32 occurrences of 29 variables (average 1.1)
c [gauss-3] limit 580374 penalty 2 = 2 + 0
c [gauss-3] fully completed
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-22] removed 14 variables
c [treelook-4] limit 1160748 penalty 0 = 0 + 0 boost 1
c [treelook-4] scheduled 118380 literals 70%
c [treelook-4] scheduling used 1160750 steps
c [treelook-4] not fully scheduled
c [treelook-4] limit 1160748 penalty 0 = 0 + 0 boost 1
c [treelook-4] used 1405008 steps
c [treelook-4] 118309 literals remain 70%
c [treelook-4] 24039 variables remain to probed next time 28%
c [treelook-4] removed 48 variables, found 7824 hbrs
c [unhide-10] limit 1160748 with penalty 1 = 0 + 1
c [unhide-10-10] 9 units, 481 failed, 19175 tauts, 0 hbrs, 92882 literals
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 262 transitive binary clauses
c [transred-6] found 5 units
c [cce-3] limit of 14509362 steps penalty 2 = 2 + 0
c [cce-3-1] eliminated 4 clauses out of 1513 (0%) of length 9
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 4 large clauses in 14509366 steps
c [cce-3-1] allowing another 7254683 steps for small clauses
c [cce-3-1] scheduling 302072 clauses = 280033 binary + 22039 ternary
c [cce-3-1] tried to eliminate 237 small clauses 0%
c [cce-3-1] eliminated 73 binary clauses 0%
c [cce-3-1] eliminated 8 ternary clauses 0%
c [cce-3-1] eliminated 81 small clauses 0%
c [cce-3-1] eliminated 7197 small clauses in 14509374 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 7201 covered clauses in round 1
c [cce-3] eliminated 7201 covered clauses in TOTAL during 1 rounds
c [elim-8] scheduling all variables this time
c [elim-8] scheduled 84050 variables 100%
c [elim-8] boosting limit by 20
c [elim-8] limit of 4642995920 steps penalty 0 = 0 + 0
c [elim-8] rescheduling of touched variables disabled
c [elim-8-1] eliminated 1253 variables 1% in round 1 in 53436047 steps
c [elim-8-1] backward subsumption/strengthening limit 53436000
c [elim-8-1-1] backward checking 4497 touched variables 5%
c [elim-8-1-1] fully completed backward checking in 1 rounds
c [elim-8-1] subsumed 11 and strengthened 87 clauses in 1886700 steps
c [elim-8-1] rescheduled 206 variables 0% by backward subsumption
c [elim-8-2] eliminated 27 variables 0% in round 2 in 479499 steps
c [elim-8-2] backward subsumption/strengthening limit 479400
c [elim-8-2-1] backward checking 200 touched variables 0%
c [elim-8-2-1] fully completed backward checking in 1 rounds
c [elim-8-2] subsumed 0 and strengthened 0 clauses in 195999 steps
c [elim-8] fully completed in 2 rounds
c [elim-8] transition to [ all 0 rem 0 ] state
c [elim-8] eliminated 1282 = 2% variables out of 84050 scheduled
c [bca-6] limit of 10000000 steps and 1082571 added (scaled 2)
c [bca-6] 141139 out of 165538 literals actually usable 85%
c [bca-6] added 146 blocked clauses in 416883 steps
c [sweep-6] limit 3482246 penalty 0 = 0 + 0
c [sweep-6-1] 4141 pos 5.6% + 69581 neg 94.4% = 73722 sched 89.1% ret 9046
c [sweep-6-1] 3535475 steps 52 queries 12403.88 avg class size
c [sweep-6-1] 381 decisions 44 SAT calls 65.23 avg env size
c [sweep-6-1] 73354 variables remain 89% (9413 retained 11%)
c [decomp-24] removed 9 variables
c [sweep-6-1] removed 9 vars (0 failed, 7 eqs, 14 impls)
c [sweep-6] considered successful since not run to completion yet
c [sweep-6] removed 9 vars in TOTAL (1 rounds, 51 queries)
c [phase-count-10] 534787 negative 98.9% of 540852 except 6065 1.1%
c [phase-count-10] 425342 positive 78.6% of 540852 except 115510 21.4%
c [phase-count-10] less non-negative clauses 6065 than limit 54000 (10.0%)
c [phase-count-10] non-pos/non-neg = 115510/6065 = 19.05 >= 2.00 = 200/100
c [lucky-phase-10] forcing lucky phase -1
c [phase-10] phase bias: 0 positive 0%, 432 negative 100%
c [sort-queue-10] sorted 30068 enqueued variables after 21709 conflicts
c [score-dist-10] active 52691 (64%), one 0 (0%), zero 30068 (36%)
c [score-dist-10] max exp 510, different 94 (18%)
c [score-dist-10] median active exp 496, avg 489.1
c [simplification-10] removed 2104 variables 2.5% (82759 remain 34%)
c [simplification-10] removed 13123 irredundant clauses 2.4% (540852 remain 39%)
c [simplification-10] maximum reduction of 2% = max (2%, 2%)
c [simplification-10] geometric conflict interval increment 6666 = 20000 / 3
c [simplification-10] new conflict interval 14666
c [simplification-10] penalized conflict interval 14666 = 1 * 14666
c [simplification-10] hard conflict limit 46375 (soft 36375 + delta 10000)
c [simplification-10] new conflict limit 36375 (hard 46375)
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   84.2   82758   540852     22118    8233    800 137584  310   844   50  37%      3  698  356   58  618%
c i   84.2   82757   540852     22119    8233    800 137584  310   844   50  37%      3  698  355   58  615%
c i   84.2   82756   540852     22120    8233    800 137584  310   844   50  37%      3  698  353   58  613%
c i   84.2   82750   540852     22121    8233    800 137584  310   844   50  37%      3  698  352   58  610%
c i   84.2   82749   540852     22122    8233    800 137584  310   844   50  37%      3  698  351   58  608%
c i   85.0   82748   540852     22510    8505    830 137594  307   855   51  36%      3  704  270   59  458%
c i   85.2   82744   540852     22581    8559    831 137594  309   854   51  36%      3  703  307   59  518%
c i   87.0   82731   540852     23406    9170    846 137608  339   885   53  38%      5  726  527   64  819%
c i   87.2   82730   540852     23481    9229    846 137609  341   886   55  38%      4  726  511   65  789%
c i   87.3   82729   540852     23561    9298    846 137610  342   888   55  39%      4  726  479   65  735%
c i   87.4   82728   540852     23564    9300    846 137610  342   888   55  39%      4  726  474   65  728%
c i   87.6   82727   540852     23632    9350    846 137611  345   889   55  39%      4  727  495   66  753%
c i   88.7   82726   540852     24203    9799    879 137628  330   892   55  37%      4  724  296   67  441%
c i   89.8   82723   540852     24681   10134    898 137680  315   857   55  37%      3  684  218   68  320%
c i   91.3   82722   540852     25256   10501    904 137685  308   807   59  38%      3  627  238   70  341%
c i   91.7   82721   540852     25472   10636    905 137693  305   786   59  39%      3  605  232   70  330%
c i   91.7   82720   540852     25473   10636    905 137693  305   786   59  39%      3  605  231   70  329%
c i   91.8   82719   540852     25506   10654    905 137707  303   783   59  39%      3  601  214   70  305%
c i   91.8   82718   540852     25521   10662    906 137710  302   781   59  39%      3  599  206   70  293%
c i   93.1   82136   540852     26030   11068    907 137722  288   739   59  39%      3  553  213   71  300%
c i   93.1   82135   540852     26038   11074    907 137723  287   738   59  39%      3  552  209   71  294%
c i   93.1   82134   540852     26065   11096    907 137723  286   735   59  39%      3  548  197   71  277%
c i   93.4   82131   540852     26177   11172    907 137725  283   722   59  39%      2  535  180   71  253%
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   93.6   82130   540852     26268   11235    907 137728  279   712   59  39%      2  524  163   71  229%
c i   94.0   82129   540852     26486   11378    908 137729  271   690   59  39%      2  500  136   71  190%
c i   94.5   82128   540852     26649   11468    908 137729  268   675   59  40%      2  484  172   72  239%
c i   96.0   82127   540852     27396   11928    921 137745  261   637   60  41%      3  440  240   73  326%
c i   96.3   82126   540852     27543   12056    924 137748  258   633   60  41%      3  436  206   74  280%
c i   96.3   82125   540852     27545   12056    924 137748  258   633   60  41%      3  436  206   74  280%
c i   96.3   82122   540852     27547   12057    924 137748  258   633   60  41%      3  435  205   74  279%
c i   96.6   82118   540852     27728   12199    926 137752  251   615   60  41%      3  416  147   74  199%
c i   97.2   82109   540852     28240   12561    928 137756  231   560   60  41%      3  359   85   74  116%
c i   97.3   82103   540852     28354   12650    931 137766  226   554   60  41%      2  352   74   74  100%
c i   99.7   82094   540852     29408   13427    948 137794  246   591   61  42%      6  383  369   77  477%
c i   99.9   82093   540852     29472   13468    949 137794  253   596   61  42%      6  388  440   78  564%
c i   99.9   82090   540852     29473   13468    949 137794  253   596   61  42%      6  387  439   78  562%
c i   99.9   82087   540852     29483   13477    949 137794  253   596   61  42%      6  388  437   78  559%
c i  100.7   82084   540852     29800   13736    954 137795  260   608   61  43%      4  398  352   79  443%
c i  100.8   82083   540852     29801   13736    954 137795  260   608   61  43%      4  398  351   79  441%
c i  100.8   82082   540852     29803   13737    954 137795  259   608   61  43%      4  398  348   79  439%
c i  101.2   82081   540852     29950   13828    965 137795  266   612   65  43%      4  401  394   80  491%
c i  102.2   82080   540852     30432   14169    975 137820  260   619   66  42%      3  405  207   81  255%
c i  102.5   82079   540852     30566   14266    976 137823  264   623   70  42%      3  408  297   82  363%
c i  102.5   82078   540852     30567   14266    976 137823  264   623   70  42%      3  408  296   82  362%
c i  105.6   82077   540852     32185   15544    988 137838  275   659   71  42%     12  435  415   87  478%
c i  107.1   82076   540852     32930   16083    991 137841  299   674   71  44%      8  445  430   90  476%
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  107.3   82075   540852     33061   16208    991 137841  293   678   71  43%      7  448  302   90  334%
c i  107.8   81961   540852     33365   16461    994 137848  298   690   71  43%      5  458  357   92  389%
c i  109.3   81904   540852     34083   17021   1000 137863  308   701   72  44%      5  464  376   95  397%
c i  109.4   81896   540852     34133   17065   1000 137864  308   704   72  44%      5  466  370   95  390%
c i  109.5   81895   540852     34199   17124   1000 137864  309   707   72  44%      4  469  370   95  389%
c i  111.0   81894   540852     35012   17851   1001 137875  312   748   83  42%      5  504  313   98  320%
c i  112.8   81893   540852     36129   18691   1002 137883  293   690   84  42%      7  438  218  100  218%
c 
c [simplification-11] limit 36475 conflicts (hard 46375) hit after 36476 conflicts
c [quatres-6] found 37930 quaternary clauses 41% in total
c [quatres-6-2] added 5 quaternary resolvents
c [ternres-6] limit 19526655 with penalty 0 = 0 + 0
c [ternres-6] all 81893 free variables schedulable
c [ternres-6] 94 ternary resolvents (0 bin, 94 trn)
c [ternres-6] fully completed ternary resolution
c [decomp-25] removed 979 variables
c [basicprobe-4] limit 97633277 penalty 0 = 0 + 0
c [basicprobe-4-0] 28358 probes remain 35% after last round
c [basicprobe-4-0] 494 units = 479 failed (97%) + 15 lifted (3%)
c [basicprobe-4-0] removed 1165 variables, found 78277 hbrs
c [bate-3] eliminated 200 asymmetric tautologies during probing
c [unhide-11] limit 1952665 with penalty 1 = 0 + 1
c [unhide-11-11] 2 units, 59 failed, 8966 tauts, 0 hbrs, 221929 literals
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 224 transitive binary clauses
c [transred-7] found 1 units
c [block-4] scheduling all variables this time
c [block-4] scheduled 80549 variables 100%
c [block-4] limit of 48816638 steps penalty 2 = 2 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 27 blocked clauses
c [block-4] 27 < 1/100 * 522922 = 5229 considered unsuccessful
c [elim-9] scheduling all variables this time
c [elim-9] scheduled 80549 variables 100%
c [elim-9] limit of 390533111 steps penalty 0 = 0 + 0
c [elim-9] rescheduling of touched variables disabled
c [elim-9-1] eliminated 1067 variables 1% in round 1 in 50936921 steps
c [elim-9-1] backward subsumption/strengthening limit 50936900
c [elim-9-1-1] backward checking 4024 touched variables 5%
c [elim-9-1-1] fully completed backward checking in 1 rounds
c [elim-9-1] subsumed 8 and strengthened 66 clauses in 1429014 steps
c [elim-9-1] rescheduled 168 variables 0% by backward subsumption
c [elim-9-2] eliminated 20 variables 0% in round 2 in 161748 steps
c [elim-9-2] backward subsumption/strengthening limit 161700
c [elim-9-2-1] backward checking 153 touched variables 0%
c [elim-9-2-1] fully completed backward checking in 1 rounds
c [elim-9-2] subsumed 4 and strengthened 1 clauses in 156478 steps
c [elim-9-2] rescheduled 9 variables 0% by backward subsumption
c [elim-9-3] no variable eliminated in round 3 in 37901 steps
c [elim-9] fully completed in 3 rounds
c [elim-9] transition to [ all 0 rem 0 ] state
c [elim-9] eliminated 1092 = 1% variables out of 80549 scheduled
c [bca-7] limit of 10000000 steps and 1039954 added (scaled 2)
c [bca-7] 130699 out of 158916 literals actually usable 82%
c [bca-7] added 64 blocked clauses in 382160 steps
c [sweep-7] limit 5857996 penalty 0 = 0 + 0
c [sweep-7-1] 4087 pos 5.8% + 66427 neg 94.2% = 70514 sched 88.7% ret 8943
c [sweep-7-1] 5915284 steps 55 queries 7320.15 avg class size
c [sweep-7-1] 679 decisions 40 SAT calls 70.78 avg env size
c [sweep-7-1] 70157 variables remain 88% (9246 retained 12%)
c [decomp-26] removed 77 variables
c [sweep-7-1] removed 77 vars (0 failed, 14 eqs, 25 impls)
c [sweep-7] 77 < 1/1000 * 79457 = 79 considered unsuccessful
c [sweep-7] removed 77 vars in TOTAL (1 rounds, 54 queries)
c [phase-count-11] 513286 negative 98.9% of 519211 except 5925 1.1%
c [phase-count-11] 408477 positive 78.7% of 519211 except 110734 21.3%
c [phase-count-11] skipping relative phase luck test
c [phase-11] phase bias: 171 positive 100%, 0 negative 0%
c [sort-queue-11] sorted 27729 enqueued variables after 36476 conflicts
c [score-dist-11] active 51651 (65%), one 0 (0%), zero 27729 (35%)
c [score-dist-11] max exp 509, different 150 (29%)
c [score-dist-11] median active exp 492, avg 475.6
c [simplification-11] removed 2513 variables 3.1% (79380 remain 32%)
c [simplification-11] removed 21641 irredundant clauses 4.0% (519211 remain 38%)
c [simplification-11] maximum reduction of 4% = max (3%, 4%)
c [simplification-11] geometric conflict interval increment 4000 = 20000 / 5
c [simplification-11] new conflict interval 18666
c [simplification-11] penalized conflict interval 18666 = 1 * 18666
c [simplification-11] hard conflict limit 65142 (soft 55142 + delta 10000)
c [simplification-11] new conflict limit 55142 (hard 65142)
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  122.2   79379   519211     36510   14638   1025 202464  293   683   64  43%      5  429  285  101  281%
c i  122.8   79377   519211     36849   14925   1027 202466  295   683   66  43%      4  426  318  102  311%
c i  122.8   79376   519211     36850   14925   1027 202466  295   683   66  43%      4  426  317  102  310%
c i  122.8   79375   519211     36851   14925   1027 202466  295   683   66  43%      4  426  315  102  308%
c i  122.8   79374   519211     36857   14928   1027 202466  295   682   66  43%      4  426  319  102  312%
c i  122.8   79373   519211     36861   14930   1027 202466  295   682   66  43%      4  425  320  102  313%
c i  122.8   79372   519211     36862   14930   1027 202466  295   682   66  43%      4  425  319  102  312%
c i  122.9   79371   519211     36878   14943   1027 202466  295   681   66  43%      4  425  321  102  314%
c i  122.9   79370   519211     36880   14943   1027 202467  295   681   66  43%      4  424  319  102  311%
c i  122.9   79369   519211     36882   14943   1028 202467  295   681   66  43%      4  424  316  102  309%
c i  123.1   79368   519211     36940   14983   1029 202468  295   679   66  44%      4  422  317  103  309%
c i  123.1   79367   519211     36942   14983   1029 202469  295   679   66  44%      4  422  314  103  306%
c i  123.1   79364   519211     36943   14983   1029 202469  295   679   66  44%      4  421  313  103  305%
c i  123.1   79363   519211     36957   14988   1029 202469  295   678   66  44%      3  421  314  103  306%
c i  123.1   79362   519211     36958   14988   1029 202469  295   678   66  44%      3  420  313  103  305%
c i  125.2   79361   519211     37932   15627   1043 202471  285   631   66  45%      5  367  218  105  208%
c i  125.4   79311   519211     38021   15695   1043 202471  282   626   66  45%      5  362  199  105  190%
c i  125.4   79310   519211     38022   15695   1043 202471  282   626   66  45%      5  362  198  105  189%
c i  125.4   79309   519211     38023   15695   1043 202471  282   626   66  45%      5  362  197  105  188%
c i  125.4   79308   519211     38024   15695   1043 202471  282   626   66  45%      5  362  196  105  187%
c i  125.4   79307   519211     38025   15695   1043 202471  282   626   66  45%      5  362  196  105  187%
c i  125.4   79306   519211     38026   15695   1043 202471  282   626   66  45%      5  362  195  105  186%
c i  125.4   79305   519211     38027   15695   1043 202471  282   625   66  45%      5  361  194  105  185%
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  125.4   79304   519211     38029   15695   1043 202472  282   625   66  45%      5  361  193  105  184%
c i  125.4   79303   519211     38030   15695   1043 202472  282   625   66  45%      5  361  192  105  183%
c i  125.4   79302   519211     38031   15695   1043 202472  282   625   66  45%      5  361  191  105  182%
c i  125.4   79301   519211     38036   15699   1043 202472  281   624   66  45%      5  361  188  105  179%
c i  125.4   79300   519211     38037   15699   1043 202472  281   624   66  45%      5  360  187  105  178%
c i  125.7   79299   519211     38193   15826   1043 202472  279   623   66  45%      4  358  204  105  194%
c i  127.5   79294   519211     39030   16385   1065 202483  264   576   66  46%      5  307  189  106  178%
c i  128.8   79290   519211     39686   16743   1080 202484  251   540   66  47%      4  268  169  107  158%
c i  130.4   79283   519211     40328   17138   1082 202487  242   505   72  48%      4  231  188  108  175%
c i  130.4   79282   519211     40333   17141   1082 202487  242   505   72  48%      4  231  188  108  174%
c i  130.4   79281   519211     40342   17148   1082 202487  241   504   72  48%      4  230  188  108  174%
c i  130.7   79280   519211     40464   17216   1083 202487  238   496   72  48%      3  221  170  108  158%
c i  130.7   79279   519211     40472   17218   1083 202487  238   496   72  48%      3  221  169  108  157%
c i  131.2   79278   519211     40679   17305   1084 202488  235   482   72  49%      2  207  173  108  160%
c i  132.2   79277   519211     41219   17695   1096 202489  221   463   72  48%      2  186  120  108  111%
c i  132.8   79276   519211     41488   17853   1101 202490  224   459   72  49%      2  181  210  109  193%
c i  132.8   79275   519211     41490   17854   1101 202490  223   459   72  49%      2  181  208  109  192%
c i  133.8   79274   519211     41902   18108   1108 202490  224   449   72  50%      2  171  231  109  211%
c i  133.8   79273   519211     41949   18144   1109 202492  223   448   72  50%      1  169  207  109  189%
c i  135.7   79272   519211     42782   18696   1111 202494  214   423   72  51%      4  142  170  110  155%
c i  135.7   79271   519211     42783   18696   1111 202494  214   423   72  51%      4  142  170  110  154%
c i  137.0   79270   519211     43286   18968   1112 202497  216   414   72  52%      3  132  235  111  211%
c i  141.8   79269   519211     45322   20009   1141 202503  216   368   72  59%     16   83  208  114  182%
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  142.7   79255   519211     45681   20169   1141 202503  213   357   72  60%     12   71  182  115  159%
c i  143.5   79254   519211     45989   20265   1141 202503  210   346   72  61%      8   60  170  115  148%
c i  144.2   79252   519211     46318   20434   1141 202506  204   335   72  61%      6   49  143  115  124%
c i  146.7   79251   519211     47528   21096   1145 202513  191   310   76  62%      8   23  171  116  148%
c i  146.8   79250   519211     47537   21096   1145 202513  191   310   76  62%      8   23  173  116  149%
c i  146.8   79249   519211     47549   21096   1145 202514  191   310   76  62%      8   23  174  116  151%
c i  147.8   79248   519211     48080   21436   1153 202535  182   306   76  60%      5   19  123  116  106%
c i  147.9   79247   519211     48180   21502   1153 202535  181   305   77  59%      5   18  129  116  111%
c i  147.9   79246   519211     48188   21507   1154 202535  181   305   77  59%      4   18  126  116  108%
c i  148.1   79245   519211     48341   21623   1157 202537  179   308   77  58%      4   20  136  116  118%
c i  149.3   79244   519211     48885   21952   1162 202542  189   317   77  59%      3   29  229  117  196%
c i  150.2   79243   519211     49260   22143   1163 202542  186   309   77  60%      2   22  166  117  141%
c i  165.2   79238   519211     56011   25517   1179 202570  178   252   93  71%     83  -35  139  123  113%
c i  165.2   79237   519211     56012   25517   1179 202570  178   252   93  71%     83  -35  139  123  113%
c i  175.6   79236   519211     60257   27144   1179 202574  170   222  100  77%     43  -62  168  126  133%
c i  185.0   79232   519211     65121   29722   1217 202612  173   260  101  66%     50  -19  173  129  134%
c 
c [simplification-12] limit 55338 conflicts (hard 65142) hit after 65144 conflicts
c [quatres-7] found 38232 quaternary clauses 42% in total
c [quatres-7-2] added 4 quaternary resolvents
c [ternres-7] limit 36076386 with penalty 0 = 0 + 0
c [ternres-7] all 79171 free variables schedulable
c [ternres-7] 70 ternary resolvents (0 bin, 70 trn)
c [ternres-7] fully completed ternary resolution
c [decomp-27] removed 212 variables
c [simpleprobe-5] all 79168 free variables schedulable
c [simpleprobe-5] limit 144305544 penalty 0 = 0 + 0
c [decomp-28] removed 2082 variables
c [simpleprobe-5] fully completed simple probing
c [simpleprobe-5] removed 2082 variables, found 60704 hbrs, 951 units
c [unhide-12] limit 1803819 with penalty 2 = 0 + 2
c [unhide-12-12] 10 units, 99 failed, 42190 tauts, 0 hbrs, 129704 literals
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 313 transitive binary clauses
c [transred-8] found 1 units
c [cce-4] boosting limit by 10
c [cce-4] limit of 901909650 steps penalty 1 = 1 + 0
c [cce-4-1] eliminated 9 clauses out of 1200 (1%) of length 9
c [cce-4-1] eliminated 12 clauses out of 554 (2%) of length 8
c [cce-4-1] eliminated 45 clauses out of 762 (6%) of length 7
c [cce-4-1] eliminated 3270 clauses out of 5580 (59%) of length 6
c [cce-4-1] eliminated 29053 clauses out of 41337 (70%) of length 5
c [cce-4-1] eliminated 23661 clauses out of 37514 (63%) of length 4
c [cce-4-1] completed large round (ATE)
c [cce-4-1] eliminated 56050 large clauses in 826594983 steps
c [cce-4-1] allowing another 413297491 steps for small clauses
c [cce-4-1] scheduling 387988 clauses = 258756 binary + 129232 ternary
c [cce-4-1] tried to eliminate 19336 small clauses 5%
c [cce-4-1] eliminated 3397 binary clauses 1%
c [cce-4-1] eliminated 1000 ternary clauses 1%
c [cce-4-1] eliminated 4397 small clauses 1%
c [cce-4-1] eliminated 5979 small clauses in 901909671 steps
c [cce-4-1] incomplete small round (ATE)
c [cce-4-1] eliminated 62029 covered clauses in round 1
c [cce-4] eliminated 62029 covered clauses in TOTAL during 1 rounds
c [elim-10] scheduling all variables this time
c [elim-10] scheduled 76932 variables 100%
c [elim-10] limit of 721527722 steps penalty 0 = 0 + 0
c [elim-10] rescheduling of touched variables disabled
c [elim-10-1] eliminated 21989 variables 29% in round 1 in 37606766 steps
c [elim-10-1] backward subsumption/strengthening limit 37606700
c [elim-10-1-1] backward checking 45111 touched variables 59%
c [elim-10-1-1] fully completed backward checking in 1 rounds
c [elim-10-1] subsumed 19 and strengthened 59 clauses in 6040222 steps
c [elim-10-1] rescheduled 133 variables 0% by backward subsumption
c [elim-10-2] eliminated 4 variables 0% in round 2 in 64814 steps
c [elim-10-2] backward subsumption/strengthening limit 64800
c [elim-10-2-1] backward checking 62 touched variables 0%
c [elim-10-2-1] incomplete backward checking 0 remain 0%
c [elim-10-2] subsumed 0 and strengthened 0 clauses in 64801 steps
c [elim-10-2] fully rescheduled 54939 variables 71%
c [elim-10-3] eliminated 70 variables 0% in round 3 in 33770398 steps
c [elim-10-3] backward subsumption/strengthening limit 33770300
c [elim-10-3-1] backward checking 520 touched variables 1%
c [elim-10-3-1] fully completed backward checking in 1 rounds
c [elim-10-3] subsumed 0 and strengthened 2 clauses in 788378 steps
c [elim-10] incomplete 7 not tried 0% in round 3
c [elim-10] transition to [ all 1 rem 1 ] state
c [elim-10] eliminated 22063 = 29% variables out of 76932 scheduled
c [bca-8] limit of 10000000 steps and 772488 added (scaled 2)
c [bca-8] 101041 out of 109740 literals actually usable 92%
c [bca-8] added 284 blocked clauses in 242169 steps
c [phase-count-12] 384995 negative 99.8% of 385773 except 778 0.2%
c [phase-count-12] 279084 positive 72.3% of 385773 except 106689 27.7%
c [phase-count-12] skipping relative phase luck test
c [phase-12] phase bias: 1 positive 1%, 141 negative 99%
c [sort-queue-12] sorted 17158 enqueued variables after 65144 conflicts
c [score-dist-12] active 37711 (69%), one 0 (0%), zero 17158 (31%)
c [score-dist-12] max exp 510, different 260 (51%)
c [score-dist-12] median active exp 482, avg 439.5
c [simplification-12] removed 24302 variables 30.7% (54869 remain 22%)
c [simplification-12] removed 133438 irredundant clauses 25.7% (385773 remain 28%)
c [simplification-12] maximum reduction of 31% = max (31%, 26%)
c [simplification-12] large reduction 31% >= 5% limit
c [simplification-12] next conflict interval 2000 = 2000/1
c [simplification-12] penalized conflict interval 2000 = 1 * 2000
c [simplification-12] hard conflict limit 77144 (soft 67144 + delta 10000)
c [simplification-12] new conflict limit 67144 (hard 77144)
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  217.9   54868   385773     65572    3272   1867 177888  161   251   37  64%     29  -28   76  128   59%
c i  219.2   54867   385773     69020    5877   1893 177901  107   196   41  55%     28  -81   28  125   22%
c i  219.3   54813   385773     69174    6009   1894 177904  111   213   41  52%     23  -63  111  126   89%
c i  219.3   54812   385773     69185    6017   1894 177905  111   214   41  52%     22  -62  114  126   91%
c i  219.3   54811   385773     69188    6019   1894 177905  111   214   41  52%     22  -62  114  126   90%
c 
c [simplification-13] limit 67147 conflicts (hard 77144) hit after 69572 conflicts
c [quatres-8] found 27356 quaternary clauses 56% in total
c [quatres-8-1] removed 4 duplicate quaternary clauses
c [quatres-8-2] added 1 single-self-subsuming ternary resolvents
c [quatres-8-2] added 30 quaternary resolvents
c [ternres-8] limit 36657282 with penalty 0 = 0 + 0
c [ternres-8] all 54811 free variables schedulable
c [ternres-8] 434 ternary resolvents (1 bin, 433 trn)
c [ternres-8] fully completed ternary resolution
c [decomp-29] removed 62 variables
c [treelook-5] limit 3665728 penalty 0 = 0 + 0 boost 1
c [treelook-5] scheduled 66048 literals 60%
c [treelook-5] scheduling used 1006617 steps
c [treelook-5] scheduled completely
c [treelook-5] limit 3665728 penalty 0 = 0 + 0 boost 1
c [treelook-5] used 3786789 steps
c [treelook-5] 65845 literals remain 60%
c [treelook-5] 9246 variables remain to probed next time 17%
c [decomp-30] removed 3 variables
c [treelook-5] removed 64 variables, found 30522 hbrs
c [unhide-13] limit 7331456 with penalty 0 = 0 + 0
c [unhide-13-16] 2 units, 309 failed, 43271 tauts, 0 hbrs, 96164 literals
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 302 transitive binary clauses
c [transred-9] found 1 units
c [cce-5] limit of 183286411 steps penalty 0 = 0 + 0
c [cce-5-1] eliminated 6 clauses out of 32 (19%) of length 7
c [cce-5-1] eliminated 457 clauses out of 3808 (12%) of length 6
c [cce-5-1] eliminated 979 clauses out of 15987 (6%) of length 5
c [cce-5-1] incomplete large round (ACCE)
c [cce-5-1] eliminated 1442 large clauses in 183286411 steps
c [cce-5-1] allowing another 91643205 steps for small clauses
c [cce-5-1] scheduling 305415 clauses = 183883 binary + 121532 ternary
c [cce-5-1] tried to eliminate 4042 small clauses 1%
c [cce-5-1] eliminated 797 binary clauses 0%
c [cce-5-1] eliminated 205 ternary clauses 0%
c [cce-5-1] eliminated 1002 small clauses 0%
c [cce-5-1] eliminated 2548 small clauses in 183286411 steps
c [cce-5-1] incomplete small round (ACCE)
c [cce-5-1] eliminated 3990 covered clauses in round 1
c [cce-5] eliminated 3990 covered clauses in TOTAL during 1 rounds
c [elim-11] no untried remaining variables left
c [elim-11] scheduled 54391 variables 100%
c [elim-11] limit of 733145645 steps penalty 0 = 0 + 0
c [elim-11] rescheduling of touched variables disabled
c [elim-11-1] eliminated 521 variables 1% in round 1 in 31534908 steps
c [elim-11-1] backward subsumption/strengthening limit 31534900
c [elim-11-1-1] backward checking 3360 touched variables 6%
c [elim-11-1-1] fully completed backward checking in 1 rounds
c [elim-11-1] subsumed 1 and strengthened 14 clauses in 855601 steps
c [elim-11-1] rescheduled 36 variables 0% by backward subsumption
c [elim-11-2] no variable eliminated in round 2 in 15196 steps
c [elim-11] fully completed in 2 rounds
c [elim-11] transition to [ all 0 rem 0 ] state
c [elim-11] eliminated 521 = 1% variables out of 54391 scheduled
c [elim-11] 521 < 1/100 * 54391 = 543 considered unsuccessful
c [bca-9] limit of 10000000 steps and 738542 added (scaled 2)
c [bca-9] 96230 out of 107742 literals actually usable 89%
c [bca-9] added 340 blocked clauses in 233832 steps
c [sweep-8] limit 5498592 penalty 1 = 1 + 0
c [sweep-8-1] 4148 pos 8.5% + 44489 neg 91.5% = 48637 sched 90.3% ret 5233
c [sweep-8-1] 5502846 steps 96 queries 5220.46 avg class size
c [sweep-8-1] 1358 decisions 93 SAT calls 89.72 avg env size
c [sweep-8-1] 47370 variables remain 88% (6403 retained 12%)
c [decomp-31] removed 106 variables
c [sweep-8-1] removed 106 vars (0 failed, 6 eqs, 8 impls)
c [sweep-8] removed 106 vars in TOTAL (1 rounds, 95 queries)
c [phase-count-13] 367204 negative 99.8% of 367957 except 753 0.2%
c [phase-count-13] 264740 positive 71.9% of 367957 except 103217 28.1%
c [phase-count-13] skipping relative phase luck test
c [phase-13] phase bias: 5 positive 100%, 0 negative 0%
c [sort-queue-13] sorted 15470 enqueued variables after 69572 conflicts
c [score-dist-13] active 38294 (71%), one 0 (0%), zero 15470 (29%)
c [score-dist-13] max exp 509, different 275 (54%)
c [score-dist-13] median active exp 490, avg 450.0
c [simplification-13] removed 1047 variables 1.9% (53764 remain 22%)
c [simplification-13] removed 17816 irredundant clauses 4.6% (367957 remain 27%)
c [simplification-13] maximum reduction of 5% = max (2%, 5%)
c [simplification-13] large reduction 5% >= 5% limit
c [simplification-13] next conflict interval 2000 = 2000/1
c [simplification-13] penalized conflict interval 2000 = 1 * 2000
c [simplification-13] hard conflict limit 81572 (soft 71572 + delta 10000)
c [simplification-13] new conflict limit 71572 (hard 81572)
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  229.1   53763   367957     69656    6347   2171 173462  131   296   47  44%     11   19  325  127  257%
c i  229.2   53762   367957     69794    6470   2172 173462  137   315   47  43%      8   39  312  127  245%
c i  229.6   53761   367957     70117    6772   2175 173467  138   346   47  40%      3   69  205  127  161%
c i  229.7   53759   367957     70164    6810   2176 173467  137   348   47  39%      3   71  187  127  147%
c i  229.7   53757   367957     70170    6815   2176 173467  137   348   47  39%      3   72  185  127  145%
c i  230.7   53753   367957     71227    7680   2188 173478  157   381   49  41%     -1  102  138  129  107%
c i  231.4   53690   367957     72448    8675   2210 173495  148   405   50  36%     -1  125  164  129  127%
c i  231.4   53689   367957     72449    8675   2210 173495  148   405   50  36%     -1  125  163  129  127%
c i  231.7   53688   367957     72776    8954   2210 173498  159   421   50  38%     -3  140  246  130  190%
c 
c [simplification-14] limit 71583 conflicts (hard 81572) hit after 74138 conflicts
c [quatres-9] found 26463 quaternary clauses 57% in total
c [quatres-9-1] removed 1 duplicate quaternary clauses
c [quatres-9-2] added 2 single-self-subsuming ternary resolvents
c [quatres-9-2] added 3 quaternary resolvents
c [ternres-9] limit 37786525 with penalty 0 = 0 + 0
c [ternres-9] all 53688 free variables schedulable
c [ternres-9] 463 ternary resolvents (0 bin, 463 trn)
c [ternres-9] fully completed ternary resolution
c [gauss-4] limit 944663 penalty 3 = 3 + 0
c [gauss-4] extracted 12 xors of average arity 2.9
c [gauss-4] connected 35 occurrences of 35 variables (average 1.0)
c [gauss-4] limit 944663 penalty 3 = 3 + 0
c [gauss-4] fully completed
c [gauss-4] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-32] removed 5 variables
c [basicprobe-5] limit 188932629 penalty 0 = 0 + 0
c [basicprobe-5-0] 8753 probes remain 17% after last round
c [basicprobe-5-0] 1108 units = 1068 failed (96%) + 40 lifted (4%)
c [basicprobe-5-0] removed 1950 variables, found 350713 hbrs
c [bate-4] eliminated 1697 asymmetric tautologies during probing
c [unhide-14] limit 7557305 with penalty 0 = 0 + 0
c [unhide-14-20] 11 units, 380 failed, 77386 tauts, 0 hbrs, 83031 literals
c [transred-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 205 transitive binary clauses
c [cce-6] limit of 188932629 steps penalty 0 = 0 + 0
c [cce-6-1] eliminated 7 clauses out of 3092 (0%) of length 6
c [cce-6-1] eliminated 1077 clauses out of 13859 (8%) of length 5
c [cce-6-1] incomplete large round (ATE)
c [cce-6-1] eliminated 1084 large clauses in 188932642 steps
c [cce-6-1] allowing another 94466321 steps for small clauses
c [cce-6-1] scheduling 277172 clauses = 172043 binary + 105129 ternary
c [cce-6-1] tried to eliminate 4751 small clauses 2%
c [cce-6-1] eliminated 756 binary clauses 0%
c [cce-6-1] eliminated 173 ternary clauses 0%
c [cce-6-1] eliminated 929 small clauses 0%
c [cce-6-1] eliminated 1254 small clauses in 188932641 steps
c [cce-6-1] incomplete small round (ATE)
c [cce-6-1] eliminated 2338 covered clauses in round 1
c [cce-6] eliminated 2338 covered clauses in TOTAL during 1 rounds
c [cce-6] 2338 < 1/100 * 338912 = 3389 considered unsuccessful
c [bca-10] limit of 10000000 steps and 674402 added (scaled 2)
c [bca-10] 89095 out of 102608 literals actually usable 87%
c [bca-10] added 78 blocked clauses in 216516 steps
c [sweep-9] limit 11335957 penalty 0 = 0 + 0
c [sweep-9-1] 3927 pos 8.6% + 41592 neg 91.4% = 45519 sched 88.7% ret 5784
c [sweep-9-1] 11336595 steps 222 queries 1671.90 avg class size
c [sweep-9-1] 2956 decisions 205 SAT calls 96.48 avg env size
c [sweep-9-1] 42476 variables remain 83% (8636 retained 17%)
c [decomp-33] removed 321 variables
c [sweep-9-1] removed 321 vars (0 failed, 23 eqs, 33 impls)
c [sweep-9] removed 321 vars in TOTAL (1 rounds, 221 queries)
c [phase-count-14] 334438 negative 99.8% of 335192 except 754 0.2%
c [phase-count-14] 239036 positive 71.3% of 335192 except 96156 28.7%
c [phase-count-14] skipping relative phase luck test
c [phase-14] phase bias: 1 positive 8%, 11 negative 92%
c [sort-queue-14] sorted 13141 enqueued variables after 74138 conflicts
c [score-dist-14] active 37841 (74%), one 0 (0%), zero 13141 (26%)
c [score-dist-14] max exp 509, different 286 (56%)
c [score-dist-14] median active exp 498, avg 464.7
c [simplification-14] removed 2706 variables 5.0% (50982 remain 21%)
c [simplification-14] removed 32765 irredundant clauses 8.9% (335192 remain 24%)
c [simplification-14] maximum reduction of 9% = max (5%, 9%)
c [simplification-14] large reduction 9% >= 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 86138 (soft 76138 + delta 10000)
c [simplification-14] new conflict limit 76138 (hard 86138)
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  249.3   50981   335192     75403   10554   3608 432332  146   382   56  38%     15   96  156  129  120%
c 
c [simplification-15] limit 76138 conflicts (hard 86138) hit after 76140 conflicts
c [quatres-10] found 22627 quaternary clauses 56% in total
c [quatres-10-1] removed 1 duplicate quaternary clauses
c [quatres-10-2] added 4 single-self-subsuming ternary resolvents
c [quatres-10-2] added 1 quaternary resolvents
c [ternres-10] limit 38209641 with penalty 0 = 0 + 0
c [ternres-10] all 50919 free variables schedulable
c [ternres-10] 963 ternary resolvents (2 bin, 961 trn)
c [ternres-10] fully completed ternary resolution
c [card-5] limit 1194051 penalty 4 = 4 + 0
c [card-5] found 1890 at-most-one constraints of average size 3.9
c [card-5] no at-most-two constraint found
c [card-5] using previous limit 1194051 for elimination
c [card-5] 1890 out of 1890 constraints (100%) meet size limits
c [card-5] no units found
c [card-5] no at-most-one constraints generated
c [decomp-34] removed 65 variables
c [simpleprobe-6] all 50917 free variables schedulable
c [simpleprobe-6] limit 152838566 penalty 0 = 0 + 0
c [decomp-35] removed 747 variables
c [simpleprobe-6] fully completed simple probing
c [simpleprobe-6] removed 747 variables, found 125653 hbrs, 409 units
c [unhide-15] limit 7641928 with penalty 0 = 0 + 0
c [unhide-15-24] 5 units, 217 failed, 79272 tauts, 0 hbrs, 101089 literals
c [transred-11] limit 2000000 with penalty 0 = 0 + 0
c [transred-11] removed 283 transitive binary clauses
c [transred-11] found 2 units
c [block-5] scheduling all variables this time
c [block-5] scheduled 49932 variables 100%
c [block-5] limit of 47762052 steps penalty 3 = 3 + 0
c [block-5] fully completed
c [block-5] transition to [ all 0 rem 0 ] state
c [block-5] eliminated 701 blocked clauses
c [block-5] 701 < 1/100 * 324003 = 3240 considered unsuccessful
c [elim-12] scheduling all variables this time
c [elim-12] scheduled 49925 variables 100%
c [elim-12] limit of 382096417 steps penalty 1 = 1 + 0
c [elim-12] rescheduling of touched variables disabled
c [elim-12-1] eliminated 1988 variables 4% in round 1 in 26930807 steps
c [elim-12-1] backward subsumption/strengthening limit 26930800
c [elim-12-1-1] backward checking 10058 touched variables 20%
c [elim-12-1-1] fully completed backward checking in 1 rounds
c [elim-12-1] subsumed 17 and strengthened 77 clauses in 2295265 steps
c [elim-12-1] rescheduled 201 variables 0% by backward subsumption
c [elim-12-2] eliminated 18 variables 0% in round 2 in 113876 steps
c [elim-12-2] backward subsumption/strengthening limit 113800
c [elim-12-2-1] backward checking 173 touched variables 0%
c [elim-12-2-1] fully completed backward checking in 1 rounds
c [elim-12-2] subsumed 4 and strengthened 8 clauses in 110069 steps
c [elim-12-2] rescheduled 39 variables 0% by backward subsumption
c [elim-12-3] eliminated 4 variables 0% in round 3 in 25501 steps
c [elim-12-3] backward subsumption/strengthening limit 25500
c [elim-12-3-1] backward checking 41 touched variables 0%
c [elim-12-3-1] incomplete backward checking 0 remain 0%
c [elim-12-3] subsumed 0 and strengthened 6 clauses in 25501 steps
c [elim-12] incomplete 24 not tried 0% in round 3
c [elim-12] transition to [ all 1 rem 1 ] state
c [elim-12] eliminated 2010 = 4% variables out of 49925 scheduled
c [bca-11] limit of 10000000 steps and 642099 added (scaled 2)
c [bca-11] 82190 out of 95832 literals actually usable 86%
c [bca-11] added 84 blocked clauses in 202450 steps
c [sweep-10] limit 11462892 penalty 0 = 0 + 0
c [sweep-10-1] 3314 pos 8.3% + 36644 neg 91.7% = 39958 sched 83.4% ret 7957
c [sweep-10-1] 11467823 steps 280 queries 1277.25 avg class size
c [sweep-10-1] 4527 decisions 257 SAT calls 118.48 avg env size
c [sweep-10-1] 36967 variables remain 77% (10870 retained 23%)
c [decomp-36] removed 265 variables
c [sweep-10-1] removed 265 vars (0 failed, 27 eqs, 41 impls)
c [sweep-10] removed 265 vars in TOTAL (1 rounds, 279 queries)
c [phase-count-15] 318921 negative 99.8% of 319696 except 775 0.2%
c [phase-count-15] 224757 positive 70.3% of 319696 except 94939 29.7%
c [phase-count-15] skipping relative phase luck test
c [phase-15] phase bias: 1 positive 25%, 3 negative 75%
c [sort-queue-15] sorted 10694 enqueued variables after 76140 conflicts
c [score-dist-15] active 36956 (78%), one 0 (0%), zero 10694 (22%)
c [score-dist-15] max exp 509, different 286 (56%)
c [score-dist-15] median active exp 499, avg 470.9
c [simplification-15] removed 3269 variables 6.4% (47650 remain 19%)
c [simplification-15] removed 15496 irredundant clauses 4.6% (319696 remain 23%)
c [simplification-15] maximum reduction of 6% = max (6%, 5%)
c [simplification-15] large reduction 6% >= 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 88140 (soft 78140 + delta 10000)
c [simplification-15] new conflict limit 78140 (hard 88140)
c 
c [simplification-16] limit 78140 conflicts (hard 88140) hit after 78141 conflicts
c [quatres-11] found 22181 quaternary clauses 55% in total
c [quatres-11-1] removed 2 duplicate quaternary clauses
c [quatres-11-2] added 3 quaternary resolvents
c [ternres-11] limit 38638104 with penalty 0 = 0 + 0
c [ternres-11] all 47650 free variables schedulable
c [ternres-11] 913 ternary resolvents (4 bin, 909 trn)
c [ternres-11] fully completed ternary resolution
c [decomp-37] removed 1 variables
c [treelook-6] limit 3863810 penalty 0 = 0 + 0 boost 1
c [treelook-6] scheduled 57723 literals 61%
c [treelook-6] scheduling used 1014793 steps
c [treelook-6] scheduled completely
c [treelook-6] limit 3863810 penalty 0 = 0 + 0 boost 1
c [treelook-6] used 3903303 steps
c [treelook-6] 57615 literals remain 60%
c [treelook-6] 8458 variables remain to probed next time 18%
c [treelook-6] removed 4 variables, found 31281 hbrs
c [unhide-16] limit 7727620 with penalty 0 = 0 + 0
c [unhide-16-28] 14 units, 124 failed, 43043 tauts, 0 hbrs, 192911 literals
c [transred-12] limit 2000000 with penalty 0 = 0 + 0
c [transred-12] removed 257 transitive binary clauses
c [cce-7] limit of 96595262 steps penalty 1 = 1 + 0
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 29
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 28
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 27
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 26
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 25
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 24
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 23
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 22
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 21
c [cce-7-1] eliminated 1 clauses out of 1 (100%) of length 20
c [cce-7-1] eliminated 2 clauses out of 3 (67%) of length 19
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 18
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 17
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 16
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 15
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 14
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 13
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 12
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 11
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 10
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 9
c [cce-7-1] eliminated 1 clauses out of 7 (14%) of length 8
c [cce-7-1] eliminated 3 clauses out of 26 (12%) of length 7
c [cce-7-1] eliminated 3 clauses out of 3080 (0%) of length 6
c [cce-7-1] eliminated 2 clauses out of 13147 (0%) of length 5
c [cce-7-1] incomplete large round (ACCE)
c [cce-7-1] eliminated 40 large clauses in 96595263 steps
c [cce-7-1] allowing another 48297631 steps for small clauses
c [cce-7-1] scheduling 256802 clauses = 162012 binary + 94790 ternary
c [cce-7-1] tried to eliminate 2559 small clauses 1%
c [cce-7-1] eliminated 410 binary clauses 0%
c [cce-7-1] eliminated 114 ternary clauses 0%
c [cce-7-1] eliminated 524 small clauses 0%
c [cce-7-1] eliminated 528 small clauses in 96595270 steps
c [cce-7-1] incomplete small round (ACCE)
c [cce-7-1] eliminated 568 covered clauses in round 1
c [cce-7] eliminated 568 covered clauses in TOTAL during 1 rounds
c [cce-7] 568 < 1/100 * 315792 = 3157 considered unsuccessful
c [elim-13] no untried remaining variables left
c [elim-13] scheduled 47468 variables 100%
c [elim-13] almost no limit of 100000000000 steps
c [elim-13] rescheduling of touched variables disabled
c [elim-13-1] eliminated 349 variables 1% in round 1 in 26897072 steps
c [elim-13-1] backward subsumption/strengthening limit 26897000
c [elim-13-1-1] backward checking 2240 touched variables 5%
c [elim-13-1-1] fully completed backward checking in 1 rounds
c [elim-13-1] subsumed 6 and strengthened 7 clauses in 579117 steps
c [elim-13-1] rescheduled 32 variables 0% by backward subsumption
c [elim-13-2] eliminated 4 variables 0% in round 2 in 44936 steps
c [elim-13-2] backward subsumption/strengthening limit 44900
c [elim-13-2-1] backward checking 27 touched variables 0%
c [elim-13-2-1] incomplete backward checking 8 remain 30%
c [elim-13-2] subsumed 3 and strengthened 2 clauses in 44967 steps
c [elim-13-2] rescheduled 12 variables 0% by backward subsumption
c [elim-13-3] no variable eliminated in round 3 in 20302 steps
c [elim-13] fully completed in 3 rounds
c [elim-13] transition to [ all 0 rem 0 ] state
c [elim-13] eliminated 354 = 1% variables out of 47468 scheduled
c [elim-13] 354 < 1/100 * 47468 = 474 considered unsuccessful
c [bca-12] limit of 10000000 steps and 630445 added (scaled 2)
c [bca-12] 79344 out of 94230 literals actually usable 84%
c [bca-12] added 92 blocked clauses in 196624 steps
c [sweep-11] boosting sweeping limit by 10
c [sweep-11] limit 115914310 penalty 0 = 0 + 0
c [sweep-11-1] 3348 pos 9.2% + 33031 neg 90.8% = 36379 sched 77.2% ret 10735
c [sweep-11-1] 116036799 steps 2867 queries 141.99 avg class size
c [sweep-11-1] 23228 decisions 2579 SAT calls 87.44 avg env size
c [sweep-11-1] 13774 variables remain 30% (32573 retained 70%)
c [decomp-39] removed 1505 variables
c [sweep-11-1] removed 1505 vars (1 failed, 337 eqs, 608 impls)
c [sweep-11] removed 1505 vars in TOTAL (1 rounds, 2866 queries)
c [phase-count-16] 307590 negative 99.8% of 308328 except 738 0.2%
c [phase-count-16] 217243 positive 70.5% of 308328 except 91085 29.5%
c [phase-count-16] skipping relative phase luck test
c [phase-16] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-16] sorted 8218 enqueued variables after 78141 conflicts
c [score-dist-16] active 37391 (82%), one 0 (0%), zero 8218 (18%)
c [score-dist-16] max exp 509, different 260 (51%)
c [score-dist-16] median active exp 503, avg 488.7
c [simplification-16] removed 2041 variables 4.3% (45609 remain 19%)
c [simplification-16] removed 11368 irredundant clauses 3.6% (308328 remain 22%)
c [simplification-16] maximum reduction of 4% = max (4%, 4%)
c [simplification-16] geometric conflict interval increment 4000 = 20000 / 5
c [simplification-16] new conflict interval 22666
c [simplification-16] penalized conflict interval 22666 = 1 * 22666
c [simplification-16] hard conflict limit 112140 (soft 100807 + delta 11333)
c [simplification-16] new conflict limit 100807 (hard 112140)
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  272.8   45608   308328     79116   13279   4112 485309  290   593   61  49%     30  297  528  141  374%
c i  272.9   45607   308328     79191   13341   4112 485309  293   593   61  49%     27  296  514  142  363%
c i  272.9   45606   308328     79192   13341   4112 485309  293   593   61  49%     27  296  512  142  362%
c i  272.9   45605   308328     79193   13341   4112 485309  293   593   61  49%     27  296  510  142  360%
c i  272.9   45603   308328     79277   13409   4113 485309  295   592   61  50%     24  295  474  142  334%
c i  273.0   45602   308328     79293   13423   4113 485309  295   592   61  50%     24  295  467  142  329%
c i  273.0   45601   308328     79300   13429   4113 485309  295   592   61  50%     23  295  463  142  326%
c i  276.1   45596   308328     82416   15256   4122 485315  313   531   70  59%     22  222  285  151  189%
c i  282.7   45595   308328     89279   18806   4142 485401  224   336   79  67%     75   14  146  158   93%
c i  282.9   45561   308328     89610   19046   4149 485421  224   354   79  63%     50   32  197  158  125%
c i  283.1   45556   308328     89723   19110   4149 485451  224   357   79  63%     43   35  211  158  134%
c i  284.5   45555   308328     91133   19942   4151 485455  233   365   79  64%      8   42  186  160  116%
c i  286.3   45554   308328     92986   20955   4152 485458  240   354   93  68%      2   31  284  163  175%
c i  291.0   45551   308328     97230   23438   4163 485471  325   464   94  70%     33  135  382  175  218%
c i  292.8   45545   308328     98772   24058   4165 485473  335   462   97  72%      5  130  276  180  154%
c 
c [simplification-17] limit 100828 conflicts (hard 112140) hit after 100830 conflicts
c [quatres-12] found 19584 quaternary clauses 51% in total
c [quatres-12-1] removed 3 duplicate quaternary clauses
c [quatres-12-2] added 5 single-self-subsuming ternary resolvents
c [quatres-12-2] added 8 quaternary resolvents
c [ternres-12] limit 44907106 with penalty 0 = 0 + 0
c [ternres-12] all 45542 free variables schedulable
c [ternres-12] 866 ternary resolvents (3 bin, 863 trn)
c [ternres-12] fully completed ternary resolution
c [decomp-40] removed 75 variables
c [basicprobe-6] limit 224535532 penalty 0 = 0 + 0
c [basicprobe-6-0] 8215 sched 19%, 1005 failed, 109 lifted, 311462 hbrs
c [decomp-41] removed 1496 variables
c [basicprobe-6-1] 13436 probes remain 31% after last round
c [basicprobe-6-1] 1197 units = 1088 failed (91%) + 109 lifted (9%)
c [basicprobe-6-1] removed 1708 variables, found 343631 hbrs
c [bate-5] eliminated 502 asymmetric tautologies during probing
c [unhide-17] limit 4490710 with penalty 1 = 0 + 1
c [unhide-17-30] 5 units, 63 failed, 84343 tauts, 0 hbrs, 820140 literals
c [transred-13] limit 2000000 with penalty 0 = 0 + 0
c [transred-13] removed 402 transitive binary clauses
c [bca-13] limit of 10000000 steps and 575449 added (scaled 2)
c [bca-13] 68162 out of 87504 literals actually usable 78%
c [bca-13] added 37 blocked clauses in 179366 steps
c [sweep-12] limit 13472131 penalty 0 = 0 + 0
c [sweep-12-1] 1102 pos 8.6% + 11642 neg 91.4% = 12744 sched 29.1% ret 31007
c [sweep-12-1] 13529229 steps 363 queries 420.90 avg class size
c [sweep-12-1] 3173 decisions 311 SAT calls 92.34 avg env size
c [sweep-12-1] 11242 variables remain 26% (32132 retained 74%)
c [decomp-42] removed 521 variables
c [sweep-12-1] removed 521 vars (0 failed, 54 eqs, 86 impls)
c [sweep-12] removed 521 vars in TOTAL (1 rounds, 362 queries)
c [phase-count-17] 284236 negative 99.7% of 284964 except 728 0.3%
c [phase-count-17] 198393 positive 69.6% of 284964 except 86571 30.4%
c [phase-count-17] skipping relative phase luck test
c [phase-17] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-17] sorted 6926 enqueued variables after 100830 conflicts
c [score-dist-17] active 36304 (84%), one 0 (0%), zero 6926 (16%)
c [score-dist-17] max exp 510, different 330 (65%)
c [score-dist-17] median active exp 488, avg 456.2
c [simplification-17] removed 2312 variables 5.1% (43230 remain 18%)
c [simplification-17] removed 23364 irredundant clauses 7.6% (284964 remain 21%)
c [simplification-17] maximum reduction of 8% = max (5%, 8%)
c [simplification-17] large reduction 8% >= 5% limit
c [simplification-17] next conflict interval 2000 = 2000/1
c [simplification-17] penalized conflict interval 2000 = 1 * 2000
c [simplification-17] hard conflict limit 112830 (soft 102830 + delta 10000)
c [simplification-17] new conflict limit 102830 (hard 112830)
c 
c [simplification-18] limit 102830 conflicts (hard 112830) hit after 102834 conflicts
c [quatres-13] found 17871 quaternary clauses 51% in total
c [quatres-13-2] added 1 single-self-subsuming ternary resolvents
c [ternres-13] limit 45530844 with penalty 0 = 0 + 0
c [ternres-13] all 43230 free variables schedulable
c [ternres-13] 695 ternary resolvents (11 bin, 684 trn)
c [ternres-13] fully completed ternary resolution
c [decomp-43] removed 10 variables
c [simpleprobe-7] all 43220 free variables schedulable
c [simpleprobe-7] limit 182123376 penalty 0 = 0 + 0
c [decomp-44] removed 298 variables
c [simpleprobe-7] fully completed simple probing
c [simpleprobe-7] removed 298 variables, found 203837 hbrs, 119 units
c [unhide-18] limit 4553084 with penalty 1 = 0 + 1
c [unhide-18-32] 2 units, 68 failed, 147324 tauts, 0 hbrs, 114552 literals
c [transred-14] limit 2000000 with penalty 0 = 0 + 0
c [transred-14] removed 444 transitive binary clauses
c [transred-14] found 1 units
c [elim-14] scheduling all variables this time
c [elim-14] scheduled 42885 variables 100%
c [elim-14] limit of 400000000 steps penalty 1 = 1 + 0
c [elim-14] rescheduling of touched variables disabled
c [elim-14-1] eliminated 1090 variables 3% in round 1 in 23706207 steps
c [elim-14-1] backward subsumption/strengthening limit 23706200
c [elim-14-1-1] backward checking 5662 touched variables 13%
c [elim-14-1-1] fully completed backward checking in 1 rounds
c [elim-14-1] subsumed 2 and strengthened 30 clauses in 1350766 steps
c [elim-14-1] rescheduled 92 variables 0% by backward subsumption
c [elim-14-2] eliminated 8 variables 0% in round 2 in 34834 steps
c [elim-14-2] backward subsumption/strengthening limit 34800
c [elim-14-2-1] backward checking 90 touched variables 0%
c [elim-14-2-1] incomplete backward checking 0 remain 0%
c [elim-14-2] subsumed 0 and strengthened 6 clauses in 34801 steps
c [elim-14-2] rescheduled 24 variables 0% by backward subsumption
c [elim-14-3] eliminated 2 variables 0% in round 3 in 13105 steps
c [elim-14-3] backward subsumption/strengthening limit 13100
c [elim-14-3-1] backward checking 22 touched variables 0%
c [elim-14-3-1] incomplete backward checking 0 remain 0%
c [elim-14-3] subsumed 0 and strengthened 4 clauses in 13101 steps
c [elim-14] incomplete 16 not tried 0% in round 3
c [elim-14] transition to [ all 1 rem 1 ] state
c [elim-14] eliminated 1100 = 3% variables out of 42885 scheduled
c [bca-14] limit of 10000000 steps and 557548 added (scaled 2)
c [bca-14] 64443 out of 83572 literals actually usable 77%
c [bca-14] added 59 blocked clauses in 169172 steps
c [sweep-13] limit 13659253 penalty 0 = 0 + 0
c [sweep-13-1] 1002 pos 9.4% + 9695 neg 90.6% = 10697 sched 25.6% ret 31088
c [sweep-13-1] 13688696 steps 405 queries 403.44 avg class size
c [sweep-13-1] 3911 decisions 372 SAT calls 94.63 avg env size
c [sweep-13-1] 9490 variables remain 23% (32224 retained 77%)
c [decomp-45] removed 157 variables
c [sweep-13-1] removed 157 vars (0 failed, 37 eqs, 72 impls)
c [sweep-13] removed 157 vars in TOTAL (1 rounds, 404 queries)
c [phase-count-18] 276804 negative 99.8% of 277494 except 690 0.2%
c [phase-count-18] 192111 positive 69.2% of 277494 except 85383 30.8%
c [phase-count-18] skipping relative phase luck test
c [phase-18] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-18] sorted 6320 enqueued variables after 102834 conflicts
c [score-dist-18] active 35308 (85%), one 0 (0%), zero 6320 (15%)
c [score-dist-18] max exp 510, different 333 (65%)
c [score-dist-18] median active exp 494, avg 457.4
c [simplification-18] removed 1602 variables 3.7% (41628 remain 17%)
c [simplification-18] removed 7470 irredundant clauses 2.6% (277494 remain 20%)
c [simplification-18] maximum reduction of 4% = max (4%, 3%)
c [simplification-18] geometric conflict interval increment 4533 = 22666 / 5
c [simplification-18] new conflict interval 27199
c [simplification-18] penalized conflict interval 27199 = 1 * 27199
c [simplification-18] hard conflict limit 143632 (soft 130033 + delta 13599)
c [simplification-18] new conflict limit 130033 (hard 143632)
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  321.8   41627   277494    106613   25625   4636 670013  258   315   86  82%     85  -25  196  189  103%
c i  329.8   41626   277494    114354   30489   4654 670038  293   406  108  72%     79   61  208  203  102%
c i  330.0   41625   277494    114547   30651   4654 670039  285   401  108  71%     61   55  155  203   77%
c i  330.0   41623   277494    114597   30691   4654 670039  283   400  108  71%     57   54  146  203   72%
c i  346.1   41622   277494    136817   41603   4720 670103  147   200  121  73%    263 -122  135  191   71%
c i  346.3   41617   277494    136981   41707   4720 670109  146   204  121  72%    214 -118  134  190   71%
c i  349.9   41616   277494    141199   43977   4734 670137  191   287  125  67%    -15  -31  287  192  150%
c i  349.9   41583   277494    141256   43996   4734 670137  193   288  125  67%    -18  -30  293  192  153%
c 
c [simplification-19] limit 130033 conflicts (hard 143632) hit after 143633 conflicts
c [quatres-14] found 17893 quaternary clauses 49% in total
c [quatres-14-2] added 1 single-self-subsuming ternary resolvents
c [quatres-14-2] added 1 quaternary resolvents
c [ternres-14] limit 54768778 with penalty 0 = 0 + 0
c [ternres-14] all 41580 free variables schedulable
c [ternres-14] 316 ternary resolvents (1 bin, 315 trn)
c [ternres-14] fully completed ternary resolution
c [gauss-5] limit 684609 penalty 4 = 4 + 0
c [gauss-5] extracted 15 xors of average arity 2.9
c [gauss-5] connected 44 occurrences of 44 variables (average 1.0)
c [gauss-5] limit 684609 penalty 4 = 4 + 0
c [gauss-5] fully completed
c [gauss-5] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-46] removed 7 variables
c [treelook-7] limit 5476877 penalty 0 = 0 + 0 boost 1
c [treelook-7] scheduled 52032 literals 63%
c [treelook-7] scheduling used 1220806 steps
c [treelook-7] scheduled completely
c [treelook-7] limit 5476877 penalty 0 = 0 + 0 boost 1
c [treelook-7] used 5487848 steps
c [treelook-7] 51883 literals remain 62%
c [treelook-7] 7559 variables remain to probed next time 18%
c [decomp-47] removed 1 variables
c [treelook-7] removed 18 variables, found 34748 hbrs
c [unhide-19] limit 2738438 with penalty 2 = 0 + 2
c [unhide-19-34] 14 units, 29 failed, 73364 tauts, 0 hbrs, 340370 literals
c [transred-15] limit 2000000 with penalty 0 = 0 + 0
c [transred-15] removed 428 transitive binary clauses
c [transred-15] found 1 units
c [cce-8] boosting limit by 10
c [cce-8] limit of 684609730 steps penalty 2 = 2 + 0
c [cce-8-1] eliminated 1 clauses out of 1 (100%) of length 86
c [cce-8-1] eliminated 2 clauses out of 2 (100%) of length 85
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 84
c [cce-8-1] eliminated 2 clauses out of 2 (100%) of length 83
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 82
c [cce-8-1] eliminated 2 clauses out of 2 (100%) of length 81
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 80
c [cce-8-1] eliminated 2 clauses out of 2 (100%) of length 79
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 78
c [cce-8-1] eliminated 3 clauses out of 3 (100%) of length 77
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 76
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 75
c [cce-8-1] eliminated 2 clauses out of 2 (100%) of length 74
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 73
c [cce-8-1] eliminated 2 clauses out of 2 (100%) of length 72
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 71
c [cce-8-1] eliminated 2 clauses out of 2 (100%) of length 70
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 69
c [cce-8-1] eliminated 2 clauses out of 2 (100%) of length 68
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 67
c [cce-8-1] eliminated 2 clauses out of 2 (100%) of length 66
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 65
c [cce-8-1] eliminated 2 clauses out of 2 (100%) of length 64
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 63
c [cce-8-1] eliminated 2 clauses out of 2 (100%) of length 62
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 61
c [cce-8-1] eliminated 2 clauses out of 2 (100%) of length 60
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 59
c [cce-8-1] eliminated 2 clauses out of 2 (100%) of length 58
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 57
c [cce-8-1] eliminated 2 clauses out of 2 (100%) of length 56
c [cce-8-1] eliminated 1 clauses out of 2 (50%) of length 55
c [cce-8-1] eliminated 2 clauses out of 2 (100%) of length 54
c [cce-8-1] eliminated 1 clauses out of 3 (33%) of length 53
c [cce-8-1] eliminated 4 clauses out of 4 (100%) of length 52
c [cce-8-1] eliminated 2 clauses out of 4 (50%) of length 51
c [cce-8-1] eliminated 3 clauses out of 4 (75%) of length 50
c [cce-8-1] eliminated 3 clauses out of 4 (75%) of length 49
c [cce-8-1] eliminated 3 clauses out of 5 (60%) of length 48
c [cce-8-1] eliminated 5 clauses out of 6 (83%) of length 47
c [cce-8-1] eliminated 4 clauses out of 6 (67%) of length 46
c [cce-8-1] eliminated 5 clauses out of 6 (83%) of length 45
c [cce-8-1] eliminated 4 clauses out of 6 (67%) of length 44
c [cce-8-1] eliminated 5 clauses out of 6 (83%) of length 43
c [cce-8-1] eliminated 4 clauses out of 6 (67%) of length 42
c [cce-8-1] eliminated 5 clauses out of 6 (83%) of length 41
c [cce-8-1] eliminated 4 clauses out of 6 (67%) of length 40
c [cce-8-1] eliminated 5 clauses out of 6 (83%) of length 39
c [cce-8-1] eliminated 4 clauses out of 6 (67%) of length 38
c [cce-8-1] eliminated 5 clauses out of 6 (83%) of length 37
c [cce-8-1] eliminated 4 clauses out of 6 (67%) of length 36
c [cce-8-1] eliminated 4 clauses out of 6 (67%) of length 35
c [cce-8-1] eliminated 5 clauses out of 7 (71%) of length 34
c [cce-8-1] eliminated 6 clauses out of 7 (86%) of length 33
c [cce-8-1] eliminated 6 clauses out of 8 (75%) of length 32
c [cce-8-1] eliminated 6 clauses out of 9 (67%) of length 31
c [cce-8-1] eliminated 7 clauses out of 12 (58%) of length 30
c [cce-8-1] eliminated 8 clauses out of 11 (73%) of length 29
c [cce-8-1] eliminated 8 clauses out of 11 (73%) of length 28
c [cce-8-1] eliminated 10 clauses out of 12 (83%) of length 27
c [cce-8-1] eliminated 8 clauses out of 14 (57%) of length 26
c [cce-8-1] eliminated 11 clauses out of 14 (79%) of length 25
c [cce-8-1] eliminated 10 clauses out of 16 (62%) of length 24
c [cce-8-1] eliminated 13 clauses out of 16 (81%) of length 23
c [cce-8-1] eliminated 10 clauses out of 16 (62%) of length 22
c [cce-8-1] eliminated 14 clauses out of 18 (78%) of length 21
c [cce-8-1] eliminated 14 clauses out of 21 (67%) of length 20
c [cce-8-1] eliminated 16 clauses out of 20 (80%) of length 19
c [cce-8-1] eliminated 15 clauses out of 23 (65%) of length 18
c [cce-8-1] eliminated 19 clauses out of 26 (73%) of length 17
c [cce-8-1] eliminated 17 clauses out of 26 (65%) of length 16
c [cce-8-1] eliminated 21 clauses out of 26 (81%) of length 15
c [cce-8-1] eliminated 18 clauses out of 24 (75%) of length 14
c [cce-8-1] eliminated 18 clauses out of 26 (69%) of length 13
c [cce-8-1] eliminated 23 clauses out of 28 (82%) of length 12
c [cce-8-1] eliminated 20 clauses out of 31 (65%) of length 11
c [cce-8-1] eliminated 26 clauses out of 33 (79%) of length 10
c [cce-8-1] eliminated 23 clauses out of 36 (64%) of length 9
c [cce-8-1] eliminated 29 clauses out of 41 (71%) of length 8
c [cce-8-1] eliminated 25 clauses out of 66 (38%) of length 7
c [cce-8-1] eliminated 38 clauses out of 2896 (1%) of length 6
c [cce-8-1] eliminated 378 clauses out of 11758 (3%) of length 5
c [cce-8-1] eliminated 1638 clauses out of 17134 (10%) of length 4
c [cce-8-1] completed large round (ATE)
c [cce-8-1] eliminated 2584 large clauses in 434274440 steps
c [cce-8-1] allowing another 217137220 steps for small clauses
c [cce-8-1] scheduling 169448 clauses = 153096 binary + 16352 ternary
c [cce-8-1] tried to eliminate 38128 small clauses 23%
c [cce-8-1] eliminated 7493 binary clauses 5%
c [cce-8-1] eliminated 1146 ternary clauses 7%
c [cce-8-1] eliminated 8639 small clauses 5%
c [cce-8-1] eliminated 8877 small clauses in 684609730 steps
c [cce-8-1] incomplete small round (ATE)
c [cce-8-1] eliminated 11461 covered clauses in round 1
c [cce-8] eliminated 11461 covered clauses in TOTAL during 1 rounds
c [elim-15] no untried remaining variables left
c [elim-15] scheduled 41520 variables 100%
c [elim-15] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-15] rescheduling of touched variables disabled
c [elim-15-1] eliminated 714 variables 2% in round 1 in 22775464 steps
c [elim-15-1] backward subsumption/strengthening limit 22775400
c [elim-15-1-1] backward checking 4936 touched variables 12%
c [elim-15-1-1] fully completed backward checking in 1 rounds
c [elim-15-1] subsumed 9 and strengthened 24 clauses in 1063568 steps
c [elim-15-1] rescheduled 73 variables 0% by backward subsumption
c [elim-15-2] eliminated 10 variables 0% in round 2 in 33945 steps
c [elim-15-2] backward subsumption/strengthening limit 33900
c [elim-15-2-1] backward checking 89 touched variables 0%
c [elim-15-2-1] incomplete backward checking 2 remain 2%
c [elim-15-2] subsumed 4 and strengthened 6 clauses in 33922 steps
c [elim-15-2] rescheduled 23 variables 0% by backward subsumption
c [elim-15-3] eliminated 3 variables 0% in round 3 in 28616 steps
c [elim-15-3] backward subsumption/strengthening limit 28600
c [elim-15-3-1] backward checking 21 touched variables 0%
c [elim-15-3-1] incomplete backward checking 0 remain 0%
c [elim-15-3] subsumed 0 and strengthened 0 clauses in 28601 steps
c [elim-15] fully completed in 3 rounds
c [elim-15] transition to [ all 0 rem 0 ] state
c [elim-15] eliminated 727 = 2% variables out of 41520 scheduled
c [bca-15] limit of 10000000 steps and 527367 added (scaled 2)
c [bca-15] 61005 out of 81588 literals actually usable 75%
c [bca-15] added 27 blocked clauses in 179502 steps
c [sweep-14] limit 16430633 penalty 0 = 0 + 0
c [sweep-14-1] 890 pos 9.8% + 8194 neg 90.2% = 9084 sched 22.3% ret 31709
c [sweep-14-1] 16440237 steps 462 queries 292.42 avg class size
c [sweep-14-1] 4396 decisions 423 SAT calls 119.28 avg env size
c [sweep-14-1] 7672 variables remain 19% (33021 retained 81%)
c [decomp-48] removed 206 variables
c [sweep-14-1] removed 206 vars (0 failed, 42 eqs, 86 impls)
c [sweep-14] removed 206 vars in TOTAL (1 rounds, 461 queries)
c [phase-count-19] 261530 negative 99.8% of 262182 except 652 0.2%
c [phase-count-19] 184121 positive 70.2% of 262182 except 78061 29.8%
c [phase-count-19] skipping relative phase luck test
c [phase-19] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-19] sorted 6256 enqueued variables after 143633 conflicts
c [score-dist-19] active 34331 (85%), one 233 (1%), zero 6023 (15%)
c [score-dist-19] max exp 509, different 426 (84%)
c [score-dist-19] median active exp 486, avg 419.1
c [simplification-19] removed 993 variables 2.4% (40587 remain 16%)
c [simplification-19] removed 15312 irredundant clauses 5.5% (262182 remain 19%)
c [simplification-19] maximum reduction of 6% = max (2%, 6%)
c [simplification-19] large reduction 6% >= 5% limit
c [simplification-19] next conflict interval 2000 = 2000/1
c [simplification-19] penalized conflict interval 2000 = 1 * 2000
c [simplification-19] hard conflict limit 155633 (soft 145633 + delta 10000)
c [simplification-19] new conflict limit 145633 (hard 155633)
c 
c [simplification-20] limit 145633 conflicts (hard 155633) hit after 146576 conflicts
c [quatres-15] found 16424 quaternary clauses 48% in total
c [quatres-15-1] removed 2 duplicate quaternary clauses
c [quatres-15-2] added 2 single-self-subsuming ternary resolvents
c [quatres-15-2] added 8 quaternary resolvents
c [ternres-15] limit 55441977 with penalty 0 = 0 + 0
c [ternres-15] all 40587 free variables schedulable
c [ternres-15] 636 ternary resolvents (2 bin, 634 trn)
c [ternres-15] fully completed ternary resolution
c [basicprobe-7] limit 277209886 penalty 0 = 0 + 0
c [basicprobe-7-0] 12623 sched 32%, 494 failed, 21 lifted, 176959 hbrs
c [decomp-50] removed 747 variables
c [basicprobe-7-1] 14034 probes remain 35% after last round
c [basicprobe-7-1] 522 units = 501 failed (96%) + 21 lifted (4%)
c [basicprobe-7-1] removed 754 variables, found 178131 hbrs
c [bate-6] eliminated 261 asymmetric tautologies during probing
c [unhide-20] limit 2772098 with penalty 2 = 0 + 2
c [unhide-20-35] 0 units, 12 failed, 80137 tauts, 0 hbrs, 73758 literals
c [transred-16] limit 2000000 with penalty 0 = 0 + 0
c [transred-16] removed 464 transitive binary clauses
c [transred-16] found 1 units
c [block-6] scheduling all variables this time
c [block-6] scheduled 39817 variables 100%
c [block-6] limit of 34651235 steps penalty 4 = 4 + 0
c [block-6] fully completed
c [block-6] transition to [ all 0 rem 0 ] state
c [block-6] eliminated 30 blocked clauses
c [block-6] 30 < 1/100 * 254603 = 2546 considered unsuccessful
c [elim-16] scheduling all variables this time
c [elim-16] scheduled 39816 variables 100%
c [elim-16] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-16] rescheduling of touched variables disabled
c [elim-16-1] eliminated 261 variables 1% in round 1 in 22016601 steps
c [elim-16-1] backward subsumption/strengthening limit 22016600
c [elim-16-1-1] backward checking 1815 touched variables 5%
c [elim-16-1-1] fully completed backward checking in 1 rounds
c [elim-16-1] subsumed 1 and strengthened 10 clauses in 431940 steps
c [elim-16-1] rescheduled 27 variables 0% by backward subsumption
c [elim-16-2] eliminated 2 variables 0% in round 2 in 11552 steps
c [elim-16-2] backward subsumption/strengthening limit 11500
c [elim-16-2-1] backward checking 24 touched variables 0%
c [elim-16-2-1] incomplete backward checking 1 remain 4%
c [elim-16-2] subsumed 1 and strengthened 0 clauses in 11526 steps
c [elim-16-2] rescheduled 3 variables 0% by backward subsumption
c [elim-16-3] no variable eliminated in round 3 in 33928 steps
c [elim-16] fully completed in 3 rounds
c [elim-16] transition to [ all 0 rem 0 ] state
c [elim-16] eliminated 263 = 1% variables out of 39816 scheduled
c [elim-16] 263 < 1/100 * 39816 = 398 considered unsuccessful
c [bca-16] limit of 10000000 steps and 509331 added (scaled 2)
c [bca-16] 58341 out of 79108 literals actually usable 74%
c [bca-16] added 22 blocked clauses in 173685 steps
c [sweep-15] limit 16632593 penalty 0 = 0 + 0
c [sweep-15-1] 772 pos 10.4% + 6631 neg 89.6% = 7403 sched 18.7% ret 32150
c [sweep-15-1] 16695138 steps 563 queries 234.38 avg class size
c [sweep-15-1] 4740 decisions 509 SAT calls 100.80 avg env size
c [sweep-15-1] 5931 variables remain 15% (33599 retained 85%)
c [decomp-51] removed 175 variables
c [sweep-15-1] removed 175 vars (0 failed, 59 eqs, 113 impls)
c [sweep-15] removed 175 vars in TOTAL (1 rounds, 562 queries)
c [phase-count-20] 252946 negative 99.7% of 253597 except 651 0.3%
c [phase-count-20] 176590 positive 69.6% of 253597 except 77007 30.4%
c [phase-count-20] skipping relative phase luck test
c [phase-20] phase bias: 1 positive 100%, 0 negative 0%
c [sort-queue-20] sorted 5634 enqueued variables after 146576 conflicts
c [score-dist-20] active 33744 (86%), one 213 (1%), zero 5421 (14%)
c [score-dist-20] max exp 509, different 426 (84%)
c [score-dist-20] median active exp 495, avg 433.5
c [simplification-20] removed 1209 variables 3.0% (39378 remain 16%)
c [simplification-20] removed 8585 irredundant clauses 3.3% (253597 remain 18%)
c [simplification-20] maximum reduction of 3% = max (3%, 3%)
c [simplification-20] geometric conflict interval increment 6799 = 27199 / 4
c [simplification-20] new conflict interval 33998
c [simplification-20] penalized conflict interval 33998 = 1 * 33998
c [simplification-20] hard conflict limit 197573 (soft 180574 + delta 16999)
c [simplification-20] new conflict limit 180574 (hard 197573)
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  412.0   39377   253597    164989   51013   5889 676000  150   206  133  73%    251  -92  109  186   58%
c -  419.2   39377   253597    173132   24890   5895 676015  262   349   61  75%      8   58  313  192  163%
c 
c [simplification-21] limit 180574 conflicts (hard 197573) hit after 180579 conflicts
c [quatres-16] found 15913 quaternary clauses 46% in total
c [quatres-16-1] removed 1 duplicate quaternary clauses
c [quatres-16-2] added 1 single-self-subsuming ternary resolvents
c [ternres-16] limit 62606612 with penalty 0 = 0 + 0
c [ternres-16] all 39377 free variables schedulable
c [ternres-16] 179 ternary resolvents (1 bin, 178 trn)
c [ternres-16] fully completed ternary resolution
c [card-6] limit 1956456 penalty 4 = 4 + 0
c [card-6] found 1740 at-most-one constraints of average size 4.0
c [card-6] no at-most-two constraint found
c [card-6] using previous limit 1956456 for elimination
c [card-6] 1740 out of 1740 constraints (100%) meet size limits
c [card-6] no units found
c [card-6] no at-most-one constraints generated
c [decomp-52] removed 1 variables
c [simpleprobe-8] all 39377 free variables schedulable
c [simpleprobe-8] limit 200000000 penalty 0 = 0 + 0
c [decomp-53] removed 107 variables
c [simpleprobe-8] fully completed simple probing
c [simpleprobe-8] removed 107 variables, found 153223 hbrs, 43 units
c [unhide-21] limit 6260661 with penalty 1 = 0 + 1
c [unhide-21-38] 1 units, 31 failed, 126294 tauts, 0 hbrs, 94907 literals
c [transred-17] limit 2000000 with penalty 0 = 0 + 0
c [transred-17] removed 469 transitive binary clauses
c [transred-17] found 2 units
c [cce-9] limit of 156516530 steps penalty 1 = 1 + 0
c [cce-9-1] eliminated 1 clauses out of 1 (100%) of length 127
c [cce-9-1] eliminated 2 clauses out of 2 (100%) of length 126
c [cce-9-1] eliminated 1 clauses out of 2 (50%) of length 125
c [cce-9-1] eliminated 2 clauses out of 2 (100%) of length 124
c [cce-9-1] eliminated 1 clauses out of 2 (50%) of length 123
c [cce-9-1] eliminated 2 clauses out of 2 (100%) of length 122
c [cce-9-1] eliminated 1 clauses out of 2 (50%) of length 121
c [cce-9-1] eliminated 2 clauses out of 2 (100%) of length 120
c [cce-9-1] eliminated 1 clauses out of 2 (50%) of length 119
c [cce-9-1] eliminated 2 clauses out of 2 (100%) of length 118
c [cce-9-1] eliminated 1 clauses out of 2 (50%) of length 117
c [cce-9-1] eliminated 2 clauses out of 2 (100%) of length 116
c [cce-9-1] eliminated 1 clauses out of 2 (50%) of length 115
c [cce-9-1] eliminated 2 clauses out of 2 (100%) of length 114
c [cce-9-1] eliminated 1 clauses out of 2 (50%) of length 113
c [cce-9-1] eliminated 2 clauses out of 2 (100%) of length 112
c [cce-9-1] eliminated 1 clauses out of 2 (50%) of length 111
c [cce-9-1] eliminated 2 clauses out of 2 (100%) of length 110
c [cce-9-1] eliminated 1 clauses out of 2 (50%) of length 109
c [cce-9-1] eliminated 1 clauses out of 2 (50%) of length 108
c [cce-9-1] eliminated 2 clauses out of 2 (100%) of length 107
c [cce-9-1] eliminated 1 clauses out of 2 (50%) of length 106
c [cce-9-1] eliminated 2 clauses out of 2 (100%) of length 105
c [cce-9-1] eliminated 1 clauses out of 2 (50%) of length 104
c [cce-9-1] eliminated 2 clauses out of 2 (100%) of length 103
c [cce-9-1] eliminated 1 clauses out of 2 (50%) of length 102
c [cce-9-1] eliminated 2 clauses out of 2 (100%) of length 101
c [cce-9-1] eliminated 1 clauses out of 2 (50%) of length 100
c [cce-9-1] eliminated 2 clauses out of 2 (100%) of length 99
c [cce-9-1] eliminated 1 clauses out of 2 (50%) of length 98
c [cce-9-1] eliminated 2 clauses out of 2 (100%) of length 97
c [cce-9-1] eliminated 1 clauses out of 2 (50%) of length 96
c [cce-9-1] eliminated 2 clauses out of 2 (100%) of length 95
c [cce-9-1] eliminated 1 clauses out of 2 (50%) of length 94
c [cce-9-1] eliminated 1 clauses out of 2 (50%) of length 93
c [cce-9-1] eliminated 1 clauses out of 2 (50%) of length 92
c [cce-9-1] eliminated 1 clauses out of 2 (50%) of length 91
c [cce-9-1] eliminated 1 clauses out of 2 (50%) of length 90
c [cce-9-1] eliminated 1 clauses out of 2 (50%) of length 89
c [cce-9-1] eliminated 1 clauses out of 2 (50%) of length 88
c [cce-9-1] eliminated 1 clauses out of 3 (33%) of length 54
c [cce-9-1] eliminated 1 clauses out of 1 (100%) of length 53
c [cce-9-1] eliminated 2 clauses out of 4 (50%) of length 39
c [cce-9-1] eliminated 2 clauses out of 6 (33%) of length 38
c [cce-9-1] eliminated 3 clauses out of 5 (60%) of length 37
c [cce-9-1] eliminated 3 clauses out of 6 (50%) of length 36
c [cce-9-1] eliminated 2 clauses out of 7 (29%) of length 35
c [cce-9-1] eliminated 4 clauses out of 6 (67%) of length 34
c [cce-9-1] eliminated 2 clauses out of 5 (40%) of length 33
c [cce-9-1] eliminated 4 clauses out of 6 (67%) of length 32
c [cce-9-1] eliminated 2 clauses out of 7 (29%) of length 31
c [cce-9-1] eliminated 3 clauses out of 8 (38%) of length 30
c [cce-9-1] eliminated 3 clauses out of 7 (43%) of length 29
c [cce-9-1] eliminated 3 clauses out of 7 (43%) of length 28
c [cce-9-1] eliminated 3 clauses out of 6 (50%) of length 27
c [cce-9-1] eliminated 3 clauses out of 10 (30%) of length 26
c [cce-9-1] eliminated 3 clauses out of 7 (43%) of length 25
c [cce-9-1] eliminated 3 clauses out of 9 (33%) of length 24
c [cce-9-1] eliminated 3 clauses out of 8 (38%) of length 23
c [cce-9-1] eliminated 3 clauses out of 10 (30%) of length 22
c [cce-9-1] eliminated 2 clauses out of 9 (22%) of length 21
c [cce-9-1] eliminated 4 clauses out of 10 (40%) of length 20
c [cce-9-1] eliminated 4 clauses out of 9 (44%) of length 19
c [cce-9-1] eliminated 3 clauses out of 11 (27%) of length 18
c [cce-9-1] eliminated 5 clauses out of 13 (38%) of length 17
c [cce-9-1] eliminated 6 clauses out of 13 (46%) of length 16
c [cce-9-1] eliminated 6 clauses out of 17 (35%) of length 15
c [cce-9-1] eliminated 7 clauses out of 15 (47%) of length 14
c [cce-9-1] eliminated 9 clauses out of 21 (43%) of length 13
c [cce-9-1] eliminated 8 clauses out of 18 (44%) of length 12
c [cce-9-1] eliminated 11 clauses out of 27 (41%) of length 11
c [cce-9-1] eliminated 16 clauses out of 30 (53%) of length 10
c [cce-9-1] eliminated 10 clauses out of 28 (36%) of length 9
c [cce-9-1] eliminated 10 clauses out of 32 (31%) of length 8
c [cce-9-1] eliminated 24 clauses out of 78 (31%) of length 7
c [cce-9-1] eliminated 28 clauses out of 2798 (1%) of length 6
c [cce-9-1] eliminated 186 clauses out of 11051 (2%) of length 5
c [cce-9-1] incomplete large round (ACCE)
c [cce-9-1] eliminated 448 large clauses in 156516532 steps
c [cce-9-1] allowing another 78258266 steps for small clauses
c [cce-9-1] scheduling 154804 clauses = 140704 binary + 14100 ternary
c [cce-9-1] tried to eliminate 6337 small clauses 4%
c [cce-9-1] eliminated 1128 binary clauses 1%
c [cce-9-1] eliminated 191 ternary clauses 1%
c [cce-9-1] eliminated 1319 small clauses 1%
c [cce-9-1] eliminated 1515 small clauses in 156516531 steps
c [cce-9-1] incomplete small round (ACCE)
c [cce-9-1] eliminated 1963 covered clauses in round 1
c [cce-9] eliminated 1963 covered clauses in TOTAL during 1 rounds
c [cce-9] 1963 < 1/100 * 249639 = 2496 considered unsuccessful
c [bca-17] limit of 10000000 steps and 496806 added (scaled 2)
c [bca-17] 57878 out of 78440 literals actually usable 74%
c [bca-17] added 64 blocked clauses in 157827 steps
c [sweep-16] limit 18781983 penalty 0 = 0 + 0
c [sweep-16-1] 732 pos 12.6% + 5077 neg 87.4% = 5809 sched 14.8% ret 33410
c [sweep-16-1] 18856632 steps 706 queries 161.52 avg class size
c [sweep-16-1] 5088 decisions 654 SAT calls 71.73 avg env size
c [sweep-16-1] 4160 variables remain 11% (35044 retained 89%)
c [decomp-54] removed 111 variables
c [sweep-16-1] removed 111 vars (0 failed, 55 eqs, 129 impls)
c [sweep-16] removed 111 vars in TOTAL (1 rounds, 705 queries)
c [phase-count-21] 246770 negative 99.7% of 247421 except 651 0.3%
c [phase-count-21] 172589 positive 69.8% of 247421 except 74832 30.2%
c [phase-count-21] skipping relative phase luck test
c [phase-21] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-21] sorted 5720 enqueued variables after 180579 conflicts
c [score-dist-21] active 33388 (85%), one 572 (1%), zero 5148 (13%)
c [score-dist-21] max exp 510, different 442 (86%)
c [score-dist-21] median active exp 489, avg 412.9
c [simplification-21] removed 269 variables 0.7% (39108 remain 16%)
c [simplification-21] removed 6176 irredundant clauses 2.4% (247421 remain 18%)
c [simplification-21] maximum reduction of 2% = max (1%, 2%)
c [simplification-21] geometric conflict interval increment 11332 = 33998 / 3
c [simplification-21] new conflict interval 45330
c [simplification-21] penalized conflict interval 45330 = 1 * 45330
c [simplification-21] hard conflict limit 248574 (soft 225909 + delta 22665)
c [simplification-21] new conflict limit 225909 (hard 248574)
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  438.4   39107   247421    180626   28312   6123 706696  378   455   79  83%    118  150  386  214  180%
c i  468.3   39105   247421    216427   45669   6275 706788  190   275  129  69%    356  -29  190  208   91%
c i  474.8   39103   247421    223781   48769   6287 706808  210   283  135  74%    -81  -17  232  208  111%
c -  492.5   39092   247421    243905   28177   6308 706823  142   181   62  79%    125  -96  137  193   71%
c 
c [simplification-22] limit 225909 conflicts (hard 248574) hit after 248574 conflicts
c [quatres-17] found 15924 quaternary clauses 46% in total
c [quatres-17-1] removed 1 duplicate quaternary clauses
c [quatres-17-2] added 4 single-self-subsuming ternary resolvents
c [quatres-17-2] added 7 quaternary resolvents
c [ternres-17] limit 77429225 with penalty 0 = 0 + 0
c [ternres-17] all 39092 free variables schedulable
c [ternres-17] 56 ternary resolvents (1 bin, 55 trn)
c [ternres-17] fully completed ternary resolution
c [decomp-55] removed 16 variables
c [treelook-8] limit 7742922 penalty 0 = 0 + 0 boost 1
c [treelook-8] scheduled 49386 literals 63%
c [treelook-8] scheduling used 1171630 steps
c [treelook-8] scheduled completely
c [treelook-8] limit 7742922 penalty 0 = 0 + 0 boost 1
c [treelook-8] used 7787355 steps
c [treelook-8] 49089 literals remain 63%
c [treelook-8] 7234 variables remain to probed next time 19%
c [treelook-8] removed 25 variables, found 41147 hbrs
c [unhide-22] limit 15485845 with penalty 0 = 0 + 0
c [unhide-22-45] 1 units, 49 failed, 201431 tauts, 0 hbrs, 181373 literals
c [transred-18] limit 2000000 with penalty 0 = 0 + 0
c [transred-18] removed 321 transitive binary clauses
c [elim-17] scheduling all variables this time
c [elim-17] scheduled 39015 variables 100%
c [elim-17] limit of 400000000 steps penalty 1 = 1 + 0
c [elim-17] rescheduling of touched variables disabled
c [elim-17-1] eliminated 329 variables 1% in round 1 in 20865250 steps
c [elim-17-1] backward subsumption/strengthening limit 20865200
c [elim-17-1-1] backward checking 2337 touched variables 6%
c [elim-17-1-1] fully completed backward checking in 1 rounds
c [elim-17-1] subsumed 0 and strengthened 13 clauses in 490334 steps
c [elim-17-1] rescheduled 45 variables 0% by backward subsumption
c [elim-17-2] no variable eliminated in round 2 in 20478 steps
c [elim-17] fully completed in 2 rounds
c [elim-17] transition to [ all 0 rem 0 ] state
c [elim-17] eliminated 329 = 1% variables out of 39015 scheduled
c [elim-17] 329 < 1/100 * 39015 = 390 considered unsuccessful
c [bca-18] limit of 10000000 steps and 490150 added (scaled 2)
c [bca-18] 56151 out of 77374 literals actually usable 73%
c [bca-18] added 274 blocked clauses in 154862 steps
c [sweep-17] limit 23228767 penalty 0 = 0 + 0
c [sweep-17-1] 478 pos 12.0% + 3517 neg 88.0% = 3995 sched 10.3% ret 34691
c [sweep-17-1] 23269902 steps 1020 queries 63.64 avg class size
c [sweep-17-1] 6473 decisions 943 SAT calls 61.27 avg env size
c [sweep-17-1] 2026 variables remain 5% (36623 retained 95%)
c [decomp-57] removed 172 variables
c [sweep-17-1] removed 172 vars (0 failed, 83 eqs, 169 impls)
c [sweep-17] removed 172 vars in TOTAL (1 rounds, 1019 queries)
c [phase-count-22] 243401 negative 99.7% of 244057 except 656 0.3%
c [phase-count-22] 170709 positive 69.9% of 244057 except 73348 30.1%
c [phase-count-22] skipping relative phase luck test
c [phase-22] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-22] sorted 8664 enqueued variables after 248574 conflicts
c [score-dist-22] active 29850 (78%), one 3739 (10%), zero 4925 (13%)
c [score-dist-22] max exp 510, different 444 (87%)
c [score-dist-22] median active exp 498, avg 420.4
c [simplification-22] removed 578 variables 1.5% (38514 remain 16%)
c [simplification-22] removed 3364 irredundant clauses 1.4% (244057 remain 18%)
c [simplification-22] maximum reduction of 1% = max (1%, 1%)
c [simplification-22] geometric conflict interval increment 22665 = 45330 / 2
c [simplification-22] new conflict interval 67995
c [simplification-22] penalized conflict interval 67995 = 1 * 67995
c [simplification-22] hard conflict limit 350566 (soft 316569 + delta 33997)
c [simplification-22] new conflict limit 316569 (hard 350566)
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  531.7   38513   244057    278206   43275   5919 529445   96   120   94  80%    491 -103   89  158   57%
c i  536.8   38512   244057    284140   45345   5922 529450   99   122  107  81%   -249  -92   71  154   46%
c i  537.4   38511   244057    285044   45863   5923 529453  104   136  107  76%   -287  -77  140  153   91%
c -  555.2   38511   244057    307138   30484   5955 529508  102   149   57  69%     49  -52  127  142   89%
c i  562.6   38510   244057    315819   35459   5972 529522  103   148   76  70%    170  -49   82  139   59%
c i  562.6   38505   244057    315821   35460   5972 529522  103   148   76  70%    169  -49   82  139   59%
c i  562.6   38504   244057    315823   35461   5972 529522  103   148   76  70%    168  -49   82  139   59%
c i  562.6   38499   244057    315825   35462   5972 529522  103   148   76  70%    168  -49   81  139   58%
c 
c [simplification-23] limit 316584 conflicts (hard 350566) hit after 350567 conflicts
c [quatres-18] found 16082 quaternary clauses 44% in total
c [quatres-18-1] removed 1 duplicate quaternary clauses
c [quatres-18-2] added 1 single-self-subsuming ternary resolvents
c [ternres-18] limit 98675343 with penalty 0 = 0 + 0
c [ternres-18] all 38497 free variables schedulable
c [ternres-18] 211 ternary resolvents (2 bin, 209 trn)
c [ternres-18] fully completed ternary resolution
c [decomp-58] removed 20 variables
c [basicprobe-8] limit 400000000 penalty 0 = 0 + 0
c [basicprobe-8-0] 13755 sched 36%, 397 failed, 37 lifted, 60623 hbrs
c [decomp-59] removed 697 variables
c [basicprobe-8-1] 5670 probes remain 15% after last round
c [basicprobe-8-1] 594 units = 552 failed (93%) + 42 lifted (7%)
c [basicprobe-8-1] removed 980 variables, found 72287 hbrs
c [bate-7] eliminated 183 asymmetric tautologies during probing
c [unhide-23] limit 4933767 with penalty 2 = 0 + 2
c [unhide-23-47] 1 units, 10 failed, 50102 tauts, 0 hbrs, 1171227 literals
c [transred-19] limit 2000000 with penalty 0 = 0 + 0
c [transred-19] removed 377 transitive binary clauses
c [bca-19] limit of 10000000 steps and 469027 added (scaled 2)
c [bca-19] 52240 out of 75016 literals actually usable 70%
c [bca-19] added 62 blocked clauses in 175438 steps
c [sweep-18] almost no limit of 4000000000 steps
c [sweep-18-1] 210 pos 11.2% + 1673 neg 88.8% = 1883 sched 5.0% ret 35624
c [sweep-18-1] 20935679 steps 1346 queries 20.41 avg class size
c [sweep-18-1] 8020 decisions 1209 SAT calls 56.43 avg env size
c [sweep-18-1] fully completed sweeping round
c [decomp-60] removed 168 variables
c [sweep-18-1] removed 168 vars (0 failed, 137 eqs, 229 impls)
c [sweep-18-2] 3986 pos 10.7% + 33353 neg 89.3% = 37339 sched 100.0% ret 0
c [sweep-18-2] 183099649 steps 5599 queries 60.20 avg class size
c [sweep-18-2] 61540 decisions 5318 SAT calls 102.55 avg env size
c [sweep-18-2] fully completed sweeping round
c [decomp-61] removed 386 variables
c [sweep-18-2] removed 386 vars (0 failed, 310 eqs, 802 impls)
c [sweep-18-3] 3983 pos 10.8% + 32970 neg 89.2% = 36953 sched 100.0% ret 0
c [sweep-18-3] 183867386 steps 5372 queries 51.65 avg class size
c [sweep-18-3] 64237 decisions 5207 SAT calls 112.65 avg env size
c [sweep-18-3] fully completed sweeping round
c [decomp-62] removed 239 variables
c [sweep-18-3] removed 239 vars (0 failed, 189 eqs, 566 impls)
c [sweep-18] removed 793 vars in TOTAL (3 rounds, 12314 queries)
c [sort-queue-23] sorted 6251 enqueued variables after 350567 conflicts
c [score-dist-23] active 30463 (83%), one 2503 (7%), zero 3748 (10%)
c [score-dist-23] max exp 511, different 323 (63%)
c [score-dist-23] median active exp 503, avg 486.3
c [simplification-23] removed 1783 variables 4.6% (36714 remain 15%)
c [simplification-23] removed 12369 irredundant clauses 5.1% (231688 remain 17%)
c [simplification-23] maximum reduction of 5% = max (5%, 5%)
c [simplification-23] large reduction 5% >= 5% limit
c [simplification-23] next conflict interval 3505 = min (350567/100, 67995)
c [simplification-23] penalized conflict interval 3505 = 1 * 3505
c [simplification-23] hard conflict limit 364072 (soft 354072 + delta 10000)
c [simplification-23] new conflict limit 354072 (hard 364072)
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 -  632.3   36714   231688    350567   31456   5706 563928   82   110   45  75%    234  -61   70  118   59%
c i  633.9   36713   231688    352370   32459   5706 563933   88   128   70  69%    256  -41   95  118   81%
c 
c [simplification-24] limit 354072 conflicts (hard 364072) hit after 364076 conflicts
c [quatres-19] found 14652 quaternary clauses 41% in total
c [quatres-19-2] added 6 single-self-subsuming ternary resolvents
c [ternres-19] limit 101447752 with penalty 0 = 0 + 0
c [ternres-19] all 36713 free variables schedulable
c [ternres-19] 473 ternary resolvents (3 bin, 470 trn)
c [ternres-19] fully completed ternary resolution
c [decomp-63] removed 1 variables
c [simpleprobe-9] all 36713 free variables schedulable
c [simpleprobe-9] limit 200000000 penalty 0 = 0 + 0
c [decomp-64] removed 177 variables
c [simpleprobe-9] fully completed simple probing
c [simpleprobe-9] removed 177 variables, found 96076 hbrs, 82 units
c [unhide-24] limit 10000000 with penalty 1 = 0 + 1
c [unhide-24-52] 1 units, 12 failed, 203344 tauts, 0 hbrs, 594056 literals
c [transred-20] limit 2000000 with penalty 0 = 0 + 0
c [transred-20] removed 434 transitive binary clauses
c [cce-10] limit of 126809690 steps penalty 2 = 2 + 0
c [cce-10-1] eliminated 1 clauses out of 2 (50%) of length 115
c [cce-10-1] eliminated 1 clauses out of 1 (100%) of length 114
c [cce-10-1] eliminated 1 clauses out of 3 (33%) of length 113
c [cce-10-1] eliminated 1 clauses out of 2 (50%) of length 112
c [cce-10-1] eliminated 1 clauses out of 3 (33%) of length 111
c [cce-10-1] eliminated 2 clauses out of 2 (100%) of length 110
c [cce-10-1] eliminated 1 clauses out of 3 (33%) of length 109
c [cce-10-1] eliminated 1 clauses out of 2 (50%) of length 108
c [cce-10-1] eliminated 2 clauses out of 3 (67%) of length 107
c [cce-10-1] eliminated 1 clauses out of 3 (33%) of length 106
c [cce-10-1] eliminated 1 clauses out of 2 (50%) of length 105
c [cce-10-1] eliminated 1 clauses out of 3 (33%) of length 104
c [cce-10-1] eliminated 1 clauses out of 2 (50%) of length 103
c [cce-10-1] eliminated 1 clauses out of 3 (33%) of length 102
c [cce-10-1] eliminated 1 clauses out of 2 (50%) of length 101
c [cce-10-1] eliminated 1 clauses out of 3 (33%) of length 100
c [cce-10-1] eliminated 1 clauses out of 2 (50%) of length 99
c [cce-10-1] eliminated 1 clauses out of 3 (33%) of length 98
c [cce-10-1] eliminated 1 clauses out of 2 (50%) of length 97
c [cce-10-1] eliminated 1 clauses out of 3 (33%) of length 96
c [cce-10-1] eliminated 1 clauses out of 2 (50%) of length 95
c [cce-10-1] eliminated 1 clauses out of 3 (33%) of length 94
c [cce-10-1] eliminated 1 clauses out of 2 (50%) of length 93
c [cce-10-1] eliminated 2 clauses out of 4 (50%) of length 92
c [cce-10-1] eliminated 1 clauses out of 3 (33%) of length 91
c [cce-10-1] eliminated 1 clauses out of 3 (33%) of length 90
c [cce-10-1] eliminated 1 clauses out of 3 (33%) of length 89
c [cce-10-1] eliminated 1 clauses out of 3 (33%) of length 88
c [cce-10-1] eliminated 1 clauses out of 4 (25%) of length 87
c [cce-10-1] eliminated 1 clauses out of 3 (33%) of length 86
c [cce-10-1] eliminated 2 clauses out of 3 (67%) of length 85
c [cce-10-1] eliminated 1 clauses out of 2 (50%) of length 84
c [cce-10-1] eliminated 1 clauses out of 2 (50%) of length 83
c [cce-10-1] eliminated 1 clauses out of 3 (33%) of length 82
c [cce-10-1] eliminated 1 clauses out of 2 (50%) of length 81
c [cce-10-1] eliminated 1 clauses out of 4 (25%) of length 80
c [cce-10-1] eliminated 1 clauses out of 2 (50%) of length 79
c [cce-10-1] eliminated 2 clauses out of 3 (67%) of length 78
c [cce-10-1] eliminated 1 clauses out of 2 (50%) of length 77
c [cce-10-1] eliminated 1 clauses out of 3 (33%) of length 76
c [cce-10-1] eliminated 1 clauses out of 2 (50%) of length 75
c [cce-10-1] eliminated 1 clauses out of 3 (33%) of length 74
c [cce-10-1] eliminated 1 clauses out of 4 (25%) of length 73
c [cce-10-1] eliminated 2 clauses out of 3 (67%) of length 72
c [cce-10-1] eliminated 1 clauses out of 3 (33%) of length 71
c [cce-10-1] eliminated 1 clauses out of 3 (33%) of length 70
c [cce-10-1] eliminated 2 clauses out of 3 (67%) of length 69
c [cce-10-1] eliminated 1 clauses out of 3 (33%) of length 68
c [cce-10-1] eliminated 1 clauses out of 3 (33%) of length 67
c [cce-10-1] eliminated 2 clauses out of 3 (67%) of length 66
c [cce-10-1] eliminated 1 clauses out of 3 (33%) of length 65
c [cce-10-1] eliminated 1 clauses out of 3 (33%) of length 64
c [cce-10-1] eliminated 1 clauses out of 2 (50%) of length 63
c [cce-10-1] eliminated 2 clauses out of 4 (50%) of length 62
c [cce-10-1] eliminated 1 clauses out of 3 (33%) of length 61
c [cce-10-1] eliminated 1 clauses out of 5 (20%) of length 60
c [cce-10-1] eliminated 1 clauses out of 2 (50%) of length 59
c [cce-10-1] eliminated 1 clauses out of 4 (25%) of length 58
c [cce-10-1] eliminated 1 clauses out of 2 (50%) of length 57
c [cce-10-1] eliminated 1 clauses out of 4 (25%) of length 56
c [cce-10-1] eliminated 1 clauses out of 2 (50%) of length 55
c [cce-10-1] eliminated 1 clauses out of 3 (33%) of length 54
c [cce-10-1] eliminated 2 clauses out of 3 (67%) of length 53
c [cce-10-1] eliminated 2 clauses out of 6 (33%) of length 52
c [cce-10-1] eliminated 2 clauses out of 4 (50%) of length 51
c [cce-10-1] eliminated 3 clauses out of 6 (50%) of length 50
c [cce-10-1] eliminated 1 clauses out of 3 (33%) of length 49
c [cce-10-1] eliminated 1 clauses out of 3 (33%) of length 48
c [cce-10-1] eliminated 1 clauses out of 5 (20%) of length 47
c [cce-10-1] eliminated 2 clauses out of 4 (50%) of length 46
c [cce-10-1] eliminated 1 clauses out of 5 (20%) of length 45
c [cce-10-1] eliminated 1 clauses out of 2 (50%) of length 44
c [cce-10-1] eliminated 1 clauses out of 4 (25%) of length 43
c [cce-10-1] eliminated 1 clauses out of 4 (25%) of length 42
c [cce-10-1] eliminated 2 clauses out of 6 (33%) of length 41
c [cce-10-1] eliminated 1 clauses out of 4 (25%) of length 40
c [cce-10-1] eliminated 1 clauses out of 6 (17%) of length 39
c [cce-10-1] eliminated 1 clauses out of 3 (33%) of length 38
c [cce-10-1] eliminated 1 clauses out of 5 (20%) of length 37
c [cce-10-1] eliminated 1 clauses out of 3 (33%) of length 36
c [cce-10-1] eliminated 1 clauses out of 6 (17%) of length 35
c [cce-10-1] eliminated 1 clauses out of 4 (25%) of length 34
c [cce-10-1] eliminated 1 clauses out of 6 (17%) of length 33
c [cce-10-1] eliminated 1 clauses out of 3 (33%) of length 32
c [cce-10-1] eliminated 1 clauses out of 7 (14%) of length 23
c [cce-10-1] eliminated 2 clauses out of 8 (25%) of length 22
c [cce-10-1] eliminated 2 clauses out of 11 (18%) of length 21
c [cce-10-1] eliminated 2 clauses out of 11 (18%) of length 20
c [cce-10-1] eliminated 2 clauses out of 11 (18%) of length 19
c [cce-10-1] eliminated 3 clauses out of 8 (38%) of length 18
c [cce-10-1] eliminated 1 clauses out of 10 (10%) of length 17
c [cce-10-1] eliminated 3 clauses out of 12 (25%) of length 16
c [cce-10-1] eliminated 2 clauses out of 9 (22%) of length 15
c [cce-10-1] eliminated 1 clauses out of 14 (7%) of length 14
c [cce-10-1] eliminated 1 clauses out of 10 (10%) of length 13
c [cce-10-1] eliminated 1 clauses out of 10 (10%) of length 12
c [cce-10-1] eliminated 1 clauses out of 14 (7%) of length 11
c [cce-10-1] eliminated 1 clauses out of 17 (6%) of length 10
c [cce-10-1] eliminated 3 clauses out of 20 (15%) of length 9
c [cce-10-1] eliminated 6 clauses out of 28 (21%) of length 8
c [cce-10-1] eliminated 8 clauses out of 64 (12%) of length 7
c [cce-10-1] eliminated 11 clauses out of 2756 (0%) of length 6
c [cce-10-1] eliminated 11 clauses out of 10344 (0%) of length 5
c [cce-10-1] incomplete large round (ATE)
c [cce-10-1] eliminated 162 large clauses in 126809692 steps
c [cce-10-1] allowing another 63404846 steps for small clauses
c [cce-10-1] scheduling 187977 clauses = 135416 binary + 52561 ternary
c [cce-10-1] tried to eliminate 4932 small clauses 3%
c [cce-10-1] eliminated 531 binary clauses 0%
c [cce-10-1] eliminated 126 ternary clauses 0%
c [cce-10-1] eliminated 657 small clauses 0%
c [cce-10-1] eliminated 657 small clauses in 126809692 steps
c [cce-10-1] incomplete small round (ATE)
c [cce-10-1] eliminated 819 covered clauses in round 1
c [cce-10] eliminated 819 covered clauses in TOTAL during 1 rounds
c [cce-10] 819 < 1/100 * 227463 = 2274 considered unsuccessful
c [bca-20] limit of 10000000 steps and 454942 added (scaled 2)
c [bca-20] 49076 out of 73002 literals actually usable 67%
c [bca-20] added 41 blocked clauses in 146896 steps
c [sweep-19] limit 30434325 penalty 0 = 0 + 0
c [sweep-19-1] 3930 pos 10.8% + 32570 neg 89.2% = 36500 sched 100.0% ret 0
c [sweep-19-1] 30452485 steps 723 queries 308.80 avg class size
c [sweep-19-1] 16322 decisions 696 SAT calls 173.36 avg env size
c [sweep-19-1] 22616 variables remain 62% (13835 retained 38%)
c [decomp-65] removed 133 variables
c [sweep-19-1] removed 133 vars (0 failed, 34 eqs, 67 impls)
c [sweep-19] removed 133 vars in TOTAL (1 rounds, 722 queries)
c [sort-queue-24] sorted 5741 enqueued variables after 364076 conflicts
c [score-dist-24] active 30626 (84%), one 2328 (6%), zero 3413 (9%)
c [score-dist-24] max exp 510, different 305 (60%)
c [score-dist-24] median active exp 497, avg 471.7
c [simplification-24] removed 346 variables 0.9% (36367 remain 15%)
c [simplification-24] removed 5845 irredundant clauses 2.5% (225843 remain 16%)
c [simplification-24] maximum reduction of 3% = max (1%, 3%)
c [simplification-24] geometric conflict interval increment 16998 = 67995 / 4
c [simplification-24] new conflict interval 84993
c [simplification-24] penalized conflict interval 84993 = 1 * 84993
c [simplification-24] hard conflict limit 491565 (soft 449069 + delta 42496)
c [simplification-24] new conflict limit 449069 (hard 491565)
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 -  688.7   36367   225843    396504   33431   6124 452516  205   284   55  72%    336  134  263  112  234%
c i  712.7   36366   225843    422894   47353   6196 452598  111   157  105  71%    564  -18   81  126   64%
c i  715.6   36365   225843    426064   49055   6202 452611  121   171  105  71%   -430   -4   67  126   53%
c i  728.5   36362   225843    440990   59140   6227 452650  145   235  129  62%   -214   58  119  126   94%
c i  728.5   36361   225843    441007   59150   6227 452651  145   234  129  62%   -218   57  119  126   94%
c i  730.7   36360   225843    443268   60144   6235 452651  152   228  129  67%   -375   49  174  127  137%
c i  730.7   36359   225843    443303   60162   6235 452652  152   229  129  67%   -377   50  175  127  138%
c i  731.5   36358   225843    444136   60582   6236 452652  165   243  129  68%   -392   63  212  129  165%
c i  731.5   36357   225843    444137   60582   6236 452652  165   243  129  68%   -392   63  211  129  164%
c i  731.6   36356   225843    444147   60591   6236 452652  165   243  129  68%   -392   63  211  129  164%
c i  731.6   36355   225843    444153   60595   6236 452652  165   243  129  68%   -392   63  210  129  163%
c i  731.8   36354   225843    444339   60660   6236 452652  166   242  129  69%   -394   62  194  129  151%
c -  739.1   36354   225843    451383   34175   6243 452661  100   145   75  69%   -282  -36   79  125   64%
c i  749.6   36353   225843    463389   42079   6282 452679   88   154   96  57%    -63  -23   76  120   63%
c 
c [simplification-25] limit 449081 conflicts (hard 491565) hit after 491568 conflicts
c [quatres-20] found 14738 quaternary clauses 39% in total
c [quatres-20-2] added 2 single-self-subsuming ternary resolvents
c [quatres-20-2] added 1 quaternary resolvents
c [ternres-20] limit 128803187 with penalty 0 = 0 + 0
c [ternres-20] all 36353 free variables schedulable
c [ternres-20] 83 ternary resolvents (2 bin, 81 trn)
c [ternres-20] fully completed ternary resolution
c [gauss-6] limit 1610039 penalty 4 = 4 + 0
c [gauss-6] extracted 45 xors of average arity 3.0
c [gauss-6] connected 135 occurrences of 135 variables (average 1.0)
c [gauss-6] limit 1610039 penalty 4 = 4 + 0
c [gauss-6] fully completed
c [gauss-6] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-66] removed 1 variables
c [treelook-9] limit 12880318 penalty 0 = 0 + 0 boost 1
c [treelook-9] scheduled 46635 literals 64%
c [treelook-9] scheduling used 972399 steps
c [treelook-9] scheduled completely
c [treelook-9] limit 12880318 penalty 0 = 0 + 0 boost 1
c [treelook-9] used 12896862 steps
c [treelook-9] 46230 literals remain 64%
c [treelook-9] 6779 variables remain to probed next time 19%
c [decomp-67] removed 1 variables
c [treelook-9] removed 6 variables, found 97565 hbrs
c [unhide-25] limit 5000000 with penalty 2 = 0 + 2
c [unhide-25-54] 1 units, 16 failed, 61276 tauts, 0 hbrs, 961661 literals
c [transred-21] limit 2000000 with penalty 0 = 0 + 0
c [transred-21] removed 412 transitive binary clauses
c [elim-18] scheduling all variables this time
c [elim-18] scheduled 36332 variables 100%
c [elim-18] boosting limit by 20
c [elim-18] limit of 4000000000 steps penalty 2 = 2 + 0
c [elim-18] rescheduling of touched variables disabled
c [elim-18-1] eliminated 573 variables 2% in round 1 in 19650145 steps
c [elim-18-1] backward subsumption/strengthening limit 19650100
c [elim-18-1-1] backward checking 3238 touched variables 9%
c [elim-18-1-1] fully completed backward checking in 1 rounds
c [elim-18-1] subsumed 7 and strengthened 19 clauses in 604123 steps
c [elim-18-1] rescheduled 76 variables 0% by backward subsumption
c [elim-18-2] eliminated 6 variables 0% in round 2 in 38317 steps
c [elim-18-2] backward subsumption/strengthening limit 38300
c [elim-18-2-1] backward checking 56 touched variables 0%
c [elim-18-2-1] incomplete backward checking 0 remain 0%
c [elim-18-2] subsumed 2 and strengthened 4 clauses in 38301 steps
c [elim-18-2] rescheduled 15 variables 0% by backward subsumption
c [elim-18-3] eliminated 2 variables 0% in round 3 in 8462 steps
c [elim-18-3] backward subsumption/strengthening limit 8400
c [elim-18-3-1] backward checking 23 touched variables 0%
c [elim-18-3-1] incomplete backward checking 0 remain 0%
c [elim-18-3] subsumed 1 and strengthened 0 clauses in 8401 steps
c [elim-18] incomplete 3 not tried 0% in round 3
c [elim-18] transition to [ all 1 rem 1 ] state
c [elim-18] eliminated 581 = 2% variables out of 36332 scheduled
c [bca-21] limit of 10000000 steps and 450112 added (scaled 2)
c [bca-21] 46368 out of 71504 literals actually usable 65%
c [bca-21] added 41 blocked clauses in 157155 steps
c [sweep-20] limit 38640956 penalty 0 = 0 + 0
c [sweep-20-1] 3459 pos 15.6% + 18704 neg 84.4% = 22163 sched 62.0% ret 13588
c [sweep-20-1] 38684396 steps 1020 queries 230.54 avg class size
c [sweep-20-1] 18108 decisions 998 SAT calls 129.79 avg env size
c [sweep-20-1] 13756 variables remain 38% (21992 retained 62%)
c [decomp-68] removed 34 variables
c [sweep-20-1] removed 34 vars (0 failed, 26 eqs, 82 impls)
c [sweep-20] 34 < 1/1000 * 35751 = 35 considered unsuccessful
c [sweep-20] removed 34 vars in TOTAL (1 rounds, 1019 queries)
c [sort-queue-25] sorted 8042 enqueued variables after 491568 conflicts
c [score-dist-25] active 27675 (77%), one 4903 (14%), zero 3139 (9%)
c [score-dist-25] max exp 509, different 444 (87%)
c [score-dist-25] median active exp 502, avg 446.0
c [simplification-25] removed 636 variables 1.7% (35717 remain 15%)
c [simplification-25] removed 1702 irredundant clauses 0.8% (224141 remain 16%)
c [simplification-25] maximum reduction of 2% = max (2%, 1%)
c [simplification-25] geometric conflict interval increment 28331 = 84993 / 3
c [simplification-25] new conflict interval 113324
c [simplification-25] penalized conflict interval 113324 = 1 * 113324
c [simplification-25] hard conflict limit 661554 (soft 604892 + delta 56662)
c [simplification-25] new conflict limit 604892 (hard 661554)
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.2   35716   224141    498923   61437   6195 456961   93   132  121  71%    216  -25  119  108  110%
c -  803.2   35716   224141    506203   35648   6207 456970  113   167   55  67%   -203   14  292  108  272%
c i  861.4   35715   224141    569085   60380   6228 457001  181   212  147  85%    554   43  189  136  140%
c -  881.9   35715   224141    590144   36195   6234 457010  123   160   58  77%   -125  -12  118  136   87%
c i  927.1   35714   224141    637619   61733   6248 457057   85   122  149  70%    467  -26  136  115  118%
c -  935.0   35714   224141    646444   36958   6260 457061   73   108   57  67%   -413  -35   72  110   65%
c i  945.5   35713   224141    659036   49248   6267 457091   54    79  129  68%   -162  -55   50  100   50%
c 
c [simplification-26] limit 604892 conflicts (hard 661554) hit after 661556 conflicts
c [quatres-21] found 14904 quaternary clauses 39% in total
c [quatres-21-1] removed 1 duplicate quaternary clauses
c [quatres-21-2] added 3 quaternary resolvents
c [ternres-21] limit 164218259 with penalty 0 = 0 + 0
c [ternres-21] all 35713 free variables schedulable
c [ternres-21] 142 ternary resolvents (1 bin, 141 trn)
c [ternres-21] fully completed ternary resolution
c [decomp-69] removed 5 variables
c [basicprobe-9] limit 400000000 penalty 0 = 0 + 0
c [basicprobe-9-0] 5581 sched 16%, 223 failed, 5 lifted, 21535 hbrs
c [decomp-70] removed 346 variables
c [basicprobe-9-1] 12580 sched 36%, 191 failed, 11 lifted, 30676 hbrs
c [decomp-71] removed 249 variables
c [basicprobe-9-2] 7393 probes remain 21% after last round
c [basicprobe-9-2] 497 units = 481 failed (97%) + 16 lifted (3%)
c [basicprobe-9-2] removed 673 variables, found 56096 hbrs
c [bate-8] eliminated 96 asymmetric tautologies during probing
c [unhide-26] limit 5000000 with penalty 2 = 0 + 2
c [unhide-26-57] 1 units, 19 failed, 68626 tauts, 0 hbrs, 1770110 literals
c [transred-22] limit 2000000 with penalty 0 = 0 + 0
c [transred-22] removed 394 transitive binary clauses
c [transred-22] found 1 units
c [block-7] scheduling all variables this time
c [block-7] scheduled 35020 variables 100%
c [block-7] limit of 50000000 steps penalty 4 = 4 + 0
c [block-7] fully completed
c [block-7] transition to [ all 0 rem 0 ] state
c [block-7] eliminated 73 blocked clauses
c [block-7] 73 < 1/100 * 215535 = 2155 considered unsuccessful
c [bca-22] limit of 10000000 steps and 432447 added (scaled 2)
c [bca-22] 45581 out of 70042 literals actually usable 65%
c [bca-22] added 43 blocked clauses in 148553 steps
c [sort-queue-26] sorted 12160 enqueued variables after 661556 conflicts
c [score-dist-26] active 22860 (65%), one 9593 (27%), zero 2567 (7%)
c [score-dist-26] max exp 509, different 364 (71%)
c [score-dist-26] median active exp 500, avg 462.7
c [simplification-26] removed 693 variables 1.9% (35020 remain 14%)
c [simplification-26] removed 8765 irredundant clauses 3.9% (215376 remain 16%)
c [simplification-26] maximum reduction of 4% = max (2%, 4%)
c [simplification-26] geometric conflict interval increment 22664 = 113324 / 5
c [simplification-26] new conflict interval 135988
c [simplification-26] penalized conflict interval 135988 = 1 * 135988
c [simplification-26] hard conflict limit 865538 (soft 797544 + delta 67994)
c [simplification-26] new conflict limit 797544 (hard 865538)
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  994.4   35019   215376    685301   64827   6249 430967   92   121  148  76%      2  -18   98  104   94%
c
c CAUGHT SIGNAL 15 SIGTERM
c
c s UNKNOWN
c bate: 3032 basic ate = 2969 trn 98% + 63 lrg 2% in 8 updates
c bcas: 22 count, 2433 added (700 skipped), 5966647 steps
c bkwd: tried 491877 clauses, 983514 lits, 2.00 lits/clause
c bkwd: checked 16286300 occs, 33.11 occs/clause, 16.56 occs/lit
c bkwd: subsumed 12 binary, 75 ternary, 14 large
c bkwd: strengthened 1 binary, 0 ternary (0% self), 710 large (0% self)
c blkd: 7 bces, 13118 removed, 10699116 resolutions, 29693910 steps
c blkd: 18399 blocking literals 4%, 8 pure
c bump: 692646 bumped seen, 602537574 lits 869.9 on average
c card: 6 count, 0 units, 0 am1, 307158296 steps
c card: 0 rescheduled, 0 eliminated, 0 resolved, 71994 subsumed
c card: 18029 at-most-one constraints found, average size 4.76
c card: 18029 at-most-one constraints used 100%, average size 4.76
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: 10 cces, 79739 eliminated, 78771 ate 99%, 968 abce 1%
c cces: 0 probed, 0 lifted, 0 failed
c cces: 0 cached, 0 rsz, 0 cols 0%, 0 srch, 0 hits 0%
c clls: 1 sat, 0 simp, 0 freeze, 0 melt
c clls: 4740073 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 218 gcs, 0 rescored clauses, 2676 rescored vars
c dcps: 71 decompositions, 10443 equivalent 4%
c deco: 311431 decision-only clauses 45%, 74% reduction
c decs: 8313105 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 18 elims, 109501 eliminated 42%, 216 pure 0%
c elms: 45 rounds, 2.5 rounds/bve
c elms: 86374 small 79%, 22903 large 21%
c elms: 258372 tried small, 86374 succeeded 33%, 171998 failed 67%
c elms: 44209 subsumed, 73217 strengthened, 1701 blocked
c elms: 24984571 copies, 24773702 resolutions, 7099199 ipos
c elms: 6785185 subchks, 4178500 strchks
c gaus: 6 extractions, 162 extracted, 2.8 size, 3 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 13640794 steps, 6820397 extr 50%, 652 elim 0%
c glue: 146.3 orig avg, 146.3 real avg, 9.1 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 2370549 = 734359 simple 31% + 1516711 trn 64% + 119479 lrg 5%, 5571 sub 0%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 692646 clauses, 294.8 length
c lrnd: 204197939 lits = 424856922 orig - 220658983 removed 52%
c lrnd: 308933 uips 45%, 337428 flips 49%
c mins: 338160 mins 51%, 2959 bin 0%, 5603 size 1%
c mins: 229022144 poisoned searches, 61856443 hits, 27% hit rate
c mins: 283631375 used twice searches, 17568034 hits, 6% hit rate
c move: moved 40696, 27182 bin 67%, 13514 trn 33%
c otfs: 4733 driving 43%, 6289 restarting 57%
c otfs: str 11022, 10882 red 99%, 140 irr 1%
c otfs: str 11022, 0 bin 0%, 103 trn 1%, 10919 lrg 99%
c otfs: sub 122, 122 red 100%, 0 irr 0%
c otfs: sub 122, 0 bin 0%, 0 trn 0%, 122 lrg 100%
c phas: 22 computed, 129346 set, 180 pos (0%), 129166 neg (100%)
c prbs: 9 basic, 160116 probed, 4409 failed, 247 lifted
c prbs: 9 simple, 1206274 probed, 2038 failed, 1244 eqs
c prbs: 9 treelook, 1079 probed, 42 failed, 0 lifted
c prom: 42130 locked 2% out of 2293599 tried
c prps: 2464361292 props, 275 props/dec
c prps: 93% srch, 7% simp, 0% lkhd
c quat: 21 count, 87 quat, 34 self1, 0 self2, 436 dup
c queu: 26 sorted, 8313105 next (75113 steps 0.01)
c queu: 687282083 enq (1137817133 steps 1.66), 602537574 deq 88%
c redc: 3624 clauses 24%, 15366 tried 2%, 72 sat 0%
c redc: 9428 lits 6%, 154571 tried 0%, 72 sat 0%
c redc: 404 times jump level reduced, 67.2 levels on average
c reds: 9 count, 76664.7 conflicts per reduce
c reds: 0 memlim 0%, 9 arith 100%
c reds: 243079 collected 89%, 29150 retired 11%
c rmbd: 57667 removed, 15975 red 28%
c rsts: 11514 restarts 92%, 1050 skipped 8%
c rsts: 1050 saturating 100%, 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: 26 count, 24 confs 92%, 0 vars 0%
c simp: 1 its 4%, 1 bin 4%, 0 trns 0%
c subl: 692646 count (933862 tried 1.3), 292740 sub out of 685409 (42.7%)
c swps: 20 count, 22 rounds, 21604 queries (982.0/round)
c swps: 20237 sat calls, 242 unsat (0.4% success rate)
c swps: 232545 decisions 11.5, 7397 conflicts 0.4
c swps; 330.0 avg class size, 100.5 avg environment size
c swps: 1 failed, 3310 impls, 1552 equivs
c swp0: 7193 type 0 queries, 3262 unsat (45.3%), 6775 sat (94.2%)
c swp1: 14411 type 1 queries, 7760 unsat (53.8%), 13277 sat (92.1%)
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: 18017729 calls to obtain time
c tops: 104297 fixed 40%, 375 its, 1839.95 confs/it
c trds: 22 transitive reductions, 7313 removed, 58 failed
c trds: 37064 nodes, 116253 edges, 44025800 steps
c trim: 6012584 words, 22.9 MB
c trnr: 21 count, 34 bin, 6869 trn, 187354017 steps
c unhd: 26 count, 57 rounds, 156653779 steps
c unhd: 1602 non-trivial sccs of average size 2.1
c unhd: 172 units, 171 bin, 1 trn, 0 lrg
c unhd: 11980 failed, 11901 stamp, 0 lits, 43 bin, 18 trn, 0 lrg
c unhd: 1518979 tauts, 27288 bin 2%, 16463 trn 1%, 635 lrg 0%
c unhd: 1518979 tauts, 1474593 stamp 97%, 1417928 red 93%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 7365928 str, 171 bin 0%, 4163 trn 0%, 7361594 lrg 100%, 7343279 red 100%
c vars: 35017 remaining 14% and 224241 removed 86% out of 259258
c vars: 104297 fixed 40%, 109501 eliminated 42%, 10443 equivalent 4%
c vsts: 18835288194 visits, 91% srch, 9% simp, 0% lkhd
c vsts: 7.5 search visits per propagation, 24712.1 per conflict
c wchs: 1750293149 pushed, 82037153 enlarged, 315 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all         685496        243079         29150      64990859      12565717        335225
c 
c  0 0         16512   2       857   0         0   0  25798497  40   3099466  25     44985  13     1.3
c  1 5          4754   1      1006   0       704   2   3676691   6    565212   4     13838   4     0.5
c  2 6         15103   2      5761   2      1268   4   5454308   8   1005585   8     29715   9     1.7
c  3 9         20801   3     10234   4      1277   4   5664937   9<  1155353   9     27480   8     3.0
c  4 14        21145   3     11740   5      1336   5   4615744   7   1056775   8<    25451   8     6.2
c  5 21        22140   3     13011   5      1494   5   4388650   7   1103815   9     25364   8     6.1
c  6 30        25682   4     16249   7      1476   5   4185721   6   1036605   8     22326   7<   11.2
c  7 41        28629   4     18742   8      1759   6   2972442   5    775568   6     21397   6     8.6
c  8 54        35621   5     23105  10<     2065   7   2617139   4    750970   6     23757   7     9.4
c  9 69        56729   8<    39143  16      2593   9<  2242179   3    704943   6     27319   8    24.9
c 10 86       126053  18     56691  23      4885  17   1786885   3    663528   5     32518  10    33.7
c 11 126      181410  26     24370  10      5625  19   1108593   2    428337   3     22298   7    27.7
c 12 230      120774  18     20645   8      4484  15    434748   1    201299   2     15819   5    32.4
c 13 534       10142   1      1525   1       184   1     44322   0     18259   0      2956   1    10.5
c 14 1526          1   0         0   0         0   0         3   0         2   0         2   0     0.0
c 15 5046          0   0         0   0         0   0         0   0         0   0         0   0     0.0
c 
c avg                  9.2           8.3           8.5           3.0           4.3           5.7
c std                  3.1           2.7           3.2           3.3           3.6           3.8
c 
c  119.574  12% bump
c   69.531   7% unhide
c   68.551   7% probe
c   64.801   6% cce
c   41.029   4% sweep
c   23.016   2% elim
c   10.871   1% rescore
c    5.000   1% decide
c    4.836   0% bca
c 
c   10.851 < 1% rest (below)
c 
c    3.613   0% block
c    2.514   0% transred
c    2.024   0% gauss
c    1.449   0% ternres
c    0.850   0% quatres
c    0.402   0% card
c    0.000   0% locs
c    0.000   0% queuesort
c ==================================
c    5.115   1% preprocessing     2%
c  293.622  29% inprocessing     98%
c ==================================
c  298.737  30% simplifying
c  700.505  70% search
c ==================================
c  999.246 100% all
c 
c        689982 conflicts,         690.5 confs/sec
c          2171 ternaries,         317.8 confs/ternary
c          2843 binaries,          242.7 confs/binary
c           375 iterations,       1840.0 confs/iteration
c 
c             9 reductions,          0.0 redus/sec,  76664.7 confs/reduction
c         11514 restarts,           11.5 rests/sec,     59.9 confs/restart
c       8313105 decisions,        8319.4 decis/sec,     12.0 decis/conflict
c    2464361292 propagations,  2466220.7 props/sec,    296.4 props/decision
c 
c 999.2 seconds, 174.1 MB
c
c CAUGHT SIGNAL 15 SIGTERM
c
c launch: done
