c launch: /data/cnf/sc2014/app/UR-15-10p1.cnf.bz2
c host: atom25
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-15-10p1.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/UR-15-10p1.cnf.bz2
c no embedded options
c found 'p cnf 199996 1019200' header
c read 199996 variables, 1019200 clauses, 2430990 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 189747 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  189747  1008281         0       0      0     0    0     0   53   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 6083 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] 6083 out of 6083 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 54081 variables
c [simpleprobe-1] all 145915 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 53 variables
c [simpleprobe-1] 237 variables remain 0% (145625 retained 100%)
c [simpleprobe-1] removed 53 variables, found 13804 hbrs, 1 units
c [unhide-1] limit 100000 with penalty 0 = 0 + 0
c [unhide-1-1] 4 units, 592 failed, 7212 tauts, 0 hbrs, 8802 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 145473 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 32892 not tried 23% in round 1
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 55795 = 38% variables out of 145473 scheduled
c [elim-1] considered successful since not run to completion yet
c [phase-count-1] 615269 negative 99.2% of 620148 except 4879 0.8%
c [phase-count-1] 489917 positive 79.0% of 620148 except 130231 21.0%
c [phase-count-1] less non-negative clauses 4879 than limit 62000 (10.0%)
c [phase-count-1] non-pos/non-neg = 130231/4879 = 26.69 >= 2.00 = 200/100
c [lucky-phase-1] forcing lucky phase -1
c [phase-1] phase bias: 0 positive 0%, 89678 negative 100%
c [sort-queue-1] sorted 89678 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 89678 (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 62173 variables 40.9% (89678 remain 47%)
c [simplification-1] removed 388133 irredundant clauses 38.5% (620148 remain 62%)
c [simplification-1] maximum reduction of 41% = max (41%, 38%)
c [simplification-1] large reduction 41% >= 5% limit
c [simplification-1] next conflict interval 1000 = 2000/2
c [simplification-1] penalized conflict interval 1000 = 1 * 1000
c [simplification-1] hard conflict limit 11000 (soft 1000 + delta 10000)
c [simplification-1] new conflict limit 1000 (hard 11000)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i    3.9   89677   620148         8       7      0  9660    0     5   43   0%      0    5    0    0 25223%
c i    4.0   89622   620148        45      39      1  9661    0     7   44   3%      0    7    3    0 24078%
c i    4.2   89606   620148       156     125     14  9669    0    19   44   2%      0   19    4    0 18434%
c i    4.5   89596   620148       272     221     23  9678    1    26   44   3%      0   26    9    0 17918%
c i    4.5   89516   620148       273     221     23  9678    1    26   44   3%      0   26    9    0 17848%
c i    5.0   89515   620148       522     424     42  9689    2    48   44   4%      1   48   14    0 11412%
c i    5.3   88830   620148       644     535     47  9691    2    63   44   4%      1   63   17    0 10778%
c i    5.7   88795   620148       842     712     55  9692    7   100   45   7%      1   99   59    0 13307%
c i    5.9   88736   620148       930     777     57  9696    9   112   45   8%      1  111   70    1 12290%
c i    5.9   88724   620148       941     782     57  9701    9   114   45   8%      1  113   67    1 11787%
c 
c [simplification-2] limit of 10 iterations hit after 10 iterations
c [decomp-3] removed 991 variables
c [simpleprobe-2] 232 schedulable variables 0%
c [simpleprobe-2] limit 2284236 penalty 0 = 0 + 0
c [simpleprobe-2] fully completed simple probing
c [simpleprobe-2] removed 0 variables, found 409 hbrs, 0 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 58578 literals 33%
c [treelook-1] scheduling used 301111 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 305761 steps
c [treelook-1] 58561 literals remain 33%
c [treelook-1] 56125 variables remain to probed next time 63%
c [treelook-1] removed 11 variables, found 1807 hbrs
c [basicprobe-1] limit 4905264 based on 613158 irredundant clauses
c [basicprobe-1-0] 32955 probes remain 39% after last round
c [basicprobe-1-0] 21 units = 21 failed (100%) + 0 lifted (0%)
c [basicprobe-1-0] removed 3577 variables, found 24450 hbrs
c [unhide-2] limit 114211 with penalty 0 = 0 + 0
c [unhide-2-2] 1 units, 1390 failed, 6287 tauts, 0 hbrs, 4017 literals
c [elim-2] 31809 variables 38% will be scheduled this time
c [elim-2] scheduled 31809 variables 38%
c [elim-2] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-2] rescheduling of touched variables disabled
c [elim-2] incomplete 10107 not tried 12% in round 1
c [elim-2] transition to [ all 0 rem 1 ] state
c [elim-2] eliminated 1 = 0% variables out of 31809 scheduled
c [elim-2] considered successful since not run to completion yet
c [phase-count-2] 567271 negative 99.1% of 572150 except 4879 0.9%
c [phase-count-2] 450502 positive 78.7% of 572150 except 121648 21.3%
c [phase-count-2] less non-negative clauses 4879 than limit 57200 (10.0%)
c [phase-count-2] non-pos/non-neg = 121648/4879 = 24.93 >= 2.00 = 200/100
c [lucky-phase-2] forcing lucky phase -1
c [phase-2] phase bias: 0 positive 0%, 1418 negative 100%
c [sort-queue-2] sorted 59331 enqueued variables after 941 conflicts
c [score-dist-2] active 24716 (29%), one 0 (0%), zero 59331 (71%)
c [score-dist-2] max exp 508, different 8 (2%)
c [score-dist-2] median active exp 504, avg 504.0
c [simplification-2] removed 4670 variables 5.3% (84047 remain 44%)
c [simplification-2] removed 47998 irredundant clauses 7.7% (572150 remain 57%)
c [simplification-2] maximum reduction of 8% = max (5%, 8%)
c [simplification-2] forced so keeping old conflict interval 0
c [simplification-2] conflict limit remains at 1011 (hard 11000)
c [simplification-2] new iteration interval 100
c 
c [simplification-3] limit 1011 conflicts (hard 11000) hit after 1011 conflicts
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 4301 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] 4301 out of 4301 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [decomp-6] removed 83 variables
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] scheduled 45436 literals 27%
c [treelook-2] scheduling used 338071 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] used 349990 steps
c [treelook-2] 45418 literals remain 27%
c [treelook-2] 31047 variables remain to probed next time 37%
c [decomp-7] removed 1 variables
c [treelook-2] removed 15 variables, found 1489 hbrs
c [unhide-3] limit 123296 with penalty 0 = 0 + 0
c [unhide-3-3] 9 units, 770 failed, 7981 tauts, 0 hbrs, 4948 literals
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 83048 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 17576 not tried 21% in round 1
c [elim-3] transition to [ all 1 rem 1 ] state
c [elim-3] eliminated 1485 = 2% variables out of 83048 scheduled
c [elim-3] considered successful since not run to completion yet
c [phase-count-3] 550472 negative 99.1% of 555316 except 4844 0.9%
c [phase-count-3] 437428 positive 78.8% of 555316 except 117888 21.2%
c [phase-count-3] less non-negative clauses 4844 than limit 55500 (10.0%)
c [phase-count-3] non-pos/non-neg = 117888/4844 = 24.34 >= 2.00 = 200/100
c [lucky-phase-3] forcing lucky phase -1
c [phase-3] phase bias: 0 positive 0%, 1417 negative 100%
c [sort-queue-3] sorted 57343 enqueued variables after 1011 conflicts
c [score-dist-3] active 24220 (30%), one 0 (0%), zero 57343 (70%)
c [score-dist-3] max exp 508, different 8 (2%)
c [score-dist-3] median active exp 504, avg 504.1
c [simplification-3] removed 2484 variables 3.0% (81563 remain 43%)
c [simplification-3] removed 16834 irredundant clauses 2.9% (555316 remain 55%)
c [simplification-3] maximum reduction of 3% = max (3%, 3%)
c [simplification-3] geometric conflict interval increment 5000 = 20000 / 4
c [simplification-3] new conflict interval 5000
c [simplification-3] penalized conflict interval 5000 = 1 * 5000
c [simplification-3] hard conflict limit 16011 (soft 6011 + delta 10000)
c [simplification-3] new conflict limit 6011 (hard 16011)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   10.8   81562   555316      1121     902     58 26909   19   141   41  14%      1  140  176    1 13927%
c i   10.8   81554   555316      1132     906     58 26909   21   142   42  14%      1  141  191    1 14100%
c i   10.9   81550   555316      1183     935     58 26910   26   151   42  17%      1  150  239    2 13896%
c i   11.0   81235   555316      1187     937     59 26910   26   151   42  17%      1  150  235    2 13690%
c i   11.1   81226   555316      1272    1014     59 26914   28   164   42  17%      1  163  203    2 10861%
c i   11.6   81217   555316      1488    1180     61 26926   47   199   42  24%      1  197  320    3 10133%
c i   11.6   81209   555316      1489    1180     61 26926   47   199   42  24%      1  197  319    3 10094%
c i   11.6   81203   555316      1490    1180     61 26926   47   199   42  24%      1  197  318    3 10055%
c i   11.6   81192   555316      1491    1180     61 26926   47   198   42  24%      1  196  317    3 10016%
c i   11.6   81184   555316      1504    1192     61 26926   48   200   42  24%      1  198  324    3 9953%
c i   11.7   81174   555316      1506    1193     61 26926   48   200   42  24%      1  198  324    3 9934%
c i   11.7   81166   555316      1524    1210     61 26926   50   203   42  25%      1  201  332    3 9810%
c i   11.7   81165   555316      1527    1210     61 26928   50   203   42  25%      1  201  328    3 9696%
c i   11.7   81153   555316      1529    1211     61 26928   50   203   42  25%      1  201  329    3 9676%
c i   11.7   81143   555316      1530    1211     61 26928   50   203   42  25%      1  201  327    3 9639%
c i   11.7   81131   555316      1531    1211     61 26928   50   203   42  25%      1  201  326    3 9601%
c i   12.9   81118   555316      2112    1656     66 26942   70   282   44  25%      3  277  184    5 3578%
c i   13.8   80507   555316      2445    1875     69 26942  102   319   46  32%      3  314  416    8 5544%
c i   13.8   80506   555316      2447    1875     69 26942  102   319   46  32%      3  314  416    8 5532%
c i   13.8   80505   555316      2449    1875     69 26942  102   319   46  32%      3  314  416    8 5519%
c i   13.8   80504   555316      2450    1875     69 26942  102   319   46  32%      3  314  414    8 5498%
c i   13.8   80503   555316      2451    1875     69 26942  102   319   46  32%      3  314  412    8 5476%
c i   13.8   80502   555316      2452    1875     69 26942  102   319   46  32%      3  314  411    8 5455%
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   14.1   80501   555316      2550    1931     69 26943  112   329   46  34%      2  323  455    8 5469%
c i   14.1   80500   555316      2554    1934     69 26943  112   330   46  34%      2  324  451    8 5416%
c i   14.1   80499   555316      2555    1934     69 26943  112   330   46  34%      2  323  450    8 5395%
c i   14.1   80498   555316      2557    1935     69 26943  112   330   46  34%      2  323  447    8 5364%
c i   14.1   80497   555316      2559    1936     69 26943  112   330   46  34%      2  323  445    8 5333%
c i   14.1   80496   555316      2560    1936     69 26943  112   330   46  34%      2  323  443    8 5312%
c i   14.1   80495   555316      2561    1936     69 26943  112   330   46  34%      2  323  441    8 5292%
c i   14.1   80494   555316      2562    1936     69 26943  112   329   46  34%      2  323  440    8 5271%
c i   14.1   80493   555316      2563    1936     69 26943  112   329   46  34%      2  323  438    8 5250%
c i   14.1   80492   555316      2564    1936     69 26943  112   329   46  34%      2  323  436    8 5230%
c i   14.2   80491   555316      2613    1979     69 26943  112   335   46  33%      2  329  377    8 4486%
c i   14.3   80476   555316      2634    1998     69 26943  112   338   46  33%      2  331  357    8 4229%
c i   14.3   80475   555316      2640    2002     69 26943  112   338   46  33%      2  332  350    8 4150%
c i   14.3   80301   555316      2644    2003     69 26943  112   339   46  33%      2  332  352    8 4153%
c i   14.3   80300   555316      2647    2005     69 26943  112   339   46  33%      2  332  351    8 4139%
c i   14.3   80299   555316      2648    2005     69 26943  112   339   46  33%      2  332  350    8 4123%
c i   14.3   80298   555316      2649    2005     69 26943  112   339   46  33%      2  332  348    8 4107%
c i   14.3   80297   555316      2650    2005     69 26943  112   338   46  33%      2  332  347    8 4091%
c i   14.4   80296   555316      2651    2005     69 26943  112   338   46  33%      2  332  345    8 4075%
c i   14.4   80295   555316      2652    2005     69 26943  112   338   46  33%      2  332  344    8 4059%
c i   14.4   80294   555316      2653    2005     69 26943  112   338   46  33%      2  332  343    8 4043%
c i   14.4   80293   555316      2656    2004     69 26943  112   338   46  33%      2  332  342    8 4029%
c i   14.6   80292   555316      2773    2091     70 26949  116   351   47  33%      2  344  303    9 3406%
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   14.8   80271   555316      2870    2166     70 26949  122   362   47  34%      2  354  323    9 3429%
c i   17.0   80265   555316      3982    2857     72 26959  181   473   51  38%      7  458  210   16 1339%
c 
c [simplification-4] limit of 143 binary hit after 143 binaries
c [decomp-8] removed 1386 variables
c [basicprobe-2] limit 16860776 penalty 0 = 0 + 0
c [basicprobe-2-0] 28819 probes remain 37% after last round
c [basicprobe-2-0] 68 units = 68 failed (100%) + 0 lifted (0%)
c [basicprobe-2-0] removed 3126 variables, found 45348 hbrs
c [unhide-4] limit 674431 with penalty 0 = 0 + 0
c [unhide-4-4] 13 units, 1023 failed, 7356 tauts, 0 hbrs, 130235 literals
c [elim-4] 9776 variables 13% will be scheduled this time
c [elim-4] scheduled 9776 variables 13%
c [elim-4] boosting limit by 20
c [elim-4] limit of 1348862100 steps penalty 0 = 0 + 0
c [elim-4] rescheduling of touched variables disabled
c [elim-4-1] no variable eliminated in round 1 in 19136552 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 9776 scheduled
c [phase-count-4] 507588 negative 99.1% of 512432 except 4844 0.9%
c [phase-count-4] 400961 positive 78.2% of 512432 except 111471 21.8%
c [phase-count-4] less non-negative clauses 4844 than limit 51200 (10.0%)
c [phase-count-4] non-pos/non-neg = 111471/4844 = 23.01 >= 2.00 = 200/100
c [lucky-phase-4] forcing lucky phase -1
c [phase-4] phase bias: 0 positive 0%, 751 negative 100%
c [sort-queue-4] sorted 44683 enqueued variables after 6006 conflicts
c [score-dist-4] active 31540 (41%), one 0 (0%), zero 44683 (59%)
c [score-dist-4] max exp 513, different 13 (3%)
c [score-dist-4] median active exp 505, avg 505.9
c [simplification-4] removed 4011 variables 5.0% (76223 remain 40%)
c [simplification-4] removed 42884 irredundant clauses 7.7% (512432 remain 51%)
c [simplification-4] maximum reduction of 8% = max (5%, 8%)
c [simplification-4] forced so keeping old conflict interval 5000
c [simplification-4] conflict limit remains at 6257 (hard 16011)
c [simplification-4] new binary interval 1000
c 
c [simplification-5] limit 6257 conflicts (hard 16011) hit after 6257 conflicts
c [quatres-1] found 30908 quaternary clauses 37% in total
c [quatres-1-2] added 1 quaternary resolvents
c [ternres-1] boosting ternary resolution limit by 5
c [ternres-1] limit 20000000 with penalty 0 = 0 + 0
c [ternres-1] all 76223 free variables schedulable
c [ternres-1] 6 ternary resolvents (0 bin, 6 trn)
c [ternres-1] fully completed ternary resolution
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 109 xors of average arity 2.4
c [gauss-1] connected 263 occurrences of 223 variables (average 1.2)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] fully completed
c [gauss-1] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-9] removed 82 variables
c [unhide-5] limit 701016 with penalty 0 = 0 + 0
c [unhide-5-5] 3 units, 275 failed, 10607 tauts, 0 hbrs, 39453 literals
c [transred-1] limit 2000000 with penalty 0 = 0 + 0
c [transred-1] removed 189 transitive binary clauses
c [transred-1] found 5 units
c [block-1] scheduling all variables this time
c [block-1] scheduled 75868 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 9331 blocked clauses
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 13 clauses out of 356 (4%) of length 10
c [cce-1-1] eliminated 67 clauses out of 1754 (4%) of length 9
c [cce-1-1] eliminated 9 clauses out of 450 (2%) of length 8
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 89 large clauses in 30000003 steps
c [cce-1-1] allowing another 15000001 steps for small clauses
c [cce-1-1] scheduling 266848 clauses = 252398 binary + 14450 ternary
c [cce-1-1] tried to eliminate 438 small clauses 0%
c [cce-1-1] eliminated 130 binary clauses 0%
c [cce-1-1] eliminated 6 ternary clauses 0%
c [cce-1-1] eliminated 136 small clauses 0%
c [cce-1-1] eliminated 136 small clauses in 30000002 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 225 covered clauses in round 1
c [cce-1] eliminated 225 covered clauses in TOTAL during 1 rounds
c [cce-1] 225 < 1/100 * 491637 = 4916 considered unsuccessful
c [bca-1] limit of 10000000 steps and 983324 added (scaled 2)
c [bca-1] 137890 out of 151738 literals actually usable 91%
c [bca-1] added 170 blocked clauses in 431533 steps
c [sweep-1] limit 1051524 penalty 0 = 0 + 0
c [sweep-1-1] 3320 pos 4.4% + 72548 neg 95.6% = 75868 sched 100.0% ret 0
c [sweep-1-1] 1085946 steps 12 queries 21602.92 avg class size
c [sweep-1-1] 102 decisions 10 SAT calls 41.40 avg env size
c [sweep-1-1] 75827 variables remain 100% (41 retained 0%)
c [decomp-10] removed 1 variables
c [sweep-1-1] removed 1 vars (0 failed, 1 eqs, 2 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 1 vars in TOTAL (1 rounds, 11 queries)
c [phase-count-5] 486586 negative 99.0% of 491410 except 4824 1.0%
c [phase-count-5] 392619 positive 79.9% of 491410 except 98791 20.1%
c [phase-count-5] less non-negative clauses 4824 than limit 49100 (10.0%)
c [phase-count-5] non-pos/non-neg = 98791/4824 = 20.48 >= 2.00 = 200/100
c [lucky-phase-5] forcing lucky phase -1
c [phase-5] phase bias: 0 positive 0%, 749 negative 100%
c [sort-queue-5] sorted 44233 enqueued variables after 6257 conflicts
c [score-dist-5] active 31634 (42%), one 0 (0%), zero 44233 (58%)
c [score-dist-5] max exp 513, different 13 (3%)
c [score-dist-5] median active exp 505, avg 506.0
c [simplification-5] removed 356 variables 0.5% (75867 remain 40%)
c [simplification-5] removed 21022 irredundant clauses 4.1% (491410 remain 49%)
c [simplification-5] maximum reduction of 4% = max (0%, 4%)
c [simplification-5] geometric conflict interval increment 4000 = 20000 / 5
c [simplification-5] new conflict interval 9000
c [simplification-5] penalized conflict interval 9000 = 1 * 9000
c [simplification-5] hard conflict limit 25257 (soft 15257 + delta 10000)
c [simplification-5] new conflict limit 15257 (hard 25257)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   28.9   75866   491410      7068    4920    138 70025  315   714   51  44%     33  673  397   34 1161%
c i   28.9   75860   491410      7069    4920    138 70025  315   713   51  44%     33  673  395   34 1157%
c i   30.7   75851   491410      7809    5468    152 70047  373   804   55  46%     18  755  799   41 1944%
c i   30.8   75850   491410      7839    5477    152 70047  379   807   55  47%     18  758  842   42 2024%
c i   30.9   75849   491410      7840    5477    152 70047  378   807   55  47%     18  758  839   42 2016%
c i   30.9   75848   491410      7841    5477    152 70047  378   806   55  47%     18  757  835   42 2008%
c i   30.9   75847   491410      7845    5478    152 70048  378   807   55  47%     18  758  831   42 1996%
c i   33.2   75846   491410      8882    6267    163 70066  452   948   66  48%     12  886  779   52 1501%
c i   33.3   75842   491410      8886    6267    163 70066  452   948   66  48%     11  886  783   52 1507%
c i   35.7   75838   491410      9764    6623    164 70066  589  1034   66  57%      9  960 1263   66 1902%
c i   36.7   75835   491410     10105    6648    164 70066  648  1060   66  61%      6  981 1315   73 1804%
c i   38.4   75834   491410     10729    6777    169 70084  719  1102   81  65%      5 1014 1084   83 1303%
c i   40.1   75827   491410     11335    7098    172 70090  755  1135   81  67%      4 1038  865   91  945%
c i   40.1   75823   491410     11338    7098    172 70090  756  1135   81  67%      4 1037  865   91  946%
c i   40.1   75819   491410     11339    7098    172 70090  755  1135   81  67%      4 1037  862   91  942%
c i   40.1   75815   491410     11340    7098    172 70090  755  1135   81  67%      4 1037  858   91  938%
c i   40.1   75811   491410     11350    7103    172 70090  755  1135   81  67%      4 1037  857   92  935%
c i   40.1   75810   491410     11351    7103    172 70090  755  1135   81  67%      4 1037  853   92  932%
c i   40.7   75809   491410     11525    7169    173 70095  767  1142   81  67%      4 1041  954   94 1014%
c i   40.9   75808   491410     11632    7243    175 70110  761  1147   81  66%      3 1044  800   95  844%
c i   40.9   75807   491410     11633    7243    175 70110  761  1146   81  66%      3 1044  797   95  840%
c i   41.0   75806   491410     11634    7243    175 70110  761  1146   81  66%      3 1044  794   95  837%
c i   41.0   75805   491410     11635    7243    175 70110  760  1146   81  66%      3 1043  791   95  834%
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   41.0   75804   491410     11636    7243    175 70110  760  1145   81  66%      3 1043  787   95  831%
c i   41.0   75803   491410     11637    7243    175 70110  760  1145   81  66%      3 1043  784   95  827%
c i   41.0   75802   491410     11638    7243    175 70110  760  1145   81  66%      3 1042  781   95  824%
c i   41.0   75801   491410     11639    7243    175 70110  760  1145   81  66%      3 1042  778   95  821%
c i   41.0   75800   491410     11640    7243    175 70110  759  1144   81  66%      3 1042  775   95  818%
c i   41.0   75799   491410     11641    7243    175 70110  759  1144   81  66%      3 1042  772   95  815%
c i   41.0   75798   491410     11642    7243    175 70110  759  1144   81  66%      3 1041  769   95  811%
c i   41.0   75797   491410     11643    7243    175 70110  759  1143   81  66%      3 1041  766   95  808%
c i   41.0   75796   491410     11644    7243    175 70110  759  1143   81  66%      3 1041  763   95  805%
c i   41.0   75795   491410     11645    7243    175 70110  759  1143   81  66%      3 1040  760   95  802%
c i   41.2   75794   491410     11720    7304    175 70112  755  1147   81  66%      3 1043  709   95  744%
c i   41.5   75790   491410     11835    7384    176 70113  751  1151   81  65%      2 1046  668   96  694%
c i   41.5   75789   491410     11836    7384    176 70113  750  1151   81  65%      2 1046  665   96  692%
c i   42.8   75788   491410     12296    7637    181 70123  769  1172   81  66%      2 1059  857  102  841%
c i   44.5   75787   491410     12811    7836    185 70125  809  1190   81  68%      3 1069 1120  110 1021%
c i   46.7   75786   491410     13329    8002    185 70138  853  1203   81  71%      3 1073 1157  118  980%
c i   47.1   75785   491410     13521    8162    185 70142  837  1206   81  69%      2 1073  800  119  671%
c i   47.3   75784   491410     13636    8239    186 70146  838  1206   81  69%      2 1072  830  120  689%
c i   47.3   75783   491410     13637    8239    186 70146  837  1206   81  69%      2 1071  827  120  686%
c i   47.3   75782   491410     13638    8239    186 70146  837  1206   81  69%      2 1071  823  120  683%
c i   47.6   75781   491410     13766    8303    187 70147  840  1207   81  70%      2 1070  872  122  714%
c i   47.7   75780   491410     13782    8307    187 70147  842  1207   81  70%      1 1070  890  122  727%
c i   47.8   75779   491410     13813    8316    190 70148  843  1206   81  70%      1 1069  904  123  736%
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   48.6   75778   491410     14139    8453    190 70155  860  1209  111  71%      1 1067 1020  127  800%
c i   48.6   75777   491410     14140    8453    190 70155  860  1209  111  71%      1 1066 1016  127  797%
c i   49.4   75776   491410     14440    8590    193 70160  863  1209  111  71%      1 1062  920  131  703%
c i   49.4   75775   491410     14441    8590    193 70160  863  1209  111  71%      1 1062  916  131  700%
c i   49.4   75774   491410     14442    8590    193 70160  863  1209  111  71%      1 1061  913  131  697%
c i   49.4   75773   491410     14443    8590    193 70160  862  1209  111  71%      1 1061  909  131  694%
c i   49.4   75772   491410     14444    8590    193 70160  862  1208  111  71%      1 1061  906  131  692%
c i   49.4   75771   491410     14445    8590    193 70160  862  1208  111  71%      1 1060  902  131  689%
c i   49.9   75770   491410     14616    8659    193 70168  866  1207  111  72%      1 1056  928  133  697%
c i   49.9   75769   491410     14617    8659    193 70168  866  1206  111  72%      1 1056  924  133  694%
c i   49.9   75768   491410     14618    8659    193 70168  866  1206  111  72%      1 1056  920  133  692%
c i   49.9   75767   491410     14619    8659    193 70168  866  1206  111  72%      1 1055  917  133  689%
c i   52.1   75766   491410     15435    9021    197 70182  874  1199  111  73%      3 1036  889  143  623%
c i   52.1   75765   491410     15436    9021    197 70182  874  1199  111  73%      3 1035  885  143  621%
c 
c [simplification-6] limit 15585 conflicts (hard 25257) hit after 15586 conflicts
c [quatres-2] found 30690 quaternary clauses 37% in total
c [ternres-2] limit 8691181 with penalty 0 = 0 + 0
c [ternres-2] all 75765 free variables schedulable
c [ternres-2] 0 ternary resolvents (0 bin, 0 trn)
c [ternres-2] fully completed ternary resolution
c [card-3] limit 1086397 penalty 2 = 2 + 0
c [card-3] found 3899 at-most-one constraints of average size 4.1
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 1086397 for elimination
c [card-3] 3899 out of 3899 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [decomp-11] removed 103 variables
c [simpleprobe-3] all 75764 free variables schedulable
c [simpleprobe-3] limit 17382363 penalty 1 = 1 + 0
c [decomp-12] removed 749 variables
c [simpleprobe-3] 18086 variables remain 24% (56929 retained 76%)
c [simpleprobe-3] removed 749 variables, found 45252 hbrs, 480 units
c [unhide-6] limit 869118 with penalty 1 = 0 + 1
c [unhide-6-6] 1 units, 321 failed, 9374 tauts, 0 hbrs, 550285 literals
c [transred-2] limit 2000000 with penalty 0 = 0 + 0
c [transred-2] removed 254 transitive binary clauses
c [transred-2] found 5 units
c [block-2] scheduling all variables this time
c [block-2] scheduled 74616 variables 100%
c [block-2] limit of 86911817 steps penalty 0 = 0 + 0
c [block-2] fully completed
c [block-2] transition to [ all 0 rem 0 ] state
c [block-2] eliminated 529 blocked clauses
c [block-2] 529 < 1/100 * 483132 = 4831 considered unsuccessful
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 74616 variables 100%
c [elim-5] limit of 86911817 steps penalty 1 = 1 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5-1] eliminated 1001 variables 1% in round 1 in 43037389 steps
c [elim-5-1] backward subsumption/strengthening limit 43037300
c [elim-5-1-1] backward checking 4439 touched variables 6%
c [elim-5-1-1] fully completed backward checking in 1 rounds
c [elim-5-1] subsumed 3 and strengthened 35 clauses in 1877510 steps
c [elim-5-1] rescheduled 87 variables 0% by backward subsumption
c [elim-5-2] eliminated 12 variables 0% in round 2 in 108022 steps
c [elim-5-2] backward subsumption/strengthening limit 108000
c [elim-5-2-1] backward checking 90 touched variables 0%
c [elim-5-2-1] incomplete backward checking 0 remain 0%
c [elim-5-2] subsumed 0 and strengthened 0 clauses in 108001 steps
c [elim-5-2] fully rescheduled 73603 variables 99%
c [elim-5] incomplete 306 not tried 0% in round 3
c [elim-5] transition to [ all 1 rem 1 ] state
c [elim-5] eliminated 1024 = 1% variables out of 74616 scheduled
c [bca-2] limit of 10000000 steps and 956727 added (scaled 2)
c [bca-2] 131652 out of 147186 literals actually usable 89%
c [bca-2] added 115 blocked clauses in 408151 steps
c [sweep-2] limit 2607354 penalty 0 = 0 + 0
c [sweep-2-1] 3437 pos 4.7% + 70120 neg 95.3% = 73557 sched 100.0% ret 35
c [sweep-2-1] 2781746 steps 29 queries 13747.79 avg class size
c [sweep-2-1] 247 decisions 22 SAT calls 119.55 avg env size
c [sweep-2-1] 73404 variables remain 100% (160 retained 0%)
c [decomp-13] removed 44 variables
c [sweep-2-1] removed 44 vars (0 failed, 7 eqs, 15 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 44 vars in TOTAL (1 rounds, 28 queries)
c [phase-count-6] 473031 negative 99.0% of 477811 except 4780 1.0%
c [phase-count-6] 379616 positive 79.4% of 477811 except 98195 20.6%
c [phase-count-6] less non-negative clauses 4780 than limit 47700 (10.0%)
c [phase-count-6] non-pos/non-neg = 98195/4780 = 20.54 >= 2.00 = 200/100
c [lucky-phase-6] forcing lucky phase -1
c [phase-6] phase bias: 0 positive 0%, 523 negative 100%
c [sort-queue-6] sorted 37061 enqueued variables after 15586 conflicts
c [score-dist-6] active 36487 (50%), one 0 (0%), zero 37061 (50%)
c [score-dist-6] max exp 515, different 15 (3%)
c [score-dist-6] median active exp 507, avg 507.4
c [simplification-6] removed 2217 variables 2.9% (73548 remain 39%)
c [simplification-6] removed 13599 irredundant clauses 2.8% (477811 remain 47%)
c [simplification-6] maximum reduction of 3% = max (3%, 3%)
c [simplification-6] geometric conflict interval increment 5000 = 20000 / 4
c [simplification-6] new conflict interval 14000
c [simplification-6] penalized conflict interval 14000 = 1 * 14000
c [simplification-6] hard conflict limit 39586 (soft 29586 + delta 10000)
c [simplification-6] new conflict limit 29586 (hard 39586)
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   59.7   73547   477811     15693    4355    189 106519  869  1200   49  72%      3 1033  798  145  550%
c i   59.7   73546   477811     15708    4369    189 106519  866  1200   49  72%      3 1032  767  145  528%
c i   65.0   73545   477811     17912    5480    195 106543  872  1185   59  74%     19  984  875  169  519%
c i   65.1   73544   477811     17913    5480    195 106543  872  1184   59  74%     19  984  871  169  517%
c i   65.1   73543   477811     17914    5480    195 106543  872  1184   59  74%     19  983  868  169  515%
c i   65.1   73542   477811     17915    5480    195 106543  871  1184   59  74%     19  983  865  169  513%
c i   65.1   73541   477811     17916    5480    195 106543  871  1183   59  74%     19  983  861  169  511%
c i   65.2   73540   477811     17956    5496    195 106544  871  1182   59  74%     18  981  859  169  508%
c i   65.2   73539   477811     17957    5496    195 106544  871  1182   59  74%     18  981  855  169  506%
c i   65.2   73538   477811     17958    5496    195 106544  870  1182   59  74%     18  980  852  169  504%
c i   65.2   73537   477811     17964    5501    195 106544  869  1181   59  74%     18  980  832  169  493%
c i   65.2   73536   477811     17966    5501    195 106545  869  1181   59  74%     18  979  826  169  489%
c i   65.2   73535   477811     17967    5501    195 106545  869  1181   59  74%     18  979  823  169  487%
c i   66.8   73534   477811     18511    5708    196 106545  876  1168   59  75%     11  959  955  175  545%
c i   66.8   73533   477811     18514    5710    196 106545  876  1168   59  75%     11  958  952  175  543%
c i   78.0   73532   477811     23017    7100    221 106577  875  1080   98  81%     51  811  771  221  349%
c i   78.0   73531   477811     23018    7100    221 106577  874  1080   98  81%     51  811  768  221  348%
c i   78.0   73530   477811     23019    7100    221 106577  874  1080   98  81%     51  810  765  221  346%
c i   78.0   73529   477811     23020    7100    221 106577  874  1080   98  81%     51  810  762  221  345%
c i   78.0   73528   477811     23021    7100    221 106577  874  1079   98  81%     51  810  759  221  344%
c i   83.5   73527   477811     25600    8394    242 106585  818  1058   98  77%     25  760  750  240  313%
c i   83.5   73526   477811     25601    8394    242 106585  817  1058   98  77%     25  760  747  240  312%
c i   83.6   73525   477811     25602    8394    242 106585  817  1057   98  77%     25  759  745  240  311%
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   83.6   73524   477811     25603    8394    242 106585  817  1057   98  77%     25  759  742  240  310%
c i   90.8   73523   477811     28958    9686    249 106606  820  1049   98  78%     33  714  671  268  250%
c i   91.1   73518   477811     29056    9736    251 106607  820  1048   98  78%     29  712  718  269  267%
c 
c [simplification-7] limit 29735 conflicts (hard 39586) hit after 29738 conflicts
c [gauss-2] limit 1591588 penalty 1 = 1 + 0
c [gauss-2] extracted 31 xors of average arity 3.0
c [gauss-2] connected 93 occurrences of 78 variables (average 1.2)
c [gauss-2] limit 1591588 penalty 1 = 1 + 0
c [gauss-2] fully completed
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-14] removed 1 variables
c [treelook-3] limit 1591588 penalty 0 = 0 + 0 boost 1
c [treelook-3] scheduled 123540 literals 85%
c [treelook-3] scheduling used 1508315 steps
c [treelook-3] scheduled completely
c [treelook-3] limit 1591588 penalty 0 = 0 + 0 boost 1
c [treelook-3] used 1640117 steps
c [treelook-3] 123520 literals remain 85%
c [treelook-3] 24325 variables remain to probed next time 33%
c [treelook-3] removed 0 variables, found 6316 hbrs
c [unhide-7] limit 1591588 with penalty 1 = 0 + 1
c [unhide-7-7] 0 units, 286 failed, 5147 tauts, 0 hbrs, 689447 literals
c [transred-3] limit 2000000 with penalty 0 = 0 + 0
c [transred-3] removed 225 transitive binary clauses
c [transred-3] found 8 units
c [cce-2] limit of 39789706 steps penalty 1 = 1 + 0
c [cce-2-1] eliminated 27 clauses out of 442 (6%) of length 8
c [cce-2-1] eliminated 112 clauses out of 721 (16%) of length 7
c [cce-2-1] eliminated 3094 clauses out of 4944 (63%) of length 6
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] eliminated 3233 large clauses in 39789713 steps
c [cce-2-1] allowing another 19894856 steps for small clauses
c [cce-2-1] scheduling 255753 clauses = 239764 binary + 15989 ternary
c [cce-2-1] tried to eliminate 644 small clauses 0%
c [cce-2-1] eliminated 169 binary clauses 0%
c [cce-2-1] eliminated 25 ternary clauses 0%
c [cce-2-1] eliminated 194 small clauses 0%
c [cce-2-1] eliminated 1811 small clauses in 39789708 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 5044 covered clauses in round 1
c [cce-2] eliminated 5044 covered clauses in TOTAL during 1 rounds
c [elim-6] 304 variables 0% will be scheduled this time
c [elim-6] scheduled 304 variables 0%
c [elim-6] limit of 318317651 steps penalty 0 = 0 + 0
c [elim-6] rescheduling of touched variables disabled
c [elim-6-1] no variable eliminated in round 1 in 1086131 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 304 scheduled
c [bca-3] limit of 10000000 steps and 932086 added (scaled 2)
c [bca-3] 128203 out of 145408 literals actually usable 88%
c [bca-3] added 47 blocked clauses in 395260 steps
c [sweep-3] limit 4774764 penalty 0 = 0 + 0
c [sweep-3-1] 3314 pos 4.6% + 69241 neg 95.4% = 72555 sched 99.8% ret 148
c [sweep-3-1] 5285288 steps 47 queries 6061.06 avg class size
c [sweep-3-1] 562 decisions 41 SAT calls 182.88 avg env size
c [sweep-3-1] 71370 variables remain 99% (959 retained 1%)
c [decomp-16] removed 379 variables
c [sweep-3-1] removed 379 vars (0 failed, 6 eqs, 8 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 379 vars in TOTAL (1 rounds, 46 queries)
c [phase-count-7] 462599 negative 99.6% of 464287 except 1688 0.4%
c [phase-count-7] 368974 positive 79.5% of 464287 except 95313 20.5%
c [phase-count-7] less non-negative clauses 1688 than limit 46400 (10.0%)
c [phase-count-7] non-pos/non-neg = 95313/1688 = 56.47 >= 2.00 = 200/100
c [lucky-phase-7] forcing lucky phase -1
c [phase-7] phase bias: 0 positive 0%, 498 negative 100%
c [sort-queue-7] sorted 34012 enqueued variables after 29738 conflicts
c [score-dist-7] active 38312 (53%), one 0 (0%), zero 34012 (47%)
c [score-dist-7] max exp 516, different 16 (3%)
c [score-dist-7] median active exp 508, avg 508.0
c [simplification-7] removed 563 variables 0.8% (72324 remain 38%)
c [simplification-7] removed 13524 irredundant clauses 2.8% (464287 remain 46%)
c [simplification-7] maximum reduction of 3% = max (1%, 3%)
c [simplification-7] geometric conflict interval increment 5000 = 20000 / 4
c [simplification-7] new conflict interval 19000
c [simplification-7] penalized conflict interval 19000 = 1 * 19000
c [simplification-7] hard conflict limit 58738 (soft 48738 + delta 10000)
c [simplification-7] new conflict limit 48738 (hard 58738)
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  103.6   72323   464287     31803   10848    279 115879  858  1038   82  83%     24  673  967  294  329%
c i  110.1   72317   464287     35122   12003    285 115892  871  1026  113  85%     30  630  668  323  207%
c i  110.1   72312   464287     35139   12015    285 115893  870  1026  113  85%     30  629  659  323  204%
c i  115.4   72311   464287     37667   12866    288 115896  858  1010  113  85%     20  590  830  343  242%
c i  126.4   72307   464287     42708   14387    301 115900  845   965  173  88%     53  504  857  379  226%
c i  129.0   72303   464287     44331   14639    303 115900  865   955  173  91%     15  481  882  391  225%
c i  129.0   72302   464287     44332   14639    303 115900  865   955  173  91%     15  481  879  391  224%
c i  129.0   72301   464287     44333   14639    303 115900  865   954  173  91%     15  481  875  391  224%
c i  129.0   72300   464287     44334   14639    303 115900  865   954  173  91%     15  481  872  391  223%
c i  129.0   72299   464287     44335   14639    303 115900  865   954  173  91%     15  481  869  391  222%
c i  129.1   72298   464287     44336   14639    303 115900  864   954  173  91%     15  480  865  391  221%
c i  129.1   72297   464287     44337   14639    303 115900  864   954  173  91%     15  480  862  391  220%
c i  129.1   72296   464287     44338   14639    303 115900  864   953  173  91%     15  480  858  391  219%
c i  129.1   72295   464287     44339   14639    303 115900  864   953  173  91%     15  480  855  391  218%
c i  129.1   72294   464287     44340   14639    303 115900  864   953  173  91%     15  479  852  391  218%
c i  129.1   72293   464287     44341   14639    303 115900  863   953  173  91%     15  479  848  391  217%
c 
c [simplification-8] limit 48838 conflicts (hard 58738) hit after 48838 conflicts
c [quatres-3] found 33412 quaternary clauses 42% in total
c [quatres-3-2] added 1 quaternary resolvents
c [ternres-3] limit 11725326 with penalty 1 = 1 + 0
c [ternres-3] all 72250 free variables schedulable
c [ternres-3] 44 ternary resolvents (0 bin, 44 trn)
c [ternres-3] fully completed ternary resolution
c [decomp-17] removed 78 variables
c [basicprobe-3] limit 117253261 penalty 0 = 0 + 0
c [basicprobe-3-0] 24172 probes remain 35% after last round
c [basicprobe-3-0] 430 units = 430 failed (100%) + 0 lifted (0%)
c [basicprobe-3-0] removed 2715 variables, found 245373 hbrs
c [bate-1] eliminated 271 asymmetric tautologies during probing
c [unhide-8] limit 1172532 with penalty 2 = 0 + 2
c [unhide-8-8] 5 units, 472 failed, 26258 tauts, 0 hbrs, 611203 literals
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 133 transitive binary clauses
c [transred-4] found 1 units
c [block-3] scheduling all variables this time
c [block-3] scheduled 69227 variables 100%
c [block-3] limit of 117253261 steps penalty 1 = 1 + 0
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 401 blocked clauses
c [block-3] 401 < 1/100 * 445760 = 4457 considered unsuccessful
c [cce-3] limit of 117253261 steps penalty 0 = 0 + 0
c [cce-3-1] eliminated 4 clauses out of 676 (1%) of length 7
c [cce-3-1] eliminated 126 clauses out of 1726 (7%) of length 6
c [cce-3-1] eliminated 5095 clauses out of 35961 (14%) of length 5
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 5225 large clauses in 117253261 steps
c [cce-3-1] allowing another 58626630 steps for small clauses
c [cce-3-1] scheduling 244796 clauses = 229194 binary + 15602 ternary
c [cce-3-1] tried to eliminate 2185 small clauses 1%
c [cce-3-1] eliminated 568 binary clauses 0%
c [cce-3-1] eliminated 73 ternary clauses 0%
c [cce-3-1] eliminated 641 small clauses 0%
c [cce-3-1] eliminated 641 small clauses in 117253268 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 5866 covered clauses in round 1
c [cce-3] eliminated 5866 covered clauses in TOTAL during 1 rounds
c [bca-4] limit of 10000000 steps and 873396 added (scaled 2)
c [bca-4] 120547 out of 138450 literals actually usable 87%
c [bca-4] added 62 blocked clauses in 354968 steps
c [sweep-4] limit 7035195 penalty 0 = 0 + 0
c [sweep-4-1] 3034 pos 4.4% + 65357 neg 95.6% = 68391 sched 98.8% ret 833
c [sweep-4-1] 7094055 steps 65 queries 5200.71 avg class size
c [sweep-4-1] 675 decisions 57 SAT calls 101.49 avg env size
c [sweep-4-1] 67238 variables remain 97% (1945 retained 3%)
c [decomp-18] removed 165 variables
c [sweep-4-1] removed 165 vars (0 failed, 8 eqs, 21 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 165 vars in TOTAL (1 rounds, 64 queries)
c [phase-count-8] 434909 negative 99.8% of 435769 except 860 0.2%
c [phase-count-8] 343390 positive 78.8% of 435769 except 92379 21.2%
c [phase-count-8] less non-negative clauses 860 than limit 43500 (10.0%)
c [phase-count-8] non-pos/non-neg = 92379/860 = 107.42 >= 2.00 = 200/100
c [lucky-phase-8] forcing lucky phase -1
c [phase-8] phase bias: 0 positive 0%, 478 negative 100%
c [sort-queue-8] sorted 30206 enqueued variables after 48838 conflicts
c [score-dist-8] active 38853 (56%), one 0 (0%), zero 30206 (44%)
c [score-dist-8] max exp 517, different 17 (3%)
c [score-dist-8] median active exp 509, avg 508.4
c [simplification-8] removed 3191 variables 4.4% (69059 remain 36%)
c [simplification-8] removed 28518 irredundant clauses 6.1% (435769 remain 43%)
c [simplification-8] maximum reduction of 6% = max (4%, 6%)
c [simplification-8] large reduction 6% >= 5% limit
c [simplification-8] next conflict interval 2000 = 2000/1
c [simplification-8] penalized conflict interval 2000 = 1 * 2000
c [simplification-8] hard conflict limit 60838 (soft 50838 + delta 10000)
c [simplification-8] new conflict limit 50838 (hard 60838)
c 
c [simplification-9] limit 50838 conflicts (hard 60838) hit after 50838 conflicts
c [quatres-4] found 33784 quaternary clauses 49% in total
c [quatres-4-1] removed 1 duplicate quaternary clauses
c [ternres-4] limit 24004628 with penalty 0 = 0 + 0
c [ternres-4] all 69059 free variables schedulable
c [ternres-4] 6 ternary resolvents (0 bin, 6 trn)
c [ternres-4] fully completed ternary resolution
c [simpleprobe-4] 17283 schedulable variables 25%
c [simpleprobe-4] limit 96018514 penalty 0 = 0 + 0
c [decomp-20] removed 448 variables
c [simpleprobe-4] fully completed simple probing
c [simpleprobe-4] removed 448 variables, found 53905 hbrs, 218 units
c [unhide-9] limit 1200231 with penalty 2 = 0 + 2
c [unhide-9-9] 3 units, 63 failed, 9549 tauts, 0 hbrs, 115146 literals
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 156 transitive binary clauses
c [transred-5] found 3 units
c [cce-4] boosting limit by 10
c [cce-4] limit of 1200231430 steps penalty 0 = 0 + 0
c [cce-4-1] eliminated 20523 clauses out of 30733 (67%) of length 5
c [cce-4-1] eliminated 20836 clauses out of 32922 (63%) of length 4
c [cce-4-1] completed large round (ATE)
c [cce-4-1] eliminated 41359 large clauses in 676558965 steps
c [cce-4-1] allowing another 338279482 steps for small clauses
c [cce-4-1] scheduling 341657 clauses = 222163 binary + 119494 ternary
c [cce-4-1] tried to eliminate 31026 small clauses 9%
c [cce-4-1] eliminated 5103 binary clauses 2%
c [cce-4-1] eliminated 1223 ternary clauses 1%
c [cce-4-1] eliminated 6326 small clauses 2%
c [cce-4-1] eliminated 7105 small clauses in 1200231441 steps
c [cce-4-1] incomplete small round (ATE)
c [cce-4-1] eliminated 48464 covered clauses in round 1
c [cce-4] eliminated 48464 covered clauses in TOTAL during 1 rounds
c [elim-7] scheduling all variables this time
c [elim-7] scheduled 68527 variables 100%
c [elim-7] limit of 240046286 steps penalty 1 = 1 + 0
c [elim-7] rescheduling of touched variables disabled
c [elim-7-1] eliminated 21070 variables 31% in round 1 in 31176349 steps
c [elim-7-1] backward subsumption/strengthening limit 31176300
c [elim-7-1-1] backward checking 41637 touched variables 61%
c [elim-7-1-1] fully completed backward checking in 1 rounds
c [elim-7-1] subsumed 11 and strengthened 45 clauses in 5526017 steps
c [elim-7-1] rescheduled 138 variables 0% by backward subsumption
c [elim-7-2] eliminated 7 variables 0% in round 2 in 85553 steps
c [elim-7-2] backward subsumption/strengthening limit 85500
c [elim-7-2-1] backward checking 68 touched variables 0%
c [elim-7-2-1] incomplete backward checking 0 remain 0%
c [elim-7-2] subsumed 0 and strengthened 3 clauses in 85501 steps
c [elim-7-2] rescheduled 9 variables 0% by backward subsumption
c [elim-7-3] no variable eliminated in round 3 in 5159 steps
c [elim-7] fully completed in 3 rounds
c [elim-7] transition to [ all 0 rem 0 ] state
c [elim-7] eliminated 21077 = 31% variables out of 68527 scheduled
c [bca-5] limit of 10000000 steps and 665629 added (scaled 2)
c [bca-5] 91479 out of 94902 literals actually usable 96%
c [bca-5] added 240 blocked clauses in 216368 steps
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 72013880 penalty 0 = 0 + 0
c [sweep-5-1] 3015 pos 6.5% + 43150 neg 93.5% = 46165 sched 97.3% ret 1285
c [sweep-5-1] 72018471 steps 1414 queries 267.90 avg class size
c [sweep-5-1] 13040 decisions 1317 SAT calls 70.82 avg env size
c [sweep-5-1] 23897 variables remain 51% (22598 retained 49%)
c [decomp-21] removed 1530 variables
c [sweep-5-1] removed 1530 vars (0 failed, 124 eqs, 262 impls)
c [sweep-5] considered successful since not run to completion yet
c [sweep-5] removed 1530 vars in TOTAL (1 rounds, 1413 queries)
c [phase-count-9] 325006 negative 99.9% of 325438 except 432 0.1%
c [phase-count-9] 243583 positive 74.8% of 325438 except 81855 25.2%
c [phase-count-9] less non-negative clauses 432 than limit 32500 (10.0%)
c [phase-count-9] non-pos/non-neg = 81855/432 = 189.48 >= 2.00 = 200/100
c [lucky-phase-9] forcing lucky phase -1
c [phase-9] phase bias: 0 positive 0%, 215 negative 100%
c [sort-queue-9] sorted 13271 enqueued variables after 50838 conflicts
c [score-dist-9] active 32649 (71%), one 0 (0%), zero 13271 (29%)
c [score-dist-9] max exp 517, different 17 (3%)
c [score-dist-9] median active exp 506, avg 507.3
c [simplification-9] removed 23139 variables 33.5% (45920 remain 24%)
c [simplification-9] removed 110331 irredundant clauses 25.3% (325438 remain 32%)
c [simplification-9] maximum reduction of 34% = max (34%, 25%)
c [simplification-9] large reduction 34% >= 5% limit
c [simplification-9] next conflict interval 2000 = 2000/1
c [simplification-9] penalized conflict interval 2000 = 1 * 2000
c [simplification-9] hard conflict limit 62838 (soft 52838 + delta 10000)
c [simplification-9] new conflict limit 52838 (hard 62838)
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  198.8   45919   325438     52442    2305   1592 370822  604   747   40  81%     95  223  305  422   72%
c 
c [simplification-10] limit 52838 conflicts (hard 62838) hit after 52840 conflicts
c [ternres-5] limit 24189713 with penalty 0 = 0 + 0
c [ternres-5] all 45919 free variables schedulable
c [ternres-5] 648 ternary resolvents (0 bin, 648 trn)
c [ternres-5] fully completed ternary resolution
c [card-4] limit 1511857 penalty 3 = 3 + 0
c [card-4] found 2359 at-most-one constraints of average size 4.4
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 1511857 for elimination
c [card-4] 2359 out of 2359 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [gauss-3] limit 1209485 penalty 2 = 2 + 0
c [gauss-3] extracted 17 xors of average arity 2.9
c [gauss-3] connected 49 occurrences of 49 variables (average 1.0)
c [gauss-3] limit 1209485 penalty 2 = 2 + 0
c [gauss-3] fully completed
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-22] removed 3 variables
c [unhide-10] limit 4837942 with penalty 0 = 0 + 0
c [unhide-10-12] 3 units, 878 failed, 52616 tauts, 0 hbrs, 12079 literals
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 172 transitive binary clauses
c [cce-5] limit of 120948567 steps penalty 0 = 0 + 0
c [cce-5-1] eliminated 2 clauses out of 56 (4%) of length 7
c [cce-5-1] eliminated 288 clauses out of 2998 (10%) of length 6
c [cce-5-1] eliminated 533 clauses out of 12796 (4%) of length 5
c [cce-5-1] incomplete large round (ACCE)
c [cce-5-1] eliminated 823 large clauses in 120948567 steps
c [cce-5-1] allowing another 60474283 steps for small clauses
c [cce-5-1] scheduling 258931 clauses = 149000 binary + 109931 ternary
c [cce-5-1] tried to eliminate 2364 small clauses 1%
c [cce-5-1] eliminated 415 binary clauses 0%
c [cce-5-1] eliminated 109 ternary clauses 0%
c [cce-5-1] eliminated 524 small clauses 0%
c [cce-5-1] eliminated 1711 small clauses in 120948568 steps
c [cce-5-1] incomplete small round (ACCE)
c [cce-5-1] eliminated 2534 covered clauses in round 1
c [cce-5] eliminated 2534 covered clauses in TOTAL during 1 rounds
c [cce-5] 2534 < 1/100 * 317145 = 3171 considered unsuccessful
c [elim-8] scheduling all variables this time
c [elim-8] scheduled 45325 variables 100%
c [elim-8] boosting limit by 20
c [elim-8] limit of 9675885400 steps penalty 0 = 0 + 0
c [elim-8] rescheduling of touched variables disabled
c [elim-8-1] eliminated 550 variables 1% in round 1 in 28133090 steps
c [elim-8-1] backward subsumption/strengthening limit 28133000
c [elim-8-1-1] backward checking 3346 touched variables 7%
c [elim-8-1-1] fully completed backward checking in 1 rounds
c [elim-8-1] subsumed 4 and strengthened 23 clauses in 1075680 steps
c [elim-8-1] rescheduled 83 variables 0% by backward subsumption
c [elim-8-2] eliminated 2 variables 0% in round 2 in 138607 steps
c [elim-8-2] backward subsumption/strengthening limit 138600
c [elim-8-2-1] backward checking 38 touched variables 0%
c [elim-8-2-1] fully completed backward checking in 1 rounds
c [elim-8-2] subsumed 0 and strengthened 0 clauses in 61571 steps
c [elim-8] fully completed in 2 rounds
c [elim-8] transition to [ all 0 rem 0 ] state
c [elim-8] eliminated 552 = 1% variables out of 45325 scheduled
c [bca-6] limit of 10000000 steps and 627645 added (scaled 2)
c [bca-6] 81031 out of 89548 literals actually usable 90%
c [bca-6] added 116 blocked clauses in 189338 steps
c [sweep-6] limit 7256914 penalty 0 = 0 + 0
c [sweep-6-1] 1951 pos 8.5% + 21127 neg 91.5% = 23078 sched 51.5% ret 21695
c [sweep-6-1] 7272635 steps 158 queries 1495.51 avg class size
c [sweep-6-1] 1788 decisions 142 SAT calls 97.27 avg env size
c [sweep-6-1] 22493 variables remain 50% (22262 retained 50%)
c [decomp-23] removed 156 variables
c [sweep-6-1] removed 156 vars (0 failed, 17 eqs, 26 impls)
c [sweep-6] considered successful since not run to completion yet
c [sweep-6] removed 156 vars in TOTAL (1 rounds, 157 queries)
c [phase-count-10] 312621 negative 99.9% of 313046 except 425 0.1%
c [phase-count-10] 233298 positive 74.5% of 313046 except 79748 25.5%
c [phase-count-10] less non-negative clauses 425 than limit 31300 (10.0%)
c [phase-count-10] non-pos/non-neg = 79748/425 = 187.64 >= 2.00 = 200/100
c [lucky-phase-10] forcing lucky phase -1
c [phase-10] phase bias: 0 positive 0%, 203 negative 100%
c [sort-queue-10] sorted 12333 enqueued variables after 52840 conflicts
c [score-dist-10] active 32284 (72%), one 0 (0%), zero 12333 (28%)
c [score-dist-10] max exp 517, different 17 (3%)
c [score-dist-10] median active exp 507, avg 507.4
c [simplification-10] removed 1302 variables 2.8% (44617 remain 24%)
c [simplification-10] removed 12392 irredundant clauses 3.8% (313046 remain 31%)
c [simplification-10] maximum reduction of 4% = max (3%, 4%)
c [simplification-10] geometric conflict interval increment 4000 = 20000 / 5
c [simplification-10] new conflict interval 23000
c [simplification-10] penalized conflict interval 23000 = 1 * 23000
c [simplification-10] hard conflict limit 87340 (soft 75840 + delta 11500)
c [simplification-10] new conflict limit 75840 (hard 87340)
c 
c [simplification-11] limit 75840 conflicts (hard 87340) hit after 87340 conflicts
c [quatres-5] found 22669 quaternary clauses 59% in total
c [quatres-5-2] added 3 single-self-subsuming ternary resolvents
c [quatres-5-2] added 20 quaternary resolvents
c [ternres-6] limit 28119261 with penalty 0 = 0 + 0
c [ternres-6] all 44617 free variables schedulable
c [ternres-6] 184 ternary resolvents (0 bin, 184 trn)
c [ternres-6] fully completed ternary resolution
c [treelook-4] limit 1405963 penalty 1 = 1 + 0 boost 1
c [treelook-4] scheduled 65700 literals 74%
c [treelook-4] scheduling used 1245185 steps
c [treelook-4] scheduled completely
c [treelook-4] limit 1405963 penalty 1 = 1 + 0 boost 1
c [treelook-4] used 1415891 steps
c [treelook-4] 65654 literals remain 74%
c [treelook-4] 10088 variables remain to probed next time 23%
c [treelook-4] removed 8 variables, found 1309 hbrs
c [unhide-11] limit 5623852 with penalty 0 = 0 + 0
c [unhide-11-16] 4 units, 302 failed, 12574 tauts, 0 hbrs, 82713 literals
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 115 transitive binary clauses
c [block-4] scheduling all variables this time
c [block-4] scheduled 44407 variables 100%
c [block-4] limit of 70298153 steps penalty 2 = 2 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 305 blocked clauses
c [block-4] 305 < 1/100 * 308886 = 3088 considered unsuccessful
c [elim-9] scheduling all variables this time
c [elim-9] scheduled 44407 variables 100%
c [elim-9] limit of 562385226 steps penalty 0 = 0 + 0
c [elim-9] rescheduling of touched variables disabled
c [elim-9-1] eliminated 420 variables 1% in round 1 in 28419930 steps
c [elim-9-1] backward subsumption/strengthening limit 28419900
c [elim-9-1-1] backward checking 2298 touched variables 5%
c [elim-9-1-1] fully completed backward checking in 1 rounds
c [elim-9-1] subsumed 0 and strengthened 14 clauses in 705544 steps
c [elim-9-1] rescheduled 36 variables 0% by backward subsumption
c [elim-9-2] eliminated 2 variables 0% in round 2 in 20152 steps
c [elim-9-2] backward subsumption/strengthening limit 20100
c [elim-9-2-1] backward checking 13 touched variables 0%
c [elim-9-2-1] incomplete backward checking 0 remain 0%
c [elim-9-2] subsumed 0 and strengthened 0 clauses in 20101 steps
c [elim-9-2] fully rescheduled 43985 variables 99%
c [elim-9-3] eliminated 2 variables 0% in round 3 in 28319827 steps
c [elim-9-3] backward subsumption/strengthening limit 28319800
c [elim-9-3-1] backward checking 17 touched variables 0%
c [elim-9-3-1] fully completed backward checking in 1 rounds
c [elim-9-3] subsumed 0 and strengthened 0 clauses in 43322 steps
c [elim-9] fully completed in 3 rounds
c [elim-9] transition to [ all 0 rem 0 ] state
c [elim-9] eliminated 424 = 1% variables out of 44407 scheduled
c [elim-9] 424 < 1/100 * 44407 = 444 considered unsuccessful
c [bca-7] limit of 10000000 steps and 616111 added (scaled 2)
c [bca-7] 77259 out of 87968 literals actually usable 88%
c [bca-7] added 66 blocked clauses in 185295 steps
c [sweep-7] limit 8435778 penalty 0 = 0 + 0
c [sweep-7-1] 1874 pos 8.5% + 20183 neg 91.5% = 22057 sched 50.1% ret 21926
c [sweep-7-1] 8437827 steps 226 queries 1404.49 avg class size
c [sweep-7-1] 2747 decisions 213 SAT calls 96.92 avg env size
c [sweep-7-1] 20933 variables remain 48% (22784 retained 52%)
c [decomp-26] removed 318 variables
c [sweep-7-1] removed 318 vars (0 failed, 17 eqs, 35 impls)
c [sweep-7] removed 318 vars in TOTAL (1 rounds, 225 queries)
c [phase-count-11] 305967 negative 99.9% of 306390 except 423 0.1%
c [phase-count-11] 228220 positive 74.5% of 306390 except 78170 25.5%
c [phase-count-11] skipping relative phase luck test
c [phase-11] phase bias: 25 positive 100%, 0 negative 0%
c [sort-queue-11] sorted 11405 enqueued variables after 87340 conflicts
c [score-dist-11] active 32260 (74%), one 0 (0%), zero 11405 (26%)
c [score-dist-11] max exp 518, different 18 (3%)
c [score-dist-11] median active exp 508, avg 508.1
c [simplification-11] removed 952 variables 2.1% (43665 remain 23%)
c [simplification-11] removed 6656 irredundant clauses 2.1% (306390 remain 30%)
c [simplification-11] maximum reduction of 2% = max (2%, 2%)
c [simplification-11] geometric conflict interval increment 7666 = 23000 / 3
c [simplification-11] new conflict interval 30666
c [simplification-11] penalized conflict interval 30666 = 1 * 30666
c [simplification-11] hard conflict limit 133339 (soft 118006 + delta 15333)
c [simplification-11] new conflict limit 118006 (hard 133339)
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  236.0   43664   306390     90201    8577   2144 291846  359   432   60  83%    430  -46  269  389   69%
c i  238.7   43661   306390     93295    9876   2154 291858  357   464   70  77%    -85  -13  359  388   93%
c 
c [simplification-12] limit 118006 conflicts (hard 133339) hit after 118006 conflicts
c [quatres-6] found 22332 quaternary clauses 59% in total
c [quatres-6-2] added 6 quaternary resolvents
c [ternres-7] limit 34492652 with penalty 0 = 0 + 0
c [ternres-7] all 43660 free variables schedulable
c [ternres-7] 190 ternary resolvents (0 bin, 190 trn)
c [ternres-7] fully completed ternary resolution
c [decomp-27] removed 5 variables
c [basicprobe-4] limit 172463262 penalty 0 = 0 + 0
c [basicprobe-4-0] 6769 probes remain 16% after last round
c [basicprobe-4-0] 746 units = 699 failed (94%) + 47 lifted (6%)
c [basicprobe-4-0] removed 1168 variables, found 427204 hbrs
c [bate-2] eliminated 1440 asymmetric tautologies during probing
c [unhide-12] limit 3449265 with penalty 1 = 0 + 1
c [unhide-12-18] 4 units, 187 failed, 45898 tauts, 0 hbrs, 146865 literals
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 138 transitive binary clauses
c [transred-8] found 1 units
c [cce-6] limit of 86231631 steps penalty 1 = 1 + 0
c [cce-6-1] eliminated 1 clauses out of 2623 (0%) of length 6
c [cce-6-1] eliminated 301 clauses out of 11392 (3%) of length 5
c [cce-6-1] incomplete large round (ATE)
c [cce-6-1] eliminated 302 large clauses in 86231633 steps
c [cce-6-1] allowing another 43115816 steps for small clauses
c [cce-6-1] scheduling 158255 clauses = 142100 binary + 16155 ternary
c [cce-6-1] tried to eliminate 2545 small clauses 2%
c [cce-6-1] eliminated 543 binary clauses 0%
c [cce-6-1] eliminated 75 ternary clauses 0%
c [cce-6-1] eliminated 618 small clauses 0%
c [cce-6-1] eliminated 771 small clauses in 86231631 steps
c [cce-6-1] incomplete small round (ATE)
c [cce-6-1] eliminated 1073 covered clauses in round 1
c [cce-6] eliminated 1073 covered clauses in TOTAL during 1 rounds
c [cce-6] 1073 < 1/100 * 291224 = 2912 considered unsuccessful
c [bca-8] limit of 10000000 steps and 581210 added (scaled 2)
c [bca-8] 72829 out of 84842 literals actually usable 86%
c [bca-8] added 29 blocked clauses in 180613 steps
c [sweep-8] limit 10347795 penalty 0 = 0 + 0
c [sweep-8-1] 1852 pos 9.1% + 18489 neg 90.9% = 20341 sched 48.0% ret 22079
c [sweep-8-1] 10394190 steps 209 queries 1118.25 avg class size
c [sweep-8-1] 2138 decisions 194 SAT calls 107.55 avg env size
c [sweep-8-1] 19348 variables remain 46% (22957 retained 54%)
c [decomp-28] removed 197 variables
c [sweep-8-1] removed 197 vars (0 failed, 16 eqs, 31 impls)
c [sweep-8] removed 197 vars in TOTAL (1 rounds, 208 queries)
c [phase-count-12] 289177 negative 99.9% of 289599 except 422 0.1%
c [phase-count-12] 214712 positive 74.1% of 289599 except 74887 25.9%
c [phase-count-12] skipping relative phase luck test
c [phase-12] phase bias: 3 positive 100%, 0 negative 0%
c [sort-queue-12] sorted 10480 enqueued variables after 118006 conflicts
c [score-dist-12] active 31743 (75%), one 0 (0%), zero 10480 (25%)
c [score-dist-12] max exp 518, different 18 (3%)
c [score-dist-12] median active exp 508, avg 508.7
c [simplification-12] removed 1437 variables 3.3% (42223 remain 22%)
c [simplification-12] removed 16791 irredundant clauses 5.5% (289599 remain 29%)
c [simplification-12] maximum reduction of 5% = max (3%, 5%)
c [simplification-12] large reduction 5% >= 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 130006 (soft 120006 + delta 10000)
c [simplification-12] new conflict limit 120006 (hard 130006)
c 
c [simplification-13] limit 120006 conflicts (hard 130006) hit after 120010 conflicts
c [quatres-7] found 21080 quaternary clauses 59% in total
c [ternres-8] limit 34969696 with penalty 0 = 0 + 0
c [ternres-8] all 42223 free variables schedulable
c [ternres-8] 496 ternary resolvents (0 bin, 496 trn)
c [ternres-8] fully completed ternary resolution
c [simpleprobe-5] all 42223 free variables schedulable
c [simpleprobe-5] limit 139878784 penalty 0 = 0 + 0
c [decomp-30] removed 217 variables
c [simpleprobe-5] 568 variables remain 1% (41438 retained 99%)
c [simpleprobe-5] removed 217 variables, found 141067 hbrs, 119 units
c [unhide-13] limit 3496969 with penalty 1 = 0 + 1
c [unhide-13-20] 5 units, 23 failed, 54226 tauts, 0 hbrs, 122473 literals
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 239 transitive binary clauses
c [elim-10] scheduling all variables this time
c [elim-10] scheduled 41925 variables 100%
c [elim-10] limit of 349696961 steps penalty 1 = 1 + 0
c [elim-10] rescheduling of touched variables disabled
c [elim-10-1] eliminated 729 variables 2% in round 1 in 27071039 steps
c [elim-10-1] backward subsumption/strengthening limit 27071000
c [elim-10-1-1] backward checking 3987 touched variables 10%
c [elim-10-1-1] fully completed backward checking in 1 rounds
c [elim-10-1] subsumed 6 and strengthened 32 clauses in 1109917 steps
c [elim-10-1] rescheduled 66 variables 0% by backward subsumption
c [elim-10-2] eliminated 4 variables 0% in round 2 in 42057 steps
c [elim-10-2] backward subsumption/strengthening limit 42000
c [elim-10-2-1] backward checking 46 touched variables 0%
c [elim-10-2-1] incomplete backward checking 0 remain 0%
c [elim-10-2] subsumed 0 and strengthened 0 clauses in 42001 steps
c [elim-10-2] fully rescheduled 41192 variables 98%
c [elim-10-3] eliminated 45 variables 0% in round 3 in 27104110 steps
c [elim-10-3] backward subsumption/strengthening limit 27104100
c [elim-10-3-1] backward checking 262 touched variables 1%
c [elim-10-3-1] fully completed backward checking in 1 rounds
c [elim-10-3] subsumed 0 and strengthened 0 clauses in 110850 steps
c [elim-10] fully completed in 3 rounds
c [elim-10] transition to [ all 0 rem 0 ] state
c [elim-10] eliminated 778 = 2% variables out of 41925 scheduled
c [bca-9] limit of 10000000 steps and 571200 added (scaled 2)
c [bca-9] 70370 out of 82296 literals actually usable 86%
c [bca-9] added 85 blocked clauses in 173390 steps
c [sweep-9] limit 10490908 penalty 0 = 0 + 0
c [sweep-9-1] 1820 pos 9.7% + 16873 neg 90.3% = 18693 sched 45.4% ret 22454
c [sweep-9-1] 10528281 steps 313 queries 791.04 avg class size
c [sweep-9-1] 3402 decisions 292 SAT calls 101.24 avg env size
c [sweep-9-1] 17347 variables remain 42% (23792 retained 58%)
c [decomp-31] removed 51 variables
c [sweep-9-1] removed 51 vars (0 failed, 21 eqs, 41 impls)
c [sweep-9] removed 51 vars in TOTAL (1 rounds, 312 queries)
c [phase-count-13] 284582 negative 99.9% of 284995 except 413 0.1%
c [phase-count-13] 210951 positive 74.0% of 284995 except 74044 26.0%
c [phase-count-13] skipping relative phase luck test
c [phase-13] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-13] sorted 9975 enqueued variables after 120010 conflicts
c [score-dist-13] active 31121 (76%), one 0 (0%), zero 9975 (24%)
c [score-dist-13] max exp 518, different 18 (3%)
c [score-dist-13] median active exp 508, avg 508.7
c [simplification-13] removed 1127 variables 2.7% (41096 remain 22%)
c [simplification-13] removed 4604 irredundant clauses 1.6% (284995 remain 28%)
c [simplification-13] maximum reduction of 3% = max (3%, 2%)
c [simplification-13] geometric conflict interval increment 7666 = 30666 / 4
c [simplification-13] new conflict interval 38332
c [simplification-13] penalized conflict interval 38332 = 1 * 38332
c [simplification-13] hard conflict limit 177508 (soft 158342 + delta 19166)
c [simplification-13] new conflict limit 158342 (hard 177508)
c 
c [simplification-14] limit 158342 conflicts (hard 177508) hit after 158342 conflicts
c [ternres-9] limit 45578258 with penalty 0 = 0 + 0
c [ternres-9] all 41096 free variables schedulable
c [ternres-9] 337 ternary resolvents (0 bin, 337 trn)
c [ternres-9] fully completed ternary resolution
c [gauss-4] limit 1139456 penalty 3 = 3 + 0
c [gauss-4] extracted 10 xors of average arity 3.0
c [gauss-4] connected 30 occurrences of 30 variables (average 1.0)
c [gauss-4] limit 1139456 penalty 3 = 3 + 0
c [gauss-4] fully completed
c [gauss-4] exported 0 unary, 0 binary and 0 ternary equations
c [treelook-5] limit 4557825 penalty 0 = 0 + 0 boost 1
c [treelook-5] scheduled 61091 literals 74%
c [treelook-5] scheduling used 1556766 steps
c [treelook-5] scheduled completely
c [treelook-5] limit 4557825 penalty 0 = 0 + 0 boost 1
c [treelook-5] used 4632409 steps
c [treelook-5] 60995 literals remain 74%
c [treelook-5] 9310 variables remain to probed next time 23%
c [treelook-5] removed 4 variables, found 18436 hbrs
c [unhide-14] limit 2278912 with penalty 2 = 0 + 2
c [unhide-14-21] 0 units, 37 failed, 24693 tauts, 0 hbrs, 301067 literals
c [transred-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 182 transitive binary clauses
c [elim-11] scheduling all variables this time
c [elim-11] scheduled 41079 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 5 variables 0% in round 1 in 27107500 steps
c [elim-11-1] backward subsumption/strengthening limit 27107500
c [elim-11-1-1] backward checking 60 touched variables 0%
c [elim-11-1-1] fully completed backward checking in 1 rounds
c [elim-11-1] subsumed 1 and strengthened 1 clauses in 114105 steps
c [elim-11-1] rescheduled 7 variables 0% by backward subsumption
c [elim-11-2] no variable eliminated in round 2 in 3527 steps
c [elim-11] fully completed in 2 rounds
c [elim-11] transition to [ all 0 rem 0 ] state
c [elim-11] eliminated 5 = 0% variables out of 41079 scheduled
c [elim-11] 5 < 1/100 * 41079 = 410 considered unsuccessful
c [bca-10] limit of 10000000 steps and 570533 added (scaled 2)
c [bca-10] 68608 out of 82150 literals actually usable 84%
c [bca-10] added 51 blocked clauses in 180725 steps
c [sweep-10] limit 13673477 penalty 0 = 0 + 0
c [sweep-10-1] 1646 pos 9.5% + 15670 neg 90.5% = 17316 sched 42.2% ret 23758
c [sweep-10-1] 13696676 steps 389 queries 522.65 avg class size
c [sweep-10-1] 3918 decisions 360 SAT calls 113.77 avg env size
c [sweep-10-1] 15671 variables remain 38% (25286 retained 62%)
c [decomp-34] removed 224 variables
c [sweep-10-1] removed 224 vars (0 failed, 30 eqs, 68 impls)
c [sweep-10] removed 224 vars in TOTAL (1 rounds, 388 queries)
c [phase-count-14] 283625 negative 99.9% of 284038 except 413 0.1%
c [phase-count-14] 210468 positive 74.1% of 284038 except 73570 25.9%
c [phase-count-14] skipping relative phase luck test
c [phase-14] phase bias: 0 positive 0%, 1 negative 100%
c [sort-queue-14] sorted 9380 enqueued variables after 158342 conflicts
c [score-dist-14] active 31470 (77%), one 0 (0%), zero 9380 (23%)
c [score-dist-14] max exp 519, different 19 (4%)
c [score-dist-14] median active exp 509, avg 509.2
c [simplification-14] removed 246 variables 0.6% (40850 remain 22%)
c [simplification-14] removed 957 irredundant clauses 0.3% (284038 remain 28%)
c [simplification-14] maximum reduction of 1% = max (1%, 0%)
c [simplification-14] geometric conflict interval increment 19166 = 38332 / 2
c [simplification-14] new conflict interval 57498
c [simplification-14] penalized conflict interval 57498 = 1 * 57498
c [simplification-14] hard conflict limit 244589 (soft 215840 + delta 28749)
c [simplification-14] new conflict limit 215840 (hard 244589)
c 
c [simplification-15] limit 215840 conflicts (hard 244589) hit after 215841 conflicts
c [quatres-8] found 19703 quaternary clauses 56% in total
c [quatres-8-1] removed 1 duplicate quaternary clauses
c [quatres-8-2] added 2 single-self-subsuming ternary resolvents
c [quatres-8-2] added 2 quaternary resolvents
c [ternres-10] limit 65663827 with penalty 0 = 0 + 0
c [ternres-10] all 40850 free variables schedulable
c [ternres-10] 139 ternary resolvents (0 bin, 139 trn)
c [ternres-10] fully completed ternary resolution
c [card-5] limit 2051994 penalty 4 = 4 + 0
c [card-5] found 1304 at-most-one constraints of average size 4.1
c [card-5] no at-most-two constraint found
c [card-5] using previous limit 2051994 for elimination
c [card-5] 1304 out of 1304 constraints (100%) meet size limits
c [card-5] no units found
c [card-5] no at-most-one constraints generated
c [basicprobe-5] limit 328319137 penalty 0 = 0 + 0
c [basicprobe-5-0] 6858 sched 17%, 619 failed, 21 lifted, 308232 hbrs
c [decomp-36] removed 1080 variables
c [basicprobe-5-1] 8559 probes remain 22% after last round
c [basicprobe-5-1] 749 units = 724 failed (97%) + 25 lifted (3%)
c [basicprobe-5-1] removed 1470 variables, found 406969 hbrs
c [bate-3] eliminated 1024 asymmetric tautologies during probing
c [unhide-15] limit 1641595 with penalty 3 = 0 + 3
c [unhide-15-22] 1 units, 2 failed, 5392 tauts, 0 hbrs, 585091 literals
c [transred-11] limit 2000000 with penalty 0 = 0 + 0
c [transred-11] removed 248 transitive binary clauses
c [block-5] scheduling all variables this time
c [block-5] scheduled 39377 variables 100%
c [block-5] limit of 82079784 steps penalty 3 = 3 + 0
c [block-5] fully completed
c [block-5] transition to [ all 0 rem 0 ] state
c [block-5] eliminated 80 blocked clauses
c [block-5] 80 < 1/100 * 269204 = 2692 considered unsuccessful
c [cce-7] limit of 82079784 steps penalty 2 = 2 + 0
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 61
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 60
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 59
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 58
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 57
c [cce-7-1] eliminated 1 clauses out of 3 (33%) of length 56
c [cce-7-1] eliminated 3 clauses out of 3 (100%) of length 55
c [cce-7-1] eliminated 3 clauses out of 4 (75%) of length 54
c [cce-7-1] eliminated 3 clauses out of 4 (75%) of length 53
c [cce-7-1] eliminated 3 clauses out of 4 (75%) of length 52
c [cce-7-1] eliminated 3 clauses out of 4 (75%) of length 51
c [cce-7-1] eliminated 3 clauses out of 4 (75%) of length 50
c [cce-7-1] eliminated 3 clauses out of 4 (75%) of length 49
c [cce-7-1] eliminated 3 clauses out of 4 (75%) of length 48
c [cce-7-1] eliminated 3 clauses out of 4 (75%) of length 47
c [cce-7-1] eliminated 3 clauses out of 4 (75%) of length 46
c [cce-7-1] eliminated 3 clauses out of 4 (75%) of length 45
c [cce-7-1] eliminated 3 clauses out of 4 (75%) of length 44
c [cce-7-1] eliminated 3 clauses out of 4 (75%) of length 43
c [cce-7-1] eliminated 3 clauses out of 4 (75%) of length 42
c [cce-7-1] eliminated 3 clauses out of 4 (75%) of length 41
c [cce-7-1] eliminated 3 clauses out of 4 (75%) of length 40
c [cce-7-1] eliminated 3 clauses out of 4 (75%) of length 39
c [cce-7-1] eliminated 3 clauses out of 4 (75%) of length 38
c [cce-7-1] eliminated 3 clauses out of 4 (75%) of length 37
c [cce-7-1] eliminated 3 clauses out of 4 (75%) of length 36
c [cce-7-1] eliminated 3 clauses out of 4 (75%) of length 35
c [cce-7-1] eliminated 3 clauses out of 4 (75%) of length 34
c [cce-7-1] eliminated 3 clauses out of 4 (75%) of length 33
c [cce-7-1] eliminated 3 clauses out of 4 (75%) of length 32
c [cce-7-1] eliminated 3 clauses out of 4 (75%) of length 31
c [cce-7-1] eliminated 3 clauses out of 5 (60%) of length 30
c [cce-7-1] eliminated 5 clauses out of 6 (83%) of length 29
c [cce-7-1] eliminated 4 clauses out of 6 (67%) of length 28
c [cce-7-1] eliminated 5 clauses out of 6 (83%) of length 27
c [cce-7-1] eliminated 4 clauses out of 6 (67%) of length 26
c [cce-7-1] eliminated 5 clauses out of 6 (83%) of length 25
c [cce-7-1] eliminated 4 clauses out of 7 (57%) of length 24
c [cce-7-1] eliminated 7 clauses out of 8 (88%) of length 23
c [cce-7-1] eliminated 5 clauses out of 9 (56%) of length 22
c [cce-7-1] eliminated 9 clauses out of 10 (90%) of length 21
c [cce-7-1] eliminated 6 clauses out of 11 (55%) of length 20
c [cce-7-1] eliminated 10 clauses out of 11 (91%) of length 19
c [cce-7-1] eliminated 8 clauses out of 13 (62%) of length 18
c [cce-7-1] eliminated 13 clauses out of 16 (81%) of length 17
c [cce-7-1] eliminated 9 clauses out of 17 (53%) of length 16
c [cce-7-1] eliminated 19 clauses out of 20 (95%) of length 15
c [cce-7-1] eliminated 11 clauses out of 21 (52%) of length 14
c [cce-7-1] eliminated 20 clauses out of 24 (83%) of length 13
c [cce-7-1] eliminated 19 clauses out of 29 (66%) of length 12
c [cce-7-1] eliminated 22 clauses out of 29 (76%) of length 11
c [cce-7-1] eliminated 25 clauses out of 32 (78%) of length 10
c [cce-7-1] eliminated 24 clauses out of 39 (62%) of length 9
c [cce-7-1] eliminated 34 clauses out of 41 (83%) of length 8
c [cce-7-1] eliminated 29 clauses out of 92 (32%) of length 7
c [cce-7-1] eliminated 39 clauses out of 2605 (1%) of length 6
c [cce-7-1] eliminated 38 clauses out of 9962 (0%) of length 5
c [cce-7-1] incomplete large round (ACCE)
c [cce-7-1] eliminated 461 large clauses in 82079787 steps
c [cce-7-1] allowing another 41039893 steps for small clauses
c [cce-7-1] scheduling 223917 clauses = 136466 binary + 87451 ternary
c [cce-7-1] tried to eliminate 1967 small clauses 1%
c [cce-7-1] eliminated 322 binary clauses 0%
c [cce-7-1] eliminated 64 ternary clauses 0%
c [cce-7-1] eliminated 386 small clauses 0%
c [cce-7-1] eliminated 386 small clauses in 82079789 steps
c [cce-7-1] incomplete small round (ACCE)
c [cce-7-1] eliminated 847 covered clauses in round 1
c [cce-7] eliminated 847 covered clauses in TOTAL during 1 rounds
c [cce-7] 847 < 1/100 * 269097 = 2690 considered unsuccessful
c [bca-11] limit of 10000000 steps and 537490 added (scaled 2)
c [bca-11] 64097 out of 78756 literals actually usable 81%
c [bca-11] added 6 blocked clauses in 189684 steps
c [sweep-11] boosting sweeping limit by 10
c [sweep-11] limit 196991480 penalty 0 = 0 + 0
c [sweep-11-1] 1627 pos 10.9% + 13232 neg 89.1% = 14859 sched 37.7% ret 24518
c [sweep-11-1] 173864806 steps 5220 queries 37.62 avg class size
c [sweep-11-1] 32510 decisions 4270 SAT calls 94.45 avg env size
c [sweep-11-1] fully completed sweeping round
c [decomp-37] removed 1251 variables
c [sweep-11-1] removed 1251 vars (3 failed, 967 eqs, 1195 impls)
c [sweep-11-2] 2975 pos 7.8% + 35151 neg 92.2% = 38126 sched 100.0% ret 0
c [sweep-11-2] 23184522 steps 355 queries 537.52 avg class size
c [sweep-11-2] 6651 decisions 350 SAT calls 271.83 avg env size
c [sweep-11-2] 28853 variables remain 76% (9229 retained 24%)
c [decomp-38] removed 51 variables
c [sweep-11-2] removed 51 vars (0 failed, 8 eqs, 30 impls)
c [sweep-11] removed 1302 vars in TOTAL (2 rounds, 5573 queries)
c [phase-count-15] 264905 negative 99.8% of 265321 except 416 0.2%
c [phase-count-15] 196937 positive 74.2% of 265321 except 68384 25.8%
c [phase-count-15] skipping relative phase luck test
c [phase-15] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-15] sorted 8177 enqueued variables after 215841 conflicts
c [score-dist-15] active 29898 (79%), one 0 (0%), zero 8177 (21%)
c [score-dist-15] max exp 519, different 19 (4%)
c [score-dist-15] median active exp 510, avg 509.8
c [simplification-15] removed 2775 variables 6.8% (38075 remain 20%)
c [simplification-15] removed 18717 irredundant clauses 6.6% (265321 remain 26%)
c [simplification-15] maximum reduction of 7% = max (7%, 7%)
c [simplification-15] large reduction 7% >= 5% limit
c [simplification-15] next conflict interval 2158 = min (215841/100, 57498)
c [simplification-15] penalized conflict interval 2158 = 1 * 2158
c [simplification-15] hard conflict limit 227999 (soft 217999 + delta 10000)
c [simplification-15] new conflict limit 217999 (hard 227999)
c 
c [simplification-16] limit 217999 conflicts (hard 227999) hit after 218000 conflicts
c [quatres-9] found 17605 quaternary clauses 54% in total
c [quatres-9-1] removed 2 duplicate quaternary clauses
c [quatres-9-2] added 1 quaternary resolvents
c [ternres-11] limit 66505808 with penalty 0 = 0 + 0
c [ternres-11] all 38075 free variables schedulable
c [ternres-11] 503 ternary resolvents (1 bin, 502 trn)
c [ternres-11] fully completed ternary resolution
c [decomp-39] removed 1 variables
c [simpleprobe-6] 535 schedulable variables 1%
c [simpleprobe-6] limit 200000000 penalty 0 = 0 + 0
c [decomp-40] removed 90 variables
c [simpleprobe-6] 1866 variables remain 5% (36118 retained 95%)
c [simpleprobe-6] removed 90 variables, found 106459 hbrs, 49 units
c [unhide-16] limit 1662645 with penalty 3 = 0 + 3
c [unhide-16-23] 1 units, 21 failed, 172661 tauts, 0 hbrs, 366670 literals
c [transred-12] limit 2000000 with penalty 0 = 0 + 0
c [transred-12] removed 314 transitive binary clauses
c [elim-12] scheduling all variables this time
c [elim-12] scheduled 37958 variables 100%
c [elim-12] limit of 400000000 steps penalty 1 = 1 + 0
c [elim-12] rescheduling of touched variables disabled
c [elim-12-1] eliminated 647 variables 2% in round 1 in 24374172 steps
c [elim-12-1] backward subsumption/strengthening limit 24374100
c [elim-12-1-1] backward checking 3873 touched variables 10%
c [elim-12-1-1] fully completed backward checking in 1 rounds
c [elim-12-1] subsumed 7 and strengthened 7 clauses in 1020371 steps
c [elim-12-1] rescheduled 31 variables 0% by backward subsumption
c [elim-12-2] eliminated 3 variables 0% in round 2 in 15740 steps
c [elim-12-2] backward subsumption/strengthening limit 15700
c [elim-12-2-1] backward checking 39 touched variables 0%
c [elim-12-2-1] incomplete backward checking 7 remain 18%
c [elim-12-2] subsumed 6 and strengthened 0 clauses in 15712 steps
c [elim-12-2] rescheduled 8 variables 0% by backward subsumption
c [elim-12-3] no variable eliminated in round 3 in 9034 steps
c [elim-12] fully completed in 3 rounds
c [elim-12] transition to [ all 0 rem 0 ] state
c [elim-12] eliminated 650 = 2% variables out of 37958 scheduled
c [bca-12] limit of 10000000 steps and 526797 added (scaled 2)
c [bca-12] 58379 out of 74618 literals actually usable 78%
c [bca-12] added 24 blocked clauses in 174477 steps
c [sweep-12] limit 19951742 penalty 0 = 0 + 0
c [sweep-12-1] 2672 pos 9.5% + 25579 neg 90.5% = 28251 sched 75.7% ret 9057
c [sweep-12-1] 20024995 steps 381 queries 465.36 avg class size
c [sweep-12-1] 5553 decisions 369 SAT calls 181.55 avg env size
c [sweep-12-1] 23597 variables remain 63% (13684 retained 37%)
c [decomp-41] removed 39 variables
c [sweep-12-1] removed 39 vars (0 failed, 12 eqs, 33 impls)
c [sweep-12] removed 39 vars in TOTAL (1 rounds, 380 queries)
c [phase-count-16] 261892 negative 99.8% of 262306 except 414 0.2%
c [phase-count-16] 194559 positive 74.2% of 262306 except 67747 25.8%
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 7989 enqueued variables after 218000 conflicts
c [score-dist-16] active 29280 (79%), one 0 (0%), zero 7989 (21%)
c [score-dist-16] max exp 519, different 19 (4%)
c [score-dist-16] median active exp 510, avg 509.9
c [simplification-16] removed 806 variables 2.1% (37269 remain 20%)
c [simplification-16] removed 3015 irredundant clauses 1.1% (262306 remain 26%)
c [simplification-16] maximum reduction of 2% = max (2%, 1%)
c [simplification-16] geometric conflict interval increment 19166 = 57498 / 3
c [simplification-16] new conflict interval 76664
c [simplification-16] penalized conflict interval 76664 = 1 * 76664
c [simplification-16] hard conflict limit 332996 (soft 294664 + delta 38332)
c [simplification-16] new conflict limit 294664 (hard 332996)
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  467.2   37268   262306    218378   48757   4379 921671  460   641  218  72%    848   33  412  492   84%
c i  467.4   37255   262306    218525   48874   4379 921671  462   644  218  72%    587   37  448  492   91%
c -  479.0   37252   262306    226166   22924   4386 921672  523   657   79  80%   -896   43  459  498   92%
c 
c [simplification-17] limit 294664 conflicts (hard 332996) hit after 294715 conflicts
c [quatres-10] found 17343 quaternary clauses 52% in total
c [ternres-12] limit 91130655 with penalty 0 = 0 + 0
c [ternres-12] all 37252 free variables schedulable
c [ternres-12] 150 ternary resolvents (0 bin, 150 trn)
c [ternres-12] fully completed ternary resolution
c [decomp-42] removed 17 variables
c [treelook-6] limit 9113065 penalty 0 = 0 + 0 boost 1
c [treelook-6] scheduled 56375 literals 76%
c [treelook-6] scheduling used 1745477 steps
c [treelook-6] scheduled completely
c [treelook-6] limit 9113065 penalty 0 = 0 + 0 boost 1
c [treelook-6] used 9136148 steps
c [treelook-6] 56181 literals remain 75%
c [treelook-6] 8172 variables remain to probed next time 22%
c [decomp-43] removed 2 variables
c [treelook-6] removed 7 variables, found 48520 hbrs
c [unhide-17] limit 2278266 with penalty 3 = 0 + 3
c [unhide-17-25] 0 units, 7 failed, 80908 tauts, 0 hbrs, 808925 literals
c [transred-13] limit 2000000 with penalty 0 = 0 + 0
c [transred-13] removed 258 transitive binary clauses
c [elim-13] scheduling all variables this time
c [elim-13] scheduled 37240 variables 100%
c [elim-13] almost no limit of 100000000000 steps
c [elim-13] rescheduling of touched variables disabled
c [elim-13-1] eliminated 243 variables 1% in round 1 in 24499435 steps
c [elim-13-1] backward subsumption/strengthening limit 24499400
c [elim-13-1-1] backward checking 1139 touched variables 3%
c [elim-13-1-1] fully completed backward checking in 1 rounds
c [elim-13-1] subsumed 0 and strengthened 4 clauses in 288834 steps
c [elim-13-1] rescheduled 7 variables 0% by backward subsumption
c [elim-13-2] eliminated 2 variables 0% in round 2 in 6988 steps
c [elim-13-2] backward subsumption/strengthening limit 6900
c [elim-13-2-1] backward checking 14 touched variables 0%
c [elim-13-2-1] incomplete backward checking 3 remain 21%
c [elim-13-2] subsumed 2 and strengthened 4 clauses in 6922 steps
c [elim-13-2] rescheduled 7 variables 0% by backward subsumption
c [elim-13-3] eliminated 2 variables 0% in round 3 in 6313 steps
c [elim-13-3] backward subsumption/strengthening limit 6300
c [elim-13-3-1] backward checking 16 touched variables 0%
c [elim-13-3-1] incomplete backward checking 7 remain 44%
c [elim-13-3] subsumed 3 and strengthened 4 clauses in 6354 steps
c [elim-13] incomplete 7 not tried 0% in round 3
c [elim-13] transition to [ all 1 rem 1 ] state
c [elim-13] eliminated 247 = 1% variables out of 37240 scheduled
c [elim-13] 247 < 1/100 * 37240 = 372 considered unsuccessful
c [bca-13] limit of 10000000 steps and 521071 added (scaled 2)
c [bca-13] 57914 out of 73988 literals actually usable 78%
c [bca-13] added 16 blocked clauses in 171133 steps
c [sweep-13] limit 27339196 penalty 0 = 0 + 0
c [sweep-13-1] 2458 pos 10.5% + 20909 neg 89.5% = 23367 sched 63.2% ret 13626
c [sweep-13-1] 27359847 steps 613 queries 345.90 avg class size
c [sweep-13-1] 9971 decisions 596 SAT calls 173.35 avg env size
c [sweep-13-1] 18002 variables remain 49% (18986 retained 51%)
c [decomp-44] removed 25 variables
c [sweep-13-1] removed 25 vars (0 failed, 17 eqs, 66 impls)
c [sweep-13] 25 < 1/1000 * 36993 = 36 considered unsuccessful
c [sweep-13] removed 25 vars in TOTAL (1 rounds, 612 queries)
c [phase-count-17] 259550 negative 99.8% of 259964 except 414 0.2%
c [phase-count-17] 193554 positive 74.5% of 259964 except 66410 25.5%
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 7852 enqueued variables after 294715 conflicts
c [score-dist-17] active 29116 (79%), one 0 (0%), zero 7852 (21%)
c [score-dist-17] max exp 519, different 19 (4%)
c [score-dist-17] median active exp 511, avg 510.4
c [simplification-17] removed 284 variables 0.8% (36968 remain 19%)
c [simplification-17] removed 2342 irredundant clauses 0.9% (259964 remain 26%)
c [simplification-17] maximum reduction of 1% = max (1%, 1%)
c [simplification-17] geometric conflict interval increment 38332 = 76664 / 2
c [simplification-17] new conflict interval 114996
c [simplification-17] penalized conflict interval 114996 = 1 * 114996
c [simplification-17] hard conflict limit 467209 (soft 409711 + delta 57498)
c [simplification-17] new conflict limit 409711 (hard 467209)
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 -  620.0   36968   259964    321467   26021   4432 834876  580   625   81  93%    575   11  614  534  115%
c -  763.8   36968   259964    422012   26909   4471 834931  328   361   76  91%    927 -138  325  434   75%
c 
c [simplification-18] limit 409711 conflicts (hard 467209) hit after 467210 conflicts
c [ternres-13] limit 153934583 with penalty 0 = 0 + 0
c [ternres-13] all 36968 free variables schedulable
c [ternres-13] 136 ternary resolvents (0 bin, 136 trn)
c [ternres-13] fully completed ternary resolution
c [decomp-45] removed 2 variables
c [basicprobe-6] limit 400000000 penalty 0 = 0 + 0
c [basicprobe-6-0] 8068 sched 22%, 206 failed, 1 lifted, 169942 hbrs
c [decomp-46] removed 277 variables
c [basicprobe-6-1] 7450 probes remain 20% after last round
c [basicprobe-6-1] 252 units = 251 failed (100%) + 1 lifted (0%)
c [basicprobe-6-1] removed 494 variables, found 201008 hbrs
c [bate-4] eliminated 205 asymmetric tautologies during probing
c [unhide-18] limit 5000000 with penalty 2 = 0 + 2
c [unhide-18-27] 0 units, 5 failed, 75426 tauts, 0 hbrs, 206575 literals
c [transred-14] limit 2000000 with penalty 0 = 0 + 0
c [transred-14] removed 226 transitive binary clauses
c [bca-14] limit of 10000000 steps and 509315 added (scaled 2)
c [bca-14] 56641 out of 72942 literals actually usable 78%
c [bca-14] added 13 blocked clauses in 155415 steps
c [phase-count-18] 253737 negative 99.8% of 254151 except 414 0.2%
c [phase-count-18] 189635 positive 74.6% of 254151 except 64516 25.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 7497 enqueued variables after 467210 conflicts
c [score-dist-18] active 28973 (79%), one 0 (0%), zero 7497 (21%)
c [score-dist-18] max exp 520, different 20 (4%)
c [score-dist-18] median active exp 512, avg 511.0
c [simplification-18] removed 498 variables 1.3% (36470 remain 19%)
c [simplification-18] removed 5813 irredundant clauses 2.2% (254151 remain 25%)
c [simplification-18] maximum reduction of 2% = max (1%, 2%)
c [simplification-18] geometric conflict interval increment 38332 = 114996 / 3
c [simplification-18] new conflict interval 153328
c [simplification-18] penalized conflict interval 153328 = 1 * 153328
c [simplification-18] hard conflict limit 697202 (soft 620538 + delta 76664)
c [simplification-18] new conflict limit 620538 (hard 697202)
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 -  932.0   36470   254151    536502   27264   4523 925470  333   376   73  88%   1007  -51  341  365   93%
c
c CAUGHT SIGNAL 15 SIGTERM
c
c s UNKNOWN
c bate: 2940 basic ate = 2679 trn 91% + 261 lrg 9% in 4 updates
c bcas: 14 count, 1040 added (890 skipped), 3406350 steps
c bkwd: tried 285284 clauses, 570492 lits, 2.00 lits/clause
c bkwd: checked 7986680 occs, 28.00 occs/clause, 14.00 occs/lit
c bkwd: subsumed 7 binary, 21 ternary, 15 large
c bkwd: strengthened 0 binary, 0 ternary (0% self), 172 large (0% self)
c blkd: 5 bces, 10646 removed, 6609499 resolutions, 18481810 steps
c blkd: 13233 blocking literals 3%, 3 pure
c bump: 588869 bumped seen, 834901999 lits 1417.8 on average
c card: 5 count, 0 units, 0 am1, 273419313 steps
c card: 0 rescheduled, 0 eliminated, 0 resolved, 74610 subsumed
c card: 17946 at-most-one constraints found, average size 4.79
c card: 17946 at-most-one constraints used 100%, average size 4.79
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, 60317 eliminated, 59975 ate 99%, 342 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: 3450190 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 129 gcs, 0 rescored clauses, 0 rescored vars
c dcps: 46 decompositions, 8501 equivalent 4%
c deco: 404596 decision-only clauses 69%, 54% reduction
c decs: 6543682 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 13 elims, 82041 eliminated 41%, 243 pure 0%
c elms: 31 rounds, 2.4 rounds/bve
c elms: 63497 small 77%, 18298 large 22%
c elms: 158885 tried small, 63497 succeeded 40%, 95388 failed 60%
c elms: 29228 subsumed, 55535 strengthened, 819 blocked
c elms: 17285184 copies, 16901362 resolutions, 3963359 ipos
c elms: 4503247 subchks, 3471572 strchks
c gaus: 4 extractions, 167 extracted, 2.6 size, 3 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 11882360 steps, 5941180 extr 50%, 1045 elim 0%
c glue: 463.4 orig avg, 463.4 real avg, 11.8 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 2030164 = 360896 simple 18% + 1644832 trn 81% + 24436 lrg 1%, 3568 sub 0%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 588869 clauses, 533.8 length
c lrnd: 314353300 lits = 564533509 orig - 250180209 removed 44%
c lrnd: 217591 uips 37%, 332424 flips 56%
c mins: 67351 mins 14%, 1009 bin 0%, 1950 size 0%
c mins: 19570570 poisoned searches, 5551129 hits, 28% hit rate
c mins: 27028502 used twice searches, 5539809 hits, 20% hit rate
c move: moved 26692, 17459 bin 65%, 9233 trn 35%
c otfs: 6176 driving 35%, 11561 restarting 65%
c otfs: str 17737, 17592 red 99%, 145 irr 1%
c otfs: str 17737, 0 bin 0%, 90 trn 1%, 17647 lrg 99%
c otfs: sub 34, 34 red 100%, 0 irr 0%
c otfs: sub 34, 0 bin 0%, 0 trn 0%, 34 lrg 100%
c phas: 18 computed, 95959 set, 28 pos (0%), 95931 neg (100%)
c prbs: 6 basic, 68260 probed, 2193 failed, 73 lifted
c prbs: 6 simple, 710658 probed, 867 failed, 260 eqs
c prbs: 6 treelook, 361 probed, 17 failed, 0 lifted
c prom: 3257 locked 0% out of 806518 tried
c prps: 2527361417 props, 372 props/dec
c prps: 96% srch, 4% simp, 0% lkhd
c quat: 10 count, 31 quat, 5 self1, 0 self2, 204 dup
c queu: 18 sorted, 6543682 next (39379 steps 0.01)
c queu: 835596901 enq (1828658302 steps 2.19), 834901999 deq 100%
c redc: 926 clauses 18%, 5100 tried 1%, 39 sat 1%
c redc: 1829 lits 4%, 42953 tried 0%, 39 sat 0%
c redc: 68 times jump level reduced, 113.4 levels on average
c reds: 4 count, 147891.5 conflicts per reduce
c reds: 0 memlim 0%, 4 arith 100%
c reds: 103005 collected 89%, 12735 retired 11%
c rmbd: 54987 removed, 24736 red 45%
c rsts: 5409 restarts 63%, 3165 skipped 37%
c rsts: 3165 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: 588869 count (891291 tried 1.5), 400030 sub out of 585817 (68.3%)
c swps: 13 count, 14 rounds, 9417 queries (672.6/round)
c swps: 8233 sat calls, 124 unsat (0.4% success rate)
c swps: 83304 decisions 10.1, 3480 conflicts 0.4
c swps; 390.2 avg class size, 109.8 avg environment size
c swps: 3 failed, 1833 impls, 1251 equivs
c swp0: 3135 type 0 queries, 1834 unsat (58.5%), 2660 sat (84.8%)
c swp1: 6282 type 1 queries, 3695 unsat (58.8%), 5506 sat (87.6%)
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: 14265595 calls to obtain time
c tops: 72984 fixed 36%, 165 its, 3585.25 confs/it
c trds: 14 transitive reductions, 2849 removed, 23 failed
c trds: 13868 nodes, 48847 edges, 28025805 steps
c trim: 3895871 words, 14.9 MB
c trnr: 13 count, 1 bin, 2838 trn, 140819893 steps
c unhd: 18 count, 27 rounds, 74274604 steps
c unhd: 586 non-trivial sccs of average size 2.1
c unhd: 57 units, 57 bin, 0 trn, 0 lrg
c unhd: 6654 failed, 6632 stamp, 0 lits, 9 bin, 7 trn, 0 lrg
c unhd: 614165 tauts, 16000 bin 3%, 10312 trn 2%, 358 lrg 0%
c unhd: 614165 tauts, 587495 stamp 96%, 567957 red 92%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 4785994 str, 57 bin 0%, 2059 trn 0%, 4783878 lrg 100%, 4772170 red 100%
c vars: 36470 remaining 18% and 163526 removed 82% out of 199996
c vars: 72984 fixed 36%, 82041 eliminated 41%, 8501 equivalent 4%
c vsts: 20686042250 visits, 95% srch, 5% simp, 0% lkhd
c vsts: 8.1 search visits per propagation, 33249.0 per conflict
c wchs: 1647031510 pushed, 46650073 enlarged, 193 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all         585848        103005         12735      46738310      12619459        302244
c 
c  0 0          4703   1         4   0         0   0  12887039  28   1933756  15     14783   5     0.3
c  1 5           846   0         7   0       128   1   2455195   5    412193   3      5562   2     0.1
c  2 6          1922   0        37   0        92   1   4168653   9    758205   6     10632   4     0.3
c  3 9          2275   0       109   0        57   0   3122718   7    685748   5     12655   4     0.5
c  4 14         2762   0       183   0       100   1   2743420   6    674956   5     15495   5     0.7
c  5 21         3294   1       372   0       100   1   3005485   6<   801631   6     13044   4     0.8
c  6 30         3584   1       459   0       155   1   2599257   6    768156   6     17587   6     1.1
c  7 41         4061   1       498   0       188   1   2224895   5    669382   5<    13179   4     1.6
c  8 54         4446   1       823   1       175   1   1933200   4    697308   6     14318   5     2.0
c  9 69         4984   1      1260   1       221   2   1698001   4    679336   5     11764   4<    2.2
c 10 86        11659   2      4344   4       472   4   3044302   7   1116384   9     26538   9     5.4
c 11 126       30574   5     18804  18      1068   8   3309917   7   1422668  11     46530  15    16.5
c 12 230      288230  49<    58601  57<     5692  45<  2909246   6   1626920  13     77836  26   105.7
c 13 534      222508  38     17504  17      4287  34    636982   1    372816   3     22321   7   116.0
c 
c avg                 11.9          11.7          11.6           4.7           6.6           8.6
c std                  1.9           1.2           2.2           4.2           4.3           3.9
c 
c  174.602  17% bump
c   47.625   5% cce
c   47.494   5% probe
c   46.104   5% unhide
c   22.564   2% sweep
c   15.618   2% elim
c    3.912   0% decide
c 
c   10.595 < 1% rest (below)
c 
c    3.539   0% bca
c    2.640   0% block
c    1.627   0% transred
c    1.017   0% gauss
c    0.961   0% ternres
c    0.442   0% quatres
c    0.370   0% card
c    0.000   0% locs
c    0.000   0% queuesort
c    0.000   0% rescore
c ==================================
c    3.878   0% preprocessing     2%
c  199.057  20% inprocessing     98%
c ==================================
c  202.935  20% simplifying
c  796.515  80% search
c ==================================
c  999.450 100% all
c 
c        591566 conflicts,         591.9 confs/sec
c           908 ternaries,         651.5 confs/ternary
c           901 binaries,          656.6 confs/binary
c           165 iterations,       3585.2 confs/iteration
c 
c             4 reductions,          0.0 redus/sec, 147891.5 confs/reduction
c          5409 restarts,            5.4 rests/sec,    109.4 confs/restart
c       6543682 decisions,        6547.3 decis/sec,     11.1 decis/conflict
c    2527361417 propagations,  2528751.1 props/sec,    386.2 props/decision
c 
c 999.5 seconds, 383.9 MB
c
c CAUGHT SIGNAL 15 SIGTERM
c
c launch: done
