c launch: /data/cnf/sc2014/app/UR-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/UR-20-10p1.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/UR-20-10p1.cnf.bz2
c no embedded options
c found 'p cnf 259234 1387934' header
c read 259234 variables, 1387934 clauses, 3351923 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=1
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 246085 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] INC (--score=1)
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  246085  1373915         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 6535 at-most-one constraints of average size 5.7
c [card-1] no at-most-two constraint found
c [card-1] using previous limit 2000000 for elimination
c [card-1] 6535 out of 6535 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 196454 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 144 variables
c [simpleprobe-1] 15292 variables remain 8% (181018 retained 92%)
c [simpleprobe-1] removed 144 variables, found 17443 hbrs, 1 units
c [unhide-1] limit 66116 based on 1057870 irredundant clauses
c [unhide-1-1] 1 units, 672 failed, 9916 tauts, 0 hbrs, 9346 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 195745 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 62823 not tried 32% in round 1
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 74694 = 38% variables out of 195745 scheduled
c [elim-1] considered successful since not run to completion yet
c [phase-count-1] 889020 negative 99.3% of 895640 except 6620 0.7%
c [phase-count-1] 723947 positive 80.8% of 895640 except 171693 19.2%
c [phase-count-1] less non-negative clauses 6620 than limit 89500 (10.0%)
c [phase-count-1] non-pos/non-neg = 171693/6620 = 25.94 >= 2.00 = 200/100
c [lucky-phase-1] forcing lucky phase -1
c [phase-1] phase bias: 0 positive 0%, 121051 negative 100%
c [sort-queue-1] sorted 121051 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 121051 (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 81605 variables 40.3% (121051 remain 49%)
c [simplification-1] removed 478275 irredundant clauses 34.8% (895640 remain 65%)
c [simplification-1] maximum reduction of 40% = max (40%, 35%)
c [simplification-1] large reduction 40% >= 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.2  121050   895640        15      12      1 12549    0     5   59   1%      0    5    1    0 24855%
c i    5.2  120891   895640        34      26      3 12551    0     5   59   2%      0    5    2    0 24038%
c i    5.3  120775   895640        38      27      4 12552    0     6   59   2%      0    6    2    0 23742%
c i    5.3  120109   895640       114      84     15 12557    0     7   59   3%      0    7    3    0 19865%
c i    5.3  120099   895640       115      84     15 12557    0     7   59   3%      0    7    3    0 19788%
c i    5.3  119395   895640       116      84     15 12557    0     7   59   3%      0    7    3    0 19711%
c i    5.5  119378   895640       192     142     20 12568    1    12   59   4%      0   12    6    0 18100%
c i    5.5  119150   895640       194     142     21 12568    1    12   59   4%      0   12    6    0 17966%
c i    5.8  119136   895640       299     221     32 12578    1    19   60   5%      0   19   10    0 16946%
c i    5.8  118905   895640       305     226     32 12578    1    20   60   5%      0   20   10    0 16655%
c 
c [simplification-2] limit of 10 iterations hit after 10 iterations
c [decomp-3] removed 2344 variables
c [simpleprobe-2] 14567 schedulable variables 12%
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [simpleprobe-2] 15239 variables remain 13% (103468 retained 87%)
c [simpleprobe-2] removed 0 variables, found 1647 hbrs, 0 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 32603 literals 14%
c [treelook-1] scheduling used 324306 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 399334 steps
c [treelook-1] 32601 literals remain 14%
c [treelook-1] 32418 variables remain to probed next time 27%
c [treelook-1] removed 0 variables, found 3271 hbrs
c [basicprobe-1] limit 7040080 based on 880010 irredundant clauses
c [basicprobe-1-0] 41554 probes remain 37% after last round
c [basicprobe-1-0] 33 units = 33 failed (100%) + 0 lifted (0%)
c [basicprobe-1-0] removed 6745 variables, found 27939 hbrs
c [unhide-2] limit 55000 based on 880010 irredundant clauses
c [unhide-2-2] 4 units, 1893 failed, 9847 tauts, 0 hbrs, 1537 literals
c [elim-2] 59347 variables 54% will be scheduled this time
c [elim-2] scheduled 59347 variables 54%
c [elim-2] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-2] rescheduling of touched variables disabled
c [elim-2] incomplete 24063 not tried 22% in round 1
c [elim-2] transition to [ all 0 rem 1 ] state
c [elim-2] eliminated 130 = 0% variables out of 59347 scheduled
c [elim-2] considered successful since not run to completion yet
c [phase-count-2] 794935 negative 99.2% of 801555 except 6620 0.8%
c [phase-count-2] 646301 positive 80.6% of 801555 except 155254 19.4%
c [phase-count-2] less non-negative clauses 6620 than limit 80100 (10.0%)
c [phase-count-2] non-pos/non-neg = 155254/6620 = 23.45 >= 2.00 = 200/100
c [lucky-phase-2] forcing lucky phase -1
c [phase-2] phase bias: 0 positive 0%, 16345 negative 100%
c [sort-queue-2] sorted 100164 enqueued variables after 305 conflicts
c [score-dist-2] active 10156 (9%), one 0 (0%), zero 100164 (91%)
c [score-dist-2] max exp 506, different 6 (1%)
c [score-dist-2] median active exp 503, avg 503.2
c [simplification-2] removed 8450 variables 7.1% (110320 remain 45%)
c [simplification-2] removed 94085 irredundant clauses 10.5% (801555 remain 58%)
c [simplification-2] maximum reduction of 11% = max (7%, 11%)
c [simplification-2] forced so keeping old conflict interval 0
c [simplification-2] conflict limit remains at 1028 (hard 11000)
c [simplification-2] new iteration interval 100
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i    9.7  110319   801555       595     435     58 30952    2    41   54   4%      1   41   10    0 9229%
c i    9.8  109815   801555       597     436     58 30952    2    41   54   4%      1   41   10    0 9234%
c i    9.9  109502   801555       636     468     62 30954    2    46   54   4%      1   45   13    0 10123%
c 
c [simplification-3] limit 1033 conflicts (hard 11000) hit after 1033 conflicts
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 3743 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] 3743 out of 3743 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [decomp-6] removed 1065 variables
c [unhide-3] limit 74943 with penalty 1 = 0 + 1
c [unhide-3-3] 4 units, 750 failed, 17053 tauts, 0 hbrs, 2968 literals
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 108465 variables 100%
c [elim-3] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-3] rescheduling of touched variables disabled
c [elim-3] incomplete 31941 not tried 29% in round 1
c [elim-3] transition to [ all 1 rem 1 ] state
c [elim-3] eliminated 1588 = 1% variables out of 108465 scheduled
c [elim-3] considered successful since not run to completion yet
c [phase-count-3] 763014 negative 99.1% of 769572 except 6558 0.9%
c [phase-count-3] 619872 positive 80.5% of 769572 except 149700 19.5%
c [phase-count-3] less non-negative clauses 6558 than limit 76900 (10.0%)
c [phase-count-3] non-pos/non-neg = 149700/6558 = 22.83 >= 2.00 = 200/100
c [lucky-phase-3] forcing lucky phase -1
c [phase-3] phase bias: 0 positive 0%, 5056 negative 100%
c [sort-queue-3] sorted 77842 enqueued variables after 1033 conflicts
c [score-dist-3] active 29035 (27%), one 0 (0%), zero 77842 (73%)
c [score-dist-3] max exp 508, different 8 (2%)
c [score-dist-3] median active exp 504, avg 503.7
c [simplification-3] removed 2625 variables 2.4% (106877 remain 43%)
c [simplification-3] removed 31983 irredundant clauses 4.0% (769572 remain 56%)
c [simplification-3] maximum reduction of 4% = max (2%, 4%)
c [simplification-3] geometric conflict interval increment 4000 = 20000 / 5
c [simplification-3] new conflict interval 4000
c [simplification-3] penalized conflict interval 4000 = 1 * 4000
c [simplification-3] hard conflict limit 15033 (soft 5033 + delta 10000)
c [simplification-3] new conflict limit 5033 (hard 15033)
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   13.6  106876   769572      1133     816     84 28333    6   118   53   5%      2  117   33    0 8041%
c i   13.9  106371   769572      1348     991     96 28344   10   131   54   8%      2  130   68    1 9442%
c i   14.2  106219   769572      1481    1054     98 28347   17   138   54  13%      2  136  132    1 11237%
c i   14.2  106212   769572      1485    1055     98 28349   17   138   54  13%      2  136  130    1 11073%
c i   14.2  106207   769572      1486    1055     98 28349   17   138   54  13%      2  136  129    1 11030%
c i   14.2  106196   769572      1487    1055     98 28349   17   138   54  13%      2  136  129    1 10987%
c i   14.2  106188   769572      1488    1055     98 28349   17   138   54  13%      2  136  128    1 10944%
c i   14.7  106185   769572      1717    1246    111 28367   17   162   54  11%      2  160   59    1 4903%
c i   14.9  105765   769572      1771    1293    113 28368   17   171   54  10%      2  168   54    1 4345%
c i   15.8  105660   769572      2120    1606    119 28379   24   221   54  11%      2  218   73    2 4192%
c i   16.5  105484   769572      2383    1826    128 28394   25   241   55  10%      2  237   51    2 2699%
c i   16.8  105419   769572      2488    1908    132 28397   25   248   55  10%      2  244   54    2 2735%
c i   17.0  105418   769572      2544    1946    134 28398   28   251   55  11%      2  247   86    2 3994%
c i   17.2  105413   769572      2604    1985    134 28402   31   254   55  12%      2  249  112    2 4791%
c i   17.5  105400   769572      2693    2049    134 28403   36   260   55  14%      2  255  163    3 5991%
c i   19.4  105395   769572      3431    2697    145 28410   70   354   56  20%      4  346  319    5 5973%
c 
c [simplification-4] limit of 187 binary hit after 187 binaries
c [decomp-7] removed 1504 variables
c [treelook-2] limit 190290 based on 761162 irredundant clauses
c [treelook-2] scheduled 24110 literals 11%
c [treelook-2] scheduling used 262447 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 190290 based on 761162 irredundant clauses
c [treelook-2] used 389837 steps
c [treelook-2] 24105 literals remain 11%
c [treelook-2] 17512 variables remain to probed next time 17%
c [treelook-2] removed 0 variables, found 2356 hbrs
c [unhide-4] limit 308832 with penalty 1 = 0 + 1
c [unhide-4-4] 4 units, 710 failed, 4430 tauts, 0 hbrs, 23146 literals
c [elim-4] 23644 variables 23% will be scheduled this time
c [elim-4] scheduled 23644 variables 23%
c [elim-4] boosting limit by 20
c [elim-4] limit of 1235331920 steps penalty 0 = 0 + 0
c [elim-4] rescheduling of touched variables disabled
c [elim-4-1] no variable eliminated in round 1 in 48503528 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 23644 scheduled
c [phase-count-4] 741309 negative 99.1% of 747867 except 6558 0.9%
c [phase-count-4] 602958 positive 80.6% of 747867 except 144909 19.4%
c [phase-count-4] less non-negative clauses 6558 than limit 74700 (10.0%)
c [phase-count-4] non-pos/non-neg = 144909/6558 = 22.10 >= 2.00 = 200/100
c [lucky-phase-4] forcing lucky phase -1
c [phase-4] phase bias: 0 positive 0%, 3021 negative 100%
c [sort-queue-4] sorted 62551 enqueued variables after 4004 conflicts
c [score-dist-4] active 41583 (40%), one 0 (0%), zero 62551 (60%)
c [score-dist-4] max exp 511, different 11 (2%)
c [score-dist-4] median active exp 505, avg 505.0
c [simplification-4] removed 1255 variables 1.2% (104134 remain 42%)
c [simplification-4] removed 21705 irredundant clauses 2.8% (747867 remain 54%)
c [simplification-4] maximum reduction of 3% = max (1%, 3%)
c [simplification-4] forced so keeping old conflict interval 4000
c [simplification-4] conflict limit remains at 5065 (hard 15033)
c [simplification-4] new binary interval 1000
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   24.1  104133   747867      4239    3319    151 25707  113   427   58  26%      6  414  330    9 3646%
c i   24.4  104126   747867      4344    3382    154 25707  122   436   58  28%      5  422  390   10 3972%
c i   24.4  104125   747867      4345    3382    154 25707  122   436   58  28%      5  422  388   10 3957%
c i   25.9  104124   747867      4785    3593    164 25717  165   467   60  35%      5  450  512   13 3826%
c 
c [simplification-5] limit 5075 conflicts (hard 15033) hit after 5075 conflicts
c [quatres-1] found 42706 quaternary clauses 38% in total
c [ternres-1] boosting ternary resolution limit by 5
c [ternres-1] limit 20074115 with penalty 0 = 0 + 0
c [ternres-1] all 104117 free variables schedulable
c [ternres-1] 5 ternary resolvents (0 bin, 5 trn)
c [ternres-1] fully completed ternary resolution
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 20 xors of average arity 3.0
c [gauss-1] connected 60 occurrences of 60 variables (average 1.0)
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 3 variables
c [basicprobe-2] limit 20074115 penalty 0 = 0 + 0
c [basicprobe-2-0] 36595 probes remain 36% after last round
c [basicprobe-2-0] 95 units = 95 failed (100%) + 0 lifted (0%)
c [basicprobe-2-0] removed 3415 variables, found 50272 hbrs
c [bate-1] eliminated 58 asymmetric tautologies during probing
c [unhide-5] limit 401482 with penalty 1 = 0 + 1
c [unhide-5-5] 8 units, 327 failed, 14045 tauts, 0 hbrs, 35612 literals
c [transred-1] limit 2000000 with penalty 0 = 0 + 0
c [transred-1] removed 179 transitive binary clauses
c [transred-1] found 8 units
c [block-1] scheduling all variables this time
c [block-1] scheduled 100236 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 10575 blocked clauses
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 3 clauses out of 333 (1%) of length 10
c [cce-1-1] eliminated 103 clauses out of 2195 (5%) of length 9
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 106 large clauses in 30000002 steps
c [cce-1-1] allowing another 15000001 steps for small clauses
c [cce-1-1] scheduling 347062 clauses = 330154 binary + 16908 ternary
c [cce-1-1] tried to eliminate 409 small clauses 0%
c [cce-1-1] eliminated 132 binary clauses 0%
c [cce-1-1] eliminated 10 ternary clauses 0%
c [cce-1-1] eliminated 142 small clauses 0%
c [cce-1-1] eliminated 142 small clauses in 30000001 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 248 covered clauses in round 1
c [cce-1] eliminated 248 covered clauses in TOTAL during 1 rounds
c [cce-1] 248 < 1/100 * 701874 = 7018 considered unsuccessful
c [bca-1] limit of 10000000 steps and 1403752 added (scaled 2)
c [bca-1] 182482 out of 200474 literals actually usable 91%
c [bca-1] added 230 blocked clauses in 547939 steps
c [sweep-1] limit 1403252 based on 701626 irredundant clauses
c [sweep-1-1] 4594 pos 4.6% + 95642 neg 95.4% = 100236 sched 100.0% ret 0
c [sweep-1-1] 1598388 steps 28 queries 28857.50 avg class size
c [sweep-1-1] 175 decisions 22 SAT calls 35.45 avg env size
c [sweep-1-1] 100129 variables remain 100% (106 retained 0%)
c [decomp-10] removed 280 variables
c [sweep-1-1] removed 280 vars (0 failed, 5 eqs, 10 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 280 vars in TOTAL (1 rounds, 27 queries)
c [phase-count-5] 694530 negative 99.1% of 701068 except 6538 0.9%
c [phase-count-5] 575180 positive 82.0% of 701068 except 125888 18.0%
c [phase-count-5] less non-negative clauses 6538 than limit 70100 (10.0%)
c [phase-count-5] non-pos/non-neg = 125888/6538 = 19.25 >= 2.00 = 200/100
c [lucky-phase-5] forcing lucky phase -1
c [phase-5] phase bias: 0 positive 0%, 2909 negative 100%
c [sort-queue-5] sorted 58782 enqueued variables after 5075 conflicts
c [score-dist-5] active 41174 (41%), one 0 (0%), zero 58782 (59%)
c [score-dist-5] max exp 512, different 12 (2%)
c [score-dist-5] median active exp 505, avg 505.5
c [simplification-5] removed 4161 variables 4.0% (99956 remain 41%)
c [simplification-5] removed 46799 irredundant clauses 6.3% (701068 remain 51%)
c [simplification-5] maximum reduction of 6% = max (4%, 6%)
c [simplification-5] large reduction 6% >= 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 17075 (soft 7075 + delta 10000)
c [simplification-5] new conflict limit 7075 (hard 17075)
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   32.5   99955   701068      5294    3798    240 81618  201   494   59  41%      4  473  473   17 2793%
c i   33.1   99951   701068      5612    3997    243 81625  217   509   59  43%      4  487  429   19 2271%
c 
c [simplification-6] limit 7075 conflicts (hard 17075) hit after 7075 conflicts
c [ternres-2] limit 5379081 with penalty 0 = 0 + 0
c [ternres-2] all 99951 free variables schedulable
c [ternres-2] 1 ternary resolvents (0 bin, 1 trn)
c [ternres-2] 66517 variables remain 67% (33434 retained 33%)
c [card-3] limit 672385 penalty 2 = 2 + 0
c [card-3] found 2414 at-most-one constraints of average size 4.3
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 672385 for elimination
c [card-3] 2414 out of 2414 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [decomp-11] removed 7 variables
c [unhide-6] limit 537908 with penalty 1 = 0 + 1
c [unhide-6-6] 1 units, 739 failed, 9331 tauts, 0 hbrs, 21001 literals
c [transred-2] limit 2000000 with penalty 0 = 0 + 0
c [transred-2] removed 164 transitive binary clauses
c [transred-2] found 5 units
c [block-2] scheduling all variables this time
c [block-2] scheduled 99272 variables 100%
c [block-2] limit of 53790813 steps penalty 0 = 0 + 0
c [block-2] fully completed
c [block-2] transition to [ all 0 rem 0 ] state
c [block-2] eliminated 644 blocked clauses
c [block-2] 644 < 1/100 * 700911 = 7009 considered unsuccessful
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 99272 variables 100%
c [elim-5] limit of 53790813 steps penalty 1 = 1 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5] incomplete 5302 not tried 5% in round 1
c [elim-5] transition to [ all 1 rem 1 ] state
c [elim-5] eliminated 2040 = 2% variables out of 99272 scheduled
c [bca-2] limit of 10000000 steps and 1380937 added (scaled 2)
c [bca-2] 178522 out of 194466 literals actually usable 92%
c [bca-2] added 150 blocked clauses in 546256 steps
c [sweep-2] limit 1613724 penalty 0 = 0 + 0
c [sweep-2-1] 4538 pos 4.7% + 92603 neg 95.3% = 97141 sched 99.9% ret 91
c [sweep-2-1] 1733776 steps 26 queries 22619.19 avg class size
c [sweep-2-1] 259 decisions 20 SAT calls 102.05 avg env size
c [sweep-2-1] 97002 variables remain 100% (193 retained 0%)
c [decomp-12] removed 59 variables
c [sweep-2-1] removed 59 vars (0 failed, 6 eqs, 9 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 59 vars in TOTAL (1 rounds, 25 queries)
c [phase-count-6] 683440 negative 99.1% of 689858 except 6418 0.9%
c [phase-count-6] 564186 positive 81.8% of 689858 except 125672 18.2%
c [phase-count-6] less non-negative clauses 6418 than limit 68900 (10.0%)
c [phase-count-6] non-pos/non-neg = 125672/6418 = 19.58 >= 2.00 = 200/100
c [lucky-phase-6] forcing lucky phase -1
c [phase-6] phase bias: 0 positive 0%, 2596 negative 100%
c [sort-queue-6] sorted 56593 enqueued variables after 7075 conflicts
c [score-dist-6] active 40580 (42%), one 0 (0%), zero 56593 (58%)
c [score-dist-6] max exp 513, different 13 (3%)
c [score-dist-6] median active exp 506, avg 506.0
c [simplification-6] removed 2778 variables 2.8% (97173 remain 39%)
c [simplification-6] removed 11210 irredundant clauses 1.6% (689858 remain 50%)
c [simplification-6] maximum reduction of 3% = max (3%, 2%)
c [simplification-6] geometric conflict interval increment 5000 = 20000 / 4
c [simplification-6] new conflict interval 9000
c [simplification-6] penalized conflict interval 9000 = 1 * 9000
c [simplification-6] hard conflict limit 26075 (soft 16075 + delta 10000)
c [simplification-6] new conflict limit 16075 (hard 26075)
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   42.9   97172   689858      7725    3316    261 70605  318   569   55  56%     19  530  311   33  931%
c i   43.1   97058   689858      7796    3367    261 70606  319   571   55  56%     18  531  331   34  980%
c i   49.0   97048   689858     10020    4511    311 70620  354   612   63  58%     22  555  431   46  941%
c i   50.3   97044   689858     10560    4980    317 70625  318   660   64  48%     14  597  103   46  224%
c i   56.3   96914   689858     12861    6769    370 70649  309   782   68  39%     22  696  332   54  609%
c 
c [simplification-7] limit 16075 conflicts (hard 26075) hit after 16075 conflicts
c [quatres-2] found 48156 quaternary clauses 44% in total
c [quatres-2-2] added 1 single-self-subsuming ternary resolvents
c [quatres-2-2] added 1 quaternary resolvents
c [ternres-3] limit 12273695 with penalty 0 = 0 + 0
c [ternres-3] 64490 schedulable variables 66%
c [ternres-3] 15 ternary resolvents (0 bin, 15 trn)
c [ternres-3] fully completed ternary resolution
c [gauss-2] limit 1227369 penalty 1 = 1 + 0
c [gauss-2] extracted 13 xors of average arity 3.0
c [gauss-2] connected 39 occurrences of 36 variables (average 1.1)
c [gauss-2] limit 1227369 penalty 1 = 1 + 0
c [gauss-2] fully completed
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-13] removed 31 variables
c [simpleprobe-3] 13047 schedulable variables 13%
c [simpleprobe-3] limit 24547391 penalty 1 = 1 + 0
c [decomp-14] removed 47 variables
c [simpleprobe-3] 3730 variables remain 4% (93103 retained 96%)
c [simpleprobe-3] removed 47 variables, found 27529 hbrs, 31 units
c [unhide-7] limit 1227369 with penalty 1 = 0 + 1
c [unhide-7-7] 4 units, 132 failed, 13710 tauts, 0 hbrs, 121108 literals
c [transred-3] limit 2000000 with penalty 0 = 0 + 0
c [transred-3] removed 194 transitive binary clauses
c [transred-3] found 6 units
c [cce-2] limit of 30684239 steps penalty 1 = 1 + 0
c [cce-2-1] eliminated 45 clauses out of 2068 (2%) of length 9
c [cce-2-1] eliminated 39 clauses out of 517 (8%) of length 8
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] eliminated 84 large clauses in 30684245 steps
c [cce-2-1] allowing another 15342122 steps for small clauses
c [cce-2-1] scheduling 552329 clauses = 315216 binary + 237113 ternary
c [cce-2-1] tried to eliminate 433 small clauses 0%
c [cce-2-1] eliminated 85 binary clauses 0%
c [cce-2-1] eliminated 26 ternary clauses 0%
c [cce-2-1] eliminated 111 small clauses 0%
c [cce-2-1] eliminated 1938 small clauses in 30684247 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 2022 covered clauses in round 1
c [cce-2] eliminated 2022 covered clauses in TOTAL during 1 rounds
c [cce-2] 2022 < 1/100 * 679284 = 6792 considered unsuccessful
c [elim-6] 5301 variables 5% will be scheduled this time
c [elim-6] scheduled 5301 variables 5%
c [elim-6] limit of 245473915 steps penalty 0 = 0 + 0
c [elim-6] rescheduling of touched variables disabled
c [elim-6-1] no variable eliminated in round 1 in 14310215 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 5301 scheduled
c [bca-3] limit of 10000000 steps and 1354756 added (scaled 2)
c [bca-3] 171597 out of 193300 literals actually usable 89%
c [bca-3] added 57 blocked clauses in 512253 steps
c [sweep-3] limit 3682108 penalty 0 = 0 + 0
c [sweep-3-1] 4843 pos 5.0% + 91626 neg 95.0% = 96469 sched 99.8% ret 180
c [sweep-3-1] 3699118 steps 25 queries 21646.84 avg class size
c [sweep-3-1] 390 decisions 20 SAT calls 93.45 avg env size
c [sweep-3-1] 95949 variables remain 100% (404 retained 0%)
c [decomp-15] removed 307 variables
c [sweep-3-1] removed 307 vars (0 failed, 4 eqs, 11 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 307 vars in TOTAL (1 rounds, 24 queries)
c [phase-count-7] 669279 negative 99.1% of 675697 except 6418 0.9%
c [phase-count-7] 553465 positive 81.9% of 675697 except 122232 18.1%
c [phase-count-7] less non-negative clauses 6418 than limit 67500 (10.0%)
c [phase-count-7] non-pos/non-neg = 122232/6418 = 19.05 >= 2.00 = 200/100
c [lucky-phase-7] forcing lucky phase -1
c [phase-7] phase bias: 0 positive 0%, 1683 negative 100%
c [sort-queue-7] sorted 49584 enqueued variables after 16075 conflicts
c [score-dist-7] active 46758 (49%), one 0 (0%), zero 49584 (51%)
c [score-dist-7] max exp 515, different 15 (3%)
c [score-dist-7] median active exp 507, avg 507.1
c [simplification-7] removed 569 variables 0.6% (96342 remain 39%)
c [simplification-7] removed 14161 irredundant clauses 2.1% (675697 remain 49%)
c [simplification-7] maximum reduction of 2% = max (1%, 2%)
c [simplification-7] geometric conflict interval increment 6666 = 20000 / 3
c [simplification-7] new conflict interval 15666
c [simplification-7] penalized conflict interval 15666 = 1 * 15666
c [simplification-7] hard conflict limit 41741 (soft 31741 + delta 10000)
c [simplification-7] new conflict limit 31741 (hard 41741)
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.9   96341   675697     27094   11611    429 94628  599   762  114  79%    185  541  640  164  391%
c i  110.2   96336   675697     27741   11775    429 94641  609   764  114  80%     90  539  568  169  336%
c 
c [simplification-8] limit 31741 conflicts (hard 41741) hit after 31741 conflicts
c [quatres-3] found 46178 quaternary clauses 43% in total
c [ternres-4] limit 25358486 with penalty 0 = 0 + 0
c [ternres-4] all 96330 free variables schedulable
c [ternres-4] 0 ternary resolvents (0 bin, 0 trn)
c [ternres-4] fully completed ternary resolution
c [decomp-16] removed 21 variables
c [unhide-8] limit 1267924 with penalty 2 = 0 + 2
c [unhide-8-8] 7 units, 393 failed, 10775 tauts, 0 hbrs, 112019 literals
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 187 transitive binary clauses
c [transred-4] found 6 units
c [block-3] scheduling all variables this time
c [block-3] scheduled 95966 variables 100%
c [block-3] limit of 126792434 steps penalty 1 = 1 + 0
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 538 blocked clauses
c [block-3] 538 < 1/100 * 675479 = 6754 considered unsuccessful
c [bca-4] limit of 10000000 steps and 1342946 added (scaled 2)
c [bca-4] 169041 out of 191934 literals actually usable 88%
c [bca-4] added 124 blocked clauses in 506946 steps
c [sweep-4] limit 7607546 penalty 0 = 0 + 0
c [sweep-4-1] 4644 pos 4.9% + 90938 neg 95.1% = 95582 sched 99.6% ret 384
c [sweep-4-1] 7865298 steps 54 queries 12209.19 avg class size
c [sweep-4-1] 467 decisions 45 SAT calls 76.33 avg env size
c [sweep-4-1] 94170 variables remain 98% (1684 retained 2%)
c [decomp-17] removed 121 variables
c [sweep-4-1] removed 121 vars (0 failed, 11 eqs, 16 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 121 vars in TOTAL (1 rounds, 53 queries)
c [phase-count-8] 663784 negative 99.0% of 670195 except 6411 1.0%
c [phase-count-8] 548131 positive 81.8% of 670195 except 122064 18.2%
c [phase-count-8] less non-negative clauses 6411 than limit 67000 (10.0%)
c [phase-count-8] non-pos/non-neg = 122064/6411 = 19.04 >= 2.00 = 200/100
c [lucky-phase-8] forcing lucky phase -1
c [phase-8] phase bias: 0 positive 0%, 1623 negative 100%
c [sort-queue-8] sorted 47269 enqueued variables after 31741 conflicts
c [score-dist-8] active 48576 (51%), one 0 (0%), zero 47269 (49%)
c [score-dist-8] max exp 516, different 16 (3%)
c [score-dist-8] median active exp 508, avg 508.0
c [simplification-8] removed 485 variables 0.5% (95845 remain 39%)
c [simplification-8] removed 5502 irredundant clauses 0.8% (670195 remain 49%)
c [simplification-8] maximum reduction of 1% = max (1%, 1%)
c [simplification-8] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-8] new conflict interval 25666
c [simplification-8] penalized conflict interval 25666 = 1 * 25666
c [simplification-8] hard conflict limit 70240 (soft 57407 + delta 12833)
c [simplification-8] new conflict limit 57407 (hard 70240)
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  132.8   95844   670195     33143   13155    437 88842  651   761   95  86%     44  493  623  208  299%
c i  133.4   95840   670195     33381   13265    438 88843  645   764   95  84%     30  494  576  210  275%
c i  139.1   95831   670195     36887   13703    438 88850  692   776  111  89%     16  480  639  237  270%
c i  139.2   95830   670195     36888   13703    438 88850  691   776  111  89%     16  480  637  237  269%
c i  139.2   95829   670195     36893   13707    438 88850  691   776  111  89%     16  480  628  237  265%
c i  139.2   95828   670195     36895   13708    438 88850  690   776  111  89%     16  480  624  237  264%
c i  139.2   95827   670195     36896   13708    438 88850  690   775  111  89%     16  480  621  237  263%
c i  139.2   95826   670195     36897   13708    438 88850  690   775  111  89%     16  480  619  237  262%
c i  139.2   95825   670195     36898   13708    438 88850  690   775  111  89%     15  479  617  237  261%
c i  139.3   95824   670195     36899   13708    438 88850  690   775  111  89%     15  479  614  237  260%
c i  139.3   95823   670195     36906   13714    438 88850  689   775  111  89%     15  479  603  237  255%
c i  139.3   95822   670195     36908   13715    438 88850  689   775  111  89%     15  479  599  237  253%
c i  139.3   95821   670195     36911   13717    438 88850  688   775  111  89%     15  479  593  237  251%
c i  139.3   95820   670195     36912   13717    438 88850  688   775  111  89%     15  479  591  237  250%
c i  142.9   95819   670195     38227   14513    443 88852  668   792  111  84%     -5  487  584  244  239%
c i  153.5   95812   670195     41073   15844    460 88855  650   779  111  83%      6  453  613  260  235%
c i  153.5   95807   670195     41074   15844    460 88855  650   779  111  83%      6  453  611  260  234%
c i  153.5   95801   670195     41085   15852    460 88855  649   779  111  83%      5  452  598  260  230%
c i  159.7   95795   670195     42769   16708    464 88858  617   766  142  80%     -6  428  570  268  213%
c i  159.7   95742   670195     42770   16708    464 88858  616   766  142  80%     -6  428  568  268  212%
c i  159.8   95737   670195     42779   16716    464 88858  615   766  142  80%     -6  428  550  268  206%
c i  161.7   95729   670195     43546   17157    468 88864  587   770  142  76%    -12  428  416  270  154%
c i  176.1   95728   670195     48056   18579    472 88877  642   766  152  84%     30  394  548  297  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  178.8   95633   670195     49014   19012    474 88880  612   757  152  81%      2  380  491  300  164%
c 
c [simplification-9] limit 57504 conflicts (hard 70240) hit after 57508 conflicts
c [decomp-18] removed 248 variables
c [unhide-9] limit 2275657 with penalty 2 = 0 + 2
c [unhide-9-9] 2 units, 92 failed, 7155 tauts, 0 hbrs, 390144 literals
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 229 transitive binary clauses
c [transred-5] found 3 units
c [elim-7] scheduling all variables this time
c [elim-7] scheduled 95459 variables 100%
c [elim-7] limit of 400000000 steps penalty 1 = 1 + 0
c [elim-7] rescheduling of touched variables disabled
c [elim-7-1] eliminated 1388 variables 1% in round 1 in 65222313 steps
c [elim-7-1] backward subsumption/strengthening limit 65222300
c [elim-7-1-1] backward checking 5127 touched variables 5%
c [elim-7-1-1] fully completed backward checking in 1 rounds
c [elim-7-1] subsumed 0 and strengthened 94 clauses in 2297362 steps
c [elim-7-1] rescheduled 194 variables 0% by backward subsumption
c [elim-7-2] eliminated 30 variables 0% in round 2 in 287861 steps
c [elim-7-2] backward subsumption/strengthening limit 287800
c [elim-7-2-1] backward checking 206 touched variables 0%
c [elim-7-2-1] fully completed backward checking in 1 rounds
c [elim-7-2] subsumed 0 and strengthened 0 clauses in 207672 steps
c [elim-7] fully completed in 2 rounds
c [elim-7] transition to [ all 0 rem 0 ] state
c [elim-7] eliminated 1418 = 1% variables out of 95459 scheduled
c [bca-5] limit of 10000000 steps and 1318198 added (scaled 2)
c [bca-5] 166965 out of 188084 literals actually usable 89%
c [bca-5] added 78 blocked clauses in 501396 steps
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 136539430 penalty 0 = 0 + 0
c [sweep-5-1] 4319 pos 4.7% + 88166 neg 95.3% = 92485 sched 98.3% ret 1556
c [sweep-5-1] 136544969 steps 1714 queries 669.65 avg class size
c [sweep-5-1] 13336 decisions 1432 SAT calls 79.04 avg env size
c [sweep-5-1] 48222 variables remain 52% (44106 retained 48%)
c [decomp-19] removed 2474 variables
c [sweep-5-1] removed 2474 vars (0 failed, 320 eqs, 536 impls)
c [sweep-5] considered successful since not run to completion yet
c [sweep-5] removed 2474 vars in TOTAL (1 rounds, 1713 queries)
c [phase-count-9] 639366 negative 99.1% of 645477 except 6111 0.9%
c [phase-count-9] 528916 positive 81.9% of 645477 except 116561 18.1%
c [phase-count-9] less non-negative clauses 6111 than limit 64500 (10.0%)
c [phase-count-9] non-pos/non-neg = 116561/6111 = 19.07 >= 2.00 = 200/100
c [lucky-phase-9] forcing lucky phase -1
c [phase-9] phase bias: 0 positive 0%, 747 negative 100%
c [sort-queue-9] sorted 39962 enqueued variables after 57508 conflicts
c [score-dist-9] active 51605 (56%), one 0 (0%), zero 39962 (44%)
c [score-dist-9] max exp 517, different 17 (3%)
c [score-dist-9] median active exp 508, avg 508.0
c [simplification-9] removed 4066 variables 4.3% (91567 remain 37%)
c [simplification-9] removed 24718 irredundant clauses 3.7% (645477 remain 47%)
c [simplification-9] maximum reduction of 4% = max (4%, 4%)
c [simplification-9] geometric conflict interval increment 5133 = 25666 / 5
c [simplification-9] new conflict interval 30799
c [simplification-9] penalized conflict interval 30799 = 1 * 30799
c [simplification-9] hard conflict limit 103706 (soft 88307 + delta 15399)
c [simplification-9] new conflict limit 88307 (hard 103706)
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  223.5   91566   645477     58447    9303    481 212800  564   714   71  79%    101  289  473  336  141%
c i  223.6   91565   645477     58448    9303    481 212800  564   714   71  79%    101  288  471  336  140%
c i  230.4   91564   645477     61596   10545    491 212812  529   707   82  75%      9  268  458  343  134%
c i  233.8   91559   645477     63251   11439    494 212816  519   732   82  71%    -10  286  369  347  106%
c i  239.2   91554   645477     65475   12358    498 212825  517   738   97  70%     -8  282  493  353  140%
c i  241.7   91547   645477     66579   12745    499 212828  538   740   97  73%    -16  280  550  357  154%
c i  244.1   91542   645477     67339   12956    507 212833  542   731   97  74%    -20  267  572  359  159%
c i  244.1   91540   645477     67341   12956    508 212833  542   731   97  74%    -20  267  567  359  158%
c i  252.3   91536   645477     70267   14263    528 212852  510   705  103  72%      2  231  534  364  147%
c i  252.3   91532   645477     70271   14265    528 212852  509   705  103  72%      2  231  528  364  145%
c i  252.3   91530   645477     70273   14265    528 212852  509   705  103  72%      2  231  526  364  144%
c i  252.3   91526   645477     70276   14265    530 212852  509   705  103  72%      1  230  520  364  143%
c i  253.8   91517   645477     70677   14362    531 212852  511   697  103  73%     -7  222  530  365  145%
c i  272.4   91516   645477     76517   15690    531 212858  566   658  127  86%     45  166  606  383  158%
c i  276.8   91510   645477     77855   15876    532 212859  575   653  127  88%     -1  157  594  387  153%
c i  290.3   91507   645477     82597   16564    536 212863  567   622  173  91%     28  116  562  400  141%
c 
c [simplification-10] limit 88332 conflicts (hard 103706) hit after 88333 conflicts
c [quatres-4] found 38866 quaternary clauses 40% in total
c [quatres-4-2] added 2 single-self-subsuming ternary resolvents
c [ternres-5] limit 33253172 with penalty 1 = 1 + 0
c [ternres-5] all 91507 free variables schedulable
c [ternres-5] 100 ternary resolvents (0 bin, 100 trn)
c [ternres-5] fully completed ternary resolution
c [card-4] limit 4156646 penalty 3 = 3 + 0
c [card-4] found 8987 at-most-one constraints of average size 3.9
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 4156646 for elimination
c [card-4] 8987 out of 8987 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [gauss-3] limit 3325317 penalty 2 = 2 + 0
c [gauss-3] extracted 67 xors of average arity 2.6
c [gauss-3] connected 177 occurrences of 120 variables (average 1.5)
c [gauss-3] limit 3325317 penalty 2 = 2 + 0
c [gauss-3] fully completed
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-20] removed 17 variables
c [treelook-3] limit 1662658 penalty 2 = 2 + 0 boost 1
c [treelook-3] scheduled 125975 literals 69%
c [treelook-3] scheduling used 1663437 steps
c [treelook-3] not fully scheduled
c [treelook-3] limit 1662658 penalty 2 = 2 + 0 boost 1
c [treelook-3] used 1703838 steps
c [treelook-3] 125945 literals remain 69%
c [treelook-3] 14195 variables remain to probed next time 16%
c [decomp-21] removed 3 variables
c [treelook-3] removed 6 variables, found 5380 hbrs
c [unhide-10] limit 3325317 with penalty 2 = 0 + 2
c [unhide-10-10] 20 units, 457 failed, 23260 tauts, 0 hbrs, 163784 literals
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 144 transitive binary clauses
c [transred-6] found 2 units
c [cce-3] limit of 83132931 steps penalty 2 = 2 + 0
c [cce-3-1] eliminated 1 clauses out of 1722 (0%) of length 9
c [cce-3-1] eliminated 7 clauses out of 554 (1%) of length 8
c [cce-3-1] eliminated 63 clauses out of 716 (9%) of length 7
c [cce-3-1] eliminated 3634 clauses out of 5809 (63%) of length 6
c [cce-3-1] eliminated 904 clauses out of 47804 (2%) of length 5
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 4609 large clauses in 83132937 steps
c [cce-3-1] allowing another 41566468 steps for small clauses
c [cce-3-1] scheduling 320976 clauses = 298453 binary + 22523 ternary
c [cce-3-1] tried to eliminate 1399 small clauses 0%
c [cce-3-1] eliminated 378 binary clauses 0%
c [cce-3-1] eliminated 49 ternary clauses 0%
c [cce-3-1] eliminated 427 small clauses 0%
c [cce-3-1] eliminated 5837 small clauses in 83132944 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 10446 covered clauses in round 1
c [cce-3] eliminated 10446 covered clauses in TOTAL during 1 rounds
c [elim-8] scheduling all variables this time
c [elim-8] scheduled 90884 variables 100%
c [elim-8] boosting limit by 20
c [elim-8] limit of 16000000000 steps penalty 0 = 0 + 0
c [elim-8] rescheduling of touched variables disabled
c [elim-8-1] eliminated 4201 variables 5% in round 1 in 64997517 steps
c [elim-8-1] backward subsumption/strengthening limit 64997500
c [elim-8-1-1] backward checking 11981 touched variables 13%
c [elim-8-1-1] fully completed backward checking in 1 rounds
c [elim-8-1] subsumed 0 and strengthened 343 clauses in 4477986 steps
c [elim-8-1] rescheduled 708 variables 1% by backward subsumption
c [elim-8-2] eliminated 111 variables 0% in round 2 in 1505653 steps
c [elim-8-2] backward subsumption/strengthening limit 1505600
c [elim-8-2-1] backward checking 775 touched variables 1%
c [elim-8-2-1] fully completed backward checking in 1 rounds
c [elim-8-2] subsumed 0 and strengthened 0 clauses in 489856 steps
c [elim-8] fully completed in 2 rounds
c [elim-8] transition to [ all 0 rem 0 ] state
c [elim-8] eliminated 4312 = 5% variables out of 90884 scheduled
c [bca-6] limit of 10000000 steps and 1241671 added (scaled 2)
c [bca-6] 157555 out of 173146 literals actually usable 91%
c [bca-6] added 908 blocked clauses in 477607 steps
c [sweep-6] limit 19951903 penalty 0 = 0 + 0
c [sweep-6-1] 3314 pos 7.2% + 42480 neg 92.8% = 45794 sched 52.9% ret 40778
c [sweep-6-1] 19992230 steps 297 queries 2352.38 avg class size
c [sweep-6-1] 2408 decisions 245 SAT calls 106.40 avg env size
c [sweep-6-1] 43512 variables remain 50% (42911 retained 50%)
c [decomp-22] removed 291 variables
c [sweep-6-1] removed 291 vars (0 failed, 55 eqs, 103 impls)
c [sweep-6] considered successful since not run to completion yet
c [sweep-6] removed 291 vars in TOTAL (1 rounds, 296 queries)
c [phase-count-10] 618082 negative 99.8% of 619437 except 1355 0.2%
c [phase-count-10] 504823 positive 81.5% of 619437 except 114614 18.5%
c [phase-count-10] less non-negative clauses 1355 than limit 61900 (10.0%)
c [phase-count-10] non-pos/non-neg = 114614/1355 = 84.59 >= 2.00 = 200/100
c [lucky-phase-10] forcing lucky phase -1
c [phase-10] phase bias: 0 positive 0%, 635 negative 100%
c [sort-queue-10] sorted 32818 enqueued variables after 88333 conflicts
c [score-dist-10] active 53463 (62%), one 0 (0%), zero 32818 (38%)
c [score-dist-10] max exp 518, different 18 (3%)
c [score-dist-10] median active exp 507, avg 508.0
c [simplification-10] removed 5226 variables 5.7% (86281 remain 35%)
c [simplification-10] removed 26040 irredundant clauses 4.0% (619437 remain 45%)
c [simplification-10] maximum reduction of 6% = max (6%, 4%)
c [simplification-10] large reduction 6% >= 5% limit
c [simplification-10] next conflict interval 2000 = 2000/1
c [simplification-10] penalized conflict interval 2000 = 1 * 2000
c [simplification-10] hard conflict limit 100333 (soft 90333 + delta 10000)
c [simplification-10] new conflict limit 90333 (hard 100333)
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  314.1   86280   619437     88516    5759    581 221819  531   588   57  90%     45   74  300  412   73%
c i  314.1   86279   619437     88520    5762    581 221819  530   588   57  90%     45   74  297  412   72%
c i  314.1   86278   619437     88521    5762    581 221819  530   588   57  90%     45   74  295  412   72%
c i  314.2   86277   619437     88602    5829    581 221819  523   590   57  89%     39   76  264  412   64%
c i  314.2   86274   619437     88605    5831    581 221819  523   590   57  89%     39   76  263  412   64%
c i  314.2   86270   619437     88607    5831    581 221819  523   590   57  89%     39   76  262  412   64%
c i  314.2   86266   619437     88609    5832    581 221819  523   590   57  89%     38   76  260  412   63%
c i  314.3   86263   619437     88666    5880    583 221820  517   593   57  87%     35   79  234  411   57%
c i  314.4   86262   619437     88700    5903    583 221820  516   594   57  87%     32   79  244  411   59%
c i  315.1   86254   619437     89093    6146    587 221820  502   605   58  83%     13   90  351  411   86%
c i  315.1   86245   619437     89109    6159    587 221821  500   607   58  82%     12   91  339  411   82%
c i  315.2   86231   619437     89169    6211    587 221821  496   612   58  81%     10   97  311  411   76%
c i  315.4   86230   619437     89290    6307    591 221828  489   622   58  79%      5  106  289  410   70%
c i  315.4   86227   619437     89329    6339    591 221830  487   624   58  78%      4  109  288  410   70%
c i  315.6   86225   619437     89387    6386    590 221835  485   627   58  77%      2  111  292  410   71%
c i  315.6   86224   619437     89405    6397    590 221835  484   628   58  77%      1  112  300  410   73%
c i  315.9   86223   619437     89638    6495    592 221838  490   639   59  77%     -5  123  453  411  110%
c i  316.3   86216   619437     89874    6598    593 221838  492   648   60  76%    -10  131  496  411  121%
c i  316.4   86215   619437     89904    6625    593 221838  491   649   60  76%    -11  132  476  411  116%
c i  318.6   86176   619437     91081    7361    599 221857  480   687   65  70%    -17  168  425  412  103%
c i  318.7   86175   619437     91184    7454    599 221857  474   690   65  69%    -19  170  365  412   89%
c i  321.0   86174   619437     92476    8355    604 221858  447   699   69  64%    -19  176  313  411   76%
c i  321.0   86173   619437     92518    8390    606 221861  442   700   69  63%    -19  177  268  411   65%
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  322.2   86172   619437     93264    8722    606 221873  445   700   69  64%    -22  175  413  411  100%
c 
c [simplification-11] limit 90358 conflicts (hard 100333) hit after 96120 conflicts
c [quatres-5] found 38175 quaternary clauses 42% in total
c [quatres-5-2] added 4 quaternary resolvents
c [ternres-6] limit 70442260 with penalty 0 = 0 + 0
c [ternres-6] all 86172 free variables schedulable
c [ternres-6] 51 ternary resolvents (0 bin, 51 trn)
c [ternres-6] fully completed ternary resolution
c [decomp-23] removed 120 variables
c [basicprobe-3] limit 352211300 penalty 0 = 0 + 0
c [basicprobe-3-0] 20804 probes remain 26% after last round
c [basicprobe-3-0] 1733 units = 1705 failed (98%) + 28 lifted (2%)
c [basicprobe-3-0] removed 4909 variables, found 754710 hbrs
c [bate-2] eliminated 727 asymmetric tautologies during probing
c [unhide-11] limit 7044226 with penalty 1 = 0 + 1
c [unhide-11-12] 26 units, 674 failed, 144095 tauts, 0 hbrs, 154676 literals
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 113 transitive binary clauses
c [block-4] scheduling all variables this time
c [block-4] scheduled 80617 variables 100%
c [block-4] limit of 176105650 steps penalty 2 = 2 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 208 blocked clauses
c [block-4] 208 < 1/100 * 573758 = 5737 considered unsuccessful
c [elim-9] scheduling all variables this time
c [elim-9] scheduled 80610 variables 100%
c [elim-9] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-9] rescheduling of touched variables disabled
c [elim-9-1] eliminated 3024 variables 4% in round 1 in 57019640 steps
c [elim-9-1] backward subsumption/strengthening limit 57019600
c [elim-9-1-1] backward checking 9989 touched variables 12%
c [elim-9-1-1] fully completed backward checking in 1 rounds
c [elim-9-1] subsumed 17 and strengthened 557 clauses in 3258465 steps
c [elim-9-1] rescheduled 1302 variables 2% by backward subsumption
c [elim-9-2] eliminated 185 variables 0% in round 2 in 1759383 steps
c [elim-9-2] backward subsumption/strengthening limit 1759300
c [elim-9-2-1] backward checking 1398 touched variables 2%
c [elim-9-2-1] fully completed backward checking in 1 rounds
c [elim-9-2] subsumed 5 and strengthened 3 clauses in 666583 steps
c [elim-9-2] rescheduled 10 variables 0% by backward subsumption
c [elim-9-3] no variable eliminated in round 3 in 6690 steps
c [elim-9] fully completed in 3 rounds
c [elim-9] transition to [ all 0 rem 0 ] state
c [elim-9] eliminated 3237 = 4% variables out of 80610 scheduled
c [bca-7] limit of 10000000 steps and 1119955 added (scaled 2)
c [bca-7] 140557 out of 154748 literals actually usable 91%
c [bca-7] added 149 blocked clauses in 406082 steps
c [sweep-7] limit 21132678 penalty 0 = 0 + 0
c [sweep-7-1] 3182 pos 7.9% + 37284 neg 92.1% = 40466 sched 52.3% ret 36907
c [sweep-7-1] 21242483 steps 374 queries 1263.65 avg class size
c [sweep-7-1] 3512 decisions 337 SAT calls 97.32 avg env size
c [sweep-7-1] 36967 variables remain 48% (40177 retained 52%)
c [decomp-24] removed 586 variables
c [sweep-7-1] removed 586 vars (0 failed, 42 eqs, 75 impls)
c [sweep-7] removed 586 vars in TOTAL (1 rounds, 373 queries)
c [phase-count-11] 556211 negative 99.8% of 557495 except 1284 0.2%
c [phase-count-11] 451420 positive 81.0% of 557495 except 106075 19.0%
c [phase-count-11] skipping relative phase luck test
c [phase-11] phase bias: 156 positive 100%, 0 negative 0%
c [sort-queue-11] sorted 26007 enqueued variables after 96120 conflicts
c [score-dist-11] active 50780 (66%), one 0 (0%), zero 26007 (34%)
c [score-dist-11] max exp 518, different 18 (3%)
c [score-dist-11] median active exp 507, avg 507.9
c [simplification-11] removed 9385 variables 10.9% (76787 remain 31%)
c [simplification-11] removed 61942 irredundant clauses 10.0% (557495 remain 41%)
c [simplification-11] maximum reduction of 11% = max (11%, 10%)
c [simplification-11] large reduction 11% >= 5% limit
c [simplification-11] next conflict interval 2000 = 2000/1
c [simplification-11] penalized conflict interval 2000 = 1 * 2000
c [simplification-11] hard conflict limit 108120 (soft 98120 + delta 10000)
c [simplification-11] new conflict limit 98120 (hard 108120)
c 
c [simplification-12] limit 98120 conflicts (hard 108120) hit after 98121 conflicts
c [quatres-6] found 38307 quaternary clauses 50% in total
c [quatres-6-2] added 1 single-self-subsuming ternary resolvents
c [quatres-6-2] added 10 quaternary resolvents
c [ternres-7] limit 71569932 with penalty 0 = 0 + 0
c [ternres-7] all 76787 free variables schedulable
c [ternres-7] 261 ternary resolvents (0 bin, 261 trn)
c [ternres-7] fully completed ternary resolution
c [simpleprobe-4] 3235 schedulable variables 4%
c [simpleprobe-4] limit 200000000 penalty 0 = 0 + 0
c [decomp-26] removed 1047 variables
c [simpleprobe-4] 1391 variables remain 2% (74349 retained 98%)
c [simpleprobe-4] removed 1047 variables, found 155356 hbrs, 468 units
c [unhide-12] limit 7156993 with penalty 1 = 0 + 1
c [unhide-12-14] 18 units, 244 failed, 90778 tauts, 0 hbrs, 17180 literals
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 178 transitive binary clauses
c [transred-8] found 1 units
c [cce-4] boosting limit by 10
c [cce-4] limit of 1789248300 steps penalty 1 = 1 + 0
c [cce-4-1] eliminated 3 clauses out of 790 (0%) of length 7
c [cce-4-1] eliminated 28 clauses out of 2667 (1%) of length 6
c [cce-4-1] eliminated 21433 clauses out of 31562 (68%) of length 5
c [cce-4-1] eliminated 19805 clauses out of 35619 (56%) of length 4
c [cce-4-1] completed large round (ATE)
c [cce-4-1] eliminated 41269 large clauses in 754515991 steps
c [cce-4-1] allowing another 377257995 steps for small clauses
c [cce-4-1] scheduling 447206 clauses = 248226 binary + 198980 ternary
c [cce-4-1] tried to eliminate 34061 small clauses 8%
c [cce-4-1] eliminated 4868 binary clauses 2%
c [cce-4-1] eliminated 1765 ternary clauses 1%
c [cce-4-1] eliminated 6633 small clauses 1%
c [cce-4-1] eliminated 7152 small clauses in 1789248301 steps
c [cce-4-1] incomplete small round (ATE)
c [cce-4-1] eliminated 48421 covered clauses in round 1
c [cce-4] eliminated 48421 covered clauses in TOTAL during 1 rounds
c [elim-10] scheduling all variables this time
c [elim-10] scheduled 75486 variables 100%
c [elim-10] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-10] rescheduling of touched variables disabled
c [elim-10-1] eliminated 16881 variables 22% in round 1 in 46985222 steps
c [elim-10-1] backward subsumption/strengthening limit 46985200
c [elim-10-1-1] backward checking 37285 touched variables 49%
c [elim-10-1-1] fully completed backward checking in 1 rounds
c [elim-10-1] subsumed 8 and strengthened 43 clauses in 5574366 steps
c [elim-10-1] rescheduled 128 variables 0% by backward subsumption
c [elim-10-2] eliminated 4 variables 0% in round 2 in 111389 steps
c [elim-10-2] backward subsumption/strengthening limit 111300
c [elim-10-2-1] backward checking 51 touched variables 0%
c [elim-10-2-1] incomplete backward checking 0 remain 0%
c [elim-10-2] subsumed 5 and strengthened 1 clauses in 111301 steps
c [elim-10-2] rescheduled 8 variables 0% by backward subsumption
c [elim-10-3] eliminated 1 variables 0% in round 3 in 7126 steps
c [elim-10-3] backward subsumption/strengthening limit 7100
c [elim-10-3-1] backward checking 13 touched variables 0%
c [elim-10-3-1] incomplete backward checking 0 remain 0%
c [elim-10-3] subsumed 4 and strengthened 0 clauses in 7101 steps
c [elim-10] incomplete 6 not tried 0% in round 3
c [elim-10] transition to [ all 1 rem 1 ] state
c [elim-10] eliminated 16888 = 22% variables out of 75486 scheduled
c [bca-8] limit of 10000000 steps and 908498 added (scaled 2)
c [bca-8] 110811 out of 117198 literals actually usable 95%
c [bca-8] added 419 blocked clauses in 254460 steps
c [sweep-8] limit 21470979 penalty 0 = 0 + 0
c [sweep-8-1] 3138 pos 9.8% + 28949 neg 90.2% = 32087 sched 54.8% ret 26511
c [sweep-8-1] 21475967 steps 434 queries 690.48 avg class size
c [sweep-8-1] 4467 decisions 405 SAT calls 91.52 avg env size
c [sweep-8-1] 28526 variables remain 49% (29892 retained 51%)
c [decomp-27] removed 333 variables
c [sweep-8-1] removed 333 vars (0 failed, 32 eqs, 68 impls)
c [sweep-8] removed 333 vars in TOTAL (1 rounds, 433 queries)
c [phase-count-12] 451024 negative 99.8% of 451858 except 834 0.2%
c [phase-count-12] 353546 positive 78.2% of 451858 except 98312 21.8%
c [phase-count-12] skipping relative phase luck test
c [phase-12] phase bias: 1 positive 1%, 72 negative 99%
c [sort-queue-12] sorted 19031 enqueued variables after 98121 conflicts
c [score-dist-12] active 39234 (67%), one 0 (0%), zero 19031 (33%)
c [score-dist-12] max exp 518, different 18 (3%)
c [score-dist-12] median active exp 507, avg 507.8
c [simplification-12] removed 18522 variables 24.1% (58265 remain 24%)
c [simplification-12] removed 105637 irredundant clauses 18.9% (451858 remain 33%)
c [simplification-12] maximum reduction of 24% = max (24%, 19%)
c [simplification-12] large reduction 24% >= 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 110121 (soft 100121 + delta 10000)
c [simplification-12] new conflict limit 100121 (hard 110121)
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  405.7   58264   451858     99236    2161   2538 711040  448   609   56  74%     46   71  273  419   65%
c i  406.0   58263   451858     99649    2378   2539 711041  425   588   56  72%     21   49  186  417   44%
c 
c [simplification-13] limit 100121 conflicts (hard 110121) hit after 100121 conflicts
c [quatres-7] found 24646 quaternary clauses 57% in total
c [quatres-7-2] added 2 single-self-subsuming ternary resolvents
c [ternres-8] limit 72000118 with penalty 0 = 0 + 0
c [ternres-8] all 58263 free variables schedulable
c [ternres-8] 642 ternary resolvents (3 bin, 639 trn)
c [ternres-8] fully completed ternary resolution
c [decomp-28] removed 10 variables
c [unhide-13] limit 14400023 with penalty 0 = 0 + 0
c [unhide-13-20] 26 units, 676 failed, 73763 tauts, 0 hbrs, 14564 literals
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 145 transitive binary clauses
c [cce-5] limit of 360000594 steps penalty 0 = 0 + 0
c [cce-5-1] eliminated 2 clauses out of 2 (100%) of length 24
c [cce-5-1] eliminated 1 clauses out of 2 (50%) of length 23
c [cce-5-1] eliminated 2 clauses out of 2 (100%) of length 22
c [cce-5-1] eliminated 1 clauses out of 2 (50%) of length 21
c [cce-5-1] eliminated 2 clauses out of 2 (100%) of length 20
c [cce-5-1] eliminated 1 clauses out of 1 (100%) of length 19
c [cce-5-1] eliminated 1 clauses out of 2 (50%) of length 18
c [cce-5-1] eliminated 2 clauses out of 2 (100%) of length 17
c [cce-5-1] eliminated 1 clauses out of 2 (50%) of length 16
c [cce-5-1] eliminated 2 clauses out of 2 (100%) of length 15
c [cce-5-1] eliminated 1 clauses out of 2 (50%) of length 14
c [cce-5-1] eliminated 2 clauses out of 2 (100%) of length 13
c [cce-5-1] eliminated 1 clauses out of 2 (50%) of length 12
c [cce-5-1] eliminated 2 clauses out of 2 (100%) of length 11
c [cce-5-1] eliminated 1 clauses out of 2 (50%) of length 10
c [cce-5-1] eliminated 2 clauses out of 3 (67%) of length 9
c [cce-5-1] eliminated 1 clauses out of 3 (33%) of length 8
c [cce-5-1] eliminated 7 clauses out of 48 (15%) of length 7
c [cce-5-1] eliminated 255 clauses out of 3685 (7%) of length 6
c [cce-5-1] eliminated 2278 clauses out of 13599 (17%) of length 5
c [cce-5-1] eliminated 29 clauses out of 23943 (0%) of length 4
c [cce-5-1] incomplete large round (ACCE)
c [cce-5-1] eliminated 2594 large clauses in 360000595 steps
c [cce-5-1] allowing another 180000297 steps for small clauses
c [cce-5-1] scheduling 378043 clauses = 188941 binary + 189102 ternary
c [cce-5-1] tried to eliminate 4501 small clauses 1%
c [cce-5-1] eliminated 640 binary clauses 0%
c [cce-5-1] eliminated 236 ternary clauses 0%
c [cce-5-1] eliminated 876 small clauses 0%
c [cce-5-1] eliminated 1412 small clauses in 360000597 steps
c [cce-5-1] incomplete small round (ACCE)
c [cce-5-1] eliminated 4006 covered clauses in round 1
c [cce-5] eliminated 4006 covered clauses in TOTAL during 1 rounds
c [cce-5] 4006 < 1/100 * 442074 = 4420 considered unsuccessful
c [elim-11] no untried remaining variables left
c [elim-11] scheduled 57753 variables 100%
c [elim-11] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-11] rescheduling of touched variables disabled
c [elim-11-1] eliminated 573 variables 1% in round 1 in 41822505 steps
c [elim-11-1] backward subsumption/strengthening limit 41822500
c [elim-11-1-1] backward checking 3499 touched variables 6%
c [elim-11-1-1] fully completed backward checking in 1 rounds
c [elim-11-1] subsumed 3 and strengthened 24 clauses in 1010160 steps
c [elim-11-1] rescheduled 57 variables 0% by backward subsumption
c [elim-11-2] eliminated 6 variables 0% in round 2 in 35153 steps
c [elim-11-2] backward subsumption/strengthening limit 35100
c [elim-11-2-1] backward checking 41 touched variables 0%
c [elim-11-2-1] incomplete backward checking 0 remain 0%
c [elim-11-2] subsumed 1 and strengthened 2 clauses in 35101 steps
c [elim-11-2] rescheduled 11 variables 0% by backward subsumption
c [elim-11-3] eliminated 1 variables 0% in round 3 in 153849 steps
c [elim-11-3] backward subsumption/strengthening limit 153800
c [elim-11-3-1] backward checking 10 touched variables 0%
c [elim-11-3-1] fully completed backward checking in 1 rounds
c [elim-11-3] subsumed 0 and strengthened 2 clauses in 49796 steps
c [elim-11] incomplete 8 not tried 0% in round 3
c [elim-11] transition to [ all 1 rem 1 ] state
c [elim-11] eliminated 581 = 1% variables out of 57753 scheduled
c [bca-9] limit of 10000000 steps and 874579 added (scaled 2)
c [bca-9] 105626 out of 114346 literals actually usable 92%
c [bca-9] added 478 blocked clauses in 241953 steps
c [sweep-9] limit 21600035 penalty 0 = 0 + 0
c [sweep-9-1] 2712 pos 9.7% + 25276 neg 90.3% = 27988 sched 49.0% ret 29184
c [sweep-9-1] 21628933 steps 536 queries 784.33 avg class size
c [sweep-9-1] 5249 decisions 484 SAT calls 88.61 avg env size
c [sweep-9-1] 24952 variables remain 44% (32102 retained 56%)
c [decomp-29] removed 347 variables
c [sweep-9-1] removed 347 vars (0 failed, 51 eqs, 89 impls)
c [sweep-9] removed 347 vars in TOTAL (1 rounds, 535 queries)
c [phase-count-13] 434191 negative 99.8% of 435012 except 821 0.2%
c [phase-count-13] 340319 positive 78.2% of 435012 except 94693 21.8%
c [phase-count-13] skipping relative phase luck test
c [phase-13] phase bias: 0 positive 0%, 5 negative 100%
c [sort-queue-13] sorted 17328 enqueued variables after 100121 conflicts
c [score-dist-13] active 39497 (70%), one 0 (0%), zero 17328 (30%)
c [score-dist-13] max exp 518, different 18 (3%)
c [score-dist-13] median active exp 507, avg 507.8
c [simplification-13] removed 1438 variables 2.5% (56825 remain 23%)
c [simplification-13] removed 16846 irredundant clauses 3.7% (435012 remain 32%)
c [simplification-13] maximum reduction of 4% = max (2%, 4%)
c [simplification-13] geometric conflict interval increment 6159 = 30799 / 5
c [simplification-13] new conflict interval 36958
c [simplification-13] penalized conflict interval 36958 = 1 * 36958
c [simplification-13] hard conflict limit 155558 (soft 137079 + delta 18479)
c [simplification-13] new conflict limit 137079 (hard 155558)
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  441.1   56824   435012    120352    9133   2973 648230  288   419  107  69%    242  -88  246  385   64%
c i  462.6   56823   435012    148792   14813   2988 648251  363   388  155  94%    304  -84  287  377   76%
c 
c [simplification-14] limit 137079 conflicts (hard 155558) hit after 155560 conflicts
c [quatres-8] found 23815 quaternary clauses 60% in total
c [quatres-8-2] added 1 single-self-subsuming ternary resolvents
c [quatres-8-2] added 14 quaternary resolvents
c [ternres-9] limit 84761547 with penalty 0 = 0 + 0
c [ternres-9] all 56819 free variables schedulable
c [ternres-9] 319 ternary resolvents (0 bin, 319 trn)
c [ternres-9] fully completed ternary resolution
c [gauss-4] limit 2119038 penalty 3 = 3 + 0
c [gauss-4] extracted 13 xors of average arity 3.0
c [gauss-4] connected 39 occurrences of 39 variables (average 1.0)
c [gauss-4] limit 2119038 penalty 3 = 3 + 0
c [gauss-4] fully completed
c [gauss-4] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-30] removed 10 variables
c [treelook-4] limit 4238077 penalty 1 = 1 + 0 boost 1
c [treelook-4] scheduled 78641 literals 69%
c [treelook-4] scheduling used 1620088 steps
c [treelook-4] scheduled completely
c [treelook-4] limit 4238077 penalty 1 = 1 + 0 boost 1
c [treelook-4] used 4295638 steps
c [treelook-4] 78548 literals remain 69%
c [treelook-4] 9115 variables remain to probed next time 16%
c [treelook-4] removed 28 variables, found 811 hbrs
c [unhide-14] limit 8476154 with penalty 1 = 0 + 1
c [unhide-14-23] 4 units, 118 failed, 21535 tauts, 0 hbrs, 272617 literals
c [transred-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 117 transitive binary clauses
c [elim-12] no untried remaining variables left
c [elim-12] scheduled 56640 variables 100%
c [elim-12] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-12] rescheduling of touched variables disabled
c [elim-12-1] eliminated 206 variables 0% in round 1 in 41396997 steps
c [elim-12-1] backward subsumption/strengthening limit 41396900
c [elim-12-1-1] backward checking 1332 touched variables 2%
c [elim-12-1-1] fully completed backward checking in 1 rounds
c [elim-12-1] subsumed 3 and strengthened 13 clauses in 452684 steps
c [elim-12-1] rescheduled 50 variables 0% by backward subsumption
c [elim-12-2] eliminated 2 variables 0% in round 2 in 65881 steps
c [elim-12-2] backward subsumption/strengthening limit 65800
c [elim-12-2-1] backward checking 29 touched variables 0%
c [elim-12-2-1] fully completed backward checking in 1 rounds
c [elim-12-2] subsumed 0 and strengthened 2 clauses in 51592 steps
c [elim-12-2] rescheduled 8 variables 0% by backward subsumption
c [elim-12-3] eliminated 1 variables 0% in round 3 in 8078 steps
c [elim-12-3] backward subsumption/strengthening limit 8000
c [elim-12-3-1] backward checking 10 touched variables 0%
c [elim-12-3-1] incomplete backward checking 0 remain 0%
c [elim-12-3] subsumed 0 and strengthened 2 clauses in 8001 steps
c [elim-12] incomplete 8 not tried 0% in round 3
c [elim-12] transition to [ all 1 rem 1 ] state
c [elim-12] eliminated 210 = 0% variables out of 56640 scheduled
c [elim-12] 210 < 1/100 * 56640 = 566 considered unsuccessful
c [bca-10] limit of 10000000 steps and 862282 added (scaled 2)
c [bca-10] 100200 out of 112862 literals actually usable 89%
c [bca-10] added 118 blocked clauses in 238774 steps
c [sweep-10] limit 25428464 penalty 0 = 0 + 0
c [sweep-10-1] 2703 pos 11.0% + 21930 neg 89.0% = 24633 sched 43.7% ret 31797
c [sweep-10-1] 25438777 steps 714 queries 514.96 avg class size
c [sweep-10-1] 6370 decisions 656 SAT calls 96.08 avg env size
c [sweep-10-1] 21310 variables remain 38% (35086 retained 62%)
c [decomp-32] removed 251 variables
c [sweep-10-1] removed 251 vars (0 failed, 66 eqs, 111 impls)
c [sweep-10] removed 251 vars in TOTAL (1 rounds, 713 queries)
c [phase-count-14] 428784 negative 99.8% of 429594 except 810 0.2%
c [phase-count-14] 335607 positive 78.1% of 429594 except 93987 21.9%
c [phase-count-14] skipping relative phase luck test
c [phase-14] phase bias: 2 positive 29%, 5 negative 71%
c [sort-queue-14] sorted 16243 enqueued variables after 155560 conflicts
c [score-dist-14] active 39936 (71%), one 0 (0%), zero 16243 (29%)
c [score-dist-14] max exp 518, different 18 (3%)
c [score-dist-14] median active exp 507, avg 508.2
c [simplification-14] removed 640 variables 1.1% (56179 remain 23%)
c [simplification-14] removed 5418 irredundant clauses 1.2% (429594 remain 31%)
c [simplification-14] maximum reduction of 1% = max (1%, 1%)
c [simplification-14] geometric conflict interval increment 18479 = 36958 / 2
c [simplification-14] new conflict interval 55437
c [simplification-14] penalized conflict interval 55437 = 1 * 55437
c [simplification-14] hard conflict limit 238715 (soft 210997 + delta 27718)
c [simplification-14] new conflict limit 210997 (hard 238715)
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  478.7   56178   429594    156597   13604   3077 652447  361   477   78  76%    -15   10  306  371   82%
c i  478.8   56177   429594    156730   13685   3079 652447  359   479   78  75%    -28   12  295  371   79%
c i  488.9   56176   429594    167373   18265   3108 652463  284   456   88  62%     35   -4  273  357   77%
c i  509.4   56175   429594    182059   22103   3139 652473  429   512  118  84%     99   40  472  376  126%
c i  542.8   56174   429594    210246   29819   3173 652494  370   462  226  80%    270  -18  285  391   73%
c i  542.8   56173   429594    210247   29819   3173 652494  370   462  226  80%    270  -18  284  391   73%
c 
c [simplification-15] limit 211007 conflicts (hard 238715) hit after 220690 conflicts
c [quatres-9] found 23916 quaternary clauses 60% in total
c [quatres-9-2] added 1 single-self-subsuming ternary resolvents
c [quatres-9-2] added 1 quaternary resolvents
c [ternres-10] limit 106213279 with penalty 0 = 0 + 0
c [ternres-10] all 56172 free variables schedulable
c [ternres-10] 111 ternary resolvents (0 bin, 111 trn)
c [ternres-10] fully completed ternary resolution
c [card-5] limit 3319164 penalty 4 = 4 + 0
c [card-5] found 3085 at-most-one constraints of average size 4.0
c [card-5] no at-most-two constraint found
c [card-5] using previous limit 3319164 for elimination
c [card-5] 3085 out of 3085 constraints (100%) meet size limits
c [card-5] no units found
c [card-5] no at-most-one constraints generated
c [decomp-33] removed 12 variables
c [basicprobe-4] limit 400000000 penalty 0 = 0 + 0
c [basicprobe-4-0] 15951 sched 30%, 1502 failed, 209 lifted, 743482 hbrs
c [decomp-34] removed 2691 variables
c [basicprobe-4-1] 14726 probes remain 28% after last round
c [basicprobe-4-1] 1793 units = 1584 failed (88%) + 209 lifted (12%)
c [basicprobe-4-1] removed 2857 variables, found 794341 hbrs
c [bate-3] eliminated 1943 asymmetric tautologies during probing
c [unhide-15] limit 5000000 with penalty 2 = 0 + 2
c [unhide-15-25] 4 units, 114 failed, 131010 tauts, 0 hbrs, 282729 literals
c [transred-11] limit 2000000 with penalty 0 = 0 + 0
c [transred-11] removed 114 transitive binary clauses
c [block-5] scheduling all variables this time
c [block-5] scheduled 53184 variables 100%
c [block-5] limit of 100000000 steps penalty 3 = 3 + 0
c [block-5] fully completed
c [block-5] transition to [ all 0 rem 0 ] state
c [block-5] eliminated 300 blocked clauses
c [block-5] 300 < 1/100 * 394439 = 3944 considered unsuccessful
c [cce-6] limit of 265533197 steps penalty 1 = 1 + 0
c [cce-6-1] eliminated 3 clauses out of 3 (100%) of length 31
c [cce-6-1] eliminated 2 clauses out of 3 (67%) of length 30
c [cce-6-1] eliminated 3 clauses out of 3 (100%) of length 29
c [cce-6-1] eliminated 3 clauses out of 4 (75%) of length 28
c [cce-6-1] eliminated 3 clauses out of 4 (75%) of length 27
c [cce-6-1] eliminated 3 clauses out of 4 (75%) of length 26
c [cce-6-1] eliminated 3 clauses out of 4 (75%) of length 25
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 24
c [cce-6-1] eliminated 2 clauses out of 3 (67%) of length 23
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 22
c [cce-6-1] eliminated 2 clauses out of 3 (67%) of length 21
c [cce-6-1] eliminated 2 clauses out of 3 (67%) of length 20
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 19
c [cce-6-1] eliminated 2 clauses out of 3 (67%) of length 18
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 17
c [cce-6-1] eliminated 2 clauses out of 3 (67%) of length 16
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 15
c [cce-6-1] eliminated 2 clauses out of 3 (67%) of length 14
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 13
c [cce-6-1] eliminated 2 clauses out of 3 (67%) of length 12
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 11
c [cce-6-1] eliminated 7 clauses out of 9 (78%) of length 10
c [cce-6-1] eliminated 1 clauses out of 3 (33%) of length 9
c [cce-6-1] eliminated 2 clauses out of 4 (50%) of length 8
c [cce-6-1] eliminated 1 clauses out of 39 (3%) of length 7
c [cce-6-1] eliminated 18 clauses out of 2999 (1%) of length 6
c [cce-6-1] eliminated 78 clauses out of 10181 (1%) of length 5
c [cce-6-1] eliminated 40 clauses out of 20699 (0%) of length 4
c [cce-6-1] incomplete large round (ATE)
c [cce-6-1] eliminated 188 large clauses in 265533201 steps
c [cce-6-1] allowing another 132766600 steps for small clauses
c [cce-6-1] scheduling 340188 clauses = 176224 binary + 163964 ternary
c [cce-6-1] tried to eliminate 3886 small clauses 1%
c [cce-6-1] eliminated 501 binary clauses 0%
c [cce-6-1] eliminated 125 ternary clauses 0%
c [cce-6-1] eliminated 626 small clauses 0%
c [cce-6-1] eliminated 626 small clauses in 265533200 steps
c [cce-6-1] incomplete small round (ATE)
c [cce-6-1] eliminated 814 covered clauses in round 1
c [cce-6] eliminated 814 covered clauses in TOTAL during 1 rounds
c [cce-6] 814 < 1/100 * 393434 = 3934 considered unsuccessful
c [bca-11] limit of 10000000 steps and 787095 added (scaled 2)
c [bca-11] 91639 out of 106352 literals actually usable 86%
c [bca-11] added 61 blocked clauses in 234516 steps
c [sweep-11] boosting sweeping limit by 10
c [sweep-11] limit 318639830 penalty 0 = 0 + 0
c [sweep-11-1] 2077 pos 10.4% + 17911 neg 89.6% = 19988 sched 37.6% ret 33187
c [sweep-11-1] 182119361 steps 7307 queries 55.78 avg class size
c [sweep-11-1] 33192 decisions 5662 SAT calls 82.89 avg env size
c [sweep-11-1] fully completed sweeping round
c [decomp-35] removed 2393 variables
c [sweep-11-1] removed 2393 vars (0 failed, 1661 eqs, 1584 impls)
c [sweep-11-2] 4232 pos 8.3% + 46550 neg 91.7% = 50782 sched 100.0% ret 0
c [sweep-11-2] 136523063 steps 2769 queries 115.41 avg class size
c [sweep-11-2] 25271 decisions 2675 SAT calls 114.58 avg env size
c [sweep-11-2] 13686 variables remain 27% (36945 retained 73%)
c [decomp-36] removed 258 variables
c [sweep-11-2] removed 258 vars (0 failed, 101 eqs, 338 impls)
c [sweep-11] removed 2651 vars in TOTAL (2 rounds, 10074 queries)
c [phase-count-15] 384154 negative 99.8% of 384958 except 804 0.2%
c [phase-count-15] 300830 positive 78.1% of 384958 except 84128 21.9%
c [phase-count-15] skipping relative phase luck test
c [phase-15] phase bias: 1 positive 100%, 0 negative 0%
c [sort-queue-15] sorted 13315 enqueued variables after 220690 conflicts
c [score-dist-15] active 37209 (74%), one 0 (0%), zero 13315 (26%)
c [score-dist-15] max exp 519, different 19 (4%)
c [score-dist-15] median active exp 508, avg 508.8
c [simplification-15] removed 5648 variables 10.1% (50524 remain 21%)
c [simplification-15] removed 44636 irredundant clauses 10.4% (384958 remain 28%)
c [simplification-15] maximum reduction of 10% = max (10%, 10%)
c [simplification-15] large reduction 10% >= 5% limit
c [simplification-15] next conflict interval 2206 = min (220690/100, 55437)
c [simplification-15] penalized conflict interval 2206 = 1 * 2206
c [simplification-15] hard conflict limit 232896 (soft 222896 + delta 10000)
c [simplification-15] new conflict limit 222896 (hard 232896)
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  605.1   50523   384958    221750   34462   4183 1396392  429   509  146  84%     16   29  435  394  110%
c i  606.9   50522   384958    223287   34880   4184 1396394  425   506  146  84%    -98   26  381  395   97%
c i  613.1   50521   384958    227781   35624   4185 1396395  420   471  166  89%    -84  -10  363  397   92%
c i  614.8   50516   384958    229139   35987   4185 1396395  405   460  167  88%   -112  -21  341  396   86%
c 
c [simplification-16] limit 222896 conflicts (hard 232896) hit after 232896 conflicts
c [quatres-10] found 20066 quaternary clauses 57% in total
c [quatres-10-1] removed 4 duplicate quaternary clauses
c [quatres-10-2] added 5 single-self-subsuming ternary resolvents
c [ternres-11] limit 110466729 with penalty 0 = 0 + 0
c [ternres-11] all 50516 free variables schedulable
c [ternres-11] 899 ternary resolvents (2 bin, 897 trn)
c [ternres-11] fully completed ternary resolution
c [decomp-37] removed 10 variables
c [simpleprobe-5] 1004 schedulable variables 2%
c [simpleprobe-5] limit 200000000 penalty 0 = 0 + 0
c [decomp-38] removed 237 variables
c [simpleprobe-5] 8127 variables remain 16% (42150 retained 84%)
c [simpleprobe-5] removed 237 variables, found 188083 hbrs, 127 units
c [unhide-16] limit 5000000 with penalty 2 = 0 + 2
c [unhide-16-26] 4 units, 53 failed, 205404 tauts, 0 hbrs, 95748 literals
c [transred-12] limit 2000000 with penalty 0 = 0 + 0
c [transred-12] removed 271 transitive binary clauses
c [elim-13] no untried remaining variables left
c [elim-13] scheduled 50224 variables 100%
c [elim-13] almost no limit of 100000000000 steps
c [elim-13] rescheduling of touched variables disabled
c [elim-13-1] eliminated 1087 variables 2% in round 1 in 38647292 steps
c [elim-13-1] backward subsumption/strengthening limit 38647200
c [elim-13-1-1] backward checking 6060 touched variables 12%
c [elim-13-1-1] fully completed backward checking in 1 rounds
c [elim-13-1] subsumed 5 and strengthened 54 clauses in 1934141 steps
c [elim-13-1] rescheduled 173 variables 0% by backward subsumption
c [elim-13-2] eliminated 10 variables 0% in round 2 in 110993 steps
c [elim-13-2] backward subsumption/strengthening limit 110900
c [elim-13-2-1] backward checking 171 touched variables 0%
c [elim-13-2-1] incomplete backward checking 0 remain 0%
c [elim-13-2] subsumed 5 and strengthened 4 clauses in 110901 steps
c [elim-13-2] rescheduled 25 variables 0% by backward subsumption
c [elim-13-3] eliminated 3 variables 0% in round 3 in 58759 steps
c [elim-13-3] backward subsumption/strengthening limit 58700
c [elim-13-3-1] backward checking 82 touched variables 0%
c [elim-13-3-1] incomplete backward checking 0 remain 0%
c [elim-13-3] subsumed 0 and strengthened 2 clauses in 58701 steps
c [elim-13] incomplete 8 not tried 0% in round 3
c [elim-13] transition to [ all 1 rem 1 ] state
c [elim-13] eliminated 1100 = 2% variables out of 50224 scheduled
c [bca-12] limit of 10000000 steps and 753774 added (scaled 2)
c [bca-12] 79910 out of 98250 literals actually usable 81%
c [bca-12] added 38 blocked clauses in 206637 steps
c [sweep-12] limit 33140018 penalty 0 = 0 + 0
c [sweep-12-1] 1585 pos 12.1% + 11557 neg 87.9% = 13142 sched 26.8% ret 35982
c [sweep-12-1] 33205706 steps 884 queries 254.66 avg class size
c [sweep-12-1] 7568 decisions 850 SAT calls 106.99 avg env size
c [sweep-12-1] 9797 variables remain 20% (39306 retained 80%)
c [decomp-39] removed 57 variables
c [sweep-12-1] removed 57 vars (0 failed, 34 eqs, 127 impls)
c [sweep-12] removed 57 vars in TOTAL (1 rounds, 883 queries)
c [phase-count-16] 374856 negative 99.8% of 375597 except 741 0.2%
c [phase-count-16] 292392 positive 77.8% of 375597 except 83205 22.2%
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 12851 enqueued variables after 232896 conflicts
c [score-dist-16] active 36216 (74%), one 0 (0%), zero 12851 (26%)
c [score-dist-16] max exp 519, different 19 (4%)
c [score-dist-16] median active exp 508, avg 508.9
c [simplification-16] removed 1449 variables 2.9% (49067 remain 20%)
c [simplification-16] removed 9361 irredundant clauses 2.4% (375597 remain 27%)
c [simplification-16] maximum reduction of 3% = max (3%, 2%)
c [simplification-16] geometric conflict interval increment 13859 = 55437 / 4
c [simplification-16] new conflict interval 69296
c [simplification-16] penalized conflict interval 69296 = 1 * 69296
c [simplification-16] hard conflict limit 336840 (soft 302192 + delta 34648)
c [simplification-16] new conflict limit 302192 (hard 336840)
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  698.2   49066   375597    284528   44169   4609 1295201  288   315  217  92%    518 -106  170  360   47%
c 
c [simplification-17] limit 302192 conflicts (hard 336840) hit after 304305 conflicts
c [quatres-11] found 20274 quaternary clauses 56% in total
c [quatres-11-1] removed 1 duplicate quaternary clauses
c [quatres-11-2] added 4 single-self-subsuming ternary resolvents
c [quatres-11-2] added 6 quaternary resolvents
c [ternres-12] limit 136019033 with penalty 0 = 0 + 0
c [ternres-12] all 49063 free variables schedulable
c [ternres-12] 344 ternary resolvents (0 bin, 344 trn)
c [ternres-12] fully completed ternary resolution
c [decomp-40] removed 6 variables
c [treelook-5] limit 13601903 penalty 0 = 0 + 0 boost 1
c [treelook-5] scheduled 68155 literals 69%
c [treelook-5] scheduling used 1778085 steps
c [treelook-5] scheduled completely
c [treelook-5] limit 13601903 penalty 0 = 0 + 0 boost 1
c [treelook-5] used 13621430 steps
c [treelook-5] 67924 literals remain 69%
c [treelook-5] 7671 variables remain to probed next time 16%
c [treelook-5] removed 44 variables, found 19928 hbrs
c [unhide-17] limit 2500000 with penalty 3 = 0 + 3
c [unhide-17-28] 4 units, 26 failed, 86022 tauts, 0 hbrs, 338307 literals
c [transred-13] limit 2000000 with penalty 0 = 0 + 0
c [transred-13] removed 221 transitive binary clauses
c [transred-13] found 1 units
c [elim-14] no untried remaining variables left
c [elim-14] scheduled 48984 variables 100%
c [elim-14] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-14] rescheduling of touched variables disabled
c [elim-14-1] eliminated 145 variables 0% in round 1 in 37353135 steps
c [elim-14-1] backward subsumption/strengthening limit 37353100
c [elim-14-1-1] backward checking 1097 touched variables 2%
c [elim-14-1-1] fully completed backward checking in 1 rounds
c [elim-14-1] subsumed 1 and strengthened 11 clauses in 457450 steps
c [elim-14-1] rescheduled 29 variables 0% by backward subsumption
c [elim-14-2] eliminated 2 variables 0% in round 2 in 13365 steps
c [elim-14-2] backward subsumption/strengthening limit 13300
c [elim-14-2-1] backward checking 27 touched variables 0%
c [elim-14-2-1] incomplete backward checking 0 remain 0%
c [elim-14-2] subsumed 0 and strengthened 2 clauses in 13301 steps
c [elim-14-2] rescheduled 8 variables 0% by backward subsumption
c [elim-14-3] eliminated 1 variables 0% in round 3 in 18298 steps
c [elim-14-3] backward subsumption/strengthening limit 18200
c [elim-14-3-1] backward checking 10 touched variables 0%
c [elim-14-3-1] incomplete backward checking 0 remain 0%
c [elim-14-3] subsumed 0 and strengthened 2 clauses in 18201 steps
c [elim-14] incomplete 8 not tried 0% in round 3
c [elim-14] transition to [ all 1 rem 1 ] state
c [elim-14] eliminated 148 = 0% variables out of 48984 scheduled
c [elim-14] 148 < 1/100 * 48984 = 489 considered unsuccessful
c [bca-13] limit of 10000000 steps and 743117 added (scaled 2)
c [bca-13] 78512 out of 97674 literals actually usable 80%
c [bca-13] added 31 blocked clauses in 218167 steps
c [sweep-13] limit 40805709 penalty 0 = 0 + 0
c [sweep-13-1] 1243 pos 12.8% + 8503 neg 87.2% = 9746 sched 20.0% ret 39090
c [sweep-13-1] 40830570 steps 1219 queries 137.78 avg class size
c [sweep-13-1] 7775 decisions 1171 SAT calls 80.51 avg env size
c [sweep-13-1] 6014 variables remain 12% (42814 retained 88%)
c [decomp-42] removed 58 variables
c [sweep-13-1] removed 58 vars (0 failed, 49 eqs, 183 impls)
c [sweep-13] removed 58 vars in TOTAL (1 rounds, 1218 queries)
c [phase-count-17] 369517 negative 99.8% of 370253 except 736 0.2%
c [phase-count-17] 288888 positive 78.0% of 370253 except 81365 22.0%
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 12660 enqueued variables after 304305 conflicts
c [score-dist-17] active 36118 (74%), one 0 (0%), zero 12660 (26%)
c [score-dist-17] max exp 519, different 19 (4%)
c [score-dist-17] median active exp 508, avg 509.3
c [simplification-17] removed 285 variables 0.6% (48778 remain 20%)
c [simplification-17] removed 5344 irredundant clauses 1.4% (370253 remain 27%)
c [simplification-17] maximum reduction of 1% = max (1%, 1%)
c [simplification-17] geometric conflict interval increment 34648 = 69296 / 2
c [simplification-17] new conflict interval 103944
c [simplification-17] penalized conflict interval 103944 = 1 * 103944
c [simplification-17] hard conflict limit 460221 (soft 408249 + delta 51972)
c [simplification-17] new conflict limit 408249 (hard 460221)
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 -  741.3   48778   370253    309750   22927   4719 1256081  350   487   83  72%     82   82  488  337  145%
c 
c [simplification-18] limit 408249 conflicts (hard 460221) hit after 422146 conflicts
c [quatres-12] found 20235 quaternary clauses 56% in total
c [ternres-13] limit 181649241 with penalty 0 = 0 + 0
c [ternres-13] all 48778 free variables schedulable
c [ternres-13] 216 ternary resolvents (0 bin, 216 trn)
c [ternres-13] fully completed ternary resolution
c [basicprobe-5] limit 400000000 penalty 0 = 0 + 0
c [basicprobe-5-0] 13245 sched 28%, 523 failed, 25 lifted, 368150 hbrs
c [decomp-44] removed 719 variables
c [basicprobe-5-1] 12836 probes remain 27% after last round
c [basicprobe-5-1] 592 units = 567 failed (96%) + 25 lifted (4%)
c [basicprobe-5-1] removed 773 variables, found 383034 hbrs
c [bate-4] eliminated 256 asymmetric tautologies during probing
c [unhide-18] limit 5000000 with penalty 2 = 0 + 2
c [unhide-18-29] 1 units, 35 failed, 143742 tauts, 0 hbrs, 206808 literals
c [transred-14] limit 2000000 with penalty 0 = 0 + 0
c [transred-14] removed 282 transitive binary clauses
c [cce-7] limit of 227061552 steps penalty 2 = 2 + 0
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 36
c [cce-7-1] eliminated 1 clauses out of 3 (33%) of length 35
c [cce-7-1] eliminated 2 clauses out of 4 (50%) of length 34
c [cce-7-1] eliminated 5 clauses out of 6 (83%) of length 33
c [cce-7-1] eliminated 3 clauses out of 5 (60%) of length 32
c [cce-7-1] eliminated 3 clauses out of 4 (75%) of length 31
c [cce-7-1] eliminated 2 clauses out of 4 (50%) of length 30
c [cce-7-1] eliminated 4 clauses out of 5 (80%) of length 29
c [cce-7-1] eliminated 4 clauses out of 8 (50%) of length 28
c [cce-7-1] eliminated 5 clauses out of 10 (50%) of length 27
c [cce-7-1] eliminated 7 clauses out of 11 (64%) of length 26
c [cce-7-1] eliminated 6 clauses out of 11 (55%) of length 25
c [cce-7-1] eliminated 9 clauses out of 11 (82%) of length 24
c [cce-7-1] eliminated 6 clauses out of 12 (50%) of length 23
c [cce-7-1] eliminated 10 clauses out of 12 (83%) of length 22
c [cce-7-1] eliminated 7 clauses out of 14 (50%) of length 21
c [cce-7-1] eliminated 8 clauses out of 13 (62%) of length 20
c [cce-7-1] eliminated 8 clauses out of 14 (57%) of length 19
c [cce-7-1] eliminated 11 clauses out of 17 (65%) of length 18
c [cce-7-1] eliminated 9 clauses out of 16 (56%) of length 17
c [cce-7-1] eliminated 14 clauses out of 20 (70%) of length 16
c [cce-7-1] eliminated 14 clauses out of 21 (67%) of length 15
c [cce-7-1] eliminated 13 clauses out of 24 (54%) of length 14
c [cce-7-1] eliminated 13 clauses out of 21 (62%) of length 13
c [cce-7-1] eliminated 20 clauses out of 31 (65%) of length 12
c [cce-7-1] eliminated 22 clauses out of 34 (65%) of length 11
c [cce-7-1] eliminated 26 clauses out of 36 (72%) of length 10
c [cce-7-1] eliminated 21 clauses out of 39 (54%) of length 9
c [cce-7-1] eliminated 28 clauses out of 44 (64%) of length 8
c [cce-7-1] eliminated 26 clauses out of 84 (31%) of length 7
c [cce-7-1] eliminated 57 clauses out of 2939 (2%) of length 6
c [cce-7-1] eliminated 159 clauses out of 9457 (2%) of length 5
c [cce-7-1] eliminated 40 clauses out of 19147 (0%) of length 4
c [cce-7-1] incomplete large round (ACCE)
c [cce-7-1] eliminated 565 large clauses in 227061557 steps
c [cce-7-1] allowing another 113530778 steps for small clauses
c [cce-7-1] scheduling 314462 clauses = 175653 binary + 138809 ternary
c [cce-7-1] tried to eliminate 3758 small clauses 1%
c [cce-7-1] eliminated 556 binary clauses 0%
c [cce-7-1] eliminated 106 ternary clauses 0%
c [cce-7-1] eliminated 662 small clauses 0%
c [cce-7-1] eliminated 924 small clauses in 227061556 steps
c [cce-7-1] incomplete small round (ACCE)
c [cce-7-1] eliminated 1489 covered clauses in round 1
c [cce-7] eliminated 1489 covered clauses in TOTAL during 1 rounds
c [cce-7] 1489 < 1/100 * 360759 = 3607 considered unsuccessful
c [bca-14] limit of 10000000 steps and 720460 added (scaled 2)
c [bca-14] 77301 out of 95962 literals actually usable 81%
c [bca-14] added 19 blocked clauses in 206807 steps
c [sweep-14] limit 54494772 penalty 0 = 0 + 0
c [sweep-14-1] 634 pos 10.7% + 5319 neg 89.3% = 5953 sched 12.4% ret 42027
c [sweep-14-1] 54549159 steps 2012 queries 66.23 avg class size
c [sweep-14-1] 11130 decisions 1926 SAT calls 70.40 avg env size
c [sweep-14-1] 1461 variables remain 3% (46482 retained 97%)
c [decomp-45] removed 167 variables
c [sweep-14-1] removed 167 vars (0 failed, 87 eqs, 322 impls)
c [sweep-14] removed 167 vars in TOTAL (1 rounds, 2011 queries)
c [phase-count-18] 357856 negative 99.8% of 358597 except 741 0.2%
c [phase-count-18] 278325 positive 77.6% of 358597 except 80272 22.4%
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 11951 enqueued variables after 422146 conflicts
c [score-dist-18] active 35862 (75%), one 0 (0%), zero 11951 (25%)
c [score-dist-18] max exp 520, different 20 (4%)
c [score-dist-18] median active exp 509, avg 509.6
c [simplification-18] removed 965 variables 2.0% (47813 remain 19%)
c [simplification-18] removed 11656 irredundant clauses 3.1% (358597 remain 26%)
c [simplification-18] maximum reduction of 3% = max (2%, 3%)
c [simplification-18] geometric conflict interval increment 25986 = 103944 / 4
c [simplification-18] new conflict interval 129930
c [simplification-18] penalized conflict interval 129930 = 1 * 129930
c [simplification-18] hard conflict limit 617041 (soft 552076 + delta 64965)
c [simplification-18] new conflict limit 552076 (hard 617041)
c
c CAUGHT SIGNAL 15 SIGTERM
c
c s UNKNOWN
c bate: 2984 basic ate = 2839 trn 95% + 145 lrg 5% in 4 updates
c bcas: 14 count, 2860 added (582 skipped), 5099793 steps
c bkwd: tried 436586 clauses, 873009 lits, 2.00 lits/clause
c bkwd: checked 14194397 occs, 32.51 occs/clause, 16.26 occs/lit
c bkwd: subsumed 10 binary, 33 ternary, 14 large
c bkwd: strengthened 1 binary, 1 ternary (100% self), 1159 large (0% self)
c blkd: 5 bces, 12265 removed, 9946293 resolutions, 27956216 steps
c blkd: 15233 blocking literals 3%, 16 pure
c bump: 473526 bumped seen, 670333263 lits 1415.6 on average
c card: 5 count, 0 units, 0 am1, 283599857 steps
c card: 0 rescheduled, 0 eliminated, 0 resolved, 99961 subsumed
c card: 24764 at-most-one constraints found, average size 4.55
c card: 24764 at-most-one constraints used 100%, average size 4.55
c card: 0 at-most-two constraints found, average size 0.00
c card: 0 at-most-two constraints used 0%, average size 0.00
c cces: 7 cces, 58892 eliminated, 58288 ate 99%, 604 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: 4739857 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 142 gcs, 0 rescored clauses, 0 rescored vars
c dcps: 45 decompositions, 11153 equivalent 4%
c deco: 367595 decision-only clauses 78%, 62% reduction
c decs: 6301263 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 14 elims, 106326 eliminated 41%, 103 pure 0%
c elms: 35 rounds, 2.5 rounds/bve
c elms: 84192 small 79%, 22015 large 21%
c elms: 193063 tried small, 84192 succeeded 44%, 108871 failed 56%
c elms: 50476 subsumed, 70587 strengthened, 2037 blocked
c elms: 21924933 copies, 21678253 resolutions, 4626288 ipos
c elms: 6426707 subchks, 3433513 strchks
c gaus: 4 extractions, 113 extracted, 2.8 size, 3 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 17344596 steps, 8672298 extr 50%, 906 elim 0%
c glue: 384.3 orig avg, 384.3 real avg, 11.4 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 3053483 = 390058 simple 13% + 2652549 trn 87% + 10876 lrg 0%, 5886 sub 0%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 473526 clauses, 434.6 length
c lrnd: 205809169 lits = 482645220 orig - 276836051 removed 57%
c lrnd: 204833 uips 43%, 239426 flips 51%
c mins: 76664 mins 17%, 984 bin 0%, 1987 size 0%
c mins: 29321311 poisoned searches, 8112856 hits, 28% hit rate
c mins: 37438239 used twice searches, 5612051 hits, 15% hit rate
c move: moved 30549, 19021 bin 62%, 11528 trn 38%
c otfs: 3400 driving 51%, 3269 restarting 49%
c otfs: str 6669, 6570 red 99%, 99 irr 1%
c otfs: str 6669, 0 bin 0%, 89 trn 1%, 6580 lrg 99%
c otfs: sub 29, 29 red 100%, 0 irr 0%
c otfs: sub 29, 0 bin 0%, 0 trn 0%, 29 lrg 100%
c phas: 18 computed, 155908 set, 160 pos (0%), 155748 neg (100%)
c prbs: 5 basic, 78468 probed, 3984 failed, 262 lifted
c prbs: 5 simple, 594588 probed, 627 failed, 559 eqs
c prbs: 5 treelook, 246 probed, 40 failed, 0 lifted
c prom: 184 locked 0% out of 488303 tried
c prps: 2554951530 props, 385 props/dec
c prps: 95% srch, 5% simp, 0% lkhd
c quat: 12 count, 36 quat, 17 self1, 0 self2, 2228 dup
c queu: 18 sorted, 6301263 next (31455 steps 0.00)
c queu: 671368499 enq (1547973867 steps 2.31), 670333263 deq 100%
c redc: 1136 clauses 18%, 6144 tried 1%, 30 sat 0%
c redc: 2703 lits 5%, 51692 tried 0%, 30 sat 0%
c redc: 121 times jump level reduced, 100.5 levels on average
c reds: 1 count, 472216.0 conflicts per reduce
c reds: 0 memlim 0%, 1 arith 100%
c reds: 25000 collected 82%, 5585 retired 18%
c rmbd: 55527 removed, 14400 red 26%
c rsts: 6461 restarts 73%, 2337 skipped 27%
c rsts: 2337 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: 18 count, 16 confs 89%, 0 vars 0%
c simp: 1 its 6%, 1 bin 6%, 0 trns 0%
c subl: 473526 count (682885 tried 1.4), 347743 sub out of 470146 (74.0%)
c swps: 14 count, 15 rounds, 18378 queries (1225.2/round)
c swps: 15950 sat calls, 157 unsat (0.3% success rate)
c swps: 121569 decisions 7.6, 4710 conflicts 0.3
c swps; 394.9 avg class size, 89.0 avg environment size
c swps: 0 failed, 3582 impls, 2524 equivs
c swp0: 6121 type 0 queries, 3675 unsat (60.0%), 5190 sat (84.8%)
c swp1: 12257 type 1 queries, 7391 unsat (60.3%), 10664 sat (87.0%)
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: 13550030 calls to obtain time
c tops: 93942 fixed 36%, 121 its, 3902.61 confs/it
c trds: 14 transitive reductions, 2538 removed, 32 failed
c trds: 13909 nodes, 42526 edges, 28019274 steps
c trim: 3781500 words, 14.4 MB
c trnr: 13 count, 5 bin, 2959 trn, 231932183 steps
c unhd: 18 count, 29 rounds, 107319757 steps
c unhd: 1682 non-trivial sccs of average size 2.1
c unhd: 142 units, 141 bin, 1 trn, 0 lrg
c unhd: 8105 failed, 8031 stamp, 0 lits, 57 bin, 6 trn, 0 lrg
c unhd: 1015871 tauts, 24025 bin 2%, 13213 trn 1%, 317 lrg 0%
c unhd: 1015871 tauts, 978316 stamp 96%, 940305 red 93%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 2263294 str, 141 bin 0%, 2557 trn 0%, 2260596 lrg 100%, 2246685 red 99%
c vars: 47813 remaining 18% and 211421 removed 82% out of 259234
c vars: 93942 fixed 36%, 106326 eliminated 41%, 11153 equivalent 4%
c vsts: 21343393822 visits, 94% srch, 6% simp, 0% lkhd
c vsts: 8.2 search visits per propagation, 42396.8 per conflict
c wchs: 1160098951 pushed, 53093867 enlarged, 205 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all         470182         25000          5585      37905187       9908567        236495
c 
c  0 0          5379   1         2   0         0   0  11184468  30   1972418  20     16680   7     0.2
c  1 5           864   0         1   0        72   1   1800595   5    284821   3      3162   1     0.1
c  2 6          2008   0        11   0        63   1   2594436   7    509136   5      7410   3     0.2
c  3 9          2599   1        40   0        61   1   3332097   9    743269   8     14834   6     0.4
c  4 14         3744   1       482   2        72   1   3777416  10<  1031802  10     14170   6     0.7
c  5 21         4014   1       586   2        79   1   2753158   7    812375   8<    15206   6     0.9
c  6 30         4303   1       722   3       124   2   2830107   7    718044   7     13362   6     1.4
c  7 41         5115   1      1048   4       141   3   2465844   7    789810   8     12556   5     1.9
c  8 54         5385   1      1338   5       170   3   1521078   4    506558   5     12997   5<    2.5
c  9 69         6333   1      1905   8       204   4   1239305   3    481478   5     18959   8     3.6
c 10 86        14879   3      4903  20<      459   8   1636692   4    722585   7     37819  16     9.9
c 11 126       26487   6<     7347  29       675  12<  1744374   5    822910   8     46339  20    18.9
c 12 230      302206  64      5418  22      2921  52    843123   2    433304   4     20135   9   141.3
c 13 534       86866  18      1197   5       544  10    182494   0     80057   1      2866   1    64.8
c 
c avg                 11.5          10.2          10.8           4.0           5.3           7.6
c std                  2.2           2.0           2.5           3.7           3.9           3.7
c 
c  145.608  15% bump
c   70.628   7% cce
c   59.296   6% probe
c   41.917   4% sweep
c   38.864   4% unhide
c   19.848   2% elim
c    4.068   0% bca
c 
c   13.509 < 1% rest (below)
c 
c    3.851   0% decide
c    3.174   0% block
c    1.926   0% transred
c    1.696   0% ternres
c    1.635   0% gauss
c    0.692   0% quatres
c    0.535   0% card
c    0.000   0% locs
c    0.000   0% queuesort
c    0.000   0% rescore
c ==================================
c    5.159   1% preprocessing     2%
c  254.006  25% inprocessing     98%
c ==================================
c  259.165  26% simplifying
c  740.047  74% search
c ==================================
c  999.216 100% all
c 
c        472216 conflicts,         472.6 confs/sec
c           883 ternaries,         534.8 confs/ternary
c           878 binaries,          537.8 confs/binary
c           121 iterations,       3902.6 confs/iteration
c 
c             1 reductions,          0.0 redus/sec, 472216.0 confs/reduction
c          6461 restarts,            6.5 rests/sec,     73.1 confs/restart
c       6301263 decisions,        6306.2 decis/sec,     13.3 decis/conflict
c    2554951530 propagations,  2556955.2 props/sec,    405.5 props/decision
c 
c 999.2 seconds, 369.3 MB
c
c CAUGHT SIGNAL 15 SIGTERM
c
c launch: done
